Proof of Theorem pntibndlem2
Step | Hyp | Ref
| Expression |
1 | | pntibndlem2.10 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | nnrpd 11870 |
. 2
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
3 | | pntibndlem2.11 |
. . . . 5
⊢ (𝜑 → ((𝑌 < 𝑁 ∧ 𝑁 ≤ ((𝑀 / 2) · 𝑌)) ∧ (abs‘((𝑅‘𝑁) / 𝑁)) ≤ (𝐸 / 2))) |
4 | 3 | simpld 475 |
. . . 4
⊢ (𝜑 → (𝑌 < 𝑁 ∧ 𝑁 ≤ ((𝑀 / 2) · 𝑌))) |
5 | 4 | simpld 475 |
. . 3
⊢ (𝜑 → 𝑌 < 𝑁) |
6 | | 1red 10055 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
7 | | ioossre 12235 |
. . . . . . . 8
⊢ (0(,)1)
⊆ ℝ |
8 | | pntibnd.r |
. . . . . . . . 9
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
9 | | pntibndlem1.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
10 | | pntibndlem1.l |
. . . . . . . . 9
⊢ 𝐿 = ((1 / 4) / (𝐴 + 3)) |
11 | 8, 9, 10 | pntibndlem1 25278 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ (0(,)1)) |
12 | 7, 11 | sseldi 3601 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ ℝ) |
13 | | pntibndlem3.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ (0(,)1)) |
14 | 7, 13 | sseldi 3601 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℝ) |
15 | 12, 14 | remulcld 10070 |
. . . . . 6
⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℝ) |
16 | 6, 15 | readdcld 10069 |
. . . . 5
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ) |
17 | 1 | nnred 11035 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℝ) |
18 | 16, 17 | remulcld 10070 |
. . . 4
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑁) ∈ ℝ) |
19 | | 2re 11090 |
. . . . 5
⊢ 2 ∈
ℝ |
20 | | remulcl 10021 |
. . . . 5
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ) → (2 · 𝑁) ∈ ℝ) |
21 | 19, 17, 20 | sylancr 695 |
. . . 4
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) |
22 | | pntibndlem3.c |
. . . . . . . . . 10
⊢ 𝐶 = ((2 · 𝐵) +
(log‘2)) |
23 | | pntibndlem3.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
24 | 23 | rpred 11872 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℝ) |
25 | | remulcl 10021 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ 𝐵
∈ ℝ) → (2 · 𝐵) ∈ ℝ) |
26 | 19, 24, 25 | sylancr 695 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · 𝐵) ∈
ℝ) |
27 | | 2rp 11837 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ+ |
28 | 27 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℝ+) |
29 | 28 | relogcld 24369 |
. . . . . . . . . . 11
⊢ (𝜑 → (log‘2) ∈
ℝ) |
30 | 26, 29 | readdcld 10069 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 · 𝐵) + (log‘2)) ∈
ℝ) |
31 | 22, 30 | syl5eqel 2705 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℝ) |
32 | | eliooord 12233 |
. . . . . . . . . . . 12
⊢ (𝐸 ∈ (0(,)1) → (0 <
𝐸 ∧ 𝐸 < 1)) |
33 | 13, 32 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1)) |
34 | 33 | simpld 475 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < 𝐸) |
35 | 14, 34 | elrpd 11869 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
36 | 31, 35 | rerpdivcld 11903 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 / 𝐸) ∈ ℝ) |
37 | 36 | reefcld 14818 |
. . . . . . 7
⊢ (𝜑 → (exp‘(𝐶 / 𝐸)) ∈ ℝ) |
38 | | pnfxr 10092 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
39 | | icossre 12254 |
. . . . . . 7
⊢
(((exp‘(𝐶 /
𝐸)) ∈ ℝ ∧
+∞ ∈ ℝ*) → ((exp‘(𝐶 / 𝐸))[,)+∞) ⊆
ℝ) |
40 | 37, 38, 39 | sylancl 694 |
. . . . . 6
⊢ (𝜑 → ((exp‘(𝐶 / 𝐸))[,)+∞) ⊆
ℝ) |
41 | | pntibndlem2.8 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) |
42 | 40, 41 | sseldd 3604 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℝ) |
43 | | ioossre 12235 |
. . . . . 6
⊢ (𝑋(,)+∞) ⊆
ℝ |
44 | | pntibndlem2.9 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ (𝑋(,)+∞)) |
45 | 43, 44 | sseldi 3601 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ ℝ) |
46 | 42, 45 | remulcld 10070 |
. . . 4
⊢ (𝜑 → (𝑀 · 𝑌) ∈ ℝ) |
47 | 19 | a1i 11 |
. . . . 5
⊢ (𝜑 → 2 ∈
ℝ) |
48 | | eliooord 12233 |
. . . . . . . . . . . . 13
⊢ (𝐿 ∈ (0(,)1) → (0 <
𝐿 ∧ 𝐿 < 1)) |
49 | 11, 48 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 < 𝐿 ∧ 𝐿 < 1)) |
50 | 49 | simpld 475 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 𝐿) |
51 | 12, 50 | elrpd 11869 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈
ℝ+) |
52 | 51 | rpge0d 11876 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝐿) |
53 | 49 | simprd 479 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 < 1) |
54 | 35 | rpge0d 11876 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝐸) |
55 | 33 | simprd 479 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 < 1) |
56 | 12, 6, 14, 6, 52, 53, 54, 55 | ltmul12ad 10965 |
. . . . . . . 8
⊢ (𝜑 → (𝐿 · 𝐸) < (1 · 1)) |
57 | | 1t1e1 11175 |
. . . . . . . 8
⊢ (1
· 1) = 1 |
58 | 56, 57 | syl6breq 4694 |
. . . . . . 7
⊢ (𝜑 → (𝐿 · 𝐸) < 1) |
59 | 15, 6, 6, 58 | ltadd2dd 10196 |
. . . . . 6
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < (1 + 1)) |
60 | | df-2 11079 |
. . . . . 6
⊢ 2 = (1 +
1) |
61 | 59, 60 | syl6breqr 4695 |
. . . . 5
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < 2) |
62 | 16, 47, 2, 61 | ltmul1dd 11927 |
. . . 4
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑁) < (2 · 𝑁)) |
63 | 4 | simprd 479 |
. . . . . 6
⊢ (𝜑 → 𝑁 ≤ ((𝑀 / 2) · 𝑌)) |
64 | 42 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℂ) |
65 | 45 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ ℂ) |
66 | | rpcnne0 11850 |
. . . . . . . 8
⊢ (2 ∈
ℝ+ → (2 ∈ ℂ ∧ 2 ≠ 0)) |
67 | 27, 66 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → (2 ∈ ℂ ∧ 2
≠ 0)) |
68 | | div23 10704 |
. . . . . . 7
⊢ ((𝑀 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((𝑀 · 𝑌) / 2) = ((𝑀 / 2) · 𝑌)) |
69 | 64, 65, 67, 68 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → ((𝑀 · 𝑌) / 2) = ((𝑀 / 2) · 𝑌)) |
70 | 63, 69 | breqtrrd 4681 |
. . . . 5
⊢ (𝜑 → 𝑁 ≤ ((𝑀 · 𝑌) / 2)) |
71 | 17, 46, 28 | lemuldiv2d 11922 |
. . . . 5
⊢ (𝜑 → ((2 · 𝑁) ≤ (𝑀 · 𝑌) ↔ 𝑁 ≤ ((𝑀 · 𝑌) / 2))) |
72 | 70, 71 | mpbird 247 |
. . . 4
⊢ (𝜑 → (2 · 𝑁) ≤ (𝑀 · 𝑌)) |
73 | 18, 21, 46, 62, 72 | ltletrd 10197 |
. . 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 25279 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁))) |
77 | 76 | simp1d 1073 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ ℝ) |
78 | 2 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈
ℝ+) |
79 | 76 | simp2d 1074 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ≤ 𝑢) |
80 | 77, 78, 79 | rpgecld 11911 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ ℝ+) |
81 | 8 | pntrf 25252 |
. . . . . . . . . 10
⊢ 𝑅:ℝ+⟶ℝ |
82 | 81 | ffvelrni 6358 |
. . . . . . . . 9
⊢ (𝑢 ∈ ℝ+
→ (𝑅‘𝑢) ∈
ℝ) |
83 | 80, 82 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅‘𝑢) ∈ ℝ) |
84 | 83, 80 | rerpdivcld 11903 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑢) / 𝑢) ∈ ℝ) |
85 | 84 | recnd 10068 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑢) / 𝑢) ∈ ℂ) |
86 | 85 | abscld 14175 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑢) / 𝑢)) ∈ ℝ) |
87 | 81 | ffvelrni 6358 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℝ+
→ (𝑅‘𝑁) ∈
ℝ) |
88 | 2, 87 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑅‘𝑁) ∈ ℝ) |
89 | 88, 1 | nndivred 11069 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑅‘𝑁) / 𝑁) ∈ ℝ) |
90 | 89 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑁) / 𝑁) ∈ ℝ) |
91 | 90 | recnd 10068 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑁) / 𝑁) ∈ ℂ) |
92 | 85, 91 | subcld 10392 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁)) ∈ ℂ) |
93 | 92 | abscld 14175 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) ∈ ℝ) |
94 | 91 | abscld 14175 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑁) / 𝑁)) ∈ ℝ) |
95 | 93, 94 | readdcld 10069 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) + (abs‘((𝑅‘𝑁) / 𝑁))) ∈ ℝ) |
96 | 14 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐸 ∈ ℝ) |
97 | 85, 91 | abs2difd 14196 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅‘𝑢) / 𝑢)) − (abs‘((𝑅‘𝑁) / 𝑁))) ≤ (abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁)))) |
98 | 86, 94, 93 | lesubaddd 10624 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((abs‘((𝑅‘𝑢) / 𝑢)) − (abs‘((𝑅‘𝑁) / 𝑁))) ≤ (abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) ↔ (abs‘((𝑅‘𝑢) / 𝑢)) ≤ ((abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) + (abs‘((𝑅‘𝑁) / 𝑁))))) |
99 | 97, 98 | mpbid 222 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑢) / 𝑢)) ≤ ((abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) + (abs‘((𝑅‘𝑁) / 𝑁)))) |
100 | 96 | rehalfcld 11279 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 2) ∈ ℝ) |
101 | 17 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ ℝ) |
102 | 77, 101 | resubcld 10458 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 − 𝑁) ∈ ℝ) |
103 | 102, 78 | rerpdivcld 11903 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 − 𝑁) / 𝑁) ∈ ℝ) |
104 | | 3re 11094 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℝ |
105 | 104 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 3 ∈
ℝ) |
106 | 86, 105 | readdcld 10069 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅‘𝑢) / 𝑢)) + 3) ∈ ℝ) |
107 | 103, 106 | remulcld 10070 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) ∈ ℝ) |
108 | | pntibndlem2.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
109 | 108 | rpred 11872 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ ℝ) |
110 | 109 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℝ) |
111 | | 1red 10055 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 ∈
ℝ) |
112 | | 4nn 11187 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℕ |
113 | | nnrp 11842 |
. . . . . . . . . . . . . . . . . 18
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) |
114 | 112, 113 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 4 ∈
ℝ+) |
115 | 35, 114 | rpdivcld 11889 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐸 / 4) ∈
ℝ+) |
116 | 108, 115 | rpdivcld 11889 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑇 / (𝐸 / 4)) ∈
ℝ+) |
117 | 116 | rpred 11872 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑇 / (𝐸 / 4)) ∈ ℝ) |
118 | 117 | reefcld 14818 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) ∈ ℝ) |
119 | 118 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(𝑇 / (𝐸 / 4))) ∈ ℝ) |
120 | | efgt1 14846 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 / (𝐸 / 4)) ∈ ℝ+ → 1
< (exp‘(𝑇 / (𝐸 / 4)))) |
121 | 116, 120 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 < (exp‘(𝑇 / (𝐸 / 4)))) |
122 | 121 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 < (exp‘(𝑇 / (𝐸 / 4)))) |
123 | | pntibndlem2.7 |
. . . . . . . . . . . . . . . 16
⊢ 𝑋 = ((exp‘(𝑇 / (𝐸 / 4))) + 𝑍) |
124 | | pntibndlem3.6 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑍 ∈
ℝ+) |
125 | 124 | rpred 11872 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑍 ∈ ℝ) |
126 | 118, 125 | readdcld 10069 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((exp‘(𝑇 / (𝐸 / 4))) + 𝑍) ∈ ℝ) |
127 | 123, 126 | syl5eqel 2705 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ∈ ℝ) |
128 | 118, 124 | ltaddrpd 11905 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < ((exp‘(𝑇 / (𝐸 / 4))) + 𝑍)) |
129 | 128, 123 | syl6breqr 4695 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < 𝑋) |
130 | | eliooord 12233 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑌 ∈ (𝑋(,)+∞) → (𝑋 < 𝑌 ∧ 𝑌 < +∞)) |
131 | 44, 130 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑋 < 𝑌 ∧ 𝑌 < +∞)) |
132 | 131 | simpld 475 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 < 𝑌) |
133 | 118, 127,
45, 129, 132 | lttrd 10198 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < 𝑌) |
134 | 118, 45, 17, 133, 5 | lttrd 10198 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (exp‘(𝑇 / (𝐸 / 4))) < 𝑁) |
135 | 134 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(𝑇 / (𝐸 / 4))) < 𝑁) |
136 | 111, 119,
101, 122, 135 | lttrd 10198 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 < 𝑁) |
137 | 101, 136 | rplogcld 24375 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (log‘𝑁) ∈
ℝ+) |
138 | 110, 137 | rerpdivcld 11903 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℝ) |
139 | 107, 138 | readdcld 10069 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))) ∈ ℝ) |
140 | | peano2re 10209 |
. . . . . . . . . . . 12
⊢
((abs‘((𝑅‘𝑢) / 𝑢)) ∈ ℝ → ((abs‘((𝑅‘𝑢) / 𝑢)) + 1) ∈ ℝ) |
141 | 86, 140 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅‘𝑢) / 𝑢)) + 1) ∈ ℝ) |
142 | 103, 141 | remulcld 10070 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) ∈ ℝ) |
143 | | chpcl 24850 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ℝ →
(ψ‘𝑢) ∈
ℝ) |
144 | 77, 143 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑢) ∈ ℝ) |
145 | | chpcl 24850 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℝ →
(ψ‘𝑁) ∈
ℝ) |
146 | 101, 145 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑁) ∈ ℝ) |
147 | 144, 146 | resubcld 10458 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((ψ‘𝑢) − (ψ‘𝑁)) ∈ ℝ) |
148 | 147, 78 | rerpdivcld 11903 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ∈ ℝ) |
149 | 142, 148 | readdcld 10069 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) ∈ ℝ) |
150 | 103, 86 | remulcld 10070 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) ∈ ℝ) |
151 | 88 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅‘𝑁) ∈ ℝ) |
152 | 83, 151 | resubcld 10458 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑢) − (𝑅‘𝑁)) ∈ ℝ) |
153 | 152 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑢) − (𝑅‘𝑁)) ∈ ℂ) |
154 | 153 | abscld 14175 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) ∈ ℝ) |
155 | 154, 78 | rerpdivcld 11903 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁) ∈ ℝ) |
156 | 150, 155 | readdcld 10069 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁)) ∈ ℝ) |
157 | 103, 84 | remulcld 10070 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) ∈ ℝ) |
158 | 157 | renegcld 10457 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) ∈ ℝ) |
159 | 158 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) ∈ ℂ) |
160 | 152, 78 | rerpdivcld 11903 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁) ∈ ℝ) |
161 | 160 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁) ∈ ℂ) |
162 | 159, 161 | abstrid 14195 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(-(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) + (((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁))) ≤ ((abs‘-(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢))) + (abs‘(((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁)))) |
163 | 77 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ ℂ) |
164 | 101 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ ℂ) |
165 | 78 | rpne0d 11877 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ≠ 0) |
166 | 163, 164,
164, 165 | divsubdird 10840 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 − 𝑁) / 𝑁) = ((𝑢 / 𝑁) − (𝑁 / 𝑁))) |
167 | 164, 165 | dividd 10799 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 / 𝑁) = 1) |
168 | 167 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) − (𝑁 / 𝑁)) = ((𝑢 / 𝑁) − 1)) |
169 | 166, 168 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 − 𝑁) / 𝑁) = ((𝑢 / 𝑁) − 1)) |
170 | 169 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) = (((𝑢 / 𝑁) − 1) · ((𝑅‘𝑢) / 𝑢))) |
171 | 77, 78 | rerpdivcld 11903 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ∈ ℝ) |
172 | 171 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ∈ ℂ) |
173 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 1 ∈
ℂ) |
174 | 172, 173,
85 | subdird 10487 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 / 𝑁) − 1) · ((𝑅‘𝑢) / 𝑢)) = (((𝑢 / 𝑁) · ((𝑅‘𝑢) / 𝑢)) − (1 · ((𝑅‘𝑢) / 𝑢)))) |
175 | 80 | rpcnne0d 11881 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ ℂ ∧ 𝑢 ≠ 0)) |
176 | 78 | rpcnne0d 11881 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
177 | 83 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅‘𝑢) ∈ ℂ) |
178 | | dmdcan 10735 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑢 ∈ ℂ ∧ 𝑢 ≠ 0) ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ (𝑅‘𝑢) ∈ ℂ) → ((𝑢 / 𝑁) · ((𝑅‘𝑢) / 𝑢)) = ((𝑅‘𝑢) / 𝑁)) |
179 | 175, 176,
177, 178 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) · ((𝑅‘𝑢) / 𝑢)) = ((𝑅‘𝑢) / 𝑁)) |
180 | 85 | mulid2d 10058 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 · ((𝑅‘𝑢) / 𝑢)) = ((𝑅‘𝑢) / 𝑢)) |
181 | 179, 180 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 / 𝑁) · ((𝑅‘𝑢) / 𝑢)) − (1 · ((𝑅‘𝑢) / 𝑢))) = (((𝑅‘𝑢) / 𝑁) − ((𝑅‘𝑢) / 𝑢))) |
182 | 170, 174,
181 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) = (((𝑅‘𝑢) / 𝑁) − ((𝑅‘𝑢) / 𝑢))) |
183 | 182 | negeqd 10275 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) = -(((𝑅‘𝑢) / 𝑁) − ((𝑅‘𝑢) / 𝑢))) |
184 | 83, 78 | rerpdivcld 11903 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑢) / 𝑁) ∈ ℝ) |
185 | 184 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑢) / 𝑁) ∈ ℂ) |
186 | 185, 85 | negsubdi2d 10408 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑅‘𝑢) / 𝑁) − ((𝑅‘𝑢) / 𝑢)) = (((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑢) / 𝑁))) |
187 | 183, 186 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → -(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) = (((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑢) / 𝑁))) |
188 | 151 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅‘𝑁) ∈ ℂ) |
189 | 177, 188,
164, 165 | divsubdird 10840 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁) = (((𝑅‘𝑢) / 𝑁) − ((𝑅‘𝑁) / 𝑁))) |
190 | 187, 189 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (-(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) + (((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁)) = ((((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑢) / 𝑁)) + (((𝑅‘𝑢) / 𝑁) − ((𝑅‘𝑁) / 𝑁)))) |
191 | 85, 185, 91 | npncand 10416 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑢) / 𝑁)) + (((𝑅‘𝑢) / 𝑁) − ((𝑅‘𝑁) / 𝑁))) = (((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) |
192 | 190, 191 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (-(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) + (((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁)) = (((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) |
193 | 192 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(-(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) + (((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁))) = (abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁)))) |
194 | 157 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)) ∈ ℂ) |
195 | 194 | absnegd 14188 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘-(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢))) = (abs‘(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢)))) |
196 | 103 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 − 𝑁) / 𝑁) ∈ ℂ) |
197 | 196, 85 | absmuld 14193 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢))) = ((abs‘((𝑢 − 𝑁) / 𝑁)) · (abs‘((𝑅‘𝑢) / 𝑢)))) |
198 | 77, 101 | subge0d 10617 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (0 ≤ (𝑢 − 𝑁) ↔ 𝑁 ≤ 𝑢)) |
199 | 79, 198 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 0 ≤ (𝑢 − 𝑁)) |
200 | 102, 78, 199 | divge0d 11912 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 0 ≤ ((𝑢 − 𝑁) / 𝑁)) |
201 | 103, 200 | absidd 14161 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑢 − 𝑁) / 𝑁)) = ((𝑢 − 𝑁) / 𝑁)) |
202 | 201 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑢 − 𝑁) / 𝑁)) · (abs‘((𝑅‘𝑢) / 𝑢))) = (((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢)))) |
203 | 195, 197,
202 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘-(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢))) = (((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢)))) |
204 | 153, 164,
165 | absdivd 14194 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁)) = ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / (abs‘𝑁))) |
205 | 78 | rprege0d 11879 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁)) |
206 | | absid 14036 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) → (abs‘𝑁) = 𝑁) |
207 | 205, 206 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘𝑁) = 𝑁) |
208 | 207 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / (abs‘𝑁)) = ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁)) |
209 | 204, 208 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁)) = ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁)) |
210 | 203, 209 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘-(((𝑢 − 𝑁) / 𝑁) · ((𝑅‘𝑢) / 𝑢))) + (abs‘(((𝑅‘𝑢) − (𝑅‘𝑁)) / 𝑁))) = ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁))) |
211 | 162, 193,
210 | 3brtr3d 4684 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) ≤ ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁))) |
212 | 102, 147 | readdcld 10069 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) ∈ ℝ) |
213 | 212, 78 | rerpdivcld 11903 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁) ∈ ℝ) |
214 | 147 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((ψ‘𝑢) − (ψ‘𝑁)) ∈ ℂ) |
215 | 164, 163 | subcld 10392 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 − 𝑢) ∈ ℂ) |
216 | 214, 215 | abstrid 14195 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁 − 𝑢))) ≤ ((abs‘((ψ‘𝑢) − (ψ‘𝑁))) + (abs‘(𝑁 − 𝑢)))) |
217 | 8 | pntrval 25251 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ ℝ+
→ (𝑅‘𝑢) = ((ψ‘𝑢) − 𝑢)) |
218 | 80, 217 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅‘𝑢) = ((ψ‘𝑢) − 𝑢)) |
219 | 8 | pntrval 25251 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℝ+
→ (𝑅‘𝑁) = ((ψ‘𝑁) − 𝑁)) |
220 | 78, 219 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑅‘𝑁) = ((ψ‘𝑁) − 𝑁)) |
221 | 218, 220 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑅‘𝑢) − (𝑅‘𝑁)) = (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁))) |
222 | 144 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑢) ∈ ℂ) |
223 | 146 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑁) ∈ ℂ) |
224 | | subadd4 10325 |
. . . . . . . . . . . . . . . . . 18
⊢
((((ψ‘𝑢)
∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) →
(((ψ‘𝑢) −
(ψ‘𝑁)) −
(𝑢 − 𝑁)) = (((ψ‘𝑢) + 𝑁) − ((ψ‘𝑁) + 𝑢))) |
225 | | sub4 10326 |
. . . . . . . . . . . . . . . . . 18
⊢
((((ψ‘𝑢)
∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) →
(((ψ‘𝑢) −
(ψ‘𝑁)) −
(𝑢 − 𝑁)) = (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁))) |
226 | | addsub4 10324 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((ψ‘𝑢)
∈ ℂ ∧ 𝑁
∈ ℂ) ∧ ((ψ‘𝑁) ∈ ℂ ∧ 𝑢 ∈ ℂ)) → (((ψ‘𝑢) + 𝑁) − ((ψ‘𝑁) + 𝑢)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁 − 𝑢))) |
227 | 226 | an42s 870 |
. . . . . . . . . . . . . . . . . 18
⊢
((((ψ‘𝑢)
∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) →
(((ψ‘𝑢) + 𝑁) − ((ψ‘𝑁) + 𝑢)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁 − 𝑢))) |
228 | 224, 225,
227 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . . 17
⊢
((((ψ‘𝑢)
∈ ℂ ∧ (ψ‘𝑁) ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑁 ∈ ℂ)) →
(((ψ‘𝑢) −
𝑢) −
((ψ‘𝑁) −
𝑁)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁 − 𝑢))) |
229 | 222, 223,
163, 164, 228 | syl22anc 1327 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − 𝑢) − ((ψ‘𝑁) − 𝑁)) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁 − 𝑢))) |
230 | 221, 229 | eqtr2d 2657 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁 − 𝑢)) = ((𝑅‘𝑢) − (𝑅‘𝑁))) |
231 | 230 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((ψ‘𝑢) − (ψ‘𝑁)) + (𝑁 − 𝑢))) = (abs‘((𝑅‘𝑢) − (𝑅‘𝑁)))) |
232 | | chpwordi 24883 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢) → (ψ‘𝑁) ≤ (ψ‘𝑢)) |
233 | 101, 77, 79, 232 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (ψ‘𝑁) ≤ (ψ‘𝑢)) |
234 | 146, 144,
233 | abssubge0d 14170 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((ψ‘𝑢) − (ψ‘𝑁))) = ((ψ‘𝑢) − (ψ‘𝑁))) |
235 | 101, 77, 79 | abssuble0d 14171 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(𝑁 − 𝑢)) = (𝑢 − 𝑁)) |
236 | 234, 235 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((ψ‘𝑢) − (ψ‘𝑁))) + (abs‘(𝑁 − 𝑢))) = (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑢 − 𝑁))) |
237 | 102 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 − 𝑁) ∈ ℂ) |
238 | 214, 237 | addcomd 10238 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) + (𝑢 − 𝑁)) = ((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁)))) |
239 | 236, 238 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((ψ‘𝑢) − (ψ‘𝑁))) + (abs‘(𝑁 − 𝑢))) = ((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁)))) |
240 | 216, 231,
239 | 3brtr3d 4684 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) ≤ ((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁)))) |
241 | 154, 212,
78, 240 | lediv1dd 11930 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁) ≤ (((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁)) |
242 | 155, 213,
150, 241 | leadd2dd 10642 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁)) ≤ ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + (((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁))) |
243 | 150 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) ∈ ℂ) |
244 | 148 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ∈ ℂ) |
245 | 243, 196,
244 | addassd 10062 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((𝑢 − 𝑁) / 𝑁)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) = ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + (((𝑢 − 𝑁) / 𝑁) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)))) |
246 | 86 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑢) / 𝑢)) ∈ ℂ) |
247 | 196, 246,
173 | adddid 10064 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) = ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + (((𝑢 − 𝑁) / 𝑁) · 1))) |
248 | 196 | mulid1d 10057 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · 1) = ((𝑢 − 𝑁) / 𝑁)) |
249 | 248 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + (((𝑢 − 𝑁) / 𝑁) · 1)) = ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((𝑢 − 𝑁) / 𝑁))) |
250 | 247, 249 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) = ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((𝑢 − 𝑁) / 𝑁))) |
251 | 250 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) = (((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((𝑢 − 𝑁) / 𝑁)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁))) |
252 | 237, 214,
164, 165 | divdird 10839 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁) = (((𝑢 − 𝑁) / 𝑁) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁))) |
253 | 252 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + (((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁)) = ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + (((𝑢 − 𝑁) / 𝑁) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)))) |
254 | 245, 251,
253 | 3eqtr4d 2666 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) = ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + (((𝑢 − 𝑁) + ((ψ‘𝑢) − (ψ‘𝑁))) / 𝑁))) |
255 | 242, 254 | breqtrrd 4681 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · (abs‘((𝑅‘𝑢) / 𝑢))) + ((abs‘((𝑅‘𝑢) − (𝑅‘𝑁))) / 𝑁)) ≤ ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁))) |
256 | 93, 156, 149, 211, 255 | letrd 10194 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) ≤ ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁))) |
257 | | remulcl 10021 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℝ ∧ ((𝑢
− 𝑁) / 𝑁) ∈ ℝ) → (2
· ((𝑢 − 𝑁) / 𝑁)) ∈ ℝ) |
258 | 19, 103, 257 | sylancr 695 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · ((𝑢 − 𝑁) / 𝑁)) ∈ ℝ) |
259 | 258, 138 | readdcld 10069 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((2 · ((𝑢 − 𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))) ∈ ℝ) |
260 | | remulcl 10021 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℝ ∧ (𝑢
− 𝑁) ∈ ℝ)
→ (2 · (𝑢
− 𝑁)) ∈
ℝ) |
261 | 19, 102, 260 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · (𝑢 − 𝑁)) ∈ ℝ) |
262 | 101, 137 | rerpdivcld 11903 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑁 / (log‘𝑁)) ∈ ℝ) |
263 | 110, 262 | remulcld 10070 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℝ) |
264 | 261, 263 | readdcld 10069 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((2 · (𝑢 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) ∈ ℝ) |
265 | 18 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((1 + (𝐿 · 𝐸)) · 𝑁) ∈ ℝ) |
266 | 21 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · 𝑁) ∈ ℝ) |
267 | 76 | simp3d 1075 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁)) |
268 | | ltle 10126 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((1 +
(𝐿 · 𝐸)) ∈ ℝ ∧ 2 ∈
ℝ) → ((1 + (𝐿
· 𝐸)) < 2 →
(1 + (𝐿 · 𝐸)) ≤ 2)) |
269 | 16, 19, 268 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) < 2 → (1 + (𝐿 · 𝐸)) ≤ 2)) |
270 | 61, 269 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ≤ 2) |
271 | 270 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 + (𝐿 · 𝐸)) ≤ 2) |
272 | 16 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 + (𝐿 · 𝐸)) ∈ ℝ) |
273 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 2 ∈
ℝ) |
274 | 272, 273,
78 | lemul1d 11915 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((1 + (𝐿 · 𝐸)) ≤ 2 ↔ ((1 + (𝐿 · 𝐸)) · 𝑁) ≤ (2 · 𝑁))) |
275 | 271, 274 | mpbid 222 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((1 + (𝐿 · 𝐸)) · 𝑁) ≤ (2 · 𝑁)) |
276 | 77, 265, 266, 267, 275 | letrd 10194 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ≤ (2 · 𝑁)) |
277 | | elicc2 12238 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℝ ∧ (2
· 𝑁) ∈ ℝ)
→ (𝑢 ∈ (𝑁[,](2 · 𝑁)) ↔ (𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ (2 · 𝑁)))) |
278 | 101, 266,
277 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ (𝑁[,](2 · 𝑁)) ↔ (𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ (2 · 𝑁)))) |
279 | 77, 79, 276, 278 | mpbir3and 1245 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑢 ∈ (𝑁[,](2 · 𝑁))) |
280 | | 1re 10039 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ |
281 | 280 | rexri 10097 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ* |
282 | | elioopnf 12267 |
. . . . . . . . . . . . . . . . 17
⊢ (1 ∈
ℝ* → (𝑁 ∈ (1(,)+∞) ↔ (𝑁 ∈ ℝ ∧ 1 <
𝑁))) |
283 | 281, 282 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ (1(,)+∞) ↔
(𝑁 ∈ ℝ ∧ 1
< 𝑁)) |
284 | 101, 136,
283 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑁 ∈ (1(,)+∞)) |
285 | | pntibndlem2.6 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦 − 𝑥)) + (𝑇 · (𝑥 / (log‘𝑥))))) |
286 | 285 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦 − 𝑥)) + (𝑇 · (𝑥 / (log‘𝑥))))) |
287 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑁 → 𝑥 = 𝑁) |
288 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁)) |
289 | 287, 288 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑁 → (𝑥[,](2 · 𝑥)) = (𝑁[,](2 · 𝑁))) |
290 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑁 → (ψ‘𝑥) = (ψ‘𝑁)) |
291 | 290 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑁 → ((ψ‘𝑦) − (ψ‘𝑥)) = ((ψ‘𝑦) − (ψ‘𝑁))) |
292 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑁 → (𝑦 − 𝑥) = (𝑦 − 𝑁)) |
293 | 292 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑁 → (2 · (𝑦 − 𝑥)) = (2 · (𝑦 − 𝑁))) |
294 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑁 → (log‘𝑥) = (log‘𝑁)) |
295 | 287, 294 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑁 → (𝑥 / (log‘𝑥)) = (𝑁 / (log‘𝑁))) |
296 | 295 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑁 → (𝑇 · (𝑥 / (log‘𝑥))) = (𝑇 · (𝑁 / (log‘𝑁)))) |
297 | 293, 296 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑁 → ((2 · (𝑦 − 𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))) = ((2 · (𝑦 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))) |
298 | 291, 297 | breq12d 4666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑁 → (((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦 − 𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))) ↔ ((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))) |
299 | 289, 298 | raleqbidv 3152 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑁 → (∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦 − 𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))) ↔ ∀𝑦 ∈ (𝑁[,](2 · 𝑁))((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))) |
300 | 299 | rspcv 3305 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ (1(,)+∞) →
(∀𝑥 ∈
(1(,)+∞)∀𝑦
∈ (𝑥[,](2 ·
𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦 − 𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))) → ∀𝑦 ∈ (𝑁[,](2 · 𝑁))((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))) |
301 | 284, 286,
300 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ∀𝑦 ∈ (𝑁[,](2 · 𝑁))((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))) |
302 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑢 → (ψ‘𝑦) = (ψ‘𝑢)) |
303 | 302 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑢 → ((ψ‘𝑦) − (ψ‘𝑁)) = ((ψ‘𝑢) − (ψ‘𝑁))) |
304 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑢 → (𝑦 − 𝑁) = (𝑢 − 𝑁)) |
305 | 304 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑢 → (2 · (𝑦 − 𝑁)) = (2 · (𝑢 − 𝑁))) |
306 | 305 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑢 → ((2 · (𝑦 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) = ((2 · (𝑢 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))) |
307 | 303, 306 | breq12d 4666 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑢 → (((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) ↔ ((ψ‘𝑢) − (ψ‘𝑁)) ≤ ((2 · (𝑢 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))) |
308 | 307 | rspcv 3305 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ (𝑁[,](2 · 𝑁)) → (∀𝑦 ∈ (𝑁[,](2 · 𝑁))((ψ‘𝑦) − (ψ‘𝑁)) ≤ ((2 · (𝑦 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) → ((ψ‘𝑢) − (ψ‘𝑁)) ≤ ((2 · (𝑢 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))))) |
309 | 279, 301,
308 | sylc 65 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((ψ‘𝑢) − (ψ‘𝑁)) ≤ ((2 · (𝑢 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁))))) |
310 | 147, 264,
78, 309 | lediv1dd 11930 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ≤ (((2 · (𝑢 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁)) |
311 | 261 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · (𝑢 − 𝑁)) ∈ ℂ) |
312 | 108 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈
ℝ+) |
313 | 312 | rpred 11872 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℝ) |
314 | 313, 262 | remulcld 10070 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℝ) |
315 | 314 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℂ) |
316 | | divdir 10710 |
. . . . . . . . . . . . . 14
⊢ (((2
· (𝑢 − 𝑁)) ∈ ℂ ∧ (𝑇 · (𝑁 / (log‘𝑁))) ∈ ℂ ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) → (((2 · (𝑢 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁) = (((2 · (𝑢 − 𝑁)) / 𝑁) + ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁))) |
317 | 311, 315,
176, 316 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((2 · (𝑢 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁) = (((2 · (𝑢 − 𝑁)) / 𝑁) + ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁))) |
318 | | 2cnd 11093 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 2 ∈
ℂ) |
319 | 318, 237,
164, 165 | divassd 10836 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((2 · (𝑢 − 𝑁)) / 𝑁) = (2 · ((𝑢 − 𝑁) / 𝑁))) |
320 | 110 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝑇 ∈ ℂ) |
321 | 137 | rpcnne0d 11881 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((log‘𝑁) ∈ ℂ ∧ (log‘𝑁) ≠ 0)) |
322 | | div12 10707 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧
((log‘𝑁) ∈
ℂ ∧ (log‘𝑁)
≠ 0)) → (𝑇 ·
(𝑁 / (log‘𝑁))) = (𝑁 · (𝑇 / (log‘𝑁)))) |
323 | 320, 164,
321, 322 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 · (𝑁 / (log‘𝑁))) = (𝑁 · (𝑇 / (log‘𝑁)))) |
324 | 323 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁) = ((𝑁 · (𝑇 / (log‘𝑁))) / 𝑁)) |
325 | 312, 137 | rpdivcld 11889 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈
ℝ+) |
326 | 325 | rpcnd 11874 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℂ) |
327 | 326, 164,
165 | divcan3d 10806 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑁 · (𝑇 / (log‘𝑁))) / 𝑁) = (𝑇 / (log‘𝑁))) |
328 | 324, 327 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁) = (𝑇 / (log‘𝑁))) |
329 | 319, 328 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((2 · (𝑢 − 𝑁)) / 𝑁) + ((𝑇 · (𝑁 / (log‘𝑁))) / 𝑁)) = ((2 · ((𝑢 − 𝑁) / 𝑁)) + (𝑇 / (log‘𝑁)))) |
330 | 317, 329 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((2 · (𝑢 − 𝑁)) + (𝑇 · (𝑁 / (log‘𝑁)))) / 𝑁) = ((2 · ((𝑢 − 𝑁) / 𝑁)) + (𝑇 / (log‘𝑁)))) |
331 | 310, 330 | breqtrd 4679 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁) ≤ ((2 · ((𝑢 − 𝑁) / 𝑁)) + (𝑇 / (log‘𝑁)))) |
332 | 148, 259,
142, 331 | leadd2dd 10642 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) ≤ ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + ((2 · ((𝑢 − 𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))))) |
333 | 142 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) ∈ ℂ) |
334 | 258 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · ((𝑢 − 𝑁) / 𝑁)) ∈ ℂ) |
335 | 138 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ∈ ℂ) |
336 | 333, 334,
335 | addassd 10062 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (2 · ((𝑢 − 𝑁) / 𝑁))) + (𝑇 / (log‘𝑁))) = ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + ((2 · ((𝑢 − 𝑁) / 𝑁)) + (𝑇 / (log‘𝑁))))) |
337 | | 2cn 11091 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
338 | | mulcom 10022 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ ((𝑢
− 𝑁) / 𝑁) ∈ ℂ) → (2
· ((𝑢 − 𝑁) / 𝑁)) = (((𝑢 − 𝑁) / 𝑁) · 2)) |
339 | 337, 196,
338 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (2 · ((𝑢 − 𝑁) / 𝑁)) = (((𝑢 − 𝑁) / 𝑁) · 2)) |
340 | 339 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (2 · ((𝑢 − 𝑁) / 𝑁))) = ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((𝑢 − 𝑁) / 𝑁) · 2))) |
341 | 141 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅‘𝑢) / 𝑢)) + 1) ∈ ℂ) |
342 | 196, 341,
318 | adddid 10064 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · (((abs‘((𝑅‘𝑢) / 𝑢)) + 1) + 2)) = ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((𝑢 − 𝑁) / 𝑁) · 2))) |
343 | 246, 173,
318 | addassd 10062 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((abs‘((𝑅‘𝑢) / 𝑢)) + 1) + 2) = ((abs‘((𝑅‘𝑢) / 𝑢)) + (1 + 2))) |
344 | | 1p2e3 11152 |
. . . . . . . . . . . . . . . 16
⊢ (1 + 2) =
3 |
345 | 344 | oveq2i 6661 |
. . . . . . . . . . . . . . 15
⊢
((abs‘((𝑅‘𝑢) / 𝑢)) + (1 + 2)) = ((abs‘((𝑅‘𝑢) / 𝑢)) + 3) |
346 | 343, 345 | syl6eq 2672 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((abs‘((𝑅‘𝑢) / 𝑢)) + 1) + 2) = ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) |
347 | 346 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · (((abs‘((𝑅‘𝑢) / 𝑢)) + 1) + 2)) = (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3))) |
348 | 340, 342,
347 | 3eqtr2d 2662 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (2 · ((𝑢 − 𝑁) / 𝑁))) = (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3))) |
349 | 348 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (2 · ((𝑢 − 𝑁) / 𝑁))) + (𝑇 / (log‘𝑁))) = ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁)))) |
350 | 336, 349 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + ((2 · ((𝑢 − 𝑁) / 𝑁)) + (𝑇 / (log‘𝑁)))) = ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁)))) |
351 | 332, 350 | breqtrd 4679 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 1)) + (((ψ‘𝑢) − (ψ‘𝑁)) / 𝑁)) ≤ ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁)))) |
352 | 93, 149, 139, 256, 351 | letrd 10194 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) ≤ ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁)))) |
353 | 100 | rehalfcld 11279 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) / 2) ∈ ℝ) |
354 | 77, 272, 78 | ledivmul2d 11926 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) ≤ (1 + (𝐿 · 𝐸)) ↔ 𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁))) |
355 | 267, 354 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ≤ (1 + (𝐿 · 𝐸))) |
356 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
357 | 15 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐿 · 𝐸) ∈ ℝ) |
358 | 357 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐿 · 𝐸) ∈ ℂ) |
359 | | addcom 10222 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ (𝐿
· 𝐸) ∈ ℂ)
→ (1 + (𝐿 ·
𝐸)) = ((𝐿 · 𝐸) + 1)) |
360 | 356, 358,
359 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 + (𝐿 · 𝐸)) = ((𝐿 · 𝐸) + 1)) |
361 | 355, 360 | breqtrd 4679 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 / 𝑁) ≤ ((𝐿 · 𝐸) + 1)) |
362 | 171, 111,
357 | lesubaddd 10624 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 / 𝑁) − 1) ≤ (𝐿 · 𝐸) ↔ (𝑢 / 𝑁) ≤ ((𝐿 · 𝐸) + 1))) |
363 | 361, 362 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 / 𝑁) − 1) ≤ (𝐿 · 𝐸)) |
364 | 169, 363 | eqbrtrd 4675 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑢 − 𝑁) / 𝑁) ≤ (𝐿 · 𝐸)) |
365 | 9 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐴 ∈
ℝ+) |
366 | 365 | rpred 11872 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐴 ∈ ℝ) |
367 | 74 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴) |
368 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑢 → (𝑅‘𝑥) = (𝑅‘𝑢)) |
369 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑢 → 𝑥 = 𝑢) |
370 | 368, 369 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑢 → ((𝑅‘𝑥) / 𝑥) = ((𝑅‘𝑢) / 𝑢)) |
371 | 370 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑢 → (abs‘((𝑅‘𝑥) / 𝑥)) = (abs‘((𝑅‘𝑢) / 𝑢))) |
372 | 371 | breq1d 4663 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑢 → ((abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴 ↔ (abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐴)) |
373 | 372 | rspcv 3305 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ ℝ+
→ (∀𝑥 ∈
ℝ+ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴 → (abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐴)) |
374 | 80, 367, 373 | sylc 65 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐴) |
375 | 86, 366, 105, 374 | leadd1dd 10641 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘((𝑅‘𝑢) / 𝑢)) + 3) ≤ (𝐴 + 3)) |
376 | 103, 200 | jca 554 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) ∈ ℝ ∧ 0 ≤ ((𝑢 − 𝑁) / 𝑁))) |
377 | | 3nn 11186 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℕ |
378 | | nnrp 11842 |
. . . . . . . . . . . . . . . 16
⊢ (3 ∈
ℕ → 3 ∈ ℝ+) |
379 | 377, 378 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℝ+ |
380 | | rpaddcl 11854 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ+
∧ 3 ∈ ℝ+) → (𝐴 + 3) ∈
ℝ+) |
381 | 365, 379,
380 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐴 + 3) ∈
ℝ+) |
382 | 381 | rprege0d 11879 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐴 + 3) ∈ ℝ ∧ 0 ≤ (𝐴 + 3))) |
383 | | lemul12b 10880 |
. . . . . . . . . . . . 13
⊢
((((((𝑢 −
𝑁) / 𝑁) ∈ ℝ ∧ 0 ≤ ((𝑢 − 𝑁) / 𝑁)) ∧ (𝐿 · 𝐸) ∈ ℝ) ∧ (((abs‘((𝑅‘𝑢) / 𝑢)) + 3) ∈ ℝ ∧ ((𝐴 + 3) ∈ ℝ ∧ 0
≤ (𝐴 + 3)))) →
((((𝑢 − 𝑁) / 𝑁) ≤ (𝐿 · 𝐸) ∧ ((abs‘((𝑅‘𝑢) / 𝑢)) + 3) ≤ (𝐴 + 3)) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) ≤ ((𝐿 · 𝐸) · (𝐴 + 3)))) |
384 | 376, 357,
106, 382, 383 | syl22anc 1327 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) ≤ (𝐿 · 𝐸) ∧ ((abs‘((𝑅‘𝑢) / 𝑢)) + 3) ≤ (𝐴 + 3)) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) ≤ ((𝐿 · 𝐸) · (𝐴 + 3)))) |
385 | 364, 375,
384 | mp2and 715 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) ≤ ((𝐿 · 𝐸) · (𝐴 + 3))) |
386 | 35 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐸 ∈
ℝ+) |
387 | 112, 113 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 4 ∈
ℝ+) |
388 | 386, 387 | rpdivcld 11889 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 4) ∈
ℝ+) |
389 | 388 | rpcnd 11874 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 4) ∈ ℂ) |
390 | 381 | rpcnd 11874 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐴 + 3) ∈ ℂ) |
391 | 381 | rpne0d 11877 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐴 + 3) ≠ 0) |
392 | 389, 390,
391 | divcan1d 10802 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝐸 / 4) / (𝐴 + 3)) · (𝐴 + 3)) = (𝐸 / 4)) |
393 | 14 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐸 ∈ ℂ) |
394 | 393 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 𝐸 ∈ ℂ) |
395 | 387 | rpcnd 11874 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 4 ∈
ℂ) |
396 | 387 | rpne0d 11877 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 4 ≠ 0) |
397 | 394, 395,
396 | divrec2d 10805 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 4) = ((1 / 4) · 𝐸)) |
398 | 397 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 4) / (𝐴 + 3)) = (((1 / 4) · 𝐸) / (𝐴 + 3))) |
399 | | 4cn 11098 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℂ |
400 | | 4ne0 11117 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ≠
0 |
401 | 399, 400 | reccli 10755 |
. . . . . . . . . . . . . . . . 17
⊢ (1 / 4)
∈ ℂ |
402 | 401 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (1 / 4) ∈
ℂ) |
403 | 402, 394,
390, 391 | div23d 10838 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((1 / 4) · 𝐸) / (𝐴 + 3)) = (((1 / 4) / (𝐴 + 3)) · 𝐸)) |
404 | 10 | oveq1i 6660 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 · 𝐸) = (((1 / 4) / (𝐴 + 3)) · 𝐸) |
405 | 403, 404 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((1 / 4) · 𝐸) / (𝐴 + 3)) = (𝐿 · 𝐸)) |
406 | 398, 405 | eqtr2d 2657 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐿 · 𝐸) = ((𝐸 / 4) / (𝐴 + 3))) |
407 | 406 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐿 · 𝐸) · (𝐴 + 3)) = (((𝐸 / 4) / (𝐴 + 3)) · (𝐴 + 3))) |
408 | | 2ne0 11113 |
. . . . . . . . . . . . . . 15
⊢ 2 ≠
0 |
409 | 408 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → 2 ≠ 0) |
410 | 394, 318,
318, 409, 409 | divdiv1d 10832 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) / 2) = (𝐸 / (2 · 2))) |
411 | | 2t2e4 11177 |
. . . . . . . . . . . . . 14
⊢ (2
· 2) = 4 |
412 | 411 | oveq2i 6661 |
. . . . . . . . . . . . 13
⊢ (𝐸 / (2 · 2)) = (𝐸 / 4) |
413 | 410, 412 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) / 2) = (𝐸 / 4)) |
414 | 392, 407,
413 | 3eqtr4d 2666 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐿 · 𝐸) · (𝐴 + 3)) = ((𝐸 / 2) / 2)) |
415 | 385, 414 | breqtrd 4679 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) ≤ ((𝐸 / 2) / 2)) |
416 | 117 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (𝐸 / 4)) ∈ ℝ) |
417 | 137 | rpred 11872 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (log‘𝑁) ∈ ℝ) |
418 | 78 | reeflogd 24370 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(log‘𝑁)) = 𝑁) |
419 | 135, 418 | breqtrrd 4681 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (exp‘(𝑇 / (𝐸 / 4))) < (exp‘(log‘𝑁))) |
420 | | eflt 14847 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 / (𝐸 / 4)) ∈ ℝ ∧ (log‘𝑁) ∈ ℝ) → ((𝑇 / (𝐸 / 4)) < (log‘𝑁) ↔ (exp‘(𝑇 / (𝐸 / 4))) < (exp‘(log‘𝑁)))) |
421 | 416, 417,
420 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝑇 / (𝐸 / 4)) < (log‘𝑁) ↔ (exp‘(𝑇 / (𝐸 / 4))) < (exp‘(log‘𝑁)))) |
422 | 419, 421 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (𝐸 / 4)) < (log‘𝑁)) |
423 | 416, 417,
422 | ltled 10185 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (𝐸 / 4)) ≤ (log‘𝑁)) |
424 | 110, 388,
137, 423 | lediv23d 11938 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ≤ (𝐸 / 4)) |
425 | 424, 413 | breqtrrd 4681 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑇 / (log‘𝑁)) ≤ ((𝐸 / 2) / 2)) |
426 | 107, 138,
353, 353, 415, 425 | le2addd 10646 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))) ≤ (((𝐸 / 2) / 2) + ((𝐸 / 2) / 2))) |
427 | 100 | recnd 10068 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝐸 / 2) ∈ ℂ) |
428 | 427 | 2halvesd 11278 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (((𝐸 / 2) / 2) + ((𝐸 / 2) / 2)) = (𝐸 / 2)) |
429 | 426, 428 | breqtrd 4679 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((((𝑢 − 𝑁) / 𝑁) · ((abs‘((𝑅‘𝑢) / 𝑢)) + 3)) + (𝑇 / (log‘𝑁))) ≤ (𝐸 / 2)) |
430 | 93, 139, 100, 352, 429 | letrd 10194 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) ≤ (𝐸 / 2)) |
431 | 3 | simprd 479 |
. . . . . . . 8
⊢ (𝜑 → (abs‘((𝑅‘𝑁) / 𝑁)) ≤ (𝐸 / 2)) |
432 | 431 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑁) / 𝑁)) ≤ (𝐸 / 2)) |
433 | 93, 94, 100, 100, 430, 432 | le2addd 10646 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) + (abs‘((𝑅‘𝑁) / 𝑁))) ≤ ((𝐸 / 2) + (𝐸 / 2))) |
434 | 394 | 2halvesd 11278 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸) |
435 | 433, 434 | breqtrd 4679 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → ((abs‘(((𝑅‘𝑢) / 𝑢) − ((𝑅‘𝑁) / 𝑁))) + (abs‘((𝑅‘𝑁) / 𝑁))) ≤ 𝐸) |
436 | 86, 95, 96, 99, 435 | letrd 10194 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) |
437 | 436 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) |
438 | 5, 73, 437 | jca31 557 |
. 2
⊢ (𝜑 → ((𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
439 | | breq2 4657 |
. . . . 5
⊢ (𝑧 = 𝑁 → (𝑌 < 𝑧 ↔ 𝑌 < 𝑁)) |
440 | | oveq2 6658 |
. . . . . 6
⊢ (𝑧 = 𝑁 → ((1 + (𝐿 · 𝐸)) · 𝑧) = ((1 + (𝐿 · 𝐸)) · 𝑁)) |
441 | 440 | breq1d 4663 |
. . . . 5
⊢ (𝑧 = 𝑁 → (((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌) ↔ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌))) |
442 | 439, 441 | anbi12d 747 |
. . . 4
⊢ (𝑧 = 𝑁 → ((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ↔ (𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)))) |
443 | | id 22 |
. . . . . 6
⊢ (𝑧 = 𝑁 → 𝑧 = 𝑁) |
444 | 443, 440 | oveq12d 6668 |
. . . . 5
⊢ (𝑧 = 𝑁 → (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧)) = (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) |
445 | 444 | raleqdv 3144 |
. . . 4
⊢ (𝑧 = 𝑁 → (∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸 ↔ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
446 | 442, 445 | anbi12d 747 |
. . 3
⊢ (𝑧 = 𝑁 → (((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ↔ ((𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) |
447 | 446 | rspcev 3309 |
. 2
⊢ ((𝑁 ∈ ℝ+
∧ ((𝑌 < 𝑁 ∧ ((1 + (𝐿 · 𝐸)) · 𝑁) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) → ∃𝑧 ∈ ℝ+ ((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
448 | 2, 438, 447 | syl2anc 693 |
1
⊢ (𝜑 → ∃𝑧 ∈ ℝ+ ((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |