Proof of Theorem iserex
Step | Hyp | Ref
| Expression |
1 | | seqeq1 10397 |
. . . . 5
⊢ (𝑁 = 𝑀 → seq𝑁( + , 𝐹) = seq𝑀( + , 𝐹)) |
2 | 1 | eleq1d 2239 |
. . . 4
⊢ (𝑁 = 𝑀 → (seq𝑁( + , 𝐹) ∈ dom ⇝ ↔ seq𝑀( + , 𝐹) ∈ dom ⇝ )) |
3 | 2 | bicomd 140 |
. . 3
⊢ (𝑁 = 𝑀 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ )) |
4 | 3 | a1i 9 |
. 2
⊢ (𝜑 → (𝑁 = 𝑀 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))) |
5 | | simpll 524 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → 𝜑) |
6 | | iserex.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
7 | | clim2ser.1 |
. . . . . . . . . . . 12
⊢ 𝑍 =
(ℤ≥‘𝑀) |
8 | 6, 7 | eleqtrdi 2263 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
9 | | eluzelz 9489 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
10 | 8, 9 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) |
11 | 10 | zcnd 9328 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℂ) |
12 | | ax-1cn 7860 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
13 | | npcan 8121 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
14 | 11, 12, 13 | sylancl 411 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
15 | 14 | seqeq1d 10400 |
. . . . . . 7
⊢ (𝜑 → seq((𝑁 − 1) + 1)( + , 𝐹) = seq𝑁( + , 𝐹)) |
16 | 5, 15 | syl 14 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → seq((𝑁 − 1) + 1)( + , 𝐹) = seq𝑁( + , 𝐹)) |
17 | | simplr 525 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
18 | 17, 7 | eleqtrrdi 2264 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → (𝑁 − 1) ∈ 𝑍) |
19 | | iserex.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
20 | 5, 19 | sylan 281 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
21 | | simpr 109 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |
22 | | climdm 11251 |
. . . . . . . 8
⊢ (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑀( + , 𝐹) ⇝ ( ⇝ ‘seq𝑀( + , 𝐹))) |
23 | 21, 22 | sylib 121 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → seq𝑀( + , 𝐹) ⇝ ( ⇝ ‘seq𝑀( + , 𝐹))) |
24 | 7, 18, 20, 23 | clim2ser 11293 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → seq((𝑁 − 1) + 1)( + , 𝐹) ⇝ (( ⇝
‘seq𝑀( + , 𝐹)) − (seq𝑀( + , 𝐹)‘(𝑁 − 1)))) |
25 | 16, 24 | eqbrtrrd 4011 |
. . . . 5
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → seq𝑁( + , 𝐹) ⇝ (( ⇝ ‘seq𝑀( + , 𝐹)) − (seq𝑀( + , 𝐹)‘(𝑁 − 1)))) |
26 | | climrel 11236 |
. . . . . 6
⊢ Rel
⇝ |
27 | 26 | releldmi 4848 |
. . . . 5
⊢ (seq𝑁( + , 𝐹) ⇝ (( ⇝ ‘seq𝑀( + , 𝐹)) − (seq𝑀( + , 𝐹)‘(𝑁 − 1))) → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
28 | 25, 27 | syl 14 |
. . . 4
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
29 | | simpr 109 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
30 | 29, 7 | eleqtrrdi 2264 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (𝑁 − 1) ∈ 𝑍) |
31 | 30 | adantr 274 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) → (𝑁 − 1) ∈ 𝑍) |
32 | | simpll 524 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) → 𝜑) |
33 | 32, 19 | sylan 281 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
34 | 32, 15 | syl 14 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) → seq((𝑁 − 1) + 1)( + , 𝐹) = seq𝑁( + , 𝐹)) |
35 | | simpr 109 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
36 | | climdm 11251 |
. . . . . . . 8
⊢ (seq𝑁( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ⇝ ( ⇝ ‘seq𝑁( + , 𝐹))) |
37 | 35, 36 | sylib 121 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) → seq𝑁( + , 𝐹) ⇝ ( ⇝ ‘seq𝑁( + , 𝐹))) |
38 | 34, 37 | eqbrtrd 4009 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) → seq((𝑁 − 1) + 1)( + , 𝐹) ⇝ ( ⇝
‘seq𝑁( + , 𝐹))) |
39 | 7, 31, 33, 38 | clim2ser2 11294 |
. . . . 5
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) → seq𝑀( + , 𝐹) ⇝ (( ⇝ ‘seq𝑁( + , 𝐹)) + (seq𝑀( + , 𝐹)‘(𝑁 − 1)))) |
40 | 26 | releldmi 4848 |
. . . . 5
⊢ (seq𝑀( + , 𝐹) ⇝ (( ⇝ ‘seq𝑁( + , 𝐹)) + (seq𝑀( + , 𝐹)‘(𝑁 − 1))) → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |
41 | 39, 40 | syl 14 |
. . . 4
⊢ (((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) ∧ seq𝑁( + , 𝐹) ∈ dom ⇝ ) → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |
42 | 28, 41 | impbida 591 |
. . 3
⊢ ((𝜑 ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ )) |
43 | 42 | ex 114 |
. 2
⊢ (𝜑 → ((𝑁 − 1) ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))) |
44 | | uzm1 9510 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈
(ℤ≥‘𝑀))) |
45 | 8, 44 | syl 14 |
. 2
⊢ (𝜑 → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈
(ℤ≥‘𝑀))) |
46 | 4, 43, 45 | mpjaod 713 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ )) |