Step | Hyp | Ref
| Expression |
1 | | elfznn0 12302 |
. . 3
⊢ (𝐾 ∈ (0...(deg‘𝐹)) → 𝐾 ∈
ℕ0) |
2 | | elqaa.6 |
. . . . 5
⊢ 𝑅 = (seq0( · , 𝑁)‘(deg‘𝐹)) |
3 | 2 | fveq2i 6106 |
. . . 4
⊢ ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘𝑅) = ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘(seq0( · , 𝑁)‘(deg‘𝐹))) |
4 | | nnmulcl 10920 |
. . . . . 6
⊢ ((𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑖 · 𝑗) ∈ ℕ) |
5 | 4 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 · 𝑗) ∈ ℕ) |
6 | | elfznn0 12302 |
. . . . . 6
⊢ (𝑖 ∈ (0...(deg‘𝐹)) → 𝑖 ∈ ℕ0) |
7 | | elqaa.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) |
8 | | elqaa.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ((Poly‘ℚ) ∖
{0𝑝})) |
9 | | elqaa.3 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝐴) = 0) |
10 | | elqaa.4 |
. . . . . . . . 9
⊢ 𝐵 = (coeff‘𝐹) |
11 | | elqaa.5 |
. . . . . . . . 9
⊢ 𝑁 = (𝑘 ∈ ℕ0 ↦
inf({𝑛 ∈ ℕ
∣ ((𝐵‘𝑘) · 𝑛) ∈ ℤ}, ℝ, <
)) |
12 | 7, 8, 9, 10, 11, 2 | elqaalem1 23878 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑁‘𝑖) ∈ ℕ ∧ ((𝐵‘𝑖) · (𝑁‘𝑖)) ∈ ℤ)) |
13 | 12 | simpld 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑁‘𝑖) ∈ ℕ) |
14 | 13 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0)
→ (𝑁‘𝑖) ∈
ℕ) |
15 | 6, 14 | sylan2 490 |
. . . . 5
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → (𝑁‘𝑖) ∈ ℕ) |
16 | | eldifi 3694 |
. . . . . . . 8
⊢ (𝐹 ∈ ((Poly‘ℚ)
∖ {0𝑝}) → 𝐹 ∈
(Poly‘ℚ)) |
17 | | dgrcl 23793 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘ℚ)
→ (deg‘𝐹) ∈
ℕ0) |
18 | 8, 16, 17 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (deg‘𝐹) ∈
ℕ0) |
19 | | nn0uz 11598 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
20 | 18, 19 | syl6eleq 2698 |
. . . . . 6
⊢ (𝜑 → (deg‘𝐹) ∈
(ℤ≥‘0)) |
21 | 20 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ ℕ0) →
(deg‘𝐹) ∈
(ℤ≥‘0)) |
22 | | nnz 11276 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ℕ → 𝑖 ∈
ℤ) |
23 | 22 | ad2antrl 760 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈
ℤ) |
24 | 7, 8, 9, 10, 11, 2 | elqaalem1 23878 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐾 ∈ ℕ0) → ((𝑁‘𝐾) ∈ ℕ ∧ ((𝐵‘𝐾) · (𝑁‘𝐾)) ∈ ℤ)) |
25 | 24 | simpld 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ∈ ℕ0) → (𝑁‘𝐾) ∈ ℕ) |
26 | 25 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑁‘𝐾) ∈ ℕ) |
27 | 23, 26 | zmodcld 12553 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 mod (𝑁‘𝐾)) ∈
ℕ0) |
28 | 27 | nn0zd 11356 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 mod (𝑁‘𝐾)) ∈ ℤ) |
29 | | nnz 11276 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℤ) |
30 | 29 | ad2antll 761 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈
ℤ) |
31 | 30, 26 | zmodcld 12553 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑗 mod (𝑁‘𝐾)) ∈
ℕ0) |
32 | 31 | nn0zd 11356 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑗 mod (𝑁‘𝐾)) ∈ ℤ) |
33 | 26 | nnrpd 11746 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑁‘𝐾) ∈
ℝ+) |
34 | | nnre 10904 |
. . . . . . . . 9
⊢ (𝑖 ∈ ℕ → 𝑖 ∈
ℝ) |
35 | 34 | ad2antrl 760 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈
ℝ) |
36 | | modabs2 12566 |
. . . . . . . 8
⊢ ((𝑖 ∈ ℝ ∧ (𝑁‘𝐾) ∈ ℝ+) → ((𝑖 mod (𝑁‘𝐾)) mod (𝑁‘𝐾)) = (𝑖 mod (𝑁‘𝐾))) |
37 | 35, 33, 36 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑖 mod (𝑁‘𝐾)) mod (𝑁‘𝐾)) = (𝑖 mod (𝑁‘𝐾))) |
38 | | nnre 10904 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ) |
39 | 38 | ad2antll 761 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈
ℝ) |
40 | | modabs2 12566 |
. . . . . . . 8
⊢ ((𝑗 ∈ ℝ ∧ (𝑁‘𝐾) ∈ ℝ+) → ((𝑗 mod (𝑁‘𝐾)) mod (𝑁‘𝐾)) = (𝑗 mod (𝑁‘𝐾))) |
41 | 39, 33, 40 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑗 mod (𝑁‘𝐾)) mod (𝑁‘𝐾)) = (𝑗 mod (𝑁‘𝐾))) |
42 | 28, 23, 32, 30, 33, 37, 41 | modmul12d 12586 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) →
(((𝑖 mod (𝑁‘𝐾)) · (𝑗 mod (𝑁‘𝐾))) mod (𝑁‘𝐾)) = ((𝑖 · 𝑗) mod (𝑁‘𝐾))) |
43 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → (𝑘 mod (𝑁‘𝐾)) = (𝑖 mod (𝑁‘𝐾))) |
44 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾))) = (𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾))) |
45 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝑖 mod (𝑁‘𝐾)) ∈ V |
46 | 43, 44, 45 | fvmpt 6191 |
. . . . . . . . 9
⊢ (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘𝑖) = (𝑖 mod (𝑁‘𝐾))) |
47 | 46 | ad2antrl 760 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘𝑖) = (𝑖 mod (𝑁‘𝐾))) |
48 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝑘 mod (𝑁‘𝐾)) = (𝑗 mod (𝑁‘𝐾))) |
49 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝑗 mod (𝑁‘𝐾)) ∈ V |
50 | 48, 44, 49 | fvmpt 6191 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘𝑗) = (𝑗 mod (𝑁‘𝐾))) |
51 | 50 | ad2antll 761 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘𝑗) = (𝑗 mod (𝑁‘𝐾))) |
52 | 47, 51 | oveq12d 6567 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) →
(((𝑘 ∈ ℕ ↦
(𝑘 mod (𝑁‘𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘𝑗)) = ((𝑖 mod (𝑁‘𝐾))𝑃(𝑗 mod (𝑁‘𝐾)))) |
53 | | oveq12 6558 |
. . . . . . . . . 10
⊢ ((𝑥 = (𝑖 mod (𝑁‘𝐾)) ∧ 𝑦 = (𝑗 mod (𝑁‘𝐾))) → (𝑥 · 𝑦) = ((𝑖 mod (𝑁‘𝐾)) · (𝑗 mod (𝑁‘𝐾)))) |
54 | 53 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝑥 = (𝑖 mod (𝑁‘𝐾)) ∧ 𝑦 = (𝑗 mod (𝑁‘𝐾))) → ((𝑥 · 𝑦) mod (𝑁‘𝐾)) = (((𝑖 mod (𝑁‘𝐾)) · (𝑗 mod (𝑁‘𝐾))) mod (𝑁‘𝐾))) |
55 | | elqaa.7 |
. . . . . . . . 9
⊢ 𝑃 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 · 𝑦) mod (𝑁‘𝐾))) |
56 | | ovex 6577 |
. . . . . . . . 9
⊢ (((𝑖 mod (𝑁‘𝐾)) · (𝑗 mod (𝑁‘𝐾))) mod (𝑁‘𝐾)) ∈ V |
57 | 54, 55, 56 | ovmpt2a 6689 |
. . . . . . . 8
⊢ (((𝑖 mod (𝑁‘𝐾)) ∈ V ∧ (𝑗 mod (𝑁‘𝐾)) ∈ V) → ((𝑖 mod (𝑁‘𝐾))𝑃(𝑗 mod (𝑁‘𝐾))) = (((𝑖 mod (𝑁‘𝐾)) · (𝑗 mod (𝑁‘𝐾))) mod (𝑁‘𝐾))) |
58 | 45, 49, 57 | mp2an 704 |
. . . . . . 7
⊢ ((𝑖 mod (𝑁‘𝐾))𝑃(𝑗 mod (𝑁‘𝐾))) = (((𝑖 mod (𝑁‘𝐾)) · (𝑗 mod (𝑁‘𝐾))) mod (𝑁‘𝐾)) |
59 | 52, 58 | syl6eq 2660 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) →
(((𝑘 ∈ ℕ ↦
(𝑘 mod (𝑁‘𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘𝑗)) = (((𝑖 mod (𝑁‘𝐾)) · (𝑗 mod (𝑁‘𝐾))) mod (𝑁‘𝐾))) |
60 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑘 = (𝑖 · 𝑗) → (𝑘 mod (𝑁‘𝐾)) = ((𝑖 · 𝑗) mod (𝑁‘𝐾))) |
61 | | ovex 6577 |
. . . . . . . 8
⊢ ((𝑖 · 𝑗) mod (𝑁‘𝐾)) ∈ V |
62 | 60, 44, 61 | fvmpt 6191 |
. . . . . . 7
⊢ ((𝑖 · 𝑗) ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘(𝑖 · 𝑗)) = ((𝑖 · 𝑗) mod (𝑁‘𝐾))) |
63 | 5, 62 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘(𝑖 · 𝑗)) = ((𝑖 · 𝑗) mod (𝑁‘𝐾))) |
64 | 42, 59, 63 | 3eqtr4rd 2655 |
. . . . 5
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘(𝑖 · 𝑗)) = (((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘𝑗))) |
65 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑘 = (𝑁‘𝑖) → (𝑘 mod (𝑁‘𝐾)) = ((𝑁‘𝑖) mod (𝑁‘𝐾))) |
66 | | ovex 6577 |
. . . . . . . . 9
⊢ ((𝑁‘𝑖) mod (𝑁‘𝐾)) ∈ V |
67 | 65, 44, 66 | fvmpt 6191 |
. . . . . . . 8
⊢ ((𝑁‘𝑖) ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘(𝑁‘𝑖)) = ((𝑁‘𝑖) mod (𝑁‘𝐾))) |
68 | 14, 67 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0)
→ ((𝑘 ∈ ℕ
↦ (𝑘 mod (𝑁‘𝐾)))‘(𝑁‘𝑖)) = ((𝑁‘𝑖) mod (𝑁‘𝐾))) |
69 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → (𝑁‘𝑘) = (𝑁‘𝑖)) |
70 | 69 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑘 = 𝑖 → ((𝑁‘𝑘) mod (𝑁‘𝐾)) = ((𝑁‘𝑖) mod (𝑁‘𝐾))) |
71 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
↦ ((𝑁‘𝑘) mod (𝑁‘𝐾))) = (𝑘 ∈ ℕ0 ↦ ((𝑁‘𝑘) mod (𝑁‘𝐾))) |
72 | 70, 71, 66 | fvmpt 6191 |
. . . . . . . 8
⊢ (𝑖 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((𝑁‘𝑘) mod (𝑁‘𝐾)))‘𝑖) = ((𝑁‘𝑖) mod (𝑁‘𝐾))) |
73 | 72 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0)
→ ((𝑘 ∈
ℕ0 ↦ ((𝑁‘𝑘) mod (𝑁‘𝐾)))‘𝑖) = ((𝑁‘𝑖) mod (𝑁‘𝐾))) |
74 | 68, 73 | eqtr4d 2647 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0)
→ ((𝑘 ∈ ℕ
↦ (𝑘 mod (𝑁‘𝐾)))‘(𝑁‘𝑖)) = ((𝑘 ∈ ℕ0 ↦ ((𝑁‘𝑘) mod (𝑁‘𝐾)))‘𝑖)) |
75 | 6, 74 | sylan2 490 |
. . . . 5
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘(𝑁‘𝑖)) = ((𝑘 ∈ ℕ0 ↦ ((𝑁‘𝑘) mod (𝑁‘𝐾)))‘𝑖)) |
76 | 5, 15, 21, 64, 75 | seqhomo 12710 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘(seq0( · , 𝑁)‘(deg‘𝐹))) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁‘𝑘) mod (𝑁‘𝐾))))‘(deg‘𝐹))) |
77 | 3, 76 | syl5eq 2656 |
. . 3
⊢ ((𝜑 ∧ 𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘𝑅) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁‘𝑘) mod (𝑁‘𝐾))))‘(deg‘𝐹))) |
78 | 1, 77 | sylan2 490 |
. 2
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘𝑅) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁‘𝑘) mod (𝑁‘𝐾))))‘(deg‘𝐹))) |
79 | | 0zd 11266 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℤ) |
80 | 4 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 · 𝑗) ∈ ℕ) |
81 | 19, 79, 13, 80 | seqf 12684 |
. . . . . . 7
⊢ (𝜑 → seq0( · , 𝑁):ℕ0⟶ℕ) |
82 | 81, 18 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 → (seq0( · , 𝑁)‘(deg‘𝐹)) ∈
ℕ) |
83 | 2, 82 | syl5eqel 2692 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ ℕ) |
84 | 83 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ ℕ0) → 𝑅 ∈
ℕ) |
85 | | oveq1 6556 |
. . . . 5
⊢ (𝑘 = 𝑅 → (𝑘 mod (𝑁‘𝐾)) = (𝑅 mod (𝑁‘𝐾))) |
86 | | ovex 6577 |
. . . . 5
⊢ (𝑅 mod (𝑁‘𝐾)) ∈ V |
87 | 85, 44, 86 | fvmpt 6191 |
. . . 4
⊢ (𝑅 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘𝑅) = (𝑅 mod (𝑁‘𝐾))) |
88 | 84, 87 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘𝑅) = (𝑅 mod (𝑁‘𝐾))) |
89 | 1, 88 | sylan2 490 |
. 2
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁‘𝐾)))‘𝑅) = (𝑅 mod (𝑁‘𝐾))) |
90 | | vex 3176 |
. . . . 5
⊢ 𝑖 ∈ V |
91 | | vex 3176 |
. . . . 5
⊢ 𝑗 ∈ V |
92 | | oveq12 6558 |
. . . . . . 7
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑥 · 𝑦) = (𝑖 · 𝑗)) |
93 | 92 | oveq1d 6564 |
. . . . . 6
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → ((𝑥 · 𝑦) mod (𝑁‘𝐾)) = ((𝑖 · 𝑗) mod (𝑁‘𝐾))) |
94 | 93, 55, 61 | ovmpt2a 6689 |
. . . . 5
⊢ ((𝑖 ∈ V ∧ 𝑗 ∈ V) → (𝑖𝑃𝑗) = ((𝑖 · 𝑗) mod (𝑁‘𝐾))) |
95 | 90, 91, 94 | mp2an 704 |
. . . 4
⊢ (𝑖𝑃𝑗) = ((𝑖 · 𝑗) mod (𝑁‘𝐾)) |
96 | | nn0mulcl 11206 |
. . . . . 6
⊢ ((𝑖 ∈ ℕ0
∧ 𝑗 ∈
ℕ0) → (𝑖 · 𝑗) ∈
ℕ0) |
97 | 96 | nn0zd 11356 |
. . . . 5
⊢ ((𝑖 ∈ ℕ0
∧ 𝑗 ∈
ℕ0) → (𝑖 · 𝑗) ∈ ℤ) |
98 | 1, 25 | sylan2 490 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → (𝑁‘𝐾) ∈ ℕ) |
99 | | zmodcl 12552 |
. . . . 5
⊢ (((𝑖 · 𝑗) ∈ ℤ ∧ (𝑁‘𝐾) ∈ ℕ) → ((𝑖 · 𝑗) mod (𝑁‘𝐾)) ∈
ℕ0) |
100 | 97, 98, 99 | syl2anr 494 |
. . . 4
⊢ (((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) ∧ (𝑖 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0))
→ ((𝑖 · 𝑗) mod (𝑁‘𝐾)) ∈
ℕ0) |
101 | 95, 100 | syl5eqel 2692 |
. . 3
⊢ (((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) ∧ (𝑖 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0))
→ (𝑖𝑃𝑗) ∈
ℕ0) |
102 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑚 → (𝐵‘𝑘) = (𝐵‘𝑚)) |
103 | 102 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑚 → ((𝐵‘𝑘) · 𝑛) = ((𝐵‘𝑚) · 𝑛)) |
104 | 103 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑚 → (((𝐵‘𝑘) · 𝑛) ∈ ℤ ↔ ((𝐵‘𝑚) · 𝑛) ∈ ℤ)) |
105 | 104 | rabbidv 3164 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → {𝑛 ∈ ℕ ∣ ((𝐵‘𝑘) · 𝑛) ∈ ℤ} = {𝑛 ∈ ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}) |
106 | 105 | infeq1d 8266 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → inf({𝑛 ∈ ℕ ∣ ((𝐵‘𝑘) · 𝑛) ∈ ℤ}, ℝ, < ) =
inf({𝑛 ∈ ℕ
∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}, ℝ, <
)) |
107 | 106 | cbvmptv 4678 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
↦ inf({𝑛 ∈
ℕ ∣ ((𝐵‘𝑘) · 𝑛) ∈ ℤ}, ℝ, < )) = (𝑚 ∈ ℕ0
↦ inf({𝑛 ∈
ℕ ∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}, ℝ, <
)) |
108 | 11, 107 | eqtri 2632 |
. . . . . . . . . . 11
⊢ 𝑁 = (𝑚 ∈ ℕ0 ↦
inf({𝑛 ∈ ℕ
∣ ((𝐵‘𝑚) · 𝑛) ∈ ℤ}, ℝ, <
)) |
109 | 7, 8, 9, 10, 108, 2 | elqaalem1 23878 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑁‘𝑘) ∈ ℕ ∧ ((𝐵‘𝑘) · (𝑁‘𝑘)) ∈ ℤ)) |
110 | 109 | simpld 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑁‘𝑘) ∈ ℕ) |
111 | 110 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝑁‘𝑘) ∈
ℕ) |
112 | 111 | nnzd 11357 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝑁‘𝑘) ∈
ℤ) |
113 | 25 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝑁‘𝐾) ∈
ℕ) |
114 | 112, 113 | zmodcld 12553 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑁‘𝑘) mod (𝑁‘𝐾)) ∈
ℕ0) |
115 | 114, 71 | fmptd 6292 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑁‘𝑘) mod (𝑁‘𝐾))):ℕ0⟶ℕ0) |
116 | 1, 115 | sylan2 490 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → (𝑘 ∈ ℕ0 ↦ ((𝑁‘𝑘) mod (𝑁‘𝐾))):ℕ0⟶ℕ0) |
117 | | ffvelrn 6265 |
. . . 4
⊢ (((𝑘 ∈ ℕ0
↦ ((𝑁‘𝑘) mod (𝑁‘𝐾))):ℕ0⟶ℕ0
∧ 𝑖 ∈
ℕ0) → ((𝑘
∈ ℕ0 ↦ ((𝑁‘𝑘) mod (𝑁‘𝐾)))‘𝑖) ∈ ℕ0) |
118 | 116, 6, 117 | syl2an 493 |
. . 3
⊢ (((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁‘𝑘) mod (𝑁‘𝐾)))‘𝑖) ∈
ℕ0) |
119 | | c0ex 9913 |
. . . . 5
⊢ 0 ∈
V |
120 | | oveq12 6558 |
. . . . . . 7
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑖) → (𝑥 · 𝑦) = (0 · 𝑖)) |
121 | 120 | oveq1d 6564 |
. . . . . 6
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑖) → ((𝑥 · 𝑦) mod (𝑁‘𝐾)) = ((0 · 𝑖) mod (𝑁‘𝐾))) |
122 | | ovex 6577 |
. . . . . 6
⊢ ((0
· 𝑖) mod (𝑁‘𝐾)) ∈ V |
123 | 121, 55, 122 | ovmpt2a 6689 |
. . . . 5
⊢ ((0
∈ V ∧ 𝑖 ∈ V)
→ (0𝑃𝑖) = ((0 · 𝑖) mod (𝑁‘𝐾))) |
124 | 119, 90, 123 | mp2an 704 |
. . . 4
⊢ (0𝑃𝑖) = ((0 · 𝑖) mod (𝑁‘𝐾)) |
125 | | nn0cn 11179 |
. . . . . . 7
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℂ) |
126 | 125 | mul02d 10113 |
. . . . . 6
⊢ (𝑖 ∈ ℕ0
→ (0 · 𝑖) =
0) |
127 | 126 | oveq1d 6564 |
. . . . 5
⊢ (𝑖 ∈ ℕ0
→ ((0 · 𝑖) mod
(𝑁‘𝐾)) = (0 mod (𝑁‘𝐾))) |
128 | 98 | nnrpd 11746 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → (𝑁‘𝐾) ∈
ℝ+) |
129 | | 0mod 12563 |
. . . . . 6
⊢ ((𝑁‘𝐾) ∈ ℝ+ → (0 mod
(𝑁‘𝐾)) = 0) |
130 | 128, 129 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → (0 mod (𝑁‘𝐾)) = 0) |
131 | 127, 130 | sylan9eqr 2666 |
. . . 4
⊢ (((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → ((0
· 𝑖) mod (𝑁‘𝐾)) = 0) |
132 | 124, 131 | syl5eq 2656 |
. . 3
⊢ (((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → (0𝑃𝑖) = 0) |
133 | | oveq12 6558 |
. . . . . . 7
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 0) → (𝑥 · 𝑦) = (𝑖 · 0)) |
134 | 133 | oveq1d 6564 |
. . . . . 6
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 0) → ((𝑥 · 𝑦) mod (𝑁‘𝐾)) = ((𝑖 · 0) mod (𝑁‘𝐾))) |
135 | | ovex 6577 |
. . . . . 6
⊢ ((𝑖 · 0) mod (𝑁‘𝐾)) ∈ V |
136 | 134, 55, 135 | ovmpt2a 6689 |
. . . . 5
⊢ ((𝑖 ∈ V ∧ 0 ∈ V)
→ (𝑖𝑃0) = ((𝑖 · 0) mod (𝑁‘𝐾))) |
137 | 90, 119, 136 | mp2an 704 |
. . . 4
⊢ (𝑖𝑃0) = ((𝑖 · 0) mod (𝑁‘𝐾)) |
138 | 125 | mul01d 10114 |
. . . . . 6
⊢ (𝑖 ∈ ℕ0
→ (𝑖 · 0) =
0) |
139 | 138 | oveq1d 6564 |
. . . . 5
⊢ (𝑖 ∈ ℕ0
→ ((𝑖 · 0) mod
(𝑁‘𝐾)) = (0 mod (𝑁‘𝐾))) |
140 | 139, 130 | sylan9eqr 2666 |
. . . 4
⊢ (((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → ((𝑖 · 0) mod (𝑁‘𝐾)) = 0) |
141 | 137, 140 | syl5eq 2656 |
. . 3
⊢ (((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → (𝑖𝑃0) = 0) |
142 | | simpr 476 |
. . 3
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → 𝐾 ∈ (0...(deg‘𝐹))) |
143 | 18 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → (deg‘𝐹) ∈
ℕ0) |
144 | 1 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → 𝐾 ∈
ℕ0) |
145 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑁‘𝑘) = (𝑁‘𝐾)) |
146 | 145 | oveq1d 6564 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ((𝑁‘𝑘) mod (𝑁‘𝐾)) = ((𝑁‘𝐾) mod (𝑁‘𝐾))) |
147 | | ovex 6577 |
. . . . . 6
⊢ ((𝑁‘𝐾) mod (𝑁‘𝐾)) ∈ V |
148 | 146, 71, 147 | fvmpt 6191 |
. . . . 5
⊢ (𝐾 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((𝑁‘𝑘) mod (𝑁‘𝐾)))‘𝐾) = ((𝑁‘𝐾) mod (𝑁‘𝐾))) |
149 | 144, 148 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁‘𝑘) mod (𝑁‘𝐾)))‘𝐾) = ((𝑁‘𝐾) mod (𝑁‘𝐾))) |
150 | 98 | nncnd 10913 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → (𝑁‘𝐾) ∈ ℂ) |
151 | 98 | nnne0d 10942 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → (𝑁‘𝐾) ≠ 0) |
152 | 150, 151 | dividd 10678 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁‘𝐾) / (𝑁‘𝐾)) = 1) |
153 | | 1z 11284 |
. . . . . 6
⊢ 1 ∈
ℤ |
154 | 152, 153 | syl6eqel 2696 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁‘𝐾) / (𝑁‘𝐾)) ∈ ℤ) |
155 | 98 | nnred 10912 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → (𝑁‘𝐾) ∈ ℝ) |
156 | | mod0 12537 |
. . . . . 6
⊢ (((𝑁‘𝐾) ∈ ℝ ∧ (𝑁‘𝐾) ∈ ℝ+) →
(((𝑁‘𝐾) mod (𝑁‘𝐾)) = 0 ↔ ((𝑁‘𝐾) / (𝑁‘𝐾)) ∈ ℤ)) |
157 | 155, 128,
156 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → (((𝑁‘𝐾) mod (𝑁‘𝐾)) = 0 ↔ ((𝑁‘𝐾) / (𝑁‘𝐾)) ∈ ℤ)) |
158 | 154, 157 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁‘𝐾) mod (𝑁‘𝐾)) = 0) |
159 | 149, 158 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁‘𝑘) mod (𝑁‘𝐾)))‘𝐾) = 0) |
160 | 101, 118,
132, 141, 142, 143, 159 | seqz 12711 |
. 2
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁‘𝑘) mod (𝑁‘𝐾))))‘(deg‘𝐹)) = 0) |
161 | 78, 89, 160 | 3eqtr3d 2652 |
1
⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → (𝑅 mod (𝑁‘𝐾)) = 0) |