Theorem zadd02 ≪ | index | src | ≫

theorem zadd02 (a: nat): $ a +Z 0 = a $;


a +Z 0 = zfst a -ZN zsnd a -> zfst a -ZN zsnd a = a -> a +Z 0 = a
zfst a + zfst 0 = zfst a -> zsnd a + zsnd 0 = zsnd a -> zfst a + zfst 0 -ZN (zsnd a + zsnd 0) = zfst a -ZN zsnd a
zfst a + zfst 0 = zfst a -> zsnd a + zsnd 0 = zsnd a -> a +Z 0 = zfst a -ZN zsnd a
zfst a + zfst 0 = zfst a + 0 -> zfst a + 0 = zfst a -> zfst a + zfst 0 = zfst a
zfst 0 = 0 -> zfst a + zfst 0 = zfst a + 0
zfst 0 = 0
zfst a + zfst 0 = zfst a + 0
zfst a + 0 = zfst a -> zfst a + zfst 0 = zfst a
zfst a + 0 = zfst a
zfst a + zfst 0 = zfst a
zsnd a + zsnd 0 = zsnd a -> a +Z 0 = zfst a -ZN zsnd a
zsnd a + zsnd 0 = zsnd a + 0 -> zsnd a + 0 = zsnd a -> zsnd a + zsnd 0 = zsnd a
zsnd 0 = 0 -> zsnd a + zsnd 0 = zsnd a + 0
zsnd 0 = 0
zsnd a + zsnd 0 = zsnd a + 0
zsnd a + 0 = zsnd a -> zsnd a + zsnd 0 = zsnd a
zsnd a + 0 = zsnd a
zsnd a + zsnd 0 = zsnd a
a +Z 0 = zfst a -ZN zsnd a
zfst a -ZN zsnd a = a -> a +Z 0 = a
zfst a -ZN zsnd a = a
a +Z 0 = a

Step	Hyp	Ref	Expression
1		eqtr	a +Z 0 = zfst a -ZN zsnd a -> zfst a -ZN zsnd a = a -> a +Z 0 = a
2		znsubeq	zfst a + zfst 0 = zfst a -> zsnd a + zsnd 0 = zsnd a -> zfst a + zfst 0 -ZN (zsnd a + zsnd 0) = zfst a -ZN zsnd a
3	2	conv zadd	zfst a + zfst 0 = zfst a -> zsnd a + zsnd 0 = zsnd a -> a +Z 0 = zfst a -ZN zsnd a
4		eqtr	zfst a + zfst 0 = zfst a + 0 -> zfst a + 0 = zfst a -> zfst a + zfst 0 = zfst a
5		addeq2	zfst 0 = 0 -> zfst a + zfst 0 = zfst a + 0
6		zfst0	zfst 0 = 0
7	5, 6	ax_mp	zfst a + zfst 0 = zfst a + 0
8	4, 7	ax_mp	zfst a + 0 = zfst a -> zfst a + zfst 0 = zfst a
9		add0	zfst a + 0 = zfst a
10	8, 9	ax_mp	zfst a + zfst 0 = zfst a
11	3, 10	ax_mp	zsnd a + zsnd 0 = zsnd a -> a +Z 0 = zfst a -ZN zsnd a
12		eqtr	zsnd a + zsnd 0 = zsnd a + 0 -> zsnd a + 0 = zsnd a -> zsnd a + zsnd 0 = zsnd a
13		addeq2	zsnd 0 = 0 -> zsnd a + zsnd 0 = zsnd a + 0
14		zsnd0	zsnd 0 = 0
15	13, 14	ax_mp	zsnd a + zsnd 0 = zsnd a + 0
16	12, 15	ax_mp	zsnd a + 0 = zsnd a -> zsnd a + zsnd 0 = zsnd a
17		add0	zsnd a + 0 = zsnd a
18	16, 17	ax_mp	zsnd a + zsnd 0 = zsnd a
19	11, 18	ax_mp	a +Z 0 = zfst a -ZN zsnd a
20	1, 19	ax_mp	zfst a -ZN zsnd a = a -> a +Z 0 = a
21		zfstsnd	zfst a -ZN zsnd a = a
22	20, 21	ax_mp	a +Z 0 = a

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)