Theorem ltpow2 ≪ | index | src | ≫ 

theorem ltpow2 (a b c: nat): $ 1 < a -> (b < c <-> a ^ b < a ^ c) $;
StepHypRefExpression
1 mul11 
1 * a ^ b = a ^ b
2 1 a1i 
1 < a /\ b < c -> 1 * a ^ b = a ^ b
3 powadd 
a ^ (c - b + b) = a ^ (c - b) * a ^ b
4 npcan 
b <= c -> c - b + b = c
5 ltle 
b < c -> b <= c
6 5 anwr 
1 < a /\ b < c -> b <= c
7 4, 6 syl 
1 < a /\ b < c -> c - b + b = c
8 7 poweq2d 
1 < a /\ b < c -> a ^ (c - b + b) = a ^ c
9 3, 8 syl5eqr 
1 < a /\ b < c -> a ^ (c - b) * a ^ b = a ^ c
10 2, 9 lteqd 
1 < a /\ b < c -> (1 * a ^ b < a ^ (c - b) * a ^ b <-> a ^ b < a ^ c)
11 ltmul1 
0 < a ^ b -> (1 < a ^ (c - b) <-> 1 * a ^ b < a ^ (c - b) * a ^ b)
12 powpos 
0 < a -> 0 < a ^ b
13 lttr 
0 < 1 -> 1 < a -> 0 < a
14 d0lt1 
0 < 1
15 13, 14 ax_mp 
1 < a -> 0 < a
16 15 anwl 
1 < a /\ b < c -> 0 < a
17 12, 16 syl 
1 < a /\ b < c -> 0 < a ^ b
18 11, 17 syl 
1 < a /\ b < c -> (1 < a ^ (c - b) <-> 1 * a ^ b < a ^ (c - b) * a ^ b)
19 subpos 
b < c <-> 0 < c - b
20 19 conv d1, lt 
b < c <-> 1 <= c - b
21 anr 
1 < a /\ b < c -> b < c
22 20, 21 sylib 
1 < a /\ b < c -> 1 <= c - b
23 powltid2 
1 < a -> c - b < a ^ (c - b)
24 23 anwl 
1 < a /\ b < c -> c - b < a ^ (c - b)
25 22, 24 lelttrd 
1 < a /\ b < c -> 1 < a ^ (c - b)
26 18, 25 mpbid 
1 < a /\ b < c -> 1 * a ^ b < a ^ (c - b) * a ^ b
27 10, 26 mpbid 
1 < a /\ b < c -> a ^ b < a ^ c
28 ltnle 
a ^ b < a ^ c <-> ~a ^ c <= a ^ b
29 ltnle 
b < c <-> ~c <= b
30 28, 29 imeqi 
a ^ b < a ^ c -> b < c <-> ~a ^ c <= a ^ b -> ~c <= b
31 lepow2a 
a != 0 -> c <= b -> a ^ c <= a ^ b
32 lt01 
0 < a <-> a != 0
33 32, 15 sylib 
1 < a -> a != 0
34 31, 33 syl 
1 < a -> c <= b -> a ^ c <= a ^ b
35 34 con3d 
1 < a -> ~a ^ c <= a ^ b -> ~c <= b
36 30, 35 sylibr 
1 < a -> a ^ b < a ^ c -> b < c
37 36 imp 
1 < a /\ a ^ b < a ^ c -> b < c
38 27, 37 ibida 
1 < 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)