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 ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) )