iaa

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

		Ref	Expression
	Assertion	iaa	$⊢ i \in 𝔸$

Step	Hyp	Ref	Expression
1		qsscn	$⊢ ℚ \subseteq ℂ$
2		1q	$⊢ 1 \in ℚ$
3		2nn0	$⊢ 2 \in ℕ_{0}$
4		eqid	$⊢ (z \in ℂ ⟼ 1 z^{2}) = (z \in ℂ ⟼ 1 z^{2})$
5	4	ply1term	$⊢ (ℚ \subseteq ℂ \land 1 \in ℚ \land 2 \in ℕ_{0}) \to (z \in ℂ ⟼ 1 z^{2}) \in Poly (ℚ)$
6	1 2 3 5	mp3an	$⊢ (z \in ℂ ⟼ 1 z^{2}) \in Poly (ℚ)$
7	6	a1i	$⊢ ⊤ \to (z \in ℂ ⟼ 1 z^{2}) \in Poly (ℚ)$
8		ax-1cn	$⊢ 1 \in ℂ$
9		ax-1ne0	$⊢ 1 \neq 0$
10	4	dgr1term	$⊢ (1 \in ℂ \land 1 \neq 0 \land 2 \in ℕ_{0}) \to \deg ((z \in ℂ ⟼ 1 z^{2})) = 2$
11	8 9 3 10	mp3an	$⊢ \deg ((z \in ℂ ⟼ 1 z^{2})) = 2$
12		2ne0	$⊢ 2 \neq 0$
13	11 12	eqnetri	$⊢ \deg ((z \in ℂ ⟼ 1 z^{2})) \neq 0$
14	13	a1i	$⊢ ⊤ \to \deg ((z \in ℂ ⟼ 1 z^{2})) \neq 0$
15		ax-icn	$⊢ i \in ℂ$
16	15	a1i	$⊢ ⊤ \to i \in ℂ$
17		oveq1	$⊢ z = i \to z^{2} = i^{2}$
18	17	oveq2d	$⊢ z = i \to 1 z^{2} = 1 i^{2}$
19		ovex	$⊢ 1 i^{2} \in V$
20	18 4 19	fvmpt	$⊢ i \in ℂ \to (z \in ℂ ⟼ 1 z^{2}) (i) = 1 i^{2}$
21	15 20	ax-mp	$⊢ (z \in ℂ ⟼ 1 z^{2}) (i) = 1 i^{2}$
22	15	sqcli	$⊢ i^{2} \in ℂ$
23	22	mullidi	$⊢ 1 i^{2} = i^{2}$
24		i2	$⊢ i^{2} = - 1$
25		qssaa	$⊢ ℚ \subseteq 𝔸$
26		zssq	$⊢ ℤ \subseteq ℚ$
27		neg1z	$⊢ - 1 \in ℤ$
28	26 27	sselii	$⊢ - 1 \in ℚ$
29	25 28	sselii	$⊢ - 1 \in 𝔸$
30	24 29	eqeltri	$⊢ i^{2} \in 𝔸$
31	23 30	eqeltri	$⊢ 1 i^{2} \in 𝔸$
32	21 31	eqeltri	$⊢ (z \in ℂ ⟼ 1 z^{2}) (i) \in 𝔸$
33	32	a1i	$⊢ ⊤ \to (z \in ℂ ⟼ 1 z^{2}) (i) \in 𝔸$
34	7 14 16 33	preimaaa	$⊢ ⊤ \to i \in 𝔸$
35	34	mptru	$⊢ i \in 𝔸$

Metamath Proof Explorer