Theorem muladd ≪ | index | src | ≫ 

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