Theorem zmulcom ≪ | index | src | ≫

theorem zmulcom (a b: nat): $ a *Z b = b *Z a $;


zfst a * zfst b + zsnd a * zsnd b = zfst b * zfst a + zsnd b * zsnd a ->
  zfst a * zsnd b + zsnd a * zfst b = zfst b * zsnd a + zsnd b * zfst a ->
  zfst a * zfst b + zsnd a * zsnd b -ZN (zfst a * zsnd b + zsnd a * zfst b) = zfst b * zfst a + zsnd b * zsnd a -ZN (zfst b * zsnd a + zsnd b * zfst a)
zfst a * zfst b + zsnd a * zsnd b = zfst b * zfst a + zsnd b * zsnd a ->
  zfst a * zsnd b + zsnd a * zfst b = zfst b * zsnd a + zsnd b * zfst a ->
  a *Z b = b *Z a
zfst a * zfst b = zfst b * zfst a -> zsnd a * zsnd b = zsnd b * zsnd a -> zfst a * zfst b + zsnd a * zsnd b = zfst b * zfst a + zsnd b * zsnd a
zfst a * zfst b = zfst b * zfst a
zsnd a * zsnd b = zsnd b * zsnd a -> zfst a * zfst b + zsnd a * zsnd b = zfst b * zfst a + zsnd b * zsnd a
zsnd a * zsnd b = zsnd b * zsnd a
zfst a * zfst b + zsnd a * zsnd b = zfst b * zfst a + zsnd b * zsnd a
zfst a * zsnd b + zsnd a * zfst b = zfst b * zsnd a + zsnd b * zfst a -> a *Z b = b *Z a
zfst a * zsnd b + zsnd a * zfst b = zsnd a * zfst b + zfst a * zsnd b ->
  zsnd a * zfst b + zfst a * zsnd b = zfst b * zsnd a + zsnd b * zfst a ->
  zfst a * zsnd b + zsnd a * zfst b = zfst b * zsnd a + zsnd b * zfst a
zfst a * zsnd b + zsnd a * zfst b = zsnd a * zfst b + zfst a * zsnd b
zsnd a * zfst b + zfst a * zsnd b = zfst b * zsnd a + zsnd b * zfst a -> zfst a * zsnd b + zsnd a * zfst b = zfst b * zsnd a + zsnd b * zfst a
zsnd a * zfst b = zfst b * zsnd a -> zfst a * zsnd b = zsnd b * zfst a -> zsnd a * zfst b + zfst a * zsnd b = zfst b * zsnd a + zsnd b * zfst a
zsnd a * zfst b = zfst b * zsnd a
zfst a * zsnd b = zsnd b * zfst a -> zsnd a * zfst b + zfst a * zsnd b = zfst b * zsnd a + zsnd b * zfst a
zfst a * zsnd b = zsnd b * zfst a
zsnd a * zfst b + zfst a * zsnd b = zfst b * zsnd a + zsnd b * zfst a
zfst a * zsnd b + zsnd a * zfst b = zfst b * zsnd a + zsnd b * zfst a
a *Z b = b *Z a

Step	Hyp	Ref	Expression
1		znsubeq	zfst a * zfst b + zsnd a * zsnd b = zfst b * zfst a + zsnd b * zsnd a -> zfst a * zsnd b + zsnd a * zfst b = zfst b * zsnd a + zsnd b * zfst a -> zfst a * zfst b + zsnd a * zsnd b -ZN (zfst a * zsnd b + zsnd a * zfst b) = zfst b * zfst a + zsnd b * zsnd a -ZN (zfst b * zsnd a + zsnd b * zfst a)
2	1	conv zmul	zfst a * zfst b + zsnd a * zsnd b = zfst b * zfst a + zsnd b * zsnd a -> zfst a * zsnd b + zsnd a * zfst b = zfst b * zsnd a + zsnd b * zfst a -> a Z b = b Z a
3		addeq	zfst a * zfst b = zfst b * zfst a -> zsnd a * zsnd b = zsnd b * zsnd a -> zfst a * zfst b + zsnd a * zsnd b = zfst b * zfst a + zsnd b * zsnd a
4		mulcom	zfst a * zfst b = zfst b * zfst a
5	3, 4	ax_mp	zsnd a * zsnd b = zsnd b * zsnd a -> zfst a * zfst b + zsnd a * zsnd b = zfst b * zfst a + zsnd b * zsnd a
6		mulcom	zsnd a * zsnd b = zsnd b * zsnd a
7	5, 6	ax_mp	zfst a * zfst b + zsnd a * zsnd b = zfst b * zfst a + zsnd b * zsnd a
8	2, 7	ax_mp	zfst a * zsnd b + zsnd a * zfst b = zfst b * zsnd a + zsnd b * zfst a -> a Z b = b Z a
9		eqtr	zfst a * zsnd b + zsnd a * zfst b = zsnd a * zfst b + zfst a * zsnd b -> zsnd a * zfst b + zfst a * zsnd b = zfst b * zsnd a + zsnd b * zfst a -> zfst a * zsnd b + zsnd a * zfst b = zfst b * zsnd a + zsnd b * zfst a
10		addcom	zfst a * zsnd b + zsnd a * zfst b = zsnd a * zfst b + zfst a * zsnd b
11	9, 10	ax_mp	zsnd a * zfst b + zfst a * zsnd b = zfst b * zsnd a + zsnd b * zfst a -> zfst a * zsnd b + zsnd a * zfst b = zfst b * zsnd a + zsnd b * zfst a
12		addeq	zsnd a * zfst b = zfst b * zsnd a -> zfst a * zsnd b = zsnd b * zfst a -> zsnd a * zfst b + zfst a * zsnd b = zfst b * zsnd a + zsnd b * zfst a
13		mulcom	zsnd a * zfst b = zfst b * zsnd a
14	12, 13	ax_mp	zfst a * zsnd b = zsnd b * zfst a -> zsnd a * zfst b + zfst a * zsnd b = zfst b * zsnd a + zsnd b * zfst a
15		mulcom	zfst a * zsnd b = zsnd b * zfst a
16	14, 15	ax_mp	zsnd a * zfst b + zfst a * zsnd b = zfst b * zsnd a + zsnd b * zfst a
17	11, 16	ax_mp	zfst a * zsnd b + zsnd a * zfst b = zfst b * zsnd a + zsnd b * zfst a
18	8, 17	ax_mp	a Z b = b Z 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 (peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)