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

Theorem pntibndlem2 25214
Description: Lemma for pntibnd 25216. The main work, after eliminating all the quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016.)
Hypotheses
Ref Expression
pntibnd.r 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
pntibndlem1.1 (𝜑𝐴 ∈ ℝ+)
pntibndlem1.l 𝐿 = ((1 / 4) / (𝐴 + 3))
pntibndlem3.2 (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)
pntibndlem3.3 (𝜑𝐵 ∈ ℝ+)
pntibndlem3.k 𝐾 = (exp‘(𝐵 / (𝐸 / 2)))
pntibndlem3.c 𝐶 = ((2 · 𝐵) + (log‘2))
pntibndlem3.4 (𝜑𝐸 ∈ (0(,)1))
pntibndlem3.6 (𝜑𝑍 ∈ ℝ+)
pntibndlem2.10 (𝜑𝑁 ∈ ℕ)
pntibndlem2.5 (𝜑𝑇 ∈ ℝ+)
pntibndlem2.6 (𝜑 → ∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))))
pntibndlem2.7 𝑋 = ((exp‘(𝑇 / (𝐸 / 4))) + 𝑍)
pntibndlem2.8 (𝜑𝑀 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞))
pntibndlem2.9 (𝜑𝑌 ∈ (𝑋(,)+∞))
pntibndlem2.11 (𝜑 → ((𝑌 < 𝑁𝑁 ≤ ((𝑀 / 2) · 𝑌)) ∧ (abs‘((𝑅𝑁) / 𝑁)) ≤ (𝐸 / 2)))
Assertion
Ref Expression
pntibndlem2 (𝜑 → ∃𝑧 ∈ ℝ+ ((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
Distinct variable groups:   𝑢,𝑎,𝑥,𝑦,𝑧,𝐸   𝑢,𝐿,𝑥,𝑧   𝑁,𝑎,𝑢,𝑥,𝑦,𝑧   𝑢,𝐴,𝑥   𝑢,𝐶,𝑥,𝑦   𝑢,𝑅,𝑥,𝑦,𝑧   𝑧,𝑀   𝑥,𝑇,𝑦   𝑧,𝑌   𝑢,𝑍,𝑥,𝑦   𝜑,𝑢
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑎)   𝐴(𝑦,𝑧,𝑎)   𝐵(𝑥,𝑦,𝑧,𝑢,𝑎)   𝐶(𝑧,𝑎)   𝑅(𝑎)   𝑇(𝑧,𝑢,𝑎)   𝐾(𝑥,𝑦,𝑧,𝑢,𝑎)   𝐿(𝑦,𝑎)   𝑀(𝑥,𝑦,𝑢,𝑎)   𝑋(𝑥,𝑦,𝑧,𝑢,𝑎)   𝑌(𝑥,𝑦,𝑢,𝑎)   𝑍(𝑧,𝑎)

Proof of Theorem pntibndlem2
StepHypRef Expression
1 pntibndlem2.10 . . 3 (𝜑𝑁 ∈ ℕ)
21nnrpd 11830 . 2 (𝜑𝑁 ∈ ℝ+)
3 pntibndlem2.11 . . . . 5 (𝜑 → ((𝑌 < 𝑁𝑁 ≤ ((𝑀 / 2) · 𝑌)) ∧ (abs‘((𝑅𝑁) / 𝑁)) ≤ (𝐸 / 2)))
43simpld 475 . . . 4 (𝜑 → (𝑌 < 𝑁𝑁 ≤ ((𝑀 / 2) · 𝑌)))
54simpld 475 . . 3 (𝜑𝑌 < 𝑁)
6 1red 10015 . . . . . 6 (𝜑 → 1 ∈ ℝ)
7 ioossre 12193 . . . . . . . 8 (0(,)1) ⊆ ℝ
8 pntibnd.r . . . . . . . . 9 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
9 pntibndlem1.1 . . . . . . . . 9 (𝜑𝐴 ∈ ℝ+)
10 pntibndlem1.l . . . . . . . . 9 𝐿 = ((1 / 4) / (𝐴 + 3))
118, 9, 10pntibndlem1 25212 . . . . . . . 8 (𝜑𝐿 ∈ (0(,)1))
127, 11sseldi 3586 . . . . . . 7 (𝜑𝐿 ∈ ℝ)
13 pntibndlem3.4 . . . . . . . 8 (𝜑𝐸 ∈ (0(,)1))
147, 13sseldi 3586 . . . . . . 7 (𝜑𝐸 ∈ ℝ)
1512, 14remulcld 10030 . . . . . 6 (𝜑 → (𝐿 · 𝐸) ∈ ℝ)
166, 15readdcld 10029 . . . . 5 (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ)
171nnred 10995 . . . . 5 (𝜑𝑁 ∈ ℝ)
1816, 17remulcld 10030 . . . 4 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑁) ∈ ℝ)
19 2re 11050 . . . . 5 2 ∈ ℝ
20 remulcl 9981 . . . . 5 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
2119, 17, 20sylancr 694 . . . 4 (𝜑 → (2 · 𝑁) ∈ ℝ)
22 pntibndlem3.c . . . . . . . . . 10 𝐶 = ((2 · 𝐵) + (log‘2))
23 pntibndlem3.3 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℝ+)
2423rpred 11832 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ)
25 remulcl 9981 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (2 · 𝐵) ∈ ℝ)
2619, 24, 25sylancr 694 . . . . . . . . . . 11 (𝜑 → (2 · 𝐵) ∈ ℝ)
27 2rp 11797 . . . . . . . . . . . . 13 2 ∈ ℝ+
2827a1i 11 . . . . . . . . . . . 12 (𝜑 → 2 ∈ ℝ+)
2928relogcld 24307 . . . . . . . . . . 11 (𝜑 → (log‘2) ∈ ℝ)
3026, 29readdcld 10029 . . . . . . . . . 10 (𝜑 → ((2 · 𝐵) + (log‘2)) ∈ ℝ)
3122, 30syl5eqel 2702 . . . . . . . . 9 (𝜑𝐶 ∈ ℝ)
32 eliooord 12191 . . . . . . . . . . . 12 (𝐸 ∈ (0(,)1) → (0 < 𝐸𝐸 < 1))
3313, 32syl 17 . . . . . . . . . . 11 (𝜑 → (0 < 𝐸𝐸 < 1))
3433simpld 475 . . . . . . . . . 10 (𝜑 → 0 < 𝐸)
3514, 34elrpd 11829 . . . . . . . . 9 (𝜑𝐸 ∈ ℝ+)
3631, 35rerpdivcld 11863 . . . . . . . 8 (𝜑 → (𝐶 / 𝐸) ∈ ℝ)
3736reefcld 14762 . . . . . . 7 (𝜑 → (exp‘(𝐶 / 𝐸)) ∈ ℝ)
38 pnfxr 10052 . . . . . . 7 +∞ ∈ ℝ*
39 icossre 12212 . . . . . . 7 (((exp‘(𝐶 / 𝐸)) ∈ ℝ ∧ +∞ ∈ ℝ*) → ((exp‘(𝐶 / 𝐸))[,)+∞) ⊆ ℝ)
4037, 38, 39sylancl 693 . . . . . 6 (𝜑 → ((exp‘(𝐶 / 𝐸))[,)+∞) ⊆ ℝ)
41 pntibndlem2.8 . . . . . 6 (𝜑𝑀 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞))
4240, 41sseldd 3589 . . . . 5 (𝜑𝑀 ∈ ℝ)
43 ioossre 12193 . . . . . 6 (𝑋(,)+∞) ⊆ ℝ
44 pntibndlem2.9 . . . . . 6 (𝜑𝑌 ∈ (𝑋(,)+∞))
4543, 44sseldi 3586 . . . . 5 (𝜑𝑌 ∈ ℝ)
4642, 45remulcld 10030 . . . 4 (𝜑 → (𝑀 · 𝑌) ∈ ℝ)
4719a1i 11 . . . . 5 (𝜑 → 2 ∈ ℝ)
48 eliooord 12191 . . . . . . . . . . . . 13 (𝐿 ∈ (0(,)1) → (0 < 𝐿𝐿 < 1))
4911, 48syl 17 . . . . . . . . . . . 12 (𝜑 → (0 < 𝐿𝐿 < 1))
5049simpld 475 . . . . . . . . . . 11 (𝜑 → 0 < 𝐿)
5112, 50elrpd 11829 . . . . . . . . . 10 (𝜑𝐿 ∈ ℝ+)
5251rpge0d 11836 . . . . . . . . 9 (𝜑 → 0 ≤ 𝐿)
5349simprd 479 . . . . . . . . 9 (𝜑𝐿 < 1)
5435rpge0d 11836 . . . . . . . . 9 (𝜑 → 0 ≤ 𝐸)
5533simprd 479 . . . . . . . . 9 (𝜑𝐸 < 1)
5612, 6, 14, 6, 52, 53, 54, 55ltmul12ad 10925 . . . . . . . 8 (𝜑 → (𝐿 · 𝐸) < (1 · 1))
57 1t1e1 11135 . . . . . . . 8 (1 · 1) = 1
5856, 57syl6breq 4664 . . . . . . 7 (𝜑 → (𝐿 · 𝐸) < 1)
5915, 6, 6, 58ltadd2dd 10156 . . . . . 6 (𝜑 → (1 + (𝐿 · 𝐸)) < (1 + 1))
60 df-2 11039 . . . . . 6 2 = (1 + 1)
6159, 60syl6breqr 4665 . . . . 5 (𝜑 → (1 + (𝐿 · 𝐸)) < 2)
6216, 47, 2, 61ltmul1dd 11887 . . . 4 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑁) < (2 · 𝑁))
634simprd 479 . . . . . 6 (𝜑𝑁 ≤ ((𝑀 / 2) · 𝑌))
6442recnd 10028 . . . . . . 7 (𝜑𝑀 ∈ ℂ)
6545recnd 10028 . . . . . . 7 (𝜑𝑌 ∈ ℂ)
66 rpcnne0 11810 . . . . . . . 8 (2 ∈ ℝ+ → (2 ∈ ℂ ∧ 2 ≠ 0))
6727, 66mp1i 13 . . . . . . 7 (𝜑 → (2 ∈ ℂ ∧ 2 ≠ 0))
68 div23 10664 . . . . . . 7 ((𝑀 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑀 · 𝑌) / 2) = ((𝑀 / 2) · 𝑌))
6964, 65, 67, 68syl3anc 1323 . . . . . 6 (𝜑 → ((𝑀 · 𝑌) / 2) = ((𝑀 / 2) · 𝑌))
7063, 69breqtrrd 4651 . . . . 5 (𝜑𝑁 ≤ ((𝑀 · 𝑌) / 2))
7117, 46, 28lemuldiv2d 11882 . . . . 5 (𝜑 → ((2 · 𝑁) ≤ (𝑀 · 𝑌) ↔ 𝑁 ≤ ((𝑀 · 𝑌) / 2)))
7270, 71mpbird 247 . . . 4 (𝜑 → (2 · 𝑁) ≤ (𝑀 · 𝑌))
7318, 21, 46, 62, 72ltletrd 10157 . . 3 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌))
74 pntibndlem3.2 . . . . . . . . . . . 12 (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)
75 pntibndlem3.k . . . . . . . . . . . 12 𝐾 = (exp‘(𝐵 / (𝐸 / 2)))
768, 9, 10, 74, 23, 75, 22, 13, 9, 1pntibndlem2a 25213 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ ℝ ∧ 𝑁𝑢𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁)))
7776simp1d 1071 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ ℝ)
782adantr 481 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ ℝ+)
7976simp2d 1072 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁𝑢)
8077, 78, 79rpgecld 11871 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ ℝ+)
818pntrf 25186 . . . . . . . . . 10 𝑅:ℝ+⟶ℝ
8281ffvelrni 6324 . . . . . . . . 9 (𝑢 ∈ ℝ+ → (𝑅𝑢) ∈ ℝ)
8380, 82syl 17 . . . . . . . 8 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑢) ∈ ℝ)
8483, 80rerpdivcld 11863 . . . . . . 7 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) / 𝑢) ∈ ℝ)
8584recnd 10028 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) / 𝑢) ∈ ℂ)
8685abscld 14125 . . . . 5 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) / 𝑢)) ∈ ℝ)
8781ffvelrni 6324 . . . . . . . . . . . 12 (𝑁 ∈ ℝ+ → (𝑅𝑁) ∈ ℝ)
882, 87syl 17 . . . . . . . . . . 11 (𝜑 → (𝑅𝑁) ∈ ℝ)
8988, 1nndivred 11029 . . . . . . . . . 10 (𝜑 → ((𝑅𝑁) / 𝑁) ∈ ℝ)
9089adantr 481 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑁) / 𝑁) ∈ ℝ)
9190recnd 10028 . . . . . . . 8 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑁) / 𝑁) ∈ ℂ)
9285, 91subcld 10352 . . . . . . 7 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁)) ∈ ℂ)
9392abscld 14125 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ∈ ℝ)
9491abscld 14125 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑁) / 𝑁)) ∈ ℝ)
9593, 94readdcld 10029 . . . . 5 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) + (abs‘((𝑅𝑁) / 𝑁))) ∈ ℝ)
9614adantr 481 . . . . 5 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐸 ∈ ℝ)
9785, 91abs2difd 14146 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) / 𝑢)) − (abs‘((𝑅𝑁) / 𝑁))) ≤ (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))))
9886, 94, 93lesubaddd 10584 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((abs‘((𝑅𝑢) / 𝑢)) − (abs‘((𝑅𝑁) / 𝑁))) ≤ (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ↔ (abs‘((𝑅𝑢) / 𝑢)) ≤ ((abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) + (abs‘((𝑅𝑁) / 𝑁)))))
9997, 98mpbid 222 . . . . 5 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) / 𝑢)) ≤ ((abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) + (abs‘((𝑅𝑁) / 𝑁))))
10096rehalfcld 11239 . . . . . . 7 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 2) ∈ ℝ)
10117adantr 481 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ ℝ)
10277, 101resubcld 10418 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢𝑁) ∈ ℝ)
103102, 78rerpdivcld 11863 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) / 𝑁) ∈ ℝ)
104 3re 11054 . . . . . . . . . . . 12 3 ∈ ℝ
105104a1i 11 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 3 ∈ ℝ)
10686, 105readdcld 10029 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) / 𝑢)) + 3) ∈ ℝ)
107103, 106remulcld 10030 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) ∈ ℝ)
108 pntibndlem2.5 . . . . . . . . . . . 12 (𝜑𝑇 ∈ ℝ+)
109108rpred 11832 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℝ)
110109adantr 481 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℝ)
111 1red 10015 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 ∈ ℝ)
112 4nn 11147 . . . . . . . . . . . . . . . . . 18 4 ∈ ℕ
113 nnrp 11802 . . . . . . . . . . . . . . . . . 18 (4 ∈ ℕ → 4 ∈ ℝ+)
114112, 113mp1i 13 . . . . . . . . . . . . . . . . 17 (𝜑 → 4 ∈ ℝ+)
11535, 114rpdivcld 11849 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 / 4) ∈ ℝ+)
116108, 115rpdivcld 11849 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇 / (𝐸 / 4)) ∈ ℝ+)
117116rpred 11832 . . . . . . . . . . . . . 14 (𝜑 → (𝑇 / (𝐸 / 4)) ∈ ℝ)
118117reefcld 14762 . . . . . . . . . . . . 13 (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) ∈ ℝ)
119118adantr 481 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(𝑇 / (𝐸 / 4))) ∈ ℝ)
120 efgt1 14790 . . . . . . . . . . . . . 14 ((𝑇 / (𝐸 / 4)) ∈ ℝ+ → 1 < (exp‘(𝑇 / (𝐸 / 4))))
121116, 120syl 17 . . . . . . . . . . . . 13 (𝜑 → 1 < (exp‘(𝑇 / (𝐸 / 4))))
122121adantr 481 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 < (exp‘(𝑇 / (𝐸 / 4))))
123 pntibndlem2.7 . . . . . . . . . . . . . . . 16 𝑋 = ((exp‘(𝑇 / (𝐸 / 4))) + 𝑍)
124 pntibndlem3.6 . . . . . . . . . . . . . . . . . 18 (𝜑𝑍 ∈ ℝ+)
125124rpred 11832 . . . . . . . . . . . . . . . . 17 (𝜑𝑍 ∈ ℝ)
126118, 125readdcld 10029 . . . . . . . . . . . . . . . 16 (𝜑 → ((exp‘(𝑇 / (𝐸 / 4))) + 𝑍) ∈ ℝ)
127123, 126syl5eqel 2702 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ ℝ)
128118, 124ltaddrpd 11865 . . . . . . . . . . . . . . . 16 (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < ((exp‘(𝑇 / (𝐸 / 4))) + 𝑍))
129128, 123syl6breqr 4665 . . . . . . . . . . . . . . 15 (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < 𝑋)
130 eliooord 12191 . . . . . . . . . . . . . . . . 17 (𝑌 ∈ (𝑋(,)+∞) → (𝑋 < 𝑌𝑌 < +∞))
13144, 130syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 < 𝑌𝑌 < +∞))
132131simpld 475 . . . . . . . . . . . . . . 15 (𝜑𝑋 < 𝑌)
133118, 127, 45, 129, 132lttrd 10158 . . . . . . . . . . . . . 14 (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < 𝑌)
134118, 45, 17, 133, 5lttrd 10158 . . . . . . . . . . . . 13 (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < 𝑁)
135134adantr 481 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(𝑇 / (𝐸 / 4))) < 𝑁)
136111, 119, 101, 122, 135lttrd 10158 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 < 𝑁)
137101, 136rplogcld 24313 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (log‘𝑁) ∈ ℝ+)
138110, 137rerpdivcld 11863 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℝ)
139107, 138readdcld 10029 . . . . . . . 8 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))) ∈ ℝ)
140 peano2re 10169 . . . . . . . . . . . 12 ((abs‘((𝑅𝑢) / 𝑢)) ∈ ℝ → ((abs‘((𝑅𝑢) / 𝑢)) + 1) ∈ ℝ)
14186, 140syl 17 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) / 𝑢)) + 1) ∈ ℝ)
142103, 141remulcld 10030 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) ∈ ℝ)
143 chpcl 24784 . . . . . . . . . . . . 13 (𝑢 ∈ ℝ → (ψ‘𝑢) ∈ ℝ)
14477, 143syl 17 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑢) ∈ ℝ)
145 chpcl 24784 . . . . . . . . . . . . 13 (𝑁 ∈ ℝ → (ψ‘𝑁) ∈ ℝ)
146101, 145syl 17 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑁) ∈ ℝ)
147144, 146resubcld 10418 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((ψ‘𝑢) − (ψ‘𝑁)) ∈ ℝ)
148147, 78rerpdivcld 11863 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ∈ ℝ)
149142, 148readdcld 10029 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) ∈ ℝ)
150103, 86remulcld 10030 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) ∈ ℝ)
15188adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑁) ∈ ℝ)
15283, 151resubcld 10418 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) − (𝑅𝑁)) ∈ ℝ)
153152recnd 10028 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) − (𝑅𝑁)) ∈ ℂ)
154153abscld 14125 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) − (𝑅𝑁))) ∈ ℝ)
155154, 78rerpdivcld 11863 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁) ∈ ℝ)
156150, 155readdcld 10029 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁)) ∈ ℝ)
157103, 84remulcld 10030 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) ∈ ℝ)
158157renegcld 10417 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) ∈ ℝ)
159158recnd 10028 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) ∈ ℂ)
160152, 78rerpdivcld 11863 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅𝑢) − (𝑅𝑁)) / 𝑁) ∈ ℝ)
161160recnd 10028 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅𝑢) − (𝑅𝑁)) / 𝑁) ∈ ℂ)
162159, 161abstrid 14145 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) + (((𝑅𝑢) − (𝑅𝑁)) / 𝑁))) ≤ ((abs‘-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))) + (abs‘(((𝑅𝑢) − (𝑅𝑁)) / 𝑁))))
16377recnd 10028 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ ℂ)
164101recnd 10028 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ ℂ)
16578rpne0d 11837 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ≠ 0)
166163, 164, 164, 165divsubdird 10800 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) / 𝑁) = ((𝑢 / 𝑁) − (𝑁 / 𝑁)))
167164, 165dividd 10759 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 / 𝑁) = 1)
168167oveq2d 6631 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) − (𝑁 / 𝑁)) = ((𝑢 / 𝑁) − 1))
169166, 168eqtrd 2655 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) / 𝑁) = ((𝑢 / 𝑁) − 1))
170169oveq1d 6630 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) = (((𝑢 / 𝑁) − 1) · ((𝑅𝑢) / 𝑢)))
17177, 78rerpdivcld 11863 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ∈ ℝ)
172171recnd 10028 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ∈ ℂ)
173 1cnd 10016 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 ∈ ℂ)
174172, 173, 85subdird 10447 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 / 𝑁) − 1) · ((𝑅𝑢) / 𝑢)) = (((𝑢 / 𝑁) · ((𝑅𝑢) / 𝑢)) − (1 · ((𝑅𝑢) / 𝑢))))
17580rpcnne0d 11841 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ ℂ ∧ 𝑢 ≠ 0))
17678rpcnne0d 11841 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
17783recnd 10028 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑢) ∈ ℂ)
178 dmdcan 10695 . . . . . . . . . . . . . . . . . . 19 (((𝑢 ∈ ℂ ∧ 𝑢 ≠ 0) ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ (𝑅𝑢) ∈ ℂ) → ((𝑢 / 𝑁) · ((𝑅𝑢) / 𝑢)) = ((𝑅𝑢) / 𝑁))
179175, 176, 177, 178syl3anc 1323 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) · ((𝑅𝑢) / 𝑢)) = ((𝑅𝑢) / 𝑁))
18085mulid2d 10018 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 · ((𝑅𝑢) / 𝑢)) = ((𝑅𝑢) / 𝑢))
181179, 180oveq12d 6633 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 / 𝑁) · ((𝑅𝑢) / 𝑢)) − (1 · ((𝑅𝑢) / 𝑢))) = (((𝑅𝑢) / 𝑁) − ((𝑅𝑢) / 𝑢)))
182170, 174, 1813eqtrd 2659 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) = (((𝑅𝑢) / 𝑁) − ((𝑅𝑢) / 𝑢)))
183182negeqd 10235 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) = -(((𝑅𝑢) / 𝑁) − ((𝑅𝑢) / 𝑢)))
18483, 78rerpdivcld 11863 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) / 𝑁) ∈ ℝ)
185184recnd 10028 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) / 𝑁) ∈ ℂ)
186185, 85negsubdi2d 10368 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑅𝑢) / 𝑁) − ((𝑅𝑢) / 𝑢)) = (((𝑅𝑢) / 𝑢) − ((𝑅𝑢) / 𝑁)))
187183, 186eqtrd 2655 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) = (((𝑅𝑢) / 𝑢) − ((𝑅𝑢) / 𝑁)))
188151recnd 10028 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑁) ∈ ℂ)
189177, 188, 164, 165divsubdird 10800 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅𝑢) − (𝑅𝑁)) / 𝑁) = (((𝑅𝑢) / 𝑁) − ((𝑅𝑁) / 𝑁)))
190187, 189oveq12d 6633 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) + (((𝑅𝑢) − (𝑅𝑁)) / 𝑁)) = ((((𝑅𝑢) / 𝑢) − ((𝑅𝑢) / 𝑁)) + (((𝑅𝑢) / 𝑁) − ((𝑅𝑁) / 𝑁))))
19185, 185, 91npncand 10376 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑅𝑢) / 𝑢) − ((𝑅𝑢) / 𝑁)) + (((𝑅𝑢) / 𝑁) − ((𝑅𝑁) / 𝑁))) = (((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁)))
192190, 191eqtrd 2655 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) + (((𝑅𝑢) − (𝑅𝑁)) / 𝑁)) = (((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁)))
193192fveq2d 6162 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) + (((𝑅𝑢) − (𝑅𝑁)) / 𝑁))) = (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))))
194157recnd 10028 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) ∈ ℂ)
195194absnegd 14138 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))) = (abs‘(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))))
196103recnd 10028 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) / 𝑁) ∈ ℂ)
197196, 85absmuld 14143 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))) = ((abs‘((𝑢𝑁) / 𝑁)) · (abs‘((𝑅𝑢) / 𝑢))))
19877, 101subge0d 10577 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (0 ≤ (𝑢𝑁) ↔ 𝑁𝑢))
19979, 198mpbird 247 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 0 ≤ (𝑢𝑁))
200102, 78, 199divge0d 11872 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 0 ≤ ((𝑢𝑁) / 𝑁))
201103, 200absidd 14111 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑢𝑁) / 𝑁)) = ((𝑢𝑁) / 𝑁))
202201oveq1d 6630 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑢𝑁) / 𝑁)) · (abs‘((𝑅𝑢) / 𝑢))) = (((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))))
203195, 197, 2023eqtrd 2659 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))) = (((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))))
204153, 164, 165absdivd 14144 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) − (𝑅𝑁)) / 𝑁)) = ((abs‘((𝑅𝑢) − (𝑅𝑁))) / (abs‘𝑁)))
20578rprege0d 11839 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁))
206 absid 13986 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → (abs‘𝑁) = 𝑁)
207205, 206syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘𝑁) = 𝑁)
208207oveq2d 6631 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) − (𝑅𝑁))) / (abs‘𝑁)) = ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁))
209204, 208eqtrd 2655 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) − (𝑅𝑁)) / 𝑁)) = ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁))
210203, 209oveq12d 6633 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))) + (abs‘(((𝑅𝑢) − (𝑅𝑁)) / 𝑁))) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁)))
211162, 193, 2103brtr3d 4654 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ≤ ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁)))
212102, 147readdcld 10029 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) ∈ ℝ)
213212, 78rerpdivcld 11863 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁) ∈ ℝ)
214147recnd 10028 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((ψ‘𝑢) − (ψ‘𝑁)) ∈ ℂ)
215164, 163subcld 10352 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁𝑢) ∈ ℂ)
216214, 215abstrid 14145 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢))) ≤ ((abs‘((ψ‘𝑢) − (ψ‘𝑁))) + (abs‘(𝑁𝑢))))
2178pntrval 25185 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ℝ+ → (𝑅𝑢) = ((ψ‘𝑢) − 𝑢))
21880, 217syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑢) = ((ψ‘𝑢) − 𝑢))
2198pntrval 25185 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℝ+ → (𝑅𝑁) = ((ψ‘𝑁) − 𝑁))
22078, 219syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑁) = ((ψ‘𝑁) − 𝑁))
221218, 220oveq12d 6633 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) − (𝑅𝑁)) = (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁)))
222144recnd 10028 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑢) ∈ ℂ)
223146recnd 10028 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑁) ∈ ℂ)
224 subadd4 10285 . . . . . . . . . . . . . . . . . 18 ((((ψ‘𝑢) ∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (((ψ‘𝑢) − (ψ‘𝑁)) − (𝑢𝑁)) = (((ψ‘𝑢) + 𝑁) − ((ψ‘𝑁) + 𝑢)))
225 sub4 10286 . . . . . . . . . . . . . . . . . 18 ((((ψ‘𝑢) ∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (((ψ‘𝑢) − (ψ‘𝑁)) − (𝑢𝑁)) = (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁)))
226 addsub4 10284 . . . . . . . . . . . . . . . . . . 19 ((((ψ‘𝑢) ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ ((ψ‘𝑁) ∈ ℂ ∧ 𝑢 ∈ ℂ)) → (((ψ‘𝑢) + 𝑁) − ((ψ‘𝑁) + 𝑢)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢)))
227226an42s 869 . . . . . . . . . . . . . . . . . 18 ((((ψ‘𝑢) ∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (((ψ‘𝑢) + 𝑁) − ((ψ‘𝑁) + 𝑢)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢)))
228224, 225, 2273eqtr3d 2663 . . . . . . . . . . . . . . . . 17 ((((ψ‘𝑢) ∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢)))
229222, 223, 163, 164, 228syl22anc 1324 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢)))
230221, 229eqtr2d 2656 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢)) = ((𝑅𝑢) − (𝑅𝑁)))
231230fveq2d 6162 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢))) = (abs‘((𝑅𝑢) − (𝑅𝑁))))
232 chpwordi 24817 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ 𝑁𝑢) → (ψ‘𝑁) ≤ (ψ‘𝑢))
233101, 77, 79, 232syl3anc 1323 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑁) ≤ (ψ‘𝑢))
234146, 144, 233abssubge0d 14120 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((ψ‘𝑢) − (ψ‘𝑁))) = ((ψ‘𝑢) − (ψ‘𝑁)))
235101, 77, 79abssuble0d 14121 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(𝑁𝑢)) = (𝑢𝑁))
236234, 235oveq12d 6633 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((ψ‘𝑢) − (ψ‘𝑁))) + (abs‘(𝑁𝑢))) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑢𝑁)))
237102recnd 10028 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢𝑁) ∈ ℂ)
238214, 237addcomd 10198 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑢𝑁)) = ((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))))
239236, 238eqtrd 2655 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((ψ‘𝑢) − (ψ‘𝑁))) + (abs‘(𝑁𝑢))) = ((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))))
240216, 231, 2393brtr3d 4654 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) − (𝑅𝑁))) ≤ ((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))))
241154, 212, 78, 240lediv1dd 11890 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁) ≤ (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁))
242155, 213, 150, 241leadd2dd 10602 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁)) ≤ ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁)))
243150recnd 10028 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) ∈ ℂ)
244148recnd 10028 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ∈ ℂ)
245243, 196, 244addassd 10022 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((𝑢𝑁) / 𝑁)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) / 𝑁) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁))))
24686recnd 10028 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) / 𝑢)) ∈ ℂ)
247196, 246, 173adddid 10024 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) / 𝑁) · 1)))
248196mulid1d 10017 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · 1) = ((𝑢𝑁) / 𝑁))
249248oveq2d 6631 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) / 𝑁) · 1)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((𝑢𝑁) / 𝑁)))
250247, 249eqtrd 2655 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((𝑢𝑁) / 𝑁)))
251250oveq1d 6630 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) = (((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((𝑢𝑁) / 𝑁)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)))
252237, 214, 164, 165divdird 10799 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁) = (((𝑢𝑁) / 𝑁) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)))
253252oveq2d 6631 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) / 𝑁) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁))))
254245, 251, 2533eqtr4d 2665 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁)))
255242, 254breqtrrd 4651 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁)) ≤ ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)))
25693, 156, 149, 211, 255letrd 10154 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ≤ ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)))
257 remulcl 9981 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ ((𝑢𝑁) / 𝑁) ∈ ℝ) → (2 · ((𝑢𝑁) / 𝑁)) ∈ ℝ)
25819, 103, 257sylancr 694 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · ((𝑢𝑁) / 𝑁)) ∈ ℝ)
259258, 138readdcld 10029 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))) ∈ ℝ)
260 remulcl 9981 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ (𝑢𝑁) ∈ ℝ) → (2 · (𝑢𝑁)) ∈ ℝ)
26119, 102, 260sylancr 694 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · (𝑢𝑁)) ∈ ℝ)
262101, 137rerpdivcld 11863 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 / (log‘𝑁)) ∈ ℝ)
263110, 262remulcld 10030 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℝ)
264261, 263readdcld 10029 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) ∈ ℝ)
26518adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((1 + (𝐿 · 𝐸)) · 𝑁) ∈ ℝ)
26621adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · 𝑁) ∈ ℝ)
26776simp3d 1073 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁))
268 ltle 10086 . . . . . . . . . . . . . . . . . . . 20 (((1 + (𝐿 · 𝐸)) ∈ ℝ ∧ 2 ∈ ℝ) → ((1 + (𝐿 · 𝐸)) < 2 → (1 + (𝐿 · 𝐸)) ≤ 2))
26916, 19, 268sylancl 693 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1 + (𝐿 · 𝐸)) < 2 → (1 + (𝐿 · 𝐸)) ≤ 2))
27061, 269mpd 15 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1 + (𝐿 · 𝐸)) ≤ 2)
271270adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 + (𝐿 · 𝐸)) ≤ 2)
27216adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 + (𝐿 · 𝐸)) ∈ ℝ)
27319a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 2 ∈ ℝ)
274272, 273, 78lemul1d 11875 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((1 + (𝐿 · 𝐸)) ≤ 2 ↔ ((1 + (𝐿 · 𝐸)) · 𝑁) ≤ (2 · 𝑁)))
275271, 274mpbid 222 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((1 + (𝐿 · 𝐸)) · 𝑁) ≤ (2 · 𝑁))
27677, 265, 266, 267, 275letrd 10154 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ≤ (2 · 𝑁))
277 elicc2 12196 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ) → (𝑢 ∈ (𝑁[,](2 · 𝑁)) ↔ (𝑢 ∈ ℝ ∧ 𝑁𝑢𝑢 ≤ (2 · 𝑁))))
278101, 266, 277syl2anc 692 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ (𝑁[,](2 · 𝑁)) ↔ (𝑢 ∈ ℝ ∧ 𝑁𝑢𝑢 ≤ (2 · 𝑁))))
27977, 79, 276, 278mpbir3and 1243 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ (𝑁[,](2 · 𝑁)))
280 1re 9999 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
281280rexri 10057 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ*
282 elioopnf 12225 . . . . . . . . . . . . . . . . 17 (1 ∈ ℝ* → (𝑁 ∈ (1(,)+∞) ↔ (𝑁 ∈ ℝ ∧ 1 < 𝑁)))
283281, 282ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (1(,)+∞) ↔ (𝑁 ∈ ℝ ∧ 1 < 𝑁))
284101, 136, 283sylanbrc 697 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ (1(,)+∞))
285 pntibndlem2.6 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))))
286285adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))))
287 id 22 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑁𝑥 = 𝑁)
288 oveq2 6623 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁))
289287, 288oveq12d 6633 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑁 → (𝑥[,](2 · 𝑥)) = (𝑁[,](2 · 𝑁)))
290 fveq2 6158 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑁 → (ψ‘𝑥) = (ψ‘𝑁))
291290oveq2d 6631 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑁 → ((ψ‘𝑦) − (ψ‘𝑥)) = ((ψ‘𝑦) − (ψ‘𝑁)))
292 oveq2 6623 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑁 → (𝑦𝑥) = (𝑦𝑁))
293292oveq2d 6631 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑁 → (2 · (𝑦𝑥)) = (2 · (𝑦𝑁)))
294 fveq2 6158 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑁 → (log‘𝑥) = (log‘𝑁))
295287, 294oveq12d 6633 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑁 → (𝑥 / (log‘𝑥)) = (𝑁 / (log‘𝑁)))
296295oveq2d 6631 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑁 → (𝑇 · (𝑥 / (log‘𝑥))) = (𝑇 · (𝑁 / (log‘𝑁))))
297293, 296oveq12d 6633 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑁 → ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))) = ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))
298291, 297breq12d 4636 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑁 → (((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))) ↔ ((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))))
299289, 298raleqbidv 3145 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑁 → (∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))) ↔ ∀𝑦 ∈ (𝑁[,](2 · 𝑁))((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))))
300299rspcv 3295 . . . . . . . . . . . . . . 15 (𝑁 ∈ (1(,)+∞) → (∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))) → ∀𝑦 ∈ (𝑁[,](2 · 𝑁))((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))))
301284, 286, 300sylc 65 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ∀𝑦 ∈ (𝑁[,](2 · 𝑁))((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))
302 fveq2 6158 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑢 → (ψ‘𝑦) = (ψ‘𝑢))
303302oveq1d 6630 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑢 → ((ψ‘𝑦) − (ψ‘𝑁)) = ((ψ‘𝑢) − (ψ‘𝑁)))
304 oveq1 6622 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑢 → (𝑦𝑁) = (𝑢𝑁))
305304oveq2d 6631 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑢 → (2 · (𝑦𝑁)) = (2 · (𝑢𝑁)))
306305oveq1d 6630 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑢 → ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) = ((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))
307303, 306breq12d 4636 . . . . . . . . . . . . . . 15 (𝑦 = 𝑢 → (((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) ↔ ((ψ‘𝑢) − (ψ‘𝑁)) ≤ ((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))))
308307rspcv 3295 . . . . . . . . . . . . . 14 (𝑢 ∈ (𝑁[,](2 · 𝑁)) → (∀𝑦 ∈ (𝑁[,](2 · 𝑁))((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) → ((ψ‘𝑢) − (ψ‘𝑁)) ≤ ((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))))
309279, 301, 308sylc 65 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((ψ‘𝑢) − (ψ‘𝑁)) ≤ ((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))
310147, 264, 78, 309lediv1dd 11890 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ≤ (((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁))
311261recnd 10028 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · (𝑢𝑁)) ∈ ℂ)
312108adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℝ+)
313312rpred 11832 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℝ)
314313, 262remulcld 10030 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℝ)
315314recnd 10028 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℂ)
316 divdir 10670 . . . . . . . . . . . . . 14 (((2 · (𝑢𝑁)) ∈ ℂ ∧ (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℂ ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) → (((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁) = (((2 · (𝑢𝑁)) / 𝑁) + ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁)))
317311, 315, 176, 316syl3anc 1323 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁) = (((2 · (𝑢𝑁)) / 𝑁) + ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁)))
318 2cnd 11053 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 2 ∈ ℂ)
319318, 237, 164, 165divassd 10796 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((2 · (𝑢𝑁)) / 𝑁) = (2 · ((𝑢𝑁) / 𝑁)))
320110recnd 10028 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℂ)
321137rpcnne0d 11841 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((log‘𝑁) ∈ ℂ ∧ (log‘𝑁) ≠ 0))
322 div12 10667 . . . . . . . . . . . . . . . . 17 ((𝑇 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ ((log‘𝑁) ∈ ℂ ∧ (log‘𝑁) ≠ 0)) → (𝑇 · (𝑁 / (log‘𝑁))) = (𝑁 · (𝑇 / (log‘𝑁))))
323320, 164, 321, 322syl3anc 1323 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) = (𝑁 · (𝑇 / (log‘𝑁))))
324323oveq1d 6630 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁) = ((𝑁 · (𝑇 / (log‘𝑁))) / 𝑁))
325312, 137rpdivcld 11849 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℝ+)
326325rpcnd 11834 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℂ)
327326, 164, 165divcan3d 10766 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑁 · (𝑇 / (log‘𝑁))) / 𝑁) = (𝑇 / (log‘𝑁)))
328324, 327eqtrd 2655 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁) = (𝑇 / (log‘𝑁)))
329319, 328oveq12d 6633 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((2 · (𝑢𝑁)) / 𝑁) + ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁)) = ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))))
330317, 329eqtrd 2655 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁) = ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))))
331310, 330breqtrd 4649 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ≤ ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))))
332148, 259, 142, 331leadd2dd 10602 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) ≤ ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁)))))
333142recnd 10028 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) ∈ ℂ)
334258recnd 10028 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · ((𝑢𝑁) / 𝑁)) ∈ ℂ)
335138recnd 10028 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℂ)
336333, 334, 335addassd 10022 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (2 · ((𝑢𝑁) / 𝑁))) + (𝑇 / (log‘𝑁))) = ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁)))))
337 2cn 11051 . . . . . . . . . . . . . . 15 2 ∈ ℂ
338 mulcom 9982 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ ((𝑢𝑁) / 𝑁) ∈ ℂ) → (2 · ((𝑢𝑁) / 𝑁)) = (((𝑢𝑁) / 𝑁) · 2))
339337, 196, 338sylancr 694 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · ((𝑢𝑁) / 𝑁)) = (((𝑢𝑁) / 𝑁) · 2))
340339oveq2d 6631 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (2 · ((𝑢𝑁) / 𝑁))) = ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((𝑢𝑁) / 𝑁) · 2)))
341141recnd 10028 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) / 𝑢)) + 1) ∈ ℂ)
342196, 341, 318adddid 10024 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · (((abs‘((𝑅𝑢) / 𝑢)) + 1) + 2)) = ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((𝑢𝑁) / 𝑁) · 2)))
343246, 173, 318addassd 10022 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((abs‘((𝑅𝑢) / 𝑢)) + 1) + 2) = ((abs‘((𝑅𝑢) / 𝑢)) + (1 + 2)))
344 1p2e3 11112 . . . . . . . . . . . . . . . 16 (1 + 2) = 3
345344oveq2i 6626 . . . . . . . . . . . . . . 15 ((abs‘((𝑅𝑢) / 𝑢)) + (1 + 2)) = ((abs‘((𝑅𝑢) / 𝑢)) + 3)
346343, 345syl6eq 2671 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((abs‘((𝑅𝑢) / 𝑢)) + 1) + 2) = ((abs‘((𝑅𝑢) / 𝑢)) + 3))
347346oveq2d 6631 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · (((abs‘((𝑅𝑢) / 𝑢)) + 1) + 2)) = (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)))
348340, 342, 3473eqtr2d 2661 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (2 · ((𝑢𝑁) / 𝑁))) = (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)))
349348oveq1d 6630 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (2 · ((𝑢𝑁) / 𝑁))) + (𝑇 / (log‘𝑁))) = ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))))
350336, 349eqtr3d 2657 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁)))) = ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))))
351332, 350breqtrd 4649 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) ≤ ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))))
35293, 149, 139, 256, 351letrd 10154 . . . . . . . 8 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ≤ ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))))
353100rehalfcld 11239 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) / 2) ∈ ℝ)
35477, 272, 78ledivmul2d 11886 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) ≤ (1 + (𝐿 · 𝐸)) ↔ 𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁)))
355267, 354mpbird 247 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ≤ (1 + (𝐿 · 𝐸)))
356 ax-1cn 9954 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
35715adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐿 · 𝐸) ∈ ℝ)
358357recnd 10028 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐿 · 𝐸) ∈ ℂ)
359 addcom 10182 . . . . . . . . . . . . . . . 16 ((1 ∈ ℂ ∧ (𝐿 · 𝐸) ∈ ℂ) → (1 + (𝐿 · 𝐸)) = ((𝐿 · 𝐸) + 1))
360356, 358, 359sylancr 694 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 + (𝐿 · 𝐸)) = ((𝐿 · 𝐸) + 1))
361355, 360breqtrd 4649 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ≤ ((𝐿 · 𝐸) + 1))
362171, 111, 357lesubaddd 10584 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 / 𝑁) − 1) ≤ (𝐿 · 𝐸) ↔ (𝑢 / 𝑁) ≤ ((𝐿 · 𝐸) + 1)))
363361, 362mpbird 247 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) − 1) ≤ (𝐿 · 𝐸))
364169, 363eqbrtrd 4645 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) / 𝑁) ≤ (𝐿 · 𝐸))
3659adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐴 ∈ ℝ+)
366365rpred 11832 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐴 ∈ ℝ)
36774adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)
368 fveq2 6158 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑢 → (𝑅𝑥) = (𝑅𝑢))
369 id 22 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑢𝑥 = 𝑢)
370368, 369oveq12d 6633 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑢 → ((𝑅𝑥) / 𝑥) = ((𝑅𝑢) / 𝑢))
371370fveq2d 6162 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑢 → (abs‘((𝑅𝑥) / 𝑥)) = (abs‘((𝑅𝑢) / 𝑢)))
372371breq1d 4633 . . . . . . . . . . . . . . 15 (𝑥 = 𝑢 → ((abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴 ↔ (abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐴))
373372rspcv 3295 . . . . . . . . . . . . . 14 (𝑢 ∈ ℝ+ → (∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴 → (abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐴))
37480, 367, 373sylc 65 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐴)
37586, 366, 105, 374leadd1dd 10601 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) / 𝑢)) + 3) ≤ (𝐴 + 3))
376103, 200jca 554 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) ∈ ℝ ∧ 0 ≤ ((𝑢𝑁) / 𝑁)))
377 3nn 11146 . . . . . . . . . . . . . . . 16 3 ∈ ℕ
378 nnrp 11802 . . . . . . . . . . . . . . . 16 (3 ∈ ℕ → 3 ∈ ℝ+)
379377, 378ax-mp 5 . . . . . . . . . . . . . . 15 3 ∈ ℝ+
380 rpaddcl 11814 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ+ ∧ 3 ∈ ℝ+) → (𝐴 + 3) ∈ ℝ+)
381365, 379, 380sylancl 693 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐴 + 3) ∈ ℝ+)
382381rprege0d 11839 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐴 + 3) ∈ ℝ ∧ 0 ≤ (𝐴 + 3)))
383 lemul12b 10840 . . . . . . . . . . . . 13 ((((((𝑢𝑁) / 𝑁) ∈ ℝ ∧ 0 ≤ ((𝑢𝑁) / 𝑁)) ∧ (𝐿 · 𝐸) ∈ ℝ) ∧ (((abs‘((𝑅𝑢) / 𝑢)) + 3) ∈ ℝ ∧ ((𝐴 + 3) ∈ ℝ ∧ 0 ≤ (𝐴 + 3)))) → ((((𝑢𝑁) / 𝑁) ≤ (𝐿 · 𝐸) ∧ ((abs‘((𝑅𝑢) / 𝑢)) + 3) ≤ (𝐴 + 3)) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) ≤ ((𝐿 · 𝐸) · (𝐴 + 3))))
384376, 357, 106, 382, 383syl22anc 1324 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) ≤ (𝐿 · 𝐸) ∧ ((abs‘((𝑅𝑢) / 𝑢)) + 3) ≤ (𝐴 + 3)) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) ≤ ((𝐿 · 𝐸) · (𝐴 + 3))))
385364, 375, 384mp2and 714 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) ≤ ((𝐿 · 𝐸) · (𝐴 + 3)))
38635adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐸 ∈ ℝ+)
387112, 113mp1i 13 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 4 ∈ ℝ+)
388386, 387rpdivcld 11849 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 4) ∈ ℝ+)
389388rpcnd 11834 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 4) ∈ ℂ)
390381rpcnd 11834 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐴 + 3) ∈ ℂ)
391381rpne0d 11837 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐴 + 3) ≠ 0)
392389, 390, 391divcan1d 10762 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝐸 / 4) / (𝐴 + 3)) · (𝐴 + 3)) = (𝐸 / 4))
39314recnd 10028 . . . . . . . . . . . . . . . . 17 (𝜑𝐸 ∈ ℂ)
394393adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐸 ∈ ℂ)
395387rpcnd 11834 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 4 ∈ ℂ)
396387rpne0d 11837 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 4 ≠ 0)
397394, 395, 396divrec2d 10765 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 4) = ((1 / 4) · 𝐸))
398397oveq1d 6630 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 4) / (𝐴 + 3)) = (((1 / 4) · 𝐸) / (𝐴 + 3)))
399 4cn 11058 . . . . . . . . . . . . . . . . . 18 4 ∈ ℂ
400 4ne0 11077 . . . . . . . . . . . . . . . . . 18 4 ≠ 0
401399, 400reccli 10715 . . . . . . . . . . . . . . . . 17 (1 / 4) ∈ ℂ
402401a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 / 4) ∈ ℂ)
403402, 394, 390, 391div23d 10798 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((1 / 4) · 𝐸) / (𝐴 + 3)) = (((1 / 4) / (𝐴 + 3)) · 𝐸))
40410oveq1i 6625 . . . . . . . . . . . . . . 15 (𝐿 · 𝐸) = (((1 / 4) / (𝐴 + 3)) · 𝐸)
405403, 404syl6eqr 2673 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((1 / 4) · 𝐸) / (𝐴 + 3)) = (𝐿 · 𝐸))
406398, 405eqtr2d 2656 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐿 · 𝐸) = ((𝐸 / 4) / (𝐴 + 3)))
407406oveq1d 6630 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐿 · 𝐸) · (𝐴 + 3)) = (((𝐸 / 4) / (𝐴 + 3)) · (𝐴 + 3)))
408 2ne0 11073 . . . . . . . . . . . . . . 15 2 ≠ 0
409408a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 2 ≠ 0)
410394, 318, 318, 409, 409divdiv1d 10792 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) / 2) = (𝐸 / (2 · 2)))
411 2t2e4 11137 . . . . . . . . . . . . . 14 (2 · 2) = 4
412411oveq2i 6626 . . . . . . . . . . . . 13 (𝐸 / (2 · 2)) = (𝐸 / 4)
413410, 412syl6eq 2671 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) / 2) = (𝐸 / 4))
414392, 407, 4133eqtr4d 2665 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐿 · 𝐸) · (𝐴 + 3)) = ((𝐸 / 2) / 2))
415385, 414breqtrd 4649 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) ≤ ((𝐸 / 2) / 2))
416117adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (𝐸 / 4)) ∈ ℝ)
417137rpred 11832 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (log‘𝑁) ∈ ℝ)
41878reeflogd 24308 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(log‘𝑁)) = 𝑁)
419135, 418breqtrrd 4651 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(𝑇 / (𝐸 / 4))) < (exp‘(log‘𝑁)))
420 eflt 14791 . . . . . . . . . . . . . . 15 (((𝑇 / (𝐸 / 4)) ∈ ℝ ∧ (log‘𝑁) ∈ ℝ) → ((𝑇 / (𝐸 / 4)) < (log‘𝑁) ↔ (exp‘(𝑇 / (𝐸 / 4))) < (exp‘(log‘𝑁))))
421416, 417, 420syl2anc 692 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑇 / (𝐸 / 4)) < (log‘𝑁) ↔ (exp‘(𝑇 / (𝐸 / 4))) < (exp‘(log‘𝑁))))
422419, 421mpbird 247 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (𝐸 / 4)) < (log‘𝑁))
423416, 417, 422ltled 10145 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (𝐸 / 4)) ≤ (log‘𝑁))
424110, 388, 137, 423lediv23d 11898 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ≤ (𝐸 / 4))
425424, 413breqtrrd 4651 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ≤ ((𝐸 / 2) / 2))
426107, 138, 353, 353, 415, 425le2addd 10606 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))) ≤ (((𝐸 / 2) / 2) + ((𝐸 / 2) / 2)))
427100recnd 10028 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 2) ∈ ℂ)
4284272halvesd 11238 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝐸 / 2) / 2) + ((𝐸 / 2) / 2)) = (𝐸 / 2))
429426, 428breqtrd 4649 . . . . . . . 8 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))) ≤ (𝐸 / 2))
43093, 139, 100, 352, 429letrd 10154 . . . . . . 7 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ≤ (𝐸 / 2))
4313simprd 479 . . . . . . . 8 (𝜑 → (abs‘((𝑅𝑁) / 𝑁)) ≤ (𝐸 / 2))
432431adantr 481 . . . . . . 7 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑁) / 𝑁)) ≤ (𝐸 / 2))
43393, 94, 100, 100, 430, 432le2addd 10606 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) + (abs‘((𝑅𝑁) / 𝑁))) ≤ ((𝐸 / 2) + (𝐸 / 2)))
4343942halvesd 11238 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸)
435433, 434breqtrd 4649 . . . . 5 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) + (abs‘((𝑅𝑁) / 𝑁))) ≤ 𝐸)
43686, 95, 96, 99, 435letrd 10154 . . . 4 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)
437436ralrimiva 2962 . . 3 (𝜑 → ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)
4385, 73, 437jca31 556 . 2 (𝜑 → ((𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
439 breq2 4627 . . . . 5 (𝑧 = 𝑁 → (𝑌 < 𝑧𝑌 < 𝑁))
440 oveq2 6623 . . . . . 6 (𝑧 = 𝑁 → ((1 + (𝐿 · 𝐸)) · 𝑧) = ((1 + (𝐿 · 𝐸)) · 𝑁))
441440breq1d 4633 . . . . 5 (𝑧 = 𝑁 → (((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌) ↔ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)))
442439, 441anbi12d 746 . . . 4 (𝑧 = 𝑁 → ((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ↔ (𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌))))
443 id 22 . . . . . 6 (𝑧 = 𝑁𝑧 = 𝑁)
444443, 440oveq12d 6633 . . . . 5 (𝑧 = 𝑁 → (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧)) = (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁)))
445444raleqdv 3137 . . . 4 (𝑧 = 𝑁 → (∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸 ↔ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
446442, 445anbi12d 746 . . 3 (𝑧 = 𝑁 → (((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸) ↔ ((𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)))
447446rspcev 3299 . 2 ((𝑁 ∈ ℝ+ ∧ ((𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)) → ∃𝑧 ∈ ℝ+ ((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
4482, 438, 447syl2anc 692 1 (𝜑 → ∃𝑧 ∈ ℝ+ ((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2908  wrex 2909  wss 3560   class class class wbr 4623  cmpt 4683  cfv 5857  (class class class)co 6615  cc 9894  cr 9895  0cc0 9896  1c1 9897   + caddc 9899   · cmul 9901  +∞cpnf 10031  *cxr 10033   < clt 10034  cle 10035  cmin 10226  -cneg 10227   / cdiv 10644  cn 10980  2c2 11030  3c3 11031  4c4 11032  +crp 11792  (,)cioo 12133  [,)cico 12135  [,]cicc 12136  abscabs 13924  expce 14736  logclog 24239  ψcchp 24753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-inf2 8498  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974  ax-addf 9975  ax-mulf 9976
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-iin 4495  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-se 5044  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-isom 5866  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-of 6862  df-om 7028  df-1st 7128  df-2nd 7129  df-supp 7256  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-2o 7521  df-oadd 7524  df-er 7702  df-map 7819  df-pm 7820  df-ixp 7869  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-fsupp 8236  df-fi 8277  df-sup 8308  df-inf 8309  df-oi 8375  df-card 8725  df-cda 8950  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-4 11041  df-5 11042  df-6 11043  df-7 11044  df-8 11045  df-9 11046  df-n0 11253  df-z 11338  df-dec 11454  df-uz 11648  df-q 11749  df-rp 11793  df-xneg 11906  df-xadd 11907  df-xmul 11908  df-ioo 12137  df-ioc 12138  df-ico 12139  df-icc 12140  df-fz 12285  df-fzo 12423  df-fl 12549  df-mod 12625  df-seq 12758  df-exp 12817  df-fac 13017  df-bc 13046  df-hash 13074  df-shft 13757  df-cj 13789  df-re 13790  df-im 13791  df-sqrt 13925  df-abs 13926  df-limsup 14152  df-clim 14169  df-rlim 14170  df-sum 14367  df-ef 14742  df-sin 14744  df-cos 14745  df-pi 14747  df-dvds 14927  df-gcd 15160  df-prm 15329  df-pc 15485  df-struct 15802  df-ndx 15803  df-slot 15804  df-base 15805  df-sets 15806  df-ress 15807  df-plusg 15894  df-mulr 15895  df-starv 15896  df-sca 15897  df-vsca 15898  df-ip 15899  df-tset 15900  df-ple 15901  df-ds 15904  df-unif 15905  df-hom 15906  df-cco 15907  df-rest 16023  df-topn 16024  df-0g 16042  df-gsum 16043  df-topgen 16044  df-pt 16045  df-prds 16048  df-xrs 16102  df-qtop 16107  df-imas 16108  df-xps 16110  df-mre 16186  df-mrc 16187  df-acs 16189  df-mgm 17182  df-sgrp 17224  df-mnd 17235  df-submnd 17276  df-mulg 17481  df-cntz 17690  df-cmn 18135  df-psmet 19678  df-xmet 19679  df-met 19680  df-bl 19681  df-mopn 19682  df-fbas 19683  df-fg 19684  df-cnfld 19687  df-top 20639  df-topon 20656  df-topsp 20677  df-bases 20690  df-cld 20763  df-ntr 20764  df-cls 20765  df-nei 20842  df-lp 20880  df-perf 20881  df-cn 20971  df-cnp 20972  df-haus 21059  df-tx 21305  df-hmeo 21498  df-fil 21590  df-fm 21682  df-flim 21683  df-flf 21684  df-xms 22065  df-ms 22066  df-tms 22067  df-cncf 22621  df-limc 23570  df-dv 23571  df-log 24241  df-vma 24758  df-chp 24759
This theorem is referenced by:  pntibndlem3  25215
  Copyright terms: Public domain W3C validator