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

Theorem elqaalem2 25762
Description: Lemma for elqaa 25764. (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 13576 . . 3 (𝐾 ∈ (0...(deg‘𝐹)) → 𝐾 ∈ ℕ0)
2 elqaa.6 . . . . 5 𝑅 = (seq0( · , 𝑁)‘(deg‘𝐹))
32fveq2i 6881 . . . 4 ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(seq0( · , 𝑁)‘(deg‘𝐹)))
4 nnmulcl 12218 . . . . . 6 ((𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑖 · 𝑗) ∈ ℕ)
54adantl 482 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 · 𝑗) ∈ ℕ)
6 elfznn0 13576 . . . . . 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 25761 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ0) → ((𝑁𝑖) ∈ ℕ ∧ ((𝐵𝑖) · (𝑁𝑖)) ∈ ℤ))
1312simpld 495 . . . . . . 7 ((𝜑𝑖 ∈ ℕ0) → (𝑁𝑖) ∈ ℕ)
1413adantlr 713 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → (𝑁𝑖) ∈ ℕ)
156, 14sylan2 593 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → (𝑁𝑖) ∈ ℕ)
16 eldifi 4122 . . . . . . . 8 (𝐹 ∈ ((Poly‘ℚ) ∖ {0𝑝}) → 𝐹 ∈ (Poly‘ℚ))
17 dgrcl 25676 . . . . . . . 8 (𝐹 ∈ (Poly‘ℚ) → (deg‘𝐹) ∈ ℕ0)
188, 16, 173syl 18 . . . . . . 7 (𝜑 → (deg‘𝐹) ∈ ℕ0)
19 nn0uz 12846 . . . . . . 7 0 = (ℤ‘0)
2018, 19eleqtrdi 2842 . . . . . 6 (𝜑 → (deg‘𝐹) ∈ (ℤ‘0))
2120adantr 481 . . . . 5 ((𝜑𝐾 ∈ ℕ0) → (deg‘𝐹) ∈ (ℤ‘0))
22 nnz 12561 . . . . . . . . . 10 (𝑖 ∈ ℕ → 𝑖 ∈ ℤ)
2322ad2antrl 726 . . . . . . . . 9 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℤ)
247, 8, 9, 10, 11, 2elqaalem1 25761 . . . . . . . . . . 11 ((𝜑𝐾 ∈ ℕ0) → ((𝑁𝐾) ∈ ℕ ∧ ((𝐵𝐾) · (𝑁𝐾)) ∈ ℤ))
2524simpld 495 . . . . . . . . . 10 ((𝜑𝐾 ∈ ℕ0) → (𝑁𝐾) ∈ ℕ)
2625adantr 481 . . . . . . . . 9 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑁𝐾) ∈ ℕ)
2723, 26zmodcld 13839 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 mod (𝑁𝐾)) ∈ ℕ0)
2827nn0zd 12566 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 mod (𝑁𝐾)) ∈ ℤ)
29 nnz 12561 . . . . . . . . . 10 (𝑗 ∈ ℕ → 𝑗 ∈ ℤ)
3029ad2antll 727 . . . . . . . . 9 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℤ)
3130, 26zmodcld 13839 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑗 mod (𝑁𝐾)) ∈ ℕ0)
3231nn0zd 12566 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑗 mod (𝑁𝐾)) ∈ ℤ)
3326nnrpd 12996 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑁𝐾) ∈ ℝ+)
34 nnre 12201 . . . . . . . . 9 (𝑖 ∈ ℕ → 𝑖 ∈ ℝ)
3534ad2antrl 726 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℝ)
36 modabs2 13852 . . . . . . . 8 ((𝑖 ∈ ℝ ∧ (𝑁𝐾) ∈ ℝ+) → ((𝑖 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑖 mod (𝑁𝐾)))
3735, 33, 36syl2anc 584 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑖 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑖 mod (𝑁𝐾)))
38 nnre 12201 . . . . . . . . 9 (𝑗 ∈ ℕ → 𝑗 ∈ ℝ)
3938ad2antll 727 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℝ)
40 modabs2 13852 . . . . . . . 8 ((𝑗 ∈ ℝ ∧ (𝑁𝐾) ∈ ℝ+) → ((𝑗 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑗 mod (𝑁𝐾)))
4139, 33, 40syl2anc 584 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑗 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑗 mod (𝑁𝐾)))
4228, 23, 32, 30, 33, 37, 41modmul12d 13872 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
43 oveq1 7400 . . . . . . . . . 10 (𝑘 = 𝑖 → (𝑘 mod (𝑁𝐾)) = (𝑖 mod (𝑁𝐾)))
44 eqid 2731 . . . . . . . . . 10 (𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾))) = (𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))
45 ovex 7426 . . . . . . . . . 10 (𝑖 mod (𝑁𝐾)) ∈ V
4643, 44, 45fvmpt 6984 . . . . . . . . 9 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖) = (𝑖 mod (𝑁𝐾)))
4746ad2antrl 726 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖) = (𝑖 mod (𝑁𝐾)))
48 oveq1 7400 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝑘 mod (𝑁𝐾)) = (𝑗 mod (𝑁𝐾)))
49 ovex 7426 . . . . . . . . . 10 (𝑗 mod (𝑁𝐾)) ∈ V
5048, 44, 49fvmpt 6984 . . . . . . . . 9 (𝑗 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗) = (𝑗 mod (𝑁𝐾)))
5150ad2antll 727 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗) = (𝑗 mod (𝑁𝐾)))
5247, 51oveq12d 7411 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗)) = ((𝑖 mod (𝑁𝐾))𝑃(𝑗 mod (𝑁𝐾))))
53 oveq12 7402 . . . . . . . . . 10 ((𝑥 = (𝑖 mod (𝑁𝐾)) ∧ 𝑦 = (𝑗 mod (𝑁𝐾))) → (𝑥 · 𝑦) = ((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))))
5453oveq1d 7408 . . . . . . . . 9 ((𝑥 = (𝑖 mod (𝑁𝐾)) ∧ 𝑦 = (𝑗 mod (𝑁𝐾))) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)))
55 elqaa.7 . . . . . . . . 9 𝑃 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 · 𝑦) mod (𝑁𝐾)))
56 ovex 7426 . . . . . . . . 9 (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)) ∈ V
5754, 55, 56ovmpoa 7546 . . . . . . . 8 (((𝑖 mod (𝑁𝐾)) ∈ V ∧ (𝑗 mod (𝑁𝐾)) ∈ V) → ((𝑖 mod (𝑁𝐾))𝑃(𝑗 mod (𝑁𝐾))) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)))
5845, 49, 57mp2an 690 . . . . . . 7 ((𝑖 mod (𝑁𝐾))𝑃(𝑗 mod (𝑁𝐾))) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾))
5952, 58eqtrdi 2787 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗)) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)))
60 oveq1 7400 . . . . . . . 8 (𝑘 = (𝑖 · 𝑗) → (𝑘 mod (𝑁𝐾)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
61 ovex 7426 . . . . . . . 8 ((𝑖 · 𝑗) mod (𝑁𝐾)) ∈ V
6260, 44, 61fvmpt 6984 . . . . . . 7 ((𝑖 · 𝑗) ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑖 · 𝑗)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
635, 62syl 17 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑖 · 𝑗)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
6442, 59, 633eqtr4rd 2782 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑖 · 𝑗)) = (((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗)))
65 oveq1 7400 . . . . . . . . 9 (𝑘 = (𝑁𝑖) → (𝑘 mod (𝑁𝐾)) = ((𝑁𝑖) mod (𝑁𝐾)))
66 ovex 7426 . . . . . . . . 9 ((𝑁𝑖) mod (𝑁𝐾)) ∈ V
6765, 44, 66fvmpt 6984 . . . . . . . 8 ((𝑁𝑖) ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑁𝑖) mod (𝑁𝐾)))
6814, 67syl 17 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑁𝑖) mod (𝑁𝐾)))
69 fveq2 6878 . . . . . . . . . 10 (𝑘 = 𝑖 → (𝑁𝑘) = (𝑁𝑖))
7069oveq1d 7408 . . . . . . . . 9 (𝑘 = 𝑖 → ((𝑁𝑘) mod (𝑁𝐾)) = ((𝑁𝑖) mod (𝑁𝐾)))
71 eqid 2731 . . . . . . . . 9 (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))) = (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))
7270, 71, 66fvmpt 6984 . . . . . . . 8 (𝑖 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) = ((𝑁𝑖) mod (𝑁𝐾)))
7372adantl 482 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) = ((𝑁𝑖) mod (𝑁𝐾)))
7468, 73eqtr4d 2774 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖))
756, 74sylan2 593 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖))
765, 15, 21, 64, 75seqhomo 13997 . . . 4 ((𝜑𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(seq0( · , 𝑁)‘(deg‘𝐹))) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)))
773, 76eqtrid 2783 . . 3 ((𝜑𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)))
781, 77sylan2 593 . 2 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)))
79 0zd 12552 . . . . . . . 8 (𝜑 → 0 ∈ ℤ)
804adantl 482 . . . . . . . 8 ((𝜑 ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 · 𝑗) ∈ ℕ)
8119, 79, 13, 80seqf 13971 . . . . . . 7 (𝜑 → seq0( · , 𝑁):ℕ0⟶ℕ)
8281, 18ffvelcdmd 7072 . . . . . 6 (𝜑 → (seq0( · , 𝑁)‘(deg‘𝐹)) ∈ ℕ)
832, 82eqeltrid 2836 . . . . 5 (𝜑𝑅 ∈ ℕ)
8483adantr 481 . . . 4 ((𝜑𝐾 ∈ ℕ0) → 𝑅 ∈ ℕ)
85 oveq1 7400 . . . . 5 (𝑘 = 𝑅 → (𝑘 mod (𝑁𝐾)) = (𝑅 mod (𝑁𝐾)))
86 ovex 7426 . . . . 5 (𝑅 mod (𝑁𝐾)) ∈ V
8785, 44, 86fvmpt 6984 . . . 4 (𝑅 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (𝑅 mod (𝑁𝐾)))
8884, 87syl 17 . . 3 ((𝜑𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (𝑅 mod (𝑁𝐾)))
891, 88sylan2 593 . 2 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (𝑅 mod (𝑁𝐾)))
90 oveq12 7402 . . . . . . 7 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑥 · 𝑦) = (𝑖 · 𝑗))
9190oveq1d 7408 . . . . . 6 ((𝑥 = 𝑖𝑦 = 𝑗) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
9291, 55, 61ovmpoa 7546 . . . . 5 ((𝑖 ∈ V ∧ 𝑗 ∈ V) → (𝑖𝑃𝑗) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
9392el2v 3481 . . . 4 (𝑖𝑃𝑗) = ((𝑖 · 𝑗) mod (𝑁𝐾))
94 nn0mulcl 12490 . . . . . 6 ((𝑖 ∈ ℕ0𝑗 ∈ ℕ0) → (𝑖 · 𝑗) ∈ ℕ0)
9594nn0zd 12566 . . . . 5 ((𝑖 ∈ ℕ0𝑗 ∈ ℕ0) → (𝑖 · 𝑗) ∈ ℤ)
961, 25sylan2 593 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℕ)
97 zmodcl 13838 . . . . 5 (((𝑖 · 𝑗) ∈ ℤ ∧ (𝑁𝐾) ∈ ℕ) → ((𝑖 · 𝑗) mod (𝑁𝐾)) ∈ ℕ0)
9895, 96, 97syl2anr 597 . . . 4 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ (𝑖 ∈ ℕ0𝑗 ∈ ℕ0)) → ((𝑖 · 𝑗) mod (𝑁𝐾)) ∈ ℕ0)
9993, 98eqeltrid 2836 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ (𝑖 ∈ ℕ0𝑗 ∈ ℕ0)) → (𝑖𝑃𝑗) ∈ ℕ0)
100 fveq2 6878 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑚 → (𝐵𝑘) = (𝐵𝑚))
101100oveq1d 7408 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑚 → ((𝐵𝑘) · 𝑛) = ((𝐵𝑚) · 𝑛))
102101eleq1d 2817 . . . . . . . . . . . . . . 15 (𝑘 = 𝑚 → (((𝐵𝑘) · 𝑛) ∈ ℤ ↔ ((𝐵𝑚) · 𝑛) ∈ ℤ))
103102rabbidv 3439 . . . . . . . . . . . . . 14 (𝑘 = 𝑚 → {𝑛 ∈ ℕ ∣ ((𝐵𝑘) · 𝑛) ∈ ℤ} = {𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ})
104103infeq1d 9454 . . . . . . . . . . . . 13 (𝑘 = 𝑚 → inf({𝑛 ∈ ℕ ∣ ((𝐵𝑘) · 𝑛) ∈ ℤ}, ℝ, < ) = inf({𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ}, ℝ, < ))
105104cbvmptv 5254 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵𝑘) · 𝑛) ∈ ℤ}, ℝ, < )) = (𝑚 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ}, ℝ, < ))
10611, 105eqtri 2759 . . . . . . . . . . 11 𝑁 = (𝑚 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ}, ℝ, < ))
1077, 8, 9, 10, 106, 2elqaalem1 25761 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((𝑁𝑘) ∈ ℕ ∧ ((𝐵𝑘) · (𝑁𝑘)) ∈ ℤ))
108107simpld 495 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (𝑁𝑘) ∈ ℕ)
109108adantlr 713 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑁𝑘) ∈ ℕ)
110109nnzd 12567 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑁𝑘) ∈ ℤ)
11125adantr 481 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑁𝐾) ∈ ℕ)
112110, 111zmodcld 13839 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → ((𝑁𝑘) mod (𝑁𝐾)) ∈ ℕ0)
113112fmpttd 7099 . . . . 5 ((𝜑𝐾 ∈ ℕ0) → (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))):ℕ0⟶ℕ0)
1141, 113sylan2 593 . . . 4 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))):ℕ0⟶ℕ0)
115 ffvelcdm 7068 . . . 4 (((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))):ℕ0⟶ℕ0𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) ∈ ℕ0)
116114, 6, 115syl2an 596 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) ∈ ℕ0)
117 c0ex 11190 . . . . 5 0 ∈ V
118 vex 3477 . . . . 5 𝑖 ∈ V
119 oveq12 7402 . . . . . . 7 ((𝑥 = 0 ∧ 𝑦 = 𝑖) → (𝑥 · 𝑦) = (0 · 𝑖))
120119oveq1d 7408 . . . . . 6 ((𝑥 = 0 ∧ 𝑦 = 𝑖) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = ((0 · 𝑖) mod (𝑁𝐾)))
121 ovex 7426 . . . . . 6 ((0 · 𝑖) mod (𝑁𝐾)) ∈ V
122120, 55, 121ovmpoa 7546 . . . . 5 ((0 ∈ V ∧ 𝑖 ∈ V) → (0𝑃𝑖) = ((0 · 𝑖) mod (𝑁𝐾)))
123117, 118, 122mp2an 690 . . . 4 (0𝑃𝑖) = ((0 · 𝑖) mod (𝑁𝐾))
124 nn0cn 12464 . . . . . . 7 (𝑖 ∈ ℕ0𝑖 ∈ ℂ)
125124mul02d 11394 . . . . . 6 (𝑖 ∈ ℕ0 → (0 · 𝑖) = 0)
126125oveq1d 7408 . . . . 5 (𝑖 ∈ ℕ0 → ((0 · 𝑖) mod (𝑁𝐾)) = (0 mod (𝑁𝐾)))
12796nnrpd 12996 . . . . . 6 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℝ+)
128 0mod 13849 . . . . . 6 ((𝑁𝐾) ∈ ℝ+ → (0 mod (𝑁𝐾)) = 0)
129127, 128syl 17 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (0 mod (𝑁𝐾)) = 0)
130126, 129sylan9eqr 2793 . . . 4 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → ((0 · 𝑖) mod (𝑁𝐾)) = 0)
131123, 130eqtrid 2783 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → (0𝑃𝑖) = 0)
132 oveq12 7402 . . . . . . 7 ((𝑥 = 𝑖𝑦 = 0) → (𝑥 · 𝑦) = (𝑖 · 0))
133132oveq1d 7408 . . . . . 6 ((𝑥 = 𝑖𝑦 = 0) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = ((𝑖 · 0) mod (𝑁𝐾)))
134 ovex 7426 . . . . . 6 ((𝑖 · 0) mod (𝑁𝐾)) ∈ V
135133, 55, 134ovmpoa 7546 . . . . 5 ((𝑖 ∈ V ∧ 0 ∈ V) → (𝑖𝑃0) = ((𝑖 · 0) mod (𝑁𝐾)))
136118, 117, 135mp2an 690 . . . 4 (𝑖𝑃0) = ((𝑖 · 0) mod (𝑁𝐾))
137124mul01d 11395 . . . . . 6 (𝑖 ∈ ℕ0 → (𝑖 · 0) = 0)
138137oveq1d 7408 . . . . 5 (𝑖 ∈ ℕ0 → ((𝑖 · 0) mod (𝑁𝐾)) = (0 mod (𝑁𝐾)))
139138, 129sylan9eqr 2793 . . . 4 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → ((𝑖 · 0) mod (𝑁𝐾)) = 0)
140136, 139eqtrid 2783 . . 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 6878 . . . . . . 7 (𝑘 = 𝐾 → (𝑁𝑘) = (𝑁𝐾))
145144oveq1d 7408 . . . . . 6 (𝑘 = 𝐾 → ((𝑁𝑘) mod (𝑁𝐾)) = ((𝑁𝐾) mod (𝑁𝐾)))
146 ovex 7426 . . . . . 6 ((𝑁𝐾) mod (𝑁𝐾)) ∈ V
147145, 71, 146fvmpt 6984 . . . . 5 (𝐾 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝐾) = ((𝑁𝐾) mod (𝑁𝐾)))
148143, 147syl 17 . . . 4 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝐾) = ((𝑁𝐾) mod (𝑁𝐾)))
14996nncnd 12210 . . . . . . 7 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℂ)
15096nnne0d 12244 . . . . . . 7 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ≠ 0)
151149, 150dividd 11970 . . . . . 6 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁𝐾) / (𝑁𝐾)) = 1)
152 1z 12574 . . . . . 6 1 ∈ ℤ
153151, 152eqeltrdi 2840 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁𝐾) / (𝑁𝐾)) ∈ ℤ)
15496nnred 12209 . . . . . 6 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℝ)
155 mod0 13823 . . . . . 6 (((𝑁𝐾) ∈ ℝ ∧ (𝑁𝐾) ∈ ℝ+) → (((𝑁𝐾) mod (𝑁𝐾)) = 0 ↔ ((𝑁𝐾) / (𝑁𝐾)) ∈ ℤ))
156154, 127, 155syl2anc 584 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (((𝑁𝐾) mod (𝑁𝐾)) = 0 ↔ ((𝑁𝐾) / (𝑁𝐾)) ∈ ℤ))
157153, 156mpbird 256 . . . 4 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁𝐾) mod (𝑁𝐾)) = 0)
158148, 157eqtrd 2771 . . 3 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝐾) = 0)
15999, 116, 131, 140, 141, 142, 158seqz 13998 . 2 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)) = 0)
16078, 89, 1593eqtr3d 2779 1 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑅 mod (𝑁𝐾)) = 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  {crab 3431  Vcvv 3473  cdif 3941  {csn 4622  cmpt 5224  wf 6528  cfv 6532  (class class class)co 7393  cmpo 7395  infcinf 9418  cc 11090  cr 11091  0cc0 11092  1c1 11093   · cmul 11097   < clt 11230   / cdiv 11853  cn 12194  0cn0 12454  cz 12540  cuz 12804  cq 12914  +crp 12956  ...cfz 13466   mod cmo 13816  seqcseq 13948  0𝑝c0p 25115  Polycply 25627  coeffccoe 25629  degcdgr 25630
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708  ax-inf2 9618  ax-cnex 11148  ax-resscn 11149  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-addrcl 11153  ax-mulcl 11154  ax-mulrcl 11155  ax-mulcom 11156  ax-addass 11157  ax-mulass 11158  ax-distr 11159  ax-i2m1 11160  ax-1ne0 11161  ax-1rid 11162  ax-rnegex 11163  ax-rrecex 11164  ax-cnre 11165  ax-pre-lttri 11166  ax-pre-lttrn 11167  ax-pre-ltadd 11168  ax-pre-mulgt0 11169  ax-pre-sup 11170
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-isom 6541  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-of 7653  df-om 7839  df-1st 7957  df-2nd 7958  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-1o 8448  df-er 8686  df-map 8805  df-pm 8806  df-en 8923  df-dom 8924  df-sdom 8925  df-fin 8926  df-sup 9419  df-inf 9420  df-oi 9487  df-card 9916  df-pnf 11232  df-mnf 11233  df-xr 11234  df-ltxr 11235  df-le 11236  df-sub 11428  df-neg 11429  df-div 11854  df-nn 12195  df-2 12257  df-3 12258  df-n0 12455  df-z 12541  df-uz 12805  df-q 12915  df-rp 12957  df-fz 13467  df-fzo 13610  df-fl 13739  df-mod 13817  df-seq 13949  df-exp 14010  df-hash 14273  df-cj 15028  df-re 15029  df-im 15030  df-sqrt 15164  df-abs 15165  df-clim 15414  df-rlim 15415  df-sum 15615  df-0p 25116  df-ply 25631  df-coe 25633  df-dgr 25634
This theorem is referenced by:  elqaalem3  25763
  Copyright terms: Public domain W3C validator