let u be integer-yielding FinSequence; :: thesis: 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; :: thesis: ( 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 AS1:
len m = len u
; :: thesis: 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; :: thesis: 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 ; :: thesis: ( i in dom m implies Sum (u (#) c),u . i are_congruent_mod m . i )
assume AS2:
i in dom m
; :: thesis: Sum (u (#) c),u . i are_congruent_mod m . i
AS3:
len m = len c
by defCi;
then K: dom m =
Seg (len c)
by FINSEQ_1:def 3
.=
dom c
by FINSEQ_1:def 3
;
J1:
dom m = Seg (len u)
by AS1, FINSEQ_1:def 3;
then J:
( 1 <= i & i <= len u )
by AS2, FINSEQ_1:3;
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 );
now let v,
cc be
integer-yielding FinSequence;
:: thesis: ( 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
(
v = u | 0 &
cc = c | 0 )
;
:: thesis: ( ( 0 < i & Sum (v (#) cc), 0 are_congruent_mod m . i ) or ( 0 >= i & Sum (v (#) cc),u . i are_congruent_mod m . i ) )then
(dom v) /\ (dom cc) = {}
;
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 J1, AS2, FINSEQ_1:3, INT_1:32, RVSUM_1:102;
:: thesis: verum end;
then A:
S1[ 0 ]
;
B:
now let k be
Element of
NAT ;
:: thesis: ( 0 <= k & k < len u & S1[k] implies S1[k + 1] )assume C0:
(
0 <= k &
k < len u &
S1[
k] )
;
:: thesis: S1[k + 1]now let v,
cc be
integer-yielding FinSequence;
:: thesis: ( 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 ) )assume C:
(
v = u | (k + 1) &
cc = c | (k + 1) )
;
:: thesis: ( ( 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 ) )set v' =
u | k;
set cc' =
c | k;
F1:
0 + 1
<= k + 1
by XREAL_1:8;
then F1a:
( 1
<= k + 1 &
k + 1
<= len c )
by AS1, AS3, C0, NAT_1:13;
then
k + 1
in Seg (len c)
;
then C1:
k + 1
in dom c
by FINSEQ_1:def 3;
len cc = k + 1
by C, F1a, FINSEQ_1:80;
then
k + 1
in Seg (len cc)
by F1;
then E1:
k + 1
in dom cc
by FINSEQ_1:def 3;
k + 1
<= len u
by C0, NAT_1:13;
then
len v = k + 1
by C, FINSEQ_1:80;
then
k + 1
in Seg (len v)
by F1;
then E2:
k + 1
in dom v
by FINSEQ_1:def 3;
F3:
k + 1
<= len u
by C0, NAT_1:13;
C5:
cc . (k + 1) = c . (k + 1)
by E1, C, FUNCT_1:70;
C2:
v . (k + 1) = u . (k + 1)
by E2, C, FUNCT_1:70;
E4:
len u = len c
by AS1, defCi;
C6:
(u | k) (#) (c | k) = (u (#) c) | k
by E4, Z10, C0;
reconsider r =
(v . (k + 1)) * (cc . (k + 1)) as
Element of
REAL by XREAL_0:def 1;
reconsider s =
<*r*> as
FinSequence of
REAL ;
reconsider a =
v (#) cc,
b =
(u | k) (#) (c | k) as
FinSequence of
REAL by ZZ1;
C4:
k < k + 1
by NAT_1:13;
((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);
G1:
k + 1
<= len (u (#) c)
by AS1, AS3, F3, length3;
then G2:
k <= len (u (#) c)
by NAT_1:13;
Ga:
len (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) =
(len ((u (#) c) | k)) + 1
by FINSEQ_2:19
.=
k + 1
by G2, FINSEQ_1:80
;
Gb:
k + 1
= len ((u (#) c) | (k + 1))
by G1, FINSEQ_1:80;
now let j be
Nat;
:: thesis: ( 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 X:
( 1
<= j &
j <= len (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) )
;
:: thesis: (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . b1 = ((u (#) c) | (k + 1)) . b1A:
j in NAT
by ORDINAL1:def 13;
per cases
( j in dom ((u (#) c) | k) or not j in dom ((u (#) c) | k) )
;
suppose G3:
not
j in dom ((u (#) c) | k)
;
:: thesis: (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . b1 = ((u (#) c) | (k + 1)) . b1
k <= len (u (#) c)
by E4, C0, length3;
then G8:
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 A, X, G3;
then G5a:
(
j >= k + 1 &
j <= k + 1 )
by X, Ga, NAT_1:13;
then G5:
j = k + 1
by XXREAL_0:1;
j in Seg (k + 1)
by A, X, Ga;
then G4:
j in dom ((u (#) c) | (k + 1))
by Gb, FINSEQ_1:def 3;
k + 1
<= len (u (#) c)
by F1a, E4, length3;
then
j in Seg (len (u (#) c))
by G5, F1;
then G6:
j in dom (u (#) c)
by FINSEQ_1:def 3;
G7:
((u (#) c) | (k + 1)) . j =
(u (#) c) . j
by G4, FUNCT_1:70
.=
(v . (k + 1)) * (cc . (k + 1))
by G5, C2, C5, G6, VALUED_1:def 4
;
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 (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . (k + 1) =
<*((v . (k + 1)) * (cc . (k + 1)))*> . 1
by G8, FINSEQ_1:def 7
.=
(v . (k + 1)) * (cc . (k + 1))
by FINSEQ_1:57
;
hence
(((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . j = ((u (#) c) | (k + 1)) . j
by G7, G5a, XXREAL_0:1;
:: thesis: verum end; end;
hence
((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*> = (u (#) c) | (k + 1)
by Ga, Gb, FINSEQ_1:18;
:: thesis: verum
end; then X:
a = b ^ s
by F3, C, E4, Z10, C6;
C3:
Sum (v (#) cc) =
(Sum b) + (Sum s)
by X, RVSUM_1:105
.=
(Sum ((u | k) (#) (c | k))) + ((v . (k + 1)) * (cc . (k + 1)))
by RVSUM_1:103
;
now per cases
( k + 1 < i or k + 1 = i or k + 1 > i )
by XXREAL_0:1;
case D0:
k + 1
< i
;
:: thesis: Sum (v (#) cc), 0 are_congruent_mod m . ithen
k < i
by NAT_1:13;
then D1:
Sum ((u | k) (#) (c | k)),
0 are_congruent_mod m . i
by C0;
D2:
cc . (k + 1),
0 are_congruent_mod m . i
by C5, K, C1, D0, AS2, l2;
v . (k + 1),
v . (k + 1) are_congruent_mod m . i
by INT_1:32;
then
(v . (k + 1)) * (cc . (k + 1)),
(v . (k + 1)) * 0 are_congruent_mod m . i
by D2, INT_1:39;
then
Sum (v (#) cc),
0 + ((v . (k + 1)) * 0 ) are_congruent_mod m . i
by C3, D1, INT_1:37;
hence
Sum (v (#) cc),
0 are_congruent_mod m . i
;
:: thesis: verum end; case D0:
k + 1
= i
;
:: thesis: Sum (v (#) cc),0 + (u . i) are_congruent_mod m . ithen D1:
Sum ((u | k) (#) (c | k)),
0 are_congruent_mod m . i
by C4, C0;
D2:
cc . (k + 1),1
are_congruent_mod m . i
by C5, C1, D0, l1;
v . (k + 1),
v . (k + 1) are_congruent_mod m . i
by INT_1:32;
then
(v . (k + 1)) * (cc . (k + 1)),
(u . (k + 1)) * 1
are_congruent_mod m . i
by C2, D2, INT_1:39;
hence
Sum (v (#) cc),
0 + (u . i) are_congruent_mod m . i
by D1, C3, D0, INT_1:37;
:: thesis: verum end; case D0:
k + 1
> i
;
:: thesis: Sum (v (#) cc),(u . i) + 0 are_congruent_mod m . ithen
k >= i
by NAT_1:13;
then D1:
Sum ((u | k) (#) (c | k)),
u . i are_congruent_mod m . i
by C0;
D2:
cc . (k + 1),
0 are_congruent_mod m . i
by C5, K, C1, D0, AS2, l2;
v . (k + 1),
v . (k + 1) are_congruent_mod m . i
by INT_1:32;
then
(v . (k + 1)) * (cc . (k + 1)),
(u . (k + 1)) * 0 are_congruent_mod m . i
by C2, D2, INT_1:39;
hence
Sum (v (#) cc),
(u . i) + 0 are_congruent_mod m . i
by D1, C3, INT_1:37;
:: thesis: 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 ) )
;
:: thesis: verum end; hence
S1[
k + 1]
;
:: thesis: verum end;
I:
for k being Element of NAT st 0 <= k & k <= len u holds
S1[k]
from POLYNOM2:sch 4(A, B);
len u = len c
by AS1, defCi;
then
( u = u | (len u) & c | (len u) = c )
by FINSEQ_1:79;
hence
Sum (u (#) c),u . i are_congruent_mod m . i
by I, J; :: thesis: verum