# Metamath Proof Explorer

## Theorem iaa

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

Ref Expression
Assertion iaa ${⊢}\mathrm{i}\in 𝔸$

### Proof

Step Hyp Ref Expression
1 ax-icn ${⊢}\mathrm{i}\in ℂ$
2 cnex ${⊢}ℂ\in \mathrm{V}$
3 2 a1i ${⊢}\top \to ℂ\in \mathrm{V}$
4 sqcl ${⊢}{z}\in ℂ\to {{z}}^{2}\in ℂ$
5 4 adantl ${⊢}\left(\top \wedge {z}\in ℂ\right)\to {{z}}^{2}\in ℂ$
6 ax-1cn ${⊢}1\in ℂ$
7 6 a1i ${⊢}\left(\top \wedge {z}\in ℂ\right)\to 1\in ℂ$
8 eqidd ${⊢}\top \to \left({z}\in ℂ⟼{{z}}^{2}\right)=\left({z}\in ℂ⟼{{z}}^{2}\right)$
9 fconstmpt ${⊢}ℂ×\left\{1\right\}=\left({z}\in ℂ⟼1\right)$
10 9 a1i ${⊢}\top \to ℂ×\left\{1\right\}=\left({z}\in ℂ⟼1\right)$
11 3 5 7 8 10 offval2 ${⊢}\top \to \left({z}\in ℂ⟼{{z}}^{2}\right){+}_{f}\left(ℂ×\left\{1\right\}\right)=\left({z}\in ℂ⟼{{z}}^{2}+1\right)$
12 zsscn ${⊢}ℤ\subseteq ℂ$
13 1z ${⊢}1\in ℤ$
14 2nn0 ${⊢}2\in {ℕ}_{0}$
15 plypow ${⊢}\left(ℤ\subseteq ℂ\wedge 1\in ℤ\wedge 2\in {ℕ}_{0}\right)\to \left({z}\in ℂ⟼{{z}}^{2}\right)\in \mathrm{Poly}\left(ℤ\right)$
16 12 13 14 15 mp3an ${⊢}\left({z}\in ℂ⟼{{z}}^{2}\right)\in \mathrm{Poly}\left(ℤ\right)$
17 16 a1i ${⊢}\top \to \left({z}\in ℂ⟼{{z}}^{2}\right)\in \mathrm{Poly}\left(ℤ\right)$
18 plyconst ${⊢}\left(ℤ\subseteq ℂ\wedge 1\in ℤ\right)\to ℂ×\left\{1\right\}\in \mathrm{Poly}\left(ℤ\right)$
19 12 13 18 mp2an ${⊢}ℂ×\left\{1\right\}\in \mathrm{Poly}\left(ℤ\right)$
20 19 a1i ${⊢}\top \to ℂ×\left\{1\right\}\in \mathrm{Poly}\left(ℤ\right)$
21 zaddcl ${⊢}\left({x}\in ℤ\wedge {y}\in ℤ\right)\to {x}+{y}\in ℤ$
22 21 adantl ${⊢}\left(\top \wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\to {x}+{y}\in ℤ$
23 17 20 22 plyadd ${⊢}\top \to \left({z}\in ℂ⟼{{z}}^{2}\right){+}_{f}\left(ℂ×\left\{1\right\}\right)\in \mathrm{Poly}\left(ℤ\right)$
24 11 23 eqeltrrd ${⊢}\top \to \left({z}\in ℂ⟼{{z}}^{2}+1\right)\in \mathrm{Poly}\left(ℤ\right)$
25 24 mptru ${⊢}\left({z}\in ℂ⟼{{z}}^{2}+1\right)\in \mathrm{Poly}\left(ℤ\right)$
26 0cn ${⊢}0\in ℂ$
27 sq0i ${⊢}{z}=0\to {{z}}^{2}=0$
28 27 oveq1d ${⊢}{z}=0\to {{z}}^{2}+1=0+1$
29 0p1e1 ${⊢}0+1=1$
30 28 29 syl6eq ${⊢}{z}=0\to {{z}}^{2}+1=1$
31 eqid ${⊢}\left({z}\in ℂ⟼{{z}}^{2}+1\right)=\left({z}\in ℂ⟼{{z}}^{2}+1\right)$
32 1ex ${⊢}1\in \mathrm{V}$
33 30 31 32 fvmpt ${⊢}0\in ℂ\to \left({z}\in ℂ⟼{{z}}^{2}+1\right)\left(0\right)=1$
34 26 33 ax-mp ${⊢}\left({z}\in ℂ⟼{{z}}^{2}+1\right)\left(0\right)=1$
35 ax-1ne0 ${⊢}1\ne 0$
36 34 35 eqnetri ${⊢}\left({z}\in ℂ⟼{{z}}^{2}+1\right)\left(0\right)\ne 0$
37 ne0p ${⊢}\left(0\in ℂ\wedge \left({z}\in ℂ⟼{{z}}^{2}+1\right)\left(0\right)\ne 0\right)\to \left({z}\in ℂ⟼{{z}}^{2}+1\right)\ne {0}_{𝑝}$
38 26 36 37 mp2an ${⊢}\left({z}\in ℂ⟼{{z}}^{2}+1\right)\ne {0}_{𝑝}$
39 eldifsn ${⊢}\left({z}\in ℂ⟼{{z}}^{2}+1\right)\in \left(\mathrm{Poly}\left(ℤ\right)\setminus \left\{{0}_{𝑝}\right\}\right)↔\left(\left({z}\in ℂ⟼{{z}}^{2}+1\right)\in \mathrm{Poly}\left(ℤ\right)\wedge \left({z}\in ℂ⟼{{z}}^{2}+1\right)\ne {0}_{𝑝}\right)$
40 25 38 39 mpbir2an ${⊢}\left({z}\in ℂ⟼{{z}}^{2}+1\right)\in \left(\mathrm{Poly}\left(ℤ\right)\setminus \left\{{0}_{𝑝}\right\}\right)$
41 oveq1 ${⊢}{z}=\mathrm{i}\to {{z}}^{2}={\mathrm{i}}^{2}$
42 i2 ${⊢}{\mathrm{i}}^{2}=-1$
43 41 42 syl6eq ${⊢}{z}=\mathrm{i}\to {{z}}^{2}=-1$
44 43 oveq1d ${⊢}{z}=\mathrm{i}\to {{z}}^{2}+1=-1+1$
45 neg1cn ${⊢}-1\in ℂ$
46 1pneg1e0 ${⊢}1+-1=0$
47 6 45 46 addcomli ${⊢}-1+1=0$
48 44 47 syl6eq ${⊢}{z}=\mathrm{i}\to {{z}}^{2}+1=0$
49 c0ex ${⊢}0\in \mathrm{V}$
50 48 31 49 fvmpt ${⊢}\mathrm{i}\in ℂ\to \left({z}\in ℂ⟼{{z}}^{2}+1\right)\left(\mathrm{i}\right)=0$
51 1 50 ax-mp ${⊢}\left({z}\in ℂ⟼{{z}}^{2}+1\right)\left(\mathrm{i}\right)=0$
52 fveq1 ${⊢}{f}=\left({z}\in ℂ⟼{{z}}^{2}+1\right)\to {f}\left(\mathrm{i}\right)=\left({z}\in ℂ⟼{{z}}^{2}+1\right)\left(\mathrm{i}\right)$
53 52 eqeq1d ${⊢}{f}=\left({z}\in ℂ⟼{{z}}^{2}+1\right)\to \left({f}\left(\mathrm{i}\right)=0↔\left({z}\in ℂ⟼{{z}}^{2}+1\right)\left(\mathrm{i}\right)=0\right)$
54 53 rspcev ${⊢}\left(\left({z}\in ℂ⟼{{z}}^{2}+1\right)\in \left(\mathrm{Poly}\left(ℤ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\wedge \left({z}\in ℂ⟼{{z}}^{2}+1\right)\left(\mathrm{i}\right)=0\right)\to \exists {f}\in \left(\mathrm{Poly}\left(ℤ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left(\mathrm{i}\right)=0$
55 40 51 54 mp2an ${⊢}\exists {f}\in \left(\mathrm{Poly}\left(ℤ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left(\mathrm{i}\right)=0$
56 elaa ${⊢}\mathrm{i}\in 𝔸↔\left(\mathrm{i}\in ℂ\wedge \exists {f}\in \left(\mathrm{Poly}\left(ℤ\right)\setminus \left\{{0}_{𝑝}\right\}\right)\phantom{\rule{.4em}{0ex}}{f}\left(\mathrm{i}\right)=0\right)$
57 1 55 56 mpbir2an ${⊢}\mathrm{i}\in 𝔸$