Step | Hyp | Ref
| Expression |
1 | | serige0.1 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | eluzel2 8624 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
3 | 1, 2 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
4 | | cnex 7097 |
. . . . . 6
⊢ ℂ
∈ V |
5 | 4 | a1i 9 |
. . . . 5
⊢ (𝜑 → ℂ ∈
V) |
6 | | ssrab2 3079 |
. . . . . . 7
⊢ {𝑥 ∈ ℝ ∣ 0 ≤
𝑥} ⊆
ℝ |
7 | | ax-resscn 7068 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
8 | 6, 7 | sstri 3008 |
. . . . . 6
⊢ {𝑥 ∈ ℝ ∣ 0 ≤
𝑥} ⊆
ℂ |
9 | 8 | a1i 9 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥} ⊆
ℂ) |
10 | | serige0.2 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℝ) |
11 | | serige0.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 0 ≤ (𝐹‘𝑘)) |
12 | | breq2 3789 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝑘) → (0 ≤ 𝑥 ↔ 0 ≤ (𝐹‘𝑘))) |
13 | 12 | elrab 2749 |
. . . . . 6
⊢ ((𝐹‘𝑘) ∈ {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥} ↔ ((𝐹‘𝑘) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑘))) |
14 | 10, 11, 13 | sylanbrc 408 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥}) |
15 | | breq2 3789 |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → (0 ≤ 𝑥 ↔ 0 ≤ 𝑘)) |
16 | 15 | elrab 2749 |
. . . . . . 7
⊢ (𝑘 ∈ {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥} ↔ (𝑘 ∈ ℝ ∧ 0 ≤ 𝑘)) |
17 | | breq2 3789 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (0 ≤ 𝑥 ↔ 0 ≤ 𝑦)) |
18 | 17 | elrab 2749 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥} ↔ (𝑦 ∈ ℝ ∧ 0 ≤ 𝑦)) |
19 | | readdcl 7099 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑘 + 𝑦) ∈ ℝ) |
20 | 19 | ad2ant2r 492 |
. . . . . . . 8
⊢ (((𝑘 ∈ ℝ ∧ 0 ≤
𝑘) ∧ (𝑦 ∈ ℝ ∧ 0 ≤
𝑦)) → (𝑘 + 𝑦) ∈ ℝ) |
21 | | addge0 7555 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (0 ≤
𝑘 ∧ 0 ≤ 𝑦)) → 0 ≤ (𝑘 + 𝑦)) |
22 | 21 | an4s 552 |
. . . . . . . 8
⊢ (((𝑘 ∈ ℝ ∧ 0 ≤
𝑘) ∧ (𝑦 ∈ ℝ ∧ 0 ≤
𝑦)) → 0 ≤ (𝑘 + 𝑦)) |
23 | | breq2 3789 |
. . . . . . . . 9
⊢ (𝑥 = (𝑘 + 𝑦) → (0 ≤ 𝑥 ↔ 0 ≤ (𝑘 + 𝑦))) |
24 | 23 | elrab 2749 |
. . . . . . . 8
⊢ ((𝑘 + 𝑦) ∈ {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥} ↔ ((𝑘 + 𝑦) ∈ ℝ ∧ 0 ≤ (𝑘 + 𝑦))) |
25 | 20, 22, 24 | sylanbrc 408 |
. . . . . . 7
⊢ (((𝑘 ∈ ℝ ∧ 0 ≤
𝑘) ∧ (𝑦 ∈ ℝ ∧ 0 ≤
𝑦)) → (𝑘 + 𝑦) ∈ {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥}) |
26 | 16, 18, 25 | syl2anb 285 |
. . . . . 6
⊢ ((𝑘 ∈ {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥} ∧ 𝑦 ∈ {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥}) → (𝑘 + 𝑦) ∈ {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥}) |
27 | 26 | adantl 271 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥} ∧ 𝑦 ∈ {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥})) → (𝑘 + 𝑦) ∈ {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥}) |
28 | | addcl 7098 |
. . . . . 6
⊢ ((𝑘 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑘 + 𝑦) ∈ ℂ) |
29 | 28 | adantl 271 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑘 + 𝑦) ∈ ℂ) |
30 | 3, 5, 9, 14, 27, 29 | iseqss 9446 |
. . . 4
⊢ (𝜑 → seq𝑀( + , 𝐹, {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥}) = seq𝑀( + , 𝐹, ℂ)) |
31 | 30 | fveq1d 5200 |
. . 3
⊢ (𝜑 → (seq𝑀( + , 𝐹, {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥})‘𝑁) = (seq𝑀( + , 𝐹, ℂ)‘𝑁)) |
32 | | reex 7107 |
. . . . . 6
⊢ ℝ
∈ V |
33 | 32 | rabex 3922 |
. . . . 5
⊢ {𝑥 ∈ ℝ ∣ 0 ≤
𝑥} ∈
V |
34 | 33 | a1i 9 |
. . . 4
⊢ (𝜑 → {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥} ∈ V) |
35 | 1, 34, 14, 27 | iseqcl 9443 |
. . 3
⊢ (𝜑 → (seq𝑀( + , 𝐹, {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥})‘𝑁) ∈ {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥}) |
36 | 31, 35 | eqeltrrd 2156 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹, ℂ)‘𝑁) ∈ {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥}) |
37 | | breq2 3789 |
. . . 4
⊢ (𝑥 = (seq𝑀( + , 𝐹, ℂ)‘𝑁) → (0 ≤ 𝑥 ↔ 0 ≤ (seq𝑀( + , 𝐹, ℂ)‘𝑁))) |
38 | 37 | elrab 2749 |
. . 3
⊢
((seq𝑀( + , 𝐹, ℂ)‘𝑁) ∈ {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥} ↔ ((seq𝑀( + , 𝐹, ℂ)‘𝑁) ∈ ℝ ∧ 0 ≤ (seq𝑀( + , 𝐹, ℂ)‘𝑁))) |
39 | 38 | simprbi 269 |
. 2
⊢
((seq𝑀( + , 𝐹, ℂ)‘𝑁) ∈ {𝑥 ∈ ℝ ∣ 0 ≤ 𝑥} → 0 ≤ (seq𝑀( + , 𝐹, ℂ)‘𝑁)) |
40 | 36, 39 | syl 14 |
1
⊢ (𝜑 → 0 ≤ (seq𝑀( + , 𝐹, ℂ)‘𝑁)) |