Step | Hyp | Ref
| Expression |
1 | | eqid 2081 |
. 2
⊢
(ℤ≥‘(𝑁 + 1)) =
(ℤ≥‘(𝑁 + 1)) |
2 | | clim2ser.2 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
3 | | clim2ser.1 |
. . . . 5
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | 2, 3 | syl6eleq 2171 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
5 | | peano2uz 8671 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
6 | 4, 5 | syl 14 |
. . 3
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
7 | | eluzelz 8628 |
. . 3
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈ ℤ) |
8 | 6, 7 | syl 14 |
. 2
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
9 | | clim2ser.5 |
. 2
⊢ (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ 𝐴) |
10 | | eluzel2 8624 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
11 | 4, 10 | syl 14 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
12 | | clim2ser.4 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
13 | 3, 11, 12 | iserf 9453 |
. . 3
⊢ (𝜑 → seq𝑀( + , 𝐹, ℂ):𝑍⟶ℂ) |
14 | 13, 2 | ffvelrnd 5324 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹, ℂ)‘𝑁) ∈ ℂ) |
15 | | iseqex 9433 |
. . 3
⊢ seq(𝑁 + 1)( + , 𝐹, ℂ) ∈ V |
16 | 15 | a1i 9 |
. 2
⊢ (𝜑 → seq(𝑁 + 1)( + , 𝐹, ℂ) ∈ V) |
17 | 13 | adantr 270 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → seq𝑀( + , 𝐹, ℂ):𝑍⟶ℂ) |
18 | 6, 3 | syl6eleqr 2172 |
. . . 4
⊢ (𝜑 → (𝑁 + 1) ∈ 𝑍) |
19 | 3 | uztrn2 8636 |
. . . 4
⊢ (((𝑁 + 1) ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑗 ∈ 𝑍) |
20 | 18, 19 | sylan 277 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑗 ∈ 𝑍) |
21 | 17, 20 | ffvelrnd 5324 |
. 2
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (seq𝑀( + , 𝐹, ℂ)‘𝑗) ∈ ℂ) |
22 | | addcl 7098 |
. . . . . 6
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 + 𝑥) ∈ ℂ) |
23 | 22 | adantl 271 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 + 𝑥) ∈ ℂ) |
24 | | addass 7103 |
. . . . . 6
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑘 + 𝑥) + 𝑦) = (𝑘 + (𝑥 + 𝑦))) |
25 | 24 | adantl 271 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝑘 + 𝑥) + 𝑦) = (𝑘 + (𝑥 + 𝑦))) |
26 | | simpr 108 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑗 ∈
(ℤ≥‘(𝑁 + 1))) |
27 | | cnex 7097 |
. . . . . 6
⊢ ℂ
∈ V |
28 | 27 | a1i 9 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → ℂ ∈
V) |
29 | 4 | adantr 270 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ (ℤ≥‘𝑀)) |
30 | 3 | eleq2i 2145 |
. . . . . . 7
⊢ (𝑘 ∈ 𝑍 ↔ 𝑘 ∈ (ℤ≥‘𝑀)) |
31 | 30, 12 | sylan2br 282 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
32 | 31 | adantlr 460 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
33 | 23, 25, 26, 28, 29, 32 | iseqsplit 9458 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (seq𝑀( + , 𝐹, ℂ)‘𝑗) = ((seq𝑀( + , 𝐹, ℂ)‘𝑁) + (seq(𝑁 + 1)( + , 𝐹, ℂ)‘𝑗))) |
34 | 33 | oveq1d 5547 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → ((seq𝑀( + , 𝐹, ℂ)‘𝑗) − (seq𝑀( + , 𝐹, ℂ)‘𝑁)) = (((seq𝑀( + , 𝐹, ℂ)‘𝑁) + (seq(𝑁 + 1)( + , 𝐹, ℂ)‘𝑗)) − (seq𝑀( + , 𝐹, ℂ)‘𝑁))) |
35 | 14 | adantr 270 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (seq𝑀( + , 𝐹, ℂ)‘𝑁) ∈ ℂ) |
36 | 3 | uztrn2 8636 |
. . . . . . . 8
⊢ (((𝑁 + 1) ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈ 𝑍) |
37 | 18, 36 | sylan 277 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈ 𝑍) |
38 | 37, 12 | syldan 276 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝐹‘𝑘) ∈ ℂ) |
39 | 1, 8, 38 | iserf 9453 |
. . . . 5
⊢ (𝜑 → seq(𝑁 + 1)( + , 𝐹,
ℂ):(ℤ≥‘(𝑁 + 1))⟶ℂ) |
40 | 39 | ffvelrnda 5323 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (seq(𝑁 + 1)( + , 𝐹, ℂ)‘𝑗) ∈ ℂ) |
41 | 35, 40 | pncan2d 7421 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (((seq𝑀( + , 𝐹, ℂ)‘𝑁) + (seq(𝑁 + 1)( + , 𝐹, ℂ)‘𝑗)) − (seq𝑀( + , 𝐹, ℂ)‘𝑁)) = (seq(𝑁 + 1)( + , 𝐹, ℂ)‘𝑗)) |
42 | 34, 41 | eqtr2d 2114 |
. 2
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (seq(𝑁 + 1)( + , 𝐹, ℂ)‘𝑗) = ((seq𝑀( + , 𝐹, ℂ)‘𝑗) − (seq𝑀( + , 𝐹, ℂ)‘𝑁))) |
43 | 1, 8, 9, 14, 16, 21, 42 | climsubc1 10170 |
1
⊢ (𝜑 → seq(𝑁 + 1)( + , 𝐹, ℂ) ⇝ (𝐴 − (seq𝑀( + , 𝐹, ℂ)‘𝑁))) |