Theorem addcom ≪ | index | src | ≫ 

theorem addcom (a b: nat): $ a + b = b + a $;
StepHypRefExpression
1 addeq2 
x = b -> a + x = a + b
2 addeq1 
x = b -> x + a = b + a
3 1, 2 eqeqd 
x = b -> (a + x = x + a <-> a + b = b + a)
4 addeq2 
x = 0 -> a + x = a + 0
5 addeq1 
x = 0 -> x + a = 0 + a
6 4, 5 eqeqd 
x = 0 -> (a + x = x + a <-> a + 0 = 0 + a)
7 addeq2 
x = y -> a + x = a + y
8 addeq1 
x = y -> x + a = y + a
9 7, 8 eqeqd 
x = y -> (a + x = x + a <-> a + y = y + a)
10 addeq2 
x = suc y -> a + x = a + suc y
11 addeq1 
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 = a -> 0 + a = a -> a + 0 = 0 + a
14 add0 
a + 0 = a
15 13, 14 ax_mp 
0 + a = a -> a + 0 = 0 + a
16 add01 
0 + a = a
17 15, 16 ax_mp 
a + 0 = 0 + a
18 addS 
a + suc y = suc (a + y)
19 addS1 
suc y + a = suc (y + a)
20 suceq 
a + y = y + a -> suc (a + y) = suc (y + 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, add0, addS)