let u be INT -valued FinSequence; :: thesis: for m being CR_Sequence
for z1, z2 being Integer st 0 <= z1 & z1 < Product m & ( for i being Nat st i in dom m holds
z1,u . i are_congruent_mod m . i ) & 0 <= z2 & z2 < Product m & ( for i being Nat st i in dom m holds
z2,u . i are_congruent_mod m . i ) holds
z1 = z2
let m be CR_Sequence; :: thesis: for z1, z2 being Integer st 0 <= z1 & z1 < Product m & ( for i being Nat st i in dom m holds
z1,u . i are_congruent_mod m . i ) & 0 <= z2 & z2 < Product m & ( for i being Nat st i in dom m holds
z2,u . i are_congruent_mod m . i ) holds
z1 = z2
let z1, z2 be Integer; :: thesis: ( 0 <= z1 & z1 < Product m & ( for i being Nat st i in dom m holds
z1,u . i are_congruent_mod m . i ) & 0 <= z2 & z2 < Product m & ( for i being Nat st i in dom m holds
z2,u . i are_congruent_mod m . i ) implies z1 = z2 )
assume that
A1: 0 <= z1 and
A2: z1 < Product m and
A3: for i being Nat st i in dom m holds
z1,u . i are_congruent_mod m . i and
A4: 0 <= z2 and
A5: z2 < Product m and
A6: for i being Nat st i in dom m holds
z2,u . i are_congruent_mod m . i ; :: thesis: z1 = z2
defpred S1[ Nat] means for m1 being CR_Sequence st m1 = m | $1 holds
z1,z2 are_congruent_mod Product m1;
A7: now :: thesis: for i being Element of NAT st i in dom m holds
z1,z2 are_congruent_mod m . i
let i be Element of NAT ; :: thesis: ( i in dom m implies z1,z2 are_congruent_mod m . i )
assume A8: i in dom m ; :: thesis: z1,z2 are_congruent_mod m . i
then A9: u . i,z2 are_congruent_mod m . i by A6, INT_1:14;
z1,u . i are_congruent_mod m . i by A3, A8;
hence z1,z2 are_congruent_mod m . i by A9, INT_1:15; :: thesis: verum
end;
A10: now :: thesis: for k being Element of NAT st 0 <= k & k < len m & S1[k] holds
S1[k + 1]
let k be Element of NAT ; :: thesis: ( 0 <= k & k < len m & S1[k] implies S1[k + 1] )
assume that
0 <= k and
A11: k < len m ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A12: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for m1 being CR_Sequence st m1 = m | (k + 1) holds
z1,z2 are_congruent_mod Product m1
set m2 = m | k;
let m1 be CR_Sequence; :: thesis: ( m1 = m | (k + 1) implies z1,z2 are_congruent_mod Product b1 )
A13: 1 <= k + 1 by NAT_1:11;
A14: k + 1 <= len m by A11, NAT_1:13;
then k + 1 in Seg (len m) by A13;
then A15: k + 1 in dom m by FINSEQ_1:def 3;
assume A16: m1 = m | (k + 1) ; :: thesis: z1,z2 are_congruent_mod Product b1
then A17: len m1 = k + 1 by A14, FINSEQ_1:59;
then k + 1 in Seg (len m1) by A13;
then A18: k + 1 in dom m1 by FINSEQ_1:def 3;
per cases ( k > 0 or k = 0 ) ;
suppose k > 0 ; :: thesis: z1,z2 are_congruent_mod Product b1
then reconsider m2 = m | k as CR_Sequence by A11, Th24;
set mm = (Product m1) / (m1 . (k + 1));
A19: z1,z2 are_congruent_mod Product m2 by A12;
reconsider m9 = m as FinSequence of INT by Lm1;
A20: m . (k + 1) = m1 . (k + 1) by A16, A18, FUNCT_1:47;
m . (k + 1) in rng m by A15, FUNCT_1:3;
then A21: m1 . (k + 1) > 0 by A20, PARTFUN3:def 1;
reconsider mm = (Product m1) / (m1 . (k + 1)) as Integer by A18, Th9;
A22: mm * (m1 . (k + 1)) = (Product m1) * (((m1 . (k + 1)) ") * (m1 . (k + 1)))
.= (Product m1) * 1 by A21, XCMPLX_0:def 7
.= Product m1 ;
(m9 | (k + 1)) | k = m9 | k by FINSEQ_1:82, NAT_1:11;
then m1 = m2 ^ <*(m1 . (k + 1))*> by A16, A17, FINSEQ_3:55;
then Product m1 = (Product m2) * (m1 . (k + 1)) by RVSUM_1:96;
then mm = (Product m2) * ((m1 . (k + 1)) * ((m1 . (k + 1)) ")) ;
then A23: mm = (Product m2) * 1 by A21, XCMPLX_0:def 7;
z1,z2 are_congruent_mod m1 . (k + 1) by A7, A15, A20;
hence z1,z2 are_congruent_mod Product m1 by A18, A19, A23, A22, Th21, Th25; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A27: m | (len m) = m by FINSEQ_1:58;
A28: S1[ 0 ] ;
for k being Element of NAT st 0 <= k & k <= len m holds
S1[k] from INT_1:sch 7(A28, A10);
 then A29: z1,z2 are_congruent_mod Product m by A27;
thus z1 = z1 mod (Product m) by A1, A2, NAT_D:63
.= z2 mod (Product m) by A29, NAT_D:64
.= z2 by A4, A5, NAT_D:63 ; :: thesis: verum