Proof of Theorem iiserex
Step | Hyp | Ref
| Expression |
1 | | iseqeq1 9214 |
. . . . 5
⊢ (𝑁 = 𝑀 → seq𝑁( + , 𝐹, ℂ) = seq𝑀( + , 𝐹, ℂ)) |
2 | 1 | eleq1d 2106 |
. . . 4
⊢ (𝑁 = 𝑀 → (seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝ ↔
seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝
)) |
3 | 2 | bicomd 129 |
. . 3
⊢ (𝑁 = 𝑀 → (seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ↔
seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝
)) |
4 | 3 | a1i 9 |
. 2
⊢ (𝜑 → (𝑁 = 𝑀 → (seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ↔
seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝
))) |
5 | | simpll 481 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ) → 𝜑) |
6 | | iserex.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
7 | | clim2ser.1 |
. . . . . . . . . . . 12
⊢ 𝑍 =
(ℤ≥‘𝑀) |
8 | 6, 7 | syl6eleq 2130 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
9 | | eluzelz 8482 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
10 | 8, 9 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) |
11 | 10 | zcnd 8361 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℂ) |
12 | | ax-1cn 6977 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
13 | | npcan 7220 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
14 | 11, 12, 13 | sylancl 392 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
15 | | iseqeq1 9214 |
. . . . . . . 8
⊢ (((𝑁 − 1) + 1) = 𝑁 → seq((𝑁 − 1) + 1)( + , 𝐹, ℂ) = seq𝑁( + , 𝐹, ℂ)) |
16 | 14, 15 | syl 14 |
. . . . . . 7
⊢ (𝜑 → seq((𝑁 − 1) + 1)( + , 𝐹, ℂ) = seq𝑁( + , 𝐹, ℂ)) |
17 | 5, 16 | syl 14 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ) →
seq((𝑁 − 1) + 1)( + ,
𝐹, ℂ) = seq𝑁( + , 𝐹, ℂ)) |
18 | | simplr 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ) →
(𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
19 | 18, 7 | syl6eleqr 2131 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ) →
(𝑁 − 1) ∈ 𝑍) |
20 | | iserex.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
21 | 5, 20 | sylan 267 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
22 | | simpr 103 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ) →
seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝
) |
23 | | climdm 9816 |
. . . . . . . 8
⊢ (seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ↔
seq𝑀( + , 𝐹, ℂ) ⇝ ( ⇝ ‘seq𝑀( + , 𝐹, ℂ))) |
24 | 22, 23 | sylib 127 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ) →
seq𝑀( + , 𝐹, ℂ) ⇝ ( ⇝ ‘seq𝑀( + , 𝐹, ℂ))) |
25 | 7, 19, 21, 24 | clim2iser 9857 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ) →
seq((𝑁 − 1) + 1)( + ,
𝐹, ℂ) ⇝ ((
⇝ ‘seq𝑀( + ,
𝐹, ℂ)) −
(seq𝑀( + , 𝐹, ℂ)‘(𝑁 − 1)))) |
26 | 17, 25 | eqbrtrrd 3786 |
. . . . 5
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ) →
seq𝑁( + , 𝐹, ℂ) ⇝ (( ⇝
‘seq𝑀( + , 𝐹, ℂ)) − (seq𝑀( + , 𝐹, ℂ)‘(𝑁 − 1)))) |
27 | | climrel 9801 |
. . . . . 6
⊢ Rel
⇝ |
28 | 27 | releldmi 4573 |
. . . . 5
⊢ (seq𝑁( + , 𝐹, ℂ) ⇝ (( ⇝
‘seq𝑀( + , 𝐹, ℂ)) − (seq𝑀( + , 𝐹, ℂ)‘(𝑁 − 1))) → seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝
) |
29 | 26, 28 | syl 14 |
. . . 4
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ) →
seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝
) |
30 | | simpr 103 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
31 | 30, 7 | syl6eleqr 2131 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (𝑁 − 1) ∈ 𝑍) |
32 | 31 | adantr 261 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝ ) →
(𝑁 − 1) ∈ 𝑍) |
33 | | simpll 481 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝ ) → 𝜑) |
34 | 33, 20 | sylan 267 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝ ) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
35 | 33, 16 | syl 14 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝ ) →
seq((𝑁 − 1) + 1)( + ,
𝐹, ℂ) = seq𝑁( + , 𝐹, ℂ)) |
36 | | simpr 103 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝ ) →
seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝
) |
37 | | climdm 9816 |
. . . . . . . 8
⊢ (seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝ ↔
seq𝑁( + , 𝐹, ℂ) ⇝ ( ⇝ ‘seq𝑁( + , 𝐹, ℂ))) |
38 | 36, 37 | sylib 127 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝ ) →
seq𝑁( + , 𝐹, ℂ) ⇝ ( ⇝ ‘seq𝑁( + , 𝐹, ℂ))) |
39 | 35, 38 | eqbrtrd 3784 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝ ) →
seq((𝑁 − 1) + 1)( + ,
𝐹, ℂ) ⇝ (
⇝ ‘seq𝑁( + ,
𝐹,
ℂ))) |
40 | 7, 32, 34, 39 | clim2iser2 9858 |
. . . . 5
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝ ) →
seq𝑀( + , 𝐹, ℂ) ⇝ (( ⇝
‘seq𝑁( + , 𝐹, ℂ)) + (seq𝑀( + , 𝐹, ℂ)‘(𝑁 − 1)))) |
41 | 27 | releldmi 4573 |
. . . . 5
⊢ (seq𝑀( + , 𝐹, ℂ) ⇝ (( ⇝
‘seq𝑁( + , 𝐹, ℂ)) + (seq𝑀( + , 𝐹, ℂ)‘(𝑁 − 1))) → seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝
) |
42 | 40, 41 | syl 14 |
. . . 4
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝ ) →
seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝
) |
43 | 29, 42 | impbida 528 |
. . 3
⊢ ((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ↔
seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝
)) |
44 | 43 | ex 108 |
. 2
⊢ (𝜑 → ((𝑁 − 1) ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ↔
seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝
))) |
45 | | uzm1 8503 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈
(ℤ≥‘𝑀))) |
46 | 8, 45 | syl 14 |
. 2
⊢ (𝜑 → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈
(ℤ≥‘𝑀))) |
47 | 4, 44, 46 | mpjaod 638 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ↔
seq𝑁( + , 𝐹, ℂ) ∈ dom ⇝
)) |