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