Metamath Proof Explorer

Theorem dchrisumlem1

Description: Lemma for dchrisum . Lemma 9.4.1 of Shapiro, p. 377. (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
rpvmasum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
rpvmasum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
rpvmasum.1 ⊢ 1 = ( 0g ‘ 𝐺 )
dchrisum.b ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
dchrisum.n1 ⊢ ( 𝜑 → 𝑋 ≠ 1 )
dchrisum.2 ⊢ ( 𝑛 = 𝑥 → 𝐴 = 𝐵 )
dchrisum.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
dchrisum.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
dchrisum.5 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
dchrisum.6 ⊢ ( 𝜑 → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
dchrisum.7 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · 𝐴 ) )
dchrisum.9 ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
dchrisum.10 ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( 0 ..^ 𝑁 ) ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
Assertion dchrisumlem1 ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑈 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2 rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3 rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 rpvmasum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
5 rpvmasum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
6 rpvmasum.1 ⊢ 1 = ( 0g ‘ 𝐺 )
7 dchrisum.b ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8 dchrisum.n1 ⊢ ( 𝜑 → 𝑋 ≠ 1 )
9 dchrisum.2 ⊢ ( 𝑛 = 𝑥 → 𝐴 = 𝐵 )
10 dchrisum.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
11 dchrisum.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
12 dchrisum.5 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
13 dchrisum.6 ⊢ ( 𝜑 → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
14 dchrisum.7 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · 𝐴 ) )
15 dchrisum.9 ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
16 dchrisum.10 ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( 0 ..^ 𝑁 ) ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
17 fzodisj ⊢ ( ( 0 ..^ ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ) ∩ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ 𝑈 ) ) = ∅
18 17 a1i ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( ( 0 ..^ ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ) ∩ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ 𝑈 ) ) = ∅ )
19 3 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
21 nn0re ⊢ ( 𝑈 ∈ ℕ0 → 𝑈 ∈ ℝ )
22 21 adantl ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → 𝑈 ∈ ℝ )
23 3 adantr ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → 𝑁 ∈ ℕ )
24 22 23 nndivred ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( 𝑈 / 𝑁 ) ∈ ℝ )
25 23 nnrpd ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → 𝑁 ∈ ℝ+ )
26 nn0ge0 ⊢ ( 𝑈 ∈ ℕ0 → 0 ≤ 𝑈 )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → 0 ≤ 𝑈 )
28 22 25 27 divge0d ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → 0 ≤ ( 𝑈 / 𝑁 ) )
29 flge0nn0 ⊢ ( ( ( 𝑈 / 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 𝑈 / 𝑁 ) ) → ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ∈ ℕ0 )
30 24 28 29 syl2anc ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ∈ ℕ0 )
31 20 30 nn0mulcld ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ∈ ℕ0 )
32 flle ⊢ ( ( 𝑈 / 𝑁 ) ∈ ℝ → ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ≤ ( 𝑈 / 𝑁 ) )
33 24 32 syl ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ≤ ( 𝑈 / 𝑁 ) )
34 reflcl ⊢ ( ( 𝑈 / 𝑁 ) ∈ ℝ → ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ∈ ℝ )
35 24 34 syl ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ∈ ℝ )
36 35 22 25 lemuldiv2d ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ≤ 𝑈 ↔ ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ≤ ( 𝑈 / 𝑁 ) ) )
37 33 36 mpbird ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ≤ 𝑈 )
38 fznn0 ⊢ ( 𝑈 ∈ ℕ0 → ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ∈ ( 0 ... 𝑈 ) ↔ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ∈ ℕ0 ∧ ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ≤ 𝑈 ) ) )
39 38 adantl ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ∈ ( 0 ... 𝑈 ) ↔ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ∈ ℕ0 ∧ ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ≤ 𝑈 ) ) )
40 31 37 39 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ∈ ( 0 ... 𝑈 ) )
41 fzosplit ⊢ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ∈ ( 0 ... 𝑈 ) → ( 0 ..^ 𝑈 ) = ( ( 0 ..^ ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ) ∪ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ 𝑈 ) ) )
42 40 41 syl ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( 0 ..^ 𝑈 ) = ( ( 0 ..^ ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ) ∪ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ 𝑈 ) ) )
43 fzofi ⊢ ( 0 ..^ 𝑈 ) ∈ Fin
44 43 a1i ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( 0 ..^ 𝑈 ) ∈ Fin )
45 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ..^ 𝑈 ) ) → 𝑋 ∈ 𝐷 )
46 elfzoelz ⊢ ( 𝑛 ∈ ( 0 ..^ 𝑈 ) → 𝑛 ∈ ℤ )
47 46 adantl ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ..^ 𝑈 ) ) → 𝑛 ∈ ℤ )
48 4 1 5 2 45 47 dchrzrhcl ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ..^ 𝑈 ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
49 18 42 44 48 fsumsplit ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → Σ 𝑛 ∈ ( 0 ..^ 𝑈 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ 𝑈 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
50 oveq2 ⊢ ( 𝑘 = 0 → ( 𝑁 · 𝑘 ) = ( 𝑁 · 0 ) )
51 50 oveq2d ⊢ ( 𝑘 = 0 → ( 0 ..^ ( 𝑁 · 𝑘 ) ) = ( 0 ..^ ( 𝑁 · 0 ) ) )
52 51 sumeq1d ⊢ ( 𝑘 = 0 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 0 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
53 52 eqeq1d ⊢ ( 𝑘 = 0 → ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ↔ Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 0 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) )
54 53 imbi2d ⊢ ( 𝑘 = 0 → ( ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) ↔ ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 0 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) ) )
55 oveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝑁 · 𝑘 ) = ( 𝑁 · 𝑚 ) )
56 55 oveq2d ⊢ ( 𝑘 = 𝑚 → ( 0 ..^ ( 𝑁 · 𝑘 ) ) = ( 0 ..^ ( 𝑁 · 𝑚 ) ) )
57 56 sumeq1d ⊢ ( 𝑘 = 𝑚 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑚 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
58 57 eqeq1d ⊢ ( 𝑘 = 𝑚 → ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ↔ Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑚 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) )
59 58 imbi2d ⊢ ( 𝑘 = 𝑚 → ( ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) ↔ ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑚 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) ) )
60 oveq2 ⊢ ( 𝑘 = ( 𝑚 + 1 ) → ( 𝑁 · 𝑘 ) = ( 𝑁 · ( 𝑚 + 1 ) ) )
61 60 oveq2d ⊢ ( 𝑘 = ( 𝑚 + 1 ) → ( 0 ..^ ( 𝑁 · 𝑘 ) ) = ( 0 ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) )
62 61 sumeq1d ⊢ ( 𝑘 = ( 𝑚 + 1 ) → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
63 62 eqeq1d ⊢ ( 𝑘 = ( 𝑚 + 1 ) → ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ↔ Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) )
64 63 imbi2d ⊢ ( 𝑘 = ( 𝑚 + 1 ) → ( ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) ↔ ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) ) )
65 oveq2 ⊢ ( 𝑘 = ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) → ( 𝑁 · 𝑘 ) = ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) )
66 65 oveq2d ⊢ ( 𝑘 = ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) → ( 0 ..^ ( 𝑁 · 𝑘 ) ) = ( 0 ..^ ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ) )
67 66 sumeq1d ⊢ ( 𝑘 = ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
68 67 eqeq1d ⊢ ( 𝑘 = ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) → ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ↔ Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) )
69 68 imbi2d ⊢ ( 𝑘 = ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) → ( ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) ↔ ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) ) )
70 3 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
71 70 mul01d ⊢ ( 𝜑 → ( 𝑁 · 0 ) = 0 )
72 71 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( 𝑁 · 0 ) ) = ( 0 ..^ 0 ) )
73 fzo0 ⊢ ( 0 ..^ 0 ) = ∅
74 72 73 eqtrdi ⊢ ( 𝜑 → ( 0 ..^ ( 𝑁 · 0 ) ) = ∅ )
75 74 sumeq1d ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 0 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ∅ ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
76 sum0 ⊢ Σ 𝑛 ∈ ∅ ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0
77 75 76 eqtrdi ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 0 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 )
78 oveq1 ⊢ ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑚 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 → ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑚 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) = ( 0 + Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
79 fzodisj ⊢ ( ( 0 ..^ ( 𝑁 · 𝑚 ) ) ∩ ( ( 𝑁 · 𝑚 ) ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ) = ∅
80 79 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( 0 ..^ ( 𝑁 · 𝑚 ) ) ∩ ( ( 𝑁 · 𝑚 ) ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ) = ∅ )
81 nn0re ⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℝ )
82 81 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℝ )
83 82 lep1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ≤ ( 𝑚 + 1 ) )
84 peano2re ⊢ ( 𝑚 ∈ ℝ → ( 𝑚 + 1 ) ∈ ℝ )
85 82 84 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑚 + 1 ) ∈ ℝ )
86 3 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑁 ∈ ℕ )
87 86 nnred ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
88 86 nngt0d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 0 < 𝑁 )
89 lemul2 ⊢ ( ( 𝑚 ∈ ℝ ∧ ( 𝑚 + 1 ) ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( 𝑚 ≤ ( 𝑚 + 1 ) ↔ ( 𝑁 · 𝑚 ) ≤ ( 𝑁 · ( 𝑚 + 1 ) ) ) )
90 82 85 87 88 89 syl112anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑚 ≤ ( 𝑚 + 1 ) ↔ ( 𝑁 · 𝑚 ) ≤ ( 𝑁 · ( 𝑚 + 1 ) ) ) )
91 83 90 mpbid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑁 · 𝑚 ) ≤ ( 𝑁 · ( 𝑚 + 1 ) ) )
92 nn0mulcl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑁 · 𝑚 ) ∈ ℕ0 )
93 19 92 sylan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑁 · 𝑚 ) ∈ ℕ0 )
94 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
95 93 94 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑁 · 𝑚 ) ∈ ( ℤ≥ ‘ 0 ) )
96 nn0p1nn ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℕ )
97 nnmulcl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑚 + 1 ) ∈ ℕ ) → ( 𝑁 · ( 𝑚 + 1 ) ) ∈ ℕ )
98 3 96 97 syl2an ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑁 · ( 𝑚 + 1 ) ) ∈ ℕ )
99 98 nnzd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑁 · ( 𝑚 + 1 ) ) ∈ ℤ )
100 elfz5 ⊢ ( ( ( 𝑁 · 𝑚 ) ∈ ( ℤ≥ ‘ 0 ) ∧ ( 𝑁 · ( 𝑚 + 1 ) ) ∈ ℤ ) → ( ( 𝑁 · 𝑚 ) ∈ ( 0 ... ( 𝑁 · ( 𝑚 + 1 ) ) ) ↔ ( 𝑁 · 𝑚 ) ≤ ( 𝑁 · ( 𝑚 + 1 ) ) ) )
101 95 99 100 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑁 · 𝑚 ) ∈ ( 0 ... ( 𝑁 · ( 𝑚 + 1 ) ) ) ↔ ( 𝑁 · 𝑚 ) ≤ ( 𝑁 · ( 𝑚 + 1 ) ) ) )
102 91 101 mpbird ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑁 · 𝑚 ) ∈ ( 0 ... ( 𝑁 · ( 𝑚 + 1 ) ) ) )
103 fzosplit ⊢ ( ( 𝑁 · 𝑚 ) ∈ ( 0 ... ( 𝑁 · ( 𝑚 + 1 ) ) ) → ( 0 ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) = ( ( 0 ..^ ( 𝑁 · 𝑚 ) ) ∪ ( ( 𝑁 · 𝑚 ) ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ) )
104 102 103 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 0 ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) = ( ( 0 ..^ ( 𝑁 · 𝑚 ) ) ∪ ( ( 𝑁 · 𝑚 ) ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ) )
105 fzofi ⊢ ( 0 ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ∈ Fin
106 105 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 0 ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ∈ Fin )
107 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ) → 𝑋 ∈ 𝐷 )
108 elfzoelz ⊢ ( 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) → 𝑛 ∈ ℤ )
109 108 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ) → 𝑛 ∈ ℤ )
110 4 1 5 2 107 109 dchrzrhcl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
111 80 104 106 110 fsumsplit ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑚 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
112 86 nncnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
113 82 recnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℂ )
114 1cnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 1 ∈ ℂ )
115 112 113 114 adddid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑁 · ( 𝑚 + 1 ) ) = ( ( 𝑁 · 𝑚 ) + ( 𝑁 · 1 ) ) )
116 112 mulridd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑁 · 1 ) = 𝑁 )
117 116 oveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑁 · 𝑚 ) + ( 𝑁 · 1 ) ) = ( ( 𝑁 · 𝑚 ) + 𝑁 ) )
118 115 117 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑁 · ( 𝑚 + 1 ) ) = ( ( 𝑁 · 𝑚 ) + 𝑁 ) )
119 118 oveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑁 · 𝑚 ) ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) = ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑁 ) ) )
120 119 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
121 oveq2 ⊢ ( 𝑘 = 𝑁 → ( ( 𝑁 · 𝑚 ) + 𝑘 ) = ( ( 𝑁 · 𝑚 ) + 𝑁 ) )
122 121 oveq2d ⊢ ( 𝑘 = 𝑁 → ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑘 ) ) = ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑁 ) ) )
123 122 sumeq1d ⊢ ( 𝑘 = 𝑁 → Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
124 oveq2 ⊢ ( 𝑘 = 𝑁 → ( 0 ..^ 𝑘 ) = ( 0 ..^ 𝑁 ) )
125 124 sumeq1d ⊢ ( 𝑘 = 𝑁 → Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
126 123 125 eqeq12d ⊢ ( 𝑘 = 𝑁 → ( Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ↔ Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
127 93 nn0zd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑁 · 𝑚 ) ∈ ℤ )
128 127 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 · 𝑚 ) ∈ ℤ )
129 nn0z ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ )
130 zaddcl ⊢ ( ( ( 𝑁 · 𝑚 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑁 · 𝑚 ) + 𝑘 ) ∈ ℤ )
131 127 129 130 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 · 𝑚 ) + 𝑘 ) ∈ ℤ )
132 peano2zm ⊢ ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) ∈ ℤ → ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − 1 ) ∈ ℤ )
133 131 132 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − 1 ) ∈ ℤ )
134 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ... ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − 1 ) ) ) → 𝑋 ∈ 𝐷 )
135 elfzelz ⊢ ( 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ... ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − 1 ) ) → 𝑛 ∈ ℤ )
136 135 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ... ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − 1 ) ) ) → 𝑛 ∈ ℤ )
137 4 1 5 2 134 136 dchrzrhcl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ... ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − 1 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
138 2fveq3 ⊢ ( 𝑛 = ( 𝑖 + ( 𝑁 · 𝑚 ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑖 + ( 𝑁 · 𝑚 ) ) ) ) )
139 128 128 133 137 138 fsumshftm ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ... ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑖 ∈ ( ( ( 𝑁 · 𝑚 ) − ( 𝑁 · 𝑚 ) ) ... ( ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − 1 ) − ( 𝑁 · 𝑚 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑖 + ( 𝑁 · 𝑚 ) ) ) ) )
140 fzoval ⊢ ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) ∈ ℤ → ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑘 ) ) = ( ( 𝑁 · 𝑚 ) ... ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − 1 ) ) )
141 131 140 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑘 ) ) = ( ( 𝑁 · 𝑚 ) ... ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − 1 ) ) )
142 141 sumeq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ... ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
143 129 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℤ )
144 fzoval ⊢ ( 𝑘 ∈ ℤ → ( 0 ..^ 𝑘 ) = ( 0 ... ( 𝑘 − 1 ) ) )
145 143 144 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 0 ..^ 𝑘 ) = ( 0 ... ( 𝑘 − 1 ) ) )
146 128 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 · 𝑚 ) ∈ ℂ )
147 146 subidd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 · 𝑚 ) − ( 𝑁 · 𝑚 ) ) = 0 )
148 131 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 · 𝑚 ) + 𝑘 ) ∈ ℂ )
149 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 1 ∈ ℂ )
150 148 149 146 sub32d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − 1 ) − ( 𝑁 · 𝑚 ) ) = ( ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − ( 𝑁 · 𝑚 ) ) − 1 ) )
151 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
152 151 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℂ )
153 146 152 pncan2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − ( 𝑁 · 𝑚 ) ) = 𝑘 )
154 153 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − ( 𝑁 · 𝑚 ) ) − 1 ) = ( 𝑘 − 1 ) )
155 150 154 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − 1 ) − ( 𝑁 · 𝑚 ) ) = ( 𝑘 − 1 ) )
156 147 155 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑁 · 𝑚 ) − ( 𝑁 · 𝑚 ) ) ... ( ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − 1 ) − ( 𝑁 · 𝑚 ) ) ) = ( 0 ... ( 𝑘 − 1 ) ) )
157 145 156 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 0 ..^ 𝑘 ) = ( ( ( 𝑁 · 𝑚 ) − ( 𝑁 · 𝑚 ) ) ... ( ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − 1 ) − ( 𝑁 · 𝑚 ) ) ) )
158 157 sumeq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → Σ 𝑖 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑖 + ( 𝑁 · 𝑚 ) ) ) ) = Σ 𝑖 ∈ ( ( ( 𝑁 · 𝑚 ) − ( 𝑁 · 𝑚 ) ) ... ( ( ( ( 𝑁 · 𝑚 ) + 𝑘 ) − 1 ) − ( 𝑁 · 𝑚 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑖 + ( 𝑁 · 𝑚 ) ) ) ) )
159 139 142 158 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑖 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑖 + ( 𝑁 · 𝑚 ) ) ) ) )
160 3 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
161 nn0z ⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℤ )
162 dvdsmul1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → 𝑁 ∥ ( 𝑁 · 𝑚 ) )
163 160 161 162 syl2an ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑁 ∥ ( 𝑁 · 𝑚 ) )
164 163 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑘 ) ) → 𝑁 ∥ ( 𝑁 · 𝑚 ) )
165 elfzoelz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑘 ) → 𝑖 ∈ ℤ )
166 165 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑘 ) ) → 𝑖 ∈ ℤ )
167 166 zcnd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑘 ) ) → 𝑖 ∈ ℂ )
168 146 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑘 ) ) → ( 𝑁 · 𝑚 ) ∈ ℂ )
169 167 168 pncan2d ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑘 ) ) → ( ( 𝑖 + ( 𝑁 · 𝑚 ) ) − 𝑖 ) = ( 𝑁 · 𝑚 ) )
170 164 169 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑘 ) ) → 𝑁 ∥ ( ( 𝑖 + ( 𝑁 · 𝑚 ) ) − 𝑖 ) )
171 86 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
172 171 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑘 ) ) → 𝑁 ∈ ℕ0 )
173 zaddcl ⊢ ( ( 𝑖 ∈ ℤ ∧ ( 𝑁 · 𝑚 ) ∈ ℤ ) → ( 𝑖 + ( 𝑁 · 𝑚 ) ) ∈ ℤ )
174 165 128 173 syl2anr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑘 ) ) → ( 𝑖 + ( 𝑁 · 𝑚 ) ) ∈ ℤ )
175 1 2 zndvds ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑖 + ( 𝑁 · 𝑚 ) ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( ( 𝐿 ‘ ( 𝑖 + ( 𝑁 · 𝑚 ) ) ) = ( 𝐿 ‘ 𝑖 ) ↔ 𝑁 ∥ ( ( 𝑖 + ( 𝑁 · 𝑚 ) ) − 𝑖 ) ) )
176 172 174 166 175 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑘 ) ) → ( ( 𝐿 ‘ ( 𝑖 + ( 𝑁 · 𝑚 ) ) ) = ( 𝐿 ‘ 𝑖 ) ↔ 𝑁 ∥ ( ( 𝑖 + ( 𝑁 · 𝑚 ) ) − 𝑖 ) ) )
177 170 176 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑘 ) ) → ( 𝐿 ‘ ( 𝑖 + ( 𝑁 · 𝑚 ) ) ) = ( 𝐿 ‘ 𝑖 ) )
178 177 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑘 ) ) → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑖 + ( 𝑁 · 𝑚 ) ) ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) )
179 178 sumeq2dv ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → Σ 𝑖 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑖 + ( 𝑁 · 𝑚 ) ) ) ) = Σ 𝑖 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) )
180 2fveq3 ⊢ ( 𝑖 = 𝑛 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
181 180 cbvsumv ⊢ Σ 𝑖 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) = Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) )
182 179 181 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → Σ 𝑖 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑖 + ( 𝑁 · 𝑚 ) ) ) ) = Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
183 159 182 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
184 183 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ∀ 𝑘 ∈ ℕ0 Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
185 126 184 171 rspcdva ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
186 fveq2 ⊢ ( 𝑘 = ( 𝐿 ‘ 𝑛 ) → ( 𝑋 ‘ 𝑘 ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
187 3 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
188 ifnefalse ⊢ ( 𝑁 ≠ 0 → if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 ) )
189 187 188 syl ⊢ ( 𝜑 → if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 ) )
190 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
191 189 190 eqeltrdi ⊢ ( 𝜑 → if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ∈ Fin )
192 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
193 2 reseq1i ⊢ ( 𝐿 ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) = ( ( ℤRHom ‘ 𝑍 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) )
194 eqid ⊢ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) )
195 1 192 193 194 znf1o ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐿 ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ ( Base ‘ 𝑍 ) )
196 19 195 syl ⊢ ( 𝜑 → ( 𝐿 ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ ( Base ‘ 𝑍 ) )
197 fvres ⊢ ( 𝑛 ∈ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) → ( ( 𝐿 ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) ‘ 𝑛 ) = ( 𝐿 ‘ 𝑛 ) )
198 197 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) → ( ( 𝐿 ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) ‘ 𝑛 ) = ( 𝐿 ‘ 𝑛 ) )
199 4 1 5 192 7 dchrf ⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ )
200 199 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑋 ‘ 𝑘 ) ∈ ℂ )
201 186 191 196 198 200 fsumf1o ⊢ ( 𝜑 → Σ 𝑘 ∈ ( Base ‘ 𝑍 ) ( 𝑋 ‘ 𝑘 ) = Σ 𝑛 ∈ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
202 4 1 5 6 7 192 dchrsum ⊢ ( 𝜑 → Σ 𝑘 ∈ ( Base ‘ 𝑍 ) ( 𝑋 ‘ 𝑘 ) = if ( 𝑋 = 1 , ( ϕ ‘ 𝑁 ) , 0 ) )
203 ifnefalse ⊢ ( 𝑋 ≠ 1 → if ( 𝑋 = 1 , ( ϕ ‘ 𝑁 ) , 0 ) = 0 )
204 8 203 syl ⊢ ( 𝜑 → if ( 𝑋 = 1 , ( ϕ ‘ 𝑁 ) , 0 ) = 0 )
205 202 204 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( Base ‘ 𝑍 ) ( 𝑋 ‘ 𝑘 ) = 0 )
206 189 sumeq1d ⊢ ( 𝜑 → Σ 𝑛 ∈ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
207 201 205 206 3eqtr3rd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 )
208 207 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → Σ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 )
209 120 185 208 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 )
210 209 oveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 0 + Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) = ( 0 + 0 ) )
211 00id ⊢ ( 0 + 0 ) = 0
212 210 211 eqtr2di ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 0 = ( 0 + Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
213 111 212 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ↔ ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑚 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) = ( 0 + Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) )
214 78 213 imbitrrid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑚 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) )
215 214 expcom ⊢ ( 𝑚 ∈ ℕ0 → ( 𝜑 → ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑚 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) ) )
216 215 a2d ⊢ ( 𝑚 ∈ ℕ0 → ( ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · 𝑚 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) → ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( 𝑚 + 1 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) ) )
217 54 59 64 69 77 216 nn0ind ⊢ ( ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ∈ ℕ0 → ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) )
218 217 impcom ⊢ ( ( 𝜑 ∧ ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ∈ ℕ0 ) → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 )
219 30 218 syldan ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 )
220 modval ⊢ ( ( 𝑈 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( 𝑈 mod 𝑁 ) = ( 𝑈 − ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ) )
221 22 25 220 syl2anc ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( 𝑈 mod 𝑁 ) = ( 𝑈 − ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ) )
222 221 oveq2d ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + ( 𝑈 mod 𝑁 ) ) = ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + ( 𝑈 − ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ) ) )
223 31 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ∈ ℂ )
224 nn0cn ⊢ ( 𝑈 ∈ ℕ0 → 𝑈 ∈ ℂ )
225 224 adantl ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → 𝑈 ∈ ℂ )
226 223 225 pncan3d ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + ( 𝑈 − ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ) ) = 𝑈 )
227 222 226 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → 𝑈 = ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + ( 𝑈 mod 𝑁 ) ) )
228 227 oveq2d ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ 𝑈 ) = ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + ( 𝑈 mod 𝑁 ) ) ) )
229 228 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → Σ 𝑛 ∈ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ 𝑈 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + ( 𝑈 mod 𝑁 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
230 nn0z ⊢ ( 𝑈 ∈ ℕ0 → 𝑈 ∈ ℤ )
231 zmodcl ⊢ ( ( 𝑈 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑈 mod 𝑁 ) ∈ ℕ0 )
232 230 3 231 syl2anr ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( 𝑈 mod 𝑁 ) ∈ ℕ0 )
233 184 ralrimiva ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ0 ∀ 𝑘 ∈ ℕ0 Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
234 233 adantr ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ∀ 𝑚 ∈ ℕ0 ∀ 𝑘 ∈ ℕ0 Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
235 oveq2 ⊢ ( 𝑚 = ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) → ( 𝑁 · 𝑚 ) = ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) )
236 235 oveq1d ⊢ ( 𝑚 = ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) → ( ( 𝑁 · 𝑚 ) + 𝑘 ) = ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + 𝑘 ) )
237 235 236 oveq12d ⊢ ( 𝑚 = ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) → ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑘 ) ) = ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + 𝑘 ) ) )
238 237 sumeq1d ⊢ ( 𝑚 = ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) → Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
239 238 eqeq1d ⊢ ( 𝑚 = ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) → ( Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ↔ Σ 𝑛 ∈ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
240 oveq2 ⊢ ( 𝑘 = ( 𝑈 mod 𝑁 ) → ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + 𝑘 ) = ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + ( 𝑈 mod 𝑁 ) ) )
241 240 oveq2d ⊢ ( 𝑘 = ( 𝑈 mod 𝑁 ) → ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + 𝑘 ) ) = ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + ( 𝑈 mod 𝑁 ) ) ) )
242 241 sumeq1d ⊢ ( 𝑘 = ( 𝑈 mod 𝑁 ) → Σ 𝑛 ∈ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + ( 𝑈 mod 𝑁 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
243 oveq2 ⊢ ( 𝑘 = ( 𝑈 mod 𝑁 ) → ( 0 ..^ 𝑘 ) = ( 0 ..^ ( 𝑈 mod 𝑁 ) ) )
244 243 sumeq1d ⊢ ( 𝑘 = ( 𝑈 mod 𝑁 ) → Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
245 242 244 eqeq12d ⊢ ( 𝑘 = ( 𝑈 mod 𝑁 ) → ( Σ 𝑛 ∈ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ↔ Σ 𝑛 ∈ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + ( 𝑈 mod 𝑁 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
246 239 245 rspc2va ⊢ ( ( ( ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ∈ ℕ0 ∧ ( 𝑈 mod 𝑁 ) ∈ ℕ0 ) ∧ ∀ 𝑚 ∈ ℕ0 ∀ 𝑘 ∈ ℕ0 Σ 𝑛 ∈ ( ( 𝑁 · 𝑚 ) ..^ ( ( 𝑁 · 𝑚 ) + 𝑘 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) → Σ 𝑛 ∈ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + ( 𝑈 mod 𝑁 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
247 30 232 234 246 syl21anc ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → Σ 𝑛 ∈ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) + ( 𝑈 mod 𝑁 ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
248 229 247 eqtrd ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → Σ 𝑛 ∈ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ 𝑈 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
249 219 248 oveq12d ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( ( 𝑁 · ( ⌊ ‘ ( 𝑈 / 𝑁 ) ) ) ..^ 𝑈 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) = ( 0 + Σ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
250 fzofi ⊢ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ∈ Fin
251 250 a1i ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ∈ Fin )
252 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ) → 𝑋 ∈ 𝐷 )
253 elfzoelz ⊢ ( 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) → 𝑛 ∈ ℤ )
254 253 adantl ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ) → 𝑛 ∈ ℤ )
255 4 1 5 2 252 254 dchrzrhcl ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
256 251 255 fsumcl ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → Σ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
257 256 addlidd ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( 0 + Σ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
258 49 249 257 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → Σ 𝑛 ∈ ( 0 ..^ 𝑈 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
259 258 fveq2d ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑈 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) = ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
260 oveq2 ⊢ ( 𝑢 = ( 𝑈 mod 𝑁 ) → ( 0 ..^ 𝑢 ) = ( 0 ..^ ( 𝑈 mod 𝑁 ) ) )
261 260 sumeq1d ⊢ ( 𝑢 = ( 𝑈 mod 𝑁 ) → Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
262 261 fveq2d ⊢ ( 𝑢 = ( 𝑈 mod 𝑁 ) → ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) = ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
263 262 breq1d ⊢ ( 𝑢 = ( 𝑈 mod 𝑁 ) → ( ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 ↔ ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 ) )
264 16 adantr ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ∀ 𝑢 ∈ ( 0 ..^ 𝑁 ) ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
265 zmodfzo ⊢ ( ( 𝑈 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑈 mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
266 230 3 265 syl2anr ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( 𝑈 mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
267 263 264 266 rspcdva ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝑈 mod 𝑁 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
268 259 267 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑈 ∈ ℕ0 ) → ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑈 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )