chtppilimlem2

	Ref	Expression
Hypotheses	chtppilim.1	$⊢ φ \to A \in ℝ^{+}$
	chtppilim.2	$⊢ φ \to A < 1$
Assertion	chtppilimlem2	$⊢ φ \to \exists z \in ℝ \forall x \in [2, +∞) (z \leq x \to A^{2} \underline{π} (x) \log x < θ (x))$

Proof

Step	Hyp	Ref	Expression
1		chtppilim.1	$⊢ φ \to A \in ℝ^{+}$
2		chtppilim.2	$⊢ φ \to A < 1$
3		simpr	$⊢ (φ \land x \in [2, +∞)) \to x \in [2, +∞)$
4		2re	$⊢ 2 \in ℝ$
5		elicopnf	$⊢ 2 \in ℝ \to (x \in [2, +∞) \leftrightarrow (x \in ℝ \land 2 \leq x))$
6	4 5	ax-mp	$⊢ x \in [2, +∞) \leftrightarrow (x \in ℝ \land 2 \leq x)$
7	3 6	sylib	$⊢ (φ \land x \in [2, +∞)) \to (x \in ℝ \land 2 \leq x)$
8	7	simpld	$⊢ (φ \land x \in [2, +∞)) \to x \in ℝ$
9		0red	$⊢ (φ \land x \in [2, +∞)) \to 0 \in ℝ$
10	4	a1i	$⊢ (φ \land x \in [2, +∞)) \to 2 \in ℝ$
11		2pos	$⊢ 0 < 2$
12	11	a1i	$⊢ (φ \land x \in [2, +∞)) \to 0 < 2$
13	7	simprd	$⊢ (φ \land x \in [2, +∞)) \to 2 \leq x$
14	9 10 8 12 13	ltletrd	$⊢ (φ \land x \in [2, +∞)) \to 0 < x$
15	8 14	elrpd	$⊢ (φ \land x \in [2, +∞)) \to x \in ℝ^{+}$
16	1	rpred	$⊢ φ \to A \in ℝ$
17	16	adantr	$⊢ (φ \land x \in [2, +∞)) \to A \in ℝ$
18	15 17	rpcxpcld	$⊢ (φ \land x \in [2, +∞)) \to x^{A} \in ℝ^{+}$
19		ppinncl	$⊢ (x \in ℝ \land 2 \leq x) \to \underline{π} (x) \in ℕ$
20	7 19	syl	$⊢ (φ \land x \in [2, +∞)) \to \underline{π} (x) \in ℕ$
21	20	nnrpd	$⊢ (φ \land x \in [2, +∞)) \to \underline{π} (x) \in ℝ^{+}$
22	18 21	rpdivcld	$⊢ (φ \land x \in [2, +∞)) \to \frac{x^{A}}{\underline{π} (x)} \in ℝ^{+}$
23	22	ralrimiva	$⊢ φ \to \forall x \in [2, +∞) \frac{x^{A}}{\underline{π} (x)} \in ℝ^{+}$
24		1re	$⊢ 1 \in ℝ$
25		difrp	$⊢ (A \in ℝ \land 1 \in ℝ) \to (A < 1 \leftrightarrow 1 - A \in ℝ^{+})$
26	16 24 25	sylancl	$⊢ φ \to (A < 1 \leftrightarrow 1 - A \in ℝ^{+})$
27	2 26	mpbid	$⊢ φ \to 1 - A \in ℝ^{+}$
28		ovexd	$⊢ φ \to [2, +∞) \in V$
29	24	a1i	$⊢ (φ \land x \in [2, +∞)) \to 1 \in ℝ$
30		1lt2	$⊢ 1 < 2$
31	30	a1i	$⊢ (φ \land x \in [2, +∞)) \to 1 < 2$
32	29 10 8 31 13	ltletrd	$⊢ (φ \land x \in [2, +∞)) \to 1 < x$
33	8 32	rplogcld	$⊢ (φ \land x \in [2, +∞)) \to \log x \in ℝ^{+}$
34	15 33	rpdivcld	$⊢ (φ \land x \in [2, +∞)) \to \frac{x}{\log x} \in ℝ^{+}$
35	34 21	rpdivcld	$⊢ (φ \land x \in [2, +∞)) \to \frac{\frac{x}{\log x}}{\underline{π} (x)} \in ℝ^{+}$
36	27	adantr	$⊢ (φ \land x \in [2, +∞)) \to 1 - A \in ℝ^{+}$
37	36	rpred	$⊢ (φ \land x \in [2, +∞)) \to 1 - A \in ℝ$
38	15 37	rpcxpcld	$⊢ (φ \land x \in [2, +∞)) \to x^{1 - A} \in ℝ^{+}$
39	33 38	rpdivcld	$⊢ (φ \land x \in [2, +∞)) \to \frac{\log x}{x^{1 - A}} \in ℝ^{+}$
40		eqidd	$⊢ φ \to (x \in [2, +∞) ⟼ \frac{\frac{x}{\log x}}{\underline{π} (x)}) = (x \in [2, +∞) ⟼ \frac{\frac{x}{\log x}}{\underline{π} (x)})$
41		eqidd	$⊢ φ \to (x \in [2, +∞) ⟼ \frac{\log x}{x^{1 - A}}) = (x \in [2, +∞) ⟼ \frac{\log x}{x^{1 - A}})$
42	28 35 39 40 41	offval2	$⊢ φ \to (x \in [2, +∞) ⟼ \frac{\frac{x}{\log x}}{\underline{π} (x)}) \times_{f} (x \in [2, +∞) ⟼ \frac{\log x}{x^{1 - A}}) = (x \in [2, +∞) ⟼ (\frac{\frac{x}{\log x}}{\underline{π} (x)}) (\frac{\log x}{x^{1 - A}}))$
43	34	rpcnd	$⊢ (φ \land x \in [2, +∞)) \to \frac{x}{\log x} \in ℂ$
44	39	rpcnd	$⊢ (φ \land x \in [2, +∞)) \to \frac{\log x}{x^{1 - A}} \in ℂ$
45	21	rpcnne0d	$⊢ (φ \land x \in [2, +∞)) \to (\underline{π} (x) \in ℂ \land \underline{π} (x) \neq 0)$
46		div23	$⊢ (\frac{x}{\log x} \in ℂ \land \frac{\log x}{x^{1 - A}} \in ℂ \land (\underline{π} (x) \in ℂ \land \underline{π} (x) \neq 0)) \to \frac{(\frac{x}{\log x}) (\frac{\log x}{x^{1 - A}})}{\underline{π} (x)} = (\frac{\frac{x}{\log x}}{\underline{π} (x)}) (\frac{\log x}{x^{1 - A}})$
47	43 44 45 46	syl3anc	$⊢ (φ \land x \in [2, +∞)) \to \frac{(\frac{x}{\log x}) (\frac{\log x}{x^{1 - A}})}{\underline{π} (x)} = (\frac{\frac{x}{\log x}}{\underline{π} (x)}) (\frac{\log x}{x^{1 - A}})$
48	33	rpcnne0d	$⊢ (φ \land x \in [2, +∞)) \to (\log x \in ℂ \land \log x \neq 0)$
49	38	rpcnne0d	$⊢ (φ \land x \in [2, +∞)) \to (x^{1 - A} \in ℂ \land x^{1 - A} \neq 0)$
50	8	recnd	$⊢ (φ \land x \in [2, +∞)) \to x \in ℂ$
51		dmdcan	$⊢ ((\log x \in ℂ \land \log x \neq 0) \land (x^{1 - A} \in ℂ \land x^{1 - A} \neq 0) \land x \in ℂ) \to (\frac{\log x}{x^{1 - A}}) (\frac{x}{\log x}) = \frac{x}{x^{1 - A}}$
52	48 49 50 51	syl3anc	$⊢ (φ \land x \in [2, +∞)) \to (\frac{\log x}{x^{1 - A}}) (\frac{x}{\log x}) = \frac{x}{x^{1 - A}}$
53	43 44	mulcomd	$⊢ (φ \land x \in [2, +∞)) \to (\frac{x}{\log x}) (\frac{\log x}{x^{1 - A}}) = (\frac{\log x}{x^{1 - A}}) (\frac{x}{\log x})$
54	15	rpcnne0d	$⊢ (φ \land x \in [2, +∞)) \to (x \in ℂ \land x \neq 0)$
55		ax-1cn	$⊢ 1 \in ℂ$
56	55	a1i	$⊢ (φ \land x \in [2, +∞)) \to 1 \in ℂ$
57	36	rpcnd	$⊢ (φ \land x \in [2, +∞)) \to 1 - A \in ℂ$
58		cxpsub	$⊢ ((x \in ℂ \land x \neq 0) \land 1 \in ℂ \land 1 - A \in ℂ) \to x^{1 - (1 - A)} = \frac{x^{1}}{x^{1 - A}}$
59	54 56 57 58	syl3anc	$⊢ (φ \land x \in [2, +∞)) \to x^{1 - (1 - A)} = \frac{x^{1}}{x^{1 - A}}$
60	17	recnd	$⊢ (φ \land x \in [2, +∞)) \to A \in ℂ$
61		nncan	$⊢ (1 \in ℂ \land A \in ℂ) \to 1 - (1 - A) = A$
62	55 60 61	sylancr	$⊢ (φ \land x \in [2, +∞)) \to 1 - (1 - A) = A$
63	62	oveq2d	$⊢ (φ \land x \in [2, +∞)) \to x^{1 - (1 - A)} = x^{A}$
64	59 63	eqtr3d	$⊢ (φ \land x \in [2, +∞)) \to \frac{x^{1}}{x^{1 - A}} = x^{A}$
65	50	cxp1d	$⊢ (φ \land x \in [2, +∞)) \to x^{1} = x$
66	65	oveq1d	$⊢ (φ \land x \in [2, +∞)) \to \frac{x^{1}}{x^{1 - A}} = \frac{x}{x^{1 - A}}$
67	64 66	eqtr3d	$⊢ (φ \land x \in [2, +∞)) \to x^{A} = \frac{x}{x^{1 - A}}$
68	52 53 67	3eqtr4d	$⊢ (φ \land x \in [2, +∞)) \to (\frac{x}{\log x}) (\frac{\log x}{x^{1 - A}}) = x^{A}$
69	68	oveq1d	$⊢ (φ \land x \in [2, +∞)) \to \frac{(\frac{x}{\log x}) (\frac{\log x}{x^{1 - A}})}{\underline{π} (x)} = \frac{x^{A}}{\underline{π} (x)}$
70	47 69	eqtr3d	$⊢ (φ \land x \in [2, +∞)) \to (\frac{\frac{x}{\log x}}{\underline{π} (x)}) (\frac{\log x}{x^{1 - A}}) = \frac{x^{A}}{\underline{π} (x)}$
71	70	mpteq2dva	$⊢ φ \to (x \in [2, +∞) ⟼ (\frac{\frac{x}{\log x}}{\underline{π} (x)}) (\frac{\log x}{x^{1 - A}})) = (x \in [2, +∞) ⟼ \frac{x^{A}}{\underline{π} (x)})$
72	42 71	eqtrd	$⊢ φ \to (x \in [2, +∞) ⟼ \frac{\frac{x}{\log x}}{\underline{π} (x)}) \times_{f} (x \in [2, +∞) ⟼ \frac{\log x}{x^{1 - A}}) = (x \in [2, +∞) ⟼ \frac{x^{A}}{\underline{π} (x)})$
73		chebbnd1	$⊢ (x \in [2, +∞) ⟼ \frac{\frac{x}{\log x}}{\underline{π} (x)}) \in 𝑂 (1)$
74	15	ex	$⊢ φ \to (x \in [2, +∞) \to x \in ℝ^{+})$
75	74	ssrdv	$⊢ φ \to [2, +∞) \subseteq ℝ^{+}$
76		cxploglim	$⊢ 1 - A \in ℝ^{+} \to (x \in ℝ^{+} ⟼ \frac{\log x}{x^{1 - A}}) \underset{ℝ}{⇝} 0$
77	27 76	syl	$⊢ φ \to (x \in ℝ^{+} ⟼ \frac{\log x}{x^{1 - A}}) \underset{ℝ}{⇝} 0$
78	75 77	rlimres2	$⊢ φ \to (x \in [2, +∞) ⟼ \frac{\log x}{x^{1 - A}}) \underset{ℝ}{⇝} 0$
79		o1rlimmul	$⊢ ((x \in [2, +∞) ⟼ \frac{\frac{x}{\log x}}{\underline{π} (x)}) \in 𝑂 (1) \land (x \in [2, +∞) ⟼ \frac{\log x}{x^{1 - A}}) \underset{ℝ}{⇝} 0) \to ((x \in [2, +∞) ⟼ \frac{\frac{x}{\log x}}{\underline{π} (x)}) \times_{f} (x \in [2, +∞) ⟼ \frac{\log x}{x^{1 - A}})) \underset{ℝ}{⇝} 0$
80	73 78 79	sylancr	$⊢ φ \to ((x \in [2, +∞) ⟼ \frac{\frac{x}{\log x}}{\underline{π} (x)}) \times_{f} (x \in [2, +∞) ⟼ \frac{\log x}{x^{1 - A}})) \underset{ℝ}{⇝} 0$
81	72 80	eqbrtrrd	$⊢ φ \to (x \in [2, +∞) ⟼ \frac{x^{A}}{\underline{π} (x)}) \underset{ℝ}{⇝} 0$
82	23 27 81	rlimi	$⊢ φ \to \exists z \in ℝ \forall x \in [2, +∞) (z \leq x \to \|(\frac{x^{A}}{\underline{π} (x)}) - 0\| < 1 - A)$
83	22	rpcnd	$⊢ (φ \land x \in [2, +∞)) \to \frac{x^{A}}{\underline{π} (x)} \in ℂ$
84	83	subid1d	$⊢ (φ \land x \in [2, +∞)) \to (\frac{x^{A}}{\underline{π} (x)}) - 0 = \frac{x^{A}}{\underline{π} (x)}$
85	84	fveq2d	$⊢ (φ \land x \in [2, +∞)) \to \|(\frac{x^{A}}{\underline{π} (x)}) - 0\| = \|\frac{x^{A}}{\underline{π} (x)}\|$
86	22	rpred	$⊢ (φ \land x \in [2, +∞)) \to \frac{x^{A}}{\underline{π} (x)} \in ℝ$
87	22	rpge0d	$⊢ (φ \land x \in [2, +∞)) \to 0 \leq \frac{x^{A}}{\underline{π} (x)}$
88	86 87	absidd	$⊢ (φ \land x \in [2, +∞)) \to \|\frac{x^{A}}{\underline{π} (x)}\| = \frac{x^{A}}{\underline{π} (x)}$
89	85 88	eqtrd	$⊢ (φ \land x \in [2, +∞)) \to \|(\frac{x^{A}}{\underline{π} (x)}) - 0\| = \frac{x^{A}}{\underline{π} (x)}$
90	89	breq1d	$⊢ (φ \land x \in [2, +∞)) \to (\|(\frac{x^{A}}{\underline{π} (x)}) - 0\| < 1 - A \leftrightarrow \frac{x^{A}}{\underline{π} (x)} < 1 - A)$
91	1	adantr	$⊢ (φ \land (x \in [2, +∞) \land \frac{x^{A}}{\underline{π} (x)} < 1 - A)) \to A \in ℝ^{+}$
92	2	adantr	$⊢ (φ \land (x \in [2, +∞) \land \frac{x^{A}}{\underline{π} (x)} < 1 - A)) \to A < 1$
93		simprl	$⊢ (φ \land (x \in [2, +∞) \land \frac{x^{A}}{\underline{π} (x)} < 1 - A)) \to x \in [2, +∞)$
94		simprr	$⊢ (φ \land (x \in [2, +∞) \land \frac{x^{A}}{\underline{π} (x)} < 1 - A)) \to \frac{x^{A}}{\underline{π} (x)} < 1 - A$
95	91 92 93 94	chtppilimlem1	$⊢ (φ \land (x \in [2, +∞) \land \frac{x^{A}}{\underline{π} (x)} < 1 - A)) \to A^{2} \underline{π} (x) \log x < θ (x)$
96	95	expr	$⊢ (φ \land x \in [2, +∞)) \to (\frac{x^{A}}{\underline{π} (x)} < 1 - A \to A^{2} \underline{π} (x) \log x < θ (x))$
97	90 96	sylbid	$⊢ (φ \land x \in [2, +∞)) \to (\|(\frac{x^{A}}{\underline{π} (x)}) - 0\| < 1 - A \to A^{2} \underline{π} (x) \log x < θ (x))$
98	97	imim2d	$⊢ (φ \land x \in [2, +∞)) \to ((z \leq x \to \|(\frac{x^{A}}{\underline{π} (x)}) - 0\| < 1 - A) \to (z \leq x \to A^{2} \underline{π} (x) \log x < θ (x)))$
99	98	ralimdva	$⊢ φ \to (\forall x \in [2, +∞) (z \leq x \to \|(\frac{x^{A}}{\underline{π} (x)}) - 0\| < 1 - A) \to \forall x \in [2, +∞) (z \leq x \to A^{2} \underline{π} (x) \log x < θ (x)))$
100	99	reximdv	$⊢ φ \to (\exists z \in ℝ \forall x \in [2, +∞) (z \leq x \to \|(\frac{x^{A}}{\underline{π} (x)}) - 0\| < 1 - A) \to \exists z \in ℝ \forall x \in [2, +∞) (z \leq x \to A^{2} \underline{π} (x) \log x < θ (x)))$
101	82 100	mpd	$⊢ φ \to \exists z \in ℝ \forall x \in [2, +∞) (z \leq x \to A^{2} \underline{π} (x) \log x < θ (x))$

Metamath Proof Explorer

Theorem chtppilimlem2

Proof