Proof of Theorem ntrivcvgap
Step | Hyp | Ref
| Expression |
1 | | ntrivcvgap.2 |
. 2
⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦)) |
2 | | uzm1 9470 |
. . . . . . . . 9
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝑛 = 𝑀 ∨ (𝑛 − 1) ∈
(ℤ≥‘𝑀))) |
3 | | ntrivcvg.1 |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | 2, 3 | eleq2s 2252 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑍 → (𝑛 = 𝑀 ∨ (𝑛 − 1) ∈
(ℤ≥‘𝑀))) |
5 | 4 | ad2antlr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → (𝑛 = 𝑀 ∨ (𝑛 − 1) ∈
(ℤ≥‘𝑀))) |
6 | | seqeq1 10351 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑀 → seq𝑛( · , 𝐹) = seq𝑀( · , 𝐹)) |
7 | 6 | breq1d 3976 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑀 → (seq𝑛( · , 𝐹) ⇝ 𝑦 ↔ seq𝑀( · , 𝐹) ⇝ 𝑦)) |
8 | | seqex 10350 |
. . . . . . . . . . 11
⊢ seq𝑀( · , 𝐹) ∈ V |
9 | | vex 2715 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
10 | 8, 9 | breldm 4791 |
. . . . . . . . . 10
⊢ (seq𝑀( · , 𝐹) ⇝ 𝑦 → seq𝑀( · , 𝐹) ∈ dom ⇝ ) |
11 | 7, 10 | syl6bi 162 |
. . . . . . . . 9
⊢ (𝑛 = 𝑀 → (seq𝑛( · , 𝐹) ⇝ 𝑦 → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
12 | 11 | adantld 276 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
13 | | eluzel2 9445 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
14 | 13, 3 | eleq2s 2252 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ 𝑍 → 𝑀 ∈ ℤ) |
15 | 14 | ad3antlr 485 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → 𝑀 ∈ ℤ) |
16 | | ntrivcvg.3 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
17 | 16 | ad5ant15 513 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
18 | 3, 15, 17 | prodf 11439 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹):𝑍⟶ℂ) |
19 | | simplr 520 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → (𝑛 − 1) ∈ 𝑍) |
20 | 18, 19 | ffvelrnd 5604 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → (seq𝑀( · , 𝐹)‘(𝑛 − 1)) ∈ ℂ) |
21 | | climcl 11183 |
. . . . . . . . . . . . . 14
⊢ (seq𝑛( · , 𝐹) ⇝ 𝑦 → 𝑦 ∈ ℂ) |
22 | 21 | adantl 275 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → 𝑦 ∈ ℂ) |
23 | 20, 22 | mulcld 7899 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → ((seq𝑀( · , 𝐹)‘(𝑛 − 1)) · 𝑦) ∈ ℂ) |
24 | | uzssz 9459 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
25 | 3, 24 | eqsstri 3160 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑍 ⊆
ℤ |
26 | | simplr 520 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → 𝑛 ∈ 𝑍) |
27 | 25, 26 | sseldi 3126 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → 𝑛 ∈ ℤ) |
28 | 27 | zcnd 9288 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → 𝑛 ∈ ℂ) |
29 | | 1cnd 7895 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → 1 ∈ ℂ) |
30 | 28, 29 | npcand 8191 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → ((𝑛 − 1) + 1) = 𝑛) |
31 | 30 | seqeq1d 10354 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → seq((𝑛 − 1) + 1)( · , 𝐹) = seq𝑛( · , 𝐹)) |
32 | 31 | breq1d 3976 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) → (seq((𝑛 − 1) + 1)( · , 𝐹) ⇝ 𝑦 ↔ seq𝑛( · , 𝐹) ⇝ 𝑦)) |
33 | 32 | biimpar 295 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq((𝑛 − 1) + 1)( · , 𝐹) ⇝ 𝑦) |
34 | 3, 19, 17, 33 | clim2prod 11440 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ⇝ ((seq𝑀( · , 𝐹)‘(𝑛 − 1)) · 𝑦)) |
35 | | breldmg 4793 |
. . . . . . . . . . . 12
⊢
((seq𝑀( · ,
𝐹) ∈ V ∧
((seq𝑀( · , 𝐹)‘(𝑛 − 1)) · 𝑦) ∈ ℂ ∧ seq𝑀( · , 𝐹) ⇝ ((seq𝑀( · , 𝐹)‘(𝑛 − 1)) · 𝑦)) → seq𝑀( · , 𝐹) ∈ dom ⇝ ) |
36 | 8, 23, 34, 35 | mp3an2i 1324 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ (𝑛 − 1) ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ ) |
37 | 36 | an32s 558 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ (𝑛 − 1) ∈ 𝑍) → seq𝑀( · , 𝐹) ∈ dom ⇝ ) |
38 | 37 | expcom 115 |
. . . . . . . . 9
⊢ ((𝑛 − 1) ∈ 𝑍 → (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
39 | 3 | eqcomi 2161 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) = 𝑍 |
40 | 38, 39 | eleq2s 2252 |
. . . . . . . 8
⊢ ((𝑛 − 1) ∈
(ℤ≥‘𝑀) → (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
41 | 12, 40 | jaoi 706 |
. . . . . . 7
⊢ ((𝑛 = 𝑀 ∨ (𝑛 − 1) ∈
(ℤ≥‘𝑀)) → (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
42 | 5, 41 | mpcom 36 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ ) |
43 | 42 | ex 114 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (seq𝑛( · , 𝐹) ⇝ 𝑦 → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
44 | 43 | adantld 276 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
45 | 44 | exlimdv 1799 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
46 | 45 | rexlimdva 2574 |
. 2
⊢ (𝜑 → (∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) → seq𝑀( · , 𝐹) ∈ dom ⇝ )) |
47 | 1, 46 | mpd 13 |
1
⊢ (𝜑 → seq𝑀( · , 𝐹) ∈ dom ⇝ ) |