Step | Hyp | Ref
| Expression |
1 | | nnuz 12477 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 12208 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ) |
4 | | rpvmasum.g |
. . . . . . . . . 10
⊢ 𝐺 = (DChr‘𝑁) |
5 | | rpvmasum.z |
. . . . . . . . . 10
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
6 | | rpvmasum.d |
. . . . . . . . . 10
⊢ 𝐷 = (Base‘𝐺) |
7 | | rpvmasum.l |
. . . . . . . . . 10
⊢ 𝐿 = (ℤRHom‘𝑍) |
8 | | dchrisum.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
9 | 8 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑋 ∈ 𝐷) |
10 | 3 | nnzd 12281 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℤ) |
11 | 4, 5, 6, 7, 9, 10 | dchrzrhcl 26126 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑋‘(𝐿‘𝑖)) ∈ ℂ) |
12 | | dchrisum.4 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈
ℝ) |
13 | 12 | ralrimiva 3105 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ) |
14 | | nnrp 12597 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ → 𝑖 ∈
ℝ+) |
15 | | nfcsb1v 3836 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴 |
16 | 15 | nfel1 2920 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ |
17 | | csbeq1a 3825 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑖 → 𝐴 = ⦋𝑖 / 𝑛⦌𝐴) |
18 | 17 | eleq1d 2822 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑖 → (𝐴 ∈ ℝ ↔ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ)) |
19 | 16, 18 | rspc 3525 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℝ+
→ (∀𝑛 ∈
ℝ+ 𝐴
∈ ℝ → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ)) |
20 | 19 | impcom 411 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ℝ+ 𝐴
∈ ℝ ∧ 𝑖
∈ ℝ+) → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ) |
21 | 13, 14, 20 | syl2an 599 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ) |
22 | 21 | recnd 10861 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℂ) |
23 | 11, 22 | mulcld 10853 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ) |
24 | | nfcv 2904 |
. . . . . . . . 9
⊢
Ⅎ𝑛𝑖 |
25 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝑋‘(𝐿‘𝑖)) |
26 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑛
· |
27 | 25, 26, 15 | nfov 7243 |
. . . . . . . . 9
⊢
Ⅎ𝑛((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) |
28 | | 2fveq3 6722 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑖 → (𝑋‘(𝐿‘𝑛)) = (𝑋‘(𝐿‘𝑖))) |
29 | 28, 17 | oveq12d 7231 |
. . . . . . . . 9
⊢ (𝑛 = 𝑖 → ((𝑋‘(𝐿‘𝑛)) · 𝐴) = ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) |
30 | | dchrisum.7 |
. . . . . . . . 9
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) |
31 | 24, 27, 29, 30 | fvmptf 6839 |
. . . . . . . 8
⊢ ((𝑖 ∈ ℕ ∧ ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ) → (𝐹‘𝑖) = ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) |
32 | 3, 23, 31 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) = ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) |
33 | 32, 23 | eqeltrd 2838 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ ℂ) |
34 | 1, 2, 33 | serf 13604 |
. . . . 5
⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ) |
35 | 34 | ffvelrnda 6904 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℂ) |
36 | 12 | recnd 10861 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈
ℂ) |
37 | 36 | ralrimiva 3105 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℂ) |
38 | 37 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∀𝑛 ∈
ℝ+ 𝐴
∈ ℂ) |
39 | | id 22 |
. . . . . . . 8
⊢ (𝑒 ∈ ℝ+
→ 𝑒 ∈
ℝ+) |
40 | | 2re 11904 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
41 | | dchrisum.9 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ ℝ) |
42 | | remulcl 10814 |
. . . . . . . . . 10
⊢ ((2
∈ ℝ ∧ 𝑅
∈ ℝ) → (2 · 𝑅) ∈ ℝ) |
43 | 40, 41, 42 | sylancr 590 |
. . . . . . . . 9
⊢ (𝜑 → (2 · 𝑅) ∈
ℝ) |
44 | | rpvmasum.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
45 | | lbfzo0 13282 |
. . . . . . . . . . . 12
⊢ (0 ∈
(0..^𝑁) ↔ 𝑁 ∈
ℕ) |
46 | 44, 45 | sylibr 237 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈ (0..^𝑁)) |
47 | | dchrisum.10 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |
48 | | oveq2 7221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 0 → (0..^𝑢) = (0..^0)) |
49 | | fzo0 13266 |
. . . . . . . . . . . . . . . . 17
⊢ (0..^0) =
∅ |
50 | 48, 49 | eqtrdi 2794 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 0 → (0..^𝑢) = ∅) |
51 | 50 | sumeq1d 15265 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 0 → Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ ∅ (𝑋‘(𝐿‘𝑛))) |
52 | | sum0 15285 |
. . . . . . . . . . . . . . 15
⊢
Σ𝑛 ∈
∅ (𝑋‘(𝐿‘𝑛)) = 0 |
53 | 51, 52 | eqtrdi 2794 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 0 → Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛)) = 0) |
54 | 53 | abs00bd 14855 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 0 →
(abs‘Σ𝑛 ∈
(0..^𝑢)(𝑋‘(𝐿‘𝑛))) = 0) |
55 | 54 | breq1d 5063 |
. . . . . . . . . . . 12
⊢ (𝑢 = 0 →
((abs‘Σ𝑛 ∈
(0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅 ↔ 0 ≤ 𝑅)) |
56 | 55 | rspcv 3532 |
. . . . . . . . . . 11
⊢ (0 ∈
(0..^𝑁) →
(∀𝑢 ∈
(0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅 → 0 ≤ 𝑅)) |
57 | 46, 47, 56 | sylc 65 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 𝑅) |
58 | | 0le2 11932 |
. . . . . . . . . . 11
⊢ 0 ≤
2 |
59 | | mulge0 11350 |
. . . . . . . . . . 11
⊢ (((2
∈ ℝ ∧ 0 ≤ 2) ∧ (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅)) → 0 ≤ (2 ·
𝑅)) |
60 | 40, 58, 59 | mpanl12 702 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → 0 ≤ (2
· 𝑅)) |
61 | 41, 57, 60 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (2 · 𝑅)) |
62 | 43, 61 | ge0p1rpd 12658 |
. . . . . . . 8
⊢ (𝜑 → ((2 · 𝑅) + 1) ∈
ℝ+) |
63 | | rpdivcl 12611 |
. . . . . . . 8
⊢ ((𝑒 ∈ ℝ+
∧ ((2 · 𝑅) + 1)
∈ ℝ+) → (𝑒 / ((2 · 𝑅) + 1)) ∈
ℝ+) |
64 | 39, 62, 63 | syl2anr 600 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (𝑒 / ((2 · 𝑅) + 1)) ∈
ℝ+) |
65 | | dchrisum.6 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟
0) |
66 | 65 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (𝑛 ∈ ℝ+
↦ 𝐴)
⇝𝑟 0) |
67 | 38, 64, 66 | rlimi 15074 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑚 ∈ ℝ
∀𝑛 ∈
ℝ+ (𝑚 ≤
𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)))) |
68 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 𝑚 ∈ ℝ) |
69 | | dchrisum.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ ℕ) |
70 | 69 | nnred 11845 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℝ) |
71 | 70 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 𝑀 ∈ ℝ) |
72 | 68, 71 | ifcld 4485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ) |
73 | | 0red 10836 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 0 ∈
ℝ) |
74 | 69 | nngt0d 11879 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < 𝑀) |
75 | 74 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 0 < 𝑀) |
76 | | max1 12775 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) |
77 | 70, 76 | sylan 583 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) |
78 | 73, 71, 72, 75, 77 | ltletrd 10992 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 0 < if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) |
79 | 72, 78 | elrpd 12625 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈
ℝ+) |
80 | 79 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈
ℝ+) |
81 | | nfv 1922 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛 𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀) |
82 | | nfcv 2904 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛abs |
83 | | nfcsb1v 3836 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 |
84 | | nfcv 2904 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛
− |
85 | | nfcv 2904 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛0 |
86 | 83, 84, 85 | nfov 7243 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0) |
87 | 82, 86 | nffv 6727 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) |
88 | | nfcv 2904 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛
< |
89 | | nfcv 2904 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(𝑒 / ((2 · 𝑅) + 1)) |
90 | 87, 88, 89 | nfbr 5100 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛(abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) |
91 | 81, 90 | nfim 1904 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → (abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) |
92 | | breq2 5057 |
. . . . . . . . . . 11
⊢ (𝑛 = if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → (𝑚 ≤ 𝑛 ↔ 𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀))) |
93 | | csbeq1a 3825 |
. . . . . . . . . . . . 13
⊢ (𝑛 = if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → 𝐴 = ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) |
94 | 93 | fvoveq1d 7235 |
. . . . . . . . . . . 12
⊢ (𝑛 = if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → (abs‘(𝐴 − 0)) =
(abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0))) |
95 | 94 | breq1d 5063 |
. . . . . . . . . . 11
⊢ (𝑛 = if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → ((abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) ↔
(abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)))) |
96 | 92, 95 | imbi12d 348 |
. . . . . . . . . 10
⊢ (𝑛 = if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → ((𝑚 ≤ 𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) ↔ (𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → (abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))))) |
97 | 91, 96 | rspc 3525 |
. . . . . . . . 9
⊢ (if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ+ →
(∀𝑛 ∈
ℝ+ (𝑚 ≤
𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) → (𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → (abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))))) |
98 | 80, 97 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(∀𝑛 ∈
ℝ+ (𝑚 ≤
𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) → (𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → (abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))))) |
99 | 70 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑀 ∈
ℝ) |
100 | | max2 12777 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) |
101 | 99, 100 | sylancom 591 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) |
102 | 13 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
∀𝑛 ∈
ℝ+ 𝐴
∈ ℝ) |
103 | 83 | nfel1 2920 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑛⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 ∈ ℝ |
104 | 93 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → (𝐴 ∈ ℝ ↔
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 ∈ ℝ)) |
105 | 103, 104 | rspc 3525 |
. . . . . . . . . . . . . . . . . 18
⊢ (if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ+ →
(∀𝑛 ∈
ℝ+ 𝐴
∈ ℝ → ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 ∈ ℝ)) |
106 | 80, 102, 105 | sylc 65 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 ∈ ℝ) |
107 | 106 | recnd 10861 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 ∈ ℂ) |
108 | 107 | subid1d 11178 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0) = ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) |
109 | 108 | fveq2d 6721 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) =
(abs‘⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴)) |
110 | 72 | adantlr 715 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ) |
111 | 99, 76 | sylancom 591 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) |
112 | | elicopnf 13033 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℝ → (if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) ↔ (if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ ∧ 𝑀 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) |
113 | 99, 112 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) ↔ (if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ ∧ 𝑀 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) |
114 | 110, 111,
113 | mpbir2and 713 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞)) |
115 | 44 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑁 ∈
ℕ) |
116 | | rpvmasum.1 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 =
(0g‘𝐺) |
117 | 8 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑋 ∈ 𝐷) |
118 | | dchrisum.n1 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑋 ≠ 1 ) |
119 | 118 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑋 ≠ 1 ) |
120 | | dchrisum.2 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) |
121 | 69 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑀 ∈
ℕ) |
122 | 12 | ad4ant14 752 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑛 ∈ ℝ+)
→ 𝐴 ∈
ℝ) |
123 | | simpll 767 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝜑) |
124 | | dchrisum.5 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) |
125 | 123, 124 | syl3an1 1165 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ (𝑛 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) |
126 | 65 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (𝑛 ∈ ℝ+
↦ 𝐴)
⇝𝑟 0) |
127 | 5, 7, 115, 4, 6, 116, 117, 119, 120, 121, 122, 125, 126, 30 | dchrisumlema 26369 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
((if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ+ →
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 ∈ ℝ) ∧ (if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) → 0 ≤
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴))) |
128 | 127 | simprd 499 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) → 0 ≤
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴)) |
129 | 114, 128 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 0 ≤
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) |
130 | 106, 129 | absidd 14986 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(abs‘⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) = ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) |
131 | 109, 130 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) = ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) |
132 | 131 | breq1d 5063 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
((abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) ↔ ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 < (𝑒 / ((2 · 𝑅) + 1)))) |
133 | | rpre 12594 |
. . . . . . . . . . . . . 14
⊢ (𝑒 ∈ ℝ+
→ 𝑒 ∈
ℝ) |
134 | 133 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑒 ∈
ℝ) |
135 | 62 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2
· 𝑅) + 1) ∈
ℝ+) |
136 | 106, 134,
135 | ltmuldiv2d 12676 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((((2
· 𝑅) + 1) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒 ↔ ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 < (𝑒 / ((2 · 𝑅) + 1)))) |
137 | 132, 136 | bitr4d 285 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
((abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) ↔ (((2 · 𝑅) + 1) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒)) |
138 | 43 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (2
· 𝑅) ∈
ℝ) |
139 | 135 | rpred 12628 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2
· 𝑅) + 1) ∈
ℝ) |
140 | 138 | lep1d 11763 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (2
· 𝑅) ≤ ((2
· 𝑅) +
1)) |
141 | 138, 139,
106, 129, 140 | lemul1ad 11771 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2
· 𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ≤ (((2 · 𝑅) + 1) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴)) |
142 | 138, 106 | remulcld 10863 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2
· 𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∈ ℝ) |
143 | 139, 106 | remulcld 10863 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (((2
· 𝑅) + 1) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∈ ℝ) |
144 | | lelttr 10923 |
. . . . . . . . . . . . 13
⊢ ((((2
· 𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∈ ℝ ∧ (((2 · 𝑅) + 1) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) → ((((2 · 𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ≤ (((2 · 𝑅) + 1) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∧ (((2 · 𝑅) + 1) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒) → ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒)) |
145 | 142, 143,
134, 144 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((((2
· 𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ≤ (((2 · 𝑅) + 1) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∧ (((2 · 𝑅) + 1) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒) → ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒)) |
146 | 141, 145 | mpand 695 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((((2
· 𝑅) + 1) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒 → ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒)) |
147 | 137, 146 | sylbid 243 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
((abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) → ((2 · 𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒)) |
148 | | 1red 10834 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 1 ∈
ℝ) |
149 | 69 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 𝑀 ∈ ℕ) |
150 | 149 | nnge1d 11878 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 1 ≤ 𝑀) |
151 | 148, 71, 72, 150, 77 | letrd 10989 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 1 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) |
152 | | flge1nn 13396 |
. . . . . . . . . . . . 13
⊢
((if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ ∧ 1 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) → (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) ∈ ℕ) |
153 | 72, 151, 152 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) →
(⌊‘if(𝑀 ≤
𝑚, 𝑚, 𝑀)) ∈ ℕ) |
154 | 153 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(⌊‘if(𝑀 ≤
𝑚, 𝑚, 𝑀)) ∈ ℕ) |
155 | 44 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑁 ∈ ℕ) |
156 | 8 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑋 ∈ 𝐷) |
157 | 118 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑋 ≠ 1 ) |
158 | 69 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑀 ∈ ℕ) |
159 | 12 | ad4ant14 752 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈
ℝ) |
160 | 124 | 3adant1r 1179 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) |
161 | 160 | 3adant1r 1179 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) |
162 | 65 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟
0) |
163 | 41 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑅 ∈ ℝ) |
164 | 47 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |
165 | 79 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈
ℝ+) |
166 | 77 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑀 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) |
167 | 72 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ) |
168 | | fllep1 13376 |
. . . . . . . . . . . . . . . 16
⊢ (if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ≤ ((⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) + 1)) |
169 | 167, 168 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ≤ ((⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) + 1)) |
170 | 153 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) ∈ ℕ) |
171 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) |
172 | 5, 7, 155, 4, 6, 116, 156, 157, 120, 158, 159, 161, 162, 30, 163, 164, 165, 166, 169, 170, 171 | dchrisumlem2 26371 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴)) |
173 | 172 | adantllr 719 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴)) |
174 | 34 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → seq1( + , 𝐹):ℕ⟶ℂ) |
175 | | eluznn 12514 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑘 ∈ ℕ) |
176 | 154, 175 | sylan 583 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑘 ∈ ℕ) |
177 | 174, 176 | ffvelrnd 6905 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (seq1( + , 𝐹)‘𝑘) ∈ ℂ) |
178 | 154 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) ∈ ℕ) |
179 | 174, 178 | ffvelrnd 6905 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))) ∈ ℂ) |
180 | 177, 179 | subcld 11189 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → ((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) ∈ ℂ) |
181 | 180 | abscld 15000 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) ∈ ℝ) |
182 | 142 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∈ ℝ) |
183 | 134 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑒 ∈ ℝ) |
184 | | lelttr 10923 |
. . . . . . . . . . . . . 14
⊢
(((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) ∈ ℝ ∧ ((2 ·
𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) → (((abs‘((seq1(
+ , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∧ ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) < 𝑒)) |
185 | 181, 182,
183, 184 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∧ ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) < 𝑒)) |
186 | 173, 185 | mpand 695 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒 → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) < 𝑒)) |
187 | 186 | ralrimdva 3110 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (((2
· 𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒 → ∀𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) < 𝑒)) |
188 | | fveq2 6717 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) →
(ℤ≥‘𝑗) =
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) |
189 | | fveq2 6717 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) → (seq1( + , 𝐹)‘𝑗) = (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) |
190 | 189 | oveq2d 7229 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) → ((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗)) = ((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) |
191 | 190 | fveq2d 6721 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) = (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))))) |
192 | 191 | breq1d 5063 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) → ((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒 ↔ (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) < 𝑒)) |
193 | 188, 192 | raleqbidv 3313 |
. . . . . . . . . . . 12
⊢ (𝑗 = (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒 ↔ ∀𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) < 𝑒)) |
194 | 193 | rspcev 3537 |
. . . . . . . . . . 11
⊢
(((⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) < 𝑒) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒) |
195 | 154, 187,
194 | syl6an 684 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (((2
· 𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)) |
196 | 147, 195 | syld 47 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
((abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)) |
197 | 101, 196 | embantd 59 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → (abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)) |
198 | 98, 197 | syld 47 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(∀𝑛 ∈
ℝ+ (𝑚 ≤
𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) → ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)) |
199 | 198 | rexlimdva 3203 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
(∃𝑚 ∈ ℝ
∀𝑛 ∈
ℝ+ (𝑚 ≤
𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) → ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)) |
200 | 67, 199 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒) |
201 | 200 | ralrimiva 3105 |
. . . 4
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒) |
202 | | seqex 13576 |
. . . . 5
⊢ seq1( + ,
𝐹) ∈
V |
203 | 202 | a1i 11 |
. . . 4
⊢ (𝜑 → seq1( + , 𝐹) ∈ V) |
204 | 1, 35, 201, 203 | caucvg 15242 |
. . 3
⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝
) |
205 | 202 | eldm 5769 |
. . 3
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
↔ ∃𝑡seq1( + ,
𝐹) ⇝ 𝑡) |
206 | 204, 205 | sylib 221 |
. 2
⊢ (𝜑 → ∃𝑡seq1( + , 𝐹) ⇝ 𝑡) |
207 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → seq1( + , 𝐹) ⇝ 𝑡) |
208 | | elrege0 13042 |
. . . . . . . 8
⊢ ((2
· 𝑅) ∈
(0[,)+∞) ↔ ((2 · 𝑅) ∈ ℝ ∧ 0 ≤ (2 ·
𝑅))) |
209 | 43, 61, 208 | sylanbrc 586 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝑅) ∈
(0[,)+∞)) |
210 | 209 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → (2 · 𝑅) ∈ (0[,)+∞)) |
211 | | eqid 2737 |
. . . . . . . 8
⊢
(ℤ≥‘(⌊‘𝑚)) =
(ℤ≥‘(⌊‘𝑚)) |
212 | | pnfxr 10887 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
213 | | icossre 13016 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝑀[,)+∞) ⊆
ℝ) |
214 | 70, 212, 213 | sylancl 589 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀[,)+∞) ⊆
ℝ) |
215 | 214 | sselda 3901 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ) |
216 | 215 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ) |
217 | 216 | flcld 13373 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (⌊‘𝑚) ∈
ℤ) |
218 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → seq1( + , 𝐹) ⇝ 𝑡) |
219 | 34 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → seq1( + , 𝐹):ℕ⟶ℂ) |
220 | | 1red 10834 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 1 ∈
ℝ) |
221 | 70 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℝ) |
222 | 69 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℕ) |
223 | 222 | nnge1d 11878 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 1 ≤ 𝑀) |
224 | | elicopnf 13033 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℝ → (𝑚 ∈ (𝑀[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 𝑀 ≤ 𝑚))) |
225 | 70, 224 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑚 ∈ (𝑀[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 𝑀 ≤ 𝑚))) |
226 | 225 | simplbda 503 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ≤ 𝑚) |
227 | 226 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ≤ 𝑚) |
228 | 220, 221,
216, 223, 227 | letrd 10989 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 1 ≤ 𝑚) |
229 | | flge1nn 13396 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℝ ∧ 1 ≤
𝑚) →
(⌊‘𝑚) ∈
ℕ) |
230 | 216, 228,
229 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (⌊‘𝑚) ∈
ℕ) |
231 | 219, 230 | ffvelrnd 6905 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈
ℂ) |
232 | | nnex 11836 |
. . . . . . . . . . . 12
⊢ ℕ
∈ V |
233 | 232 | mptex 7039 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ ↦ ((seq1(
+ , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ∈ V |
234 | 233 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ∈ V) |
235 | 219 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → seq1( + , 𝐹):ℕ⟶ℂ) |
236 | | eluznn 12514 |
. . . . . . . . . . . 12
⊢
(((⌊‘𝑚)
∈ ℕ ∧ 𝑖
∈ (ℤ≥‘(⌊‘𝑚))) → 𝑖 ∈ ℕ) |
237 | 230, 236 | sylan 583 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑖 ∈ ℕ) |
238 | 235, 237 | ffvelrnd 6905 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (seq1( + , 𝐹)‘𝑖) ∈ ℂ) |
239 | | fveq2 6717 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → (seq1( + , 𝐹)‘𝑘) = (seq1( + , 𝐹)‘𝑖)) |
240 | 239 | oveq2d 7229 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) |
241 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ ↦ ((seq1(
+ , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) = (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) |
242 | | ovex 7246 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)) ∈ V |
243 | 240, 241,
242 | fvmpt3i 6823 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((seq1(
+ , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) |
244 | 237, 243 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) |
245 | 211, 217,
218, 231, 234, 238, 244 | climsubc2 15200 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ⇝ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) |
246 | 232 | mptex 7039 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ ↦
(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) ∈ V |
247 | 246 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ (abs‘((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) ∈ V) |
248 | | fvex 6730 |
. . . . . . . . . . . . . 14
⊢ (seq1( +
, 𝐹)‘(⌊‘𝑚)) ∈ V |
249 | 248 | fvconst2 7019 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℕ → ((ℕ
× {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) = (seq1( + , 𝐹)‘(⌊‘𝑚))) |
250 | 237, 249 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((ℕ × {(seq1( + ,
𝐹)‘(⌊‘𝑚))})‘𝑖) = (seq1( + , 𝐹)‘(⌊‘𝑚))) |
251 | 250 | oveq1d 7228 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (((ℕ × {(seq1( + ,
𝐹)‘(⌊‘𝑚))})‘𝑖) − (seq1( + , 𝐹)‘𝑖)) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) |
252 | 244, 251 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) = (((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) − (seq1( + , 𝐹)‘𝑖))) |
253 | 231 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈ ℂ) |
254 | 250, 253 | eqeltrd 2838 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((ℕ × {(seq1( + ,
𝐹)‘(⌊‘𝑚))})‘𝑖) ∈ ℂ) |
255 | 254, 238 | subcld 11189 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (((ℕ × {(seq1( + ,
𝐹)‘(⌊‘𝑚))})‘𝑖) − (seq1( + , 𝐹)‘𝑖)) ∈ ℂ) |
256 | 252, 255 | eqeltrd 2838 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) ∈ ℂ) |
257 | 240 | fveq2d 6721 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))) |
258 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ ↦
(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) = (𝑘 ∈ ℕ ↦ (abs‘((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) |
259 | | fvex 6730 |
. . . . . . . . . . . 12
⊢
(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ∈ V |
260 | 257, 258,
259 | fvmpt3i 6823 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦
(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))) |
261 | 237, 260 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))) |
262 | 244 | fveq2d 6721 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (abs‘((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))) |
263 | 261, 262 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖))) |
264 | 211, 245,
247, 217, 256, 263 | climabs 15165 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ (abs‘((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) ⇝ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡))) |
265 | 43 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (2 · 𝑅) ∈
ℝ) |
266 | | 0red 10836 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀[,)+∞)) → 0 ∈
ℝ) |
267 | 70 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℝ) |
268 | 74 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀[,)+∞)) → 0 < 𝑀) |
269 | 266, 267,
215, 268, 226 | ltletrd 10992 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀[,)+∞)) → 0 < 𝑚) |
270 | 215, 269 | elrpd 12625 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ+) |
271 | | nfcsb1v 3836 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 |
272 | 271 | nfel1 2920 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 ∈ ℝ |
273 | | csbeq1a 3825 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
274 | 273 | eleq1d 2822 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝐴 ∈ ℝ ↔ ⦋𝑚 / 𝑛⦌𝐴 ∈ ℝ)) |
275 | 272, 274 | rspc 3525 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℝ+
→ (∀𝑛 ∈
ℝ+ 𝐴
∈ ℝ → ⦋𝑚 / 𝑛⦌𝐴 ∈ ℝ)) |
276 | 13, 275 | mpan9 510 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
⦋𝑚 / 𝑛⦌𝐴 ∈ ℝ) |
277 | 270, 276 | syldan 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀[,)+∞)) → ⦋𝑚 / 𝑛⦌𝐴 ∈ ℝ) |
278 | 277 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → ⦋𝑚 / 𝑛⦌𝐴 ∈ ℝ) |
279 | 265, 278 | remulcld 10863 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
280 | 279 | recnd 10861 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴) ∈ ℂ) |
281 | | 1z 12207 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
282 | 1 | eqimss2i 3960 |
. . . . . . . . . 10
⊢
(ℤ≥‘1) ⊆ ℕ |
283 | 282, 232 | climconst2 15109 |
. . . . . . . . 9
⊢ ((((2
· 𝑅) ·
⦋𝑚 / 𝑛⦌𝐴) ∈ ℂ ∧ 1 ∈ ℤ)
→ (ℕ × {((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)}) ⇝ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)) |
284 | 280, 281,
283 | sylancl 589 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (ℕ × {((2
· 𝑅) ·
⦋𝑚 / 𝑛⦌𝐴)}) ⇝ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)) |
285 | 253, 238 | subcld 11189 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)) ∈ ℂ) |
286 | 285 | abscld 15000 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) ∈ ℝ) |
287 | 261, 286 | eqeltrd 2838 |
. . . . . . . 8
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) ∈ ℝ) |
288 | | ovex 7246 |
. . . . . . . . . . 11
⊢ ((2
· 𝑅) ·
⦋𝑚 / 𝑛⦌𝐴) ∈ V |
289 | 288 | fvconst2 7019 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ℕ → ((ℕ
× {((2 · 𝑅)
· ⦋𝑚 /
𝑛⦌𝐴)})‘𝑖) = ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)) |
290 | 237, 289 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((ℕ × {((2 ·
𝑅) ·
⦋𝑚 / 𝑛⦌𝐴)})‘𝑖) = ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)) |
291 | 279 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
292 | 290, 291 | eqeltrd 2838 |
. . . . . . . 8
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((ℕ × {((2 ·
𝑅) ·
⦋𝑚 / 𝑛⦌𝐴)})‘𝑖) ∈ ℝ) |
293 | | simplll 775 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝜑) |
294 | 293, 44 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑁 ∈ ℕ) |
295 | 293, 8 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑋 ∈ 𝐷) |
296 | 293, 118 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑋 ≠ 1 ) |
297 | 222 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑀 ∈ ℕ) |
298 | 293, 12 | sylan 583 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ seq1( + ,
𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈
ℝ) |
299 | 293, 124 | syl3an1 1165 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ seq1( + ,
𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) |
300 | 293, 65 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟
0) |
301 | 293, 41 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑅 ∈ ℝ) |
302 | 293, 47 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |
303 | 270 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ+) |
304 | 303 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑚 ∈ ℝ+) |
305 | 227 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑀 ≤ 𝑚) |
306 | 216 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑚 ∈ ℝ) |
307 | | reflcl 13371 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℝ →
(⌊‘𝑚) ∈
ℝ) |
308 | | peano2re 11005 |
. . . . . . . . . . . 12
⊢
((⌊‘𝑚)
∈ ℝ → ((⌊‘𝑚) + 1) ∈ ℝ) |
309 | 306, 307,
308 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((⌊‘𝑚) + 1) ∈ ℝ) |
310 | | flltp1 13375 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℝ → 𝑚 < ((⌊‘𝑚) + 1)) |
311 | 306, 310 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑚 < ((⌊‘𝑚) + 1)) |
312 | 306, 309,
311 | ltled 10980 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑚 ≤ ((⌊‘𝑚) + 1)) |
313 | 230 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (⌊‘𝑚) ∈ ℕ) |
314 | | simpr 488 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) |
315 | 5, 7, 294, 4, 6, 116, 295, 296, 120, 297, 298, 299, 300, 30, 301, 302, 304, 305, 312, 313, 314 | dchrisumlem2 26371 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (abs‘((seq1( + , 𝐹)‘𝑖) − (seq1( + , 𝐹)‘(⌊‘𝑚)))) ≤ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)) |
316 | 253, 238 | abssubd 15017 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) = (abs‘((seq1( + , 𝐹)‘𝑖) − (seq1( + , 𝐹)‘(⌊‘𝑚))))) |
317 | 261, 316 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((seq1( + , 𝐹)‘𝑖) − (seq1( + , 𝐹)‘(⌊‘𝑚))))) |
318 | 315, 317,
290 | 3brtr4d 5085 |
. . . . . . . 8
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) ≤ ((ℕ × {((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)})‘𝑖)) |
319 | 211, 217,
264, 284, 287, 292, 318 | climle 15201 |
. . . . . . 7
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (abs‘((seq1( + ,
𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)) |
320 | 319 | ralrimiva 3105 |
. . . . . 6
⊢ ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → ∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)) |
321 | | oveq1 7220 |
. . . . . . . . . 10
⊢ (𝑐 = (2 · 𝑅) → (𝑐 · 𝐵) = ((2 · 𝑅) · 𝐵)) |
322 | 321 | breq2d 5065 |
. . . . . . . . 9
⊢ (𝑐 = (2 · 𝑅) → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵))) |
323 | 322 | ralbidv 3118 |
. . . . . . . 8
⊢ (𝑐 = (2 · 𝑅) → (∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵) ↔ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵))) |
324 | | 2fveq3 6722 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑥 → (seq1( + , 𝐹)‘(⌊‘𝑚)) = (seq1( + , 𝐹)‘(⌊‘𝑥))) |
325 | 324 | fvoveq1d 7235 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑥 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡))) |
326 | | vex 3412 |
. . . . . . . . . . . . 13
⊢ 𝑚 ∈ V |
327 | 326 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑥 → 𝑚 ∈ V) |
328 | | equequ2 2034 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑥 → (𝑛 = 𝑚 ↔ 𝑛 = 𝑥)) |
329 | 328 | biimpa 480 |
. . . . . . . . . . . . 13
⊢ ((𝑚 = 𝑥 ∧ 𝑛 = 𝑚) → 𝑛 = 𝑥) |
330 | 329, 120 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑚 = 𝑥 ∧ 𝑛 = 𝑚) → 𝐴 = 𝐵) |
331 | 327, 330 | csbied 3849 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑥 → ⦋𝑚 / 𝑛⦌𝐴 = 𝐵) |
332 | 331 | oveq2d 7229 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑥 → ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴) = ((2 · 𝑅) · 𝐵)) |
333 | 325, 332 | breq12d 5066 |
. . . . . . . . 9
⊢ (𝑚 = 𝑥 → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵))) |
334 | 333 | cbvralvw 3358 |
. . . . . . . 8
⊢
(∀𝑚 ∈
(𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴) ↔ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵)) |
335 | 323, 334 | bitr4di 292 |
. . . . . . 7
⊢ (𝑐 = (2 · 𝑅) → (∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵) ↔ ∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴))) |
336 | 335 | rspcev 3537 |
. . . . . 6
⊢ (((2
· 𝑅) ∈
(0[,)+∞) ∧ ∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)) → ∃𝑐 ∈ (0[,)+∞)∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)) |
337 | 210, 320,
336 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → ∃𝑐 ∈ (0[,)+∞)∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)) |
338 | | r19.42v 3263 |
. . . . 5
⊢
(∃𝑐 ∈
(0[,)+∞)(seq1( + , 𝐹)
⇝ 𝑡 ∧
∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( +
, 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)) ↔ (seq1( + , 𝐹) ⇝ 𝑡 ∧ ∃𝑐 ∈ (0[,)+∞)∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))) |
339 | 207, 337,
338 | sylanbrc 586 |
. . . 4
⊢ ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → ∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))) |
340 | 339 | ex 416 |
. . 3
⊢ (𝜑 → (seq1( + , 𝐹) ⇝ 𝑡 → ∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)))) |
341 | 340 | eximdv 1925 |
. 2
⊢ (𝜑 → (∃𝑡seq1( + , 𝐹) ⇝ 𝑡 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)))) |
342 | 206, 341 | mpd 15 |
1
⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))) |