Step | Hyp | Ref
| Expression |
1 | | aasscn 23877 |
. . . 4
⊢ 𝔸
⊆ ℂ |
2 | | eldifi 3694 |
. . . 4
⊢ (𝐴 ∈ (𝔸 ∖ {0})
→ 𝐴 ∈
𝔸) |
3 | 1, 2 | sseldi 3566 |
. . 3
⊢ (𝐴 ∈ (𝔸 ∖ {0})
→ 𝐴 ∈
ℂ) |
4 | | elaa 23875 |
. . . . . 6
⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧
∃𝑔 ∈
((Poly‘ℤ) ∖ {0𝑝})(𝑔‘𝐴) = 0)) |
5 | 2, 4 | sylib 207 |
. . . . 5
⊢ (𝐴 ∈ (𝔸 ∖ {0})
→ (𝐴 ∈ ℂ
∧ ∃𝑔 ∈
((Poly‘ℤ) ∖ {0𝑝})(𝑔‘𝐴) = 0)) |
6 | 5 | simprd 478 |
. . . 4
⊢ (𝐴 ∈ (𝔸 ∖ {0})
→ ∃𝑔 ∈
((Poly‘ℤ) ∖ {0𝑝})(𝑔‘𝐴) = 0) |
7 | 2 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝐴 ∈ (𝔸 ∖ {0})
∧ 𝑔 ∈
((Poly‘ℤ) ∖ {0𝑝}) ∧ (𝑔‘𝐴) = 0) → 𝐴 ∈ 𝔸) |
8 | | eldifsni 4261 |
. . . . . . 7
⊢ (𝐴 ∈ (𝔸 ∖ {0})
→ 𝐴 ≠
0) |
9 | 8 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝐴 ∈ (𝔸 ∖ {0})
∧ 𝑔 ∈
((Poly‘ℤ) ∖ {0𝑝}) ∧ (𝑔‘𝐴) = 0) → 𝐴 ≠ 0) |
10 | | eldifi 3694 |
. . . . . . 7
⊢ (𝑔 ∈ ((Poly‘ℤ)
∖ {0𝑝}) → 𝑔 ∈
(Poly‘ℤ)) |
11 | 10 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝐴 ∈ (𝔸 ∖ {0})
∧ 𝑔 ∈
((Poly‘ℤ) ∖ {0𝑝}) ∧ (𝑔‘𝐴) = 0) → 𝑔 ∈
(Poly‘ℤ)) |
12 | | eldifsni 4261 |
. . . . . . 7
⊢ (𝑔 ∈ ((Poly‘ℤ)
∖ {0𝑝}) → 𝑔 ≠ 0𝑝) |
13 | 12 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝐴 ∈ (𝔸 ∖ {0})
∧ 𝑔 ∈
((Poly‘ℤ) ∖ {0𝑝}) ∧ (𝑔‘𝐴) = 0) → 𝑔 ≠ 0𝑝) |
14 | | simp3 1056 |
. . . . . 6
⊢ ((𝐴 ∈ (𝔸 ∖ {0})
∧ 𝑔 ∈
((Poly‘ℤ) ∖ {0𝑝}) ∧ (𝑔‘𝐴) = 0) → (𝑔‘𝐴) = 0) |
15 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((coeff‘𝑔)‘𝑚) = ((coeff‘𝑔)‘𝑛)) |
16 | 15 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (((coeff‘𝑔)‘𝑚) ≠ 0 ↔ ((coeff‘𝑔)‘𝑛) ≠ 0)) |
17 | 16 | cbvrabv 3172 |
. . . . . . 7
⊢ {𝑚 ∈ ℕ0
∣ ((coeff‘𝑔)‘𝑚) ≠ 0} = {𝑛 ∈ ℕ0 ∣
((coeff‘𝑔)‘𝑛) ≠ 0} |
18 | 17 | infeq1i 8267 |
. . . . . 6
⊢
inf({𝑚 ∈
ℕ0 ∣ ((coeff‘𝑔)‘𝑚) ≠ 0}, ℝ, < ) = inf({𝑛 ∈ ℕ0
∣ ((coeff‘𝑔)‘𝑛) ≠ 0}, ℝ, < ) |
19 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (𝑗 + inf({𝑚 ∈ ℕ0 ∣
((coeff‘𝑔)‘𝑚) ≠ 0}, ℝ, < )) = (𝑘 + inf({𝑚 ∈ ℕ0 ∣
((coeff‘𝑔)‘𝑚) ≠ 0}, ℝ, < ))) |
20 | 19 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → ((coeff‘𝑔)‘(𝑗 + inf({𝑚 ∈ ℕ0 ∣
((coeff‘𝑔)‘𝑚) ≠ 0}, ℝ, < ))) =
((coeff‘𝑔)‘(𝑘 + inf({𝑚 ∈ ℕ0 ∣
((coeff‘𝑔)‘𝑚) ≠ 0}, ℝ, <
)))) |
21 | 20 | cbvmptv 4678 |
. . . . . 6
⊢ (𝑗 ∈ ℕ0
↦ ((coeff‘𝑔)‘(𝑗 + inf({𝑚 ∈ ℕ0 ∣
((coeff‘𝑔)‘𝑚) ≠ 0}, ℝ, < )))) = (𝑘 ∈ ℕ0
↦ ((coeff‘𝑔)‘(𝑘 + inf({𝑚 ∈ ℕ0 ∣
((coeff‘𝑔)‘𝑚) ≠ 0}, ℝ, <
)))) |
22 | | eqid 2610 |
. . . . . 6
⊢ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈
(0...((deg‘𝑔) −
inf({𝑚 ∈
ℕ0 ∣ ((coeff‘𝑔)‘𝑚) ≠ 0}, ℝ, < )))(((𝑗 ∈ ℕ0
↦ ((coeff‘𝑔)‘(𝑗 + inf({𝑚 ∈ ℕ0 ∣
((coeff‘𝑔)‘𝑚) ≠ 0}, ℝ, < ))))‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝑔) − inf({𝑚 ∈ ℕ0
∣ ((coeff‘𝑔)‘𝑚) ≠ 0}, ℝ, < )))(((𝑗 ∈ ℕ0
↦ ((coeff‘𝑔)‘(𝑗 + inf({𝑚 ∈ ℕ0 ∣
((coeff‘𝑔)‘𝑚) ≠ 0}, ℝ, < ))))‘𝑘) · (𝑧↑𝑘))) |
23 | 7, 9, 11, 13, 14, 18, 21, 22 | elaa2lem 39126 |
. . . . 5
⊢ ((𝐴 ∈ (𝔸 ∖ {0})
∧ 𝑔 ∈
((Poly‘ℤ) ∖ {0𝑝}) ∧ (𝑔‘𝐴) = 0) → ∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) |
24 | 23 | rexlimdv3a 3015 |
. . . 4
⊢ (𝐴 ∈ (𝔸 ∖ {0})
→ (∃𝑔 ∈
((Poly‘ℤ) ∖ {0𝑝})(𝑔‘𝐴) = 0 → ∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0))) |
25 | 6, 24 | mpd 15 |
. . 3
⊢ (𝐴 ∈ (𝔸 ∖ {0})
→ ∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) |
26 | 3, 25 | jca 553 |
. 2
⊢ (𝐴 ∈ (𝔸 ∖ {0})
→ (𝐴 ∈ ℂ
∧ ∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0))) |
27 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (Poly‘ℤ)
∧ ((coeff‘𝑓)‘0) ≠ 0) → 𝑓 ∈
(Poly‘ℤ)) |
28 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 0𝑝 →
(coeff‘𝑓) =
(coeff‘0𝑝)) |
29 | | coe0 23816 |
. . . . . . . . . . . . . . 15
⊢
(coeff‘0𝑝) = (ℕ0 ×
{0}) |
30 | 28, 29 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 0𝑝 →
(coeff‘𝑓) =
(ℕ0 × {0})) |
31 | 30 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 0𝑝 →
((coeff‘𝑓)‘0) =
((ℕ0 × {0})‘0)) |
32 | | 0nn0 11184 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
33 | | fvconst2g 6372 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℕ0 ∧ 0 ∈ ℕ0) →
((ℕ0 × {0})‘0) = 0) |
34 | 32, 32, 33 | mp2an 704 |
. . . . . . . . . . . . 13
⊢
((ℕ0 × {0})‘0) = 0 |
35 | 31, 34 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝑓 = 0𝑝 →
((coeff‘𝑓)‘0) =
0) |
36 | 35 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ (Poly‘ℤ)
∧ ((coeff‘𝑓)‘0) ≠ 0) ∧ 𝑓 = 0𝑝) →
((coeff‘𝑓)‘0) =
0) |
37 | | neneq 2788 |
. . . . . . . . . . . 12
⊢
(((coeff‘𝑓)‘0) ≠ 0 → ¬
((coeff‘𝑓)‘0) =
0) |
38 | 37 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ (Poly‘ℤ)
∧ ((coeff‘𝑓)‘0) ≠ 0) ∧ 𝑓 = 0𝑝) → ¬
((coeff‘𝑓)‘0) =
0) |
39 | 36, 38 | pm2.65da 598 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (Poly‘ℤ)
∧ ((coeff‘𝑓)‘0) ≠ 0) → ¬ 𝑓 =
0𝑝) |
40 | | velsn 4141 |
. . . . . . . . . 10
⊢ (𝑓 ∈ {0𝑝}
↔ 𝑓 =
0𝑝) |
41 | 39, 40 | sylnibr 318 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (Poly‘ℤ)
∧ ((coeff‘𝑓)‘0) ≠ 0) → ¬ 𝑓 ∈
{0𝑝}) |
42 | 27, 41 | eldifd 3551 |
. . . . . . . 8
⊢ ((𝑓 ∈ (Poly‘ℤ)
∧ ((coeff‘𝑓)‘0) ≠ 0) → 𝑓 ∈ ((Poly‘ℤ) ∖
{0𝑝})) |
43 | 42 | adantrr 749 |
. . . . . . 7
⊢ ((𝑓 ∈ (Poly‘ℤ)
∧ (((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) → 𝑓 ∈ ((Poly‘ℤ) ∖
{0𝑝})) |
44 | | simprr 792 |
. . . . . . 7
⊢ ((𝑓 ∈ (Poly‘ℤ)
∧ (((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) → (𝑓‘𝐴) = 0) |
45 | 43, 44 | jca 553 |
. . . . . 6
⊢ ((𝑓 ∈ (Poly‘ℤ)
∧ (((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) → (𝑓 ∈ ((Poly‘ℤ) ∖
{0𝑝}) ∧ (𝑓‘𝐴) = 0)) |
46 | 45 | reximi2 2993 |
. . . . 5
⊢
(∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0) → ∃𝑓 ∈ ((Poly‘ℤ) ∖
{0𝑝})(𝑓‘𝐴) = 0) |
47 | 46 | anim2i 591 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) → (𝐴 ∈ ℂ ∧ ∃𝑓 ∈ ((Poly‘ℤ)
∖ {0𝑝})(𝑓‘𝐴) = 0)) |
48 | | elaa 23875 |
. . . 4
⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧
∃𝑓 ∈
((Poly‘ℤ) ∖ {0𝑝})(𝑓‘𝐴) = 0)) |
49 | 47, 48 | sylibr 223 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) → 𝐴 ∈ 𝔸) |
50 | | simpr 476 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) → ∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) |
51 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑓 𝐴 ∈ ℂ |
52 | | nfre1 2988 |
. . . . . 6
⊢
Ⅎ𝑓∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0) |
53 | 51, 52 | nfan 1816 |
. . . . 5
⊢
Ⅎ𝑓(𝐴 ∈ ℂ ∧
∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) |
54 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑓 ¬ 𝐴 ∈ {0} |
55 | | simpl3r 1110 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑓 ∈ (Poly‘ℤ)
∧ (((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) ∧ 𝐴 = 0) → (𝑓‘𝐴) = 0) |
56 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 = 0 → (𝑓‘𝐴) = (𝑓‘0)) |
57 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(coeff‘𝑓) =
(coeff‘𝑓) |
58 | 57 | coefv0 23808 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (Poly‘ℤ)
→ (𝑓‘0) =
((coeff‘𝑓)‘0)) |
59 | 56, 58 | sylan9eqr 2666 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ (Poly‘ℤ)
∧ 𝐴 = 0) → (𝑓‘𝐴) = ((coeff‘𝑓)‘0)) |
60 | 59 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ (Poly‘ℤ)
∧ ((coeff‘𝑓)‘0) ≠ 0) ∧ 𝐴 = 0) → (𝑓‘𝐴) = ((coeff‘𝑓)‘0)) |
61 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ (Poly‘ℤ)
∧ ((coeff‘𝑓)‘0) ≠ 0) ∧ 𝐴 = 0) → ((coeff‘𝑓)‘0) ≠
0) |
62 | 60, 61 | eqnetrd 2849 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (Poly‘ℤ)
∧ ((coeff‘𝑓)‘0) ≠ 0) ∧ 𝐴 = 0) → (𝑓‘𝐴) ≠ 0) |
63 | 62 | neneqd 2787 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ (Poly‘ℤ)
∧ ((coeff‘𝑓)‘0) ≠ 0) ∧ 𝐴 = 0) → ¬ (𝑓‘𝐴) = 0) |
64 | 63 | adantlrr 753 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ (Poly‘ℤ)
∧ (((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) ∧ 𝐴 = 0) → ¬ (𝑓‘𝐴) = 0) |
65 | 64 | 3adantl1 1210 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑓 ∈ (Poly‘ℤ)
∧ (((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) ∧ 𝐴 = 0) → ¬ (𝑓‘𝐴) = 0) |
66 | 55, 65 | pm2.65da 598 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑓 ∈ (Poly‘ℤ)
∧ (((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) → ¬ 𝐴 = 0) |
67 | | elsng 4139 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ {0} ↔ 𝐴 = 0)) |
68 | 67 | biimpa 500 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ∈ {0}) → 𝐴 = 0) |
69 | 68 | 3ad2antl1 1216 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑓 ∈ (Poly‘ℤ)
∧ (((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) ∧ 𝐴 ∈ {0}) → 𝐴 = 0) |
70 | 66, 69 | mtand 689 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑓 ∈ (Poly‘ℤ)
∧ (((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) → ¬ 𝐴 ∈ {0}) |
71 | 70 | 3exp 1256 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝑓 ∈ (Poly‘ℤ)
→ ((((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0) → ¬ 𝐴 ∈ {0}))) |
72 | 71 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) → (𝑓 ∈ (Poly‘ℤ) →
((((coeff‘𝑓)‘0)
≠ 0 ∧ (𝑓‘𝐴) = 0) → ¬ 𝐴 ∈ {0}))) |
73 | 53, 54, 72 | rexlimd 3008 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) → (∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0) → ¬ 𝐴 ∈ {0})) |
74 | 50, 73 | mpd 15 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) → ¬ 𝐴 ∈ {0}) |
75 | 49, 74 | eldifd 3551 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) → 𝐴 ∈ (𝔸 ∖
{0})) |
76 | 26, 75 | impbii 198 |
1
⊢ (𝐴 ∈ (𝔸 ∖ {0})
↔ (𝐴 ∈ ℂ
∧ ∃𝑓 ∈
(Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0))) |