Theorem zmulb0 ≪ | index | src | ≫ 

theorem zmulb0 (a b: nat): $ b0 a *Z b0 b = b0 (a * b) $;
StepHypRefExpression
1 eqtr3 
(a -ZN 0) *Z (b -ZN 0) = b0 a *Z b0 b -> (a -ZN 0) *Z (b -ZN 0) = b0 (a * b) -> b0 a *Z b0 b = b0 (a * b)
2 zmuleq 
a -ZN 0 = b0 a -> b -ZN 0 = b0 b -> (a -ZN 0) *Z (b -ZN 0) = b0 a *Z b0 b
3 znsub02 
a -ZN 0 = b0 a
4 2, 3 ax_mp 
b -ZN 0 = b0 b -> (a -ZN 0) *Z (b -ZN 0) = b0 a *Z b0 b
5 znsub02 
b -ZN 0 = b0 b
6 4, 5 ax_mp 
(a -ZN 0) *Z (b -ZN 0) = b0 a *Z b0 b
7 1, 6 ax_mp 
(a -ZN 0) *Z (b -ZN 0) = b0 (a * b) -> b0 a *Z b0 b = b0 (a * b)
8 eqtr4 
(a -ZN 0) *Z (b -ZN 0) = a * b + 0 * 0 -ZN (a * 0 + b * 0) -> b0 (a * b) = a * b + 0 * 0 -ZN (a * 0 + b * 0) -> (a -ZN 0) *Z (b -ZN 0) = b0 (a * b)
9 zmulzn 
(a -ZN 0) *Z (b -ZN 0) = a * b + 0 * 0 -ZN (a * 0 + b * 0)
10 8, 9 ax_mp 
b0 (a * b) = a * b + 0 * 0 -ZN (a * 0 + b * 0) -> (a -ZN 0) *Z (b -ZN 0) = b0 (a * b)
11 eqtr3 
a * b -ZN 0 = b0 (a * b) -> a * b -ZN 0 = a * b + 0 * 0 -ZN (a * 0 + b * 0) -> b0 (a * b) = a * b + 0 * 0 -ZN (a * 0 + b * 0)
12 znsub02 
a * b -ZN 0 = b0 (a * b)
13 11, 12 ax_mp 
a * b -ZN 0 = a * b + 0 * 0 -ZN (a * 0 + b * 0) -> b0 (a * b) = a * b + 0 * 0 -ZN (a * 0 + b * 0)
14 znsubeq 
a * b = a * b + 0 * 0 -> 0 = a * 0 + b * 0 -> a * b -ZN 0 = a * b + 0 * 0 -ZN (a * 0 + b * 0)
15 eqtr2 
a * b + 0 * 0 = a * b + 0 -> a * b + 0 = a * b -> a * b = a * b + 0 * 0
16 addeq2 
0 * 0 = 0 -> a * b + 0 * 0 = a * b + 0
17 mul0 
0 * 0 = 0
18 16, 17 ax_mp 
a * b + 0 * 0 = a * b + 0
19 15, 18 ax_mp 
a * b + 0 = a * b -> a * b = a * b + 0 * 0
20 add0 
a * b + 0 = a * b
21 19, 20 ax_mp 
a * b = a * b + 0 * 0
22 14, 21 ax_mp 
0 = a * 0 + b * 0 -> a * b -ZN 0 = a * b + 0 * 0 -ZN (a * 0 + b * 0)
23 eqtr2 
a * 0 + b * 0 = 0 + 0 -> 0 + 0 = 0 -> 0 = a * 0 + b * 0
24 addeq 
a * 0 = 0 -> b * 0 = 0 -> a * 0 + b * 0 = 0 + 0
25 mul0 
a * 0 = 0
26 24, 25 ax_mp 
b * 0 = 0 -> a * 0 + b * 0 = 0 + 0
27 mul0 
b * 0 = 0
28 26, 27 ax_mp 
a * 0 + b * 0 = 0 + 0
29 23, 28 ax_mp 
0 + 0 = 0 -> 0 = a * 0 + b * 0
30 add0 
0 + 0 = 0
31 29, 30 ax_mp 
0 = a * 0 + b * 0
32 22, 31 ax_mp 
a * b -ZN 0 = a * b + 0 * 0 -ZN (a * 0 + b * 0)
33 13, 32 ax_mp 
b0 (a * b) = a * b + 0 * 0 -ZN (a * 0 + b * 0)
34 10, 33 ax_mp 
(a -ZN 0) *Z (b -ZN 0) = b0 (a * b)
35 7, 34 ax_mp 
b0 a *Z b0 b = b0 (a * b)

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)