This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dchrisumlem1

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

Ref Expression
Hypotheses rpvmasum.z 
|- Z = ( Z/nZ ` N )
rpvmasum.l 
|- L = ( ZRHom ` Z )
rpvmasum.a 
|- ( ph -> N e. NN )
rpvmasum.g 
|- G = ( DChr ` N )
rpvmasum.d 
|- D = ( Base ` G )
rpvmasum.1 
|- .1. = ( 0g ` G )
dchrisum.b 
|- ( ph -> X e. D )
dchrisum.n1 
|- ( ph -> X =/= .1. )
dchrisum.2 
|- ( n = x -> A = B )
dchrisum.3 
|- ( ph -> M e. NN )
dchrisum.4 
|- ( ( ph /\ n e. RR+ ) -> A e. RR )
dchrisum.5 
|- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
dchrisum.6 
|- ( ph -> ( n e. RR+ |-> A ) ~~>r 0 )
dchrisum.7 
|- F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. A ) )
dchrisum.9 
|- ( ph -> R e. RR )
dchrisum.10 
|- ( ph -> A. u e. ( 0 ..^ N ) ( abs ` sum_ n e. ( 0 ..^ u ) ( X ` ( L ` n ) ) ) <_ R )
Assertion dchrisumlem1 
|- ( ( ph /\ U e. NN0 ) -> ( abs ` sum_ n e. ( 0 ..^ U ) ( X ` ( L ` n ) ) ) <_ R )

Proof

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