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