Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elqaalem2 Structured version   Visualization version   GIF version

Theorem elqaalem2 25015
 Description: Lemma for elqaa 25017. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by AV, 3-Oct-2020.)
Hypotheses
Ref Expression
elqaa.1 (𝜑𝐴 ∈ ℂ)
elqaa.2 (𝜑𝐹 ∈ ((Poly‘ℚ) ∖ {0𝑝}))
elqaa.3 (𝜑 → (𝐹𝐴) = 0)
elqaa.4 𝐵 = (coeff‘𝐹)
elqaa.5 𝑁 = (𝑘 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵𝑘) · 𝑛) ∈ ℤ}, ℝ, < ))
elqaa.6 𝑅 = (seq0( · , 𝑁)‘(deg‘𝐹))
elqaa.7 𝑃 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 · 𝑦) mod (𝑁𝐾)))
Assertion
Ref Expression
elqaalem2 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑅 mod (𝑁𝐾)) = 0)
Distinct variable groups:   𝑘,𝑛,𝑥,𝑦,𝐴   𝐵,𝑘,𝑛   𝜑,𝑘   𝑘,𝐾,𝑛,𝑥,𝑦   𝑘,𝑁,𝑛,𝑥,𝑦   𝑅,𝑘
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑛)   𝐵(𝑥,𝑦)   𝑃(𝑥,𝑦,𝑘,𝑛)   𝑅(𝑥,𝑦,𝑛)   𝐹(𝑥,𝑦,𝑘,𝑛)

