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 )