Metamath Proof Explorer

Theorem iaa

Description: The imaginary unit is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Assertion iaa 
|- _i e. AA

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 cnex 
 |-  CC e. _V
3 2 a1i 
 |-  ( T. -> CC e. _V )
4 sqcl 
 |-  ( z e. CC -> ( z ^ 2 ) e. CC )
5 4 adantl 
 |-  ( ( T. /\ z e. CC ) -> ( z ^ 2 ) e. CC )
6 ax-1cn 
 |-  1 e. CC
7 6 a1i 
 |-  ( ( T. /\ z e. CC ) -> 1 e. CC )
8 eqidd 
 |-  ( T. -> ( z e. CC |-> ( z ^ 2 ) ) = ( z e. CC |-> ( z ^ 2 ) ) )
9 fconstmpt 
 |-  ( CC X. { 1 } ) = ( z e. CC |-> 1 )
10 9 a1i 
 |-  ( T. -> ( CC X. { 1 } ) = ( z e. CC |-> 1 ) )
11 3 5 7 8 10 offval2 
 |-  ( T. -> ( ( z e. CC |-> ( z ^ 2 ) ) oF + ( CC X. { 1 } ) ) = ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) )
12 zsscn 
 |-  ZZ C_ CC
13 1z 
 |-  1 e. ZZ
14 2nn0 
 |-  2 e. NN0
15 plypow 
 |-  ( ( ZZ C_ CC /\ 1 e. ZZ /\ 2 e. NN0 ) -> ( z e. CC |-> ( z ^ 2 ) ) e. ( Poly ` ZZ ) )
16 12 13 14 15 mp3an 
 |-  ( z e. CC |-> ( z ^ 2 ) ) e. ( Poly ` ZZ )
17 16 a1i 
 |-  ( T. -> ( z e. CC |-> ( z ^ 2 ) ) e. ( Poly ` ZZ ) )
18 plyconst 
 |-  ( ( ZZ C_ CC /\ 1 e. ZZ ) -> ( CC X. { 1 } ) e. ( Poly ` ZZ ) )
19 12 13 18 mp2an 
 |-  ( CC X. { 1 } ) e. ( Poly ` ZZ )
20 19 a1i 
 |-  ( T. -> ( CC X. { 1 } ) e. ( Poly ` ZZ ) )
21 zaddcl 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x + y ) e. ZZ )
22 21 adantl 
 |-  ( ( T. /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( x + y ) e. ZZ )
23 17 20 22 plyadd 
 |-  ( T. -> ( ( z e. CC |-> ( z ^ 2 ) ) oF + ( CC X. { 1 } ) ) e. ( Poly ` ZZ ) )
24 11 23 eqeltrrd 
 |-  ( T. -> ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) e. ( Poly ` ZZ ) )
25 24 mptru 
 |-  ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) e. ( Poly ` ZZ )
26 0cn 
 |-  0 e. CC
27 sq0i 
 |-  ( z = 0 -> ( z ^ 2 ) = 0 )
28 27 oveq1d 
 |-  ( z = 0 -> ( ( z ^ 2 ) + 1 ) = ( 0 + 1 ) )
29 0p1e1 
 |-  ( 0 + 1 ) = 1
30 28 29 eqtrdi 
 |-  ( z = 0 -> ( ( z ^ 2 ) + 1 ) = 1 )
31 eqid 
 |-  ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) = ( z e. CC |-> ( ( z ^ 2 ) + 1 ) )
32 1ex 
 |-  1 e. _V
33 30 31 32 fvmpt 
 |-  ( 0 e. CC -> ( ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) ` 0 ) = 1 )
34 26 33 ax-mp 
 |-  ( ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) ` 0 ) = 1
35 ax-1ne0 
 |-  1 =/= 0
36 34 35 eqnetri 
 |-  ( ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) ` 0 ) =/= 0
37 ne0p 
 |-  ( ( 0 e. CC /\ ( ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) ` 0 ) =/= 0 ) -> ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) =/= 0p )
38 26 36 37 mp2an 
 |-  ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) =/= 0p
39 eldifsn 
 |-  ( ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) e. ( ( Poly ` ZZ ) \ { 0p } ) <-> ( ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) e. ( Poly ` ZZ ) /\ ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) =/= 0p ) )
40 25 38 39 mpbir2an 
 |-  ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) e. ( ( Poly ` ZZ ) \ { 0p } )
41 oveq1 
 |-  ( z = _i -> ( z ^ 2 ) = ( _i ^ 2 ) )
42 i2 
 |-  ( _i ^ 2 ) = -u 1
43 41 42 eqtrdi 
 |-  ( z = _i -> ( z ^ 2 ) = -u 1 )
44 43 oveq1d 
 |-  ( z = _i -> ( ( z ^ 2 ) + 1 ) = ( -u 1 + 1 ) )
45 neg1cn 
 |-  -u 1 e. CC
46 1pneg1e0 
 |-  ( 1 + -u 1 ) = 0
47 6 45 46 addcomli 
 |-  ( -u 1 + 1 ) = 0
48 44 47 eqtrdi 
 |-  ( z = _i -> ( ( z ^ 2 ) + 1 ) = 0 )
49 c0ex 
 |-  0 e. _V
50 48 31 49 fvmpt 
 |-  ( _i e. CC -> ( ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) ` _i ) = 0 )
51 1 50 ax-mp 
 |-  ( ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) ` _i ) = 0
52 fveq1 
 |-  ( f = ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) -> ( f ` _i ) = ( ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) ` _i ) )
53 52 eqeq1d 
 |-  ( f = ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) -> ( ( f ` _i ) = 0 <-> ( ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) ` _i ) = 0 ) )
54 53 rspcev 
 |-  ( ( ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( ( z e. CC |-> ( ( z ^ 2 ) + 1 ) ) ` _i ) = 0 ) -> E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` _i ) = 0 )
55 40 51 54 mp2an 
 |-  E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` _i ) = 0
56 elaa 
 |-  ( _i e. AA <-> ( _i e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` _i ) = 0 ) )
57 1 55 56 mpbir2an 
 |-  _i e. AA