Theorem powadd ≪ | index | src | ≫ 

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