Step | Hyp | Ref
| Expression |
1 | | nnuz 11723 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11408 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | simpr 477 |
. . . . . . . 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 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑋 ∈ 𝐷) |
10 | 3 | nnzd 11481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℤ) |
11 | 4, 5, 6, 7, 9, 10 | dchrzrhcl 24970 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑋‘(𝐿‘𝑖)) ∈ ℂ) |
12 | | dchrisum.4 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈
ℝ) |
13 | 12 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ) |
14 | | nnrp 11842 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ → 𝑖 ∈
ℝ+) |
15 | | nfcsb1v 3549 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴 |
16 | 15 | nfel1 2779 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ |
17 | | csbeq1a 3542 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑖 → 𝐴 = ⦋𝑖 / 𝑛⦌𝐴) |
18 | 17 | eleq1d 2686 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑖 → (𝐴 ∈ ℝ ↔ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ)) |
19 | 16, 18 | rspc 3303 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℝ+
→ (∀𝑛 ∈
ℝ+ 𝐴
∈ ℝ → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ)) |
20 | 19 | impcom 446 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ℝ+ 𝐴
∈ ℝ ∧ 𝑖
∈ ℝ+) → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ) |
21 | 13, 14, 20 | syl2an 494 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ) |
22 | 21 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℂ) |
23 | 11, 22 | mulcld 10060 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ) |
24 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑛𝑖 |
25 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝑋‘(𝐿‘𝑖)) |
26 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑛
· |
27 | 25, 26, 15 | nfov 6676 |
. . . . . . . . 9
⊢
Ⅎ𝑛((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) |
28 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑖 → (𝐿‘𝑛) = (𝐿‘𝑖)) |
29 | 28 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑖 → (𝑋‘(𝐿‘𝑛)) = (𝑋‘(𝐿‘𝑖))) |
30 | 29, 17 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑛 = 𝑖 → ((𝑋‘(𝐿‘𝑛)) · 𝐴) = ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) |
31 | | dchrisum.7 |
. . . . . . . . 9
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) |
32 | 24, 27, 30, 31 | fvmptf 6301 |
. . . . . . . 8
⊢ ((𝑖 ∈ ℕ ∧ ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ) → (𝐹‘𝑖) = ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) |
33 | 3, 23, 32 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) = ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) |
34 | 33, 23 | eqeltrd 2701 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ ℂ) |
35 | 1, 2, 34 | serf 12829 |
. . . . 5
⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ) |
36 | 35 | ffvelrnda 6359 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℂ) |
37 | 12 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈
ℂ) |
38 | 37 | ralrimiva 2966 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℂ) |
39 | 38 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∀𝑛 ∈
ℝ+ 𝐴
∈ ℂ) |
40 | | id 22 |
. . . . . . . 8
⊢ (𝑒 ∈ ℝ+
→ 𝑒 ∈
ℝ+) |
41 | | 2re 11090 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
42 | | dchrisum.9 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ ℝ) |
43 | | remulcl 10021 |
. . . . . . . . . 10
⊢ ((2
∈ ℝ ∧ 𝑅
∈ ℝ) → (2 · 𝑅) ∈ ℝ) |
44 | 41, 42, 43 | sylancr 695 |
. . . . . . . . 9
⊢ (𝜑 → (2 · 𝑅) ∈
ℝ) |
45 | | rpvmasum.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
46 | | lbfzo0 12507 |
. . . . . . . . . . . 12
⊢ (0 ∈
(0..^𝑁) ↔ 𝑁 ∈
ℕ) |
47 | 45, 46 | sylibr 224 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈ (0..^𝑁)) |
48 | | dchrisum.10 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |
49 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 0 → (0..^𝑢) = (0..^0)) |
50 | | fzo0 12492 |
. . . . . . . . . . . . . . . . 17
⊢ (0..^0) =
∅ |
51 | 49, 50 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 0 → (0..^𝑢) = ∅) |
52 | 51 | sumeq1d 14431 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 0 → Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ ∅ (𝑋‘(𝐿‘𝑛))) |
53 | | sum0 14452 |
. . . . . . . . . . . . . . 15
⊢
Σ𝑛 ∈
∅ (𝑋‘(𝐿‘𝑛)) = 0 |
54 | 52, 53 | syl6eq 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 0 → Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛)) = 0) |
55 | 54 | abs00bd 14031 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 0 →
(abs‘Σ𝑛 ∈
(0..^𝑢)(𝑋‘(𝐿‘𝑛))) = 0) |
56 | 55 | breq1d 4663 |
. . . . . . . . . . . 12
⊢ (𝑢 = 0 →
((abs‘Σ𝑛 ∈
(0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅 ↔ 0 ≤ 𝑅)) |
57 | 56 | rspcv 3305 |
. . . . . . . . . . 11
⊢ (0 ∈
(0..^𝑁) →
(∀𝑢 ∈
(0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅 → 0 ≤ 𝑅)) |
58 | 47, 48, 57 | sylc 65 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 𝑅) |
59 | | 0le2 11111 |
. . . . . . . . . . 11
⊢ 0 ≤
2 |
60 | | mulge0 10546 |
. . . . . . . . . . 11
⊢ (((2
∈ ℝ ∧ 0 ≤ 2) ∧ (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅)) → 0 ≤ (2 ·
𝑅)) |
61 | 41, 59, 60 | mpanl12 718 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → 0 ≤ (2
· 𝑅)) |
62 | 42, 58, 61 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (2 · 𝑅)) |
63 | 44, 62 | ge0p1rpd 11902 |
. . . . . . . 8
⊢ (𝜑 → ((2 · 𝑅) + 1) ∈
ℝ+) |
64 | | rpdivcl 11856 |
. . . . . . . 8
⊢ ((𝑒 ∈ ℝ+
∧ ((2 · 𝑅) + 1)
∈ ℝ+) → (𝑒 / ((2 · 𝑅) + 1)) ∈
ℝ+) |
65 | 40, 63, 64 | syl2anr 495 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (𝑒 / ((2 · 𝑅) + 1)) ∈
ℝ+) |
66 | | dchrisum.6 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟
0) |
67 | 66 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (𝑛 ∈ ℝ+
↦ 𝐴)
⇝𝑟 0) |
68 | 39, 65, 67 | rlimi 14244 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑚 ∈ ℝ
∀𝑛 ∈
ℝ+ (𝑚 ≤
𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)))) |
69 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 𝑚 ∈ ℝ) |
70 | | dchrisum.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ ℕ) |
71 | 70 | nnred 11035 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℝ) |
72 | 71 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 𝑀 ∈ ℝ) |
73 | 69, 72 | ifcld 4131 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ) |
74 | | 0red 10041 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 0 ∈
ℝ) |
75 | 70 | nngt0d 11064 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < 𝑀) |
76 | 75 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 0 < 𝑀) |
77 | | max1 12016 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) |
78 | 71, 77 | sylan 488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) |
79 | 74, 72, 73, 76, 78 | ltletrd 10197 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 0 < if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) |
80 | 73, 79 | elrpd 11869 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈
ℝ+) |
81 | 80 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈
ℝ+) |
82 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛 𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀) |
83 | | nfcv 2764 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛abs |
84 | | nfcsb1v 3549 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 |
85 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛
− |
86 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛0 |
87 | 84, 85, 86 | nfov 6676 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0) |
88 | 83, 87 | nffv 6198 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) |
89 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛
< |
90 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(𝑒 / ((2 · 𝑅) + 1)) |
91 | 88, 89, 90 | nfbr 4699 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛(abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) |
92 | 82, 91 | nfim 1825 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → (abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) |
93 | | breq2 4657 |
. . . . . . . . . . 11
⊢ (𝑛 = if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → (𝑚 ≤ 𝑛 ↔ 𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀))) |
94 | | csbeq1a 3542 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → 𝐴 = ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) |
95 | 94 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝑛 = if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → (𝐴 − 0) = (⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) |
96 | 95 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑛 = if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → (abs‘(𝐴 − 0)) =
(abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0))) |
97 | 96 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (𝑛 = if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → ((abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) ↔
(abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)))) |
98 | 93, 97 | imbi12d 334 |
. . . . . . . . . 10
⊢ (𝑛 = if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → ((𝑚 ≤ 𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) ↔ (𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → (abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))))) |
99 | 92, 98 | rspc 3303 |
. . . . . . . . 9
⊢ (if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ+ →
(∀𝑛 ∈
ℝ+ (𝑚 ≤
𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) → (𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → (abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))))) |
100 | 81, 99 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(∀𝑛 ∈
ℝ+ (𝑚 ≤
𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) → (𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → (abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))))) |
101 | 71 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑀 ∈
ℝ) |
102 | | max2 12018 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) |
103 | 101, 102 | sylancom 701 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) |
104 | 13 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
∀𝑛 ∈
ℝ+ 𝐴
∈ ℝ) |
105 | 84 | nfel1 2779 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑛⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 ∈ ℝ |
106 | 94 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → (𝐴 ∈ ℝ ↔
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 ∈ ℝ)) |
107 | 105, 106 | rspc 3303 |
. . . . . . . . . . . . . . . . . 18
⊢ (if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ+ →
(∀𝑛 ∈
ℝ+ 𝐴
∈ ℝ → ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 ∈ ℝ)) |
108 | 81, 104, 107 | sylc 65 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 ∈ ℝ) |
109 | 108 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 ∈ ℂ) |
110 | 109 | subid1d 10381 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0) = ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) |
111 | 110 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) =
(abs‘⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴)) |
112 | 73 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ) |
113 | 101, 77 | sylancom 701 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) |
114 | | elicopnf 12269 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℝ → (if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) ↔ (if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ ∧ 𝑀 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) |
115 | 101, 114 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) ↔ (if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ ∧ 𝑀 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) |
116 | 112, 113,
115 | mpbir2and 957 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞)) |
117 | 45 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑁 ∈
ℕ) |
118 | | rpvmasum.1 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 =
(0g‘𝐺) |
119 | 8 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑋 ∈ 𝐷) |
120 | | dchrisum.n1 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑋 ≠ 1 ) |
121 | 120 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑋 ≠ 1 ) |
122 | | dchrisum.2 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) |
123 | 70 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑀 ∈
ℕ) |
124 | 104 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑛 ∈ ℝ+)
→ 𝐴 ∈
ℝ) |
125 | | simpll 790 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝜑) |
126 | | dchrisum.5 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) |
127 | 125, 126 | syl3an1 1359 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ (𝑛 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) |
128 | 66 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (𝑛 ∈ ℝ+
↦ 𝐴)
⇝𝑟 0) |
129 | 5, 7, 117, 4, 6, 118, 119, 121, 122, 123, 124, 127, 128, 31 | dchrisumlema 25177 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
((if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ+ →
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 ∈ ℝ) ∧ (if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) → 0 ≤
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴))) |
130 | 129 | simprd 479 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) → 0 ≤
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴)) |
131 | 116, 130 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 0 ≤
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) |
132 | 108, 131 | absidd 14161 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(abs‘⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) = ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) |
133 | 111, 132 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) = ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) |
134 | 133 | breq1d 4663 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
((abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) ↔ ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 < (𝑒 / ((2 · 𝑅) + 1)))) |
135 | | rpre 11839 |
. . . . . . . . . . . . . 14
⊢ (𝑒 ∈ ℝ+
→ 𝑒 ∈
ℝ) |
136 | 135 | ad2antlr 763 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑒 ∈
ℝ) |
137 | 63 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2
· 𝑅) + 1) ∈
ℝ+) |
138 | 108, 136,
137 | ltmuldiv2d 11920 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((((2
· 𝑅) + 1) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒 ↔ ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 < (𝑒 / ((2 · 𝑅) + 1)))) |
139 | 134, 138 | bitr4d 271 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
((abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) ↔ (((2 · 𝑅) + 1) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒)) |
140 | 44 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (2
· 𝑅) ∈
ℝ) |
141 | 137 | rpred 11872 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2
· 𝑅) + 1) ∈
ℝ) |
142 | 140 | lep1d 10955 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (2
· 𝑅) ≤ ((2
· 𝑅) +
1)) |
143 | 140, 141,
108, 131, 142 | lemul1ad 10963 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2
· 𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ≤ (((2 · 𝑅) + 1) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴)) |
144 | 140, 108 | remulcld 10070 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2
· 𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∈ ℝ) |
145 | 141, 108 | remulcld 10070 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (((2
· 𝑅) + 1) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∈ ℝ) |
146 | | lelttr 10128 |
. . . . . . . . . . . . 13
⊢ ((((2
· 𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∈ ℝ ∧ (((2 · 𝑅) + 1) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) → ((((2 · 𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ≤ (((2 · 𝑅) + 1) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∧ (((2 · 𝑅) + 1) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒) → ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒)) |
147 | 144, 145,
136, 146 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((((2
· 𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ≤ (((2 · 𝑅) + 1) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∧ (((2 · 𝑅) + 1) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒) → ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒)) |
148 | 143, 147 | mpand 711 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((((2
· 𝑅) + 1) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒 → ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒)) |
149 | 139, 148 | sylbid 230 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
((abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) → ((2 · 𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒)) |
150 | | 1red 10055 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 1 ∈
ℝ) |
151 | 70 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 𝑀 ∈ ℕ) |
152 | 151 | nnge1d 11063 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 1 ≤ 𝑀) |
153 | 150, 72, 73, 152, 78 | letrd 10194 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → 1 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) |
154 | | flge1nn 12622 |
. . . . . . . . . . . . 13
⊢
((if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ ∧ 1 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) → (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) ∈ ℕ) |
155 | 73, 153, 154 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) →
(⌊‘if(𝑀 ≤
𝑚, 𝑚, 𝑀)) ∈ ℕ) |
156 | 155 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(⌊‘if(𝑀 ≤
𝑚, 𝑚, 𝑀)) ∈ ℕ) |
157 | 45 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑁 ∈ ℕ) |
158 | 8 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑋 ∈ 𝐷) |
159 | 120 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑋 ≠ 1 ) |
160 | 70 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑀 ∈ ℕ) |
161 | 12 | adantlr 751 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈
ℝ) |
162 | 161 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈
ℝ) |
163 | 126 | 3adant1r 1319 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) |
164 | 163 | 3adant1r 1319 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) |
165 | 66 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟
0) |
166 | 42 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑅 ∈ ℝ) |
167 | 48 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |
168 | 80 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈
ℝ+) |
169 | 78 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑀 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) |
170 | 73 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ) |
171 | | fllep1 12602 |
. . . . . . . . . . . . . . . 16
⊢ (if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ∈ ℝ → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ≤ ((⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) + 1)) |
172 | 170, 171 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → if(𝑀 ≤ 𝑚, 𝑚, 𝑀) ≤ ((⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) + 1)) |
173 | 155 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) ∈ ℕ) |
174 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) |
175 | 5, 7, 157, 4, 6, 118, 158, 159, 122, 160, 162, 164, 165, 31, 166, 167, 168, 169, 172, 173, 174 | dchrisumlem2 25179 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴)) |
176 | 175 | adantllr 755 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴)) |
177 | 35 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → seq1( + , 𝐹):ℕ⟶ℂ) |
178 | | eluznn 11758 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑘 ∈ ℕ) |
179 | 156, 178 | sylan 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑘 ∈ ℕ) |
180 | 177, 179 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (seq1( + , 𝐹)‘𝑘) ∈ ℂ) |
181 | 156 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) ∈ ℕ) |
182 | 177, 181 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))) ∈ ℂ) |
183 | 180, 182 | subcld 10392 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → ((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) ∈ ℂ) |
184 | 183 | abscld 14175 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) ∈ ℝ) |
185 | 144 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∈ ℝ) |
186 | 136 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → 𝑒 ∈ ℝ) |
187 | | lelttr 10128 |
. . . . . . . . . . . . . 14
⊢
(((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) ∈ ℝ ∧ ((2 ·
𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) → (((abs‘((seq1(
+ , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∧ ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) < 𝑒)) |
188 | 184, 185,
186, 187 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) ∧ ((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) < 𝑒)) |
189 | 176, 188 | mpand 711 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) → (((2 · 𝑅) · ⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒 → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) < 𝑒)) |
190 | 189 | ralrimdva 2969 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (((2
· 𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒 → ∀𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) < 𝑒)) |
191 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) →
(ℤ≥‘𝑗) =
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) |
192 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) → (seq1( + , 𝐹)‘𝑗) = (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))) |
193 | 192 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) → ((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗)) = ((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) |
194 | 193 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) = (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))))) |
195 | 194 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) → ((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒 ↔ (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) < 𝑒)) |
196 | 191, 195 | raleqbidv 3152 |
. . . . . . . . . . . 12
⊢ (𝑗 = (⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒 ↔ ∀𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) < 𝑒)) |
197 | 196 | rspcev 3309 |
. . . . . . . . . . 11
⊢
(((⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)) ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀)))(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀 ≤ 𝑚, 𝑚, 𝑀))))) < 𝑒) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒) |
198 | 156, 190,
197 | syl6an 568 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (((2
· 𝑅) ·
⦋if(𝑀 ≤
𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴) < 𝑒 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)) |
199 | 149, 198 | syld 47 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
((abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)) |
200 | 103, 199 | embantd 59 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((𝑚 ≤ if(𝑀 ≤ 𝑚, 𝑚, 𝑀) → (abs‘(⦋if(𝑀 ≤ 𝑚, 𝑚, 𝑀) / 𝑛⦌𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)) |
201 | 100, 200 | syld 47 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) →
(∀𝑛 ∈
ℝ+ (𝑚 ≤
𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) → ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)) |
202 | 201 | rexlimdva 3031 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
(∃𝑚 ∈ ℝ
∀𝑛 ∈
ℝ+ (𝑚 ≤
𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) → ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)) |
203 | 68, 202 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒) |
204 | 203 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒) |
205 | | seqex 12803 |
. . . . 5
⊢ seq1( + ,
𝐹) ∈
V |
206 | 205 | a1i 11 |
. . . 4
⊢ (𝜑 → seq1( + , 𝐹) ∈ V) |
207 | 1, 36, 204, 206 | caucvg 14409 |
. . 3
⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝
) |
208 | 205 | eldm 5321 |
. . 3
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
↔ ∃𝑡seq1( + ,
𝐹) ⇝ 𝑡) |
209 | 207, 208 | sylib 208 |
. 2
⊢ (𝜑 → ∃𝑡seq1( + , 𝐹) ⇝ 𝑡) |
210 | | simpr 477 |
. . . . 5
⊢ ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → seq1( + , 𝐹) ⇝ 𝑡) |
211 | | elrege0 12278 |
. . . . . . . 8
⊢ ((2
· 𝑅) ∈
(0[,)+∞) ↔ ((2 · 𝑅) ∈ ℝ ∧ 0 ≤ (2 ·
𝑅))) |
212 | 44, 62, 211 | sylanbrc 698 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝑅) ∈
(0[,)+∞)) |
213 | 212 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → (2 · 𝑅) ∈ (0[,)+∞)) |
214 | | eqid 2622 |
. . . . . . . 8
⊢
(ℤ≥‘(⌊‘𝑚)) =
(ℤ≥‘(⌊‘𝑚)) |
215 | | pnfxr 10092 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
216 | | icossre 12254 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝑀[,)+∞) ⊆
ℝ) |
217 | 71, 215, 216 | sylancl 694 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀[,)+∞) ⊆
ℝ) |
218 | 217 | sselda 3603 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ) |
219 | 218 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ) |
220 | 219 | flcld 12599 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (⌊‘𝑚) ∈
ℤ) |
221 | | simplr 792 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → seq1( + , 𝐹) ⇝ 𝑡) |
222 | 35 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → seq1( + , 𝐹):ℕ⟶ℂ) |
223 | | 1red 10055 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 1 ∈
ℝ) |
224 | 71 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℝ) |
225 | 70 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℕ) |
226 | 225 | nnge1d 11063 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 1 ≤ 𝑀) |
227 | | elicopnf 12269 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℝ → (𝑚 ∈ (𝑀[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 𝑀 ≤ 𝑚))) |
228 | 71, 227 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑚 ∈ (𝑀[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 𝑀 ≤ 𝑚))) |
229 | 228 | simplbda 654 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ≤ 𝑚) |
230 | 229 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ≤ 𝑚) |
231 | 223, 224,
219, 226, 230 | letrd 10194 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 1 ≤ 𝑚) |
232 | | flge1nn 12622 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℝ ∧ 1 ≤
𝑚) →
(⌊‘𝑚) ∈
ℕ) |
233 | 219, 231,
232 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (⌊‘𝑚) ∈
ℕ) |
234 | 222, 233 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈
ℂ) |
235 | | nnex 11026 |
. . . . . . . . . . . 12
⊢ ℕ
∈ V |
236 | 235 | mptex 6486 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ ↦ ((seq1(
+ , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ∈ V |
237 | 236 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ∈ V) |
238 | 222 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → seq1( + , 𝐹):ℕ⟶ℂ) |
239 | | eluznn 11758 |
. . . . . . . . . . . 12
⊢
(((⌊‘𝑚)
∈ ℕ ∧ 𝑖
∈ (ℤ≥‘(⌊‘𝑚))) → 𝑖 ∈ ℕ) |
240 | 233, 239 | sylan 488 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑖 ∈ ℕ) |
241 | 238, 240 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (seq1( + , 𝐹)‘𝑖) ∈ ℂ) |
242 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → (seq1( + , 𝐹)‘𝑘) = (seq1( + , 𝐹)‘𝑖)) |
243 | 242 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) |
244 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ ↦ ((seq1(
+ , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) = (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) |
245 | | ovex 6678 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)) ∈ V |
246 | 243, 244,
245 | fvmpt3i 6287 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((seq1(
+ , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) |
247 | 240, 246 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) |
248 | 214, 220,
221, 234, 237, 241, 247 | climsubc2 14369 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ⇝ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) |
249 | 235 | mptex 6486 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ ↦
(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) ∈ V |
250 | 249 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ (abs‘((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) ∈ V) |
251 | | fvex 6201 |
. . . . . . . . . . . . . 14
⊢ (seq1( +
, 𝐹)‘(⌊‘𝑚)) ∈ V |
252 | 251 | fvconst2 6469 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℕ → ((ℕ
× {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) = (seq1( + , 𝐹)‘(⌊‘𝑚))) |
253 | 240, 252 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((ℕ × {(seq1( + ,
𝐹)‘(⌊‘𝑚))})‘𝑖) = (seq1( + , 𝐹)‘(⌊‘𝑚))) |
254 | 253 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (((ℕ × {(seq1( + ,
𝐹)‘(⌊‘𝑚))})‘𝑖) − (seq1( + , 𝐹)‘𝑖)) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) |
255 | 247, 254 | eqtr4d 2659 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) = (((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) − (seq1( + , 𝐹)‘𝑖))) |
256 | 234 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈ ℂ) |
257 | 253, 256 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((ℕ × {(seq1( + ,
𝐹)‘(⌊‘𝑚))})‘𝑖) ∈ ℂ) |
258 | 257, 241 | subcld 10392 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (((ℕ × {(seq1( + ,
𝐹)‘(⌊‘𝑚))})‘𝑖) − (seq1( + , 𝐹)‘𝑖)) ∈ ℂ) |
259 | 255, 258 | eqeltrd 2701 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) ∈ ℂ) |
260 | 243 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))) |
261 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ ↦
(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) = (𝑘 ∈ ℕ ↦ (abs‘((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) |
262 | | fvex 6201 |
. . . . . . . . . . . 12
⊢
(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ∈ V |
263 | 260, 261,
262 | fvmpt3i 6287 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦
(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))) |
264 | 240, 263 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))) |
265 | 247 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (abs‘((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))) |
266 | 264, 265 | eqtr4d 2659 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖))) |
267 | 214, 248,
250, 220, 259, 266 | climabs 14334 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ (abs‘((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) ⇝ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡))) |
268 | 44 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (2 · 𝑅) ∈
ℝ) |
269 | | 0red 10041 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀[,)+∞)) → 0 ∈
ℝ) |
270 | 71 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℝ) |
271 | 75 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀[,)+∞)) → 0 < 𝑀) |
272 | 269, 270,
218, 271, 229 | ltletrd 10197 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀[,)+∞)) → 0 < 𝑚) |
273 | 218, 272 | elrpd 11869 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ+) |
274 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 |
275 | 274 | nfel1 2779 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 ∈ ℝ |
276 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
277 | 276 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝐴 ∈ ℝ ↔ ⦋𝑚 / 𝑛⦌𝐴 ∈ ℝ)) |
278 | 275, 277 | rspc 3303 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℝ+
→ (∀𝑛 ∈
ℝ+ 𝐴
∈ ℝ → ⦋𝑚 / 𝑛⦌𝐴 ∈ ℝ)) |
279 | 13, 278 | mpan9 486 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
⦋𝑚 / 𝑛⦌𝐴 ∈ ℝ) |
280 | 273, 279 | syldan 487 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀[,)+∞)) → ⦋𝑚 / 𝑛⦌𝐴 ∈ ℝ) |
281 | 280 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → ⦋𝑚 / 𝑛⦌𝐴 ∈ ℝ) |
282 | 268, 281 | remulcld 10070 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
283 | 282 | recnd 10068 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴) ∈ ℂ) |
284 | | 1z 11407 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
285 | 1 | eqimss2i 3660 |
. . . . . . . . . 10
⊢
(ℤ≥‘1) ⊆ ℕ |
286 | 285, 235 | climconst2 14279 |
. . . . . . . . 9
⊢ ((((2
· 𝑅) ·
⦋𝑚 / 𝑛⦌𝐴) ∈ ℂ ∧ 1 ∈ ℤ)
→ (ℕ × {((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)}) ⇝ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)) |
287 | 283, 284,
286 | sylancl 694 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (ℕ × {((2
· 𝑅) ·
⦋𝑚 / 𝑛⦌𝐴)}) ⇝ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)) |
288 | 256, 241 | subcld 10392 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)) ∈ ℂ) |
289 | 288 | abscld 14175 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) ∈ ℝ) |
290 | 264, 289 | eqeltrd 2701 |
. . . . . . . 8
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) ∈ ℝ) |
291 | | ovex 6678 |
. . . . . . . . . . 11
⊢ ((2
· 𝑅) ·
⦋𝑚 / 𝑛⦌𝐴) ∈ V |
292 | 291 | fvconst2 6469 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ℕ → ((ℕ
× {((2 · 𝑅)
· ⦋𝑚 /
𝑛⦌𝐴)})‘𝑖) = ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)) |
293 | 240, 292 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((ℕ × {((2 ·
𝑅) ·
⦋𝑚 / 𝑛⦌𝐴)})‘𝑖) = ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)) |
294 | 282 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
295 | 293, 294 | eqeltrd 2701 |
. . . . . . . 8
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((ℕ × {((2 ·
𝑅) ·
⦋𝑚 / 𝑛⦌𝐴)})‘𝑖) ∈ ℝ) |
296 | | simplll 798 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝜑) |
297 | 296, 45 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑁 ∈ ℕ) |
298 | 296, 8 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑋 ∈ 𝐷) |
299 | 296, 120 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑋 ≠ 1 ) |
300 | 225 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑀 ∈ ℕ) |
301 | 296, 12 | sylan 488 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ seq1( + ,
𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈
ℝ) |
302 | 296, 126 | syl3an1 1359 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ seq1( + ,
𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) |
303 | 296, 66 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟
0) |
304 | 296, 42 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑅 ∈ ℝ) |
305 | 296, 48 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |
306 | 273 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ+) |
307 | 306 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑚 ∈ ℝ+) |
308 | 230 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑀 ≤ 𝑚) |
309 | 219 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑚 ∈ ℝ) |
310 | | reflcl 12597 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℝ →
(⌊‘𝑚) ∈
ℝ) |
311 | | peano2re 10209 |
. . . . . . . . . . . 12
⊢
((⌊‘𝑚)
∈ ℝ → ((⌊‘𝑚) + 1) ∈ ℝ) |
312 | 309, 310,
311 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((⌊‘𝑚) + 1) ∈ ℝ) |
313 | | flltp1 12601 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℝ → 𝑚 < ((⌊‘𝑚) + 1)) |
314 | 309, 313 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑚 < ((⌊‘𝑚) + 1)) |
315 | 309, 312,
314 | ltled 10185 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑚 ≤ ((⌊‘𝑚) + 1)) |
316 | 233 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (⌊‘𝑚) ∈ ℕ) |
317 | | simpr 477 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) |
318 | 5, 7, 297, 4, 6, 118, 298, 299, 122, 300, 301, 302, 303, 31, 304, 305, 307, 308, 315, 316, 317 | dchrisumlem2 25179 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (abs‘((seq1( + , 𝐹)‘𝑖) − (seq1( + , 𝐹)‘(⌊‘𝑚)))) ≤ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)) |
319 | 256, 241 | abssubd 14192 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) = (abs‘((seq1( + , 𝐹)‘𝑖) − (seq1( + , 𝐹)‘(⌊‘𝑚))))) |
320 | 264, 319 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((seq1( + , 𝐹)‘𝑖) − (seq1( + , 𝐹)‘(⌊‘𝑚))))) |
321 | 318, 320,
293 | 3brtr4d 4685 |
. . . . . . . 8
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈
(ℤ≥‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( +
, 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) ≤ ((ℕ × {((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)})‘𝑖)) |
322 | 214, 220,
267, 287, 290, 295, 321 | climle 14370 |
. . . . . . 7
⊢ (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (abs‘((seq1( + ,
𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)) |
323 | 322 | ralrimiva 2966 |
. . . . . 6
⊢ ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → ∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)) |
324 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑐 = (2 · 𝑅) → (𝑐 · 𝐵) = ((2 · 𝑅) · 𝐵)) |
325 | 324 | breq2d 4665 |
. . . . . . . . 9
⊢ (𝑐 = (2 · 𝑅) → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵))) |
326 | 325 | ralbidv 2986 |
. . . . . . . 8
⊢ (𝑐 = (2 · 𝑅) → (∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵) ↔ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵))) |
327 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑥 → (⌊‘𝑚) = (⌊‘𝑥)) |
328 | 327 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑥 → (seq1( + , 𝐹)‘(⌊‘𝑚)) = (seq1( + , 𝐹)‘(⌊‘𝑥))) |
329 | 328 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑥 → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡) = ((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) |
330 | 329 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑥 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡))) |
331 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ 𝑚 ∈ V |
332 | 331 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑥 → 𝑚 ∈ V) |
333 | | equequ2 1953 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑥 → (𝑛 = 𝑚 ↔ 𝑛 = 𝑥)) |
334 | 333 | biimpa 501 |
. . . . . . . . . . . . 13
⊢ ((𝑚 = 𝑥 ∧ 𝑛 = 𝑚) → 𝑛 = 𝑥) |
335 | 334, 122 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑚 = 𝑥 ∧ 𝑛 = 𝑚) → 𝐴 = 𝐵) |
336 | 332, 335 | csbied 3560 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑥 → ⦋𝑚 / 𝑛⦌𝐴 = 𝐵) |
337 | 336 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑥 → ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴) = ((2 · 𝑅) · 𝐵)) |
338 | 330, 337 | breq12d 4666 |
. . . . . . . . 9
⊢ (𝑚 = 𝑥 → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵))) |
339 | 338 | cbvralv 3171 |
. . . . . . . 8
⊢
(∀𝑚 ∈
(𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴) ↔ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵)) |
340 | 326, 339 | syl6bbr 278 |
. . . . . . 7
⊢ (𝑐 = (2 · 𝑅) → (∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵) ↔ ∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴))) |
341 | 340 | rspcev 3309 |
. . . . . 6
⊢ (((2
· 𝑅) ∈
(0[,)+∞) ∧ ∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · ⦋𝑚 / 𝑛⦌𝐴)) → ∃𝑐 ∈ (0[,)+∞)∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)) |
342 | 213, 323,
341 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → ∃𝑐 ∈ (0[,)+∞)∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)) |
343 | | r19.42v 3092 |
. . . . 5
⊢
(∃𝑐 ∈
(0[,)+∞)(seq1( + , 𝐹)
⇝ 𝑡 ∧
∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( +
, 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)) ↔ (seq1( + , 𝐹) ⇝ 𝑡 ∧ ∃𝑐 ∈ (0[,)+∞)∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))) |
344 | 210, 342,
343 | sylanbrc 698 |
. . . 4
⊢ ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → ∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))) |
345 | 344 | ex 450 |
. . 3
⊢ (𝜑 → (seq1( + , 𝐹) ⇝ 𝑡 → ∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)))) |
346 | 345 | eximdv 1846 |
. 2
⊢ (𝜑 → (∃𝑡seq1( + , 𝐹) ⇝ 𝑡 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)))) |
347 | 209, 346 | mpd 15 |
1
⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))) |