:: 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;