Theorem powmul ≪ | index | src | ≫ 

theorem powmul (a b c: nat): $ a ^ (b * c) = (a ^ b) ^ c $;
StepHypRefExpression
1 eqidd 
_1 = c -> a = a
2 eqidd 
_1 = c -> b = b
3 id 
_1 = c -> _1 = c
4 2, 3 muleqd 
_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 6, 3 poweqd 
_1 = c -> (a ^ b) ^ _1 = (a ^ b) ^ c
8 5, 7 eqeqd 
_1 = c -> (a ^ (b * _1) = (a ^ b) ^ _1 <-> a ^ (b * c) = (a ^ b) ^ c)
9 eqidd 
_1 = 0 -> a = a
10 eqidd 
_1 = 0 -> b = b
11 id 
_1 = 0 -> _1 = 0
12 10, 11 muleqd 
_1 = 0 -> b * _1 = b * 0
13 9, 12 poweqd 
_1 = 0 -> a ^ (b * _1) = a ^ (b * 0)
14 eqidd 
_1 = 0 -> a ^ b = a ^ b
15 14, 11 poweqd 
_1 = 0 -> (a ^ b) ^ _1 = (a ^ b) ^ 0
16 13, 15 eqeqd 
_1 = 0 -> (a ^ (b * _1) = (a ^ b) ^ _1 <-> a ^ (b * 0) = (a ^ b) ^ 0)
17 eqidd 
_1 = a1 -> a = a
18 eqidd 
_1 = a1 -> b = b
19 id 
_1 = a1 -> _1 = a1
20 18, 19 muleqd 
_1 = a1 -> b * _1 = b * a1
21 17, 20 poweqd 
_1 = a1 -> a ^ (b * _1) = a ^ (b * a1)
22 eqidd 
_1 = a1 -> a ^ b = a ^ b
23 22, 19 poweqd 
_1 = a1 -> (a ^ b) ^ _1 = (a ^ b) ^ a1
24 21, 23 eqeqd 
_1 = a1 -> (a ^ (b * _1) = (a ^ b) ^ _1 <-> a ^ (b * a1) = (a ^ b) ^ a1)
25 eqidd 
_1 = suc a1 -> a = a
26 eqidd 
_1 = suc a1 -> b = b
27 id 
_1 = suc a1 -> _1 = suc a1
28 26, 27 muleqd 
_1 = suc a1 -> b * _1 = b * suc a1
29 25, 28 poweqd 
_1 = suc a1 -> a ^ (b * _1) = a ^ (b * suc a1)
30 eqidd 
_1 = suc a1 -> a ^ b = a ^ b
31 30, 27 poweqd 
_1 = suc a1 -> (a ^ b) ^ _1 = (a ^ b) ^ suc a1
32 29, 31 eqeqd 
_1 = suc a1 -> (a ^ (b * _1) = (a ^ b) ^ _1 <-> a ^ (b * suc a1) = (a ^ b) ^ suc a1)
33 eqtr 
a ^ (b * 0) = a ^ 0 -> a ^ 0 = (a ^ b) ^ 0 -> a ^ (b * 0) = (a ^ b) ^ 0
34 poweq2 
b * 0 = 0 -> a ^ (b * 0) = a ^ 0
35 mul0 
b * 0 = 0
36 34, 35 ax_mp 
a ^ (b * 0) = a ^ 0
37 33, 36 ax_mp 
a ^ 0 = (a ^ b) ^ 0 -> a ^ (b * 0) = (a ^ b) ^ 0
38 eqtr4 
a ^ 0 = 1 -> (a ^ b) ^ 0 = 1 -> a ^ 0 = (a ^ b) ^ 0
39 pow0 
a ^ 0 = 1
40 38, 39 ax_mp 
(a ^ b) ^ 0 = 1 -> a ^ 0 = (a ^ b) ^ 0
41 pow0 
(a ^ b) ^ 0 = 1
42 40, 41 ax_mp 
a ^ 0 = (a ^ b) ^ 0
43 37, 42 ax_mp 
a ^ (b * 0) = (a ^ b) ^ 0
44 poweq2 
b * suc a1 = b * a1 + b -> a ^ (b * suc a1) = a ^ (b * a1 + b)
45 mulS 
b * suc a1 = b * a1 + b
46 44, 45 ax_mp 
a ^ (b * suc a1) = a ^ (b * a1 + b)
47 powadd 
a ^ (b * a1 + b) = a ^ (b * a1) * a ^ b
48 powS2 
(a ^ b) ^ suc a1 = (a ^ b) ^ a1 * a ^ b
49 muleq1 
a ^ (b * a1) = (a ^ b) ^ a1 -> a ^ (b * a1) * a ^ b = (a ^ b) ^ a1 * a ^ b
50 48, 49 syl6eqr 
a ^ (b * a1) = (a ^ b) ^ a1 -> a ^ (b * a1) * a ^ b = (a ^ b) ^ suc a1
51 47, 50 syl5eq 
a ^ (b * a1) = (a ^ b) ^ a1 -> a ^ (b * a1 + b) = (a ^ b) ^ suc a1
52 46, 51 syl5eq 
a ^ (b * a1) = (a ^ b) ^ a1 -> a ^ (b * suc a1) = (a ^ b) ^ suc a1
53 8, 16, 24, 32, 43, 52 ind 
a ^ (b * c) = (a ^ b) ^ 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)