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

Theorem elqaalem2 24120
Description: Lemma for elqaa 24122. (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 12471 . . 3 (𝐾 ∈ (0...(deg‘𝐹)) → 𝐾 ∈ ℕ0)
2 elqaa.6 . . . . 5 𝑅 = (seq0( · , 𝑁)‘(deg‘𝐹))
32fveq2i 6232 . . . 4 ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(seq0( · , 𝑁)‘(deg‘𝐹)))
4 nnmulcl 11081 . . . . . 6 ((𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑖 · 𝑗) ∈ ℕ)
54adantl 481 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 · 𝑗) ∈ ℕ)
6 elfznn0 12471 . . . . . 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 24119 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ0) → ((𝑁𝑖) ∈ ℕ ∧ ((𝐵𝑖) · (𝑁𝑖)) ∈ ℤ))
1312simpld 474 . . . . . . 7 ((𝜑𝑖 ∈ ℕ0) → (𝑁𝑖) ∈ ℕ)
1413adantlr 751 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → (𝑁𝑖) ∈ ℕ)
156, 14sylan2 490 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → (𝑁𝑖) ∈ ℕ)
16 eldifi 3765 . . . . . . . 8 (𝐹 ∈ ((Poly‘ℚ) ∖ {0𝑝}) → 𝐹 ∈ (Poly‘ℚ))
17 dgrcl 24034 . . . . . . . 8 (𝐹 ∈ (Poly‘ℚ) → (deg‘𝐹) ∈ ℕ0)
188, 16, 173syl 18 . . . . . . 7 (𝜑 → (deg‘𝐹) ∈ ℕ0)
19 nn0uz 11760 . . . . . . 7 0 = (ℤ‘0)
2018, 19syl6eleq 2740 . . . . . 6 (𝜑 → (deg‘𝐹) ∈ (ℤ‘0))
2120adantr 480 . . . . 5 ((𝜑𝐾 ∈ ℕ0) → (deg‘𝐹) ∈ (ℤ‘0))
22 nnz 11437 . . . . . . . . . 10 (𝑖 ∈ ℕ → 𝑖 ∈ ℤ)
2322ad2antrl 764 . . . . . . . . 9 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℤ)
247, 8, 9, 10, 11, 2elqaalem1 24119 . . . . . . . . . . 11 ((𝜑𝐾 ∈ ℕ0) → ((𝑁𝐾) ∈ ℕ ∧ ((𝐵𝐾) · (𝑁𝐾)) ∈ ℤ))
2524simpld 474 . . . . . . . . . 10 ((𝜑𝐾 ∈ ℕ0) → (𝑁𝐾) ∈ ℕ)
2625adantr 480 . . . . . . . . 9 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑁𝐾) ∈ ℕ)
2723, 26zmodcld 12731 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 mod (𝑁𝐾)) ∈ ℕ0)
2827nn0zd 11518 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 mod (𝑁𝐾)) ∈ ℤ)
29 nnz 11437 . . . . . . . . . 10 (𝑗 ∈ ℕ → 𝑗 ∈ ℤ)
3029ad2antll 765 . . . . . . . . 9 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℤ)
3130, 26zmodcld 12731 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑗 mod (𝑁𝐾)) ∈ ℕ0)
3231nn0zd 11518 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑗 mod (𝑁𝐾)) ∈ ℤ)
3326nnrpd 11908 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑁𝐾) ∈ ℝ+)
34 nnre 11065 . . . . . . . . 9 (𝑖 ∈ ℕ → 𝑖 ∈ ℝ)
3534ad2antrl 764 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℝ)
36 modabs2 12744 . . . . . . . 8 ((𝑖 ∈ ℝ ∧ (𝑁𝐾) ∈ ℝ+) → ((𝑖 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑖 mod (𝑁𝐾)))
3735, 33, 36syl2anc 694 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑖 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑖 mod (𝑁𝐾)))
38 nnre 11065 . . . . . . . . 9 (𝑗 ∈ ℕ → 𝑗 ∈ ℝ)
3938ad2antll 765 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℝ)
40 modabs2 12744 . . . . . . . 8 ((𝑗 ∈ ℝ ∧ (𝑁𝐾) ∈ ℝ+) → ((𝑗 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑗 mod (𝑁𝐾)))
4139, 33, 40syl2anc 694 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑗 mod (𝑁𝐾)) mod (𝑁𝐾)) = (𝑗 mod (𝑁𝐾)))
4228, 23, 32, 30, 33, 37, 41modmul12d 12764 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
43 oveq1 6697 . . . . . . . . . 10 (𝑘 = 𝑖 → (𝑘 mod (𝑁𝐾)) = (𝑖 mod (𝑁𝐾)))
44 eqid 2651 . . . . . . . . . 10 (𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾))) = (𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))
45 ovex 6718 . . . . . . . . . 10 (𝑖 mod (𝑁𝐾)) ∈ V
4643, 44, 45fvmpt 6321 . . . . . . . . 9 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖) = (𝑖 mod (𝑁𝐾)))
4746ad2antrl 764 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖) = (𝑖 mod (𝑁𝐾)))
48 oveq1 6697 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝑘 mod (𝑁𝐾)) = (𝑗 mod (𝑁𝐾)))
49 ovex 6718 . . . . . . . . . 10 (𝑗 mod (𝑁𝐾)) ∈ V
5048, 44, 49fvmpt 6321 . . . . . . . . 9 (𝑗 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗) = (𝑗 mod (𝑁𝐾)))
5150ad2antll 765 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗) = (𝑗 mod (𝑁𝐾)))
5247, 51oveq12d 6708 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗)) = ((𝑖 mod (𝑁𝐾))𝑃(𝑗 mod (𝑁𝐾))))
53 oveq12 6699 . . . . . . . . . 10 ((𝑥 = (𝑖 mod (𝑁𝐾)) ∧ 𝑦 = (𝑗 mod (𝑁𝐾))) → (𝑥 · 𝑦) = ((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))))
5453oveq1d 6705 . . . . . . . . 9 ((𝑥 = (𝑖 mod (𝑁𝐾)) ∧ 𝑦 = (𝑗 mod (𝑁𝐾))) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)))
55 elqaa.7 . . . . . . . . 9 𝑃 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 · 𝑦) mod (𝑁𝐾)))
56 ovex 6718 . . . . . . . . 9 (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)) ∈ V
5754, 55, 56ovmpt2a 6833 . . . . . . . 8 (((𝑖 mod (𝑁𝐾)) ∈ V ∧ (𝑗 mod (𝑁𝐾)) ∈ V) → ((𝑖 mod (𝑁𝐾))𝑃(𝑗 mod (𝑁𝐾))) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)))
5845, 49, 57mp2an 708 . . . . . . 7 ((𝑖 mod (𝑁𝐾))𝑃(𝑗 mod (𝑁𝐾))) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾))
5952, 58syl6eq 2701 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗)) = (((𝑖 mod (𝑁𝐾)) · (𝑗 mod (𝑁𝐾))) mod (𝑁𝐾)))
60 oveq1 6697 . . . . . . . 8 (𝑘 = (𝑖 · 𝑗) → (𝑘 mod (𝑁𝐾)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
61 ovex 6718 . . . . . . . 8 ((𝑖 · 𝑗) mod (𝑁𝐾)) ∈ V
6260, 44, 61fvmpt 6321 . . . . . . 7 ((𝑖 · 𝑗) ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑖 · 𝑗)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
635, 62syl 17 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑖 · 𝑗)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
6442, 59, 633eqtr4rd 2696 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑖 · 𝑗)) = (((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑖)𝑃((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑗)))
65 oveq1 6697 . . . . . . . . 9 (𝑘 = (𝑁𝑖) → (𝑘 mod (𝑁𝐾)) = ((𝑁𝑖) mod (𝑁𝐾)))
66 ovex 6718 . . . . . . . . 9 ((𝑁𝑖) mod (𝑁𝐾)) ∈ V
6765, 44, 66fvmpt 6321 . . . . . . . 8 ((𝑁𝑖) ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑁𝑖) mod (𝑁𝐾)))
6814, 67syl 17 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑁𝑖) mod (𝑁𝐾)))
69 fveq2 6229 . . . . . . . . . 10 (𝑘 = 𝑖 → (𝑁𝑘) = (𝑁𝑖))
7069oveq1d 6705 . . . . . . . . 9 (𝑘 = 𝑖 → ((𝑁𝑘) mod (𝑁𝐾)) = ((𝑁𝑖) mod (𝑁𝐾)))
71 eqid 2651 . . . . . . . . 9 (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))) = (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))
7270, 71, 66fvmpt 6321 . . . . . . . 8 (𝑖 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) = ((𝑁𝑖) mod (𝑁𝐾)))
7372adantl 481 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) = ((𝑁𝑖) mod (𝑁𝐾)))
7468, 73eqtr4d 2688 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖))
756, 74sylan2 490 . . . . 5 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(𝑁𝑖)) = ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖))
765, 15, 21, 64, 75seqhomo 12888 . . . 4 ((𝜑𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘(seq0( · , 𝑁)‘(deg‘𝐹))) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)))
773, 76syl5eq 2697 . . 3 ((𝜑𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)))
781, 77sylan2 490 . 2 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)))
79 0zd 11427 . . . . . . . 8 (𝜑 → 0 ∈ ℤ)
804adantl 481 . . . . . . . 8 ((𝜑 ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 · 𝑗) ∈ ℕ)
8119, 79, 13, 80seqf 12862 . . . . . . 7 (𝜑 → seq0( · , 𝑁):ℕ0⟶ℕ)
8281, 18ffvelrnd 6400 . . . . . 6 (𝜑 → (seq0( · , 𝑁)‘(deg‘𝐹)) ∈ ℕ)
832, 82syl5eqel 2734 . . . . 5 (𝜑𝑅 ∈ ℕ)
8483adantr 480 . . . 4 ((𝜑𝐾 ∈ ℕ0) → 𝑅 ∈ ℕ)
85 oveq1 6697 . . . . 5 (𝑘 = 𝑅 → (𝑘 mod (𝑁𝐾)) = (𝑅 mod (𝑁𝐾)))
86 ovex 6718 . . . . 5 (𝑅 mod (𝑁𝐾)) ∈ V
8785, 44, 86fvmpt 6321 . . . 4 (𝑅 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (𝑅 mod (𝑁𝐾)))
8884, 87syl 17 . . 3 ((𝜑𝐾 ∈ ℕ0) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (𝑅 mod (𝑁𝐾)))
891, 88sylan2 490 . 2 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ ↦ (𝑘 mod (𝑁𝐾)))‘𝑅) = (𝑅 mod (𝑁𝐾)))
90 vex 3234 . . . . 5 𝑖 ∈ V
91 vex 3234 . . . . 5 𝑗 ∈ V
92 oveq12 6699 . . . . . . 7 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑥 · 𝑦) = (𝑖 · 𝑗))
9392oveq1d 6705 . . . . . 6 ((𝑥 = 𝑖𝑦 = 𝑗) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
9493, 55, 61ovmpt2a 6833 . . . . 5 ((𝑖 ∈ V ∧ 𝑗 ∈ V) → (𝑖𝑃𝑗) = ((𝑖 · 𝑗) mod (𝑁𝐾)))
9590, 91, 94mp2an 708 . . . 4 (𝑖𝑃𝑗) = ((𝑖 · 𝑗) mod (𝑁𝐾))
96 nn0mulcl 11367 . . . . . 6 ((𝑖 ∈ ℕ0𝑗 ∈ ℕ0) → (𝑖 · 𝑗) ∈ ℕ0)
9796nn0zd 11518 . . . . 5 ((𝑖 ∈ ℕ0𝑗 ∈ ℕ0) → (𝑖 · 𝑗) ∈ ℤ)
981, 25sylan2 490 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℕ)
99 zmodcl 12730 . . . . 5 (((𝑖 · 𝑗) ∈ ℤ ∧ (𝑁𝐾) ∈ ℕ) → ((𝑖 · 𝑗) mod (𝑁𝐾)) ∈ ℕ0)
10097, 98, 99syl2anr 494 . . . 4 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ (𝑖 ∈ ℕ0𝑗 ∈ ℕ0)) → ((𝑖 · 𝑗) mod (𝑁𝐾)) ∈ ℕ0)
10195, 100syl5eqel 2734 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ (𝑖 ∈ ℕ0𝑗 ∈ ℕ0)) → (𝑖𝑃𝑗) ∈ ℕ0)
102 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑚 → (𝐵𝑘) = (𝐵𝑚))
103102oveq1d 6705 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑚 → ((𝐵𝑘) · 𝑛) = ((𝐵𝑚) · 𝑛))
104103eleq1d 2715 . . . . . . . . . . . . . . 15 (𝑘 = 𝑚 → (((𝐵𝑘) · 𝑛) ∈ ℤ ↔ ((𝐵𝑚) · 𝑛) ∈ ℤ))
105104rabbidv 3220 . . . . . . . . . . . . . 14 (𝑘 = 𝑚 → {𝑛 ∈ ℕ ∣ ((𝐵𝑘) · 𝑛) ∈ ℤ} = {𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ})
106105infeq1d 8424 . . . . . . . . . . . . 13 (𝑘 = 𝑚 → inf({𝑛 ∈ ℕ ∣ ((𝐵𝑘) · 𝑛) ∈ ℤ}, ℝ, < ) = inf({𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ}, ℝ, < ))
107106cbvmptv 4783 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵𝑘) · 𝑛) ∈ ℤ}, ℝ, < )) = (𝑚 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ}, ℝ, < ))
10811, 107eqtri 2673 . . . . . . . . . . 11 𝑁 = (𝑚 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵𝑚) · 𝑛) ∈ ℤ}, ℝ, < ))
1097, 8, 9, 10, 108, 2elqaalem1 24119 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((𝑁𝑘) ∈ ℕ ∧ ((𝐵𝑘) · (𝑁𝑘)) ∈ ℤ))
110109simpld 474 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (𝑁𝑘) ∈ ℕ)
111110adantlr 751 . . . . . . . 8 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑁𝑘) ∈ ℕ)
112111nnzd 11519 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑁𝑘) ∈ ℤ)
11325adantr 480 . . . . . . 7 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑁𝐾) ∈ ℕ)
114112, 113zmodcld 12731 . . . . . 6 (((𝜑𝐾 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → ((𝑁𝑘) mod (𝑁𝐾)) ∈ ℕ0)
115114, 71fmptd 6425 . . . . 5 ((𝜑𝐾 ∈ ℕ0) → (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))):ℕ0⟶ℕ0)
1161, 115sylan2 490 . . . 4 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))):ℕ0⟶ℕ0)
117 ffvelrn 6397 . . . 4 (((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))):ℕ0⟶ℕ0𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) ∈ ℕ0)
118116, 6, 117syl2an 493 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝑖) ∈ ℕ0)
119 c0ex 10072 . . . . 5 0 ∈ V
120 oveq12 6699 . . . . . . 7 ((𝑥 = 0 ∧ 𝑦 = 𝑖) → (𝑥 · 𝑦) = (0 · 𝑖))
121120oveq1d 6705 . . . . . 6 ((𝑥 = 0 ∧ 𝑦 = 𝑖) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = ((0 · 𝑖) mod (𝑁𝐾)))
122 ovex 6718 . . . . . 6 ((0 · 𝑖) mod (𝑁𝐾)) ∈ V
123121, 55, 122ovmpt2a 6833 . . . . 5 ((0 ∈ V ∧ 𝑖 ∈ V) → (0𝑃𝑖) = ((0 · 𝑖) mod (𝑁𝐾)))
124119, 90, 123mp2an 708 . . . 4 (0𝑃𝑖) = ((0 · 𝑖) mod (𝑁𝐾))
125 nn0cn 11340 . . . . . . 7 (𝑖 ∈ ℕ0𝑖 ∈ ℂ)
126125mul02d 10272 . . . . . 6 (𝑖 ∈ ℕ0 → (0 · 𝑖) = 0)
127126oveq1d 6705 . . . . 5 (𝑖 ∈ ℕ0 → ((0 · 𝑖) mod (𝑁𝐾)) = (0 mod (𝑁𝐾)))
12898nnrpd 11908 . . . . . 6 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℝ+)
129 0mod 12741 . . . . . 6 ((𝑁𝐾) ∈ ℝ+ → (0 mod (𝑁𝐾)) = 0)
130128, 129syl 17 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (0 mod (𝑁𝐾)) = 0)
131127, 130sylan9eqr 2707 . . . 4 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → ((0 · 𝑖) mod (𝑁𝐾)) = 0)
132124, 131syl5eq 2697 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → (0𝑃𝑖) = 0)
133 oveq12 6699 . . . . . . 7 ((𝑥 = 𝑖𝑦 = 0) → (𝑥 · 𝑦) = (𝑖 · 0))
134133oveq1d 6705 . . . . . 6 ((𝑥 = 𝑖𝑦 = 0) → ((𝑥 · 𝑦) mod (𝑁𝐾)) = ((𝑖 · 0) mod (𝑁𝐾)))
135 ovex 6718 . . . . . 6 ((𝑖 · 0) mod (𝑁𝐾)) ∈ V
136134, 55, 135ovmpt2a 6833 . . . . 5 ((𝑖 ∈ V ∧ 0 ∈ V) → (𝑖𝑃0) = ((𝑖 · 0) mod (𝑁𝐾)))
13790, 119, 136mp2an 708 . . . 4 (𝑖𝑃0) = ((𝑖 · 0) mod (𝑁𝐾))
138125mul01d 10273 . . . . . 6 (𝑖 ∈ ℕ0 → (𝑖 · 0) = 0)
139138oveq1d 6705 . . . . 5 (𝑖 ∈ ℕ0 → ((𝑖 · 0) mod (𝑁𝐾)) = (0 mod (𝑁𝐾)))
140139, 130sylan9eqr 2707 . . . 4 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → ((𝑖 · 0) mod (𝑁𝐾)) = 0)
141137, 140syl5eq 2697 . . 3 (((𝜑𝐾 ∈ (0...(deg‘𝐹))) ∧ 𝑖 ∈ ℕ0) → (𝑖𝑃0) = 0)
142 simpr 476 . . 3 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → 𝐾 ∈ (0...(deg‘𝐹)))
14318adantr 480 . . 3 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (deg‘𝐹) ∈ ℕ0)
1441adantl 481 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → 𝐾 ∈ ℕ0)
145 fveq2 6229 . . . . . . 7 (𝑘 = 𝐾 → (𝑁𝑘) = (𝑁𝐾))
146145oveq1d 6705 . . . . . 6 (𝑘 = 𝐾 → ((𝑁𝑘) mod (𝑁𝐾)) = ((𝑁𝐾) mod (𝑁𝐾)))
147 ovex 6718 . . . . . 6 ((𝑁𝐾) mod (𝑁𝐾)) ∈ V
148146, 71, 147fvmpt 6321 . . . . 5 (𝐾 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝐾) = ((𝑁𝐾) mod (𝑁𝐾)))
149144, 148syl 17 . . . 4 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝐾) = ((𝑁𝐾) mod (𝑁𝐾)))
15098nncnd 11074 . . . . . . 7 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℂ)
15198nnne0d 11103 . . . . . . 7 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ≠ 0)
152150, 151dividd 10837 . . . . . 6 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁𝐾) / (𝑁𝐾)) = 1)
153 1z 11445 . . . . . 6 1 ∈ ℤ
154152, 153syl6eqel 2738 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁𝐾) / (𝑁𝐾)) ∈ ℤ)
15598nnred 11073 . . . . . 6 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑁𝐾) ∈ ℝ)
156 mod0 12715 . . . . . 6 (((𝑁𝐾) ∈ ℝ ∧ (𝑁𝐾) ∈ ℝ+) → (((𝑁𝐾) mod (𝑁𝐾)) = 0 ↔ ((𝑁𝐾) / (𝑁𝐾)) ∈ ℤ))
157155, 128, 156syl2anc 694 . . . . 5 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (((𝑁𝐾) mod (𝑁𝐾)) = 0 ↔ ((𝑁𝐾) / (𝑁𝐾)) ∈ ℤ))
158154, 157mpbird 247 . . . 4 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑁𝐾) mod (𝑁𝐾)) = 0)
159149, 158eqtrd 2685 . . 3 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → ((𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾)))‘𝐾) = 0)
160101, 118, 132, 141, 142, 143, 159seqz 12889 . 2 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (seq0(𝑃, (𝑘 ∈ ℕ0 ↦ ((𝑁𝑘) mod (𝑁𝐾))))‘(deg‘𝐹)) = 0)
16178, 89, 1603eqtr3d 2693 1 ((𝜑𝐾 ∈ (0...(deg‘𝐹))) → (𝑅 mod (𝑁𝐾)) = 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  {crab 2945  Vcvv 3231  cdif 3604  {csn 4210  cmpt 4762  wf 5922  cfv 5926  (class class class)co 6690  cmpt2 6692  infcinf 8388  cc 9972  cr 9973  0cc0 9974  1c1 9975   · cmul 9979   < clt 10112   / cdiv 10722  cn 11058  0cn0 11330  cz 11415  cuz 11725  cq 11826  +crp 11870  ...cfz 12364   mod cmo 12708  seqcseq 12841  0𝑝c0p 23481  Polycply 23985  coeffccoe 23987  degcdgr 23988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-rlim 14264  df-sum 14461  df-0p 23482  df-ply 23989  df-coe 23991  df-dgr 23992
This theorem is referenced by:  elqaalem3  24121
  Copyright terms: Public domain W3C validator