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 ⊢ ( 𝑧 ∈ ℂ → ( 𝑧 ↑ 2 ) ∈ ℂ )
5 4 adantl ⊢ ( ( ⊤ ∧ 𝑧 ∈ ℂ ) → ( 𝑧 ↑ 2 ) ∈ ℂ )
6 ax-1cn ⊢ 1 ∈ ℂ
7 6 a1i ⊢ ( ( ⊤ ∧ 𝑧 ∈ ℂ ) → 1 ∈ ℂ )
8 eqidd ⊢ ( ⊤ → ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 2 ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 2 ) ) )
9 fconstmpt ⊢ ( ℂ × { 1 } ) = ( 𝑧 ∈ ℂ ↦ 1 )
10 9 a1i ⊢ ( ⊤ → ( ℂ × { 1 } ) = ( 𝑧 ∈ ℂ ↦ 1 ) )
11 3 5 7 8 10 offval2 ⊢ ( ⊤ → ( ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 2 ) ) ∘f + ( ℂ × { 1 } ) ) = ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) )
12 zsscn ⊢ ℤ ⊆ ℂ
13 1z ⊢ 1 ∈ ℤ
14 2nn0 ⊢ 2 ∈ ℕ0
15 plypow ⊢ ( ( ℤ ⊆ ℂ ∧ 1 ∈ ℤ ∧ 2 ∈ ℕ0 ) → ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 2 ) ) ∈ ( Poly ‘ ℤ ) )
16 12 13 14 15 mp3an ⊢ ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 2 ) ) ∈ ( Poly ‘ ℤ )
17 16 a1i ⊢ ( ⊤ → ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 2 ) ) ∈ ( Poly ‘ ℤ ) )
18 plyconst ⊢ ( ( ℤ ⊆ ℂ ∧ 1 ∈ ℤ ) → ( ℂ × { 1 } ) ∈ ( Poly ‘ ℤ ) )
19 12 13 18 mp2an ⊢ ( ℂ × { 1 } ) ∈ ( Poly ‘ ℤ )
20 19 a1i ⊢ ( ⊤ → ( ℂ × { 1 } ) ∈ ( Poly ‘ ℤ ) )
21 zaddcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 + 𝑦 ) ∈ ℤ )
22 21 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 + 𝑦 ) ∈ ℤ )
23 17 20 22 plyadd ⊢ ( ⊤ → ( ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 2 ) ) ∘f + ( ℂ × { 1 } ) ) ∈ ( Poly ‘ ℤ ) )
24 11 23 eqeltrrd ⊢ ( ⊤ → ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ∈ ( Poly ‘ ℤ ) )
25 24 mptru ⊢ ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ∈ ( Poly ‘ ℤ )
26 0cn ⊢ 0 ∈ ℂ
27 sq0i ⊢ ( 𝑧 = 0 → ( 𝑧 ↑ 2 ) = 0 )
28 27 oveq1d ⊢ ( 𝑧 = 0 → ( ( 𝑧 ↑ 2 ) + 1 ) = ( 0 + 1 ) )
29 0p1e1 ⊢ ( 0 + 1 ) = 1
30 28 29 eqtrdi ⊢ ( 𝑧 = 0 → ( ( 𝑧 ↑ 2 ) + 1 ) = 1 )
31 eqid ⊢ ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) = ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) )
32 1ex ⊢ 1 ∈ V
33 30 31 32 fvmpt ⊢ ( 0 ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ‘ 0 ) = 1 )
34 26 33 ax-mp ⊢ ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ‘ 0 ) = 1
35 ax-1ne0 ⊢ 1 ≠ 0
36 34 35 eqnetri ⊢ ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ‘ 0 ) ≠ 0
37 ne0p ⊢ ( ( 0 ∈ ℂ ∧ ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ‘ 0 ) ≠ 0 ) → ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ≠ 0𝑝 )
38 26 36 37 mp2an ⊢ ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ≠ 0𝑝
39 eldifsn ⊢ ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ↔ ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ∈ ( Poly ‘ ℤ ) ∧ ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ≠ 0𝑝 ) )
40 25 38 39 mpbir2an ⊢ ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } )
41 oveq1 ⊢ ( 𝑧 = i → ( 𝑧 ↑ 2 ) = ( i ↑ 2 ) )
42 i2 ⊢ ( i ↑ 2 ) = - 1
43 41 42 eqtrdi ⊢ ( 𝑧 = i → ( 𝑧 ↑ 2 ) = - 1 )
44 43 oveq1d ⊢ ( 𝑧 = i → ( ( 𝑧 ↑ 2 ) + 1 ) = ( - 1 + 1 ) )
45 neg1cn ⊢ - 1 ∈ ℂ
46 1pneg1e0 ⊢ ( 1 + - 1 ) = 0
47 6 45 46 addcomli ⊢ ( - 1 + 1 ) = 0
48 44 47 eqtrdi ⊢ ( 𝑧 = i → ( ( 𝑧 ↑ 2 ) + 1 ) = 0 )
49 c0ex ⊢ 0 ∈ V
50 48 31 49 fvmpt ⊢ ( i ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ‘ i ) = 0 )
51 1 50 ax-mp ⊢ ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ‘ i ) = 0
52 fveq1 ⊢ ( 𝑓 = ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) → ( 𝑓 ‘ i ) = ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ‘ i ) )
53 52 eqeq1d ⊢ ( 𝑓 = ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) → ( ( 𝑓 ‘ i ) = 0 ↔ ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ‘ i ) = 0 ) )
54 53 rspcev ⊢ ( ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ 2 ) + 1 ) ) ‘ i ) = 0 ) → ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ i ) = 0 )
55 40 51 54 mp2an ⊢ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ i ) = 0
56 elaa ⊢ ( i ∈ 𝔸 ↔ ( i ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ i ) = 0 ) )
57 1 55 56 mpbir2an ⊢ i ∈ 𝔸