Metamath Proof Explorer

Theorem ostth2lem1

Description: Lemma for ostth2 , although it is just a simple statement about exponentials which does not involve any specifics of ostth2 . If a power is upper bounded by a linear term, the exponent must be less than one. Or in big-O notation, n e. o ( A ^ n ) for any 1 < A . (Contributed by Mario Carneiro, 10-Sep-2014)

Ref Expression
Hypotheses ostth2lem1.1 
|- ( ph -> A e. RR )
ostth2lem1.2 
|- ( ph -> B e. RR )
ostth2lem1.3 
|- ( ( ph /\ n e. NN ) -> ( A ^ n ) <_ ( n x. B ) )
Assertion ostth2lem1 
|- ( ph -> A <_ 1 )

Proof

Step Hyp Ref Expression
1 ostth2lem1.1 
 |-  ( ph -> A e. RR )
2 ostth2lem1.2 
 |-  ( ph -> B e. RR )
3 ostth2lem1.3 
 |-  ( ( ph /\ n e. NN ) -> ( A ^ n ) <_ ( n x. B ) )
4 2re 
 |-  2 e. RR
5 2 adantr 
 |-  ( ( ph /\ 1 < A ) -> B e. RR )
6 remulcl 
 |-  ( ( 2 e. RR /\ B e. RR ) -> ( 2 x. B ) e. RR )
7 4 5 6 sylancr 
 |-  ( ( ph /\ 1 < A ) -> ( 2 x. B ) e. RR )
8 simpr 
 |-  ( ( ph /\ 1 < A ) -> 1 < A )
9 1re 
 |-  1 e. RR
10 1 adantr 
 |-  ( ( ph /\ 1 < A ) -> A e. RR )
11 difrp 
 |-  ( ( 1 e. RR /\ A e. RR ) -> ( 1 < A <-> ( A - 1 ) e. RR+ ) )
12 9 10 11 sylancr 
 |-  ( ( ph /\ 1 < A ) -> ( 1 < A <-> ( A - 1 ) e. RR+ ) )
13 8 12 mpbid 
 |-  ( ( ph /\ 1 < A ) -> ( A - 1 ) e. RR+ )
14 7 13 rerpdivcld 
 |-  ( ( ph /\ 1 < A ) -> ( ( 2 x. B ) / ( A - 1 ) ) e. RR )
15 expnbnd 
 |-  ( ( ( ( 2 x. B ) / ( A - 1 ) ) e. RR /\ A e. RR /\ 1 < A ) -> E. k e. NN ( ( 2 x. B ) / ( A - 1 ) ) < ( A ^ k ) )
16 14 10 8 15 syl3anc 
 |-  ( ( ph /\ 1 < A ) -> E. k e. NN ( ( 2 x. B ) / ( A - 1 ) ) < ( A ^ k ) )
17 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
18 reexpcl 
 |-  ( ( A e. RR /\ k e. NN0 ) -> ( A ^ k ) e. RR )
19 10 17 18 syl2an 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ k ) e. RR )
20 14 adantr 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( 2 x. B ) / ( A - 1 ) ) e. RR )
21 13 rpred 
 |-  ( ( ph /\ 1 < A ) -> ( A - 1 ) e. RR )
22 21 adantr 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A - 1 ) e. RR )
23 nnre 
 |-  ( k e. NN -> k e. RR )
24 23 adantl 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> k e. RR )
25 22 24 remulcld 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( A - 1 ) x. k ) e. RR )
26 25 19 remulcld 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. k ) x. ( A ^ k ) ) e. RR )
27 1 ad2antrr 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> A e. RR )
28 2nn 
 |-  2 e. NN
29 simpr 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> k e. NN )
30 nnmulcl 
 |-  ( ( 2 e. NN /\ k e. NN ) -> ( 2 x. k ) e. NN )
31 28 29 30 sylancr 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( 2 x. k ) e. NN )
32 31 nnnn0d 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( 2 x. k ) e. NN0 )
33 27 32 reexpcld 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ ( 2 x. k ) ) e. RR )
34 31 nnred 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( 2 x. k ) e. RR )
35 2 ad2antrr 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> B e. RR )
36 34 35 remulcld 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( 2 x. k ) x. B ) e. RR )
37 0red 
 |-  ( ( ph /\ 1 < A ) -> 0 e. RR )
38 9 a1i 
 |-  ( ( ph /\ 1 < A ) -> 1 e. RR )
39 0lt1 
 |-  0 < 1
40 39 a1i 
 |-  ( ( ph /\ 1 < A ) -> 0 < 1 )
41 37 38 10 40 8 lttrd 
 |-  ( ( ph /\ 1 < A ) -> 0 < A )
42 10 41 elrpd 
 |-  ( ( ph /\ 1 < A ) -> A e. RR+ )
43 nnz 
 |-  ( k e. NN -> k e. ZZ )
44 rpexpcl 
 |-  ( ( A e. RR+ /\ k e. ZZ ) -> ( A ^ k ) e. RR+ )
45 42 43 44 syl2an 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ k ) e. RR+ )
46 peano2re 
 |-  ( ( ( A - 1 ) x. k ) e. RR -> ( ( ( A - 1 ) x. k ) + 1 ) e. RR )
47 25 46 syl 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. k ) + 1 ) e. RR )
48 25 ltp1d 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( A - 1 ) x. k ) < ( ( ( A - 1 ) x. k ) + 1 ) )
49 17 adantl 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> k e. NN0 )
50 42 adantr 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> A e. RR+ )
51 50 rpge0d 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> 0 <_ A )
52 bernneq2 
 |-  ( ( A e. RR /\ k e. NN0 /\ 0 <_ A ) -> ( ( ( A - 1 ) x. k ) + 1 ) <_ ( A ^ k ) )
