Metamath Proof Explorer

Theorem chtppilimlem2

Description: Lemma for chtppilim . (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Hypotheses chtppilim.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
chtppilim.2 ⊢ ( 𝜑 → 𝐴 < 1 )
Assertion chtppilimlem2 ( 𝜑 → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( ( 𝐴 ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 chtppilim.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2 chtppilim.2 ⊢ ( 𝜑 → 𝐴 < 1 )
3 2re ⊢ 2 ∈ ℝ
4 elicopnf ⊢ ( 2 ∈ ℝ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) ) )
5 3 4 ax-mp ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) )
6 5 bilani ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) )
7 6 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 𝑥 ∈ ℝ )
8 0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 0 ∈ ℝ )
9 3 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 2 ∈ ℝ )
10 2pos ⊢ 0 < 2
11 10 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 0 < 2 )
12 6 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 2 ≤ 𝑥 )
13 8 9 7 11 12 ltletrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 0 < 𝑥 )
14 7 13 elrpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 𝑥 ∈ ℝ+ )
15 1 rpred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 𝐴 ∈ ℝ )
17 14 16 rpcxpcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 𝑥 ↑𝑐 𝐴 ) ∈ ℝ+ )
18 ppinncl ⊢ ( ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) → ( π ‘ 𝑥 ) ∈ ℕ )
19 6 18 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( π ‘ 𝑥 ) ∈ ℕ )
20 19 nnrpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( π ‘ 𝑥 ) ∈ ℝ+ )
21 17 20 rpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) ∈ ℝ+ )
22 21 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) ∈ ℝ+ )
23 1re ⊢ 1 ∈ ℝ
24 difrp ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐴 < 1 ↔ ( 1 − 𝐴 ) ∈ ℝ+ ) )
25 15 23 24 sylancl ⊢ ( 𝜑 → ( 𝐴 < 1 ↔ ( 1 − 𝐴 ) ∈ ℝ+ ) )
26 2 25 mpbid ⊢ ( 𝜑 → ( 1 − 𝐴 ) ∈ ℝ+ )
27 ovexd ⊢ ( 𝜑 → ( 2 [,) +∞ ) ∈ V )
28 23 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 1 ∈ ℝ )
29 1lt2 ⊢ 1 < 2
30 29 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 1 < 2 )
31 28 9 7 30 12 ltletrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 1 < 𝑥 )
32 7 31 rplogcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
33 14 32 rpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 𝑥 / ( log ‘ 𝑥 ) ) ∈ ℝ+ )
34 33 20 rpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ∈ ℝ+ )
35 26 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 1 − 𝐴 ) ∈ ℝ+ )
36 35 rpred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 1 − 𝐴 ) ∈ ℝ )
37 14 36 rpcxpcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ∈ ℝ+ )
38 32 37 rpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ∈ ℝ+ )
39 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) )
40 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) )
41 27 34 38 39 40 offval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) · ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) ) )
42 33 rpcnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 𝑥 / ( log ‘ 𝑥 ) ) ∈ ℂ )
43 38 rpcnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ∈ ℂ )
44 20 rpcnne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( π ‘ 𝑥 ) ∈ ℂ ∧ ( π ‘ 𝑥 ) ≠ 0 ) )
45 div23 ⊢ ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) ∈ ℂ ∧ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ∈ ℂ ∧ ( ( π ‘ 𝑥 ) ∈ ℂ ∧ ( π ‘ 𝑥 ) ≠ 0 ) ) → ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) · ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) / ( π ‘ 𝑥 ) ) = ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) · ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) )
46 42 43 44 45 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) · ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) / ( π ‘ 𝑥 ) ) = ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) · ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) )
47 32 rpcnne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( log ‘ 𝑥 ) ∈ ℂ ∧ ( log ‘ 𝑥 ) ≠ 0 ) )
48 37 rpcnne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ∈ ℂ ∧ ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ≠ 0 ) )
49 7 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 𝑥 ∈ ℂ )
50 dmdcan ⊢ ( ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ ( log ‘ 𝑥 ) ≠ 0 ) ∧ ( ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ∈ ℂ ∧ ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ≠ 0 ) ∧ 𝑥 ∈ ℂ ) → ( ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) · ( 𝑥 / ( log ‘ 𝑥 ) ) ) = ( 𝑥 / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) )
51 47 48 49 50 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) · ( 𝑥 / ( log ‘ 𝑥 ) ) ) = ( 𝑥 / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) )
52 42 43 mulcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( 𝑥 / ( log ‘ 𝑥 ) ) · ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) = ( ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) · ( 𝑥 / ( log ‘ 𝑥 ) ) ) )
53 14 rpcnne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
54 ax-1cn ⊢ 1 ∈ ℂ
55 54 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 1 ∈ ℂ )
56 35 rpcnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 1 − 𝐴 ) ∈ ℂ )
57 cxpsub ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ 1 ∈ ℂ ∧ ( 1 − 𝐴 ) ∈ ℂ ) → ( 𝑥 ↑𝑐 ( 1 − ( 1 − 𝐴 ) ) ) = ( ( 𝑥 ↑𝑐 1 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) )
58 53 55 56 57 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 𝑥 ↑𝑐 ( 1 − ( 1 − 𝐴 ) ) ) = ( ( 𝑥 ↑𝑐 1 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) )
59 16 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 𝐴 ∈ ℂ )
60 nncan ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 1 − ( 1 − 𝐴 ) ) = 𝐴 )
61 54 59 60 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 1 − ( 1 − 𝐴 ) ) = 𝐴 )
62 61 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 𝑥 ↑𝑐 ( 1 − ( 1 − 𝐴 ) ) ) = ( 𝑥 ↑𝑐 𝐴 ) )
63 58 62 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( 𝑥 ↑𝑐 1 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) = ( 𝑥 ↑𝑐 𝐴 ) )
64 49 cxp1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 𝑥 ↑𝑐 1 ) = 𝑥 )
65 64 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( 𝑥 ↑𝑐 1 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) = ( 𝑥 / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) )
66 63 65 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 𝑥 ↑𝑐 𝐴 ) = ( 𝑥 / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) )
67 51 52 66 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( 𝑥 / ( log ‘ 𝑥 ) ) · ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) = ( 𝑥 ↑𝑐 𝐴 ) )
68 67 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) · ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) / ( π ‘ 𝑥 ) ) = ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) )
69 46 68 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) · ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) = ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) )
70 69 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) · ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) ) )
71 41 70 eqtrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) ) )
72 chebbnd1 ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) ∈ 𝑂(1)
73 14 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ+ ) )
74 73 ssrdv ⊢ ( 𝜑 → ( 2 [,) +∞ ) ⊆ ℝ+ )
75 cxploglim ⊢ ( ( 1 − 𝐴 ) ∈ ℝ+ → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) ⇝𝑟 0 )
76 26 75 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) ⇝𝑟 0 )
77 74 76 rlimres2 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) ⇝𝑟 0 )
78 o1rlimmul ⊢ ( ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) ∈ 𝑂(1) ∧ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) ⇝𝑟 0 ) → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) ) ⇝𝑟 0 )
79 72 77 78 sylancr ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 − 𝐴 ) ) ) ) ) ⇝𝑟 0 )
80 71 79 eqbrtrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) ) ⇝𝑟 0 )
81 22 26 80 rlimi ⊢ ( 𝜑 → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) − 0 ) ) < ( 1 − 𝐴 ) ) )
82 21 rpcnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) ∈ ℂ )
83 82 subid1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) − 0 ) = ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) )
84 83 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( abs ‘ ( ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) − 0 ) ) = ( abs ‘ ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) ) )
85 21 rpred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) ∈ ℝ )
86 21 rpge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 0 ≤ ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) )
87 85 86 absidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( abs ‘ ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) ) = ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) )
88 84 87 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( abs ‘ ( ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) − 0 ) ) = ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) )
89 88 breq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( abs ‘ ( ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) − 0 ) ) < ( 1 − 𝐴 ) ↔ ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) < ( 1 − 𝐴 ) ) )
90 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) < ( 1 − 𝐴 ) ) ) → 𝐴 ∈ ℝ+ )
91 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) < ( 1 − 𝐴 ) ) ) → 𝐴 < 1 )
92 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) < ( 1 − 𝐴 ) ) ) → 𝑥 ∈ ( 2 [,) +∞ ) )
93 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) < ( 1 − 𝐴 ) ) ) → ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) < ( 1 − 𝐴 ) )
94 90 91 92 93 chtppilimlem1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) < ( 1 − 𝐴 ) ) ) → ( ( 𝐴 ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) )
95 94 expr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) < ( 1 − 𝐴 ) → ( ( 𝐴 ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) )
96 89 95 sylbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( abs ‘ ( ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) − 0 ) ) < ( 1 − 𝐴 ) → ( ( 𝐴 ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) )
97 96 imim2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) − 0 ) ) < ( 1 − 𝐴 ) ) → ( 𝑧 ≤ 𝑥 → ( ( 𝐴 ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) ) )
98 97 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) − 0 ) ) < ( 1 − 𝐴 ) ) → ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( ( 𝐴 ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) ) )
99 98 reximdv ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( ( 𝑥 ↑𝑐 𝐴 ) / ( π ‘ 𝑥 ) ) − 0 ) ) < ( 1 − 𝐴 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( ( 𝐴 ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) ) )
100 81 99 mpd ⊢ ( 𝜑 → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( ( 𝐴 ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) )