Metamath Proof Explorer

Theorem leexp1a

Description: Weak base ordering relationship for exponentiation. (Contributed by NM, 18-Dec-2005)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( j = 0 -> ( A ^ j ) = ( A ^ 0 ) )
2 oveq2 
 |-  ( j = 0 -> ( B ^ j ) = ( B ^ 0 ) )
3 1 2 breq12d 
 |-  ( j = 0 -> ( ( A ^ j ) <_ ( B ^ j ) <-> ( A ^ 0 ) <_ ( B ^ 0 ) ) )
4 3 imbi2d 
 |-  ( j = 0 -> ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> ( A ^ j ) <_ ( B ^ j ) ) <-> ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> ( A ^ 0 ) <_ ( B ^ 0 ) ) ) )
5 oveq2 
 |-  ( j = k -> ( A ^ j ) = ( A ^ k ) )
6 oveq2 
 |-  ( j = k -> ( B ^ j ) = ( B ^ k ) )
7 5 6 breq12d 
 |-  ( j = k -> ( ( A ^ j ) <_ ( B ^ j ) <-> ( A ^ k ) <_ ( B ^ k ) ) )
8 7 imbi2d 
 |-  ( j = k -> ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> ( A ^ j ) <_ ( B ^ j ) ) <-> ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> ( A ^ k ) <_ ( B ^ k ) ) ) )
9 oveq2 
 |-  ( j = ( k + 1 ) -> ( A ^ j ) = ( A ^ ( k + 1 ) ) )
10 oveq2 
 |-  ( j = ( k + 1 ) -> ( B ^ j ) = ( B ^ ( k + 1 ) ) )
11 9 10 breq12d 
 |-  ( j = ( k + 1 ) -> ( ( A ^ j ) <_ ( B ^ j ) <-> ( A ^ ( k + 1 ) ) <_ ( B ^ ( k + 1 ) ) ) )
12 11 imbi2d 
 |-  ( j = ( k + 1 ) -> ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> ( A ^ j ) <_ ( B ^ j ) ) <-> ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> ( A ^ ( k + 1 ) ) <_ ( B ^ ( k + 1 ) ) ) ) )
13 oveq2 
 |-  ( j = N -> ( A ^ j ) = ( A ^ N ) )
14 oveq2 
 |-  ( j = N -> ( B ^ j ) = ( B ^ N ) )
15 13 14 breq12d 
 |-  ( j = N -> ( ( A ^ j ) <_ ( B ^ j ) <-> ( A ^ N ) <_ ( B ^ N ) ) )
16 15 imbi2d 
 |-  ( j = N -> ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> ( A ^ j ) <_ ( B ^ j ) ) <-> ( ( ( 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 exp0 
 |-  ( A e. CC -> ( A ^ 0 ) = 1 )
20 19 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^ 0 ) = 1 )
21 1le1 
 |-  1 <_ 1
22 20 21 eqbrtrdi 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^ 0 ) <_ 1 )
23 exp0 
 |-  ( B e. CC -> ( B ^ 0 ) = 1 )
24 23 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( B ^ 0 ) = 1 )
25 22 24 breqtrrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^ 0 ) <_ ( B ^ 0 ) )
26 17 18 25 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A ^ 0 ) <_ ( B ^ 0 ) )
27 26 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> ( A ^ 0 ) <_ ( B ^ 0 ) )
28 reexpcl 
 |-  ( ( A e. RR /\ k e. NN0 ) -> ( A ^ k ) e. RR )
29 28 ad4ant14 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) -> ( A ^ k ) e. RR )
30 simplll 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) -> A e. RR )
31 simpr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) -> k e. NN0 )
32 simplrl 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) -> 0 <_ A )
33 expge0 
 |-  ( ( A e. RR /\ k e. NN0 /\ 0 <_ A ) -> 0 <_ ( A ^ k ) )
34 30 31 32 33 syl3anc 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) -> 0 <_ ( A ^ k ) )
35 reexpcl 
 |-  ( ( B e. RR /\ k e. NN0 ) -> ( B ^ k ) e. RR )
36 35 ad4ant24 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) -> ( B ^ k ) e. RR )
37 29 34 36 jca31 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) -> ( ( ( A ^ k ) e. RR /\ 0 <_ ( A ^ k ) ) /\ ( B ^ k ) e. RR ) )
38 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
39 simpl 
 |-  ( ( 0 <_ A /\ A <_ B ) -> 0 <_ A )
