Metamath Proof Explorer

Theorem efexple

Description: Convert a bound on a power to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014)

Ref Expression
Assertion efexple 
|- ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> ( ( A ^ N ) <_ B <-> N <_ ( |_ ` ( ( log ` B ) / ( log ` A ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. RR /\ 1 < A ) -> A e. RR )
2 0lt1 
 |-  0 < 1
3 0re 
 |-  0 e. RR
4 1re 
 |-  1 e. RR
5 lttr 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ A e. RR ) -> ( ( 0 < 1 /\ 1 < A ) -> 0 < A ) )
6 3 4 5 mp3an12 
 |-  ( A e. RR -> ( ( 0 < 1 /\ 1 < A ) -> 0 < A ) )
7 2 6 mpani 
 |-  ( A e. RR -> ( 1 < A -> 0 < A ) )
8 7 imp 
 |-  ( ( A e. RR /\ 1 < A ) -> 0 < A )
9 1 8 elrpd 
 |-  ( ( A e. RR /\ 1 < A ) -> A e. RR+ )
10 9 3ad2ant1 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> A e. RR+ )
11 simp2 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> N e. ZZ )
12 reexplog 
 |-  ( ( A e. RR+ /\ N e. ZZ ) -> ( A ^ N ) = ( exp ` ( N x. ( log ` A ) ) ) )
13 10 11 12 syl2anc 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> ( A ^ N ) = ( exp ` ( N x. ( log ` A ) ) ) )
14 reeflog 
 |-  ( B e. RR+ -> ( exp ` ( log ` B ) ) = B )
15 14 3ad2ant3 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> ( exp ` ( log ` B ) ) = B )
16 15 eqcomd 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> B = ( exp ` ( log ` B ) ) )
17 13 16 breq12d 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> ( ( A ^ N ) <_ B <-> ( exp ` ( N x. ( log ` A ) ) ) <_ ( exp ` ( log ` B ) ) ) )
18 zre 
 |-  ( N e. ZZ -> N e. RR )
19 18 3ad2ant2 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> N e. RR )
20 rplogcl 
 |-  ( ( A e. RR /\ 1 < A ) -> ( log ` A ) e. RR+ )
21 20 3ad2ant1 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> ( log ` A ) e. RR+ )
22 21 rpred 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> ( log ` A ) e. RR )
23 19 22 remulcld 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> ( N x. ( log ` A ) ) e. RR )
24 relogcl 
 |-  ( B e. RR+ -> ( log ` B ) e. RR )
25 24 3ad2ant3 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> ( log ` B ) e. RR )
26 efle 
 |-  ( ( ( N x. ( log ` A ) ) e. RR /\ ( log ` B ) e. RR ) -> ( ( N x. ( log ` A ) ) <_ ( log ` B ) <-> ( exp ` ( N x. ( log ` A ) ) ) <_ ( exp ` ( log ` B ) ) ) )
27 23 25 26 syl2anc 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> ( ( N x. ( log ` A ) ) <_ ( log ` B ) <-> ( exp ` ( N x. ( log ` A ) ) ) <_ ( exp ` ( log ` B ) ) ) )
28 19 25 21 lemuldivd 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> ( ( N x. ( log ` A ) ) <_ ( log ` B ) <-> N <_ ( ( log ` B ) / ( log ` A ) ) ) )
29 25 21 rerpdivcld 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> ( ( log ` B ) / ( log ` A ) ) e. RR )
30 flge 
 |-  ( ( ( ( log ` B ) / ( log ` A ) ) e. RR /\ N e. ZZ ) -> ( N <_ ( ( log ` B ) / ( log ` A ) ) <-> N <_ ( |_ ` ( ( log ` B ) / ( log ` A ) ) ) ) )
31 29 11 30 syl2anc 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> ( N <_ ( ( log ` B ) / ( log ` A ) ) <-> N <_ ( |_ ` ( ( log ` B ) / ( log ` A ) ) ) ) )
32 28 31 bitrd 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> ( ( N x. ( log ` A ) ) <_ ( log ` B ) <-> N <_ ( |_ ` ( ( log ` B ) / ( log ` A ) ) ) ) )
33 17 27 32 3bitr2d 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> ( ( A ^ N ) <_ B <-> N <_ ( |_ ` ( ( log ` B ) / ( log ` A ) ) ) ) )