Theorem mulass ≪ | index | src | ≫ 

theorem mulass (a b c: nat): $ a * b * c = a * (b * c) $;
StepHypRefExpression
1 muleq2 
x = c -> a * b * x = a * b * c
2 muleq2 
x = c -> b * x = b * c
3 2 muleq2d 
x = c -> a * (b * x) = a * (b * c)
4 1, 3 eqeqd 
x = c -> (a * b * x = a * (b * x) <-> a * b * c = a * (b * c))
5 muleq2 
x = 0 -> a * b * x = a * b * 0
6 muleq2 
x = 0 -> b * x = b * 0
7 6 muleq2d 
x = 0 -> a * (b * x) = a * (b * 0)
8 5, 7 eqeqd 
x = 0 -> (a * b * x = a * (b * x) <-> a * b * 0 = a * (b * 0))
9 muleq2 
x = y -> a * b * x = a * b * y
10 muleq2 
x = y -> b * x = b * y
11 10 muleq2d 
x = y -> a * (b * x) = a * (b * y)
12 9, 11 eqeqd 
x = y -> (a * b * x = a * (b * x) <-> a * b * y = a * (b * y))
13 muleq2 
x = suc y -> a * b * x = a * b * suc y
14 muleq2 
x = suc y -> b * x = b * suc y
15 14 muleq2d 
x = suc y -> a * (b * x) = a * (b * suc y)
16 13, 15 eqeqd 
x = suc y -> (a * b * x = a * (b * x) <-> a * b * suc y = a * (b * suc y))
17 eqtr4 
a * b * 0 = 0 -> a * (b * 0) = 0 -> a * b * 0 = a * (b * 0)
18 mul0 
a * b * 0 = 0
19 17, 18 ax_mp 
a * (b * 0) = 0 -> a * b * 0 = a * (b * 0)
20 eqtr 
a * (b * 0) = a * 0 -> a * 0 = 0 -> a * (b * 0) = 0
21 muleq2 
b * 0 = 0 -> a * (b * 0) = a * 0
22 mul0 
b * 0 = 0
23 21, 22 ax_mp 
a * (b * 0) = a * 0
24 20, 23 ax_mp 
a * 0 = 0 -> a * (b * 0) = 0
25 mul0 
a * 0 = 0
26 24, 25 ax_mp 
a * (b * 0) = 0
27 19, 26 ax_mp 
a * b * 0 = a * (b * 0)
28 mulS 
a * b * suc y = a * b * y + a * b
29 eqtr 
a * (b * suc y) = a * (b * y + b) -> a * (b * y + b) = a * (b * y) + a * b -> a * (b * suc y) = a * (b * y) + a * b
30 muleq2 
b * suc y = b * y + b -> a * (b * suc y) = a * (b * y + b)
31 mulS 
b * suc y = b * y + b
32 30, 31 ax_mp 
a * (b * suc y) = a * (b * y + b)
33 29, 32 ax_mp 
a * (b * y + b) = a * (b * y) + a * b -> a * (b * suc y) = a * (b * y) + a * b
34 muladd 
a * (b * y + b) = a * (b * y) + a * b
35 33, 34 ax_mp 
a * (b * suc y) = a * (b * y) + a * b
36 addeq1 
a * b * y = a * (b * y) -> a * b * y + a * b = a * (b * y) + a * b
37 28, 35, 36 eqtr4g 
a * b * y = a * (b * y) -> a * b * suc y = a * (b * suc y)
38 4, 8, 12, 16, 27, 37 ind 
a * b * c = a * (b * c)

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_peano (peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)