Theorem mulcom ≪ | index | src | ≫ 

theorem mulcom (a b: nat): $ a * b = b * a $;
StepHypRefExpression
1 muleq2 
x = b -> a * x = a * b
2 muleq1 
x = b -> x * a = b * a
3 1, 2 eqeqd 
x = b -> (a * x = x * a <-> a * b = b * a)
4 muleq2 
x = 0 -> a * x = a * 0
5 muleq1 
x = 0 -> x * a = 0 * a
6 4, 5 eqeqd 
x = 0 -> (a * x = x * a <-> a * 0 = 0 * a)
7 muleq2 
x = y -> a * x = a * y
8 muleq1 
x = y -> x * a = y * a
9 7, 8 eqeqd 
x = y -> (a * x = x * a <-> a * y = y * a)
10 muleq2 
x = suc y -> a * x = a * suc y
11 muleq1 
x = suc y -> x * a = suc y * a
12 10, 11 eqeqd 
x = suc y -> (a * x = x * a <-> a * suc y = suc y * a)
13 eqtr4 
a * 0 = 0 -> 0 * a = 0 -> a * 0 = 0 * a
14 mul0 
a * 0 = 0
15 13, 14 ax_mp 
0 * a = 0 -> a * 0 = 0 * a
16 mul01 
0 * a = 0
17 15, 16 ax_mp 
a * 0 = 0 * a
18 mulS 
a * suc y = a * y + a
19 mulS1 
suc y * a = y * a + a
20 addeq1 
a * y = y * a -> a * y + a = y * a + a
21 18, 19, 20 eqtr4g 
a * y = y * a -> a * suc y = suc y * a
22 3, 6, 9, 12, 17, 21 ind 
a * b = b * 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_peano (peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)