Theorem powadd ≪ | index | src | ≫ 

theorem powadd (a b c: nat): $ a ^ (b + c) = a ^ b * a ^ c $;
StepHypRefExpression
1 eqidd 
_1 = c -> a = a
2 eqidd 
_1 = c -> b = b
3 id 
_1 = c -> _1 = c
4 2, 3 addeqd 
_1 = c -> b + _1 = b + c
5 1, 4 poweqd 
_1 = c -> a ^ (b + _1) = a ^ (b + c)
6 eqidd 
_1 = c -> a ^ b = a ^ b
7 1, 3 poweqd 
_1 = c -> a ^ _1 = a ^ c
8 6, 7 muleqd 
_1 = c -> a ^ b * a ^ _1 = a ^ b * a ^ c
9 5, 8 eqeqd 
_1 = c -> (a ^ (b + _1) = a ^ b * a ^ _1 <-> a ^ (b + c) = a ^ b * a ^ c)
10 eqidd 
_1 = 0 -> a = a
11 eqidd 
_1 = 0 -> b = b
12 id 
_1 = 0 -> _1 = 0
13 11, 12 addeqd 
_1 = 0 -> b + _1 = b + 0
14 10, 13 poweqd 
_1 = 0 -> a ^ (b + _1) = a ^ (b + 0)
15 eqidd 
_1 = 0 -> a ^ b = a ^ b
16 10, 12 poweqd 
_1 = 0 -> a ^ _1 = a ^ 0
17 15, 16 muleqd 
_1 = 0 -> a ^ b * a ^ _1 = a ^ b * a ^ 0
18 14, 17 eqeqd 
_1 = 0 -> (a ^ (b + _1) = a ^ b * a ^ _1 <-> a ^ (b + 0) = a ^ b * a ^ 0)
19 eqidd 
_1 = a1 -> a = a
20 eqidd 
_1 = a1 -> b = b
21 id 
_1 = a1 -> _1 = a1
22 20, 21 addeqd 
_1 = a1 -> b + _1 = b + a1
23 19, 22 poweqd 
_1 = a1 -> a ^ (b + _1) = a ^ (b + a1)
24 eqidd 
_1 = a1 -> a ^ b = a ^ b
25 19, 21 poweqd 
_1 = a1 -> a ^ _1 = a ^ a1
26 24, 25 muleqd 
_1 = a1 -> a ^ b * a ^ _1 = a ^ b * a ^ a1
27 23, 26 eqeqd 
_1 = a1 -> (a ^ (b + _1) = a ^ b * a ^ _1 <-> a ^ (b + a1) = a ^ b * a ^ a1)
28 eqidd 
_1 = suc a1 -> a = a
29 eqidd 
_1 = suc a1 -> b = b
30 id 
_1 = suc a1 -> _1 = suc a1
31 29, 30 addeqd 
_1 = suc a1 -> b + _1 = b + suc a1
32 28, 31 poweqd 
_1 = suc a1 -> a ^ (b + _1) = a ^ (b + suc a1)
33 eqidd 
_1 = suc a1 -> a ^ b = a ^ b
34 28, 30 poweqd 
_1 = suc a1 -> a ^ _1 = a ^ suc a1
35 33, 34 muleqd 
_1 = suc a1 -> a ^ b * a ^ _1 = a ^ b * a ^ suc a1
36 32, 35 eqeqd 
_1 = suc a1 -> (a ^ (b + _1) = a ^ b * a ^ _1 <-> a ^ (b + suc a1) = a ^ b * a ^ suc a1)
37 eqtr4 
a ^ (b + 0) = a ^ b -> a ^ b * a ^ 0 = a ^ b -> a ^ (b + 0) = a ^ b * a ^ 0
38 poweq2 
b + 0 = b -> a ^ (b + 0) = a ^ b
39 add0 
b + 0 = b
40 38, 39 ax_mp 
a ^ (b + 0) = a ^ b
41 37, 40 ax_mp 
a ^ b * a ^ 0 = a ^ b -> a ^ (b + 0) = a ^ b * a ^ 0
42 eqtr 
a ^ b * a ^ 0 = a ^ b * 1 -> a ^ b * 1 = a ^ b -> a ^ b * a ^ 0 = a ^ b
43 muleq2 
a ^ 0 = 1 -> a ^ b * a ^ 0 = a ^ b * 1
44 pow0 
a ^ 0 = 1
45 43, 44 ax_mp 
a ^ b * a ^ 0 = a ^ b * 1
46 42, 45 ax_mp 
a ^ b * 1 = a ^ b -> a ^ b * a ^ 0 = a ^ b
47 mul12 
a ^ b * 1 = a ^ b
48 46, 47 ax_mp 
a ^ b * a ^ 0 = a ^ b
49 41, 48 ax_mp 
a ^ (b + 0) = a ^ b * a ^ 0
50 poweq2 
b + suc a1 = suc (b + a1) -> a ^ (b + suc a1) = a ^ suc (b + a1)
51 addS 
b + suc a1 = suc (b + a1)
52 50, 51 ax_mp 
a ^ (b + suc a1) = a ^ suc (b + a1)
53 muleq2 
a ^ suc a1 = a ^ a1 * a -> a ^ b * a ^ suc a1 = a ^ b * (a ^ a1 * a)
54 powS2 
a ^ suc a1 = a ^ a1 * a
55 53, 54 ax_mp 
a ^ b * a ^ suc a1 = a ^ b * (a ^ a1 * a)
56 powS2 
a ^ suc (b + a1) = a ^ (b + a1) * a
57 mulass 
a ^ b * a ^ a1 * a = a ^ b * (a ^ a1 * a)
58 muleq1 
a ^ (b + a1) = a ^ b * a ^ a1 -> a ^ (b + a1) * a = a ^ b * a ^ a1 * a
59 57, 58 syl6eq 
a ^ (b + a1) = a ^ b * a ^ a1 -> a ^ (b + a1) * a = a ^ b * (a ^ a1 * a)
60 56, 59 syl5eq 
a ^ (b + a1) = a ^ b * a ^ a1 -> a ^ suc (b + a1) = a ^ b * (a ^ a1 * a)
61 52, 55, 60 eqtr4g 
a ^ (b + a1) = a ^ b * a ^ a1 -> a ^ (b + suc a1) = a ^ b * a ^ suc a1
62 9, 18, 27, 36, 49, 61 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_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)