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

Theorem pntibndlem2 27084
Description: Lemma for pntibnd 27086. 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 13011 . 2 (𝜑𝑁 ∈ ℝ+)
3 pntibndlem2.11 . . . . 5 (𝜑 → ((𝑌 < 𝑁𝑁 ≤ ((𝑀 / 2) · 𝑌)) ∧ (abs‘((𝑅𝑁) / 𝑁)) ≤ (𝐸 / 2)))
43simpld 496 . . . 4 (𝜑 → (𝑌 < 𝑁𝑁 ≤ ((𝑀 / 2) · 𝑌)))
54simpld 496 . . 3 (𝜑𝑌 < 𝑁)
6 1red 11212 . . . . . 6 (𝜑 → 1 ∈ ℝ)
7 ioossre 13382 . . . . . . . 8 (0(,)1) ⊆ ℝ
8 pntibnd.r . . . . . . . . 9 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
9 pntibndlem1.1 . . . . . . . . 9 (𝜑𝐴 ∈ ℝ+)
10 pntibndlem1.l . . . . . . . . 9 𝐿 = ((1 / 4) / (𝐴 + 3))
118, 9, 10pntibndlem1 27082 . . . . . . . 8 (𝜑𝐿 ∈ (0(,)1))
127, 11sselid 3980 . . . . . . 7 (𝜑𝐿 ∈ ℝ)
13 pntibndlem3.4 . . . . . . . 8 (𝜑𝐸 ∈ (0(,)1))
147, 13sselid 3980 . . . . . . 7 (𝜑𝐸 ∈ ℝ)
1512, 14remulcld 11241 . . . . . 6 (𝜑 → (𝐿 · 𝐸) ∈ ℝ)
166, 15readdcld 11240 . . . . 5 (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ)
171nnred 12224 . . . . 5 (𝜑𝑁 ∈ ℝ)
1816, 17remulcld 11241 . . . 4 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑁) ∈ ℝ)
19 2re 12283 . . . . 5 2 ∈ ℝ
20 remulcl 11192 . . . . 5 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
2119, 17, 20sylancr 588 . . . 4 (𝜑 → (2 · 𝑁) ∈ ℝ)
22 pntibndlem3.c . . . . . . . . . 10 𝐶 = ((2 · 𝐵) + (log‘2))
23 pntibndlem3.3 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℝ+)
2423rpred 13013 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ)
25 remulcl 11192 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (2 · 𝐵) ∈ ℝ)
2619, 24, 25sylancr 588 . . . . . . . . . . 11 (𝜑 → (2 · 𝐵) ∈ ℝ)
27 2rp 12976 . . . . . . . . . . . . 13 2 ∈ ℝ+
2827a1i 11 . . . . . . . . . . . 12 (𝜑 → 2 ∈ ℝ+)
2928relogcld 26123 . . . . . . . . . . 11 (𝜑 → (log‘2) ∈ ℝ)
3026, 29readdcld 11240 . . . . . . . . . 10 (𝜑 → ((2 · 𝐵) + (log‘2)) ∈ ℝ)
3122, 30eqeltrid 2838 . . . . . . . . 9 (𝜑𝐶 ∈ ℝ)
32 eliooord 13380 . . . . . . . . . . . 12 (𝐸 ∈ (0(,)1) → (0 < 𝐸𝐸 < 1))
3313, 32syl 17 . . . . . . . . . . 11 (𝜑 → (0 < 𝐸𝐸 < 1))
3433simpld 496 . . . . . . . . . 10 (𝜑 → 0 < 𝐸)
3514, 34elrpd 13010 . . . . . . . . 9 (𝜑𝐸 ∈ ℝ+)
3631, 35rerpdivcld 13044 . . . . . . . 8 (𝜑 → (𝐶 / 𝐸) ∈ ℝ)
3736reefcld 16028 . . . . . . 7 (𝜑 → (exp‘(𝐶 / 𝐸)) ∈ ℝ)
38 pnfxr 11265 . . . . . . 7 +∞ ∈ ℝ*
39 icossre 13402 . . . . . . 7 (((exp‘(𝐶 / 𝐸)) ∈ ℝ ∧ +∞ ∈ ℝ*) → ((exp‘(𝐶 / 𝐸))[,)+∞) ⊆ ℝ)
4037, 38, 39sylancl 587 . . . . . 6 (𝜑 → ((exp‘(𝐶 / 𝐸))[,)+∞) ⊆ ℝ)
41 pntibndlem2.8 . . . . . 6 (𝜑𝑀 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞))
4240, 41sseldd 3983 . . . . 5 (𝜑𝑀 ∈ ℝ)
43 ioossre 13382 . . . . . 6 (𝑋(,)+∞) ⊆ ℝ
44 pntibndlem2.9 . . . . . 6 (𝜑𝑌 ∈ (𝑋(,)+∞))
4543, 44sselid 3980 . . . . 5 (𝜑𝑌 ∈ ℝ)
4642, 45remulcld 11241 . . . 4 (𝜑 → (𝑀 · 𝑌) ∈ ℝ)
4719a1i 11 . . . . 5 (𝜑 → 2 ∈ ℝ)
48 eliooord 13380 . . . . . . . . . . . . 13 (𝐿 ∈ (0(,)1) → (0 < 𝐿𝐿 < 1))
4911, 48syl 17 . . . . . . . . . . . 12 (𝜑 → (0 < 𝐿𝐿 < 1))
5049simpld 496 . . . . . . . . . . 11 (𝜑 → 0 < 𝐿)
5112, 50elrpd 13010 . . . . . . . . . 10 (𝜑𝐿 ∈ ℝ+)
5251rpge0d 13017 . . . . . . . . 9 (𝜑 → 0 ≤ 𝐿)
5349simprd 497 . . . . . . . . 9 (𝜑𝐿 < 1)
5435rpge0d 13017 . . . . . . . . 9 (𝜑 → 0 ≤ 𝐸)
5533simprd 497 . . . . . . . . 9 (𝜑𝐸 < 1)
5612, 6, 14, 6, 52, 53, 54, 55ltmul12ad 12152 . . . . . . . 8 (𝜑 → (𝐿 · 𝐸) < (1 · 1))
57 1t1e1 12371 . . . . . . . 8 (1 · 1) = 1
5856, 57breqtrdi 5189 . . . . . . 7 (𝜑 → (𝐿 · 𝐸) < 1)
5915, 6, 6, 58ltadd2dd 11370 . . . . . 6 (𝜑 → (1 + (𝐿 · 𝐸)) < (1 + 1))
60 df-2 12272 . . . . . 6 2 = (1 + 1)
6159, 60breqtrrdi 5190 . . . . 5 (𝜑 → (1 + (𝐿 · 𝐸)) < 2)
6216, 47, 2, 61ltmul1dd 13068 . . . 4 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑁) < (2 · 𝑁))
634simprd 497 . . . . . 6 (𝜑𝑁 ≤ ((𝑀 / 2) · 𝑌))
6442recnd 11239 . . . . . . 7 (𝜑𝑀 ∈ ℂ)
6545recnd 11239 . . . . . . 7 (𝜑𝑌 ∈ ℂ)
66 rpcnne0 12989 . . . . . . . 8 (2 ∈ ℝ+ → (2 ∈ ℂ ∧ 2 ≠ 0))
6727, 66mp1i 13 . . . . . . 7 (𝜑 → (2 ∈ ℂ ∧ 2 ≠ 0))
68 div23 11888 . . . . . . 7 ((𝑀 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑀 · 𝑌) / 2) = ((𝑀 / 2) · 𝑌))
6964, 65, 67, 68syl3anc 1372 . . . . . 6 (𝜑 → ((𝑀 · 𝑌) / 2) = ((𝑀 / 2) · 𝑌))
7063, 69breqtrrd 5176 . . . . 5 (𝜑𝑁 ≤ ((𝑀 · 𝑌) / 2))
7117, 46, 28lemuldiv2d 13063 . . . . 5 (𝜑 → ((2 · 𝑁) ≤ (𝑀 · 𝑌) ↔ 𝑁 ≤ ((𝑀 · 𝑌) / 2)))
7270, 71mpbird 257 . . . 4 (𝜑 → (2 · 𝑁) ≤ (𝑀 · 𝑌))
7318, 21, 46, 62, 72ltletrd 11371 . . 3 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌))
74 pntibndlem3.2 . . . . . . . . . . . 12 (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)
75 pntibndlem3.k . . . . . . . . . . . 12 𝐾 = (exp‘(𝐵 / (𝐸 / 2)))
768, 9, 10, 74, 23, 75, 22, 13, 9, 1pntibndlem2a 27083 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ ℝ ∧ 𝑁𝑢𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁)))
7776simp1d 1143 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ ℝ)
782adantr 482 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ ℝ+)
7976simp2d 1144 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁𝑢)
8077, 78, 79rpgecld 13052 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ ℝ+)
818pntrf 27056 . . . . . . . . . 10 𝑅:ℝ+⟶ℝ
8281ffvelcdmi 7083 . . . . . . . . 9 (𝑢 ∈ ℝ+ → (𝑅𝑢) ∈ ℝ)
8380, 82syl 17 . . . . . . . 8 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑢) ∈ ℝ)
8483, 80rerpdivcld 13044 . . . . . . 7 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) / 𝑢) ∈ ℝ)
8584recnd 11239 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) / 𝑢) ∈ ℂ)
8685abscld 15380 . . . . 5 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) / 𝑢)) ∈ ℝ)
8781ffvelcdmi 7083 . . . . . . . . . . . 12 (𝑁 ∈ ℝ+ → (𝑅𝑁) ∈ ℝ)
882, 87syl 17 . . . . . . . . . . 11 (𝜑 → (𝑅𝑁) ∈ ℝ)
8988, 1nndivred 12263 . . . . . . . . . 10 (𝜑 → ((𝑅𝑁) / 𝑁) ∈ ℝ)
9089adantr 482 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑁) / 𝑁) ∈ ℝ)
9190recnd 11239 . . . . . . . 8 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑁) / 𝑁) ∈ ℂ)
9285, 91subcld 11568 . . . . . . 7 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁)) ∈ ℂ)
9392abscld 15380 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ∈ ℝ)
9491abscld 15380 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑁) / 𝑁)) ∈ ℝ)
9593, 94readdcld 11240 . . . . 5 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) + (abs‘((𝑅𝑁) / 𝑁))) ∈ ℝ)
9614adantr 482 . . . . 5 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐸 ∈ ℝ)
9785, 91abs2difd 15401 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) / 𝑢)) − (abs‘((𝑅𝑁) / 𝑁))) ≤ (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))))
9886, 94, 93lesubaddd 11808 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((abs‘((𝑅𝑢) / 𝑢)) − (abs‘((𝑅𝑁) / 𝑁))) ≤ (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ↔ (abs‘((𝑅𝑢) / 𝑢)) ≤ ((abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) + (abs‘((𝑅𝑁) / 𝑁)))))
9997, 98mpbid 231 . . . . 5 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) / 𝑢)) ≤ ((abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) + (abs‘((𝑅𝑁) / 𝑁))))
10096rehalfcld 12456 . . . . . . 7 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 2) ∈ ℝ)
10117adantr 482 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ ℝ)
10277, 101resubcld 11639 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢𝑁) ∈ ℝ)
103102, 78rerpdivcld 13044 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) / 𝑁) ∈ ℝ)
104 3re 12289 . . . . . . . . . . . 12 3 ∈ ℝ
105104a1i 11 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 3 ∈ ℝ)
10686, 105readdcld 11240 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) / 𝑢)) + 3) ∈ ℝ)
107103, 106remulcld 11241 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) ∈ ℝ)
108 pntibndlem2.5 . . . . . . . . . . . 12 (𝜑𝑇 ∈ ℝ+)
109108rpred 13013 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℝ)
110109adantr 482 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℝ)
111 1red 11212 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 ∈ ℝ)
112 4nn 12292 . . . . . . . . . . . . . . . . . 18 4 ∈ ℕ
113 nnrp 12982 . . . . . . . . . . . . . . . . . 18 (4 ∈ ℕ → 4 ∈ ℝ+)
114112, 113mp1i 13 . . . . . . . . . . . . . . . . 17 (𝜑 → 4 ∈ ℝ+)
11535, 114rpdivcld 13030 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 / 4) ∈ ℝ+)
116108, 115rpdivcld 13030 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇 / (𝐸 / 4)) ∈ ℝ+)
117116rpred 13013 . . . . . . . . . . . . . 14 (𝜑 → (𝑇 / (𝐸 / 4)) ∈ ℝ)
118117reefcld 16028 . . . . . . . . . . . . 13 (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) ∈ ℝ)
119118adantr 482 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(𝑇 / (𝐸 / 4))) ∈ ℝ)
120 efgt1 16056 . . . . . . . . . . . . . 14 ((𝑇 / (𝐸 / 4)) ∈ ℝ+ → 1 < (exp‘(𝑇 / (𝐸 / 4))))
121116, 120syl 17 . . . . . . . . . . . . 13 (𝜑 → 1 < (exp‘(𝑇 / (𝐸 / 4))))
122121adantr 482 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 < (exp‘(𝑇 / (𝐸 / 4))))
123 pntibndlem2.7 . . . . . . . . . . . . . . . 16 𝑋 = ((exp‘(𝑇 / (𝐸 / 4))) + 𝑍)
124 pntibndlem3.6 . . . . . . . . . . . . . . . . . 18 (𝜑𝑍 ∈ ℝ+)
125124rpred 13013 . . . . . . . . . . . . . . . . 17 (𝜑𝑍 ∈ ℝ)
126118, 125readdcld 11240 . . . . . . . . . . . . . . . 16 (𝜑 → ((exp‘(𝑇 / (𝐸 / 4))) + 𝑍) ∈ ℝ)
127123, 126eqeltrid 2838 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ ℝ)
128118, 124ltaddrpd 13046 . . . . . . . . . . . . . . . 16 (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < ((exp‘(𝑇 / (𝐸 / 4))) + 𝑍))
129128, 123breqtrrdi 5190 . . . . . . . . . . . . . . 15 (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < 𝑋)
130 eliooord 13380 . . . . . . . . . . . . . . . . 17 (𝑌 ∈ (𝑋(,)+∞) → (𝑋 < 𝑌𝑌 < +∞))
13144, 130syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 < 𝑌𝑌 < +∞))
132131simpld 496 . . . . . . . . . . . . . . 15 (𝜑𝑋 < 𝑌)
133118, 127, 45, 129, 132lttrd 11372 . . . . . . . . . . . . . 14 (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < 𝑌)
134118, 45, 17, 133, 5lttrd 11372 . . . . . . . . . . . . 13 (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < 𝑁)
135134adantr 482 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(𝑇 / (𝐸 / 4))) < 𝑁)
136111, 119, 101, 122, 135lttrd 11372 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 < 𝑁)
137101, 136rplogcld 26129 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (log‘𝑁) ∈ ℝ+)
138110, 137rerpdivcld 13044 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℝ)
139107, 138readdcld 11240 . . . . . . . 8 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))) ∈ ℝ)
140 peano2re 11384 . . . . . . . . . . . 12 ((abs‘((𝑅𝑢) / 𝑢)) ∈ ℝ → ((abs‘((𝑅𝑢) / 𝑢)) + 1) ∈ ℝ)
14186, 140syl 17 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) / 𝑢)) + 1) ∈ ℝ)
142103, 141remulcld 11241 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) ∈ ℝ)
143 chpcl 26618 . . . . . . . . . . . . 13 (𝑢 ∈ ℝ → (ψ‘𝑢) ∈ ℝ)
14477, 143syl 17 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑢) ∈ ℝ)
145 chpcl 26618 . . . . . . . . . . . . 13 (𝑁 ∈ ℝ → (ψ‘𝑁) ∈ ℝ)
146101, 145syl 17 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑁) ∈ ℝ)
147144, 146resubcld 11639 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((ψ‘𝑢) − (ψ‘𝑁)) ∈ ℝ)
148147, 78rerpdivcld 13044 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ∈ ℝ)
149142, 148readdcld 11240 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) ∈ ℝ)
150103, 86remulcld 11241 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) ∈ ℝ)
15188adantr 482 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑁) ∈ ℝ)
15283, 151resubcld 11639 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) − (𝑅𝑁)) ∈ ℝ)
153152recnd 11239 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) − (𝑅𝑁)) ∈ ℂ)
154153abscld 15380 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) − (𝑅𝑁))) ∈ ℝ)
155154, 78rerpdivcld 13044 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁) ∈ ℝ)
156150, 155readdcld 11240 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁)) ∈ ℝ)
157103, 84remulcld 11241 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) ∈ ℝ)
158157renegcld 11638 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) ∈ ℝ)
159158recnd 11239 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) ∈ ℂ)
160152, 78rerpdivcld 13044 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅𝑢) − (𝑅𝑁)) / 𝑁) ∈ ℝ)
161160recnd 11239 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅𝑢) − (𝑅𝑁)) / 𝑁) ∈ ℂ)
162159, 161abstrid 15400 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) + (((𝑅𝑢) − (𝑅𝑁)) / 𝑁))) ≤ ((abs‘-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))) + (abs‘(((𝑅𝑢) − (𝑅𝑁)) / 𝑁))))
16377recnd 11239 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ ℂ)
164101recnd 11239 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ ℂ)
16578rpne0d 13018 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ≠ 0)
166163, 164, 164, 165divsubdird 12026 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) / 𝑁) = ((𝑢 / 𝑁) − (𝑁 / 𝑁)))
167164, 165dividd 11985 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 / 𝑁) = 1)
168167oveq2d 7422 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) − (𝑁 / 𝑁)) = ((𝑢 / 𝑁) − 1))
169166, 168eqtrd 2773 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) / 𝑁) = ((𝑢 / 𝑁) − 1))
170169oveq1d 7421 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) = (((𝑢 / 𝑁) − 1) · ((𝑅𝑢) / 𝑢)))
17177, 78rerpdivcld 13044 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ∈ ℝ)
172171recnd 11239 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ∈ ℂ)
173 1cnd 11206 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 ∈ ℂ)
174172, 173, 85subdird 11668 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 / 𝑁) − 1) · ((𝑅𝑢) / 𝑢)) = (((𝑢 / 𝑁) · ((𝑅𝑢) / 𝑢)) − (1 · ((𝑅𝑢) / 𝑢))))
17580rpcnne0d 13022 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ ℂ ∧ 𝑢 ≠ 0))
17678rpcnne0d 13022 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
17783recnd 11239 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑢) ∈ ℂ)
178 dmdcan 11921 . . . . . . . . . . . . . . . . . . 19 (((𝑢 ∈ ℂ ∧ 𝑢 ≠ 0) ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ (𝑅𝑢) ∈ ℂ) → ((𝑢 / 𝑁) · ((𝑅𝑢) / 𝑢)) = ((𝑅𝑢) / 𝑁))
179175, 176, 177, 178syl3anc 1372 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) · ((𝑅𝑢) / 𝑢)) = ((𝑅𝑢) / 𝑁))
18085mullidd 11229 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 · ((𝑅𝑢) / 𝑢)) = ((𝑅𝑢) / 𝑢))
181179, 180oveq12d 7424 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 / 𝑁) · ((𝑅𝑢) / 𝑢)) − (1 · ((𝑅𝑢) / 𝑢))) = (((𝑅𝑢) / 𝑁) − ((𝑅𝑢) / 𝑢)))
182170, 174, 1813eqtrd 2777 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) = (((𝑅𝑢) / 𝑁) − ((𝑅𝑢) / 𝑢)))
183182negeqd 11451 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) = -(((𝑅𝑢) / 𝑁) − ((𝑅𝑢) / 𝑢)))
18483, 78rerpdivcld 13044 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) / 𝑁) ∈ ℝ)
185184recnd 11239 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) / 𝑁) ∈ ℂ)
186185, 85negsubdi2d 11584 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑅𝑢) / 𝑁) − ((𝑅𝑢) / 𝑢)) = (((𝑅𝑢) / 𝑢) − ((𝑅𝑢) / 𝑁)))
187183, 186eqtrd 2773 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) = (((𝑅𝑢) / 𝑢) − ((𝑅𝑢) / 𝑁)))
188151recnd 11239 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑁) ∈ ℂ)
189177, 188, 164, 165divsubdird 12026 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅𝑢) − (𝑅𝑁)) / 𝑁) = (((𝑅𝑢) / 𝑁) − ((𝑅𝑁) / 𝑁)))
190187, 189oveq12d 7424 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) + (((𝑅𝑢) − (𝑅𝑁)) / 𝑁)) = ((((𝑅𝑢) / 𝑢) − ((𝑅𝑢) / 𝑁)) + (((𝑅𝑢) / 𝑁) − ((𝑅𝑁) / 𝑁))))
19185, 185, 91npncand 11592 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑅𝑢) / 𝑢) − ((𝑅𝑢) / 𝑁)) + (((𝑅𝑢) / 𝑁) − ((𝑅𝑁) / 𝑁))) = (((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁)))
192190, 191eqtrd 2773 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) + (((𝑅𝑢) − (𝑅𝑁)) / 𝑁)) = (((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁)))
193192fveq2d 6893 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) + (((𝑅𝑢) − (𝑅𝑁)) / 𝑁))) = (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))))
194157recnd 11239 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢)) ∈ ℂ)
195194absnegd 15393 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))) = (abs‘(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))))
196103recnd 11239 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) / 𝑁) ∈ ℂ)
197196, 85absmuld 15398 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))) = ((abs‘((𝑢𝑁) / 𝑁)) · (abs‘((𝑅𝑢) / 𝑢))))
19877, 101subge0d 11801 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (0 ≤ (𝑢𝑁) ↔ 𝑁𝑢))
19979, 198mpbird 257 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 0 ≤ (𝑢𝑁))
200102, 78, 199divge0d 13053 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 0 ≤ ((𝑢𝑁) / 𝑁))
201103, 200absidd 15366 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑢𝑁) / 𝑁)) = ((𝑢𝑁) / 𝑁))
202201oveq1d 7421 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑢𝑁) / 𝑁)) · (abs‘((𝑅𝑢) / 𝑢))) = (((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))))
203195, 197, 2023eqtrd 2777 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))) = (((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))))
204153, 164, 165absdivd 15399 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) − (𝑅𝑁)) / 𝑁)) = ((abs‘((𝑅𝑢) − (𝑅𝑁))) / (abs‘𝑁)))
20578rprege0d 13020 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁))
206 absid 15240 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → (abs‘𝑁) = 𝑁)
207205, 206syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘𝑁) = 𝑁)
208207oveq2d 7422 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) − (𝑅𝑁))) / (abs‘𝑁)) = ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁))
209204, 208eqtrd 2773 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) − (𝑅𝑁)) / 𝑁)) = ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁))
210203, 209oveq12d 7424 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘-(((𝑢𝑁) / 𝑁) · ((𝑅𝑢) / 𝑢))) + (abs‘(((𝑅𝑢) − (𝑅𝑁)) / 𝑁))) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁)))
211162, 193, 2103brtr3d 5179 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ≤ ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁)))
212102, 147readdcld 11240 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) ∈ ℝ)
213212, 78rerpdivcld 13044 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁) ∈ ℝ)
214147recnd 11239 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((ψ‘𝑢) − (ψ‘𝑁)) ∈ ℂ)
215164, 163subcld 11568 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁𝑢) ∈ ℂ)
216214, 215abstrid 15400 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢))) ≤ ((abs‘((ψ‘𝑢) − (ψ‘𝑁))) + (abs‘(𝑁𝑢))))
2178pntrval 27055 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ℝ+ → (𝑅𝑢) = ((ψ‘𝑢) − 𝑢))
21880, 217syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑢) = ((ψ‘𝑢) − 𝑢))
2198pntrval 27055 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℝ+ → (𝑅𝑁) = ((ψ‘𝑁) − 𝑁))
22078, 219syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅𝑁) = ((ψ‘𝑁) − 𝑁))
221218, 220oveq12d 7424 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅𝑢) − (𝑅𝑁)) = (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁)))
222144recnd 11239 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑢) ∈ ℂ)
223146recnd 11239 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑁) ∈ ℂ)
224 subadd4 11501 . . . . . . . . . . . . . . . . . 18 ((((ψ‘𝑢) ∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (((ψ‘𝑢) − (ψ‘𝑁)) − (𝑢𝑁)) = (((ψ‘𝑢) + 𝑁) − ((ψ‘𝑁) + 𝑢)))
225 sub4 11502 . . . . . . . . . . . . . . . . . 18 ((((ψ‘𝑢) ∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (((ψ‘𝑢) − (ψ‘𝑁)) − (𝑢𝑁)) = (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁)))
226 addsub4 11500 . . . . . . . . . . . . . . . . . . 19 ((((ψ‘𝑢) ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ ((ψ‘𝑁) ∈ ℂ ∧ 𝑢 ∈ ℂ)) → (((ψ‘𝑢) + 𝑁) − ((ψ‘𝑁) + 𝑢)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢)))
227226an42s 660 . . . . . . . . . . . . . . . . . 18 ((((ψ‘𝑢) ∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (((ψ‘𝑢) + 𝑁) − ((ψ‘𝑁) + 𝑢)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢)))
228224, 225, 2273eqtr3d 2781 . . . . . . . . . . . . . . . . 17 ((((ψ‘𝑢) ∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢)))
229222, 223, 163, 164, 228syl22anc 838 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢)))
230221, 229eqtr2d 2774 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢)) = ((𝑅𝑢) − (𝑅𝑁)))
231230fveq2d 6893 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁𝑢))) = (abs‘((𝑅𝑢) − (𝑅𝑁))))
232102recnd 11239 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢𝑁) ∈ ℂ)
233 chpwordi 26651 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ 𝑁𝑢) → (ψ‘𝑁) ≤ (ψ‘𝑢))
234101, 77, 79, 233syl3anc 1372 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑁) ≤ (ψ‘𝑢))
235146, 144, 234abssubge0d 15375 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((ψ‘𝑢) − (ψ‘𝑁))) = ((ψ‘𝑢) − (ψ‘𝑁)))
236101, 77, 79abssuble0d 15376 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(𝑁𝑢)) = (𝑢𝑁))
237235, 236oveq12d 7424 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((ψ‘𝑢) − (ψ‘𝑁))) + (abs‘(𝑁𝑢))) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑢𝑁)))
238214, 232, 237comraddd 11425 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((ψ‘𝑢) − (ψ‘𝑁))) + (abs‘(𝑁𝑢))) = ((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))))
239216, 231, 2383brtr3d 5179 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) − (𝑅𝑁))) ≤ ((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))))
240154, 212, 78, 239lediv1dd 13071 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁) ≤ (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁))
241155, 213, 150, 240leadd2dd 11826 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁)) ≤ ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁)))
242150recnd 11239 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) ∈ ℂ)
243148recnd 11239 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ∈ ℂ)
244242, 196, 243addassd 11233 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((𝑢𝑁) / 𝑁)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) / 𝑁) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁))))
24586recnd 11239 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) / 𝑢)) ∈ ℂ)
246196, 245, 173adddid 11235 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) / 𝑁) · 1)))
247196mulridd 11228 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · 1) = ((𝑢𝑁) / 𝑁))
248247oveq2d 7422 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) / 𝑁) · 1)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((𝑢𝑁) / 𝑁)))
249246, 248eqtrd 2773 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((𝑢𝑁) / 𝑁)))
250249oveq1d 7421 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) = (((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((𝑢𝑁) / 𝑁)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)))
251232, 214, 164, 165divdird 12025 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁) = (((𝑢𝑁) / 𝑁) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)))
252251oveq2d 7422 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) / 𝑁) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁))))
253244, 250, 2523eqtr4d 2783 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) = ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + (((𝑢𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁)))
254241, 253breqtrrd 5176 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · (abs‘((𝑅𝑢) / 𝑢))) + ((abs‘((𝑅𝑢) − (𝑅𝑁))) / 𝑁)) ≤ ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)))
25593, 156, 149, 211, 254letrd 11368 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ≤ ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)))
256 remulcl 11192 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ ((𝑢𝑁) / 𝑁) ∈ ℝ) → (2 · ((𝑢𝑁) / 𝑁)) ∈ ℝ)
25719, 103, 256sylancr 588 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · ((𝑢𝑁) / 𝑁)) ∈ ℝ)
258257, 138readdcld 11240 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))) ∈ ℝ)
259 remulcl 11192 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ (𝑢𝑁) ∈ ℝ) → (2 · (𝑢𝑁)) ∈ ℝ)
26019, 102, 259sylancr 588 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · (𝑢𝑁)) ∈ ℝ)
261101, 137rerpdivcld 13044 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 / (log‘𝑁)) ∈ ℝ)
262110, 261remulcld 11241 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℝ)
263260, 262readdcld 11240 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) ∈ ℝ)
264 fveq2 6889 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑢 → (ψ‘𝑦) = (ψ‘𝑢))
265264oveq1d 7421 . . . . . . . . . . . . . . 15 (𝑦 = 𝑢 → ((ψ‘𝑦) − (ψ‘𝑁)) = ((ψ‘𝑢) − (ψ‘𝑁)))
266 oveq1 7413 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑢 → (𝑦𝑁) = (𝑢𝑁))
267266oveq2d 7422 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑢 → (2 · (𝑦𝑁)) = (2 · (𝑢𝑁)))
268267oveq1d 7421 . . . . . . . . . . . . . . 15 (𝑦 = 𝑢 → ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) = ((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))
269265, 268breq12d 5161 . . . . . . . . . . . . . 14 (𝑦 = 𝑢 → (((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) ↔ ((ψ‘𝑢) − (ψ‘𝑁)) ≤ ((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))))
270 id 22 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑁𝑥 = 𝑁)
271 oveq2 7414 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁))
272270, 271oveq12d 7424 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑁 → (𝑥[,](2 · 𝑥)) = (𝑁[,](2 · 𝑁)))
273 fveq2 6889 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑁 → (ψ‘𝑥) = (ψ‘𝑁))
274273oveq2d 7422 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑁 → ((ψ‘𝑦) − (ψ‘𝑥)) = ((ψ‘𝑦) − (ψ‘𝑁)))
275 oveq2 7414 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑁 → (𝑦𝑥) = (𝑦𝑁))
276275oveq2d 7422 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑁 → (2 · (𝑦𝑥)) = (2 · (𝑦𝑁)))
277 fveq2 6889 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑁 → (log‘𝑥) = (log‘𝑁))
278270, 277oveq12d 7424 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑁 → (𝑥 / (log‘𝑥)) = (𝑁 / (log‘𝑁)))
279278oveq2d 7422 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑁 → (𝑇 · (𝑥 / (log‘𝑥))) = (𝑇 · (𝑁 / (log‘𝑁))))
280276, 279oveq12d 7424 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑁 → ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))) = ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))
281274, 280breq12d 5161 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑁 → (((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))) ↔ ((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))))
282272, 281raleqbidv 3343 . . . . . . . . . . . . . . 15 (𝑥 = 𝑁 → (∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))) ↔ ∀𝑦 ∈ (𝑁[,](2 · 𝑁))((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))))
283 pntibndlem2.6 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))))
284283adantr 482 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))))
285 1xr 11270 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ*
286 elioopnf 13417 . . . . . . . . . . . . . . . . 17 (1 ∈ ℝ* → (𝑁 ∈ (1(,)+∞) ↔ (𝑁 ∈ ℝ ∧ 1 < 𝑁)))
287285, 286ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (1(,)+∞) ↔ (𝑁 ∈ ℝ ∧ 1 < 𝑁))
288101, 136, 287sylanbrc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ (1(,)+∞))
289282, 284, 288rspcdva 3614 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ∀𝑦 ∈ (𝑁[,](2 · 𝑁))((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))
29018adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((1 + (𝐿 · 𝐸)) · 𝑁) ∈ ℝ)
29121adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · 𝑁) ∈ ℝ)
29276simp3d 1145 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁))
293 ltle 11299 . . . . . . . . . . . . . . . . . . . 20 (((1 + (𝐿 · 𝐸)) ∈ ℝ ∧ 2 ∈ ℝ) → ((1 + (𝐿 · 𝐸)) < 2 → (1 + (𝐿 · 𝐸)) ≤ 2))
29416, 19, 293sylancl 587 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1 + (𝐿 · 𝐸)) < 2 → (1 + (𝐿 · 𝐸)) ≤ 2))
29561, 294mpd 15 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1 + (𝐿 · 𝐸)) ≤ 2)
296295adantr 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 + (𝐿 · 𝐸)) ≤ 2)
29716adantr 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 + (𝐿 · 𝐸)) ∈ ℝ)
29819a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 2 ∈ ℝ)
299297, 298, 78lemul1d 13056 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((1 + (𝐿 · 𝐸)) ≤ 2 ↔ ((1 + (𝐿 · 𝐸)) · 𝑁) ≤ (2 · 𝑁)))
300296, 299mpbid 231 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((1 + (𝐿 · 𝐸)) · 𝑁) ≤ (2 · 𝑁))
30177, 290, 291, 292, 300letrd 11368 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ≤ (2 · 𝑁))
302 elicc2 13386 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ) → (𝑢 ∈ (𝑁[,](2 · 𝑁)) ↔ (𝑢 ∈ ℝ ∧ 𝑁𝑢𝑢 ≤ (2 · 𝑁))))
303101, 291, 302syl2anc 585 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ (𝑁[,](2 · 𝑁)) ↔ (𝑢 ∈ ℝ ∧ 𝑁𝑢𝑢 ≤ (2 · 𝑁))))
30477, 79, 301, 303mpbir3and 1343 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ (𝑁[,](2 · 𝑁)))
305269, 289, 304rspcdva 3614 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((ψ‘𝑢) − (ψ‘𝑁)) ≤ ((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))
306147, 263, 78, 305lediv1dd 13071 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ≤ (((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁))
307260recnd 11239 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · (𝑢𝑁)) ∈ ℂ)
308108adantr 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℝ+)
309308rpred 13013 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℝ)
310309, 261remulcld 11241 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℝ)
311310recnd 11239 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℂ)
312 divdir 11894 . . . . . . . . . . . . . 14 (((2 · (𝑢𝑁)) ∈ ℂ ∧ (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℂ ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) → (((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁) = (((2 · (𝑢𝑁)) / 𝑁) + ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁)))
313307, 311, 176, 312syl3anc 1372 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁) = (((2 · (𝑢𝑁)) / 𝑁) + ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁)))
314 2cnd 12287 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 2 ∈ ℂ)
315314, 232, 164, 165divassd 12022 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((2 · (𝑢𝑁)) / 𝑁) = (2 · ((𝑢𝑁) / 𝑁)))
316110recnd 11239 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℂ)
317137rpcnne0d 13022 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((log‘𝑁) ∈ ℂ ∧ (log‘𝑁) ≠ 0))
318 div12 11891 . . . . . . . . . . . . . . . . 17 ((𝑇 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ ((log‘𝑁) ∈ ℂ ∧ (log‘𝑁) ≠ 0)) → (𝑇 · (𝑁 / (log‘𝑁))) = (𝑁 · (𝑇 / (log‘𝑁))))
319316, 164, 317, 318syl3anc 1372 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) = (𝑁 · (𝑇 / (log‘𝑁))))
320319oveq1d 7421 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁) = ((𝑁 · (𝑇 / (log‘𝑁))) / 𝑁))
321308, 137rpdivcld 13030 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℝ+)
322321rpcnd 13015 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℂ)
323322, 164, 165divcan3d 11992 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑁 · (𝑇 / (log‘𝑁))) / 𝑁) = (𝑇 / (log‘𝑁)))
324320, 323eqtrd 2773 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁) = (𝑇 / (log‘𝑁)))
325315, 324oveq12d 7424 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((2 · (𝑢𝑁)) / 𝑁) + ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁)) = ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))))
326313, 325eqtrd 2773 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((2 · (𝑢𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁) = ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))))
327306, 326breqtrd 5174 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ≤ ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))))
328148, 258, 142, 327leadd2dd 11826 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) ≤ ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁)))))
329142recnd 11239 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) ∈ ℂ)
330257recnd 11239 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · ((𝑢𝑁) / 𝑁)) ∈ ℂ)
331138recnd 11239 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℂ)
332329, 330, 331addassd 11233 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (2 · ((𝑢𝑁) / 𝑁))) + (𝑇 / (log‘𝑁))) = ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁)))))
333 2cn 12284 . . . . . . . . . . . . . . 15 2 ∈ ℂ
334 mulcom 11193 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ ((𝑢𝑁) / 𝑁) ∈ ℂ) → (2 · ((𝑢𝑁) / 𝑁)) = (((𝑢𝑁) / 𝑁) · 2))
335333, 196, 334sylancr 588 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · ((𝑢𝑁) / 𝑁)) = (((𝑢𝑁) / 𝑁) · 2))
336335oveq2d 7422 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (2 · ((𝑢𝑁) / 𝑁))) = ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((𝑢𝑁) / 𝑁) · 2)))
337141recnd 11239 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) / 𝑢)) + 1) ∈ ℂ)
338196, 337, 314adddid 11235 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · (((abs‘((𝑅𝑢) / 𝑢)) + 1) + 2)) = ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((𝑢𝑁) / 𝑁) · 2)))
339245, 173, 314addassd 11233 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((abs‘((𝑅𝑢) / 𝑢)) + 1) + 2) = ((abs‘((𝑅𝑢) / 𝑢)) + (1 + 2)))
340 1p2e3 12352 . . . . . . . . . . . . . . . 16 (1 + 2) = 3
341340oveq2i 7417 . . . . . . . . . . . . . . 15 ((abs‘((𝑅𝑢) / 𝑢)) + (1 + 2)) = ((abs‘((𝑅𝑢) / 𝑢)) + 3)
342339, 341eqtrdi 2789 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((abs‘((𝑅𝑢) / 𝑢)) + 1) + 2) = ((abs‘((𝑅𝑢) / 𝑢)) + 3))
343342oveq2d 7422 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · (((abs‘((𝑅𝑢) / 𝑢)) + 1) + 2)) = (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)))
344336, 338, 3433eqtr2d 2779 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (2 · ((𝑢𝑁) / 𝑁))) = (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)))
345344oveq1d 7421 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (2 · ((𝑢𝑁) / 𝑁))) + (𝑇 / (log‘𝑁))) = ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))))
346332, 345eqtr3d 2775 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + ((2 · ((𝑢𝑁) / 𝑁)) + (𝑇 / (log‘𝑁)))) = ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))))
347328, 346breqtrd 5174 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) ≤ ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))))
34893, 149, 139, 255, 347letrd 11368 . . . . . . . 8 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ≤ ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))))
349100rehalfcld 12456 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) / 2) ∈ ℝ)
35077, 297, 78ledivmul2d 13067 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) ≤ (1 + (𝐿 · 𝐸)) ↔ 𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁)))
351292, 350mpbird 257 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ≤ (1 + (𝐿 · 𝐸)))
352 ax-1cn 11165 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
35315adantr 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐿 · 𝐸) ∈ ℝ)
354353recnd 11239 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐿 · 𝐸) ∈ ℂ)
355 addcom 11397 . . . . . . . . . . . . . . . 16 ((1 ∈ ℂ ∧ (𝐿 · 𝐸) ∈ ℂ) → (1 + (𝐿 · 𝐸)) = ((𝐿 · 𝐸) + 1))
356352, 354, 355sylancr 588 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 + (𝐿 · 𝐸)) = ((𝐿 · 𝐸) + 1))
357351, 356breqtrd 5174 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ≤ ((𝐿 · 𝐸) + 1))
358171, 111, 353lesubaddd 11808 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 / 𝑁) − 1) ≤ (𝐿 · 𝐸) ↔ (𝑢 / 𝑁) ≤ ((𝐿 · 𝐸) + 1)))
359357, 358mpbird 257 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) − 1) ≤ (𝐿 · 𝐸))
360169, 359eqbrtrd 5170 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢𝑁) / 𝑁) ≤ (𝐿 · 𝐸))
3619adantr 482 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐴 ∈ ℝ+)
362361rpred 13013 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐴 ∈ ℝ)
363 fveq2 6889 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑢 → (𝑅𝑥) = (𝑅𝑢))
364 id 22 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑢𝑥 = 𝑢)
365363, 364oveq12d 7424 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑢 → ((𝑅𝑥) / 𝑥) = ((𝑅𝑢) / 𝑢))
366365fveq2d 6893 . . . . . . . . . . . . . . 15 (𝑥 = 𝑢 → (abs‘((𝑅𝑥) / 𝑥)) = (abs‘((𝑅𝑢) / 𝑢)))
367366breq1d 5158 . . . . . . . . . . . . . 14 (𝑥 = 𝑢 → ((abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴 ↔ (abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐴))
36874adantr 482 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)
369367, 368, 80rspcdva 3614 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐴)
37086, 362, 105, 369leadd1dd 11825 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅𝑢) / 𝑢)) + 3) ≤ (𝐴 + 3))
371103, 200jca 513 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) ∈ ℝ ∧ 0 ≤ ((𝑢𝑁) / 𝑁)))
372 3rp 12977 . . . . . . . . . . . . . . 15 3 ∈ ℝ+
373 rpaddcl 12993 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ+ ∧ 3 ∈ ℝ+) → (𝐴 + 3) ∈ ℝ+)
374361, 372, 373sylancl 587 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐴 + 3) ∈ ℝ+)
375374rprege0d 13020 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐴 + 3) ∈ ℝ ∧ 0 ≤ (𝐴 + 3)))
376 lemul12b 12068 . . . . . . . . . . . . 13 ((((((𝑢𝑁) / 𝑁) ∈ ℝ ∧ 0 ≤ ((𝑢𝑁) / 𝑁)) ∧ (𝐿 · 𝐸) ∈ ℝ) ∧ (((abs‘((𝑅𝑢) / 𝑢)) + 3) ∈ ℝ ∧ ((𝐴 + 3) ∈ ℝ ∧ 0 ≤ (𝐴 + 3)))) → ((((𝑢𝑁) / 𝑁) ≤ (𝐿 · 𝐸) ∧ ((abs‘((𝑅𝑢) / 𝑢)) + 3) ≤ (𝐴 + 3)) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) ≤ ((𝐿 · 𝐸) · (𝐴 + 3))))
377371, 353, 106, 375, 376syl22anc 838 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) ≤ (𝐿 · 𝐸) ∧ ((abs‘((𝑅𝑢) / 𝑢)) + 3) ≤ (𝐴 + 3)) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) ≤ ((𝐿 · 𝐸) · (𝐴 + 3))))
378360, 370, 377mp2and 698 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) ≤ ((𝐿 · 𝐸) · (𝐴 + 3)))
37935adantr 482 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐸 ∈ ℝ+)
380112, 113mp1i 13 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 4 ∈ ℝ+)
381379, 380rpdivcld 13030 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 4) ∈ ℝ+)
382381rpcnd 13015 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 4) ∈ ℂ)
383374rpcnd 13015 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐴 + 3) ∈ ℂ)
384374rpne0d 13018 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐴 + 3) ≠ 0)
385382, 383, 384divcan1d 11988 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝐸 / 4) / (𝐴 + 3)) · (𝐴 + 3)) = (𝐸 / 4))
38614recnd 11239 . . . . . . . . . . . . . . . . 17 (𝜑𝐸 ∈ ℂ)
387386adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐸 ∈ ℂ)
388380rpcnd 13015 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 4 ∈ ℂ)
389380rpne0d 13018 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 4 ≠ 0)
390387, 388, 389divrec2d 11991 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 4) = ((1 / 4) · 𝐸))
391390oveq1d 7421 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 4) / (𝐴 + 3)) = (((1 / 4) · 𝐸) / (𝐴 + 3)))
392 4cn 12294 . . . . . . . . . . . . . . . . . 18 4 ∈ ℂ
393 4ne0 12317 . . . . . . . . . . . . . . . . . 18 4 ≠ 0
394392, 393reccli 11941 . . . . . . . . . . . . . . . . 17 (1 / 4) ∈ ℂ
395394a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 / 4) ∈ ℂ)
396395, 387, 383, 384div23d 12024 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((1 / 4) · 𝐸) / (𝐴 + 3)) = (((1 / 4) / (𝐴 + 3)) · 𝐸))
39710oveq1i 7416 . . . . . . . . . . . . . . 15 (𝐿 · 𝐸) = (((1 / 4) / (𝐴 + 3)) · 𝐸)
398396, 397eqtr4di 2791 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((1 / 4) · 𝐸) / (𝐴 + 3)) = (𝐿 · 𝐸))
399391, 398eqtr2d 2774 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐿 · 𝐸) = ((𝐸 / 4) / (𝐴 + 3)))
400399oveq1d 7421 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐿 · 𝐸) · (𝐴 + 3)) = (((𝐸 / 4) / (𝐴 + 3)) · (𝐴 + 3)))
401 2ne0 12313 . . . . . . . . . . . . . . 15 2 ≠ 0
402401a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 2 ≠ 0)
403387, 314, 314, 402, 402divdiv1d 12018 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) / 2) = (𝐸 / (2 · 2)))
404 2t2e4 12373 . . . . . . . . . . . . . 14 (2 · 2) = 4
405404oveq2i 7417 . . . . . . . . . . . . 13 (𝐸 / (2 · 2)) = (𝐸 / 4)
406403, 405eqtrdi 2789 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) / 2) = (𝐸 / 4))
407385, 400, 4063eqtr4d 2783 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐿 · 𝐸) · (𝐴 + 3)) = ((𝐸 / 2) / 2))
408378, 407breqtrd 5174 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) ≤ ((𝐸 / 2) / 2))
409117adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (𝐸 / 4)) ∈ ℝ)
410137rpred 13013 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (log‘𝑁) ∈ ℝ)
41178reeflogd 26124 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(log‘𝑁)) = 𝑁)
412135, 411breqtrrd 5176 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(𝑇 / (𝐸 / 4))) < (exp‘(log‘𝑁)))
413 eflt 16057 . . . . . . . . . . . . . . 15 (((𝑇 / (𝐸 / 4)) ∈ ℝ ∧ (log‘𝑁) ∈ ℝ) → ((𝑇 / (𝐸 / 4)) < (log‘𝑁) ↔ (exp‘(𝑇 / (𝐸 / 4))) < (exp‘(log‘𝑁))))
414409, 410, 413syl2anc 585 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑇 / (𝐸 / 4)) < (log‘𝑁) ↔ (exp‘(𝑇 / (𝐸 / 4))) < (exp‘(log‘𝑁))))
415412, 414mpbird 257 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (𝐸 / 4)) < (log‘𝑁))
416409, 410, 415ltled 11359 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (𝐸 / 4)) ≤ (log‘𝑁))
417110, 381, 137, 416lediv23d 13081 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ≤ (𝐸 / 4))
418417, 406breqtrrd 5176 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ≤ ((𝐸 / 2) / 2))
419107, 138, 349, 349, 408, 418le2addd 11830 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))) ≤ (((𝐸 / 2) / 2) + ((𝐸 / 2) / 2)))
420100recnd 11239 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 2) ∈ ℂ)
4214202halvesd 12455 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝐸 / 2) / 2) + ((𝐸 / 2) / 2)) = (𝐸 / 2))
422419, 421breqtrd 5174 . . . . . . . 8 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢𝑁) / 𝑁) · ((abs‘((𝑅𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))) ≤ (𝐸 / 2))
42393, 139, 100, 348, 422letrd 11368 . . . . . . 7 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) ≤ (𝐸 / 2))
4243simprd 497 . . . . . . . 8 (𝜑 → (abs‘((𝑅𝑁) / 𝑁)) ≤ (𝐸 / 2))
425424adantr 482 . . . . . . 7 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑁) / 𝑁)) ≤ (𝐸 / 2))
42693, 94, 100, 100, 423, 425le2addd 11830 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) + (abs‘((𝑅𝑁) / 𝑁))) ≤ ((𝐸 / 2) + (𝐸 / 2)))
4273872halvesd 12455 . . . . . 6 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸)
428426, 427breqtrd 5174 . . . . 5 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘(((𝑅𝑢) / 𝑢) − ((𝑅𝑁) / 𝑁))) + (abs‘((𝑅𝑁) / 𝑁))) ≤ 𝐸)
42986, 95, 96, 99, 428letrd 11368 . . . 4 ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)
430429ralrimiva 3147 . . 3 (𝜑 → ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)
4315, 73, 430jca31 516 . 2 (𝜑 → ((𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
432 breq2 5152 . . . . 5 (𝑧 = 𝑁 → (𝑌 < 𝑧𝑌 < 𝑁))
433 oveq2 7414 . . . . . 6 (𝑧 = 𝑁 → ((1 + (𝐿 · 𝐸)) · 𝑧) = ((1 + (𝐿 · 𝐸)) · 𝑁))
434433breq1d 5158 . . . . 5 (𝑧 = 𝑁 → (((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌) ↔ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)))
435432, 434anbi12d 632 . . . 4 (𝑧 = 𝑁 → ((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ↔ (𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌))))
436 id 22 . . . . . 6 (𝑧 = 𝑁𝑧 = 𝑁)
437436, 433oveq12d 7424 . . . . 5 (𝑧 = 𝑁 → (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧)) = (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁)))
438437raleqdv 3326 . . . 4 (𝑧 = 𝑁 → (∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸 ↔ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
439435, 438anbi12d 632 . . 3 (𝑧 = 𝑁 → (((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸) ↔ ((𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)))
440439rspcev 3613 . 2 ((𝑁 ∈ ℝ+ ∧ ((𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)) → ∃𝑧 ∈ ℝ+ ((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
4412, 431, 440syl2anc 585 1 (𝜑 → ∃𝑧 ∈ ℝ+ ((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wcel 2107  wne 2941  wral 3062  wrex 3071  wss 3948   class class class wbr 5148  cmpt 5231  cfv 6541  (class class class)co 7406  cc 11105  cr 11106  0cc0 11107  1c1 11108   + caddc 11110   · cmul 11112  +∞cpnf 11242  *cxr 11244   < clt 11245  cle 11246  cmin 11441  -cneg 11442   / cdiv 11868  cn 12209  2c2 12264  3c3 12265  4c4 12266  +crp 12971  (,)cioo 13321  [,)cico 13323  [,]cicc 13324  abscabs 15178  expce 16002  logclog 26055  ψcchp 26587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-inf2 9633  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185  ax-addf 11186  ax-mulf 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-of 7667  df-om 7853  df-1st 7972  df-2nd 7973  df-supp 8144  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-2o 8464  df-oadd 8467  df-er 8700  df-map 8819  df-pm 8820  df-ixp 8889  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fsupp 9359  df-fi 9403  df-sup 9434  df-inf 9435  df-oi 9502  df-dju 9893  df-card 9931  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ioc 13326  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-mod 13832  df-seq 13964  df-exp 14025  df-fac 14231  df-bc 14260  df-hash 14288  df-shft 15011  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-limsup 15412  df-clim 15429  df-rlim 15430  df-sum 15630  df-ef 16008  df-sin 16010  df-cos 16011  df-pi 16013  df-dvds 16195  df-gcd 16433  df-prm 16606  df-pc 16767  df-struct 17077  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17142  df-ress 17171  df-plusg 17207  df-mulr 17208  df-starv 17209  df-sca 17210  df-vsca 17211  df-ip 17212  df-tset 17213  df-ple 17214  df-ds 17216  df-unif 17217  df-hom 17218  df-cco 17219  df-rest 17365  df-topn 17366  df-0g 17384  df-gsum 17385  df-topgen 17386  df-pt 17387  df-prds 17390  df-xrs 17445  df-qtop 17450  df-imas 17451  df-xps 17453  df-mre 17527  df-mrc 17528  df-acs 17530  df-mgm 18558  df-sgrp 18607  df-mnd 18623  df-submnd 18669  df-mulg 18946  df-cntz 19176  df-cmn 19645  df-psmet 20929  df-xmet 20930  df-met 20931  df-bl 20932  df-mopn 20933  df-fbas 20934  df-fg 20935  df-cnfld 20938  df-top 22388  df-topon 22405  df-topsp 22427  df-bases 22441  df-cld 22515  df-ntr 22516  df-cls 22517  df-nei 22594  df-lp 22632  df-perf 22633  df-cn 22723  df-cnp 22724  df-haus 22811  df-tx 23058  df-hmeo 23251  df-fil 23342  df-fm 23434  df-flim 23435  df-flf 23436  df-xms 23818  df-ms 23819  df-tms 23820  df-cncf 24386  df-limc 25375  df-dv 25376  df-log 26057  df-vma 26592  df-chp 26593
This theorem is referenced by:  pntibndlem3  27085
  Copyright terms: Public domain W3C validator