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∈ℂ→z2∈ℂ
5 4 adantl ⊢⊤∧z∈ℂ→z2∈ℂ
6 ax-1cn ⊢1∈ℂ
7 6 a1i ⊢⊤∧z∈ℂ→1∈ℂ
8 eqidd ⊢⊤→z∈ℂ⟼z2=z∈ℂ⟼z2
9 fconstmpt ⊢ℂ×1=z∈ℂ⟼1
10 9 a1i ⊢⊤→ℂ×1=z∈ℂ⟼1
11 3 5 7 8 10 offval2 ⊢⊤→z∈ℂ⟼z2+fℂ×1=z∈ℂ⟼z2+1
12 zsscn ⊢ℤ⊆ℂ
13 1z ⊢1∈ℤ
14 2nn0 ⊢2∈ℕ0
15 plypow ⊢ℤ⊆ℂ∧1∈ℤ∧2∈ℕ0→z∈ℂ⟼z2∈Poly⁡ℤ
16 12 13 14 15 mp3an ⊢z∈ℂ⟼z2∈Poly⁡ℤ
17 16 a1i ⊢⊤→z∈ℂ⟼z2∈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∈ℂ⟼z2+fℂ×1∈Poly⁡ℤ
24 11 23 eqeltrrd ⊢⊤→z∈ℂ⟼z2+1∈Poly⁡ℤ
25 24 mptru ⊢z∈ℂ⟼z2+1∈Poly⁡ℤ
26 0cn ⊢0∈ℂ
27 sq0i ⊢z=0→z2=0
28 27 oveq1d ⊢z=0→z2+1=0+1
29 0p1e1 ⊢0+1=1
30 28 29 eqtrdi ⊢z=0→z2+1=1
31 eqid ⊢z∈ℂ⟼z2+1=z∈ℂ⟼z2+1
32 1ex ⊢1∈V
33 30 31 32 fvmpt ⊢0∈ℂ→z∈ℂ⟼z2+1⁡0=1
34 26 33 ax-mp ⊢z∈ℂ⟼z2+1⁡0=1
35 ax-1ne0 ⊢1≠0
36 34 35 eqnetri ⊢z∈ℂ⟼z2+1⁡0≠0
37 ne0p ⊢0∈ℂ∧z∈ℂ⟼z2+1⁡0≠0→z∈ℂ⟼z2+1≠0𝑝
38 26 36 37 mp2an ⊢z∈ℂ⟼z2+1≠0𝑝
39 eldifsn ⊢z∈ℂ⟼z2+1∈Poly⁡ℤ∖0𝑝↔z∈ℂ⟼z2+1∈Poly⁡ℤ∧z∈ℂ⟼z2+1≠0𝑝
40 25 38 39 mpbir2an ⊢z∈ℂ⟼z2+1∈Poly⁡ℤ∖0𝑝
41 oveq1 ⊢z=i→z2=i2
42 i2 ⊢i2=−1
43 41 42 eqtrdi ⊢z=i→z2=−1
44 43 oveq1d ⊢z=i→z2+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→z2+1=0
49 c0ex ⊢0∈V
50 48 31 49 fvmpt ⊢i∈ℂ→z∈ℂ⟼z2+1⁡i=0
51 1 50 ax-mp ⊢z∈ℂ⟼z2+1⁡i=0
52 fveq1 ⊢f=z∈ℂ⟼z2+1→f⁡i=z∈ℂ⟼z2+1⁡i
53 52 eqeq1d ⊢f=z∈ℂ⟼z2+1→f⁡i=0↔z∈ℂ⟼z2+1⁡i=0
54 53 rspcev ⊢z∈ℂ⟼z2+1∈Poly⁡ℤ∖0𝑝∧z∈ℂ⟼z2+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∈𝔸