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 sseldi ( 𝐴 ∈ ( 𝔸 ∖ { 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 ) ) )