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 ) )