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 qsscn 
 |-  QQ C_ CC
2 1q 
 |-  1 e. QQ
3 2nn0 
 |-  2 e. NN0
4 eqid 
 |-  ( z e. CC |-> ( 1 x. ( z ^ 2 ) ) ) = ( z e. CC |-> ( 1 x. ( z ^ 2 ) ) )
5 4 ply1term 
 |-  ( ( QQ C_ CC /\ 1 e. QQ /\ 2 e. NN0 ) -> ( z e. CC |-> ( 1 x. ( z ^ 2 ) ) ) e. ( Poly ` QQ ) )
6 1 2 3 5 mp3an 
 |-  ( z e. CC |-> ( 1 x. ( z ^ 2 ) ) ) e. ( Poly ` QQ )
7 6 a1i 
 |-  ( T. -> ( z e. CC |-> ( 1 x. ( z ^ 2 ) ) ) e. ( Poly ` QQ ) )
8 ax-1cn 
 |-  1 e. CC
9 ax-1ne0 
 |-  1 =/= 0
10 4 dgr1term 
 |-  ( ( 1 e. CC /\ 1 =/= 0 /\ 2 e. NN0 ) -> ( deg ` ( z e. CC |-> ( 1 x. ( z ^ 2 ) ) ) ) = 2 )
11 8 9 3 10 mp3an 
 |-  ( deg ` ( z e. CC |-> ( 1 x. ( z ^ 2 ) ) ) ) = 2
12 2ne0 
 |-  2 =/= 0
13 11 12 eqnetri 
 |-  ( deg ` ( z e. CC |-> ( 1 x. ( z ^ 2 ) ) ) ) =/= 0
14 13 a1i 
 |-  ( T. -> ( deg ` ( z e. CC |-> ( 1 x. ( z ^ 2 ) ) ) ) =/= 0 )
15 ax-icn 
 |-  _i e. CC
16 15 a1i 
 |-  ( T. -> _i e. CC )
17 oveq1 
 |-  ( z = _i -> ( z ^ 2 ) = ( _i ^ 2 ) )
18 17 oveq2d 
 |-  ( z = _i -> ( 1 x. ( z ^ 2 ) ) = ( 1 x. ( _i ^ 2 ) ) )
19 ovex 
 |-  ( 1 x. ( _i ^ 2 ) ) e. _V
20 18 4 19 fvmpt 
 |-  ( _i e. CC -> ( ( z e. CC |-> ( 1 x. ( z ^ 2 ) ) ) ` _i ) = ( 1 x. ( _i ^ 2 ) ) )
21 15 20 ax-mp 
 |-  ( ( z e. CC |-> ( 1 x. ( z ^ 2 ) ) ) ` _i ) = ( 1 x. ( _i ^ 2 ) )
22 15 sqcli 
 |-  ( _i ^ 2 ) e. CC
23 22 mullidi 
 |-  ( 1 x. ( _i ^ 2 ) ) = ( _i ^ 2 )
24 i2 
 |-  ( _i ^ 2 ) = -u 1
25 qssaa 
 |-  QQ C_ AA
26 zssq 
 |-  ZZ C_ QQ
27 neg1z 
 |-  -u 1 e. ZZ
28 26 27 sselii 
 |-  -u 1 e. QQ
29 25 28 sselii 
 |-  -u 1 e. AA
30 24 29 eqeltri 
 |-  ( _i ^ 2 ) e. AA
31 23 30 eqeltri 
 |-  ( 1 x. ( _i ^ 2 ) ) e. AA
32 21 31 eqeltri 
 |-  ( ( z e. CC |-> ( 1 x. ( z ^ 2 ) ) ) ` _i ) e. AA
33 32 a1i 
 |-  ( T. -> ( ( z e. CC |-> ( 1 x. ( z ^ 2 ) ) ) ` _i ) e. AA )
34 7 14 16 33 preimaaa 
 |-  ( T. -> _i e. AA )
35 34 mptru 
 |-  _i e. AA