iaa

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

		Ref	Expression
	Assertion	iaa	$⊢ i \in 𝔸$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$⊢ i \in ℂ$
2		cnex	$⊢ ℂ \in V$
3	2	a1i	$⊢ ⊤ \to ℂ \in V$
4		sqcl	$⊢ z \in ℂ \to z^{2} \in ℂ$
5	4	adantl	$⊢ (⊤ \land z \in ℂ) \to z^{2} \in ℂ$
6		ax-1cn	$⊢ 1 \in ℂ$
7	6	a1i	$⊢ (⊤ \land z \in ℂ) \to 1 \in ℂ$
8		eqidd	$⊢ ⊤ \to (z \in ℂ ⟼ z^{2}) = (z \in ℂ ⟼ z^{2})$
9		fconstmpt	$⊢ ℂ \times \{1\} = (z \in ℂ ⟼ 1)$
10	9	a1i	$⊢ ⊤ \to ℂ \times \{1\} = (z \in ℂ ⟼ 1)$
11	3 5 7 8 10	offval2	$⊢ ⊤ \to (z \in ℂ ⟼ z^{2}) +_{f} (ℂ \times \{1\}) = (z \in ℂ ⟼ z^{2} + 1)$
12		zsscn	$⊢ ℤ \subseteq ℂ$
13		1z	$⊢ 1 \in ℤ$
14		2nn0	$⊢ 2 \in ℕ_{0}$
15		plypow	$⊢ (ℤ \subseteq ℂ \land 1 \in ℤ \land 2 \in ℕ_{0}) \to (z \in ℂ ⟼ z^{2}) \in Poly (ℤ)$
16	12 13 14 15	mp3an	$⊢ (z \in ℂ ⟼ z^{2}) \in Poly (ℤ)$
17	16	a1i	$⊢ ⊤ \to (z \in ℂ ⟼ z^{2}) \in Poly (ℤ)$
18		plyconst	$⊢ (ℤ \subseteq ℂ \land 1 \in ℤ) \to ℂ \times \{1\} \in Poly (ℤ)$
19	12 13 18	mp2an	$⊢ ℂ \times \{1\} \in Poly (ℤ)$
20	19	a1i	$⊢ ⊤ \to ℂ \times \{1\} \in Poly (ℤ)$
21		zaddcl	$⊢ (x \in ℤ \land y \in ℤ) \to x + y \in ℤ$
22	21	adantl	$⊢ (⊤ \land (x \in ℤ \land y \in ℤ)) \to x + y \in ℤ$
23	17 20 22	plyadd	$⊢ ⊤ \to (z \in ℂ ⟼ z^{2}) +_{f} (ℂ \times \{1\}) \in Poly (ℤ)$
24	11 23	eqeltrrd	$⊢ ⊤ \to (z \in ℂ ⟼ z^{2} + 1) \in Poly (ℤ)$
25	24	mptru	$⊢ (z \in ℂ ⟼ z^{2} + 1) \in Poly (ℤ)$
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	$⊢ (z \in ℂ ⟼ z^{2} + 1) = (z \in ℂ ⟼ z^{2} + 1)$
32		1ex	$⊢ 1 \in V$
33	30 31 32	fvmpt	$⊢ 0 \in ℂ \to (z \in ℂ ⟼ z^{2} + 1) (0) = 1$
34	26 33	ax-mp	$⊢ (z \in ℂ ⟼ z^{2} + 1) (0) = 1$
35		ax-1ne0	$⊢ 1 \neq 0$
36	34 35	eqnetri	$⊢ (z \in ℂ ⟼ z^{2} + 1) (0) \neq 0$
37		ne0p	$⊢ (0 \in ℂ \land (z \in ℂ ⟼ z^{2} + 1) (0) \neq 0) \to (z \in ℂ ⟼ z^{2} + 1) \neq 0_{𝑝}$
38	26 36 37	mp2an	$⊢ (z \in ℂ ⟼ z^{2} + 1) \neq 0_{𝑝}$
39		eldifsn	$⊢ (z \in ℂ ⟼ z^{2} + 1) \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \leftrightarrow ((z \in ℂ ⟼ z^{2} + 1) \in Poly (ℤ) \land (z \in ℂ ⟼ z^{2} + 1) \neq 0_{𝑝})$
40	25 38 39	mpbir2an	$⊢ (z \in ℂ ⟼ z^{2} + 1) \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
41		oveq1	$⊢ z = i \to z^{2} = i^{2}$
42		i2	$⊢ i^{2} = - 1$
43	41 42	syl6eq	$⊢ z = i \to z^{2} = - 1$
44	43	oveq1d	$⊢ z = 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 = i \to z^{2} + 1 = 0$
49		c0ex	$⊢ 0 \in V$
50	48 31 49	fvmpt	$⊢ i \in ℂ \to (z \in ℂ ⟼ z^{2} + 1) (i) = 0$
51	1 50	ax-mp	$⊢ (z \in ℂ ⟼ z^{2} + 1) (i) = 0$
52		fveq1	$⊢ f = (z \in ℂ ⟼ z^{2} + 1) \to f (i) = (z \in ℂ ⟼ z^{2} + 1) (i)$
53	52	eqeq1d	$⊢ f = (z \in ℂ ⟼ z^{2} + 1) \to (f (i) = 0 \leftrightarrow (z \in ℂ ⟼ z^{2} + 1) (i) = 0)$
54	53	rspcev	$⊢ ((z \in ℂ ⟼ z^{2} + 1) \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land (z \in ℂ ⟼ z^{2} + 1) (i) = 0) \to \exists f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) f (i) = 0$
55	40 51 54	mp2an	$⊢ \exists f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) f (i) = 0$
56		elaa	$⊢ i \in 𝔸 \leftrightarrow (i \in ℂ \land \exists f \in (Poly (ℤ) ∖ \{0_{𝑝}\}) f (i) = 0)$
57	1 55 56	mpbir2an	$⊢ i \in 𝔸$

Metamath Proof Explorer

Theorem iaa

Proof