Step | Hyp | Ref
| Expression |
1 | | ntrivcvgfvn0.4 |
. 2
⊢ (𝜑 → 𝑋 ≠ 0) |
2 | | fclim 14284 |
. . . . . . . 8
⊢ ⇝
:dom ⇝ ⟶ℂ |
3 | | ffun 6048 |
. . . . . . . 8
⊢ ( ⇝
:dom ⇝ ⟶ℂ → Fun ⇝ ) |
4 | 2, 3 | ax-mp 5 |
. . . . . . 7
⊢ Fun
⇝ |
5 | | ntrivcvgfvn0.3 |
. . . . . . 7
⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝑋) |
6 | | funbrfv 6234 |
. . . . . . 7
⊢ (Fun
⇝ → (seq𝑀(
· , 𝐹) ⇝ 𝑋 → ( ⇝
‘seq𝑀( · ,
𝐹)) = 𝑋)) |
7 | 4, 5, 6 | mpsyl 68 |
. . . . . 6
⊢ (𝜑 → ( ⇝ ‘seq𝑀( · , 𝐹)) = 𝑋) |
8 | 7 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → ( ⇝ ‘seq𝑀( · , 𝐹)) = 𝑋) |
9 | | eqid 2622 |
. . . . . . 7
⊢
(ℤ≥‘𝑁) = (ℤ≥‘𝑁) |
10 | | ntrivcvgfvn0.1 |
. . . . . . . . . 10
⊢ 𝑍 =
(ℤ≥‘𝑀) |
11 | | uzssz 11707 |
. . . . . . . . . 10
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
12 | 10, 11 | eqsstri 3635 |
. . . . . . . . 9
⊢ 𝑍 ⊆
ℤ |
13 | | ntrivcvgfvn0.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
14 | 12, 13 | sseldi 3601 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℤ) |
15 | 14 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → 𝑁 ∈ ℤ) |
16 | | seqex 12803 |
. . . . . . . 8
⊢ seq𝑀( · , 𝐹) ∈ V |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → seq𝑀( · , 𝐹) ∈ V) |
18 | | 0cnd 10033 |
. . . . . . 7
⊢ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → 0 ∈
ℂ) |
19 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑁 → (seq𝑀( · , 𝐹)‘𝑚) = (seq𝑀( · , 𝐹)‘𝑁)) |
20 | 19 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑁 → ((seq𝑀( · , 𝐹)‘𝑚) = 0 ↔ (seq𝑀( · , 𝐹)‘𝑁) = 0)) |
21 | 20 | imbi2d 330 |
. . . . . . . . 9
⊢ (𝑚 = 𝑁 → (((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑚) = 0) ↔ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑁) = 0))) |
22 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (seq𝑀( · , 𝐹)‘𝑚) = (seq𝑀( · , 𝐹)‘𝑛)) |
23 | 22 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((seq𝑀( · , 𝐹)‘𝑚) = 0 ↔ (seq𝑀( · , 𝐹)‘𝑛) = 0)) |
24 | 23 | imbi2d 330 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑚) = 0) ↔ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑛) = 0))) |
25 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → (seq𝑀( · , 𝐹)‘𝑚) = (seq𝑀( · , 𝐹)‘(𝑛 + 1))) |
26 | 25 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → ((seq𝑀( · , 𝐹)‘𝑚) = 0 ↔ (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = 0)) |
27 | 26 | imbi2d 330 |
. . . . . . . . 9
⊢ (𝑚 = (𝑛 + 1) → (((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑚) = 0) ↔ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = 0))) |
28 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → (seq𝑀( · , 𝐹)‘𝑚) = (seq𝑀( · , 𝐹)‘𝑘)) |
29 | 28 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑘 → ((seq𝑀( · , 𝐹)‘𝑚) = 0 ↔ (seq𝑀( · , 𝐹)‘𝑘) = 0)) |
30 | 29 | imbi2d 330 |
. . . . . . . . 9
⊢ (𝑚 = 𝑘 → (((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑚) = 0) ↔ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑘) = 0))) |
31 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑁) = 0) |
32 | 31 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑁) = 0)) |
33 | 13, 10 | syl6eleq 2711 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
34 | | uztrn 11704 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → 𝑛 ∈ (ℤ≥‘𝑀)) |
35 | 33, 34 | sylan2 491 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝜑) → 𝑛 ∈ (ℤ≥‘𝑀)) |
36 | 35 | 3adant3 1081 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑛) = 0) → 𝑛 ∈ (ℤ≥‘𝑀)) |
37 | | seqp1 12816 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1)))) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑛) = 0) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1)))) |
39 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢
((seq𝑀( · ,
𝐹)‘𝑛) = 0 → ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))) = (0 · (𝐹‘(𝑛 + 1)))) |
40 | 39 | 3ad2ant3 1084 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑛) = 0) → ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))) = (0 · (𝐹‘(𝑛 + 1)))) |
41 | | peano2uz 11741 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘𝑁) → (𝑛 + 1) ∈
(ℤ≥‘𝑁)) |
42 | 10 | uztrn2 11705 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ 𝑍 ∧ (𝑛 + 1) ∈
(ℤ≥‘𝑁)) → (𝑛 + 1) ∈ 𝑍) |
43 | 13, 41, 42 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑛 + 1) ∈ 𝑍) |
44 | | ntrivcvgfvn0.5 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
45 | 44 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ∈ ℂ) |
46 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) |
47 | 46 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘(𝑛 + 1)) ∈ ℂ)) |
48 | 47 | rspcv 3305 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 + 1) ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ∈ ℂ → (𝐹‘(𝑛 + 1)) ∈ ℂ)) |
49 | 45, 48 | mpan9 486 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑛 + 1) ∈ 𝑍) → (𝐹‘(𝑛 + 1)) ∈ ℂ) |
50 | 43, 49 | syldan 487 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐹‘(𝑛 + 1)) ∈ ℂ) |
51 | 50 | ancoms 469 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝜑) → (𝐹‘(𝑛 + 1)) ∈ ℂ) |
52 | 51 | mul02d 10234 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝜑) → (0 · (𝐹‘(𝑛 + 1))) = 0) |
53 | 52 | 3adant3 1081 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑛) = 0) → (0 · (𝐹‘(𝑛 + 1))) = 0) |
54 | 38, 40, 53 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘𝑁) ∧ 𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑛) = 0) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = 0) |
55 | 54 | 3exp 1264 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘𝑁) → (𝜑 → ((seq𝑀( · , 𝐹)‘𝑛) = 0 → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = 0))) |
56 | 55 | adantrd 484 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(ℤ≥‘𝑁) → ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → ((seq𝑀( · , 𝐹)‘𝑛) = 0 → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = 0))) |
57 | 56 | a2d 29 |
. . . . . . . . 9
⊢ (𝑛 ∈
(ℤ≥‘𝑁) → (((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑛) = 0) → ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = 0))) |
58 | 21, 24, 27, 30, 32, 57 | uzind4 11746 |
. . . . . . . 8
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑘) = 0)) |
59 | 58 | impcom 446 |
. . . . . . 7
⊢ (((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (seq𝑀( · , 𝐹)‘𝑘) = 0) |
60 | 9, 15, 17, 18, 59 | climconst 14274 |
. . . . . 6
⊢ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → seq𝑀( · , 𝐹) ⇝ 0) |
61 | | funbrfv 6234 |
. . . . . 6
⊢ (Fun
⇝ → (seq𝑀(
· , 𝐹) ⇝ 0
→ ( ⇝ ‘seq𝑀( · , 𝐹)) = 0)) |
62 | 4, 60, 61 | mpsyl 68 |
. . . . 5
⊢ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → ( ⇝ ‘seq𝑀( · , 𝐹)) = 0) |
63 | 8, 62 | eqtr3d 2658 |
. . . 4
⊢ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → 𝑋 = 0) |
64 | 63 | ex 450 |
. . 3
⊢ (𝜑 → ((seq𝑀( · , 𝐹)‘𝑁) = 0 → 𝑋 = 0)) |
65 | 64 | necon3d 2815 |
. 2
⊢ (𝜑 → (𝑋 ≠ 0 → (seq𝑀( · , 𝐹)‘𝑁) ≠ 0)) |
66 | 1, 65 | mpd 15 |
1
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ≠ 0) |