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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ostth2lem1.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ostth2lem1.3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ↑ 𝑛 ) ≤ ( 𝑛 · 𝐵 ) )
Assertion ostth2lem1 ( 𝜑 → 𝐴 ≤ 1 )

Proof

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