Metamath Proof Explorer

Theorem 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 ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
Assertion pntrmax ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑐

Proof

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