Step | Hyp | Ref
| Expression |
1 | | fveq2 5198 |
. . . . . 6
⊢ (𝑛 = 1 → (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑛) = (seq1(
· , (ℕ × {𝐴}), ℂ)‘1)) |
2 | 1 | breq1d 3795 |
. . . . 5
⊢ (𝑛 = 1 → ((seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑛) # 0
↔ (seq1( · , (ℕ × {𝐴}), ℂ)‘1) # 0)) |
3 | 2 | imbi2d 228 |
. . . 4
⊢ (𝑛 = 1 → (((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (seq1( · , (ℕ
× {𝐴}),
ℂ)‘𝑛) # 0)
↔ ((𝐴 ∈ ℂ
∧ 𝐴 # 0) → (seq1(
· , (ℕ × {𝐴}), ℂ)‘1) #
0))) |
4 | | fveq2 5198 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (seq1( · , (ℕ ×
{𝐴}), ℂ)‘𝑛) = (seq1( · , (ℕ
× {𝐴}),
ℂ)‘𝑘)) |
5 | 4 | breq1d 3795 |
. . . . 5
⊢ (𝑛 = 𝑘 → ((seq1( · , (ℕ ×
{𝐴}), ℂ)‘𝑛) # 0 ↔ (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑘) #
0)) |
6 | 5 | imbi2d 228 |
. . . 4
⊢ (𝑛 = 𝑘 → (((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (seq1( · , (ℕ
× {𝐴}),
ℂ)‘𝑛) # 0)
↔ ((𝐴 ∈ ℂ
∧ 𝐴 # 0) → (seq1(
· , (ℕ × {𝐴}), ℂ)‘𝑘) # 0))) |
7 | | fveq2 5198 |
. . . . . 6
⊢ (𝑛 = (𝑘 + 1) → (seq1( · , (ℕ
× {𝐴}),
ℂ)‘𝑛) = (seq1(
· , (ℕ × {𝐴}), ℂ)‘(𝑘 + 1))) |
8 | 7 | breq1d 3795 |
. . . . 5
⊢ (𝑛 = (𝑘 + 1) → ((seq1( · , (ℕ
× {𝐴}),
ℂ)‘𝑛) # 0
↔ (seq1( · , (ℕ × {𝐴}), ℂ)‘(𝑘 + 1)) # 0)) |
9 | 8 | imbi2d 228 |
. . . 4
⊢ (𝑛 = (𝑘 + 1) → (((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (seq1( · , (ℕ
× {𝐴}),
ℂ)‘𝑛) # 0)
↔ ((𝐴 ∈ ℂ
∧ 𝐴 # 0) → (seq1(
· , (ℕ × {𝐴}), ℂ)‘(𝑘 + 1)) # 0))) |
10 | | fveq2 5198 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (seq1( · , (ℕ ×
{𝐴}), ℂ)‘𝑛) = (seq1( · , (ℕ
× {𝐴}),
ℂ)‘𝑁)) |
11 | 10 | breq1d 3795 |
. . . . 5
⊢ (𝑛 = 𝑁 → ((seq1( · , (ℕ ×
{𝐴}), ℂ)‘𝑛) # 0 ↔ (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑁) #
0)) |
12 | 11 | imbi2d 228 |
. . . 4
⊢ (𝑛 = 𝑁 → (((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (seq1( · , (ℕ
× {𝐴}),
ℂ)‘𝑛) # 0)
↔ ((𝐴 ∈ ℂ
∧ 𝐴 # 0) → (seq1(
· , (ℕ × {𝐴}), ℂ)‘𝑁) # 0))) |
13 | | simpr 108 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → 𝐴 # 0) |
14 | | 1zzd 8378 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → 1 ∈
ℤ) |
15 | | cnex 7097 |
. . . . . . . . 9
⊢ ℂ
∈ V |
16 | 15 | a1i 9 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → ℂ ∈
V) |
17 | | elnnuz 8655 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ ↔ 𝑥 ∈
(ℤ≥‘1)) |
18 | | fvconst2g 5396 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ) →
((ℕ × {𝐴})‘𝑥) = 𝐴) |
19 | 17, 18 | sylan2br 282 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈
(ℤ≥‘1)) → ((ℕ × {𝐴})‘𝑥) = 𝐴) |
20 | 19 | adantlr 460 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ 𝑥 ∈ (ℤ≥‘1))
→ ((ℕ × {𝐴})‘𝑥) = 𝐴) |
21 | | simpll 495 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ 𝑥 ∈ (ℤ≥‘1))
→ 𝐴 ∈
ℂ) |
22 | 20, 21 | eqeltrd 2155 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ 𝑥 ∈ (ℤ≥‘1))
→ ((ℕ × {𝐴})‘𝑥) ∈ ℂ) |
23 | | mulcl 7100 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
24 | 23 | adantl 271 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) |
25 | 14, 16, 22, 24 | iseq1 9442 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘1) = ((ℕ × {𝐴})‘1)) |
26 | | 1nn 8050 |
. . . . . . . . 9
⊢ 1 ∈
ℕ |
27 | | fvconst2g 5396 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℕ) → ((ℕ × {𝐴})‘1) = 𝐴) |
28 | 26, 27 | mpan2 415 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((ℕ
× {𝐴})‘1) =
𝐴) |
29 | 28 | adantr 270 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → ((ℕ ×
{𝐴})‘1) = 𝐴) |
30 | 25, 29 | eqtrd 2113 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘1) = 𝐴) |
31 | 30 | breq1d 3795 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → ((seq1( · ,
(ℕ × {𝐴}),
ℂ)‘1) # 0 ↔ 𝐴 # 0)) |
32 | 13, 31 | mpbird 165 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘1) # 0) |
33 | | simpl 107 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) → 𝑘 ∈ ℕ) |
34 | | elnnuz 8655 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈
(ℤ≥‘1)) |
35 | 33, 34 | sylib 120 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) → 𝑘 ∈
(ℤ≥‘1)) |
36 | 35 | adantr 270 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) ∧ (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑘) # 0)
→ 𝑘 ∈
(ℤ≥‘1)) |
37 | 15 | a1i 9 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) ∧ (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑘) # 0)
→ ℂ ∈ V) |
38 | 22 | adantll 459 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) ∧ 𝑥 ∈ (ℤ≥‘1))
→ ((ℕ × {𝐴})‘𝑥) ∈ ℂ) |
39 | 38 | adantlr 460 |
. . . . . . . . 9
⊢ ((((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) ∧ (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑘) # 0)
∧ 𝑥 ∈
(ℤ≥‘1)) → ((ℕ × {𝐴})‘𝑥) ∈ ℂ) |
40 | 23 | adantl 271 |
. . . . . . . . 9
⊢ ((((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) ∧ (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑘) # 0)
∧ (𝑥 ∈ ℂ
∧ 𝑦 ∈ ℂ))
→ (𝑥 · 𝑦) ∈
ℂ) |
41 | 36, 37, 39, 40 | iseqcl 9443 |
. . . . . . . 8
⊢ (((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) ∧ (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑘) # 0)
→ (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑘) ∈ ℂ) |
42 | | simplrl 501 |
. . . . . . . 8
⊢ (((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) ∧ (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑘) # 0)
→ 𝐴 ∈
ℂ) |
43 | | simpr 108 |
. . . . . . . 8
⊢ (((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) ∧ (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑘) # 0)
→ (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑘) # 0) |
44 | | simplrr 502 |
. . . . . . . 8
⊢ (((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) ∧ (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑘) # 0)
→ 𝐴 #
0) |
45 | 41, 42, 43, 44 | mulap0d 7748 |
. . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) ∧ (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑘) # 0)
→ ((seq1( · , (ℕ × {𝐴}), ℂ)‘𝑘) · 𝐴) # 0) |
46 | 15 | a1i 9 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) → ℂ ∈
V) |
47 | 23 | adantl 271 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) |
48 | 35, 46, 38, 47 | iseqp1 9445 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) → (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘(𝑘 + 1)) =
((seq1( · , (ℕ × {𝐴}), ℂ)‘𝑘) · ((ℕ × {𝐴})‘(𝑘 + 1)))) |
49 | | simprl 497 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) → 𝐴 ∈ ℂ) |
50 | 33 | peano2nnd 8054 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) → (𝑘 + 1) ∈
ℕ) |
51 | | fvconst2g 5396 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ (𝑘 + 1) ∈ ℕ) →
((ℕ × {𝐴})‘(𝑘 + 1)) = 𝐴) |
52 | 49, 50, 51 | syl2anc 403 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) → ((ℕ ×
{𝐴})‘(𝑘 + 1)) = 𝐴) |
53 | 52 | oveq2d 5548 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) → ((seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑘) ·
((ℕ × {𝐴})‘(𝑘 + 1))) = ((seq1( · , (ℕ ×
{𝐴}), ℂ)‘𝑘) · 𝐴)) |
54 | 48, 53 | eqtrd 2113 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) → (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘(𝑘 + 1)) =
((seq1( · , (ℕ × {𝐴}), ℂ)‘𝑘) · 𝐴)) |
55 | 54 | breq1d 3795 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) → ((seq1( · ,
(ℕ × {𝐴}),
ℂ)‘(𝑘 + 1)) # 0
↔ ((seq1( · , (ℕ × {𝐴}), ℂ)‘𝑘) · 𝐴) # 0)) |
56 | 55 | adantr 270 |
. . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) ∧ (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑘) # 0)
→ ((seq1( · , (ℕ × {𝐴}), ℂ)‘(𝑘 + 1)) # 0 ↔ ((seq1( · , (ℕ
× {𝐴}),
ℂ)‘𝑘) ·
𝐴) # 0)) |
57 | 45, 56 | mpbird 165 |
. . . . . 6
⊢ (((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐴 # 0)) ∧ (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑘) # 0)
→ (seq1( · , (ℕ × {𝐴}), ℂ)‘(𝑘 + 1)) # 0) |
58 | 57 | exp31 356 |
. . . . 5
⊢ (𝑘 ∈ ℕ → ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → ((seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑘) # 0
→ (seq1( · , (ℕ × {𝐴}), ℂ)‘(𝑘 + 1)) # 0))) |
59 | 58 | a2d 26 |
. . . 4
⊢ (𝑘 ∈ ℕ → (((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑘) # 0)
→ ((𝐴 ∈ ℂ
∧ 𝐴 # 0) → (seq1(
· , (ℕ × {𝐴}), ℂ)‘(𝑘 + 1)) # 0))) |
60 | 3, 6, 9, 12, 32, 59 | nnind 8055 |
. . 3
⊢ (𝑁 ∈ ℕ → ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑁) #
0)) |
61 | 60 | impcom 123 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ 𝑁 ∈ ℕ) → (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑁) #
0) |
62 | 61 | 3impa 1133 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ) → (seq1( · ,
(ℕ × {𝐴}),
ℂ)‘𝑁) #
0) |