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

Theorem elqaalem2 24836
Description: Lemma for elqaa 24838. (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 12988 . . 3 (𝐾 ∈ (0...(deg‘𝐹)) → 𝐾 ∈ ℕ0)
2 elqaa.6 . . . . 5 𝑅 = (seq0( · , 𝑁)‘(deg‘𝐹))
32fveq2i 6666 . . . 4 ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(seq0( · , 𝑁)‘(deg‘𝐹)))
4 nnmulcl 11649 . . . . . 6 ((𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑖 · 𝑗) ∈ ℕ)
54adantl 482 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 · 𝑗) ∈ ℕ)
6 elfznn0 12988 . . . . . 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 24835 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ0) → ((𝑁𝑖) ∈ ℕ ∧ ((𝐵𝑖) · (𝑁𝑖)) ∈ ℤ))
1312simpld 495 . . . . . . 7 ((𝜑𝑖 ∈ ℕ0) → (𝑁𝑖) ∈ ℕ)
1413adantlr 711 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → (𝑁𝑖) ∈ ℕ)
156, 14sylan2 592 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → (𝑁𝑖) ∈ ℕ)
16 eldifi 4100 . . . . . . . 8 (𝐹 ∈ ((Poly‘ℚ) ∖ {0𝑝}) → 𝐹 ∈ (Poly‘ℚ))
17 dgrcl 24750 . . . . . . . 8 (𝐹 ∈ (Poly‘ℚ) → (deg‘𝐹) ∈ ℕ0)
188, 16, 173syl 18 . . . . . . 7 (𝜑 → (deg‘𝐹) ∈ ℕ0)
19 nn0uz 12268 . . . . . . 7 0 = (ℤ‘0)
2018, 19eleqtrdi 2920 . . . . . 6 (𝜑 → (deg‘𝐹) ∈ (ℤ‘0))
2120adantr 481 . . . . 5 ((𝜑𝐾 ∈ ℕ0) → (deg‘𝐹) ∈ (ℤ‘0))
22 nnz 11992 . . . . . . . . . 10 (𝑖 ∈ ℕ → 𝑖 ∈ ℤ)
2322ad2antrl 724 . . . . . . . . 9 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℤ)
247, 8, 9, 10, 11, 2elqaalem1 24835 . . . . . . . . . . 11 ((𝜑𝐾 ∈ ℕ0) → ((𝑁𝐾) ∈ ℕ ∧ ((𝐵𝐾) · (𝑁𝐾)) ∈ ℤ))
2524simpld 495 . . . . . . . . . 10 ((𝜑𝐾 ∈ ℕ0) → (𝑁𝐾) ∈ ℕ)
2625adantr 481 . . . . . . . . 9 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑁𝐾) ∈ ℕ)
2723, 26zmodcld 13248 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 mod (𝑁𝐾)) ∈ ℕ0)
2827nn0zd 12073 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 mod (𝑁𝐾)) ∈ ℤ)
29 nnz 11992 . . . . . . . . . 10 (𝑗 ∈ ℕ → 𝑗 ∈ ℤ)
3029ad2antll 725 . . . . . . . . 9 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℤ)
3130, 26zmodcld 13248 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑗 mod (𝑁𝐾)) ∈ ℕ0)
3231nn0zd 12073 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑗 mod (𝑁𝐾)) ∈ ℤ)
3326nnrpd 12417 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑁𝐾) ∈ ℝ+)
34 nnre 11633 . . . . . . . . 9 (𝑖 ∈ ℕ → 𝑖 ∈ ℝ)
3534ad2antrl 724 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℝ)
36 modabs2 13261 . . . . . . . 8 ((𝑖 ∈ ℝ ∧ (𝑁𝐾) ∈ ℝ+) → ((𝑖 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑖 mod (𝑁𝐾)))
3735, 33, 36syl2anc 584 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑖 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑖 mod (𝑁𝐾)))
38 nnre 11633 . . . . . . . . 9 (𝑗 ∈ ℕ → 𝑗 ∈ ℝ)
3938ad2antll 725 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℝ)
40 modabs2 13261 . . . . . . . 8 ((𝑗 ∈ ℝ ∧ (𝑁𝐾) ∈ ℝ+) → ((𝑗 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑗 mod (𝑁𝐾)))
4139, 33, 40syl2anc 584 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑗 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑗 mod (𝑁𝐾)))
4228, 23, 32, 30, 33, 37, 41modmul12d 13281 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
43 oveq1 7152 . . . . . . . . . 10 (𝑘 = 𝑖 → (𝑘 mod (𝑁𝐾)) = (𝑖 mod (𝑁𝐾)))
44 eqid 2818 . . . . . . . . . 10 (𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾))) = (𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))
45 ovex 7178 . . . . . . . . . 10 (𝑖 mod (𝑁𝐾)) ∈ V
4643, 44, 45fvmpt 6761 . . . . . . . . 9 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖) = (𝑖 mod (𝑁𝐾)))
4746ad2antrl 724 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖) = (𝑖 mod (𝑁𝐾)))
48 oveq1 7152 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝑘 mod (𝑁𝐾)) = (𝑗 mod (𝑁𝐾)))
49 ovex 7178 . . . . . . . . . 10 (𝑗 mod (𝑁𝐾)) ∈ V
5048, 44, 49fvmpt 6761 . . . . . . . . 9 (𝑗 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗) = (𝑗 mod (𝑁𝐾)))
5150ad2antll 725 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗) = (𝑗 mod (𝑁𝐾)))
5247, 51oveq12d 7163 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗)) = ((𝑖 mod (𝑁𝐾))𝑃(𝑗 mod (𝑁𝐾))))
53 oveq12 7154 . . . . . . . . . 10 ((𝑥 = (𝑖 mod (𝑁𝐾)) ∧ 𝑦 = (𝑗 mod (𝑁𝐾))) → (𝑥 · 𝑦) = ((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))))
5453oveq1d 7160 . . . . . . . . 9 ((𝑥 = (𝑖 mod (𝑁𝐾)) ∧ 𝑦 = (𝑗 mod (𝑁𝐾))) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)))
55 elqaa.7 . . . . . . . . 9 𝑃 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 · 𝑦) mod (𝑁𝐾)))
56 ovex 7178 . . . . . . . . 9 (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)) ∈ V
5754, 55, 56ovmpoa 7294 . . . . . . . 8 (((𝑖 mod (𝑁𝐾)) ∈ V ∧ (𝑗 mod (𝑁𝐾)) ∈ V) → ((𝑖 mod (𝑁𝐾))𝑃(𝑗 mod (𝑁𝐾))) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)))
5845, 49, 57mp2an 688 . . . . . . 7 ((𝑖 mod (𝑁𝐾))𝑃(𝑗 mod (𝑁𝐾))) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾))
5952, 58syl6eq 2869 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗)) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)))
60 oveq1 7152 . . . . . . . 8 (𝑘 = (𝑖 · 𝑗) → (𝑘 mod (𝑁𝐾)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
61 ovex 7178 . . . . . . . 8 ((𝑖 · 𝑗) mod (𝑁𝐾)) ∈ V
6260, 44, 61fvmpt 6761 . . . . . . 7 ((𝑖 · 𝑗) ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑖 · 𝑗)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
635, 62syl 17 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑖 · 𝑗)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
6442, 59, 633eqtr4rd 2864 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑖 · 𝑗)) = (((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗)))
65 oveq1 7152 . . . . . . . . 9 (𝑘 = (𝑁𝑖) → (𝑘 mod (𝑁𝐾)) = ((𝑁𝑖) mod (𝑁𝐾)))
66 ovex 7178 . . . . . . . . 9 ((𝑁𝑖) mod (𝑁𝐾)) ∈ V
6765, 44, 66fvmpt 6761 . . . . . . . 8 ((𝑁𝑖) ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑁𝑖) mod (𝑁𝐾)))
6814, 67syl 17 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑁𝑖) mod (𝑁𝐾)))
69 fveq2 6663 . . . . . . . . . 10 (𝑘 = 𝑖 → (𝑁𝑘) = (𝑁𝑖))
7069oveq1d 7160 . . . . . . . . 9 (𝑘 = 𝑖 → ((𝑁𝑘) mod (𝑁𝐾)) = ((𝑁𝑖) mod (𝑁𝐾)))
71 eqid 2818 . . . . . . . . 9 (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))) = (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))
7270, 71, 66fvmpt 6761 . . . . . . . 8 (𝑖 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) = ((𝑁𝑖) mod (𝑁𝐾)))
7372adantl 482 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) = ((𝑁𝑖) mod (𝑁𝐾)))
7468, 73eqtr4d 2856 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖))
756, 74sylan2 592 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖))
765, 15, 21, 64, 75seqhomo 13405 . . . 4 ((𝜑𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(seq0( · , 𝑁)‘(deg‘𝐹))) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)))
773, 76syl5eq 2865 . . 3 ((𝜑𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)))
781, 77sylan2 592 . 2 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)))
79 0zd 11981 . . . . . . . 8 (𝜑 → 0 ∈ ℤ)
804adantl 482 . . . . . . . 8 ((𝜑 ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 · 𝑗) ∈ ℕ)
8119, 79, 13, 80seqf 13379 . . . . . . 7 (𝜑 → seq0( · , 𝑁):ℕ0⟶ℕ)
8281, 18ffvelrnd 6844 . . . . . 6 (𝜑 → (seq0( · , 𝑁)‘(deg‘𝐹)) ∈ ℕ)
832, 82eqeltrid 2914 . . . . 5 (𝜑𝑅 ∈ ℕ)
8483adantr 481 . . . 4 ((𝜑𝐾 ∈ ℕ0) → 𝑅 ∈ ℕ)
85 oveq1 7152 . . . . 5 (𝑘 = 𝑅 → (𝑘 mod (𝑁𝐾)) = (𝑅 mod (𝑁𝐾)))
86 ovex 7178 . . . . 5 (𝑅 mod (𝑁𝐾)) ∈ V
8785, 44, 86fvmpt 6761 . . . 4 (𝑅 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (𝑅 mod (𝑁𝐾)))
8884, 87syl 17 . . 3 ((𝜑𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (𝑅 mod (𝑁𝐾)))
891, 88sylan2 592 . 2 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (𝑅 mod (𝑁𝐾)))
90 oveq12 7154 . . . . . . 7 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑥 · 𝑦) = (𝑖 · 𝑗))
9190oveq1d 7160 . . . . . 6 ((𝑥 = 𝑖𝑦 = 𝑗) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
9291, 55, 61ovmpoa 7294 . . . . 5 ((𝑖 ∈ V ∧ 𝑗 ∈ V) → (𝑖𝑃𝑗) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
9392el2v 3499 . . . 4 (𝑖𝑃𝑗) = ((𝑖 · 𝑗) mod (𝑁𝐾))
94 nn0mulcl 11921 . . . . . 6 ((𝑖 ∈ ℕ0𝑗 ∈ ℕ0) → (𝑖 · 𝑗) ∈ ℕ0)
9594nn0zd 12073 . . . . 5 ((𝑖 ∈ ℕ0𝑗 ∈ ℕ0) → (𝑖 · 𝑗) ∈ ℤ)
961, 25sylan2 592 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℕ)
97 zmodcl 13247 . . . . 5 (((𝑖 · 𝑗) ∈ ℤ ∧ (𝑁𝐾) ∈ ℕ) → ((𝑖 · 𝑗) mod (𝑁𝐾)) ∈ ℕ0)
9895, 96, 97syl2anr 596 . . . 4 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ (𝑖 ∈ ℕ0𝑗 ∈ ℕ0)) → ((𝑖 · 𝑗) mod (𝑁𝐾)) ∈ ℕ0)
9993, 98eqeltrid 2914 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ (𝑖 ∈ ℕ0𝑗 ∈ ℕ0)) → (𝑖𝑃𝑗) ∈ ℕ0)
100 fveq2 6663 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑚 → (𝐵𝑘) = (𝐵𝑚))
101100oveq1d 7160 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑚 → ((𝐵𝑘) · 𝑛) = ((𝐵𝑚) · 𝑛))
102101eleq1d 2894 . . . . . . . . . . . . . . 15 (𝑘 = 𝑚 → (((𝐵𝑘) · 𝑛) ∈ ℤ ↔ ((𝐵𝑚) · 𝑛) ∈ ℤ))
103102rabbidv 3478 . . . . . . . . . . . . . 14 (𝑘 = 𝑚 → {𝑛 ∈ ℕ ∣ ((𝐵𝑘) · 𝑛) ∈ ℤ} = {𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ})
104103infeq1d 8929 . . . . . . . . . . . . 13 (𝑘 = 𝑚 → inf({𝑛 ∈ ℕ ∣ ((𝐵𝑘) · 𝑛) ∈ ℤ}, ℝ, < ) = inf({𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ}, ℝ, < ))
105104cbvmptv 5160 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵𝑘) · 𝑛) ∈ ℤ}, ℝ, < )) = (𝑚 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ}, ℝ, < ))
10611, 105eqtri 2841 . . . . . . . . . . 11 𝑁 = (𝑚 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ}, ℝ, < ))
1077, 8, 9, 10, 106, 2elqaalem1 24835 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((𝑁𝑘) ∈ ℕ ∧ ((𝐵𝑘) · (𝑁𝑘)) ∈ ℤ))
108107simpld 495 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (𝑁𝑘) ∈ ℕ)
109108adantlr 711 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑁𝑘) ∈ ℕ)
110109nnzd 12074 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑁𝑘) ∈ ℤ)
11125adantr 481 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑁𝐾) ∈ ℕ)
112110, 111zmodcld 13248 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → ((𝑁𝑘) mod (𝑁𝐾)) ∈ ℕ0)
113112fmpttd 6871 . . . . 5 ((𝜑𝐾 ∈ ℕ0) → (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))):ℕ0⟶ℕ0)
1141, 113sylan2 592 . . . 4 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))):ℕ0⟶ℕ0)
115 ffvelrn 6841 . . . 4 (((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))):ℕ0⟶ℕ0𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) ∈ ℕ0)
116114, 6, 115syl2an 595 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) ∈ ℕ0)
117 c0ex 10623 . . . . 5 0 ∈ V
118 vex 3495 . . . . 5 𝑖 ∈ V
119 oveq12 7154 . . . . . . 7 ((𝑥 = 0 ∧ 𝑦 = 𝑖) → (𝑥 · 𝑦) = (0 · 𝑖))
120119oveq1d 7160 . . . . . 6 ((𝑥 = 0 ∧ 𝑦 = 𝑖) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = ((0 · 𝑖) mod (𝑁𝐾)))
121 ovex 7178 . . . . . 6 ((0 · 𝑖) mod (𝑁𝐾)) ∈ V
122120, 55, 121ovmpoa 7294 . . . . 5 ((0 ∈ V ∧ 𝑖 ∈ V) → (0𝑃𝑖) = ((0 · 𝑖) mod (𝑁𝐾)))
123117, 118, 122mp2an 688 . . . 4 (0𝑃𝑖) = ((0 · 𝑖) mod (𝑁𝐾))
124 nn0cn 11895 . . . . . . 7 (𝑖 ∈ ℕ0𝑖 ∈ ℂ)
125124mul02d 10826 . . . . . 6 (𝑖 ∈ ℕ0 → (0 · 𝑖) = 0)
126125oveq1d 7160 . . . . 5 (𝑖 ∈ ℕ0 → ((0 · 𝑖) mod (𝑁𝐾)) = (0 mod (𝑁𝐾)))
12796nnrpd 12417 . . . . . 6 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℝ+)
128 0mod 13258 . . . . . 6 ((𝑁𝐾) ∈ ℝ+ → (0 mod (𝑁𝐾)) = 0)
129127, 128syl 17 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (0 mod (𝑁𝐾)) = 0)
130126, 129sylan9eqr 2875 . . . 4 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → ((0 · 𝑖) mod (𝑁𝐾)) = 0)
131123, 130syl5eq 2865 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → (0𝑃𝑖) = 0)
132 oveq12 7154 . . . . . . 7 ((𝑥 = 𝑖𝑦 = 0) → (𝑥 · 𝑦) = (𝑖 · 0))
133132oveq1d 7160 . . . . . 6 ((𝑥 = 𝑖𝑦 = 0) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = ((𝑖 · 0) mod (𝑁𝐾)))
134 ovex 7178 . . . . . 6 ((𝑖 · 0) mod (𝑁𝐾)) ∈ V
135133, 55, 134ovmpoa 7294 . . . . 5 ((𝑖 ∈ V ∧ 0 ∈ V) → (𝑖𝑃0) = ((𝑖 · 0) mod (𝑁𝐾)))
136118, 117, 135mp2an 688 . . . 4 (𝑖𝑃0) = ((𝑖 · 0) mod (𝑁𝐾))
137124mul01d 10827 . . . . . 6 (𝑖 ∈ ℕ0 → (𝑖 · 0) = 0)
138137oveq1d 7160 . . . . 5 (𝑖 ∈ ℕ0 → ((𝑖 · 0) mod (𝑁𝐾)) = (0 mod (𝑁𝐾)))
139138, 129sylan9eqr 2875 . . . 4 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → ((𝑖 · 0) mod (𝑁𝐾)) = 0)
140136, 139syl5eq 2865 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → (𝑖𝑃0) = 0)
141 simpr 485 . . 3 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → 𝐾 ∈ (0...(deg‘𝐹)))
14218adantr 481 . . 3 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (deg‘𝐹) ∈ ℕ0)
1431adantl 482 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → 𝐾 ∈ ℕ0)
144 fveq2 6663 . . . . . . 7 (𝑘 = 𝐾 → (𝑁𝑘) = (𝑁𝐾))
145144oveq1d 7160 . . . . . 6 (𝑘 = 𝐾 → ((𝑁𝑘) mod (𝑁𝐾)) = ((𝑁𝐾) mod (𝑁𝐾)))
146 ovex 7178 . . . . . 6 ((𝑁𝐾) mod (𝑁𝐾)) ∈ V
147145, 71, 146fvmpt 6761 . . . . 5 (𝐾 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝐾) = ((𝑁𝐾) mod (𝑁𝐾)))
148143, 147syl 17 . . . 4 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝐾) = ((𝑁𝐾) mod (𝑁𝐾)))
14996nncnd 11642 . . . . . . 7 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℂ)
15096nnne0d 11675 . . . . . . 7 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ≠ 0)
151149, 150dividd 11402 . . . . . 6 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁𝐾) / (𝑁𝐾)) = 1)
152 1z 12000 . . . . . 6 1 ∈ ℤ
153151, 152syl6eqel 2918 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁𝐾) / (𝑁𝐾)) ∈ ℤ)
15496nnred 11641 . . . . . 6 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℝ)
155 mod0 13232 . . . . . 6 (((𝑁𝐾) ∈ ℝ ∧ (𝑁𝐾) ∈ ℝ+) → (((𝑁𝐾) mod (𝑁𝐾)) = 0 ↔ ((𝑁𝐾) / (𝑁𝐾)) ∈ ℤ))
156154, 127, 155syl2anc 584 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (((𝑁𝐾) mod (𝑁𝐾)) = 0 ↔ ((𝑁𝐾) / (𝑁𝐾)) ∈ ℤ))
157153, 156mpbird 258 . . . 4 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁𝐾) mod (𝑁𝐾)) = 0)
158148, 157eqtrd 2853 . . 3 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝐾) = 0)
15999, 116, 131, 140, 141, 142, 158seqz 13406 . 2 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)) = 0)
16078, 89, 1593eqtr3d 2861 1 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑅 mod (𝑁𝐾)) = 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  {crab 3139  Vcvv 3492  cdif 3930  {csn 4557  cmpt 5137  wf 6344  cfv 6348  (class class class)co 7145  cmpo 7147  infcinf 8893  cc 10523  cr 10524  0cc0 10525  1c1 10526   · cmul 10530   < clt 10663   / cdiv 11285  cn 11626  0cn0 11885  cz 11969  cuz 12231  cq 12336  +crp 12377  ...cfz 12880   mod cmo 13225  seqcseq 13357  0𝑝c0p 24197  Polycply 24701  coeffccoe 24703  degcdgr 24704
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603  ax-addf 10604
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-oadd 8095  df-er 8278  df-map 8397  df-pm 8398  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-sup 8894  df-inf 8895  df-oi 8962  df-card 9356  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-q 12337  df-rp 12378  df-fz 12881  df-fzo 13022  df-fl 13150  df-mod 13226  df-seq 13358  df-exp 13418  df-hash 13679  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583  df-clim 14833  df-rlim 14834  df-sum 15031  df-0p 24198  df-ply 24705  df-coe 24707  df-dgr 24708
This theorem is referenced by:  elqaalem3  24837
  Copyright terms: Public domain W3C validator