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