Theorem powltid2 ≪ | index | src | ≫ 

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