Theorem powltid2 ≪ | index | src | ≫ 

theorem powltid2 (a b: nat): $ 1 < a -> b < a ^ b $;
StepHypRefExpression
1 id 
_1 = b -> _1 = b
2 1 poweq2d 
_1 = b -> a ^ _1 = a ^ b
3 1, 2 lteqd 
_1 = b -> (_1 < a ^ _1 <-> b < a ^ b)
4 id 
_1 = 0 -> _1 = 0
5 4 poweq2d 
_1 = 0 -> a ^ _1 = a ^ 0
6 4, 5 lteqd 
_1 = 0 -> (_1 < a ^ _1 <-> 0 < a ^ 0)
7 id 
_1 = a1 -> _1 = a1
8 7 poweq2d 
_1 = a1 -> a ^ _1 = a ^ a1
9 7, 8 lteqd 
_1 = a1 -> (_1 < a ^ _1 <-> a1 < a ^ a1)
10 id 
_1 = suc a1 -> _1 = suc a1
11 10 poweq2d 
_1 = suc a1 -> a ^ _1 = a ^ suc a1
12 10, 11 lteqd 
_1 = suc a1 -> (_1 < a ^ _1 <-> suc a1 < a ^ suc a1)
13 lteq2 
a ^ 0 = 1 -> (0 < a ^ 0 <-> 0 < 1)
14 pow0 
a ^ 0 = 1
15 13, 14 ax_mp 
0 < a ^ 0 <-> 0 < 1
16 d0lt1 
0 < 1
17 15, 16 mpbir 
0 < a ^ 0
18 17 a1i 
1 < a -> 0 < a ^ 0
19 anr 
1 < a /\ a1 < a ^ a1 -> a1 < a ^ a1
20 19 conv lt 
1 < a /\ a1 < a ^ a1 -> suc a1 <= a ^ a1
21 lteq 
1 * a ^ a1 = a ^ a1 -> a * a ^ a1 = a ^ suc a1 -> (1 * a ^ a1 < a * a ^ a1 <-> a ^ a1 < a ^ suc a1)
22 mul11 
1 * a ^ a1 = a ^ a1
23 21, 22 ax_mp 
a * a ^ a1 = a ^ suc a1 -> (1 * a ^ a1 < a * a ^ a1 <-> a ^ a1 < a ^ suc a1)
24 eqcom 
a ^ suc a1 = a * a ^ a1 -> a * a ^ a1 = a ^ suc a1
25 powS 
a ^ suc a1 = a * a ^ a1
26 24, 25 ax_mp 
a * a ^ a1 = a ^ suc a1
27 23, 26 ax_mp 
1 * a ^ a1 < a * a ^ a1 <-> a ^ a1 < a ^ suc a1
28 ltmul1 
0 < a ^ a1 -> (1 < a <-> 1 * a ^ a1 < a * a ^ a1)
29 powpos 
0 < a -> 0 < a ^ a1
30 lttr 
0 < 1 -> 1 < a -> 0 < a
31 30, 16 ax_mp 
1 < a -> 0 < a
32 31 anwl 
1 < a /\ a1 < a ^ a1 -> 0 < a
33 29, 32 syl 
1 < a /\ a1 < a ^ a1 -> 0 < a ^ a1
34 28, 33 syl 
1 < a /\ a1 < a ^ a1 -> (1 < a <-> 1 * a ^ a1 < a * a ^ a1)
35 anl 
1 < a /\ a1 < a ^ a1 -> 1 < a
36 34, 35 mpbid 
1 < a /\ a1 < a ^ a1 -> 1 * a ^ a1 < a * a ^ a1
37 27, 36 sylib 
1 < a /\ a1 < a ^ a1 -> a ^ a1 < a ^ suc a1
38 20, 37 lelttrd 
1 < a /\ a1 < a ^ a1 -> suc a1 < a ^ suc a1
39 3, 6, 9, 12, 18, 38 indd 
1 < a -> b < a ^ b

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)