:: INT_4 semantic presentation begin theorem Th1: :: INT_4:1 for X being real-membered set for a being real number holds X,a ++ X are_equipotent proof let X be real-membered set ; ::_thesis: for a being real number holds X,a ++ X are_equipotent let a be real number ; ::_thesis: X,a ++ X are_equipotent deffunc H1( Real) -> Element of REAL = a + $1; consider f being Function such that A1: ( dom f = X & ( for x being Element of REAL st x in X holds f . x = H1(x) ) ) from GRAPH_5:sch_1(); A2: rng f = a ++ X proof thus rng f c= a ++ X :: according to XBOOLE_0:def_10 ::_thesis: a ++ X c= rng f proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in a ++ X ) assume z in rng f ; ::_thesis: z in a ++ X then consider x being set such that A3: x in dom f and A4: z = f . x by FUNCT_1:def_3; reconsider x = x as real number by A1, A3; reconsider x = x as Real by XREAL_0:def_1; a + x is real ; then reconsider z9 = z as Real by A1, A3, A4; z9 = a + x by A1, A3, A4; hence z in a ++ X by A1, A3, MEMBER_1:141; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in a ++ X or z in rng f ) assume A5: z in a ++ X ; ::_thesis: z in rng f then reconsider z = z as Element of REAL ; consider x being Element of COMPLEX such that A6: z = a + x and A7: x in X by A5, MEMBER_1:143; X c= REAL by MEMBERED:3; then reconsider x = x as Element of REAL by A7; f . x = z by A1, A7, A6; hence z in rng f by A1, A7, FUNCT_1:def_3; ::_thesis: verum end; take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = X & rng f = a ++ X ) f is one-to-one proof let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume that A8: x in dom f and A9: y in dom f and A10: f . x = f . y ; ::_thesis: x = y reconsider x = x, y = y as Real by A1, A8, A9, XREAL_0:def_1; f . x = a + x by A1, A8; then a + x = a + y by A1, A9, A10; hence x = y ; ::_thesis: verum end; hence ( f is one-to-one & dom f = X & rng f = a ++ X ) by A1, A2; ::_thesis: verum end; registration let X be finite real-membered set ; let a be real number ; clusterK687(X,a) -> finite ; coherence a ++ X is finite by Th1, CARD_1:38; end; theorem Th2: :: INT_4:2 for X being real-membered set for a being real number holds card X = card (a ++ X) proof let X be real-membered set ; ::_thesis: for a being real number holds card X = card (a ++ X) let a be real number ; ::_thesis: card X = card (a ++ X) X,a ++ X are_equipotent by Th1; hence card X = card (a ++ X) by CARD_1:5; ::_thesis: verum end; Lm1: for a being Integer for X being Subset of INT holds a ++ X c= INT proof let a be Integer; ::_thesis: for X being Subset of INT holds a ++ X c= INT let X be Subset of INT; ::_thesis: a ++ X c= INT let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a ++ X or x in INT ) assume A1: x in a ++ X ; ::_thesis: x in INT then reconsider x9 = x as Real ; consider y being Element of COMPLEX such that A2: x9 = a + y and A3: y in X by A1, MEMBER_1:143; reconsider y9 = y as Integer by A3; x9 = a + y9 by A2; hence x in INT by INT_1:def_2; ::_thesis: verum end; Lm2: for a being Integer for X being Subset of INT holds a ** X c= INT proof let a be Integer; ::_thesis: for X being Subset of INT holds a ** X c= INT let X be Subset of INT; ::_thesis: a ** X c= INT let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a ** X or x in INT ) assume A1: x in a ** X ; ::_thesis: x in INT then reconsider x9 = x as Real ; consider y being Element of COMPLEX such that A2: x9 = a * y and A3: y in X by A1, MEMBER_1:195; reconsider y9 = y as Integer by A3; x9 = a * y9 by A2; hence x in INT by INT_1:def_2; ::_thesis: verum end; Lm3: for x being Integer for X being Subset of INT for a being Integer holds ( x in a ** X iff ex y being Integer st ( y in X & x = a * y ) ) proof let x be Integer; ::_thesis: for X being Subset of INT for a being Integer holds ( x in a ** X iff ex y being Integer st ( y in X & x = a * y ) ) let X be Subset of INT; ::_thesis: for a being Integer holds ( x in a ** X iff ex y being Integer st ( y in X & x = a * y ) ) let a be Integer; ::_thesis: ( x in a ** X iff ex y being Integer st ( y in X & x = a * y ) ) hereby ::_thesis: ( ex y being Integer st ( y in X & x = a * y ) implies x in a ** X ) assume x in a ** X ; ::_thesis: ex z being Integer st ( z in X & x = a * z ) then consider z being Element of COMPLEX such that A1: x = a * z and A2: z in X by MEMBER_1:195; reconsider z = z as Integer by A2; take z = z; ::_thesis: ( z in X & x = a * z ) thus ( z in X & x = a * z ) by A2, A1; ::_thesis: verum end; given y being Integer such that A3: ( y in X & x = a * y ) ; ::_thesis: x in a ** X reconsider x9 = x as Real by XREAL_0:def_1; reconsider y = y as Real by XREAL_0:def_1; ex z being Real st ( z in X & x9 = a * z ) proof take y ; ::_thesis: ( y in X & x9 = a * y ) thus ( y in X & x9 = a * y ) by A3; ::_thesis: verum end; hence x in a ** X by MEMBER_1:193; ::_thesis: verum end; theorem Th3: :: INT_4:3 for X being real-membered set for a being real number st a <> 0 holds X,a ** X are_equipotent proof let X be real-membered set ; ::_thesis: for a being real number st a <> 0 holds X,a ** X are_equipotent let a be real number ; ::_thesis: ( a <> 0 implies X,a ** X are_equipotent ) deffunc H1( Real) -> Element of REAL = a * $1; consider f being Function such that A1: ( dom f = X & ( for x being Element of REAL st x in X holds f . x = H1(x) ) ) from GRAPH_5:sch_1(); assume A2: a <> 0 ; ::_thesis: X,a ** X are_equipotent A3: f is one-to-one proof let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume that A4: ( x in dom f & y in dom f ) and A5: f . x = f . y ; ::_thesis: x = y reconsider x = x, y = y as Element of REAL by A1, A4, XREAL_0:def_1; ( f . x = a * x & f . y = a * y ) by A1, A4; hence x = y by A2, A5, XCMPLX_1:5; ::_thesis: verum end; take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = X & rng f = a ** X ) rng f = a ** X proof thus rng f c= a ** X :: according to XBOOLE_0:def_10 ::_thesis: a ** X c= rng f proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in a ** X ) assume z in rng f ; ::_thesis: z in a ** X then consider x being set such that A6: x in dom f and A7: z = f . x by FUNCT_1:def_3; reconsider x9 = x as Real by A1, A6, XREAL_0:def_1; z = a * x9 by A1, A6, A7; hence z in a ** X by A1, A6, MEMBER_1:193; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in a ** X or z in rng f ) assume A8: z in a ** X ; ::_thesis: z in rng f then reconsider z = z as Element of REAL ; consider x being Element of COMPLEX such that A9: z = a * x and A10: x in X by A8, MEMBER_1:195; reconsider x = x as Real by A10, XREAL_0:def_1; f . x = z by A1, A10, A9; hence z in rng f by A1, A10, FUNCT_1:def_3; ::_thesis: verum end; hence ( f is one-to-one & dom f = X & rng f = a ** X ) by A1, A3; ::_thesis: verum end; theorem Th4: :: INT_4:4 for X being real-membered set for a being real number holds ( ( a = 0 & not X is empty implies a ** X = {0} ) & ( not a ** X = {0} or a = 0 or X = {0} ) ) proof let X be real-membered set ; ::_thesis: for a being real number holds ( ( a = 0 & not X is empty implies a ** X = {0} ) & ( not a ** X = {0} or a = 0 or X = {0} ) ) let a be real number ; ::_thesis: ( ( a = 0 & not X is empty implies a ** X = {0} ) & ( not a ** X = {0} or a = 0 or X = {0} ) ) thus ( a = 0 & not X is empty implies a ** X = {0} ) ::_thesis: ( not a ** X = {0} or a = 0 or X = {0} ) proof assume that A1: a = 0 and A2: not X is empty ; ::_thesis: a ** X = {0} thus a ** X c= {0} :: according to XBOOLE_0:def_10 ::_thesis: {0} c= a ** X proof let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in a ** X or i in {0} ) assume A3: i in a ** X ; ::_thesis: i in {0} then reconsider i = i as Real ; ex x being Element of COMPLEX st ( i = a * x & x in X ) by A3, MEMBER_1:195; hence i in {0} by A1, TARSKI:def_1; ::_thesis: verum end; then ( a ** X = {} or a ** X = {0} ) by ZFMISC_1:33; hence {0} c= a ** X by A2, INTEGRA2:7; ::_thesis: verum end; assume that A4: a ** X = {0} and A5: a <> 0 ; ::_thesis: X = {0} X,a ** X are_equipotent by A5, Th3; then consider x being set such that A6: X = {x} by A4, CARD_1:28; A7: x in X by A6, TARSKI:def_1; then reconsider x = x as real number ; a * x in a ** X by A7, MEMBER_1:193; then a * x = 0 by A4, TARSKI:def_1; hence X = {0} by A5, A6, XCMPLX_1:6; ::_thesis: verum end; registration let X be finite real-membered set ; let a be real number ; clusterK693(X,a) -> finite ; coherence a ** X is finite proof percases ( a <> 0 or a = 0 ) ; suppose a <> 0 ; ::_thesis: a ** X is finite hence a ** X is finite by Th3, CARD_1:38; ::_thesis: verum end; supposeA1: a = 0 ; ::_thesis: a ** X is finite percases ( X is empty or not X is empty ) ; suppose X is empty ; ::_thesis: a ** X is finite hence a ** X is finite by INTEGRA2:7; ::_thesis: verum end; suppose not X is empty ; ::_thesis: a ** X is finite hence a ** X is finite by A1, Th4; ::_thesis: verum end; end; end; end; end; end; theorem Th5: :: INT_4:5 for X being real-membered set for a being real number st a <> 0 holds card X = card (a ** X) proof let X be real-membered set ; ::_thesis: for a being real number st a <> 0 holds card X = card (a ** X) let a be real number ; ::_thesis: ( a <> 0 implies card X = card (a ** X) ) assume a <> 0 ; ::_thesis: card X = card (a ** X) then X,a ** X are_equipotent by Th3; hence card X = card (a ** X) by CARD_1:5; ::_thesis: verum end; begin Lm4: for i1, i2, i3 being Integer st i1 divides i2 & i1 divides i3 holds i1 divides i2 - i3 proof let i1, i2, i3 be Integer; ::_thesis: ( i1 divides i2 & i1 divides i3 implies i1 divides i2 - i3 ) assume that A1: i1 divides i2 and A2: i1 divides i3 ; ::_thesis: i1 divides i2 - i3 consider i4 being Integer such that A3: i2 = i1 * i4 by A1, INT_1:def_3; consider i5 being Integer such that A4: i3 = i1 * i5 by A2, INT_1:def_3; i2 - i3 = i1 * (i4 - i5) by A3, A4; hence i1 divides i2 - i3 by INT_1:def_3; ::_thesis: verum end; Lm5: for i, a, b being Integer st i divides a & i divides a - b holds i divides b proof let i, a, b be Integer; ::_thesis: ( i divides a & i divides a - b implies i divides b ) assume that A1: i divides a and A2: i divides a - b ; ::_thesis: i divides b A3: b = (- (a - b)) + a ; i divides - (a - b) by A2, INT_2:10; hence i divides b by A1, A3, WSIERP_1:4; ::_thesis: verum end; Lm6: for p, n being Nat st p is prime & p,n are_relative_prime holds not p divides n proof let p, n be Nat; ::_thesis: ( p is prime & p,n are_relative_prime implies not p divides n ) assume that A1: p is prime and A2: p,n are_relative_prime ; ::_thesis: not p divides n assume p divides n ; ::_thesis: contradiction then n gcd p = p by NEWTON:49; then n gcd p > 1 by A1, INT_2:def_4; hence contradiction by A2, INT_2:def_3; ::_thesis: verum end; Lm7: for p being Nat st p > 0 holds p >= 1 + 0 by NAT_1:13; theorem Th6: :: INT_4:6 for i, i1 being Integer st i divides i1 & i1 <> 0 holds abs i <= abs i1 proof let i, i1 be Integer; ::_thesis: ( i divides i1 & i1 <> 0 implies abs i <= abs i1 ) assume ( i divides i1 & i1 <> 0 ) ; ::_thesis: abs i <= abs i1 then ( abs i1 <> 0 & abs i divides abs i1 ) by ABSVALUE:2, INT_2:16; hence abs i <= abs i1 by NAT_D:7; ::_thesis: verum end; theorem Th7: :: INT_4:7 for i1, i2, i3 being Integer st i3 <> 0 holds ( i1 divides i2 iff i1 * i3 divides i2 * i3 ) proof let i1, i2, i3 be Integer; ::_thesis: ( i3 <> 0 implies ( i1 divides i2 iff i1 * i3 divides i2 * i3 ) ) assume A1: i3 <> 0 ; ::_thesis: ( i1 divides i2 iff i1 * i3 divides i2 * i3 ) thus ( i1 divides i2 implies i1 * i3 divides i2 * i3 ) ::_thesis: ( i1 * i3 divides i2 * i3 implies i1 divides i2 ) proof assume i1 divides i2 ; ::_thesis: i1 * i3 divides i2 * i3 then consider i4 being Integer such that A2: i2 = i1 * i4 by INT_1:def_3; i2 * i3 = (i1 * i3) * i4 by A2; hence i1 * i3 divides i2 * i3 by INT_1:def_3; ::_thesis: verum end; assume i1 * i3 divides i2 * i3 ; ::_thesis: i1 divides i2 then consider i5 being Integer such that A3: i2 * i3 = (i1 * i3) * i5 by INT_1:def_3; i2 * i3 = (i1 * i5) * i3 by A3; then i2 = i1 * i5 by A1, XCMPLX_1:5; hence i1 divides i2 by INT_1:def_3; ::_thesis: verum end; theorem :: INT_4:8 for a, b, m being Nat for n being Element of NAT st a mod m = b mod m holds (a |^ n) mod m = (b |^ n) mod m proof let a, b, m be Nat; ::_thesis: for n being Element of NAT st a mod m = b mod m holds (a |^ n) mod m = (b |^ n) mod m let n be Element of NAT ; ::_thesis: ( a mod m = b mod m implies (a |^ n) mod m = (b |^ n) mod m ) defpred S1[ Nat] means (a |^ $1) mod m = (b |^ $1) mod m; assume A1: a mod m = b mod m ; ::_thesis: (a |^ n) mod m = (b |^ n) mod m 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] reconsider l1 = a |^ k, l2 = b |^ k, a = a, b = b, m = m as Element of NAT by ORDINAL1:def_12; (a |^ (k + 1)) mod m = ((a |^ k) * a) mod m by NEWTON:6 .= ((l1 mod m) * (a mod m)) mod m by EULER_2:9 .= (l2 * b) mod m by A1, A3, EULER_2:9 .= (b |^ (k + 1)) mod m by NEWTON:6 ; hence S1[k + 1] ; ::_thesis: verum end; a |^ 0 = 1 by NEWTON:4; then A4: S1[ 0 ] by NEWTON:4; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A2); hence (a |^ n) mod m = (b |^ n) mod m ; ::_thesis: verum end; theorem Th9: :: INT_4:9 for i1, i, i2, i3 being Integer st i1 * i,i2 * i are_congruent_mod i3 & i,i3 are_relative_prime holds i1,i2 are_congruent_mod i3 proof let i1, i, i2, i3 be Integer; ::_thesis: ( i1 * i,i2 * i are_congruent_mod i3 & i,i3 are_relative_prime implies i1,i2 are_congruent_mod i3 ) assume that A1: i1 * i,i2 * i are_congruent_mod i3 and A2: i,i3 are_relative_prime ; ::_thesis: i1,i2 are_congruent_mod i3 i3 divides (i1 * i) - (i2 * i) by A1, INT_2:15; then i3 divides (i1 - i2) * i ; then i3 divides i1 - i2 by A2, INT_2:25; hence i1,i2 are_congruent_mod i3 by INT_2:15; ::_thesis: verum end; theorem Th10: :: INT_4:10 for i1, i2, i3 being Integer for k being Nat st i1,i2 are_congruent_mod i3 holds i1 * k,i2 * k are_congruent_mod i3 * k proof let i1, i2, i3 be Integer; ::_thesis: for k being Nat st i1,i2 are_congruent_mod i3 holds i1 * k,i2 * k are_congruent_mod i3 * k let k be Nat; ::_thesis: ( i1,i2 are_congruent_mod i3 implies i1 * k,i2 * k are_congruent_mod i3 * k ) assume i1,i2 are_congruent_mod i3 ; ::_thesis: i1 * k,i2 * k are_congruent_mod i3 * k then consider i4 being Integer such that A1: i3 * i4 = i1 - i2 by INT_1:def_5; (i3 * k) * i4 = (i3 * i4) * k .= (i1 + (- i2)) * k by A1 .= (i1 * k) - (i2 * k) ; hence i1 * k,i2 * k are_congruent_mod i3 * k by INT_1:def_5; ::_thesis: verum end; theorem Th11: :: INT_4:11 for i1, i2, i, i3 being Integer st i1,i2 are_congruent_mod i holds i1 * i3,i2 * i3 are_congruent_mod i proof let i1, i2, i, i3 be Integer; ::_thesis: ( i1,i2 are_congruent_mod i implies i1 * i3,i2 * i3 are_congruent_mod i ) assume i1,i2 are_congruent_mod i ; ::_thesis: i1 * i3,i2 * i3 are_congruent_mod i then i divides i1 - i2 by INT_2:15; then i divides (i1 - i2) * i3 by INT_2:2; then i divides (i1 * i3) - (i2 * i3) ; hence i1 * i3,i2 * i3 are_congruent_mod i by INT_2:15; ::_thesis: verum end; theorem Th12: :: INT_4:12 for i being Integer holds 0 = 0 mod i proof let i be Integer; ::_thesis: 0 = 0 mod i percases ( i = 0 or i <> 0 ) ; suppose i = 0 ; ::_thesis: 0 = 0 mod i hence 0 = 0 mod i by INT_1:def_10; ::_thesis: verum end; supposeA1: i <> 0 ; ::_thesis: 0 = 0 mod i 0 div i = 0 by INT_1:25; then 0 mod i = 0 - (i * 0) by A1, INT_1:def_10; hence 0 = 0 mod i ; ::_thesis: verum end; end; end; theorem Th13: :: INT_4:13 for b being Integer st b > 0 holds for a being Integer ex q, r being Integer st ( a = (b * q) + r & r >= 0 & r < b ) proof let b be Integer; ::_thesis: ( b > 0 implies for a being Integer ex q, r being Integer st ( a = (b * q) + r & r >= 0 & r < b ) ) assume A1: b > 0 ; ::_thesis: for a being Integer ex q, r being Integer st ( a = (b * q) + r & r >= 0 & r < b ) let a be Integer; ::_thesis: ex q, r being Integer st ( a = (b * q) + r & r >= 0 & r < b ) percases ( a >= 0 or a < 0 ) ; supposeA2: a >= 0 ; ::_thesis: ex q, r being Integer st ( a = (b * q) + r & r >= 0 & r < b ) A3: b in NAT by A1, INT_1:3; a in NAT by A2, INT_1:3; then consider k, t being Nat such that A4: ( a = (b * k) + t & t < b ) by A1, A3, NAT_1:17; take k ; ::_thesis: ex r being Integer st ( a = (b * k) + r & r >= 0 & r < b ) take t ; ::_thesis: ( a = (b * k) + t & t >= 0 & t < b ) thus ( a = (b * k) + t & t >= 0 & t < b ) by A4; ::_thesis: verum end; supposeA5: a < 0 ; ::_thesis: ex q, r being Integer st ( a = (b * q) + r & r >= 0 & r < b ) A6: b in NAT by A1, INT_1:3; - a in NAT by A5, INT_1:3; then consider k, t being Nat such that A7: - a = (b * k) + t and A8: t < b by A1, A6, NAT_1:17; percases ( t = 0 or t <> 0 ) ; supposeA9: t = 0 ; ::_thesis: ex q, r being Integer st ( a = (b * q) + r & r >= 0 & r < b ) take q = - k; ::_thesis: ex r being Integer st ( a = (b * q) + r & r >= 0 & r < b ) take r = 0 ; ::_thesis: ( a = (b * q) + r & r >= 0 & r < b ) a = b * (- k) by A7, A9; hence a = (b * q) + r ; ::_thesis: ( r >= 0 & r < b ) thus ( r >= 0 & r < b ) by A1; ::_thesis: verum end; supposeA10: t <> 0 ; ::_thesis: ex q, r being Integer st ( a = (b * q) + r & r >= 0 & r < b ) take q = (- k) - 1; ::_thesis: ex r being Integer st ( a = (b * q) + r & r >= 0 & r < b ) take r = b - t; ::_thesis: ( a = (b * q) + r & r >= 0 & r < b ) a = (b * ((- k) - 1)) + (b - t) by A7; hence a = (b * q) + r ; ::_thesis: ( r >= 0 & r < b ) thus ( r >= 0 & r < b ) by A8, A10, XREAL_1:44, XREAL_1:50; ::_thesis: verum end; end; end; end; end; theorem :: INT_4:14 for i1, i2, i3 being Integer st i1,i2 are_congruent_mod i3 holds i1 gcd i3 = i2 gcd i3 proof let i1, i2, i3 be Integer; ::_thesis: ( i1,i2 are_congruent_mod i3 implies i1 gcd i3 = i2 gcd i3 ) set d = i2 gcd i3; reconsider d = i2 gcd i3 as Nat ; assume i1,i2 are_congruent_mod i3 ; ::_thesis: i1 gcd i3 = i2 gcd i3 then i3 divides i1 - i2 by INT_2:15; then consider i being Integer such that A1: i1 - i2 = i3 * i by INT_1:def_3; A2: d = (abs i2) gcd (abs i3) by INT_2:34; then d divides abs i2 by NAT_D:def_5; then abs d divides abs i2 by ABSVALUE:def_1; then A3: d divides i2 by INT_2:16; A4: i2 = i1 - (i3 * i) by A1; A5: for n being Nat st n divides abs i1 & n divides abs i3 holds n divides d proof let n be Nat; ::_thesis: ( n divides abs i1 & n divides abs i3 implies n divides d ) assume that A6: n divides abs i1 and A7: n divides abs i3 ; ::_thesis: n divides d abs n divides abs i3 by A7, ABSVALUE:def_1; then n divides i3 by INT_2:16; then A8: n divides i3 * i by INT_2:2; abs n divides abs i1 by A6, ABSVALUE:def_1; then n divides i1 by INT_2:16; then n divides i2 by A4, A8, Lm4; then abs n divides abs i2 by INT_2:16; then n divides abs i2 by ABSVALUE:def_1; hence n divides d by A2, A7, NAT_D:def_5; ::_thesis: verum end; A9: d divides abs i3 by A2, NAT_D:def_5; then abs d divides abs i3 by ABSVALUE:def_1; then d divides i3 by INT_2:16; then A10: d divides i3 * i by INT_2:2; i1 = (i3 * i) + i2 by A1; then ( abs d = d & d divides i1 ) by A3, A10, ABSVALUE:def_1, WSIERP_1:4; then d divides abs i1 by INT_2:16; then (abs i1) gcd (abs i3) = d by A9, A5, NAT_D:def_5; hence i1 gcd i3 = i2 gcd i3 by INT_2:34; ::_thesis: verum end; theorem Th15: :: INT_4:15 for a, m, b being Integer st a,m are_relative_prime holds ex x being Integer st ((a * x) - b) mod m = 0 proof let a, m, b be Integer; ::_thesis: ( a,m are_relative_prime implies ex x being Integer st ((a * x) - b) mod m = 0 ) assume a,m are_relative_prime ; ::_thesis: ex x being Integer st ((a * x) - b) mod m = 0 then a gcd m = 1 by INT_2:def_3; then consider s, t being Integer such that A1: 1 = (s * a) + (t * m) by NAT_D:68; take b * s ; ::_thesis: ((a * (b * s)) - b) mod m = 0 (((a * b) * s) - b) mod m = (((a * s) - 1) * b) mod m .= ((- (m * t)) * b) mod m by A1 .= (0 + (m * ((- t) * b))) mod m .= 0 mod m by NAT_D:61 .= 0 by Th12 ; hence ((a * (b * s)) - b) mod m = 0 ; ::_thesis: verum end; theorem Th16: :: INT_4:16 for m, a, b being Integer st m > 0 & a,m are_relative_prime holds ex n being Nat st ((a * n) - b) mod m = 0 proof let m, a, b be Integer; ::_thesis: ( m > 0 & a,m are_relative_prime implies ex n being Nat st ((a * n) - b) mod m = 0 ) assume that A1: m > 0 and A2: a,m are_relative_prime ; ::_thesis: ex n being Nat st ((a * n) - b) mod m = 0 consider x being Integer such that A3: ((a * x) - b) mod m = 0 by A2, Th15; consider q, n being Integer such that A4: x = (m * q) + n and A5: n >= 0 and n < m by A1, Th13; A6: ((a * x) - b) mod m = (((a * q) * m) + ((a * n) - b)) mod m by A4 .= ((a * n) - b) mod m by EULER_1:12 ; n in NAT by A5, INT_1:3; then reconsider n = n as Nat ; take n ; ::_thesis: ((a * n) - b) mod m = 0 thus ((a * n) - b) mod m = 0 by A3, A6; ::_thesis: verum end; theorem :: INT_4:17 for m, a, b being Integer st m <> 0 & not a gcd m divides b holds for x being Integer holds not ((a * x) - b) mod m = 0 proof let m, a, b be Integer; ::_thesis: ( m <> 0 & not a gcd m divides b implies for x being Integer holds not ((a * x) - b) mod m = 0 ) assume that A1: m <> 0 and A2: not a gcd m divides b ; ::_thesis: for x being Integer holds not ((a * x) - b) mod m = 0 given y being Integer such that A3: ((a * y) - b) mod m = 0 ; ::_thesis: contradiction a gcd m divides m by INT_2:21; then A4: ex i being Integer st m = (a gcd m) * i by INT_1:def_3; ((a * y) - b) mod m = 0 mod m by A3, Th12; then (a * y) - b, 0 are_congruent_mod m by A1, NAT_D:64; then (a * y) - b, 0 are_congruent_mod a gcd m by A4, INT_1:20; then A5: a gcd m divides ((a * y) - b) - 0 by INT_2:15; a gcd m divides a * y by INT_2:2, INT_2:21; hence contradiction by A2, A5, Lm5; ::_thesis: verum end; theorem :: INT_4:18 for m, a, b being Integer st m <> 0 & a gcd m divides b holds ex x being Integer st ((a * x) - b) mod m = 0 proof let m, a, b be Integer; ::_thesis: ( m <> 0 & a gcd m divides b implies ex x being Integer st ((a * x) - b) mod m = 0 ) assume that A1: m <> 0 and A2: a gcd m divides b ; ::_thesis: ex x being Integer st ((a * x) - b) mod m = 0 consider a1, m1 being Integer such that A3: a = (a gcd m) * a1 and A4: m = (a gcd m) * m1 and A5: a1,m1 are_relative_prime by A1, INT_2:23; consider b1 being Integer such that A6: b = (a gcd m) * b1 by A2, INT_1:def_3; A7: m1 <> 0 by A1, A4; consider y being Integer such that A8: ((a1 * y) - b1) mod m1 = 0 by A5, Th15; take y ; ::_thesis: ((a * y) - b) mod m = 0 ((a1 * y) - b1) mod m1 = 0 mod m1 by A8, Th12; then (a1 * y) - b1, 0 are_congruent_mod m1 by A7, NAT_D:64; then ((a1 * y) - b1) * (a gcd m),(a gcd m) * 0 are_congruent_mod m1 * (a gcd m) by Th10; then ((a * y) - b) mod m = 0 mod m by A3, A4, A6, NAT_D:64; hence ((a * y) - b) mod m = 0 by Th12; ::_thesis: verum end; begin theorem Th19: :: INT_4:19 for n, p, q being Nat st n > 0 & p > 0 holds (p * q) mod (p |^ n) = p * (q mod (p |^ (n -' 1))) proof let n, p, q be Nat; ::_thesis: ( n > 0 & p > 0 implies (p * q) mod (p |^ n) = p * (q mod (p |^ (n -' 1))) ) assume that A1: n > 0 and A2: p > 0 ; ::_thesis: (p * q) mod (p |^ n) = p * (q mod (p |^ (n -' 1))) A3: n >= 0 + 1 by A1, NAT_1:13; p * (q mod (p |^ (n -' 1))) = p * (q - ((q div (p |^ (n -' 1))) * (p |^ (n -' 1)))) by A2, NEWTON:63 .= (p * q) - ((q div (p |^ (n -' 1))) * (p * (p |^ (n -' 1)))) .= (p * q) - ((q div (p |^ (n -' 1))) * (p |^ ((n -' 1) + 1))) by NEWTON:6 .= (p * q) - ((q div (p |^ (n -' 1))) * (p |^ n)) by A3, XREAL_1:235 ; then A4: p * q = ((q div (p |^ (n -' 1))) * (p |^ n)) + (p * (q mod (p |^ (n -' 1)))) ; p * (q mod (p |^ (n -' 1))) < p * (p |^ (n -' 1)) by A2, NAT_D:1, XREAL_1:68; then p * (q mod (p |^ (n -' 1))) < p |^ ((n -' 1) + 1) by NEWTON:6; then p * (q mod (p |^ (n -' 1))) < p |^ n by A3, XREAL_1:235; hence (p * q) mod (p |^ n) = p * (q mod (p |^ (n -' 1))) by A4, NAT_D:def_2; ::_thesis: verum end; theorem :: INT_4:20 for p, q, n being Nat holds (p * q) mod (p * n) = p * (q mod n) proof let p, q, n be Nat; ::_thesis: (p * q) mod (p * n) = p * (q mod n) percases ( n = 0 or n > 0 ) ; supposeA1: n = 0 ; ::_thesis: (p * q) mod (p * n) = p * (q mod n) then q mod n = 0 by NAT_D:def_2; hence (p * q) mod (p * n) = p * (q mod n) by A1, NAT_D:def_2; ::_thesis: verum end; supposeA2: n > 0 ; ::_thesis: (p * q) mod (p * n) = p * (q mod n) then A3: p * q = p * ((n * (q div n)) + (q mod n)) by NAT_D:2 .= ((p * n) * (q div n)) + (p * (q mod n)) ; percases ( p = 0 or p > 0 ) ; suppose p = 0 ; ::_thesis: (p * q) mod (p * n) = p * (q mod n) hence (p * q) mod (p * n) = p * (q mod n) by NAT_D:def_2; ::_thesis: verum end; suppose p > 0 ; ::_thesis: (p * q) mod (p * n) = p * (q mod n) then p * (q mod n) < p * n by A2, NAT_D:1, XREAL_1:68; hence (p * q) mod (p * n) = p * (q mod n) by A3, NAT_D:def_2; ::_thesis: verum end; end; end; end; end; theorem Th21: :: INT_4:21 for n, p, q being Nat st n > 0 & p is prime & p,q are_relative_prime holds not p divides q mod (p |^ n) proof let n, p, q be Nat; ::_thesis: ( n > 0 & p is prime & p,q are_relative_prime implies not p divides q mod (p |^ n) ) assume that A1: n > 0 and A2: p is prime and A3: p,q are_relative_prime ; ::_thesis: not p divides q mod (p |^ n) n >= 0 + 1 by A1, NAT_1:13; then p |^ 1 divides p |^ n by NEWTON:89; then p divides p |^ n by NEWTON:5; then A4: p divides (p |^ n) * (q div (p |^ n)) by NAT_D:9; q = ((p |^ n) * (q div (p |^ n))) + (q mod (p |^ n)) by A2, NAT_D:2; hence not p divides q mod (p |^ n) by A2, A3, A4, Lm6, NAT_D:8; ::_thesis: verum end; theorem Th22: :: INT_4:22 for p, q, n being Nat st n > 0 holds ( (p - q) mod n = 0 iff p mod n = q mod n ) proof let p, q, n be Nat; ::_thesis: ( n > 0 implies ( (p - q) mod n = 0 iff p mod n = q mod n ) ) assume A1: n > 0 ; ::_thesis: ( (p - q) mod n = 0 iff p mod n = q mod n ) thus ( (p - q) mod n = 0 implies p mod n = q mod n ) ::_thesis: ( p mod n = q mod n implies (p - q) mod n = 0 ) proof assume (p - q) mod n = 0 ; ::_thesis: p mod n = q mod n then n divides p - q by A1, INT_1:62; then consider s being Integer such that A2: n * s = p - q by INT_1:def_3; percases ( p > q or p = q or p < q ) by XXREAL_0:1; suppose p > q ; ::_thesis: p mod n = q mod n then s > 0 by A2, XREAL_1:50; then s in NAT by INT_1:3; then reconsider s9 = s as Nat ; p mod n = ((n * s9) + q) mod n by A2 .= q mod n by NAT_D:21 ; hence p mod n = q mod n ; ::_thesis: verum end; suppose p = q ; ::_thesis: p mod n = q mod n hence p mod n = q mod n ; ::_thesis: verum end; supposeA3: p < q ; ::_thesis: p mod n = q mod n A4: q - p = n * (- s) by A2; then - s > 0 by A3, XREAL_1:50; then - s in NAT by INT_1:3; then reconsider s9 = - s as Nat ; q - p = n * s9 by A4; then q mod n = ((n * s9) + p) mod n .= p mod n by NAT_D:21 ; hence p mod n = q mod n ; ::_thesis: verum end; end; end; assume A5: p mod n = q mod n ; ::_thesis: (p - q) mod n = 0 p = (n * (p div n)) + (p mod n) by A1, NAT_D:2 .= (n * (p div n)) + (q - (n * (q div n))) by A1, A5, NEWTON:63 .= q + (n * ((p div n) - (q div n))) ; then n divides p - q by INT_1:def_3; hence (p - q) mod n = 0 by A1, INT_1:62; ::_thesis: verum end; theorem :: INT_4:23 for a, b, m being Nat st m > 0 holds ( a mod m = b mod m iff m divides a - b ) proof let a, b, m be Nat; ::_thesis: ( m > 0 implies ( a mod m = b mod m iff m divides a - b ) ) assume A1: m > 0 ; ::_thesis: ( a mod m = b mod m iff m divides a - b ) thus ( a mod m = b mod m implies m divides a - b ) ::_thesis: ( m divides a - b implies a mod m = b mod m ) proof assume a mod m = b mod m ; ::_thesis: m divides a - b then (a - b) mod m = 0 by A1, Th22; hence m divides a - b by A1, INT_1:62; ::_thesis: verum end; assume m divides a - b ; ::_thesis: a mod m = b mod m then (a - b) mod m = 0 by A1, INT_1:62; hence a mod m = b mod m by A1, Th22; ::_thesis: verum end; theorem :: INT_4:24 for n, p, q being Nat st n > 0 & p is prime & p,q are_relative_prime holds for x being Integer holds not ((p * (x ^2)) - q) mod (p |^ n) = 0 proof let n, p, q be Nat; ::_thesis: ( n > 0 & p is prime & p,q are_relative_prime implies for x being Integer holds not ((p * (x ^2)) - q) mod (p |^ n) = 0 ) assume that A1: n > 0 and A2: p is prime and A3: p,q are_relative_prime ; ::_thesis: for x being Integer holds not ((p * (x ^2)) - q) mod (p |^ n) = 0 given x being Integer such that A4: ((p * (x ^2)) - q) mod (p |^ n) = 0 ; ::_thesis: contradiction (p * (x ^2)) mod (p |^ n) = q mod (p |^ n) by A2, A4, Th22; then p * ((x ^2) mod (p |^ (n -' 1))) = q mod (p |^ n) by A1, A2, Th19; then p divides q mod (p |^ n) by NAT_D:def_3; hence contradiction by A1, A2, A3, Th21; ::_thesis: verum end; theorem :: INT_4:25 for n, p, q being Nat st n > 0 & p is prime & p,q are_relative_prime holds for x being Integer holds not ((p * x) - q) mod (p |^ n) = 0 proof let n, p, q be Nat; ::_thesis: ( n > 0 & p is prime & p,q are_relative_prime implies for x being Integer holds not ((p * x) - q) mod (p |^ n) = 0 ) assume that A1: n > 0 and A2: p is prime and A3: p,q are_relative_prime ; ::_thesis: for x being Integer holds not ((p * x) - q) mod (p |^ n) = 0 A4: p > 1 by A2, INT_2:def_4; given x being Integer such that A5: ((p * x) - q) mod (p |^ n) = 0 ; ::_thesis: contradiction percases ( x >= 0 or x < 0 ) ; suppose x >= 0 ; ::_thesis: contradiction then x in NAT by INT_1:3; then reconsider x = x as Nat ; (p * x) mod (p |^ n) = q mod (p |^ n) by A2, A5, Th22; then p * (x mod (p |^ (n -' 1))) = q mod (p |^ n) by A1, A2, Th19; then p divides q mod (p |^ n) by NAT_D:def_3; hence contradiction by A1, A2, A3, Th21; ::_thesis: verum end; suppose x < 0 ; ::_thesis: contradiction then - x in NAT by INT_1:3; then reconsider l = - x as Nat ; A6: p divides p * l by NAT_D:9; p |^ n divides (p * x) - q by A2, A5, INT_1:62; then p |^ n divides (- 1) * ((p * x) - q) by INT_2:2; then consider k being Integer such that A7: (p * l) + q = (p |^ n) * k by INT_1:def_3; k >= 0 by A2, A7, XREAL_1:132; then k in NAT by INT_1:3; then reconsider k = k as Nat ; (p * l) + q = (p |^ n) * k by A7; then A8: p |^ n divides (p * l) + q by NAT_D:def_3; p divides p |^ n by A1, NAT_3:3; then A9: p divides (p * l) + q by A8, NAT_D:4; reconsider p = p, q = q as Element of NAT by ORDINAL1:def_12; p gcd q > 1 by A4, A9, A6, NAT_D:10, NEWTON:49; hence contradiction by A3, INT_2:def_3; ::_thesis: verum end; end; end; begin definition let m be Integer; func Cong m -> Relation of INT means :Def1: :: INT_4:def 1 for x, y being Integer holds ( [x,y] in it iff x,y are_congruent_mod m ); existence ex b1 being Relation of INT st for x, y being Integer holds ( [x,y] in b1 iff x,y are_congruent_mod m ) proof defpred S1[ Element of INT , Element of INT ] means $1,$2 are_congruent_mod m; consider R being Relation of INT,INT such that A1: for x, y being Element of INT holds ( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2(); take R ; ::_thesis: for x, y being Integer holds ( [x,y] in R iff x,y are_congruent_mod m ) let x, y be Integer; ::_thesis: ( [x,y] in R iff x,y are_congruent_mod m ) for x, y being Integer holds ( [x,y] in R iff x,y are_congruent_mod m ) proof let x, y be Integer; ::_thesis: ( [x,y] in R iff x,y are_congruent_mod m ) reconsider x = x, y = y as Element of INT by INT_1:def_2; ( [x,y] in R iff S1[x,y] ) by A1; hence ( [x,y] in R iff x,y are_congruent_mod m ) ; ::_thesis: verum end; hence ( [x,y] in R iff x,y are_congruent_mod m ) ; ::_thesis: verum end; uniqueness for b1, b2 being Relation of INT st ( for x, y being Integer holds ( [x,y] in b1 iff x,y are_congruent_mod m ) ) & ( for x, y being Integer holds ( [x,y] in b2 iff x,y are_congruent_mod m ) ) holds b1 = b2 proof let P1, P2 be Relation of INT; ::_thesis: ( ( for x, y being Integer holds ( [x,y] in P1 iff x,y are_congruent_mod m ) ) & ( for x, y being Integer holds ( [x,y] in P2 iff x,y are_congruent_mod m ) ) implies P1 = P2 ) assume that A2: for x, y being Integer holds ( [x,y] in P1 iff x,y are_congruent_mod m ) and A3: for x, y being Integer holds ( [x,y] in P2 iff x,y are_congruent_mod m ) ; ::_thesis: P1 = P2 A4: for x, y being Integer holds ( [x,y] in P1 iff [x,y] in P2 ) proof let x, y be Integer; ::_thesis: ( [x,y] in P1 iff [x,y] in P2 ) ( [x,y] in P1 iff x,y are_congruent_mod m ) by A2; hence ( [x,y] in P1 iff [x,y] in P2 ) by A3; ::_thesis: verum end; thus P1 c= P2 :: according to XBOOLE_0:def_10 ::_thesis: P2 c= P1 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in P1 or a in P2 ) assume A5: a in P1 ; ::_thesis: a in P2 then consider x, y being set such that A6: a = [x,y] and A7: ( x in INT & y in INT ) by RELSET_1:2; reconsider x = x, y = y as Integer by A7; [x,y] in P2 by A4, A5, A6; hence a in P2 by A6; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in P2 or a in P1 ) assume A8: a in P2 ; ::_thesis: a in P1 then consider x, y being set such that A9: a = [x,y] and A10: ( x in INT & y in INT ) by RELSET_1:2; reconsider x = x, y = y as Integer by A10; [x,y] in P1 by A4, A8, A9; hence a in P1 by A9; ::_thesis: verum end; end; :: deftheorem Def1 defines Cong INT_4:def_1_:_ for m being Integer for b2 being Relation of INT holds ( b2 = Cong m iff for x, y being Integer holds ( [x,y] in b2 iff x,y are_congruent_mod m ) ); registration let m be Integer; cluster Cong m -> total ; coherence Cong m is total proof thus dom (Cong m) c= INT ; :: according to PARTFUN1:def_2,XBOOLE_0:def_10 ::_thesis: INT c= dom (Cong m) thus INT c= dom (Cong m) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in INT or x in dom (Cong m) ) assume x in INT ; ::_thesis: x in dom (Cong m) then reconsider x = x as Integer ; x,x are_congruent_mod m by INT_1:11; then [x,x] in Cong m by Def1; hence x in dom (Cong m) by XTUPLE_0:def_12; ::_thesis: verum end; end; end; Lm8: for m being Integer holds Cong m is Equivalence_Relation of INT proof let m be Integer; ::_thesis: Cong m is Equivalence_Relation of INT A1: Cong m is_symmetric_in INT proof let x, y be set ; :: according to RELAT_2:def_3 ::_thesis: ( not x in INT or not y in INT or not [x,y] in Cong m or [y,x] in Cong m ) assume that A2: x in INT and A3: y in INT and A4: [x,y] in Cong m ; ::_thesis: [y,x] in Cong m reconsider y = y as Integer by A3; reconsider x = x as Integer by A2; x,y are_congruent_mod m by A4, Def1; then y,x are_congruent_mod m by INT_1:14; hence [y,x] in Cong m by Def1; ::_thesis: verum end; A5: Cong m is_transitive_in INT proof let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in INT or not y in INT or not z in INT or not [x,y] in Cong m or not [y,z] in Cong m or [x,z] in Cong m ) assume that A6: ( x in INT & y in INT & z in INT ) and A7: ( [x,y] in Cong m & [y,z] in Cong m ) ; ::_thesis: [x,z] in Cong m reconsider x = x, y = y, z = z as Integer by A6; ( x,y are_congruent_mod m & y,z are_congruent_mod m ) by A7, Def1; then x,z are_congruent_mod m by INT_1:15; hence [x,z] in Cong m by Def1; ::_thesis: verum end; field (Cong m) = INT by ORDERS_1:12; hence Cong m is Equivalence_Relation of INT by A1, A5, RELAT_2:def_11, RELAT_2:def_16; ::_thesis: verum end; registration let m be Integer; cluster Cong m -> reflexive symmetric transitive ; coherence ( Cong m is reflexive & Cong m is symmetric & Cong m is transitive ) by Lm8; end; theorem Th26: :: INT_4:26 for m, a, x, b being Integer st m <> 0 & ((a * x) - b) mod m = 0 holds for y being Integer holds ( ( a,m are_relative_prime & ((a * y) - b) mod m = 0 implies y in Class ((Cong m),x) ) & ( y in Class ((Cong m),x) implies ((a * y) - b) mod m = 0 ) ) proof let m, a, x, b be Integer; ::_thesis: ( m <> 0 & ((a * x) - b) mod m = 0 implies for y being Integer holds ( ( a,m are_relative_prime & ((a * y) - b) mod m = 0 implies y in Class ((Cong m),x) ) & ( y in Class ((Cong m),x) implies ((a * y) - b) mod m = 0 ) ) ) assume that A1: m <> 0 and A2: ((a * x) - b) mod m = 0 ; ::_thesis: for y being Integer holds ( ( a,m are_relative_prime & ((a * y) - b) mod m = 0 implies y in Class ((Cong m),x) ) & ( y in Class ((Cong m),x) implies ((a * y) - b) mod m = 0 ) ) let y be Integer; ::_thesis: ( ( a,m are_relative_prime & ((a * y) - b) mod m = 0 implies y in Class ((Cong m),x) ) & ( y in Class ((Cong m),x) implies ((a * y) - b) mod m = 0 ) ) hereby ::_thesis: ( y in Class ((Cong m),x) implies ((a * y) - b) mod m = 0 ) assume that A3: a,m are_relative_prime and A4: ((a * y) - b) mod m = 0 ; ::_thesis: y in Class ((Cong m),x) (a * x) - b,(a * y) - b are_congruent_mod m by A1, A2, A4, NAT_D:64; then ((a * x) - b) + b,a * y are_congruent_mod m by INT_1:19; then x,y are_congruent_mod m by A3, Th9; then [x,y] in Cong m by Def1; hence y in Class ((Cong m),x) by EQREL_1:18; ::_thesis: verum end; assume y in Class ((Cong m),x) ; ::_thesis: ((a * y) - b) mod m = 0 then [x,y] in Cong m by EQREL_1:18; then x,y are_congruent_mod m by Def1; then A5: x * a,y * a are_congruent_mod m by Th11; ((a * x) - b) mod m = 0 mod m by A2, Th12; then 0 ,(a * x) - b are_congruent_mod m by A1, NAT_D:64; then 0 + b,a * x are_congruent_mod m by INT_1:19; then 0 + b,a * y are_congruent_mod m by A5, INT_1:15; then 0 ,(a * y) - b are_congruent_mod m by INT_1:19; then ((a * y) - b) mod m = 0 mod m by NAT_D:64; hence ((a * y) - b) mod m = 0 by Th12; ::_thesis: verum end; theorem :: INT_4:27 for a, b, m, x being Integer st m <> 0 & a,m are_relative_prime & ((a * x) - b) mod m = 0 holds ex s being Integer st [x,(b * s)] in Cong m proof let a, b, m, x be Integer; ::_thesis: ( m <> 0 & a,m are_relative_prime & ((a * x) - b) mod m = 0 implies ex s being Integer st [x,(b * s)] in Cong m ) assume that A1: m <> 0 and A2: a,m are_relative_prime and A3: ((a * x) - b) mod m = 0 ; ::_thesis: ex s being Integer st [x,(b * s)] in Cong m a gcd m = 1 by A2, INT_2:def_3; then consider r, t being Integer such that A4: 1 = (r * a) + (t * m) by NAT_D:68; ((a * x) - b) mod m = 0 mod m by A3, Th12; then (a * x) - b, 0 are_congruent_mod m by A1, NAT_D:64; then ((a * x) - b) * r,0 * r are_congruent_mod m by Th11; then (x * (a * r)) - (b * r), 0 are_congruent_mod m ; then A5: (x * (1 - (t * m))) - (b * r), 0 are_congruent_mod m by A4; take s = r; ::_thesis: [x,(b * s)] in Cong m ((x - ((x * t) * m)) - (b * r)) mod m = ((x - (b * r)) + (((- x) * t) * m)) mod m .= (x - (b * r)) mod m by NAT_D:61 ; then (x - (b * r)) mod m = 0 mod m by A5, NAT_D:64; then 0 ,x - (b * r) are_congruent_mod m by A1, NAT_D:64; then 0 + (b * r),x are_congruent_mod m by INT_1:19; then x,b * s are_congruent_mod m by INT_1:14; hence [x,(b * s)] in Cong m by Def1; ::_thesis: verum end; theorem :: INT_4:28 for a, m being Element of NAT st a <> 0 & m > 1 & a,m are_relative_prime holds for b, x being Integer st ((a * x) - b) mod m = 0 holds [x,(b * (a |^ ((Euler m) -' 1)))] in Cong m proof let a, m be Element of NAT ; ::_thesis: ( a <> 0 & m > 1 & a,m are_relative_prime implies for b, x being Integer st ((a * x) - b) mod m = 0 holds [x,(b * (a |^ ((Euler m) -' 1)))] in Cong m ) assume that A1: a <> 0 and A2: m > 1 and A3: a,m are_relative_prime ; ::_thesis: for b, x being Integer st ((a * x) - b) mod m = 0 holds [x,(b * (a |^ ((Euler m) -' 1)))] in Cong m let b, x be Integer; ::_thesis: ( ((a * x) - b) mod m = 0 implies [x,(b * (a |^ ((Euler m) -' 1)))] in Cong m ) (a |^ (Euler m)) mod m = 1 by A1, A2, A3, EULER_2:18; then a |^ (Euler m) = (m * ((a |^ (Euler m)) div m)) + 1 by A2, NAT_D:2; then m divides (a |^ (Euler m)) - 1 by INT_1:def_3; then a |^ (Euler m),1 are_congruent_mod m by INT_2:15; then A4: (a |^ (Euler m)) * x,1 * x are_congruent_mod m by Th11; Euler m <> 0 proof set X = { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ; 1 gcd m = 1 by NEWTON:51; then m,1 are_relative_prime by INT_2:def_3; then A5: 1 in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } by A2; assume Euler m = 0 ; ::_thesis: contradiction hence contradiction by A5; ::_thesis: verum end; then A6: ((Euler m) -' 1) + 1 = ((Euler m) - 1) + 1 by NAT_1:14, XREAL_1:233 .= Euler m ; assume ((a * x) - b) mod m = 0 ; ::_thesis: [x,(b * (a |^ ((Euler m) -' 1)))] in Cong m then m divides ((a * x) - b) - 0 by A2, INT_1:62; then (a * x) - b, 0 are_congruent_mod m by INT_2:15; then 0 ,(a * x) - b are_congruent_mod m by INT_1:14; then (a |^ ((Euler m) -' 1)) * 0,(a |^ ((Euler m) -' 1)) * ((a * x) - b) are_congruent_mod m by Th11; then 0 ,(((a |^ ((Euler m) -' 1)) * a) * x) - ((a |^ ((Euler m) -' 1)) * b) are_congruent_mod m ; then 0 ,((a |^ (((Euler m) -' 1) + 1)) * x) - ((a |^ ((Euler m) -' 1)) * b) are_congruent_mod m by NEWTON:6; then 0 + ((a |^ ((Euler m) -' 1)) * b),(a |^ (Euler m)) * x are_congruent_mod m by A6, INT_1:19; then (a |^ ((Euler m) -' 1)) * b,x are_congruent_mod m by A4, INT_1:15; then x,b * (a |^ ((Euler m) -' 1)) are_congruent_mod m by INT_1:14; hence [x,(b * (a |^ ((Euler m) -' 1)))] in Cong m by Def1; ::_thesis: verum end; theorem :: INT_4:29 for m, a, b being Integer st m <> 0 & a gcd m divides b holds ex fp being FinSequence of INT st ( len fp = a gcd m & ( for c being Element of NAT st c in dom fp holds ((a * (fp . c)) - b) mod m = 0 ) & ( for c1, c2 being Element of NAT st c1 in dom fp & c2 in dom fp & c1 <> c2 holds not fp . c1,fp . c2 are_congruent_mod m ) ) proof let m, a, b be Integer; ::_thesis: ( m <> 0 & a gcd m divides b implies ex fp being FinSequence of INT st ( len fp = a gcd m & ( for c being Element of NAT st c in dom fp holds ((a * (fp . c)) - b) mod m = 0 ) & ( for c1, c2 being Element of NAT st c1 in dom fp & c2 in dom fp & c1 <> c2 holds not fp . c1,fp . c2 are_congruent_mod m ) ) ) assume that A1: m <> 0 and A2: a gcd m divides b ; ::_thesis: ex fp being FinSequence of INT st ( len fp = a gcd m & ( for c being Element of NAT st c in dom fp holds ((a * (fp . c)) - b) mod m = 0 ) & ( for c1, c2 being Element of NAT st c1 in dom fp & c2 in dom fp & c1 <> c2 holds not fp . c1,fp . c2 are_congruent_mod m ) ) set l = a gcd m; reconsider l = a gcd m as Element of NAT by ORDINAL1:def_12; consider a1, m1 being Integer such that A3: a = l * a1 and A4: m = l * m1 and A5: a1,m1 are_relative_prime by A1, INT_2:23; consider b1 being Integer such that A6: b = l * b1 by A2, INT_1:def_3; consider x1 being Integer such that A7: ((a1 * x1) - b1) mod m1 = 0 by A5, Th15; deffunc H1( Nat) -> Element of REAL = x1 + (($1 - 1) * m1); consider fp being FinSequence such that A8: ( len fp = l & ( for c being Nat st c in dom fp holds fp . c = H1(c) ) ) from FINSEQ_1:sch_2(); for c being Nat st c in dom fp holds fp . c in INT proof let c be Nat; ::_thesis: ( c in dom fp implies fp . c in INT ) assume c in dom fp ; ::_thesis: fp . c in INT then fp . c = x1 + ((c - 1) * m1) by A8; hence fp . c in INT by INT_1:def_2; ::_thesis: verum end; then reconsider fp = fp as FinSequence of INT by FINSEQ_2:12; A9: m1 <> 0 by A1, A4; A10: for c1, c2 being Element of NAT st c1 in dom fp & c2 in dom fp & c1 <> c2 holds not fp . c1,fp . c2 are_congruent_mod m proof let c1, c2 be Element of NAT ; ::_thesis: ( c1 in dom fp & c2 in dom fp & c1 <> c2 implies not fp . c1,fp . c2 are_congruent_mod m ) assume that A11: c1 in dom fp and A12: c2 in dom fp and A13: c1 <> c2 ; ::_thesis: not fp . c1,fp . c2 are_congruent_mod m assume A14: fp . c1,fp . c2 are_congruent_mod m ; ::_thesis: contradiction ( fp . c1 = x1 + ((c1 - 1) * m1) & fp . c2 = x1 + ((c2 - 1) * m1) ) by A8, A11, A12; then m divides (((c1 - 1) * m1) + x1) - (((c2 - 1) * m1) + x1) by A14, INT_2:15; then consider w being Integer such that A15: (c1 - c2) * m1 = (l * m1) * w by A4, INT_1:def_3; (c1 - c2) * m1 = (l * w) * m1 by A15; then c1 - c2 = l * w by A9, XCMPLX_1:5; then A16: l divides c1 - c2 by INT_1:def_3; A17: c2 in Seg l by A8, A12, FINSEQ_1:def_3; then A18: c2 >= 1 by FINSEQ_1:1; A19: c1 in Seg l by A8, A11, FINSEQ_1:def_3; then c1 <= l by FINSEQ_1:1; then c1 - c2 <= l - 1 by A18, XREAL_1:13; then A20: c1 - c2 < l by XREAL_1:147; A21: c2 <= l by A17, FINSEQ_1:1; c1 >= 1 by A19, FINSEQ_1:1; then c1 - c2 >= 1 - l by A21, XREAL_1:13; then c1 - c2 > - l by XREAL_1:145; then A22: abs (c1 - c2) < l by A20, SEQ_2:1; c1 - c2 <> 0 by A13; then abs l <= abs (c1 - c2) by A16, Th6; hence contradiction by A22, ABSVALUE:def_1; ::_thesis: verum end; take fp ; ::_thesis: ( len fp = a gcd m & ( for c being Element of NAT st c in dom fp holds ((a * (fp . c)) - b) mod m = 0 ) & ( for c1, c2 being Element of NAT st c1 in dom fp & c2 in dom fp & c1 <> c2 holds not fp . c1,fp . c2 are_congruent_mod m ) ) ((a1 * x1) - b1) mod m1 = 0 mod m1 by A7, Th12; then (a1 * x1) - b1, 0 are_congruent_mod m1 by A9, NAT_D:64; then ((a1 * x1) - b1) * l,0 * l are_congruent_mod m1 * l by Th10; then A23: ((a * x1) - b) mod m = 0 mod m by A3, A4, A6, NAT_D:64; for c being Element of NAT st c in dom fp holds ((a * (fp . c)) - b) mod m = 0 proof let c be Element of NAT ; ::_thesis: ( c in dom fp implies ((a * (fp . c)) - b) mod m = 0 ) assume c in dom fp ; ::_thesis: ((a * (fp . c)) - b) mod m = 0 hence ((a * (fp . c)) - b) mod m = ((a * (x1 + ((c - 1) * m1))) - b) mod m by A8 .= (((a * x1) - b) + ((a1 * (c - 1)) * m)) mod m by A3, A4 .= ((a * x1) - b) mod m by NAT_D:61 .= 0 by A23, Th12 ; ::_thesis: verum end; hence ( len fp = a gcd m & ( for c being Element of NAT st c in dom fp holds ((a * (fp . c)) - b) mod m = 0 ) & ( for c1, c2 being Element of NAT st c1 in dom fp & c2 in dom fp & c1 <> c2 holds not fp . c1,fp . c2 are_congruent_mod m ) ) by A8, A10; ::_thesis: verum end; begin theorem Th30: :: INT_4:30 for fp being FinSequence of NAT for d, b, n being Element of NAT st b in dom fp & len fp = n + 1 holds Del ((fp ^ <*d*>),b) = (Del (fp,b)) ^ <*d*> proof let fp be FinSequence of NAT ; ::_thesis: for d, b, n being Element of NAT st b in dom fp & len fp = n + 1 holds Del ((fp ^ <*d*>),b) = (Del (fp,b)) ^ <*d*> let d, b, n be Element of NAT ; ::_thesis: ( b in dom fp & len fp = n + 1 implies Del ((fp ^ <*d*>),b) = (Del (fp,b)) ^ <*d*> ) assume that A1: b in dom fp and A2: len fp = n + 1 ; ::_thesis: Del ((fp ^ <*d*>),b) = (Del (fp,b)) ^ <*d*> A3: len (Del (fp,b)) = n by A1, A2, FINSEQ_3:109; then A4: len ((Del (fp,b)) ^ <*d*>) = n + 1 by FINSEQ_2:16; A5: ( len (fp ^ <*d*>) = (n + 1) + 1 & b in dom (fp ^ <*d*>) ) by A1, A2, FINSEQ_2:16, FINSEQ_3:22; then A6: len (Del ((fp ^ <*d*>),b)) = len ((Del (fp,b)) ^ <*d*>) by A4, FINSEQ_3:109; for k being Nat st 1 <= k & k <= len (Del ((fp ^ <*d*>),b)) holds (Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len (Del ((fp ^ <*d*>),b)) implies (Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . k ) assume that A7: 1 <= k and A8: k <= len (Del ((fp ^ <*d*>),b)) ; ::_thesis: (Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . k A9: k in dom fp by A2, A4, A6, A7, A8, FINSEQ_3:25; percases ( k < b or b <= k ) ; supposeA10: k < b ; ::_thesis: (Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . k b <= n + 1 by A1, A2, FINSEQ_3:25; then k < n + 1 by A10, XXREAL_0:2; then k <= n by NAT_1:13; then k in dom (Del (fp,b)) by A3, A7, FINSEQ_3:25; then A11: ((Del (fp,b)) ^ <*d*>) . k = (Del (fp,b)) . k by FINSEQ_1:def_7 .= fp . k by A10, FINSEQ_3:110 ; set fpd = fp ^ <*d*>; (Del ((fp ^ <*d*>),b)) . k = (fp ^ <*d*>) . k by A10, FINSEQ_3:110 .= fp . k by A9, FINSEQ_1:def_7 ; hence (Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . k by A11; ::_thesis: verum end; supposeA12: b <= k ; ::_thesis: (Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . k then A13: (Del ((fp ^ <*d*>),b)) . k = (fp ^ <*d*>) . (k + 1) by A4, A5, A6, A8, FINSEQ_3:111; percases ( k <= n or k = n + 1 ) by A4, A6, A8, NAT_1:8; supposeA14: k <= n ; ::_thesis: (Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . k then k in dom (Del (fp,b)) by A3, A7, FINSEQ_3:25; then A15: ((Del (fp,b)) ^ <*d*>) . k = (Del (fp,b)) . k by FINSEQ_1:def_7 .= fp . (k + 1) by A1, A2, A12, A14, FINSEQ_3:111 ; A16: k + 1 >= 1 by NAT_1:11; k + 1 <= n + 1 by A14, XREAL_1:6; then k + 1 in dom fp by A2, A16, FINSEQ_3:25; hence (Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . k by A13, A15, FINSEQ_1:def_7; ::_thesis: verum end; supposeA17: k = n + 1 ; ::_thesis: (Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . k then (Del ((fp ^ <*d*>),b)) . k = d by A2, A13, FINSEQ_1:42; hence (Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . k by A3, A17, FINSEQ_1:42; ::_thesis: verum end; end; end; end; end; hence Del ((fp ^ <*d*>),b) = (Del (fp,b)) ^ <*d*> by A4, A5, FINSEQ_1:14, FINSEQ_3:109; ::_thesis: verum end; theorem Th31: :: INT_4:31 for fp being FinSequence of NAT st len fp >= 2 & ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 ) holds for b being Element of NAT st b in dom fp holds (Product (Del (fp,b))) gcd (fp . b) = 1 proof let fp be FinSequence of NAT ; ::_thesis: ( len fp >= 2 & ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 ) implies for b being Element of NAT st b in dom fp holds (Product (Del (fp,b))) gcd (fp . b) = 1 ) defpred S1[ FinSequence of NAT ] means for b being Element of NAT st b in dom $1 holds (Product (Del ($1,b))) gcd ($1 . b) = 1; defpred S2[ FinSequence of NAT ] means for b, c being Element of NAT st b in dom $1 & c in dom $1 & b <> c holds ($1 . b) gcd ($1 . c) = 1; defpred S3[ set ] means ex f being FinSequence of NAT st ( f = $1 & ( len f >= 2 & S2[f] implies S1[f] ) ); A1: now__::_thesis:_for_fp_being_FinSequence_of_NAT_ for_d_being_Element_of_NAT_st_S3[fp]_holds_ S3[fp_^_<*d*>] let fp be FinSequence of NAT ; ::_thesis: for d being Element of NAT st S3[fp] holds S3[fp ^ <*d*>] let d be Element of NAT ; ::_thesis: ( S3[fp] implies S3[fp ^ <*d*>] ) assume A2: S3[fp] ; ::_thesis: S3[fp ^ <*d*>] set k = len fp; set fp1 = fp ^ <*d*>; now__::_thesis:_(_len_(fp_^_<*d*>)_>=_2_&_S2[fp_^_<*d*>]_implies_S1[fp_^_<*d*>]_) assume that A3: len (fp ^ <*d*>) >= 2 and A4: S2[fp ^ <*d*>] ; ::_thesis: S1[fp ^ <*d*>] A5: len (fp ^ <*d*>) = (len fp) + 1 by FINSEQ_2:16; now__::_thesis:_S1[fp_^_<*d*>] percases ( len (fp ^ <*d*>) = 2 or len (fp ^ <*d*>) > 2 ) by A3, XXREAL_0:1; supposeA6: len (fp ^ <*d*>) = 2 ; ::_thesis: S1[fp ^ <*d*>] then ( 1 in dom (fp ^ <*d*>) & 2 in dom (fp ^ <*d*>) ) by FINSEQ_3:25; then A7: ((fp ^ <*d*>) . 2) gcd ((fp ^ <*d*>) . 1) = 1 by A4; A8: fp ^ <*d*> = <*((fp ^ <*d*>) . 1),((fp ^ <*d*>) . 2)*> by A6, FINSEQ_1:44; for b being Element of NAT st b in dom (fp ^ <*d*>) holds (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1 proof let b be Element of NAT ; ::_thesis: ( b in dom (fp ^ <*d*>) implies (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1 ) assume b in dom (fp ^ <*d*>) ; ::_thesis: (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1 then A9: b in Seg (len (fp ^ <*d*>)) by FINSEQ_1:def_3; percases ( b = 1 or b = 2 ) by A6, A9, FINSEQ_1:2, TARSKI:def_2; suppose b = 1 ; ::_thesis: (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1 hence (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = (Product <*((fp ^ <*d*>) . 2)*>) gcd ((fp ^ <*d*>) . 1) by A8, WSIERP_1:19 .= 1 by A7, RVSUM_1:95 ; ::_thesis: verum end; suppose b = 2 ; ::_thesis: (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1 hence (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = (Product <*((fp ^ <*d*>) . 1)*>) gcd ((fp ^ <*d*>) . 2) by A8, WSIERP_1:19 .= 1 by A7, RVSUM_1:95 ; ::_thesis: verum end; end; end; hence S1[fp ^ <*d*>] ; ::_thesis: verum end; suppose len (fp ^ <*d*>) > 2 ; ::_thesis: S1[fp ^ <*d*>] then A10: (len fp) + 1 > 1 + 1 by FINSEQ_2:16; then len fp >= 1 + 1 by NAT_1:13; then consider n being Nat such that A11: len fp = n + 1 by NAT_1:6; A12: S2[fp] proof A13: dom fp c= dom (fp ^ <*d*>) by FINSEQ_1:26; let b, c be Element of NAT ; ::_thesis: ( b in dom fp & c in dom fp & b <> c implies (fp . b) gcd (fp . c) = 1 ) assume that A14: ( b in dom fp & c in dom fp ) and A15: b <> c ; ::_thesis: (fp . b) gcd (fp . c) = 1 ( (fp ^ <*d*>) . b = fp . b & (fp ^ <*d*>) . c = fp . c ) by A14, FINSEQ_1:def_7; hence (fp . b) gcd (fp . c) = 1 by A4, A14, A15, A13; ::_thesis: verum end; A16: for a being Nat st a in dom fp holds (fp . a) gcd d = 1 proof let a be Nat; ::_thesis: ( a in dom fp implies (fp . a) gcd d = 1 ) A17: (len fp) + 1 in dom (fp ^ <*d*>) by A5, FINSEQ_5:6; A18: ( dom fp c= dom (fp ^ <*d*>) & (fp ^ <*d*>) . ((len fp) + 1) = d ) by FINSEQ_1:26, FINSEQ_1:42; assume A19: a in dom fp ; ::_thesis: (fp . a) gcd d = 1 (len fp) + 1 > len fp by NAT_1:13; then A20: (len fp) + 1 <> a by A19, FINSEQ_3:25; (fp ^ <*d*>) . a = fp . a by A19, FINSEQ_1:def_7; hence (fp . a) gcd d = 1 by A4, A19, A18, A20, A17; ::_thesis: verum end; reconsider n = n as Element of NAT by ORDINAL1:def_12; A21: len fp = n + 1 by A11; for b being Element of NAT st b in dom (fp ^ <*d*>) holds (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1 proof let b be Element of NAT ; ::_thesis: ( b in dom (fp ^ <*d*>) implies (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1 ) assume A22: b in dom (fp ^ <*d*>) ; ::_thesis: (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1 A23: b >= 1 by A22, FINSEQ_3:25; A24: b <= (len fp) + 1 by A5, A22, FINSEQ_3:25; percases ( b <= len fp or b = (len fp) + 1 ) by A24, NAT_1:8; suppose b <= len fp ; ::_thesis: (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1 then A25: b in dom fp by A23, FINSEQ_3:25; then ( (Product (Del (fp,b))) gcd (fp . b) = 1 & (fp . b) gcd d = 1 ) by A2, A10, A12, A16, NAT_1:13; then ((Product (Del (fp,b))) * d) gcd (fp . b) = 1 by WSIERP_1:7; then A26: (Product ((Del (fp,b)) ^ <*d*>)) gcd (fp . b) = 1 by RVSUM_1:96; Del ((fp ^ <*d*>),b) = (Del (fp,b)) ^ <*d*> by A21, A25, Th30; hence (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1 by A25, A26, FINSEQ_1:def_7; ::_thesis: verum end; suppose b = (len fp) + 1 ; ::_thesis: (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1 hence (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = (Product (Del ((fp ^ <*d*>),((len fp) + 1)))) gcd d by FINSEQ_1:42 .= (Product fp) gcd d by WSIERP_1:40 .= 1 by A16, WSIERP_1:36 ; ::_thesis: verum end; end; end; hence S1[fp ^ <*d*>] ; ::_thesis: verum end; end; end; hence S1[fp ^ <*d*>] ; ::_thesis: verum end; hence S3[fp ^ <*d*>] ; ::_thesis: verum end; A27: S3[ <*> NAT] proof take <*> NAT ; ::_thesis: ( <*> NAT = <*> NAT & ( len (<*> NAT) >= 2 & S2[ <*> NAT] implies S1[ <*> NAT] ) ) thus ( <*> NAT = <*> NAT & ( len (<*> NAT) >= 2 & S2[ <*> NAT] implies S1[ <*> NAT] ) ) ; ::_thesis: verum end; for fp being FinSequence of NAT holds S3[fp] from FINSEQ_2:sch_2(A27, A1); then ex f being FinSequence of NAT st ( f = fp & ( len f >= 2 & S2[f] implies S1[f] ) ) ; hence ( len fp >= 2 & ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 ) implies for b being Element of NAT st b in dom fp holds (Product (Del (fp,b))) gcd (fp . b) = 1 ) ; ::_thesis: verum end; theorem Th32: :: INT_4:32 for fp being FinSequence of NAT for a being Nat st a in dom fp holds fp . a divides Product fp proof let fp be FinSequence of NAT ; ::_thesis: for a being Nat st a in dom fp holds fp . a divides Product fp let a be Nat; ::_thesis: ( a in dom fp implies fp . a divides Product fp ) assume a in dom fp ; ::_thesis: fp . a divides Product fp then fp . a in rng fp by FUNCT_1:3; hence fp . a divides Product fp by NAT_3:7; ::_thesis: verum end; theorem :: INT_4:33 for p being Nat for fp being FinSequence of NAT for a being Nat st a in dom fp & p divides fp . a holds p divides Product fp proof let p be Nat; ::_thesis: for fp being FinSequence of NAT for a being Nat st a in dom fp & p divides fp . a holds p divides Product fp let fp be FinSequence of NAT ; ::_thesis: for a being Nat st a in dom fp & p divides fp . a holds p divides Product fp let a be Nat; ::_thesis: ( a in dom fp & p divides fp . a implies p divides Product fp ) assume that A1: a in dom fp and A2: p divides fp . a ; ::_thesis: p divides Product fp fp . a divides Product fp by A1, Th32; hence p divides Product fp by A2, NAT_D:4; ::_thesis: verum end; theorem :: INT_4:34 for fp being FinSequence of NAT for n being Element of NAT for a being Nat st len fp = n + 1 & a >= 1 & a <= n holds (Del (fp,a)) . n = fp . (len fp) proof let fp be FinSequence of NAT ; ::_thesis: for n being Element of NAT for a being Nat st len fp = n + 1 & a >= 1 & a <= n holds (Del (fp,a)) . n = fp . (len fp) let n be Element of NAT ; ::_thesis: for a being Nat st len fp = n + 1 & a >= 1 & a <= n holds (Del (fp,a)) . n = fp . (len fp) let a be Nat; ::_thesis: ( len fp = n + 1 & a >= 1 & a <= n implies (Del (fp,a)) . n = fp . (len fp) ) assume that A1: len fp = n + 1 and A2: a >= 1 and A3: a <= n ; ::_thesis: (Del (fp,a)) . n = fp . (len fp) n < n + 1 by XREAL_1:29; then a < n + 1 by A3, XXREAL_0:2; then a in dom fp by A1, A2, FINSEQ_3:25; hence (Del (fp,a)) . n = fp . (len fp) by A1, A3, WSIERP_1:def_1; ::_thesis: verum end; theorem Th35: :: INT_4:35 for fp being FinSequence of NAT for a being Nat for b being Element of NAT st a in dom fp & b in dom fp & a <> b & len fp >= 1 holds fp . b divides Product (Del (fp,a)) proof let fp be FinSequence of NAT ; ::_thesis: for a being Nat for b being Element of NAT st a in dom fp & b in dom fp & a <> b & len fp >= 1 holds fp . b divides Product (Del (fp,a)) let a be Nat; ::_thesis: for b being Element of NAT st a in dom fp & b in dom fp & a <> b & len fp >= 1 holds fp . b divides Product (Del (fp,a)) let b be Element of NAT ; ::_thesis: ( a in dom fp & b in dom fp & a <> b & len fp >= 1 implies fp . b divides Product (Del (fp,a)) ) assume that A1: a in dom fp and A2: b in dom fp and A3: a <> b and A4: len fp >= 1 ; ::_thesis: fp . b divides Product (Del (fp,a)) consider n being Nat such that A5: len fp = n + 1 by A4, NAT_1:6; A6: a <= n + 1 by A1, A5, FINSEQ_3:25; A7: a >= 1 by A1, FINSEQ_3:25; A8: b >= 1 by A2, FINSEQ_3:25; A9: (len (Del (fp,a))) + 1 = n + 1 by A1, A5, WSIERP_1:def_1; A10: b <= n + 1 by A2, A5, FINSEQ_3:25; percases ( a <= n or a = n + 1 ) by A6, NAT_1:8; supposeA11: a <= n ; ::_thesis: fp . b divides Product (Del (fp,a)) percases ( b < a or a < b ) by A3, XXREAL_0:1; supposeA12: b < a ; ::_thesis: fp . b divides Product (Del (fp,a)) then b <= n by A11, XXREAL_0:2; then A13: b in dom (Del (fp,a)) by A8, A9, FINSEQ_3:25; (Del (fp,a)) . b = fp . b by A1, A12, WSIERP_1:def_1; hence fp . b divides Product (Del (fp,a)) by A13, Th32; ::_thesis: verum end; supposeA14: a < b ; ::_thesis: fp . b divides Product (Del (fp,a)) then b >= a + 1 by NAT_1:13; then b - 1 >= a by XREAL_1:19; then b -' 1 >= a by A8, XREAL_1:233; then A15: (Del (fp,a)) . (b -' 1) = fp . ((b -' 1) + 1) by A1, WSIERP_1:def_1; b > 1 by A7, A14, XXREAL_0:2; then b - 1 > 0 by XREAL_1:50; then b -' 1 > 0 by A8, XREAL_1:233; then A16: b -' 1 >= 1 by Lm7; b - 1 <= (n + 1) - 1 by A10, XREAL_1:9; then b -' 1 <= n by A8, XREAL_1:233; then b -' 1 in dom (Del (fp,a)) by A9, A16, FINSEQ_3:25; then (Del (fp,a)) . (b -' 1) divides Product (Del (fp,a)) by Th32; hence fp . b divides Product (Del (fp,a)) by A8, A15, XREAL_1:235; ::_thesis: verum end; end; end; supposeA17: a = n + 1 ; ::_thesis: fp . b divides Product (Del (fp,a)) then b < n + 1 by A3, A10, XXREAL_0:1; then b <= n by NAT_1:13; then A18: b in dom (Del (fp,a)) by A8, A9, FINSEQ_3:25; b < a by A3, A10, A17, XXREAL_0:1; then (Del (fp,a)) . b = fp . b by A1, WSIERP_1:def_1; hence fp . b divides Product (Del (fp,a)) by A18, Th32; ::_thesis: verum end; end; end; Lm9: for i1, i2 being Integer for n being Nat st n > 0 & i1 mod n = 0 holds (i1 * i2) mod n = 0 proof let i1, i2 be Integer; ::_thesis: for n being Nat st n > 0 & i1 mod n = 0 holds (i1 * i2) mod n = 0 let n be Nat; ::_thesis: ( n > 0 & i1 mod n = 0 implies (i1 * i2) mod n = 0 ) assume that A1: n > 0 and A2: i1 mod n = 0 ; ::_thesis: (i1 * i2) mod n = 0 n divides i1 by A1, A2, INT_1:62; then n divides i1 * i2 by INT_2:2; hence (i1 * i2) mod n = 0 by A1, INT_1:62; ::_thesis: verum end; theorem Th36: :: INT_4:36 for fp being FinSequence of NAT for a being Nat st ( for b being Nat st b in dom fp holds a divides fp . b ) holds a divides Sum fp proof let fp be FinSequence of NAT ; ::_thesis: for a being Nat st ( for b being Nat st b in dom fp holds a divides fp . b ) holds a divides Sum fp let a be Nat; ::_thesis: ( ( for b being Nat st b in dom fp holds a divides fp . b ) implies a divides Sum fp ) defpred S1[ FinSequence of NAT ] means for b being Nat st b in dom $1 holds a divides $1 . b; defpred S2[ FinSequence of NAT ] means a divides Sum $1; defpred S3[ set ] means ex f being FinSequence of NAT st ( f = $1 & ( S1[f] implies S2[f] ) ); A1: now__::_thesis:_for_fp_being_FinSequence_of_NAT_ for_d_being_Element_of_NAT_st_S3[fp]_holds_ S3[fp_^_<*d*>] let fp be FinSequence of NAT ; ::_thesis: for d being Element of NAT st S3[fp] holds S3[fp ^ <*d*>] let d be Element of NAT ; ::_thesis: ( S3[fp] implies S3[fp ^ <*d*>] ) assume A2: S3[fp] ; ::_thesis: S3[fp ^ <*d*>] set fp1 = fp ^ <*d*>; now__::_thesis:_(_S1[fp_^_<*d*>]_implies_S2[fp_^_<*d*>]_) assume A3: S1[fp ^ <*d*>] ; ::_thesis: S2[fp ^ <*d*>] A4: S1[fp] proof let b be Nat; ::_thesis: ( b in dom fp implies a divides fp . b ) assume A5: b in dom fp ; ::_thesis: a divides fp . b ( dom fp c= dom (fp ^ <*d*>) & (fp ^ <*d*>) . b = fp . b ) by A5, FINSEQ_1:26, FINSEQ_1:def_7; hence a divides fp . b by A3, A5; ::_thesis: verum end; len (fp ^ <*d*>) in dom (fp ^ <*d*>) by FINSEQ_5:6; then a divides (fp ^ <*d*>) . (len (fp ^ <*d*>)) by A3; then a divides (fp ^ <*d*>) . ((len fp) + 1) by FINSEQ_2:16; then a divides d by FINSEQ_1:42; then a divides (Sum fp) + d by A2, A4, NAT_D:8; hence S2[fp ^ <*d*>] by RVSUM_1:74; ::_thesis: verum end; hence S3[fp ^ <*d*>] ; ::_thesis: verum end; A6: S3[ <*> NAT] by NAT_D:6, RVSUM_1:72; for fp being FinSequence of NAT holds S3[fp] from FINSEQ_2:sch_2(A6, A1); then ex f being FinSequence of NAT st ( f = fp & ( S1[f] implies S2[f] ) ) ; hence ( ( for b being Nat st b in dom fp holds a divides fp . b ) implies a divides Sum fp ) ; ::_thesis: verum end; theorem :: INT_4:37 for fp being FinSequence of NAT st len fp >= 2 & ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds fp . b <> 0 ) holds for fp1 being FinSequence of NAT ex x being Integer st for b being Element of NAT st b in dom fp holds (x - (fp1 . b)) mod (fp . b) = 0 proof let fp be FinSequence of NAT ; ::_thesis: ( len fp >= 2 & ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds fp . b <> 0 ) implies for fp1 being FinSequence of NAT ex x being Integer st for b being Element of NAT st b in dom fp holds (x - (fp1 . b)) mod (fp . b) = 0 ) assume that A1: len fp >= 2 and A2: for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 and A3: for b being Element of NAT st b in dom fp holds fp . b <> 0 ; ::_thesis: for fp1 being FinSequence of NAT ex x being Integer st for b being Element of NAT st b in dom fp holds (x - (fp1 . b)) mod (fp . b) = 0 consider fp2 being FinSequence of NAT , q being Element of NAT such that A4: fp = fp2 ^ <*q*> by A1, FINSEQ_2:19; deffunc H1( Nat) -> set = { l where l is Element of NAT : (((Product (Del (fp,$1))) * l) - 1) mod (fp . $1) = 0 } ; defpred S1[ Nat, Nat] means $2 in H1($1); A5: for a being Nat st a in Seg (len fp) holds ex n being Element of NAT st S1[a,n] proof let a be Nat; ::_thesis: ( a in Seg (len fp) implies ex n being Element of NAT st S1[a,n] ) reconsider l = fp . a as Integer ; assume a in Seg (len fp) ; ::_thesis: ex n being Element of NAT st S1[a,n] then A6: a in dom fp by FINSEQ_1:def_3; then (Product (Del (fp,a))) gcd (fp . a) = 1 by A1, A2, Th31; then A7: Product (Del (fp,a)),l are_relative_prime by INT_2:def_3; l <> 0 by A3, A6; then consider n being Nat such that A8: (((Product (Del (fp,a))) * n) - 1) mod l = 0 by A7, Th16; reconsider n = n as Element of NAT by ORDINAL1:def_12; take n ; ::_thesis: S1[a,n] thus S1[a,n] by A8; ::_thesis: verum end; consider s being FinSequence of NAT such that A9: ( dom s = Seg (len fp) & ( for a being Nat st a in Seg (len fp) holds S1[a,s . a] ) ) from FINSEQ_1:sch_5(A5); let fp1 be FinSequence of NAT ; ::_thesis: ex x being Integer st for b being Element of NAT st b in dom fp holds (x - (fp1 . b)) mod (fp . b) = 0 set k = len fp2; deffunc H2( Nat) -> Element of REAL = ((Product (Del (fp,$1))) * (s . $1)) * (fp1 . $1); consider s1 being FinSequence such that A10: ( len s1 = (len fp2) + 1 & ( for a being Nat st a in dom s1 holds s1 . a = H2(a) ) ) from FINSEQ_1:sch_2(); for a being Nat st a in dom s1 holds s1 . a in NAT proof let a be Nat; ::_thesis: ( a in dom s1 implies s1 . a in NAT ) assume A11: a in dom s1 ; ::_thesis: s1 . a in NAT reconsider a = a as Element of NAT by ORDINAL1:def_12; s1 . a = ((Product (Del (fp,a))) * (s . a)) * (fp1 . a) by A10, A11; hence s1 . a in NAT by ORDINAL1:def_12; ::_thesis: verum end; then reconsider s1 = s1 as FinSequence of NAT by FINSEQ_2:12; set x = Sum s1; take Sum s1 ; ::_thesis: for b being Element of NAT st b in dom fp holds ((Sum s1) - (fp1 . b)) mod (fp . b) = 0 A12: len fp = (len fp2) + 1 by A4, FINSEQ_2:16; A13: for a being Nat for b being Element of NAT st a in dom fp & b in dom fp & a <> b holds fp . b divides s1 . a proof let a be Nat; ::_thesis: for b being Element of NAT st a in dom fp & b in dom fp & a <> b holds fp . b divides s1 . a let b be Element of NAT ; ::_thesis: ( a in dom fp & b in dom fp & a <> b implies fp . b divides s1 . a ) assume that A14: a in dom fp and A15: ( b in dom fp & a <> b ) ; ::_thesis: fp . b divides s1 . a len fp >= 1 by A1, XXREAL_0:2; then fp . b divides (Product (Del (fp,a))) * ((s . a) * (fp1 . a)) by A14, A15, Th35, NAT_D:9; then A16: fp . b divides ((Product (Del (fp,a))) * (s . a)) * (fp1 . a) ; a in dom s1 by A12, A10, A14, FINSEQ_3:29; hence fp . b divides s1 . a by A10, A16; ::_thesis: verum end; A17: for b being Element of NAT st b in dom fp holds fp . b divides Sum (Del (s1,b)) proof let b be Element of NAT ; ::_thesis: ( b in dom fp implies fp . b divides Sum (Del (s1,b)) ) assume A18: b in dom fp ; ::_thesis: fp . b divides Sum (Del (s1,b)) then b in Seg (len s1) by A12, A10, FINSEQ_1:def_3; then A19: b in dom s1 by FINSEQ_1:def_3; then A20: (len (Del (s1,b))) + 1 = (len fp2) + 1 by A10, WSIERP_1:def_1; for a being Nat st a in dom (Del (s1,b)) holds fp . b divides (Del (s1,b)) . a proof let a be Nat; ::_thesis: ( a in dom (Del (s1,b)) implies fp . b divides (Del (s1,b)) . a ) assume A21: a in dom (Del (s1,b)) ; ::_thesis: fp . b divides (Del (s1,b)) . a then A22: ( a >= 1 & a <= len fp2 ) by A20, FINSEQ_3:25; dom (Del (s1,b)) c= dom s1 by WSIERP_1:39; then a in dom s1 by A21; then a in Seg ((len fp2) + 1) by A10, FINSEQ_1:def_3; then A23: a in dom fp by A12, FINSEQ_1:def_3; percases ( a < b or a >= b ) ; supposeA24: a < b ; ::_thesis: fp . b divides (Del (s1,b)) . a then (Del (s1,b)) . a = s1 . a by A19, WSIERP_1:def_1; hence fp . b divides (Del (s1,b)) . a by A13, A18, A23, A24; ::_thesis: verum end; supposeA25: a >= b ; ::_thesis: fp . b divides (Del (s1,b)) . a ( a + 1 <= (len fp2) + 1 & a + 1 > 1 ) by A22, XREAL_1:6, XREAL_1:29; then A26: a + 1 in dom fp by A12, FINSEQ_3:25; ( (Del (s1,b)) . a = s1 . (a + 1) & a + 1 > b ) by A19, A25, WSIERP_1:def_1, XREAL_1:39; hence fp . b divides (Del (s1,b)) . a by A13, A18, A26; ::_thesis: verum end; end; end; hence fp . b divides Sum (Del (s1,b)) by Th36; ::_thesis: verum end; for b being Element of NAT st b in dom fp holds ((Sum s1) - (fp1 . b)) mod (fp . b) = 0 proof let b be Element of NAT ; ::_thesis: ( b in dom fp implies ((Sum s1) - (fp1 . b)) mod (fp . b) = 0 ) assume A27: b in dom fp ; ::_thesis: ((Sum s1) - (fp1 . b)) mod (fp . b) = 0 then A28: fp . b <> 0 by A3; A29: fp . b divides Sum (Del (s1,b)) by A17, A27; A30: ((Sum (Del (s1,b))) + ((s1 . b) - (fp1 . b))) mod (fp . b) = ((s1 . b) - (fp1 . b)) mod (fp . b) proof reconsider l = Sum (Del (s1,b)) as Integer ; A31: l mod (fp . b) = 0 by A29, A28, INT_1:62; ((Sum (Del (s1,b))) + ((s1 . b) - (fp1 . b))) mod (fp . b) = ((l mod (fp . b)) + (((s1 . b) - (fp1 . b)) mod (fp . b))) mod (fp . b) by NAT_D:66 .= ((s1 . b) - (fp1 . b)) mod (fp . b) by A31, NAT_D:65 ; hence ((Sum (Del (s1,b))) + ((s1 . b) - (fp1 . b))) mod (fp . b) = ((s1 . b) - (fp1 . b)) mod (fp . b) ; ::_thesis: verum end; A32: ( b >= 1 & b <= (len fp2) + 1 ) by A12, A27, FINSEQ_3:25; then A33: b in Seg ((len fp2) + 1) ; then b in dom s1 by A10, FINSEQ_1:def_3; then A34: (s1 . b) - (fp1 . b) = (((Product (Del (fp,b))) * (s . b)) * (fp1 . b)) - (1 * (fp1 . b)) by A10 .= (((Product (Del (fp,b))) * (s . b)) - 1) * (fp1 . b) ; s . b in H1(b) by A12, A9, A33; then A35: ex ll being Element of NAT st ( ll = s . b & (((Product (Del (fp,b))) * ll) - 1) mod (fp . b) = 0 ) ; b in dom s1 by A10, A32, FINSEQ_3:25; then ((Sum s1) - (fp1 . b)) mod (fp . b) = (((Sum (Del (s1,b))) + (s1 . b)) - (fp1 . b)) mod (fp . b) by WSIERP_1:20 .= 0 by A28, A34, A35, A30, Lm9 ; hence ((Sum s1) - (fp1 . b)) mod (fp . b) = 0 ; ::_thesis: verum end; hence for b being Element of NAT st b in dom fp holds ((Sum s1) - (fp1 . b)) mod (fp . b) = 0 ; ::_thesis: verum end; theorem Th38: :: INT_4:38 for fp being FinSequence of NAT for a being Nat st ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds fp . b divides a ) holds Product fp divides a proof let fp be FinSequence of NAT ; ::_thesis: for a being Nat st ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds fp . b divides a ) holds Product fp divides a let a be Nat; ::_thesis: ( ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds fp . b divides a ) implies Product fp divides a ) defpred S1[ FinSequence of NAT ] means ( ( for b, c being Element of NAT st b in dom $1 & c in dom $1 & b <> c holds ($1 . b) gcd ($1 . c) = 1 ) & ( for b being Element of NAT st b in dom $1 holds $1 . b divides a ) ); defpred S2[ FinSequence of NAT ] means Product $1 divides a; defpred S3[ set ] means ex f being FinSequence of NAT st ( f = $1 & ( S1[f] implies S2[f] ) ); A1: now__::_thesis:_for_fp_being_FinSequence_of_NAT_ for_d_being_Element_of_NAT_st_S3[fp]_holds_ S3[fp_^_<*d*>] let fp be FinSequence of NAT ; ::_thesis: for d being Element of NAT st S3[fp] holds S3[fp ^ <*d*>] let d be Element of NAT ; ::_thesis: ( S3[fp] implies S3[fp ^ <*d*>] ) assume A2: S3[fp] ; ::_thesis: S3[fp ^ <*d*>] set fp1 = fp ^ <*d*>; (len fp) + 1 >= 0 + 1 by XREAL_1:6; then A3: len (fp ^ <*d*>) >= 1 by FINSEQ_2:16; now__::_thesis:_(_S1[fp_^_<*d*>]_implies_S2[fp_^_<*d*>]_) assume A4: S1[fp ^ <*d*>] ; ::_thesis: S2[fp ^ <*d*>] for a being Nat st a in dom fp holds (fp . a) gcd d = 1 proof let a be Nat; ::_thesis: ( a in dom fp implies (fp . a) gcd d = 1 ) A5: len (fp ^ <*d*>) in dom (fp ^ <*d*>) by A3, FINSEQ_3:25; assume A6: a in dom fp ; ::_thesis: (fp . a) gcd d = 1 then a <= len fp by FINSEQ_3:25; then a < (len fp) + 1 by XREAL_1:39; then A7: a < len (fp ^ <*d*>) by FINSEQ_2:16; a in dom (fp ^ <*d*>) by A6, FINSEQ_2:15; then ((fp ^ <*d*>) . a) gcd ((fp ^ <*d*>) . (len (fp ^ <*d*>))) = 1 by A4, A7, A5; then A8: ((fp ^ <*d*>) . a) gcd ((fp ^ <*d*>) . ((len fp) + 1)) = 1 by FINSEQ_2:16; (fp ^ <*d*>) . a = fp . a by A6, FINSEQ_1:def_7; hence (fp . a) gcd d = 1 by A8, FINSEQ_1:42; ::_thesis: verum end; then (Product fp) gcd d = 1 by WSIERP_1:36; then A9: Product fp,d are_relative_prime by INT_2:def_3; A10: dom fp c= dom (fp ^ <*d*>) by FINSEQ_1:26; A11: for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 proof let b, c be Element of NAT ; ::_thesis: ( b in dom fp & c in dom fp & b <> c implies (fp . b) gcd (fp . c) = 1 ) assume that A12: ( b in dom fp & c in dom fp ) and A13: b <> c ; ::_thesis: (fp . b) gcd (fp . c) = 1 ( (fp ^ <*d*>) . b = fp . b & (fp ^ <*d*>) . c = fp . c ) by A12, FINSEQ_1:def_7; hence (fp . b) gcd (fp . c) = 1 by A4, A10, A12, A13; ::_thesis: verum end; A14: for b being Element of NAT st b in dom fp holds fp . b divides a proof let b be Element of NAT ; ::_thesis: ( b in dom fp implies fp . b divides a ) assume A15: b in dom fp ; ::_thesis: fp . b divides a then (fp ^ <*d*>) . b = fp . b by FINSEQ_1:def_7; hence fp . b divides a by A4, A10, A15; ::_thesis: verum end; len (fp ^ <*d*>) in dom (fp ^ <*d*>) by FINSEQ_5:6; then (fp ^ <*d*>) . (len (fp ^ <*d*>)) divides a by A4; then (fp ^ <*d*>) . ((len fp) + 1) divides a by FINSEQ_2:16; then d divides a by FINSEQ_1:42; then (Product fp) * d divides a by A2, A11, A14, A9, PEPIN:4; hence S2[fp ^ <*d*>] by RVSUM_1:96; ::_thesis: verum end; hence S3[fp ^ <*d*>] ; ::_thesis: verum end; A16: S3[ <*> NAT] proof take <*> NAT ; ::_thesis: ( <*> NAT = <*> NAT & ( S1[ <*> NAT] implies S2[ <*> NAT] ) ) thus ( <*> NAT = <*> NAT & ( S1[ <*> NAT] implies S2[ <*> NAT] ) ) by NAT_D:6, RVSUM_1:94; ::_thesis: verum end; for fp being FinSequence of NAT holds S3[fp] from FINSEQ_2:sch_2(A16, A1); then ex f being FinSequence of NAT st ( f = fp & ( S1[f] implies S2[f] ) ) ; hence ( ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds fp . b divides a ) implies Product fp divides a ) ; ::_thesis: verum end; theorem :: INT_4:39 for x, y being Integer for fp being FinSequence of NAT st ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds fp . b > 0 ) holds for fp1 being FinSequence of NAT st ( for b being Element of NAT st b in dom fp holds ( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) holds x,y are_congruent_mod Product fp proof let x, y be Integer; ::_thesis: for fp being FinSequence of NAT st ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds fp . b > 0 ) holds for fp1 being FinSequence of NAT st ( for b being Element of NAT st b in dom fp holds ( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) holds x,y are_congruent_mod Product fp let fp be FinSequence of NAT ; ::_thesis: ( ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds fp . b > 0 ) implies for fp1 being FinSequence of NAT st ( for b being Element of NAT st b in dom fp holds ( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) holds x,y are_congruent_mod Product fp ) assume that A1: for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 and A2: for b being Element of NAT st b in dom fp holds fp . b > 0 ; ::_thesis: for fp1 being FinSequence of NAT st ( for b being Element of NAT st b in dom fp holds ( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) holds x,y are_congruent_mod Product fp let fp1 be FinSequence of NAT ; ::_thesis: ( ( for b being Element of NAT st b in dom fp holds ( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) implies x,y are_congruent_mod Product fp ) assume A3: for b being Element of NAT st b in dom fp holds ( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ; ::_thesis: x,y are_congruent_mod Product fp percases ( x >= y or x < y ) ; suppose x >= y ; ::_thesis: x,y are_congruent_mod Product fp then x - y in NAT by INT_1:3, XREAL_1:48; then reconsider k = x - y as Nat ; for b being Element of NAT st b in dom fp holds fp . b divides k proof let b be Element of NAT ; ::_thesis: ( b in dom fp implies fp . b divides k ) assume A4: b in dom fp ; ::_thesis: fp . b divides k A5: fp . b > 0 by A2, A4; (y - (fp1 . b)) mod (fp . b) = 0 by A3, A4; then A6: fp . b divides y - (fp1 . b) by A5, INT_1:62; (x - (fp1 . b)) mod (fp . b) = 0 by A3, A4; then fp . b divides x - (fp1 . b) by A5, INT_1:62; then fp . b divides (x - (fp1 . b)) - (y - (fp1 . b)) by A6, Lm4; then consider i being Integer such that A7: x - y = (fp . b) * i by INT_1:def_3; i >= 0 proof assume i < 0 ; ::_thesis: contradiction then k < 0 by A2, A4, A7, XREAL_1:132; hence contradiction ; ::_thesis: verum end; then i in NAT by INT_1:3; then reconsider i = i as Nat ; i is Nat ; hence fp . b divides k by A7, NAT_D:def_3; ::_thesis: verum end; then Product fp divides k by A1, Th38; hence x,y are_congruent_mod Product fp by INT_2:15; ::_thesis: verum end; suppose x < y ; ::_thesis: x,y are_congruent_mod Product fp then y - x > 0 by XREAL_1:50; then y - x in NAT by INT_1:3; then reconsider k = y - x as Nat ; for b being Element of NAT st b in dom fp holds fp . b divides k proof let b be Element of NAT ; ::_thesis: ( b in dom fp implies fp . b divides k ) assume A8: b in dom fp ; ::_thesis: fp . b divides k A9: fp . b > 0 by A2, A8; (y - (fp1 . b)) mod (fp . b) = 0 by A3, A8; then A10: fp . b divides y - (fp1 . b) by A9, INT_1:62; (x - (fp1 . b)) mod (fp . b) = 0 by A3, A8; then fp . b divides x - (fp1 . b) by A9, INT_1:62; then fp . b divides (y - (fp1 . b)) - (x - (fp1 . b)) by A10, Lm4; then consider i being Integer such that A11: y - x = (fp . b) * i by INT_1:def_3; k = (fp . b) * i by A11; then i >= 0 by A2, A8, XREAL_1:132; then i in NAT by INT_1:3; then reconsider i = i as Nat ; i is Nat ; hence fp . b divides k by A11, NAT_D:def_3; ::_thesis: verum end; then Product fp divides k by A1, Th38; then y,x are_congruent_mod Product fp by INT_2:15; hence x,y are_congruent_mod Product fp by INT_1:14; ::_thesis: verum end; end; end; Lm10: for x, y being Integer holds ( ( x divides y implies y mod x = 0 ) & ( x <> 0 & y mod x = 0 implies x divides y ) ) proof let x, y be Integer; ::_thesis: ( ( x divides y implies y mod x = 0 ) & ( x <> 0 & y mod x = 0 implies x divides y ) ) A1: ( x divides y implies y mod x = 0 ) proof assume x divides y ; ::_thesis: y mod x = 0 then consider i being Integer such that A2: y = x * i by INT_1:def_3; y mod x = ((x * i) + 0) mod x by A2 .= 0 mod x by EULER_1:12 .= 0 by Th12 ; hence y mod x = 0 ; ::_thesis: verum end; ( x <> 0 & y mod x = 0 implies x divides y ) proof assume that A3: x <> 0 and A4: y mod x = 0 ; ::_thesis: x divides y y = ((y div x) * x) + (y mod x) by A3, INT_1:59 .= (y div x) * x by A4 ; hence x divides y by INT_1:def_3; ::_thesis: verum end; hence ( ( x divides y implies y mod x = 0 ) & ( x <> 0 & y mod x = 0 implies x divides y ) ) by A1; ::_thesis: verum end; Lm11: for x, y being Integer st x divides y holds y = (y div x) * x proof let x, y be Integer; ::_thesis: ( x divides y implies y = (y div x) * x ) assume A1: x divides y ; ::_thesis: y = (y div x) * x then A2: y mod x = 0 by Lm10; percases ( x = 0 or x <> 0 ) ; suppose x = 0 ; ::_thesis: y = (y div x) * x hence y = (y div x) * x by A1, INT_2:3; ::_thesis: verum end; suppose x <> 0 ; ::_thesis: y = (y div x) * x hence y = ((y div x) * x) + (y mod x) by INT_1:59 .= (y div x) * x by A2 ; ::_thesis: verum end; end; end; Lm12: for x, y being Integer st ( x <> 0 or y <> 0 ) holds x div (x gcd y),y div (x gcd y) are_relative_prime proof let x, y be Integer; ::_thesis: ( ( x <> 0 or y <> 0 ) implies x div (x gcd y),y div (x gcd y) are_relative_prime ) assume A1: ( x <> 0 or y <> 0 ) ; ::_thesis: x div (x gcd y),y div (x gcd y) are_relative_prime then A2: x gcd y <> 0 by INT_2:5; A3: y = (y div (x gcd y)) * (x gcd y) by Lm11, INT_2:21; consider a, b being Integer such that A4: x = (x gcd y) * a and A5: ( y = (x gcd y) * b & a,b are_relative_prime ) by A1, INT_2:23; x = (x div (x gcd y)) * (x gcd y) by Lm11, INT_2:21; then a = x div (x gcd y) by A2, A4, XCMPLX_1:5; hence x div (x gcd y),y div (x gcd y) are_relative_prime by A2, A3, A5, XCMPLX_1:5; ::_thesis: verum end; Lm13: for x, i, y being Integer st x divides i & y divides i & x,y are_relative_prime holds x * y divides i proof let x, i, y be Integer; ::_thesis: ( x divides i & y divides i & x,y are_relative_prime implies x * y divides i ) assume that A1: x divides i and A2: ( y divides i & x,y are_relative_prime ) ; ::_thesis: x * y divides i consider m being Integer such that A3: i = x * m by A1, INT_1:def_3; y divides m by A2, A3, INT_2:25; then consider r being Integer such that A4: m = y * r by INT_1:def_3; i = (x * y) * r by A3, A4; hence x * y divides i by INT_1:def_3; ::_thesis: verum end; theorem Th40: :: INT_4:40 for m1, m2, c1, c2 being Integer st m1 <> 0 & m2 <> 0 & m1,m2 are_relative_prime holds ex r being Integer st ( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds x,c1 + (m1 * r) are_congruent_mod m1 * m2 ) & ((m1 * r) - (c2 - c1)) mod m2 = 0 ) proof let m1, m2, c1, c2 be Integer; ::_thesis: ( m1 <> 0 & m2 <> 0 & m1,m2 are_relative_prime implies ex r being Integer st ( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds x,c1 + (m1 * r) are_congruent_mod m1 * m2 ) & ((m1 * r) - (c2 - c1)) mod m2 = 0 ) ) assume that A1: m1 <> 0 and A2: m2 <> 0 and A3: m1,m2 are_relative_prime ; ::_thesis: ex r being Integer st ( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds x,c1 + (m1 * r) are_congruent_mod m1 * m2 ) & ((m1 * r) - (c2 - c1)) mod m2 = 0 ) consider r being Integer such that A4: ((m1 * r) - (c2 - c1)) mod m2 = 0 by A3, Th15; take r ; ::_thesis: ( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds x,c1 + (m1 * r) are_congruent_mod m1 * m2 ) & ((m1 * r) - (c2 - c1)) mod m2 = 0 ) for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds x,c1 + (m1 * r) are_congruent_mod m1 * m2 proof let x be Integer; ::_thesis: ( (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 implies x,c1 + (m1 * r) are_congruent_mod m1 * m2 ) assume that A5: (x - c1) mod m1 = 0 and A6: (x - c2) mod m2 = 0 ; ::_thesis: x,c1 + (m1 * r) are_congruent_mod m1 * m2 set y = (x - c1) div m1; A7: x - c1 = (((x - c1) div m1) * m1) + ((x - c1) mod m1) by A1, INT_1:59 .= ((x - c1) div m1) * m1 by A5 ; then (x - c2) mod m2 = ((m1 * ((x - c1) div m1)) - (c2 - c1)) mod m2 ; then (x - c1) div m1 in Class ((Cong m2),r) by A2, A3, A4, A6, Th26; then [r,((x - c1) div m1)] in Cong m2 by EQREL_1:18; then r,(x - c1) div m1 are_congruent_mod m2 by Def1; then (x - c1) div m1,r are_congruent_mod m2 by INT_1:14; then m2 divides ((x - c1) div m1) - r by INT_2:15; then consider t being Integer such that A8: ((x - c1) div m1) - r = m2 * t by INT_1:def_3; x = c1 + (((x - c1) div m1) * m1) by A7 .= c1 + ((r + (m2 * t)) * m1) by A8 .= (c1 + (r * m1)) + ((m1 * m2) * t) ; then m1 * m2 divides x - (c1 + (r * m1)) by INT_2:2; hence x,c1 + (m1 * r) are_congruent_mod m1 * m2 by INT_2:15; ::_thesis: verum end; hence ( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds x,c1 + (m1 * r) are_congruent_mod m1 * m2 ) & ((m1 * r) - (c2 - c1)) mod m2 = 0 ) by A4; ::_thesis: verum end; theorem Th41: :: INT_4:41 for m1, m2, c1, c2 being Integer st m1 <> 0 & m2 <> 0 & not m1 gcd m2 divides c1 - c2 holds for x being Integer holds ( not (x - c1) mod m1 = 0 or not (x - c2) mod m2 = 0 ) proof let m1, m2, c1, c2 be Integer; ::_thesis: ( m1 <> 0 & m2 <> 0 & not m1 gcd m2 divides c1 - c2 implies for x being Integer holds ( not (x - c1) mod m1 = 0 or not (x - c2) mod m2 = 0 ) ) assume that A1: m1 <> 0 and A2: m2 <> 0 and A3: not m1 gcd m2 divides c1 - c2 ; ::_thesis: for x being Integer holds ( not (x - c1) mod m1 = 0 or not (x - c2) mod m2 = 0 ) A4: m1 gcd m2 divides m2 by INT_2:21; given x being Integer such that A5: (x - c1) mod m1 = 0 and A6: (x - c2) mod m2 = 0 ; ::_thesis: contradiction m2 divides x - c2 by A2, A6, Lm10; then A7: m1 gcd m2 divides x - c2 by A4, INT_2:9; A8: m1 gcd m2 divides m1 by INT_2:21; m1 divides x - c1 by A1, A5, Lm10; then m1 gcd m2 divides x - c1 by A8, INT_2:9; then m1 gcd m2 divides (x - c2) - (x - c1) by A7, Lm4; hence contradiction by A3; ::_thesis: verum end; theorem Th42: :: INT_4:42 for m1, m2, c2, c1 being Integer st m1 <> 0 & m2 <> 0 & m1 gcd m2 divides c2 - c1 holds ex r being Integer st ( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 ) proof let m1, m2, c2, c1 be Integer; ::_thesis: ( m1 <> 0 & m2 <> 0 & m1 gcd m2 divides c2 - c1 implies ex r being Integer st ( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 ) ) assume that A1: m1 <> 0 and A2: m2 <> 0 and A3: m1 gcd m2 divides c2 - c1 ; ::_thesis: ex r being Integer st ( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 ) set d = m1 gcd m2; set d1 = m1 div (m1 gcd m2); set d2 = m2 div (m1 gcd m2); set d3 = (c2 - c1) div (m1 gcd m2); A4: m1 div (m1 gcd m2),m2 div (m1 gcd m2) are_relative_prime by A1, Lm12; then consider r being Integer such that A5: (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 by Th15; take r ; ::_thesis: ( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 ) A6: m1 = (m1 div (m1 gcd m2)) * (m1 gcd m2) by Lm11, INT_2:21; A7: m2 = (m2 div (m1 gcd m2)) * (m1 gcd m2) by Lm11, INT_2:21; A8: m1 gcd m2 <> 0 by A1, INT_2:5; for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 proof let x be Integer; ::_thesis: ( (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 implies x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 ) assume that A9: (x - c1) mod m1 = 0 and A10: (x - c2) mod m2 = 0 ; ::_thesis: x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 set y = (x - c1) div m1; A11: x - c1 = (((x - c1) div m1) * m1) + ((x - c1) mod m1) by A1, INT_1:59 .= ((x - c1) div m1) * m1 by A9 ; then x - ((m1 * r) + c1) = m1 * (((x - c1) div m1) - r) ; then A12: m1 divides x - ((m1 * r) + c1) by INT_1:def_3; (x - c2) mod m2 = ((m1 * ((x - c1) div m1)) - (c2 - c1)) mod m2 by A11 .= ((((m1 gcd m2) * (m1 div (m1 gcd m2))) * ((x - c1) div m1)) - ((m1 gcd m2) * ((c2 - c1) div (m1 gcd m2)))) mod ((m1 gcd m2) * (m2 div (m1 gcd m2))) by A3, A6, A7, Lm11 ; then (m2 div (m1 gcd m2)) * (m1 gcd m2) divides (((m1 div (m1 gcd m2)) * ((x - c1) div m1)) - ((c2 - c1) div (m1 gcd m2))) * (m1 gcd m2) by A2, A7, A10, Lm10; then m2 div (m1 gcd m2) divides ((m1 div (m1 gcd m2)) * ((x - c1) div m1)) - ((c2 - c1) div (m1 gcd m2)) by A8, Th7; then A13: (((m1 div (m1 gcd m2)) * ((x - c1) div m1)) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 by Lm10; m2 div (m1 gcd m2) <> 0 by A2, A7; then r in Class ((Cong (m2 div (m1 gcd m2))),((x - c1) div m1)) by A4, A5, A13, Th26; then [((x - c1) div m1),r] in Cong (m2 div (m1 gcd m2)) by EQREL_1:18; then (x - c1) div m1,r are_congruent_mod m2 div (m1 gcd m2) by Def1; then m2 div (m1 gcd m2) divides ((x - c1) div m1) - r by INT_2:15; then consider w being Integer such that A14: ((x - c1) div m1) - r = (m2 div (m1 gcd m2)) * w by INT_1:def_3; x = c1 + (((x - c1) div m1) * m1) by A11 .= c1 + ((((m2 div (m1 gcd m2)) * w) + r) * m1) by A14 .= ((m1 * r) + c1) + ((w * (m1 div (m1 gcd m2))) * m2) by A6, A7 ; then m2 divides x - ((m1 * r) + c1) by INT_1:def_3; then m1 lcm m2 divides x - ((m1 * r) + c1) by A12, INT_2:19; hence x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 by INT_2:15; ::_thesis: verum end; hence ( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 ) by A5; ::_thesis: verum end; theorem :: INT_4:43 for m1, m2, a, c1, b, c2 being Integer st m1 <> 0 & m2 <> 0 & a gcd m1 divides c1 & b gcd m2 divides c2 & m1,m2 are_relative_prime holds ex w, r, s being Integer st ( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 ) proof let m1, m2, a, c1, b, c2 be Integer; ::_thesis: ( m1 <> 0 & m2 <> 0 & a gcd m1 divides c1 & b gcd m2 divides c2 & m1,m2 are_relative_prime implies ex w, r, s being Integer st ( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 ) ) assume that A1: m1 <> 0 and A2: m2 <> 0 and A3: a gcd m1 divides c1 and A4: b gcd m2 divides c2 and A5: m1,m2 are_relative_prime ; ::_thesis: ex w, r, s being Integer st ( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 ) set d2 = b gcd m2; A6: b gcd m2 <> 0 by A2, INT_2:5; set d1 = a gcd m1; A7: a gcd m1 <> 0 by A1, INT_2:5; A8: a div (a gcd m1),m1 div (a gcd m1) are_relative_prime by A1, Lm12; then consider r being Integer such that A9: (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 by Th15; A10: c2 = (c2 div (b gcd m2)) * (b gcd m2) by A4, Lm11; A11: b = (b div (b gcd m2)) * (b gcd m2) by Lm11, INT_2:21; A12: m2 = (m2 div (b gcd m2)) * (b gcd m2) by Lm11, INT_2:21; then A13: m2 div (b gcd m2) divides m2 by INT_1:def_3; A14: m2 div (b gcd m2) <> 0 by A2, A12; A15: c1 = (c1 div (a gcd m1)) * (a gcd m1) by A3, Lm11; A16: a = (a div (a gcd m1)) * (a gcd m1) by Lm11, INT_2:21; A17: b div (b gcd m2),m2 div (b gcd m2) are_relative_prime by A2, Lm12; then consider s being Integer such that A18: (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 by Th15; A19: m1 = (m1 div (a gcd m1)) * (a gcd m1) by Lm11, INT_2:21; then A20: m1 div (a gcd m1) divides m1 by INT_1:def_3; A21: m1 div (a gcd m1),m2 div (b gcd m2) are_relative_prime proof reconsider e = (m1 div (a gcd m1)) gcd (m2 div (b gcd m2)) as Element of NAT by ORDINAL1:def_12; assume not m1 div (a gcd m1),m2 div (b gcd m2) are_relative_prime ; ::_thesis: contradiction then A22: (m1 div (a gcd m1)) gcd (m2 div (b gcd m2)) <> 1 by INT_2:def_3; e divides m2 div (b gcd m2) by INT_2:21; then A23: e divides m2 by A13, INT_2:9; e divides m1 div (a gcd m1) by INT_2:21; then e divides m1 by A20, INT_2:9; then e divides m1 gcd m2 by A23, INT_2:22; then e divides 1 by A5, INT_2:def_3; hence contradiction by A22, WSIERP_1:15; ::_thesis: verum end; then consider w being Integer such that A24: (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 by Th15; take w ; ::_thesis: ex r, s being Integer st ( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 ) take r ; ::_thesis: ex s being Integer st ( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 ) take s ; ::_thesis: ( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 ) A25: m1 div (a gcd m1) <> 0 by A1, A19; for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) proof let x be Integer; ::_thesis: ( ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 implies x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) assume that A26: ((a * x) - c1) mod m1 = 0 and A27: ((b * x) - c2) mod m2 = 0 ; ::_thesis: x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) (m1 div (a gcd m1)) * (a gcd m1) divides (((a div (a gcd m1)) * x) - (c1 div (a gcd m1))) * (a gcd m1) by A1, A19, A15, A16, A26, Lm10; then m1 div (a gcd m1) divides ((a div (a gcd m1)) * x) - (c1 div (a gcd m1)) by A7, Th7; then (((a div (a gcd m1)) * x) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 by Lm10; then r in Class ((Cong (m1 div (a gcd m1))),x) by A8, A9, A25, Th26; then [x,r] in Cong (m1 div (a gcd m1)) by EQREL_1:18; then x,r are_congruent_mod m1 div (a gcd m1) by Def1; then A28: m1 div (a gcd m1) divides x - r by INT_2:15; (m2 div (b gcd m2)) * (b gcd m2) divides (((b div (b gcd m2)) * x) - (c2 div (b gcd m2))) * (b gcd m2) by A2, A12, A10, A11, A27, Lm10; then m2 div (b gcd m2) divides ((b div (b gcd m2)) * x) - (c2 div (b gcd m2)) by A6, Th7; then (((b div (b gcd m2)) * x) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 by Lm10; then s in Class ((Cong (m2 div (b gcd m2))),x) by A17, A18, A14, Th26; then [x,s] in Cong (m2 div (b gcd m2)) by EQREL_1:18; then x,s are_congruent_mod m2 div (b gcd m2) by Def1; then A29: m2 div (b gcd m2) divides x - s by INT_2:15; m2 div (b gcd m2) divides ((m1 div (a gcd m1)) * w) - (s - r) by A14, A24, Lm10; then A30: m2 div (b gcd m2) divides (x - s) - ((((m1 div (a gcd m1)) * w) + r) - s) by A29, Lm4; m1 div (a gcd m1) divides (m1 div (a gcd m1)) * w by INT_2:2; then m1 div (a gcd m1) divides (x - r) - ((m1 div (a gcd m1)) * w) by A28, Lm4; then (m1 div (a gcd m1)) * (m2 div (b gcd m2)) divides x - (r + ((m1 div (a gcd m1)) * w)) by A21, A30, Lm13; hence x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) by INT_2:15; ::_thesis: verum end; hence ( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 ) by A9, A18, A24; ::_thesis: verum end; theorem :: INT_4:44 for m1, m2, m3, a, b, c being Integer st m1 <> 0 & m2 <> 0 & m3 <> 0 & m1,m2 are_relative_prime & m1,m3 are_relative_prime & m2,m3 are_relative_prime holds ex r, s being Integer st for x being Integer st (x - a) mod m1 = 0 & (x - b) mod m2 = 0 & (x - c) mod m3 = 0 holds ( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 ) proof let m1, m2, m3, a, b, c be Integer; ::_thesis: ( m1 <> 0 & m2 <> 0 & m3 <> 0 & m1,m2 are_relative_prime & m1,m3 are_relative_prime & m2,m3 are_relative_prime implies ex r, s being Integer st for x being Integer st (x - a) mod m1 = 0 & (x - b) mod m2 = 0 & (x - c) mod m3 = 0 holds ( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 ) ) assume that A1: ( m1 <> 0 & m2 <> 0 ) and A2: m3 <> 0 and A3: m1,m2 are_relative_prime and A4: ( m1,m3 are_relative_prime & m2,m3 are_relative_prime ) ; ::_thesis: ex r, s being Integer st for x being Integer st (x - a) mod m1 = 0 & (x - b) mod m2 = 0 & (x - c) mod m3 = 0 holds ( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 ) consider r being Integer such that A5: for x being Integer st (x - a) mod m1 = 0 & (x - b) mod m2 = 0 holds x,a + (m1 * r) are_congruent_mod m1 * m2 and A6: ((m1 * r) - (b - a)) mod m2 = 0 by A1, A3, Th40; m1 * m2 <> 0 by A1, XCMPLX_1:6; then consider s being Integer such that A7: ( ( for x being Integer st (x - (a + (m1 * r))) mod (m1 * m2) = 0 & (x - c) mod m3 = 0 holds x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 ) & (((m1 * m2) * s) - (c - (a + (m1 * r)))) mod m3 = 0 ) by A2, A4, Th40, INT_2:26; take r ; ::_thesis: ex s being Integer st for x being Integer st (x - a) mod m1 = 0 & (x - b) mod m2 = 0 & (x - c) mod m3 = 0 holds ( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 ) take s ; ::_thesis: for x being Integer st (x - a) mod m1 = 0 & (x - b) mod m2 = 0 & (x - c) mod m3 = 0 holds ( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 ) for x being Integer st (x - a) mod m1 = 0 & (x - b) mod m2 = 0 & (x - c) mod m3 = 0 holds ( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 ) proof let x be Integer; ::_thesis: ( (x - a) mod m1 = 0 & (x - b) mod m2 = 0 & (x - c) mod m3 = 0 implies ( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 ) ) assume that A8: ( (x - a) mod m1 = 0 & (x - b) mod m2 = 0 ) and A9: (x - c) mod m3 = 0 ; ::_thesis: ( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 ) x,a + (m1 * r) are_congruent_mod m1 * m2 by A5, A8; then m1 * m2 divides x - (a + (m1 * r)) by INT_2:15; then (x - (a + (m1 * r))) mod (m1 * m2) = 0 by Lm10; hence ( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 ) by A6, A7, A9; ::_thesis: verum end; hence for x being Integer st (x - a) mod m1 = 0 & (x - b) mod m2 = 0 & (x - c) mod m3 = 0 holds ( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 ) ; ::_thesis: verum end; theorem :: INT_4:45 for m1, m2, m3, a, b, c being Integer st m1 <> 0 & m2 <> 0 & m3 <> 0 & ( not m1 gcd m2 divides a - b or not m1 gcd m3 divides a - c or not m2 gcd m3 divides b - c ) holds for x being Integer holds ( not (x - a) mod m1 = 0 or not (x - b) mod m2 = 0 or not (x - c) mod m3 = 0 ) by Th41; theorem Th46: :: INT_4:46 for n1, n2, n3 being non zero Nat holds (n1 gcd n3) lcm (n2 gcd n3) = (n1 lcm n2) gcd n3 proof let n1, n2, n3 be non zero Nat; ::_thesis: (n1 gcd n3) lcm (n2 gcd n3) = (n1 lcm n2) gcd n3 set d1 = n1 gcd n3; set d2 = n2 gcd n3; set M = n1 lcm n2; reconsider d = (n1 lcm n2) gcd n3 as non empty Nat by INT_2:5; reconsider M = n1 lcm n2 as non empty Nat by INT_2:4; ( n1 gcd n3 divides n3 & n2 gcd n3 divides n3 ) by NAT_D:def_5; then A1: (n1 gcd n3) lcm (n2 gcd n3) divides n3 by NAT_D:def_4; ( n2 gcd n3 divides n2 & n2 divides M ) by NAT_D:def_4, NAT_D:def_5; then A2: n2 gcd n3 divides M by NAT_D:4; A3: for p being Nat holds ( not p in support (pfexp d) or (ppf d) . p divides n1 or (ppf d) . p divides n2 ) proof let p be Nat; ::_thesis: ( not p in support (pfexp d) or (ppf d) . p divides n1 or (ppf d) . p divides n2 ) assume that A4: p in support (pfexp d) and A5: not (ppf d) . p divides n1 and A6: not (ppf d) . p divides n2 ; ::_thesis: contradiction A7: not p |^ (p |-count d) divides n2 by A4, A6, NAT_3:def_9; A8: p is Prime by A4, NAT_3:34; A9: not p |^ (p |-count d) divides n1 by A4, A5, NAT_3:def_9; A10: p |-count d > p |-count M proof A11: p |-count M = (pfexp M) . p by A8, NAT_3:def_8 .= (max ((pfexp n1),(pfexp n2))) . p by NAT_3:54 ; percases ( (pfexp n1) . p <= (pfexp n2) . p or (pfexp n1) . p > (pfexp n2) . p ) ; suppose (pfexp n1) . p <= (pfexp n2) . p ; ::_thesis: p |-count d > p |-count M then p |-count M = (pfexp n2) . p by A11, NAT_3:def_4 .= p |-count n2 by A8, NAT_3:def_8 ; hence p |-count d > p |-count M by A7, A8, MOEBIUS1:9; ::_thesis: verum end; suppose (pfexp n1) . p > (pfexp n2) . p ; ::_thesis: p |-count d > p |-count M then p |-count M = (pfexp n1) . p by A11, NAT_3:def_4 .= p |-count n1 by A8, NAT_3:def_8 ; hence p |-count d > p |-count M by A9, A8, MOEBIUS1:9; ::_thesis: verum end; end; end; d divides M by NAT_D:def_5; hence contradiction by A8, A10, NAT_3:30; ::_thesis: verum end; A12: for p being Nat st p in support (pfexp d) holds (ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3) proof A13: n2 gcd n3 divides (n1 gcd n3) lcm (n2 gcd n3) by NAT_D:def_4; let p be Nat; ::_thesis: ( p in support (pfexp d) implies (ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3) ) A14: n1 gcd n3 divides (n1 gcd n3) lcm (n2 gcd n3) by NAT_D:def_4; assume A15: p in support (pfexp d) ; ::_thesis: (ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3) then A16: p is Prime by NAT_3:34; d divides n3 by NAT_D:def_5; then p |-count d <= p |-count n3 by A16, NAT_3:30; then p |^ (p |-count d) divides p |^ (p |-count n3) by NEWTON:89; then A17: (ppf d) . p divides p |^ (p |-count n3) by A15, NAT_3:def_9; p <> 1 by A16, INT_2:def_4; then p |^ (p |-count n3) divides n3 by NAT_3:def_7; then A18: (ppf d) . p divides n3 by A17, NAT_D:4; percases ( (ppf d) . p divides n1 or (ppf d) . p divides n2 ) by A3, A15; suppose (ppf d) . p divides n1 ; ::_thesis: (ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3) then (ppf d) . p divides n1 gcd n3 by A18, NAT_D:def_5; hence (ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3) by A14, NAT_D:4; ::_thesis: verum end; suppose (ppf d) . p divides n2 ; ::_thesis: (ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3) then (ppf d) . p divides n2 gcd n3 by A18, NAT_D:def_5; hence (ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3) by A13, NAT_D:4; ::_thesis: verum end; end; end; Product (ppf d) divides (n1 gcd n3) lcm (n2 gcd n3) proof set g = ppf d; set K = canFS (support (ppf d)); consider f being FinSequence of COMPLEX such that A19: Product (ppf d) = Product f and A20: f = (ppf d) * (canFS (support (ppf d))) by NAT_3:def_5; rng f c= NAT by A20, VALUED_0:def_6; then reconsider f = f as FinSequence of NAT by FINSEQ_1:def_4; A21: rng (canFS (support (ppf d))) = support (ppf d) by FUNCT_2:def_3; then rng (canFS (support (ppf d))) c= NAT by XBOOLE_1:1; then reconsider K = canFS (support (ppf d)) as FinSequence of NAT by FINSEQ_1:def_4; A22: for m, n being Element of NAT st m in dom f & n in dom f & m <> n holds (f . m) gcd (f . n) = 1 proof let m, n be Element of NAT ; ::_thesis: ( m in dom f & n in dom f & m <> n implies (f . m) gcd (f . n) = 1 ) assume that A23: m in dom f and A24: n in dom f and A25: m <> n ; ::_thesis: (f . m) gcd (f . n) = 1 A26: m in dom K by A20, A23, FUNCT_1:11; then K . m in support (ppf d) by A21, FUNCT_1:3; then A27: K . m in support (pfexp d) by NAT_3:def_9; then A28: K . m is prime by NAT_3:34; A29: n in dom K by A20, A24, FUNCT_1:11; then K . n in support (ppf d) by A21, FUNCT_1:3; then A30: K . n in support (pfexp d) by NAT_3:def_9; then A31: K . n is prime by NAT_3:34; f . n = (ppf d) . (K . n) by A20, A24, FUNCT_1:12; then A32: f . n = (K . n) |^ ((K . n) |-count d) by A30, NAT_3:def_9; f . m = (ppf d) . (K . m) by A20, A23, FUNCT_1:12; then A33: f . m = (K . m) |^ ((K . m) |-count d) by A27, NAT_3:def_9; K . m <> K . n by A25, A26, A29, FUNCT_1:def_4; then A34: K . n,(K . m) |^ ((K . m) |-count d) are_relative_prime by A28, A31, EULER_2:17, INT_2:30; A35: K . n > 0 by A30, NAT_3:34; K . m > 0 by A27, NAT_3:34; then (K . n) |^ ((K . n) |-count d),(K . m) |^ ((K . m) |-count d) are_relative_prime by A35, A34, EULER_2:17; hence (f . m) gcd (f . n) = 1 by A33, A32, INT_2:def_3; ::_thesis: verum end; for m being Element of NAT st m in dom f holds f . m divides (n1 gcd n3) lcm (n2 gcd n3) proof let m be Element of NAT ; ::_thesis: ( m in dom f implies f . m divides (n1 gcd n3) lcm (n2 gcd n3) ) assume A36: m in dom f ; ::_thesis: f . m divides (n1 gcd n3) lcm (n2 gcd n3) then m in dom K by A20, FUNCT_1:11; then K . m in support (ppf d) by A21, FUNCT_1:3; then K . m in support (pfexp d) by NAT_3:def_9; then (ppf d) . (K . m) divides (n1 gcd n3) lcm (n2 gcd n3) by A12; hence f . m divides (n1 gcd n3) lcm (n2 gcd n3) by A20, A36, FUNCT_1:12; ::_thesis: verum end; hence Product (ppf d) divides (n1 gcd n3) lcm (n2 gcd n3) by A19, A22, Th38; ::_thesis: verum end; then A37: d divides (n1 gcd n3) lcm (n2 gcd n3) by NAT_3:61; ( n1 gcd n3 divides n1 & n1 divides M ) by NAT_D:def_4, NAT_D:def_5; then n1 gcd n3 divides M by NAT_D:4; then (n1 gcd n3) lcm (n2 gcd n3) divides M by A2, NAT_D:def_4; then (n1 gcd n3) lcm (n2 gcd n3) divides d by A1, NAT_D:def_5; hence (n1 gcd n3) lcm (n2 gcd n3) = (n1 lcm n2) gcd n3 by A37, NAT_D:5; ::_thesis: verum end; theorem :: INT_4:47 for a, b, c being Integer for n1, n2, n3 being non zero Nat st n1 gcd n2 divides a - b holds ex r, s being Integer st for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds ( x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 & (((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2)) = 0 & ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 ) proof let a, b, c be Integer; ::_thesis: for n1, n2, n3 being non zero Nat st n1 gcd n2 divides a - b holds ex r, s being Integer st for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds ( x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 & (((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2)) = 0 & ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 ) let n1, n2, n3 be non zero Nat; ::_thesis: ( n1 gcd n2 divides a - b implies ex r, s being Integer st for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds ( x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 & (((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2)) = 0 & ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 ) ) set d1 = n1 gcd n2; set d2 = n1 gcd n3; set d3 = n2 gcd n3; set dd1 = n1 gcd n2; set K = n1 lcm n2; A1: n2 divides n1 lcm n2 by NAT_D:def_4; assume n1 gcd n2 divides a - b ; ::_thesis: ex r, s being Integer st for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds ( x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 & (((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2)) = 0 & ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 ) then n1 gcd n2 divides - (a - b) by INT_2:10; then consider r being Integer such that A2: for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 holds x,a + (n1 * r) are_congruent_mod n1 lcm n2 and A3: (((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2)) = 0 by Th42; take r ; ::_thesis: ex s being Integer st for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds ( x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 & (((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2)) = 0 & ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 ) set y = a + (n1 * r); A4: (n1 lcm n2) div ((n1 lcm n2) gcd n3),n3 div ((n1 lcm n2) gcd n3) are_relative_prime by Lm12; then consider s being Integer such that A5: ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 by Th15; take s ; ::_thesis: for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds ( x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 & (((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2)) = 0 & ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 ) A6: n1 divides n1 lcm n2 by NAT_D:def_4; A7: for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds (n1 lcm n2) gcd n3 divides (a + (n1 * r)) - c proof let x be Integer; ::_thesis: ( (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 implies (n1 lcm n2) gcd n3 divides (a + (n1 * r)) - c ) assume that A8: ( (x - a) mod n1 = 0 & (x - b) mod n2 = 0 ) and A9: (x - c) mod n3 = 0 ; ::_thesis: (n1 lcm n2) gcd n3 divides (a + (n1 * r)) - c A10: n3 divides x - c by A9, Lm10; x,a + (n1 * r) are_congruent_mod n1 lcm n2 by A2, A8; then n1 lcm n2 divides x - (a + (n1 * r)) by INT_2:15; then A11: n1 lcm n2 divides - (x - (a + (n1 * r))) by INT_2:10; then n1 divides (a + (n1 * r)) - x by A6, INT_2:9; then consider t1 being Integer such that A12: (a + (n1 * r)) - x = n1 * t1 by INT_1:def_3; n2 gcd n3 divides n3 by NAT_D:def_5; then A13: n2 gcd n3 divides x - c by A10, INT_2:9; n1 gcd n3 divides n3 by NAT_D:def_5; then A14: n1 gcd n3 divides x - c by A10, INT_2:9; n2 divides (a + (n1 * r)) - x by A1, A11, INT_2:9; then consider t2 being Integer such that A15: (a + (n1 * r)) - x = n2 * t2 by INT_1:def_3; n2 gcd n3 divides n2 by NAT_D:def_5; then A16: n2 gcd n3 divides n2 * t2 by INT_2:2; (a + (n1 * r)) - c = (x - c) + (n2 * t2) by A15; then A17: n2 gcd n3 divides (a + (n1 * r)) - c by A16, A13, WSIERP_1:4; n1 gcd n3 divides n1 by NAT_D:def_5; then A18: n1 gcd n3 divides n1 * t1 by INT_2:2; (a + (n1 * r)) - c = (x - c) + (n1 * t1) by A12; then n1 gcd n3 divides (a + (n1 * r)) - c by A18, A14, WSIERP_1:4; then (n1 gcd n3) lcm (n2 gcd n3) divides (a + (n1 * r)) - c by A17, INT_2:19; hence (n1 lcm n2) gcd n3 divides (a + (n1 * r)) - c by Th46; ::_thesis: verum end; for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 proof A19: n1 lcm n2 <> 0 by INT_2:4; let x be Integer; ::_thesis: ( (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 implies x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 ) assume that A20: ( (x - a) mod n1 = 0 & (x - b) mod n2 = 0 ) and A21: (x - c) mod n3 = 0 ; ::_thesis: x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 (n1 lcm n2) gcd n3 divides (a + (n1 * r)) - c by A7, A20, A21; then (n1 lcm n2) gcd n3 divides - ((a + (n1 * r)) - c) by INT_2:10; then consider w being Integer such that A22: for x being Integer st (x - (a + (n1 * r))) mod (n1 lcm n2) = 0 & (x - c) mod n3 = 0 holds x,(a + (n1 * r)) + ((n1 lcm n2) * w) are_congruent_mod (n1 lcm n2) lcm n3 and A23: ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * w) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 by A19, Th42; A24: n3 = (n3 div ((n1 lcm n2) gcd n3)) * ((n1 lcm n2) gcd n3) by Lm11, INT_2:21; then n3 div ((n1 lcm n2) gcd n3) <> 0 ; then w in Class ((Cong (n3 div ((n1 lcm n2) gcd n3))),s) by A4, A5, A23, Th26; then [s,w] in Cong (n3 div ((n1 lcm n2) gcd n3)) by EQREL_1:18; then s,w are_congruent_mod n3 div ((n1 lcm n2) gcd n3) by Def1; then A25: (n1 lcm n2) * s,(n1 lcm n2) * w are_congruent_mod (n1 lcm n2) * (n3 div ((n1 lcm n2) gcd n3)) by Th10; (n1 lcm n2) * (n3 div ((n1 lcm n2) gcd n3)) = (((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * ((n1 lcm n2) gcd n3)) * (n3 div ((n1 lcm n2) gcd n3)) by Lm11, INT_2:21 .= n3 * ((n1 lcm n2) div ((n1 lcm n2) gcd n3)) by A24 ; then (n1 lcm n2) * s,(n1 lcm n2) * w are_congruent_mod n3 by A25, INT_1:20; then A26: n3 divides ((n1 lcm n2) * s) - ((n1 lcm n2) * w) by INT_2:15; n1 lcm n2 divides (n1 lcm n2) * (s - w) by INT_2:2; then (n1 lcm n2) lcm n3 divides (((n1 lcm n2) * s) + (a + (n1 * r))) - (((n1 lcm n2) * w) + (a + (n1 * r))) by A26, INT_2:19; then ((n1 lcm n2) * s) + (a + (n1 * r)),((n1 lcm n2) * w) + (a + (n1 * r)) are_congruent_mod (n1 lcm n2) lcm n3 by INT_2:15; then A27: ((n1 lcm n2) * w) + (a + (n1 * r)),((n1 lcm n2) * s) + (a + (n1 * r)) are_congruent_mod (n1 lcm n2) lcm n3 by INT_1:14; x,a + (n1 * r) are_congruent_mod n1 lcm n2 by A2, A20; then n1 lcm n2 divides x - (a + (n1 * r)) by INT_2:15; then (x - (a + (n1 * r))) mod (n1 lcm n2) = 0 by Lm10; then x,((n1 lcm n2) * w) + (a + (n1 * r)) are_congruent_mod (n1 lcm n2) lcm n3 by A21, A22; hence x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 by A27, INT_1:15; ::_thesis: verum end; hence for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds ( x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 & (((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2)) = 0 & ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 ) by A3, A5; ::_thesis: verum end; begin definition let m be Nat; let X be set ; predX is_CRS_of m means :Def2: :: INT_4:def 2 ex fp being FinSequence of INT st ( X = rng fp & len fp = m & ( for b being Nat st b in dom fp holds fp . b in Class ((Cong m),(b -' 1)) ) ); end; :: deftheorem Def2 defines is_CRS_of INT_4:def_2_:_ for m being Nat for X being set holds ( X is_CRS_of m iff ex fp being FinSequence of INT st ( X = rng fp & len fp = m & ( for b being Nat st b in dom fp holds fp . b in Class ((Cong m),(b -' 1)) ) ) ); theorem Th48: :: INT_4:48 for m being Element of NAT holds { a where a is Element of NAT : a < m } is_CRS_of m proof let m be Element of NAT ; ::_thesis: { a where a is Element of NAT : a < m } is_CRS_of m deffunc H1( Nat) -> Element of NAT = $1 -' 1; consider fp being FinSequence such that A1: ( len fp = m & ( for a being Nat st a in dom fp holds fp . a = H1(a) ) ) from FINSEQ_1:sch_2(); for a being Nat st a in dom fp holds fp . a in INT proof let a be Nat; ::_thesis: ( a in dom fp implies fp . a in INT ) assume a in dom fp ; ::_thesis: fp . a in INT then fp . a = H1(a) by A1; hence fp . a in INT by INT_1:def_2; ::_thesis: verum end; then reconsider fp = fp as FinSequence of INT by FINSEQ_2:12; A2: { a where a is Element of NAT : a < m } = rng fp proof set A = { a where a is Element of NAT : a < m } ; A3: rng fp c= { a where a is Element of NAT : a < m } proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng fp or b in { a where a is Element of NAT : a < m } ) assume b in rng fp ; ::_thesis: b in { a where a is Element of NAT : a < m } then consider k being set such that A4: k in dom fp and A5: b = fp . k by FUNCT_1:def_3; reconsider k = k as Element of NAT by A4; A6: k in Seg m by A1, A4, FINSEQ_1:def_3; then k <= m by FINSEQ_1:1; then A7: k - 1 < m by XREAL_1:147; k >= 1 by A6, FINSEQ_1:1; then A8: k -' 1 < m by A7, XREAL_1:233; reconsider b = b as Integer by A5; b = k -' 1 by A1, A4, A5; hence b in { a where a is Element of NAT : a < m } by A8; ::_thesis: verum end; { a where a is Element of NAT : a < m } c= rng fp proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { a where a is Element of NAT : a < m } or b in rng fp ) assume b in { a where a is Element of NAT : a < m } ; ::_thesis: b in rng fp then consider k being Element of NAT such that A9: k = b and A10: k < m ; ( k + 1 >= 1 & k + 1 <= m ) by A10, NAT_1:11, NAT_1:13; then A11: k + 1 in dom fp by A1, FINSEQ_3:25; then fp . (k + 1) = (k + 1) -' 1 by A1 .= k by NAT_D:34 ; hence b in rng fp by A9, A11, FUNCT_1:def_3; ::_thesis: verum end; hence { a where a is Element of NAT : a < m } = rng fp by A3, XBOOLE_0:def_10; ::_thesis: verum end; for a being Nat st a in dom fp holds fp . a in Class ((Cong m),(a -' 1)) proof let a be Nat; ::_thesis: ( a in dom fp implies fp . a in Class ((Cong m),(a -' 1)) ) a -' 1,a -' 1 are_congruent_mod m by INT_1:11; then A12: [(a -' 1),(a -' 1)] in Cong m by Def1; assume a in dom fp ; ::_thesis: fp . a in Class ((Cong m),(a -' 1)) then fp . a = a -' 1 by A1; hence fp . a in Class ((Cong m),(a -' 1)) by A12, EQREL_1:18; ::_thesis: verum end; hence { a where a is Element of NAT : a < m } is_CRS_of m by A1, A2, Def2; ::_thesis: verum end; theorem Th49: :: INT_4:49 for m being Element of NAT for X being finite set st X is_CRS_of m holds ( card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds not [x,y] in Cong m ) ) proof let m be Element of NAT ; ::_thesis: for X being finite set st X is_CRS_of m holds ( card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds not [x,y] in Cong m ) ) let X be finite set ; ::_thesis: ( X is_CRS_of m implies ( card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds not [x,y] in Cong m ) ) ) assume X is_CRS_of m ; ::_thesis: ( card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds not [x,y] in Cong m ) ) then consider fp being FinSequence of INT such that A1: X = rng fp and A2: len fp = m and A3: for b being Nat st b in dom fp holds fp . b in Class ((Cong m),(b -' 1)) by Def2; A4: for x, y being Integer st x in X & y in X & x <> y holds not [x,y] in Cong m proof let x, y be Integer; ::_thesis: ( x in X & y in X & x <> y implies not [x,y] in Cong m ) assume that A5: x in X and A6: y in X and A7: x <> y ; ::_thesis: not [x,y] in Cong m consider a being set such that A8: a in dom fp and A9: x = fp . a by A1, A5, FUNCT_1:def_3; reconsider a = a as Element of NAT by A8; x in Class ((Cong m),(a -' 1)) by A3, A8, A9; then [(a -' 1),x] in Cong m by EQREL_1:18; then A10: a -' 1,x are_congruent_mod m by Def1; consider b being set such that A11: b in dom fp and A12: y = fp . b by A1, A6, FUNCT_1:def_3; reconsider b = b as Element of NAT by A11; A13: b in Seg m by A2, A11, FINSEQ_1:def_3; then A14: b >= 1 by FINSEQ_1:1; y in Class ((Cong m),(b -' 1)) by A3, A11, A12; then [(b -' 1),y] in Cong m by EQREL_1:18; then b -' 1,y are_congruent_mod m by Def1; then A15: y,b -' 1 are_congruent_mod m by INT_1:14; assume [x,y] in Cong m ; ::_thesis: contradiction then x,y are_congruent_mod m by Def1; then x,b -' 1 are_congruent_mod m by A15, INT_1:15; then a -' 1,b -' 1 are_congruent_mod m by A10, INT_1:15; then A16: m divides (a -' 1) - (b -' 1) by INT_2:15; A17: a in Seg m by A2, A8, FINSEQ_1:def_3; then A18: a >= 1 by FINSEQ_1:1; b <= m by A13, FINSEQ_1:1; then a - b >= 1 - m by A18, XREAL_1:13; then A19: a - b > - m by XREAL_1:145; a <= m by A17, FINSEQ_1:1; then a - b <= m - 1 by A14, XREAL_1:13; then a - b < m by XREAL_1:147; then abs (a - b) < m by A19, SEQ_2:1; then A20: abs (a - b) < abs m by ABSVALUE:def_1; A21: (a -' 1) - (b -' 1) = (a - 1) - (b -' 1) by A18, XREAL_1:233 .= (a - 1) - (b - 1) by A14, XREAL_1:233 .= a - b ; now__::_thesis:_not_a_<>_b assume a <> b ; ::_thesis: contradiction then a - b <> 0 ; hence contradiction by A16, A21, A20, Th6; ::_thesis: verum end; hence contradiction by A7, A9, A12; ::_thesis: verum end; for a, b being set st a in dom fp & b in dom fp & fp . a = fp . b holds a = b proof let a, b be set ; ::_thesis: ( a in dom fp & b in dom fp & fp . a = fp . b implies a = b ) assume that A22: a in dom fp and A23: b in dom fp and A24: fp . a = fp . b ; ::_thesis: a = b reconsider a = a, b = b as Element of NAT by A22, A23; A25: b in Seg m by A2, A23, FINSEQ_1:def_3; then A26: b >= 1 by FINSEQ_1:1; reconsider l = fp . a, ll = fp . b as Element of INT by A22, A23, FINSEQ_2:11; fp . b in Class ((Cong m),(b -' 1)) by A3, A23; then [(b -' 1),(fp . b)] in Cong m by EQREL_1:18; then b -' 1,ll are_congruent_mod m by Def1; then A27: l,b -' 1 are_congruent_mod m by A24, INT_1:14; A28: a in Seg m by A2, A22, FINSEQ_1:def_3; then A29: a >= 1 by FINSEQ_1:1; then A30: (a -' 1) - (b -' 1) = (a - 1) - (b -' 1) by XREAL_1:233 .= (a - 1) - (b - 1) by A26, XREAL_1:233 .= a - b ; b <= m by A25, FINSEQ_1:1; then a - b >= 1 - m by A29, XREAL_1:13; then A31: a - b > - m by XREAL_1:145; a <= m by A28, FINSEQ_1:1; then a - b <= m - 1 by A26, XREAL_1:13; then a - b < m by XREAL_1:147; then abs (a - b) < m by A31, SEQ_2:1; then A32: abs (a - b) < abs m by ABSVALUE:def_1; fp . a in Class ((Cong m),(a -' 1)) by A3, A22; then [(a -' 1),(fp . a)] in Cong m by EQREL_1:18; then a -' 1,l are_congruent_mod m by Def1; then a -' 1,b -' 1 are_congruent_mod m by A27, INT_1:15; then A33: m divides a - b by A30, INT_2:15; now__::_thesis:_not_a_<>_b assume a <> b ; ::_thesis: contradiction then a - b <> 0 ; hence contradiction by A33, A32, Th6; ::_thesis: verum end; hence a = b ; ::_thesis: verum end; then fp is one-to-one by FUNCT_1:def_4; hence ( card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds not [x,y] in Cong m ) ) by A1, A2, A4, FINSEQ_4:62; ::_thesis: verum end; theorem Th50: :: INT_4:50 for m being Element of NAT holds ( {} is_CRS_of m iff m = 0 ) proof let m be Element of NAT ; ::_thesis: ( {} is_CRS_of m iff m = 0 ) set fp = <*> INT; thus ( {} is_CRS_of m implies m = 0 ) by Th49, CARD_1:27; ::_thesis: ( m = 0 implies {} is_CRS_of m ) assume m = 0 ; ::_thesis: {} is_CRS_of m then A1: len (<*> INT) = m ; ( {} = rng (<*> INT) & ( for b being Nat st b in dom (<*> INT) holds (<*> INT) . b in Class ((Cong m),(b -' 1)) ) ) ; hence {} is_CRS_of m by A1, Def2; ::_thesis: verum end; theorem Th51: :: INT_4:51 for m being Element of NAT for X being finite set st card X = m holds ex fp being FinSequence st ( len fp = m & ( for a being Element of NAT st a in dom fp holds fp . a in X ) & fp is one-to-one ) proof let m be Element of NAT ; ::_thesis: for X being finite set st card X = m holds ex fp being FinSequence st ( len fp = m & ( for a being Element of NAT st a in dom fp holds fp . a in X ) & fp is one-to-one ) defpred S1[ Nat] means for X being finite set st card X = $1 holds ex fp being FinSequence st ( len fp = $1 & ( for a being Element of NAT st a in dom fp holds fp . a in X ) & fp is one-to-one ); let X be finite set ; ::_thesis: ( card X = m implies ex fp being FinSequence st ( len fp = m & ( for a being Element of NAT st a in dom fp holds fp . a in X ) & fp is one-to-one ) ) A1: for m being Element of NAT st S1[m] holds S1[m + 1] proof let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] ) assume A2: S1[m] ; ::_thesis: S1[m + 1] let X be finite set ; ::_thesis: ( card X = m + 1 implies ex fp being FinSequence st ( len fp = m + 1 & ( for a being Element of NAT st a in dom fp holds fp . a in X ) & fp is one-to-one ) ) assume A3: card X = m + 1 ; ::_thesis: ex fp being FinSequence st ( len fp = m + 1 & ( for a being Element of NAT st a in dom fp holds fp . a in X ) & fp is one-to-one ) then consider x being set such that A4: x in X by CARD_1:27, XBOOLE_0:def_1; set Y = X \ {x}; card (X \ {x}) = (card X) - (card {x}) by A4, EULER_1:4 .= (m + 1) - 1 by A3, CARD_1:30 .= m ; then consider fp1 being FinSequence such that A5: len fp1 = m and A6: for a being Element of NAT st a in dom fp1 holds fp1 . a in X \ {x} and A7: fp1 is one-to-one by A2; set fp = fp1 ^ <*x*>; A8: len (fp1 ^ <*x*>) = m + 1 by A5, FINSEQ_2:16; for a, b being set st a in dom (fp1 ^ <*x*>) & b in dom (fp1 ^ <*x*>) & a <> b holds (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b proof let a, b be set ; ::_thesis: ( a in dom (fp1 ^ <*x*>) & b in dom (fp1 ^ <*x*>) & a <> b implies (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b ) assume that A9: a in dom (fp1 ^ <*x*>) and A10: b in dom (fp1 ^ <*x*>) and A11: a <> b ; ::_thesis: (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b A12: a in Seg (m + 1) by A8, A9, FINSEQ_1:def_3; A13: b in Seg (m + 1) by A8, A10, FINSEQ_1:def_3; reconsider a = a, b = b as Element of NAT by A9, A10; percases ( a in Seg m or a = m + 1 ) by A12, FINSEQ_2:7; supposeA14: a in Seg m ; ::_thesis: (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b percases ( b in Seg m or b = m + 1 ) by A13, FINSEQ_2:7; suppose b in Seg m ; ::_thesis: (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b then A15: b in dom fp1 by A5, FINSEQ_1:def_3; then A16: (fp1 ^ <*x*>) . b = fp1 . b by FINSEQ_1:def_7; A17: a in dom fp1 by A5, A14, FINSEQ_1:def_3; then (fp1 ^ <*x*>) . a = fp1 . a by FINSEQ_1:def_7; hence (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b by A7, A11, A17, A15, A16, FUNCT_1:def_4; ::_thesis: verum end; supposeA18: b = m + 1 ; ::_thesis: (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b a in dom fp1 by A5, A14, FINSEQ_1:def_3; then ( fp1 . a in X \ {x} & (fp1 ^ <*x*>) . a = fp1 . a ) by A6, FINSEQ_1:def_7; then A19: not (fp1 ^ <*x*>) . a in {x} by XBOOLE_0:def_5; (fp1 ^ <*x*>) . b = x by A5, A18, FINSEQ_1:42; hence (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b by A19, TARSKI:def_1; ::_thesis: verum end; end; end; supposeA20: a = m + 1 ; ::_thesis: (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b then b in Seg m by A11, A13, FINSEQ_2:7; then b in dom fp1 by A5, FINSEQ_1:def_3; then ( fp1 . b in X \ {x} & (fp1 ^ <*x*>) . b = fp1 . b ) by A6, FINSEQ_1:def_7; then not (fp1 ^ <*x*>) . b in {x} by XBOOLE_0:def_5; then (fp1 ^ <*x*>) . b <> x by TARSKI:def_1; hence (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b by A5, A20, FINSEQ_1:42; ::_thesis: verum end; end; end; then A21: for a, b being set st a in dom (fp1 ^ <*x*>) & b in dom (fp1 ^ <*x*>) & (fp1 ^ <*x*>) . a = (fp1 ^ <*x*>) . b holds a = b ; take fp1 ^ <*x*> ; ::_thesis: ( len (fp1 ^ <*x*>) = m + 1 & ( for a being Element of NAT st a in dom (fp1 ^ <*x*>) holds (fp1 ^ <*x*>) . a in X ) & fp1 ^ <*x*> is one-to-one ) for a being Element of NAT st a in dom (fp1 ^ <*x*>) holds (fp1 ^ <*x*>) . a in X proof let a be Element of NAT ; ::_thesis: ( a in dom (fp1 ^ <*x*>) implies (fp1 ^ <*x*>) . a in X ) assume a in dom (fp1 ^ <*x*>) ; ::_thesis: (fp1 ^ <*x*>) . a in X then A22: a in Seg (m + 1) by A8, FINSEQ_1:def_3; percases ( a in Seg m or a = m + 1 ) by A22, FINSEQ_2:7; suppose a in Seg m ; ::_thesis: (fp1 ^ <*x*>) . a in X then A23: a in dom fp1 by A5, FINSEQ_1:def_3; then (fp1 ^ <*x*>) . a = fp1 . a by FINSEQ_1:def_7; then (fp1 ^ <*x*>) . a in X \ {x} by A6, A23; hence (fp1 ^ <*x*>) . a in X ; ::_thesis: verum end; suppose a = m + 1 ; ::_thesis: (fp1 ^ <*x*>) . a in X hence (fp1 ^ <*x*>) . a in X by A4, A5, FINSEQ_1:42; ::_thesis: verum end; end; end; hence ( len (fp1 ^ <*x*>) = m + 1 & ( for a being Element of NAT st a in dom (fp1 ^ <*x*>) holds (fp1 ^ <*x*>) . a in X ) & fp1 ^ <*x*> is one-to-one ) by A5, A21, FINSEQ_2:16, FUNCT_1:def_4; ::_thesis: verum end; A24: S1[ 0 ] proof set fp = <*> NAT; let X be finite set ; ::_thesis: ( card X = 0 implies ex fp being FinSequence st ( len fp = 0 & ( for a being Element of NAT st a in dom fp holds fp . a in X ) & fp is one-to-one ) ) assume card X = 0 ; ::_thesis: ex fp being FinSequence st ( len fp = 0 & ( for a being Element of NAT st a in dom fp holds fp . a in X ) & fp is one-to-one ) take <*> NAT ; ::_thesis: ( len (<*> NAT) = 0 & ( for a being Element of NAT st a in dom (<*> NAT) holds (<*> NAT) . a in X ) & <*> NAT is one-to-one ) thus len (<*> NAT) = 0 ; ::_thesis: ( ( for a being Element of NAT st a in dom (<*> NAT) holds (<*> NAT) . a in X ) & <*> NAT is one-to-one ) thus ( ( for a being Element of NAT st a in dom (<*> NAT) holds (<*> NAT) . a in X ) & <*> NAT is one-to-one ) ; ::_thesis: verum end; for m being Element of NAT holds S1[m] from NAT_1:sch_1(A24, A1); hence ( card X = m implies ex fp being FinSequence st ( len fp = m & ( for a being Element of NAT st a in dom fp holds fp . a in X ) & fp is one-to-one ) ) ; ::_thesis: verum end; theorem Th52: :: INT_4:52 for m being Element of NAT for X being finite Subset of INT st card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds not [x,y] in Cong m ) holds X is_CRS_of m proof let m be Element of NAT ; ::_thesis: for X being finite Subset of INT st card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds not [x,y] in Cong m ) holds X is_CRS_of m let X be finite Subset of INT; ::_thesis: ( card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds not [x,y] in Cong m ) implies X is_CRS_of m ) assume that A1: card X = m and A2: for x, y being Integer st x in X & y in X & x <> y holds not [x,y] in Cong m ; ::_thesis: X is_CRS_of m percases ( X is empty or not X is empty ) ; suppose X is empty ; ::_thesis: X is_CRS_of m hence X is_CRS_of m by A1, Th50, CARD_1:27; ::_thesis: verum end; suppose not X is empty ; ::_thesis: X is_CRS_of m then reconsider X = X as non empty finite Subset of INT ; defpred S1[ Nat, set ] means $2 in Class ((Cong m),($1 -' 1)); A3: X <> {} ; A4: for a being Nat st a in Seg m holds ex y being Element of X st S1[a,y] proof set Y = Segm m; let a be Nat; ::_thesis: ( a in Seg m implies ex y being Element of X st S1[a,y] ) assume A5: a in Seg m ; ::_thesis: ex y being Element of X st S1[a,y] a <= m by A5, FINSEQ_1:1; then A6: a - 1 < m by XREAL_1:147; consider fp being FinSequence such that A7: len fp = m and A8: for b being Element of NAT st b in dom fp holds fp . b in X and A9: fp is one-to-one by A1, Th51; for b being Nat st b in dom fp holds fp . b in X by A8; then reconsider fp = fp as FinSequence of X by FINSEQ_2:12; defpred S2[ Nat, set ] means fp . $1 in Class ((Cong m),$2); A10: for c being Element of NAT st c in Seg m holds ex r being Element of Segm m st S2[c,r] proof let c be Element of NAT ; ::_thesis: ( c in Seg m implies ex r being Element of Segm m st S2[c,r] ) assume c in Seg m ; ::_thesis: ex r being Element of Segm m st S2[c,r] consider q, r being Integer such that A11: fp . c = (m * q) + r and A12: r >= 0 and A13: r < m by A1, Th13; (fp . c) mod m = r mod m by A11, NAT_D:61; then r,fp . c are_congruent_mod m by A1, NAT_D:64; then A14: [r,(fp . c)] in Cong m by Def1; reconsider r = r as Element of NAT by A12, INT_1:3; reconsider r = r as Element of Segm m by A13, NAT_1:44; take r ; ::_thesis: S2[c,r] thus S2[c,r] by A14, EQREL_1:18; ::_thesis: verum end; reconsider Y = Segm m as non empty set by A1, A3; A15: for c being Nat st c in Seg m holds ex r being Element of Y st S2[c,r] by A10; consider fr being FinSequence of Y such that A16: ( dom fr = Seg m & ( for c being Nat st c in Seg m holds S2[c,fr . c] ) ) from FINSEQ_1:sch_5(A15); for x1, x2 being set st x1 in dom fr & x2 in dom fr & fr . x1 = fr . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom fr & x2 in dom fr & fr . x1 = fr . x2 implies x1 = x2 ) assume that A17: x1 in dom fr and A18: x2 in dom fr and A19: fr . x1 = fr . x2 ; ::_thesis: x1 = x2 ( fp . x1 in Class ((Cong m),(fr . x1)) & fp . x2 in Class ((Cong m),(fr . x1)) ) by A16, A17, A18, A19; then A20: [(fp . x1),(fp . x2)] in Cong m by EQREL_1:22; assume A21: x1 <> x2 ; ::_thesis: contradiction reconsider x1 = x1, x2 = x2 as Element of NAT by A17, A18; A22: x1 in dom fp by A7, A16, A17, FINSEQ_1:def_3; then A23: fp . x1 in X by FINSEQ_2:11; A24: x2 in dom fp by A7, A16, A18, FINSEQ_1:def_3; then A25: fp . x2 in X by FINSEQ_2:11; fp . x1 <> fp . x2 by A9, A21, A22, A24, FUNCT_1:def_4; hence contradiction by A2, A20, A23, A25; ::_thesis: verum end; then fr is one-to-one by FUNCT_1:def_4; then A26: card (rng fr) = len fr by FINSEQ_4:62 .= m by A16, FINSEQ_1:def_3 ; reconsider Y = Y as finite set ; a >= 1 by A5, FINSEQ_1:1; then a -' 1 < m by A6, XREAL_1:233; then A27: a -' 1 in Y by NAT_1:44; m = { l where l is Element of NAT : l < m } by AXIOMS:4; then Y is_CRS_of m by Th48; then card Y = m by Th49; then rng fr = Y by A26, CARD_FIN:1; then consider w being set such that A28: w in dom fr and A29: fr . w = a -' 1 by A27, FUNCT_1:def_3; reconsider w = w as Element of NAT by A28; w in dom fp by A7, A16, A28, FINSEQ_1:def_3; then reconsider y = fp . w as Element of X by FINSEQ_2:11; take y ; ::_thesis: S1[a,y] thus S1[a,y] by A16, A28, A29; ::_thesis: verum end; consider fp being FinSequence of X such that A30: ( dom fp = Seg m & ( for a being Nat st a in Seg m holds S1[a,fp . a] ) ) from FINSEQ_1:sch_5(A4); A31: rng fp c= X by FINSEQ_1:def_4; A32: len fp = m by A30, FINSEQ_1:def_3; for a, b being set st a in dom fp & b in dom fp & fp . a = fp . b holds a = b proof let a, b be set ; ::_thesis: ( a in dom fp & b in dom fp & fp . a = fp . b implies a = b ) assume that A33: a in dom fp and A34: b in dom fp and A35: fp . a = fp . b ; ::_thesis: a = b reconsider a = a, b = b as Element of NAT by A33, A34; A36: b >= 1 by A30, A34, FINSEQ_1:1; A37: a >= 1 by A30, A33, FINSEQ_1:1; then A38: (a -' 1) - (b -' 1) = (a - 1) - (b -' 1) by XREAL_1:233 .= (a - 1) - (b - 1) by A36, XREAL_1:233 .= a - b ; reconsider l = fp . a, ll = fp . b as Element of INT by A33, A34, FINSEQ_2:11; fp . b in Class ((Cong m),(b -' 1)) by A30, A34; then [(b -' 1),(fp . b)] in Cong m by EQREL_1:18; then b -' 1,ll are_congruent_mod m by Def1; then A39: l,b -' 1 are_congruent_mod m by A35, INT_1:14; b <= m by A30, A34, FINSEQ_1:1; then a - b >= 1 - m by A37, XREAL_1:13; then A40: a - b > - m by XREAL_1:145; a <= m by A30, A33, FINSEQ_1:1; then a - b <= m - 1 by A36, XREAL_1:13; then a - b < m by XREAL_1:147; then abs (a - b) < m by A40, SEQ_2:1; then A41: abs (a - b) < abs m by ABSVALUE:def_1; fp . a in Class ((Cong m),(a -' 1)) by A30, A33; then [(a -' 1),(fp . a)] in Cong m by EQREL_1:18; then a -' 1,l are_congruent_mod m by Def1; then a -' 1,b -' 1 are_congruent_mod m by A39, INT_1:15; then A42: m divides a - b by A38, INT_2:15; now__::_thesis:_not_a_<>_b assume a <> b ; ::_thesis: contradiction then a - b <> 0 ; hence contradiction by A42, A41, Th6; ::_thesis: verum end; hence a = b ; ::_thesis: verum end; then fp is one-to-one by FUNCT_1:def_4; then card X = card (rng fp) by A1, A32, FINSEQ_4:62; then X = rng fp by A31, CARD_FIN:1; hence X is_CRS_of m by A30, A32, Def2; ::_thesis: verum end; end; end; theorem :: INT_4:53 for m being Element of NAT for a being Integer for X being finite Subset of INT st X is_CRS_of m holds a ++ X is_CRS_of m proof let m be Element of NAT ; ::_thesis: for a being Integer for X being finite Subset of INT st X is_CRS_of m holds a ++ X is_CRS_of m let a be Integer; ::_thesis: for X being finite Subset of INT st X is_CRS_of m holds a ++ X is_CRS_of m let X be finite Subset of INT; ::_thesis: ( X is_CRS_of m implies a ++ X is_CRS_of m ) assume A1: X is_CRS_of m ; ::_thesis: a ++ X is_CRS_of m then card X = m by Th49; then A2: card (a ++ X) = m by Th2; A3: for i, j being Integer st i in a ++ X & j in a ++ X & i <> j holds not [i,j] in Cong m proof let i, j be Integer; ::_thesis: ( i in a ++ X & j in a ++ X & i <> j implies not [i,j] in Cong m ) assume that A4: i in a ++ X and A5: j in a ++ X and A6: i <> j ; ::_thesis: not [i,j] in Cong m consider u being Element of COMPLEX such that A7: i = a + u and A8: u in X by A4, MEMBER_1:143; consider w being Element of COMPLEX such that A9: j = a + w and A10: w in X by A5, MEMBER_1:143; reconsider u9 = u, w9 = w as Integer by A8, A10; assume [i,j] in Cong m ; ::_thesis: contradiction then i,j are_congruent_mod m by Def1; then m divides (a + u9) - (a + w9) by A7, A9, INT_2:15; then m divides u9 - w9 ; then A11: u9,w9 are_congruent_mod m by INT_2:15; not [u9,w9] in Cong m by A1, A6, A8, A7, A10, A9, Th49; hence contradiction by A11, Def1; ::_thesis: verum end; a ++ X is Subset of INT by Lm1; hence a ++ X is_CRS_of m by A2, A3, Th52; ::_thesis: verum end; theorem :: INT_4:54 for m being Element of NAT for a being Integer for X being finite Subset of INT st a,m are_relative_prime & X is_CRS_of m holds a ** X is_CRS_of m proof let m be Element of NAT ; ::_thesis: for a being Integer for X being finite Subset of INT st a,m are_relative_prime & X is_CRS_of m holds a ** X is_CRS_of m let a be Integer; ::_thesis: for X being finite Subset of INT st a,m are_relative_prime & X is_CRS_of m holds a ** X is_CRS_of m let X be finite Subset of INT; ::_thesis: ( a,m are_relative_prime & X is_CRS_of m implies a ** X is_CRS_of m ) assume that A1: a,m are_relative_prime and A2: X is_CRS_of m ; ::_thesis: a ** X is_CRS_of m A3: card X = m by A2, Th49; A4: a ** X c= INT by Lm2; percases ( a = 0 or a <> 0 ) ; supposeA5: a = 0 ; ::_thesis: a ** X is_CRS_of m then a gcd m = abs m by WSIERP_1:8 .= m by ABSVALUE:def_1 ; then A6: m = 1 by A1, INT_2:def_3; then ex x being set st X = {x} by A3, CARD_2:42; then A7: a ** X = {0} by A5, Th4; A8: for x, y being Integer st x in a ** X & y in a ** X & x <> y holds not [x,y] in Cong m proof let x, y be Integer; ::_thesis: ( x in a ** X & y in a ** X & x <> y implies not [x,y] in Cong m ) assume that A9: x in a ** X and A10: ( y in a ** X & x <> y ) ; ::_thesis: not [x,y] in Cong m assume [x,y] in Cong m ; ::_thesis: contradiction x = 0 by A7, A9, TARSKI:def_1; hence contradiction by A7, A10, TARSKI:def_1; ::_thesis: verum end; card (a ** X) = m by A6, A7, CARD_2:42; hence a ** X is_CRS_of m by A4, A8, Th52; ::_thesis: verum end; supposeA11: a <> 0 ; ::_thesis: a ** X is_CRS_of m A12: for x, y being Integer st x in a ** X & y in a ** X & x <> y holds not [x,y] in Cong m proof let x, y be Integer; ::_thesis: ( x in a ** X & y in a ** X & x <> y implies not [x,y] in Cong m ) assume that A13: x in a ** X and A14: y in a ** X and A15: x <> y ; ::_thesis: not [x,y] in Cong m consider y1 being Integer such that A16: y1 in X and A17: y = a * y1 by A14, Lm3; consider x1 being Integer such that A18: x1 in X and A19: x = a * x1 by A13, Lm3; not [x1,y1] in Cong m by A2, A15, A18, A19, A16, A17, Th49; then A20: not x1,y1 are_congruent_mod m by Def1; assume [x,y] in Cong m ; ::_thesis: contradiction then a * x1,a * y1 are_congruent_mod m by A19, A17, Def1; hence contradiction by A1, A20, Th9; ::_thesis: verum end; card (a ** X) = m by A3, A11, Th5; hence a ** X is_CRS_of m by A4, A12, Th52; ::_thesis: verum end; end; end;