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 qsscn 
 |-  QQ C_ CC
3 1z 
 |-  1 e. ZZ
4 zq 
 |-  ( 1 e. ZZ -> 1 e. QQ )
5 3 4 ax-mp 
 |-  1 e. QQ
6 plyid 
 |-  ( ( QQ C_ CC /\ 1 e. QQ ) -> Xp e. ( Poly ` QQ ) )
7 2 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 2 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 ax-mp 
 |-  -u 1 e. QQ
17 16 a1i 
 |-  ( A e. QQ -> -u 1 e. QQ )
18 8 10 12 14 17 plysub 
 |-  ( A e. QQ -> ( Xp oF - ( CC X. { A } ) ) e. ( Poly ` QQ ) )
19 peano2cn 
 |-  ( A e. CC -> ( A + 1 ) e. CC )
20 1 19 syl 
 |-  ( A e. QQ -> ( A + 1 ) e. CC )
21 fnresi 
 |-  ( _I |` CC ) Fn CC
22 df-idp 
 |-  Xp = ( _I |` CC )
23 22 fneq1i 
 |-  ( Xp Fn CC <-> ( _I |` CC ) Fn CC )
24 21 23 mpbir 
 |-  Xp Fn CC
25 24 a1i 
 |-  ( A e. QQ -> Xp Fn CC )
26 fnconstg 
 |-  ( A e. QQ -> ( CC X. { A } ) Fn CC )
27 cnex 
 |-  CC e. _V
28 27 a1i 
 |-  ( A e. QQ -> CC e. _V )
29 inidm 
 |-  ( CC i^i CC ) = CC
30 22 fveq1i 
 |-  ( Xp ` ( A + 1 ) ) = ( ( _I |` CC ) ` ( A + 1 ) )
31 fvresi 
 |-  ( ( A + 1 ) e. CC -> ( ( _I |` CC ) ` ( A + 1 ) ) = ( A + 1 ) )
32 30 31 syl5eq 
 |-  ( ( A + 1 ) e. CC -> ( Xp ` ( A + 1 ) ) = ( A + 1 ) )
33 32 adantl 
 |-  ( ( A e. QQ /\ ( A + 1 ) e. CC ) -> ( Xp ` ( A + 1 ) ) = ( A + 1 ) )
34 fvconst2g 
 |-  ( ( A e. QQ /\ ( A + 1 ) e. CC ) -> ( ( CC X. { A } ) ` ( A + 1 ) ) = A )
35 25 26 28 28 29 33 34 ofval 
 |-  ( ( A e. QQ /\ ( A + 1 ) e. CC ) -> ( ( Xp oF - ( CC X. { A } ) ) ` ( A + 1 ) ) = ( ( A + 1 ) - A ) )
36 20 35 mpdan 
 |-  ( A e. QQ -> ( ( Xp oF - ( CC X. { A } ) ) ` ( A + 1 ) ) = ( ( A + 1 ) - A ) )
37 ax-1cn 
 |-  1 e. CC
38 pncan2 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A + 1 ) - A ) = 1 )
39 1 37 38 sylancl 
 |-  ( A e. QQ -> ( ( A + 1 ) - A ) = 1 )
40 36 39 eqtrd 
 |-  ( A e. QQ -> ( ( Xp oF - ( CC X. { A } ) ) ` ( A + 1 ) ) = 1 )
41 ax-1ne0 
 |-  1 =/= 0
42 41 a1i 
 |-  ( A e. QQ -> 1 =/= 0 )
43 40 42 eqnetrd 
 |-  ( A e. QQ -> ( ( Xp oF - ( CC X. { A } ) ) ` ( A + 1 ) ) =/= 0 )
44 ne0p 
 |-  ( ( ( A + 1 ) e. CC /\ ( ( Xp oF - ( CC X. { A } ) ) ` ( A + 1 ) ) =/= 0 ) -> ( Xp oF - ( CC X. { A } ) ) =/= 0p )
45 20 43 44 syl2anc 
 |-  ( A e. QQ -> ( Xp oF - ( CC X. { A } ) ) =/= 0p )
46 eldifsn 
 |-  ( ( Xp oF - ( CC X. { A } ) ) e. ( ( Poly ` QQ ) \ { 0p } ) <-> ( ( Xp oF - ( CC X. { A } ) ) e. ( Poly ` QQ ) /\ ( Xp oF - ( CC X. { A } ) ) =/= 0p ) )
47 18 45 46 sylanbrc 
 |-  ( A e. QQ -> ( Xp oF - ( CC X. { A } ) ) e. ( ( Poly ` QQ ) \ { 0p } ) )
48 22 fveq1i 
 |-  ( Xp ` A ) = ( ( _I |` CC ) ` A )
49 fvresi 
 |-  ( A e. CC -> ( ( _I |` CC ) ` A ) = A )
50 48 49 syl5eq 
 |-  ( A e. CC -> ( Xp ` A ) = A )
51 50 adantl 
 |-  ( ( A e. QQ /\ A e. CC ) -> ( Xp ` A ) = A )
52 fvconst2g 
 |-  ( ( A e. QQ /\ A e. CC ) -> ( ( CC X. { A } ) ` A ) = A )
53 25 26 28 28 29 51 52 ofval 
 |-  ( ( A e. QQ /\ A e. CC ) -> ( ( Xp oF - ( CC X. { A } ) ) ` A ) = ( A - A ) )
54 1 53 mpdan 
 |-  ( A e. QQ -> ( ( Xp oF - ( CC X. { A } ) ) ` A ) = ( A - A ) )
55 1 subidd 
 |-  ( A e. QQ -> ( A - A ) = 0 )
56 54 55 eqtrd 
 |-  ( A e. QQ -> ( ( Xp oF - ( CC X. { A } ) ) ` A ) = 0 )
57 fveq1 
 |-  ( f = ( Xp oF - ( CC X. { A } ) ) -> ( f ` A ) = ( ( Xp oF - ( CC X. { A } ) ) ` A ) )
58 57 eqeq1d 
 |-  ( f = ( Xp oF - ( CC X. { A } ) ) -> ( ( f ` A ) = 0 <-> ( ( Xp oF - ( CC X. { A } ) ) ` A ) = 0 ) )
59 58 rspcev 
 |-  ( ( ( Xp oF - ( CC X. { A } ) ) e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( ( Xp oF - ( CC X. { A } ) ) ` A ) = 0 ) -> E. f e. ( ( Poly ` QQ ) \ { 0p } ) ( f ` A ) = 0 )
60 47 56 59 syl2anc 
 |-  ( A e. QQ -> E. f e. ( ( Poly ` QQ ) \ { 0p } ) ( f ` A ) = 0 )
61 elqaa 
 |-  ( A e. AA <-> ( A e. CC /\ E. f e. ( ( Poly ` QQ ) \ { 0p } ) ( f ` A ) = 0 ) )
62 1 60 61 sylanbrc 
 |-  ( A e. QQ -> A e. AA )