Theorem zfstsubsnd ≪ | index | src | ≫

theorem zfstsubsnd (n: nat): $ zfst n - zsnd n = zfst n $;


(zfst n = 0 -> zfst n - zsnd n = zfst n) -> (zsnd n = 0 -> zfst n - zsnd n = zfst n) -> zfst n = 0 \/ zsnd n = 0 -> zfst n - zsnd n = zfst n
zfst n = 0 -> zfst n - zsnd n = 0 - zsnd n
0 - zsnd n = 0
zfst n = 0 -> zfst n = 0
zfst n = 0 -> zfst n = 0 - zsnd n
zfst n = 0 -> zfst n - zsnd n = zfst n
(zsnd n = 0 -> zfst n - zsnd n = zfst n) -> zfst n = 0 \/ zsnd n = 0 -> zfst n - zsnd n = zfst n
zfst n - 0 = zfst n
zsnd n = 0 -> zfst n - zsnd n = zfst n - 0
zsnd n = 0 -> zfst n - zsnd n = zfst n
zfst n = 0 \/ zsnd n = 0 -> zfst n - zsnd n = zfst n
zfst n = 0 \/ zsnd n = 0
zfst n - zsnd n = zfst n

Step	Hyp	Ref	Expression
1		eor	(zfst n = 0 -> zfst n - zsnd n = zfst n) -> (zsnd n = 0 -> zfst n - zsnd n = zfst n) -> zfst n = 0 \/ zsnd n = 0 -> zfst n - zsnd n = zfst n
2		subeq1	zfst n = 0 -> zfst n - zsnd n = 0 - zsnd n
3		sub01	0 - zsnd n = 0
4		id	zfst n = 0 -> zfst n = 0
5	3, 4	syl6eqr	zfst n = 0 -> zfst n = 0 - zsnd n
6	2, 5	eqtr4d	zfst n = 0 -> zfst n - zsnd n = zfst n
7	1, 6	ax_mp	(zsnd n = 0 -> zfst n - zsnd n = zfst n) -> zfst n = 0 \/ zsnd n = 0 -> zfst n - zsnd n = zfst n
8		sub02	zfst n - 0 = zfst n
9		subeq2	zsnd n = 0 -> zfst n - zsnd n = zfst n - 0
10	8, 9	syl6eq	zsnd n = 0 -> zfst n - zsnd n = zfst n
11	7, 10	ax_mp	zfst n = 0 \/ zsnd n = 0 -> zfst n - zsnd n = zfst n
12		zfstsnd0	zfst n = 0 \/ zsnd n = 0
13	11, 12	ax_mp	zfst n - zsnd n = zfst n

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)