Proof of Theorem ntrivcvg
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ntrivcvg.2 | . 2
⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦)) | 
| 2 |  | uzm1 12916 | . . . . . . . . 9
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝑛 = 𝑀 ∨ (𝑛 − 1) ∈
(ℤ≥‘𝑀))) | 
| 3 |  | ntrivcvg.1 | . . . . . . . . 9
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 4 | 2, 3 | eleq2s 2859 | . . . . . . . 8
⊢ (𝑛 ∈ 𝑍 → (𝑛 = 𝑀 ∨ (𝑛 − 1) ∈
(ℤ≥‘𝑀))) | 
| 5 | 4 | ad2antlr 727 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → (𝑛 = 𝑀 ∨ (𝑛 − 1) ∈
(ℤ≥‘𝑀))) | 
| 6 |  | seqeq1 14045 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑀 → seq𝑛( · , 𝐹) = seq𝑀( · , 𝐹)) | 
| 7 | 6 | breq1d 5153 | . . . . . . . . . 10
⊢ (𝑛 = 𝑀 → (seq𝑛( · , 𝐹) ⇝ 𝑦 ↔ seq𝑀( · , 𝐹) ⇝ 𝑦)) | 
| 8 |  | seqex 14044 | . . . . . . . . . . 11
⊢ seq𝑀( · , 𝐹) ∈ V | 
| 9 |  | vex 3484 | . . . . . . . . . . 11
⊢ 𝑦 ∈ V | 
| 10 | 8, 9 | breldm 5919 | . . . . . . . . . 10
⊢ (seq𝑀( · , 𝐹) ⇝ 𝑦 → seq𝑀( · , 𝐹) ∈ dom ⇝ ) | 
| 11 | 7, 10 | biimtrdi 253 | . . . . . . . . 9
⊢ (𝑛 = 𝑀 → (seq𝑛( · , 𝐹) ⇝ 𝑦 → seq𝑀( · , 𝐹) ∈ dom ⇝ )) | 
| 12 | 11 | adantld 490 | . . . . . . . 8
⊢ (𝑛 = 𝑀 → (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) | 
| 13 |  | simplr 769 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → (𝑛 − 1) ∈ 𝑍) | 
| 14 |  | ntrivcvg.3 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) | 
| 15 | 14 | ad5ant15 759 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) | 
| 16 |  | uzssz 12899 | . . . . . . . . . . . . . . . . . . . 20
⊢
(ℤ≥‘𝑀) ⊆ ℤ | 
| 17 | 3, 16 | eqsstri 4030 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑍 ⊆
ℤ | 
| 18 |  | simplr 769 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → 𝑛 ∈ 𝑍) | 
| 19 | 17, 18 | sselid 3981 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → 𝑛 ∈ ℤ) | 
| 20 | 19 | zcnd 12723 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → 𝑛 ∈ ℂ) | 
| 21 |  | 1cnd 11256 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → 1 ∈ ℂ) | 
| 22 | 20, 21 | npcand 11624 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → ((𝑛 − 1) + 1) = 𝑛) | 
| 23 | 22 | seqeq1d 14048 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → seq((𝑛 − 1) + 1)( · , 𝐹) = seq𝑛( · , 𝐹)) | 
| 24 | 23 | breq1d 5153 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → (seq((𝑛 − 1) + 1)( · , 𝐹) ⇝ 𝑦 ↔ seq𝑛( · , 𝐹) ⇝ 𝑦)) | 
| 25 | 24 | biimpar 477 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq((𝑛 − 1) + 1)( · , 𝐹) ⇝ 𝑦) | 
| 26 | 3, 13, 15, 25 | clim2prod 15924 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ⇝ ((seq𝑀( · , 𝐹)‘(𝑛 − 1)) · 𝑦)) | 
| 27 |  | ovex 7464 | . . . . . . . . . . . . 13
⊢
((seq𝑀( · ,
𝐹)‘(𝑛 − 1)) · 𝑦) ∈ V | 
| 28 | 8, 27 | breldm 5919 | . . . . . . . . . . . 12
⊢ (seq𝑀( · , 𝐹) ⇝ ((seq𝑀( · , 𝐹)‘(𝑛 − 1)) · 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ ) | 
| 29 | 26, 28 | syl 17 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ ) | 
| 30 | 29 | an32s 652 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ (𝑛 − 1) ∈ 𝑍) → seq𝑀( · , 𝐹) ∈ dom ⇝ ) | 
| 31 | 30 | expcom 413 | . . . . . . . . 9
⊢ ((𝑛 − 1) ∈ 𝑍 → (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) | 
| 32 | 3 | eqcomi 2746 | . . . . . . . . 9
⊢
(ℤ≥‘𝑀) = 𝑍 | 
| 33 | 31, 32 | eleq2s 2859 | . . . . . . . 8
⊢ ((𝑛 − 1) ∈
(ℤ≥‘𝑀) → (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) | 
| 34 | 12, 33 | jaoi 858 | . . . . . . 7
⊢ ((𝑛 = 𝑀 ∨ (𝑛 − 1) ∈
(ℤ≥‘𝑀)) → (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) | 
| 35 | 5, 34 | mpcom 38 | . . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ ) | 
| 36 | 35 | ex 412 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (seq𝑛( · , 𝐹) ⇝ 𝑦 → seq𝑀( · , 𝐹) ∈ dom ⇝ )) | 
| 37 | 36 | adantld 490 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) | 
| 38 | 37 | exlimdv 1933 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) | 
| 39 | 38 | rexlimdva 3155 | . 2
⊢ (𝜑 → (∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) | 
| 40 | 1, 39 | mpd 15 | 1
⊢ (𝜑 → seq𝑀( · , 𝐹) ∈ dom ⇝ ) |