53 27 49 51 52 syl3anc 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. k ) + 1 ) <_ ( A ^ k ) )
54 25 47 19 48 53 ltletrd 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( A - 1 ) x. k ) < ( A ^ k ) )
55 25 19 45 54 ltmul1dd 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. k ) x. ( A ^ k ) ) < ( ( A ^ k ) x. ( A ^ k ) ) )
56 24 recnd 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> k e. CC )
57 56 2timesd 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( 2 x. k ) = ( k + k ) )
58 57 oveq2d 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ ( 2 x. k ) ) = ( A ^ ( k + k ) ) )
59 27 recnd 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> A e. CC )
60 59 49 49 expaddd 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ ( k + k ) ) = ( ( A ^ k ) x. ( A ^ k ) ) )
61 58 60 eqtrd 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ ( 2 x. k ) ) = ( ( A ^ k ) x. ( A ^ k ) ) )
62 55 61 breqtrrd 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. k ) x. ( A ^ k ) ) < ( A ^ ( 2 x. k ) ) )
63 oveq2 
 |-  ( n = ( 2 x. k ) -> ( A ^ n ) = ( A ^ ( 2 x. k ) ) )
64 oveq1 
 |-  ( n = ( 2 x. k ) -> ( n x. B ) = ( ( 2 x. k ) x. B ) )
65 63 64 breq12d 
 |-  ( n = ( 2 x. k ) -> ( ( A ^ n ) <_ ( n x. B ) <-> ( A ^ ( 2 x. k ) ) <_ ( ( 2 x. k ) x. B ) ) )
66 3 ralrimiva 
 |-  ( ph -> A. n e. NN ( A ^ n ) <_ ( n x. B ) )
67 66 ad2antrr 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> A. n e. NN ( A ^ n ) <_ ( n x. B ) )
68 65 67 31 rspcdva 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ ( 2 x. k ) ) <_ ( ( 2 x. k ) x. B ) )
69 26 33 36 62 68 ltletrd 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. k ) x. ( A ^ k ) ) < ( ( 2 x. k ) x. B ) )
70 22 recnd 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A - 1 ) e. CC )
71 19 recnd 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ k ) e. CC )
72 70 71 56 mul32d 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. ( A ^ k ) ) x. k ) = ( ( ( A - 1 ) x. k ) x. ( A ^ k ) ) )
73 2cnd 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> 2 e. CC )
74 35 recnd 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> B e. CC )
75 73 74 56 mul32d 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( 2 x. B ) x. k ) = ( ( 2 x. k ) x. B ) )
76 69 72 75 3brtr4d 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. ( A ^ k ) ) x. k ) < ( ( 2 x. B ) x. k ) )
77 22 19 remulcld 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( A - 1 ) x. ( A ^ k ) ) e. RR )
78 7 adantr 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( 2 x. B ) e. RR )
79 nngt0 
 |-  ( k e. NN -> 0 < k )
80 79 adantl 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> 0 < k )
81 ltmul1 
 |-  ( ( ( ( A - 1 ) x. ( A ^ k ) ) e. RR /\ ( 2 x. B ) e. RR /\ ( k e. RR /\ 0 < k ) ) -> ( ( ( A - 1 ) x. ( A ^ k ) ) < ( 2 x. B ) <-> ( ( ( A - 1 ) x. ( A ^ k ) ) x. k ) < ( ( 2 x. B ) x. k ) ) )
82 77 78 24 80 81 syl112anc 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. ( A ^ k ) ) < ( 2 x. B ) <-> ( ( ( A - 1 ) x. ( A ^ k ) ) x. k ) < ( ( 2 x. B ) x. k ) ) )
83 76 82 mpbird 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( A - 1 ) x. ( A ^ k ) ) < ( 2 x. B ) )
84 13 rpgt0d 
 |-  ( ( ph /\ 1 < A ) -> 0 < ( A - 1 ) )
85 84 adantr 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> 0 < ( A - 1 ) )
86 ltmuldiv2 
 |-  ( ( ( A ^ k ) e. RR /\ ( 2 x. B ) e. RR /\ ( ( A - 1 ) e. RR /\ 0 < ( A - 1 ) ) ) -> ( ( ( A - 1 ) x. ( A ^ k ) ) < ( 2 x. B ) <-> ( A ^ k ) < ( ( 2 x. B ) / ( A - 1 ) ) ) )
87 19 78 22 85 86 syl112anc 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. ( A ^ k ) ) < ( 2 x. B ) <-> ( A ^ k ) < ( ( 2 x. B ) / ( A - 1 ) ) ) )
88 83 87 mpbid 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ k ) < ( ( 2 x. B ) / ( A - 1 ) ) )
89 19 20 88 ltnsymd 
 |-  ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> -. ( ( 2 x. B ) / ( A - 1 ) ) < ( A ^ k ) )
90 89 nrexdv 
 |-  ( ( ph /\ 1 < A ) -> -. E. k e. NN ( ( 2 x. B ) / ( A - 1 ) ) < ( A ^ k ) )
91 16 90 pm2.65da 
 |-  ( ph -> -. 1 < A )
92 lenlt 
 |-  ( ( A e. RR /\ 1 e. RR ) -> ( A <_ 1 <-> -. 1 < A ) )
93 1 9 92 sylancl 
 |-  ( ph -> ( A <_ 1 <-> -. 1 < A ) )
94 91 93 mpbird 
 |-  ( ph -> A <_ 1 )