Metamath Proof Explorer


Theorem iaa

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

Ref Expression
Assertion iaa i 𝔸

Proof

Step Hyp Ref Expression
1 ax-icn i
2 cnex V
3 2 a1i V
4 sqcl z z 2
5 4 adantl z z 2
6 ax-1cn 1
7 6 a1i z 1
8 eqidd z z 2 = z z 2
9 fconstmpt × 1 = z 1
10 9 a1i × 1 = z 1
11 3 5 7 8 10 offval2 z z 2 + f × 1 = z z 2 + 1
12 zsscn
13 1z 1
14 2nn0 2 0
15 plypow 1 2 0 z z 2 Poly
16 12 13 14 15 mp3an z z 2 Poly
17 16 a1i z z 2 Poly
18 plyconst 1 × 1 Poly
19 12 13 18 mp2an × 1 Poly
20 19 a1i × 1 Poly
21 zaddcl x y x + y
22 21 adantl x y x + y
23 17 20 22 plyadd z z 2 + f × 1 Poly
24 11 23 eqeltrrd z z 2 + 1 Poly
25 24 mptru z z 2 + 1 Poly
26 0cn 0
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 z 2 + 1 = z z 2 + 1
32 1ex 1 V
33 30 31 32 fvmpt 0 z z 2 + 1 0 = 1
34 26 33 ax-mp z z 2 + 1 0 = 1
35 ax-1ne0 1 0
36 34 35 eqnetri z z 2 + 1 0 0
37 ne0p 0 z z 2 + 1 0 0 z z 2 + 1 0 𝑝
38 26 36 37 mp2an z z 2 + 1 0 𝑝
39 eldifsn z z 2 + 1 Poly 0 𝑝 z z 2 + 1 Poly z z 2 + 1 0 𝑝
40 25 38 39 mpbir2an z z 2 + 1 Poly 0 𝑝
41 oveq1 z = i z 2 = i 2
42 i2 i 2 = 1
43 41 42 eqtrdi z = i z 2 = 1
44 43 oveq1d z = i z 2 + 1 = - 1 + 1
45 neg1cn 1
46 1pneg1e0 1 + -1 = 0
47 6 45 46 addcomli - 1 + 1 = 0
48 44 47 eqtrdi z = i z 2 + 1 = 0
49 c0ex 0 V
50 48 31 49 fvmpt i z z 2 + 1 i = 0
51 1 50 ax-mp z z 2 + 1 i = 0
52 fveq1 f = z z 2 + 1 f i = z z 2 + 1 i
53 52 eqeq1d f = z z 2 + 1 f i = 0 z z 2 + 1 i = 0
54 53 rspcev z z 2 + 1 Poly 0 𝑝 z z 2 + 1 i = 0 f Poly 0 𝑝 f i = 0
55 40 51 54 mp2an f Poly 0 𝑝 f i = 0
56 elaa i 𝔸 i f Poly 0 𝑝 f i = 0
57 1 55 56 mpbir2an i 𝔸