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

Theorem pntibndlem2 26185
 Description: Lemma for pntibnd 26187. 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 12420 . 2 (𝜑𝑁 ∈ ℝ+)
3 pntibndlem2.11 . . . . 5 (𝜑 → ((𝑌 < 𝑁𝑁 ≤ ((𝑀 / 2) · 𝑌)) ∧ (abs‘((𝑅𝑁) / 𝑁)) ≤ (𝐸 / 2)))
43simpld 498 . . . 4 (𝜑 → (𝑌 < 𝑁𝑁 ≤ ((𝑀 / 2) · 𝑌)))
54simpld 498 . . 3 (𝜑𝑌 < 𝑁)
6 1red 10634 . . . . . 6 (𝜑 → 1 ∈ ℝ)
7 ioossre 12789 . . . . . . . 8 (0(,)1) ⊆ ℝ
8 pntibnd.r . . . . . . . . 9 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
9 pntibndlem1.1 . . . . . . . . 9 (𝜑𝐴 ∈ ℝ+)
10 pntibndlem1.l . . . . . . . . 9 𝐿 = ((1 / 4) / (𝐴 + 3))
118, 9, 10pntibndlem1 26183 . . . . . . . 8 (𝜑𝐿 ∈ (0(,)1))
127, 11sseldi 3913 . . . . . . 7 (𝜑𝐿 ∈ ℝ)
13 pntibndlem3.4 . . . . . . . 8 (𝜑𝐸 ∈ (0(,)1))
147, 13sseldi 3913 . . . . . . 7 (𝜑𝐸 ∈ ℝ)
1512, 14remulcld 10663 . . . . . 6 (𝜑 → (𝐿 · 𝐸) ∈ ℝ)
166, 15readdcld 10662 . . . . 5 (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ)
171nnred 11643 . . . . 5 (𝜑𝑁 ∈ ℝ)
1816, 17remulcld 10663 . . . 4 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑁) ∈ ℝ)
19 2re 11702 . . . . 5 2 ∈ ℝ
20 remulcl 10614 . . . . 5 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
2119, 17, 20sylancr 590 . . . 4 (𝜑 → (2 · 𝑁) ∈ ℝ)
22 pntibndlem3.c . . . . . . . . . 10 𝐶 = ((2 · 𝐵) + (log‘2))
23 pntibndlem3.3 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℝ+)
2423rpred 12422 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ)
25 remulcl 10614 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (2 · 𝐵) ∈ ℝ)
2619, 24, 25sylancr 590 . . . . . . . . . . 11 (𝜑 → (2 · 𝐵) ∈ ℝ)
27 2rp 12385 . . . . . . . . . . . . 13 2 ∈ ℝ+
2827a1i 11 . . . . . . . . . . . 12 (𝜑 → 2 ∈ ℝ+)
2928relogcld 25224 . . . . . . . . . . 11 (𝜑 → (log‘2) ∈ ℝ)
3026, 29readdcld 10662 . . . . . . . . . 10 (𝜑 → ((2 · 𝐵) + (log‘2)) ∈ ℝ)
3122, 30eqeltrid 2894 . . . . . . . . 9 (𝜑𝐶 ∈ ℝ)
32 eliooord 12787 . . . . . . . . . . . 12 (𝐸 ∈ (0(,)1) → (0 < 𝐸𝐸 < 1))
3313, 32syl 17 . . . . . . . . . . 11 (𝜑 → (0 < 𝐸𝐸 < 1))
3433simpld 498 . . . . . . . . . 10 (𝜑 → 0 < 𝐸)
3514, 34elrpd 12419 . . . . . . . . 9 (𝜑𝐸 ∈ ℝ+)
3631, 35rerpdivcld 12453 . . . . . . . 8 (𝜑 → (𝐶 / 𝐸) ∈ ℝ)
3736reefcld 15436 . . . . . . 7 (𝜑 → (exp‘(𝐶 / 𝐸)) ∈ ℝ)
38 pnfxr 10687 . . . . . . 7 +∞ ∈ ℝ*
39 icossre 12809 . . . . . . 7 (((exp‘(𝐶 / 𝐸)) ∈ ℝ ∧ +∞ ∈ ℝ*) → ((exp‘(𝐶 / 𝐸))[,)+∞) ⊆ ℝ)
4037, 38, 39sylancl 589 . . . . . 6 (𝜑 → ((exp‘(𝐶 / 𝐸))[,)+∞) ⊆ ℝ)
41 pntibndlem2.8 . . . . . 6 (𝜑𝑀 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞))
4240, 41sseldd 3916 . . . . 5 (𝜑𝑀 ∈ ℝ)
43 ioossre 12789 . . . . . 6 (𝑋(,)+∞) ⊆ ℝ
44 pntibndlem2.9 . . . . . 6 (𝜑𝑌 ∈ (𝑋(,)+∞))
4543, 44sseldi 3913 . . . . 5 (𝜑𝑌 ∈ ℝ)
4642, 45remulcld 10663 . . . 4 (𝜑 → (𝑀 · 𝑌) ∈ ℝ)
4719a1i 11 . . . . 5 (𝜑 → 2 ∈ ℝ)
48 eliooord 12787 . . . . . . . . . . . . 13 (𝐿 ∈ (0(,)1) → (0 < 𝐿𝐿 < 1))
4911, 48syl 17 . . . . . . . . . . . 12 (𝜑 → (0 < 𝐿𝐿 < 1))
5049simpld 498 . . . . . . . . . . 11 (𝜑 → 0 < 𝐿)
5112, 50elrpd 12419 . . . . . . . . . 10 (𝜑𝐿 ∈ ℝ+)
5251rpge0d 12426 . . . . . . . . 9 (𝜑 → 0 ≤ 𝐿)
5349simprd 499 . . . . . . . . 9 (𝜑𝐿 < 1)
5435rpge0d 12426 . . . . . . . . 9 (𝜑 → 0 ≤ 𝐸)
5533simprd 499 . . . . . . . . 9 (𝜑𝐸 < 1)
5612, 6, 14, 6, 52, 53, 54, 55ltmul12ad 11573 . . . . . . . 8 (𝜑 → (𝐿 · 𝐸) < (1 · 1))
57 1t1e1 11790 . . . . . . . 8 (1 · 1) = 1
5856, 57breqtrdi 5072 . . . . . . 7 (𝜑 → (𝐿 · 𝐸) < 1)
5915, 6, 6, 58ltadd2dd 10791 . . . . . 6 (𝜑 → (1 + (𝐿 · 𝐸)) < (1 + 1))
60 df-2 11691 . . . . . 6 2 = (1 + 1)
6159, 60breqtrrdi 5073 . . . . 5 (𝜑 → (1 + (𝐿 · 𝐸)) < 2)
6216, 47, 2, 61ltmul1dd 12477 . . . 4 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑁) < (2 · 𝑁))
634simprd 499 . . . . . 6 (𝜑𝑁 ≤ ((𝑀 / 2) · 𝑌))
6442recnd 10661 . . . . . . 7 (𝜑𝑀 ∈ ℂ)
6545recnd 10661 . . . . . . 7 (𝜑𝑌 ∈ ℂ)
66 rpcnne0 12398 . . . . . . . 8 (2 ∈ ℝ+ → (2 ∈ ℂ ∧ 2 ≠ 0))
6727, 66mp1i 13 . . . . . . 7 (𝜑 → (2 ∈ ℂ ∧ 2 ≠ 0))
68 div23 11309 . . . . . . 7 ((𝑀 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑀 · 𝑌) / 2) = ((𝑀 / 2) · 𝑌))
6964, 65, 67, 68syl3anc 1368 . . . . . 6 (𝜑 → ((𝑀 · 𝑌) / 2) = ((𝑀 / 2) · 𝑌))
7063, 69breqtrrd 5059 . . . . 5 (𝜑𝑁 ≤ ((𝑀 · 𝑌) / 2))
7117, 46, 28lemuldiv2d 12472 . . . . 5 (𝜑 → ((2 · 𝑁) ≤ (𝑀 · 𝑌) ↔ 𝑁 ≤ ((𝑀 · 𝑌) / 2)))
7270, 71mpbird 260 . . . 4 (𝜑 → (2 · 𝑁) ≤ (𝑀 · 𝑌))
7318, 21, 46, 62, 72ltletrd 10792 . . 3 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌))
74 pntibndlem3.2 . . . . . . . . . . . 12 (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)
75 pntibndlem3.k . . . . . . . . . . . 12 𝐾 = (exp‘(𝐵 / (𝐸 / 2)))
768, 9, 10, 74, 23, 75, 22, 13, 9, 1pntibndlem2a 26184 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ ℝ ∧ 𝑁𝑢𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁)))
7776simp1d 1139 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ ℝ)
782adantr 484 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ ℝ+)
7976simp2d 1140 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁𝑢)
8077, 78, 79rpgecld 12461 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ ℝ+)
818pntrf 26157 . . . . . . . . . 10 𝑅:ℝ+⟶ℝ
8281ffvelrni 6828 . . . . . . . . 9 (𝑢 ∈ ℝ+ → (𝑅𝑢) ∈ ℝ)
8380, 82syl 17 . . . . . . . 8 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑢) ∈ ℝ)
8483, 80rerpdivcld 12453 . . . . . . 7 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) / 𝑢) ∈ ℝ)
8584recnd 10661 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) / 𝑢) ∈ ℂ)
8685abscld 14791 . . . . 5 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) / 𝑢)) ∈ ℝ)
8781ffvelrni 6828 . . . . . . . . . . . 12 (𝑁 ∈ ℝ+ → (𝑅𝑁) ∈ ℝ)
882, 87syl 17 . . . . . . . . . . 11 (𝜑 → (𝑅𝑁) ∈ ℝ)
8988, 1nndivred 11682 . . . . . . . . . 10 (𝜑 → ((𝑅𝑁) / 𝑁) ∈ ℝ)
9089adantr 484 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑁) / 𝑁) ∈ ℝ)
9190recnd 10661 . . . . . . . 8 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑁) / 𝑁) ∈ ℂ)
9285, 91subcld 10989 . . . . . . 7 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁)) ∈ ℂ)
9392abscld 14791 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ∈ ℝ)
9491abscld 14791 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑁) / 𝑁)) ∈ ℝ)
9593, 94readdcld 10662 . . . . 5 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) + (abs‘((𝑅𝑁) / 𝑁))) ∈ ℝ)
9614adantr 484 . . . . 5 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐸 ∈ ℝ)
9785, 91abs2difd 14812 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) / 𝑢)) − (abs‘((𝑅𝑁) / 𝑁))) ≤ (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))))
9886, 94, 93lesubaddd 11229 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((abs‘((𝑅𝑢) / 𝑢)) − (abs‘((𝑅𝑁) / 𝑁))) ≤ (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ↔ (abs‘((𝑅𝑢) / 𝑢)) ≤ ((abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) + (abs‘((𝑅𝑁) / 𝑁)))))
9997, 98mpbid 235 . . . . 5 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) / 𝑢)) ≤ ((abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) + (abs‘((𝑅𝑁) / 𝑁))))
10096rehalfcld 11875 . . . . . . 7 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 2) ∈ ℝ)
10117adantr 484 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ ℝ)
10277, 101resubcld 11060 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢𝑁) ∈ ℝ)
103102, 78rerpdivcld 12453 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) / 𝑁) ∈ ℝ)
104 3re 11708 . . . . . . . . . . . 12 3 ∈ ℝ
105104a1i 11 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 3 ∈ ℝ)
10686, 105readdcld 10662 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) / 𝑢)) + 3) ∈ ℝ)
107103, 106remulcld 10663 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) ∈ ℝ)
108 pntibndlem2.5 . . . . . . . . . . . 12 (𝜑𝑇 ∈ ℝ+)
109108rpred 12422 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℝ)
110109adantr 484 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℝ)
111 1red 10634 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 ∈ ℝ)
112 4nn 11711 . . . . . . . . . . . . . . . . . 18 4 ∈ ℕ
113 nnrp 12391 . . . . . . . . . . . . . . . . . 18 (4 ∈ ℕ → 4 ∈ ℝ+)
114112, 113mp1i 13 . . . . . . . . . . . . . . . . 17 (𝜑 → 4 ∈ ℝ+)
11535, 114rpdivcld 12439 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 / 4) ∈ ℝ+)
116108, 115rpdivcld 12439 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇 / (𝐸 / 4)) ∈ ℝ+)
117116rpred 12422 . . . . . . . . . . . . . 14 (𝜑 → (𝑇 / (𝐸 / 4)) ∈ ℝ)
118117reefcld 15436 . . . . . . . . . . . . 13 (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) ∈ ℝ)
119118adantr 484 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(𝑇 / (𝐸 / 4))) ∈ ℝ)
120 efgt1 15464 . . . . . . . . . . . . . 14 ((𝑇 / (𝐸 / 4)) ∈ ℝ+ → 1 < (exp‘(𝑇 / (𝐸 / 4))))
121116, 120syl 17 . . . . . . . . . . . . 13 (𝜑 → 1 < (exp‘(𝑇 / (𝐸 / 4))))
122121adantr 484 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 < (exp‘(𝑇 / (𝐸 / 4))))
123 pntibndlem2.7 . . . . . . . . . . . . . . . 16 𝑋 = ((exp‘(𝑇 / (𝐸 / 4))) + 𝑍)
124 pntibndlem3.6 . . . . . . . . . . . . . . . . . 18 (𝜑𝑍 ∈ ℝ+)
125124rpred 12422 . . . . . . . . . . . . . . . . 17 (𝜑𝑍 ∈ ℝ)
126118, 125readdcld 10662 . . . . . . . . . . . . . . . 16 (𝜑 → ((exp‘(𝑇 / (𝐸 / 4))) + 𝑍) ∈ ℝ)
127123, 126eqeltrid 2894 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ ℝ)
128118, 124ltaddrpd 12455 . . . . . . . . . . . . . . . 16 (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < ((exp‘(𝑇 / (𝐸 / 4))) + 𝑍))
129128, 123breqtrrdi 5073 . . . . . . . . . . . . . . 15 (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < 𝑋)
130 eliooord 12787 . . . . . . . . . . . . . . . . 17 (𝑌 ∈ (𝑋(,)+∞) → (𝑋 < 𝑌𝑌 < +∞))
13144, 130syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 < 𝑌𝑌 < +∞))
132131simpld 498 . . . . . . . . . . . . . . 15 (𝜑𝑋 < 𝑌)
133118, 127, 45, 129, 132lttrd 10793 . . . . . . . . . . . . . 14 (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < 𝑌)
134118, 45, 17, 133, 5lttrd 10793 . . . . . . . . . . . . 13 (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < 𝑁)
135134adantr 484 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(𝑇 / (𝐸 / 4))) < 𝑁)
136111, 119, 101, 122, 135lttrd 10793 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 < 𝑁)
137101, 136rplogcld 25230 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (log‘𝑁) ∈ ℝ+)
138110, 137rerpdivcld 12453 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℝ)
139107, 138readdcld 10662 . . . . . . . 8 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))) ∈ ℝ)
140 peano2re 10805 . . . . . . . . . . . 12 ((abs‘((𝑅𝑢) / 𝑢)) ∈ ℝ → ((abs‘((𝑅𝑢) / 𝑢)) + 1) ∈ ℝ)
14186, 140syl 17 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) / 𝑢)) + 1) ∈ ℝ)
142103, 141remulcld 10663 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) ∈ ℝ)
143 chpcl 25719 . . . . . . . . . . . . 13 (𝑢 ∈ ℝ → (ψ‘𝑢) ∈ ℝ)
14477, 143syl 17 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑢) ∈ ℝ)
145 chpcl 25719 . . . . . . . . . . . . 13 (𝑁 ∈ ℝ → (ψ‘𝑁) ∈ ℝ)
146101, 145syl 17 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑁) ∈ ℝ)
147144, 146resubcld 11060 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((ψ‘𝑢) − (ψ‘𝑁)) ∈ ℝ)
148147, 78rerpdivcld 12453 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ∈ ℝ)
149142, 148readdcld 10662 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) ∈ ℝ)
150103, 86remulcld 10663 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) ∈ ℝ)
15188adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑁) ∈ ℝ)
15283, 151resubcld 11060 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) − (𝑅𝑁)) ∈ ℝ)
153152recnd 10661 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) − (𝑅𝑁)) ∈ ℂ)
154153abscld 14791 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) − (𝑅𝑁))) ∈ ℝ)
155154, 78rerpdivcld 12453 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁) ∈ ℝ)
156150, 155readdcld 10662 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁)) ∈ ℝ)
157103, 84remulcld 10663 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) ∈ ℝ)
158157renegcld 11059 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) ∈ ℝ)
159158recnd 10661 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) ∈ ℂ)
160152, 78rerpdivcld 12453 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅𝑢) − (𝑅𝑁)) / 𝑁) ∈ ℝ)
161160recnd 10661 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅𝑢) − (𝑅𝑁)) / 𝑁) ∈ ℂ)
162159, 161abstrid 14811 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) + (((𝑅𝑢) − (𝑅𝑁)) / 𝑁))) ≤ ((abs‘-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))) + (abs‘(((𝑅𝑢) − (𝑅𝑁)) / 𝑁))))
16377recnd 10661 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ ℂ)
164101recnd 10661 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ ℂ)
16578rpne0d 12427 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ≠ 0)
166163, 164, 164, 165divsubdird 11447 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) / 𝑁) = ((𝑢 / 𝑁) − (𝑁 / 𝑁)))
167164, 165dividd 11406 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 / 𝑁) = 1)
168167oveq2d 7152 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) − (𝑁 / 𝑁)) = ((𝑢 / 𝑁) − 1))
169166, 168eqtrd 2833 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) / 𝑁) = ((𝑢 / 𝑁) − 1))
170169oveq1d 7151 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) = (((𝑢 / 𝑁) − 1) · ((𝑅𝑢) / 𝑢)))
17177, 78rerpdivcld 12453 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ∈ ℝ)
172171recnd 10661 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ∈ ℂ)
173 1cnd 10628 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 ∈ ℂ)
174172, 173, 85subdird 11089 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 / 𝑁) − 1) · ((𝑅𝑢) / 𝑢)) = (((𝑢 / 𝑁) · ((𝑅𝑢) / 𝑢)) − (1 · ((𝑅𝑢) / 𝑢))))
17580rpcnne0d 12431 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ ℂ ∧ 𝑢 ≠ 0))
17678rpcnne0d 12431 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
17783recnd 10661 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑢) ∈ ℂ)
178 dmdcan 11342 . . . . . . . . . . . . . . . . . . 19 (((𝑢 ∈ ℂ ∧ 𝑢 ≠ 0) ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ (𝑅𝑢) ∈ ℂ) → ((𝑢 / 𝑁) · ((𝑅𝑢) / 𝑢)) = ((𝑅𝑢) / 𝑁))
179175, 176, 177, 178syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) · ((𝑅𝑢) / 𝑢)) = ((𝑅𝑢) / 𝑁))
18085mulid2d 10651 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 · ((𝑅𝑢) / 𝑢)) = ((𝑅𝑢) / 𝑢))
181179, 180oveq12d 7154 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 / 𝑁) · ((𝑅𝑢) / 𝑢)) − (1 · ((𝑅𝑢) / 𝑢))) = (((𝑅𝑢) / 𝑁) − ((𝑅𝑢) / 𝑢)))
182170, 174, 1813eqtrd 2837 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) = (((𝑅𝑢) / 𝑁) − ((𝑅𝑢) / 𝑢)))
183182negeqd 10872 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) = -(((𝑅𝑢) / 𝑁) − ((𝑅𝑢) / 𝑢)))
18483, 78rerpdivcld 12453 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) / 𝑁) ∈ ℝ)
185184recnd 10661 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) / 𝑁) ∈ ℂ)
186185, 85negsubdi2d 11005 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑅𝑢) / 𝑁) − ((𝑅𝑢) / 𝑢)) = (((𝑅𝑢) / 𝑢) − ((𝑅𝑢) / 𝑁)))
187183, 186eqtrd 2833 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) = (((𝑅𝑢) / 𝑢) − ((𝑅𝑢) / 𝑁)))
188151recnd 10661 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑁) ∈ ℂ)
189177, 188, 164, 165divsubdird 11447 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅𝑢) − (𝑅𝑁)) / 𝑁) = (((𝑅𝑢) / 𝑁) − ((𝑅𝑁) / 𝑁)))
190187, 189oveq12d 7154 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) + (((𝑅𝑢) − (𝑅𝑁)) / 𝑁)) = ((((𝑅𝑢) / 𝑢) − ((𝑅𝑢) / 𝑁)) + (((𝑅𝑢) / 𝑁) − ((𝑅𝑁) / 𝑁))))
19185, 185, 91npncand 11013 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑅𝑢) / 𝑢) − ((𝑅𝑢) / 𝑁)) + (((𝑅𝑢) / 𝑁) − ((𝑅𝑁) / 𝑁))) = (((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁)))
192190, 191eqtrd 2833 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) + (((𝑅𝑢) − (𝑅𝑁)) / 𝑁)) = (((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁)))
193192fveq2d 6650 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) + (((𝑅𝑢) − (𝑅𝑁)) / 𝑁))) = (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))))
194157recnd 10661 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) ∈ ℂ)
195194absnegd 14804 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))) = (abs‘(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))))
196103recnd 10661 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) / 𝑁) ∈ ℂ)
197196, 85absmuld 14809 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))) = ((abs‘((𝑢𝑁) / 𝑁)) · (abs‘((𝑅𝑢) / 𝑢))))
19877, 101subge0d 11222 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (0 ≤ (𝑢𝑁) ↔ 𝑁𝑢))
19979, 198mpbird 260 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 0 ≤ (𝑢𝑁))
200102, 78, 199divge0d 12462 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 0 ≤ ((𝑢𝑁) / 𝑁))
201103, 200absidd 14777 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑢𝑁) / 𝑁)) = ((𝑢𝑁) / 𝑁))
202201oveq1d 7151 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑢𝑁) / 𝑁)) · (abs‘((𝑅𝑢) / 𝑢))) = (((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))))
203195, 197, 2023eqtrd 2837 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))) = (((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))))
204153, 164, 165absdivd 14810 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) − (𝑅𝑁)) / 𝑁)) = ((abs‘((𝑅𝑢) − (𝑅𝑁))) / (abs‘𝑁)))
20578rprege0d 12429 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁))
206 absid 14651 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → (abs‘𝑁) = 𝑁)
207205, 206syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘𝑁) = 𝑁)
208207oveq2d 7152 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) − (𝑅𝑁))) / (abs‘𝑁)) = ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁))
209204, 208eqtrd 2833 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) − (𝑅𝑁)) / 𝑁)) = ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁))
210203, 209oveq12d 7154 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))) + (abs‘(((𝑅𝑢) − (𝑅𝑁)) / 𝑁))) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁)))
211162, 193, 2103brtr3d 5062 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ≤ ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁)))
212102, 147readdcld 10662 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) ∈ ℝ)
213212, 78rerpdivcld 12453 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁) ∈ ℝ)
214147recnd 10661 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((ψ‘𝑢) − (ψ‘𝑁)) ∈ ℂ)
215164, 163subcld 10989 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁𝑢) ∈ ℂ)
216214, 215abstrid 14811 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢))) ≤ ((abs‘((ψ‘𝑢) − (ψ‘𝑁))) + (abs‘(𝑁𝑢))))
2178pntrval 26156 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ℝ+ → (𝑅𝑢) = ((ψ‘𝑢) − 𝑢))
21880, 217syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑢) = ((ψ‘𝑢) − 𝑢))
2198pntrval 26156 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℝ+ → (𝑅𝑁) = ((ψ‘𝑁) − 𝑁))
22078, 219syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑁) = ((ψ‘𝑁) − 𝑁))
221218, 220oveq12d 7154 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) − (𝑅𝑁)) = (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁)))
222144recnd 10661 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑢) ∈ ℂ)
223146recnd 10661 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑁) ∈ ℂ)
224 subadd4 10922 . . . . . . . . . . . . . . . . . 18 ((((ψ‘𝑢) ∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (((ψ‘𝑢) − (ψ‘𝑁)) − (𝑢𝑁)) = (((ψ‘𝑢) + 𝑁) − ((ψ‘𝑁) + 𝑢)))
225 sub4 10923 . . . . . . . . . . . . . . . . . 18 ((((ψ‘𝑢) ∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (((ψ‘𝑢) − (ψ‘𝑁)) − (𝑢𝑁)) = (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁)))
226 addsub4 10921 . . . . . . . . . . . . . . . . . . 19 ((((ψ‘𝑢) ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ ((ψ‘𝑁) ∈ ℂ ∧ 𝑢 ∈ ℂ)) → (((ψ‘𝑢) + 𝑁) − ((ψ‘𝑁) + 𝑢)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢)))
227226an42s 660 . . . . . . . . . . . . . . . . . 18 ((((ψ‘𝑢) ∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (((ψ‘𝑢) + 𝑁) − ((ψ‘𝑁) + 𝑢)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢)))
228224, 225, 2273eqtr3d 2841 . . . . . . . . . . . . . . . . 17 ((((ψ‘𝑢) ∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢)))
229222, 223, 163, 164, 228syl22anc 837 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢)))
230221, 229eqtr2d 2834 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢)) = ((𝑅𝑢) − (𝑅𝑁)))
231230fveq2d 6650 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢))) = (abs‘((𝑅𝑢) − (𝑅𝑁))))
232102recnd 10661 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢𝑁) ∈ ℂ)
233 chpwordi 25752 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ 𝑁𝑢) → (ψ‘𝑁) ≤ (ψ‘𝑢))
234101, 77, 79, 233syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑁) ≤ (ψ‘𝑢))
235146, 144, 234abssubge0d 14786 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((ψ‘𝑢) − (ψ‘𝑁))) = ((ψ‘𝑢) − (ψ‘𝑁)))
236101, 77, 79abssuble0d 14787 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(𝑁𝑢)) = (𝑢𝑁))
237235, 236oveq12d 7154 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((ψ‘𝑢) − (ψ‘𝑁))) + (abs‘(𝑁𝑢))) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑢𝑁)))
238214, 232, 237comraddd 10846 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((ψ‘𝑢) − (ψ‘𝑁))) + (abs‘(𝑁𝑢))) = ((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))))
239216, 231, 2383brtr3d 5062 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) − (𝑅𝑁))) ≤ ((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))))
240154, 212, 78, 239lediv1dd 12480 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁) ≤ (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁))
241155, 213, 150, 240leadd2dd 11247 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁)) ≤ ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁)))
242150recnd 10661 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) ∈ ℂ)
243148recnd 10661 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ∈ ℂ)
244242, 196, 243addassd 10655 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((𝑢𝑁) / 𝑁)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) / 𝑁) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁))))
24586recnd 10661 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) / 𝑢)) ∈ ℂ)
246196, 245, 173adddid 10657 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) / 𝑁) · 1)))
247196mulid1d 10650 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · 1) = ((𝑢𝑁) / 𝑁))
248247oveq2d 7152 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) / 𝑁) · 1)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((𝑢𝑁) / 𝑁)))
249246, 248eqtrd 2833 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((𝑢𝑁) / 𝑁)))
250249oveq1d 7151 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) = (((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((𝑢𝑁) / 𝑁)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)))
251232, 214, 164, 165divdird 11446 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁) = (((𝑢𝑁) / 𝑁) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)))
252251oveq2d 7152 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) / 𝑁) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁))))
253244, 250, 2523eqtr4d 2843 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁)))
254241, 253breqtrrd 5059 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁)) ≤ ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)))
25593, 156, 149, 211, 254letrd 10789 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ≤ ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)))
256 remulcl 10614 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ ((𝑢𝑁) / 𝑁) ∈ ℝ) → (2 · ((𝑢𝑁) / 𝑁)) ∈ ℝ)
25719, 103, 256sylancr 590 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · ((𝑢𝑁) / 𝑁)) ∈ ℝ)
258257, 138readdcld 10662 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))) ∈ ℝ)
259 remulcl 10614 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ (𝑢𝑁) ∈ ℝ) → (2 · (𝑢𝑁)) ∈ ℝ)
26019, 102, 259sylancr 590 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · (𝑢𝑁)) ∈ ℝ)
261101, 137rerpdivcld 12453 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 / (log‘𝑁)) ∈ ℝ)
262110, 261remulcld 10663 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℝ)
263260, 262readdcld 10662 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) ∈ ℝ)
264 fveq2 6646 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑢 → (ψ‘𝑦) = (ψ‘𝑢))
265264oveq1d 7151 . . . . . . . . . . . . . . 15 (𝑦 = 𝑢 → ((ψ‘𝑦) − (ψ‘𝑁)) = ((ψ‘𝑢) − (ψ‘𝑁)))
266 oveq1 7143 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑢 → (𝑦𝑁) = (𝑢𝑁))
267266oveq2d 7152 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑢 → (2 · (𝑦𝑁)) = (2 · (𝑢𝑁)))
268267oveq1d 7151 . . . . . . . . . . . . . . 15 (𝑦 = 𝑢 → ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) = ((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))
269265, 268breq12d 5044 . . . . . . . . . . . . . 14 (𝑦 = 𝑢 → (((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) ↔ ((ψ‘𝑢) − (ψ‘𝑁)) ≤ ((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))))
270 id 22 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑁𝑥 = 𝑁)
271 oveq2 7144 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁))
272270, 271oveq12d 7154 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑁 → (𝑥[,](2 · 𝑥)) = (𝑁[,](2 · 𝑁)))
273 fveq2 6646 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑁 → (ψ‘𝑥) = (ψ‘𝑁))
274273oveq2d 7152 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑁 → ((ψ‘𝑦) − (ψ‘𝑥)) = ((ψ‘𝑦) − (ψ‘𝑁)))
275 oveq2 7144 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑁 → (𝑦𝑥) = (𝑦𝑁))
276275oveq2d 7152 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑁 → (2 · (𝑦𝑥)) = (2 · (𝑦𝑁)))
277 fveq2 6646 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑁 → (log‘𝑥) = (log‘𝑁))
278270, 277oveq12d 7154 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑁 → (𝑥 / (log‘𝑥)) = (𝑁 / (log‘𝑁)))
279278oveq2d 7152 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑁 → (𝑇 · (𝑥 / (log‘𝑥))) = (𝑇 · (𝑁 / (log‘𝑁))))
280276, 279oveq12d 7154 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑁 → ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))) = ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))
281274, 280breq12d 5044 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑁 → (((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))) ↔ ((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))))
282272, 281raleqbidv 3354 . . . . . . . . . . . . . . 15 (𝑥 = 𝑁 → (∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))) ↔ ∀𝑦 ∈ (𝑁[,](2 · 𝑁))((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))))
283 pntibndlem2.6 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))))
284283adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))))
285 1xr 10692 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ*
286 elioopnf 12824 . . . . . . . . . . . . . . . . 17 (1 ∈ ℝ* → (𝑁 ∈ (1(,)+∞) ↔ (𝑁 ∈ ℝ ∧ 1 < 𝑁)))
287285, 286ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (1(,)+∞) ↔ (𝑁 ∈ ℝ ∧ 1 < 𝑁))
288101, 136, 287sylanbrc 586 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ (1(,)+∞))
289282, 284, 288rspcdva 3573 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ∀𝑦 ∈ (𝑁[,](2 · 𝑁))((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))
29018adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((1 + (𝐿 · 𝐸)) · 𝑁) ∈ ℝ)
29121adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · 𝑁) ∈ ℝ)
29276simp3d 1141 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁))
293 ltle 10721 . . . . . . . . . . . . . . . . . . . 20 (((1 + (𝐿 · 𝐸)) ∈ ℝ ∧ 2 ∈ ℝ) → ((1 + (𝐿 · 𝐸)) < 2 → (1 + (𝐿 · 𝐸)) ≤ 2))
29416, 19, 293sylancl 589 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1 + (𝐿 · 𝐸)) < 2 → (1 + (𝐿 · 𝐸)) ≤ 2))
29561, 294mpd 15 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1 + (𝐿 · 𝐸)) ≤ 2)
296295adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 + (𝐿 · 𝐸)) ≤ 2)
29716adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 + (𝐿 · 𝐸)) ∈ ℝ)
29819a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 2 ∈ ℝ)
299297, 298, 78lemul1d 12465 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((1 + (𝐿 · 𝐸)) ≤ 2 ↔ ((1 + (𝐿 · 𝐸)) · 𝑁) ≤ (2 · 𝑁)))
300296, 299mpbid 235 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((1 + (𝐿 · 𝐸)) · 𝑁) ≤ (2 · 𝑁))
30177, 290, 291, 292, 300letrd 10789 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ≤ (2 · 𝑁))
302 elicc2 12793 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ) → (𝑢 ∈ (𝑁[,](2 · 𝑁)) ↔ (𝑢 ∈ ℝ ∧ 𝑁𝑢𝑢 ≤ (2 · 𝑁))))
303101, 291, 302syl2anc 587 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ (𝑁[,](2 · 𝑁)) ↔ (𝑢 ∈ ℝ ∧ 𝑁𝑢𝑢 ≤ (2 · 𝑁))))
30477, 79, 301, 303mpbir3and 1339 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ (𝑁[,](2 · 𝑁)))
305269, 289, 304rspcdva 3573 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((ψ‘𝑢) − (ψ‘𝑁)) ≤ ((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))
306147, 263, 78, 305lediv1dd 12480 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ≤ (((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁))
307260recnd 10661 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · (𝑢𝑁)) ∈ ℂ)
308108adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℝ+)
309308rpred 12422 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℝ)
310309, 261remulcld 10663 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℝ)
311310recnd 10661 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℂ)
312 divdir 11315 . . . . . . . . . . . . . 14 (((2 · (𝑢𝑁)) ∈ ℂ ∧ (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℂ ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) → (((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁) = (((2 · (𝑢𝑁)) / 𝑁) + ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁)))
313307, 311, 176, 312syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁) = (((2 · (𝑢𝑁)) / 𝑁) + ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁)))
314 2cnd 11706 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 2 ∈ ℂ)
315314, 232, 164, 165divassd 11443 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((2 · (𝑢𝑁)) / 𝑁) = (2 · ((𝑢𝑁) / 𝑁)))
316110recnd 10661 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℂ)
317137rpcnne0d 12431 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((log‘𝑁) ∈ ℂ ∧ (log‘𝑁) ≠ 0))
318 div12 11312 . . . . . . . . . . . . . . . . 17 ((𝑇 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ ((log‘𝑁) ∈ ℂ ∧ (log‘𝑁) ≠ 0)) → (𝑇 · (𝑁 / (log‘𝑁))) = (𝑁 · (𝑇 / (log‘𝑁))))
319316, 164, 317, 318syl3anc 1368 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) = (𝑁 · (𝑇 / (log‘𝑁))))
320319oveq1d 7151 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁) = ((𝑁 · (𝑇 / (log‘𝑁))) / 𝑁))
321308, 137rpdivcld 12439 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℝ+)
322321rpcnd 12424 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℂ)
323322, 164, 165divcan3d 11413 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑁 · (𝑇 / (log‘𝑁))) / 𝑁) = (𝑇 / (log‘𝑁)))
324320, 323eqtrd 2833 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁) = (𝑇 / (log‘𝑁)))
325315, 324oveq12d 7154 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((2 · (𝑢𝑁)) / 𝑁) + ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁)) = ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))))
326313, 325eqtrd 2833 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁) = ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))))
327306, 326breqtrd 5057 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ≤ ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))))
328148, 258, 142, 327leadd2dd 11247 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) ≤ ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁)))))
329142recnd 10661 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) ∈ ℂ)
330257recnd 10661 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · ((𝑢𝑁) / 𝑁)) ∈ ℂ)
331138recnd 10661 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℂ)
332329, 330, 331addassd 10655 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (2 · ((𝑢𝑁) / 𝑁))) + (𝑇 / (log‘𝑁))) = ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁)))))
333 2cn 11703 . . . . . . . . . . . . . . 15 2 ∈ ℂ
334 mulcom 10615 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ ((𝑢𝑁) / 𝑁) ∈ ℂ) → (2 · ((𝑢𝑁) / 𝑁)) = (((𝑢𝑁) / 𝑁) · 2))
335333, 196, 334sylancr 590 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · ((𝑢𝑁) / 𝑁)) = (((𝑢𝑁) / 𝑁) · 2))
336335oveq2d 7152 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (2 · ((𝑢𝑁) / 𝑁))) = ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((𝑢𝑁) / 𝑁) · 2)))
337141recnd 10661 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) / 𝑢)) + 1) ∈ ℂ)
338196, 337, 314adddid 10657 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · (((abs‘((𝑅𝑢) / 𝑢)) + 1) + 2)) = ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((𝑢𝑁) / 𝑁) · 2)))
339245, 173, 314addassd 10655 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((abs‘((𝑅𝑢) / 𝑢)) + 1) + 2) = ((abs‘((𝑅𝑢) / 𝑢)) + (1 + 2)))
340 1p2e3 11771 . . . . . . . . . . . . . . . 16 (1 + 2) = 3
341340oveq2i 7147 . . . . . . . . . . . . . . 15 ((abs‘((𝑅𝑢) / 𝑢)) + (1 + 2)) = ((abs‘((𝑅𝑢) / 𝑢)) + 3)
342339, 341eqtrdi 2849 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((abs‘((𝑅𝑢) / 𝑢)) + 1) + 2) = ((abs‘((𝑅𝑢) / 𝑢)) + 3))
343342oveq2d 7152 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · (((abs‘((𝑅𝑢) / 𝑢)) + 1) + 2)) = (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)))
344336, 338, 3433eqtr2d 2839 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (2 · ((𝑢𝑁) / 𝑁))) = (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)))
345344oveq1d 7151 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (2 · ((𝑢𝑁) / 𝑁))) + (𝑇 / (log‘𝑁))) = ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))))
346332, 345eqtr3d 2835 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁)))) = ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))))
347328, 346breqtrd 5057 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) ≤ ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))))
34893, 149, 139, 255, 347letrd 10789 . . . . . . . 8 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ≤ ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))))
349100rehalfcld 11875 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) / 2) ∈ ℝ)
35077, 297, 78ledivmul2d 12476 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) ≤ (1 + (𝐿 · 𝐸)) ↔ 𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁)))
351292, 350mpbird 260 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ≤ (1 + (𝐿 · 𝐸)))
352 ax-1cn 10587 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
35315adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐿 · 𝐸) ∈ ℝ)
354353recnd 10661 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐿 · 𝐸) ∈ ℂ)
355 addcom 10818 . . . . . . . . . . . . . . . 16 ((1 ∈ ℂ ∧ (𝐿 · 𝐸) ∈ ℂ) → (1 + (𝐿 · 𝐸)) = ((𝐿 · 𝐸) + 1))
356352, 354, 355sylancr 590 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 + (𝐿 · 𝐸)) = ((𝐿 · 𝐸) + 1))
357351, 356breqtrd 5057 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ≤ ((𝐿 · 𝐸) + 1))
358171, 111, 353lesubaddd 11229 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 / 𝑁) − 1) ≤ (𝐿 · 𝐸) ↔ (𝑢 / 𝑁) ≤ ((𝐿 · 𝐸) + 1)))
359357, 358mpbird 260 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) − 1) ≤ (𝐿 · 𝐸))
360169, 359eqbrtrd 5053 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) / 𝑁) ≤ (𝐿 · 𝐸))
3619adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐴 ∈ ℝ+)
362361rpred 12422 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐴 ∈ ℝ)
363 fveq2 6646 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑢 → (𝑅𝑥) = (𝑅𝑢))
364 id 22 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑢𝑥 = 𝑢)
365363, 364oveq12d 7154 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑢 → ((𝑅𝑥) / 𝑥) = ((𝑅𝑢) / 𝑢))
366365fveq2d 6650 . . . . . . . . . . . . . . 15 (𝑥 = 𝑢 → (abs‘((𝑅𝑥) / 𝑥)) = (abs‘((𝑅𝑢) / 𝑢)))
367366breq1d 5041 . . . . . . . . . . . . . 14 (𝑥 = 𝑢 → ((abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴 ↔ (abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐴))
36874adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)
369367, 368, 80rspcdva 3573 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐴)
37086, 362, 105, 369leadd1dd 11246 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) / 𝑢)) + 3) ≤ (𝐴 + 3))
371103, 200jca 515 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) ∈ ℝ ∧ 0 ≤ ((𝑢𝑁) / 𝑁)))
372 3rp 12386 . . . . . . . . . . . . . . 15 3 ∈ ℝ+
373 rpaddcl 12402 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ+ ∧ 3 ∈ ℝ+) → (𝐴 + 3) ∈ ℝ+)
374361, 372, 373sylancl 589 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐴 + 3) ∈ ℝ+)
375374rprege0d 12429 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐴 + 3) ∈ ℝ ∧ 0 ≤ (𝐴 + 3)))
376 lemul12b 11489 . . . . . . . . . . . . 13 ((((((𝑢𝑁) / 𝑁) ∈ ℝ ∧ 0 ≤ ((𝑢𝑁) / 𝑁)) ∧ (𝐿 · 𝐸) ∈ ℝ) ∧ (((abs‘((𝑅𝑢) / 𝑢)) + 3) ∈ ℝ ∧ ((𝐴 + 3) ∈ ℝ ∧ 0 ≤ (𝐴 + 3)))) → ((((𝑢𝑁) / 𝑁) ≤ (𝐿 · 𝐸) ∧ ((abs‘((𝑅𝑢) / 𝑢)) + 3) ≤ (𝐴 + 3)) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) ≤ ((𝐿 · 𝐸) · (𝐴 + 3))))
377371, 353, 106, 375, 376syl22anc 837 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) ≤ (𝐿 · 𝐸) ∧ ((abs‘((𝑅𝑢) / 𝑢)) + 3) ≤ (𝐴 + 3)) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) ≤ ((𝐿 · 𝐸) · (𝐴 + 3))))
378360, 370, 377mp2and 698 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) ≤ ((𝐿 · 𝐸) · (𝐴 + 3)))
37935adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐸 ∈ ℝ+)
380112, 113mp1i 13 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 4 ∈ ℝ+)
381379, 380rpdivcld 12439 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 4) ∈ ℝ+)
382381rpcnd 12424 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 4) ∈ ℂ)
383374rpcnd 12424 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐴 + 3) ∈ ℂ)
384374rpne0d 12427 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐴 + 3) ≠ 0)
385382, 383, 384divcan1d 11409 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝐸 / 4) / (𝐴 + 3)) · (𝐴 + 3)) = (𝐸 / 4))
38614recnd 10661 . . . . . . . . . . . . . . . . 17 (𝜑𝐸 ∈ ℂ)
387386adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐸 ∈ ℂ)
388380rpcnd 12424 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 4 ∈ ℂ)
389380rpne0d 12427 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 4 ≠ 0)
390387, 388, 389divrec2d 11412 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 4) = ((1 / 4) · 𝐸))
391390oveq1d 7151 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 4) / (𝐴 + 3)) = (((1 / 4) · 𝐸) / (𝐴 + 3)))
392 4cn 11713 . . . . . . . . . . . . . . . . . 18 4 ∈ ℂ
393 4ne0 11736 . . . . . . . . . . . . . . . . . 18 4 ≠ 0
394392, 393reccli 11362 . . . . . . . . . . . . . . . . 17 (1 / 4) ∈ ℂ
395394a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 / 4) ∈ ℂ)
396395, 387, 383, 384div23d 11445 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((1 / 4) · 𝐸) / (𝐴 + 3)) = (((1 / 4) / (𝐴 + 3)) · 𝐸))
39710oveq1i 7146 . . . . . . . . . . . . . . 15 (𝐿 · 𝐸) = (((1 / 4) / (𝐴 + 3)) · 𝐸)
398396, 397eqtr4di 2851 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((1 / 4) · 𝐸) / (𝐴 + 3)) = (𝐿 · 𝐸))
399391, 398eqtr2d 2834 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐿 · 𝐸) = ((𝐸 / 4) / (𝐴 + 3)))
400399oveq1d 7151 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐿 · 𝐸) · (𝐴 + 3)) = (((𝐸 / 4) / (𝐴 + 3)) · (𝐴 + 3)))
401 2ne0 11732 . . . . . . . . . . . . . . 15 2 ≠ 0
402401a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 2 ≠ 0)
403387, 314, 314, 402, 402divdiv1d 11439 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) / 2) = (𝐸 / (2 · 2)))
404 2t2e4 11792 . . . . . . . . . . . . . 14 (2 · 2) = 4
405404oveq2i 7147 . . . . . . . . . . . . 13 (𝐸 / (2 · 2)) = (𝐸 / 4)
406403, 405eqtrdi 2849 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) / 2) = (𝐸 / 4))
407385, 400, 4063eqtr4d 2843 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐿 · 𝐸) · (𝐴 + 3)) = ((𝐸 / 2) / 2))
408378, 407breqtrd 5057 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) ≤ ((𝐸 / 2) / 2))
409117adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (𝐸 / 4)) ∈ ℝ)
410137rpred 12422 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (log‘𝑁) ∈ ℝ)
41178reeflogd 25225 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(log‘𝑁)) = 𝑁)
412135, 411breqtrrd 5059 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(𝑇 / (𝐸 / 4))) < (exp‘(log‘𝑁)))
413 eflt 15465 . . . . . . . . . . . . . . 15 (((𝑇 / (𝐸 / 4)) ∈ ℝ ∧ (log‘𝑁) ∈ ℝ) → ((𝑇 / (𝐸 / 4)) < (log‘𝑁) ↔ (exp‘(𝑇 / (𝐸 / 4))) < (exp‘(log‘𝑁))))
414409, 410, 413syl2anc 587 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑇 / (𝐸 / 4)) < (log‘𝑁) ↔ (exp‘(𝑇 / (𝐸 / 4))) < (exp‘(log‘𝑁))))
415412, 414mpbird 260 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (𝐸 / 4)) < (log‘𝑁))
416409, 410, 415ltled 10780 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (𝐸 / 4)) ≤ (log‘𝑁))
417110, 381, 137, 416lediv23d 12490 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ≤ (𝐸 / 4))
418417, 406breqtrrd 5059 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ≤ ((𝐸 / 2) / 2))
419107, 138, 349, 349, 408, 418le2addd 11251 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))) ≤ (((𝐸 / 2) / 2) + ((𝐸 / 2) / 2)))
420100recnd 10661 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 2) ∈ ℂ)
4214202halvesd 11874 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝐸 / 2) / 2) + ((𝐸 / 2) / 2)) = (𝐸 / 2))
422419, 421breqtrd 5057 . . . . . . . 8 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))) ≤ (𝐸 / 2))
42393, 139, 100, 348, 422letrd 10789 . . . . . . 7 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ≤ (𝐸 / 2))
4243simprd 499 . . . . . . . 8 (𝜑 → (abs‘((𝑅𝑁) / 𝑁)) ≤ (𝐸 / 2))
425424adantr 484 . . . . . . 7 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑁) / 𝑁)) ≤ (𝐸 / 2))
42693, 94, 100, 100, 423, 425le2addd 11251 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) + (abs‘((𝑅𝑁) / 𝑁))) ≤ ((𝐸 / 2) + (𝐸 / 2)))
4273872halvesd 11874 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸)
428426, 427breqtrd 5057 . . . . 5 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) + (abs‘((𝑅𝑁) / 𝑁))) ≤ 𝐸)
42986, 95, 96, 99, 428letrd 10789 . . . 4 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)
430429ralrimiva 3149 . . 3 (𝜑 → ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)
4315, 73, 430jca31 518 . 2 (𝜑 → ((𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
432 breq2 5035 . . . . 5 (𝑧 = 𝑁 → (𝑌 < 𝑧𝑌 < 𝑁))
433 oveq2 7144 . . . . . 6 (𝑧 = 𝑁 → ((1 + (𝐿 · 𝐸)) · 𝑧) = ((1 + (𝐿 · 𝐸)) · 𝑁))
434433breq1d 5041 . . . . 5 (𝑧 = 𝑁 → (((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌) ↔ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)))
435432, 434anbi12d 633 . . . 4 (𝑧 = 𝑁 → ((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ↔ (𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌))))
436 id 22 . . . . . 6 (𝑧 = 𝑁𝑧 = 𝑁)
437436, 433oveq12d 7154 . . . . 5 (𝑧 = 𝑁 → (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧)) = (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁)))
438437raleqdv 3364 . . . 4 (𝑧 = 𝑁 → (∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸 ↔ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
439435, 438anbi12d 633 . . 3 (𝑧 = 𝑁 → (((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸) ↔ ((𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)))
440439rspcev 3571 . 2 ((𝑁 ∈ ℝ+ ∧ ((𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)) → ∃𝑧 ∈ ℝ+ ((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
4412, 431, 440syl2anc 587 1 (𝜑 → ∃𝑧 ∈ ℝ+ ((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107   ⊆ wss 3881   class class class wbr 5031   ↦ cmpt 5111  ‘cfv 6325  (class class class)co 7136  ℂcc 10527  ℝcr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534  +∞cpnf 10664  ℝ*cxr 10666   < clt 10667   ≤ cle 10668   − cmin 10862  -cneg 10863   / cdiv 11289  ℕcn 11628  2c2 11683  3c3 11684  4c4 11685  ℝ+crp 12380  (,)cioo 12729  [,)cico 12731  [,]cicc 12732  abscabs 14588  expce 15410  logclog 25156  ψcchp 25688 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-inf2 9091  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-iin 4885  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-se 5480  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-isom 6334  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-of 7391  df-om 7564  df-1st 7674  df-2nd 7675  df-supp 7817  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-2o 8089  df-oadd 8092  df-er 8275  df-map 8394  df-pm 8395  df-ixp 8448  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-fsupp 8821  df-fi 8862  df-sup 8893  df-inf 8894  df-oi 8961  df-dju 9317  df-card 9355  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11629  df-2 11691  df-3 11692  df-4 11693  df-5 11694  df-6 11695  df-7 11696  df-8 11697  df-9 11698  df-n0 11889  df-z 11973  df-dec 12090  df-uz 12235  df-q 12340  df-rp 12381  df-xneg 12498  df-xadd 12499  df-xmul 12500  df-ioo 12733  df-ioc 12734  df-ico 12735  df-icc 12736  df-fz 12889  df-fzo 13032  df-fl 13160  df-mod 13236  df-seq 13368  df-exp 13429  df-fac 13633  df-bc 13662  df-hash 13690  df-shft 14421  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-limsup 14823  df-clim 14840  df-rlim 14841  df-sum 15038  df-ef 15416  df-sin 15418  df-cos 15419  df-pi 15421  df-dvds 15603  df-gcd 15837  df-prm 16009  df-pc 16167  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-mulr 16574  df-starv 16575  df-sca 16576  df-vsca 16577  df-ip 16578  df-tset 16579  df-ple 16580  df-ds 16582  df-unif 16583  df-hom 16584  df-cco 16585  df-rest 16691  df-topn 16692  df-0g 16710  df-gsum 16711  df-topgen 16712  df-pt 16713  df-prds 16716  df-xrs 16770  df-qtop 16775  df-imas 16776  df-xps 16778  df-mre 16852  df-mrc 16853  df-acs 16855  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-submnd 17952  df-mulg 18221  df-cntz 18443  df-cmn 18904  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-mopn 20091  df-fbas 20092  df-fg 20093  df-cnfld 20096  df-top 21509  df-topon 21526  df-topsp 21548  df-bases 21561  df-cld 21634  df-ntr 21635  df-cls 21636  df-nei 21713  df-lp 21751  df-perf 21752  df-cn 21842  df-cnp 21843  df-haus 21930  df-tx 22177  df-hmeo 22370  df-fil 22461  df-fm 22553  df-flim 22554  df-flf 22555  df-xms 22937  df-ms 22938  df-tms 22939  df-cncf 23493  df-limc 24479  df-dv 24480  df-log 25158  df-vma 25693  df-chp 25694 This theorem is referenced by:  pntibndlem3  26186
 Copyright terms: Public domain W3C validator