pntrmax - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pntrmax		Structured version Visualization version GIF version

Theorem pntrmax 27447

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

**Hypothesis**
Ref	Expression
pntrval.r	⊢ 𝑅 = (𝑎 ∈ ℝ⁺ ↦ ((ψ‘𝑎) − 𝑎))

**Assertion**
Ref	Expression
pntrmax	⊢ ∃𝑐 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑐

Distinct variable groups: 𝑥,𝑎 𝑥,𝑐,𝑅 Allowed substitution hint: 𝑅(𝑎)

Proof of Theorem pntrmax Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rpssre 12984	. . . 4 ⊢ ℝ⁺ ⊆ ℝ
2	1	a1i 11	. . 3 ⊢ (⊤ → ℝ⁺ ⊆ ℝ)
3		1red 11216	. . 3 ⊢ (⊤ → 1 ∈ ℝ)
4		pntrval.r	. . . . . . . 8 ⊢ 𝑅 = (𝑎 ∈ ℝ⁺ ↦ ((ψ‘𝑎) − 𝑎))
5	4	pntrval 27445	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → (𝑅‘𝑥) = ((ψ‘𝑥) − 𝑥))
6		rpre 12985	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
7		chpcl 27006	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (ψ‘𝑥) ∈ ℝ)
8	6, 7	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → (ψ‘𝑥) ∈ ℝ)
9	8, 6	resubcld 11643	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → ((ψ‘𝑥) − 𝑥) ∈ ℝ)
10	5, 9	eqeltrd 2827	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → (𝑅‘𝑥) ∈ ℝ)
11		rerpdivcl 13007	. . . . . 6 ⊢ (((𝑅‘𝑥) ∈ ℝ ∧ 𝑥 ∈ ℝ⁺) → ((𝑅‘𝑥) / 𝑥) ∈ ℝ)
12	10, 11	mpancom 685	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ → ((𝑅‘𝑥) / 𝑥) ∈ ℝ)
13	12	recnd 11243	. . . 4 ⊢ (𝑥 ∈ ℝ⁺ → ((𝑅‘𝑥) / 𝑥) ∈ ℂ)
14	13	adantl 481	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((𝑅‘𝑥) / 𝑥) ∈ ℂ)
15	5	oveq1d 7419	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → ((𝑅‘𝑥) / 𝑥) = (((ψ‘𝑥) − 𝑥) / 𝑥))
16	8	recnd 11243	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → (ψ‘𝑥) ∈ ℂ)
17		rpcn 12987	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℂ)
18		rpne0 12993	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ≠ 0)
19	16, 17, 17, 18	divsubdird 12030	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → (((ψ‘𝑥) − 𝑥) / 𝑥) = (((ψ‘𝑥) / 𝑥) − (𝑥 / 𝑥)))
20	17, 18	dividd 11989	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 𝑥) = 1)
21	20	oveq2d 7420	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → (((ψ‘𝑥) / 𝑥) − (𝑥 / 𝑥)) = (((ψ‘𝑥) / 𝑥) − 1))
22	15, 19, 21	3eqtrd 2770	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ → ((𝑅‘𝑥) / 𝑥) = (((ψ‘𝑥) / 𝑥) − 1))
23	22	mpteq2ia 5244	. . . 4 ⊢ (𝑥 ∈ ℝ⁺ ↦ ((𝑅‘𝑥) / 𝑥)) = (𝑥 ∈ ℝ⁺ ↦ (((ψ‘𝑥) / 𝑥) − 1))
24		rerpdivcl 13007	. . . . . . 7 ⊢ (((ψ‘𝑥) ∈ ℝ ∧ 𝑥 ∈ ℝ⁺) → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
25	8, 24	mpancom 685	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
26	25	adantl 481	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
27		1red 11216	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 1 ∈ ℝ)
28		chpo1ub 27363	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1)
29	28	a1i 11	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1))
30		ax-1cn 11167	. . . . . . 7 ⊢ 1 ∈ ℂ
31		o1const 15567	. . . . . . 7 ⊢ ((ℝ⁺ ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ 1) ∈ 𝑂(1))
32	1, 30, 31	mp2an 689	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ ↦ 1) ∈ 𝑂(1)
33	32	a1i 11	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ 1) ∈ 𝑂(1))
34	26, 27, 29, 33	o1sub2 15573	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (((ψ‘𝑥) / 𝑥) − 1)) ∈ 𝑂(1))
35	23, 34	eqeltrid 2831	. . 3 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ ((𝑅‘𝑥) / 𝑥)) ∈ 𝑂(1))
36		chpcl 27006	. . . . 5 ⊢ (𝑦 ∈ ℝ → (ψ‘𝑦) ∈ ℝ)
37		peano2re 11388	. . . . 5 ⊢ ((ψ‘𝑦) ∈ ℝ → ((ψ‘𝑦) + 1) ∈ ℝ)
38	36, 37	syl 17	. . . 4 ⊢ (𝑦 ∈ ℝ → ((ψ‘𝑦) + 1) ∈ ℝ)
39	38	ad2antrl 725	. . 3 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) → ((ψ‘𝑦) + 1) ∈ ℝ)
40	22	3ad2ant1 1130	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → ((𝑅‘𝑥) / 𝑥) = (((ψ‘𝑥) / 𝑥) − 1))
41	40	fveq2d 6888	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → (abs‘((𝑅‘𝑥) / 𝑥)) = (abs‘(((ψ‘𝑥) / 𝑥) − 1)))
42		1re 11215	. . . . . . . . . 10 ⊢ 1 ∈ ℝ
43	38	3ad2ant2 1131	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → ((ψ‘𝑦) + 1) ∈ ℝ)
44		resubcl 11525	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ ((ψ‘𝑦) + 1) ∈ ℝ) → (1 − ((ψ‘𝑦) + 1)) ∈ ℝ)
45	42, 43, 44	sylancr 586	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → (1 − ((ψ‘𝑦) + 1)) ∈ ℝ)
46		0red 11218	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → 0 ∈ ℝ)
47	25	3ad2ant1 1130	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
48		chpge0 27008	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → 0 ≤ (ψ‘𝑦))
49	48	3ad2ant2 1131	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → 0 ≤ (ψ‘𝑦))
50	36	3ad2ant2 1131	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → (ψ‘𝑦) ∈ ℝ)
51		addge02 11726	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ ∧ (ψ‘𝑦) ∈ ℝ) → (0 ≤ (ψ‘𝑦) ↔ 1 ≤ ((ψ‘𝑦) + 1)))
52	42, 50, 51	sylancr 586	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → (0 ≤ (ψ‘𝑦) ↔ 1 ≤ ((ψ‘𝑦) + 1)))
53	49, 52	mpbid 231	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → 1 ≤ ((ψ‘𝑦) + 1))
54		suble0 11729	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ ((ψ‘𝑦) + 1) ∈ ℝ) → ((1 − ((ψ‘𝑦) + 1)) ≤ 0 ↔ 1 ≤ ((ψ‘𝑦) + 1)))
55	42, 43, 54	sylancr 586	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → ((1 − ((ψ‘𝑦) + 1)) ≤ 0 ↔ 1 ≤ ((ψ‘𝑦) + 1)))
56	53, 55	mpbird 257	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → (1 − ((ψ‘𝑦) + 1)) ≤ 0)
57	8	3ad2ant1 1130	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → (ψ‘𝑥) ∈ ℝ)
58	6	3ad2ant1 1130	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → 𝑥 ∈ ℝ)
59		chpge0 27008	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → 0 ≤ (ψ‘𝑥))
60	58, 59	syl 17	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → 0 ≤ (ψ‘𝑥))
61		rpregt0 12991	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
62	61	3ad2ant1 1130	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
63		divge0 12084	. . . . . . . . . 10 ⊢ ((((ψ‘𝑥) ∈ ℝ ∧ 0 ≤ (ψ‘𝑥)) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → 0 ≤ ((ψ‘𝑥) / 𝑥))
64	57, 60, 62, 63	syl21anc 835	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → 0 ≤ ((ψ‘𝑥) / 𝑥))
65	45, 46, 47, 56, 64	letrd 11372	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → (1 − ((ψ‘𝑦) + 1)) ≤ ((ψ‘𝑥) / 𝑥))
66		2re 12287	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
67		readdcl 11192	. . . . . . . . . . 11 ⊢ (((ψ‘𝑦) ∈ ℝ ∧ 2 ∈ ℝ) → ((ψ‘𝑦) + 2) ∈ ℝ)
68	50, 66, 67	sylancl 585	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → ((ψ‘𝑦) + 2) ∈ ℝ)
69		1red 11216	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → 1 ∈ ℝ)
70	58	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 𝑥 ≤ 1) → 𝑥 ∈ ℝ)
71		1red 11216	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 𝑥 ≤ 1) → 1 ∈ ℝ)
72	66	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 𝑥 ≤ 1) → 2 ∈ ℝ)
73		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 𝑥 ≤ 1) → 𝑥 ≤ 1)
74		1lt2 12384	. . . . . . . . . . . . . . . 16 ⊢ 1 < 2
75	74	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 𝑥 ≤ 1) → 1 < 2)
76	70, 71, 72, 73, 75	lelttrd 11373	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 𝑥 ≤ 1) → 𝑥 < 2)
77		chpeq0 27091	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → ((ψ‘𝑥) = 0 ↔ 𝑥 < 2))
78	70, 77	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 𝑥 ≤ 1) → ((ψ‘𝑥) = 0 ↔ 𝑥 < 2))
79	76, 78	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 𝑥 ≤ 1) → (ψ‘𝑥) = 0)
80	79	oveq1d 7419	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 𝑥 ≤ 1) → ((ψ‘𝑥) / 𝑥) = (0 / 𝑥))
81		simp1 1133	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → 𝑥 ∈ ℝ⁺)
82	81	rpcnne0d 13028	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
83		div0 11903	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (0 / 𝑥) = 0)
84	82, 83	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → (0 / 𝑥) = 0)
85	84, 49	eqbrtrd 5163	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → (0 / 𝑥) ≤ (ψ‘𝑦))
86	85	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 𝑥 ≤ 1) → (0 / 𝑥) ≤ (ψ‘𝑦))
87	80, 86	eqbrtrd 5163	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 𝑥 ≤ 1) → ((ψ‘𝑥) / 𝑥) ≤ (ψ‘𝑦))
88	47	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 1 ≤ 𝑥) → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
89	57	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 1 ≤ 𝑥) → (ψ‘𝑥) ∈ ℝ)
90	50	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 1 ≤ 𝑥) → (ψ‘𝑦) ∈ ℝ)
91		0lt1 11737	. . . . . . . . . . . . . . . 16 ⊢ 0 < 1
92	91	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → 0 < 1)
93		lediv2a 12109	. . . . . . . . . . . . . . . 16 ⊢ ((((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥) ∧ ((ψ‘𝑥) ∈ ℝ ∧ 0 ≤ (ψ‘𝑥))) ∧ 1 ≤ 𝑥) → ((ψ‘𝑥) / 𝑥) ≤ ((ψ‘𝑥) / 1))
94	93	ex 412	. . . . . . . . . . . . . . 15 ⊢ (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥) ∧ ((ψ‘𝑥) ∈ ℝ ∧ 0 ≤ (ψ‘𝑥))) → (1 ≤ 𝑥 → ((ψ‘𝑥) / 𝑥) ≤ ((ψ‘𝑥) / 1)))
95	69, 92, 62, 57, 60, 94	syl212anc 1377	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → (1 ≤ 𝑥 → ((ψ‘𝑥) / 𝑥) ≤ ((ψ‘𝑥) / 1)))
96	95	imp 406	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 1 ≤ 𝑥) → ((ψ‘𝑥) / 𝑥) ≤ ((ψ‘𝑥) / 1))
97	89	recnd 11243	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 1 ≤ 𝑥) → (ψ‘𝑥) ∈ ℂ)
98	97	div1d 11983	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 1 ≤ 𝑥) → ((ψ‘𝑥) / 1) = (ψ‘𝑥))
99	96, 98	breqtrd 5167	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 1 ≤ 𝑥) → ((ψ‘𝑥) / 𝑥) ≤ (ψ‘𝑥))
100		simp2 1134	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℝ)
101		ltle 11303	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 < 𝑦 → 𝑥 ≤ 𝑦))
102	6, 101	sylan 579	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ) → (𝑥 < 𝑦 → 𝑥 ≤ 𝑦))
103	102	3impia 1114	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → 𝑥 ≤ 𝑦)
104		chpwordi 27039	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦) → (ψ‘𝑥) ≤ (ψ‘𝑦))
105	58, 100, 103, 104	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → (ψ‘𝑥) ≤ (ψ‘𝑦))
106	105	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 1 ≤ 𝑥) → (ψ‘𝑥) ≤ (ψ‘𝑦))
107	88, 89, 90, 99, 106	letrd 11372	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) ∧ 1 ≤ 𝑥) → ((ψ‘𝑥) / 𝑥) ≤ (ψ‘𝑦))
108	58, 69, 87, 107	lecasei 11321	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → ((ψ‘𝑥) / 𝑥) ≤ (ψ‘𝑦))
109		2nn0 12490	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
110		nn0addge1 12519	. . . . . . . . . . 11 ⊢ (((ψ‘𝑦) ∈ ℝ ∧ 2 ∈ ℕ₀) → (ψ‘𝑦) ≤ ((ψ‘𝑦) + 2))
111	50, 109, 110	sylancl 585	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → (ψ‘𝑦) ≤ ((ψ‘𝑦) + 2))
112	47, 50, 68, 108, 111	letrd 11372	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → ((ψ‘𝑥) / 𝑥) ≤ ((ψ‘𝑦) + 2))
113		df-2 12276	. . . . . . . . . . 11 ⊢ 2 = (1 + 1)
114	113	oveq2i 7415	. . . . . . . . . 10 ⊢ ((ψ‘𝑦) + 2) = ((ψ‘𝑦) + (1 + 1))
115	50	recnd 11243	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → (ψ‘𝑦) ∈ ℂ)
116	30	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → 1 ∈ ℂ)
117	115, 116, 116	add12d 11441	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → ((ψ‘𝑦) + (1 + 1)) = (1 + ((ψ‘𝑦) + 1)))
118	114, 117	eqtrid 2778	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → ((ψ‘𝑦) + 2) = (1 + ((ψ‘𝑦) + 1)))
119	112, 118	breqtrd 5167	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → ((ψ‘𝑥) / 𝑥) ≤ (1 + ((ψ‘𝑦) + 1)))
120	47, 69, 43	absdifled 15384	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → ((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ ((ψ‘𝑦) + 1) ↔ ((1 − ((ψ‘𝑦) + 1)) ≤ ((ψ‘𝑥) / 𝑥) ∧ ((ψ‘𝑥) / 𝑥) ≤ (1 + ((ψ‘𝑦) + 1)))))
121	65, 119, 120	mpbir2and 710	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ ((ψ‘𝑦) + 1))
122	41, 121	eqbrtrd 5163	. . . . . 6 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦) → (abs‘((𝑅‘𝑥) / 𝑥)) ≤ ((ψ‘𝑦) + 1))
123	122	3expb 1117	. . . . 5 ⊢ ((𝑥 ∈ ℝ⁺ ∧ (𝑦 ∈ ℝ ∧ 𝑥 < 𝑦)) → (abs‘((𝑅‘𝑥) / 𝑥)) ≤ ((ψ‘𝑦) + 1))
124	123	adantrlr 720	. . . 4 ⊢ ((𝑥 ∈ ℝ⁺ ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘((𝑅‘𝑥) / 𝑥)) ≤ ((ψ‘𝑦) + 1))
125	124	adantll 711	. . 3 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘((𝑅‘𝑥) / 𝑥)) ≤ ((ψ‘𝑦) + 1))
126	2, 3, 14, 35, 39, 125	o1bddrp 15489	. 2 ⊢ (⊤ → ∃𝑐 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑐)
127	126	mptru 1540	1 ⊢ ∃𝑐 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑐

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1084 = wceq 1533 ⊤wtru 1534 ∈ wcel 2098 ≠ wne 2934 ∀wral 3055 ∃wrex 3064 ⊆ wss 3943 class class class wbr 5141 ↦ cmpt 5224 ‘cfv 6536 (class class class)co 7404 ℂcc 11107 ℝcr 11108 0cc0 11109 1c1 11110 + caddc 11112 < clt 11249 ≤ cle 11250 − cmin 11445 / cdiv 11872 2c2 12268 ℕ₀cn0 12473 ℝ⁺crp 12977 abscabs 15184 𝑂(1)co1 15433 ψcchp 26975

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2697 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7721 ax-inf2 9635 ax-cnex 11165 ax-resscn 11166 ax-1cn 11167 ax-icn 11168 ax-addcl 11169 ax-addrcl 11170 ax-mulcl 11171 ax-mulrcl 11172 ax-mulcom 11173 ax-addass 11174 ax-mulass 11175 ax-distr 11176 ax-i2m1 11177 ax-1ne0 11178 ax-1rid 11179 ax-rnegex 11180 ax-rrecex 11181 ax-cnre 11182 ax-pre-lttri 11183 ax-pre-lttrn 11184 ax-pre-ltadd 11185 ax-pre-mulgt0 11186 ax-pre-sup 11187 ax-addf 11188

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-nel 3041 df-ral 3056 df-rex 3065 df-rmo 3370 df-reu 3371 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-pss 3962 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-tp 4628 df-op 4630 df-uni 4903 df-int 4944 df-iun 4992 df-iin 4993 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-se 5625 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6293 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6488 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7360 df-ov 7407 df-oprab 7408 df-mpo 7409 df-of 7666 df-om 7852 df-1st 7971 df-2nd 7972 df-supp 8144 df-frecs 8264 df-wrecs 8295 df-recs 8369 df-rdg 8408 df-1o 8464 df-2o 8465 df-oadd 8468 df-er 8702 df-map 8821 df-pm 8822 df-ixp 8891 df-en 8939 df-dom 8940 df-sdom 8941 df-fin 8942 df-fsupp 9361 df-fi 9405 df-sup 9436 df-inf 9437 df-oi 9504 df-dju 9895 df-card 9933 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11447 df-neg 11448 df-div 11873 df-nn 12214 df-2 12276 df-3 12277 df-4 12278 df-5 12279 df-6 12280 df-7 12281 df-8 12282 df-9 12283 df-n0 12474 df-xnn0 12546 df-z 12560 df-dec 12679 df-uz 12824 df-q 12934 df-rp 12978 df-xneg 13095 df-xadd 13096 df-xmul 13097 df-ioo 13331 df-ioc 13332 df-ico 13333 df-icc 13334 df-fz 13488 df-fzo 13631 df-fl 13760 df-mod 13838 df-seq 13970 df-exp 14030 df-fac 14236 df-bc 14265 df-hash 14293 df-shft 15017 df-cj 15049 df-re 15050 df-im 15051 df-sqrt 15185 df-abs 15186 df-limsup 15418 df-clim 15435 df-rlim 15436 df-o1 15437 df-lo1 15438 df-sum 15636 df-ef 16014 df-e 16015 df-sin 16016 df-cos 16017 df-pi 16019 df-dvds 16202 df-gcd 16440 df-prm 16613 df-pc 16776 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17151 df-ress 17180 df-plusg 17216 df-mulr 17217 df-starv 17218 df-sca 17219 df-vsca 17220 df-ip 17221 df-tset 17222 df-ple 17223 df-ds 17225 df-unif 17226 df-hom 17227 df-cco 17228 df-rest 17374 df-topn 17375 df-0g 17393 df-gsum 17394 df-topgen 17395 df-pt 17396 df-prds 17399 df-xrs 17454 df-qtop 17459 df-imas 17460 df-xps 17462 df-mre 17536 df-mrc 17537 df-acs 17539 df-mgm 18570 df-sgrp 18649 df-mnd 18665 df-submnd 18711 df-mulg 18993 df-cntz 19230 df-cmn 19699 df-psmet 21227 df-xmet 21228 df-met 21229 df-bl 21230 df-mopn 21231 df-fbas 21232 df-fg 21233 df-cnfld 21236 df-top 22746 df-topon 22763 df-topsp 22785 df-bases 22799 df-cld 22873 df-ntr 22874 df-cls 22875 df-nei 22952 df-lp 22990 df-perf 22991 df-cn 23081 df-cnp 23082 df-haus 23169 df-tx 23416 df-hmeo 23609 df-fil 23700 df-fm 23792 df-flim 23793 df-flf 23794 df-xms 24176 df-ms 24177 df-tms 24178 df-cncf 24748 df-limc 25745 df-dv 25746 df-log 26440 df-cxp 26441 df-cht 26979 df-vma 26980 df-chp 26981 df-ppi 26982

This theorem is referenced by: pntrlog2bnd 27467 pntibnd 27476 pnt3 27495

W3C validator