pnt3

Description: The Prime Number Theorem, version 3: the second Chebyshev function tends asymptotically to x . (Contributed by Mario Carneiro, 1-Jun-2016)

		Ref	Expression
	Assertion	pnt3	$⊢ (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \underset{ℝ}{⇝} 1$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ (a \in ℝ^{+} ⟼ ψ (a) - a) = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2	1	pntrmax	$⊢ \exists b \in ℝ^{+} \forall r \in ℝ^{+} \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r}\| \leq b$
3	1	pntibnd	$⊢ \exists c \in ℝ^{+} \exists l \in (0, 1) \forall e \in (0, 1) \exists r \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (r, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e)$
4		simpll	$⊢ ((b \in ℝ^{+} \land \forall r \in ℝ^{+} \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r}\| \leq b) \land ((c \in ℝ^{+} \land l \in (0, 1)) \land \forall e \in (0, 1) \exists r \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (r, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e))) \to b \in ℝ^{+}$
5		simplr	$⊢ ((b \in ℝ^{+} \land \forall r \in ℝ^{+} \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r}\| \leq b) \land ((c \in ℝ^{+} \land l \in (0, 1)) \land \forall e \in (0, 1) \exists r \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (r, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e))) \to \forall r \in ℝ^{+} \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r}\| \leq b$
6		fveq2	$⊢ r = x \to (a \in ℝ^{+} ⟼ ψ (a) - a) (r) = (a \in ℝ^{+} ⟼ ψ (a) - a) (x)$
7		id	$⊢ r = x \to r = x$
8	6 7	oveq12d	$⊢ r = x \to \frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r} = \frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (x)}{x}$
9	8	fveq2d	$⊢ r = x \to \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r}\| = \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (x)}{x}\|$
10	9	breq1d	$⊢ r = x \to (\|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r}\| \leq b \leftrightarrow \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (x)}{x}\| \leq b)$
11	10	cbvralvw	$⊢ \forall r \in ℝ^{+} \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r}\| \leq b \leftrightarrow \forall x \in ℝ^{+} \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (x)}{x}\| \leq b$
12	5 11	sylib	$⊢ ((b \in ℝ^{+} \land \forall r \in ℝ^{+} \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r}\| \leq b) \land ((c \in ℝ^{+} \land l \in (0, 1)) \land \forall e \in (0, 1) \exists r \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (r, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e))) \to \forall x \in ℝ^{+} \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (x)}{x}\| \leq b$
13		simprll	$⊢ ((b \in ℝ^{+} \land \forall r \in ℝ^{+} \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r}\| \leq b) \land ((c \in ℝ^{+} \land l \in (0, 1)) \land \forall e \in (0, 1) \exists r \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (r, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e))) \to c \in ℝ^{+}$
14		simprlr	$⊢ ((b \in ℝ^{+} \land \forall r \in ℝ^{+} \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r}\| \leq b) \land ((c \in ℝ^{+} \land l \in (0, 1)) \land \forall e \in (0, 1) \exists r \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (r, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e))) \to l \in (0, 1)$
15		eqid	$⊢ b + 1 = b + 1$
16		eqid	$⊢ (1 - (\frac{1}{b + 1})) (\frac{\frac{l}{32 c}}{{(b + 1)}^{2}}) = (1 - (\frac{1}{b + 1})) (\frac{\frac{l}{32 c}}{{(b + 1)}^{2}})$
17		simprr	$⊢ ((b \in ℝ^{+} \land \forall r \in ℝ^{+} \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r}\| \leq b) \land ((c \in ℝ^{+} \land l \in (0, 1)) \land \forall e \in (0, 1) \exists r \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (r, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e))) \to \forall e \in (0, 1) \exists r \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (r, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e)$
18		breq2	$⊢ z = g \to (y < z \leftrightarrow y < g)$
19		oveq2	$⊢ z = g \to (1 + l e) z = (1 + l e) g$
20	19	breq1d	$⊢ z = g \to ((1 + l e) z < k y \leftrightarrow (1 + l e) g < k y)$
21	18 20	anbi12d	$⊢ z = g \to ((y < z \land (1 + l e) z < k y) \leftrightarrow (y < g \land (1 + l e) g < k y))$
22		id	$⊢ z = g \to z = g$
23	22 19	oveq12d	$⊢ z = g \to [z, (1 + l e) z] = [g, (1 + l e) g]$
24	23	raleqdv	$⊢ z = g \to (\forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e \leftrightarrow \forall u \in [g, (1 + l e) g] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e)$
25	21 24	anbi12d	$⊢ z = g \to (((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e) \leftrightarrow ((y < g \land (1 + l e) g < k y) \land \forall u \in [g, (1 + l e) g] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e))$
26	25	cbvrexvw	$⊢ \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e) \leftrightarrow \exists g \in ℝ^{+} ((y < g \land (1 + l e) g < k y) \land \forall u \in [g, (1 + l e) g] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e)$
27		breq1	$⊢ y = f \to (y < g \leftrightarrow f < g)$
28		oveq2	$⊢ y = f \to k y = k f$
29	28	breq2d	$⊢ y = f \to ((1 + l e) g < k y \leftrightarrow (1 + l e) g < k f)$
30	27 29	anbi12d	$⊢ y = f \to ((y < g \land (1 + l e) g < k y) \leftrightarrow (f < g \land (1 + l e) g < k f))$
31	30	anbi1d	$⊢ y = f \to (((y < g \land (1 + l e) g < k y) \land \forall u \in [g, (1 + l e) g] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e) \leftrightarrow ((f < g \land (1 + l e) g < k f) \land \forall u \in [g, (1 + l e) g] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e))$
32	31	rexbidv	$⊢ y = f \to (\exists g \in ℝ^{+} ((y < g \land (1 + l e) g < k y) \land \forall u \in [g, (1 + l e) g] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e) \leftrightarrow \exists g \in ℝ^{+} ((f < g \land (1 + l e) g < k f) \land \forall u \in [g, (1 + l e) g] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e))$
33	26 32	bitrid	$⊢ y = f \to (\exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e) \leftrightarrow \exists g \in ℝ^{+} ((f < g \land (1 + l e) g < k f) \land \forall u \in [g, (1 + l e) g] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e))$
34	33	cbvralvw	$⊢ \forall y \in (r, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e) \leftrightarrow \forall f \in (r, +∞) \exists g \in ℝ^{+} ((f < g \land (1 + l e) g < k f) \land \forall u \in [g, (1 + l e) g] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e)$
35		oveq1	$⊢ r = x \to (r, +∞) = (x, +∞)$
36	35	raleqdv	$⊢ r = x \to (\forall f \in (r, +∞) \exists g \in ℝ^{+} ((f < g \land (1 + l e) g < k f) \land \forall u \in [g, (1 + l e) g] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e) \leftrightarrow \forall f \in (x, +∞) \exists g \in ℝ^{+} ((f < g \land (1 + l e) g < k f) \land \forall u \in [g, (1 + l e) g] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e))$
37	34 36	bitrid	$⊢ r = x \to (\forall y \in (r, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e) \leftrightarrow \forall f \in (x, +∞) \exists g \in ℝ^{+} ((f < g \land (1 + l e) g < k f) \land \forall u \in [g, (1 + l e) g] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e))$
38	37	ralbidv	$⊢ r = x \to (\forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (r, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e) \leftrightarrow \forall k \in [e^{\frac{c}{e}}, +∞) \forall f \in (x, +∞) \exists g \in ℝ^{+} ((f < g \land (1 + l e) g < k f) \land \forall u \in [g, (1 + l e) g] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e))$
39	38	cbvrexvw	$⊢ \exists r \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (r, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e) \leftrightarrow \exists x \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall f \in (x, +∞) \exists g \in ℝ^{+} ((f < g \land (1 + l e) g < k f) \land \forall u \in [g, (1 + l e) g] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e)$
40	39	ralbii	$⊢ \forall e \in (0, 1) \exists r \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (r, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e) \leftrightarrow \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall f \in (x, +∞) \exists g \in ℝ^{+} ((f < g \land (1 + l e) g < k f) \land \forall u \in [g, (1 + l e) g] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e)$
41	17 40	sylib	$⊢ ((b \in ℝ^{+} \land \forall r \in ℝ^{+} \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r}\| \leq b) \land ((c \in ℝ^{+} \land l \in (0, 1)) \land \forall e \in (0, 1) \exists r \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (r, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e))) \to \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall f \in (x, +∞) \exists g \in ℝ^{+} ((f < g \land (1 + l e) g < k f) \land \forall u \in [g, (1 + l e) g] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e)$
42	1 4 12 13 14 15 16 41	pntleml	$⊢ ((b \in ℝ^{+} \land \forall r \in ℝ^{+} \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r}\| \leq b) \land ((c \in ℝ^{+} \land l \in (0, 1)) \land \forall e \in (0, 1) \exists r \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (r, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e))) \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \underset{ℝ}{⇝} 1$
43	42	expr	$⊢ ((b \in ℝ^{+} \land \forall r \in ℝ^{+} \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r}\| \leq b) \land (c \in ℝ^{+} \land l \in (0, 1))) \to (\forall e \in (0, 1) \exists r \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (r, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e) \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \underset{ℝ}{⇝} 1)$
44	43	rexlimdvva	$⊢ (b \in ℝ^{+} \land \forall r \in ℝ^{+} \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r}\| \leq b) \to (\exists c \in ℝ^{+} \exists l \in (0, 1) \forall e \in (0, 1) \exists r \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (r, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + l e) z < k y) \land \forall u \in [z, (1 + l e) z] \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (u)}{u}\| \leq e) \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \underset{ℝ}{⇝} 1)$
45	3 44	mpi	$⊢ (b \in ℝ^{+} \land \forall r \in ℝ^{+} \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r}\| \leq b) \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \underset{ℝ}{⇝} 1$
46	45	rexlimiva	$⊢ \exists b \in ℝ^{+} \forall r \in ℝ^{+} \|\frac{(a \in ℝ^{+} ⟼ ψ (a) - a) (r)}{r}\| \leq b \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \underset{ℝ}{⇝} 1$
47	2 46	ax-mp	$⊢ (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \underset{ℝ}{⇝} 1$

Metamath Proof Explorer

Theorem pnt3

Proof