pntrmax

Description: There is a bound on the residual valid for all x . (Contributed by Mario Carneiro, 9-Apr-2016)

		Ref	Expression
	Hypothesis	pntrval.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	Assertion	pntrmax	$⊢ \exists c \in ℝ^{+} \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq c$

Proof

Step	Hyp	Ref	Expression
1		pntrval.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
3	2	a1i	$⊢ ⊤ \to ℝ^{+} \subseteq ℝ$
4		1red	$⊢ ⊤ \to 1 \in ℝ$
5	1	pntrval	$⊢ x \in ℝ^{+} \to R (x) = ψ (x) - x$
6		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
7		chpcl	$⊢ x \in ℝ \to ψ (x) \in ℝ$
8	6 7	syl	$⊢ x \in ℝ^{+} \to ψ (x) \in ℝ$
9	8 6	resubcld	$⊢ x \in ℝ^{+} \to ψ (x) - x \in ℝ$
10	5 9	eqeltrd	$⊢ x \in ℝ^{+} \to R (x) \in ℝ$
11		rerpdivcl	$⊢ (R (x) \in ℝ \land x \in ℝ^{+}) \to \frac{R (x)}{x} \in ℝ$
12	10 11	mpancom	$⊢ x \in ℝ^{+} \to \frac{R (x)}{x} \in ℝ$
13	12	recnd	$⊢ x \in ℝ^{+} \to \frac{R (x)}{x} \in ℂ$
14	13	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{R (x)}{x} \in ℂ$
15	5	oveq1d	$⊢ x \in ℝ^{+} \to \frac{R (x)}{x} = \frac{ψ (x) - x}{x}$
16	8	recnd	$⊢ x \in ℝ^{+} \to ψ (x) \in ℂ$
17		rpcn	$⊢ x \in ℝ^{+} \to x \in ℂ$
18		rpne0	$⊢ x \in ℝ^{+} \to x \neq 0$
19	16 17 17 18	divsubdird	$⊢ x \in ℝ^{+} \to \frac{ψ (x) - x}{x} = (\frac{ψ (x)}{x}) - (\frac{x}{x})$
20	17 18	dividd	$⊢ x \in ℝ^{+} \to \frac{x}{x} = 1$
21	20	oveq2d	$⊢ x \in ℝ^{+} \to (\frac{ψ (x)}{x}) - (\frac{x}{x}) = (\frac{ψ (x)}{x}) - 1$
22	15 19 21	3eqtrd	$⊢ x \in ℝ^{+} \to \frac{R (x)}{x} = (\frac{ψ (x)}{x}) - 1$
23	22	mpteq2ia	$⊢ (x \in ℝ^{+} ⟼ \frac{R (x)}{x}) = (x \in ℝ^{+} ⟼ (\frac{ψ (x)}{x}) - 1)$
24		rerpdivcl	$⊢ (ψ (x) \in ℝ \land x \in ℝ^{+}) \to \frac{ψ (x)}{x} \in ℝ$
25	8 24	mpancom	$⊢ x \in ℝ^{+} \to \frac{ψ (x)}{x} \in ℝ$
26	25	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{ψ (x)}{x} \in ℝ$
27		1red	$⊢ (⊤ \land x \in ℝ^{+}) \to 1 \in ℝ$
28		chpo1ub	$⊢ (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \in 𝑂 (1)$
29	28	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \in 𝑂 (1)$
30		ax-1cn	$⊢ 1 \in ℂ$
31		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land 1 \in ℂ) \to (x \in ℝ^{+} ⟼ 1) \in 𝑂 (1)$
32	2 30 31	mp2an	$⊢ (x \in ℝ^{+} ⟼ 1) \in 𝑂 (1)$
33	32	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ 1) \in 𝑂 (1)$
34	26 27 29 33	o1sub2	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ (\frac{ψ (x)}{x}) - 1) \in 𝑂 (1)$
35	23 34	eqeltrid	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{R (x)}{x}) \in 𝑂 (1)$
36		chpcl	$⊢ y \in ℝ \to ψ (y) \in ℝ$
37		peano2re	$⊢ ψ (y) \in ℝ \to ψ (y) + 1 \in ℝ$
38	36 37	syl	$⊢ y \in ℝ \to ψ (y) + 1 \in ℝ$
39	38	ad2antrl	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to ψ (y) + 1 \in ℝ$
40	22	3ad2ant1	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to \frac{R (x)}{x} = (\frac{ψ (x)}{x}) - 1$
41	40	fveq2d	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to \|\frac{R (x)}{x}\| = \|(\frac{ψ (x)}{x}) - 1\|$
42		1re	$⊢ 1 \in ℝ$
43	38	3ad2ant2	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to ψ (y) + 1 \in ℝ$
44		resubcl	$⊢ (1 \in ℝ \land ψ (y) + 1 \in ℝ) \to 1 - (ψ (y) + 1) \in ℝ$
45	42 43 44	sylancr	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to 1 - (ψ (y) + 1) \in ℝ$
46		0red	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to 0 \in ℝ$
47	25	3ad2ant1	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to \frac{ψ (x)}{x} \in ℝ$
48		chpge0	$⊢ y \in ℝ \to 0 \leq ψ (y)$
49	48	3ad2ant2	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to 0 \leq ψ (y)$
50	36	3ad2ant2	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to ψ (y) \in ℝ$
51		addge02	$⊢ (1 \in ℝ \land ψ (y) \in ℝ) \to (0 \leq ψ (y) \leftrightarrow 1 \leq ψ (y) + 1)$
52	42 50 51	sylancr	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to (0 \leq ψ (y) \leftrightarrow 1 \leq ψ (y) + 1)$
53	49 52	mpbid	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to 1 \leq ψ (y) + 1$
54		suble0	$⊢ (1 \in ℝ \land ψ (y) + 1 \in ℝ) \to (1 - (ψ (y) + 1) \leq 0 \leftrightarrow 1 \leq ψ (y) + 1)$
55	42 43 54	sylancr	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to (1 - (ψ (y) + 1) \leq 0 \leftrightarrow 1 \leq ψ (y) + 1)$
56	53 55	mpbird	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to 1 - (ψ (y) + 1) \leq 0$
57	8	3ad2ant1	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to ψ (x) \in ℝ$
58	6	3ad2ant1	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to x \in ℝ$
59		chpge0	$⊢ x \in ℝ \to 0 \leq ψ (x)$
60	58 59	syl	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to 0 \leq ψ (x)$
61		rpregt0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 < x)$
62	61	3ad2ant1	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to (x \in ℝ \land 0 < x)$
63		divge0	$⊢ ((ψ (x) \in ℝ \land 0 \leq ψ (x)) \land (x \in ℝ \land 0 < x)) \to 0 \leq \frac{ψ (x)}{x}$
64	57 60 62 63	syl21anc	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to 0 \leq \frac{ψ (x)}{x}$
65	45 46 47 56 64	letrd	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to 1 - (ψ (y) + 1) \leq \frac{ψ (x)}{x}$
66		2re	$⊢ 2 \in ℝ$
67		readdcl	$⊢ (ψ (y) \in ℝ \land 2 \in ℝ) \to ψ (y) + 2 \in ℝ$
68	50 66 67	sylancl	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to ψ (y) + 2 \in ℝ$
69		1red	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to 1 \in ℝ$
70	58	adantr	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land x \leq 1) \to x \in ℝ$
71		1red	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land x \leq 1) \to 1 \in ℝ$
72	66	a1i	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land x \leq 1) \to 2 \in ℝ$
73		simpr	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land x \leq 1) \to x \leq 1$
74		1lt2	$⊢ 1 < 2$
75	74	a1i	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land x \leq 1) \to 1 < 2$
76	70 71 72 73 75	lelttrd	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land x \leq 1) \to x < 2$
77		chpeq0	$⊢ x \in ℝ \to (ψ (x) = 0 \leftrightarrow x < 2)$
78	70 77	syl	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land x \leq 1) \to (ψ (x) = 0 \leftrightarrow x < 2)$
79	76 78	mpbird	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land x \leq 1) \to ψ (x) = 0$
80	79	oveq1d	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land x \leq 1) \to \frac{ψ (x)}{x} = \frac{0}{x}$
81		simp1	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to x \in ℝ^{+}$
82	81	rpcnne0d	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to (x \in ℂ \land x \neq 0)$
83		div0	$⊢ (x \in ℂ \land x \neq 0) \to \frac{0}{x} = 0$
84	82 83	syl	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to \frac{0}{x} = 0$
85	84 49	eqbrtrd	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to \frac{0}{x} \leq ψ (y)$
86	85	adantr	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land x \leq 1) \to \frac{0}{x} \leq ψ (y)$
87	80 86	eqbrtrd	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land x \leq 1) \to \frac{ψ (x)}{x} \leq ψ (y)$
88	47	adantr	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land 1 \leq x) \to \frac{ψ (x)}{x} \in ℝ$
89	57	adantr	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land 1 \leq x) \to ψ (x) \in ℝ$
90	50	adantr	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land 1 \leq x) \to ψ (y) \in ℝ$
91		0lt1	$⊢ 0 < 1$
92	91	a1i	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to 0 < 1$
93		lediv2a	$⊢ (((1 \in ℝ \land 0 < 1) \land (x \in ℝ \land 0 < x) \land (ψ (x) \in ℝ \land 0 \leq ψ (x))) \land 1 \leq x) \to \frac{ψ (x)}{x} \leq \frac{ψ (x)}{1}$
94	93	ex	$⊢ ((1 \in ℝ \land 0 < 1) \land (x \in ℝ \land 0 < x) \land (ψ (x) \in ℝ \land 0 \leq ψ (x))) \to (1 \leq x \to \frac{ψ (x)}{x} \leq \frac{ψ (x)}{1})$
95	69 92 62 57 60 94	syl212anc	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to (1 \leq x \to \frac{ψ (x)}{x} \leq \frac{ψ (x)}{1})$
96	95	imp	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land 1 \leq x) \to \frac{ψ (x)}{x} \leq \frac{ψ (x)}{1}$
97	89	recnd	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land 1 \leq x) \to ψ (x) \in ℂ$
98	97	div1d	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land 1 \leq x) \to \frac{ψ (x)}{1} = ψ (x)$
99	96 98	breqtrd	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land 1 \leq x) \to \frac{ψ (x)}{x} \leq ψ (x)$
100		simp2	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to y \in ℝ$
101		ltle	$⊢ (x \in ℝ \land y \in ℝ) \to (x < y \to x \leq y)$
102	6 101	sylan	$⊢ (x \in ℝ^{+} \land y \in ℝ) \to (x < y \to x \leq y)$
103	102	3impia	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to x \leq y$
104		chpwordi	$⊢ (x \in ℝ \land y \in ℝ \land x \leq y) \to ψ (x) \leq ψ (y)$
105	58 100 103 104	syl3anc	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to ψ (x) \leq ψ (y)$
106	105	adantr	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land 1 \leq x) \to ψ (x) \leq ψ (y)$
107	88 89 90 99 106	letrd	$⊢ ((x \in ℝ^{+} \land y \in ℝ \land x < y) \land 1 \leq x) \to \frac{ψ (x)}{x} \leq ψ (y)$
108	58 69 87 107	lecasei	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to \frac{ψ (x)}{x} \leq ψ (y)$
109		2nn0	$⊢ 2 \in ℕ_{0}$
110		nn0addge1	$⊢ (ψ (y) \in ℝ \land 2 \in ℕ_{0}) \to ψ (y) \leq ψ (y) + 2$
111	50 109 110	sylancl	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to ψ (y) \leq ψ (y) + 2$
112	47 50 68 108 111	letrd	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to \frac{ψ (x)}{x} \leq ψ (y) + 2$
113		df-2	$⊢ 2 = 1 + 1$
114	113	oveq2i	$⊢ ψ (y) + 2 = ψ (y) + 1 + 1$
115	50	recnd	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to ψ (y) \in ℂ$
116	30	a1i	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to 1 \in ℂ$
117	115 116 116	add12d	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to ψ (y) + 1 + 1 = 1 + ψ (y) + 1$
118	114 117	eqtrid	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to ψ (y) + 2 = 1 + ψ (y) + 1$
119	112 118	breqtrd	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to \frac{ψ (x)}{x} \leq 1 + ψ (y) + 1$
120	47 69 43	absdifled	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to (\|(\frac{ψ (x)}{x}) - 1\| \leq ψ (y) + 1 \leftrightarrow (1 - (ψ (y) + 1) \leq \frac{ψ (x)}{x} \land \frac{ψ (x)}{x} \leq 1 + ψ (y) + 1))$
121	65 119 120	mpbir2and	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to \|(\frac{ψ (x)}{x}) - 1\| \leq ψ (y) + 1$
122	41 121	eqbrtrd	$⊢ (x \in ℝ^{+} \land y \in ℝ \land x < y) \to \|\frac{R (x)}{x}\| \leq ψ (y) + 1$
123	122	3expb	$⊢ (x \in ℝ^{+} \land (y \in ℝ \land x < y)) \to \|\frac{R (x)}{x}\| \leq ψ (y) + 1$
124	123	adantrlr	$⊢ (x \in ℝ^{+} \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|\frac{R (x)}{x}\| \leq ψ (y) + 1$
125	124	adantll	$⊢ ((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|\frac{R (x)}{x}\| \leq ψ (y) + 1$
126	3 4 14 35 39 125	o1bddrp	$⊢ ⊤ \to \exists c \in ℝ^{+} \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq c$
127	126	mptru	$⊢ \exists c \in ℝ^{+} \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq c$

Metamath Proof Explorer

Theorem pntrmax

Proof