Theorem mulS1 ≪ | index | src | ≫ 

theorem mulS1 (a b: nat): $ suc a * b = a * b + b $;
StepHypRefExpression
1 muleq2 
x = b -> suc a * x = suc a * b
2 muleq2 
x = b -> a * x = a * b
3 id 
x = b -> x = b
4 2, 3 addeqd 
x = b -> a * x + x = a * b + b
5 1, 4 eqeqd 
x = b -> (suc a * x = a * x + x <-> suc a * b = a * b + b)
6 muleq2 
x = 0 -> suc a * x = suc a * 0
7 muleq2 
x = 0 -> a * x = a * 0
8 id 
x = 0 -> x = 0
9 7, 8 addeqd 
x = 0 -> a * x + x = a * 0 + 0
10 6, 9 eqeqd 
x = 0 -> (suc a * x = a * x + x <-> suc a * 0 = a * 0 + 0)
11 muleq2 
x = y -> suc a * x = suc a * y
12 muleq2 
x = y -> a * x = a * y
13 id 
x = y -> x = y
14 12, 13 addeqd 
x = y -> a * x + x = a * y + y
15 11, 14 eqeqd 
x = y -> (suc a * x = a * x + x <-> suc a * y = a * y + y)
16 muleq2 
x = suc y -> suc a * x = suc a * suc y
17 muleq2 
x = suc y -> a * x = a * suc y
18 id 
x = suc y -> x = suc y
19 17, 18 addeqd 
x = suc y -> a * x + x = a * suc y + suc y
20 16, 19 eqeqd 
x = suc y -> (suc a * x = a * x + x <-> suc a * suc y = a * suc y + suc y)
21 eqtr4 
suc a * 0 = 0 -> a * 0 + 0 = 0 -> suc a * 0 = a * 0 + 0
22 mul0 
suc a * 0 = 0
23 21, 22 ax_mp 
a * 0 + 0 = 0 -> suc a * 0 = a * 0 + 0
24 eqtr 
a * 0 + 0 = a * 0 -> a * 0 = 0 -> a * 0 + 0 = 0
25 add0 
a * 0 + 0 = a * 0
26 24, 25 ax_mp 
a * 0 = 0 -> a * 0 + 0 = 0
27 mul0 
a * 0 = 0
28 26, 27 ax_mp 
a * 0 + 0 = 0
29 23, 28 ax_mp 
suc a * 0 = a * 0 + 0
30 mulS 
suc a * suc y = suc a * y + suc a
31 eqtr 
a * suc y + suc y = a * y + a + suc y -> a * y + a + suc y = a * y + y + suc a -> a * suc y + suc y = a * y + y + suc a
32 addeq1 
a * suc y = a * y + a -> a * suc y + suc y = a * y + a + suc y
33 mulS 
a * suc y = a * y + a
34 32, 33 ax_mp 
a * suc y + suc y = a * y + a + suc y
35 31, 34 ax_mp 
a * y + a + suc y = a * y + y + suc a -> a * suc y + suc y = a * y + y + suc a
36 eqtr 
a * y + a + suc y = suc (a * y + a + y) -> suc (a * y + a + y) = a * y + y + suc a -> a * y + a + suc y = a * y + y + suc a
37 addS 
a * y + a + suc y = suc (a * y + a + y)
38 36, 37 ax_mp 
suc (a * y + a + y) = a * y + y + suc a -> a * y + a + suc y = a * y + y + suc a
39 eqtr4 
suc (a * y + a + y) = suc (a * y + y + a) -> a * y + y + suc a = suc (a * y + y + a) -> suc (a * y + a + y) = a * y + y + suc a
40 suceq 
a * y + a + y = a * y + y + a -> suc (a * y + a + y) = suc (a * y + y + a)
41 addrass 
a * y + a + y = a * y + y + a
42 40, 41 ax_mp 
suc (a * y + a + y) = suc (a * y + y + a)
43 39, 42 ax_mp 
a * y + y + suc a = suc (a * y + y + a) -> suc (a * y + a + y) = a * y + y + suc a
44 addS 
a * y + y + suc a = suc (a * y + y + a)
45 43, 44 ax_mp 
suc (a * y + a + y) = a * y + y + suc a
46 38, 45 ax_mp 
a * y + a + suc y = a * y + y + suc a
47 35, 46 ax_mp 
a * suc y + suc y = a * y + y + suc a
48 addeq1 
suc a * y = a * y + y -> suc a * y + suc a = a * y + y + suc a
49 30, 47, 48 eqtr4g 
suc a * y = a * y + y -> suc a * suc y = a * suc y + suc y
50 5, 10, 15, 20, 29, 49 ind 
suc a * b = a * b + 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_peano (peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)