Metamath Proof Explorer

Theorem elaa2

Description: Elementhood in the set of nonzero algebraic numbers: when A is nonzero, the polynomial f can be chosen with a nonzero constant term. (Contributed by Glauco Siliprandi, 5-Apr-2020) (Proof shortened by AV, 1-Oct-2020)

Ref Expression
Assertion elaa2 ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 aasscn ⊢ 𝔸 ⊆ ℂ
2 eldifi ⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) → 𝐴 ∈ 𝔸 )
3 1 2 sselid ⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) → 𝐴 ∈ ℂ )
4 elaa ⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑔 ‘ 𝐴 ) = 0 ) )
5 2 4 sylib ⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) → ( 𝐴 ∈ ℂ ∧ ∃ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑔 ‘ 𝐴 ) = 0 ) )
6 5 simprd ⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) → ∃ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑔 ‘ 𝐴 ) = 0 )
7 2 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) ∧ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ 𝐴 ) = 0 ) → 𝐴 ∈ 𝔸 )
8 eldifsni ⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) → 𝐴 ≠ 0 )
9 8 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) ∧ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ 𝐴 ) = 0 ) → 𝐴 ≠ 0 )
10 eldifi ⊢ ( 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) → 𝑔 ∈ ( Poly ‘ ℤ ) )
11 10 3ad2ant2 ⊢ ( ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) ∧ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ 𝐴 ) = 0 ) → 𝑔 ∈ ( Poly ‘ ℤ ) )
12 eldifsni ⊢ ( 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) → 𝑔 ≠ 0𝑝 )
13 12 3ad2ant2 ⊢ ( ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) ∧ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ 𝐴 ) = 0 ) → 𝑔 ≠ 0𝑝 )
14 simp3 ⊢ ( ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) ∧ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ 𝐴 ) = 0 ) → ( 𝑔 ‘ 𝐴 ) = 0 )
15 fveq2 ⊢ ( 𝑚 = 𝑛 → ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) = ( ( coeff ‘ 𝑔 ) ‘ 𝑛 ) )
16 15 neeq1d ⊢ ( 𝑚 = 𝑛 → ( ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 ↔ ( ( coeff ‘ 𝑔 ) ‘ 𝑛 ) ≠ 0 ) )
17 16 cbvrabv ⊢ { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } = { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑛 ) ≠ 0 }
18 17 infeq1i ⊢ inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) = inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < )
19 fvoveq1 ⊢ ( 𝑗 = 𝑘 → ( ( coeff ‘ 𝑔 ) ‘ ( 𝑗 + inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) ) ) = ( ( coeff ‘ 𝑔 ) ‘ ( 𝑘 + inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) ) ) )
20 19 cbvmptv ⊢ ( 𝑗 ∈ ℕ0 ↦ ( ( coeff ‘ 𝑔 ) ‘ ( 𝑗 + inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( coeff ‘ 𝑔 ) ‘ ( 𝑘 + inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) ) ) )
21 eqid ⊢ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝑔 ) − inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) ) ) ( ( ( 𝑗 ∈ ℕ0 ↦ ( ( coeff ‘ 𝑔 ) ‘ ( 𝑗 + inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) ) ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝑔 ) − inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) ) ) ( ( ( 𝑗 ∈ ℕ0 ↦ ( ( coeff ‘ 𝑔 ) ‘ ( 𝑗 + inf ( { 𝑚 ∈ ℕ0 ∣ ( ( coeff ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 } , ℝ , < ) ) ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
22 7 9 11 13 14 18 20 21 elaa2lem ⊢ ( ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) ∧ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ 𝐴 ) = 0 ) → ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) )
23 22 rexlimdv3a ⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) → ( ∃ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑔 ‘ 𝐴 ) = 0 → ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) )
24 6 23 mpd ⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) → ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) )
25 3 24 jca ⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) → ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) )
26 simpl ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) → 𝑓 ∈ ( Poly ‘ ℤ ) )
27 fveq2 ⊢ ( 𝑓 = 0𝑝 → ( coeff ‘ 𝑓 ) = ( coeff ‘ 0𝑝 ) )
28 coe0 ⊢ ( coeff ‘ 0𝑝 ) = ( ℕ0 × { 0 } )
29 27 28 eqtrdi ⊢ ( 𝑓 = 0𝑝 → ( coeff ‘ 𝑓 ) = ( ℕ0 × { 0 } ) )
30 29 fveq1d ⊢ ( 𝑓 = 0𝑝 → ( ( coeff ‘ 𝑓 ) ‘ 0 ) = ( ( ℕ0 × { 0 } ) ‘ 0 ) )
31 0nn0 ⊢ 0 ∈ ℕ0
32 fvconst2g ⊢ ( ( 0 ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → ( ( ℕ0 × { 0 } ) ‘ 0 ) = 0 )
33 31 31 32 mp2an ⊢ ( ( ℕ0 × { 0 } ) ‘ 0 ) = 0
34 30 33 eqtrdi ⊢ ( 𝑓 = 0𝑝 → ( ( coeff ‘ 𝑓 ) ‘ 0 ) = 0 )
35 34 adantl ⊢ ( ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) ∧ 𝑓 = 0𝑝 ) → ( ( coeff ‘ 𝑓 ) ‘ 0 ) = 0 )
36 neneq ⊢ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 → ¬ ( ( coeff ‘ 𝑓 ) ‘ 0 ) = 0 )
37 36 ad2antlr ⊢ ( ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) ∧ 𝑓 = 0𝑝 ) → ¬ ( ( coeff ‘ 𝑓 ) ‘ 0 ) = 0 )
38 35 37 pm2.65da ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) → ¬ 𝑓 = 0𝑝 )
39 velsn ⊢ ( 𝑓 ∈ { 0𝑝 } ↔ 𝑓 = 0𝑝 )
40 38 39 sylnibr ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) → ¬ 𝑓 ∈ { 0𝑝 } )
41 26 40 eldifd ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) → 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) )
42 41 adantrr ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) )
43 simprr ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝑓 ‘ 𝐴 ) = 0 )
44 42 43 jca ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) )
45 44 reximi2 ⊢ ( ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) → ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 )
46 45 anim2i ⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) )
47 elaa ⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) )
48 46 47 sylibr ⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → 𝐴 ∈ 𝔸 )
49 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) )
50 nfv ⊢ Ⅎ 𝑓 𝐴 ∈ ℂ
51 nfre1 ⊢ Ⅎ 𝑓 ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 )
52 50 51 nfan ⊢ Ⅎ 𝑓 ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) )
53 nfv ⊢ Ⅎ 𝑓 ¬ 𝐴 ∈ { 0 }
54 simpl3r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝐴 = 0 ) → ( 𝑓 ‘ 𝐴 ) = 0 )
55 fveq2 ⊢ ( 𝐴 = 0 → ( 𝑓 ‘ 𝐴 ) = ( 𝑓 ‘ 0 ) )
56 eqid ⊢ ( coeff ‘ 𝑓 ) = ( coeff ‘ 𝑓 )
57 56 coefv0 ⊢ ( 𝑓 ∈ ( Poly ‘ ℤ ) → ( 𝑓 ‘ 0 ) = ( ( coeff ‘ 𝑓 ) ‘ 0 ) )
58 55 57 sylan9eqr ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ 𝐴 = 0 ) → ( 𝑓 ‘ 𝐴 ) = ( ( coeff ‘ 𝑓 ) ‘ 0 ) )
59 58 adantlr ⊢ ( ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) ∧ 𝐴 = 0 ) → ( 𝑓 ‘ 𝐴 ) = ( ( coeff ‘ 𝑓 ) ‘ 0 ) )
60 simplr ⊢ ( ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) ∧ 𝐴 = 0 ) → ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 )
61 59 60 eqnetrd ⊢ ( ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) ∧ 𝐴 = 0 ) → ( 𝑓 ‘ 𝐴 ) ≠ 0 )
62 61 neneqd ⊢ ( ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ) ∧ 𝐴 = 0 ) → ¬ ( 𝑓 ‘ 𝐴 ) = 0 )
63 62 adantlrr ⊢ ( ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝐴 = 0 ) → ¬ ( 𝑓 ‘ 𝐴 ) = 0 )
64 63 3adantl1 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝐴 = 0 ) → ¬ ( 𝑓 ‘ 𝐴 ) = 0 )
65 54 64 pm2.65da ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ¬ 𝐴 = 0 )
66 elsng ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ { 0 } ↔ 𝐴 = 0 ) )
67 66 biimpa ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ { 0 } ) → 𝐴 = 0 )
68 67 3ad2antl1 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝐴 ∈ { 0 } ) → 𝐴 = 0 )
69 65 68 mtand ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ¬ 𝐴 ∈ { 0 } )
70 69 3exp ⊢ ( 𝐴 ∈ ℂ → ( 𝑓 ∈ ( Poly ‘ ℤ ) → ( ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) → ¬ 𝐴 ∈ { 0 } ) ) )
71 70 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝑓 ∈ ( Poly ‘ ℤ ) → ( ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) → ¬ 𝐴 ∈ { 0 } ) ) )
72 52 53 71 rexlimd ⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) → ¬ 𝐴 ∈ { 0 } ) )
73 49 72 mpd ⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ¬ 𝐴 ∈ { 0 } )
74 48 73 eldifd ⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → 𝐴 ∈ ( 𝔸 ∖ { 0 } ) )
75 25 74 impbii ⊢ ( 𝐴 ∈ ( 𝔸 ∖ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) )