:: INT_6 semantic presentation
begin
Lm1: for f being INT -valued FinSequence holds f is FinSequence of INT
proof
let f be INT -valued FinSequence; ::_thesis: f is FinSequence of INT
rng f c= INT by RELAT_1:def_19;
hence f is FinSequence of INT by FINSEQ_1:def_4; ::_thesis: verum
end;
registration
let f be complex-valued FinSequence;
let n be Nat;
clusterf | n -> complex-valued ;
coherence
f | n is complex-valued ;
end;
registration
let f be INT -valued FinSequence;
let n be Nat;
clusterf | n -> INT -valued ;
coherence
f | n is INT -valued ;
end;
registration
let f be INT -valued FinSequence;
let n be Nat;
clusterf /^ n -> INT -valued ;
coherence
f /^ n is INT -valued
proof
percases ( n > len f or n <= len f ) ;
suppose n > len f ; ::_thesis: f /^ n is INT -valued
hence f /^ n is INT -valued by RFINSEQ:def_1; ::_thesis: verum
end;
supposeA1: n <= len f ; ::_thesis: f /^ n is INT -valued
now__::_thesis:_for_u_being_set_st_u_in_rng_(f_/^_n)_holds_
u_in_INT
reconsider f9 = f as FinSequence of INT by Lm1;
let u be set ; ::_thesis: ( u in rng (f /^ n) implies u in INT )
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
A2: rng f c= INT by RELAT_1:def_19;
assume u in rng (f /^ n) ; ::_thesis: u in INT
then consider x being set such that
A3: x in dom (f /^ n) and
A4: (f /^ n) . x = u by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A3;
x + n9 in dom f9 by A3, FINSEQ_5:26;
then A5: f . (x + n) in rng f by FUNCT_1:def_3;
(f /^ n) . x = f . (x + n) by A1, A3, RFINSEQ:def_1;
hence u in INT by A4, A5, A2; ::_thesis: verum
end;
then rng (f /^ n) c= INT by TARSKI:def_3;
hence f /^ n is INT -valued by RELAT_1:def_19; ::_thesis: verum
end;
end;
end;
end;
registration
let i be Integer;
cluster<*i*> -> INT -valued ;
coherence
<*i*> is INT -valued
proof
for u being set st u in {i} holds
u in INT by INT_1:def_2;
then A1: {i} c= INT by TARSKI:def_3;
rng <*i*> = {i} by FINSEQ_1:39;
hence <*i*> is INT -valued by A1, RELAT_1:def_19; ::_thesis: verum
end;
end;
registration
let f, g be INT -valued FinSequence;
clusterf ^ g -> INT -valued ;
coherence
f ^ g is INT -valued
proof
now__::_thesis:_for_u_being_set_st_u_in_rng_(f_^_g)_holds_
u_in_INT
let u be set ; ::_thesis: ( u in rng (f ^ g) implies u in INT )
A1: rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:31;
assume A2: u in rng (f ^ g) ; ::_thesis: u in INT
now__::_thesis:_(_(_u_in_rng_f_&_u_in_INT_)_or_(_u_in_rng_g_&_u_in_INT_)_)
percases ( u in rng f or u in rng g ) by A2, A1, XBOOLE_0:def_3;
caseA3: u in rng f ; ::_thesis: u in INT
rng f c= INT by RELAT_1:def_19;
hence u in INT by A3; ::_thesis: verum
end;
caseA4: u in rng g ; ::_thesis: u in INT
rng g c= INT by RELAT_1:def_19;
hence u in INT by A4; ::_thesis: verum
end;
end;
end;
hence u in INT ; ::_thesis: verum
end;
then rng (f ^ g) c= INT by TARSKI:def_3;
hence f ^ g is INT -valued by RELAT_1:def_19; ::_thesis: verum
end;
end;
theorem Th1: :: INT_6:1
for f1, f2 being complex-valued FinSequence holds len (f1 + f2) = min ((len f1),(len f2))
proof
let f1, f2 be complex-valued FinSequence; ::_thesis: len (f1 + f2) = min ((len f1),(len f2))
set g = f1 + f2;
consider n1 being Nat such that
A1: dom f1 = Seg n1 by FINSEQ_1:def_2;
n1 in NAT by ORDINAL1:def_12;
then A2: len f1 = n1 by A1, FINSEQ_1:def_3;
consider n2 being Nat such that
A3: dom f2 = Seg n2 by FINSEQ_1:def_2;
n2 in NAT by ORDINAL1:def_12;
then A4: len f2 = n2 by A3, FINSEQ_1:def_3;
A5: dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def_1;
now__::_thesis:_(_(_n1_<=_n2_&_len_(f1_+_f2)_=_min_((len_f1),(len_f2))_)_or_(_n2_<=_n1_&_len_(f1_+_f2)_=_min_((len_f1),(len_f2))_)_)
percases ( n1 <= n2 or n2 <= n1 ) ;
caseA6: n1 <= n2 ; ::_thesis: len (f1 + f2) = min ((len f1),(len f2))
then dom f1 c= dom f2 by A1, A3, FINSEQ_1:5;
then A7: dom (f1 + f2) = Seg n1 by A1, A5, XBOOLE_1:28;
min (n1,n2) = n1 by A6, XXREAL_0:def_9;
hence len (f1 + f2) = min ((len f1),(len f2)) by A2, A4, A7, FINSEQ_1:def_3; ::_thesis: verum
end;
caseA8: n2 <= n1 ; ::_thesis: len (f1 + f2) = min ((len f1),(len f2))
then dom f2 c= dom f1 by A1, A3, FINSEQ_1:5;
then A9: dom (f1 + f2) = Seg n2 by A3, A5, XBOOLE_1:28;
min (n1,n2) = n2 by A8, XXREAL_0:def_9;
hence len (f1 + f2) = min ((len f1),(len f2)) by A2, A4, A9, FINSEQ_1:def_3; ::_thesis: verum
end;
end;
end;
hence len (f1 + f2) = min ((len f1),(len f2)) ; ::_thesis: verum
end;
theorem Th2: :: INT_6:2
for f1, f2 being complex-valued FinSequence holds len (f1 - f2) = min ((len f1),(len f2))
proof
let f1, f2 be complex-valued FinSequence; ::_thesis: len (f1 - f2) = min ((len f1),(len f2))
set g = f1 - f2;
consider n1 being Nat such that
A1: dom f1 = Seg n1 by FINSEQ_1:def_2;
n1 in NAT by ORDINAL1:def_12;
then A2: len f1 = n1 by A1, FINSEQ_1:def_3;
consider n2 being Nat such that
A3: dom f2 = Seg n2 by FINSEQ_1:def_2;
n2 in NAT by ORDINAL1:def_12;
then A4: len f2 = n2 by A3, FINSEQ_1:def_3;
A5: dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_1:12;
now__::_thesis:_(_(_n1_<=_n2_&_len_(f1_-_f2)_=_min_((len_f1),(len_f2))_)_or_(_n2_<=_n1_&_len_(f1_-_f2)_=_min_((len_f1),(len_f2))_)_)
percases ( n1 <= n2 or n2 <= n1 ) ;
caseA6: n1 <= n2 ; ::_thesis: len (f1 - f2) = min ((len f1),(len f2))
then dom f1 c= dom f2 by A1, A3, FINSEQ_1:5;
then A7: dom (f1 - f2) = Seg n1 by A1, A5, XBOOLE_1:28;
min (n1,n2) = n1 by A6, XXREAL_0:def_9;
hence len (f1 - f2) = min ((len f1),(len f2)) by A2, A4, A7, FINSEQ_1:def_3; ::_thesis: verum
end;
caseA8: n2 <= n1 ; ::_thesis: len (f1 - f2) = min ((len f1),(len f2))
then dom f2 c= dom f1 by A1, A3, FINSEQ_1:5;
then A9: dom (f1 - f2) = Seg n2 by A3, A5, XBOOLE_1:28;
min (n1,n2) = n2 by A8, XXREAL_0:def_9;
hence len (f1 - f2) = min ((len f1),(len f2)) by A2, A4, A9, FINSEQ_1:def_3; ::_thesis: verum
end;
end;
end;
hence len (f1 - f2) = min ((len f1),(len f2)) ; ::_thesis: verum
end;
theorem Th3: :: INT_6:3
for f1, f2 being complex-valued FinSequence holds len (f1 (#) f2) = min ((len f1),(len f2))
proof
let f1, f2 be complex-valued FinSequence; ::_thesis: len (f1 (#) f2) = min ((len f1),(len f2))
set g = f1 (#) f2;
consider n1 being Nat such that
A1: dom f1 = Seg n1 by FINSEQ_1:def_2;
n1 in NAT by ORDINAL1:def_12;
then A2: len f1 = n1 by A1, FINSEQ_1:def_3;
consider n2 being Nat such that
A3: dom f2 = Seg n2 by FINSEQ_1:def_2;
n2 in NAT by ORDINAL1:def_12;
then A4: len f2 = n2 by A3, FINSEQ_1:def_3;
A5: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def_4;
now__::_thesis:_(_(_n1_<=_n2_&_len_(f1_(#)_f2)_=_min_((len_f1),(len_f2))_)_or_(_n2_<=_n1_&_len_(f1_(#)_f2)_=_min_((len_f1),(len_f2))_)_)
percases ( n1 <= n2 or n2 <= n1 ) ;
caseA6: n1 <= n2 ; ::_thesis: len (f1 (#) f2) = min ((len f1),(len f2))
then dom f1 c= dom f2 by A1, A3, FINSEQ_1:5;
then A7: dom (f1 (#) f2) = Seg n1 by A1, A5, XBOOLE_1:28;
min (n1,n2) = n1 by A6, XXREAL_0:def_9;
hence len (f1 (#) f2) = min ((len f1),(len f2)) by A2, A4, A7, FINSEQ_1:def_3; ::_thesis: verum
end;
caseA8: n2 <= n1 ; ::_thesis: len (f1 (#) f2) = min ((len f1),(len f2))
then dom f2 c= dom f1 by A1, A3, FINSEQ_1:5;
then A9: dom (f1 (#) f2) = Seg n2 by A3, A5, XBOOLE_1:28;
min (n1,n2) = n2 by A8, XXREAL_0:def_9;
hence len (f1 (#) f2) = min ((len f1),(len f2)) by A2, A4, A9, FINSEQ_1:def_3; ::_thesis: verum
end;
end;
end;
hence len (f1 (#) f2) = min ((len f1),(len f2)) ; ::_thesis: verum
end;
Lm2: for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
len (m1 + m2) = len m1
proof
let m1, m2 be complex-valued FinSequence; ::_thesis: ( len m1 = len m2 implies len (m1 + m2) = len m1 )
assume A1: len m1 = len m2 ; ::_thesis: len (m1 + m2) = len m1
thus len (m1 + m2) = min ((len m1),(len m2)) by Th1
.= len m1 by A1 ; ::_thesis: verum
end;
Lm3: for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
len (m1 - m2) = len m1
proof
let m1, m2 be complex-valued FinSequence; ::_thesis: ( len m1 = len m2 implies len (m1 - m2) = len m1 )
assume A1: len m1 = len m2 ; ::_thesis: len (m1 - m2) = len m1
thus len (m1 - m2) = min ((len m1),(len m2)) by Th2
.= len m1 by A1 ; ::_thesis: verum
end;
Lm4: for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
len (m1 (#) m2) = len m1
proof
let m1, m2 be complex-valued FinSequence; ::_thesis: ( len m1 = len m2 implies len (m1 (#) m2) = len m1 )
assume A1: len m1 = len m2 ; ::_thesis: len (m1 (#) m2) = len m1
thus len (m1 (#) m2) = min ((len m1),(len m2)) by Th3
.= len m1 by A1 ; ::_thesis: verum
end;
theorem Th4: :: INT_6:4
for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
for k being Nat st k <= len m1 holds
(m1 (#) m2) | k = (m1 | k) (#) (m2 | k)
proof
let m1, m2 be complex-valued FinSequence; ::_thesis: ( len m1 = len m2 implies for k being Nat st k <= len m1 holds
(m1 (#) m2) | k = (m1 | k) (#) (m2 | k) )
assume A1: len m1 = len m2 ; ::_thesis: for k being Nat st k <= len m1 holds
(m1 (#) m2) | k = (m1 | k) (#) (m2 | k)
let k9 be Nat; ::_thesis: ( k9 <= len m1 implies (m1 (#) m2) | k9 = (m1 | k9) (#) (m2 | k9) )
set p = (m1 (#) m2) | k9;
set q = (m1 | k9) (#) (m2 | k9);
assume A2: k9 <= len m1 ; ::_thesis: (m1 (#) m2) | k9 = (m1 | k9) (#) (m2 | k9)
then A3: len (m1 | k9) = k9 by FINSEQ_1:59;
reconsider k = k9 as Element of NAT by ORDINAL1:def_12;
A4: k9 <= len (m1 (#) m2) by A1, A2, Lm4;
then A5: len ((m1 (#) m2) | k9) = k9 by FINSEQ_1:59;
A6: len (m2 | k9) = k9 by A1, A2, FINSEQ_1:59;
then A7: len ((m1 | k9) (#) (m2 | k9)) = k9 by A3, Lm4;
now__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_((m1_(#)_m2)_|_k9)_holds_
((m1_(#)_m2)_|_k9)_._j_=_((m1_|_k9)_(#)_(m2_|_k9))_._j
A8: len (m1 (#) m2) = len m1 by A1, Lm4;
let j be Nat; ::_thesis: ( 1 <= j & j <= len ((m1 (#) m2) | k9) implies ((m1 (#) m2) | k9) . j = ((m1 | k9) (#) (m2 | k9)) . j )
assume that
A9: 1 <= j and
A10: j <= len ((m1 (#) m2) | k9) ; ::_thesis: ((m1 (#) m2) | k9) . j = ((m1 | k9) (#) (m2 | k9)) . j
A11: j in NAT by ORDINAL1:def_12;
then A12: j in Seg k by A5, A9, A10;
then A13: j in dom (m1 | k) by A3, FINSEQ_1:def_3;
A14: j in dom ((m1 | k9) (#) (m2 | k9)) by A7, A12, FINSEQ_1:def_3;
A15: j in dom (m2 | k) by A6, A12, FINSEQ_1:def_3;
j <= len m1 by A2, A5, A10, XXREAL_0:2;
then j in Seg (len (m1 (#) m2)) by A9, A11, A8;
then A16: j in dom (m1 (#) m2) by FINSEQ_1:def_3;
j in dom ((m1 (#) m2) | k9) by A9, A10, FINSEQ_3:25;
hence ((m1 (#) m2) | k9) . j = (m1 (#) m2) . j by FUNCT_1:47
.= (m1 . j) * (m2 . j) by A16, VALUED_1:def_4
.= ((m1 | k) . j) * (m2 . j) by A13, FUNCT_1:47
.= ((m1 | k) . j) * ((m2 | k) . j) by A15, FUNCT_1:47
.= ((m1 | k9) (#) (m2 | k9)) . j by A14, VALUED_1:def_4 ;
::_thesis: verum
end;
hence (m1 (#) m2) | k9 = (m1 | k9) (#) (m2 | k9) by A4, A7, FINSEQ_1:14, FINSEQ_1:59; ::_thesis: verum
end;
registration
let F be INT -valued FinSequence;
cluster Sum F -> integer ;
coherence
Sum F is integer
proof
set mc = addcomplex ;
consider f being FinSequence of COMPLEX such that
A1: f = F and
A2: Sum F = addcomplex $$ f by RVSUM_1:def_10;
set g = [#] (f,(the_unity_wrt addcomplex));
defpred S1[ Element of NAT ] means addcomplex $$ ((finSeg F),([#] (f,(the_unity_wrt addcomplex)))) is integer ;
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A4: ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is integer
proof
percases ( k + 1 in dom f or not k + 1 in dom f ) ;
suppose k + 1 in dom f ; ::_thesis: ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is integer
then ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) = f . (k + 1) by SETWOP_2:20;
hence ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is integer by A1; ::_thesis: verum
end;
suppose not k + 1 in dom f ; ::_thesis: ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is integer
hence ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is integer by BINOP_2:1, SETWOP_2:20; ::_thesis: verum
end;
end;
end;
assume S1[k] ; ::_thesis: S1[k + 1]
then reconsider a = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1), b = addcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt addcomplex)))) as integer number by A4;
not k + 1 in Seg k by FINSEQ_3:8;
then addcomplex $$ (((finSeg k) \/ {.(k + 1).}),([#] (f,(the_unity_wrt addcomplex)))) = addcomplex . ((addcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt addcomplex))))),(([#] (f,(the_unity_wrt addcomplex))) . (k + 1))) by SETWOP_2:2
.= b + a by BINOP_2:def_3 ;
hence S1[k + 1] by FINSEQ_1:9; ::_thesis: verum
end;
Seg 0 = {}. NAT ;
then A5: S1[ 0 ] by BINOP_2:1, SETWISEO:31;
A6: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A3);
consider n being Nat such that
A7: dom f = Seg n by FINSEQ_1:def_2;
A8: addcomplex $$ f = addcomplex $$ ((findom f),([#] (f,(the_unity_wrt addcomplex)))) by SETWOP_2:def_2;
n in NAT by ORDINAL1:def_12;
hence Sum F is integer by A2, A8, A7, A6; ::_thesis: verum
end;
cluster Product F -> integer ;
coherence
Product F is integer
proof
set mc = multcomplex ;
consider f being FinSequence of COMPLEX such that
A9: f = F and
A10: Product F = multcomplex $$ f by RVSUM_1:def_13;
set g = [#] (f,(the_unity_wrt multcomplex));
defpred S1[ Element of NAT ] means multcomplex $$ ((finSeg F),([#] (f,(the_unity_wrt multcomplex)))) is integer ;
A11: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A12: ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is integer
proof
percases ( k + 1 in dom f or not k + 1 in dom f ) ;
suppose k + 1 in dom f ; ::_thesis: ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is integer
then ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) = f . (k + 1) by SETWOP_2:20;
hence ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is integer by A9; ::_thesis: verum
end;
suppose not k + 1 in dom f ; ::_thesis: ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is integer
hence ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is integer by BINOP_2:6, SETWOP_2:20; ::_thesis: verum
end;
end;
end;
assume S1[k] ; ::_thesis: S1[k + 1]
then reconsider a = ([#] (f,(the_unity_wrt multcomplex))) . (k + 1), b = multcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt multcomplex)))) as integer number by A12;
not k + 1 in Seg k by FINSEQ_3:8;
then multcomplex $$ (((finSeg k) \/ {.(k + 1).}),([#] (f,(the_unity_wrt multcomplex)))) = multcomplex . ((multcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt multcomplex))))),(([#] (f,(the_unity_wrt multcomplex))) . (k + 1))) by SETWOP_2:2
.= b * a by BINOP_2:def_5 ;
hence S1[k + 1] by FINSEQ_1:9; ::_thesis: verum
end;
Seg 0 = {}. NAT ;
then A13: S1[ 0 ] by BINOP_2:6, SETWISEO:31;
A14: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A13, A11);
consider n being Nat such that
A15: dom f = Seg n by FINSEQ_1:def_2;
A16: multcomplex $$ f = multcomplex $$ ((findom f),([#] (f,(the_unity_wrt multcomplex)))) by SETWOP_2:def_2;
n in NAT by ORDINAL1:def_12;
hence Product F is integer by A10, A16, A15, A14; ::_thesis: verum
end;
end;
Lm5: for z being INT -valued FinSequence holds z is FinSequence of REAL
proof
let f be INT -valued FinSequence; ::_thesis: f is FinSequence of REAL
rng f c= REAL ;
hence f is FinSequence of REAL by FINSEQ_1:def_4; ::_thesis: verum
end;
theorem Th5: :: INT_6:5
for f being complex-valued FinSequence
for i being Nat st i + 1 <= len f holds
(f | i) ^ <*(f . (i + 1))*> = f | (i + 1)
proof
let f be complex-valued FinSequence; ::_thesis: for i being Nat st i + 1 <= len f holds
(f | i) ^ <*(f . (i + 1))*> = f | (i + 1)
let i be Nat; ::_thesis: ( i + 1 <= len f implies (f | i) ^ <*(f . (i + 1))*> = f | (i + 1) )
assume A1: i + 1 <= len f ; ::_thesis: (f | i) ^ <*(f . (i + 1))*> = f | (i + 1)
set f1 = (f | i) ^ <*(f . (i + 1))*>;
set f2 = f | (i + 1);
A2: i <= i + 1 by NAT_1:11;
reconsider f1 = (f | i) ^ <*(f . (i + 1))*> as complex-valued FinSequence ;
A3: len f1 = (len (f | i)) + (len <*(f . (i + 1))*>) by FINSEQ_1:22
.= (len (f | i)) + 1 by FINSEQ_1:39
.= i + 1 by A1, A2, FINSEQ_1:59, XXREAL_0:2
.= len (f | (i + 1)) by A1, FINSEQ_1:59 ;
then A4: dom f1 = Seg (len (f | (i + 1))) by FINSEQ_1:def_3
.= dom (f | (i + 1)) by FINSEQ_1:def_3 ;
A5: i <= len f by A1, A2, XXREAL_0:2;
now__::_thesis:_for_x9_being_set_st_x9_in_dom_f1_holds_
f1_._x9_=_(f_|_(i_+_1))_._x9
let x9 be set ; ::_thesis: ( x9 in dom f1 implies f1 . b1 = (f | (i + 1)) . b1 )
assume A6: x9 in dom f1 ; ::_thesis: f1 . b1 = (f | (i + 1)) . b1
then reconsider x = x9 as Element of NAT ;
A7: dom f1 = Seg (len f1) by FINSEQ_1:def_3;
then A8: 1 <= x by A6, FINSEQ_1:1;
x <= len f1 by A6, A7, FINSEQ_1:1;
then A9: x <= i + 1 by A1, A3, FINSEQ_1:59;
percases ( x = i + 1 or x < i + 1 ) by A9, XXREAL_0:1;
supposeA10: x = i + 1 ; ::_thesis: f1 . b1 = (f | (i + 1)) . b1
then x in Seg (i + 1) by A8;
then A11: x in dom (f | (i + 1)) by A1, FINSEQ_1:17;
dom <*(f . (i + 1))*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then A12: 1 in dom <*(f . (i + 1))*> by TARSKI:def_1;
len (f | i) = i by A1, A2, FINSEQ_1:59, XXREAL_0:2;
hence f1 . x9 = <*(f . (i + 1))*> . 1 by A10, A12, FINSEQ_1:def_7
.= f . (i + 1) by FINSEQ_1:40
.= (f | (i + 1)) . x9 by A10, A11, FUNCT_1:47 ;
::_thesis: verum
end;
suppose x < i + 1 ; ::_thesis: f1 . b1 = (f | (i + 1)) . b1
then A13: x <= i by NAT_1:13;
1 <= x by A6, A7, FINSEQ_1:1;
then x in Seg i by A13;
then A14: x in dom (f | i) by A5, FINSEQ_1:17;
hence f1 . x9 = (f | i) . x by FINSEQ_1:def_7
.= f . x by A14, FUNCT_1:47
.= (f | (i + 1)) . x9 by A4, A6, FUNCT_1:47 ;
::_thesis: verum
end;
end;
end;
hence (f | i) ^ <*(f . (i + 1))*> = f | (i + 1) by A4, FUNCT_1:2; ::_thesis: verum
end;
theorem Th6: :: INT_6:6
for f being complex-valued FinSequence st ex i being Nat st
( i in dom f & f . i = 0 ) holds
Product f = 0
proof
defpred S1[ Nat] means for f being complex-valued FinSequence st len f = $1 & ex i being Nat st
( i in dom f & f . i = 0 ) holds
Product f = 0 ;
let m be complex-valued FinSequence; ::_thesis: ( ex i being Nat st
( i in dom m & m . i = 0 ) implies Product m = 0 )
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_for_f_being_complex-valued_FinSequence_st_len_f_=_k_+_1_&_ex_i_being_Nat_st_
(_i_in_dom_f_&_f_._i_=_0_)_holds_
Product_f_=_0
let f be complex-valued FinSequence; ::_thesis: ( len f = k + 1 & ex i being Nat st
( i in dom f & f . i = 0 ) implies Product b1 = 0 )
set f1 = f | k;
assume A3: len f = k + 1 ; ::_thesis: ( ex i being Nat st
( i in dom f & f . i = 0 ) implies Product b1 = 0 )
then A4: len (f | k) = k by FINSEQ_1:59, NAT_1:11;
reconsider f1 = f | k as complex-valued FinSequence ;
f = f1 ^ <*(f . (k + 1))*> by A3, FINSEQ_3:55;
then A5: Product f = (Product f1) * (f . (k + 1)) by RVSUM_1:96;
assume A6: ex i being Nat st
( i in dom f & f . i = 0 ) ; ::_thesis: Product b1 = 0
percases ( f . (k + 1) = 0 or f . (k + 1) <> 0 ) ;
suppose f . (k + 1) = 0 ; ::_thesis: Product b1 = 0
hence Product f = 0 by A5; ::_thesis: verum
end;
supposeA7: f . (k + 1) <> 0 ; ::_thesis: Product b1 = 0
consider j being Nat such that
A8: j in dom f and
A9: f . j = 0 by A6;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A10: j in Seg (len f) by A8, FINSEQ_1:def_3;
then j <= k + 1 by A3, FINSEQ_1:1;
then j < k + 1 by A7, A9, XXREAL_0:1;
then A11: j <= k by NAT_1:13;
1 <= j by A10, FINSEQ_1:1;
then j in Seg k by A11;
then A12: j in dom f1 by A4, FINSEQ_1:def_3;
then f1 . j = f . j by FUNCT_1:47;
then Product f1 = 0 by A2, A4, A9, A12;
hence Product f = 0 by A5; ::_thesis: verum
end;
end;
end;
hence S1[k + 1] ; ::_thesis: verum
end;
A13: S1[ 0 ]
proof
let f be complex-valued FinSequence; ::_thesis: ( len f = 0 & ex i being Nat st
( i in dom f & f . i = 0 ) implies Product f = 0 )
assume len f = 0 ; ::_thesis: ( for i being Nat holds
( not i in dom f or not f . i = 0 ) or Product f = 0 )
then Seg (len f) = {} ;
hence ( for i being Nat holds
( not i in dom f or not f . i = 0 ) or Product f = 0 ) by FINSEQ_1:def_3; ::_thesis: verum
end;
A14: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A13, A1);
A15: ex j being Nat st len m = j ;
assume ex i being Nat st
( i in dom m & m . i = 0 ) ; ::_thesis: Product m = 0
hence Product m = 0 by A14, A15; ::_thesis: verum
end;
theorem Th7: :: INT_6:7
for n, a, b being Integer holds (a - b) mod n = ((a mod n) - (b mod n)) mod n
proof
let n, a, b be Integer; ::_thesis: (a - b) mod n = ((a mod n) - (b mod n)) mod n
percases ( n = 0 or n <> 0 ) ;
supposeA1: n = 0 ; ::_thesis: (a - b) mod n = ((a mod n) - (b mod n)) mod n
hence (a - b) mod n = 0 by INT_1:def_10
.= ((a mod n) - (b mod n)) mod n by A1, INT_1:def_10 ;
::_thesis: verum
end;
supposeA2: n <> 0 ; ::_thesis: (a - b) mod n = ((a mod n) - (b mod n)) mod n
then A3: (b mod n) + ((b div n) * n) = (b - ((b div n) * n)) + ((b div n) * n) by INT_1:def_10;
(a mod n) + ((a div n) * n) = (a - ((a div n) * n)) + ((a div n) * n) by A2, INT_1:def_10;
then (a - b) - ((a mod n) - (b mod n)) = ((a div n) - (b div n)) * n by A3;
then n divides (a - b) - ((a mod n) - (b mod n)) by INT_1:def_3;
then a - b,(a mod n) - (b mod n) are_congruent_mod n by INT_2:15;
hence (a - b) mod n = ((a mod n) - (b mod n)) mod n by NAT_D:64; ::_thesis: verum
end;
end;
end;
theorem Th8: :: INT_6:8
for i, j, k being Integer st i divides j holds
k * i divides k * j
proof
let i, j, k be Integer; ::_thesis: ( i divides j implies k * i divides k * j )
assume i divides j ; ::_thesis: k * i divides k * j
then consider z being Integer such that
A1: i * z = j by INT_1:def_3;
(i * k) * z = j * k by A1;
hence k * i divides k * j by INT_1:def_3; ::_thesis: verum
end;
theorem Th9: :: INT_6:9
for m being INT -valued FinSequence
for i being Nat st i in dom m & m . i <> 0 holds
(Product m) / (m . i) is Integer
proof
let m be INT -valued FinSequence; ::_thesis: for i being Nat st i in dom m & m . i <> 0 holds
(Product m) / (m . i) is Integer
let i9 be Nat; ::_thesis: ( i9 in dom m & m . i9 <> 0 implies (Product m) / (m . i9) is Integer )
reconsider i = i9 as Element of NAT by ORDINAL1:def_12;
reconsider m2 = m /^ i as FinSequence of INT by Lm1;
reconsider m1 = m | i as FinSequence of INT by Lm1;
reconsider m9 = m as FinSequence of INT by Lm1;
assume that
A1: i9 in dom m and
A2: m . i9 <> 0 ; ::_thesis: (Product m) / (m . i9) is Integer
A3: dom m = Seg (len m) by FINSEQ_1:def_3;
then 1 <= i by A1, FINSEQ_1:1;
then 1 - 1 <= i - 1 by XREAL_1:9;
then reconsider j = i - 1 as Element of NAT by INT_1:3;
set f = (m | j) ^ (m /^ i);
reconsider f = (m | j) ^ (m /^ i) as FinSequence of INT by Lm1;
A4: m9 = m1 ^ m2 by RFINSEQ:8;
j + 1 <= len m by A1, A3, FINSEQ_1:1;
then (m | j) ^ <*(m . i)*> = m | i by Th5;
then Product m = (Product ((m | j) ^ <*(m . i)*>)) * (Product (m /^ i)) by A4, RVSUM_1:97
.= ((Product (m | j)) * (Product <*(m . i)*>)) * (Product (m /^ i)) by RVSUM_1:97
.= ((Product (m | j)) * (Product (m /^ i))) * (Product <*(m . i)*>)
.= ((Product (m | j)) * (Product (m /^ i))) * (m . i) by RVSUM_1:95
.= (Product f) * (m . i) by RVSUM_1:97 ;
then m . i divides Product m by INT_1:def_3;
hence (Product m) / (m . i9) is Integer by A2, WSIERP_1:17; ::_thesis: verum
end;
theorem Th10: :: INT_6:10
for m being INT -valued FinSequence
for i being Nat st i in dom m holds
ex z being Integer st z * (m . i) = Product m
proof
let m be INT -valued FinSequence; ::_thesis: for i being Nat st i in dom m holds
ex z being Integer st z * (m . i) = Product m
let i be Nat; ::_thesis: ( i in dom m implies ex z being Integer st z * (m . i) = Product m )
assume A1: i in dom m ; ::_thesis: ex z being Integer st z * (m . i) = Product m
percases ( m . i <> 0 or m . i = 0 ) ;
supposeA2: m . i <> 0 ; ::_thesis: ex z being Integer st z * (m . i) = Product m
then reconsider z = (Product m) / (m . i) as Integer by A1, Th9;
take z ; ::_thesis: z * (m . i) = Product m
thus z * (m . i) = (Product m) * (((m . i) ") * (m . i))
.= (Product m) * 1 by A2, XCMPLX_0:def_7
.= Product m ; ::_thesis: verum
end;
supposeA3: m . i = 0 ; ::_thesis: ex z being Integer st z * (m . i) = Product m
take 1 ; ::_thesis: 1 * (m . i) = Product m
thus 1 * (m . i) = Product m by A1, A3, Th6; ::_thesis: verum
end;
end;
end;
Lm6: for m being INT -valued FinSequence
for i, j being Nat st i in dom m & j in dom m & j <> i & m . j <> 0 holds
ex z being Integer st z * (m . i) = (Product m) / (m . j)
proof
let m be INT -valued FinSequence; ::_thesis: for i, j being Nat st i in dom m & j in dom m & j <> i & m . j <> 0 holds
ex z being Integer st z * (m . i) = (Product m) / (m . j)
let i9, j9 be Nat; ::_thesis: ( i9 in dom m & j9 in dom m & j9 <> i9 & m . j9 <> 0 implies ex z being Integer st z * (m . i9) = (Product m) / (m . j9) )
reconsider m9 = m as FinSequence of INT by Lm1;
assume that
A1: i9 in dom m and
A2: j9 in dom m and
A3: j9 <> i9 and
A4: m . j9 <> 0 ; ::_thesis: ex z being Integer st z * (m . i9) = (Product m) / (m . j9)
reconsider i = i9, j = j9 as Element of NAT by ORDINAL1:def_12;
A5: dom m = Seg (len m) by FINSEQ_1:def_3;
then A6: j <= len m by A2, FINSEQ_1:1;
A7: 1 <= j by A2, A5, FINSEQ_1:1;
then 1 - 1 <= j - 1 by XREAL_1:9;
then reconsider kj = j - 1 as Element of NAT by INT_1:3;
set f = (m | kj) ^ (m /^ j);
reconsider f = (m | kj) ^ (m /^ j) as FinSequence of INT by Lm1;
kj + 1 = j ;
then kj <= j by NAT_1:11;
then A8: len (m | kj) = kj by A6, FINSEQ_1:59, XXREAL_0:2;
A9: dom m = Seg (len m) by FINSEQ_1:def_3;
then A10: 1 <= i by A1, FINSEQ_1:1;
then 1 - 1 <= i - 1 by XREAL_1:9;
then reconsider ki = i - 1 as Element of NAT by INT_1:3;
A11: i <= len m by A1, A9, FINSEQ_1:1;
ex l being Element of NAT st
( l in dom f & f . l = m . i )
proof
percases ( i < j or i > j ) by A3, XXREAL_0:1;
supposeA12: i < j ; ::_thesis: ex l being Element of NAT st
( l in dom f & f . l = m . i )
A13: dom (m | kj) c= dom f by FINSEQ_1:26;
i < kj + 1 by A12;
then i <= j - 1 by NAT_1:13;
then i in Seg kj by A10;
then A14: i in dom (m | kj) by A8, FINSEQ_1:def_3;
then (m | kj) . i = m . i by FUNCT_1:47;
then f . i = m . i by A14, FINSEQ_1:def_7;
hence ex l being Element of NAT st
( l in dom f & f . l = m . i ) by A14, A13; ::_thesis: verum
end;
supposeA15: i > j ; ::_thesis: ex l being Element of NAT st
( l in dom f & f . l = m . i )
then i - 1 > kj by XREAL_1:9;
then reconsider a = (i - 1) - kj as Element of NAT by INT_1:5;
i - kj > (kj + 1) - kj by A15, XREAL_1:9;
then (i - kj) - 1 > 1 - 1 by XREAL_1:9;
then ex g being Nat st a = g + 1 by NAT_1:6;
then A16: 1 <= (i - 1) - kj by NAT_1:11;
A17: len (m /^ j) = (len m) - j by A6, RFINSEQ:def_1;
then len f = kj + ((len m) - j) by A8, FINSEQ_1:22
.= (len m) - 1 ;
then A18: ki <= len f by A11, XREAL_1:9;
i - j <= (len m) - j by A11, XREAL_1:9;
then a in Seg (len (m /^ j)) by A17, A16;
then A19: (i - 1) - kj in dom (m9 /^ j) by FINSEQ_1:def_3;
ki + 1 > 1 by A7, A15, XXREAL_0:2;
then ki >= 1 by NAT_1:13;
then ki in Seg (len f) by A18;
then A20: ki in dom f by FINSEQ_1:def_3;
reconsider D = INT as set ;
reconsider ww = m9 as FinSequence of D ;
len (m | kj) < i - 1 by A8, A15, XREAL_1:9;
then f . ki = (m /^ j) . (ki - kj) by A8, A18, FINSEQ_1:24
.= (ww /^ j) /. (ki - kj) by A19, PARTFUN1:def_6
.= ww /. (j + a) by A19, FINSEQ_5:27
.= m . i by A1, PARTFUN1:def_6 ;
hence ex l being Element of NAT st
( l in dom f & f . l = m . i ) by A20; ::_thesis: verum
end;
end;
end;
then consider l being Element of NAT such that
A21: l in dom f and
A22: f . l = m . i ;
l in Seg (len f) by A21, FINSEQ_1:def_3;
then 1 <= l by FINSEQ_1:1;
then reconsider kl = l - 1 as Element of NAT by INT_1:5;
l in Seg (len f) by A21, FINSEQ_1:def_3;
then kl + 1 <= len f by FINSEQ_1:1;
then (f | kl) ^ <*(f . l)*> = f | l by Th5;
then f = ((f | kl) ^ <*(f . l)*>) ^ (f /^ l) by RFINSEQ:8;
then A23: Product f = (Product ((f | kl) ^ <*(f . l)*>)) * (Product (f /^ l)) by RVSUM_1:97
.= ((Product (f | kl)) * (Product <*(f . l)*>)) * (Product (f /^ l)) by RVSUM_1:97
.= ((Product (f | kl)) * (Product (f /^ l))) * (Product <*(m . i)*>) by A22
.= ((Product (f | kl)) * (Product (f /^ l))) * (m . i) by RVSUM_1:95
.= (Product ((f | kl) ^ (f /^ l))) * (m . i) by RVSUM_1:97 ;
kj + 1 <= len m by A2, A5, FINSEQ_1:1;
then A24: (m | kj) ^ <*(m . j)*> = m | j by Th5;
reconsider m2 = m /^ j as FinSequence of INT by Lm1;
reconsider m1 = m | j as FinSequence of INT by Lm1;
m9 = m1 ^ m2 by RFINSEQ:8;
then Product m = (Product ((m | kj) ^ <*(m . j)*>)) * (Product (m /^ j)) by A24, RVSUM_1:97
.= ((Product (m | kj)) * (Product <*(m . j)*>)) * (Product (m /^ j)) by RVSUM_1:97
.= ((Product (m | kj)) * (Product (m /^ j))) * (Product <*(m . j)*>)
.= ((Product (m | kj)) * (Product (m /^ j))) * (m . j) by RVSUM_1:95
.= (Product f) * (m . j) by RVSUM_1:97 ;
then (Product m) / (m . j) = (Product f) * ((m . j) * ((m . j) "))
.= (Product f) * 1 by A4, XCMPLX_0:def_7 ;
hence ex z being Integer st z * (m . i9) = (Product m) / (m . j9) by A23; ::_thesis: verum
end;
theorem :: INT_6:11
for m being INT -valued FinSequence
for i, j being Nat st i in dom m & j in dom m & j <> i & m . j <> 0 holds
(Product m) / ((m . i) * (m . j)) is Integer
proof
let m be INT -valued FinSequence; ::_thesis: for i, j being Nat st i in dom m & j in dom m & j <> i & m . j <> 0 holds
(Product m) / ((m . i) * (m . j)) is Integer
let i9, j9 be Nat; ::_thesis: ( i9 in dom m & j9 in dom m & j9 <> i9 & m . j9 <> 0 implies (Product m) / ((m . i9) * (m . j9)) is Integer )
assume that
A1: i9 in dom m and
A2: j9 in dom m and
A3: j9 <> i9 and
A4: m . j9 <> 0 ; ::_thesis: (Product m) / ((m . i9) * (m . j9)) is Integer
reconsider i = i9, j = j9 as Element of NAT by ORDINAL1:def_12;
A5: ex z being Integer st z * (m . i) = (Product m) / (m . j) by A1, A2, A3, A4, Lm6;
percases ( m . i = 0 or m . i <> 0 ) ;
suppose m . i = 0 ; ::_thesis: (Product m) / ((m . i9) * (m . j9)) is Integer
hence (Product m) / ((m . i9) * (m . j9)) is Integer ; ::_thesis: verum
end;
supposeA6: m . i <> 0 ; ::_thesis: (Product m) / ((m . i9) * (m . j9)) is Integer
reconsider u = (Product m) / (m . j) as Integer by A2, A4, Th9;
A7: u / (m . i) = (Product m) * (((m . j) ") * ((m . i) "))
.= (Product m) / ((m . i) * (m . j)) by XCMPLX_1:204 ;
m . i divides u by A5, INT_1:def_3;
hence (Product m) / ((m . i9) * (m . j9)) is Integer by A6, A7, WSIERP_1:17; ::_thesis: verum
end;
end;
end;
theorem :: INT_6:12
for m being INT -valued FinSequence
for i, j being Nat st i in dom m & j in dom m & j <> i & m . j <> 0 holds
ex z being Integer st z * (m . i) = (Product m) / (m . j) by Lm6;
begin
theorem Th13: :: INT_6:13
for i being Integer holds
( abs i divides i & i divides abs i )
proof
let i be Integer; ::_thesis: ( abs i divides i & i divides abs i )
percases ( abs i = i or abs i = - i ) by ABSVALUE:1;
suppose abs i = i ; ::_thesis: ( abs i divides i & i divides abs i )
hence ( abs i divides i & i divides abs i ) ; ::_thesis: verum
end;
supposeA1: abs i = - i ; ::_thesis: ( abs i divides i & i divides abs i )
then A2: i * (- 1) = abs i ;
(abs i) * (- 1) = i by A1;
hence ( abs i divides i & i divides abs i ) by A2, INT_1:def_3; ::_thesis: verum
end;
end;
end;
theorem Th14: :: INT_6:14
for i, j being Integer holds i gcd j = i gcd (abs j)
proof
let i, j be Integer; ::_thesis: i gcd j = i gcd (abs j)
set k = i gcd (abs j);
i gcd (abs j) divides abs j by INT_2:def_2;
then consider x being Integer such that
A1: (i gcd (abs j)) * x = abs j by INT_1:def_3;
abs j divides j by Th13;
then consider y being Integer such that
A2: (abs j) * y = j by INT_1:def_3;
A3: for m being Integer st m divides i & m divides j holds
m divides i gcd (abs j)
proof
j divides abs j by Th13;
then consider y being Integer such that
A4: j * y = abs j by INT_1:def_3;
let m be Integer; ::_thesis: ( m divides i & m divides j implies m divides i gcd (abs j) )
assume that
A5: m divides i and
A6: m divides j ; ::_thesis: m divides i gcd (abs j)
consider x being Integer such that
A7: m * x = j by A6, INT_1:def_3;
m * (x * y) = abs j by A7, A4;
then m divides abs j by INT_1:def_3;
hence m divides i gcd (abs j) by A5, INT_2:def_2; ::_thesis: verum
end;
(i gcd (abs j)) * (x * y) = j by A1, A2;
then A8: i gcd (abs j) divides j by INT_1:def_3;
i gcd (abs j) divides i by INT_2:def_2;
hence i gcd j = i gcd (abs j) by A8, A3, INT_2:def_2; ::_thesis: verum
end;
theorem Th15: :: INT_6:15
for i, j being Integer st i,j are_relative_prime holds
i lcm j = abs (i * j)
proof
let i, j be Integer; ::_thesis: ( i,j are_relative_prime implies i lcm j = abs (i * j) )
assume A1: i gcd j = 1 ; :: according to INT_2:def_3 ::_thesis: i lcm j = abs (i * j)
percases ( i = 0 or j = 0 or ( i <> 0 & j <> 0 ) ) ;
supposeA2: ( i = 0 or j = 0 ) ; ::_thesis: i lcm j = abs (i * j)
hence i lcm j = 0 by INT_2:4
.= abs (i * j) by A2, ABSVALUE:2 ;
::_thesis: verum
end;
supposeA3: ( i <> 0 & j <> 0 ) ; ::_thesis: i lcm j = abs (i * j)
A4: for m being Integer st i divides m & j divides m holds
abs (i * j) divides m
proof
j divides i lcm j by INT_2:def_1;
then consider kj being Integer such that
A5: j * kj = i lcm j by INT_1:def_3;
i divides i lcm j by INT_2:def_1;
then consider ki being Integer such that
A6: i * ki = i lcm j by INT_1:def_3;
A7: j divides i * j by INT_2:2;
i divides i * j by INT_2:2;
then i lcm j divides i * j by A7, INT_2:def_1;
then consider kij being Integer such that
A8: (i lcm j) * kij = i * j by INT_1:def_3;
i * j = j * (kj * kij) by A5, A8;
then i = kj * kij by A3, XCMPLX_1:5;
then A9: kij divides i by INT_1:def_3;
i * j = i * (ki * kij) by A6, A8;
then j = ki * kij by A3, XCMPLX_1:5;
then kij divides j by INT_1:def_3;
then A10: kij divides 1 by A1, A9, INT_2:def_2;
let m be Integer; ::_thesis: ( i divides m & j divides m implies abs (i * j) divides m )
assume that
A11: i divides m and
A12: j divides m ; ::_thesis: abs (i * j) divides m
A13: i lcm j divides m by A11, A12, INT_2:def_1;
percases ( kij = 1 or kij = - 1 ) by A10, INT_2:13;
suppose kij = 1 ; ::_thesis: abs (i * j) divides m
hence abs (i * j) divides m by A8, A13, ABSVALUE:def_1; ::_thesis: verum
end;
supposeA14: kij = - 1 ; ::_thesis: abs (i * j) divides m
- (i * j) <> 0 by A3, XCMPLX_1:6;
then - (- (i * j)) < 0 by A8, A14;
hence abs (i * j) divides m by A8, A13, A14, ABSVALUE:def_1; ::_thesis: verum
end;
end;
end;
j divides abs j by Th13;
then j divides (abs i) * (abs j) by INT_2:2;
then A15: j divides abs (i * j) by COMPLEX1:65;
i divides abs i by Th13;
then i divides (abs i) * (abs j) by INT_2:2;
then i divides abs (i * j) by COMPLEX1:65;
hence i lcm j = abs (i * j) by A15, A4, INT_2:def_1; ::_thesis: verum
end;
end;
end;
theorem Th16: :: INT_6:16
for i, j, k being Integer holds (i * j) gcd (i * k) = (abs i) * (j gcd k)
proof
let i, j, k be Integer; ::_thesis: (i * j) gcd (i * k) = (abs i) * (j gcd k)
percases ( i = 0 or i <> 0 ) ;
supposeA1: i = 0 ; ::_thesis: (i * j) gcd (i * k) = (abs i) * (j gcd k)
hence (i * j) gcd (i * k) = 0 * (j gcd k) by INT_2:5
.= (abs i) * (j gcd k) by A1, ABSVALUE:def_1 ;
::_thesis: verum
end;
supposeA2: i <> 0 ; ::_thesis: (i * j) gcd (i * k) = (abs i) * (j gcd k)
set d = j gcd k;
set e = (i * j) gcd (i * k);
percases ( j gcd k = 0 or j gcd k <> 0 ) ;
supposeA3: j gcd k = 0 ; ::_thesis: (i * j) gcd (i * k) = (abs i) * (j gcd k)
then A4: k = 0 by INT_2:5;
j = 0 by A3, INT_2:5;
hence (i * j) gcd (i * k) = (abs i) * (j gcd k) by A3, A4; ::_thesis: verum
end;
supposeA5: j gcd k <> 0 ; ::_thesis: (i * j) gcd (i * k) = (abs i) * (j gcd k)
A6: (i * j) gcd (i * k) divides i * k by INT_2:21;
A7: i * (j gcd k) divides i * k by Th8, INT_2:21;
i * (j gcd k) divides i * j by Th8, INT_2:21;
then i * (j gcd k) divides (i * j) gcd (i * k) by A7, INT_2:22;
then consider g being Integer such that
A8: (i * j) gcd (i * k) = (i * (j gcd k)) * g by INT_1:def_3;
A9: (i * j) gcd (i * k) divides i * j by INT_2:21;
( (j gcd k) * g divides j & (j gcd k) * g divides k )
proof
consider h1 being Integer such that
A10: ((i * (j gcd k)) * g) * h1 = i * j by A8, A9, INT_1:def_3;
i * (((j gcd k) * g) * h1) = i * j by A10;
then ((j gcd k) * g) * h1 = j by A2, XCMPLX_1:5;
hence (j gcd k) * g divides j by INT_1:def_3; ::_thesis: (j gcd k) * g divides k
consider h2 being Integer such that
A11: ((i * (j gcd k)) * g) * h2 = i * k by A8, A6, INT_1:def_3;
i * (((j gcd k) * g) * h2) = i * k by A11;
then ((j gcd k) * g) * h2 = k by A2, XCMPLX_1:5;
hence (j gcd k) * g divides k by INT_1:def_3; ::_thesis: verum
end;
then (j gcd k) * g divides j gcd k by INT_2:22;
then consider h3 being Integer such that
A12: ((j gcd k) * g) * h3 = j gcd k by INT_1:def_3;
(j gcd k) * (g * h3) = (j gcd k) * 1 by A12;
then g * h3 = 1 by A5, XCMPLX_1:5;
then A13: g divides 1 by INT_1:def_3;
percases ( g = 1 or g = - 1 ) by A13, INT_2:13;
supposeA14: g = 1 ; ::_thesis: (i * j) gcd (i * k) = (abs i) * (j gcd k)
( i < 0 implies (j gcd k) * i < 0 * i ) by A5, XREAL_1:69;
hence (i * j) gcd (i * k) = (abs i) * (j gcd k) by A8, A14, ABSVALUE:def_1; ::_thesis: verum
end;
supposeA15: g = - 1 ; ::_thesis: (i * j) gcd (i * k) = (abs i) * (j gcd k)
A16: now__::_thesis:_(_i_>_0_implies_(j_gcd_k)_*_(-_i)_<_0_*_(-_i)_)
assume i > 0 ; ::_thesis: (j gcd k) * (- i) < 0 * (- i)
then - (- i) > 0 ;
then - i < 0 ;
hence (j gcd k) * (- i) < 0 * (- i) by A5, XREAL_1:69; ::_thesis: verum
end;
(i * j) gcd (i * k) = (- i) * (j gcd k) by A8, A15;
hence (i * j) gcd (i * k) = (abs i) * (j gcd k) by A2, A16, ABSVALUE:def_1; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
theorem Th17: :: INT_6:17
for i, j being Integer holds (i * j) gcd i = abs i
proof
let i, j be Integer; ::_thesis: (i * j) gcd i = abs i
A1: for m being Integer st m divides i * j & m divides i holds
m divides abs i
proof
let m be Integer; ::_thesis: ( m divides i * j & m divides i implies m divides abs i )
assume that
m divides i * j and
A2: m divides i ; ::_thesis: m divides abs i
consider k being Integer such that
A3: m * k = i by A2, INT_1:def_3;
i divides abs i by Th13;
then consider l being Integer such that
A4: i * l = abs i by INT_1:def_3;
m * (k * l) = abs i by A3, A4;
hence m divides abs i by INT_1:def_3; ::_thesis: verum
end;
A5: abs i divides i by Th13;
then abs i divides i * j by INT_2:2;
hence (i * j) gcd i = abs i by A5, A1, INT_2:def_2; ::_thesis: verum
end;
theorem Th18: :: INT_6:18
for i, j, k being Integer holds i gcd (j gcd k) = (i gcd j) gcd k
proof
let i, j, k be Integer; ::_thesis: i gcd (j gcd k) = (i gcd j) gcd k
percases ( ( i = 0 & j = 0 & k = 0 ) or i <> 0 or j <> 0 or k <> 0 ) ;
suppose ( i = 0 & j = 0 & k = 0 ) ; ::_thesis: i gcd (j gcd k) = (i gcd j) gcd k
hence i gcd (j gcd k) = (i gcd j) gcd k ; ::_thesis: verum
end;
supposeA1: ( i <> 0 or j <> 0 or k <> 0 ) ; ::_thesis: i gcd (j gcd k) = (i gcd j) gcd k
A2: now__::_thesis:_not_i_gcd_(j_gcd_k)_=_-_((i_gcd_j)_gcd_k)
assume i gcd (j gcd k) = - ((i gcd j) gcd k) ; ::_thesis: contradiction
then (- ((i gcd j) gcd k)) * (- 1) <= 0 * (- 1) ;
then A3: (i gcd j) gcd k = 0 ;
then i gcd j = 0 by INT_2:5;
hence contradiction by A1, A3, INT_2:5; ::_thesis: verum
end;
A4: i gcd (j gcd k) divides i by INT_2:21;
A5: (i gcd j) gcd k divides k by INT_2:21;
A6: (i gcd j) gcd k divides i gcd j by INT_2:21;
i gcd j divides j by INT_2:21;
then (i gcd j) gcd k divides j by A6, INT_2:9;
then A7: (i gcd j) gcd k divides j gcd k by A5, INT_2:22;
i gcd j divides i by INT_2:21;
then (i gcd j) gcd k divides i by A6, INT_2:9;
then A8: (i gcd j) gcd k divides i gcd (j gcd k) by A7, INT_2:22;
A9: i gcd (j gcd k) divides j gcd k by INT_2:21;
j gcd k divides j by INT_2:21;
then i gcd (j gcd k) divides j by A9, INT_2:9;
then A10: i gcd (j gcd k) divides i gcd j by A4, INT_2:22;
j gcd k divides k by INT_2:21;
then i gcd (j gcd k) divides k by A9, INT_2:9;
then i gcd (j gcd k) divides (i gcd j) gcd k by A10, INT_2:22;
hence i gcd (j gcd k) = (i gcd j) gcd k by A8, A2, INT_2:11; ::_thesis: verum
end;
end;
end;
theorem Th19: :: INT_6:19
for i, j, k being Integer st i,j are_relative_prime holds
i gcd (j * k) = i gcd k
proof
let i, j, k be Integer; ::_thesis: ( i,j are_relative_prime implies i gcd (j * k) = i gcd k )
assume A1: i gcd j = 1 ; :: according to INT_2:def_3 ::_thesis: i gcd (j * k) = i gcd k
(i * k) gcd (j * k) = (abs k) * (i gcd j) by Th16;
then i gcd (abs k) = (i gcd (i * k)) gcd (j * k) by A1, Th18
.= (abs i) gcd (j * k) by Th17
.= (j * k) gcd i by Th14 ;
hence i gcd (j * k) = i gcd k by Th14; ::_thesis: verum
end;
theorem Th20: :: INT_6:20
for i, j being Integer st i,j are_relative_prime holds
i * j divides i lcm j
proof
let i, j be Integer; ::_thesis: ( i,j are_relative_prime implies i * j divides i lcm j )
assume i,j are_relative_prime ; ::_thesis: i * j divides i lcm j
then abs (i * j) divides i lcm j by Th15;
then consider z being Integer such that
A1: (abs (i * j)) * z = i lcm j by INT_1:def_3;
percases ( 0 <= i * j or 0 > i * j ) ;
suppose 0 <= i * j ; ::_thesis: i * j divides i lcm j
then z * (i * j) = i lcm j by A1, ABSVALUE:def_1;
hence i * j divides i lcm j by INT_1:def_3; ::_thesis: verum
end;
supposeA2: 0 > i * j ; ::_thesis: i * j divides i lcm j
(- z) * (i * j) = z * (- (i * j))
.= i lcm j by A1, A2, ABSVALUE:def_1 ;
hence i * j divides i lcm j by INT_1:def_3; ::_thesis: verum
end;
end;
end;
theorem Th21: :: INT_6:21
for x, y, i, j being Integer st i,j are_relative_prime & x,y are_congruent_mod i & x,y are_congruent_mod j holds
x,y are_congruent_mod i * j
proof
let x, y, i, j be Integer; ::_thesis: ( i,j are_relative_prime & x,y are_congruent_mod i & x,y are_congruent_mod j implies x,y are_congruent_mod i * j )
assume i,j are_relative_prime ; ::_thesis: ( not x,y are_congruent_mod i or not x,y are_congruent_mod j or x,y are_congruent_mod i * j )
then A1: i * j divides i lcm j by Th20;
assume that
A2: x,y are_congruent_mod i and
A3: x,y are_congruent_mod j ; ::_thesis: x,y are_congruent_mod i * j
A4: j divides x - y by A3, INT_2:15;
i divides x - y by A2, INT_2:15;
then i lcm j divides x - y by A4, INT_2:19;
then i * j divides x - y by A1, INT_2:9;
hence x,y are_congruent_mod i * j by INT_2:15; ::_thesis: verum
end;
theorem Th22: :: INT_6:22
for i, j being Integer st i,j are_relative_prime holds
ex s being Integer st s * i,1 are_congruent_mod j
proof
let i, j be Integer; ::_thesis: ( i,j are_relative_prime implies ex s being Integer st s * i,1 are_congruent_mod j )
assume i gcd j = 1 ; :: according to INT_2:def_3 ::_thesis: ex s being Integer st s * i,1 are_congruent_mod j
then consider s, t being Integer such that
A1: 1 = (s * i) + (t * j) by NAT_D:68;
take s ; ::_thesis: s * i,1 are_congruent_mod j
(s * i) - 1 = (- t) * j by A1;
then j divides (s * i) - 1 by INT_1:def_3;
hence s * i,1 are_congruent_mod j by INT_2:15; ::_thesis: verum
end;
begin
notation
let f be INT -valued FinSequence;
antonym multiplicative-trivial f for non-empty ;
end;
definition
let f be INT -valued FinSequence;
redefine attr f is non-empty means :Def1: :: INT_6:def 1
for i being Nat holds
( not i in dom f or not f . i = 0 );
compatibility
( not f is multiplicative-trivial iff for i being Nat holds
( not i in dom f or not f . i = 0 ) )
proof
thus ( f is non-empty implies for i being Nat holds
( not i in dom f or not f . i = 0 ) ) by FUNCT_1:def_9; ::_thesis: ( ( for i being Nat holds
( not i in dom f or not f . i = 0 ) ) implies not f is multiplicative-trivial )
assume A1: for i being Nat holds
( not i in dom f or not f . i = 0 ) ; ::_thesis: not f is multiplicative-trivial
let n be set ; :: according to FUNCT_1:def_9 ::_thesis: ( not n in dom f or not f . n is empty )
assume n in dom f ; ::_thesis: not f . n is empty
hence not f . n is empty by A1; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines multiplicative-trivial INT_6:def_1_:_
for f being INT -valued FinSequence holds
( not f is multiplicative-trivial iff for i being Nat holds
( not i in dom f or not f . i = 0 ) );
registration
cluster Relation-like multiplicative-trivial NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued for set ;
existence
ex b1 being INT -valued FinSequence st b1 is multiplicative-trivial
proof
set p = <*0*>;
now__::_thesis:_for_u_being_set_st_u_in_{0}_holds_
u_in_INT
let u be set ; ::_thesis: ( u in {0} implies u in INT )
assume u in {0} ; ::_thesis: u in INT
then reconsider u9 = u as Element of NAT by TARSKI:def_1;
u9 is integer number ;
hence u in INT by INT_1:def_1; ::_thesis: verum
end;
then {0} c= INT by TARSKI:def_3;
then rng <*0*> c= INT by FINSEQ_1:39;
then reconsider f = <*0*> as FinSequence of INT by FINSEQ_1:def_4;
take f ; ::_thesis: f is multiplicative-trivial
take 1 ; :: according to INT_6:def_1 ::_thesis: ( 1 in dom f & f . 1 = 0 )
len f = 1 by FINSEQ_1:40;
then dom f = Seg 1 by FINSEQ_1:def_3;
hence 1 in dom f ; ::_thesis: f . 1 = 0
thus f . 1 = 0 by FINSEQ_1:40; ::_thesis: verum
end;
cluster Relation-like non multiplicative-trivial NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued for set ;
existence
not for b1 being INT -valued FinSequence holds b1 is multiplicative-trivial by Def1;
cluster Relation-like NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding for set ;
existence
ex b1 being INT -valued FinSequence st
( not b1 is empty & b1 is positive-yielding )
proof
set p = <*1*>;
now__::_thesis:_for_u_being_set_st_u_in_{1}_holds_
u_in_INT
let u be set ; ::_thesis: ( u in {1} implies u in INT )
assume u in {1} ; ::_thesis: u in INT
then reconsider u9 = u as Element of NAT by TARSKI:def_1;
u9 is integer number ;
hence u in INT by INT_1:def_1; ::_thesis: verum
end;
then {1} c= INT by TARSKI:def_3;
then rng <*1*> c= INT by FINSEQ_1:39;
then reconsider f = <*1*> as FinSequence of INT by FINSEQ_1:def_4;
take f ; ::_thesis: ( not f is empty & f is positive-yielding )
now__::_thesis:_for_r_being_real_number_st_r_in_rng_f_holds_
0_<_r
let r be real number ; ::_thesis: ( r in rng f implies 0 < r )
assume r in rng f ; ::_thesis: 0 < r
then r in {1} by FINSEQ_1:39;
hence 0 < r by TARSKI:def_1; ::_thesis: verum
end;
hence ( not f is empty & f is positive-yielding ) by PARTFUN3:def_1; ::_thesis: verum
end;
end;
theorem :: INT_6:23
for m being multiplicative-trivial INT -valued FinSequence holds Product m = 0
proof
let m be multiplicative-trivial INT -valued FinSequence; ::_thesis: Product m = 0
ex i being Nat st
( i in dom m & m . i = 0 ) by Def1;
hence Product m = 0 by Th6; ::_thesis: verum
end;
definition
let f be INT -valued FinSequence;
attrf is Chinese_Remainder means :Def2: :: INT_6:def 2
for i, j being Nat st i in dom f & j in dom f & i <> j holds
f . i,f . j are_relative_prime ;
end;
:: deftheorem Def2 defines Chinese_Remainder INT_6:def_2_:_
for f being INT -valued FinSequence holds
( f is Chinese_Remainder iff for i, j being Nat st i in dom f & j in dom f & i <> j holds
f . i,f . j are_relative_prime );
registration
cluster Relation-like NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding Chinese_Remainder for set ;
existence
ex b1 being INT -valued FinSequence st
( not b1 is empty & b1 is positive-yielding & b1 is Chinese_Remainder )
proof
set p = <*1*>;
now__::_thesis:_for_u_being_set_st_u_in_{1}_holds_
u_in_INT
let u be set ; ::_thesis: ( u in {1} implies u in INT )
assume u in {1} ; ::_thesis: u in INT
then reconsider u9 = u as Element of NAT by TARSKI:def_1;
u9 is integer number ;
hence u in INT by INT_1:def_1; ::_thesis: verum
end;
then {1} c= INT by TARSKI:def_3;
then rng <*1*> c= INT by FINSEQ_1:39;
then reconsider f = <*1*> as FinSequence of INT by FINSEQ_1:def_4;
take f ; ::_thesis: ( not f is empty & f is positive-yielding & f is Chinese_Remainder )
A1: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_f_holds_
i_=_1
let i be Element of NAT ; ::_thesis: ( i in dom f implies i = 1 )
assume i in dom f ; ::_thesis: i = 1
then i in Seg 1 by FINSEQ_1:38;
hence i = 1 by FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum
end;
A2: now__::_thesis:_for_i9,_j9_being_Nat_st_i9_in_dom_f_&_j9_in_dom_f_&_i9_<>_j9_holds_
f_._i9,f_._j9_are_relative_prime
let i9, j9 be Nat; ::_thesis: ( i9 in dom f & j9 in dom f & i9 <> j9 implies f . i9,f . j9 are_relative_prime )
assume that
A3: i9 in dom f and
A4: j9 in dom f and
A5: i9 <> j9 ; ::_thesis: f . i9,f . j9 are_relative_prime
reconsider i = i9, j = j9 as Element of NAT by ORDINAL1:def_12;
i = 1 by A1, A3
.= j by A1, A4 ;
hence f . i9,f . j9 are_relative_prime by A5; ::_thesis: verum
end;
now__::_thesis:_for_r_being_real_number_st_r_in_rng_f_holds_
0_<_r
let r be real number ; ::_thesis: ( r in rng f implies 0 < r )
assume r in rng f ; ::_thesis: 0 < r
then r in {1} by FINSEQ_1:39;
hence 0 < r by TARSKI:def_1; ::_thesis: verum
end;
hence ( not f is empty & f is positive-yielding & f is Chinese_Remainder ) by A2, Def2, PARTFUN3:def_1; ::_thesis: verum
end;
end;
definition
mode CR_Sequence is INT -valued non empty positive-yielding Chinese_Remainder FinSequence;
end;
registration
cluster Relation-like INT -valued Function-like non empty FinSequence-like positive-yielding Chinese_Remainder -> non multiplicative-trivial for set ;
coherence
for b1 being CR_Sequence holds not b1 is multiplicative-trivial
proof
let f be CR_Sequence; ::_thesis: not f is multiplicative-trivial
now__::_thesis:_for_i_being_Nat_st_i_in_dom_f_holds_
f_._i_<>_0
let i be Nat; ::_thesis: ( i in dom f implies f . i <> 0 )
assume i in dom f ; ::_thesis: f . i <> 0
then f . i in rng f by FUNCT_1:3;
hence f . i <> 0 by PARTFUN3:def_1; ::_thesis: verum
end;
hence not f is multiplicative-trivial by Def1; ::_thesis: verum
end;
end;
registration
cluster Relation-like multiplicative-trivial INT -valued Function-like FinSequence-like -> INT -valued non empty for set ;
coherence
for b1 being INT -valued FinSequence st b1 is multiplicative-trivial holds
not b1 is empty ;
end;
theorem Th24: :: INT_6:24
for f being CR_Sequence
for m being Nat st 0 < m & m <= len f holds
f | m is CR_Sequence
proof
let f be CR_Sequence; ::_thesis: for m being Nat st 0 < m & m <= len f holds
f | m is CR_Sequence
let m be Nat; ::_thesis: ( 0 < m & m <= len f implies f | m is CR_Sequence )
reconsider fm = f | m as FinSequence of INT by Lm1;
assume that
A1: m > 0 and
A2: m <= len f ; ::_thesis: f | m is CR_Sequence
A3: len fm = m by A2, FINSEQ_1:59;
A4: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_fm_holds_
i_in_dom_f
let i be Element of NAT ; ::_thesis: ( i in dom fm implies i in dom f )
assume i in dom fm ; ::_thesis: i in dom f
then A5: i in Seg m by A3, FINSEQ_1:def_3;
then i <= m by FINSEQ_1:1;
then A6: i <= len f by A2, XXREAL_0:2;
1 <= i by A5, FINSEQ_1:1;
then i in Seg (len f) by A6;
hence i in dom f by FINSEQ_1:def_3; ::_thesis: verum
end;
A7: now__::_thesis:_for_i9,_j9_being_Nat_st_i9_in_dom_fm_&_j9_in_dom_fm_&_i9_<>_j9_holds_
fm_._i9,fm_._j9_are_relative_prime
let i9, j9 be Nat; ::_thesis: ( i9 in dom fm & j9 in dom fm & i9 <> j9 implies fm . i9,fm . j9 are_relative_prime )
assume that
A8: i9 in dom fm and
A9: j9 in dom fm and
A10: i9 <> j9 ; ::_thesis: fm . i9,fm . j9 are_relative_prime
reconsider i = i9, j = j9 as Element of NAT by ORDINAL1:def_12;
A11: f . i = fm . i by A8, FUNCT_1:47;
A12: f . j = fm . j by A9, FUNCT_1:47;
A13: j in dom f by A4, A9;
i in dom f by A4, A8;
hence fm . i9,fm . j9 are_relative_prime by A10, A13, A11, A12, Def2; ::_thesis: verum
end;
now__::_thesis:_for_r_being_real_number_st_r_in_rng_fm_holds_
r_>_0
let r be real number ; ::_thesis: ( r in rng fm implies r > 0 )
assume r in rng fm ; ::_thesis: r > 0
then consider i being set such that
A14: i in dom fm and
A15: fm . i = r by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A14;
f . i in rng f by A4, A14, FUNCT_1:3;
then f . i > 0 by PARTFUN3:def_1;
hence r > 0 by A14, A15, FUNCT_1:47; ::_thesis: verum
end;
hence f | m is CR_Sequence by A1, A3, A7, Def2, PARTFUN3:def_1; ::_thesis: verum
end;
Lm7: for m being CR_Sequence holds Product m > 0
proof
defpred S1[ Nat] means for f being CR_Sequence st len f = $1 holds
Product f > 0 ;
let m be CR_Sequence; ::_thesis: Product m > 0
A1: ex j being Nat st len m = j ;
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_for_f_being_CR_Sequence_st_len_f_=_k_+_1_holds_
Product_f_>_0
let f be CR_Sequence; ::_thesis: ( len f = k + 1 implies Product b1 > 0 )
assume A4: len f = k + 1 ; ::_thesis: Product b1 > 0
set f1 = f | k;
percases ( k > 0 or k = 0 ) ;
suppose k > 0 ; ::_thesis: Product b1 > 0
then reconsider f1 = f | k as CR_Sequence by A4, Th24, NAT_1:11;
A5: f = f1 ^ <*(f . (k + 1))*> by A4, FINSEQ_3:55;
1 <= k + 1 by NAT_1:11;
then k + 1 in Seg (k + 1) ;
then k + 1 in dom f by A4, FINSEQ_1:def_3;
then f . (k + 1) in rng f by FUNCT_1:3;
then A6: f . (k + 1) > 0 by PARTFUN3:def_1;
len f1 = k by A4, FINSEQ_1:59, NAT_1:11;
then Product f1 > 0 by A3;
then 0 * (f . (k + 1)) < (Product f1) * (f . (k + 1)) by A6, XREAL_1:68;
hence Product f > 0 by A5, RVSUM_1:96; ::_thesis: verum
end;
suppose k = 0 ; ::_thesis: Product b1 > 0
then A7: f = <*(f . 1)*> by A4, FINSEQ_1:40;
then dom f = Seg 1 by FINSEQ_1:38;
then 1 in dom f ;
then f . 1 in rng f by FUNCT_1:3;
then f . 1 > 0 by PARTFUN3:def_1;
hence Product f > 0 by A7, RVSUM_1:95; ::_thesis: verum
end;
end;
end;
hence S1[k + 1] ; ::_thesis: verum
end;
A8: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A8, A2);
hence Product m > 0 by A1; ::_thesis: verum
end;
registration
let m be CR_Sequence;
cluster Product m -> natural positive ;
coherence
( Product m is positive & Product m is natural )
proof
Product m > 0 by Lm7;
then Product m is Element of NAT by INT_1:3;
hence ( Product m is positive & Product m is natural ) by Lm7; ::_thesis: verum
end;
end;
theorem Th25: :: INT_6:25
for m being CR_Sequence
for i being Nat st i in dom m holds
for mm being Integer st mm = (Product m) / (m . i) holds
mm,m . i are_relative_prime
proof
defpred S1[ Nat] means for m being CR_Sequence st len m = $1 holds
for i being Nat st i in dom m holds
for mm being Integer st mm = (Product m) / (m . i) holds
mm,m . i are_relative_prime ;
let m be CR_Sequence; ::_thesis: for i being Nat st i in dom m holds
for mm being Integer st mm = (Product m) / (m . i) holds
mm,m . i are_relative_prime
let i be Nat; ::_thesis: ( i in dom m implies for mm being Integer st mm = (Product m) / (m . i) holds
mm,m . i are_relative_prime )
assume A1: i in dom m ; ::_thesis: for mm being Integer st mm = (Product m) / (m . i) holds
mm,m . i are_relative_prime
let mm be Integer; ::_thesis: ( mm = (Product m) / (m . i) implies mm,m . i are_relative_prime )
A2: ex l being Element of NAT st len m = l ;
A3: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_for_m_being_CR_Sequence_st_len_m_=_k_+_1_holds_
for_i9_being_Nat_st_i9_in_dom_m_holds_
for_mm_being_Integer_st_mm_=_(Product_m)_/_(m_._i9)_holds_
mm,m_._i9_are_relative_prime
let m be CR_Sequence; ::_thesis: ( len m = k + 1 implies for i9 being Nat st i9 in dom m holds
for mm being Integer st mm = (Product m) / (m . i9) holds
b5,b3 . b4 are_relative_prime )
set m1 = m | k;
assume A5: len m = k + 1 ; ::_thesis: for i9 being Nat st i9 in dom m holds
for mm being Integer st mm = (Product m) / (m . i9) holds
b5,b3 . b4 are_relative_prime
then A6: (m | k) ^ <*(m . (k + 1))*> = m | (k + 1) by Th5
.= m by A5, FINSEQ_1:58 ;
A7: len (m | k) = k by A5, FINSEQ_1:59, NAT_1:11;
1 <= k + 1 by NAT_1:11;
then k + 1 in Seg (k + 1) ;
then A8: k + 1 in dom m by A5, FINSEQ_1:def_3;
let i9 be Nat; ::_thesis: ( i9 in dom m implies for mm being Integer st mm = (Product m) / (m . i9) holds
b4,b2 . b3 are_relative_prime )
reconsider i = i9 as Element of NAT by ORDINAL1:def_12;
assume A9: i9 in dom m ; ::_thesis: for mm being Integer st mm = (Product m) / (m . i9) holds
b4,b2 . b3 are_relative_prime
then A10: i in Seg (k + 1) by A5, FINSEQ_1:def_3;
then A11: i <= k + 1 by FINSEQ_1:1;
let mm be Integer; ::_thesis: ( mm = (Product m) / (m . i9) implies b3,b1 . b2 are_relative_prime )
assume A12: mm = (Product m) / (m . i9) ; ::_thesis: b3,b1 . b2 are_relative_prime
percases ( k > 0 or k = 0 ) ;
suppose k > 0 ; ::_thesis: b3,b1 . b2 are_relative_prime
then reconsider m1 = m | k as CR_Sequence by A5, Th24, NAT_1:11;
percases ( i in dom m1 or not i in dom m1 ) ;
supposeA13: i in dom m1 ; ::_thesis: b3,b1 . b2 are_relative_prime
then i in Seg k by A7, FINSEQ_1:def_3;
then i <= k by FINSEQ_1:1;
then i <> k + 1 by NAT_1:13;
then A14: m . i,m . (k + 1) are_relative_prime by A9, A8, Def2;
reconsider mm1 = (Product m1) / (m1 . i) as Integer by A13, Th9;
A15: m1 . i = m . i by A13, FUNCT_1:47;
then mm1,m . i are_relative_prime by A4, A7, A13;
then A16: (m . i) gcd (mm1 * (m . (k + 1))) = (m . i) gcd (m . (k + 1)) by Th19
.= 1 by A14, INT_2:def_3 ;
mm1 * (m . (k + 1)) = ((Product m1) * (m . (k + 1))) * ((m . i) ") by A15
.= mm by A12, A6, RVSUM_1:96 ;
hence mm,m . i9 are_relative_prime by A16, INT_2:def_3; ::_thesis: verum
end;
supposeA17: not i in dom m1 ; ::_thesis: b3,b1 . b2 are_relative_prime
m . (k + 1) in rng m by A8, FUNCT_1:3;
then A18: m . (k + 1) > 0 by PARTFUN3:def_1;
defpred S2[ Nat] means ( $1 <= len m1 implies for s being Element of NAT st s = $1 holds
Product (m1 | s),m . (k + 1) are_relative_prime );
A19: m1 | (len m1) = m1 by FINSEQ_1:58;
A20: now__::_thesis:_for_j_being_Element_of_NAT_st_0_<=_j_&_j_<_len_m1_&_S2[j]_holds_
S2[j_+_1]
let j be Element of NAT ; ::_thesis: ( 0 <= j & j < len m1 & S2[j] implies S2[j + 1] )
assume that
0 <= j and
A21: j < len m1 ; ::_thesis: ( S2[j] implies S2[j + 1] )
assume A22: S2[j] ; ::_thesis: S2[j + 1]
now__::_thesis:_(_j_+_1_<=_len_m1_implies_S2[j_+_1]_)
assume A23: j + 1 <= len m1 ; ::_thesis: S2[j + 1]
A24: 0 + 1 <= j + 1 by XREAL_1:6;
then j + 1 in Seg (len m1) by A23;
then A25: j + 1 in dom m1 by FINSEQ_1:def_3;
j + 1 <= len m by A5, A7, A21, XREAL_1:8;
then j + 1 in Seg (len m) by A24;
then A26: j + 1 in dom m by FINSEQ_1:def_3;
j + 1 <= k by A5, A23, FINSEQ_1:59, NAT_1:11;
then A27: j + 1 <> k + 1 by NAT_1:13;
now__::_thesis:_for_s_being_Element_of_NAT_st_s_=_j_+_1_holds_
Product_(m1_|_s),m_._(k_+_1)_are_relative_prime
reconsider s9 = j as Element of NAT ;
let s be Element of NAT ; ::_thesis: ( s = j + 1 implies Product (m1 | s),m . (k + 1) are_relative_prime )
A28: m1 . (j + 1) = m . (j + 1) by A25, FUNCT_1:47;
A29: m . (j + 1),m . (k + 1) are_relative_prime by A8, A27, A26, Def2;
j <= j + 1 by NAT_1:11;
then Product (m1 | s9),m . (k + 1) are_relative_prime by A22, A23, XXREAL_0:2;
then A30: ((Product (m1 | s9)) * (m . (j + 1))) gcd (m . (k + 1)) = (m . (j + 1)) gcd (m . (k + 1)) by Th19
.= 1 by A29, INT_2:def_3 ;
assume A31: s = j + 1 ; ::_thesis: Product (m1 | s),m . (k + 1) are_relative_prime
then (m1 | s9) ^ <*(m1 . s)*> = m1 | s by A23, Th5;
then (Product (m1 | s)) gcd (m . (k + 1)) = 1 by A31, A30, A28, RVSUM_1:96;
hence Product (m1 | s),m . (k + 1) are_relative_prime by INT_2:def_3; ::_thesis: verum
end;
hence S2[j + 1] ; ::_thesis: verum
end;
hence S2[j + 1] ; ::_thesis: verum
end;
m1 | 0 is empty ;
then A32: S2[ 0 ] by RVSUM_1:94, WSIERP_1:9;
A33: for j being Element of NAT st 0 <= j & j <= len m1 holds
S2[j] from INT_1:sch_7(A32, A20);
not i in Seg k by A7, A17, FINSEQ_1:def_3;
then ( not 1 <= i or not i <= k ) ;
then not i < k + 1 by A10, FINSEQ_1:1, NAT_1:13;
then A34: i = k + 1 by A11, XXREAL_0:1;
then mm = ((Product m1) * (m . (k + 1))) * ((m . (k + 1)) ") by A12, A6, RVSUM_1:96
.= (Product m1) * ((m . (k + 1)) * ((m . (k + 1)) "))
.= (Product m1) * 1 by A18, XCMPLX_0:def_7 ;
hence mm,m . i9 are_relative_prime by A34, A33, A19; ::_thesis: verum
end;
end;
end;
suppose k = 0 ; ::_thesis: b3,b1 . b2 are_relative_prime
then A35: m = <*(m . 1)*> by A5, FINSEQ_1:40;
then A36: dom m = Seg 1 by FINSEQ_1:38;
then A37: i <= 1 by A9, FINSEQ_1:1;
1 <= i by A9, A36, FINSEQ_1:1;
then A38: i = 1 by A37, XXREAL_0:1;
Product m = m . 1 by A35, RVSUM_1:95;
then mm = 1 by A12, A38, XCMPLX_0:def_7;
hence mm,m . i9 are_relative_prime by WSIERP_1:9; ::_thesis: verum
end;
end;
end;
hence S1[k + 1] ; ::_thesis: verum
end;
A39: S1[ 0 ] ;
A40: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A39, A3);
assume mm = (Product m) / (m . i) ; ::_thesis: mm,m . i are_relative_prime
hence mm,m . i are_relative_prime by A1, A40, A2; ::_thesis: verum
end;
Lm8: for u being INT -valued FinSequence
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
proof
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;
percases ( 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;
suppose k = 0 ; ::_thesis: z1,z2 are_congruent_mod Product b1
then A24: m1 = <*(m1 . 1)*> by A17, FINSEQ_1:40;
then dom m1 = Seg 1 by FINSEQ_1:38;
then A25: 1 in dom m1 ;
1 <= len m by A14, A13, XXREAL_0:2;
then 1 in Seg (len m) ;
then A26: 1 in dom m by FINSEQ_1:def_3;
Product m1 = m1 . 1 by A24, RVSUM_1:95
.= m . 1 by A16, A25, FUNCT_1:47 ;
hence z1,z2 are_congruent_mod Product m1 by A7, A26; ::_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
end;
begin
definition
let u be Integer;
let m be INT -valued FinSequence;
func mod (u,m) -> FinSequence means :Def3: :: INT_6:def 3
( len it = len m & ( for i being Nat st i in dom it holds
it . i = u mod (m . i) ) );
existence
ex b1 being FinSequence st
( len b1 = len m & ( for i being Nat st i in dom b1 holds
b1 . i = u mod (m . i) ) )
proof
defpred S1[ set , set ] means $2 = u mod (m . $1);
A1: for k being Nat st k in Seg (len m) holds
ex x being Element of INT st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len m) implies ex x being Element of INT st S1[k,x] )
assume k in Seg (len m) ; ::_thesis: ex x being Element of INT st S1[k,x]
reconsider j = u mod (m . k) as Element of INT by INT_1:def_2;
take j ; ::_thesis: S1[k,j]
thus S1[k,j] ; ::_thesis: verum
end;
consider p being FinSequence of INT such that
A2: ( dom p = Seg (len m) & ( for k being Nat st k in Seg (len m) holds
S1[k,p . k] ) ) from FINSEQ_1:sch_5(A1);
take p ; ::_thesis: ( len p = len m & ( for i being Nat st i in dom p holds
p . i = u mod (m . i) ) )
thus len p = len m by A2, FINSEQ_1:def_3; ::_thesis: for i being Nat st i in dom p holds
p . i = u mod (m . i)
thus for i being Nat st i in dom p holds
p . i = u mod (m . i) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence st len b1 = len m & ( for i being Nat st i in dom b1 holds
b1 . i = u mod (m . i) ) & len b2 = len m & ( for i being Nat st i in dom b2 holds
b2 . i = u mod (m . i) ) holds
b1 = b2
proof
let z1, z2 be FinSequence; ::_thesis: ( len z1 = len m & ( for i being Nat st i in dom z1 holds
z1 . i = u mod (m . i) ) & len z2 = len m & ( for i being Nat st i in dom z2 holds
z2 . i = u mod (m . i) ) implies z1 = z2 )
assume that
A3: len z1 = len m and
A4: for i being Nat st i in dom z1 holds
z1 . i = u mod (m . i) ; ::_thesis: ( not len z2 = len m or ex i being Nat st
( i in dom z2 & not z2 . i = u mod (m . i) ) or z1 = z2 )
assume that
A5: len z2 = len m and
A6: for i being Nat st i in dom z2 holds
z2 . i = u mod (m . i) ; ::_thesis: z1 = z2
A7: dom z1 = Seg (len z1) by FINSEQ_1:def_3
.= dom z2 by A3, A5, FINSEQ_1:def_3 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_z1_holds_
z1_._x_=_z2_._x
let x be set ; ::_thesis: ( x in dom z1 implies z1 . x = z2 . x )
assume A8: x in dom z1 ; ::_thesis: z1 . x = z2 . x
then reconsider x9 = x as Element of NAT ;
thus z1 . x = u mod (m . x9) by A4, A8
.= z2 . x by A6, A7, A8 ; ::_thesis: verum
end;
hence z1 = z2 by A7, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines mod INT_6:def_3_:_
for u being Integer
for m being INT -valued FinSequence
for b3 being FinSequence holds
( b3 = mod (u,m) iff ( len b3 = len m & ( for i being Nat st i in dom b3 holds
b3 . i = u mod (m . i) ) ) );
registration
let u be Integer;
let m be INT -valued FinSequence;
cluster mod (u,m) -> INT -valued ;
coherence
mod (u,m) is INT -valued
proof
now__::_thesis:_for_y_being_set_st_y_in_rng_(mod_(u,m))_holds_
y_in_INT
let y be set ; ::_thesis: ( y in rng (mod (u,m)) implies y in INT )
assume y in rng (mod (u,m)) ; ::_thesis: y in INT
then consider x being set such that
A1: x in dom (mod (u,m)) and
A2: (mod (u,m)) . x = y by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A1;
reconsider x = x as Nat ;
y = u mod (m . x) by A1, A2, Def3;
hence y in INT by INT_1:def_2; ::_thesis: verum
end;
then rng (mod (u,m)) c= INT by TARSKI:def_3;
hence mod (u,m) is INT -valued by RELAT_1:def_19; ::_thesis: verum
end;
end;
definition
let m be CR_Sequence;
mode CR_coefficients of m -> FinSequence means :Def4: :: INT_6:def 4
( len it = len m & ( for i being Nat st i in dom it holds
ex s, mm being Integer st
( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & it . i = s * ((Product m) / (m . i)) ) ) );
existence
ex b1 being FinSequence st
( len b1 = len m & ( for i being Nat st i in dom b1 holds
ex s, mm being Integer st
( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & b1 . i = s * ((Product m) / (m . i)) ) ) )
proof
defpred S1[ set , set ] means ex s, mm being Integer st
( mm = (Product m) / (m . $1) & s * mm,1 are_congruent_mod m . $1 & $2 = s * ((Product m) / (m . $1)) );
A1: for k being Nat st k in Seg (len m) holds
ex x being Element of INT st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len m) implies ex x being Element of INT st S1[k,x] )
assume k in Seg (len m) ; ::_thesis: ex x being Element of INT st S1[k,x]
then A2: k in dom m by FINSEQ_1:def_3;
then reconsider mm = (Product m) / (m . k) as Integer by Th9;
consider s being Integer such that
A3: s * mm,1 are_congruent_mod m . k by A2, Th22, Th25;
set x = s * mm;
reconsider x = s * mm as Element of INT by INT_1:def_2;
take x ; ::_thesis: S1[k,x]
take s ; ::_thesis: ex mm being Integer st
( mm = (Product m) / (m . k) & s * mm,1 are_congruent_mod m . k & x = s * ((Product m) / (m . k)) )
take mm ; ::_thesis: ( mm = (Product m) / (m . k) & s * mm,1 are_congruent_mod m . k & x = s * ((Product m) / (m . k)) )
thus ( mm = (Product m) / (m . k) & s * mm,1 are_congruent_mod m . k & x = s * ((Product m) / (m . k)) ) by A3; ::_thesis: verum
end;
consider p being FinSequence of INT such that
A4: ( dom p = Seg (len m) & ( for k being Nat st k in Seg (len m) holds
S1[k,p . k] ) ) from FINSEQ_1:sch_5(A1);
take p ; ::_thesis: ( len p = len m & ( for i being Nat st i in dom p holds
ex s, mm being Integer st
( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & p . i = s * ((Product m) / (m . i)) ) ) )
thus ( len p = len m & ( for i being Nat st i in dom p holds
ex s, mm being Integer st
( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & p . i = s * ((Product m) / (m . i)) ) ) ) by A4, FINSEQ_1:def_3; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines CR_coefficients INT_6:def_4_:_
for m being CR_Sequence
for b2 being FinSequence holds
( b2 is CR_coefficients of m iff ( len b2 = len m & ( for i being Nat st i in dom b2 holds
ex s, mm being Integer st
( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & b2 . i = s * ((Product m) / (m . i)) ) ) ) );
registration
let m be CR_Sequence;
cluster -> INT -valued for CR_coefficients of m;
coherence
for b1 being CR_coefficients of m holds b1 is INT -valued
proof
let c be CR_coefficients of m; ::_thesis: c is INT -valued
now__::_thesis:_for_u_being_set_st_u_in_rng_c_holds_
u_in_INT
let u be set ; ::_thesis: ( u in rng c implies u in INT )
assume u in rng c ; ::_thesis: u in INT
then consider x being set such that
A1: x in dom c and
A2: c . x = u by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A1;
reconsider x = x as Nat ;
ex s, mm being Integer st
( mm = (Product m) / (m . x) & s * mm,1 are_congruent_mod m . x & c . x = s * ((Product m) / (m . x)) ) by A1, Def4;
hence u in INT by A2, INT_1:def_2; ::_thesis: verum
end;
then rng c c= INT by TARSKI:def_3;
hence c is INT -valued by RELAT_1:def_19; ::_thesis: verum
end;
end;
theorem Th26: :: INT_6:26
for m being CR_Sequence
for c being CR_coefficients of m
for i being Nat st i in dom c holds
c . i,1 are_congruent_mod m . i
proof
let m be CR_Sequence; ::_thesis: for c being CR_coefficients of m
for i being Nat st i in dom c holds
c . i,1 are_congruent_mod m . i
let c be CR_coefficients of m; ::_thesis: for i being Nat st i in dom c holds
c . i,1 are_congruent_mod m . i
let i be Nat; ::_thesis: ( i in dom c implies c . i,1 are_congruent_mod m . i )
assume i in dom c ; ::_thesis: c . i,1 are_congruent_mod m . i
then ex s, mm being Integer st
( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & c . i = s * ((Product m) / (m . i)) ) by Def4;
hence c . i,1 are_congruent_mod m . i ; ::_thesis: verum
end;
theorem Th27: :: INT_6:27
for m being CR_Sequence
for c being CR_coefficients of m
for i, j being Nat st i in dom c & j in dom c & i <> j holds
c . i, 0 are_congruent_mod m . j
proof
let m be CR_Sequence; ::_thesis: for c being CR_coefficients of m
for i, j being Nat st i in dom c & j in dom c & i <> j holds
c . i, 0 are_congruent_mod m . j
let c be CR_coefficients of m; ::_thesis: for i, j being Nat st i in dom c & j in dom c & i <> j holds
c . i, 0 are_congruent_mod m . j
let i, j be Nat; ::_thesis: ( i in dom c & j in dom c & i <> j implies c . i, 0 are_congruent_mod m . j )
assume that
A1: i in dom c and
A2: j in dom c and
A3: i <> j ; ::_thesis: c . i, 0 are_congruent_mod m . j
consider s, mm being Integer such that
A4: mm = (Product m) / (m . i) and
s * mm,1 are_congruent_mod m . i and
A5: c . i = s * ((Product m) / (m . i)) by A1, Def4;
len m = len c by Def4;
then dom m = Seg (len c) by FINSEQ_1:def_3
.= dom c by FINSEQ_1:def_3 ;
then consider z being Integer such that
A6: z * (m . j) = mm by A1, A2, A3, A4, Lm6;
A7: m . j, 0 are_congruent_mod m . j by INT_1:12;
A8: s,s are_congruent_mod m . j by INT_1:11;
z,z are_congruent_mod m . j by INT_1:11;
then z * (m . j),z * 0 are_congruent_mod m . j by A7, INT_1:18;
then s * mm,s * 0 are_congruent_mod m . j by A6, A8, INT_1:18;
hence c . i, 0 are_congruent_mod m . j by A4, A5; ::_thesis: verum
end;
theorem :: INT_6:28
for m being CR_Sequence
for c1, c2 being CR_coefficients of m
for i being Nat st i in dom c1 holds
c1 . i,c2 . i are_congruent_mod m . i
proof
let m be CR_Sequence; ::_thesis: for c1, c2 being CR_coefficients of m
for i being Nat st i in dom c1 holds
c1 . i,c2 . i are_congruent_mod m . i
let c1, c2 be CR_coefficients of m; ::_thesis: for i being Nat st i in dom c1 holds
c1 . i,c2 . i are_congruent_mod m . i
let i be Nat; ::_thesis: ( i in dom c1 implies c1 . i,c2 . i are_congruent_mod m . i )
assume A1: i in dom c1 ; ::_thesis: c1 . i,c2 . i are_congruent_mod m . i
then A2: ex s1, mm1 being Integer st
( mm1 = (Product m) / (m . i) & s1 * mm1,1 are_congruent_mod m . i & c1 . i = s1 * ((Product m) / (m . i)) ) by Def4;
A3: len c1 = len m by Def4
.= len c2 by Def4 ;
dom c1 = Seg (len c1) by FINSEQ_1:def_3
.= dom c2 by A3, FINSEQ_1:def_3 ;
then consider s2, mm2 being Integer such that
A4: mm2 = (Product m) / (m . i) and
A5: s2 * mm2,1 are_congruent_mod m . i and
A6: c2 . i = s2 * ((Product m) / (m . i)) by A1, Def4;
1,s2 * mm2 are_congruent_mod m . i by A5, INT_1:14;
hence c1 . i,c2 . i are_congruent_mod m . i by A2, A4, A6, INT_1:15; ::_thesis: verum
end;
theorem Th29: :: INT_6:29
for u being INT -valued FinSequence
for m being CR_Sequence st len m = len u holds
for c being CR_coefficients of m
for i being Nat st i in dom m holds
Sum (u (#) c),u . i are_congruent_mod m . i
proof
let u be INT -valued FinSequence; ::_thesis: for m being CR_Sequence st len m = len u holds
for c being CR_coefficients of m
for i being Nat 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 Nat st i in dom m holds
Sum (u (#) c),u . i are_congruent_mod m . i )
assume A1: len m = len u ; ::_thesis: for c being CR_coefficients of m
for i being Nat 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 Nat st i in dom m holds
Sum (u (#) c),u . i are_congruent_mod m . i
let i be Nat; ::_thesis: ( i in dom m implies Sum (u (#) c),u . i are_congruent_mod m . i )
defpred S1[ Nat] means for v, cc being INT -valued 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 ; ::_thesis: 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__::_thesis:_for_k_being_Element_of_NAT_st_0_<=_k_&_k_<_len_u_&_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( 0 <= k & k < len u & S1[k] implies S1[k + 1] )
assume that
0 <= k and
A6: k < len u and
A7: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_for_v,_cc_being_INT_-valued_FinSequence_st_v_=_u_|_(k_+_1)_&_cc_=_c_|_(k_+_1)_&_not_(_k_+_1_<_i_&_Sum_(v_(#)_cc),_0_are_congruent_mod_m_._i_)_holds_
(_k_+_1_>=_i_&_Sum_(v_(#)_cc),u_._i_are_congruent_mod_m_._i_)
set v9 = u | k;
set cc9 = c | k;
let v, cc be INT -valued 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 ) )
A8: 0 + 1 <= k + 1 by XREAL_1:6;
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) ; ::_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 ) )
k + 1 <= len u by A6, NAT_1:13;
then len v = k + 1 by A9, FINSEQ_1:59;
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:47;
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:59;
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:47;
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:16
.= k + 1 by A19, FINSEQ_1:59 ;
A21: k + 1 = len ((u (#) c) | (k + 1)) by A18, FINSEQ_1:59;
now__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_(((u_(#)_c)_|_k)_^_<*((v_._(k_+_1))_*_(cc_._(k_+_1)))*>)_holds_
(((u_(#)_c)_|_k)_^_<*((v_._(k_+_1))_*_(cc_._(k_+_1)))*>)_._j_=_((u_(#)_c)_|_(k_+_1))_._j
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 that
A22: 1 <= j and
A23: 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)) . b1
A24: j in NAT by ORDINAL1:def_12;
percases ( j in dom ((u (#) c) | k) or not j in dom ((u (#) c) | k) ) ;
supposeA25: j in dom ((u (#) c) | k) ; ::_thesis: (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . b1 = ((u (#) c) | (k + 1)) . b1
j in Seg (k + 1) by A20, A22, A23, A24;
then A26: j in dom ((u (#) c) | (k + 1)) by A21, FINSEQ_1:def_3;
thus (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . j = ((u (#) c) | k) . j by A25, FINSEQ_1:def_7
.= (u (#) c) . j by A25, FUNCT_1:47
.= ((u (#) c) | (k + 1)) . j by A26, FUNCT_1:47 ; ::_thesis: verum
end;
supposeA27: 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 A6, A14, Lm4;
then A28: len ((u (#) c) | k) = k by FINSEQ_1:59;
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:2, FINSEQ_1:38;
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:40 ;
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:47
.= (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; ::_thesis: verum
end;
end;
end;
hence ((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*> = (u (#) c) | (k + 1) by A20, A21, FINSEQ_1:14; ::_thesis: 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:75
.= (Sum ((u | k) (#) (c | k))) + ((v . (k + 1)) * (cc . (k + 1))) by RVSUM_1:73 ;
A34: k < k + 1 by NAT_1:13;
now__::_thesis:_(_(_k_+_1_<_i_&_Sum_(v_(#)_cc),_0_are_congruent_mod_m_._i_)_or_(_k_+_1_=_i_&_Sum_(v_(#)_cc),0_+_(u_._i)_are_congruent_mod_m_._i_)_or_(_k_+_1_>_i_&_Sum_(v_(#)_cc),(u_._i)_+_0_are_congruent_mod_m_._i_)_)
percases ( k + 1 < i or k + 1 = i or k + 1 > i ) by XXREAL_0:1;
caseA35: k + 1 < i ; ::_thesis: Sum (v (#) cc), 0 are_congruent_mod m . i
then 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:11;
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:18;
then Sum (v (#) cc),0 + ((v . (k + 1)) * 0) are_congruent_mod m . i by A33, A36, INT_1:16;
hence Sum (v (#) cc), 0 are_congruent_mod m . i ; ::_thesis: verum
end;
caseA38: k + 1 = i ; ::_thesis: Sum (v (#) cc),0 + (u . i) are_congruent_mod m . i
A39: v . (k + 1),v . (k + 1) are_congruent_mod m . i by INT_1:11;
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:18;
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:16; ::_thesis: verum
end;
caseA41: k + 1 > i ; ::_thesis: Sum (v (#) cc),(u . i) + 0 are_congruent_mod m . i
then 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:11;
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:18;
hence Sum (v (#) cc),(u . i) + 0 are_congruent_mod m . i by A33, A42, INT_1:16; ::_thesis: verum
end;
end;
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;
A44: dom m = Seg (len u) by A1, FINSEQ_1:def_3;
now__::_thesis:_for_v,_cc_being_INT_-valued_FinSequence_st_v_=_u_|_0_&_cc_=_c_|_0_&_not_(_0_<_i_&_Sum_(v_(#)_cc),_0_are_congruent_mod_m_._i_)_holds_
(_0_>=_i_&_Sum_(v_(#)_cc),u_._i_are_congruent_mod_m_._i_)
let v, cc be INT -valued 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 that
A45: v = u | 0 and
A46: 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 ) )
(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:1, INT_1:11, RVSUM_1:72; ::_thesis: 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:58;
A50: u = u | (len u) by FINSEQ_1:58;
i <= len u by A2, A44, FINSEQ_1:1;
hence Sum (u (#) c),u . i are_congruent_mod m . i by A48, A50, A49; ::_thesis: verum
end;
theorem Th30: :: INT_6:30
for u being INT -valued FinSequence
for m being CR_Sequence st len m = len u holds
for c1, c2 being CR_coefficients of m holds Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m
proof
let u be INT -valued FinSequence; ::_thesis: for m being CR_Sequence st len m = len u holds
for c1, c2 being CR_coefficients of m holds Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m
let m be CR_Sequence; ::_thesis: ( len m = len u implies for c1, c2 being CR_coefficients of m holds Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m )
assume A1: len u = len m ; ::_thesis: for c1, c2 being CR_coefficients of m holds Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m
let c1, c2 be CR_coefficients of m; ::_thesis: Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m
set s1 = (Sum (u (#) c1)) mod (Product m);
set s2 = (Sum (u (#) c2)) mod (Product m);
A2: (Sum (u (#) c1)) mod (Product m) < Product m by NAT_D:62;
A3: for i being Nat st i in dom m holds
(Sum (u (#) c1)) mod (Product m),u . i are_congruent_mod m . i
proof
let i be Nat; ::_thesis: ( i in dom m implies (Sum (u (#) c1)) mod (Product m),u . i are_congruent_mod m . i )
((Sum (u (#) c1)) mod (Product m)) mod (Product m) = (Sum (u (#) c1)) mod (Product m) by NAT_D:65;
then A4: (Sum (u (#) c1)) mod (Product m), Sum (u (#) c1) are_congruent_mod Product m by NAT_D:64;
assume A5: i in dom m ; ::_thesis: (Sum (u (#) c1)) mod (Product m),u . i are_congruent_mod m . i
then m . i in rng m by FUNCT_1:3;
then A6: m . i > 0 by PARTFUN3:def_1;
ex z being Integer st z * (m . i) = Product m by A5, Th10;
then (Sum (u (#) c1)) mod (Product m), Sum (u (#) c1) are_congruent_mod m . i by A4, INT_1:20;
then A7: ((Sum (u (#) c1)) mod (Product m)) mod (m . i) = (Sum (u (#) c1)) mod (m . i) by NAT_D:64;
Sum (u (#) c1),u . i are_congruent_mod m . i by A1, A5, Th29;
then (Sum (u (#) c1)) mod (m . i) = (u . i) mod (m . i) by NAT_D:64;
hence (Sum (u (#) c1)) mod (Product m),u . i are_congruent_mod m . i by A6, A7, NAT_D:64; ::_thesis: verum
end;
A8: 0 <= (Sum (u (#) c2)) mod (Product m) by NAT_D:62;
A9: for i being Nat st i in dom m holds
(Sum (u (#) c2)) mod (Product m),u . i are_congruent_mod m . i
proof
let i be Nat; ::_thesis: ( i in dom m implies (Sum (u (#) c2)) mod (Product m),u . i are_congruent_mod m . i )
((Sum (u (#) c2)) mod (Product m)) mod (Product m) = (Sum (u (#) c2)) mod (Product m) by NAT_D:65;
then A10: (Sum (u (#) c2)) mod (Product m), Sum (u (#) c2) are_congruent_mod Product m by NAT_D:64;
assume A11: i in dom m ; ::_thesis: (Sum (u (#) c2)) mod (Product m),u . i are_congruent_mod m . i
then m . i in rng m by FUNCT_1:3;
then A12: m . i > 0 by PARTFUN3:def_1;
ex z being Integer st z * (m . i) = Product m by A11, Th10;
then (Sum (u (#) c2)) mod (Product m), Sum (u (#) c2) are_congruent_mod m . i by A10, INT_1:20;
then A13: ((Sum (u (#) c2)) mod (Product m)) mod (m . i) = (Sum (u (#) c2)) mod (m . i) by NAT_D:64;
Sum (u (#) c2),u . i are_congruent_mod m . i by A1, A11, Th29;
then (Sum (u (#) c2)) mod (m . i) = (u . i) mod (m . i) by NAT_D:64;
hence (Sum (u (#) c2)) mod (Product m),u . i are_congruent_mod m . i by A12, A13, NAT_D:64; ::_thesis: verum
end;
A14: (Sum (u (#) c2)) mod (Product m) < Product m by NAT_D:62;
0 <= (Sum (u (#) c1)) mod (Product m) by NAT_D:62;
then (Sum (u (#) c1)) mod (Product m) = (Sum (u (#) c2)) mod (Product m) by A3, A9, A2, A8, A14, Lm8;
hence Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m by NAT_D:64; ::_thesis: verum
end;
definition
let u be INT -valued FinSequence;
let m be CR_Sequence;
assume A1: len m = len u ;
func to_int (u,m) -> Integer means :Def5: :: INT_6:def 5
for c being CR_coefficients of m holds it = (Sum (u (#) c)) mod (Product m);
existence
ex b1 being Integer st
for c being CR_coefficients of m holds b1 = (Sum (u (#) c)) mod (Product m)
proof
set cz = the CR_coefficients of m;
set z = (Sum (u (#) the CR_coefficients of m)) mod (Product m);
take (Sum (u (#) the CR_coefficients of m)) mod (Product m) ; ::_thesis: for c being CR_coefficients of m holds (Sum (u (#) the CR_coefficients of m)) mod (Product m) = (Sum (u (#) c)) mod (Product m)
now__::_thesis:_for_c_being_CR_coefficients_of_m_holds_(Sum_(u_(#)_the_CR_coefficients_of_m))_mod_(Product_m)_=_(Sum_(u_(#)_c))_mod_(Product_m)
let c be CR_coefficients of m; ::_thesis: (Sum (u (#) the CR_coefficients of m)) mod (Product m) = (Sum (u (#) c)) mod (Product m)
Sum (u (#) c), Sum (u (#) the CR_coefficients of m) are_congruent_mod Product m by A1, Th30;
hence (Sum (u (#) the CR_coefficients of m)) mod (Product m) = (Sum (u (#) c)) mod (Product m) by NAT_D:64; ::_thesis: verum
end;
hence for c being CR_coefficients of m holds (Sum (u (#) the CR_coefficients of m)) mod (Product m) = (Sum (u (#) c)) mod (Product m) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Integer st ( for c being CR_coefficients of m holds b1 = (Sum (u (#) c)) mod (Product m) ) & ( for c being CR_coefficients of m holds b2 = (Sum (u (#) c)) mod (Product m) ) holds
b1 = b2
proof
set c = the CR_coefficients of m;
let z1, z2 be Integer; ::_thesis: ( ( for c being CR_coefficients of m holds z1 = (Sum (u (#) c)) mod (Product m) ) & ( for c being CR_coefficients of m holds z2 = (Sum (u (#) c)) mod (Product m) ) implies z1 = z2 )
assume A1: for c being CR_coefficients of m holds z1 = (Sum (u (#) c)) mod (Product m) ; ::_thesis: ( ex c being CR_coefficients of m st not z2 = (Sum (u (#) c)) mod (Product m) or z1 = z2 )
assume A2: for c being CR_coefficients of m holds z2 = (Sum (u (#) c)) mod (Product m) ; ::_thesis: z1 = z2
thus z1 = (Sum (u (#) the CR_coefficients of m)) mod (Product m) by A1
.= z2 by A2 ; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines to_int INT_6:def_5_:_
for u being INT -valued FinSequence
for m being CR_Sequence st len m = len u holds
for b3 being Integer holds
( b3 = to_int (u,m) iff for c being CR_coefficients of m holds b3 = (Sum (u (#) c)) mod (Product m) );
theorem Th31: :: INT_6:31
for u being INT -valued FinSequence
for m being CR_Sequence st len m = len u holds
( 0 <= to_int (u,m) & to_int (u,m) < Product m )
proof
let u be INT -valued FinSequence; ::_thesis: for m being CR_Sequence st len m = len u holds
( 0 <= to_int (u,m) & to_int (u,m) < Product m )
let m be CR_Sequence; ::_thesis: ( len m = len u implies ( 0 <= to_int (u,m) & to_int (u,m) < Product m ) )
set z = to_int (u,m);
set c = the CR_coefficients of m;
assume len u = len m ; ::_thesis: ( 0 <= to_int (u,m) & to_int (u,m) < Product m )
then to_int (u,m) = (Sum (u (#) the CR_coefficients of m)) mod (Product m) by Def5;
hence ( 0 <= to_int (u,m) & to_int (u,m) < Product m ) by NAT_D:62; ::_thesis: verum
end;
theorem Th32: :: INT_6:32
for u being Integer
for m being CR_Sequence
for i being Nat st i in dom m holds
u,(mod (u,m)) . i are_congruent_mod m . i
proof
let u be Integer; ::_thesis: for m being CR_Sequence
for i being Nat st i in dom m holds
u,(mod (u,m)) . i are_congruent_mod m . i
let m be CR_Sequence; ::_thesis: for i being Nat st i in dom m holds
u,(mod (u,m)) . i are_congruent_mod m . i
let i be Nat; ::_thesis: ( i in dom m implies u,(mod (u,m)) . i are_congruent_mod m . i )
A1: len (mod (u,m)) = len m by Def3;
assume A2: i in dom m ; ::_thesis: u,(mod (u,m)) . i are_congruent_mod m . i
then m . i in rng m by FUNCT_1:3;
then m . i > 0 by PARTFUN3:def_1;
then u mod (m . i) = u - ((u div (m . i)) * (m . i)) by INT_1:def_10;
then A3: u - (u mod (m . i)) = (u div (m . i)) * (m . i) ;
dom (mod (u,m)) = Seg (len (mod (u,m))) by FINSEQ_1:def_3
.= dom m by A1, FINSEQ_1:def_3 ;
then (mod (u,m)) . i = u mod (m . i) by A2, Def3;
hence u,(mod (u,m)) . i are_congruent_mod m . i by A3, INT_1:def_5; ::_thesis: verum
end;
theorem Th33: :: INT_6:33
for u, v being Integer
for m being CR_Sequence
for i being Nat st i in dom m holds
((mod (u,m)) + (mod (v,m))) . i,u + v are_congruent_mod m . i
proof
let u, v be Integer; ::_thesis: for m being CR_Sequence
for i being Nat st i in dom m holds
((mod (u,m)) + (mod (v,m))) . i,u + v are_congruent_mod m . i
let m be CR_Sequence; ::_thesis: for i being Nat st i in dom m holds
((mod (u,m)) + (mod (v,m))) . i,u + v are_congruent_mod m . i
let i be Nat; ::_thesis: ( i in dom m implies ((mod (u,m)) + (mod (v,m))) . i,u + v are_congruent_mod m . i )
assume A1: i in dom m ; ::_thesis: ((mod (u,m)) + (mod (v,m))) . i,u + v are_congruent_mod m . i
A2: len (mod (v,m)) = len m by Def3;
then dom (mod (v,m)) = Seg (len m) by FINSEQ_1:def_3
.= dom m by FINSEQ_1:def_3 ;
then A3: (mod (v,m)) . i = v mod (m . i) by A1, Def3;
A4: len (mod (u,m)) = len m by Def3;
then len ((mod (u,m)) + (mod (v,m))) = len m by A2, Lm2;
then dom ((mod (u,m)) + (mod (v,m))) = Seg (len m) by FINSEQ_1:def_3
.= dom m by FINSEQ_1:def_3 ;
then A5: ((mod (u,m)) + (mod (v,m))) . i = ((mod (u,m)) . i) + ((mod (v,m)) . i) by A1, VALUED_1:def_1;
dom (mod (u,m)) = Seg (len m) by A4, FINSEQ_1:def_3
.= dom m by FINSEQ_1:def_3 ;
then (mod (u,m)) . i = u mod (m . i) by A1, Def3;
then A6: (((mod (u,m)) . i) + ((mod (v,m)) . i)) mod (m . i) = (u + v) mod (m . i) by A3, NAT_D:66;
m . i in rng m by A1, FUNCT_1:3;
then m . i > 0 by PARTFUN3:def_1;
hence ((mod (u,m)) + (mod (v,m))) . i,u + v are_congruent_mod m . i by A5, A6, NAT_D:64; ::_thesis: verum
end;
Lm9: for u, v being Integer
for m being CR_Sequence
for i being Nat st i in dom m holds
((mod (u,m)) - (mod (v,m))) . i,u - v are_congruent_mod m . i
proof
let u, v be Integer; ::_thesis: for m being CR_Sequence
for i being Nat st i in dom m holds
((mod (u,m)) - (mod (v,m))) . i,u - v are_congruent_mod m . i
let m be CR_Sequence; ::_thesis: for i being Nat st i in dom m holds
((mod (u,m)) - (mod (v,m))) . i,u - v are_congruent_mod m . i
let i be Nat; ::_thesis: ( i in dom m implies ((mod (u,m)) - (mod (v,m))) . i,u - v are_congruent_mod m . i )
assume A1: i in dom m ; ::_thesis: ((mod (u,m)) - (mod (v,m))) . i,u - v are_congruent_mod m . i
A2: len (mod (v,m)) = len m by Def3;
then dom (mod (v,m)) = Seg (len m) by FINSEQ_1:def_3
.= dom m by FINSEQ_1:def_3 ;
then A3: (mod (v,m)) . i = v mod (m . i) by A1, Def3;
A4: len (mod (u,m)) = len m by Def3;
then len ((mod (u,m)) - (mod (v,m))) = len m by A2, Lm3;
then dom ((mod (u,m)) - (mod (v,m))) = Seg (len m) by FINSEQ_1:def_3
.= dom m by FINSEQ_1:def_3 ;
then A5: ((mod (u,m)) - (mod (v,m))) . i = ((mod (u,m)) . i) - ((mod (v,m)) . i) by A1, VALUED_1:13;
dom (mod (u,m)) = Seg (len m) by A4, FINSEQ_1:def_3
.= dom m by FINSEQ_1:def_3 ;
then (mod (u,m)) . i = u mod (m . i) by A1, Def3;
then A6: (((mod (u,m)) . i) - ((mod (v,m)) . i)) mod (m . i) = (u - v) mod (m . i) by A3, Th7;
m . i in rng m by A1, FUNCT_1:3;
then m . i > 0 by PARTFUN3:def_1;
hence ((mod (u,m)) - (mod (v,m))) . i,u - v are_congruent_mod m . i by A5, A6, NAT_D:64; ::_thesis: verum
end;
theorem Th34: :: INT_6:34
for u, v being Integer
for m being CR_Sequence
for i being Nat st i in dom m holds
((mod (u,m)) (#) (mod (v,m))) . i,u * v are_congruent_mod m . i
proof
let u, v be Integer; ::_thesis: for m being CR_Sequence
for i being Nat st i in dom m holds
((mod (u,m)) (#) (mod (v,m))) . i,u * v are_congruent_mod m . i
let m be CR_Sequence; ::_thesis: for i being Nat st i in dom m holds
((mod (u,m)) (#) (mod (v,m))) . i,u * v are_congruent_mod m . i
let i be Nat; ::_thesis: ( i in dom m implies ((mod (u,m)) (#) (mod (v,m))) . i,u * v are_congruent_mod m . i )
assume A1: i in dom m ; ::_thesis: ((mod (u,m)) (#) (mod (v,m))) . i,u * v are_congruent_mod m . i
A2: len (mod (v,m)) = len m by Def3;
then dom (mod (v,m)) = Seg (len m) by FINSEQ_1:def_3
.= dom m by FINSEQ_1:def_3 ;
then A3: (mod (v,m)) . i = v mod (m . i) by A1, Def3;
A4: len (mod (u,m)) = len m by Def3;
then len ((mod (u,m)) (#) (mod (v,m))) = len m by A2, Lm4;
then dom ((mod (u,m)) (#) (mod (v,m))) = Seg (len m) by FINSEQ_1:def_3
.= dom m by FINSEQ_1:def_3 ;
then A5: ((mod (u,m)) (#) (mod (v,m))) . i = ((mod (u,m)) . i) * ((mod (v,m)) . i) by A1, VALUED_1:def_4;
dom (mod (u,m)) = Seg (len m) by A4, FINSEQ_1:def_3
.= dom m by FINSEQ_1:def_3 ;
then (mod (u,m)) . i = u mod (m . i) by A1, Def3;
then A6: (((mod (u,m)) . i) * ((mod (v,m)) . i)) mod (m . i) = (u * v) mod (m . i) by A3, NAT_D:67;
m . i in rng m by A1, FUNCT_1:3;
then m . i > 0 by PARTFUN3:def_1;
hence ((mod (u,m)) (#) (mod (v,m))) . i,u * v are_congruent_mod m . i by A5, A6, NAT_D:64; ::_thesis: verum
end;
theorem Th35: :: INT_6:35
for u, v being Integer
for m being CR_Sequence
for i being Nat st i in dom m holds
to_int (((mod (u,m)) + (mod (v,m))),m),u + v are_congruent_mod m . i
proof
let u, v be Integer; ::_thesis: for m being CR_Sequence
for i being Nat st i in dom m holds
to_int (((mod (u,m)) + (mod (v,m))),m),u + v are_congruent_mod m . i
let m be CR_Sequence; ::_thesis: for i being Nat st i in dom m holds
to_int (((mod (u,m)) + (mod (v,m))),m),u + v are_congruent_mod m . i
let i be Nat; ::_thesis: ( i in dom m implies to_int (((mod (u,m)) + (mod (v,m))),m),u + v are_congruent_mod m . i )
set z = to_int (((mod (u,m)) + (mod (v,m))),m);
set c = the CR_coefficients of m;
A1: len (mod (u,m)) = len m by Def3;
len (mod (v,m)) = len m by Def3;
then A2: len ((mod (u,m)) + (mod (v,m))) = len m by A1, Lm2;
then to_int (((mod (u,m)) + (mod (v,m))),m) = (Sum (((mod (u,m)) + (mod (v,m))) (#) the CR_coefficients of m)) mod (Product m) by Def5;
then (to_int (((mod (u,m)) + (mod (v,m))),m)) mod (Product m) = (Sum (((mod (u,m)) + (mod (v,m))) (#) the CR_coefficients of m)) mod (Product m) by NAT_D:65;
then A3: to_int (((mod (u,m)) + (mod (v,m))),m), Sum (((mod (u,m)) + (mod (v,m))) (#) the CR_coefficients of m) are_congruent_mod Product m by NAT_D:64;
assume A4: i in dom m ; ::_thesis: to_int (((mod (u,m)) + (mod (v,m))),m),u + v are_congruent_mod m . i
then ex y being Integer st y * (m . i) = Product m by Th10;
then A5: to_int (((mod (u,m)) + (mod (v,m))),m), Sum (((mod (u,m)) + (mod (v,m))) (#) the CR_coefficients of m) are_congruent_mod m . i by A3, INT_1:20;
Sum (((mod (u,m)) + (mod (v,m))) (#) the CR_coefficients of m),((mod (u,m)) + (mod (v,m))) . i are_congruent_mod m . i by A4, A2, Th29;
then A6: to_int (((mod (u,m)) + (mod (v,m))),m),((mod (u,m)) + (mod (v,m))) . i are_congruent_mod m . i by A5, INT_1:15;
((mod (u,m)) + (mod (v,m))) . i,u + v are_congruent_mod m . i by A4, Th33;
hence to_int (((mod (u,m)) + (mod (v,m))),m),u + v are_congruent_mod m . i by A6, INT_1:15; ::_thesis: verum
end;
theorem Th36: :: INT_6:36
for u, v being Integer
for m being CR_Sequence
for i being Nat st i in dom m holds
to_int (((mod (u,m)) - (mod (v,m))),m),u - v are_congruent_mod m . i
proof
let u, v be Integer; ::_thesis: for m being CR_Sequence
for i being Nat st i in dom m holds
to_int (((mod (u,m)) - (mod (v,m))),m),u - v are_congruent_mod m . i
let m be CR_Sequence; ::_thesis: for i being Nat st i in dom m holds
to_int (((mod (u,m)) - (mod (v,m))),m),u - v are_congruent_mod m . i
let i be Nat; ::_thesis: ( i in dom m implies to_int (((mod (u,m)) - (mod (v,m))),m),u - v are_congruent_mod m . i )
set z = to_int (((mod (u,m)) - (mod (v,m))),m);
set c = the CR_coefficients of m;
A1: len (mod (u,m)) = len m by Def3;
len (mod (v,m)) = len m by Def3;
then A2: len ((mod (u,m)) - (mod (v,m))) = len m by A1, Lm3;
then to_int (((mod (u,m)) - (mod (v,m))),m) = (Sum (((mod (u,m)) - (mod (v,m))) (#) the CR_coefficients of m)) mod (Product m) by Def5;
then (to_int (((mod (u,m)) - (mod (v,m))),m)) mod (Product m) = (Sum (((mod (u,m)) - (mod (v,m))) (#) the CR_coefficients of m)) mod (Product m) by NAT_D:65;
then A3: to_int (((mod (u,m)) - (mod (v,m))),m), Sum (((mod (u,m)) - (mod (v,m))) (#) the CR_coefficients of m) are_congruent_mod Product m by NAT_D:64;
assume A4: i in dom m ; ::_thesis: to_int (((mod (u,m)) - (mod (v,m))),m),u - v are_congruent_mod m . i
then ex y being Integer st y * (m . i) = Product m by Th10;
then A5: to_int (((mod (u,m)) - (mod (v,m))),m), Sum (((mod (u,m)) - (mod (v,m))) (#) the CR_coefficients of m) are_congruent_mod m . i by A3, INT_1:20;
Sum (((mod (u,m)) - (mod (v,m))) (#) the CR_coefficients of m),((mod (u,m)) - (mod (v,m))) . i are_congruent_mod m . i by A4, A2, Th29;
then A6: to_int (((mod (u,m)) - (mod (v,m))),m),((mod (u,m)) - (mod (v,m))) . i are_congruent_mod m . i by A5, INT_1:15;
((mod (u,m)) - (mod (v,m))) . i,u - v are_congruent_mod m . i by A4, Lm9;
hence to_int (((mod (u,m)) - (mod (v,m))),m),u - v are_congruent_mod m . i by A6, INT_1:15; ::_thesis: verum
end;
theorem Th37: :: INT_6:37
for u, v being Integer
for m being CR_Sequence
for i being Nat st i in dom m holds
to_int (((mod (u,m)) (#) (mod (v,m))),m),u * v are_congruent_mod m . i
proof
let u, v be Integer; ::_thesis: for m being CR_Sequence
for i being Nat st i in dom m holds
to_int (((mod (u,m)) (#) (mod (v,m))),m),u * v are_congruent_mod m . i
let m be CR_Sequence; ::_thesis: for i being Nat st i in dom m holds
to_int (((mod (u,m)) (#) (mod (v,m))),m),u * v are_congruent_mod m . i
let i be Nat; ::_thesis: ( i in dom m implies to_int (((mod (u,m)) (#) (mod (v,m))),m),u * v are_congruent_mod m . i )
set z = to_int (((mod (u,m)) (#) (mod (v,m))),m);
set c = the CR_coefficients of m;
A1: len (mod (u,m)) = len m by Def3;
len (mod (v,m)) = len m by Def3;
then A2: len ((mod (u,m)) (#) (mod (v,m))) = len m by A1, Lm4;
then to_int (((mod (u,m)) (#) (mod (v,m))),m) = (Sum (((mod (u,m)) (#) (mod (v,m))) (#) the CR_coefficients of m)) mod (Product m) by Def5;
then (to_int (((mod (u,m)) (#) (mod (v,m))),m)) mod (Product m) = (Sum (((mod (u,m)) (#) (mod (v,m))) (#) the CR_coefficients of m)) mod (Product m) by NAT_D:65;
then A3: to_int (((mod (u,m)) (#) (mod (v,m))),m), Sum (((mod (u,m)) (#) (mod (v,m))) (#) the CR_coefficients of m) are_congruent_mod Product m by NAT_D:64;
assume A4: i in dom m ; ::_thesis: to_int (((mod (u,m)) (#) (mod (v,m))),m),u * v are_congruent_mod m . i
then ex y being Integer st y * (m . i) = Product m by Th10;
then A5: to_int (((mod (u,m)) (#) (mod (v,m))),m), Sum (((mod (u,m)) (#) (mod (v,m))) (#) the CR_coefficients of m) are_congruent_mod m . i by A3, INT_1:20;
Sum (((mod (u,m)) (#) (mod (v,m))) (#) the CR_coefficients of m),((mod (u,m)) (#) (mod (v,m))) . i are_congruent_mod m . i by A4, A2, Th29;
then A6: to_int (((mod (u,m)) (#) (mod (v,m))),m),((mod (u,m)) (#) (mod (v,m))) . i are_congruent_mod m . i by A5, INT_1:15;
((mod (u,m)) (#) (mod (v,m))) . i,u * v are_congruent_mod m . i by A4, Th34;
hence to_int (((mod (u,m)) (#) (mod (v,m))),m),u * v are_congruent_mod m . i by A6, INT_1:15; ::_thesis: verum
end;
theorem :: INT_6:38
for u, v being Integer
for m being CR_Sequence st 0 <= u + v & u + v < Product m holds
to_int (((mod (u,m)) + (mod (v,m))),m) = u + v
proof
let u, v be Integer; ::_thesis: for m being CR_Sequence st 0 <= u + v & u + v < Product m holds
to_int (((mod (u,m)) + (mod (v,m))),m) = u + v
let m be CR_Sequence; ::_thesis: ( 0 <= u + v & u + v < Product m implies to_int (((mod (u,m)) + (mod (v,m))),m) = u + v )
assume that
A1: 0 <= u + v and
A2: u + v < Product m ; ::_thesis: to_int (((mod (u,m)) + (mod (v,m))),m) = u + v
set z = to_int (((mod (u,m)) + (mod (v,m))),m);
A3: for i being Nat st i in dom m holds
u + v,(mod ((u + v),m)) . i are_congruent_mod m . i by Th32;
A4: len (mod ((u + v),m)) = len m by Def3;
A5: for i being Nat st i in dom m holds
to_int (((mod (u,m)) + (mod (v,m))),m),(mod ((u + v),m)) . i are_congruent_mod m . i
proof
let i be Nat; ::_thesis: ( i in dom m implies to_int (((mod (u,m)) + (mod (v,m))),m),(mod ((u + v),m)) . i are_congruent_mod m . i )
assume A6: i in dom m ; ::_thesis: to_int (((mod (u,m)) + (mod (v,m))),m),(mod ((u + v),m)) . i are_congruent_mod m . i
then to_int (((mod (u,m)) + (mod (v,m))),m),u + v are_congruent_mod m . i by Th35;
then A7: (to_int (((mod (u,m)) + (mod (v,m))),m)) mod (m . i) = (u + v) mod (m . i) by NAT_D:64;
dom (mod ((u + v),m)) = Seg (len m) by A4, FINSEQ_1:def_3
.= dom m by FINSEQ_1:def_3 ;
then A8: (mod ((u + v),m)) . i = (u + v) mod (m . i) by A6, Def3;
m . i in rng m by A6, FUNCT_1:3;
then A9: m . i > 0 by PARTFUN3:def_1;
then m . i is Element of NAT by INT_1:3;
then (u + v) mod (m . i) = ((u + v) mod (m . i)) mod (m . i) by NAT_D:65;
hence to_int (((mod (u,m)) + (mod (v,m))),m),(mod ((u + v),m)) . i are_congruent_mod m . i by A8, A7, A9, NAT_D:64; ::_thesis: verum
end;
A10: len (mod (u,m)) = len m by Def3;
len (mod (v,m)) = len m by Def3;
then A11: len ((mod (u,m)) + (mod (v,m))) = len m by A10, Lm2;
then A12: to_int (((mod (u,m)) + (mod (v,m))),m) < Product m by Th31;
0 <= to_int (((mod (u,m)) + (mod (v,m))),m) by A11, Th31;
hence to_int (((mod (u,m)) + (mod (v,m))),m) = u + v by A1, A2, A3, A12, A5, Lm8; ::_thesis: verum
end;
theorem :: INT_6:39
for u, v being Integer
for m being CR_Sequence st 0 <= u - v & u - v < Product m holds
to_int (((mod (u,m)) - (mod (v,m))),m) = u - v
proof
let u, v be Integer; ::_thesis: for m being CR_Sequence st 0 <= u - v & u - v < Product m holds
to_int (((mod (u,m)) - (mod (v,m))),m) = u - v
let m be CR_Sequence; ::_thesis: ( 0 <= u - v & u - v < Product m implies to_int (((mod (u,m)) - (mod (v,m))),m) = u - v )
assume that
A1: 0 <= u - v and
A2: u - v < Product m ; ::_thesis: to_int (((mod (u,m)) - (mod (v,m))),m) = u - v
set z = to_int (((mod (u,m)) - (mod (v,m))),m);
A3: for i being Nat st i in dom m holds
u - v,(mod ((u - v),m)) . i are_congruent_mod m . i by Th32;
A4: len (mod ((u - v),m)) = len m by Def3;
A5: for i being Nat st i in dom m holds
to_int (((mod (u,m)) - (mod (v,m))),m),(mod ((u - v),m)) . i are_congruent_mod m . i
proof
let i be Nat; ::_thesis: ( i in dom m implies to_int (((mod (u,m)) - (mod (v,m))),m),(mod ((u - v),m)) . i are_congruent_mod m . i )
assume A6: i in dom m ; ::_thesis: to_int (((mod (u,m)) - (mod (v,m))),m),(mod ((u - v),m)) . i are_congruent_mod m . i
then to_int (((mod (u,m)) - (mod (v,m))),m),u - v are_congruent_mod m . i by Th36;
then A7: (to_int (((mod (u,m)) - (mod (v,m))),m)) mod (m . i) = (u - v) mod (m . i) by NAT_D:64;
dom (mod ((u - v),m)) = Seg (len m) by A4, FINSEQ_1:def_3
.= dom m by FINSEQ_1:def_3 ;
then A8: (mod ((u - v),m)) . i = (u - v) mod (m . i) by A6, Def3;
m . i in rng m by A6, FUNCT_1:3;
then A9: m . i > 0 by PARTFUN3:def_1;
then m . i is Element of NAT by INT_1:3;
then (u - v) mod (m . i) = ((u - v) mod (m . i)) mod (m . i) by NAT_D:65;
hence to_int (((mod (u,m)) - (mod (v,m))),m),(mod ((u - v),m)) . i are_congruent_mod m . i by A8, A7, A9, NAT_D:64; ::_thesis: verum
end;
A10: len (mod (u,m)) = len m by Def3;
len (mod (v,m)) = len m by Def3;
then A11: len ((mod (u,m)) - (mod (v,m))) = len m by A10, Lm3;
then A12: to_int (((mod (u,m)) - (mod (v,m))),m) < Product m by Th31;
0 <= to_int (((mod (u,m)) - (mod (v,m))),m) by A11, Th31;
hence to_int (((mod (u,m)) - (mod (v,m))),m) = u - v by A1, A2, A3, A12, A5, Lm8; ::_thesis: verum
end;
theorem :: INT_6:40
for u, v being Integer
for m being CR_Sequence st 0 <= u * v & u * v < Product m holds
to_int (((mod (u,m)) (#) (mod (v,m))),m) = u * v
proof
let u, v be Integer; ::_thesis: for m being CR_Sequence st 0 <= u * v & u * v < Product m holds
to_int (((mod (u,m)) (#) (mod (v,m))),m) = u * v
let m be CR_Sequence; ::_thesis: ( 0 <= u * v & u * v < Product m implies to_int (((mod (u,m)) (#) (mod (v,m))),m) = u * v )
assume that
A1: 0 <= u * v and
A2: u * v < Product m ; ::_thesis: to_int (((mod (u,m)) (#) (mod (v,m))),m) = u * v
set z = to_int (((mod (u,m)) (#) (mod (v,m))),m);
A3: for i being Nat st i in dom m holds
u * v,(mod ((u * v),m)) . i are_congruent_mod m . i by Th32;
A4: len (mod ((u * v),m)) = len m by Def3;
A5: for i being Nat st i in dom m holds
to_int (((mod (u,m)) (#) (mod (v,m))),m),(mod ((u * v),m)) . i are_congruent_mod m . i
proof
let i be Nat; ::_thesis: ( i in dom m implies to_int (((mod (u,m)) (#) (mod (v,m))),m),(mod ((u * v),m)) . i are_congruent_mod m . i )
assume A6: i in dom m ; ::_thesis: to_int (((mod (u,m)) (#) (mod (v,m))),m),(mod ((u * v),m)) . i are_congruent_mod m . i
then to_int (((mod (u,m)) (#) (mod (v,m))),m),u * v are_congruent_mod m . i by Th37;
then A7: (to_int (((mod (u,m)) (#) (mod (v,m))),m)) mod (m . i) = (u * v) mod (m . i) by NAT_D:64;
dom (mod ((u * v),m)) = Seg (len m) by A4, FINSEQ_1:def_3
.= dom m by FINSEQ_1:def_3 ;
then A8: (mod ((u * v),m)) . i = (u * v) mod (m . i) by A6, Def3;
m . i in rng m by A6, FUNCT_1:3;
then A9: m . i > 0 by PARTFUN3:def_1;
then m . i is Element of NAT by INT_1:3;
then (u * v) mod (m . i) = ((u * v) mod (m . i)) mod (m . i) by NAT_D:65;
hence to_int (((mod (u,m)) (#) (mod (v,m))),m),(mod ((u * v),m)) . i are_congruent_mod m . i by A8, A7, A9, NAT_D:64; ::_thesis: verum
end;
A10: len (mod (u,m)) = len m by Def3;
len (mod (v,m)) = len m by Def3;
then A11: len ((mod (u,m)) (#) (mod (v,m))) = len m by A10, Lm4;
then A12: to_int (((mod (u,m)) (#) (mod (v,m))),m) < Product m by Th31;
0 <= to_int (((mod (u,m)) (#) (mod (v,m))),m) by A11, Th31;
hence to_int (((mod (u,m)) (#) (mod (v,m))),m) = u * v by A1, A2, A3, A12, A5, Lm8; ::_thesis: verum
end;
begin
theorem :: INT_6:41
for u being INT -valued FinSequence
for m being CR_Sequence st len u = len m holds
ex z being Integer st
( 0 <= z & z < Product m & ( for i being Nat st i in dom u holds
z,u . i are_congruent_mod m . i ) )
proof
let u be INT -valued FinSequence; ::_thesis: for m being CR_Sequence st len u = len m holds
ex z being Integer st
( 0 <= z & z < Product m & ( for i being Nat st i in dom u holds
z,u . i are_congruent_mod m . i ) )
let m be CR_Sequence; ::_thesis: ( len u = len m implies ex z being Integer st
( 0 <= z & z < Product m & ( for i being Nat st i in dom u holds
z,u . i are_congruent_mod m . i ) ) )
assume A1: len u = len m ; ::_thesis: ex z being Integer st
( 0 <= z & z < Product m & ( for i being Nat st i in dom u holds
z,u . i are_congruent_mod m . i ) )
take z = to_int (u,m); ::_thesis: ( 0 <= z & z < Product m & ( for i being Nat st i in dom u holds
z,u . i are_congruent_mod m . i ) )
now__::_thesis:_for_i_being_Nat_st_i_in_dom_u_holds_
z,u_._i_are_congruent_mod_m_._i
set c = the CR_coefficients of m;
let i be Nat; ::_thesis: ( i in dom u implies z,u . i are_congruent_mod m . i )
assume A2: i in dom u ; ::_thesis: z,u . i are_congruent_mod m . i
set s = (Sum (u (#) the CR_coefficients of m)) mod (Product m);
((Sum (u (#) the CR_coefficients of m)) mod (Product m)) mod (Product m) = (Sum (u (#) the CR_coefficients of m)) mod (Product m) by NAT_D:65;
then A3: (Sum (u (#) the CR_coefficients of m)) mod (Product m), Sum (u (#) the CR_coefficients of m) are_congruent_mod Product m by NAT_D:64;
A4: dom m = Seg (len u) by A1, FINSEQ_1:def_3
.= dom u by FINSEQ_1:def_3 ;
then ex y being Integer st y * (m . i) = Product m by A2, Th10;
then (Sum (u (#) the CR_coefficients of m)) mod (Product m), Sum (u (#) the CR_coefficients of m) are_congruent_mod m . i by A3, INT_1:20;
then A5: ((Sum (u (#) the CR_coefficients of m)) mod (Product m)) mod (m . i) = (Sum (u (#) the CR_coefficients of m)) mod (m . i) by NAT_D:64;
dom m = Seg (len u) by A1, FINSEQ_1:def_3
.= dom u by FINSEQ_1:def_3 ;
then m . i in rng m by A2, FUNCT_1:3;
then A6: m . i > 0 by PARTFUN3:def_1;
Sum (u (#) the CR_coefficients of m),u . i are_congruent_mod m . i by A1, A2, A4, Th29;
then (Sum (u (#) the CR_coefficients of m)) mod (m . i) = (u . i) mod (m . i) by NAT_D:64;
then (Sum (u (#) the CR_coefficients of m)) mod (Product m),u . i are_congruent_mod m . i by A6, A5, NAT_D:64;
hence z,u . i are_congruent_mod m . i by A1, Def5; ::_thesis: verum
end;
hence ( 0 <= z & z < Product m & ( for i being Nat st i in dom u holds
z,u . i are_congruent_mod m . i ) ) by A1, Th31; ::_thesis: verum
end;
theorem :: INT_6:42
for u being INT -valued FinSequence
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 by Lm8;