Theorem zmul11 ≪ | index | src | ≫ 

theorem zmul11 (a: nat): $ b0 1 *Z a = a $;
StepHypRefExpression
1 eqtr3 
(1 -ZN 0) *Z (zfst a -ZN zsnd a) = b0 1 *Z a -> (1 -ZN 0) *Z (zfst a -ZN zsnd a) = a -> b0 1 *Z a = a
2 zmuleq 
1 -ZN 0 = b0 1 -> zfst a -ZN zsnd a = a -> (1 -ZN 0) *Z (zfst a -ZN zsnd a) = b0 1 *Z a
3 znsub02 
1 -ZN 0 = b0 1
4 2, 3 ax_mp 
zfst a -ZN zsnd a = a -> (1 -ZN 0) *Z (zfst a -ZN zsnd a) = b0 1 *Z a
5 zfstsnd 
zfst a -ZN zsnd a = a
6 4, 5 ax_mp 
(1 -ZN 0) *Z (zfst a -ZN zsnd a) = b0 1 *Z a
7 1, 6 ax_mp 
(1 -ZN 0) *Z (zfst a -ZN zsnd a) = a -> b0 1 *Z a = a
8 eqtr 
(1 -ZN 0) *Z (zfst a -ZN zsnd a) = 1 * zfst a + 0 * zsnd a -ZN (1 * zsnd a + zfst a * 0) ->
  1 * zfst a + 0 * zsnd a -ZN (1 * zsnd a + zfst a * 0) = a ->
  (1 -ZN 0) *Z (zfst a -ZN zsnd a) = a
9 zmulzn 
(1 -ZN 0) *Z (zfst a -ZN zsnd a) = 1 * zfst a + 0 * zsnd a -ZN (1 * zsnd a + zfst a * 0)
10 8, 9 ax_mp 
1 * zfst a + 0 * zsnd a -ZN (1 * zsnd a + zfst a * 0) = a -> (1 -ZN 0) *Z (zfst a -ZN zsnd a) = a
11 eqtr 
1 * zfst a + 0 * zsnd a -ZN (1 * zsnd a + zfst a * 0) = zfst a -ZN zsnd a -> zfst a -ZN zsnd a = a -> 1 * zfst a + 0 * zsnd a -ZN (1 * zsnd a + zfst a * 0) = a
12 znsubeq 
1 * zfst a + 0 * zsnd a = zfst a -> 1 * zsnd a + zfst a * 0 = zsnd a -> 1 * zfst a + 0 * zsnd a -ZN (1 * zsnd a + zfst a * 0) = zfst a -ZN zsnd a
13 eqtr 
1 * zfst a + 0 * zsnd a = zfst a + 0 -> zfst a + 0 = zfst a -> 1 * zfst a + 0 * zsnd a = zfst a
14 addeq 
1 * zfst a = zfst a -> 0 * zsnd a = 0 -> 1 * zfst a + 0 * zsnd a = zfst a + 0
15 mul11 
1 * zfst a = zfst a
16 14, 15 ax_mp 
0 * zsnd a = 0 -> 1 * zfst a + 0 * zsnd a = zfst a + 0
17 mul01 
0 * zsnd a = 0
18 16, 17 ax_mp 
1 * zfst a + 0 * zsnd a = zfst a + 0
19 13, 18 ax_mp 
zfst a + 0 = zfst a -> 1 * zfst a + 0 * zsnd a = zfst a
20 add0 
zfst a + 0 = zfst a
21 19, 20 ax_mp 
1 * zfst a + 0 * zsnd a = zfst a
22 12, 21 ax_mp 
1 * zsnd a + zfst a * 0 = zsnd a -> 1 * zfst a + 0 * zsnd a -ZN (1 * zsnd a + zfst a * 0) = zfst a -ZN zsnd a
23 eqtr 
1 * zsnd a + zfst a * 0 = zsnd a + 0 -> zsnd a + 0 = zsnd a -> 1 * zsnd a + zfst a * 0 = zsnd a
24 addeq 
1 * zsnd a = zsnd a -> zfst a * 0 = 0 -> 1 * zsnd a + zfst a * 0 = zsnd a + 0
25 mul11 
1 * zsnd a = zsnd a
26 24, 25 ax_mp 
zfst a * 0 = 0 -> 1 * zsnd a + zfst a * 0 = zsnd a + 0
27 mul02 
zfst a * 0 = 0
28 26, 27 ax_mp 
1 * zsnd a + zfst a * 0 = zsnd a + 0
29 23, 28 ax_mp 
zsnd a + 0 = zsnd a -> 1 * zsnd a + zfst a * 0 = zsnd a
30 add0 
zsnd a + 0 = zsnd a
31 29, 30 ax_mp 
1 * zsnd a + zfst a * 0 = zsnd a
32 22, 31 ax_mp 
1 * zfst a + 0 * zsnd a -ZN (1 * zsnd a + zfst a * 0) = zfst a -ZN zsnd a
33 11, 32 ax_mp 
zfst a -ZN zsnd a = a -> 1 * zfst a + 0 * zsnd a -ZN (1 * zsnd a + zfst a * 0) = a
34 33, 5 ax_mp 
1 * zfst a + 0 * zsnd a -ZN (1 * zsnd a + zfst a * 0) = a
35 10, 34 ax_mp 
(1 -ZN 0) *Z (zfst a -ZN zsnd a) = a
36 7, 35 ax_mp 
b0 1 *Z a = 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)