Proof of Theorem elqaalem2
Dummy variables 𝑚 𝑖 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfznn0 13049 . . 3 (𝐾 ∈ (0...(deg‘𝐹)) → 𝐾 ∈ ℕ0)
2 elqaa.6 . . . . 5 𝑅 = (seq0( · , 𝑁)‘(deg‘𝐹))
32fveq2i 6661 . . . 4 ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(seq0( · , 𝑁)‘(deg‘𝐹)))
4 nnmulcl 11698 . . . . . 6 ((𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑖 · 𝑗) ∈ ℕ)
54adantl 485 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 · 𝑗) ∈ ℕ)
6 elfznn0 13049 . . . . . 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({𝑛 ∈ ℕ ∣ ((𝐵𝑘) · 𝑛) ∈ ℤ}, ℝ, < ))
127, 8, 9, 10, 11, 2elqaalem1 25014 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ0) → ((𝑁𝑖) ∈ ℕ ∧ ((𝐵𝑖) · (𝑁𝑖)) ∈ ℤ))
1312simpld 498 . . . . . . 7 ((𝜑𝑖 ∈ ℕ0) → (𝑁𝑖) ∈ ℕ)
1413adantlr 714 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → (𝑁𝑖) ∈ ℕ)
156, 14sylan2 595 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → (𝑁𝑖) ∈ ℕ)
16 eldifi 4032 . . . . . . . 8 (𝐹 ∈ ((Poly‘ℚ) ∖ {0𝑝}) → 𝐹 ∈ (Poly‘ℚ))
17 dgrcl 24929 . . . . . . . 8 (𝐹 ∈ (Poly‘ℚ) → (deg‘𝐹) ∈ ℕ0)
188, 16, 173syl 18 . . . . . . 7 (𝜑 → (deg‘𝐹) ∈ ℕ0)
19 nn0uz 12320 . . . . . . 7 0 = (ℤ‘0)
2018, 19eleqtrdi 2862 . . . . . 6 (𝜑 → (deg‘𝐹) ∈ (ℤ‘0))
2120adantr 484 . . . . 5 ((𝜑𝐾 ∈ ℕ0) → (deg‘𝐹) ∈ (ℤ‘0))
22 nnz 12043 . . . . . . . . . 10 (𝑖 ∈ ℕ → 𝑖 ∈ ℤ)
2322ad2antrl 727 . . . . . . . . 9 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℤ)
247, 8, 9, 10, 11, 2elqaalem1 25014 . . . . . . . . . . 11 ((𝜑𝐾 ∈ ℕ0) → ((𝑁𝐾) ∈ ℕ ∧ ((𝐵𝐾) · (𝑁𝐾)) ∈ ℤ))
2524simpld 498 . . . . . . . . . 10 ((𝜑𝐾 ∈ ℕ0) → (𝑁𝐾) ∈ ℕ)
2625adantr 484 . . . . . . . . 9 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑁𝐾) ∈ ℕ)
2723, 26zmodcld 13309 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 mod (𝑁𝐾)) ∈ ℕ0)
2827nn0zd 12124 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 mod (𝑁𝐾)) ∈ ℤ)
29 nnz 12043 . . . . . . . . . 10 (𝑗 ∈ ℕ → 𝑗 ∈ ℤ)
3029ad2antll 728 . . . . . . . . 9 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℤ)
3130, 26zmodcld 13309 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑗 mod (𝑁𝐾)) ∈ ℕ0)
3231nn0zd 12124 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑗 mod (𝑁𝐾)) ∈ ℤ)
3326nnrpd 12470 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑁𝐾) ∈ ℝ+)
34 nnre 11681 . . . . . . . . 9 (𝑖 ∈ ℕ → 𝑖 ∈ ℝ)
3534ad2antrl 727 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℝ)
36 modabs2 13322 . . . . . . . 8 ((𝑖 ∈ ℝ ∧ (𝑁𝐾) ∈ ℝ+) → ((𝑖 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑖 mod (𝑁𝐾)))
3735, 33, 36syl2anc 587 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑖 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑖 mod (𝑁𝐾)))
38 nnre 11681 . . . . . . . . 9 (𝑗 ∈ ℕ → 𝑗 ∈ ℝ)
3938ad2antll 728 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℝ)
40 modabs2 13322 . . . . . . . 8 ((𝑗 ∈ ℝ ∧ (𝑁𝐾) ∈ ℝ+) → ((𝑗 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑗 mod (𝑁𝐾)))
4139, 33, 40syl2anc 587 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑗 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑗 mod (𝑁𝐾)))
4228, 23, 32, 30, 33, 37, 41modmul12d 13342 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
43 oveq1 7157 . . . . . . . . . 10 (𝑘 = 𝑖 → (𝑘 mod (𝑁𝐾)) = (𝑖 mod (𝑁𝐾)))
44 eqid 2758 . . . . . . . . . 10 (𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾))) = (𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))
45 ovex 7183 . . . . . . . . . 10 (𝑖 mod (𝑁𝐾)) ∈ V
4643, 44, 45fvmpt 6759 . . . . . . . . 9 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖) = (𝑖 mod (𝑁𝐾)))
4746ad2antrl 727 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖) = (𝑖 mod (𝑁𝐾)))
48 oveq1 7157 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝑘 mod (𝑁𝐾)) = (𝑗 mod (𝑁𝐾)))
49 ovex 7183 . . . . . . . . . 10 (𝑗 mod (𝑁𝐾)) ∈ V
5048, 44, 49fvmpt 6759 . . . . . . . . 9 (𝑗 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗) = (𝑗 mod (𝑁𝐾)))
5150ad2antll 728 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗) = (𝑗 mod (𝑁𝐾)))
5247, 51oveq12d 7168 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗)) = ((𝑖 mod (𝑁𝐾))𝑃(𝑗 mod (𝑁𝐾))))
53 oveq12 7159 . . . . . . . . . 10 ((𝑥 = (𝑖 mod (𝑁𝐾)) ∧ 𝑦 = (𝑗 mod (𝑁𝐾))) → (𝑥 · 𝑦) = ((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))))
5453oveq1d 7165 . . . . . . . . 9 ((𝑥 = (𝑖 mod (𝑁𝐾)) ∧ 𝑦 = (𝑗 mod (𝑁𝐾))) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)))
55 elqaa.7 . . . . . . . . 9 𝑃 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 · 𝑦) mod (𝑁𝐾)))
56 ovex 7183 . . . . . . . . 9 (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)) ∈ V
5754, 55, 56ovmpoa 7300 . . . . . . . 8 (((𝑖 mod (𝑁𝐾)) ∈ V ∧ (𝑗 mod (𝑁𝐾)) ∈ V) → ((𝑖 mod (𝑁𝐾))𝑃(𝑗 mod (𝑁𝐾))) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)))
5845, 49, 57mp2an 691 . . . . . . 7 ((𝑖 mod (𝑁𝐾))𝑃(𝑗 mod (𝑁𝐾))) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾))
5952, 58eqtrdi 2809 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗)) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)))
60 oveq1 7157 . . . . . . . 8 (𝑘 = (𝑖 · 𝑗) → (𝑘 mod (𝑁𝐾)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
61 ovex 7183 . . . . . . . 8 ((𝑖 · 𝑗) mod (𝑁𝐾)) ∈ V
6260, 44, 61fvmpt 6759 . . . . . . 7 ((𝑖 · 𝑗) ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑖 · 𝑗)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
635, 62syl 17 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑖 · 𝑗)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
6442, 59, 633eqtr4rd 2804 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑖 · 𝑗)) = (((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗)))
65 oveq1 7157 . . . . . . . . 9 (𝑘 = (𝑁𝑖) → (𝑘 mod (𝑁𝐾)) = ((𝑁𝑖) mod (𝑁𝐾)))
66 ovex 7183 . . . . . . . . 9 ((𝑁𝑖) mod (𝑁𝐾)) ∈ V
6765, 44, 66fvmpt 6759 . . . . . . . 8 ((𝑁𝑖) ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑁𝑖) mod (𝑁𝐾)))
6814, 67syl 17 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑁𝑖) mod (𝑁𝐾)))
69 fveq2 6658 . . . . . . . . . 10 (𝑘 = 𝑖 → (𝑁𝑘) = (𝑁𝑖))
7069oveq1d 7165 . . . . . . . . 9 (𝑘 = 𝑖 → ((𝑁𝑘) mod (𝑁𝐾)) = ((𝑁𝑖) mod (𝑁𝐾)))
71 eqid 2758 . . . . . . . . 9 (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))) = (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))
7270, 71, 66fvmpt 6759 . . . . . . . 8 (𝑖 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) = ((𝑁𝑖) mod (𝑁𝐾)))
7372adantl 485 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) = ((𝑁𝑖) mod (𝑁𝐾)))
7468, 73eqtr4d 2796 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖))
756, 74sylan2 595 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖))
765, 15, 21, 64, 75seqhomo 13467 . . . 4 ((𝜑𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(seq0( · , 𝑁)‘(deg‘𝐹))) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)))
773, 76syl5eq 2805 . . 3 ((𝜑𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)))
781, 77sylan2 595 . 2 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)))
79 0zd 12032 . . . . . . . 8 (𝜑 → 0 ∈ ℤ)
804adantl 485 . . . . . . . 8 ((𝜑 ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 · 𝑗) ∈ ℕ)
8119, 79, 13, 80seqf 13441 . . . . . . 7 (𝜑 → seq0( · , 𝑁):ℕ0⟶ℕ)
8281, 18ffvelrnd 6843 . . . . . 6 (𝜑 → (seq0( · , 𝑁)‘(deg‘𝐹)) ∈ ℕ)
832, 82eqeltrid 2856 . . . . 5 (𝜑𝑅 ∈ ℕ)
8483adantr 484 . . . 4 ((𝜑𝐾 ∈ ℕ0) → 𝑅 ∈ ℕ)
85 oveq1 7157 . . . . 5 (𝑘 = 𝑅 → (𝑘 mod (𝑁𝐾)) = (𝑅 mod (𝑁𝐾)))
86 ovex 7183 . . . . 5 (𝑅 mod (𝑁𝐾)) ∈ V
8785, 44, 86fvmpt 6759 . . . 4 (𝑅 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (𝑅 mod (𝑁𝐾)))
8884, 87syl 17 . . 3 ((𝜑𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (𝑅 mod (𝑁𝐾)))
891, 88sylan2 595 . 2 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (𝑅 mod (𝑁𝐾)))
90 oveq12 7159 . . . . . . 7 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑥 · 𝑦) = (𝑖 · 𝑗))
9190oveq1d 7165 . . . . . 6 ((𝑥 = 𝑖𝑦 = 𝑗) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
9291, 55, 61ovmpoa 7300 . . . . 5 ((𝑖 ∈ V ∧ 𝑗 ∈ V) → (𝑖𝑃𝑗) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
9392el2v 3417 . . . 4 (𝑖𝑃𝑗) = ((𝑖 · 𝑗) mod (𝑁𝐾))
94 nn0mulcl 11970 . . . . . 6 ((𝑖 ∈ ℕ0𝑗 ∈ ℕ0) → (𝑖 · 𝑗) ∈ ℕ0)
9594nn0zd 12124 . . . . 5 ((𝑖 ∈ ℕ0𝑗 ∈ ℕ0) → (𝑖 · 𝑗) ∈ ℤ)
961, 25sylan2 595 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℕ)
97 zmodcl 13308 . . . . 5 (((𝑖 · 𝑗) ∈ ℤ ∧ (𝑁𝐾) ∈ ℕ) → ((𝑖 · 𝑗) mod (𝑁𝐾)) ∈ ℕ0)
9895, 96, 97syl2anr 599 . . . 4 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ (𝑖 ∈ ℕ0𝑗 ∈ ℕ0)) → ((𝑖 · 𝑗) mod (𝑁𝐾)) ∈ ℕ0)
9993, 98eqeltrid 2856 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ (𝑖 ∈ ℕ0𝑗 ∈ ℕ0)) → (𝑖𝑃𝑗) ∈ ℕ0)
100 fveq2 6658 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑚 → (𝐵𝑘) = (𝐵𝑚))
101100oveq1d 7165 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑚 → ((𝐵𝑘) · 𝑛) = ((𝐵𝑚) · 𝑛))
102101eleq1d 2836 . . . . . . . . . . . . . . 15 (𝑘 = 𝑚 → (((𝐵𝑘) · 𝑛) ∈ ℤ ↔ ((𝐵𝑚) · 𝑛) ∈ ℤ))
103102rabbidv 3392 . . . . . . . . . . . . . 14 (𝑘 = 𝑚 → {𝑛 ∈ ℕ ∣ ((𝐵𝑘) · 𝑛) ∈ ℤ} = {𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ})
104103infeq1d 8974 . . . . . . . . . . . . 13 (𝑘 = 𝑚 → inf({𝑛 ∈ ℕ ∣ ((𝐵𝑘) · 𝑛) ∈ ℤ}, ℝ, < ) = inf({𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ}, ℝ, < ))
105104cbvmptv 5135 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵𝑘) · 𝑛) ∈ ℤ}, ℝ, < )) = (𝑚 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ}, ℝ, < ))
10611, 105eqtri 2781 . . . . . . . . . . 11 𝑁 = (𝑚 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ}, ℝ, < ))
1077, 8, 9, 10, 106, 2elqaalem1 25014 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((𝑁𝑘) ∈ ℕ ∧ ((𝐵𝑘) · (𝑁𝑘)) ∈ ℤ))
108107simpld 498 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (𝑁𝑘) ∈ ℕ)
109108adantlr 714 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑁𝑘) ∈ ℕ)
110109nnzd 12125 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑁𝑘) ∈ ℤ)
11125adantr 484 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑁𝐾) ∈ ℕ)
112110, 111zmodcld 13309 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → ((𝑁𝑘) mod (𝑁𝐾)) ∈ ℕ0)
113112fmpttd 6870 . . . . 5 ((𝜑𝐾 ∈ ℕ0) → (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))):ℕ0⟶ℕ0)
1141, 113sylan2 595 . . . 4 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))):ℕ0⟶ℕ0)
115 ffvelrn 6840 . . . 4 (((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))):ℕ0⟶ℕ0𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) ∈ ℕ0)
116114, 6, 115syl2an 598 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) ∈ ℕ0)
117 c0ex 10673 . . . . 5 0 ∈ V
118 vex 3413 . . . . 5 𝑖 ∈ V
119 oveq12 7159 . . . . . . 7 ((𝑥 = 0 ∧ 𝑦 = 𝑖) → (𝑥 · 𝑦) = (0 · 𝑖))
120119oveq1d 7165 . . . . . 6 ((𝑥 = 0 ∧ 𝑦 = 𝑖) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = ((0 · 𝑖) mod (𝑁𝐾)))
121 ovex 7183 . . . . . 6 ((0 · 𝑖) mod (𝑁𝐾)) ∈ V
122120, 55, 121ovmpoa 7300 . . . . 5 ((0 ∈ V ∧ 𝑖 ∈ V) → (0𝑃𝑖) = ((0 · 𝑖) mod (𝑁𝐾)))
123117, 118, 122mp2an 691 . . . 4 (0𝑃𝑖) = ((0 · 𝑖) mod (𝑁𝐾))
124 nn0cn 11944 . . . . . . 7 (𝑖 ∈ ℕ0𝑖 ∈ ℂ)
125124mul02d 10876 . . . . . 6 (𝑖 ∈ ℕ0 → (0 · 𝑖) = 0)
126125oveq1d 7165 . . . . 5 (𝑖 ∈ ℕ0 → ((0 · 𝑖) mod (𝑁𝐾)) = (0 mod (𝑁𝐾)))
12796nnrpd 12470 . . . . . 6 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℝ+)
128 0mod 13319 . . . . . 6 ((𝑁𝐾) ∈ ℝ+ → (0 mod (𝑁𝐾)) = 0)
129127, 128syl 17 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (0 mod (𝑁𝐾)) = 0)
130126, 129sylan9eqr 2815 . . . 4 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → ((0 · 𝑖) mod (𝑁𝐾)) = 0)
131123, 130syl5eq 2805 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → (0𝑃𝑖) = 0)
132 oveq12 7159 . . . . . . 7 ((𝑥 = 𝑖𝑦 = 0) → (𝑥 · 𝑦) = (𝑖 · 0))
133132oveq1d 7165 . . . . . 6 ((𝑥 = 𝑖𝑦 = 0) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = ((𝑖 · 0) mod (𝑁𝐾)))
134 ovex 7183 . . . . . 6 ((𝑖 · 0) mod (𝑁𝐾)) ∈ V
135133, 55, 134ovmpoa 7300 . . . . 5 ((𝑖 ∈ V ∧ 0 ∈ V) → (𝑖𝑃0) = ((𝑖 · 0) mod (𝑁𝐾)))
136118, 117, 135mp2an 691 . . . 4 (𝑖𝑃0) = ((𝑖 · 0) mod (𝑁𝐾))
137124mul01d 10877 . . . . . 6 (𝑖 ∈ ℕ0 → (𝑖 · 0) = 0)
138137oveq1d 7165 . . . . 5 (𝑖 ∈ ℕ0 → ((𝑖 · 0) mod (𝑁𝐾)) = (0 mod (𝑁𝐾)))
139138, 129sylan9eqr 2815 . . . 4 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → ((𝑖 · 0) mod (𝑁𝐾)) = 0)
140136, 139syl5eq 2805 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → (𝑖𝑃0) = 0)
141 simpr 488 . . 3 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → 𝐾 ∈ (0...(deg‘𝐹)))
14218adantr 484 . . 3 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (deg‘𝐹) ∈ ℕ0)
1431adantl 485 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → 𝐾 ∈ ℕ0)
144 fveq2 6658 . . . . . . 7 (𝑘 = 𝐾 → (𝑁𝑘) = (𝑁𝐾))
145144oveq1d 7165 . . . . . 6 (𝑘 = 𝐾 → ((𝑁𝑘) mod (𝑁𝐾)) = ((𝑁𝐾) mod (𝑁𝐾)))
146 ovex 7183 . . . . . 6 ((𝑁𝐾) mod (𝑁𝐾)) ∈ V
147145, 71, 146fvmpt 6759 . . . . 5 (𝐾 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝐾) = ((𝑁𝐾) mod (𝑁𝐾)))
148143, 147syl 17 . . . 4 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝐾) = ((𝑁𝐾) mod (𝑁𝐾)))
14996nncnd 11690 . . . . . . 7 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℂ)
15096nnne0d 11724 . . . . . . 7 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ≠ 0)
151149, 150dividd 11452 . . . . . 6 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁𝐾) / (𝑁𝐾)) = 1)
152 1z 12051 . . . . . 6 1 ∈ ℤ
153151, 152eqeltrdi 2860 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁𝐾) / (𝑁𝐾)) ∈ ℤ)
15496nnred 11689 . . . . . 6 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℝ)
155 mod0 13293 . . . . . 6 (((𝑁𝐾) ∈ ℝ ∧ (𝑁𝐾) ∈ ℝ+) → (((𝑁𝐾) mod (𝑁𝐾)) = 0 ↔ ((𝑁𝐾) / (𝑁𝐾)) ∈ ℤ))
156154, 127, 155syl2anc 587 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (((𝑁𝐾) mod (𝑁𝐾)) = 0 ↔ ((𝑁𝐾) / (𝑁𝐾)) ∈ ℤ))
157153, 156mpbird 260 . . . 4 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁𝐾) mod (𝑁𝐾)) = 0)
158148, 157eqtrd 2793 . . 3 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝐾) = 0)
15999, 116, 131, 140, 141, 142, 158seqz 13468 . 2 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)) = 0)
16078, 89, 1593eqtr3d 2801 1 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑅 mod (𝑁𝐾)) = 0)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {crab 3074  Vcvv 3409   ∖ cdif 3855  {csn 4522   ↦ cmpt 5112  ⟶wf 6331  ‘cfv 6335  (class class class)co 7150   ∈ cmpo 7152  infcinf 8938  ℂcc 10573  ℝcr 10574  0cc0 10575  1c1 10576   · cmul 10580   < clt 10713   / cdiv 11335  ℕcn 11674  ℕ0cn0 11934  ℤcz 12020  ℤ≥cuz 12282  ℚcq 12388  ℝ+crp 12430  ...cfz 12939   mod cmo 13286  seqcseq 13418  0𝑝c0p 24369  Polycply 24880  coeffccoe 24882  degcdgr 24883 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-inf2 9137  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652  ax-pre-sup 10653  ax-addf 10654 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-int 4839  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-se 5484  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-isom 6344  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7405  df-om 7580  df-1st 7693  df-2nd 7694  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-er 8299  df-map 8418  df-pm 8419  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-sup 8939  df-inf 8940  df-oi 9007  df-card 9401  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-div 11336  df-nn 11675  df-2 11737  df-3 11738  df-n0 11935  df-z 12021  df-uz 12283  df-q 12389  df-rp 12431  df-fz 12940  df-fzo 13083  df-fl 13211  df-mod 13287  df-seq 13419  df-exp 13480  df-hash 13741  df-cj 14506  df-re 14507  df-im 14508  df-sqrt 14642  df-abs 14643  df-clim 14893  df-rlim 14894  df-sum 15091  df-0p 24370  df-ply 24884  df-coe 24886  df-dgr 24887 This theorem is referenced by:  elqaalem3  25016
 Copyright terms: Public domain W3C validator