Metamath Proof Explorer

Theorem qaa

Description: Every rational number is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Assertion qaa 
|- ( A e. QQ -> A e. AA )

Proof

Step Hyp Ref Expression
1 qcn 
 |-  ( A e. QQ -> A e. CC )
2 fveq1 
 |-  ( f = ( Xp oF - ( CC X. { A } ) ) -> ( f ` A ) = ( ( Xp oF - ( CC X. { A } ) ) ` A ) )
3 2 eqeq1d 
 |-  ( f = ( Xp oF - ( CC X. { A } ) ) -> ( ( f ` A ) = 0 <-> ( ( Xp oF - ( CC X. { A } ) ) ` A ) = 0 ) )
4 qsscn 
 |-  QQ C_ CC
5 1q 
 |-  1 e. QQ
6 plyid 
 |-  ( ( QQ C_ CC /\ 1 e. QQ ) -> Xp e. ( Poly ` QQ ) )
7 4 5 6 mp2an 
 |-  Xp e. ( Poly ` QQ )
8 7 a1i 
 |-  ( A e. QQ -> Xp e. ( Poly ` QQ ) )
9 plyconst 
 |-  ( ( QQ C_ CC /\ A e. QQ ) -> ( CC X. { A } ) e. ( Poly ` QQ ) )
10 4 9 mpan 
 |-  ( A e. QQ -> ( CC X. { A } ) e. ( Poly ` QQ ) )
11 qaddcl 
 |-  ( ( x e. QQ /\ y e. QQ ) -> ( x + y ) e. QQ )
12 11 adantl 
 |-  ( ( A e. QQ /\ ( x e. QQ /\ y e. QQ ) ) -> ( x + y ) e. QQ )
13 qmulcl 
 |-  ( ( x e. QQ /\ y e. QQ ) -> ( x x. y ) e. QQ )
14 13 adantl 
 |-  ( ( A e. QQ /\ ( x e. QQ /\ y e. QQ ) ) -> ( x x. y ) e. QQ )
15 qnegcl 
 |-  ( 1 e. QQ -> -u 1 e. QQ )
16 5 15 mp1i 
 |-  ( A e. QQ -> -u 1 e. QQ )
17 8 10 12 14 16 plysub 
 |-  ( A e. QQ -> ( Xp oF - ( CC X. { A } ) ) e. ( Poly ` QQ ) )
18 peano2cn 
 |-  ( A e. CC -> ( A + 1 ) e. CC )
19 1 18 syl 
 |-  ( A e. QQ -> ( A + 1 ) e. CC )
20 fnresi 
 |-  ( _I |` CC ) Fn CC
21 df-idp 
 |-  Xp = ( _I |` CC )
22 21 fneq1i 
 |-  ( Xp Fn CC <-> ( _I |` CC ) Fn CC )
23 20 22 mpbir 
 |-  Xp Fn CC
24 23 a1i 
 |-  ( A e. QQ -> Xp Fn CC )
25 fnconstg 
 |-  ( A e. QQ -> ( CC X. { A } ) Fn CC )
26 cnex 
 |-  CC e. _V
27 26 a1i 
 |-  ( A e. QQ -> CC e. _V )
28 inidm 
 |-  ( CC i^i CC ) = CC
29 idpfv 
 |-  ( ( A + 1 ) e. CC -> ( Xp ` ( A + 1 ) ) = ( A + 1 ) )
30 29 adantl 
 |-  ( ( A e. QQ /\ ( A + 1 ) e. CC ) -> ( Xp ` ( A + 1 ) ) = ( A + 1 ) )
31 fvconst2g 
 |-  ( ( A e. QQ /\ ( A + 1 ) e. CC ) -> ( ( CC X. { A } ) ` ( A + 1 ) ) = A )
32 24 25 27 27 28 30 31 ofval 
 |-  ( ( A e. QQ /\ ( A + 1 ) e. CC ) -> ( ( Xp oF - ( CC X. { A } ) ) ` ( A + 1 ) ) = ( ( A + 1 ) - A ) )
33 19 32 mpdan 
 |-  ( A e. QQ -> ( ( Xp oF - ( CC X. { A } ) ) ` ( A + 1 ) ) = ( ( A + 1 ) - A ) )
34 ax-1cn 
 |-  1 e. CC
35 pncan2 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A + 1 ) - A ) = 1 )
36 1 34 35 sylancl 
 |-  ( A e. QQ -> ( ( A + 1 ) - A ) = 1 )
37 33 36 eqtrd 
 |-  ( A e. QQ -> ( ( Xp oF - ( CC X. { A } ) ) ` ( A + 1 ) ) = 1 )
38 ax-1ne0 
 |-  1 =/= 0
39 38 a1i 
 |-  ( A e. QQ -> 1 =/= 0 )
40 37 39 eqnetrd 
 |-  ( A e. QQ -> ( ( Xp oF - ( CC X. { A } ) ) ` ( A + 1 ) ) =/= 0 )
41 ne0p 
 |-  ( ( ( A + 1 ) e. CC /\ ( ( Xp oF - ( CC X. { A } ) ) ` ( A + 1 ) ) =/= 0 ) -> ( Xp oF - ( CC X. { A } ) ) =/= 0p )
42 19 40 41 syl2anc 
 |-  ( A e. QQ -> ( Xp oF - ( CC X. { A } ) ) =/= 0p )
43 17 42 eldifsnd 
 |-  ( A e. QQ -> ( Xp oF - ( CC X. { A } ) ) e. ( ( Poly ` QQ ) \ { 0p } ) )
44 idpfv 
 |-  ( A e. CC -> ( Xp ` A ) = A )
45 44 adantl 
 |-  ( ( A e. QQ /\ A e. CC ) -> ( Xp ` A ) = A )
46 fvconst2g 
 |-  ( ( A e. QQ /\ A e. CC ) -> ( ( CC X. { A } ) ` A ) = A )
47 24 25 27 27 28 45 46 ofval 
 |-  ( ( A e. QQ /\ A e. CC ) -> ( ( Xp oF - ( CC X. { A } ) ) ` A ) = ( A - A ) )
48 1 47 mpdan 
 |-  ( A e. QQ -> ( ( Xp oF - ( CC X. { A } ) ) ` A ) = ( A - A ) )
49 1 subidd 
 |-  ( A e. QQ -> ( A - A ) = 0 )
50 48 49 eqtrd 
 |-  ( A e. QQ -> ( ( Xp oF - ( CC X. { A } ) ) ` A ) = 0 )
51 3 43 50 rspcedvdw 
 |-  ( A e. QQ -> E. f e. ( ( Poly ` QQ ) \ { 0p } ) ( f ` A ) = 0 )
52 elqaa 
 |-  ( A e. AA <-> ( A e. CC /\ E. f e. ( ( Poly ` QQ ) \ { 0p } ) ( f ` A ) = 0 ) )
53 1 51 52 sylanbrc 
 |-  ( A e. QQ -> A e. AA )