| Step | Hyp | Ref
| Expression |
| 1 | | elqaa.1 |
. 2
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 2 | | cnex 11236 |
. . . . . . . 8
⊢ ℂ
∈ V |
| 3 | 2 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℂ ∈
V) |
| 4 | | elqaa.6 |
. . . . . . . . 9
⊢ 𝑅 = (seq0( · , 𝑁)‘(deg‘𝐹)) |
| 5 | 4 | fvexi 6920 |
. . . . . . . 8
⊢ 𝑅 ∈ V |
| 6 | 5 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑅 ∈ V) |
| 7 | | fvexd 6921 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝐹‘𝑧) ∈ V) |
| 8 | | fconstmpt 5747 |
. . . . . . . 8
⊢ (ℂ
× {𝑅}) = (𝑧 ∈ ℂ ↦ 𝑅) |
| 9 | 8 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (ℂ × {𝑅}) = (𝑧 ∈ ℂ ↦ 𝑅)) |
| 10 | | elqaa.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ((Poly‘ℚ) ∖
{0𝑝})) |
| 11 | 10 | eldifad 3963 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℚ)) |
| 12 | | plyf 26237 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘ℚ)
→ 𝐹:ℂ⟶ℂ) |
| 13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
| 14 | 13 | feqmptd 6977 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ (𝐹‘𝑧))) |
| 15 | 3, 6, 7, 9, 14 | offval2 7717 |
. . . . . 6
⊢ (𝜑 → ((ℂ × {𝑅}) ∘f ·
𝐹) = (𝑧 ∈ ℂ ↦ (𝑅 · (𝐹‘𝑧)))) |
| 16 | | fzfid 14014 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...(deg‘𝐹)) ∈ Fin) |
| 17 | | nn0uz 12920 |
. . . . . . . . . . . . . 14
⊢
ℕ0 = (ℤ≥‘0) |
| 18 | | 0zd 12625 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ∈
ℤ) |
| 19 | | ssrab2 4080 |
. . . . . . . . . . . . . . 15
⊢ {𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ} ⊆
ℕ |
| 20 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑚 → (𝐵‘𝑘) = (𝐵‘𝑚)) |
| 21 | 20 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑚 → ((𝐵‘𝑘) · 𝑛) = ((𝐵‘𝑚) · 𝑛)) |
| 22 | 21 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑚 → (((𝐵‘𝑘) · 𝑛) ∈ ℤ ↔ ((𝐵‘𝑚) · 𝑛) ∈ ℤ)) |
| 23 | 22 | rabbidv 3444 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑚 → {𝑛 ∈ ℕ ∣ ((𝐵‘𝑘) · 𝑛) ∈ ℤ} = {𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}) |
| 24 | 23 | infeq1d 9517 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑚 → inf({𝑛 ∈ ℕ ∣ ((𝐵‘𝑘) · 𝑛) ∈ ℤ}, ℝ, < ) =
inf({𝑛 ∈ ℕ
∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}, ℝ, <
)) |
| 25 | | elqaa.5 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑁 = (𝑘 ∈ ℕ0 ↦
inf({𝑛 ∈ ℕ
∣ ((𝐵‘𝑘) · 𝑛) ∈ ℤ}, ℝ, <
)) |
| 26 | | ltso 11341 |
. . . . . . . . . . . . . . . . . . 19
⊢ < Or
ℝ |
| 27 | 26 | infex 9533 |
. . . . . . . . . . . . . . . . . 18
⊢
inf({𝑛 ∈
ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}, ℝ, < ) ∈
V |
| 28 | 24, 25, 27 | fvmpt 7016 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕ0
→ (𝑁‘𝑚) = inf({𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}, ℝ, <
)) |
| 29 | 28 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁‘𝑚) = inf({𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}, ℝ, <
)) |
| 30 | | nnuz 12921 |
. . . . . . . . . . . . . . . . . 18
⊢ ℕ =
(ℤ≥‘1) |
| 31 | 19, 30 | sseqtri 4032 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ} ⊆
(ℤ≥‘1) |
| 32 | | 0z 12624 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℤ |
| 33 | | zq 12996 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ∈
ℤ → 0 ∈ ℚ) |
| 34 | 32, 33 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
ℚ |
| 35 | | elqaa.4 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐵 = (coeff‘𝐹) |
| 36 | 35 | coef2 26270 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 ∈ (Poly‘ℚ)
∧ 0 ∈ ℚ) → 𝐵:ℕ0⟶ℚ) |
| 37 | 11, 34, 36 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐵:ℕ0⟶ℚ) |
| 38 | 37 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝐵‘𝑚) ∈ ℚ) |
| 39 | | qmulz 12993 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵‘𝑚) ∈ ℚ → ∃𝑛 ∈ ℕ ((𝐵‘𝑚) · 𝑛) ∈ ℤ) |
| 40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
∃𝑛 ∈ ℕ
((𝐵‘𝑚) · 𝑛) ∈ ℤ) |
| 41 | | rabn0 4389 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ} ≠ ∅ ↔
∃𝑛 ∈ ℕ
((𝐵‘𝑚) · 𝑛) ∈ ℤ) |
| 42 | 40, 41 | sylibr 234 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → {𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ} ≠
∅) |
| 43 | | infssuzcl 12974 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ} ⊆
(ℤ≥‘1) ∧ {𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ} ≠ ∅) →
inf({𝑛 ∈ ℕ
∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}, ℝ, < ) ∈
{𝑛 ∈ ℕ ∣
((𝐵‘𝑚) · 𝑛) ∈ ℤ}) |
| 44 | 31, 42, 43 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
inf({𝑛 ∈ ℕ
∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}, ℝ, < ) ∈
{𝑛 ∈ ℕ ∣
((𝐵‘𝑚) · 𝑛) ∈ ℤ}) |
| 45 | 29, 44 | eqeltrd 2841 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁‘𝑚) ∈ {𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}) |
| 46 | 19, 45 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁‘𝑚) ∈ ℕ) |
| 47 | | nnmulcl 12290 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑚 · 𝑘) ∈ ℕ) |
| 48 | 47 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝑚 · 𝑘) ∈ ℕ) |
| 49 | 17, 18, 46, 48 | seqf 14064 |
. . . . . . . . . . . . 13
⊢ (𝜑 → seq0( · , 𝑁):ℕ0⟶ℕ) |
| 50 | | dgrcl 26272 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (Poly‘ℚ)
→ (deg‘𝐹) ∈
ℕ0) |
| 51 | 11, 50 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (deg‘𝐹) ∈
ℕ0) |
| 52 | 49, 51 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ (𝜑 → (seq0( · , 𝑁)‘(deg‘𝐹)) ∈
ℕ) |
| 53 | 4, 52 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ ℕ) |
| 54 | 53 | nncnd 12282 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ ℂ) |
| 55 | 54 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑅 ∈ ℂ) |
| 56 | | elfznn0 13660 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (0...(deg‘𝐹)) → 𝑚 ∈ ℕ0) |
| 57 | 35 | coef3 26271 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (Poly‘ℚ)
→ 𝐵:ℕ0⟶ℂ) |
| 58 | 11, 57 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵:ℕ0⟶ℂ) |
| 59 | 58 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝐵:ℕ0⟶ℂ) |
| 60 | 59 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑚 ∈ ℕ0) → (𝐵‘𝑚) ∈ ℂ) |
| 61 | | expcl 14120 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℂ ∧ 𝑚 ∈ ℕ0)
→ (𝑧↑𝑚) ∈
ℂ) |
| 62 | 61 | adantll 714 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑚 ∈ ℕ0) → (𝑧↑𝑚) ∈ ℂ) |
| 63 | 60, 62 | mulcld 11281 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑚 ∈ ℕ0) → ((𝐵‘𝑚) · (𝑧↑𝑚)) ∈ ℂ) |
| 64 | 56, 63 | sylan2 593 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑚 ∈ (0...(deg‘𝐹))) → ((𝐵‘𝑚) · (𝑧↑𝑚)) ∈ ℂ) |
| 65 | 16, 55, 64 | fsummulc2 15820 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑅 · Σ𝑚 ∈ (0...(deg‘𝐹))((𝐵‘𝑚) · (𝑧↑𝑚))) = Σ𝑚 ∈ (0...(deg‘𝐹))(𝑅 · ((𝐵‘𝑚) · (𝑧↑𝑚)))) |
| 66 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(deg‘𝐹) =
(deg‘𝐹) |
| 67 | 35, 66 | coeid2 26278 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘ℚ)
∧ 𝑧 ∈ ℂ)
→ (𝐹‘𝑧) = Σ𝑚 ∈ (0...(deg‘𝐹))((𝐵‘𝑚) · (𝑧↑𝑚))) |
| 68 | 11, 67 | sylan 580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝐹‘𝑧) = Σ𝑚 ∈ (0...(deg‘𝐹))((𝐵‘𝑚) · (𝑧↑𝑚))) |
| 69 | 68 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑅 · (𝐹‘𝑧)) = (𝑅 · Σ𝑚 ∈ (0...(deg‘𝐹))((𝐵‘𝑚) · (𝑧↑𝑚)))) |
| 70 | 55 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑚 ∈ ℕ0) → 𝑅 ∈
ℂ) |
| 71 | 70, 60, 62 | mulassd 11284 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑚 ∈ ℕ0) → ((𝑅 · (𝐵‘𝑚)) · (𝑧↑𝑚)) = (𝑅 · ((𝐵‘𝑚) · (𝑧↑𝑚)))) |
| 72 | 56, 71 | sylan2 593 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑚 ∈ (0...(deg‘𝐹))) → ((𝑅 · (𝐵‘𝑚)) · (𝑧↑𝑚)) = (𝑅 · ((𝐵‘𝑚) · (𝑧↑𝑚)))) |
| 73 | 72 | sumeq2dv 15738 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑚 ∈ (0...(deg‘𝐹))((𝑅 · (𝐵‘𝑚)) · (𝑧↑𝑚)) = Σ𝑚 ∈ (0...(deg‘𝐹))(𝑅 · ((𝐵‘𝑚) · (𝑧↑𝑚)))) |
| 74 | 65, 69, 73 | 3eqtr4d 2787 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑅 · (𝐹‘𝑧)) = Σ𝑚 ∈ (0...(deg‘𝐹))((𝑅 · (𝐵‘𝑚)) · (𝑧↑𝑚))) |
| 75 | 74 | mpteq2dva 5242 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ (𝑅 · (𝐹‘𝑧))) = (𝑧 ∈ ℂ ↦ Σ𝑚 ∈ (0...(deg‘𝐹))((𝑅 · (𝐵‘𝑚)) · (𝑧↑𝑚)))) |
| 76 | 15, 75 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → ((ℂ × {𝑅}) ∘f ·
𝐹) = (𝑧 ∈ ℂ ↦ Σ𝑚 ∈ (0...(deg‘𝐹))((𝑅 · (𝐵‘𝑚)) · (𝑧↑𝑚)))) |
| 77 | | zsscn 12621 |
. . . . . . 7
⊢ ℤ
⊆ ℂ |
| 78 | 77 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℤ ⊆
ℂ) |
| 79 | 54 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑅 ∈
ℂ) |
| 80 | 46 | nncnd 12282 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁‘𝑚) ∈ ℂ) |
| 81 | 46 | nnne0d 12316 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁‘𝑚) ≠ 0) |
| 82 | 79, 80, 81 | divcan2d 12045 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑁‘𝑚) · (𝑅 / (𝑁‘𝑚))) = 𝑅) |
| 83 | 82 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝐵‘𝑚) · ((𝑁‘𝑚) · (𝑅 / (𝑁‘𝑚)))) = ((𝐵‘𝑚) · 𝑅)) |
| 84 | 58 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝐵‘𝑚) ∈ ℂ) |
| 85 | 79, 80, 81 | divcld 12043 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑅 / (𝑁‘𝑚)) ∈ ℂ) |
| 86 | 84, 80, 85 | mulassd 11284 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (((𝐵‘𝑚) · (𝑁‘𝑚)) · (𝑅 / (𝑁‘𝑚))) = ((𝐵‘𝑚) · ((𝑁‘𝑚) · (𝑅 / (𝑁‘𝑚))))) |
| 87 | 79, 84 | mulcomd 11282 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑅 · (𝐵‘𝑚)) = ((𝐵‘𝑚) · 𝑅)) |
| 88 | 83, 86, 87 | 3eqtr4rd 2788 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑅 · (𝐵‘𝑚)) = (((𝐵‘𝑚) · (𝑁‘𝑚)) · (𝑅 / (𝑁‘𝑚)))) |
| 89 | 56, 88 | sylan2 593 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → (𝑅 · (𝐵‘𝑚)) = (((𝐵‘𝑚) · (𝑁‘𝑚)) · (𝑅 / (𝑁‘𝑚)))) |
| 90 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑁‘𝑚) → ((𝐵‘𝑚) · 𝑛) = ((𝐵‘𝑚) · (𝑁‘𝑚))) |
| 91 | 90 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑁‘𝑚) → (((𝐵‘𝑚) · 𝑛) ∈ ℤ ↔ ((𝐵‘𝑚) · (𝑁‘𝑚)) ∈ ℤ)) |
| 92 | 91 | elrab 3692 |
. . . . . . . . . . 11
⊢ ((𝑁‘𝑚) ∈ {𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ} ↔ ((𝑁‘𝑚) ∈ ℕ ∧ ((𝐵‘𝑚) · (𝑁‘𝑚)) ∈ ℤ)) |
| 93 | 92 | simprbi 496 |
. . . . . . . . . 10
⊢ ((𝑁‘𝑚) ∈ {𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ} → ((𝐵‘𝑚) · (𝑁‘𝑚)) ∈ ℤ) |
| 94 | 45, 93 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝐵‘𝑚) · (𝑁‘𝑚)) ∈ ℤ) |
| 95 | 56, 94 | sylan2 593 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → ((𝐵‘𝑚) · (𝑁‘𝑚)) ∈ ℤ) |
| 96 | | elqaa.3 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝐴) = 0) |
| 97 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 · 𝑦) mod (𝑁‘𝑚))) = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 · 𝑦) mod (𝑁‘𝑚))) |
| 98 | 1, 10, 96, 35, 25, 4, 97 | elqaalem2 26362 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → (𝑅 mod (𝑁‘𝑚)) = 0) |
| 99 | 53 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → 𝑅 ∈ ℕ) |
| 100 | 56, 46 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → (𝑁‘𝑚) ∈ ℕ) |
| 101 | | nnre 12273 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℕ → 𝑅 ∈
ℝ) |
| 102 | | nnrp 13046 |
. . . . . . . . . . 11
⊢ ((𝑁‘𝑚) ∈ ℕ → (𝑁‘𝑚) ∈
ℝ+) |
| 103 | | mod0 13916 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ ∧ (𝑁‘𝑚) ∈ ℝ+) → ((𝑅 mod (𝑁‘𝑚)) = 0 ↔ (𝑅 / (𝑁‘𝑚)) ∈ ℤ)) |
| 104 | 101, 102,
103 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℕ ∧ (𝑁‘𝑚) ∈ ℕ) → ((𝑅 mod (𝑁‘𝑚)) = 0 ↔ (𝑅 / (𝑁‘𝑚)) ∈ ℤ)) |
| 105 | 99, 100, 104 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → ((𝑅 mod (𝑁‘𝑚)) = 0 ↔ (𝑅 / (𝑁‘𝑚)) ∈ ℤ)) |
| 106 | 98, 105 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → (𝑅 / (𝑁‘𝑚)) ∈ ℤ) |
| 107 | 95, 106 | zmulcld 12728 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → (((𝐵‘𝑚) · (𝑁‘𝑚)) · (𝑅 / (𝑁‘𝑚))) ∈ ℤ) |
| 108 | 89, 107 | eqeltrd 2841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(deg‘𝐹))) → (𝑅 · (𝐵‘𝑚)) ∈ ℤ) |
| 109 | 78, 51, 108 | elplyd 26241 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑚 ∈ (0...(deg‘𝐹))((𝑅 · (𝐵‘𝑚)) · (𝑧↑𝑚))) ∈
(Poly‘ℤ)) |
| 110 | 76, 109 | eqeltrd 2841 |
. . . 4
⊢ (𝜑 → ((ℂ × {𝑅}) ∘f ·
𝐹) ∈
(Poly‘ℤ)) |
| 111 | | eldifsn 4786 |
. . . . . . 7
⊢ (𝐹 ∈ ((Poly‘ℚ)
∖ {0𝑝}) ↔ (𝐹 ∈ (Poly‘ℚ) ∧ 𝐹 ≠
0𝑝)) |
| 112 | 10, 111 | sylib 218 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∈ (Poly‘ℚ) ∧ 𝐹 ≠
0𝑝)) |
| 113 | 112 | simprd 495 |
. . . . 5
⊢ (𝜑 → 𝐹 ≠
0𝑝) |
| 114 | | oveq1 7438 |
. . . . . . 7
⊢
(((ℂ × {𝑅}) ∘f · 𝐹) = 0𝑝 →
(((ℂ × {𝑅})
∘f · 𝐹) ∘f / (ℂ ×
{𝑅})) =
(0𝑝 ∘f / (ℂ × {𝑅}))) |
| 115 | 13 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝐹‘𝑧) ∈ ℂ) |
| 116 | 53 | nnne0d 12316 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ≠ 0) |
| 117 | 116 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑅 ≠ 0) |
| 118 | 115, 55, 117 | divcan3d 12048 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝑅 · (𝐹‘𝑧)) / 𝑅) = (𝐹‘𝑧)) |
| 119 | 118 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ ((𝑅 · (𝐹‘𝑧)) / 𝑅)) = (𝑧 ∈ ℂ ↦ (𝐹‘𝑧))) |
| 120 | | ovexd 7466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑅 · (𝐹‘𝑧)) ∈ V) |
| 121 | 3, 120, 6, 15, 9 | offval2 7717 |
. . . . . . . . 9
⊢ (𝜑 → (((ℂ × {𝑅}) ∘f ·
𝐹) ∘f /
(ℂ × {𝑅})) =
(𝑧 ∈ ℂ ↦
((𝑅 · (𝐹‘𝑧)) / 𝑅))) |
| 122 | 119, 121,
14 | 3eqtr4d 2787 |
. . . . . . . 8
⊢ (𝜑 → (((ℂ × {𝑅}) ∘f ·
𝐹) ∘f /
(ℂ × {𝑅})) =
𝐹) |
| 123 | 54, 116 | div0d 12042 |
. . . . . . . . . 10
⊢ (𝜑 → (0 / 𝑅) = 0) |
| 124 | 123 | mpteq2dv 5244 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ (0 / 𝑅)) = (𝑧 ∈ ℂ ↦ 0)) |
| 125 | | 0cnd 11254 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 0 ∈
ℂ) |
| 126 | | df-0p 25705 |
. . . . . . . . . . . 12
⊢
0𝑝 = (ℂ × {0}) |
| 127 | | fconstmpt 5747 |
. . . . . . . . . . . 12
⊢ (ℂ
× {0}) = (𝑧 ∈
ℂ ↦ 0) |
| 128 | 126, 127 | eqtri 2765 |
. . . . . . . . . . 11
⊢
0𝑝 = (𝑧 ∈ ℂ ↦ 0) |
| 129 | 128 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0𝑝 =
(𝑧 ∈ ℂ ↦
0)) |
| 130 | 3, 125, 6, 129, 9 | offval2 7717 |
. . . . . . . . 9
⊢ (𝜑 → (0𝑝
∘f / (ℂ × {𝑅})) = (𝑧 ∈ ℂ ↦ (0 / 𝑅))) |
| 131 | 124, 130,
129 | 3eqtr4d 2787 |
. . . . . . . 8
⊢ (𝜑 → (0𝑝
∘f / (ℂ × {𝑅})) =
0𝑝) |
| 132 | 122, 131 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝜑 → ((((ℂ × {𝑅}) ∘f ·
𝐹) ∘f /
(ℂ × {𝑅})) =
(0𝑝 ∘f / (ℂ × {𝑅})) ↔ 𝐹 = 0𝑝)) |
| 133 | 114, 132 | imbitrid 244 |
. . . . . 6
⊢ (𝜑 → (((ℂ × {𝑅}) ∘f ·
𝐹) = 0𝑝
→ 𝐹 =
0𝑝)) |
| 134 | 133 | necon3d 2961 |
. . . . 5
⊢ (𝜑 → (𝐹 ≠ 0𝑝 → ((ℂ
× {𝑅})
∘f · 𝐹) ≠
0𝑝)) |
| 135 | 113, 134 | mpd 15 |
. . . 4
⊢ (𝜑 → ((ℂ × {𝑅}) ∘f ·
𝐹) ≠
0𝑝) |
| 136 | | eldifsn 4786 |
. . . 4
⊢
(((ℂ × {𝑅}) ∘f · 𝐹) ∈ ((Poly‘ℤ)
∖ {0𝑝}) ↔ (((ℂ × {𝑅}) ∘f · 𝐹) ∈ (Poly‘ℤ)
∧ ((ℂ × {𝑅}) ∘f · 𝐹) ≠
0𝑝)) |
| 137 | 110, 135,
136 | sylanbrc 583 |
. . 3
⊢ (𝜑 → ((ℂ × {𝑅}) ∘f ·
𝐹) ∈
((Poly‘ℤ) ∖ {0𝑝})) |
| 138 | 5 | fconst 6794 |
. . . . . . 7
⊢ (ℂ
× {𝑅}):ℂ⟶{𝑅} |
| 139 | | ffn 6736 |
. . . . . . 7
⊢ ((ℂ
× {𝑅}):ℂ⟶{𝑅} → (ℂ × {𝑅}) Fn ℂ) |
| 140 | 138, 139 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → (ℂ × {𝑅}) Fn ℂ) |
| 141 | 13 | ffnd 6737 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn ℂ) |
| 142 | | inidm 4227 |
. . . . . 6
⊢ (ℂ
∩ ℂ) = ℂ |
| 143 | 5 | fvconst2 7224 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ((ℂ
× {𝑅})‘𝐴) = 𝑅) |
| 144 | 143 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → ((ℂ ×
{𝑅})‘𝐴) = 𝑅) |
| 145 | 96 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (𝐹‘𝐴) = 0) |
| 146 | 140, 141,
3, 3, 142, 144, 145 | ofval 7708 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (((ℂ ×
{𝑅}) ∘f
· 𝐹)‘𝐴) = (𝑅 · 0)) |
| 147 | 1, 146 | mpdan 687 |
. . . 4
⊢ (𝜑 → (((ℂ × {𝑅}) ∘f ·
𝐹)‘𝐴) = (𝑅 · 0)) |
| 148 | 54 | mul01d 11460 |
. . . 4
⊢ (𝜑 → (𝑅 · 0) = 0) |
| 149 | 147, 148 | eqtrd 2777 |
. . 3
⊢ (𝜑 → (((ℂ × {𝑅}) ∘f ·
𝐹)‘𝐴) = 0) |
| 150 | | fveq1 6905 |
. . . . 5
⊢ (𝑓 = ((ℂ × {𝑅}) ∘f ·
𝐹) → (𝑓‘𝐴) = (((ℂ × {𝑅}) ∘f · 𝐹)‘𝐴)) |
| 151 | 150 | eqeq1d 2739 |
. . . 4
⊢ (𝑓 = ((ℂ × {𝑅}) ∘f ·
𝐹) → ((𝑓‘𝐴) = 0 ↔ (((ℂ × {𝑅}) ∘f ·
𝐹)‘𝐴) = 0)) |
| 152 | 151 | rspcev 3622 |
. . 3
⊢
((((ℂ × {𝑅}) ∘f · 𝐹) ∈ ((Poly‘ℤ)
∖ {0𝑝}) ∧ (((ℂ × {𝑅}) ∘f · 𝐹)‘𝐴) = 0) → ∃𝑓 ∈ ((Poly‘ℤ) ∖
{0𝑝})(𝑓‘𝐴) = 0) |
| 153 | 137, 149,
152 | syl2anc 584 |
. 2
⊢ (𝜑 → ∃𝑓 ∈ ((Poly‘ℤ) ∖
{0𝑝})(𝑓‘𝐴) = 0) |
| 154 | | elaa 26358 |
. 2
⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧
∃𝑓 ∈
((Poly‘ℤ) ∖ {0𝑝})(𝑓‘𝐴) = 0)) |
| 155 | 1, 153, 154 | sylanbrc 583 |
1
⊢ (𝜑 → 𝐴 ∈ 𝔸) |