Step | Hyp | Ref
| Expression |
1 | | elqaa.1 |
. 2
⊢ (𝜑 → 𝐴 ∈ ℂ) |
2 | | cnex 9896 |
. . . . . . . 8
⊢ ℂ
∈ V |
3 | 2 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℂ ∈
V) |
4 | | elqaa.6 |
. . . . . . . . 9
⊢ 𝑅 = (seq0( · , 𝑁)‘(deg‘𝐹)) |
5 | | fvex 6113 |
. . . . . . . . 9
⊢ (seq0(
· , 𝑁)‘(deg‘𝐹)) ∈ V |
6 | 4, 5 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝑅 ∈ V |
7 | 6 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑅 ∈ V) |
8 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐹‘𝑧) ∈ V |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝐹‘𝑧) ∈ V) |
10 | | fconstmpt 5085 |
. . . . . . . 8
⊢ (ℂ
× {𝑅}) = (𝑧 ∈ ℂ ↦ 𝑅) |
11 | 10 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (ℂ × {𝑅}) = (𝑧 ∈ ℂ ↦ 𝑅)) |
12 | | elqaa.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ((Poly‘ℚ) ∖
{0𝑝})) |
13 | 12 | eldifad 3552 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℚ)) |
14 | | plyf 23758 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘ℚ)
→ 𝐹:ℂ⟶ℂ) |
15 | 13, 14 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
16 | 15 | feqmptd 6159 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ (𝐹‘𝑧))) |
17 | 3, 7, 9, 11, 16 | offval2 6812 |
. . . . . 6
⊢ (𝜑 → ((ℂ × {𝑅}) ∘𝑓
· 𝐹) = (𝑧 ∈ ℂ ↦ (𝑅 · (𝐹‘𝑧)))) |
18 | | fzfid 12634 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...(deg‘𝐹)) ∈ Fin) |
19 | | nn0uz 11598 |
. . . . . . . . . . . . . 14
⊢
ℕ0 = (ℤ≥‘0) |
20 | | 0zd 11266 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ∈
ℤ) |
21 | | ssrab2 3650 |
. . . . . . . . . . . . . . 15
⊢ {𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ} ⊆
ℕ |
22 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑚 → (𝐵‘𝑘) = (𝐵‘𝑚)) |
23 | 22 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑚 → ((𝐵‘𝑘) · 𝑛) = ((𝐵‘𝑚) · 𝑛)) |
24 | 23 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑚 → (((𝐵‘𝑘) · 𝑛) ∈ ℤ ↔ ((𝐵‘𝑚) · 𝑛) ∈ ℤ)) |
25 | 24 | rabbidv 3164 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑚 → {𝑛 ∈ ℕ ∣ ((𝐵‘𝑘) · 𝑛) ∈ ℤ} = {𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}) |
26 | 25 | infeq1d 8266 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑚 → inf({𝑛 ∈ ℕ ∣ ((𝐵‘𝑘) · 𝑛) ∈ ℤ}, ℝ, < ) =
inf({𝑛 ∈ ℕ
∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}, ℝ, <
)) |
27 | | elqaa.5 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑁 = (𝑘 ∈ ℕ0 ↦
inf({𝑛 ∈ ℕ
∣ ((𝐵‘𝑘) · 𝑛) ∈ ℤ}, ℝ, <
)) |
28 | | ltso 9997 |
. . . . . . . . . . . . . . . . . . 19
⊢ < Or
ℝ |
29 | 28 | infex 8282 |
. . . . . . . . . . . . . . . . . 18
⊢
inf({𝑛 ∈
ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}, ℝ, < ) ∈
V |
30 | 26, 27, 29 | fvmpt 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕ0
→ (𝑁‘𝑚) = inf({𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}, ℝ, <
)) |
31 | 30 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁‘𝑚) = inf({𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}, ℝ, <
)) |
32 | | nnuz 11599 |
. . . . . . . . . . . . . . . . . 18
⊢ ℕ =
(ℤ≥‘1) |
33 | 21, 32 | sseqtri 3600 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ} ⊆
(ℤ≥‘1) |
34 | | 0z 11265 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℤ |
35 | | zq 11670 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ∈
ℤ → 0 ∈ ℚ) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
ℚ |
37 | | elqaa.4 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐵 = (coeff‘𝐹) |
38 | 37 | coef2 23791 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 ∈ (Poly‘ℚ)
∧ 0 ∈ ℚ) → 𝐵:ℕ0⟶ℚ) |
39 | 13, 36, 38 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐵:ℕ0⟶ℚ) |
40 | 39 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝐵‘𝑚) ∈ ℚ) |
41 | | qmulz 11667 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵‘𝑚) ∈ ℚ → ∃𝑛 ∈ ℕ ((𝐵‘𝑚) · 𝑛) ∈ ℤ) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
∃𝑛 ∈ ℕ
((𝐵‘𝑚) · 𝑛) ∈ ℤ) |
43 | | rabn0 3912 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ} ≠ ∅ ↔
∃𝑛 ∈ ℕ
((𝐵‘𝑚) · 𝑛) ∈ ℤ) |
44 | 42, 43 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → {𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ} ≠
∅) |
45 | | infssuzcl 11648 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ} ⊆
(ℤ≥‘1) ∧ {𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ} ≠ ∅) →
inf({𝑛 ∈ ℕ
∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}, ℝ, < ) ∈
{𝑛 ∈ ℕ ∣
((𝐵‘𝑚) · 𝑛) ∈ ℤ}) |
46 | 33, 44, 45 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
inf({𝑛 ∈ ℕ
∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}, ℝ, < ) ∈
{𝑛 ∈ ℕ ∣
((𝐵‘𝑚) · 𝑛) ∈ ℤ}) |
47 | 31, 46 | eqeltrd 2688 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁‘𝑚) ∈ {𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}) |
48 | 21, 47 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁‘𝑚) ∈ ℕ) |
49 | | nnmulcl 10920 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑚 · 𝑘) ∈ ℕ) |
50 | 49 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝑚 · 𝑘) ∈ ℕ) |
51 | 19, 20, 48, 50 | seqf 12684 |
. . . . . . . . . . . . 13
⊢ (𝜑 → seq0( · , 𝑁):ℕ0⟶ℕ) |
52 | | dgrcl 23793 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (Poly‘ℚ)
→ (deg‘𝐹) ∈
ℕ0) |
53 | 13, 52 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (deg‘𝐹) ∈
ℕ0) |
54 | 51, 53 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (𝜑 → (seq0( · , 𝑁)‘(deg‘𝐹)) ∈
ℕ) |
55 | 4, 54 | syl5eqel 2692 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ ℕ) |
56 | 55 | nncnd 10913 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ ℂ) |
57 | 56 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑅 ∈ ℂ) |
58 | | elfznn0 12302 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (0...(deg‘𝐹)) → 𝑚 ∈ ℕ0) |
59 | 37 | coef3 23792 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (Poly‘ℚ)
→ 𝐵:ℕ0⟶ℂ) |
60 | 13, 59 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵:ℕ0⟶ℂ) |
61 | 60 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝐵:ℕ0⟶ℂ) |
62 | 61 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑚 ∈ ℕ0) → (𝐵‘𝑚) ∈ ℂ) |
63 | | expcl 12740 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℂ ∧ 𝑚 ∈ ℕ0)
→ (𝑧↑𝑚) ∈
ℂ) |
64 | 63 | adantll 746 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑚 ∈ ℕ0) → (𝑧↑𝑚) ∈ ℂ) |
65 | 62, 64 | mulcld 9939 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑚 ∈ ℕ0) → ((𝐵‘𝑚) · (𝑧↑𝑚)) ∈ ℂ) |
66 | 58, 65 | sylan2 490 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑚 ∈ (0...(deg‘𝐹))) → ((𝐵‘𝑚) · (𝑧↑𝑚)) ∈ ℂ) |
67 | 18, 57, 66 | fsummulc2 14358 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑅 · Σ𝑚 ∈ (0...(deg‘𝐹))((𝐵‘𝑚) · (𝑧↑𝑚))) = Σ𝑚 ∈ (0...(deg‘𝐹))(𝑅 · ((𝐵‘𝑚) · (𝑧↑𝑚)))) |
68 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(deg‘𝐹) =
(deg‘𝐹) |
69 | 37, 68 | coeid2 23799 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘ℚ)
∧ 𝑧 ∈ ℂ)
→ (𝐹‘𝑧) = Σ𝑚 ∈ (0...(deg‘𝐹))((𝐵‘𝑚) · (𝑧↑𝑚))) |
70 | 13, 69 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝐹‘𝑧) = Σ𝑚 ∈ (0...(deg‘𝐹))((𝐵‘𝑚) · (𝑧↑𝑚))) |
71 | 70 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑅 · (𝐹‘𝑧)) = (𝑅 · Σ𝑚 ∈ (0...(deg‘𝐹))((𝐵‘𝑚) · (𝑧↑𝑚)))) |
72 | 57 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑚 ∈ ℕ0) → 𝑅 ∈
ℂ) |
73 | 72, 62, 64 | mulassd 9942 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑚 ∈ ℕ0) → ((𝑅 · (𝐵‘𝑚)) · (𝑧↑𝑚)) = (𝑅 · ((𝐵‘𝑚) · (𝑧↑𝑚)))) |
74 | 58, 73 | sylan2 490 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑚 ∈ (0...(deg‘𝐹))) → ((𝑅 · (𝐵‘𝑚)) · (𝑧↑𝑚)) = (𝑅 · ((𝐵‘𝑚) · (𝑧↑𝑚)))) |
75 | 74 | sumeq2dv 14281 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑚 ∈ (0...(deg‘𝐹))((𝑅 · (𝐵‘𝑚)) · (𝑧↑𝑚)) = Σ𝑚 ∈ (0...(deg‘𝐹))(𝑅 · ((𝐵‘𝑚) · (𝑧↑𝑚)))) |
76 | 67, 71, 75 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑅 · (𝐹‘𝑧)) = Σ𝑚 ∈ (0...(deg‘𝐹))((𝑅 · (𝐵‘𝑚)) · (𝑧↑𝑚))) |
77 | 76 | mpteq2dva 4672 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ (𝑅 · (𝐹‘𝑧))) = (𝑧 ∈ ℂ ↦ Σ𝑚 ∈ (0...(deg‘𝐹))((𝑅 · (𝐵‘𝑚)) · (𝑧↑𝑚)))) |
78 | 17, 77 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → ((ℂ × {𝑅}) ∘𝑓
· 𝐹) = (𝑧 ∈ ℂ ↦
Σ𝑚 ∈
(0...(deg‘𝐹))((𝑅 · (𝐵‘𝑚)) · (𝑧↑𝑚)))) |
79 | | zsscn 11262 |
. . . . . . 7
⊢ ℤ
⊆ ℂ |
80 | 79 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℤ ⊆
ℂ) |
81 | 56 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑅 ∈
ℂ) |
82 | 48 | nncnd 10913 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁‘𝑚) ∈ ℂ) |
83 | 48 | nnne0d 10942 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁‘𝑚) ≠ 0) |
84 | 81, 82, 83 | divcan2d 10682 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑁‘𝑚) · (𝑅 / (𝑁‘𝑚))) = 𝑅) |
85 | 84 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝐵‘𝑚) · ((𝑁‘𝑚) · (𝑅 / (𝑁‘𝑚)))) = ((𝐵‘𝑚) · 𝑅)) |
86 | 60 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝐵‘𝑚) ∈ ℂ) |
87 | 81, 82, 83 | divcld 10680 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑅 / (𝑁‘𝑚)) ∈ ℂ) |
88 | 86, 82, 87 | mulassd 9942 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (((𝐵‘𝑚) · (𝑁‘𝑚)) · (𝑅 / (𝑁‘𝑚))) = ((𝐵‘𝑚) · ((𝑁‘𝑚) · (𝑅 / (𝑁‘𝑚))))) |
89 | 81, 86 | mulcomd 9940 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑅 · (𝐵‘𝑚)) = ((𝐵‘𝑚) · 𝑅)) |
90 | 85, 88, 89 | 3eqtr4rd 2655 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑅 · (𝐵‘𝑚)) = (((𝐵‘𝑚) · (𝑁‘𝑚)) · (𝑅 / (𝑁‘𝑚)))) |
91 | 58, 90 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → (𝑅 · (𝐵‘𝑚)) = (((𝐵‘𝑚) · (𝑁‘𝑚)) · (𝑅 / (𝑁‘𝑚)))) |
92 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑁‘𝑚) → ((𝐵‘𝑚) · 𝑛) = ((𝐵‘𝑚) · (𝑁‘𝑚))) |
93 | 92 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑁‘𝑚) → (((𝐵‘𝑚) · 𝑛) ∈ ℤ ↔ ((𝐵‘𝑚) · (𝑁‘𝑚)) ∈ ℤ)) |
94 | 93 | elrab 3331 |
. . . . . . . . . . 11
⊢ ((𝑁‘𝑚) ∈ {𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ} ↔ ((𝑁‘𝑚) ∈ ℕ ∧ ((𝐵‘𝑚) · (𝑁‘𝑚)) ∈ ℤ)) |
95 | 94 | simprbi 479 |
. . . . . . . . . 10
⊢ ((𝑁‘𝑚) ∈ {𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ} → ((𝐵‘𝑚) · (𝑁‘𝑚)) ∈ ℤ) |
96 | 47, 95 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝐵‘𝑚) · (𝑁‘𝑚)) ∈ ℤ) |
97 | 58, 96 | sylan2 490 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → ((𝐵‘𝑚) · (𝑁‘𝑚)) ∈ ℤ) |
98 | | elqaa.3 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝐴) = 0) |
99 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 · 𝑦) mod (𝑁‘𝑚))) = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 · 𝑦) mod (𝑁‘𝑚))) |
100 | 1, 12, 98, 37, 27, 4, 99 | elqaalem2 23879 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → (𝑅 mod (𝑁‘𝑚)) = 0) |
101 | 55 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → 𝑅 ∈ ℕ) |
102 | 58, 48 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → (𝑁‘𝑚) ∈ ℕ) |
103 | | nnre 10904 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℕ → 𝑅 ∈
ℝ) |
104 | | nnrp 11718 |
. . . . . . . . . . 11
⊢ ((𝑁‘𝑚) ∈ ℕ → (𝑁‘𝑚) ∈
ℝ+) |
105 | | mod0 12537 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ ∧ (𝑁‘𝑚) ∈ ℝ+) → ((𝑅 mod (𝑁‘𝑚)) = 0 ↔ (𝑅 / (𝑁‘𝑚)) ∈ ℤ)) |
106 | 103, 104,
105 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℕ ∧ (𝑁‘𝑚) ∈ ℕ) → ((𝑅 mod (𝑁‘𝑚)) = 0 ↔ (𝑅 / (𝑁‘𝑚)) ∈ ℤ)) |
107 | 101, 102,
106 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → ((𝑅 mod (𝑁‘𝑚)) = 0 ↔ (𝑅 / (𝑁‘𝑚)) ∈ ℤ)) |
108 | 100, 107 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → (𝑅 / (𝑁‘𝑚)) ∈ ℤ) |
109 | 97, 108 | zmulcld 11364 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → (((𝐵‘𝑚) · (𝑁‘𝑚)) · (𝑅 / (𝑁‘𝑚))) ∈ ℤ) |
110 | 91, 109 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → (𝑅 · (𝐵‘𝑚)) ∈ ℤ) |
111 | 80, 53, 110 | elplyd 23762 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑚 ∈ (0...(deg‘𝐹))((𝑅 · (𝐵‘𝑚)) · (𝑧↑𝑚))) ∈
(Poly‘ℤ)) |
112 | 78, 111 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → ((ℂ × {𝑅}) ∘𝑓
· 𝐹) ∈
(Poly‘ℤ)) |
113 | | eldifsn 4260 |
. . . . . . 7
⊢ (𝐹 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ↔ (𝐹 ∈ (Poly‘ℚ) ∧ 𝐹 ≠
0𝑝)) |
114 | 12, 113 | sylib 207 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∈ (Poly‘ℚ) ∧ 𝐹 ≠
0𝑝)) |
115 | 114 | simprd 478 |
. . . . 5
⊢ (𝜑 → 𝐹 ≠
0𝑝) |
116 | | oveq1 6556 |
. . . . . . 7
⊢
(((ℂ × {𝑅}) ∘𝑓 ·
𝐹) = 0𝑝
→ (((ℂ × {𝑅}) ∘𝑓 ·
𝐹)
∘𝑓 / (ℂ × {𝑅})) = (0𝑝
∘𝑓 / (ℂ × {𝑅}))) |
117 | 15 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝐹‘𝑧) ∈ ℂ) |
118 | 55 | nnne0d 10942 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ≠ 0) |
119 | 118 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑅 ≠ 0) |
120 | 117, 57, 119 | divcan3d 10685 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝑅 · (𝐹‘𝑧)) / 𝑅) = (𝐹‘𝑧)) |
121 | 120 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ ((𝑅 · (𝐹‘𝑧)) / 𝑅)) = (𝑧 ∈ ℂ ↦ (𝐹‘𝑧))) |
122 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑅 · (𝐹‘𝑧)) ∈ V |
123 | 122 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑅 · (𝐹‘𝑧)) ∈ V) |
124 | 3, 123, 7, 17, 11 | offval2 6812 |
. . . . . . . . 9
⊢ (𝜑 → (((ℂ × {𝑅}) ∘𝑓
· 𝐹)
∘𝑓 / (ℂ × {𝑅})) = (𝑧 ∈ ℂ ↦ ((𝑅 · (𝐹‘𝑧)) / 𝑅))) |
125 | 121, 124,
16 | 3eqtr4d 2654 |
. . . . . . . 8
⊢ (𝜑 → (((ℂ × {𝑅}) ∘𝑓
· 𝐹)
∘𝑓 / (ℂ × {𝑅})) = 𝐹) |
126 | 56, 118 | div0d 10679 |
. . . . . . . . . 10
⊢ (𝜑 → (0 / 𝑅) = 0) |
127 | 126 | mpteq2dv 4673 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ (0 / 𝑅)) = (𝑧 ∈ ℂ ↦ 0)) |
128 | | 0cnd 9912 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 0 ∈
ℂ) |
129 | | df-0p 23243 |
. . . . . . . . . . . 12
⊢
0𝑝 = (ℂ × {0}) |
130 | | fconstmpt 5085 |
. . . . . . . . . . . 12
⊢ (ℂ
× {0}) = (𝑧 ∈
ℂ ↦ 0) |
131 | 129, 130 | eqtri 2632 |
. . . . . . . . . . 11
⊢
0𝑝 = (𝑧 ∈ ℂ ↦ 0) |
132 | 131 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0𝑝 =
(𝑧 ∈ ℂ ↦
0)) |
133 | 3, 128, 7, 132, 11 | offval2 6812 |
. . . . . . . . 9
⊢ (𝜑 → (0𝑝
∘𝑓 / (ℂ × {𝑅})) = (𝑧 ∈ ℂ ↦ (0 / 𝑅))) |
134 | 127, 133,
132 | 3eqtr4d 2654 |
. . . . . . . 8
⊢ (𝜑 → (0𝑝
∘𝑓 / (ℂ × {𝑅})) =
0𝑝) |
135 | 125, 134 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝜑 → ((((ℂ × {𝑅}) ∘𝑓
· 𝐹)
∘𝑓 / (ℂ × {𝑅})) = (0𝑝
∘𝑓 / (ℂ × {𝑅})) ↔ 𝐹 = 0𝑝)) |
136 | 116, 135 | syl5ib 233 |
. . . . . 6
⊢ (𝜑 → (((ℂ × {𝑅}) ∘𝑓
· 𝐹) =
0𝑝 → 𝐹 = 0𝑝)) |
137 | 136 | necon3d 2803 |
. . . . 5
⊢ (𝜑 → (𝐹 ≠ 0𝑝 → ((ℂ
× {𝑅})
∘𝑓 · 𝐹) ≠
0𝑝)) |
138 | 115, 137 | mpd 15 |
. . . 4
⊢ (𝜑 → ((ℂ × {𝑅}) ∘𝑓
· 𝐹) ≠
0𝑝) |
139 | | eldifsn 4260 |
. . . 4
⊢
(((ℂ × {𝑅}) ∘𝑓 ·
𝐹) ∈
((Poly‘ℤ) ∖ {0𝑝}) ↔ (((ℂ
× {𝑅})
∘𝑓 · 𝐹) ∈ (Poly‘ℤ) ∧
((ℂ × {𝑅})
∘𝑓 · 𝐹) ≠
0𝑝)) |
140 | 112, 138,
139 | sylanbrc 695 |
. . 3
⊢ (𝜑 → ((ℂ × {𝑅}) ∘𝑓
· 𝐹) ∈
((Poly‘ℤ) ∖ {0𝑝})) |
141 | 6 | fconst 6004 |
. . . . . . 7
⊢ (ℂ
× {𝑅}):ℂ⟶{𝑅} |
142 | | ffn 5958 |
. . . . . . 7
⊢ ((ℂ
× {𝑅}):ℂ⟶{𝑅} → (ℂ × {𝑅}) Fn ℂ) |
143 | 141, 142 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → (ℂ × {𝑅}) Fn ℂ) |
144 | | ffn 5958 |
. . . . . . 7
⊢ (𝐹:ℂ⟶ℂ →
𝐹 Fn
ℂ) |
145 | 15, 144 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn ℂ) |
146 | | inidm 3784 |
. . . . . 6
⊢ (ℂ
∩ ℂ) = ℂ |
147 | 6 | fvconst2 6374 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ((ℂ
× {𝑅})‘𝐴) = 𝑅) |
148 | 147 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → ((ℂ ×
{𝑅})‘𝐴) = 𝑅) |
149 | 98 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (𝐹‘𝐴) = 0) |
150 | 143, 145,
3, 3, 146, 148, 149 | ofval 6804 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (((ℂ ×
{𝑅})
∘𝑓 · 𝐹)‘𝐴) = (𝑅 · 0)) |
151 | 1, 150 | mpdan 699 |
. . . 4
⊢ (𝜑 → (((ℂ × {𝑅}) ∘𝑓
· 𝐹)‘𝐴) = (𝑅 · 0)) |
152 | 56 | mul01d 10114 |
. . . 4
⊢ (𝜑 → (𝑅 · 0) = 0) |
153 | 151, 152 | eqtrd 2644 |
. . 3
⊢ (𝜑 → (((ℂ × {𝑅}) ∘𝑓
· 𝐹)‘𝐴) = 0) |
154 | | fveq1 6102 |
. . . . 5
⊢ (𝑓 = ((ℂ × {𝑅}) ∘𝑓
· 𝐹) → (𝑓‘𝐴) = (((ℂ × {𝑅}) ∘𝑓 ·
𝐹)‘𝐴)) |
155 | 154 | eqeq1d 2612 |
. . . 4
⊢ (𝑓 = ((ℂ × {𝑅}) ∘𝑓
· 𝐹) → ((𝑓‘𝐴) = 0 ↔ (((ℂ × {𝑅}) ∘𝑓
· 𝐹)‘𝐴) = 0)) |
156 | 155 | rspcev 3282 |
. . 3
⊢
((((ℂ × {𝑅}) ∘𝑓 ·
𝐹) ∈
((Poly‘ℤ) ∖ {0𝑝}) ∧ (((ℂ ×
{𝑅})
∘𝑓 · 𝐹)‘𝐴) = 0) → ∃𝑓 ∈ ((Poly‘ℤ) ∖
{0𝑝})(𝑓‘𝐴) = 0) |
157 | 140, 153,
156 | syl2anc 691 |
. 2
⊢ (𝜑 → ∃𝑓 ∈ ((Poly‘ℤ) ∖
{0𝑝})(𝑓‘𝐴) = 0) |
158 | | elaa 23875 |
. 2
⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧
∃𝑓 ∈
((Poly‘ℤ) ∖ {0𝑝})(𝑓‘𝐴) = 0)) |
159 | 1, 157, 158 | sylanbrc 695 |
1
⊢ (𝜑 → 𝐴 ∈ 𝔸) |