MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrisumlem1 Structured version   Visualization version   GIF version
Theorem dchrisumlem1 27409
Description: Lemma for dchrisum 27412. 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 13690 . . . . . 6 ((0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))) ∩ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)) = βˆ…
21a1i 11 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))) ∩ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)) = βˆ…)
3 rpvmasum.a . . . . . . . . . 10 (πœ‘ β†’ 𝑁 ∈ β„•)
43nnnn0d 12554 . . . . . . . . 9 (πœ‘ β†’ 𝑁 ∈ β„•0)
54adantr 480 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 𝑁 ∈ β„•0)
6 nn0re 12503 . . . . . . . . . . 11 (π‘ˆ ∈ β„•0 β†’ π‘ˆ ∈ ℝ)
76adantl 481 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ π‘ˆ ∈ ℝ)
83adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 𝑁 ∈ β„•)
97, 8nndivred 12288 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (π‘ˆ / 𝑁) ∈ ℝ)
108nnrpd 13038 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 𝑁 ∈ ℝ+)
11 nn0ge0 12519 . . . . . . . . . . 11 (π‘ˆ ∈ β„•0 β†’ 0 ≀ π‘ˆ)
1211adantl 481 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 0 ≀ π‘ˆ)
137, 10, 12divge0d 13080 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ 0 ≀ (π‘ˆ / 𝑁))
14 flge0nn0 13809 . . . . . . . . 9 (((π‘ˆ / 𝑁) ∈ ℝ ∧ 0 ≀ (π‘ˆ / 𝑁)) β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0)
159, 13, 14syl2anc 583 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0)
165, 15nn0mulcld 12559 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ β„•0)
17 flle 13788 . . . . . . . . 9 ((π‘ˆ / 𝑁) ∈ ℝ β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ≀ (π‘ˆ / 𝑁))
189, 17syl 17 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ≀ (π‘ˆ / 𝑁))
19 reflcl 13785 . . . . . . . . . 10 ((π‘ˆ / 𝑁) ∈ ℝ β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ ℝ)
209, 19syl 17 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ ℝ)
2120, 7, 10lemuldiv2d 13090 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ≀ π‘ˆ ↔ (βŒŠβ€˜(π‘ˆ / 𝑁)) ≀ (π‘ˆ / 𝑁)))
2218, 21mpbird 257 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ≀ π‘ˆ)
23 fznn0 13617 . . . . . . . 8 (π‘ˆ ∈ β„•0 β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ (0...π‘ˆ) ↔ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ β„•0 ∧ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ≀ π‘ˆ)))
2423adantl 481 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ (0...π‘ˆ) ↔ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ β„•0 ∧ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ≀ π‘ˆ)))
2516, 22, 24mpbir2and 712 . . . . . 6 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ (0...π‘ˆ))
26 fzosplit 13689 . . . . . 6 ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ (0...π‘ˆ) β†’ (0..^π‘ˆ) = ((0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))) βˆͺ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)))
2725, 26syl 17 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (0..^π‘ˆ) = ((0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))) βˆͺ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)))
28 fzofi 13963 . . . . . 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 13656 . . . . . . 7 (𝑛 ∈ (0..^π‘ˆ) β†’ 𝑛 ∈ β„€)
3736adantl 481 . . . . . 6 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^π‘ˆ)) β†’ 𝑛 ∈ β„€)
3830, 31, 32, 33, 35, 37dchrzrhcl 27165 . . . . 5 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^π‘ˆ)) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
392, 27, 29, 38fsumsplit 15711 . . . 4 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ (0..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›)) = (Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›))))
40 oveq2 7422 . . . . . . . . . . . 12 (π‘˜ = 0 β†’ (𝑁 Β· π‘˜) = (𝑁 Β· 0))
4140oveq2d 7430 . . . . . . . . . . 11 (π‘˜ = 0 β†’ (0..^(𝑁 Β· π‘˜)) = (0..^(𝑁 Β· 0)))
4241sumeq1d 15671 . . . . . . . . . 10 (π‘˜ = 0 β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑁 Β· 0))(π‘‹β€˜(πΏβ€˜π‘›)))
4342eqeq1d 2729 . . . . . . . . 9 (π‘˜ = 0 β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 Β· 0))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
4443imbi2d 340 . . . . . . . 8 (π‘˜ = 0 β†’ ((πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0) ↔ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· 0))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
45 oveq2 7422 . . . . . . . . . . . 12 (π‘˜ = π‘š β†’ (𝑁 Β· π‘˜) = (𝑁 Β· π‘š))
4645oveq2d 7430 . . . . . . . . . . 11 (π‘˜ = π‘š β†’ (0..^(𝑁 Β· π‘˜)) = (0..^(𝑁 Β· π‘š)))
4746sumeq1d 15671 . . . . . . . . . 10 (π‘˜ = π‘š β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)))
4847eqeq1d 2729 . . . . . . . . 9 (π‘˜ = π‘š β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
4948imbi2d 340 . . . . . . . 8 (π‘˜ = π‘š β†’ ((πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0) ↔ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
50 oveq2 7422 . . . . . . . . . . . 12 (π‘˜ = (π‘š + 1) β†’ (𝑁 Β· π‘˜) = (𝑁 Β· (π‘š + 1)))
5150oveq2d 7430 . . . . . . . . . . 11 (π‘˜ = (π‘š + 1) β†’ (0..^(𝑁 Β· π‘˜)) = (0..^(𝑁 Β· (π‘š + 1))))
5251sumeq1d 15671 . . . . . . . . . 10 (π‘˜ = (π‘š + 1) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)))
5352eqeq1d 2729 . . . . . . . . 9 (π‘˜ = (π‘š + 1) β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
5453imbi2d 340 . . . . . . . 8 (π‘˜ = (π‘š + 1) β†’ ((πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0) ↔ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
55 oveq2 7422 . . . . . . . . . . . 12 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (𝑁 Β· π‘˜) = (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))
5655oveq2d 7430 . . . . . . . . . . 11 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (0..^(𝑁 Β· π‘˜)) = (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))))
5756sumeq1d 15671 . . . . . . . . . 10 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)))
5857eqeq1d 2729 . . . . . . . . 9 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
5958imbi2d 340 . . . . . . . 8 (π‘˜ = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ ((πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = 0) ↔ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
603nncnd 12250 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑁 ∈ β„‚)
6160mul01d 11435 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑁 Β· 0) = 0)
6261oveq2d 7430 . . . . . . . . . . 11 (πœ‘ β†’ (0..^(𝑁 Β· 0)) = (0..^0))
63 fzo0 13680 . . . . . . . . . . 11 (0..^0) = βˆ…
6462, 63eqtrdi 2783 . . . . . . . . . 10 (πœ‘ β†’ (0..^(𝑁 Β· 0)) = βˆ…)
6564sumeq1d 15671 . . . . . . . . 9 (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· 0))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ βˆ… (π‘‹β€˜(πΏβ€˜π‘›)))
66 sum0 15691 . . . . . . . . 9 Σ𝑛 ∈ βˆ… (π‘‹β€˜(πΏβ€˜π‘›)) = 0
6765, 66eqtrdi 2783 . . . . . . . 8 (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· 0))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
68 oveq1 7421 . . . . . . . . . . 11 (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))) = (0 + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))))
69 fzodisj 13690 . . . . . . . . . . . . . 14 ((0..^(𝑁 Β· π‘š)) ∩ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))) = βˆ…
7069a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ ((0..^(𝑁 Β· π‘š)) ∩ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))) = βˆ…)
71 nn0re 12503 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ β„•0 β†’ π‘š ∈ ℝ)
7271adantl 481 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ π‘š ∈ ℝ)
7372lep1d 12167 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ π‘š ≀ (π‘š + 1))
74 peano2re 11409 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ ℝ β†’ (π‘š + 1) ∈ ℝ)
7572, 74syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (π‘š + 1) ∈ ℝ)
763adantr 480 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 ∈ β„•)
7776nnred 12249 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 ∈ ℝ)
7876nngt0d 12283 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 0 < 𝑁)
79 lemul2 12089 . . . . . . . . . . . . . . . . 17 ((π‘š ∈ ℝ ∧ (π‘š + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) β†’ (π‘š ≀ (π‘š + 1) ↔ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1))))
8072, 75, 77, 78, 79syl112anc 1372 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (π‘š ≀ (π‘š + 1) ↔ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1))))
8173, 80mpbid 231 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1)))
82 nn0mulcl 12530 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ β„•0 ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„•0)
834, 82sylan 579 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„•0)
84 nn0uz 12886 . . . . . . . . . . . . . . . . 17 β„•0 = (β„€β‰₯β€˜0)
8583, 84eleqtrdi 2838 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ (β„€β‰₯β€˜0))
86 nn0p1nn 12533 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ β„•0 β†’ (π‘š + 1) ∈ β„•)
87 nnmulcl 12258 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ β„• ∧ (π‘š + 1) ∈ β„•) β†’ (𝑁 Β· (π‘š + 1)) ∈ β„•)
883, 86, 87syl2an 595 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· (π‘š + 1)) ∈ β„•)
8988nnzd 12607 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· (π‘š + 1)) ∈ β„€)
90 elfz5 13517 . . . . . . . . . . . . . . . 16 (((𝑁 Β· π‘š) ∈ (β„€β‰₯β€˜0) ∧ (𝑁 Β· (π‘š + 1)) ∈ β„€) β†’ ((𝑁 Β· π‘š) ∈ (0...(𝑁 Β· (π‘š + 1))) ↔ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1))))
9185, 89, 90syl2anc 583 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ ((𝑁 Β· π‘š) ∈ (0...(𝑁 Β· (π‘š + 1))) ↔ (𝑁 Β· π‘š) ≀ (𝑁 Β· (π‘š + 1))))
9281, 91mpbird 257 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ (0...(𝑁 Β· (π‘š + 1))))
93 fzosplit 13689 . . . . . . . . . . . . . 14 ((𝑁 Β· π‘š) ∈ (0...(𝑁 Β· (π‘š + 1))) β†’ (0..^(𝑁 Β· (π‘š + 1))) = ((0..^(𝑁 Β· π‘š)) βˆͺ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))))
9492, 93syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (0..^(𝑁 Β· (π‘š + 1))) = ((0..^(𝑁 Β· π‘š)) βˆͺ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))))
95 fzofi 13963 . . . . . . . . . . . . . 14 (0..^(𝑁 Β· (π‘š + 1))) ∈ Fin
9695a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (0..^(𝑁 Β· (π‘š + 1))) ∈ Fin)
9734ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ 𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))) β†’ 𝑋 ∈ 𝐷)
98 elfzoelz 13656 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1))) β†’ 𝑛 ∈ β„€)
9998adantl 481 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ 𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))) β†’ 𝑛 ∈ β„€)
10030, 31, 32, 33, 97, 99dchrzrhcl 27165 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ 𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
10170, 94, 96, 100fsumsplit 15711 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))))
10276nncnd 12250 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 ∈ β„‚)
10372recnd 11264 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ π‘š ∈ β„‚)
104 1cnd 11231 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 1 ∈ β„‚)
105102, 103, 104adddid 11260 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· (π‘š + 1)) = ((𝑁 Β· π‘š) + (𝑁 Β· 1)))
106102mulridd 11253 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· 1) = 𝑁)
107106oveq2d 7430 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ ((𝑁 Β· π‘š) + (𝑁 Β· 1)) = ((𝑁 Β· π‘š) + 𝑁))
108105, 107eqtrd 2767 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· (π‘š + 1)) = ((𝑁 Β· π‘š) + 𝑁))
109108oveq2d 7430 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1))) = ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁)))
110109sumeq1d 15671 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
111 oveq2 7422 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑁 β†’ ((𝑁 Β· π‘š) + π‘˜) = ((𝑁 Β· π‘š) + 𝑁))
112111oveq2d 7430 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑁 β†’ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜)) = ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁)))
113112sumeq1d 15671 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑁 β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
114 oveq2 7422 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑁 β†’ (0..^π‘˜) = (0..^𝑁))
115114sumeq1d 15671 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑁 β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›)))
116113, 115eqeq12d 2743 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑁 β†’ (Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) ↔ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›))))
11783nn0zd 12606 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„€)
118117adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„€)
119 nn0z 12605 . . . . . . . . . . . . . . . . . . . . . 22 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„€)
120 zaddcl 12624 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 Β· π‘š) ∈ β„€ ∧ π‘˜ ∈ β„€) β†’ ((𝑁 Β· π‘š) + π‘˜) ∈ β„€)
121117, 119, 120syl2an 595 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((𝑁 Β· π‘š) + π‘˜) ∈ β„€)
122 peano2zm 12627 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 Β· π‘š) + π‘˜) ∈ β„€ β†’ (((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) ∈ β„€)
123121, 122syl 17 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) ∈ β„€)
12434ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))) β†’ 𝑋 ∈ 𝐷)
125 elfzelz 13525 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1)) β†’ 𝑛 ∈ β„€)
126125adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))) β†’ 𝑛 ∈ β„€)
12730, 31, 32, 33, 124, 126dchrzrhcl 27165 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
128 2fveq3 6896 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = (𝑖 + (𝑁 Β· π‘š)) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) = (π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))))
129118, 118, 123, 127, 128fsumshftm 15751 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑖 ∈ (((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š))...((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š)))(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))))
130 fzoval 13657 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 Β· π‘š) + π‘˜) ∈ β„€ β†’ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜)) = ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1)))
131121, 130syl 17 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜)) = ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1)))
132131sumeq1d 15671 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· π‘š)...(((𝑁 Β· π‘š) + π‘˜) βˆ’ 1))(π‘‹β€˜(πΏβ€˜π‘›)))
133119adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„€)
134 fzoval 13657 . . . . . . . . . . . . . . . . . . . . . 22 (π‘˜ ∈ β„€ β†’ (0..^π‘˜) = (0...(π‘˜ βˆ’ 1)))
135133, 134syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (0..^π‘˜) = (0...(π‘˜ βˆ’ 1)))
136118zcnd 12689 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (𝑁 Β· π‘š) ∈ β„‚)
137136subidd 11581 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š)) = 0)
138121zcnd 12689 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((𝑁 Β· π‘š) + π‘˜) ∈ β„‚)
139 1cnd 11231 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ 1 ∈ β„‚)
140138, 139, 136sub32d 11625 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š)) = ((((𝑁 Β· π‘š) + π‘˜) βˆ’ (𝑁 Β· π‘š)) βˆ’ 1))
141 nn0cn 12504 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„‚)
142141adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„‚)
143136, 142pncan2d 11595 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (((𝑁 Β· π‘š) + π‘˜) βˆ’ (𝑁 Β· π‘š)) = π‘˜)
144143oveq1d 7429 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((((𝑁 Β· π‘š) + π‘˜) βˆ’ (𝑁 Β· π‘š)) βˆ’ 1) = (π‘˜ βˆ’ 1))
145140, 144eqtrd 2767 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ ((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š)) = (π‘˜ βˆ’ 1))
146137, 145oveq12d 7432 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š))...((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š))) = (0...(π‘˜ βˆ’ 1)))
147135, 146eqtr4d 2770 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ (0..^π‘˜) = (((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š))...((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š))))
148147sumeq1d 15671 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))) = Σ𝑖 ∈ (((𝑁 Β· π‘š) βˆ’ (𝑁 Β· π‘š))...((((𝑁 Β· π‘š) + π‘˜) βˆ’ 1) βˆ’ (𝑁 Β· π‘š)))(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))))
149129, 132, 1483eqtr4d 2777 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))))
1503nnzd 12607 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝑁 ∈ β„€)
151 nn0z 12605 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘š ∈ β„•0 β†’ π‘š ∈ β„€)
152 dvdsmul1 16246 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 ∈ β„€ ∧ π‘š ∈ β„€) β†’ 𝑁 βˆ₯ (𝑁 Β· π‘š))
153150, 151, 152syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 βˆ₯ (𝑁 Β· π‘š))
154153ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑁 βˆ₯ (𝑁 Β· π‘š))
155 elfzoelz 13656 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^π‘˜) β†’ 𝑖 ∈ β„€)
156155adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑖 ∈ β„€)
157156zcnd 12689 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑖 ∈ β„‚)
158136adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (𝑁 Β· π‘š) ∈ β„‚)
159157, 158pncan2d 11595 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ ((𝑖 + (𝑁 Β· π‘š)) βˆ’ 𝑖) = (𝑁 Β· π‘š))
160154, 159breqtrrd 5170 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑁 βˆ₯ ((𝑖 + (𝑁 Β· π‘š)) βˆ’ 𝑖))
16176nnnn0d 12554 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 𝑁 ∈ β„•0)
162161ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ 𝑁 ∈ β„•0)
163 zaddcl 12624 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ β„€ ∧ (𝑁 Β· π‘š) ∈ β„€) β†’ (𝑖 + (𝑁 Β· π‘š)) ∈ β„€)
164155, 118, 163syl2anr 596 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (𝑖 + (𝑁 Β· π‘š)) ∈ β„€)
16531, 33zndvds 21470 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ β„•0 ∧ (𝑖 + (𝑁 Β· π‘š)) ∈ β„€ ∧ 𝑖 ∈ β„€) β†’ ((πΏβ€˜(𝑖 + (𝑁 Β· π‘š))) = (πΏβ€˜π‘–) ↔ 𝑁 βˆ₯ ((𝑖 + (𝑁 Β· π‘š)) βˆ’ 𝑖)))
166162, 164, 156, 165syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ ((πΏβ€˜(𝑖 + (𝑁 Β· π‘š))) = (πΏβ€˜π‘–) ↔ 𝑁 βˆ₯ ((𝑖 + (𝑁 Β· π‘š)) βˆ’ 𝑖)))
167160, 166mpbird 257 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (πΏβ€˜(𝑖 + (𝑁 Β· π‘š))) = (πΏβ€˜π‘–))
168167fveq2d 6895 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))) = (π‘‹β€˜(πΏβ€˜π‘–)))
169168sumeq2dv 15673 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))) = Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘–)))
170 2fveq3 6896 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑛 β†’ (π‘‹β€˜(πΏβ€˜π‘–)) = (π‘‹β€˜(πΏβ€˜π‘›)))
171170cbvsumv 15666 . . . . . . . . . . . . . . . . . . 19 Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘–)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›))
172169, 171eqtrdi 2783 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑖 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜(𝑖 + (𝑁 Β· π‘š)))) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)))
173149, 172eqtrd 2767 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘š ∈ β„•0) ∧ π‘˜ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)))
174173ralrimiva 3141 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ βˆ€π‘˜ ∈ β„•0 Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)))
175116, 174, 161rspcdva 3608 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›)))
176 fveq2 6891 . . . . . . . . . . . . . . . . . 18 (π‘˜ = (πΏβ€˜π‘›) β†’ (π‘‹β€˜π‘˜) = (π‘‹β€˜(πΏβ€˜π‘›)))
1773nnne0d 12284 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝑁 β‰  0)
178 ifnefalse 4536 . . . . . . . . . . . . . . . . . . . 20 (𝑁 β‰  0 β†’ if(𝑁 = 0, β„€, (0..^𝑁)) = (0..^𝑁))
179177, 178syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ if(𝑁 = 0, β„€, (0..^𝑁)) = (0..^𝑁))
180 fzofi 13963 . . . . . . . . . . . . . . . . . . 19 (0..^𝑁) ∈ Fin
181179, 180eqeltrdi 2836 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ if(𝑁 = 0, β„€, (0..^𝑁)) ∈ Fin)
182 eqid 2727 . . . . . . . . . . . . . . . . . . . 20 (Baseβ€˜π‘) = (Baseβ€˜π‘)
18333reseq1i 5975 . . . . . . . . . . . . . . . . . . . 20 (𝐿 β†Ύ if(𝑁 = 0, β„€, (0..^𝑁))) = ((β„€RHomβ€˜π‘) β†Ύ if(𝑁 = 0, β„€, (0..^𝑁)))
184 eqid 2727 . . . . . . . . . . . . . . . . . . . 20 if(𝑁 = 0, β„€, (0..^𝑁)) = if(𝑁 = 0, β„€, (0..^𝑁))
18531, 182, 183, 184znf1o 21472 . . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ if(𝑁 = 0, β„€, (0..^𝑁))) β†’ ((𝐿 β†Ύ if(𝑁 = 0, β„€, (0..^𝑁)))β€˜π‘›) = (πΏβ€˜π‘›))
18930, 31, 32, 182, 34dchrf 27162 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋:(Baseβ€˜π‘)βŸΆβ„‚)
190189ffvelcdmda 7088 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ (Baseβ€˜π‘)) β†’ (π‘‹β€˜π‘˜) ∈ β„‚)
191176, 181, 186, 188, 190fsumf1o 15693 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ Ξ£π‘˜ ∈ (Baseβ€˜π‘)(π‘‹β€˜π‘˜) = Σ𝑛 ∈ if (𝑁 = 0, β„€, (0..^𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
192 rpvmasum.1 . . . . . . . . . . . . . . . . . . 19 1 = (0gβ€˜πΊ)
19330, 31, 32, 192, 34, 182dchrsum 27189 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ Ξ£π‘˜ ∈ (Baseβ€˜π‘)(π‘‹β€˜π‘˜) = if(𝑋 = 1 , (Ο•β€˜π‘), 0))
194 dchrisum.n1 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋 β‰  1 )
195 ifnefalse 4536 . . . . . . . . . . . . . . . . . . 19 (𝑋 β‰  1 β†’ if(𝑋 = 1 , (Ο•β€˜π‘), 0) = 0)
196194, 195syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ if(𝑋 = 1 , (Ο•β€˜π‘), 0) = 0)
197193, 196eqtrd 2767 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ Ξ£π‘˜ ∈ (Baseβ€˜π‘)(π‘‹β€˜π‘˜) = 0)
198179sumeq1d 15671 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ Σ𝑛 ∈ if (𝑁 = 0, β„€, (0..^𝑁))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›)))
199191, 197, 1983eqtr3rd 2776 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
200199adantr 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ (0..^𝑁)(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
201110, 175, 2003eqtrd 2771 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
202201oveq2d 7430 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (0 + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))) = (0 + 0))
203 00id 11411 . . . . . . . . . . . . 13 (0 + 0) = 0
204202, 203eqtr2di 2784 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ 0 = (0 + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))))
205101, 204eqeq12d 2743 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 ↔ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›))) = (0 + Σ𝑛 ∈ ((𝑁 Β· π‘š)..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)))))
20668, 205imbitrrid 245 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
207206expcom 413 . . . . . . . . 9 (π‘š ∈ β„•0 β†’ (πœ‘ β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0 β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
208207a2d 29 . . . . . . . 8 (π‘š ∈ β„•0 β†’ ((πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· π‘š))(π‘‹β€˜(πΏβ€˜π‘›)) = 0) β†’ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (π‘š + 1)))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)))
20944, 49, 54, 59, 67, 208nn0ind 12679 . . . . . . 7 ((βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0 β†’ (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0))
210209impcom 407 . . . . . 6 ((πœ‘ ∧ (βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
21115, 210syldan 590 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
212 modval 13860 . . . . . . . . . . 11 ((π‘ˆ ∈ ℝ ∧ 𝑁 ∈ ℝ+) β†’ (π‘ˆ mod 𝑁) = (π‘ˆ βˆ’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))))
2137, 10, 212syl2anc 583 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (π‘ˆ mod 𝑁) = (π‘ˆ βˆ’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))))
214213oveq2d 7430 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ βˆ’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))))
21516nn0cnd 12556 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) ∈ β„‚)
216 nn0cn 12504 . . . . . . . . . . 11 (π‘ˆ ∈ β„•0 β†’ π‘ˆ ∈ β„‚)
217216adantl 481 . . . . . . . . . 10 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ π‘ˆ ∈ β„‚)
218215, 217pncan3d 11596 . . . . . . . . 9 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ βˆ’ (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))) = π‘ˆ)
219214, 218eqtr2d 2768 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ π‘ˆ = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))
220219oveq2d 7430 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁))))
221220sumeq1d 15671 . . . . . 6 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)))
222 nn0z 12605 . . . . . . . 8 (π‘ˆ ∈ β„•0 β†’ π‘ˆ ∈ β„€)
223 zmodcl 13880 . . . . . . . 8 ((π‘ˆ ∈ β„€ ∧ 𝑁 ∈ β„•) β†’ (π‘ˆ mod 𝑁) ∈ β„•0)
224222, 3, 223syl2anr 596 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (π‘ˆ mod 𝑁) ∈ β„•0)
225174ralrimiva 3141 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘š ∈ β„•0 βˆ€π‘˜ ∈ β„•0 Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)))
226225adantr 480 . . . . . . 7 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ βˆ€π‘š ∈ β„•0 βˆ€π‘˜ ∈ β„•0 Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)))
227 oveq2 7422 . . . . . . . . . . 11 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (𝑁 Β· π‘š) = (𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))
228227oveq1d 7429 . . . . . . . . . . 11 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ ((𝑁 Β· π‘š) + π‘˜) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))
229227, 228oveq12d 7432 . . . . . . . . . 10 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜)) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜)))
230229sumeq1d 15671 . . . . . . . . 9 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)))
231230eqeq1d 2729 . . . . . . . 8 (π‘š = (βŒŠβ€˜(π‘ˆ / 𝑁)) β†’ (Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) ↔ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›))))
232 oveq2 7422 . . . . . . . . . . 11 (π‘˜ = (π‘ˆ mod 𝑁) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))
233232oveq2d 7430 . . . . . . . . . 10 (π‘˜ = (π‘ˆ mod 𝑁) β†’ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜)) = ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁))))
234233sumeq1d 15671 . . . . . . . . 9 (π‘˜ = (π‘ˆ mod 𝑁) β†’ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)))
235 oveq2 7422 . . . . . . . . . 10 (π‘˜ = (π‘ˆ mod 𝑁) β†’ (0..^π‘˜) = (0..^(π‘ˆ mod 𝑁)))
236235sumeq1d 15671 . . . . . . . . 9 (π‘˜ = (π‘ˆ mod 𝑁) β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
237234, 236eqeq12d 2743 . . . . . . . 8 (π‘˜ = (π‘ˆ mod 𝑁) β†’ (Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) ↔ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))))
238231, 237rspc2va 3619 . . . . . . 7 ((((βŒŠβ€˜(π‘ˆ / 𝑁)) ∈ β„•0 ∧ (π‘ˆ mod 𝑁) ∈ β„•0) ∧ βˆ€π‘š ∈ β„•0 βˆ€π‘˜ ∈ β„•0 Σ𝑛 ∈ ((𝑁 Β· π‘š)..^((𝑁 Β· π‘š) + π‘˜))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›))) β†’ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
23915, 224, 226, 238syl21anc 837 . . . . . 6 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))) + (π‘ˆ mod 𝑁)))(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
240221, 239eqtrd 2767 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
241211, 240oveq12d 7432 . . . 4 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (Σ𝑛 ∈ (0..^(𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁))))(π‘‹β€˜(πΏβ€˜π‘›)) + Σ𝑛 ∈ ((𝑁 Β· (βŒŠβ€˜(π‘ˆ / 𝑁)))..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›))) = (0 + Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))))
242 fzofi 13963 . . . . . . 7 (0..^(π‘ˆ mod 𝑁)) ∈ Fin
243242a1i 11 . . . . . 6 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (0..^(π‘ˆ mod 𝑁)) ∈ Fin)
24434ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^(π‘ˆ mod 𝑁))) β†’ 𝑋 ∈ 𝐷)
245 elfzoelz 13656 . . . . . . . 8 (𝑛 ∈ (0..^(π‘ˆ mod 𝑁)) β†’ 𝑛 ∈ β„€)
246245adantl 481 . . . . . . 7 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^(π‘ˆ mod 𝑁))) β†’ 𝑛 ∈ β„€)
24730, 31, 32, 33, 244, 246dchrzrhcl 27165 . . . . . 6 (((πœ‘ ∧ π‘ˆ ∈ β„•0) ∧ 𝑛 ∈ (0..^(π‘ˆ mod 𝑁))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
248243, 247fsumcl 15703 . . . . 5 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
249248addlidd 11437 . . . 4 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (0 + Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
25039, 241, 2493eqtrd 2771 . . 3 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ Σ𝑛 ∈ (0..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
251250fveq2d 6895 . 2 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›))) = (absβ€˜Ξ£π‘› ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))))
252 oveq2 7422 . . . . . 6 (𝑒 = (π‘ˆ mod 𝑁) β†’ (0..^𝑒) = (0..^(π‘ˆ mod 𝑁)))
253252sumeq1d 15671 . . . . 5 (𝑒 = (π‘ˆ mod 𝑁) β†’ Σ𝑛 ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›)))
254253fveq2d 6895 . . . 4 (𝑒 = (π‘ˆ mod 𝑁) β†’ (absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) = (absβ€˜Ξ£π‘› ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))))
255254breq1d 5152 . . 3 (𝑒 = (π‘ˆ mod 𝑁) β†’ ((absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅 ↔ (absβ€˜Ξ£π‘› ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅))
256 dchrisum.10 . . . 4 (πœ‘ β†’ βˆ€π‘’ ∈ (0..^𝑁)(absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
257256adantr 480 . . 3 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ βˆ€π‘’ ∈ (0..^𝑁)(absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
258 zmodfzo 13883 . . . 4 ((π‘ˆ ∈ β„€ ∧ 𝑁 ∈ β„•) β†’ (π‘ˆ mod 𝑁) ∈ (0..^𝑁))
259222, 3, 258syl2anr 596 . . 3 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (π‘ˆ mod 𝑁) ∈ (0..^𝑁))
260255, 257, 259rspcdva 3608 . 2 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^(π‘ˆ mod 𝑁))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
261251, 260eqbrtrd 5164 1 ((πœ‘ ∧ π‘ˆ ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^π‘ˆ)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099   β‰  wne 2935  βˆ€wral 3056   βˆͺ cun 3942   ∩ cin 3943  βˆ…c0 4318  ifcif 4524   class class class wbr 5142   ↦ cmpt 5225   β†Ύ cres 5674  β€“1-1-ontoβ†’wf1o 6541  β€˜cfv 6542  (class class class)co 7414  Fincfn 8955  β„‚cc 11128  β„cr 11129  0cc0 11130  1c1 11131   + caddc 11133   Β· cmul 11135   < clt 11270   ≀ cle 11271   βˆ’ cmin 11466   / cdiv 11893  β„•cn 12234  β„•0cn0 12494  β„€cz 12580  β„€β‰₯cuz 12844  β„+crp 12998  ...cfz 13508  ..^cfzo 13651  βŒŠcfl 13779   mod cmo 13858  abscabs 15205   β‡π‘Ÿ crli 15453  Ξ£csu 15656   βˆ₯ cdvds 16222  Ο•cphi 16724  Basecbs 17171  0gc0g 17412  β„€RHomczrh 21412  β„€/nβ„€czn 21415  DChrcdchr 27152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208  ax-addf 11209  ax-mulf 11210
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7865  df-1st 7987  df-2nd 7988  df-tpos 8225  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-oadd 8484  df-er 8718  df-ec 8720  df-qs 8724  df-map 8838  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-sup 9457  df-inf 9458  df-oi 9525  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-5 12300  df-6 12301  df-7 12302  df-8 12303  df-9 12304  df-n0 12495  df-xnn0 12567  df-z 12581  df-dec 12700  df-uz 12845  df-rp 12999  df-fz 13509  df-fzo 13652  df-fl 13781  df-mod 13859  df-seq 13991  df-exp 14051  df-hash 14314  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-clim 15456  df-sum 15657  df-dvds 16223  df-gcd 16461  df-phi 16726  df-struct 17107  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-plusg 17237  df-mulr 17238  df-starv 17239  df-sca 17240  df-vsca 17241  df-ip 17242  df-tset 17243  df-ple 17244  df-ds 17246  df-unif 17247  df-0g 17414  df-imas 17481  df-qus 17482  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-mhm 18731  df-grp 18884  df-minusg 18885  df-sbg 18886  df-mulg 19015  df-subg 19069  df-nsg 19070  df-eqg 19071  df-ghm 19159  df-cmn 19728  df-abl 19729  df-mgp 20066  df-rng 20084  df-ur 20113  df-ring 20166  df-cring 20167  df-oppr 20262  df-dvdsr 20285  df-unit 20286  df-invr 20316  df-rhm 20400  df-subrng 20472  df-subrg 20497  df-lmod 20734  df-lss 20805  df-lsp 20845  df-sra 21047  df-rgmod 21048  df-lidl 21093  df-rsp 21094  df-2idl 21133  df-cnfld 21267  df-zring 21360  df-zrh 21416  df-zn 21419  df-dchr 27153
This theorem is referenced by:  dchrisumlem2  27410
  Copyright terms: Public domain W3C validator