let u be integer-yielding FinSequence; for m being CR_Sequence st len m = len u holds
for c being CR_coefficients of m
for i being natural number st i in dom m holds
Sum (u (#) c),u . i are_congruent_mod m . i
let m be CR_Sequence; ( len m = len u implies for c being CR_coefficients of m
for i being natural number st i in dom m holds
Sum (u (#) c),u . i are_congruent_mod m . i )
assume A1:
len m = len u
; for c being CR_coefficients of m
for i being natural number st i in dom m holds
Sum (u (#) c),u . i are_congruent_mod m . i
let c be CR_coefficients of m; for i being natural number st i in dom m holds
Sum (u (#) c),u . i are_congruent_mod m . i
let i be natural number ; ( i in dom m implies Sum (u (#) c),u . i are_congruent_mod m . i )
defpred S1[ Nat] means for v, cc being integer-yielding FinSequence st v = u | $1 & cc = c | $1 & not ( $1 < i & Sum (v (#) cc), 0 are_congruent_mod m . i ) holds
( $1 >= i & Sum (v (#) cc),u . i are_congruent_mod m . i );
assume A2:
i in dom m
; Sum (u (#) c),u . i are_congruent_mod m . i
A3:
len m = len c
by Def4;
then A4: dom m =
Seg (len c)
by FINSEQ_1:def 3
.=
dom c
by FINSEQ_1:def 3
;
A5:
now let k be
Element of
NAT ;
( 0 <= k & k < len u & S1[k] implies S1[k + 1] )assume that
0 <= k
and A6:
k < len u
and A7:
S1[
k]
;
S1[k + 1]now set v9 =
u | k;
set cc9 =
c | k;
let v,
cc be
integer-yielding FinSequence;
( v = u | (k + 1) & cc = c | (k + 1) & not ( k + 1 < i & Sum (v (#) cc), 0 are_congruent_mod m . i ) implies ( k + 1 >= i & Sum (v (#) cc),u . i are_congruent_mod m . i ) )A8:
0 + 1
<= k + 1
by XREAL_1:8;
reconsider a =
v (#) cc,
b =
(u | k) (#) (c | k) as
FinSequence of
REAL by Lm5;
assume that A9:
v = u | (k + 1)
and A10:
cc = c | (k + 1)
;
( ( k + 1 < i & Sum (v (#) cc), 0 are_congruent_mod m . i ) or ( k + 1 >= i & Sum (v (#) cc),u . i are_congruent_mod m . i ) )
k + 1
<= len u
by A6, NAT_1:13;
then
len v = k + 1
by A9, FINSEQ_1:80;
then
k + 1
in Seg (len v)
by A8;
then
k + 1
in dom v
by FINSEQ_1:def 3;
then A11:
v . (k + 1) = u . (k + 1)
by A9, FUNCT_1:70;
A12:
k + 1
<= len c
by A1, A3, A6, NAT_1:13;
then
k + 1
in Seg (len c)
by A8;
then A13:
k + 1
in dom c
by FINSEQ_1:def 3;
reconsider r =
(v . (k + 1)) * (cc . (k + 1)) as
Element of
REAL by XREAL_0:def 1;
reconsider s =
<*r*> as
FinSequence of
REAL ;
A14:
len u = len c
by A1, Def4;
len cc = k + 1
by A10, A12, FINSEQ_1:80;
then
k + 1
in Seg (len cc)
by A8;
then
k + 1
in dom cc
by FINSEQ_1:def 3;
then A15:
cc . (k + 1) = c . (k + 1)
by A10, FUNCT_1:70;
A16:
k + 1
<= len u
by A6, NAT_1:13;
A17:
((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*> = (u (#) c) | (k + 1)
proof
set p =
((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>;
set q =
(u (#) c) | (k + 1);
A18:
k + 1
<= len (u (#) c)
by A1, A3, A16, Lm4;
then A19:
k <= len (u (#) c)
by NAT_1:13;
A20:
len (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) =
(len ((u (#) c) | k)) + 1
by FINSEQ_2:19
.=
k + 1
by A19, FINSEQ_1:80
;
A21:
k + 1
= len ((u (#) c) | (k + 1))
by A18, FINSEQ_1:80;
now let j be
Nat;
( 1 <= j & j <= len (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) implies (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . b1 = ((u (#) c) | (k + 1)) . b1 )assume that A22:
1
<= j
and A23:
j <= len (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>)
;
(((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . b1 = ((u (#) c) | (k + 1)) . b1A24:
j in NAT
by ORDINAL1:def 13;
per cases
( j in dom ((u (#) c) | k) or not j in dom ((u (#) c) | k) )
;
suppose A27:
not
j in dom ((u (#) c) | k)
;
(((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . b1 = ((u (#) c) | (k + 1)) . b1
k <= len (u (#) c)
by A6, A14, Lm4;
then A28:
len ((u (#) c) | k) = k
by FINSEQ_1:80;
then
dom ((u (#) c) | k) = Seg k
by FINSEQ_1:def 3;
then
j > k
by A22, A24, A27;
then A29:
j >= k + 1
by NAT_1:13;
then A30:
j = k + 1
by A20, A23, XXREAL_0:1;
dom <*((v . (k + 1)) * (cc . (k + 1)))*> = {1}
by FINSEQ_1:4, FINSEQ_1:55;
then
1
in dom <*((v . (k + 1)) * (cc . (k + 1)))*>
by TARSKI:def 1;
then A31:
(((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . (k + 1) =
<*((v . (k + 1)) * (cc . (k + 1)))*> . 1
by A28, FINSEQ_1:def 7
.=
(v . (k + 1)) * (cc . (k + 1))
by FINSEQ_1:57
;
k + 1
<= len (u (#) c)
by A12, A14, Lm4;
then
j in Seg (len (u (#) c))
by A8, A30;
then A32:
j in dom (u (#) c)
by FINSEQ_1:def 3;
j in Seg (k + 1)
by A20, A22, A23, A24;
then
j in dom ((u (#) c) | (k + 1))
by A21, FINSEQ_1:def 3;
then ((u (#) c) | (k + 1)) . j =
(u (#) c) . j
by FUNCT_1:70
.=
(v . (k + 1)) * (cc . (k + 1))
by A15, A11, A30, A32, VALUED_1:def 4
;
hence
(((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . j = ((u (#) c) | (k + 1)) . j
by A20, A23, A29, A31, XXREAL_0:1;
verum end; end;
hence
((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*> = (u (#) c) | (k + 1)
by A20, A21, FINSEQ_1:18;
verum
end;
(u | k) (#) (c | k) = (u (#) c) | k
by A6, A14, Th4;
then
a = b ^ s
by A9, A10, A16, A14, A17, Th4;
then A33:
Sum (v (#) cc) =
(Sum b) + (Sum s)
by RVSUM_1:105
.=
(Sum ((u | k) (#) (c | k))) + ((v . (k + 1)) * (cc . (k + 1)))
by RVSUM_1:103
;
A34:
k < k + 1
by NAT_1:13;
now per cases
( k + 1 < i or k + 1 = i or k + 1 > i )
by XXREAL_0:1;
case A35:
k + 1
< i
;
Sum (v (#) cc), 0 are_congruent_mod m . ithen
k < i
by NAT_1:13;
then A36:
Sum ((u | k) (#) (c | k)),
0 are_congruent_mod m . i
by A7;
A37:
v . (k + 1),
v . (k + 1) are_congruent_mod m . i
by INT_1:32;
cc . (k + 1),
0 are_congruent_mod m . i
by A2, A4, A13, A15, A35, Th27;
then
(v . (k + 1)) * (cc . (k + 1)),
(v . (k + 1)) * 0 are_congruent_mod m . i
by A37, INT_1:39;
then
Sum (v (#) cc),
0 + ((v . (k + 1)) * 0 ) are_congruent_mod m . i
by A33, A36, INT_1:37;
hence
Sum (v (#) cc),
0 are_congruent_mod m . i
;
verum end; case A38:
k + 1
= i
;
Sum (v (#) cc),0 + (u . i) are_congruent_mod m . iA39:
v . (k + 1),
v . (k + 1) are_congruent_mod m . i
by INT_1:32;
cc . (k + 1),1
are_congruent_mod m . i
by A13, A15, A38, Th26;
then A40:
(v . (k + 1)) * (cc . (k + 1)),
(u . (k + 1)) * 1
are_congruent_mod m . i
by A11, A39, INT_1:39;
Sum ((u | k) (#) (c | k)),
0 are_congruent_mod m . i
by A7, A34, A38;
hence
Sum (v (#) cc),
0 + (u . i) are_congruent_mod m . i
by A33, A38, A40, INT_1:37;
verum end; case A41:
k + 1
> i
;
Sum (v (#) cc),(u . i) + 0 are_congruent_mod m . ithen
k >= i
by NAT_1:13;
then A42:
Sum ((u | k) (#) (c | k)),
u . i are_congruent_mod m . i
by A7;
A43:
v . (k + 1),
v . (k + 1) are_congruent_mod m . i
by INT_1:32;
cc . (k + 1),
0 are_congruent_mod m . i
by A2, A4, A13, A15, A41, Th27;
then
(v . (k + 1)) * (cc . (k + 1)),
(u . (k + 1)) * 0 are_congruent_mod m . i
by A11, A43, INT_1:39;
hence
Sum (v (#) cc),
(u . i) + 0 are_congruent_mod m . i
by A33, A42, INT_1:37;
verum end; hence
( (
k + 1
< i &
Sum (v (#) cc),
0 are_congruent_mod m . i ) or (
k + 1
>= i &
Sum (v (#) cc),
u . i are_congruent_mod m . i ) )
;
verum end; hence
S1[
k + 1]
;
verum end;
A44:
dom m = Seg (len u)
by A1, FINSEQ_1:def 3;
now let v,
cc be
integer-yielding FinSequence;
( v = u | 0 & cc = c | 0 & not ( 0 < i & Sum (v (#) cc), 0 are_congruent_mod m . i ) implies ( 0 >= i & Sum (v (#) cc),u . i are_congruent_mod m . i ) )assume that A45:
v = u | 0
and A46:
cc = c | 0
;
( ( 0 < i & Sum (v (#) cc), 0 are_congruent_mod m . i ) or ( 0 >= i & Sum (v (#) cc),u . i are_congruent_mod m . i ) )
(dom v) /\ (dom cc) = {}
by A45, A46;
then
dom (v (#) cc) = {}
by VALUED_1:def 4;
then
v (#) cc = {}
;
hence
( (
0 < i &
Sum (v (#) cc),
0 are_congruent_mod m . i ) or (
0 >= i &
Sum (v (#) cc),
u . i are_congruent_mod m . i ) )
by A2, A44, FINSEQ_1:3, INT_1:32, RVSUM_1:102;
verum end;
then A47:
S1[ 0 ]
;
A48:
for k being Element of NAT st 0 <= k & k <= len u holds
S1[k]
from INT_1:sch 7(A47, A5);
len u = len c
by A1, Def4;
then A49:
c | (len u) = c
by FINSEQ_1:79;
A50:
u = u | (len u)
by FINSEQ_1:79;
i <= len u
by A2, A44, FINSEQ_1:3;
hence
Sum (u (#) c),u . i are_congruent_mod m . i
by A48, A50, A49; verum