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 
|- ( A e. ( AA \ { 0 } ) <-> ( A e. CC /\ E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 aasscn 
 |-  AA C_ CC
2 eldifi 
 |-  ( A e. ( AA \ { 0 } ) -> A e. AA )
3 1 2 sseldi 
 |-  ( A e. ( AA \ { 0 } ) -> A e. CC )
4 elaa 
 |-  ( A e. AA <-> ( A e. CC /\ E. g e. ( ( Poly ` ZZ ) \ { 0p } ) ( g ` A ) = 0 ) )
5 2 4 sylib 
 |-  ( A e. ( AA \ { 0 } ) -> ( A e. CC /\ E. g e. ( ( Poly ` ZZ ) \ { 0p } ) ( g ` A ) = 0 ) )
6 5 simprd 
 |-  ( A e. ( AA \ { 0 } ) -> E. g e. ( ( Poly ` ZZ ) \ { 0p } ) ( g ` A ) = 0 )
7 2 3ad2ant1 
 |-  ( ( A e. ( AA \ { 0 } ) /\ g e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( g ` A ) = 0 ) -> A e. AA )
8 eldifsni 
 |-  ( A e. ( AA \ { 0 } ) -> A =/= 0 )
9 8 3ad2ant1 
 |-  ( ( A e. ( AA \ { 0 } ) /\ g e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( g ` A ) = 0 ) -> A =/= 0 )
10 eldifi 
 |-  ( g e. ( ( Poly ` ZZ ) \ { 0p } ) -> g e. ( Poly ` ZZ ) )
11 10 3ad2ant2 
 |-  ( ( A e. ( AA \ { 0 } ) /\ g e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( g ` A ) = 0 ) -> g e. ( Poly ` ZZ ) )
12 eldifsni 
 |-  ( g e. ( ( Poly ` ZZ ) \ { 0p } ) -> g =/= 0p )
13 12 3ad2ant2 
 |-  ( ( A e. ( AA \ { 0 } ) /\ g e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( g ` A ) = 0 ) -> g =/= 0p )
14 simp3 
 |-  ( ( A e. ( AA \ { 0 } ) /\ g e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( g ` A ) = 0 ) -> ( g ` A ) = 0 )
15 fveq2 
 |-  ( m = n -> ( ( coeff ` g ) ` m ) = ( ( coeff ` g ) ` n ) )
16 15 neeq1d 
 |-  ( m = n -> ( ( ( coeff ` g ) ` m ) =/= 0 <-> ( ( coeff ` g ) ` n ) =/= 0 ) )
17 16 cbvrabv 
 |-  { m e. NN0 | ( ( coeff ` g ) ` m ) =/= 0 } = { n e. NN0 | ( ( coeff ` g ) ` n ) =/= 0 }
18 17 infeq1i 
 |-  inf ( { m e. NN0 | ( ( coeff ` g ) ` m ) =/= 0 } , RR , < ) = inf ( { n e. NN0 | ( ( coeff ` g ) ` n ) =/= 0 } , RR , < )
19 fvoveq1 
 |-  ( j = k -> ( ( coeff ` g ) ` ( j + inf ( { m e. NN0 | ( ( coeff ` g ) ` m ) =/= 0 } , RR , < ) ) ) = ( ( coeff ` g ) ` ( k + inf ( { m e. NN0 | ( ( coeff ` g ) ` m ) =/= 0 } , RR , < ) ) ) )
20 19 cbvmptv 
 |-  ( j e. NN0 |-> ( ( coeff ` g ) ` ( j + inf ( { m e. NN0 | ( ( coeff ` g ) ` m ) =/= 0 } , RR , < ) ) ) ) = ( k e. NN0 |-> ( ( coeff ` g ) ` ( k + inf ( { m e. NN0 | ( ( coeff ` g ) ` m ) =/= 0 } , RR , < ) ) ) )
21 eqid 
 |-  ( z e. CC |-> sum_ k e. ( 0 ... ( ( deg ` g ) - inf ( { m e. NN0 | ( ( coeff ` g ) ` m ) =/= 0 } , RR , < ) ) ) ( ( ( j e. NN0 |-> ( ( coeff ` g ) ` ( j + inf ( { m e. NN0 | ( ( coeff ` g ) ` m ) =/= 0 } , RR , < ) ) ) ) ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... ( ( deg ` g ) - inf ( { m e. NN0 | ( ( coeff ` g ) ` m ) =/= 0 } , RR , < ) ) ) ( ( ( j e. NN0 |-> ( ( coeff ` g ) ` ( j + inf ( { m e. NN0 | ( ( coeff ` g ) ` m ) =/= 0 } , RR , < ) ) ) ) ` k ) x. ( z ^ k ) ) )
22 7 9 11 13 14 18 20 21 elaa2lem 
 |-  ( ( A e. ( AA \ { 0 } ) /\ g e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( g ` A ) = 0 ) -> E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) )
23 22 rexlimdv3a 
 |-  ( A e. ( AA \ { 0 } ) -> ( E. g e. ( ( Poly ` ZZ ) \ { 0p } ) ( g ` A ) = 0 -> E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) )
24 6 23 mpd 
 |-  ( A e. ( AA \ { 0 } ) -> E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) )
25 3 24 jca 
 |-  ( A e. ( AA \ { 0 } ) -> ( A e. CC /\ E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) )
26 simpl 
 |-  ( ( f e. ( Poly ` ZZ ) /\ ( ( coeff ` f ) ` 0 ) =/= 0 ) -> f e. ( Poly ` ZZ ) )
27 fveq2 
 |-  ( f = 0p -> ( coeff ` f ) = ( coeff ` 0p ) )
28 coe0 
 |-  ( coeff ` 0p ) = ( NN0 X. { 0 } )
29 27 28 eqtrdi 
 |-  ( f = 0p -> ( coeff ` f ) = ( NN0 X. { 0 } ) )
30 29 fveq1d 
 |-  ( f = 0p -> ( ( coeff ` f ) ` 0 ) = ( ( NN0 X. { 0 } ) ` 0 ) )
31 0nn0 
 |-  0 e. NN0
32 fvconst2g 
 |-  ( ( 0 e. NN0 /\ 0 e. NN0 ) -> ( ( NN0 X. { 0 } ) ` 0 ) = 0 )
33 31 31 32 mp2an 
 |-  ( ( NN0 X. { 0 } ) ` 0 ) = 0
34 30 33 eqtrdi 
 |-  ( f = 0p -> ( ( coeff ` f ) ` 0 ) = 0 )
35 34 adantl 
 |-  ( ( ( f e. ( Poly ` ZZ ) /\ ( ( coeff ` f ) ` 0 ) =/= 0 ) /\ f = 0p ) -> ( ( coeff ` f ) ` 0 ) = 0 )
36 neneq 
 |-  ( ( ( coeff ` f ) ` 0 ) =/= 0 -> -. ( ( coeff ` f ) ` 0 ) = 0 )
37 36 ad2antlr 
 |-  ( ( ( f e. ( Poly ` ZZ ) /\ ( ( coeff ` f ) ` 0 ) =/= 0 ) /\ f = 0p ) -> -. ( ( coeff ` f ) ` 0 ) = 0 )
38 35 37 pm2.65da 
 |-  ( ( f e. ( Poly ` ZZ ) /\ ( ( coeff ` f ) ` 0 ) =/= 0 ) -> -. f = 0p )
39 velsn 
 |-  ( f e. { 0p } <-> f = 0p )
40 38 39 sylnibr 
 |-  ( ( f e. ( Poly ` ZZ ) /\ ( ( coeff ` f ) ` 0 ) =/= 0 ) -> -. f e. { 0p } )
41 26 40 eldifd 
 |-  ( ( f e. ( Poly ` ZZ ) /\ ( ( coeff ` f ) ` 0 ) =/= 0 ) -> f e. ( ( Poly ` ZZ ) \ { 0p } ) )
42 41 adantrr 
 |-  ( ( f e. ( Poly ` ZZ ) /\ ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) -> f e. ( ( Poly ` ZZ ) \ { 0p } ) )
43 simprr 
 |-  ( ( f e. ( Poly ` ZZ ) /\ ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) -> ( f ` A ) = 0 )
44 42 43 jca 
 |-  ( ( f e. ( Poly ` ZZ ) /\ ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) -> ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) )
45 44 reximi2 
 |-  ( E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) -> E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 )
46 45 anim2i 
 |-  ( ( A e. CC /\ E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) -> ( A e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 ) )
47 elaa 
 |-  ( A e. AA <-> ( A e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 ) )
48 46 47 sylibr 
 |-  ( ( A e. CC /\ E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) -> A e. AA )
49 simpr 
 |-  ( ( A e. CC /\ E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) -> E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) )
50 nfv 
 |-  F/ f A e. CC
51 nfre1 
 |-  F/ f E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 )
52 50 51 nfan 
 |-  F/ f ( A e. CC /\ E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) )
53 nfv 
 |-  F/ f -. A e. { 0 }
54 simpl3r 
 |-  ( ( ( A e. CC /\ f e. ( Poly ` ZZ ) /\ ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) /\ A = 0 ) -> ( f ` A ) = 0 )
55 fveq2 
 |-  ( A = 0 -> ( f ` A ) = ( f ` 0 ) )
56 eqid 
 |-  ( coeff ` f ) = ( coeff ` f )
57 56 coefv0 
 |-  ( f e. ( Poly ` ZZ ) -> ( f ` 0 ) = ( ( coeff ` f ) ` 0 ) )
58 55 57 sylan9eqr 
 |-  ( ( f e. ( Poly ` ZZ ) /\ A = 0 ) -> ( f ` A ) = ( ( coeff ` f ) ` 0 ) )
59 58 adantlr 
 |-  ( ( ( f e. ( Poly ` ZZ ) /\ ( ( coeff ` f ) ` 0 ) =/= 0 ) /\ A = 0 ) -> ( f ` A ) = ( ( coeff ` f ) ` 0 ) )
60 simplr 
 |-  ( ( ( f e. ( Poly ` ZZ ) /\ ( ( coeff ` f ) ` 0 ) =/= 0 ) /\ A = 0 ) -> ( ( coeff ` f ) ` 0 ) =/= 0 )
61 59 60 eqnetrd 
 |-  ( ( ( f e. ( Poly ` ZZ ) /\ ( ( coeff ` f ) ` 0 ) =/= 0 ) /\ A = 0 ) -> ( f ` A ) =/= 0 )
62 61 neneqd 
 |-  ( ( ( f e. ( Poly ` ZZ ) /\ ( ( coeff ` f ) ` 0 ) =/= 0 ) /\ A = 0 ) -> -. ( f ` A ) = 0 )
63 62 adantlrr 
 |-  ( ( ( f e. ( Poly ` ZZ ) /\ ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) /\ A = 0 ) -> -. ( f ` A ) = 0 )
64 63 3adantl1 
 |-  ( ( ( A e. CC /\ f e. ( Poly ` ZZ ) /\ ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) /\ A = 0 ) -> -. ( f ` A ) = 0 )
65 54 64 pm2.65da 
 |-  ( ( A e. CC /\ f e. ( Poly ` ZZ ) /\ ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) -> -. A = 0 )
66 elsng 
 |-  ( A e. CC -> ( A e. { 0 } <-> A = 0 ) )
67 66 biimpa 
 |-  ( ( A e. CC /\ A e. { 0 } ) -> A = 0 )
68 67 3ad2antl1 
 |-  ( ( ( A e. CC /\ f e. ( Poly ` ZZ ) /\ ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) /\ A e. { 0 } ) -> A = 0 )
69 65 68 mtand 
 |-  ( ( A e. CC /\ f e. ( Poly ` ZZ ) /\ ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) -> -. A e. { 0 } )
70 69 3exp 
 |-  ( A e. CC -> ( f e. ( Poly ` ZZ ) -> ( ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) -> -. A e. { 0 } ) ) )
71 70 adantr 
 |-  ( ( A e. CC /\ E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) -> ( f e. ( Poly ` ZZ ) -> ( ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) -> -. A e. { 0 } ) ) )
72 52 53 71 rexlimd 
 |-  ( ( A e. CC /\ E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) -> ( E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) -> -. A e. { 0 } ) )
73 49 72 mpd 
 |-  ( ( A e. CC /\ E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) -> -. A e. { 0 } )
74 48 73 eldifd 
 |-  ( ( A e. CC /\ E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) -> A e. ( AA \ { 0 } ) )
75 25 74 impbii 
 |-  ( A e. ( AA \ { 0 } ) <-> ( A e. CC /\ E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) ) )