Theorem chtppilimlem2 27783

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

Hypotheses

Ref	Expression
chtppilim.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)
chtppilim.2	⊢ (𝜑 → 𝐴 < 1)

Assertion

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

Distinct variable groups:   𝑥,𝑧,𝐴   𝜑,𝑥,𝑧

Proof of Theorem chtppilimlem2

Step	Hyp	Ref	Expression
1		2re 12398	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
2		elicopnf 13557	. . . . . . . . . 10 ⊢ (2 ∈ ℝ → (𝑥 ∈ (2[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 2 ≤ 𝑥)))
3	1, 2	ax-mp 5	. . . . . . . . 9 ⊢ (𝑥 ∈ (2[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 2 ≤ 𝑥))
4	3	bilani 510	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥 ∈ ℝ ∧ 2 ≤ 𝑥))
5	4	simpld 500	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 𝑥 ∈ ℝ)
6		0red 11292	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 0 ∈ ℝ)
7	1	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 2 ∈ ℝ)
8		2pos 12428	. . . . . . . . 9 ⊢ 0 < 2
9	8	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 0 < 2)
10	4	simprd 501	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 2 ≤ 𝑥)
11	6, 7, 5, 9, 10	ltletrd 11451	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 0 < 𝑥)
12	5, 11	elrpd 13142	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 𝑥 ∈ ℝ+)
13		chtppilim.1	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
14	13	rpred 13145	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ)
15	14	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 𝐴 ∈ ℝ)
16	12, 15	rpcxpcld 27043	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥↑𝑐𝐴) ∈ ℝ+)
17		ppinncl 27483	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 2 ≤ 𝑥) → (π‘𝑥) ∈ ℕ)
18	4, 17	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (π‘𝑥) ∈ ℕ)
19	18	nnrpd 13143	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (π‘𝑥) ∈ ℝ+)
20	16, 19	rpdivcld 13162	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥↑𝑐𝐴) / (π‘𝑥)) ∈ ℝ+)
21	20	ralrimiva 3155	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ (2[,)+∞)((𝑥↑𝑐𝐴) / (π‘𝑥)) ∈ ℝ+)
22		chtppilim.2	. . . 4 ⊢ (𝜑 → 𝐴 < 1)
23		1re 11289	. . . . 5 ⊢ 1 ∈ ℝ
24		difrp 13141	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 < 1 ↔ (1 − 𝐴) ∈ ℝ+))
25	14, 23, 24	sylancl 598	. . . 4 ⊢ (𝜑 → (𝐴 < 1 ↔ (1 − 𝐴) ∈ ℝ+))
26	22, 25	mpbid 235	. . 3 ⊢ (𝜑 → (1 − 𝐴) ∈ ℝ+)
27		ovexd 7447	. . . . . 6 ⊢ (𝜑 → (2[,)+∞) ∈ V)
28	23	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 1 ∈ ℝ)
29		1lt2 12496	. . . . . . . . . . 11 ⊢ 1 < 2
30	29	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 1 < 2)
31	28, 7, 5, 30, 10	ltletrd 11451	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 1 < 𝑥)
32	5, 31	rplogcld 26939	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (log‘𝑥) ∈ ℝ+)
33	12, 32	rpdivcld 13162	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥 / (log‘𝑥)) ∈ ℝ+)
34	33, 19	rpdivcld 13162	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥 / (log‘𝑥)) / (π‘𝑥)) ∈ ℝ+)
35	26	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (1 − 𝐴) ∈ ℝ+)
36	35	rpred 13145	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (1 − 𝐴) ∈ ℝ)
37	12, 36	rpcxpcld 27043	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥↑𝑐(1 − 𝐴)) ∈ ℝ+)
38	32, 37	rpdivcld 13162	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴))) ∈ ℝ+)
39		eqidd 2762	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π‘𝑥))) = (𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π‘𝑥))))
40		eqidd 2762	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (2[,)+∞) ↦ ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))) = (𝑥 ∈ (2[,)+∞) ↦ ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))))
41	27, 34, 38, 39, 40	offval2 7702	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∘f · (𝑥 ∈ (2[,)+∞) ↦ ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴))))) = (𝑥 ∈ (2[,)+∞) ↦ (((𝑥 / (log‘𝑥)) / (π‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴))))))
42	33	rpcnd 13147	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥 / (log‘𝑥)) ∈ ℂ)
43	38	rpcnd 13147	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴))) ∈ ℂ)
44	19	rpcnne0d 13154	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((π‘𝑥) ∈ ℂ ∧ (π‘𝑥) ≠ 0))
45		div23 11974	. . . . . . . 8 ⊢ (((𝑥 / (log‘𝑥)) ∈ ℂ ∧ ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴))) ∈ ℂ ∧ ((π‘𝑥) ∈ ℂ ∧ (π‘𝑥) ≠ 0)) → (((𝑥 / (log‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))) / (π‘𝑥)) = (((𝑥 / (log‘𝑥)) / (π‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))))
46	42, 43, 44, 45	syl3anc 1398	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (((𝑥 / (log‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))) / (π‘𝑥)) = (((𝑥 / (log‘𝑥)) / (π‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))))
47	32	rpcnne0d 13154	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((log‘𝑥) ∈ ℂ ∧ (log‘𝑥) ≠ 0))
48	37	rpcnne0d 13154	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥↑𝑐(1 − 𝐴)) ∈ ℂ ∧ (𝑥↑𝑐(1 − 𝐴)) ≠ 0))
49	5	recnd 11318	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 𝑥 ∈ ℂ)
50		dmdcan 12008	. . . . . . . . . 10 ⊢ ((((log‘𝑥) ∈ ℂ ∧ (log‘𝑥) ≠ 0) ∧ ((𝑥↑𝑐(1 − 𝐴)) ∈ ℂ ∧ (𝑥↑𝑐(1 − 𝐴)) ≠ 0) ∧ 𝑥 ∈ ℂ) → (((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴))) · (𝑥 / (log‘𝑥))) = (𝑥 / (𝑥↑𝑐(1 − 𝐴))))
51	47, 48, 49, 50	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴))) · (𝑥 / (log‘𝑥))) = (𝑥 / (𝑥↑𝑐(1 − 𝐴))))
52	42, 43	mulcomd 11311	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥 / (log‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))) = (((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴))) · (𝑥 / (log‘𝑥))))
53	12	rpcnne0d 13154	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
54		ax-1cn 11239	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
55	54	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 1 ∈ ℂ)
56	35	rpcnd 13147	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (1 − 𝐴) ∈ ℂ)
57		cxpsub 26992	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ 1 ∈ ℂ ∧ (1 − 𝐴) ∈ ℂ) → (𝑥↑𝑐(1 − (1 − 𝐴))) = ((𝑥↑𝑐1) / (𝑥↑𝑐(1 − 𝐴))))
58	53, 55, 56, 57	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥↑𝑐(1 − (1 − 𝐴))) = ((𝑥↑𝑐1) / (𝑥↑𝑐(1 − 𝐴))))
59	15	recnd 11318	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 𝐴 ∈ ℂ)
60		nncan 11568	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 − (1 − 𝐴)) = 𝐴)
61	54, 59, 60	sylancr 599	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (1 − (1 − 𝐴)) = 𝐴)
62	61	oveq2d 7428	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥↑𝑐(1 − (1 − 𝐴))) = (𝑥↑𝑐𝐴))
63	58, 62	eqtr3d 2798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥↑𝑐1) / (𝑥↑𝑐(1 − 𝐴))) = (𝑥↑𝑐𝐴))
64	49	cxp1d 27016	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥↑𝑐1) = 𝑥)
65	64	oveq1d 7427	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥↑𝑐1) / (𝑥↑𝑐(1 − 𝐴))) = (𝑥 / (𝑥↑𝑐(1 − 𝐴))))
66	63, 65	eqtr3d 2798	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥↑𝑐𝐴) = (𝑥 / (𝑥↑𝑐(1 − 𝐴))))
67	51, 52, 66	3eqtr4d 2806	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥 / (log‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))) = (𝑥↑𝑐𝐴))
68	67	oveq1d 7427	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (((𝑥 / (log‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))) / (π‘𝑥)) = ((𝑥↑𝑐𝐴) / (π‘𝑥)))
69	46, 68	eqtr3d 2798	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (((𝑥 / (log‘𝑥)) / (π‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))) = ((𝑥↑𝑐𝐴) / (π‘𝑥)))
70	69	mpteq2dva 5198	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (2[,)+∞) ↦ (((𝑥 / (log‘𝑥)) / (π‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴))))) = (𝑥 ∈ (2[,)+∞) ↦ ((𝑥↑𝑐𝐴) / (π‘𝑥))))
71	41, 70	eqtrd 2796	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∘f · (𝑥 ∈ (2[,)+∞) ↦ ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴))))) = (𝑥 ∈ (2[,)+∞) ↦ ((𝑥↑𝑐𝐴) / (π‘𝑥))))
72		chebbnd1 27781	. . . . 5 ⊢ (𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∈ 𝑂(1)
73	12	ex 418	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (2[,)+∞) → 𝑥 ∈ ℝ+))
74	73	ssrdv 3937	. . . . . 6 ⊢ (𝜑 → (2[,)+∞) ⊆ ℝ+)
75		cxploglim 27287	. . . . . . 7 ⊢ ((1 − 𝐴) ∈ ℝ+ → (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))) ⇝𝑟 0)
76	26, 75	syl 18	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))) ⇝𝑟 0)
77	74, 76	rlimres2 15708	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (2[,)+∞) ↦ ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))) ⇝𝑟 0)
78		o1rlimmul 15766	. . . . 5 ⊢ (((𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∈ 𝑂(1) ∧ (𝑥 ∈ (2[,)+∞) ↦ ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))) ⇝𝑟 0) → ((𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∘f · (𝑥 ∈ (2[,)+∞) ↦ ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴))))) ⇝𝑟 0)
79	72, 77, 78	sylancr 599	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∘f · (𝑥 ∈ (2[,)+∞) ↦ ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴))))) ⇝𝑟 0)
80	71, 79	eqbrtrrd 5129	. . 3 ⊢ (𝜑 → (𝑥 ∈ (2[,)+∞) ↦ ((𝑥↑𝑐𝐴) / (π‘𝑥))) ⇝𝑟 0)
81	21, 26, 80	rlimi 15660	. 2 ⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → (abs‘(((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0)) < (1 − 𝐴)))
82	20	rpcnd 13147	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥↑𝑐𝐴) / (π‘𝑥)) ∈ ℂ)
83	82	subid1d 11639	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0) = ((𝑥↑𝑐𝐴) / (π‘𝑥)))
84	83	fveq2d 6881	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (abs‘(((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0)) = (abs‘((𝑥↑𝑐𝐴) / (π‘𝑥))))
85	20	rpred 13145	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥↑𝑐𝐴) / (π‘𝑥)) ∈ ℝ)
86	20	rpge0d 13149	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 0 ≤ ((𝑥↑𝑐𝐴) / (π‘𝑥)))
87	85, 86	absidd 15570	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (abs‘((𝑥↑𝑐𝐴) / (π‘𝑥))) = ((𝑥↑𝑐𝐴) / (π‘𝑥)))
88	84, 87	eqtrd 2796	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (abs‘(((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0)) = ((𝑥↑𝑐𝐴) / (π‘𝑥)))
89	88	breq1d 5113	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((abs‘(((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0)) < (1 − 𝐴) ↔ ((𝑥↑𝑐𝐴) / (π‘𝑥)) < (1 − 𝐴)))
90	13	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (2[,)+∞) ∧ ((𝑥↑𝑐𝐴) / (π‘𝑥)) < (1 − 𝐴))) → 𝐴 ∈ ℝ+)
91	22	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (2[,)+∞) ∧ ((𝑥↑𝑐𝐴) / (π‘𝑥)) < (1 − 𝐴))) → 𝐴 < 1)
92		simprl 783	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (2[,)+∞) ∧ ((𝑥↑𝑐𝐴) / (π‘𝑥)) < (1 − 𝐴))) → 𝑥 ∈ (2[,)+∞))
93		simprr 785	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (2[,)+∞) ∧ ((𝑥↑𝑐𝐴) / (π‘𝑥)) < (1 − 𝐴))) → ((𝑥↑𝑐𝐴) / (π‘𝑥)) < (1 − 𝐴))
94	90, 91, 92, 93	chtppilimlem1 27782	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (2[,)+∞) ∧ ((𝑥↑𝑐𝐴) / (π‘𝑥)) < (1 − 𝐴))) → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥))
95	94	expr 462	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (((𝑥↑𝑐𝐴) / (π‘𝑥)) < (1 − 𝐴) → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥)))
96	89, 95	sylbid 243	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((abs‘(((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0)) < (1 − 𝐴) → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥)))
97	96	imim2d 58	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑧 ≤ 𝑥 → (abs‘(((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0)) < (1 − 𝐴)) → (𝑧 ≤ 𝑥 → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥))))
98	97	ralimdva 3175	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → (abs‘(((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0)) < (1 − 𝐴)) → ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥))))
99	98	reximdv 3178	. 2 ⊢ (𝜑 → (∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → (abs‘(((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0)) < (1 − 𝐴)) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥))))
100	81, 99	mpd 16	1 ⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  Vcvv 3451   class class class wbr 5103   ↦ cmpt 5186  ‘cfv 6531  (class class class)co 7412   ∘_f cof 7680  ℂcc 11179  ℝcr 11180  0cc0 11181  1c1 11182   · cmul 11186  +∞cpnf 11321   < clt 11324   ≤ cle 11325   − cmin 11522   / cdiv 11954  ℕcn 12316  2c2 12378  ℝ⁺crp 13101  [,)cico 13459  ↑cexp 14184  abscabs 15381   ⇝_𝑟 crli 15632  𝑂(1)co1 15633  logclog 26864  ↑_𝑐ccxp 26865  θccht 27400  πcppi 27403

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-inf2 9626  ax-cnex 11237  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-mulcom 11245  ax-addass 11246  ax-mulass 11247  ax-distr 11248  ax-i2m1 11249  ax-1ne0 11250  ax-1rid 11251  ax-rnegex 11252  ax-rrecex 11253  ax-cnre 11254  ax-pre-lttri 11255  ax-pre-lttrn 11256  ax-pre-ltadd 11257  ax-pre-mulgt0 11258  ax-pre-sup 11259  ax-addf 11260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-isom 6540  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7682  df-om 7867  df-1st 7990  df-2nd 7991  df-supp 8162  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8460  df-2o 8461  df-oadd 8464  df-er 8701  df-map 8833  df-pm 8834  df-ixp 8910  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fsupp 9338  df-fi 9387  df-sup 9418  df-inf 9419  df-oi 9488  df-dju 9963  df-card 10001  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11524  df-neg 11525  df-div 11955  df-nn 12317  df-2 12386  df-3 12387  df-4 12388  df-5 12389  df-6 12390  df-7 12391  df-8 12392  df-9 12393  df-n0 12588  df-xnn0 12661  df-z 12675  df-dec 12796  df-uz 12947  df-q 13057  df-rp 13102  df-xneg 13222  df-xadd 13223  df-xmul 13224  df-ioo 13461  df-ioc 13462  df-ico 13463  df-icc 13464  df-fz 13621  df-fzo 13769  df-fl 13912  df-mod 13990  df-seq 14125  df-exp 14185  df-fac 14398  df-bc 14427  df-hash 14455  df-shft 15200  df-cj 15246  df-re 15247  df-im 15248  df-sqrt 15382  df-abs 15383  df-limsup 15618  df-clim 15635  df-rlim 15636  df-o1 15637  df-lo1 15638  df-sum 15834  df-ef 16213  df-e 16214  df-sin 16215  df-cos 16216  df-pi 16218  df-dvds 16403  df-gcd 16645  df-prm 16827  df-pc 16995  df-struct 17305  df-sets 17322  df-slot 17340  df-ndx 17352  df-base 17368  df-ress 17389  df-plusg 17421  df-mulr 17422  df-starv 17423  df-sca 17424  df-vsca 17425  df-ip 17426  df-tset 17427  df-ple 17428  df-ds 17430  df-unif 17431  df-hom 17432  df-cco 17433  df-rest 17573  df-topn 17574  df-0g 17592  df-gsum 17593  df-topgen 17594  df-pt 17595  df-prds 17598  df-xrs 17654  df-qtop 17659  df-imas 17660  df-xps 17662  df-mre 17736  df-mrc 17737  df-acs 17739  df-mgm 18796  df-sgrp 18888  df-mnd 18904  df-submnd 18959  df-mulg 19258  df-cntz 19511  df-cmn 19976  df-psmet 21650  df-xmet 21651  df-met 21652  df-bl 21653  df-mopn 21654  df-fbas 21655  df-fg 21656  df-cnfld 21659  df-top 23192  df-topon 23209  df-topsp 23231  df-bases 23244  df-cld 23317  df-ntr 23318  df-cls 23319  df-nei 23396  df-lp 23434  df-perf 23435  df-cn 23525  df-cnp 23526  df-haus 23613  df-tx 23861  df-hmeo 24054  df-fil 24145  df-fm 24237  df-flim 24238  df-flf 24239  df-xms 24619  df-ms 24620  df-tms 24621  df-cncf 25179  df-limc 26166  df-dv 26167  df-log 26866  df-cxp 26867  df-cht 27406  df-ppi 27409

This theorem is used by:  chtppilim  27784