Step | Hyp | Ref
| Expression |
1 | | ax-icn 10674 |
. 2
⊢ i ∈
ℂ |
2 | | cnex 10696 |
. . . . . . . 8
⊢ ℂ
∈ V |
3 | 2 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ ℂ ∈ V) |
4 | | sqcl 13576 |
. . . . . . . 8
⊢ (𝑧 ∈ ℂ → (𝑧↑2) ∈
ℂ) |
5 | 4 | adantl 485 |
. . . . . . 7
⊢
((⊤ ∧ 𝑧
∈ ℂ) → (𝑧↑2) ∈ ℂ) |
6 | | ax-1cn 10673 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
7 | 6 | a1i 11 |
. . . . . . 7
⊢
((⊤ ∧ 𝑧
∈ ℂ) → 1 ∈ ℂ) |
8 | | eqidd 2739 |
. . . . . . 7
⊢ (⊤
→ (𝑧 ∈ ℂ
↦ (𝑧↑2)) =
(𝑧 ∈ ℂ ↦
(𝑧↑2))) |
9 | | fconstmpt 5585 |
. . . . . . . 8
⊢ (ℂ
× {1}) = (𝑧 ∈
ℂ ↦ 1) |
10 | 9 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (ℂ × {1}) = (𝑧 ∈ ℂ ↦ 1)) |
11 | 3, 5, 7, 8, 10 | offval2 7444 |
. . . . . 6
⊢ (⊤
→ ((𝑧 ∈ ℂ
↦ (𝑧↑2))
∘f + (ℂ × {1})) = (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1))) |
12 | | zsscn 12070 |
. . . . . . . . 9
⊢ ℤ
⊆ ℂ |
13 | | 1z 12093 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
14 | | 2nn0 11993 |
. . . . . . . . 9
⊢ 2 ∈
ℕ0 |
15 | | plypow 24954 |
. . . . . . . . 9
⊢ ((ℤ
⊆ ℂ ∧ 1 ∈ ℤ ∧ 2 ∈ ℕ0)
→ (𝑧 ∈ ℂ
↦ (𝑧↑2)) ∈
(Poly‘ℤ)) |
16 | 12, 13, 14, 15 | mp3an 1462 |
. . . . . . . 8
⊢ (𝑧 ∈ ℂ ↦ (𝑧↑2)) ∈
(Poly‘ℤ) |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (𝑧 ∈ ℂ
↦ (𝑧↑2)) ∈
(Poly‘ℤ)) |
18 | | plyconst 24955 |
. . . . . . . . 9
⊢ ((ℤ
⊆ ℂ ∧ 1 ∈ ℤ) → (ℂ × {1}) ∈
(Poly‘ℤ)) |
19 | 12, 13, 18 | mp2an 692 |
. . . . . . . 8
⊢ (ℂ
× {1}) ∈ (Poly‘ℤ) |
20 | 19 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (ℂ × {1}) ∈ (Poly‘ℤ)) |
21 | | zaddcl 12103 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 + 𝑦) ∈ ℤ) |
22 | 21 | adantl 485 |
. . . . . . 7
⊢
((⊤ ∧ (𝑥
∈ ℤ ∧ 𝑦
∈ ℤ)) → (𝑥
+ 𝑦) ∈
ℤ) |
23 | 17, 20, 22 | plyadd 24966 |
. . . . . 6
⊢ (⊤
→ ((𝑧 ∈ ℂ
↦ (𝑧↑2))
∘f + (ℂ × {1})) ∈
(Poly‘ℤ)) |
24 | 11, 23 | eqeltrrd 2834 |
. . . . 5
⊢ (⊤
→ (𝑧 ∈ ℂ
↦ ((𝑧↑2) + 1))
∈ (Poly‘ℤ)) |
25 | 24 | mptru 1549 |
. . . 4
⊢ (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) ∈
(Poly‘ℤ) |
26 | | 0cn 10711 |
. . . . 5
⊢ 0 ∈
ℂ |
27 | | sq0i 13648 |
. . . . . . . . . 10
⊢ (𝑧 = 0 → (𝑧↑2) = 0) |
28 | 27 | oveq1d 7185 |
. . . . . . . . 9
⊢ (𝑧 = 0 → ((𝑧↑2) + 1) = (0 + 1)) |
29 | | 0p1e1 11838 |
. . . . . . . . 9
⊢ (0 + 1) =
1 |
30 | 28, 29 | eqtrdi 2789 |
. . . . . . . 8
⊢ (𝑧 = 0 → ((𝑧↑2) + 1) = 1) |
31 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) = (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) |
32 | | 1ex 10715 |
. . . . . . . 8
⊢ 1 ∈
V |
33 | 30, 31, 32 | fvmpt 6775 |
. . . . . . 7
⊢ (0 ∈
ℂ → ((𝑧 ∈
ℂ ↦ ((𝑧↑2)
+ 1))‘0) = 1) |
34 | 26, 33 | ax-mp 5 |
. . . . . 6
⊢ ((𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1))‘0) =
1 |
35 | | ax-1ne0 10684 |
. . . . . 6
⊢ 1 ≠
0 |
36 | 34, 35 | eqnetri 3004 |
. . . . 5
⊢ ((𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1))‘0) ≠
0 |
37 | | ne0p 24956 |
. . . . 5
⊢ ((0
∈ ℂ ∧ ((𝑧
∈ ℂ ↦ ((𝑧↑2) + 1))‘0) ≠ 0) → (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) ≠
0𝑝) |
38 | 26, 36, 37 | mp2an 692 |
. . . 4
⊢ (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) ≠
0𝑝 |
39 | | eldifsn 4675 |
. . . 4
⊢ ((𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) ∈
((Poly‘ℤ) ∖ {0𝑝}) ↔ ((𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) ∈
(Poly‘ℤ) ∧ (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) ≠
0𝑝)) |
40 | 25, 38, 39 | mpbir2an 711 |
. . 3
⊢ (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) ∈
((Poly‘ℤ) ∖ {0𝑝}) |
41 | | oveq1 7177 |
. . . . . . . 8
⊢ (𝑧 = i → (𝑧↑2) = (i↑2)) |
42 | | i2 13657 |
. . . . . . . 8
⊢
(i↑2) = -1 |
43 | 41, 42 | eqtrdi 2789 |
. . . . . . 7
⊢ (𝑧 = i → (𝑧↑2) = -1) |
44 | 43 | oveq1d 7185 |
. . . . . 6
⊢ (𝑧 = i → ((𝑧↑2) + 1) = (-1 + 1)) |
45 | | neg1cn 11830 |
. . . . . . 7
⊢ -1 ∈
ℂ |
46 | | 1pneg1e0 11835 |
. . . . . . 7
⊢ (1 + -1)
= 0 |
47 | 6, 45, 46 | addcomli 10910 |
. . . . . 6
⊢ (-1 + 1)
= 0 |
48 | 44, 47 | eqtrdi 2789 |
. . . . 5
⊢ (𝑧 = i → ((𝑧↑2) + 1) = 0) |
49 | | c0ex 10713 |
. . . . 5
⊢ 0 ∈
V |
50 | 48, 31, 49 | fvmpt 6775 |
. . . 4
⊢ (i ∈
ℂ → ((𝑧 ∈
ℂ ↦ ((𝑧↑2)
+ 1))‘i) = 0) |
51 | 1, 50 | ax-mp 5 |
. . 3
⊢ ((𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1))‘i) =
0 |
52 | | fveq1 6673 |
. . . . 5
⊢ (𝑓 = (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) → (𝑓‘i) = ((𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1))‘i)) |
53 | 52 | eqeq1d 2740 |
. . . 4
⊢ (𝑓 = (𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1)) → ((𝑓‘i) = 0 ↔ ((𝑧 ∈ ℂ ↦ ((𝑧↑2) + 1))‘i) =
0)) |
54 | 53 | rspcev 3526 |
. . 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 25064 |
. 2
⊢ (i ∈
𝔸 ↔ (i ∈ ℂ ∧ ∃𝑓 ∈ ((Poly‘ℤ) ∖
{0𝑝})(𝑓‘i) = 0)) |
57 | 1, 55, 56 | mpbir2an 711 |
1
⊢ i ∈
𝔸 |