Proof of Theorem iserex
Step | Hyp | Ref
| Expression |
1 | | seqeq1 13406 |
. . . . 5
⊢ (𝑁 = 𝑀 → seq𝑁( + , 𝐹) = seq𝑀( + , 𝐹)) |
2 | 1 | eleq1d 2835 |
. . . 4
⊢ (𝑁 = 𝑀 → (seq𝑁( + , 𝐹) ∈ dom ⇝ ↔ seq𝑀( + , 𝐹) ∈ dom ⇝ )) |
3 | 2 | bicomd 226 |
. . 3
⊢ (𝑁 = 𝑀 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ )) |
4 | 3 | a1i 11 |
. 2
⊢ (𝜑 → (𝑁 = 𝑀 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))) |
5 | | simpll 767 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → 𝜑) |
6 | | iserex.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
7 | | clim2ser.1 |
. . . . . . . . . . . 12
⊢ 𝑍 =
(ℤ≥‘𝑀) |
8 | 6, 7 | eleqtrdi 2861 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
9 | | eluzelz 12277 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
10 | 8, 9 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) |
11 | 10 | zcnd 12112 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℂ) |
12 | | ax-1cn 10618 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
13 | | npcan 10918 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
14 | 11, 12, 13 | sylancl 590 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
15 | 14 | seqeq1d 13409 |
. . . . . . 7
⊢ (𝜑 → seq((𝑁 − 1) + 1)( + , 𝐹) = seq𝑁( + , 𝐹)) |
16 | 5, 15 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → seq((𝑁 − 1) + 1)( + , 𝐹) = seq𝑁( + , 𝐹)) |
17 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
18 | 17, 7 | eleqtrrdi 2862 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → (𝑁 − 1) ∈ 𝑍) |
19 | | iserex.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
20 | 5, 19 | sylan 584 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
21 | | simpr 489 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |
22 | | climdm 14944 |
. . . . . . . 8
⊢ (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑀( + , 𝐹) ⇝ ( ⇝ ‘seq𝑀( + , 𝐹))) |
23 | 21, 22 | sylib 221 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → seq𝑀( + , 𝐹) ⇝ ( ⇝ ‘seq𝑀( + , 𝐹))) |
24 | 7, 18, 20, 23 | clim2ser 15044 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → seq((𝑁 − 1) + 1)( + , 𝐹) ⇝ (( ⇝
‘seq𝑀( + , 𝐹)) − (seq𝑀( + , 𝐹)‘(𝑁 − 1)))) |
25 | 16, 24 | eqbrtrrd 5049 |
. . . . 5
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → seq𝑁( + , 𝐹) ⇝ (( ⇝ ‘seq𝑀( + , 𝐹)) − (seq𝑀( + , 𝐹)‘(𝑁 − 1)))) |
26 | | climrel 14882 |
. . . . . 6
⊢ Rel
⇝ |
27 | 26 | releldmi 5782 |
. . . . 5
⊢ (seq𝑁( + , 𝐹) ⇝ (( ⇝ ‘seq𝑀( + , 𝐹)) − (seq𝑀( + , 𝐹)‘(𝑁 − 1))) → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
28 | 25, 27 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
29 | | simpr 489 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
30 | 29, 7 | eleqtrrdi 2862 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (𝑁 − 1) ∈ 𝑍) |
31 | 30 | adantr 485 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) → (𝑁 − 1) ∈ 𝑍) |
32 | | simpll 767 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) → 𝜑) |
33 | 32, 19 | sylan 584 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
34 | 32, 15 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) → seq((𝑁 − 1) + 1)( + , 𝐹) = seq𝑁( + , 𝐹)) |
35 | | simpr 489 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
36 | | climdm 14944 |
. . . . . . . 8
⊢ (seq𝑁( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ⇝ ( ⇝ ‘seq𝑁( + , 𝐹))) |
37 | 35, 36 | sylib 221 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) → seq𝑁( + , 𝐹) ⇝ ( ⇝ ‘seq𝑁( + , 𝐹))) |
38 | 34, 37 | eqbrtrd 5047 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) → seq((𝑁 − 1) + 1)( + , 𝐹) ⇝ ( ⇝
‘seq𝑁( + , 𝐹))) |
39 | 7, 31, 33, 38 | clim2ser2 15045 |
. . . . 5
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) → seq𝑀( + , 𝐹) ⇝ (( ⇝ ‘seq𝑁( + , 𝐹)) + (seq𝑀( + , 𝐹)‘(𝑁 − 1)))) |
40 | 26 | releldmi 5782 |
. . . . 5
⊢ (seq𝑀( + , 𝐹) ⇝ (( ⇝ ‘seq𝑁( + , 𝐹)) + (seq𝑀( + , 𝐹)‘(𝑁 − 1))) → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |
41 | 39, 40 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |
42 | 28, 41 | impbida 801 |
. . 3
⊢ ((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ )) |
43 | 42 | ex 417 |
. 2
⊢ (𝜑 → ((𝑁 − 1) ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))) |
44 | | uzm1 12301 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈
(ℤ≥‘𝑀))) |
45 | 8, 44 | syl 17 |
. 2
⊢ (𝜑 → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈
(ℤ≥‘𝑀))) |
46 | 4, 43, 45 | mpjaod 858 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ )) |