Metamath Proof Explorer

Theorem expmordi

Description: Base ordering relationship for exponentiation of nonnegative reals to a fixed positive integer power. (Contributed by Stefan O'Rear, 16-Oct-2014)

Ref Expression
Assertion expmordi 
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) /\ N e. NN ) -> ( A ^ N ) < ( B ^ N ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( a = 1 -> ( A ^ a ) = ( A ^ 1 ) )
2 oveq2 
 |-  ( a = 1 -> ( B ^ a ) = ( B ^ 1 ) )
3 1 2 breq12d 
 |-  ( a = 1 -> ( ( A ^ a ) < ( B ^ a ) <-> ( A ^ 1 ) < ( B ^ 1 ) ) )
4 3 imbi2d 
 |-  ( a = 1 -> ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) -> ( A ^ a ) < ( B ^ a ) ) <-> ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) -> ( A ^ 1 ) < ( B ^ 1 ) ) ) )
5 oveq2 
 |-  ( a = b -> ( A ^ a ) = ( A ^ b ) )
6 oveq2 
 |-  ( a = b -> ( B ^ a ) = ( B ^ b ) )
7 5 6 breq12d 
 |-  ( a = b -> ( ( A ^ a ) < ( B ^ a ) <-> ( A ^ b ) < ( B ^ b ) ) )
8 7 imbi2d 
 |-  ( a = b -> ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) -> ( A ^ a ) < ( B ^ a ) ) <-> ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) -> ( A ^ b ) < ( B ^ b ) ) ) )
9 oveq2 
 |-  ( a = ( b + 1 ) -> ( A ^ a ) = ( A ^ ( b + 1 ) ) )
10 oveq2 
 |-  ( a = ( b + 1 ) -> ( B ^ a ) = ( B ^ ( b + 1 ) ) )
11 9 10 breq12d 
 |-  ( a = ( b + 1 ) -> ( ( A ^ a ) < ( B ^ a ) <-> ( A ^ ( b + 1 ) ) < ( B ^ ( b + 1 ) ) ) )
12 11 imbi2d 
 |-  ( a = ( b + 1 ) -> ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) -> ( A ^ a ) < ( B ^ a ) ) <-> ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) -> ( A ^ ( b + 1 ) ) < ( B ^ ( b + 1 ) ) ) ) )
13 oveq2 
 |-  ( a = N -> ( A ^ a ) = ( A ^ N ) )
14 oveq2 
 |-  ( a = N -> ( B ^ a ) = ( B ^ N ) )
15 13 14 breq12d 
 |-  ( a = N -> ( ( A ^ a ) < ( B ^ a ) <-> ( A ^ N ) < ( B ^ N ) ) )
16 15 imbi2d 
 |-  ( a = N -> ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) -> ( A ^ a ) < ( B ^ a ) ) <-> ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) -> ( A ^ N ) < ( B ^ N ) ) ) )
17 recn 
 |-  ( A e. RR -> A e. CC )
18 recn 
 |-  ( B e. RR -> B e. CC )
19 exp1 
 |-  ( A e. CC -> ( A ^ 1 ) = A )
20 exp1 
 |-  ( B e. CC -> ( B ^ 1 ) = B )
21 19 20 breqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 1 ) < ( B ^ 1 ) <-> A < B ) )
22 17 18 21 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A ^ 1 ) < ( B ^ 1 ) <-> A < B ) )
23 22 biimpar 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < B ) -> ( A ^ 1 ) < ( B ^ 1 ) )
24 23 adantrl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) -> ( A ^ 1 ) < ( B ^ 1 ) )
25 simp2ll 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> A e. RR )
26 nnnn0 
 |-  ( b e. NN -> b e. NN0 )
27 26 3ad2ant1 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> b e. NN0 )
28 25 27 reexpcld 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> ( A ^ b ) e. RR )
29 simp2lr 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> B e. RR )
30 29 27 reexpcld 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> ( B ^ b ) e. RR )
31 28 30 jca 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> ( ( A ^ b ) e. RR /\ ( B ^ b ) e. RR ) )
32 simp2rl 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> 0 <_ A )
33 25 27 32 expge0d 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> 0 <_ ( A ^ b ) )
34 simp3 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> ( A ^ b ) < ( B ^ b ) )
35 33 34 jca 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> ( 0 <_ ( A ^ b ) /\ ( A ^ b ) < ( B ^ b ) ) )
36 simp2l 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> ( A e. RR /\ B e. RR ) )
37 simp2r 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> ( 0 <_ A /\ A < B ) )
38 ltmul12a 
 |-  ( ( ( ( ( A ^ b ) e. RR /\ ( B ^ b ) e. RR ) /\ ( 0 <_ ( A ^ b ) /\ ( A ^ b ) < ( B ^ b ) ) ) /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) ) -> ( ( A ^ b ) x. A ) < ( ( B ^ b ) x. B ) )
39 31 35 36 37 38 syl22anc 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> ( ( A ^ b ) x. A ) < ( ( B ^ b ) x. B ) )
40 25 recnd 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> A e. CC )
41 40 27 expp1d 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> ( A ^ ( b + 1 ) ) = ( ( A ^ b ) x. A ) )
42 29 recnd 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> B e. CC )
43 42 27 expp1d 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> ( B ^ ( b + 1 ) ) = ( ( B ^ b ) x. B ) )
44 39 41 43 3brtr4d 
 |-  ( ( b e. NN /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( A ^ b ) < ( B ^ b ) ) -> ( A ^ ( b + 1 ) ) < ( B ^ ( b + 1 ) ) )
45 44 3exp 
 |-  ( b e. NN -> ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) -> ( ( A ^ b ) < ( B ^ b ) -> ( A ^ ( b + 1 ) ) < ( B ^ ( b + 1 ) ) ) ) )
46 45 a2d 
 |-  ( b e. NN -> ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) -> ( A ^ b ) < ( B ^ b ) ) -> ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) -> ( A ^ ( b + 1 ) ) < ( B ^ ( b + 1 ) ) ) ) )
47 4 8 12 16 24 46 nnind 
 |-  ( N e. NN -> ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) -> ( A ^ N ) < ( B ^ N ) ) )
48 47 impcom 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ N e. NN ) -> ( A ^ N ) < ( B ^ N ) )
49 48 3impa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) /\ N e. NN ) -> ( A ^ N ) < ( B ^ N ) )