| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ax-icn 11214 | . 2
⊢ i ∈
ℂ | 
| 2 |  | cnex 11236 | . . . . . . . 8
⊢ ℂ
∈ V | 
| 3 | 2 | a1i 11 | . . . . . . 7
⊢ (⊤
→ ℂ ∈ V) | 
| 4 |  | sqcl 14158 | . . . . . . . 8
⊢ (𝑧 ∈ ℂ → (𝑧↑2) ∈
ℂ) | 
| 5 | 4 | adantl 481 | . . . . . . 7
⊢
((⊤ ∧ 𝑧
∈ ℂ) → (𝑧↑2) ∈ ℂ) | 
| 6 |  | ax-1cn 11213 | . . . . . . . 8
⊢ 1 ∈
ℂ | 
| 7 | 6 | a1i 11 | . . . . . . 7
⊢
((⊤ ∧ 𝑧
∈ ℂ) → 1 ∈ ℂ) | 
| 8 |  | eqidd 2738 | . . . . . . 7
⊢ (⊤
→ (𝑧 ∈ ℂ
↦ (𝑧↑2)) =
(𝑧 ∈ ℂ ↦
(𝑧↑2))) | 
| 9 |  | fconstmpt 5747 | . . . . . . . 8
⊢ (ℂ
× {1}) = (𝑧 ∈
ℂ ↦ 1) | 
| 10 | 9 | a1i 11 | . . . . . . 7
⊢ (⊤
→ (ℂ × {1}) = (𝑧 ∈ ℂ ↦ 1)) | 
| 11 | 3, 5, 7, 8, 10 | offval2 7717 | . . . . . 6
⊢ (⊤
→ ((𝑧 ∈ ℂ
↦ (𝑧↑2))
∘f + (ℂ × {1})) = (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1))) | 
| 12 |  | zsscn 12621 | . . . . . . . . 9
⊢ ℤ
⊆ ℂ | 
| 13 |  | 1z 12647 | . . . . . . . . 9
⊢ 1 ∈
ℤ | 
| 14 |  | 2nn0 12543 | . . . . . . . . 9
⊢ 2 ∈
ℕ0 | 
| 15 |  | plypow 26244 | . . . . . . . . 9
⊢ ((ℤ
⊆ ℂ ∧ 1 ∈ ℤ ∧ 2 ∈ ℕ0)
→ (𝑧 ∈ ℂ
↦ (𝑧↑2)) ∈
(Poly‘ℤ)) | 
| 16 | 12, 13, 14, 15 | mp3an 1463 | . . . . . . . 8
⊢ (𝑧 ∈ ℂ ↦ (𝑧↑2)) ∈
(Poly‘ℤ) | 
| 17 | 16 | a1i 11 | . . . . . . 7
⊢ (⊤
→ (𝑧 ∈ ℂ
↦ (𝑧↑2)) ∈
(Poly‘ℤ)) | 
| 18 |  | plyconst 26245 | . . . . . . . . 9
⊢ ((ℤ
⊆ ℂ ∧ 1 ∈ ℤ) → (ℂ × {1}) ∈
(Poly‘ℤ)) | 
| 19 | 12, 13, 18 | mp2an 692 | . . . . . . . 8
⊢ (ℂ
× {1}) ∈ (Poly‘ℤ) | 
| 20 | 19 | a1i 11 | . . . . . . 7
⊢ (⊤
→ (ℂ × {1}) ∈ (Poly‘ℤ)) | 
| 21 |  | zaddcl 12657 | . . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 + 𝑦) ∈ ℤ) | 
| 22 | 21 | adantl 481 | . . . . . . 7
⊢
((⊤ ∧ (𝑥
∈ ℤ ∧ 𝑦
∈ ℤ)) → (𝑥
+ 𝑦) ∈
ℤ) | 
| 23 | 17, 20, 22 | plyadd 26256 | . . . . . 6
⊢ (⊤
→ ((𝑧 ∈ ℂ
↦ (𝑧↑2))
∘f + (ℂ × {1})) ∈
(Poly‘ℤ)) | 
| 24 | 11, 23 | eqeltrrd 2842 | . . . . 5
⊢ (⊤
→ (𝑧 ∈ ℂ
↦ ((𝑧↑2) + 1))
∈ (Poly‘ℤ)) | 
| 25 | 24 | mptru 1547 | . . . 4
⊢ (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) ∈
(Poly‘ℤ) | 
| 26 |  | 0cn 11253 | . . . . 5
⊢ 0 ∈
ℂ | 
| 27 |  | sq0i 14232 | . . . . . . . . . 10
⊢ (𝑧 = 0 → (𝑧↑2) = 0) | 
| 28 | 27 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝑧 = 0 → ((𝑧↑2) + 1) = (0 + 1)) | 
| 29 |  | 0p1e1 12388 | . . . . . . . . 9
⊢ (0 + 1) =
1 | 
| 30 | 28, 29 | eqtrdi 2793 | . . . . . . . 8
⊢ (𝑧 = 0 → ((𝑧↑2) + 1) = 1) | 
| 31 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) = (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) | 
| 32 |  | 1ex 11257 | . . . . . . . 8
⊢ 1 ∈
V | 
| 33 | 30, 31, 32 | fvmpt 7016 | . . . . . . 7
⊢ (0 ∈
ℂ → ((𝑧 ∈
ℂ ↦ ((𝑧↑2)
+ 1))‘0) = 1) | 
| 34 | 26, 33 | ax-mp 5 | . . . . . 6
⊢ ((𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1))‘0) =
1 | 
| 35 |  | ax-1ne0 11224 | . . . . . 6
⊢ 1 ≠
0 | 
| 36 | 34, 35 | eqnetri 3011 | . . . . 5
⊢ ((𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1))‘0) ≠
0 | 
| 37 |  | ne0p 26246 | . . . . 5
⊢ ((0
∈ ℂ ∧ ((𝑧
∈ ℂ ↦ ((𝑧↑2) + 1))‘0) ≠ 0) → (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) ≠
0𝑝) | 
| 38 | 26, 36, 37 | mp2an 692 | . . . 4
⊢ (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) ≠
0𝑝 | 
| 39 |  | eldifsn 4786 | . . . 4
⊢ ((𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) ∈
((Poly‘ℤ) ∖ {0𝑝}) ↔ ((𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) ∈
(Poly‘ℤ) ∧ (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) ≠
0𝑝)) | 
| 40 | 25, 38, 39 | mpbir2an 711 | . . 3
⊢ (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) ∈
((Poly‘ℤ) ∖ {0𝑝}) | 
| 41 |  | oveq1 7438 | . . . . . . . 8
⊢ (𝑧 = i → (𝑧↑2) = (i↑2)) | 
| 42 |  | i2 14241 | . . . . . . . 8
⊢
(i↑2) = -1 | 
| 43 | 41, 42 | eqtrdi 2793 | . . . . . . 7
⊢ (𝑧 = i → (𝑧↑2) = -1) | 
| 44 | 43 | oveq1d 7446 | . . . . . 6
⊢ (𝑧 = i → ((𝑧↑2) + 1) = (-1 + 1)) | 
| 45 |  | neg1cn 12380 | . . . . . . 7
⊢ -1 ∈
ℂ | 
| 46 |  | 1pneg1e0 12385 | . . . . . . 7
⊢ (1 + -1)
= 0 | 
| 47 | 6, 45, 46 | addcomli 11453 | . . . . . 6
⊢ (-1 + 1)
= 0 | 
| 48 | 44, 47 | eqtrdi 2793 | . . . . 5
⊢ (𝑧 = i → ((𝑧↑2) + 1) = 0) | 
| 49 |  | c0ex 11255 | . . . . 5
⊢ 0 ∈
V | 
| 50 | 48, 31, 49 | fvmpt 7016 | . . . 4
⊢ (i ∈
ℂ → ((𝑧 ∈
ℂ ↦ ((𝑧↑2)
+ 1))‘i) = 0) | 
| 51 | 1, 50 | ax-mp 5 | . . 3
⊢ ((𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1))‘i) =
0 | 
| 52 |  | fveq1 6905 | . . . . 5
⊢ (𝑓 = (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) → (𝑓‘i) = ((𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1))‘i)) | 
| 53 | 52 | eqeq1d 2739 | . . . 4
⊢ (𝑓 = (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) → ((𝑓‘i) = 0 ↔ ((𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1))‘i) =
0)) | 
| 54 | 53 | rspcev 3622 | . . 3
⊢ (((𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) ∈
((Poly‘ℤ) ∖ {0𝑝}) ∧ ((𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1))‘i) = 0)
→ ∃𝑓 ∈
((Poly‘ℤ) ∖ {0𝑝})(𝑓‘i) = 0) | 
| 55 | 40, 51, 54 | mp2an 692 | . 2
⊢
∃𝑓 ∈
((Poly‘ℤ) ∖ {0𝑝})(𝑓‘i) = 0 | 
| 56 |  | elaa 26358 | . 2
⊢ (i ∈
𝔸 ↔ (i ∈ ℂ ∧ ∃𝑓 ∈ ((Poly‘ℤ) ∖
{0𝑝})(𝑓‘i) = 0)) | 
| 57 | 1, 55, 56 | mpbir2an 711 | 1
⊢ i ∈
𝔸 |