This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem expnlbnd

Description: The reciprocal of exponentiation with a base greater than 1 has no positive lower bound. (Contributed by NM, 18-Jul-2008)

Ref Expression
Assertion expnlbnd 
|- ( ( A e. RR+ /\ B e. RR /\ 1 < B ) -> E. k e. NN ( 1 / ( B ^ k ) ) < A )

Proof

Step Hyp Ref Expression
1 rpre 
 |-  ( A e. RR+ -> A e. RR )
2 rpne0 
 |-  ( A e. RR+ -> A =/= 0 )
3 1 2 rereccld 
 |-  ( A e. RR+ -> ( 1 / A ) e. RR )
4 expnbnd 
 |-  ( ( ( 1 / A ) e. RR /\ B e. RR /\ 1 < B ) -> E. k e. NN ( 1 / A ) < ( B ^ k ) )
5 3 4 syl3an1 
 |-  ( ( A e. RR+ /\ B e. RR /\ 1 < B ) -> E. k e. NN ( 1 / A ) < ( B ^ k ) )
6 rpregt0 
 |-  ( A e. RR+ -> ( A e. RR /\ 0 < A ) )
7 6 3ad2ant1 
 |-  ( ( A e. RR+ /\ B e. RR /\ 1 < B ) -> ( A e. RR /\ 0 < A ) )
8 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
9 reexpcl 
 |-  ( ( B e. RR /\ k e. NN0 ) -> ( B ^ k ) e. RR )
10 8 9 sylan2 
 |-  ( ( B e. RR /\ k e. NN ) -> ( B ^ k ) e. RR )
11 10 adantlr 
 |-  ( ( ( B e. RR /\ 1 < B ) /\ k e. NN ) -> ( B ^ k ) e. RR )
12 simpll 
 |-  ( ( ( B e. RR /\ 1 < B ) /\ k e. NN ) -> B e. RR )
13 nnz 
 |-  ( k e. NN -> k e. ZZ )
14 13 adantl 
 |-  ( ( ( B e. RR /\ 1 < B ) /\ k e. NN ) -> k e. ZZ )
15 0lt1 
 |-  0 < 1
16 0re 
 |-  0 e. RR
17 1re 
 |-  1 e. RR
18 lttr 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ B e. RR ) -> ( ( 0 < 1 /\ 1 < B ) -> 0 < B ) )
19 16 17 18 mp3an12 
 |-  ( B e. RR -> ( ( 0 < 1 /\ 1 < B ) -> 0 < B ) )
20 15 19 mpani 
 |-  ( B e. RR -> ( 1 < B -> 0 < B ) )
21 20 imp 
 |-  ( ( B e. RR /\ 1 < B ) -> 0 < B )
22 21 adantr 
 |-  ( ( ( B e. RR /\ 1 < B ) /\ k e. NN ) -> 0 < B )
23 expgt0 
 |-  ( ( B e. RR /\ k e. ZZ /\ 0 < B ) -> 0 < ( B ^ k ) )
24 12 14 22 23 syl3anc 
 |-  ( ( ( B e. RR /\ 1 < B ) /\ k e. NN ) -> 0 < ( B ^ k ) )
25 11 24 jca 
 |-  ( ( ( B e. RR /\ 1 < B ) /\ k e. NN ) -> ( ( B ^ k ) e. RR /\ 0 < ( B ^ k ) ) )
26 25 3adantl1 
 |-  ( ( ( A e. RR+ /\ B e. RR /\ 1 < B ) /\ k e. NN ) -> ( ( B ^ k ) e. RR /\ 0 < ( B ^ k ) ) )
27 ltrec1 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( ( B ^ k ) e. RR /\ 0 < ( B ^ k ) ) ) -> ( ( 1 / A ) < ( B ^ k ) <-> ( 1 / ( B ^ k ) ) < A ) )
28 7 26 27 syl2an2r 
 |-  ( ( ( A e. RR+ /\ B e. RR /\ 1 < B ) /\ k e. NN ) -> ( ( 1 / A ) < ( B ^ k ) <-> ( 1 / ( B ^ k ) ) < A ) )
29 28 rexbidva 
 |-  ( ( A e. RR+ /\ B e. RR /\ 1 < B ) -> ( E. k e. NN ( 1 / A ) < ( B ^ k ) <-> E. k e. NN ( 1 / ( B ^ k ) ) < A ) )
30 5 29 mpbid 
 |-  ( ( A e. RR+ /\ B e. RR /\ 1 < B ) -> E. k e. NN ( 1 / ( B ^ k ) ) < A )