Theorem powmul ≪ | index | src | ≫ 

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