Proof of Theorem pntibndlem2
| Step | Hyp | Ref
| Expression |
| 1 | | pntibndlem2.10 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 2 | 1 | nnrpd 13075 |
. 2
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
| 3 | | pntibndlem2.11 |
. . . . 5
⊢ (𝜑 → ((𝑌 < 𝑁 ∧ 𝑁 ≤ ((𝑀 / 2) · 𝑌)) ∧ (abs‘((𝑅‘𝑁) / 𝑁)) ≤ (𝐸 / 2))) |
| 4 | 3 | simpld 494 |
. . . 4
⊢ (𝜑 → (𝑌 < 𝑁 ∧ 𝑁 ≤ ((𝑀 / 2) · 𝑌))) |
| 5 | 4 | simpld 494 |
. . 3
⊢ (𝜑 → 𝑌 < 𝑁) |
| 6 | | 1red 11262 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
| 7 | | ioossre 13448 |
. . . . . . . 8
⊢ (0(,)1)
⊆ ℝ |
| 8 | | pntibnd.r |
. . . . . . . . 9
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
| 9 | | pntibndlem1.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
| 10 | | pntibndlem1.l |
. . . . . . . . 9
⊢ 𝐿 = ((1 / 4) / (𝐴 + 3)) |
| 11 | 8, 9, 10 | pntibndlem1 27633 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ (0(,)1)) |
| 12 | 7, 11 | sselid 3981 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ ℝ) |
| 13 | | pntibndlem3.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ (0(,)1)) |
| 14 | 7, 13 | sselid 3981 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℝ) |
| 15 | 12, 14 | remulcld 11291 |
. . . . . 6
⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℝ) |
| 16 | 6, 15 | readdcld 11290 |
. . . . 5
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ) |
| 17 | 1 | nnred 12281 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 18 | 16, 17 | remulcld 11291 |
. . . 4
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑁) ∈ ℝ) |
| 19 | | 2re 12340 |
. . . . 5
⊢ 2 ∈
ℝ |
| 20 | | remulcl 11240 |
. . . . 5
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ) → (2 · 𝑁) ∈ ℝ) |
| 21 | 19, 17, 20 | sylancr 587 |
. . . 4
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) |
| 22 | | pntibndlem3.c |
. . . . . . . . . 10
⊢ 𝐶 = ((2 · 𝐵) +
(log‘2)) |
| 23 | | pntibndlem3.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
| 24 | 23 | rpred 13077 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 25 | | remulcl 11240 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ 𝐵
∈ ℝ) → (2 · 𝐵) ∈ ℝ) |
| 26 | 19, 24, 25 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · 𝐵) ∈
ℝ) |
| 27 | | 2rp 13039 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ+ |
| 28 | 27 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℝ+) |
| 29 | 28 | relogcld 26665 |
. . . . . . . . . . 11
⊢ (𝜑 → (log‘2) ∈
ℝ) |
| 30 | 26, 29 | readdcld 11290 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 · 𝐵) + (log‘2)) ∈
ℝ) |
| 31 | 22, 30 | eqeltrid 2845 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℝ) |
| 32 | | eliooord 13446 |
. . . . . . . . . . . 12
⊢ (𝐸 ∈ (0(,)1) → (0 <
𝐸 ∧ 𝐸 < 1)) |
| 33 | 13, 32 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1)) |
| 34 | 33 | simpld 494 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < 𝐸) |
| 35 | 14, 34 | elrpd 13074 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
| 36 | 31, 35 | rerpdivcld 13108 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 / 𝐸) ∈ ℝ) |
| 37 | 36 | reefcld 16124 |
. . . . . . 7
⊢ (𝜑 → (exp‘(𝐶 / 𝐸)) ∈ ℝ) |
| 38 | | pnfxr 11315 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
| 39 | | icossre 13468 |
. . . . . . 7
⊢
(((exp‘(𝐶 /
𝐸)) ∈ ℝ ∧
+∞ ∈ ℝ*) → ((exp‘(𝐶 / 𝐸))[,)+∞) ⊆
ℝ) |
| 40 | 37, 38, 39 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → ((exp‘(𝐶 / 𝐸))[,)+∞) ⊆
ℝ) |
| 41 | | pntibndlem2.8 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) |
| 42 | 40, 41 | sseldd 3984 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 43 | | ioossre 13448 |
. . . . . 6
⊢ (𝑋(,)+∞) ⊆
ℝ |
| 44 | | pntibndlem2.9 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ (𝑋(,)+∞)) |
| 45 | 43, 44 | sselid 3981 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ ℝ) |
| 46 | 42, 45 | remulcld 11291 |
. . . 4
⊢ (𝜑 → (𝑀 · 𝑌) ∈ ℝ) |
| 47 | 19 | a1i 11 |
. . . . 5
⊢ (𝜑 → 2 ∈
ℝ) |
| 48 | | eliooord 13446 |
. . . . . . . . . . . . 13
⊢ (𝐿 ∈ (0(,)1) → (0 <
𝐿 ∧ 𝐿 < 1)) |
| 49 | 11, 48 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 < 𝐿 ∧ 𝐿 < 1)) |
| 50 | 49 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 𝐿) |
| 51 | 12, 50 | elrpd 13074 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈
ℝ+) |
| 52 | 51 | rpge0d 13081 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝐿) |
| 53 | 49 | simprd 495 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 < 1) |
| 54 | 35 | rpge0d 13081 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝐸) |
| 55 | 33 | simprd 495 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 < 1) |
| 56 | 12, 6, 14, 6, 52, 53, 54, 55 | ltmul12ad 12209 |
. . . . . . . 8
⊢ (𝜑 → (𝐿 · 𝐸) < (1 · 1)) |
| 57 | | 1t1e1 12428 |
. . . . . . . 8
⊢ (1
· 1) = 1 |
| 58 | 56, 57 | breqtrdi 5184 |
. . . . . . 7
⊢ (𝜑 → (𝐿 · 𝐸) < 1) |
| 59 | 15, 6, 6, 58 | ltadd2dd 11420 |
. . . . . 6
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < (1 + 1)) |
| 60 | | df-2 12329 |
. . . . . 6
⊢ 2 = (1 +
1) |
| 61 | 59, 60 | breqtrrdi 5185 |
. . . . 5
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < 2) |
| 62 | 16, 47, 2, 61 | ltmul1dd 13132 |
. . . 4
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑁) < (2 · 𝑁)) |
| 63 | 4 | simprd 495 |
. . . . . 6
⊢ (𝜑 → 𝑁 ≤ ((𝑀 / 2) · 𝑌)) |
| 64 | 42 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℂ) |
| 65 | 45 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ ℂ) |
| 66 | | rpcnne0 13053 |
. . . . . . . 8
⊢ (2 ∈
ℝ+ → (2 ∈ ℂ ∧ 2 ≠ 0)) |
| 67 | 27, 66 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → (2 ∈ ℂ ∧ 2
≠ 0)) |
| 68 | | div23 11941 |
. . . . . . 7
⊢ ((𝑀 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((𝑀 · 𝑌) / 2) = ((𝑀 / 2) · 𝑌)) |
| 69 | 64, 65, 67, 68 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → ((𝑀 · 𝑌) / 2) = ((𝑀 / 2) · 𝑌)) |
| 70 | 63, 69 | breqtrrd 5171 |
. . . . 5
⊢ (𝜑 → 𝑁 ≤ ((𝑀 · 𝑌) / 2)) |
| 71 | 17, 46, 28 | lemuldiv2d 13127 |
. . . . 5
⊢ (𝜑 → ((2 · 𝑁) ≤ (𝑀 · 𝑌) ↔ 𝑁 ≤ ((𝑀 · 𝑌) / 2))) |
| 72 | 70, 71 | mpbird 257 |
. . . 4
⊢ (𝜑 → (2 · 𝑁) ≤ (𝑀 · 𝑌)) |
| 73 | 18, 21, 46, 62, 72 | ltletrd 11421 |
. . 3
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)) |
| 74 | | pntibndlem3.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴) |
| 75 | | pntibndlem3.k |
. . . . . . . . . . . 12
⊢ 𝐾 = (exp‘(𝐵 / (𝐸 / 2))) |
| 76 | 8, 9, 10, 74, 23, 75, 22, 13, 9, 1 | pntibndlem2a 27634 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁))) |
| 77 | 76 | simp1d 1143 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ ℝ) |
| 78 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈
ℝ+) |
| 79 | 76 | simp2d 1144 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ≤ 𝑢) |
| 80 | 77, 78, 79 | rpgecld 13116 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ ℝ+) |
| 81 | 8 | pntrf 27607 |
. . . . . . . . . 10
⊢ 𝑅:ℝ+⟶ℝ |
| 82 | 81 | ffvelcdmi 7103 |
. . . . . . . . 9
⊢ (𝑢 ∈ ℝ+
→ (𝑅‘𝑢) ∈
ℝ) |
| 83 | 80, 82 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅‘𝑢) ∈ ℝ) |
| 84 | 83, 80 | rerpdivcld 13108 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑢) / 𝑢) ∈ ℝ) |
| 85 | 84 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑢) / 𝑢) ∈ ℂ) |
| 86 | 85 | abscld 15475 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑢) / 𝑢)) ∈ ℝ) |
| 87 | 81 | ffvelcdmi 7103 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℝ+
→ (𝑅‘𝑁) ∈
ℝ) |
| 88 | 2, 87 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑅‘𝑁) ∈ ℝ) |
| 89 | 88, 1 | nndivred 12320 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑅‘𝑁) / 𝑁) ∈ ℝ) |
| 90 | 89 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑁) / 𝑁) ∈ ℝ) |
| 91 | 90 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑁) / 𝑁) ∈ ℂ) |
| 92 | 85, 91 | subcld 11620 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁)) ∈ ℂ) |
| 93 | 92 | abscld 15475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) ∈ ℝ) |
| 94 | 91 | abscld 15475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑁) / 𝑁)) ∈ ℝ) |
| 95 | 93, 94 | readdcld 11290 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) + (abs‘((𝑅‘𝑁) / 𝑁))) ∈ ℝ) |
| 96 | 14 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐸 ∈ ℝ) |
| 97 | 85, 91 | abs2difd 15496 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅‘𝑢) / 𝑢)) − (abs‘((𝑅‘𝑁) / 𝑁))) ≤ (abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁)))) |
| 98 | 86, 94, 93 | lesubaddd 11860 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((abs‘((𝑅‘𝑢) / 𝑢)) − (abs‘((𝑅‘𝑁) / 𝑁))) ≤ (abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) ↔ (abs‘((𝑅‘𝑢) / 𝑢)) ≤ ((abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) + (abs‘((𝑅‘𝑁) / 𝑁))))) |
| 99 | 97, 98 | mpbid 232 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑢) / 𝑢)) ≤ ((abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) + (abs‘((𝑅‘𝑁) / 𝑁)))) |
| 100 | 96 | rehalfcld 12513 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 2) ∈ ℝ) |
| 101 | 17 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ ℝ) |
| 102 | 77, 101 | resubcld 11691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 − 𝑁) ∈ ℝ) |
| 103 | 102, 78 | rerpdivcld 13108 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 − 𝑁) / 𝑁) ∈ ℝ) |
| 104 | | 3re 12346 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℝ |
| 105 | 104 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 3 ∈
ℝ) |
| 106 | 86, 105 | readdcld 11290 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅‘𝑢) / 𝑢)) + 3) ∈ ℝ) |
| 107 | 103, 106 | remulcld 11291 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) ∈ ℝ) |
| 108 | | pntibndlem2.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
| 109 | 108 | rpred 13077 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ ℝ) |
| 110 | 109 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℝ) |
| 111 | | 1red 11262 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 ∈
ℝ) |
| 112 | | 4nn 12349 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℕ |
| 113 | | nnrp 13046 |
. . . . . . . . . . . . . . . . . 18
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) |
| 114 | 112, 113 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 4 ∈
ℝ+) |
| 115 | 35, 114 | rpdivcld 13094 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐸 / 4) ∈
ℝ+) |
| 116 | 108, 115 | rpdivcld 13094 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑇 / (𝐸 / 4)) ∈
ℝ+) |
| 117 | 116 | rpred 13077 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑇 / (𝐸 / 4)) ∈ ℝ) |
| 118 | 117 | reefcld 16124 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) ∈ ℝ) |
| 119 | 118 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(𝑇 / (𝐸 / 4))) ∈ ℝ) |
| 120 | | efgt1 16152 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 / (𝐸 / 4)) ∈ ℝ+ → 1
< (exp‘(𝑇 / (𝐸 / 4)))) |
| 121 | 116, 120 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 < (exp‘(𝑇 / (𝐸 / 4)))) |
| 122 | 121 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 < (exp‘(𝑇 / (𝐸 / 4)))) |
| 123 | | pntibndlem2.7 |
. . . . . . . . . . . . . . . 16
⊢ 𝑋 = ((exp‘(𝑇 / (𝐸 / 4))) + 𝑍) |
| 124 | | pntibndlem3.6 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑍 ∈
ℝ+) |
| 125 | 124 | rpred 13077 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑍 ∈ ℝ) |
| 126 | 118, 125 | readdcld 11290 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((exp‘(𝑇 / (𝐸 / 4))) + 𝑍) ∈ ℝ) |
| 127 | 123, 126 | eqeltrid 2845 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 128 | 118, 124 | ltaddrpd 13110 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < ((exp‘(𝑇 / (𝐸 / 4))) + 𝑍)) |
| 129 | 128, 123 | breqtrrdi 5185 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < 𝑋) |
| 130 | | eliooord 13446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑌 ∈ (𝑋(,)+∞) → (𝑋 < 𝑌 ∧ 𝑌 < +∞)) |
| 131 | 44, 130 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑋 < 𝑌 ∧ 𝑌 < +∞)) |
| 132 | 131 | simpld 494 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 < 𝑌) |
| 133 | 118, 127,
45, 129, 132 | lttrd 11422 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < 𝑌) |
| 134 | 118, 45, 17, 133, 5 | lttrd 11422 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < 𝑁) |
| 135 | 134 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(𝑇 / (𝐸 / 4))) < 𝑁) |
| 136 | 111, 119,
101, 122, 135 | lttrd 11422 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 < 𝑁) |
| 137 | 101, 136 | rplogcld 26671 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (log‘𝑁) ∈
ℝ+) |
| 138 | 110, 137 | rerpdivcld 13108 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℝ) |
| 139 | 107, 138 | readdcld 11290 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))) ∈ ℝ) |
| 140 | | peano2re 11434 |
. . . . . . . . . . . 12
⊢
((abs‘((𝑅‘𝑢) / 𝑢)) ∈ ℝ → ((abs‘((𝑅‘𝑢) / 𝑢)) + 1) ∈ ℝ) |
| 141 | 86, 140 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅‘𝑢) / 𝑢)) + 1) ∈ ℝ) |
| 142 | 103, 141 | remulcld 11291 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) ∈ ℝ) |
| 143 | | chpcl 27167 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ℝ →
(ψ‘𝑢) ∈
ℝ) |
| 144 | 77, 143 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑢) ∈ ℝ) |
| 145 | | chpcl 27167 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℝ →
(ψ‘𝑁) ∈
ℝ) |
| 146 | 101, 145 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑁) ∈ ℝ) |
| 147 | 144, 146 | resubcld 11691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((ψ‘𝑢) − (ψ‘𝑁)) ∈ ℝ) |
| 148 | 147, 78 | rerpdivcld 13108 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ∈ ℝ) |
| 149 | 142, 148 | readdcld 11290 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) ∈ ℝ) |
| 150 | 103, 86 | remulcld 11291 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) ∈ ℝ) |
| 151 | 88 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅‘𝑁) ∈ ℝ) |
| 152 | 83, 151 | resubcld 11691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑢) − (𝑅‘𝑁)) ∈ ℝ) |
| 153 | 152 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑢) − (𝑅‘𝑁)) ∈ ℂ) |
| 154 | 153 | abscld 15475 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) ∈ ℝ) |
| 155 | 154, 78 | rerpdivcld 13108 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁) ∈ ℝ) |
| 156 | 150, 155 | readdcld 11290 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁)) ∈ ℝ) |
| 157 | 103, 84 | remulcld 11291 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) ∈ ℝ) |
| 158 | 157 | renegcld 11690 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) ∈ ℝ) |
| 159 | 158 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) ∈ ℂ) |
| 160 | 152, 78 | rerpdivcld 13108 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁) ∈ ℝ) |
| 161 | 160 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁) ∈ ℂ) |
| 162 | 159, 161 | abstrid 15495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(-(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) + (((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁))) ≤ ((abs‘-(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢))) + (abs‘(((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁)))) |
| 163 | 77 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ ℂ) |
| 164 | 101 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ ℂ) |
| 165 | 78 | rpne0d 13082 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ≠ 0) |
| 166 | 163, 164,
164, 165 | divsubdird 12082 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 − 𝑁) / 𝑁) = ((𝑢 / 𝑁) − (𝑁 / 𝑁))) |
| 167 | 164, 165 | dividd 12041 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 / 𝑁) = 1) |
| 168 | 167 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) − (𝑁 / 𝑁)) = ((𝑢 / 𝑁) − 1)) |
| 169 | 166, 168 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 − 𝑁) / 𝑁) = ((𝑢 / 𝑁) − 1)) |
| 170 | 169 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) = (((𝑢 / 𝑁) − 1) · ((𝑅‘𝑢) / 𝑢))) |
| 171 | 77, 78 | rerpdivcld 13108 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ∈ ℝ) |
| 172 | 171 | recnd 11289 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ∈ ℂ) |
| 173 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 ∈
ℂ) |
| 174 | 172, 173,
85 | subdird 11720 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 / 𝑁) − 1) · ((𝑅‘𝑢) / 𝑢)) = (((𝑢 / 𝑁) · ((𝑅‘𝑢) / 𝑢)) − (1 · ((𝑅‘𝑢) / 𝑢)))) |
| 175 | 80 | rpcnne0d 13086 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ ℂ ∧ 𝑢 ≠ 0)) |
| 176 | 78 | rpcnne0d 13086 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
| 177 | 83 | recnd 11289 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅‘𝑢) ∈ ℂ) |
| 178 | | dmdcan 11977 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑢 ∈ ℂ ∧ 𝑢 ≠ 0) ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ (𝑅‘𝑢) ∈ ℂ) → ((𝑢 / 𝑁) · ((𝑅‘𝑢) / 𝑢)) = ((𝑅‘𝑢) / 𝑁)) |
| 179 | 175, 176,
177, 178 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) · ((𝑅‘𝑢) / 𝑢)) = ((𝑅‘𝑢) / 𝑁)) |
| 180 | 85 | mullidd 11279 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 · ((𝑅‘𝑢) / 𝑢)) = ((𝑅‘𝑢) / 𝑢)) |
| 181 | 179, 180 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 / 𝑁) · ((𝑅‘𝑢) / 𝑢)) − (1 · ((𝑅‘𝑢) / 𝑢))) = (((𝑅‘𝑢) / 𝑁) − ((𝑅‘𝑢) / 𝑢))) |
| 182 | 170, 174,
181 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) = (((𝑅‘𝑢) / 𝑁) − ((𝑅‘𝑢) / 𝑢))) |
| 183 | 182 | negeqd 11502 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) = -(((𝑅‘𝑢) / 𝑁) − ((𝑅‘𝑢) / 𝑢))) |
| 184 | 83, 78 | rerpdivcld 13108 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑢) / 𝑁) ∈ ℝ) |
| 185 | 184 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑢) / 𝑁) ∈ ℂ) |
| 186 | 185, 85 | negsubdi2d 11636 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑅‘𝑢) / 𝑁) − ((𝑅‘𝑢) / 𝑢)) = (((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑢) / 𝑁))) |
| 187 | 183, 186 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) = (((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑢) / 𝑁))) |
| 188 | 151 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅‘𝑁) ∈ ℂ) |
| 189 | 177, 188,
164, 165 | divsubdird 12082 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁) = (((𝑅‘𝑢) / 𝑁) − ((𝑅‘𝑁) / 𝑁))) |
| 190 | 187, 189 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (-(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) + (((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁)) = ((((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑢) / 𝑁)) + (((𝑅‘𝑢) / 𝑁) − ((𝑅‘𝑁) / 𝑁)))) |
| 191 | 85, 185, 91 | npncand 11644 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑢) / 𝑁)) + (((𝑅‘𝑢) / 𝑁) − ((𝑅‘𝑁) / 𝑁))) = (((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) |
| 192 | 190, 191 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (-(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) + (((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁)) = (((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) |
| 193 | 192 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(-(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) + (((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁))) = (abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁)))) |
| 194 | 157 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) ∈ ℂ) |
| 195 | 194 | absnegd 15488 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘-(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢))) = (abs‘(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)))) |
| 196 | 103 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 − 𝑁) / 𝑁) ∈ ℂ) |
| 197 | 196, 85 | absmuld 15493 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢))) = ((abs‘((𝑢 − 𝑁) / 𝑁)) · (abs‘((𝑅‘𝑢) / 𝑢)))) |
| 198 | 77, 101 | subge0d 11853 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (0 ≤ (𝑢 − 𝑁) ↔ 𝑁 ≤ 𝑢)) |
| 199 | 79, 198 | mpbird 257 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 0 ≤ (𝑢 − 𝑁)) |
| 200 | 102, 78, 199 | divge0d 13117 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 0 ≤ ((𝑢 − 𝑁) / 𝑁)) |
| 201 | 103, 200 | absidd 15461 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑢 − 𝑁) / 𝑁)) = ((𝑢 − 𝑁) / 𝑁)) |
| 202 | 201 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑢 − 𝑁) / 𝑁)) · (abs‘((𝑅‘𝑢) / 𝑢))) = (((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢)))) |
| 203 | 195, 197,
202 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘-(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢))) = (((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢)))) |
| 204 | 153, 164,
165 | absdivd 15494 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁)) = ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / (abs‘𝑁))) |
| 205 | 78 | rprege0d 13084 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁)) |
| 206 | | absid 15335 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) → (abs‘𝑁) = 𝑁) |
| 207 | 205, 206 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘𝑁) = 𝑁) |
| 208 | 207 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / (abs‘𝑁)) = ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁)) |
| 209 | 204, 208 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁)) = ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁)) |
| 210 | 203, 209 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘-(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢))) + (abs‘(((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁))) = ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁))) |
| 211 | 162, 193,
210 | 3brtr3d 5174 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) ≤ ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁))) |
| 212 | 102, 147 | readdcld 11290 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) ∈ ℝ) |
| 213 | 212, 78 | rerpdivcld 13108 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁) ∈ ℝ) |
| 214 | 147 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((ψ‘𝑢) − (ψ‘𝑁)) ∈ ℂ) |
| 215 | 164, 163 | subcld 11620 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 − 𝑢) ∈ ℂ) |
| 216 | 214, 215 | abstrid 15495 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁 − 𝑢))) ≤ ((abs‘((ψ‘𝑢) − (ψ‘𝑁))) + (abs‘(𝑁 − 𝑢)))) |
| 217 | 8 | pntrval 27606 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ ℝ+
→ (𝑅‘𝑢) = ((ψ‘𝑢) − 𝑢)) |
| 218 | 80, 217 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅‘𝑢) = ((ψ‘𝑢) − 𝑢)) |
| 219 | 8 | pntrval 27606 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℝ+
→ (𝑅‘𝑁) = ((ψ‘𝑁) − 𝑁)) |
| 220 | 78, 219 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅‘𝑁) = ((ψ‘𝑁) − 𝑁)) |
| 221 | 218, 220 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑢) − (𝑅‘𝑁)) = (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁))) |
| 222 | 144 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑢) ∈ ℂ) |
| 223 | 146 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑁) ∈ ℂ) |
| 224 | | subadd4 11553 |
. . . . . . . . . . . . . . . . . 18
⊢
((((ψ‘𝑢)
∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) →
(((ψ‘𝑢) −
(ψ‘𝑁)) −
(𝑢 − 𝑁)) = (((ψ‘𝑢) + 𝑁) − ((ψ‘𝑁) + 𝑢))) |
| 225 | | sub4 11554 |
. . . . . . . . . . . . . . . . . 18
⊢
((((ψ‘𝑢)
∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) →
(((ψ‘𝑢) −
(ψ‘𝑁)) −
(𝑢 − 𝑁)) = (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁))) |
| 226 | | addsub4 11552 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((ψ‘𝑢)
∈ ℂ ∧ 𝑁
∈ ℂ) ∧ ((ψ‘𝑁) ∈ ℂ ∧ 𝑢 ∈ ℂ)) → (((ψ‘𝑢) + 𝑁) − ((ψ‘𝑁) + 𝑢)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁 − 𝑢))) |
| 227 | 226 | an42s 661 |
. . . . . . . . . . . . . . . . . 18
⊢
((((ψ‘𝑢)
∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) →
(((ψ‘𝑢) + 𝑁) − ((ψ‘𝑁) + 𝑢)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁 − 𝑢))) |
| 228 | 224, 225,
227 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . 17
⊢
((((ψ‘𝑢)
∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) →
(((ψ‘𝑢) −
𝑢) −
((ψ‘𝑁) −
𝑁)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁 − 𝑢))) |
| 229 | 222, 223,
163, 164, 228 | syl22anc 839 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁 − 𝑢))) |
| 230 | 221, 229 | eqtr2d 2778 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁 − 𝑢)) = ((𝑅‘𝑢) − (𝑅‘𝑁))) |
| 231 | 230 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁 − 𝑢))) = (abs‘((𝑅‘𝑢) − (𝑅‘𝑁)))) |
| 232 | 102 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 − 𝑁) ∈ ℂ) |
| 233 | | chpwordi 27200 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢) → (ψ‘𝑁) ≤ (ψ‘𝑢)) |
| 234 | 101, 77, 79, 233 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑁) ≤ (ψ‘𝑢)) |
| 235 | 146, 144,
234 | abssubge0d 15470 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((ψ‘𝑢) − (ψ‘𝑁))) = ((ψ‘𝑢) − (ψ‘𝑁))) |
| 236 | 101, 77, 79 | abssuble0d 15471 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(𝑁 − 𝑢)) = (𝑢 − 𝑁)) |
| 237 | 235, 236 | oveq12d 7449 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((ψ‘𝑢) − (ψ‘𝑁))) + (abs‘(𝑁 − 𝑢))) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑢 − 𝑁))) |
| 238 | 214, 232,
237 | comraddd 11475 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((ψ‘𝑢) − (ψ‘𝑁))) + (abs‘(𝑁 − 𝑢))) = ((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁)))) |
| 239 | 216, 231,
238 | 3brtr3d 5174 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) ≤ ((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁)))) |
| 240 | 154, 212,
78, 239 | lediv1dd 13135 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁) ≤ (((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁)) |
| 241 | 155, 213,
150, 240 | leadd2dd 11878 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁)) ≤ ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + (((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁))) |
| 242 | 150 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) ∈ ℂ) |
| 243 | 148 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ∈ ℂ) |
| 244 | 242, 196,
243 | addassd 11283 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((𝑢 − 𝑁) / 𝑁)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) = ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + (((𝑢 − 𝑁) / 𝑁) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)))) |
| 245 | 86 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑢) / 𝑢)) ∈ ℂ) |
| 246 | 196, 245,
173 | adddid 11285 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) = ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + (((𝑢 − 𝑁) / 𝑁) · 1))) |
| 247 | 196 | mulridd 11278 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · 1) = ((𝑢 − 𝑁) / 𝑁)) |
| 248 | 247 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + (((𝑢 − 𝑁) / 𝑁) · 1)) = ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((𝑢 − 𝑁) / 𝑁))) |
| 249 | 246, 248 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) = ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((𝑢 − 𝑁) / 𝑁))) |
| 250 | 249 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) = (((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((𝑢 − 𝑁) / 𝑁)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁))) |
| 251 | 232, 214,
164, 165 | divdird 12081 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁) = (((𝑢 − 𝑁) / 𝑁) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁))) |
| 252 | 251 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + (((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁)) = ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + (((𝑢 − 𝑁) / 𝑁) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)))) |
| 253 | 244, 250,
252 | 3eqtr4d 2787 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) = ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + (((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁))) |
| 254 | 241, 253 | breqtrrd 5171 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁)) ≤ ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁))) |
| 255 | 93, 156, 149, 211, 254 | letrd 11418 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) ≤ ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁))) |
| 256 | | remulcl 11240 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℝ ∧ ((𝑢
− 𝑁) / 𝑁) ∈ ℝ) → (2
· ((𝑢 − 𝑁) / 𝑁)) ∈ ℝ) |
| 257 | 19, 103, 256 | sylancr 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · ((𝑢 − 𝑁) / 𝑁)) ∈ ℝ) |
| 258 | 257, 138 | readdcld 11290 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((2 · ((𝑢 − 𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))) ∈ ℝ) |
| 259 | | remulcl 11240 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℝ ∧ (𝑢
− 𝑁) ∈ ℝ)
→ (2 · (𝑢
− 𝑁)) ∈
ℝ) |
| 260 | 19, 102, 259 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · (𝑢 − 𝑁)) ∈ ℝ) |
| 261 | 101, 137 | rerpdivcld 13108 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 / (log‘𝑁)) ∈ ℝ) |
| 262 | 110, 261 | remulcld 11291 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℝ) |
| 263 | 260, 262 | readdcld 11290 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((2 · (𝑢 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) ∈ ℝ) |
| 264 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑢 → (ψ‘𝑦) = (ψ‘𝑢)) |
| 265 | 264 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑢 → ((ψ‘𝑦) − (ψ‘𝑁)) = ((ψ‘𝑢) − (ψ‘𝑁))) |
| 266 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑢 → (𝑦 − 𝑁) = (𝑢 − 𝑁)) |
| 267 | 266 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑢 → (2 · (𝑦 − 𝑁)) = (2 · (𝑢 − 𝑁))) |
| 268 | 267 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑢 → ((2 · (𝑦 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) = ((2 · (𝑢 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))) |
| 269 | 265, 268 | breq12d 5156 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑢 → (((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) ↔ ((ψ‘𝑢) − (ψ‘𝑁)) ≤ ((2 · (𝑢 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))) |
| 270 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑁 → 𝑥 = 𝑁) |
| 271 | | oveq2 7439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁)) |
| 272 | 270, 271 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑁 → (𝑥[,](2 · 𝑥)) = (𝑁[,](2 · 𝑁))) |
| 273 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑁 → (ψ‘𝑥) = (ψ‘𝑁)) |
| 274 | 273 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑁 → ((ψ‘𝑦) − (ψ‘𝑥)) = ((ψ‘𝑦) − (ψ‘𝑁))) |
| 275 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑁 → (𝑦 − 𝑥) = (𝑦 − 𝑁)) |
| 276 | 275 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑁 → (2 · (𝑦 − 𝑥)) = (2 · (𝑦 − 𝑁))) |
| 277 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑁 → (log‘𝑥) = (log‘𝑁)) |
| 278 | 270, 277 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑁 → (𝑥 / (log‘𝑥)) = (𝑁 / (log‘𝑁))) |
| 279 | 278 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑁 → (𝑇 · (𝑥 / (log‘𝑥))) = (𝑇 · (𝑁 / (log‘𝑁)))) |
| 280 | 276, 279 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑁 → ((2 · (𝑦 − 𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))) = ((2 · (𝑦 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))) |
| 281 | 274, 280 | breq12d 5156 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑁 → (((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦 − 𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))) ↔ ((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))) |
| 282 | 272, 281 | raleqbidv 3346 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑁 → (∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦 − 𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))) ↔ ∀𝑦 ∈ (𝑁[,](2 · 𝑁))((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))) |
| 283 | | pntibndlem2.6 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦 − 𝑥)) + (𝑇 · (𝑥 / (log‘𝑥))))) |
| 284 | 283 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦 − 𝑥)) + (𝑇 · (𝑥 / (log‘𝑥))))) |
| 285 | | 1xr 11320 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ* |
| 286 | | elioopnf 13483 |
. . . . . . . . . . . . . . . . 17
⊢ (1 ∈
ℝ* → (𝑁 ∈ (1(,)+∞) ↔ (𝑁 ∈ ℝ ∧ 1 <
𝑁))) |
| 287 | 285, 286 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ (1(,)+∞) ↔
(𝑁 ∈ ℝ ∧ 1
< 𝑁)) |
| 288 | 101, 136,
287 | sylanbrc 583 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ (1(,)+∞)) |
| 289 | 282, 284,
288 | rspcdva 3623 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ∀𝑦 ∈ (𝑁[,](2 · 𝑁))((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))) |
| 290 | 18 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((1 + (𝐿 · 𝐸)) · 𝑁) ∈ ℝ) |
| 291 | 21 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · 𝑁) ∈ ℝ) |
| 292 | 76 | simp3d 1145 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁)) |
| 293 | | ltle 11349 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((1 +
(𝐿 · 𝐸)) ∈ ℝ ∧ 2 ∈
ℝ) → ((1 + (𝐿
· 𝐸)) < 2 →
(1 + (𝐿 · 𝐸)) ≤ 2)) |
| 294 | 16, 19, 293 | sylancl 586 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) < 2 → (1 + (𝐿 · 𝐸)) ≤ 2)) |
| 295 | 61, 294 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ≤ 2) |
| 296 | 295 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 + (𝐿 · 𝐸)) ≤ 2) |
| 297 | 16 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 + (𝐿 · 𝐸)) ∈ ℝ) |
| 298 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 2 ∈
ℝ) |
| 299 | 297, 298,
78 | lemul1d 13120 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((1 + (𝐿 · 𝐸)) ≤ 2 ↔ ((1 + (𝐿 · 𝐸)) · 𝑁) ≤ (2 · 𝑁))) |
| 300 | 296, 299 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((1 + (𝐿 · 𝐸)) · 𝑁) ≤ (2 · 𝑁)) |
| 301 | 77, 290, 291, 292, 300 | letrd 11418 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ≤ (2 · 𝑁)) |
| 302 | | elicc2 13452 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℝ ∧ (2
· 𝑁) ∈ ℝ)
→ (𝑢 ∈ (𝑁[,](2 · 𝑁)) ↔ (𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ (2 · 𝑁)))) |
| 303 | 101, 291,
302 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ (𝑁[,](2 · 𝑁)) ↔ (𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ (2 · 𝑁)))) |
| 304 | 77, 79, 301, 303 | mpbir3and 1343 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ (𝑁[,](2 · 𝑁))) |
| 305 | 269, 289,
304 | rspcdva 3623 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((ψ‘𝑢) − (ψ‘𝑁)) ≤ ((2 · (𝑢 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))) |
| 306 | 147, 263,
78, 305 | lediv1dd 13135 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ≤ (((2 · (𝑢 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁)) |
| 307 | 260 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · (𝑢 − 𝑁)) ∈ ℂ) |
| 308 | 108 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈
ℝ+) |
| 309 | 308 | rpred 13077 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℝ) |
| 310 | 309, 261 | remulcld 11291 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℝ) |
| 311 | 310 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℂ) |
| 312 | | divdir 11947 |
. . . . . . . . . . . . . 14
⊢ (((2
· (𝑢 − 𝑁)) ∈ ℂ ∧ (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℂ ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) → (((2 · (𝑢 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁) = (((2 · (𝑢 − 𝑁)) / 𝑁) + ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁))) |
| 313 | 307, 311,
176, 312 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((2 · (𝑢 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁) = (((2 · (𝑢 − 𝑁)) / 𝑁) + ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁))) |
| 314 | | 2cnd 12344 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 2 ∈
ℂ) |
| 315 | 314, 232,
164, 165 | divassd 12078 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((2 · (𝑢 − 𝑁)) / 𝑁) = (2 · ((𝑢 − 𝑁) / 𝑁))) |
| 316 | 110 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℂ) |
| 317 | 137 | rpcnne0d 13086 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((log‘𝑁) ∈ ℂ ∧ (log‘𝑁) ≠ 0)) |
| 318 | | div12 11944 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧
((log‘𝑁) ∈
ℂ ∧ (log‘𝑁)
≠ 0)) → (𝑇 ·
(𝑁 / (log‘𝑁))) = (𝑁 · (𝑇 / (log‘𝑁)))) |
| 319 | 316, 164,
317, 318 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) = (𝑁 · (𝑇 / (log‘𝑁)))) |
| 320 | 319 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁) = ((𝑁 · (𝑇 / (log‘𝑁))) / 𝑁)) |
| 321 | 308, 137 | rpdivcld 13094 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈
ℝ+) |
| 322 | 321 | rpcnd 13079 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℂ) |
| 323 | 322, 164,
165 | divcan3d 12048 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑁 · (𝑇 / (log‘𝑁))) / 𝑁) = (𝑇 / (log‘𝑁))) |
| 324 | 320, 323 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁) = (𝑇 / (log‘𝑁))) |
| 325 | 315, 324 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((2 · (𝑢 − 𝑁)) / 𝑁) + ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁)) = ((2 · ((𝑢 − 𝑁) / 𝑁)) + (𝑇 / (log‘𝑁)))) |
| 326 | 313, 325 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((2 · (𝑢 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁) = ((2 · ((𝑢 − 𝑁) / 𝑁)) + (𝑇 / (log‘𝑁)))) |
| 327 | 306, 326 | breqtrd 5169 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ≤ ((2 · ((𝑢 − 𝑁) / 𝑁)) + (𝑇 / (log‘𝑁)))) |
| 328 | 148, 258,
142, 327 | leadd2dd 11878 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) ≤ ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + ((2 · ((𝑢 − 𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))))) |
| 329 | 142 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) ∈ ℂ) |
| 330 | 257 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · ((𝑢 − 𝑁) / 𝑁)) ∈ ℂ) |
| 331 | 138 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℂ) |
| 332 | 329, 330,
331 | addassd 11283 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (2 · ((𝑢 − 𝑁) / 𝑁))) + (𝑇 / (log‘𝑁))) = ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + ((2 · ((𝑢 − 𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))))) |
| 333 | | 2cn 12341 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
| 334 | | mulcom 11241 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ ((𝑢
− 𝑁) / 𝑁) ∈ ℂ) → (2
· ((𝑢 − 𝑁) / 𝑁)) = (((𝑢 − 𝑁) / 𝑁) · 2)) |
| 335 | 333, 196,
334 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · ((𝑢 − 𝑁) / 𝑁)) = (((𝑢 − 𝑁) / 𝑁) · 2)) |
| 336 | 335 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (2 · ((𝑢 − 𝑁) / 𝑁))) = ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((𝑢 − 𝑁) / 𝑁) · 2))) |
| 337 | 141 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅‘𝑢) / 𝑢)) + 1) ∈ ℂ) |
| 338 | 196, 337,
314 | adddid 11285 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · (((abs‘((𝑅‘𝑢) / 𝑢)) + 1) + 2)) = ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((𝑢 − 𝑁) / 𝑁) · 2))) |
| 339 | 245, 173,
314 | addassd 11283 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((abs‘((𝑅‘𝑢) / 𝑢)) + 1) + 2) = ((abs‘((𝑅‘𝑢) / 𝑢)) + (1 + 2))) |
| 340 | | 1p2e3 12409 |
. . . . . . . . . . . . . . . 16
⊢ (1 + 2) =
3 |
| 341 | 340 | oveq2i 7442 |
. . . . . . . . . . . . . . 15
⊢
((abs‘((𝑅‘𝑢) / 𝑢)) + (1 + 2)) = ((abs‘((𝑅‘𝑢) / 𝑢)) + 3) |
| 342 | 339, 341 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((abs‘((𝑅‘𝑢) / 𝑢)) + 1) + 2) = ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) |
| 343 | 342 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · (((abs‘((𝑅‘𝑢) / 𝑢)) + 1) + 2)) = (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3))) |
| 344 | 336, 338,
343 | 3eqtr2d 2783 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (2 · ((𝑢 − 𝑁) / 𝑁))) = (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3))) |
| 345 | 344 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (2 · ((𝑢 − 𝑁) / 𝑁))) + (𝑇 / (log‘𝑁))) = ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁)))) |
| 346 | 332, 345 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + ((2 · ((𝑢 − 𝑁) / 𝑁)) + (𝑇 / (log‘𝑁)))) = ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁)))) |
| 347 | 328, 346 | breqtrd 5169 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) ≤ ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁)))) |
| 348 | 93, 149, 139, 255, 347 | letrd 11418 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) ≤ ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁)))) |
| 349 | 100 | rehalfcld 12513 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) / 2) ∈ ℝ) |
| 350 | 77, 297, 78 | ledivmul2d 13131 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) ≤ (1 + (𝐿 · 𝐸)) ↔ 𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁))) |
| 351 | 292, 350 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ≤ (1 + (𝐿 · 𝐸))) |
| 352 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
| 353 | 15 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐿 · 𝐸) ∈ ℝ) |
| 354 | 353 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐿 · 𝐸) ∈ ℂ) |
| 355 | | addcom 11447 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ (𝐿
· 𝐸) ∈ ℂ)
→ (1 + (𝐿 ·
𝐸)) = ((𝐿 · 𝐸) + 1)) |
| 356 | 352, 354,
355 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 + (𝐿 · 𝐸)) = ((𝐿 · 𝐸) + 1)) |
| 357 | 351, 356 | breqtrd 5169 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ≤ ((𝐿 · 𝐸) + 1)) |
| 358 | 171, 111,
353 | lesubaddd 11860 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 / 𝑁) − 1) ≤ (𝐿 · 𝐸) ↔ (𝑢 / 𝑁) ≤ ((𝐿 · 𝐸) + 1))) |
| 359 | 357, 358 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) − 1) ≤ (𝐿 · 𝐸)) |
| 360 | 169, 359 | eqbrtrd 5165 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 − 𝑁) / 𝑁) ≤ (𝐿 · 𝐸)) |
| 361 | 9 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐴 ∈
ℝ+) |
| 362 | 361 | rpred 13077 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐴 ∈ ℝ) |
| 363 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑢 → (𝑅‘𝑥) = (𝑅‘𝑢)) |
| 364 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑢 → 𝑥 = 𝑢) |
| 365 | 363, 364 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑢 → ((𝑅‘𝑥) / 𝑥) = ((𝑅‘𝑢) / 𝑢)) |
| 366 | 365 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑢 → (abs‘((𝑅‘𝑥) / 𝑥)) = (abs‘((𝑅‘𝑢) / 𝑢))) |
| 367 | 366 | breq1d 5153 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑢 → ((abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴 ↔ (abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐴)) |
| 368 | 74 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴) |
| 369 | 367, 368,
80 | rspcdva 3623 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐴) |
| 370 | 86, 362, 105, 369 | leadd1dd 11877 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅‘𝑢) / 𝑢)) + 3) ≤ (𝐴 + 3)) |
| 371 | 103, 200 | jca 511 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) ∈ ℝ ∧ 0 ≤ ((𝑢 − 𝑁) / 𝑁))) |
| 372 | | 3rp 13040 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℝ+ |
| 373 | | rpaddcl 13057 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ+
∧ 3 ∈ ℝ+) → (𝐴 + 3) ∈
ℝ+) |
| 374 | 361, 372,
373 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐴 + 3) ∈
ℝ+) |
| 375 | 374 | rprege0d 13084 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐴 + 3) ∈ ℝ ∧ 0 ≤ (𝐴 + 3))) |
| 376 | | lemul12b 12124 |
. . . . . . . . . . . . 13
⊢
((((((𝑢 −
𝑁) / 𝑁) ∈ ℝ ∧ 0 ≤ ((𝑢 − 𝑁) / 𝑁)) ∧ (𝐿 · 𝐸) ∈ ℝ) ∧ (((abs‘((𝑅‘𝑢) / 𝑢)) + 3) ∈ ℝ ∧ ((𝐴 + 3) ∈ ℝ ∧ 0
≤ (𝐴 + 3)))) →
((((𝑢 − 𝑁) / 𝑁) ≤ (𝐿 · 𝐸) ∧ ((abs‘((𝑅‘𝑢) / 𝑢)) + 3) ≤ (𝐴 + 3)) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) ≤ ((𝐿 · 𝐸) · (𝐴 + 3)))) |
| 377 | 371, 353,
106, 375, 376 | syl22anc 839 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) ≤ (𝐿 · 𝐸) ∧ ((abs‘((𝑅‘𝑢) / 𝑢)) + 3) ≤ (𝐴 + 3)) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) ≤ ((𝐿 · 𝐸) · (𝐴 + 3)))) |
| 378 | 360, 370,
377 | mp2and 699 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) ≤ ((𝐿 · 𝐸) · (𝐴 + 3))) |
| 379 | 35 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐸 ∈
ℝ+) |
| 380 | 112, 113 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 4 ∈
ℝ+) |
| 381 | 379, 380 | rpdivcld 13094 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 4) ∈
ℝ+) |
| 382 | 381 | rpcnd 13079 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 4) ∈ ℂ) |
| 383 | 374 | rpcnd 13079 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐴 + 3) ∈ ℂ) |
| 384 | 374 | rpne0d 13082 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐴 + 3) ≠ 0) |
| 385 | 382, 383,
384 | divcan1d 12044 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝐸 / 4) / (𝐴 + 3)) · (𝐴 + 3)) = (𝐸 / 4)) |
| 386 | 14 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐸 ∈ ℂ) |
| 387 | 386 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐸 ∈ ℂ) |
| 388 | 380 | rpcnd 13079 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 4 ∈
ℂ) |
| 389 | 380 | rpne0d 13082 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 4 ≠ 0) |
| 390 | 387, 388,
389 | divrec2d 12047 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 4) = ((1 / 4) · 𝐸)) |
| 391 | 390 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 4) / (𝐴 + 3)) = (((1 / 4) · 𝐸) / (𝐴 + 3))) |
| 392 | | 4cn 12351 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℂ |
| 393 | | 4ne0 12374 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ≠
0 |
| 394 | 392, 393 | reccli 11997 |
. . . . . . . . . . . . . . . . 17
⊢ (1 / 4)
∈ ℂ |
| 395 | 394 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 / 4) ∈
ℂ) |
| 396 | 395, 387,
383, 384 | div23d 12080 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((1 / 4) · 𝐸) / (𝐴 + 3)) = (((1 / 4) / (𝐴 + 3)) · 𝐸)) |
| 397 | 10 | oveq1i 7441 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 · 𝐸) = (((1 / 4) / (𝐴 + 3)) · 𝐸) |
| 398 | 396, 397 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((1 / 4) · 𝐸) / (𝐴 + 3)) = (𝐿 · 𝐸)) |
| 399 | 391, 398 | eqtr2d 2778 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐿 · 𝐸) = ((𝐸 / 4) / (𝐴 + 3))) |
| 400 | 399 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐿 · 𝐸) · (𝐴 + 3)) = (((𝐸 / 4) / (𝐴 + 3)) · (𝐴 + 3))) |
| 401 | | 2ne0 12370 |
. . . . . . . . . . . . . . 15
⊢ 2 ≠
0 |
| 402 | 401 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 2 ≠ 0) |
| 403 | 387, 314,
314, 402, 402 | divdiv1d 12074 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) / 2) = (𝐸 / (2 · 2))) |
| 404 | | 2t2e4 12430 |
. . . . . . . . . . . . . 14
⊢ (2
· 2) = 4 |
| 405 | 404 | oveq2i 7442 |
. . . . . . . . . . . . 13
⊢ (𝐸 / (2 · 2)) = (𝐸 / 4) |
| 406 | 403, 405 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) / 2) = (𝐸 / 4)) |
| 407 | 385, 400,
406 | 3eqtr4d 2787 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐿 · 𝐸) · (𝐴 + 3)) = ((𝐸 / 2) / 2)) |
| 408 | 378, 407 | breqtrd 5169 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) ≤ ((𝐸 / 2) / 2)) |
| 409 | 117 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (𝐸 / 4)) ∈ ℝ) |
| 410 | 137 | rpred 13077 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (log‘𝑁) ∈ ℝ) |
| 411 | 78 | reeflogd 26666 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(log‘𝑁)) = 𝑁) |
| 412 | 135, 411 | breqtrrd 5171 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(𝑇 / (𝐸 / 4))) < (exp‘(log‘𝑁))) |
| 413 | | eflt 16153 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 / (𝐸 / 4)) ∈ ℝ ∧ (log‘𝑁) ∈ ℝ) → ((𝑇 / (𝐸 / 4)) < (log‘𝑁) ↔ (exp‘(𝑇 / (𝐸 / 4))) < (exp‘(log‘𝑁)))) |
| 414 | 409, 410,
413 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑇 / (𝐸 / 4)) < (log‘𝑁) ↔ (exp‘(𝑇 / (𝐸 / 4))) < (exp‘(log‘𝑁)))) |
| 415 | 412, 414 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (𝐸 / 4)) < (log‘𝑁)) |
| 416 | 409, 410,
415 | ltled 11409 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (𝐸 / 4)) ≤ (log‘𝑁)) |
| 417 | 110, 381,
137, 416 | lediv23d 13145 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ≤ (𝐸 / 4)) |
| 418 | 417, 406 | breqtrrd 5171 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ≤ ((𝐸 / 2) / 2)) |
| 419 | 107, 138,
349, 349, 408, 418 | le2addd 11882 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))) ≤ (((𝐸 / 2) / 2) + ((𝐸 / 2) / 2))) |
| 420 | 100 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 2) ∈ ℂ) |
| 421 | 420 | 2halvesd 12512 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝐸 / 2) / 2) + ((𝐸 / 2) / 2)) = (𝐸 / 2)) |
| 422 | 419, 421 | breqtrd 5169 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))) ≤ (𝐸 / 2)) |
| 423 | 93, 139, 100, 348, 422 | letrd 11418 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) ≤ (𝐸 / 2)) |
| 424 | 3 | simprd 495 |
. . . . . . . 8
⊢ (𝜑 → (abs‘((𝑅‘𝑁) / 𝑁)) ≤ (𝐸 / 2)) |
| 425 | 424 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑁) / 𝑁)) ≤ (𝐸 / 2)) |
| 426 | 93, 94, 100, 100, 423, 425 | le2addd 11882 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) + (abs‘((𝑅‘𝑁) / 𝑁))) ≤ ((𝐸 / 2) + (𝐸 / 2))) |
| 427 | 387 | 2halvesd 12512 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸) |
| 428 | 426, 427 | breqtrd 5169 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) + (abs‘((𝑅‘𝑁) / 𝑁))) ≤ 𝐸) |
| 429 | 86, 95, 96, 99, 428 | letrd 11418 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) |
| 430 | 429 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) |
| 431 | 5, 73, 430 | jca31 514 |
. 2
⊢ (𝜑 → ((𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
| 432 | | breq2 5147 |
. . . . 5
⊢ (𝑧 = 𝑁 → (𝑌 < 𝑧 ↔ 𝑌 < 𝑁)) |
| 433 | | oveq2 7439 |
. . . . . 6
⊢ (𝑧 = 𝑁 → ((1 + (𝐿 · 𝐸)) · 𝑧) = ((1 + (𝐿 · 𝐸)) · 𝑁)) |
| 434 | 433 | breq1d 5153 |
. . . . 5
⊢ (𝑧 = 𝑁 → (((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌) ↔ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌))) |
| 435 | 432, 434 | anbi12d 632 |
. . . 4
⊢ (𝑧 = 𝑁 → ((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ↔ (𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)))) |
| 436 | | id 22 |
. . . . . 6
⊢ (𝑧 = 𝑁 → 𝑧 = 𝑁) |
| 437 | 436, 433 | oveq12d 7449 |
. . . . 5
⊢ (𝑧 = 𝑁 → (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧)) = (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) |
| 438 | 437 | raleqdv 3326 |
. . . 4
⊢ (𝑧 = 𝑁 → (∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸 ↔ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
| 439 | 435, 438 | anbi12d 632 |
. . 3
⊢ (𝑧 = 𝑁 → (((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ↔ ((𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) |
| 440 | 439 | rspcev 3622 |
. 2
⊢ ((𝑁 ∈ ℝ+
∧ ((𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) → ∃𝑧 ∈ ℝ+ ((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
| 441 | 2, 431, 440 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑧 ∈ ℝ+ ((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |