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

Theorem elqaalem2 24366
Description: Lemma for elqaa 24368. (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 12640 . . 3 (𝐾 ∈ (0...(deg‘𝐹)) → 𝐾 ∈ ℕ0)
2 elqaa.6 . . . . 5 𝑅 = (seq0( · , 𝑁)‘(deg‘𝐹))
32fveq2i 6378 . . . 4 ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(seq0( · , 𝑁)‘(deg‘𝐹)))
4 nnmulcl 11299 . . . . . 6 ((𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑖 · 𝑗) ∈ ℕ)
54adantl 473 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 · 𝑗) ∈ ℕ)
6 elfznn0 12640 . . . . . 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 24365 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ0) → ((𝑁𝑖) ∈ ℕ ∧ ((𝐵𝑖) · (𝑁𝑖)) ∈ ℤ))
1312simpld 488 . . . . . . 7 ((𝜑𝑖 ∈ ℕ0) → (𝑁𝑖) ∈ ℕ)
1413adantlr 706 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → (𝑁𝑖) ∈ ℕ)
156, 14sylan2 586 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → (𝑁𝑖) ∈ ℕ)
16 eldifi 3894 . . . . . . . 8 (𝐹 ∈ ((Poly‘ℚ) ∖ {0𝑝}) → 𝐹 ∈ (Poly‘ℚ))
17 dgrcl 24280 . . . . . . . 8 (𝐹 ∈ (Poly‘ℚ) → (deg‘𝐹) ∈ ℕ0)
188, 16, 173syl 18 . . . . . . 7 (𝜑 → (deg‘𝐹) ∈ ℕ0)
19 nn0uz 11922 . . . . . . 7 0 = (ℤ‘0)
2018, 19syl6eleq 2854 . . . . . 6 (𝜑 → (deg‘𝐹) ∈ (ℤ‘0))
2120adantr 472 . . . . 5 ((𝜑𝐾 ∈ ℕ0) → (deg‘𝐹) ∈ (ℤ‘0))
22 nnz 11646 . . . . . . . . . 10 (𝑖 ∈ ℕ → 𝑖 ∈ ℤ)
2322ad2antrl 719 . . . . . . . . 9 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℤ)
247, 8, 9, 10, 11, 2elqaalem1 24365 . . . . . . . . . . 11 ((𝜑𝐾 ∈ ℕ0) → ((𝑁𝐾) ∈ ℕ ∧ ((𝐵𝐾) · (𝑁𝐾)) ∈ ℤ))
2524simpld 488 . . . . . . . . . 10 ((𝜑𝐾 ∈ ℕ0) → (𝑁𝐾) ∈ ℕ)
2625adantr 472 . . . . . . . . 9 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑁𝐾) ∈ ℕ)
2723, 26zmodcld 12899 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 mod (𝑁𝐾)) ∈ ℕ0)
2827nn0zd 11727 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 mod (𝑁𝐾)) ∈ ℤ)
29 nnz 11646 . . . . . . . . . 10 (𝑗 ∈ ℕ → 𝑗 ∈ ℤ)
3029ad2antll 720 . . . . . . . . 9 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℤ)
3130, 26zmodcld 12899 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑗 mod (𝑁𝐾)) ∈ ℕ0)
3231nn0zd 11727 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑗 mod (𝑁𝐾)) ∈ ℤ)
3326nnrpd 12068 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑁𝐾) ∈ ℝ+)
34 nnre 11282 . . . . . . . . 9 (𝑖 ∈ ℕ → 𝑖 ∈ ℝ)
3534ad2antrl 719 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℝ)
36 modabs2 12912 . . . . . . . 8 ((𝑖 ∈ ℝ ∧ (𝑁𝐾) ∈ ℝ+) → ((𝑖 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑖 mod (𝑁𝐾)))
3735, 33, 36syl2anc 579 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑖 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑖 mod (𝑁𝐾)))
38 nnre 11282 . . . . . . . . 9 (𝑗 ∈ ℕ → 𝑗 ∈ ℝ)
3938ad2antll 720 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℝ)
40 modabs2 12912 . . . . . . . 8 ((𝑗 ∈ ℝ ∧ (𝑁𝐾) ∈ ℝ+) → ((𝑗 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑗 mod (𝑁𝐾)))
4139, 33, 40syl2anc 579 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑗 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑗 mod (𝑁𝐾)))
4228, 23, 32, 30, 33, 37, 41modmul12d 12932 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
43 oveq1 6849 . . . . . . . . . 10 (𝑘 = 𝑖 → (𝑘 mod (𝑁𝐾)) = (𝑖 mod (𝑁𝐾)))
44 eqid 2765 . . . . . . . . . 10 (𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾))) = (𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))
45 ovex 6874 . . . . . . . . . 10 (𝑖 mod (𝑁𝐾)) ∈ V
4643, 44, 45fvmpt 6471 . . . . . . . . 9 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖) = (𝑖 mod (𝑁𝐾)))
4746ad2antrl 719 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖) = (𝑖 mod (𝑁𝐾)))
48 oveq1 6849 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝑘 mod (𝑁𝐾)) = (𝑗 mod (𝑁𝐾)))
49 ovex 6874 . . . . . . . . . 10 (𝑗 mod (𝑁𝐾)) ∈ V
5048, 44, 49fvmpt 6471 . . . . . . . . 9 (𝑗 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗) = (𝑗 mod (𝑁𝐾)))
5150ad2antll 720 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗) = (𝑗 mod (𝑁𝐾)))
5247, 51oveq12d 6860 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗)) = ((𝑖 mod (𝑁𝐾))𝑃(𝑗 mod (𝑁𝐾))))
53 oveq12 6851 . . . . . . . . . 10 ((𝑥 = (𝑖 mod (𝑁𝐾)) ∧ 𝑦 = (𝑗 mod (𝑁𝐾))) → (𝑥 · 𝑦) = ((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))))
5453oveq1d 6857 . . . . . . . . 9 ((𝑥 = (𝑖 mod (𝑁𝐾)) ∧ 𝑦 = (𝑗 mod (𝑁𝐾))) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)))
55 elqaa.7 . . . . . . . . 9 𝑃 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 · 𝑦) mod (𝑁𝐾)))
56 ovex 6874 . . . . . . . . 9 (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)) ∈ V
5754, 55, 56ovmpt2a 6989 . . . . . . . 8 (((𝑖 mod (𝑁𝐾)) ∈ V ∧ (𝑗 mod (𝑁𝐾)) ∈ V) → ((𝑖 mod (𝑁𝐾))𝑃(𝑗 mod (𝑁𝐾))) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)))
5845, 49, 57mp2an 683 . . . . . . 7 ((𝑖 mod (𝑁𝐾))𝑃(𝑗 mod (𝑁𝐾))) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾))
5952, 58syl6eq 2815 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗)) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)))
60 oveq1 6849 . . . . . . . 8 (𝑘 = (𝑖 · 𝑗) → (𝑘 mod (𝑁𝐾)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
61 ovex 6874 . . . . . . . 8 ((𝑖 · 𝑗) mod (𝑁𝐾)) ∈ V
6260, 44, 61fvmpt 6471 . . . . . . 7 ((𝑖 · 𝑗) ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑖 · 𝑗)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
635, 62syl 17 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑖 · 𝑗)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
6442, 59, 633eqtr4rd 2810 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑖 · 𝑗)) = (((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗)))
65 oveq1 6849 . . . . . . . . 9 (𝑘 = (𝑁𝑖) → (𝑘 mod (𝑁𝐾)) = ((𝑁𝑖) mod (𝑁𝐾)))
66 ovex 6874 . . . . . . . . 9 ((𝑁𝑖) mod (𝑁𝐾)) ∈ V
6765, 44, 66fvmpt 6471 . . . . . . . 8 ((𝑁𝑖) ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑁𝑖) mod (𝑁𝐾)))
6814, 67syl 17 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑁𝑖) mod (𝑁𝐾)))
69 fveq2 6375 . . . . . . . . . 10 (𝑘 = 𝑖 → (𝑁𝑘) = (𝑁𝑖))
7069oveq1d 6857 . . . . . . . . 9 (𝑘 = 𝑖 → ((𝑁𝑘) mod (𝑁𝐾)) = ((𝑁𝑖) mod (𝑁𝐾)))
71 eqid 2765 . . . . . . . . 9 (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))) = (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))
7270, 71, 66fvmpt 6471 . . . . . . . 8 (𝑖 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) = ((𝑁𝑖) mod (𝑁𝐾)))
7372adantl 473 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) = ((𝑁𝑖) mod (𝑁𝐾)))
7468, 73eqtr4d 2802 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖))
756, 74sylan2 586 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖))
765, 15, 21, 64, 75seqhomo 13055 . . . 4 ((𝜑𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(seq0( · , 𝑁)‘(deg‘𝐹))) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)))
773, 76syl5eq 2811 . . 3 ((𝜑𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)))
781, 77sylan2 586 . 2 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)))
79 0zd 11636 . . . . . . . 8 (𝜑 → 0 ∈ ℤ)
804adantl 473 . . . . . . . 8 ((𝜑 ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 · 𝑗) ∈ ℕ)
8119, 79, 13, 80seqf 13029 . . . . . . 7 (𝜑 → seq0( · , 𝑁):ℕ0⟶ℕ)
8281, 18ffvelrnd 6550 . . . . . 6 (𝜑 → (seq0( · , 𝑁)‘(deg‘𝐹)) ∈ ℕ)
832, 82syl5eqel 2848 . . . . 5 (𝜑𝑅 ∈ ℕ)
8483adantr 472 . . . 4 ((𝜑𝐾 ∈ ℕ0) → 𝑅 ∈ ℕ)
85 oveq1 6849 . . . . 5 (𝑘 = 𝑅 → (𝑘 mod (𝑁𝐾)) = (𝑅 mod (𝑁𝐾)))
86 ovex 6874 . . . . 5 (𝑅 mod (𝑁𝐾)) ∈ V
8785, 44, 86fvmpt 6471 . . . 4 (𝑅 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (𝑅 mod (𝑁𝐾)))
8884, 87syl 17 . . 3 ((𝜑𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (𝑅 mod (𝑁𝐾)))
891, 88sylan2 586 . 2 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (𝑅 mod (𝑁𝐾)))
90 vex 3353 . . . . 5 𝑖 ∈ V
91 vex 3353 . . . . 5 𝑗 ∈ V
92 oveq12 6851 . . . . . . 7 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑥 · 𝑦) = (𝑖 · 𝑗))
9392oveq1d 6857 . . . . . 6 ((𝑥 = 𝑖𝑦 = 𝑗) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
9493, 55, 61ovmpt2a 6989 . . . . 5 ((𝑖 ∈ V ∧ 𝑗 ∈ V) → (𝑖𝑃𝑗) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
9590, 91, 94mp2an 683 . . . 4 (𝑖𝑃𝑗) = ((𝑖 · 𝑗) mod (𝑁𝐾))
96 nn0mulcl 11576 . . . . . 6 ((𝑖 ∈ ℕ0𝑗 ∈ ℕ0) → (𝑖 · 𝑗) ∈ ℕ0)
9796nn0zd 11727 . . . . 5 ((𝑖 ∈ ℕ0𝑗 ∈ ℕ0) → (𝑖 · 𝑗) ∈ ℤ)
981, 25sylan2 586 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℕ)
99 zmodcl 12898 . . . . 5 (((𝑖 · 𝑗) ∈ ℤ ∧ (𝑁𝐾) ∈ ℕ) → ((𝑖 · 𝑗) mod (𝑁𝐾)) ∈ ℕ0)
10097, 98, 99syl2anr 590 . . . 4 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ (𝑖 ∈ ℕ0𝑗 ∈ ℕ0)) → ((𝑖 · 𝑗) mod (𝑁𝐾)) ∈ ℕ0)
10195, 100syl5eqel 2848 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ (𝑖 ∈ ℕ0𝑗 ∈ ℕ0)) → (𝑖𝑃𝑗) ∈ ℕ0)
102 fveq2 6375 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑚 → (𝐵𝑘) = (𝐵𝑚))
103102oveq1d 6857 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑚 → ((𝐵𝑘) · 𝑛) = ((𝐵𝑚) · 𝑛))
104103eleq1d 2829 . . . . . . . . . . . . . . 15 (𝑘 = 𝑚 → (((𝐵𝑘) · 𝑛) ∈ ℤ ↔ ((𝐵𝑚) · 𝑛) ∈ ℤ))
105104rabbidv 3338 . . . . . . . . . . . . . 14 (𝑘 = 𝑚 → {𝑛 ∈ ℕ ∣ ((𝐵𝑘) · 𝑛) ∈ ℤ} = {𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ})
106105infeq1d 8590 . . . . . . . . . . . . 13 (𝑘 = 𝑚 → inf({𝑛 ∈ ℕ ∣ ((𝐵𝑘) · 𝑛) ∈ ℤ}, ℝ, < ) = inf({𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ}, ℝ, < ))
107106cbvmptv 4909 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵𝑘) · 𝑛) ∈ ℤ}, ℝ, < )) = (𝑚 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ}, ℝ, < ))
10811, 107eqtri 2787 . . . . . . . . . . 11 𝑁 = (𝑚 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ}, ℝ, < ))
1097, 8, 9, 10, 108, 2elqaalem1 24365 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((𝑁𝑘) ∈ ℕ ∧ ((𝐵𝑘) · (𝑁𝑘)) ∈ ℤ))
110109simpld 488 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (𝑁𝑘) ∈ ℕ)
111110adantlr 706 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑁𝑘) ∈ ℕ)
112111nnzd 11728 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑁𝑘) ∈ ℤ)
11325adantr 472 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑁𝐾) ∈ ℕ)
114112, 113zmodcld 12899 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → ((𝑁𝑘) mod (𝑁𝐾)) ∈ ℕ0)
115114fmpttd 6575 . . . . 5 ((𝜑𝐾 ∈ ℕ0) → (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))):ℕ0⟶ℕ0)
1161, 115sylan2 586 . . . 4 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))):ℕ0⟶ℕ0)
117 ffvelrn 6547 . . . 4 (((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))):ℕ0⟶ℕ0𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) ∈ ℕ0)
118116, 6, 117syl2an 589 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) ∈ ℕ0)
119 c0ex 10287 . . . . 5 0 ∈ V
120 oveq12 6851 . . . . . . 7 ((𝑥 = 0 ∧ 𝑦 = 𝑖) → (𝑥 · 𝑦) = (0 · 𝑖))
121120oveq1d 6857 . . . . . 6 ((𝑥 = 0 ∧ 𝑦 = 𝑖) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = ((0 · 𝑖) mod (𝑁𝐾)))
122 ovex 6874 . . . . . 6 ((0 · 𝑖) mod (𝑁𝐾)) ∈ V
123121, 55, 122ovmpt2a 6989 . . . . 5 ((0 ∈ V ∧ 𝑖 ∈ V) → (0𝑃𝑖) = ((0 · 𝑖) mod (𝑁𝐾)))
124119, 90, 123mp2an 683 . . . 4 (0𝑃𝑖) = ((0 · 𝑖) mod (𝑁𝐾))
125 nn0cn 11549 . . . . . . 7 (𝑖 ∈ ℕ0𝑖 ∈ ℂ)
126125mul02d 10488 . . . . . 6 (𝑖 ∈ ℕ0 → (0 · 𝑖) = 0)
127126oveq1d 6857 . . . . 5 (𝑖 ∈ ℕ0 → ((0 · 𝑖) mod (𝑁𝐾)) = (0 mod (𝑁𝐾)))
12898nnrpd 12068 . . . . . 6 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℝ+)
129 0mod 12909 . . . . . 6 ((𝑁𝐾) ∈ ℝ+ → (0 mod (𝑁𝐾)) = 0)
130128, 129syl 17 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (0 mod (𝑁𝐾)) = 0)
131127, 130sylan9eqr 2821 . . . 4 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → ((0 · 𝑖) mod (𝑁𝐾)) = 0)
132124, 131syl5eq 2811 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → (0𝑃𝑖) = 0)
133 oveq12 6851 . . . . . . 7 ((𝑥 = 𝑖𝑦 = 0) → (𝑥 · 𝑦) = (𝑖 · 0))
134133oveq1d 6857 . . . . . 6 ((𝑥 = 𝑖𝑦 = 0) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = ((𝑖 · 0) mod (𝑁𝐾)))
135 ovex 6874 . . . . . 6 ((𝑖 · 0) mod (𝑁𝐾)) ∈ V
136134, 55, 135ovmpt2a 6989 . . . . 5 ((𝑖 ∈ V ∧ 0 ∈ V) → (𝑖𝑃0) = ((𝑖 · 0) mod (𝑁𝐾)))
13790, 119, 136mp2an 683 . . . 4 (𝑖𝑃0) = ((𝑖 · 0) mod (𝑁𝐾))
138125mul01d 10489 . . . . . 6 (𝑖 ∈ ℕ0 → (𝑖 · 0) = 0)
139138oveq1d 6857 . . . . 5 (𝑖 ∈ ℕ0 → ((𝑖 · 0) mod (𝑁𝐾)) = (0 mod (𝑁𝐾)))
140139, 130sylan9eqr 2821 . . . 4 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → ((𝑖 · 0) mod (𝑁𝐾)) = 0)
141137, 140syl5eq 2811 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → (𝑖𝑃0) = 0)
142 simpr 477 . . 3 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → 𝐾 ∈ (0...(deg‘𝐹)))
14318adantr 472 . . 3 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (deg‘𝐹) ∈ ℕ0)
1441adantl 473 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → 𝐾 ∈ ℕ0)
145 fveq2 6375 . . . . . . 7 (𝑘 = 𝐾 → (𝑁𝑘) = (𝑁𝐾))
146145oveq1d 6857 . . . . . 6 (𝑘 = 𝐾 → ((𝑁𝑘) mod (𝑁𝐾)) = ((𝑁𝐾) mod (𝑁𝐾)))
147 ovex 6874 . . . . . 6 ((𝑁𝐾) mod (𝑁𝐾)) ∈ V
148146, 71, 147fvmpt 6471 . . . . 5 (𝐾 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝐾) = ((𝑁𝐾) mod (𝑁𝐾)))
149144, 148syl 17 . . . 4 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝐾) = ((𝑁𝐾) mod (𝑁𝐾)))
15098nncnd 11292 . . . . . . 7 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℂ)
15198nnne0d 11322 . . . . . . 7 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ≠ 0)
152150, 151dividd 11053 . . . . . 6 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁𝐾) / (𝑁𝐾)) = 1)
153 1z 11654 . . . . . 6 1 ∈ ℤ
154152, 153syl6eqel 2852 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁𝐾) / (𝑁𝐾)) ∈ ℤ)
15598nnred 11291 . . . . . 6 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℝ)
156 mod0 12883 . . . . . 6 (((𝑁𝐾) ∈ ℝ ∧ (𝑁𝐾) ∈ ℝ+) → (((𝑁𝐾) mod (𝑁𝐾)) = 0 ↔ ((𝑁𝐾) / (𝑁𝐾)) ∈ ℤ))
157155, 128, 156syl2anc 579 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (((𝑁𝐾) mod (𝑁𝐾)) = 0 ↔ ((𝑁𝐾) / (𝑁𝐾)) ∈ ℤ))
158154, 157mpbird 248 . . . 4 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁𝐾) mod (𝑁𝐾)) = 0)
159149, 158eqtrd 2799 . . 3 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝐾) = 0)
160101, 118, 132, 141, 142, 143, 159seqz 13056 . 2 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)) = 0)
16178, 89, 1603eqtr3d 2807 1 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑅 mod (𝑁𝐾)) = 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  {crab 3059  Vcvv 3350  cdif 3729  {csn 4334  cmpt 4888  wf 6064  cfv 6068  (class class class)co 6842  cmpt2 6844  infcinf 8554  cc 10187  cr 10188  0cc0 10189  1c1 10190   · cmul 10194   < clt 10328   / cdiv 10938  cn 11274  0cn0 11538  cz 11624  cuz 11886  cq 11989  +crp 12028  ...cfz 12533   mod cmo 12876  seqcseq 13008  0𝑝c0p 23727  Polycply 24231  coeffccoe 24233  degcdgr 24234
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267  ax-addf 10268
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-z 11625  df-uz 11887  df-q 11990  df-rp 12029  df-fz 12534  df-fzo 12674  df-fl 12801  df-mod 12877  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14126  df-re 14127  df-im 14128  df-sqrt 14262  df-abs 14263  df-clim 14506  df-rlim 14507  df-sum 14704  df-0p 23728  df-ply 24235  df-coe 24237  df-dgr 24238
This theorem is referenced by:  elqaalem3  24367
  Copyright terms: Public domain W3C validator