MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrisumlem1 Structured version   Visualization version   GIF version
Theorem dchrisumlem1 26999
Description: Lemma for dchrisum 27002. 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 13668 . . . . . 6 ((0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))) ∩ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)) = βˆ…
21a1i 11 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))) ∩ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)) = βˆ…)
3 rpvmasum.a . . . . . . . . . 10 (πœ‘ β†’ 𝑁 ∈ β„•)
43nnnn0d 12534 . . . . . . . . 9 (πœ‘ β†’ 𝑁 ∈ β„•0)
54adantr 481 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 𝑁 ∈ β„•0)
6 nn0re 12483 . . . . . . . . . . 11 (π‘ˆ ∈ β„•0 β†’ π‘ˆ ∈ ℝ)
76adantl 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ π‘ˆ ∈ ℝ)
83adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 𝑁 ∈ β„•)
97, 8nndivred 12268 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (π‘ˆ / 𝑁) ∈ ℝ)
108nnrpd 13016 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 𝑁 ∈ ℝ+)
11 nn0ge0 12499 . . . . . . . . . . 11 (π‘ˆ ∈ β„•0 β†’ 0 ≀ π‘ˆ)
1211adantl 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 0 ≀ π‘ˆ)
137, 10, 12divge0d 13058 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 0 ≀ (π‘ˆ / 𝑁))
14 flge0nn0 13787 . . . . . . . . 9 (((π‘ˆ / 𝑁) ∈ ℝ ∧ 0 ≀ (π‘ˆ / 𝑁)) β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0)
159, 13, 14syl2anc 584 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0)
165, 15nn0mulcld 12539 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ β„•0)
17 flle 13766 . . . . . . . . 9 ((π‘ˆ / 𝑁) ∈ ℝ β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ≀ (π‘ˆ / 𝑁))
189, 17syl 17 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ≀ (π‘ˆ / 𝑁))
19 reflcl 13763 . . . . . . . . . 10 ((π‘ˆ / 𝑁) ∈ ℝ β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ ℝ)
209, 19syl 17 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ ℝ)
2120, 7, 10lemuldiv2d 13068 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ≀ π‘ˆ ↔ (βŒŠβ€˜(π‘ˆ / 𝑁)) ≀ (π‘ˆ / 𝑁)))
2218, 21mpbird 256 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ≀ π‘ˆ)
23 fznn0 13595 . . . . . . . 8 (π‘ˆ ∈ β„•0 β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ (0...π‘ˆ) ↔ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ β„•0 ∧ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ≀ π‘ˆ)))
2423adantl 482 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ (0...π‘ˆ) ↔ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ β„•0 ∧ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ≀ π‘ˆ)))
2516, 22, 24mpbir2and 711 . . . . . 6 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ (0...π‘ˆ))
26 fzosplit 13667 . . . . . 6 ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ (0...π‘ˆ) β†’ (0..^π‘ˆ) = ((0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))) βˆͺ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)))
2725, 26syl 17 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (0..^π‘ˆ) = ((0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))) βˆͺ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)))
28 fzofi 13941 . . . . . 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 724 . . . . . 6 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^π‘ˆ)) β†’ 𝑋 ∈ 𝐷)
36 elfzoelz 13634 . . . . . . 7 (𝑛 ∈ (0..^π‘ˆ) β†’ 𝑛 ∈ β„€)
3736adantl 482 . . . . . 6 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^π‘ˆ)) β†’ 𝑛 ∈ β„€)
3830, 31, 32, 33, 35, 37dchrzrhcl 26755 . . . . 5 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^π‘ˆ)) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
392, 27, 29, 38fsumsplit 15689 . . . 4 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ (0..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›)) = (Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›))))
40 oveq2 7419 . . . . . . . . . . . 12 (π‘˜ = 0 β†’ (𝑁 Β· π‘˜) = (𝑁 Β· 0))
4140oveq2d 7427 . . . . . . . . . . 11 (π‘˜ = 0 β†’ (0..^(𝑁 Β· π‘˜)) = (0..^(𝑁 Β· 0)))
4241sumeq1d 15649 . . . . . . . . . 10 (π‘˜ = 0 β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑁 Β· 0))(π‘‹β€˜(πΏβ€˜π‘›)))
4342eqeq1d 2734 . . . . . . . . 9 (π‘˜ = 0 β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 Β· 0))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
4443imbi2d 340 . . . . . . . 8 (π‘˜ = 0 β†’ ((πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0) ↔ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· 0))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
45 oveq2 7419 . . . . . . . . . . . 12 (π‘˜ = π‘š β†’ (𝑁 Β· π‘˜) = (𝑁 Β· π‘š))
4645oveq2d 7427 . . . . . . . . . . 11 (π‘˜ = π‘š β†’ (0..^(𝑁 Β· π‘˜)) = (0..^(𝑁 Β· π‘š)))
4746sumeq1d 15649 . . . . . . . . . 10 (π‘˜ = π‘š β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)))
4847eqeq1d 2734 . . . . . . . . 9 (π‘˜ = π‘š β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
4948imbi2d 340 . . . . . . . 8 (π‘˜ = π‘š β†’ ((πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0) ↔ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
50 oveq2 7419 . . . . . . . . . . . 12 (π‘˜ = (π‘š + 1) β†’ (𝑁 Β· π‘˜) = (𝑁 Β· (π‘š + 1)))
5150oveq2d 7427 . . . . . . . . . . 11 (π‘˜ = (π‘š + 1) β†’ (0..^(𝑁 Β· π‘˜)) = (0..^(𝑁 Β· (π‘š + 1))))
5251sumeq1d 15649 . . . . . . . . . 10 (π‘˜ = (π‘š + 1) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)))
5352eqeq1d 2734 . . . . . . . . 9 (π‘˜ = (π‘š + 1) β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
5453imbi2d 340 . . . . . . . 8 (π‘˜ = (π‘š + 1) β†’ ((πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0) ↔ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
55 oveq2 7419 . . . . . . . . . . . 12 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (𝑁 Β· π‘˜) = (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))
5655oveq2d 7427 . . . . . . . . . . 11 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (0..^(𝑁 Β· π‘˜)) = (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))))
5756sumeq1d 15649 . . . . . . . . . 10 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)))
5857eqeq1d 2734 . . . . . . . . 9 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
5958imbi2d 340 . . . . . . . 8 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ ((πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0) ↔ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
603nncnd 12230 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑁 ∈ β„‚)
6160mul01d 11415 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑁 Β· 0) = 0)
6261oveq2d 7427 . . . . . . . . . . 11 (πœ‘ β†’ (0..^(𝑁 Β· 0)) = (0..^0))
63 fzo0 13658 . . . . . . . . . . 11 (0..^0) = βˆ…
6462, 63eqtrdi 2788 . . . . . . . . . 10 (πœ‘ β†’ (0..^(𝑁 Β· 0)) = βˆ…)
6564sumeq1d 15649 . . . . . . . . 9 (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· 0))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ βˆ… (π‘‹β€˜(πΏβ€˜π‘›)))
66 sum0 15669 . . . . . . . . 9 Σ𝑛 ∈ βˆ… (π‘‹β€˜(πΏβ€˜π‘›)) = 0
6765, 66eqtrdi 2788 . . . . . . . 8 (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· 0))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
68 oveq1 7418 . . . . . . . . . . 11 (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))) = (0 + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))))
69 fzodisj 13668 . . . . . . . . . . . . . 14 ((0..^(𝑁 Β· π‘š)) ∩ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))) = βˆ…
7069a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ ((0..^(𝑁 Β· π‘š)) ∩ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))) = βˆ…)
71 nn0re 12483 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ β„•0 β†’ π‘š ∈ ℝ)
7271adantl 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ π‘š ∈ ℝ)
7372lep1d 12147 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ π‘š ≀ (π‘š + 1))
74 peano2re 11389 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ ℝ β†’ (π‘š + 1) ∈ ℝ)
7572, 74syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (π‘š + 1) ∈ ℝ)
763adantr 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 ∈ β„•)
7776nnred 12229 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 ∈ ℝ)
7876nngt0d 12263 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 0 < 𝑁)
79 lemul2 12069 . . . . . . . . . . . . . . . . 17 ((π‘š ∈ ℝ ∧ (π‘š + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) β†’ (π‘š ≀ (π‘š + 1) ↔ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1))))
8072, 75, 77, 78, 79syl112anc 1374 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (π‘š ≀ (π‘š + 1) ↔ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1))))
8173, 80mpbid 231 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1)))
82 nn0mulcl 12510 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ β„•0 ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„•0)
834, 82sylan 580 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„•0)
84 nn0uz 12866 . . . . . . . . . . . . . . . . 17 β„•0 = (β„€β‰₯β€˜0)
8583, 84eleqtrdi 2843 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ (β„€β‰₯β€˜0))
86 nn0p1nn 12513 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ β„•0 β†’ (π‘š + 1) ∈ β„•)
87 nnmulcl 12238 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ β„• ∧ (π‘š + 1) ∈ β„•) β†’ (𝑁 Β· (π‘š + 1)) ∈ β„•)
883, 86, 87syl2an 596 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· (π‘š + 1)) ∈ β„•)
8988nnzd 12587 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· (π‘š + 1)) ∈ β„€)
90 elfz5 13495 . . . . . . . . . . . . . . . 16 (((𝑁 Β· π‘š) ∈ (β„€β‰₯β€˜0) ∧ (𝑁 Β· (π‘š + 1)) ∈ β„€) β†’ ((𝑁 Β· π‘š) ∈ (0...(𝑁 Β· (π‘š + 1))) ↔ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1))))
9185, 89, 90syl2anc 584 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ ((𝑁 Β· π‘š) ∈ (0...(𝑁 Β· (π‘š + 1))) ↔ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1))))
9281, 91mpbird 256 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ (0...(𝑁 Β· (π‘š + 1))))
93 fzosplit 13667 . . . . . . . . . . . . . 14 ((𝑁 Β· π‘š) ∈ (0...(𝑁 Β· (π‘š + 1))) β†’ (0..^(𝑁 Β· (π‘š + 1))) = ((0..^(𝑁 Β· π‘š)) βˆͺ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))))
9492, 93syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (0..^(𝑁 Β· (π‘š + 1))) = ((0..^(𝑁 Β· π‘š)) βˆͺ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))))
95 fzofi 13941 . . . . . . . . . . . . . 14 (0..^(𝑁 Β· (π‘š + 1))) ∈ Fin
9695a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (0..^(𝑁 Β· (π‘š + 1))) ∈ Fin)
9734ad2antrr 724 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ 𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))) β†’ 𝑋 ∈ 𝐷)
98 elfzoelz 13634 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1))) β†’ 𝑛 ∈ β„€)
9998adantl 482 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ 𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))) β†’ 𝑛 ∈ β„€)
10030, 31, 32, 33, 97, 99dchrzrhcl 26755 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ 𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
10170, 94, 96, 100fsumsplit 15689 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))))
10276nncnd 12230 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 ∈ β„‚)
10372recnd 11244 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ π‘š ∈ β„‚)
104 1cnd 11211 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 1 ∈ β„‚)
105102, 103, 104adddid 11240 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· (π‘š + 1)) = ((𝑁 Β· π‘š) + (𝑁 Β· 1)))
106102mulridd 11233 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· 1) = 𝑁)
107106oveq2d 7427 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ ((𝑁 Β· π‘š) + (𝑁 Β· 1)) = ((𝑁 Β· π‘š) + 𝑁))
108105, 107eqtrd 2772 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· (π‘š + 1)) = ((𝑁 Β· π‘š) + 𝑁))
109108oveq2d 7427 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1))) = ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁)))
110109sumeq1d 15649 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
111 oveq2 7419 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑁 β†’ ((𝑁 Β· π‘š) + π‘˜) = ((𝑁 Β· π‘š) + 𝑁))
112111oveq2d 7427 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑁 β†’ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜)) = ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁)))
113112sumeq1d 15649 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑁 β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
114 oveq2 7419 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑁 β†’ (0..^π‘˜) = (0..^𝑁))
115114sumeq1d 15649 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑁 β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›)))
116113, 115eqeq12d 2748 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑁 β†’ (Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) ↔ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›))))
11783nn0zd 12586 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„€)
118117adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„€)
119 nn0z 12585 . . . . . . . . . . . . . . . . . . . . . 22 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„€)
120 zaddcl 12604 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 Β· π‘š) ∈ β„€ ∧ π‘˜ ∈ β„€) β†’ ((𝑁 Β· π‘š) + π‘˜) ∈ β„€)
121117, 119, 120syl2an 596 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((𝑁 Β· π‘š) + π‘˜) ∈ β„€)
122 peano2zm 12607 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 Β· π‘š) + π‘˜) ∈ β„€ β†’ (((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) ∈ β„€)
123121, 122syl 17 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) ∈ β„€)
12434ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))) β†’ 𝑋 ∈ 𝐷)
125 elfzelz 13503 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1)) β†’ 𝑛 ∈ β„€)
126125adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))) β†’ 𝑛 ∈ β„€)
12730, 31, 32, 33, 124, 126dchrzrhcl 26755 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
128 2fveq3 6896 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = (𝑖 + (𝑁 Β· π‘š)) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) = (π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))))
129118, 118, 123, 127, 128fsumshftm 15729 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑖 ∈ (((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š))...((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š)))(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))))
130 fzoval 13635 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 Β· π‘š) + π‘˜) ∈ β„€ β†’ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜)) = ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1)))
131121, 130syl 17 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜)) = ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1)))
132131sumeq1d 15649 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))(π‘‹β€˜(πΏβ€˜π‘›)))
133119adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„€)
134 fzoval 13635 . . . . . . . . . . . . . . . . . . . . . 22 (π‘˜ ∈ β„€ β†’ (0..^π‘˜) = (0...(π‘˜ βˆ’ 1)))
135133, 134syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (0..^π‘˜) = (0...(π‘˜ βˆ’ 1)))
136118zcnd 12669 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„‚)
137136subidd 11561 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š)) = 0)
138121zcnd 12669 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((𝑁 Β· π‘š) + π‘˜) ∈ β„‚)
139 1cnd 11211 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ 1 ∈ β„‚)
140138, 139, 136sub32d 11605 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š)) = ((((𝑁 Β· π‘š) + π‘˜) βˆ’ (𝑁 Β· π‘š)) βˆ’ 1))
141 nn0cn 12484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„‚)
142141adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„‚)
143136, 142pncan2d 11575 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (((𝑁 Β· π‘š) + π‘˜) βˆ’ (𝑁 Β· π‘š)) = π‘˜)
144143oveq1d 7426 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((((𝑁 Β· π‘š) + π‘˜) βˆ’ (𝑁 Β· π‘š)) βˆ’ 1) = (π‘˜ βˆ’ 1))
145140, 144eqtrd 2772 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š)) = (π‘˜ βˆ’ 1))
146137, 145oveq12d 7429 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š))...((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š))) = (0...(π‘˜ βˆ’ 1)))
147135, 146eqtr4d 2775 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (0..^π‘˜) = (((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š))...((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š))))
148147sumeq1d 15649 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))) = Σ𝑖 ∈ (((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š))...((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š)))(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))))
149129, 132, 1483eqtr4d 2782 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))))
1503nnzd 12587 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝑁 ∈ β„€)
151 nn0z 12585 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘š ∈ β„•0 β†’ π‘š ∈ β„€)
152 dvdsmul1 16223 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 ∈ β„€ ∧ π‘š ∈ β„€) β†’ 𝑁 βˆ₯ (𝑁 Β· π‘š))
153150, 151, 152syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 βˆ₯ (𝑁 Β· π‘š))
154153ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑁 βˆ₯ (𝑁 Β· π‘š))
155 elfzoelz 13634 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^π‘˜) β†’ 𝑖 ∈ β„€)
156155adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑖 ∈ β„€)
157156zcnd 12669 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑖 ∈ β„‚)
158136adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (𝑁 Β· π‘š) ∈ β„‚)
159157, 158pncan2d 11575 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ ((𝑖 + (𝑁 Β· π‘š)) βˆ’ 𝑖) = (𝑁 Β· π‘š))
160154, 159breqtrrd 5176 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑁 βˆ₯ ((𝑖 + (𝑁 Β· π‘š)) βˆ’ 𝑖))
16176nnnn0d 12534 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 ∈ β„•0)
162161ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑁 ∈ β„•0)
163 zaddcl 12604 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ β„€ ∧ (𝑁 Β· π‘š) ∈ β„€) β†’ (𝑖 + (𝑁 Β· π‘š)) ∈ β„€)
164155, 118, 163syl2anr 597 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (𝑖 + (𝑁 Β· π‘š)) ∈ β„€)
16531, 33zndvds 21111 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ β„•0 ∧ (𝑖 + (𝑁 Β· π‘š)) ∈ β„€ ∧ 𝑖 ∈ β„€) β†’ ((πΏβ€˜(𝑖 + (𝑁 Β· π‘š))) = (πΏβ€˜π‘–) ↔ 𝑁 βˆ₯ ((𝑖 + (𝑁 Β· π‘š)) βˆ’ 𝑖)))
166162, 164, 156, 165syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ ((πΏβ€˜(𝑖 + (𝑁 Β· π‘š))) = (πΏβ€˜π‘–) ↔ 𝑁 βˆ₯ ((𝑖 + (𝑁 Β· π‘š)) βˆ’ 𝑖)))
167160, 166mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (πΏβ€˜(𝑖 + (𝑁 Β· π‘š))) = (πΏβ€˜π‘–))
168167fveq2d 6895 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))) = (π‘‹β€˜(πΏβ€˜π‘–)))
169168sumeq2dv 15651 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))) = Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘–)))
170 2fveq3 6896 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑛 β†’ (π‘‹β€˜(πΏβ€˜π‘–)) = (π‘‹β€˜(πΏβ€˜π‘›)))
171170cbvsumv 15644 . . . . . . . . . . . . . . . . . . 19 Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘–)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›))
172169, 171eqtrdi 2788 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)))
173149, 172eqtrd 2772 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)))
174173ralrimiva 3146 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ βˆ€π‘˜ ∈ β„•0 Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)))
175116, 174, 161rspcdva 3613 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›)))
176 fveq2 6891 . . . . . . . . . . . . . . . . . 18 (π‘˜ = (πΏβ€˜π‘›) β†’ (π‘‹β€˜π‘˜) = (π‘‹β€˜(πΏβ€˜π‘›)))
1773nnne0d 12264 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝑁 β‰  0)
178 ifnefalse 4540 . . . . . . . . . . . . . . . . . . . 20 (𝑁 β‰  0 β†’ if(𝑁 = 0, β„€, (0..^𝑁)) = (0..^𝑁))
179177, 178syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ if(𝑁 = 0, β„€, (0..^𝑁)) = (0..^𝑁))
180 fzofi 13941 . . . . . . . . . . . . . . . . . . 19 (0..^𝑁) ∈ Fin
181179, 180eqeltrdi 2841 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ if(𝑁 = 0, β„€, (0..^𝑁)) ∈ Fin)
182 eqid 2732 . . . . . . . . . . . . . . . . . . . 20 (Baseβ€˜π‘) = (Baseβ€˜π‘)
18333reseq1i 5977 . . . . . . . . . . . . . . . . . . . 20 (𝐿 β†Ύ if(𝑁 = 0, β„€, (0..^𝑁))) = ((β„€RHomβ€˜π‘) β†Ύ if(𝑁 = 0, β„€, (0..^𝑁)))
184 eqid 2732 . . . . . . . . . . . . . . . . . . . 20 if(𝑁 = 0, β„€, (0..^𝑁)) = if(𝑁 = 0, β„€, (0..^𝑁))
18531, 182, 183, 184znf1o 21113 . . . . . . . . . . . . . . . . . . 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 6910 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ if(𝑁 = 0, β„€, (0..^𝑁)) β†’ ((𝐿 β†Ύ if(𝑁 = 0, β„€, (0..^𝑁)))β€˜π‘›) = (πΏβ€˜π‘›))
188187adantl 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ if(𝑁 = 0, β„€, (0..^𝑁))) β†’ ((𝐿 β†Ύ if(𝑁 = 0, β„€, (0..^𝑁)))β€˜π‘›) = (πΏβ€˜π‘›))
18930, 31, 32, 182, 34dchrf 26752 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋:(Baseβ€˜π‘)βŸΆβ„‚)
190189ffvelcdmda 7086 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ (Baseβ€˜π‘)) β†’ (π‘‹β€˜π‘˜) ∈ β„‚)
191176, 181, 186, 188, 190fsumf1o 15671 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ Ξ£π‘˜ ∈ (Baseβ€˜π‘)(π‘‹β€˜π‘˜) = Σ𝑛 ∈ if (𝑁 = 0, β„€, (0..^𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
192 rpvmasum.1 . . . . . . . . . . . . . . . . . . 19 1 = (0gβ€˜πΊ)
19330, 31, 32, 192, 34, 182dchrsum 26779 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ Ξ£π‘˜ ∈ (Baseβ€˜π‘)(π‘‹β€˜π‘˜) = if(𝑋 = 1 , (Ο•β€˜π‘), 0))
194 dchrisum.n1 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋 β‰  1 )
195 ifnefalse 4540 . . . . . . . . . . . . . . . . . . 19 (𝑋 β‰  1 β†’ if(𝑋 = 1 , (Ο•β€˜π‘), 0) = 0)
196194, 195syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ if(𝑋 = 1 , (Ο•β€˜π‘), 0) = 0)
197193, 196eqtrd 2772 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ Ξ£π‘˜ ∈ (Baseβ€˜π‘)(π‘‹β€˜π‘˜) = 0)
198179sumeq1d 15649 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ Σ𝑛 ∈ if (𝑁 = 0, β„€, (0..^𝑁))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›)))
199191, 197, 1983eqtr3rd 2781 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
200199adantr 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
201110, 175, 2003eqtrd 2776 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
202201oveq2d 7427 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (0 + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))) = (0 + 0))
203 00id 11391 . . . . . . . . . . . . 13 (0 + 0) = 0
204202, 203eqtr2di 2789 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 0 = (0 + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))))
205101, 204eqeq12d 2748 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 ↔ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))) = (0 + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)))))
20668, 205imbitrrid 245 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
207206expcom 414 . . . . . . . . 9 (π‘š ∈ β„•0 β†’ (πœ‘ β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
208207a2d 29 . . . . . . . 8 (π‘š ∈ β„•0 β†’ ((πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0) β†’ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
20944, 49, 54, 59, 67, 208nn0ind 12659 . . . . . . 7 ((βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0 β†’ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
210209impcom 408 . . . . . 6 ((πœ‘ ∧ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
21115, 210syldan 591 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
212 modval 13838 . . . . . . . . . . 11 ((π‘ˆ ∈ ℝ ∧ 𝑁 ∈ ℝ+) β†’ (π‘ˆ mod 𝑁) = (π‘ˆ βˆ’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))))
2137, 10, 212syl2anc 584 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (π‘ˆ mod 𝑁) = (π‘ˆ βˆ’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))))
214213oveq2d 7427 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ βˆ’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))))
21516nn0cnd 12536 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ β„‚)
216 nn0cn 12484 . . . . . . . . . . 11 (π‘ˆ ∈ β„•0 β†’ π‘ˆ ∈ β„‚)
217216adantl 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ π‘ˆ ∈ β„‚)
218215, 217pncan3d 11576 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ βˆ’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))) = π‘ˆ)
219214, 218eqtr2d 2773 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ π‘ˆ = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))
220219oveq2d 7427 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁))))
221220sumeq1d 15649 . . . . . 6 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)))
222 nn0z 12585 . . . . . . . 8 (π‘ˆ ∈ β„•0 β†’ π‘ˆ ∈ β„€)
223 zmodcl 13858 . . . . . . . 8 ((π‘ˆ ∈ β„€ ∧ 𝑁 ∈ β„•) β†’ (π‘ˆ mod 𝑁) ∈ β„•0)
224222, 3, 223syl2anr 597 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (π‘ˆ mod 𝑁) ∈ β„•0)
225174ralrimiva 3146 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘š ∈ β„•0 βˆ€π‘˜ ∈ β„•0 Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)))
226225adantr 481 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ βˆ€π‘š ∈ β„•0 βˆ€π‘˜ ∈ β„•0 Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)))
227 oveq2 7419 . . . . . . . . . . 11 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (𝑁 Β· π‘š) = (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))
228227oveq1d 7426 . . . . . . . . . . 11 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ ((𝑁 Β· π‘š) + π‘˜) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))
229227, 228oveq12d 7429 . . . . . . . . . 10 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜)) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜)))
230229sumeq1d 15649 . . . . . . . . 9 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)))
231230eqeq1d 2734 . . . . . . . 8 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) ↔ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›))))
232 oveq2 7419 . . . . . . . . . . 11 (π‘˜ = (π‘ˆ mod 𝑁) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))
233232oveq2d 7427 . . . . . . . . . 10 (π‘˜ = (π‘ˆ mod 𝑁) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜)) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁))))
234233sumeq1d 15649 . . . . . . . . 9 (π‘˜ = (π‘ˆ mod 𝑁) β†’ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)))
235 oveq2 7419 . . . . . . . . . 10 (π‘˜ = (π‘ˆ mod 𝑁) β†’ (0..^π‘˜) = (0..^(π‘ˆ mod 𝑁)))
236235sumeq1d 15649 . . . . . . . . 9 (π‘˜ = (π‘ˆ mod 𝑁) β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
237234, 236eqeq12d 2748 . . . . . . . 8 (π‘˜ = (π‘ˆ mod 𝑁) β†’ (Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) ↔ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))))
238231, 237rspc2va 3623 . . . . . . 7 ((((βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0 ∧ (π‘ˆ mod 𝑁) ∈ β„•0) ∧ βˆ€π‘š ∈ β„•0 βˆ€π‘˜ ∈ β„•0 Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›))) β†’ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
23915, 224, 226, 238syl21anc 836 . . . . . 6 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
240221, 239eqtrd 2772 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
241211, 240oveq12d 7429 . . . 4 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›))) = (0 + Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))))
242 fzofi 13941 . . . . . . 7 (0..^(π‘ˆ mod 𝑁)) ∈ Fin
243242a1i 11 . . . . . 6 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (0..^(π‘ˆ mod 𝑁)) ∈ Fin)
24434ad2antrr 724 . . . . . . 7 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^(π‘ˆ mod 𝑁))) β†’ 𝑋 ∈ 𝐷)
245 elfzoelz 13634 . . . . . . . 8 (𝑛 ∈ (0..^(π‘ˆ mod 𝑁)) β†’ 𝑛 ∈ β„€)
246245adantl 482 . . . . . . 7 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^(π‘ˆ mod 𝑁))) β†’ 𝑛 ∈ β„€)
24730, 31, 32, 33, 244, 246dchrzrhcl 26755 . . . . . 6 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^(π‘ˆ mod 𝑁))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
248243, 247fsumcl 15681 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
249248addlidd 11417 . . . 4 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (0 + Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
25039, 241, 2493eqtrd 2776 . . 3 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ (0..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
251250fveq2d 6895 . 2 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›))) = (absβ€˜Ξ£π‘› ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))))
252 oveq2 7419 . . . . . 6 (𝑒 = (π‘ˆ mod 𝑁) β†’ (0..^𝑒) = (0..^(π‘ˆ mod 𝑁)))
253252sumeq1d 15649 . . . . 5 (𝑒 = (π‘ˆ mod 𝑁) β†’ Σ𝑛 ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
254253fveq2d 6895 . . . 4 (𝑒 = (π‘ˆ mod 𝑁) β†’ (absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) = (absβ€˜Ξ£π‘› ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))))
255254breq1d 5158 . . 3 (𝑒 = (π‘ˆ mod 𝑁) β†’ ((absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅 ↔ (absβ€˜Ξ£π‘› ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅))
256 dchrisum.10 . . . 4 (πœ‘ β†’ βˆ€π‘’ ∈ (0..^𝑁)(absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
257256adantr 481 . . 3 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ βˆ€π‘’ ∈ (0..^𝑁)(absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
258 zmodfzo 13861 . . . 4 ((π‘ˆ ∈ β„€ ∧ 𝑁 ∈ β„•) β†’ (π‘ˆ mod 𝑁) ∈ (0..^𝑁))
259222, 3, 258syl2anr 597 . . 3 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (π‘ˆ mod 𝑁) ∈ (0..^𝑁))
260255, 257, 259rspcdva 3613 . 2 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
261251, 260eqbrtrd 5170 1 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061   βˆͺ cun 3946   ∩ cin 3947  βˆ…c0 4322  ifcif 4528   class class class wbr 5148   ↦ cmpt 5231   β†Ύ cres 5678  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543  (class class class)co 7411  Fincfn 8941  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117   < clt 11250   ≀ cle 11251   βˆ’ cmin 11446   / cdiv 11873  β„•cn 12214  β„•0cn0 12474  β„€cz 12560  β„€β‰₯cuz 12824  β„+crp 12976  ...cfz 13486  ..^cfzo 13629  βŒŠcfl 13757   mod cmo 13836  abscabs 15183   β‡π‘Ÿ crli 15431  Ξ£csu 15634   βˆ₯ cdvds 16199  Ο•cphi 16699  Basecbs 17146  0gc0g 17387  β„€RHomczrh 21055  β„€/nβ„€czn 21058  DChrcdchr 26742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191  ax-mulf 11192
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-tpos 8213  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-er 8705  df-ec 8707  df-qs 8711  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-oi 9507  df-card 9936  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-4 12279  df-5 12280  df-6 12281  df-7 12282  df-8 12283  df-9 12284  df-n0 12475  df-xnn0 12547  df-z 12561  df-dec 12680  df-uz 12825  df-rp 12977  df-fz 13487  df-fzo 13630  df-fl 13759  df-mod 13837  df-seq 13969  df-exp 14030  df-hash 14293  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-clim 15434  df-sum 15635  df-dvds 16200  df-gcd 16438  df-phi 16701  df-struct 17082  df-sets 17099  df-slot 17117  df-ndx 17129  df-base 17147  df-ress 17176  df-plusg 17212  df-mulr 17213  df-starv 17214  df-sca 17215  df-vsca 17216  df-ip 17217  df-tset 17218  df-ple 17219  df-ds 17221  df-unif 17222  df-0g 17389  df-imas 17456  df-qus 17457  df-mgm 18563  df-sgrp 18612  df-mnd 18628  df-mhm 18673  df-grp 18824  df-minusg 18825  df-sbg 18826  df-mulg 18953  df-subg 19005  df-nsg 19006  df-eqg 19007  df-ghm 19092  df-cmn 19652  df-abl 19653  df-mgp 19990  df-ur 20007  df-ring 20060  df-cring 20061  df-oppr 20154  df-dvdsr 20175  df-unit 20176  df-invr 20206  df-rnghom 20255  df-subrg 20321  df-lmod 20477  df-lss 20548  df-lsp 20588  df-sra 20791  df-rgmod 20792  df-lidl 20793  df-rsp 20794  df-2idl 20863  df-cnfld 20951  df-zring 21024  df-zrh 21059  df-zn 21062  df-dchr 26743
This theorem is referenced by:  dchrisumlem2  27000
  Copyright terms: Public domain W3C validator