MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrisumlem1 Structured version   Visualization version   GIF version
Theorem dchrisumlem1 26992
Description: Lemma for dchrisum 26995. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.)
Hypotheses
Ref Expression
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
Ref Expression
dchrisumlem1 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
Distinct variable groups:   𝑒,𝑛,π‘₯   1 ,𝑛,π‘₯   𝑛,𝐹,𝑒,π‘₯   π‘₯,𝐴   𝑛,𝑁,𝑒,π‘₯   πœ‘,𝑛,𝑒,π‘₯   𝑅,𝑛,𝑒,π‘₯   π‘ˆ,𝑛,𝑒,π‘₯   𝐡,𝑛   𝑛,𝑍,π‘₯   𝐷,𝑛,π‘₯   𝑛,𝐿,𝑒,π‘₯   𝑛,𝑀,𝑒,π‘₯   𝑛,𝑋,𝑒,π‘₯
Allowed substitution hints:   𝐴(𝑒,𝑛)   𝐡(π‘₯,𝑒)   𝐷(𝑒)   1 (𝑒)   𝐺(π‘₯,𝑒,𝑛)   𝑍(𝑒)
Proof of Theorem dchrisumlem1
Dummy variables π‘˜ π‘š 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzodisj 13666 . . . . . 6 ((0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))) ∩ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)) = βˆ…
21a1i 11 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))) ∩ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)) = βˆ…)
3 rpvmasum.a . . . . . . . . . 10 (πœ‘ β†’ 𝑁 ∈ β„•)
43nnnn0d 12532 . . . . . . . . 9 (πœ‘ β†’ 𝑁 ∈ β„•0)
54adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 𝑁 ∈ β„•0)
6 nn0re 12481 . . . . . . . . . . 11 (π‘ˆ ∈ β„•0 β†’ π‘ˆ ∈ ℝ)
76adantl 483 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ π‘ˆ ∈ ℝ)
83adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 𝑁 ∈ β„•)
97, 8nndivred 12266 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (π‘ˆ / 𝑁) ∈ ℝ)
108nnrpd 13014 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 𝑁 ∈ ℝ+)
11 nn0ge0 12497 . . . . . . . . . . 11 (π‘ˆ ∈ β„•0 β†’ 0 ≀ π‘ˆ)
1211adantl 483 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 0 ≀ π‘ˆ)
137, 10, 12divge0d 13056 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 0 ≀ (π‘ˆ / 𝑁))
14 flge0nn0 13785 . . . . . . . . 9 (((π‘ˆ / 𝑁) ∈ ℝ ∧ 0 ≀ (π‘ˆ / 𝑁)) β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0)
159, 13, 14syl2anc 585 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0)
165, 15nn0mulcld 12537 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ β„•0)
17 flle 13764 . . . . . . . . 9 ((π‘ˆ / 𝑁) ∈ ℝ β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ≀ (π‘ˆ / 𝑁))
189, 17syl 17 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ≀ (π‘ˆ / 𝑁))
19 reflcl 13761 . . . . . . . . . 10 ((π‘ˆ / 𝑁) ∈ ℝ β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ ℝ)
209, 19syl 17 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ ℝ)
2120, 7, 10lemuldiv2d 13066 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ≀ π‘ˆ ↔ (βŒŠβ€˜(π‘ˆ / 𝑁)) ≀ (π‘ˆ / 𝑁)))
2218, 21mpbird 257 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ≀ π‘ˆ)
23 fznn0 13593 . . . . . . . 8 (π‘ˆ ∈ β„•0 β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ (0...π‘ˆ) ↔ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ β„•0 ∧ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ≀ π‘ˆ)))
2423adantl 483 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ (0...π‘ˆ) ↔ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ β„•0 ∧ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ≀ π‘ˆ)))
2516, 22, 24mpbir2and 712 . . . . . 6 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ (0...π‘ˆ))
26 fzosplit 13665 . . . . . 6 ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ (0...π‘ˆ) β†’ (0..^π‘ˆ) = ((0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))) βˆͺ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)))
2725, 26syl 17 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (0..^π‘ˆ) = ((0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))) βˆͺ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)))
28 fzofi 13939 . . . . . 6 (0..^π‘ˆ) ∈ Fin
2928a1i 11 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (0..^π‘ˆ) ∈ Fin)
30 rpvmasum.g . . . . . 6 𝐺 = (DChrβ€˜π‘)
31 rpvmasum.z . . . . . 6 𝑍 = (β„€/nβ„€β€˜π‘)
32 rpvmasum.d . . . . . 6 𝐷 = (Baseβ€˜πΊ)
33 rpvmasum.l . . . . . 6 𝐿 = (β„€RHomβ€˜π‘)
34 dchrisum.b . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ 𝐷)
3534ad2antrr 725 . . . . . 6 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^π‘ˆ)) β†’ 𝑋 ∈ 𝐷)
36 elfzoelz 13632 . . . . . . 7 (𝑛 ∈ (0..^π‘ˆ) β†’ 𝑛 ∈ β„€)
3736adantl 483 . . . . . 6 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^π‘ˆ)) β†’ 𝑛 ∈ β„€)
3830, 31, 32, 33, 35, 37dchrzrhcl 26748 . . . . 5 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^π‘ˆ)) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
392, 27, 29, 38fsumsplit 15687 . . . 4 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ (0..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›)) = (Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›))))
40 oveq2 7417 . . . . . . . . . . . 12 (π‘˜ = 0 β†’ (𝑁 Β· π‘˜) = (𝑁 Β· 0))
4140oveq2d 7425 . . . . . . . . . . 11 (π‘˜ = 0 β†’ (0..^(𝑁 Β· π‘˜)) = (0..^(𝑁 Β· 0)))
4241sumeq1d 15647 . . . . . . . . . 10 (π‘˜ = 0 β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑁 Β· 0))(π‘‹β€˜(πΏβ€˜π‘›)))
4342eqeq1d 2735 . . . . . . . . 9 (π‘˜ = 0 β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 Β· 0))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
4443imbi2d 341 . . . . . . . 8 (π‘˜ = 0 β†’ ((πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0) ↔ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· 0))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
45 oveq2 7417 . . . . . . . . . . . 12 (π‘˜ = π‘š β†’ (𝑁 Β· π‘˜) = (𝑁 Β· π‘š))
4645oveq2d 7425 . . . . . . . . . . 11 (π‘˜ = π‘š β†’ (0..^(𝑁 Β· π‘˜)) = (0..^(𝑁 Β· π‘š)))
4746sumeq1d 15647 . . . . . . . . . 10 (π‘˜ = π‘š β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)))
4847eqeq1d 2735 . . . . . . . . 9 (π‘˜ = π‘š β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
4948imbi2d 341 . . . . . . . 8 (π‘˜ = π‘š β†’ ((πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0) ↔ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
50 oveq2 7417 . . . . . . . . . . . 12 (π‘˜ = (π‘š + 1) β†’ (𝑁 Β· π‘˜) = (𝑁 Β· (π‘š + 1)))
5150oveq2d 7425 . . . . . . . . . . 11 (π‘˜ = (π‘š + 1) β†’ (0..^(𝑁 Β· π‘˜)) = (0..^(𝑁 Β· (π‘š + 1))))
5251sumeq1d 15647 . . . . . . . . . 10 (π‘˜ = (π‘š + 1) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)))
5352eqeq1d 2735 . . . . . . . . 9 (π‘˜ = (π‘š + 1) β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
5453imbi2d 341 . . . . . . . 8 (π‘˜ = (π‘š + 1) β†’ ((πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0) ↔ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
55 oveq2 7417 . . . . . . . . . . . 12 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (𝑁 Β· π‘˜) = (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))
5655oveq2d 7425 . . . . . . . . . . 11 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (0..^(𝑁 Β· π‘˜)) = (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))))
5756sumeq1d 15647 . . . . . . . . . 10 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)))
5857eqeq1d 2735 . . . . . . . . 9 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
5958imbi2d 341 . . . . . . . 8 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ ((πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0) ↔ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
603nncnd 12228 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑁 ∈ β„‚)
6160mul01d 11413 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑁 Β· 0) = 0)
6261oveq2d 7425 . . . . . . . . . . 11 (πœ‘ β†’ (0..^(𝑁 Β· 0)) = (0..^0))
63 fzo0 13656 . . . . . . . . . . 11 (0..^0) = βˆ…
6462, 63eqtrdi 2789 . . . . . . . . . 10 (πœ‘ β†’ (0..^(𝑁 Β· 0)) = βˆ…)
6564sumeq1d 15647 . . . . . . . . 9 (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· 0))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ βˆ… (π‘‹β€˜(πΏβ€˜π‘›)))
66 sum0 15667 . . . . . . . . 9 Σ𝑛 ∈ βˆ… (π‘‹β€˜(πΏβ€˜π‘›)) = 0
6765, 66eqtrdi 2789 . . . . . . . 8 (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· 0))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
68 oveq1 7416 . . . . . . . . . . 11 (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))) = (0 + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))))
69 fzodisj 13666 . . . . . . . . . . . . . 14 ((0..^(𝑁 Β· π‘š)) ∩ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))) = βˆ…
7069a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ ((0..^(𝑁 Β· π‘š)) ∩ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))) = βˆ…)
71 nn0re 12481 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ β„•0 β†’ π‘š ∈ ℝ)
7271adantl 483 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ π‘š ∈ ℝ)
7372lep1d 12145 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ π‘š ≀ (π‘š + 1))
74 peano2re 11387 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ ℝ β†’ (π‘š + 1) ∈ ℝ)
7572, 74syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (π‘š + 1) ∈ ℝ)
763adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 ∈ β„•)
7776nnred 12227 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 ∈ ℝ)
7876nngt0d 12261 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 0 < 𝑁)
79 lemul2 12067 . . . . . . . . . . . . . . . . 17 ((π‘š ∈ ℝ ∧ (π‘š + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) β†’ (π‘š ≀ (π‘š + 1) ↔ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1))))
8072, 75, 77, 78, 79syl112anc 1375 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (π‘š ≀ (π‘š + 1) ↔ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1))))
8173, 80mpbid 231 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1)))
82 nn0mulcl 12508 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ β„•0 ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„•0)
834, 82sylan 581 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„•0)
84 nn0uz 12864 . . . . . . . . . . . . . . . . 17 β„•0 = (β„€β‰₯β€˜0)
8583, 84eleqtrdi 2844 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ (β„€β‰₯β€˜0))
86 nn0p1nn 12511 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ β„•0 β†’ (π‘š + 1) ∈ β„•)
87 nnmulcl 12236 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ β„• ∧ (π‘š + 1) ∈ β„•) β†’ (𝑁 Β· (π‘š + 1)) ∈ β„•)
883, 86, 87syl2an 597 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· (π‘š + 1)) ∈ β„•)
8988nnzd 12585 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· (π‘š + 1)) ∈ β„€)
90 elfz5 13493 . . . . . . . . . . . . . . . 16 (((𝑁 Β· π‘š) ∈ (β„€β‰₯β€˜0) ∧ (𝑁 Β· (π‘š + 1)) ∈ β„€) β†’ ((𝑁 Β· π‘š) ∈ (0...(𝑁 Β· (π‘š + 1))) ↔ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1))))
9185, 89, 90syl2anc 585 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ ((𝑁 Β· π‘š) ∈ (0...(𝑁 Β· (π‘š + 1))) ↔ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1))))
9281, 91mpbird 257 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ (0...(𝑁 Β· (π‘š + 1))))
93 fzosplit 13665 . . . . . . . . . . . . . 14 ((𝑁 Β· π‘š) ∈ (0...(𝑁 Β· (π‘š + 1))) β†’ (0..^(𝑁 Β· (π‘š + 1))) = ((0..^(𝑁 Β· π‘š)) βˆͺ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))))
9492, 93syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (0..^(𝑁 Β· (π‘š + 1))) = ((0..^(𝑁 Β· π‘š)) βˆͺ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))))
95 fzofi 13939 . . . . . . . . . . . . . 14 (0..^(𝑁 Β· (π‘š + 1))) ∈ Fin
9695a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (0..^(𝑁 Β· (π‘š + 1))) ∈ Fin)
9734ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ 𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))) β†’ 𝑋 ∈ 𝐷)
98 elfzoelz 13632 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1))) β†’ 𝑛 ∈ β„€)
9998adantl 483 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ 𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))) β†’ 𝑛 ∈ β„€)
10030, 31, 32, 33, 97, 99dchrzrhcl 26748 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ 𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
10170, 94, 96, 100fsumsplit 15687 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))))
10276nncnd 12228 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 ∈ β„‚)
10372recnd 11242 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ π‘š ∈ β„‚)
104 1cnd 11209 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 1 ∈ β„‚)
105102, 103, 104adddid 11238 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· (π‘š + 1)) = ((𝑁 Β· π‘š) + (𝑁 Β· 1)))
106102mulridd 11231 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· 1) = 𝑁)
107106oveq2d 7425 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ ((𝑁 Β· π‘š) + (𝑁 Β· 1)) = ((𝑁 Β· π‘š) + 𝑁))
108105, 107eqtrd 2773 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· (π‘š + 1)) = ((𝑁 Β· π‘š) + 𝑁))
109108oveq2d 7425 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1))) = ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁)))
110109sumeq1d 15647 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
111 oveq2 7417 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑁 β†’ ((𝑁 Β· π‘š) + π‘˜) = ((𝑁 Β· π‘š) + 𝑁))
112111oveq2d 7425 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑁 β†’ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜)) = ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁)))
113112sumeq1d 15647 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑁 β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
114 oveq2 7417 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑁 β†’ (0..^π‘˜) = (0..^𝑁))
115114sumeq1d 15647 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑁 β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›)))
116113, 115eqeq12d 2749 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑁 β†’ (Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) ↔ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›))))
11783nn0zd 12584 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„€)
118117adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„€)
119 nn0z 12583 . . . . . . . . . . . . . . . . . . . . . 22 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„€)
120 zaddcl 12602 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 Β· π‘š) ∈ β„€ ∧ π‘˜ ∈ β„€) β†’ ((𝑁 Β· π‘š) + π‘˜) ∈ β„€)
121117, 119, 120syl2an 597 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((𝑁 Β· π‘š) + π‘˜) ∈ β„€)
122 peano2zm 12605 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 Β· π‘š) + π‘˜) ∈ β„€ β†’ (((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) ∈ β„€)
123121, 122syl 17 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) ∈ β„€)
12434ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))) β†’ 𝑋 ∈ 𝐷)
125 elfzelz 13501 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1)) β†’ 𝑛 ∈ β„€)
126125adantl 483 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))) β†’ 𝑛 ∈ β„€)
12730, 31, 32, 33, 124, 126dchrzrhcl 26748 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
128 2fveq3 6897 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = (𝑖 + (𝑁 Β· π‘š)) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) = (π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))))
129118, 118, 123, 127, 128fsumshftm 15727 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑖 ∈ (((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š))...((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š)))(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))))
130 fzoval 13633 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 Β· π‘š) + π‘˜) ∈ β„€ β†’ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜)) = ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1)))
131121, 130syl 17 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜)) = ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1)))
132131sumeq1d 15647 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))(π‘‹β€˜(πΏβ€˜π‘›)))
133119adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„€)
134 fzoval 13633 . . . . . . . . . . . . . . . . . . . . . 22 (π‘˜ ∈ β„€ β†’ (0..^π‘˜) = (0...(π‘˜ βˆ’ 1)))
135133, 134syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (0..^π‘˜) = (0...(π‘˜ βˆ’ 1)))
136118zcnd 12667 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„‚)
137136subidd 11559 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š)) = 0)
138121zcnd 12667 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((𝑁 Β· π‘š) + π‘˜) ∈ β„‚)
139 1cnd 11209 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ 1 ∈ β„‚)
140138, 139, 136sub32d 11603 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š)) = ((((𝑁 Β· π‘š) + π‘˜) βˆ’ (𝑁 Β· π‘š)) βˆ’ 1))
141 nn0cn 12482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„‚)
142141adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„‚)
143136, 142pncan2d 11573 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (((𝑁 Β· π‘š) + π‘˜) βˆ’ (𝑁 Β· π‘š)) = π‘˜)
144143oveq1d 7424 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((((𝑁 Β· π‘š) + π‘˜) βˆ’ (𝑁 Β· π‘š)) βˆ’ 1) = (π‘˜ βˆ’ 1))
145140, 144eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š)) = (π‘˜ βˆ’ 1))
146137, 145oveq12d 7427 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š))...((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š))) = (0...(π‘˜ βˆ’ 1)))
147135, 146eqtr4d 2776 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (0..^π‘˜) = (((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š))...((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š))))
148147sumeq1d 15647 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))) = Σ𝑖 ∈ (((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š))...((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š)))(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))))
149129, 132, 1483eqtr4d 2783 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))))
1503nnzd 12585 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝑁 ∈ β„€)
151 nn0z 12583 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘š ∈ β„•0 β†’ π‘š ∈ β„€)
152 dvdsmul1 16221 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 ∈ β„€ ∧ π‘š ∈ β„€) β†’ 𝑁 βˆ₯ (𝑁 Β· π‘š))
153150, 151, 152syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 βˆ₯ (𝑁 Β· π‘š))
154153ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑁 βˆ₯ (𝑁 Β· π‘š))
155 elfzoelz 13632 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^π‘˜) β†’ 𝑖 ∈ β„€)
156155adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑖 ∈ β„€)
157156zcnd 12667 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑖 ∈ β„‚)
158136adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (𝑁 Β· π‘š) ∈ β„‚)
159157, 158pncan2d 11573 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ ((𝑖 + (𝑁 Β· π‘š)) βˆ’ 𝑖) = (𝑁 Β· π‘š))
160154, 159breqtrrd 5177 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑁 βˆ₯ ((𝑖 + (𝑁 Β· π‘š)) βˆ’ 𝑖))
16176nnnn0d 12532 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 ∈ β„•0)
162161ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑁 ∈ β„•0)
163 zaddcl 12602 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ β„€ ∧ (𝑁 Β· π‘š) ∈ β„€) β†’ (𝑖 + (𝑁 Β· π‘š)) ∈ β„€)
164155, 118, 163syl2anr 598 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (𝑖 + (𝑁 Β· π‘š)) ∈ β„€)
16531, 33zndvds 21105 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ β„•0 ∧ (𝑖 + (𝑁 Β· π‘š)) ∈ β„€ ∧ 𝑖 ∈ β„€) β†’ ((πΏβ€˜(𝑖 + (𝑁 Β· π‘š))) = (πΏβ€˜π‘–) ↔ 𝑁 βˆ₯ ((𝑖 + (𝑁 Β· π‘š)) βˆ’ 𝑖)))
166162, 164, 156, 165syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ ((πΏβ€˜(𝑖 + (𝑁 Β· π‘š))) = (πΏβ€˜π‘–) ↔ 𝑁 βˆ₯ ((𝑖 + (𝑁 Β· π‘š)) βˆ’ 𝑖)))
167160, 166mpbird 257 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (πΏβ€˜(𝑖 + (𝑁 Β· π‘š))) = (πΏβ€˜π‘–))
168167fveq2d 6896 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))) = (π‘‹β€˜(πΏβ€˜π‘–)))
169168sumeq2dv 15649 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))) = Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘–)))
170 2fveq3 6897 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑛 β†’ (π‘‹β€˜(πΏβ€˜π‘–)) = (π‘‹β€˜(πΏβ€˜π‘›)))
171170cbvsumv 15642 . . . . . . . . . . . . . . . . . . 19 Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘–)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›))
172169, 171eqtrdi 2789 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)))
173149, 172eqtrd 2773 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)))
174173ralrimiva 3147 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ βˆ€π‘˜ ∈ β„•0 Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)))
175116, 174, 161rspcdva 3614 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›)))
176 fveq2 6892 . . . . . . . . . . . . . . . . . 18 (π‘˜ = (πΏβ€˜π‘›) β†’ (π‘‹β€˜π‘˜) = (π‘‹β€˜(πΏβ€˜π‘›)))
1773nnne0d 12262 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝑁 β‰  0)
178 ifnefalse 4541 . . . . . . . . . . . . . . . . . . . 20 (𝑁 β‰  0 β†’ if(𝑁 = 0, β„€, (0..^𝑁)) = (0..^𝑁))
179177, 178syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ if(𝑁 = 0, β„€, (0..^𝑁)) = (0..^𝑁))
180 fzofi 13939 . . . . . . . . . . . . . . . . . . 19 (0..^𝑁) ∈ Fin
181179, 180eqeltrdi 2842 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ if(𝑁 = 0, β„€, (0..^𝑁)) ∈ Fin)
182 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (Baseβ€˜π‘) = (Baseβ€˜π‘)
18333reseq1i 5978 . . . . . . . . . . . . . . . . . . . 20 (𝐿 β†Ύ if(𝑁 = 0, β„€, (0..^𝑁))) = ((β„€RHomβ€˜π‘) β†Ύ if(𝑁 = 0, β„€, (0..^𝑁)))
184 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 if(𝑁 = 0, β„€, (0..^𝑁)) = if(𝑁 = 0, β„€, (0..^𝑁))
18531, 182, 183, 184znf1o 21107 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ β„•0 β†’ (𝐿 β†Ύ if(𝑁 = 0, β„€, (0..^𝑁))):if(𝑁 = 0, β„€, (0..^𝑁))–1-1-ontoβ†’(Baseβ€˜π‘))
1864, 185syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐿 β†Ύ if(𝑁 = 0, β„€, (0..^𝑁))):if(𝑁 = 0, β„€, (0..^𝑁))–1-1-ontoβ†’(Baseβ€˜π‘))
187 fvres 6911 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ if(𝑁 = 0, β„€, (0..^𝑁)) β†’ ((𝐿 β†Ύ if(𝑁 = 0, β„€, (0..^𝑁)))β€˜π‘›) = (πΏβ€˜π‘›))
188187adantl 483 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ if(𝑁 = 0, β„€, (0..^𝑁))) β†’ ((𝐿 β†Ύ if(𝑁 = 0, β„€, (0..^𝑁)))β€˜π‘›) = (πΏβ€˜π‘›))
18930, 31, 32, 182, 34dchrf 26745 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋:(Baseβ€˜π‘)βŸΆβ„‚)
190189ffvelcdmda 7087 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ (Baseβ€˜π‘)) β†’ (π‘‹β€˜π‘˜) ∈ β„‚)
191176, 181, 186, 188, 190fsumf1o 15669 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ Ξ£π‘˜ ∈ (Baseβ€˜π‘)(π‘‹β€˜π‘˜) = Σ𝑛 ∈ if (𝑁 = 0, β„€, (0..^𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
192 rpvmasum.1 . . . . . . . . . . . . . . . . . . 19 1 = (0gβ€˜πΊ)
19330, 31, 32, 192, 34, 182dchrsum 26772 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ Ξ£π‘˜ ∈ (Baseβ€˜π‘)(π‘‹β€˜π‘˜) = if(𝑋 = 1 , (Ο•β€˜π‘), 0))
194 dchrisum.n1 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋 β‰  1 )
195 ifnefalse 4541 . . . . . . . . . . . . . . . . . . 19 (𝑋 β‰  1 β†’ if(𝑋 = 1 , (Ο•β€˜π‘), 0) = 0)
196194, 195syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ if(𝑋 = 1 , (Ο•β€˜π‘), 0) = 0)
197193, 196eqtrd 2773 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ Ξ£π‘˜ ∈ (Baseβ€˜π‘)(π‘‹β€˜π‘˜) = 0)
198179sumeq1d 15647 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ Σ𝑛 ∈ if (𝑁 = 0, β„€, (0..^𝑁))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›)))
199191, 197, 1983eqtr3rd 2782 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
200199adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
201110, 175, 2003eqtrd 2777 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
202201oveq2d 7425 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (0 + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))) = (0 + 0))
203 00id 11389 . . . . . . . . . . . . 13 (0 + 0) = 0
204202, 203eqtr2di 2790 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 0 = (0 + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))))
205101, 204eqeq12d 2749 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 ↔ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))) = (0 + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)))))
20668, 205imbitrrid 245 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
207206expcom 415 . . . . . . . . 9 (π‘š ∈ β„•0 β†’ (πœ‘ β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
208207a2d 29 . . . . . . . 8 (π‘š ∈ β„•0 β†’ ((πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0) β†’ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
20944, 49, 54, 59, 67, 208nn0ind 12657 . . . . . . 7 ((βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0 β†’ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
210209impcom 409 . . . . . 6 ((πœ‘ ∧ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
21115, 210syldan 592 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
212 modval 13836 . . . . . . . . . . 11 ((π‘ˆ ∈ ℝ ∧ 𝑁 ∈ ℝ+) β†’ (π‘ˆ mod 𝑁) = (π‘ˆ βˆ’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))))
2137, 10, 212syl2anc 585 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (π‘ˆ mod 𝑁) = (π‘ˆ βˆ’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))))
214213oveq2d 7425 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ βˆ’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))))
21516nn0cnd 12534 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ β„‚)
216 nn0cn 12482 . . . . . . . . . . 11 (π‘ˆ ∈ β„•0 β†’ π‘ˆ ∈ β„‚)
217216adantl 483 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ π‘ˆ ∈ β„‚)
218215, 217pncan3d 11574 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ βˆ’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))) = π‘ˆ)
219214, 218eqtr2d 2774 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ π‘ˆ = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))
220219oveq2d 7425 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁))))
221220sumeq1d 15647 . . . . . 6 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)))
222 nn0z 12583 . . . . . . . 8 (π‘ˆ ∈ β„•0 β†’ π‘ˆ ∈ β„€)
223 zmodcl 13856 . . . . . . . 8 ((π‘ˆ ∈ β„€ ∧ 𝑁 ∈ β„•) β†’ (π‘ˆ mod 𝑁) ∈ β„•0)
224222, 3, 223syl2anr 598 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (π‘ˆ mod 𝑁) ∈ β„•0)
225174ralrimiva 3147 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘š ∈ β„•0 βˆ€π‘˜ ∈ β„•0 Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)))
226225adantr 482 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ βˆ€π‘š ∈ β„•0 βˆ€π‘˜ ∈ β„•0 Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)))
227 oveq2 7417 . . . . . . . . . . 11 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (𝑁 Β· π‘š) = (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))
228227oveq1d 7424 . . . . . . . . . . 11 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ ((𝑁 Β· π‘š) + π‘˜) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))
229227, 228oveq12d 7427 . . . . . . . . . 10 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜)) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜)))
230229sumeq1d 15647 . . . . . . . . 9 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)))
231230eqeq1d 2735 . . . . . . . 8 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) ↔ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›))))
232 oveq2 7417 . . . . . . . . . . 11 (π‘˜ = (π‘ˆ mod 𝑁) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))
233232oveq2d 7425 . . . . . . . . . 10 (π‘˜ = (π‘ˆ mod 𝑁) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜)) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁))))
234233sumeq1d 15647 . . . . . . . . 9 (π‘˜ = (π‘ˆ mod 𝑁) β†’ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)))
235 oveq2 7417 . . . . . . . . . 10 (π‘˜ = (π‘ˆ mod 𝑁) β†’ (0..^π‘˜) = (0..^(π‘ˆ mod 𝑁)))
236235sumeq1d 15647 . . . . . . . . 9 (π‘˜ = (π‘ˆ mod 𝑁) β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
237234, 236eqeq12d 2749 . . . . . . . 8 (π‘˜ = (π‘ˆ mod 𝑁) β†’ (Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) ↔ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))))
238231, 237rspc2va 3624 . . . . . . 7 ((((βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0 ∧ (π‘ˆ mod 𝑁) ∈ β„•0) ∧ βˆ€π‘š ∈ β„•0 βˆ€π‘˜ ∈ β„•0 Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›))) β†’ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
23915, 224, 226, 238syl21anc 837 . . . . . 6 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
240221, 239eqtrd 2773 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
241211, 240oveq12d 7427 . . . 4 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›))) = (0 + Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))))
242 fzofi 13939 . . . . . . 7 (0..^(π‘ˆ mod 𝑁)) ∈ Fin
243242a1i 11 . . . . . 6 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (0..^(π‘ˆ mod 𝑁)) ∈ Fin)
24434ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^(π‘ˆ mod 𝑁))) β†’ 𝑋 ∈ 𝐷)
245 elfzoelz 13632 . . . . . . . 8 (𝑛 ∈ (0..^(π‘ˆ mod 𝑁)) β†’ 𝑛 ∈ β„€)
246245adantl 483 . . . . . . 7 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^(π‘ˆ mod 𝑁))) β†’ 𝑛 ∈ β„€)
24730, 31, 32, 33, 244, 246dchrzrhcl 26748 . . . . . 6 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^(π‘ˆ mod 𝑁))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
248243, 247fsumcl 15679 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
249248addlidd 11415 . . . 4 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (0 + Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
25039, 241, 2493eqtrd 2777 . . 3 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ (0..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
251250fveq2d 6896 . 2 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›))) = (absβ€˜Ξ£π‘› ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))))
252 oveq2 7417 . . . . . 6 (𝑒 = (π‘ˆ mod 𝑁) β†’ (0..^𝑒) = (0..^(π‘ˆ mod 𝑁)))
253252sumeq1d 15647 . . . . 5 (𝑒 = (π‘ˆ mod 𝑁) β†’ Σ𝑛 ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
254253fveq2d 6896 . . . 4 (𝑒 = (π‘ˆ mod 𝑁) β†’ (absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) = (absβ€˜Ξ£π‘› ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))))
255254breq1d 5159 . . 3 (𝑒 = (π‘ˆ mod 𝑁) β†’ ((absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅 ↔ (absβ€˜Ξ£π‘› ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅))
256 dchrisum.10 . . . 4 (πœ‘ β†’ βˆ€π‘’ ∈ (0..^𝑁)(absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
257256adantr 482 . . 3 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ βˆ€π‘’ ∈ (0..^𝑁)(absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
258 zmodfzo 13859 . . . 4 ((π‘ˆ ∈ β„€ ∧ 𝑁 ∈ β„•) β†’ (π‘ˆ mod 𝑁) ∈ (0..^𝑁))
259222, 3, 258syl2anr 598 . . 3 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (π‘ˆ mod 𝑁) ∈ (0..^𝑁))
260255, 257, 259rspcdva 3614 . 2 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
261251, 260eqbrtrd 5171 1 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062   βˆͺ cun 3947   ∩ cin 3948  βˆ…c0 4323  ifcif 4529   class class class wbr 5149   ↦ cmpt 5232   β†Ύ cres 5679  β€“1-1-ontoβ†’wf1o 6543  β€˜cfv 6544  (class class class)co 7409  Fincfn 8939  β„‚cc 11108  β„cr 11109  0cc0 11110  1c1 11111   + caddc 11113   Β· cmul 11115   < clt 11248   ≀ cle 11249   βˆ’ cmin 11444   / cdiv 11871  β„•cn 12212  β„•0cn0 12472  β„€cz 12558  β„€β‰₯cuz 12822  β„+crp 12974  ...cfz 13484  ..^cfzo 13627  βŒŠcfl 13755   mod cmo 13834  abscabs 15181   β‡π‘Ÿ crli 15429  Ξ£csu 15632   βˆ₯ cdvds 16197  Ο•cphi 16697  Basecbs 17144  0gc0g 17385  β„€RHomczrh 21049  β„€/nβ„€czn 21052  DChrcdchr 26735
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188  ax-addf 11189  ax-mulf 11190
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-of 7670  df-om 7856  df-1st 7975  df-2nd 7976  df-tpos 8211  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-oadd 8470  df-er 8703  df-ec 8705  df-qs 8709  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-sup 9437  df-inf 9438  df-oi 9505  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-xnn0 12545  df-z 12559  df-dec 12678  df-uz 12823  df-rp 12975  df-fz 13485  df-fzo 13628  df-fl 13757  df-mod 13835  df-seq 13967  df-exp 14028  df-hash 14291  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-clim 15432  df-sum 15633  df-dvds 16198  df-gcd 16436  df-phi 16699  df-struct 17080  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-ress 17174  df-plusg 17210  df-mulr 17211  df-starv 17212  df-sca 17213  df-vsca 17214  df-ip 17215  df-tset 17216  df-ple 17217  df-ds 17219  df-unif 17220  df-0g 17387  df-imas 17454  df-qus 17455  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-mhm 18671  df-grp 18822  df-minusg 18823  df-sbg 18824  df-mulg 18951  df-subg 19003  df-nsg 19004  df-eqg 19005  df-ghm 19090  df-cmn 19650  df-abl 19651  df-mgp 19988  df-ur 20005  df-ring 20058  df-cring 20059  df-oppr 20150  df-dvdsr 20171  df-unit 20172  df-invr 20202  df-rnghom 20251  df-subrg 20317  df-lmod 20473  df-lss 20543  df-lsp 20583  df-sra 20785  df-rgmod 20786  df-lidl 20787  df-rsp 20788  df-2idl 20857  df-cnfld 20945  df-zring 21018  df-zrh 21053  df-zn 21056  df-dchr 26736
This theorem is referenced by:  dchrisumlem2  26993
  Copyright terms: Public domain W3C validator