Metamath Proof Explorer

Theorem elqaalem2

Description: Lemma for elqaa . (Contributed by Mario Carneiro, 23-Jul-2014) (Revised by AV, 3-Oct-2020)

Ref Expression
Hypotheses elqaa.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
elqaa.2 ⊢ ( 𝜑 → 𝐹 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) )
elqaa.3 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 0 )
elqaa.4 ⊢ 𝐵 = ( coeff ‘ 𝐹 )
elqaa.5 ⊢ 𝑁 = ( 𝑘 ∈ ℕ0 ↦ inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) )
elqaa.6 ⊢ 𝑅 = ( seq 0 ( · , 𝑁 ) ‘ ( deg ‘ 𝐹 ) )
elqaa.7 ⊢ 𝑃 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( ( 𝑥 · 𝑦 ) mod ( 𝑁 ‘ 𝐾 ) ) )
Assertion elqaalem2 ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑅 mod ( 𝑁 ‘ 𝐾 ) ) = 0 )

Proof

Step Hyp Ref Expression
1 elqaa.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 elqaa.2 ⊢ ( 𝜑 → 𝐹 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) )
3 elqaa.3 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 0 )
4 elqaa.4 ⊢ 𝐵 = ( coeff ‘ 𝐹 )
5 elqaa.5 ⊢ 𝑁 = ( 𝑘 ∈ ℕ0 ↦ inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) )
6 elqaa.6 ⊢ 𝑅 = ( seq 0 ( · , 𝑁 ) ‘ ( deg ‘ 𝐹 ) )
7 elqaa.7 ⊢ 𝑃 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( ( 𝑥 · 𝑦 ) mod ( 𝑁 ‘ 𝐾 ) ) )
8 elfznn0 ⊢ ( 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) → 𝐾 ∈ ℕ0 )
9 6 fveq2i ⊢ ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑅 ) = ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ ( seq 0 ( · , 𝑁 ) ‘ ( deg ‘ 𝐹 ) ) )
10 nnmulcl ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( 𝑖 · 𝑗 ) ∈ ℕ )
11 10 adantl ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( 𝑖 · 𝑗 ) ∈ ℕ )
12 elfznn0 ⊢ ( 𝑖 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) → 𝑖 ∈ ℕ0 )
13 1 2 3 4 5 6 elqaalem1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑁 ‘ 𝑖 ) ∈ ℕ ∧ ( ( 𝐵 ‘ 𝑖 ) · ( 𝑁 ‘ 𝑖 ) ) ∈ ℤ ) )
14 13 simpld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑁 ‘ 𝑖 ) ∈ ℕ )
15 14 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝑁 ‘ 𝑖 ) ∈ ℕ )
16 12 15 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑁 ‘ 𝑖 ) ∈ ℕ )
17 eldifi ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) → 𝐹 ∈ ( Poly ‘ ℚ ) )
18 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ ℚ ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
19 2 17 18 3syl ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℕ0 )
20 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
21 19 20 eleqtrdi ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 0 ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) → ( deg ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 0 ) )
23 nnz ⊢ ( 𝑖 ∈ ℕ → 𝑖 ∈ ℤ )
24 23 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → 𝑖 ∈ ℤ )
25 1 2 3 4 5 6 elqaalem1 ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑁 ‘ 𝐾 ) ∈ ℕ ∧ ( ( 𝐵 ‘ 𝐾 ) · ( 𝑁 ‘ 𝐾 ) ) ∈ ℤ ) )
26 25 simpld ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 ‘ 𝐾 ) ∈ ℕ )
27 26 adantr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( 𝑁 ‘ 𝐾 ) ∈ ℕ )
28 24 27 zmodcld ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) ∈ ℕ0 )
29 28 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) ∈ ℤ )
30 nnz ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℤ )
31 30 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → 𝑗 ∈ ℤ )
32 31 27 zmodcld ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) ∈ ℕ0 )
33 32 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) ∈ ℤ )
34 27 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( 𝑁 ‘ 𝐾 ) ∈ ℝ+ )
35 nnre ⊢ ( 𝑖 ∈ ℕ → 𝑖 ∈ ℝ )
36 35 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → 𝑖 ∈ ℝ )
37 modabs2 ⊢ ( ( 𝑖 ∈ ℝ ∧ ( 𝑁 ‘ 𝐾 ) ∈ ℝ+ ) → ( ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) mod ( 𝑁 ‘ 𝐾 ) ) = ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) )
38 36 34 37 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) mod ( 𝑁 ‘ 𝐾 ) ) = ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) )
39 nnre ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ )
40 39 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → 𝑗 ∈ ℝ )
41 modabs2 ⊢ ( ( 𝑗 ∈ ℝ ∧ ( 𝑁 ‘ 𝐾 ) ∈ ℝ+ ) → ( ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) mod ( 𝑁 ‘ 𝐾 ) ) = ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) )
42 40 34 41 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) mod ( 𝑁 ‘ 𝐾 ) ) = ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) )
43 29 24 33 31 34 38 42 modmul12d ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( ( ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) · ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) ) mod ( 𝑁 ‘ 𝐾 ) ) = ( ( 𝑖 · 𝑗 ) mod ( 𝑁 ‘ 𝐾 ) ) )
44 oveq1 ⊢ ( 𝑘 = 𝑖 → ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) = ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) )
45 eqid ⊢ ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) )
46 ovex ⊢ ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) ∈ V
47 44 45 46 fvmpt ⊢ ( 𝑖 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑖 ) = ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) )
48 47 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑖 ) = ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) )
49 oveq1 ⊢ ( 𝑘 = 𝑗 → ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) = ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) )
50 ovex ⊢ ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) ∈ V
51 49 45 50 fvmpt ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑗 ) = ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) )
52 51 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑗 ) = ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) )
53 48 52 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑖 ) 𝑃 ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑗 ) ) = ( ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) 𝑃 ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) ) )
54 oveq12 ⊢ ( ( 𝑥 = ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) ∧ 𝑦 = ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) ) → ( 𝑥 · 𝑦 ) = ( ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) · ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) ) )
55 54 oveq1d ⊢ ( ( 𝑥 = ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) ∧ 𝑦 = ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) ) → ( ( 𝑥 · 𝑦 ) mod ( 𝑁 ‘ 𝐾 ) ) = ( ( ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) · ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) ) mod ( 𝑁 ‘ 𝐾 ) ) )
56 ovex ⊢ ( ( ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) · ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) ) mod ( 𝑁 ‘ 𝐾 ) ) ∈ V
57 55 7 56 ovmpoa ⊢ ( ( ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) ∈ V ∧ ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) ∈ V ) → ( ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) 𝑃 ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) ) = ( ( ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) · ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) ) mod ( 𝑁 ‘ 𝐾 ) ) )
58 46 50 57 mp2an ⊢ ( ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) 𝑃 ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) ) = ( ( ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) · ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) ) mod ( 𝑁 ‘ 𝐾 ) )
59 53 58 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑖 ) 𝑃 ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑗 ) ) = ( ( ( 𝑖 mod ( 𝑁 ‘ 𝐾 ) ) · ( 𝑗 mod ( 𝑁 ‘ 𝐾 ) ) ) mod ( 𝑁 ‘ 𝐾 ) ) )
60 oveq1 ⊢ ( 𝑘 = ( 𝑖 · 𝑗 ) → ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) = ( ( 𝑖 · 𝑗 ) mod ( 𝑁 ‘ 𝐾 ) ) )
61 ovex ⊢ ( ( 𝑖 · 𝑗 ) mod ( 𝑁 ‘ 𝐾 ) ) ∈ V
62 60 45 61 fvmpt ⊢ ( ( 𝑖 · 𝑗 ) ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ ( 𝑖 · 𝑗 ) ) = ( ( 𝑖 · 𝑗 ) mod ( 𝑁 ‘ 𝐾 ) ) )
63 11 62 syl ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ ( 𝑖 · 𝑗 ) ) = ( ( 𝑖 · 𝑗 ) mod ( 𝑁 ‘ 𝐾 ) ) )
64 43 59 63 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ ( 𝑖 · 𝑗 ) ) = ( ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑖 ) 𝑃 ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑗 ) ) )
65 oveq1 ⊢ ( 𝑘 = ( 𝑁 ‘ 𝑖 ) → ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) = ( ( 𝑁 ‘ 𝑖 ) mod ( 𝑁 ‘ 𝐾 ) ) )
66 ovex ⊢ ( ( 𝑁 ‘ 𝑖 ) mod ( 𝑁 ‘ 𝐾 ) ) ∈ V
67 65 45 66 fvmpt ⊢ ( ( 𝑁 ‘ 𝑖 ) ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ ( 𝑁 ‘ 𝑖 ) ) = ( ( 𝑁 ‘ 𝑖 ) mod ( 𝑁 ‘ 𝐾 ) ) )
68 15 67 syl ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ ( 𝑁 ‘ 𝑖 ) ) = ( ( 𝑁 ‘ 𝑖 ) mod ( 𝑁 ‘ 𝐾 ) ) )
69 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝑁 ‘ 𝑘 ) = ( 𝑁 ‘ 𝑖 ) )
70 69 oveq1d ⊢ ( 𝑘 = 𝑖 → ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) = ( ( 𝑁 ‘ 𝑖 ) mod ( 𝑁 ‘ 𝐾 ) ) )
71 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) )
72 70 71 66 fvmpt ⊢ ( 𝑖 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑖 ) = ( ( 𝑁 ‘ 𝑖 ) mod ( 𝑁 ‘ 𝐾 ) ) )
73 72 adantl ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑖 ) = ( ( 𝑁 ‘ 𝑖 ) mod ( 𝑁 ‘ 𝐾 ) ) )
74 68 73 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ ( 𝑁 ‘ 𝑖 ) ) = ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑖 ) )
75 12 74 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ ( 𝑁 ‘ 𝑖 ) ) = ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑖 ) )
76 11 16 22 64 75 seqhomo ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ ( seq 0 ( · , 𝑁 ) ‘ ( deg ‘ 𝐹 ) ) ) = ( seq 0 ( 𝑃 , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ) ) ‘ ( deg ‘ 𝐹 ) ) )
77 9 76 eqtrid ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑅 ) = ( seq 0 ( 𝑃 , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ) ) ‘ ( deg ‘ 𝐹 ) ) )
78 8 77 sylan2 ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑅 ) = ( seq 0 ( 𝑃 , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ) ) ‘ ( deg ‘ 𝐹 ) ) )
79 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
80 10 adantl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( 𝑖 · 𝑗 ) ∈ ℕ )
81 20 79 14 80 seqf ⊢ ( 𝜑 → seq 0 ( · , 𝑁 ) : ℕ0 ⟶ ℕ )
82 81 19 ffvelrnd ⊢ ( 𝜑 → ( seq 0 ( · , 𝑁 ) ‘ ( deg ‘ 𝐹 ) ) ∈ ℕ )
83 6 82 eqeltrid ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
84 83 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) → 𝑅 ∈ ℕ )
85 oveq1 ⊢ ( 𝑘 = 𝑅 → ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) = ( 𝑅 mod ( 𝑁 ‘ 𝐾 ) ) )
86 ovex ⊢ ( 𝑅 mod ( 𝑁 ‘ 𝐾 ) ) ∈ V
87 85 45 86 fvmpt ⊢ ( 𝑅 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑅 ) = ( 𝑅 mod ( 𝑁 ‘ 𝐾 ) ) )
88 84 87 syl ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑅 ) = ( 𝑅 mod ( 𝑁 ‘ 𝐾 ) ) )
89 8 88 sylan2 ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( 𝑘 mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑅 ) = ( 𝑅 mod ( 𝑁 ‘ 𝐾 ) ) )
90 oveq12 ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( 𝑥 · 𝑦 ) = ( 𝑖 · 𝑗 ) )
91 90 oveq1d ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( ( 𝑥 · 𝑦 ) mod ( 𝑁 ‘ 𝐾 ) ) = ( ( 𝑖 · 𝑗 ) mod ( 𝑁 ‘ 𝐾 ) ) )
92 91 7 61 ovmpoa ⊢ ( ( 𝑖 ∈ V ∧ 𝑗 ∈ V ) → ( 𝑖 𝑃 𝑗 ) = ( ( 𝑖 · 𝑗 ) mod ( 𝑁 ‘ 𝐾 ) ) )
93 92 el2v ⊢ ( 𝑖 𝑃 𝑗 ) = ( ( 𝑖 · 𝑗 ) mod ( 𝑁 ‘ 𝐾 ) )
94 nn0mulcl ⊢ ( ( 𝑖 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ) → ( 𝑖 · 𝑗 ) ∈ ℕ0 )
95 94 nn0zd ⊢ ( ( 𝑖 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ) → ( 𝑖 · 𝑗 ) ∈ ℤ )
96 8 26 sylan2 ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑁 ‘ 𝐾 ) ∈ ℕ )
97 zmodcl ⊢ ( ( ( 𝑖 · 𝑗 ) ∈ ℤ ∧ ( 𝑁 ‘ 𝐾 ) ∈ ℕ ) → ( ( 𝑖 · 𝑗 ) mod ( 𝑁 ‘ 𝐾 ) ) ∈ ℕ0 )
98 95 96 97 syl2anr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) ∧ ( 𝑖 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ) ) → ( ( 𝑖 · 𝑗 ) mod ( 𝑁 ‘ 𝐾 ) ) ∈ ℕ0 )
99 93 98 eqeltrid ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) ∧ ( 𝑖 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ) ) → ( 𝑖 𝑃 𝑗 ) ∈ ℕ0 )
100 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑚 ) )
101 100 oveq1d ⊢ ( 𝑘 = 𝑚 → ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) = ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) )
102 101 eleq1d ⊢ ( 𝑘 = 𝑚 → ( ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) ∈ ℤ ↔ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ ) )
103 102 rabbidv ⊢ ( 𝑘 = 𝑚 → { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) ∈ ℤ } = { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } )
104 103 infeq1d ⊢ ( 𝑘 = 𝑚 → inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) = inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) )
105 104 cbvmptv ⊢ ( 𝑘 ∈ ℕ0 ↦ inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) ) = ( 𝑚 ∈ ℕ0 ↦ inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) )
106 5 105 eqtri ⊢ 𝑁 = ( 𝑚 ∈ ℕ0 ↦ inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) )
107 1 2 3 4 106 6 elqaalem1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 ‘ 𝑘 ) ∈ ℕ ∧ ( ( 𝐵 ‘ 𝑘 ) · ( 𝑁 ‘ 𝑘 ) ) ∈ ℤ ) )
108 107 simpld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 ‘ 𝑘 ) ∈ ℕ )
109 108 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 ‘ 𝑘 ) ∈ ℕ )
110 109 nnzd ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 ‘ 𝑘 ) ∈ ℤ )
111 26 adantr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 ‘ 𝐾 ) ∈ ℕ )
112 110 111 zmodcld ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ∈ ℕ0 )
113 112 fmpttd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ) : ℕ0 ⟶ ℕ0 )
114 8 113 sylan2 ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ) : ℕ0 ⟶ ℕ0 )
115 ffvelrn ⊢ ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ) : ℕ0 ⟶ ℕ0 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑖 ) ∈ ℕ0 )
116 114 12 115 syl2an ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) ∧ 𝑖 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝑖 ) ∈ ℕ0 )
117 c0ex ⊢ 0 ∈ V
118 vex ⊢ 𝑖 ∈ V
119 oveq12 ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑖 ) → ( 𝑥 · 𝑦 ) = ( 0 · 𝑖 ) )
120 119 oveq1d ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑖 ) → ( ( 𝑥 · 𝑦 ) mod ( 𝑁 ‘ 𝐾 ) ) = ( ( 0 · 𝑖 ) mod ( 𝑁 ‘ 𝐾 ) ) )
121 ovex ⊢ ( ( 0 · 𝑖 ) mod ( 𝑁 ‘ 𝐾 ) ) ∈ V
122 120 7 121 ovmpoa ⊢ ( ( 0 ∈ V ∧ 𝑖 ∈ V ) → ( 0 𝑃 𝑖 ) = ( ( 0 · 𝑖 ) mod ( 𝑁 ‘ 𝐾 ) ) )
123 117 118 122 mp2an ⊢ ( 0 𝑃 𝑖 ) = ( ( 0 · 𝑖 ) mod ( 𝑁 ‘ 𝐾 ) )
124 nn0cn ⊢ ( 𝑖 ∈ ℕ0 → 𝑖 ∈ ℂ )
125 124 mul02d ⊢ ( 𝑖 ∈ ℕ0 → ( 0 · 𝑖 ) = 0 )
126 125 oveq1d ⊢ ( 𝑖 ∈ ℕ0 → ( ( 0 · 𝑖 ) mod ( 𝑁 ‘ 𝐾 ) ) = ( 0 mod ( 𝑁 ‘ 𝐾 ) ) )
127 96 nnrpd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑁 ‘ 𝐾 ) ∈ ℝ+ )
128 0mod ⊢ ( ( 𝑁 ‘ 𝐾 ) ∈ ℝ+ → ( 0 mod ( 𝑁 ‘ 𝐾 ) ) = 0 )
129 127 128 syl ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 0 mod ( 𝑁 ‘ 𝐾 ) ) = 0 )
130 126 129 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 0 · 𝑖 ) mod ( 𝑁 ‘ 𝐾 ) ) = 0 )
131 123 130 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) ∧ 𝑖 ∈ ℕ0 ) → ( 0 𝑃 𝑖 ) = 0 )
132 oveq12 ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 0 ) → ( 𝑥 · 𝑦 ) = ( 𝑖 · 0 ) )
133 132 oveq1d ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 0 ) → ( ( 𝑥 · 𝑦 ) mod ( 𝑁 ‘ 𝐾 ) ) = ( ( 𝑖 · 0 ) mod ( 𝑁 ‘ 𝐾 ) ) )
134 ovex ⊢ ( ( 𝑖 · 0 ) mod ( 𝑁 ‘ 𝐾 ) ) ∈ V
135 133 7 134 ovmpoa ⊢ ( ( 𝑖 ∈ V ∧ 0 ∈ V ) → ( 𝑖 𝑃 0 ) = ( ( 𝑖 · 0 ) mod ( 𝑁 ‘ 𝐾 ) ) )
136 118 117 135 mp2an ⊢ ( 𝑖 𝑃 0 ) = ( ( 𝑖 · 0 ) mod ( 𝑁 ‘ 𝐾 ) )
137 124 mul01d ⊢ ( 𝑖 ∈ ℕ0 → ( 𝑖 · 0 ) = 0 )
138 137 oveq1d ⊢ ( 𝑖 ∈ ℕ0 → ( ( 𝑖 · 0 ) mod ( 𝑁 ‘ 𝐾 ) ) = ( 0 mod ( 𝑁 ‘ 𝐾 ) ) )
139 138 129 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑖 · 0 ) mod ( 𝑁 ‘ 𝐾 ) ) = 0 )
140 136 139 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝑖 𝑃 0 ) = 0 )
141 simpr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) )
142 19 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
143 8 adantl ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → 𝐾 ∈ ℕ0 )
144 fveq2 ⊢ ( 𝑘 = 𝐾 → ( 𝑁 ‘ 𝑘 ) = ( 𝑁 ‘ 𝐾 ) )
145 144 oveq1d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) = ( ( 𝑁 ‘ 𝐾 ) mod ( 𝑁 ‘ 𝐾 ) ) )
146 ovex ⊢ ( ( 𝑁 ‘ 𝐾 ) mod ( 𝑁 ‘ 𝐾 ) ) ∈ V
147 145 71 146 fvmpt ⊢ ( 𝐾 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝐾 ) = ( ( 𝑁 ‘ 𝐾 ) mod ( 𝑁 ‘ 𝐾 ) ) )
148 143 147 syl ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝐾 ) = ( ( 𝑁 ‘ 𝐾 ) mod ( 𝑁 ‘ 𝐾 ) ) )
149 96 nncnd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑁 ‘ 𝐾 ) ∈ ℂ )
150 96 nnne0d ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑁 ‘ 𝐾 ) ≠ 0 )
151 149 150 dividd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝑁 ‘ 𝐾 ) / ( 𝑁 ‘ 𝐾 ) ) = 1 )
152 1z ⊢ 1 ∈ ℤ
153 151 152 eqeltrdi ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝑁 ‘ 𝐾 ) / ( 𝑁 ‘ 𝐾 ) ) ∈ ℤ )
154 96 nnred ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑁 ‘ 𝐾 ) ∈ ℝ )
155 mod0 ⊢ ( ( ( 𝑁 ‘ 𝐾 ) ∈ ℝ ∧ ( 𝑁 ‘ 𝐾 ) ∈ ℝ+ ) → ( ( ( 𝑁 ‘ 𝐾 ) mod ( 𝑁 ‘ 𝐾 ) ) = 0 ↔ ( ( 𝑁 ‘ 𝐾 ) / ( 𝑁 ‘ 𝐾 ) ) ∈ ℤ ) )
156 154 127 155 syl2anc ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( ( 𝑁 ‘ 𝐾 ) mod ( 𝑁 ‘ 𝐾 ) ) = 0 ↔ ( ( 𝑁 ‘ 𝐾 ) / ( 𝑁 ‘ 𝐾 ) ) ∈ ℤ ) )
157 153 156 mpbird ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝑁 ‘ 𝐾 ) mod ( 𝑁 ‘ 𝐾 ) ) = 0 )
158 148 157 eqtrd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ) ‘ 𝐾 ) = 0 )
159 99 116 131 140 141 142 158 seqz ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( seq 0 ( 𝑃 , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑁 ‘ 𝑘 ) mod ( 𝑁 ‘ 𝐾 ) ) ) ) ‘ ( deg ‘ 𝐹 ) ) = 0 )
160 78 89 159 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑅 mod ( 𝑁 ‘ 𝐾 ) ) = 0 )