Proof of Theorem ntrivcvg
Step | Hyp | Ref
| Expression |
1 | | ntrivcvg.2 |
. 2
⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦)) |
2 | | uzm1 11594 |
. . . . . . . . 9
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝑛 = 𝑀 ∨ (𝑛 − 1) ∈
(ℤ≥‘𝑀))) |
3 | | ntrivcvg.1 |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | 2, 3 | eleq2s 2706 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑍 → (𝑛 = 𝑀 ∨ (𝑛 − 1) ∈
(ℤ≥‘𝑀))) |
5 | 4 | ad2antlr 759 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → (𝑛 = 𝑀 ∨ (𝑛 − 1) ∈
(ℤ≥‘𝑀))) |
6 | | seqeq1 12666 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑀 → seq𝑛( · , 𝐹) = seq𝑀( · , 𝐹)) |
7 | 6 | breq1d 4593 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑀 → (seq𝑛( · , 𝐹) ⇝ 𝑦 ↔ seq𝑀( · , 𝐹) ⇝ 𝑦)) |
8 | | seqex 12665 |
. . . . . . . . . . 11
⊢ seq𝑀( · , 𝐹) ∈ V |
9 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
10 | 8, 9 | breldm 5251 |
. . . . . . . . . 10
⊢ (seq𝑀( · , 𝐹) ⇝ 𝑦 → seq𝑀( · , 𝐹) ∈ dom ⇝ ) |
11 | 7, 10 | syl6bi 242 |
. . . . . . . . 9
⊢ (𝑛 = 𝑀 → (seq𝑛( · , 𝐹) ⇝ 𝑦 → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
12 | 11 | adantld 482 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
13 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → (𝑛 − 1) ∈ 𝑍) |
14 | | ntrivcvg.3 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
15 | 14 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
16 | 15 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
17 | 16 | adantlr 747 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
18 | | uzssz 11583 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
19 | 3, 18 | eqsstri 3598 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑍 ⊆
ℤ |
20 | | simplr 788 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → 𝑛 ∈ 𝑍) |
21 | 19, 20 | sseldi 3566 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → 𝑛 ∈ ℤ) |
22 | 21 | zcnd 11359 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → 𝑛 ∈ ℂ) |
23 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → 1 ∈ ℂ) |
24 | 22, 23 | npcand 10275 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → ((𝑛 − 1) + 1) = 𝑛) |
25 | 24 | seqeq1d 12669 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → seq((𝑛 − 1) + 1)( · , 𝐹) = seq𝑛( · , 𝐹)) |
26 | 25 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → (seq((𝑛 − 1) + 1)( · , 𝐹) ⇝ 𝑦 ↔ seq𝑛( · , 𝐹) ⇝ 𝑦)) |
27 | 26 | biimpar 501 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq((𝑛 − 1) + 1)( · , 𝐹) ⇝ 𝑦) |
28 | 3, 13, 17, 27 | clim2prod 14459 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ⇝ ((seq𝑀( · , 𝐹)‘(𝑛 − 1)) · 𝑦)) |
29 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢
((seq𝑀( · ,
𝐹)‘(𝑛 − 1)) · 𝑦) ∈ V |
30 | 8, 29 | breldm 5251 |
. . . . . . . . . . . 12
⊢ (seq𝑀( · , 𝐹) ⇝ ((seq𝑀( · , 𝐹)‘(𝑛 − 1)) · 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ ) |
31 | 28, 30 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ ) |
32 | 31 | an32s 842 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ (𝑛 − 1) ∈ 𝑍) → seq𝑀( · , 𝐹) ∈ dom ⇝ ) |
33 | 32 | expcom 450 |
. . . . . . . . 9
⊢ ((𝑛 − 1) ∈ 𝑍 → (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
34 | 3 | eqcomi 2619 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) = 𝑍 |
35 | 33, 34 | eleq2s 2706 |
. . . . . . . 8
⊢ ((𝑛 − 1) ∈
(ℤ≥‘𝑀) → (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
36 | 12, 35 | jaoi 393 |
. . . . . . 7
⊢ ((𝑛 = 𝑀 ∨ (𝑛 − 1) ∈
(ℤ≥‘𝑀)) → (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
37 | 5, 36 | mpcom 37 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ ) |
38 | 37 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (seq𝑛( · , 𝐹) ⇝ 𝑦 → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
39 | 38 | adantld 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
40 | 39 | exlimdv 1848 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
41 | 40 | rexlimdva 3013 |
. 2
⊢ (𝜑 → (∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
42 | 1, 41 | mpd 15 |
1
⊢ (𝜑 → seq𝑀( · , 𝐹) ∈ dom ⇝ ) |