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