MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrisumlem1 Structured version   Visualization version   GIF version
Theorem dchrisumlem1 26972
Description: Lemma for dchrisum 26975. 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 13662 . . . . . 6 ((0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))) ∩ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)) = βˆ…
21a1i 11 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))) ∩ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)) = βˆ…)
3 rpvmasum.a . . . . . . . . . 10 (πœ‘ β†’ 𝑁 ∈ β„•)
43nnnn0d 12528 . . . . . . . . 9 (πœ‘ β†’ 𝑁 ∈ β„•0)
54adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 𝑁 ∈ β„•0)
6 nn0re 12477 . . . . . . . . . . 11 (π‘ˆ ∈ β„•0 β†’ π‘ˆ ∈ ℝ)
76adantl 483 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ π‘ˆ ∈ ℝ)
83adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 𝑁 ∈ β„•)
97, 8nndivred 12262 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (π‘ˆ / 𝑁) ∈ ℝ)
108nnrpd 13010 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 𝑁 ∈ ℝ+)
11 nn0ge0 12493 . . . . . . . . . . 11 (π‘ˆ ∈ β„•0 β†’ 0 ≀ π‘ˆ)
1211adantl 483 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 0 ≀ π‘ˆ)
137, 10, 12divge0d 13052 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 0 ≀ (π‘ˆ / 𝑁))
14 flge0nn0 13781 . . . . . . . . 9 (((π‘ˆ / 𝑁) ∈ ℝ ∧ 0 ≀ (π‘ˆ / 𝑁)) β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0)
159, 13, 14syl2anc 585 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0)
165, 15nn0mulcld 12533 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ β„•0)
17 flle 13760 . . . . . . . . 9 ((π‘ˆ / 𝑁) ∈ ℝ β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ≀ (π‘ˆ / 𝑁))
189, 17syl 17 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ≀ (π‘ˆ / 𝑁))
19 reflcl 13757 . . . . . . . . . 10 ((π‘ˆ / 𝑁) ∈ ℝ β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ ℝ)
209, 19syl 17 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ ℝ)
2120, 7, 10lemuldiv2d 13062 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ≀ π‘ˆ ↔ (βŒŠβ€˜(π‘ˆ / 𝑁)) ≀ (π‘ˆ / 𝑁)))
2218, 21mpbird 257 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ≀ π‘ˆ)
23 fznn0 13589 . . . . . . . 8 (π‘ˆ ∈ β„•0 β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ (0...π‘ˆ) ↔ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ β„•0 ∧ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ≀ π‘ˆ)))
2423adantl 483 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ (0...π‘ˆ) ↔ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ β„•0 ∧ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ≀ π‘ˆ)))
2516, 22, 24mpbir2and 712 . . . . . 6 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ (0...π‘ˆ))
26 fzosplit 13661 . . . . . 6 ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ (0...π‘ˆ) β†’ (0..^π‘ˆ) = ((0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))) βˆͺ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)))
2725, 26syl 17 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (0..^π‘ˆ) = ((0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))) βˆͺ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)))
28 fzofi 13935 . . . . . 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 13628 . . . . . . 7 (𝑛 ∈ (0..^π‘ˆ) β†’ 𝑛 ∈ β„€)
3736adantl 483 . . . . . 6 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^π‘ˆ)) β†’ 𝑛 ∈ β„€)
3830, 31, 32, 33, 35, 37dchrzrhcl 26728 . . . . 5 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^π‘ˆ)) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
392, 27, 29, 38fsumsplit 15683 . . . 4 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ (0..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›)) = (Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›))))
40 oveq2 7412 . . . . . . . . . . . 12 (π‘˜ = 0 β†’ (𝑁 Β· π‘˜) = (𝑁 Β· 0))
4140oveq2d 7420 . . . . . . . . . . 11 (π‘˜ = 0 β†’ (0..^(𝑁 Β· π‘˜)) = (0..^(𝑁 Β· 0)))
4241sumeq1d 15643 . . . . . . . . . 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 7412 . . . . . . . . . . . 12 (π‘˜ = π‘š β†’ (𝑁 Β· π‘˜) = (𝑁 Β· π‘š))
4645oveq2d 7420 . . . . . . . . . . 11 (π‘˜ = π‘š β†’ (0..^(𝑁 Β· π‘˜)) = (0..^(𝑁 Β· π‘š)))
4746sumeq1d 15643 . . . . . . . . . 10 (π‘˜ = π‘š β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)))
4847eqeq1d 2735 . . . . . . . . 9 (π‘˜ = π‘š β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
4948imbi2d 341 . . . . . . . 8 (π‘˜ = π‘š β†’ ((πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0) ↔ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
50 oveq2 7412 . . . . . . . . . . . 12 (π‘˜ = (π‘š + 1) β†’ (𝑁 Β· π‘˜) = (𝑁 Β· (π‘š + 1)))
5150oveq2d 7420 . . . . . . . . . . 11 (π‘˜ = (π‘š + 1) β†’ (0..^(𝑁 Β· π‘˜)) = (0..^(𝑁 Β· (π‘š + 1))))
5251sumeq1d 15643 . . . . . . . . . 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 7412 . . . . . . . . . . . 12 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (𝑁 Β· π‘˜) = (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))
5655oveq2d 7420 . . . . . . . . . . 11 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (0..^(𝑁 Β· π‘˜)) = (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))))
5756sumeq1d 15643 . . . . . . . . . 10 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)))
5857eqeq1d 2735 . . . . . . . . 9 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
5958imbi2d 341 . . . . . . . 8 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ ((πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0) ↔ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
603nncnd 12224 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑁 ∈ β„‚)
6160mul01d 11409 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑁 Β· 0) = 0)
6261oveq2d 7420 . . . . . . . . . . 11 (πœ‘ β†’ (0..^(𝑁 Β· 0)) = (0..^0))
63 fzo0 13652 . . . . . . . . . . 11 (0..^0) = βˆ…
6462, 63eqtrdi 2789 . . . . . . . . . 10 (πœ‘ β†’ (0..^(𝑁 Β· 0)) = βˆ…)
6564sumeq1d 15643 . . . . . . . . 9 (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· 0))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ βˆ… (π‘‹β€˜(πΏβ€˜π‘›)))
66 sum0 15663 . . . . . . . . 9 Σ𝑛 ∈ βˆ… (π‘‹β€˜(πΏβ€˜π‘›)) = 0
6765, 66eqtrdi 2789 . . . . . . . 8 (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· 0))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
68 oveq1 7411 . . . . . . . . . . 11 (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))) = (0 + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))))
69 fzodisj 13662 . . . . . . . . . . . . . 14 ((0..^(𝑁 Β· π‘š)) ∩ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))) = βˆ…
7069a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ ((0..^(𝑁 Β· π‘š)) ∩ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))) = βˆ…)
71 nn0re 12477 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ β„•0 β†’ π‘š ∈ ℝ)
7271adantl 483 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ π‘š ∈ ℝ)
7372lep1d 12141 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ π‘š ≀ (π‘š + 1))
74 peano2re 11383 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ ℝ β†’ (π‘š + 1) ∈ ℝ)
7572, 74syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (π‘š + 1) ∈ ℝ)
763adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 ∈ β„•)
7776nnred 12223 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 ∈ ℝ)
7876nngt0d 12257 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 0 < 𝑁)
79 lemul2 12063 . . . . . . . . . . . . . . . . 17 ((π‘š ∈ ℝ ∧ (π‘š + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) β†’ (π‘š ≀ (π‘š + 1) ↔ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1))))
8072, 75, 77, 78, 79syl112anc 1375 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (π‘š ≀ (π‘š + 1) ↔ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1))))
8173, 80mpbid 231 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1)))
82 nn0mulcl 12504 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ β„•0 ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„•0)
834, 82sylan 581 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„•0)
84 nn0uz 12860 . . . . . . . . . . . . . . . . 17 β„•0 = (β„€β‰₯β€˜0)
8583, 84eleqtrdi 2844 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ (β„€β‰₯β€˜0))
86 nn0p1nn 12507 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ β„•0 β†’ (π‘š + 1) ∈ β„•)
87 nnmulcl 12232 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ β„• ∧ (π‘š + 1) ∈ β„•) β†’ (𝑁 Β· (π‘š + 1)) ∈ β„•)
883, 86, 87syl2an 597 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· (π‘š + 1)) ∈ β„•)
8988nnzd 12581 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· (π‘š + 1)) ∈ β„€)
90 elfz5 13489 . . . . . . . . . . . . . . . 16 (((𝑁 Β· π‘š) ∈ (β„€β‰₯β€˜0) ∧ (𝑁 Β· (π‘š + 1)) ∈ β„€) β†’ ((𝑁 Β· π‘š) ∈ (0...(𝑁 Β· (π‘š + 1))) ↔ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1))))
9185, 89, 90syl2anc 585 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ ((𝑁 Β· π‘š) ∈ (0...(𝑁 Β· (π‘š + 1))) ↔ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1))))
9281, 91mpbird 257 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ (0...(𝑁 Β· (π‘š + 1))))
93 fzosplit 13661 . . . . . . . . . . . . . 14 ((𝑁 Β· π‘š) ∈ (0...(𝑁 Β· (π‘š + 1))) β†’ (0..^(𝑁 Β· (π‘š + 1))) = ((0..^(𝑁 Β· π‘š)) βˆͺ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))))
9492, 93syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (0..^(𝑁 Β· (π‘š + 1))) = ((0..^(𝑁 Β· π‘š)) βˆͺ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))))
95 fzofi 13935 . . . . . . . . . . . . . 14 (0..^(𝑁 Β· (π‘š + 1))) ∈ Fin
9695a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (0..^(𝑁 Β· (π‘š + 1))) ∈ Fin)
9734ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ 𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))) β†’ 𝑋 ∈ 𝐷)
98 elfzoelz 13628 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1))) β†’ 𝑛 ∈ β„€)
9998adantl 483 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ 𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))) β†’ 𝑛 ∈ β„€)
10030, 31, 32, 33, 97, 99dchrzrhcl 26728 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ 𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
10170, 94, 96, 100fsumsplit 15683 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))))
10276nncnd 12224 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 ∈ β„‚)
10372recnd 11238 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ π‘š ∈ β„‚)
104 1cnd 11205 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 1 ∈ β„‚)
105102, 103, 104adddid 11234 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· (π‘š + 1)) = ((𝑁 Β· π‘š) + (𝑁 Β· 1)))
106102mulridd 11227 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· 1) = 𝑁)
107106oveq2d 7420 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ ((𝑁 Β· π‘š) + (𝑁 Β· 1)) = ((𝑁 Β· π‘š) + 𝑁))
108105, 107eqtrd 2773 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· (π‘š + 1)) = ((𝑁 Β· π‘š) + 𝑁))
109108oveq2d 7420 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1))) = ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁)))
110109sumeq1d 15643 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
111 oveq2 7412 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑁 β†’ ((𝑁 Β· π‘š) + π‘˜) = ((𝑁 Β· π‘š) + 𝑁))
112111oveq2d 7420 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑁 β†’ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜)) = ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁)))
113112sumeq1d 15643 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑁 β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
114 oveq2 7412 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑁 β†’ (0..^π‘˜) = (0..^𝑁))
115114sumeq1d 15643 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑁 β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›)))
116113, 115eqeq12d 2749 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑁 β†’ (Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) ↔ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›))))
11783nn0zd 12580 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„€)
118117adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„€)
119 nn0z 12579 . . . . . . . . . . . . . . . . . . . . . 22 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„€)
120 zaddcl 12598 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 Β· π‘š) ∈ β„€ ∧ π‘˜ ∈ β„€) β†’ ((𝑁 Β· π‘š) + π‘˜) ∈ β„€)
121117, 119, 120syl2an 597 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((𝑁 Β· π‘š) + π‘˜) ∈ β„€)
122 peano2zm 12601 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 Β· π‘š) + π‘˜) ∈ β„€ β†’ (((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) ∈ β„€)
123121, 122syl 17 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) ∈ β„€)
12434ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))) β†’ 𝑋 ∈ 𝐷)
125 elfzelz 13497 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1)) β†’ 𝑛 ∈ β„€)
126125adantl 483 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))) β†’ 𝑛 ∈ β„€)
12730, 31, 32, 33, 124, 126dchrzrhcl 26728 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
128 2fveq3 6893 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = (𝑖 + (𝑁 Β· π‘š)) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) = (π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))))
129118, 118, 123, 127, 128fsumshftm 15723 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑖 ∈ (((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š))...((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š)))(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))))
130 fzoval 13629 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 Β· π‘š) + π‘˜) ∈ β„€ β†’ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜)) = ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1)))
131121, 130syl 17 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜)) = ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1)))
132131sumeq1d 15643 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))(π‘‹β€˜(πΏβ€˜π‘›)))
133119adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„€)
134 fzoval 13629 . . . . . . . . . . . . . . . . . . . . . 22 (π‘˜ ∈ β„€ β†’ (0..^π‘˜) = (0...(π‘˜ βˆ’ 1)))
135133, 134syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (0..^π‘˜) = (0...(π‘˜ βˆ’ 1)))
136118zcnd 12663 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„‚)
137136subidd 11555 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š)) = 0)
138121zcnd 12663 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((𝑁 Β· π‘š) + π‘˜) ∈ β„‚)
139 1cnd 11205 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ 1 ∈ β„‚)
140138, 139, 136sub32d 11599 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š)) = ((((𝑁 Β· π‘š) + π‘˜) βˆ’ (𝑁 Β· π‘š)) βˆ’ 1))
141 nn0cn 12478 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„‚)
142141adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„‚)
143136, 142pncan2d 11569 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (((𝑁 Β· π‘š) + π‘˜) βˆ’ (𝑁 Β· π‘š)) = π‘˜)
144143oveq1d 7419 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((((𝑁 Β· π‘š) + π‘˜) βˆ’ (𝑁 Β· π‘š)) βˆ’ 1) = (π‘˜ βˆ’ 1))
145140, 144eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š)) = (π‘˜ βˆ’ 1))
146137, 145oveq12d 7422 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š))...((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š))) = (0...(π‘˜ βˆ’ 1)))
147135, 146eqtr4d 2776 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (0..^π‘˜) = (((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š))...((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š))))
148147sumeq1d 15643 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))) = Σ𝑖 ∈ (((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š))...((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š)))(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))))
149129, 132, 1483eqtr4d 2783 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))))
1503nnzd 12581 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝑁 ∈ β„€)
151 nn0z 12579 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘š ∈ β„•0 β†’ π‘š ∈ β„€)
152 dvdsmul1 16217 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 ∈ β„€ ∧ π‘š ∈ β„€) β†’ 𝑁 βˆ₯ (𝑁 Β· π‘š))
153150, 151, 152syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 βˆ₯ (𝑁 Β· π‘š))
154153ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑁 βˆ₯ (𝑁 Β· π‘š))
155 elfzoelz 13628 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^π‘˜) β†’ 𝑖 ∈ β„€)
156155adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑖 ∈ β„€)
157156zcnd 12663 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑖 ∈ β„‚)
158136adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (𝑁 Β· π‘š) ∈ β„‚)
159157, 158pncan2d 11569 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ ((𝑖 + (𝑁 Β· π‘š)) βˆ’ 𝑖) = (𝑁 Β· π‘š))
160154, 159breqtrrd 5175 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑁 βˆ₯ ((𝑖 + (𝑁 Β· π‘š)) βˆ’ 𝑖))
16176nnnn0d 12528 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 ∈ β„•0)
162161ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑁 ∈ β„•0)
163 zaddcl 12598 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ β„€ ∧ (𝑁 Β· π‘š) ∈ β„€) β†’ (𝑖 + (𝑁 Β· π‘š)) ∈ β„€)
164155, 118, 163syl2anr 598 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (𝑖 + (𝑁 Β· π‘š)) ∈ β„€)
16531, 33zndvds 21089 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ β„•0 ∧ (𝑖 + (𝑁 Β· π‘š)) ∈ β„€ ∧ 𝑖 ∈ β„€) β†’ ((πΏβ€˜(𝑖 + (𝑁 Β· π‘š))) = (πΏβ€˜π‘–) ↔ 𝑁 βˆ₯ ((𝑖 + (𝑁 Β· π‘š)) βˆ’ 𝑖)))
166162, 164, 156, 165syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ ((πΏβ€˜(𝑖 + (𝑁 Β· π‘š))) = (πΏβ€˜π‘–) ↔ 𝑁 βˆ₯ ((𝑖 + (𝑁 Β· π‘š)) βˆ’ 𝑖)))
167160, 166mpbird 257 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (πΏβ€˜(𝑖 + (𝑁 Β· π‘š))) = (πΏβ€˜π‘–))
168167fveq2d 6892 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))) = (π‘‹β€˜(πΏβ€˜π‘–)))
169168sumeq2dv 15645 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))) = Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘–)))
170 2fveq3 6893 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑛 β†’ (π‘‹β€˜(πΏβ€˜π‘–)) = (π‘‹β€˜(πΏβ€˜π‘›)))
171170cbvsumv 15638 . . . . . . . . . . . . . . . . . . 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 3613 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›)))
176 fveq2 6888 . . . . . . . . . . . . . . . . . 18 (π‘˜ = (πΏβ€˜π‘›) β†’ (π‘‹β€˜π‘˜) = (π‘‹β€˜(πΏβ€˜π‘›)))
1773nnne0d 12258 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝑁 β‰  0)
178 ifnefalse 4539 . . . . . . . . . . . . . . . . . . . 20 (𝑁 β‰  0 β†’ if(𝑁 = 0, β„€, (0..^𝑁)) = (0..^𝑁))
179177, 178syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ if(𝑁 = 0, β„€, (0..^𝑁)) = (0..^𝑁))
180 fzofi 13935 . . . . . . . . . . . . . . . . . . 19 (0..^𝑁) ∈ Fin
181179, 180eqeltrdi 2842 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ if(𝑁 = 0, β„€, (0..^𝑁)) ∈ Fin)
182 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (Baseβ€˜π‘) = (Baseβ€˜π‘)
18333reseq1i 5975 . . . . . . . . . . . . . . . . . . . 20 (𝐿 β†Ύ if(𝑁 = 0, β„€, (0..^𝑁))) = ((β„€RHomβ€˜π‘) β†Ύ if(𝑁 = 0, β„€, (0..^𝑁)))
184 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 if(𝑁 = 0, β„€, (0..^𝑁)) = if(𝑁 = 0, β„€, (0..^𝑁))
18531, 182, 183, 184znf1o 21091 . . . . . . . . . . . . . . . . . . 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 6907 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ if(𝑁 = 0, β„€, (0..^𝑁)) β†’ ((𝐿 β†Ύ if(𝑁 = 0, β„€, (0..^𝑁)))β€˜π‘›) = (πΏβ€˜π‘›))
188187adantl 483 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ if(𝑁 = 0, β„€, (0..^𝑁))) β†’ ((𝐿 β†Ύ if(𝑁 = 0, β„€, (0..^𝑁)))β€˜π‘›) = (πΏβ€˜π‘›))
18930, 31, 32, 182, 34dchrf 26725 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋:(Baseβ€˜π‘)βŸΆβ„‚)
190189ffvelcdmda 7082 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ (Baseβ€˜π‘)) β†’ (π‘‹β€˜π‘˜) ∈ β„‚)
191176, 181, 186, 188, 190fsumf1o 15665 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ Ξ£π‘˜ ∈ (Baseβ€˜π‘)(π‘‹β€˜π‘˜) = Σ𝑛 ∈ if (𝑁 = 0, β„€, (0..^𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
192 rpvmasum.1 . . . . . . . . . . . . . . . . . . 19 1 = (0gβ€˜πΊ)
19330, 31, 32, 192, 34, 182dchrsum 26752 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ Ξ£π‘˜ ∈ (Baseβ€˜π‘)(π‘‹β€˜π‘˜) = if(𝑋 = 1 , (Ο•β€˜π‘), 0))
194 dchrisum.n1 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋 β‰  1 )
195 ifnefalse 4539 . . . . . . . . . . . . . . . . . . 19 (𝑋 β‰  1 β†’ if(𝑋 = 1 , (Ο•β€˜π‘), 0) = 0)
196194, 195syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ if(𝑋 = 1 , (Ο•β€˜π‘), 0) = 0)
197193, 196eqtrd 2773 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ Ξ£π‘˜ ∈ (Baseβ€˜π‘)(π‘‹β€˜π‘˜) = 0)
198179sumeq1d 15643 . . . . . . . . . . . . . . . . 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 7420 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (0 + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))) = (0 + 0))
203 00id 11385 . . . . . . . . . . . . 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 12653 . . . . . . 7 ((βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0 β†’ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
210209impcom 409 . . . . . 6 ((πœ‘ ∧ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
21115, 210syldan 592 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
212 modval 13832 . . . . . . . . . . 11 ((π‘ˆ ∈ ℝ ∧ 𝑁 ∈ ℝ+) β†’ (π‘ˆ mod 𝑁) = (π‘ˆ βˆ’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))))
2137, 10, 212syl2anc 585 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (π‘ˆ mod 𝑁) = (π‘ˆ βˆ’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))))
214213oveq2d 7420 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ βˆ’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))))
21516nn0cnd 12530 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ β„‚)
216 nn0cn 12478 . . . . . . . . . . 11 (π‘ˆ ∈ β„•0 β†’ π‘ˆ ∈ β„‚)
217216adantl 483 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ π‘ˆ ∈ β„‚)
218215, 217pncan3d 11570 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ βˆ’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))) = π‘ˆ)
219214, 218eqtr2d 2774 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ π‘ˆ = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))
220219oveq2d 7420 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁))))
221220sumeq1d 15643 . . . . . 6 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)))
222 nn0z 12579 . . . . . . . 8 (π‘ˆ ∈ β„•0 β†’ π‘ˆ ∈ β„€)
223 zmodcl 13852 . . . . . . . 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 7412 . . . . . . . . . . 11 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (𝑁 Β· π‘š) = (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))
228227oveq1d 7419 . . . . . . . . . . 11 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ ((𝑁 Β· π‘š) + π‘˜) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))
229227, 228oveq12d 7422 . . . . . . . . . 10 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜)) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜)))
230229sumeq1d 15643 . . . . . . . . 9 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)))
231230eqeq1d 2735 . . . . . . . 8 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) ↔ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›))))
232 oveq2 7412 . . . . . . . . . . 11 (π‘˜ = (π‘ˆ mod 𝑁) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))
233232oveq2d 7420 . . . . . . . . . 10 (π‘˜ = (π‘ˆ mod 𝑁) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜)) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁))))
234233sumeq1d 15643 . . . . . . . . 9 (π‘˜ = (π‘ˆ mod 𝑁) β†’ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)))
235 oveq2 7412 . . . . . . . . . 10 (π‘˜ = (π‘ˆ mod 𝑁) β†’ (0..^π‘˜) = (0..^(π‘ˆ mod 𝑁)))
236235sumeq1d 15643 . . . . . . . . 9 (π‘˜ = (π‘ˆ mod 𝑁) β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
237234, 236eqeq12d 2749 . . . . . . . 8 (π‘˜ = (π‘ˆ mod 𝑁) β†’ (Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) ↔ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))))
238231, 237rspc2va 3622 . . . . . . 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 7422 . . . 4 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›))) = (0 + Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))))
242 fzofi 13935 . . . . . . 7 (0..^(π‘ˆ mod 𝑁)) ∈ Fin
243242a1i 11 . . . . . 6 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (0..^(π‘ˆ mod 𝑁)) ∈ Fin)
24434ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^(π‘ˆ mod 𝑁))) β†’ 𝑋 ∈ 𝐷)
245 elfzoelz 13628 . . . . . . . 8 (𝑛 ∈ (0..^(π‘ˆ mod 𝑁)) β†’ 𝑛 ∈ β„€)
246245adantl 483 . . . . . . 7 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^(π‘ˆ mod 𝑁))) β†’ 𝑛 ∈ β„€)
24730, 31, 32, 33, 244, 246dchrzrhcl 26728 . . . . . 6 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^(π‘ˆ mod 𝑁))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
248243, 247fsumcl 15675 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
249248addlidd 11411 . . . 4 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (0 + Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
25039, 241, 2493eqtrd 2777 . . 3 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ (0..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
251250fveq2d 6892 . 2 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›))) = (absβ€˜Ξ£π‘› ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))))
252 oveq2 7412 . . . . . 6 (𝑒 = (π‘ˆ mod 𝑁) β†’ (0..^𝑒) = (0..^(π‘ˆ mod 𝑁)))
253252sumeq1d 15643 . . . . 5 (𝑒 = (π‘ˆ mod 𝑁) β†’ Σ𝑛 ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
254253fveq2d 6892 . . . 4 (𝑒 = (π‘ˆ mod 𝑁) β†’ (absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) = (absβ€˜Ξ£π‘› ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))))
255254breq1d 5157 . . 3 (𝑒 = (π‘ˆ mod 𝑁) β†’ ((absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅 ↔ (absβ€˜Ξ£π‘› ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅))
256 dchrisum.10 . . . 4 (πœ‘ β†’ βˆ€π‘’ ∈ (0..^𝑁)(absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
257256adantr 482 . . 3 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ βˆ€π‘’ ∈ (0..^𝑁)(absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
258 zmodfzo 13855 . . . 4 ((π‘ˆ ∈ β„€ ∧ 𝑁 ∈ β„•) β†’ (π‘ˆ mod 𝑁) ∈ (0..^𝑁))
259222, 3, 258syl2anr 598 . . 3 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (π‘ˆ mod 𝑁) ∈ (0..^𝑁))
260255, 257, 259rspcdva 3613 . 2 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
261251, 260eqbrtrd 5169 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 3945   ∩ cin 3946  βˆ…c0 4321  ifcif 4527   class class class wbr 5147   ↦ cmpt 5230   β†Ύ cres 5677  β€“1-1-ontoβ†’wf1o 6539  β€˜cfv 6540  (class class class)co 7404  Fincfn 8935  β„‚cc 11104  β„cr 11105  0cc0 11106  1c1 11107   + caddc 11109   Β· cmul 11111   < clt 11244   ≀ cle 11245   βˆ’ cmin 11440   / cdiv 11867  β„•cn 12208  β„•0cn0 12468  β„€cz 12554  β„€β‰₯cuz 12818  β„+crp 12970  ...cfz 13480  ..^cfzo 13623  βŒŠcfl 13751   mod cmo 13830  abscabs 15177   β‡π‘Ÿ crli 15425  Ξ£csu 15628   βˆ₯ cdvds 16193  Ο•cphi 16693  Basecbs 17140  0gc0g 17381  β„€RHomczrh 21033  β„€/nβ„€czn 21036  DChrcdchr 26715
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 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186
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 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-of 7665  df-om 7851  df-1st 7970  df-2nd 7971  df-tpos 8206  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-oadd 8465  df-er 8699  df-ec 8701  df-qs 8705  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-xnn0 12541  df-z 12555  df-dec 12674  df-uz 12819  df-rp 12971  df-fz 13481  df-fzo 13624  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-hash 14287  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-clim 15428  df-sum 15629  df-dvds 16194  df-gcd 16432  df-phi 16695  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-0g 17383  df-imas 17450  df-qus 17451  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-mhm 18667  df-grp 18818  df-minusg 18819  df-sbg 18820  df-mulg 18945  df-subg 18997  df-nsg 18998  df-eqg 18999  df-ghm 19084  df-cmn 19643  df-abl 19644  df-mgp 19980  df-ur 19997  df-ring 20049  df-cring 20050  df-oppr 20139  df-dvdsr 20160  df-unit 20161  df-invr 20191  df-rnghom 20240  df-subrg 20349  df-lmod 20461  df-lss 20531  df-lsp 20571  df-sra 20773  df-rgmod 20774  df-lidl 20775  df-rsp 20776  df-2idl 20844  df-cnfld 20930  df-zring 21003  df-zrh 21037  df-zn 21040  df-dchr 26716
This theorem is referenced by:  dchrisumlem2  26973
  Copyright terms: Public domain W3C validator