40 38 39 anim12i 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> ( A e. RR /\ 0 <_ A ) )
41 40 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) -> ( A e. RR /\ 0 <_ A ) )
42 simpllr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) -> B e. RR )
43 37 41 42 jca32 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) -> ( ( ( ( A ^ k ) e. RR /\ 0 <_ ( A ^ k ) ) /\ ( B ^ k ) e. RR ) /\ ( ( A e. RR /\ 0 <_ A ) /\ B e. RR ) ) )
44 43 adantr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) /\ ( A ^ k ) <_ ( B ^ k ) ) -> ( ( ( ( A ^ k ) e. RR /\ 0 <_ ( A ^ k ) ) /\ ( B ^ k ) e. RR ) /\ ( ( A e. RR /\ 0 <_ A ) /\ B e. RR ) ) )
45 simplrr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) -> A <_ B )
46 45 anim1ci 
 |-  ( ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) /\ ( A ^ k ) <_ ( B ^ k ) ) -> ( ( A ^ k ) <_ ( B ^ k ) /\ A <_ B ) )
47 lemul12a 
 |-  ( ( ( ( ( A ^ k ) e. RR /\ 0 <_ ( A ^ k ) ) /\ ( B ^ k ) e. RR ) /\ ( ( A e. RR /\ 0 <_ A ) /\ B e. RR ) ) -> ( ( ( A ^ k ) <_ ( B ^ k ) /\ A <_ B ) -> ( ( A ^ k ) x. A ) <_ ( ( B ^ k ) x. B ) ) )
48 44 46 47 sylc 
 |-  ( ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) /\ ( A ^ k ) <_ ( B ^ k ) ) -> ( ( A ^ k ) x. A ) <_ ( ( B ^ k ) x. B ) )
49 expp1 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ ( k + 1 ) ) = ( ( A ^ k ) x. A ) )
50 17 49 sylan 
 |-  ( ( A e. RR /\ k e. NN0 ) -> ( A ^ ( k + 1 ) ) = ( ( A ^ k ) x. A ) )
51 50 ad5ant14 
 |-  ( ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) /\ ( A ^ k ) <_ ( B ^ k ) ) -> ( A ^ ( k + 1 ) ) = ( ( A ^ k ) x. A ) )
52 expp1 
 |-  ( ( B e. CC /\ k e. NN0 ) -> ( B ^ ( k + 1 ) ) = ( ( B ^ k ) x. B ) )
53 18 52 sylan 
 |-  ( ( B e. RR /\ k e. NN0 ) -> ( B ^ ( k + 1 ) ) = ( ( B ^ k ) x. B ) )
54 53 ad5ant24 
 |-  ( ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) /\ ( A ^ k ) <_ ( B ^ k ) ) -> ( B ^ ( k + 1 ) ) = ( ( B ^ k ) x. B ) )
55 48 51 54 3brtr4d 
 |-  ( ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) /\ ( A ^ k ) <_ ( B ^ k ) ) -> ( A ^ ( k + 1 ) ) <_ ( B ^ ( k + 1 ) ) )
56 55 ex 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ k e. NN0 ) -> ( ( A ^ k ) <_ ( B ^ k ) -> ( A ^ ( k + 1 ) ) <_ ( B ^ ( k + 1 ) ) ) )
57 56 expcom 
 |-  ( k e. NN0 -> ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> ( ( A ^ k ) <_ ( B ^ k ) -> ( A ^ ( k + 1 ) ) <_ ( B ^ ( k + 1 ) ) ) ) )
58 57 a2d 
 |-  ( k e. NN0 -> ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> ( A ^ k ) <_ ( B ^ k ) ) -> ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> ( A ^ ( k + 1 ) ) <_ ( B ^ ( k + 1 ) ) ) ) )
59 4 8 12 16 27 58 nn0ind 
 |-  ( N e. NN0 -> ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> ( A ^ N ) <_ ( B ^ N ) ) )
60 59 exp4c 
 |-  ( N e. NN0 -> ( A e. RR -> ( B e. RR -> ( ( 0 <_ A /\ A <_ B ) -> ( A ^ N ) <_ ( B ^ N ) ) ) ) )
61 60 com3l 
 |-  ( A e. RR -> ( B e. RR -> ( N e. NN0 -> ( ( 0 <_ A /\ A <_ B ) -> ( A ^ N ) <_ ( B ^ N ) ) ) ) )
62 61 3imp1 
 |-  ( ( ( A e. RR /\ B e. RR /\ N e. NN0 ) /\ ( 0 <_ A /\ A <_ B ) ) -> ( A ^ N ) <_ ( B ^ N ) )