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