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		qsscn	⊢ ℚ ⊆ ℂ
2		1q	⊢ 1 ∈ ℚ
3		2nn0	⊢ 2 ∈ ℕ0
4		eqid	⊢ ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 2 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 2 ) ) )
5	4	ply1term	⊢ ( ( ℚ ⊆ ℂ ∧ 1 ∈ ℚ ∧ 2 ∈ ℕ0 ) → ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 2 ) ) ) ∈ ( Poly ‘ ℚ ) )
6	1 2 3 5	mp3an	⊢ ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 2 ) ) ) ∈ ( Poly ‘ ℚ )
7	6	a1i	⊢ ( ⊤ → ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 2 ) ) ) ∈ ( Poly ‘ ℚ ) )
8		ax-1cn	⊢ 1 ∈ ℂ
9		ax-1ne0	⊢ 1 ≠ 0
10	4	dgr1term	⊢ ( ( 1 ∈ ℂ ∧ 1 ≠ 0 ∧ 2 ∈ ℕ0 ) → ( deg ‘ ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 2 ) ) ) ) = 2 )
11	8 9 3 10	mp3an	⊢ ( deg ‘ ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 2 ) ) ) ) = 2
12		2ne0	⊢ 2 ≠ 0
13	11 12	eqnetri	⊢ ( deg ‘ ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 2 ) ) ) ) ≠ 0
14	13	a1i	⊢ ( ⊤ → ( deg ‘ ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 2 ) ) ) ) ≠ 0 )
15		ax-icn	⊢ i ∈ ℂ
16	15	a1i	⊢ ( ⊤ → i ∈ ℂ )
17		oveq1	⊢ ( 𝑧 = i → ( 𝑧 ↑ 2 ) = ( i ↑ 2 ) )
18	17	oveq2d	⊢ ( 𝑧 = i → ( 1 · ( 𝑧 ↑ 2 ) ) = ( 1 · ( i ↑ 2 ) ) )
19		ovex	⊢ ( 1 · ( i ↑ 2 ) ) ∈ V
20	18 4 19	fvmpt	⊢ ( i ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 2 ) ) ) ‘ i ) = ( 1 · ( i ↑ 2 ) ) )
21	15 20	ax-mp	⊢ ( ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 2 ) ) ) ‘ i ) = ( 1 · ( i ↑ 2 ) )
22	15	sqcli	⊢ ( i ↑ 2 ) ∈ ℂ
23	22	mullidi	⊢ ( 1 · ( i ↑ 2 ) ) = ( i ↑ 2 )
24		i2	⊢ ( i ↑ 2 ) = - 1
25		qssaa	⊢ ℚ ⊆ 𝔸
26		zssq	⊢ ℤ ⊆ ℚ
27		neg1z	⊢ - 1 ∈ ℤ
28	26 27	sselii	⊢ - 1 ∈ ℚ
29	25 28	sselii	⊢ - 1 ∈ 𝔸
30	24 29	eqeltri	⊢ ( i ↑ 2 ) ∈ 𝔸
31	23 30	eqeltri	⊢ ( 1 · ( i ↑ 2 ) ) ∈ 𝔸
32	21 31	eqeltri	⊢ ( ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 2 ) ) ) ‘ i ) ∈ 𝔸
33	32	a1i	⊢ ( ⊤ → ( ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 2 ) ) ) ‘ i ) ∈ 𝔸 )
34	7 14 16 33	preimaaa	⊢ ( ⊤ → i ∈ 𝔸 )
35	34	mptru	⊢ i ∈ 𝔸