:: EULER_2 semantic presentation
begin
Lm1: for t being Integer holds
( t < 1 iff t <= 0 )
proof
let t be Integer; ::_thesis: ( t < 1 iff t <= 0 )
( t < 1 implies t <= 0 )
proof
assume A1: t < 1 ; ::_thesis: t <= 0
assume A2: t > 0 ; ::_thesis: contradiction
then reconsider t = t as Element of NAT by INT_1:3;
t >= 1 by A2, NAT_1:14;
hence contradiction by A1; ::_thesis: verum
end;
hence ( t < 1 iff t <= 0 ) ; ::_thesis: verum
end;
Lm2: for a being Nat st a <> 0 holds
a - 1 >= 0
proof
let a be Nat; ::_thesis: ( a <> 0 implies a - 1 >= 0 )
assume a <> 0 ; ::_thesis: a - 1 >= 0
then a >= 1 by NAT_1:14;
then a - 1 >= 1 - 1 by XREAL_1:9;
hence a - 1 >= 0 ; ::_thesis: verum
end;
Lm3: for z being Integer holds 1 gcd z = 1
proof
let z be Integer; ::_thesis: 1 gcd z = 1
thus 1 gcd z = (abs 1) gcd (abs z) by INT_2:34
.= 1 gcd (abs z) by ABSVALUE:def_1
.= 1 by NEWTON:51 ; ::_thesis: verum
end;
theorem :: EULER_2:1
for a, b being Nat holds
( a,b are_relative_prime iff a,b are_relative_prime ) ;
theorem Th2: :: EULER_2:2
for m being Nat
for t being Integer st m * t >= 1 holds
t >= 1
proof
let m be Nat; ::_thesis: for t being Integer st m * t >= 1 holds
t >= 1
let t be Integer; ::_thesis: ( m * t >= 1 implies t >= 1 )
assume A1: m * t >= 1 ; ::_thesis: t >= 1
assume t < 1 ; ::_thesis: contradiction
then t <= 0 by Lm1;
hence contradiction by A1; ::_thesis: verum
end;
Lm4: for m being Nat
for z being Integer st 1 - m <= z & z <= m - 1 & m divides z holds
z = 0
proof
let m be Nat; ::_thesis: for z being Integer st 1 - m <= z & z <= m - 1 & m divides z holds
z = 0
let z be Integer; ::_thesis: ( 1 - m <= z & z <= m - 1 & m divides z implies z = 0 )
assume that
A1: 1 - m <= z and
A2: z <= m - 1 and
A3: m divides z ; ::_thesis: z = 0
consider t being Integer such that
A4: z = m * t by A3, INT_1:def_3;
assume A5: z <> 0 ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( t > 0 or t < 0 ) by A5, A4;
supposeA6: t > 0 ; ::_thesis: contradiction
then reconsider t = t as Element of NAT by INT_1:3;
m * t >= m by A6, NAT_1:14, NEWTON:33;
then (m * t) + 1 > m by NAT_1:13;
hence contradiction by A2, A4, XREAL_1:19; ::_thesis: verum
end;
supposeA7: t < 0 ; ::_thesis: contradiction
reconsider r = t + 1 as Integer ;
1 <= (m * t) + (m * 1) by A1, A4, XREAL_1:20;
then 1 <= m * (t + 1) ;
then r >= 1 by Th2;
then 1 - 1 <= t by XREAL_1:20;
hence contradiction by A7; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
theorem Th3: :: EULER_2:3
for a, b, m being Nat st a <> 0 & b <> 0 & m <> 0 & a,m are_relative_prime & b,m are_relative_prime holds
m,(a * b) mod m are_relative_prime
proof
let a, b, m be Nat; ::_thesis: ( a <> 0 & b <> 0 & m <> 0 & a,m are_relative_prime & b,m are_relative_prime implies m,(a * b) mod m are_relative_prime )
assume that
A1: a <> 0 and
A2: b <> 0 and
A3: m <> 0 and
A4: ( a,m are_relative_prime & b,m are_relative_prime ) ; ::_thesis: m,(a * b) mod m are_relative_prime
a * b,m are_relative_prime by A1, A3, A4, EULER_1:14;
then A5: (a * b) gcd m = 1 by INT_2:def_3;
consider t being Nat such that
A6: a * b = (m * t) + ((a * b) mod m) and
(a * b) mod m < m by A3, NAT_D:def_2;
a * b <> a * 0 by A1, A2, XCMPLX_1:5;
then ((a * b) + ((- t) * m)) gcd m = (a * b) gcd m by EULER_1:16;
hence m,(a * b) mod m are_relative_prime by A6, A5, INT_2:def_3; ::_thesis: verum
end;
theorem Th4: :: EULER_2:4
for m, n, a, b being Nat st m > 1 & m,n are_relative_prime & n = (a * b) mod m holds
m,b are_relative_prime
proof
let m, n, a, b be Nat; ::_thesis: ( m > 1 & m,n are_relative_prime & n = (a * b) mod m implies m,b are_relative_prime )
assume that
A1: m > 1 and
A2: m,n are_relative_prime and
A3: n = (a * b) mod m ; ::_thesis: m,b are_relative_prime
set k = m gcd b;
m gcd b divides m by NAT_D:def_5;
then consider km being Nat such that
A4: m = (m gcd b) * km by NAT_D:def_3;
A5: ( m gcd b <> 0 & km <> 0 ) by A1, A4;
reconsider km = km as Element of NAT by ORDINAL1:def_12;
m gcd b divides b by NAT_D:def_5;
then consider kb being Nat such that
A6: b = (m gcd b) * kb by NAT_D:def_3;
consider p being Nat such that
A7: a * ((m gcd b) * kb) = (((m gcd b) * km) * p) + ((a * ((m gcd b) * kb)) mod ((m gcd b) * km)) and
(a * ((m gcd b) * kb)) mod ((m gcd b) * km) < (m gcd b) * km by A1, A4, NAT_D:def_2;
set tm = (a * kb) - (km * p);
A8: (a * ((m gcd b) * kb)) mod ((m gcd b) * km) = (m gcd b) * ((a * kb) - (km * p)) by A7;
assume not m,b are_relative_prime ; ::_thesis: contradiction
then A9: m gcd b <> 1 by INT_2:def_3;
A10: m gcd b <> - 1 by NAT_1:2;
A11: ( (a * kb) - (km * p) <> 0 implies m gcd n <> 1 )
proof
assume (a * kb) - (km * p) <> 0 ; ::_thesis: m gcd n <> 1
m gcd n = (m gcd b) * (km gcd ((a * kb) - (km * p))) by A3, A4, A5, A6, A8, EULER_1:15;
hence m gcd n <> 1 by A9, A10, INT_1:9; ::_thesis: verum
end;
( (a * kb) - (km * p) = 0 implies m gcd n <> 1 ) by A1, A3, A4, A6, A8, NEWTON:52;
hence contradiction by A2, A11, INT_2:def_3; ::_thesis: verum
end;
theorem Th5: :: EULER_2:5
for m, n being Nat holds (m mod n) mod n = m mod n
proof
let m, n be Nat; ::_thesis: (m mod n) mod n = m mod n
percases ( n <> 0 or n = 0 ) ;
suppose n <> 0 ; ::_thesis: (m mod n) mod n = m mod n
then ex t being Nat st
( m = (n * t) + (m mod n) & m mod n < n ) by NAT_D:def_2;
hence (m mod n) mod n = m mod n by NAT_D:24; ::_thesis: verum
end;
supposeA1: n = 0 ; ::_thesis: (m mod n) mod n = m mod n
hence (m mod n) mod n = 0 by NAT_D:def_2
.= m mod n by A1, NAT_D:def_2 ;
::_thesis: verum
end;
end;
end;
theorem :: EULER_2:6
for l, m, n being Nat holds (l + m) mod n = ((l mod n) + (m mod n)) mod n
proof
let l, m, n be Nat; ::_thesis: (l + m) mod n = ((l mod n) + (m mod n)) mod n
thus (l + m) mod n = ((l mod n) + m) mod n by NAT_D:22
.= ((l mod n) + (m mod n)) mod n by NAT_D:23 ; ::_thesis: verum
end;
theorem Th7: :: EULER_2:7
for l, m, n being Nat holds (l * m) mod n = (l * (m mod n)) mod n
proof
let l, m, n be Nat; ::_thesis: (l * m) mod n = (l * (m mod n)) mod n
percases ( n <> 0 or n = 0 ) ;
suppose n <> 0 ; ::_thesis: (l * m) mod n = (l * (m mod n)) mod n
then consider t being Nat such that
A1: m = (n * t) + (m mod n) and
m mod n < n by NAT_D:def_2;
(l * m) mod n = (((l * t) * n) + (l * (m mod n))) mod n by A1;
hence (l * m) mod n = (l * (m mod n)) mod n by NAT_D:21; ::_thesis: verum
end;
supposeA2: n = 0 ; ::_thesis: (l * m) mod n = (l * (m mod n)) mod n
hence (l * m) mod n = 0 by NAT_D:def_2
.= (l * (m mod n)) mod n by A2, NAT_D:def_2 ;
::_thesis: verum
end;
end;
end;
theorem :: EULER_2:8
for l, m, n being Nat holds (l * m) mod n = ((l mod n) * m) mod n by Th7;
theorem Th9: :: EULER_2:9
for l, m, n being Nat holds (l * m) mod n = ((l mod n) * (m mod n)) mod n
proof
let l, m, n be Nat; ::_thesis: (l * m) mod n = ((l mod n) * (m mod n)) mod n
(l * m) mod n = (l * (m mod n)) mod n by Th7;
hence (l * m) mod n = ((l mod n) * (m mod n)) mod n by Th7; ::_thesis: verum
end;
begin
definition
let f be FinSequence of NAT ;
let a be Nat;
:: original: *
redefine funca * f -> FinSequence of NAT ;
coherence
a * f is FinSequence of NAT
proof
rng (a * f) c= NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (a * f) or x in NAT )
assume x in rng (a * f) ; ::_thesis: x in NAT
then consider xx being set such that
A1: xx in dom (a * f) and
A2: x = (a * f) . xx by FUNCT_1:def_3;
reconsider xx = xx as Element of NAT by A1;
(a * f) . xx = a * (f . xx) by RVSUM_1:44;
hence x in NAT by A2; ::_thesis: verum
end;
hence a * f is FinSequence of NAT by FINSEQ_1:def_4; ::_thesis: verum
end;
end;
theorem Th10: :: EULER_2:10
for R1, R2 being FinSequence of NAT st R1,R2 are_fiberwise_equipotent holds
Product R1 = Product R2
proof
let R1, R2 be FinSequence of NAT ; ::_thesis: ( R1,R2 are_fiberwise_equipotent implies Product R1 = Product R2 )
defpred S1[ Nat] means for f, g being FinSequence of NAT st f,g are_fiberwise_equipotent & len f = $1 holds
Product f = Product g;
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
let f, g be FinSequence of NAT ; ::_thesis: ( f,g are_fiberwise_equipotent & len f = n + 1 implies Product f = Product g )
assume that
A3: f,g are_fiberwise_equipotent and
A4: len f = n + 1 ; ::_thesis: Product f = Product g
reconsider a = f . (n + 1) as Element of NAT ;
A5: rng f = rng g by A3, CLASSES1:75;
set fn = f | n;
A6: f = (f | n) ^ <*a*> by A4, RFINSEQ:7;
0 + 1 <= n + 1 by NAT_1:13;
then n + 1 in dom f by A4, FINSEQ_3:25;
then a in rng g by A5, FUNCT_1:def_3;
then consider m being Nat such that
A7: m in dom g and
A8: g . m = a by FINSEQ_2:10;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
set gg = g /^ m;
set gm = g | m;
m <= len g by A7, FINSEQ_3:25;
then A9: len (g | m) = m by FINSEQ_1:59;
A10: 1 <= m by A7, FINSEQ_3:25;
then max (0,(m - 1)) = m - 1 by FINSEQ_2:4;
then reconsider m1 = m - 1 as Element of NAT by FINSEQ_2:5;
A11: m = m1 + 1 ;
then m1 <= m by NAT_1:11;
then A12: Seg m1 c= Seg m by FINSEQ_1:5;
m in Seg m by A10, FINSEQ_1:1;
then (g | m) . m = a by A7, A8, RFINSEQ:6;
then A13: g | m = ((g | m) | m1) ^ <*a*> by A9, A11, RFINSEQ:7;
A14: g = (g | m) ^ (g /^ m) by RFINSEQ:8;
A15: (g | m) | m1 = (g | m) | (Seg m1) by FINSEQ_1:def_15
.= (g | (Seg m)) | (Seg m1) by FINSEQ_1:def_15
.= g | ((Seg m) /\ (Seg m1)) by RELAT_1:71
.= g | (Seg m1) by A12, XBOOLE_1:28
.= g | m1 by FINSEQ_1:def_15 ;
now__::_thesis:_for_x_being_set_holds_card_(Coim_((f_|_n),x))_=_card_(Coim_(((g_|_m1)_^_(g_/^_m)),x))
let x be set ; ::_thesis: card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x))
card (Coim (f,x)) = card (Coim (g,x)) by A3, CLASSES1:def_9;
then (card ((f | n) " {x})) + (card (<*a*> " {x})) = card ((((g | m1) ^ <*a*>) ^ (g /^ m)) " {x}) by A14, A13, A15, A6, FINSEQ_3:57
.= (card (((g | m1) ^ <*a*>) " {x})) + (card ((g /^ m) " {x})) by FINSEQ_3:57
.= ((card ((g | m1) " {x})) + (card (<*a*> " {x}))) + (card ((g /^ m) " {x})) by FINSEQ_3:57
.= ((card ((g | m1) " {x})) + (card ((g /^ m) " {x}))) + (card (<*a*> " {x}))
.= (card (((g | m1) ^ (g /^ m)) " {x})) + (card (<*a*> " {x})) by FINSEQ_3:57 ;
hence card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x)) ; ::_thesis: verum
end;
then A16: f | n,(g | m1) ^ (g /^ m) are_fiberwise_equipotent by CLASSES1:def_9;
len (f | n) = n by A4, FINSEQ_1:59, NAT_1:11;
then Product (f | n) = Product ((g | m1) ^ (g /^ m)) by A2, A16;
hence Product f = (Product ((g | m1) ^ (g /^ m))) * (Product <*a*>) by A6, RVSUM_1:97
.= ((Product (g | m1)) * (Product (g /^ m))) * (Product <*a*>) by RVSUM_1:97
.= ((Product (g | m1)) * (Product <*a*>)) * (Product (g /^ m))
.= (Product (g | m)) * (Product (g /^ m)) by A13, A15, RVSUM_1:97
.= Product g by A14, RVSUM_1:97 ;
::_thesis: verum
end;
assume A17: R1,R2 are_fiberwise_equipotent ; ::_thesis: Product R1 = Product R2
A18: len R1 = len R1 ;
A19: S1[ 0 ]
proof
let f, g be FinSequence of NAT ; ::_thesis: ( f,g are_fiberwise_equipotent & len f = 0 implies Product f = Product g )
assume ( f,g are_fiberwise_equipotent & len f = 0 ) ; ::_thesis: Product f = Product g
then A20: ( len g = 0 & f = <*> NAT ) by RFINSEQ:3;
then g = <*> NAT ;
hence Product f = Product g by A20; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A19, A1);
hence Product R1 = Product R2 by A17, A18; ::_thesis: verum
end;
begin
definition
let f be FinSequence of NAT ;
let m be Nat;
funcf mod m -> FinSequence of NAT means :Def1: :: EULER_2:def 1
( len it = len f & ( for i being Nat st i in dom f holds
it . i = (f . i) mod m ) );
existence
ex b1 being FinSequence of NAT st
( len b1 = len f & ( for i being Nat st i in dom f holds
b1 . i = (f . i) mod m ) )
proof
deffunc H1( Nat) -> Element of NAT = (f . $1) mod m;
consider g being FinSequence such that
A1: len g = len f and
A2: for k being Nat st k in dom g holds
g . k = H1(k) from FINSEQ_1:sch_2();
rng g c= NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng g or x in NAT )
assume x in rng g ; ::_thesis: x in NAT
then consider y being set such that
A3: y in dom g and
A4: x = g . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A3;
g . y = (f . y) mod m by A2, A3;
hence x in NAT by A4; ::_thesis: verum
end;
then reconsider g = g as FinSequence of NAT by FINSEQ_1:def_4;
take g ; ::_thesis: ( len g = len f & ( for i being Nat st i in dom f holds
g . i = (f . i) mod m ) )
thus len g = len f by A1; ::_thesis: for i being Nat st i in dom f holds
g . i = (f . i) mod m
let k be Nat; ::_thesis: ( k in dom f implies g . k = (f . k) mod m )
assume k in dom f ; ::_thesis: g . k = (f . k) mod m
then k in dom g by A1, FINSEQ_3:29;
hence g . k = (f . k) mod m by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of NAT st len b1 = len f & ( for i being Nat st i in dom f holds
b1 . i = (f . i) mod m ) & len b2 = len f & ( for i being Nat st i in dom f holds
b2 . i = (f . i) mod m ) holds
b1 = b2
proof
let fa, fb be FinSequence of NAT ; ::_thesis: ( len fa = len f & ( for i being Nat st i in dom f holds
fa . i = (f . i) mod m ) & len fb = len f & ( for i being Nat st i in dom f holds
fb . i = (f . i) mod m ) implies fa = fb )
assume that
A5: len f = len fa and
A6: for i being Nat st i in dom f holds
fa . i = (f . i) mod m and
A7: len f = len fb and
A8: for i being Nat st i in dom f holds
fb . i = (f . i) mod m ; ::_thesis: fa = fb
now__::_thesis:_for_X_being_set_st_dom_f_=_X_holds_
fa_=_fb
let X be set ; ::_thesis: ( dom f = X implies fa = fb )
assume A9: dom f = X ; ::_thesis: fa = fb
A10: for i being Nat st i in X holds
fa . i = fb . i
proof
given j being Nat such that A11: j in X and
A12: fa . j <> fb . j ; ::_thesis: contradiction
fa . j <> (f . j) mod m by A8, A9, A11, A12;
hence contradiction by A6, A9, A11; ::_thesis: verum
end;
A13: dom f = Seg (len f) by FINSEQ_1:def_3
.= dom fb by A7, FINSEQ_1:def_3 ;
dom f = Seg (len f) by FINSEQ_1:def_3
.= dom fa by A5, FINSEQ_1:def_3 ;
hence fa = fb by A9, A13, A10, FINSEQ_1:13; ::_thesis: verum
end;
hence fa = fb ; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines mod EULER_2:def_1_:_
for f being FinSequence of NAT
for m being Nat
for b3 being FinSequence of NAT holds
( b3 = f mod m iff ( len b3 = len f & ( for i being Nat st i in dom f holds
b3 . i = (f . i) mod m ) ) );
theorem :: EULER_2:11
for m being Nat
for f being FinSequence of NAT st m <> 0 holds
(Product (f mod m)) mod m = (Product f) mod m
proof
let m be Nat; ::_thesis: for f being FinSequence of NAT st m <> 0 holds
(Product (f mod m)) mod m = (Product f) mod m
defpred S1[ Nat] means for f being FinSequence of NAT st m <> 0 & len f = $1 holds
(Product (f mod m)) mod m = (Product f) mod m;
let f be FinSequence of NAT ; ::_thesis: ( m <> 0 implies (Product (f mod m)) mod m = (Product f) mod m )
assume A1: m <> 0 ; ::_thesis: (Product (f mod m)) mod m = (Product f) mod m
A2: len f is Element of NAT ;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
let f be FinSequence of NAT ; ::_thesis: ( m <> 0 & len f = n + 1 implies (Product (f mod m)) mod m = (Product f) mod m )
assume that
A5: m <> 0 and
A6: len f = n + 1 ; ::_thesis: (Product (f mod m)) mod m = (Product f) mod m
reconsider fn = f | n as FinSequence of NAT ;
A7: len fn = n by A6, FINSEQ_1:59, NAT_1:11;
A8: len (f mod m) = n + 1 by A6, Def1;
then A9: len ((f mod m) | n) = n by FINSEQ_1:59, NAT_1:11;
A10: n <= len f by A6, NAT_1:11;
A11: for i being Nat st 1 <= i & i <= len ((f mod m) | n) holds
((f mod m) | n) . i = (fn mod m) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len ((f mod m) | n) implies ((f mod m) | n) . i = (fn mod m) . i )
assume that
A12: 1 <= i and
A13: i <= len ((f mod m) | n) ; ::_thesis: ((f mod m) | n) . i = (fn mod m) . i
A14: (f | n) . i = (f | (Seg n)) . i by FINSEQ_1:def_15;
A15: i in Seg n by A9, A12, A13, FINSEQ_1:1;
then A16: ((f mod m) | (Seg n)) . i = (f mod m) . i by FUNCT_1:49;
i <= len f by A10, A9, A13, XXREAL_0:2;
then A17: i in dom f by A12, FINSEQ_3:25;
i in dom fn by A7, A9, A12, A13, FINSEQ_3:25;
then (fn mod m) . i = (fn . i) mod m by Def1
.= (f . i) mod m by A15, A14, FUNCT_1:49
.= (f mod m) . i by A17, Def1 ;
hence ((f mod m) | n) . i = (fn mod m) . i by A16, FINSEQ_1:def_15; ::_thesis: verum
end;
0 + 1 <= n + 1 by NAT_1:13;
then n + 1 in dom f by A6, FINSEQ_3:25;
then A18: (f mod m) . (n + 1) = (f . (n + 1)) mod m by Def1;
len ((f mod m) | n) = len (fn mod m) by A7, A9, Def1;
then (f mod m) | n = fn mod m by A11, FINSEQ_1:14;
then f mod m = (fn mod m) ^ <*((f . (n + 1)) mod m)*> by A8, A18, RFINSEQ:7;
then A19: (Product (f mod m)) mod m = ((Product (fn mod m)) * ((f . (n + 1)) mod m)) mod m by RVSUM_1:96
.= (((Product (fn mod m)) mod m) * (((f . (n + 1)) mod m) mod m)) mod m by Th9
.= (((Product fn) mod m) * (((f . (n + 1)) mod m) mod m)) mod m by A4, A5, A7
.= (((Product fn) mod m) * ((f . (n + 1)) mod m)) mod m by Th5 ;
(Product f) mod m = (Product (fn ^ <*(f . (n + 1))*>)) mod m by A6, RFINSEQ:7
.= ((Product fn) * (f . (n + 1))) mod m by RVSUM_1:96 ;
hence (Product (f mod m)) mod m = (Product f) mod m by A19, Th9; ::_thesis: verum
end;
A20: S1[ 0 ]
proof
let f be FinSequence of NAT ; ::_thesis: ( m <> 0 & len f = 0 implies (Product (f mod m)) mod m = (Product f) mod m )
assume that
m <> 0 and
A21: len f = 0 ; ::_thesis: (Product (f mod m)) mod m = (Product f) mod m
A22: ( f = <*> NAT & len (f mod m) = 0 ) by A21, Def1;
then f mod m = <*> NAT ;
hence (Product (f mod m)) mod m = (Product f) mod m by A22; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A20, A3);
hence (Product (f mod m)) mod m = (Product f) mod m by A1, A2; ::_thesis: verum
end;
theorem Th12: :: EULER_2:12
for a, m, n being Nat st a <> 0 & m > 1 & (a * n) mod m = n mod m & m,n are_relative_prime holds
a mod m = 1
proof
let a, m, n be Nat; ::_thesis: ( a <> 0 & m > 1 & (a * n) mod m = n mod m & m,n are_relative_prime implies a mod m = 1 )
assume that
A1: a <> 0 and
A2: m > 1 and
A3: (a * n) mod m = n mod m and
A4: m,n are_relative_prime ; ::_thesis: a mod m = 1
consider k2 being Nat such that
A5: n = (m * k2) + (n mod m) and
n mod m < m by A2, NAT_D:def_2;
consider k1 being Nat such that
A6: a * n = (m * k1) + ((a * n) mod m) and
(a * n) mod m < m by A2, NAT_D:def_2;
(a - 1) * n = m * (k1 - k2) by A3, A6, A5;
then A7: m divides (a - 1) * n by INT_1:def_3;
reconsider t = a - 1, m = m as Integer ;
m divides t by A4, A7, INT_2:25;
then consider tt being Integer such that
A8: a - 1 = m * tt by INT_1:def_3;
a - 1 >= 0 by A1, Lm2;
then A9: tt >= 0 by A2, A8, XREAL_1:158;
A10: a = (m * tt) + 1 by A8;
reconsider tt = tt, m = m as Element of NAT by A9, INT_1:3;
a mod m = (((m * tt) mod m) + 1) mod m by A10, NAT_D:22
.= (0 + 1) mod m by NAT_D:13
.= 1 by A2, NAT_D:24 ;
hence a mod m = 1 ; ::_thesis: verum
end;
theorem :: EULER_2:13
for m being Nat
for F being FinSequence of NAT holds (F mod m) mod m = F mod m
proof
let m be Nat; ::_thesis: for F being FinSequence of NAT holds (F mod m) mod m = F mod m
let F be FinSequence of NAT ; ::_thesis: (F mod m) mod m = F mod m
A1: dom (F mod m) = Seg (len (F mod m)) by FINSEQ_1:def_3
.= Seg (len F) by Def1
.= dom F by FINSEQ_1:def_3 ;
A2: for x being set st x in dom F holds
((F mod m) mod m) . x = (F mod m) . x
proof
let x be set ; ::_thesis: ( x in dom F implies ((F mod m) mod m) . x = (F mod m) . x )
assume A3: x in dom F ; ::_thesis: ((F mod m) mod m) . x = (F mod m) . x
then reconsider x = x as Element of NAT ;
((F mod m) mod m) . x = ((F mod m) . x) mod m by A1, A3, Def1
.= ((F . x) mod m) mod m by A3, Def1
.= (F . x) mod m by Th5
.= (F mod m) . x by A3, Def1 ;
hence ((F mod m) mod m) . x = (F mod m) . x ; ::_thesis: verum
end;
dom ((F mod m) mod m) = Seg (len ((F mod m) mod m)) by FINSEQ_1:def_3
.= Seg (len (F mod m)) by Def1
.= Seg (len F) by Def1
.= dom F by FINSEQ_1:def_3 ;
hence (F mod m) mod m = F mod m by A1, A2, FUNCT_1:2; ::_thesis: verum
end;
theorem :: EULER_2:14
for a, m being Nat
for F being FinSequence of NAT holds (a * (F mod m)) mod m = (a * F) mod m
proof
let a, m be Nat; ::_thesis: for F being FinSequence of NAT holds (a * (F mod m)) mod m = (a * F) mod m
let F be FinSequence of NAT ; ::_thesis: (a * (F mod m)) mod m = (a * F) mod m
A1: dom (a * F) = Seg (len (a * F)) by FINSEQ_1:def_3
.= Seg (len F) by NEWTON:2
.= dom F by FINSEQ_1:def_3 ;
A2: dom (a * (F mod m)) = Seg (len (a * (F mod m))) by FINSEQ_1:def_3
.= Seg (len (F mod m)) by NEWTON:2
.= Seg (len F) by Def1
.= dom F by FINSEQ_1:def_3 ;
A3: for x being set st x in dom F holds
((a * (F mod m)) mod m) . x = ((a * F) mod m) . x
proof
let x be set ; ::_thesis: ( x in dom F implies ((a * (F mod m)) mod m) . x = ((a * F) mod m) . x )
assume A4: x in dom F ; ::_thesis: ((a * (F mod m)) mod m) . x = ((a * F) mod m) . x
then reconsider x = x as Element of NAT ;
((a * (F mod m)) mod m) . x = ((a * (F mod m)) . x) mod m by A2, A4, Def1
.= (a * ((F mod m) . x)) mod m by RVSUM_1:44
.= (a * ((F . x) mod m)) mod m by A4, Def1
.= (a * (F . x)) mod m by Th7
.= ((a * F) . x) mod m by RVSUM_1:44
.= ((a * F) mod m) . x by A1, A4, Def1 ;
hence ((a * (F mod m)) mod m) . x = ((a * F) mod m) . x ; ::_thesis: verum
end;
A5: dom ((a * F) mod m) = Seg (len ((a * F) mod m)) by FINSEQ_1:def_3
.= Seg (len (a * F)) by Def1
.= Seg (len F) by NEWTON:2
.= dom F by FINSEQ_1:def_3 ;
dom ((a * (F mod m)) mod m) = Seg (len ((a * (F mod m)) mod m)) by FINSEQ_1:def_3
.= Seg (len (a * (F mod m))) by Def1
.= Seg (len (F mod m)) by NEWTON:2
.= Seg (len F) by Def1
.= dom F by FINSEQ_1:def_3 ;
hence (a * (F mod m)) mod m = (a * F) mod m by A5, A3, FUNCT_1:2; ::_thesis: verum
end;
theorem :: EULER_2:15
for m being Nat
for F, G being FinSequence of NAT holds (F ^ G) mod m = (F mod m) ^ (G mod m)
proof
let m be Nat; ::_thesis: for F, G being FinSequence of NAT holds (F ^ G) mod m = (F mod m) ^ (G mod m)
let F, G be FinSequence of NAT ; ::_thesis: (F ^ G) mod m = (F mod m) ^ (G mod m)
A1: dom ((F ^ G) mod m) = Seg (len ((F ^ G) mod m)) by FINSEQ_1:def_3
.= Seg (len (F ^ G)) by Def1
.= dom (F ^ G) by FINSEQ_1:def_3 ;
A2: dom (G mod m) = Seg (len (G mod m)) by FINSEQ_1:def_3
.= Seg (len G) by Def1
.= dom G by FINSEQ_1:def_3 ;
A3: dom (F mod m) = Seg (len (F mod m)) by FINSEQ_1:def_3
.= Seg (len F) by Def1
.= dom F by FINSEQ_1:def_3 ;
A4: for x being set st x in dom (F ^ G) holds
((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x
proof
let x be set ; ::_thesis: ( x in dom (F ^ G) implies ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x )
assume A5: x in dom (F ^ G) ; ::_thesis: ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x
then reconsider x = x as Element of NAT ;
now__::_thesis:_((F_^_G)_mod_m)_._x_=_((F_mod_m)_^_(G_mod_m))_._x
percases ( x in dom F or ex n being Nat st
( n in dom G & x = (len F) + n ) ) by A5, FINSEQ_1:25;
supposeA6: x in dom F ; ::_thesis: ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x
A7: ((F ^ G) mod m) . x = ((F ^ G) . x) mod m by A5, Def1
.= (F . x) mod m by A6, FINSEQ_1:def_7 ;
((F mod m) ^ (G mod m)) . x = (F mod m) . x by A3, A6, FINSEQ_1:def_7
.= (F . x) mod m by A6, Def1 ;
hence ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x by A7; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom G & x = (len F) + n ) ; ::_thesis: ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x
then consider n being Element of NAT such that
A8: n in dom G and
A9: x = (len F) + n ;
A10: ((F ^ G) mod m) . x = ((F ^ G) . x) mod m by A5, Def1
.= (G . n) mod m by A8, A9, FINSEQ_1:def_7 ;
len (F mod m) = len F by Def1;
then ((F mod m) ^ (G mod m)) . x = (G mod m) . n by A2, A8, A9, FINSEQ_1:def_7
.= (G . n) mod m by A8, Def1 ;
hence ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x by A10; ::_thesis: verum
end;
end;
end;
hence ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x ; ::_thesis: verum
end;
dom ((F mod m) ^ (G mod m)) = Seg (len ((F mod m) ^ (G mod m))) by FINSEQ_1:def_3
.= Seg ((len (F mod m)) + (len (G mod m))) by FINSEQ_1:22
.= Seg ((len F) + (len (G mod m))) by Def1
.= Seg ((len F) + (len G)) by Def1
.= Seg (len (F ^ G)) by FINSEQ_1:22
.= dom (F ^ G) by FINSEQ_1:def_3 ;
hence (F ^ G) mod m = (F mod m) ^ (G mod m) by A1, A4, FUNCT_1:2; ::_thesis: verum
end;
theorem :: EULER_2:16
for a, m being Nat
for F, G being FinSequence of NAT holds (a * (F ^ G)) mod m = ((a * F) mod m) ^ ((a * G) mod m)
proof
let a, m be Nat; ::_thesis: for F, G being FinSequence of NAT holds (a * (F ^ G)) mod m = ((a * F) mod m) ^ ((a * G) mod m)
let F, G be FinSequence of NAT ; ::_thesis: (a * (F ^ G)) mod m = ((a * F) mod m) ^ ((a * G) mod m)
reconsider FG = F ^ G as FinSequence of NAT ;
A1: dom (a * (F ^ G)) = Seg (len (a * FG)) by FINSEQ_1:def_3
.= Seg (len FG) by NEWTON:2
.= dom (F ^ G) by FINSEQ_1:def_3 ;
A2: dom (a * G) = Seg (len (a * G)) by FINSEQ_1:def_3
.= Seg (len G) by NEWTON:2
.= dom G by FINSEQ_1:def_3 ;
A3: dom ((a * G) mod m) = Seg (len ((a * G) mod m)) by FINSEQ_1:def_3
.= Seg (len (a * G)) by Def1
.= Seg (len G) by NEWTON:2
.= dom G by FINSEQ_1:def_3 ;
A4: dom (a * F) = Seg (len (a * F)) by FINSEQ_1:def_3
.= Seg (len F) by NEWTON:2
.= dom F by FINSEQ_1:def_3 ;
A5: dom ((a * F) mod m) = Seg (len ((a * F) mod m)) by FINSEQ_1:def_3
.= Seg (len (a * F)) by Def1
.= Seg (len F) by NEWTON:2
.= dom F by FINSEQ_1:def_3 ;
A6: for x being set st x in dom (F ^ G) holds
((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x
proof
reconsider H = F ^ G as FinSequence of NAT ;
let x be set ; ::_thesis: ( x in dom (F ^ G) implies ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x )
assume A7: x in dom (F ^ G) ; ::_thesis: ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x
then reconsider x = x as Element of NAT ;
now__::_thesis:_((a_*_(F_^_G))_mod_m)_._x_=_(((a_*_F)_mod_m)_^_((a_*_G)_mod_m))_._x
percases ( x in dom F or ex n being Nat st
( n in dom G & x = (len F) + n ) ) by A7, FINSEQ_1:25;
supposeA8: x in dom F ; ::_thesis: ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x
A9: ((a * (F ^ G)) mod m) . x = ((a * (F ^ G)) . x) mod m by A1, A7, Def1
.= (a * (H . x)) mod m by RVSUM_1:44
.= (a * (F . x)) mod m by A8, FINSEQ_1:def_7 ;
(((a * F) mod m) ^ ((a * G) mod m)) . x = ((a * F) mod m) . x by A5, A8, FINSEQ_1:def_7
.= ((a * F) . x) mod m by A4, A8, Def1
.= (a * (F . x)) mod m by RVSUM_1:44 ;
hence ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x by A9; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom G & x = (len F) + n ) ; ::_thesis: ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x
then consider n being Element of NAT such that
A10: n in dom G and
A11: x = (len F) + n ;
A12: ((a * (F ^ G)) mod m) . x = ((a * (F ^ G)) . x) mod m by A1, A7, Def1
.= (a * (H . x)) mod m by RVSUM_1:44
.= (a * (G . n)) mod m by A10, A11, FINSEQ_1:def_7 ;
len ((a * F) mod m) = len (a * F) by Def1
.= len F by NEWTON:2 ;
then (((a * F) mod m) ^ ((a * G) mod m)) . x = ((a * G) mod m) . n by A3, A10, A11, FINSEQ_1:def_7
.= ((a * G) . n) mod m by A2, A10, Def1
.= (a * (G . n)) mod m by RVSUM_1:44 ;
hence ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x by A12; ::_thesis: verum
end;
end;
end;
hence ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x ; ::_thesis: verum
end;
A13: dom ((a * (F ^ G)) mod m) = Seg (len ((a * FG) mod m)) by FINSEQ_1:def_3
.= Seg (len (a * FG)) by Def1
.= Seg (len FG) by NEWTON:2
.= dom (F ^ G) by FINSEQ_1:def_3 ;
dom (((a * F) mod m) ^ ((a * G) mod m)) = Seg (len (((a * F) mod m) ^ ((a * G) mod m))) by FINSEQ_1:def_3
.= Seg ((len ((a * F) mod m)) + (len ((a * G) mod m))) by FINSEQ_1:22
.= Seg ((len (a * F)) + (len ((a * G) mod m))) by Def1
.= Seg ((len (a * F)) + (len (a * G))) by Def1
.= Seg ((len F) + (len (a * G))) by NEWTON:2
.= Seg ((len F) + (len G)) by NEWTON:2
.= Seg (len (F ^ G)) by FINSEQ_1:22
.= dom (F ^ G) by FINSEQ_1:def_3 ;
hence (a * (F ^ G)) mod m = ((a * F) mod m) ^ ((a * G) mod m) by A13, A6, FUNCT_1:2; ::_thesis: verum
end;
theorem :: EULER_2:17
for a, m being Nat st a <> 0 & m <> 0 & a,m are_relative_prime holds
for b being Nat holds a |^ b,m are_relative_prime
proof
let a, m be Nat; ::_thesis: ( a <> 0 & m <> 0 & a,m are_relative_prime implies for b being Nat holds a |^ b,m are_relative_prime )
defpred S1[ Nat] means a |^ $1,m are_relative_prime ;
assume A1: ( a <> 0 & m <> 0 & a,m are_relative_prime ) ; ::_thesis: for b being Nat holds a |^ b,m are_relative_prime
A2: for b being Nat st S1[b] holds
S1[b + 1]
proof
let b be Nat; ::_thesis: ( S1[b] implies S1[b + 1] )
A3: a |^ (b + 1) = (a |^ b) * (a |^ 1) by NEWTON:8
.= (a |^ b) * a by NEWTON:5 ;
assume a |^ b,m are_relative_prime ; ::_thesis: S1[b + 1]
hence S1[b + 1] by A1, A3, EULER_1:14; ::_thesis: verum
end;
( (a |^ 0) gcd m = 1 gcd m & m gcd 1 = 1 ) by NEWTON:4, NEWTON:51;
then A4: S1[ 0 ] by INT_2:def_3;
for b being Nat holds S1[b] from NAT_1:sch_2(A4, A2);
hence for b being Nat holds a |^ b,m are_relative_prime ; ::_thesis: verum
end;
begin
theorem Th18: :: EULER_2:18
for a, m being Nat st a <> 0 & m > 1 & a,m are_relative_prime holds
(a |^ (Euler m)) mod m = 1
proof
let a, m be Nat; ::_thesis: ( a <> 0 & m > 1 & a,m are_relative_prime implies (a |^ (Euler m)) mod m = 1 )
assume that
A1: a <> 0 and
A2: m > 1 and
A3: a,m are_relative_prime ; ::_thesis: (a |^ (Euler m)) mod m = 1
set X = { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ;
A4: a |^ (Euler m) <> 0 by A1, PREPOWER:5;
set Y = { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } ;
A5: for x being Nat st x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } holds
(a * x) mod m in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) }
proof
let x be Nat; ::_thesis: ( x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } implies (a * x) mod m in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } )
assume x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ; ::_thesis: (a * x) mod m in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) }
then consider t being Element of NAT such that
A6: t = x and
A7: m,t are_relative_prime and
A8: t >= 1 and
t <= m ;
A9: a * t,m are_relative_prime by A1, A2, A3, A7, EULER_1:14;
(a * t) mod m <> 0
proof
assume (a * t) mod m = 0 ; ::_thesis: contradiction
then consider s being Nat such that
A10: a * t = (m * s) + 0 and
0 < m by A2, NAT_D:def_2;
s gcd 1 = 1 by NEWTON:51;
then (m * s) gcd (m * 1) = m by EULER_1:5;
hence contradiction by A2, A9, A10, INT_2:def_3; ::_thesis: verum
end;
then A11: (a * t) mod m >= 1 by NAT_1:14;
A12: (a * t) mod m <= m by A2, NAT_D:1;
m,(a * t) mod m are_relative_prime by A1, A2, A3, A7, A8, Th3;
hence (a * x) mod m in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } by A6, A11, A12; ::_thesis: verum
end;
A13: { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } = { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) }
proof
thus { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } c= { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } :: according to XBOOLE_0:def_10 ::_thesis: { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } c= { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } or x in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } )
assume x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ; ::_thesis: x in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) }
then consider xx being Element of NAT such that
A14: x = xx and
A15: m,xx are_relative_prime and
xx >= 1 and
A16: xx <= m ;
consider i, j being Integer such that
A17: (i * a) + (j * m) = xx by A3, EULER_1:10;
xx <> m by A2, A15, EULER_1:1;
then xx < m by A16, XXREAL_0:1;
then A18: xx mod m = xx by NAT_D:24;
reconsider im = i mod m as Element of NAT by INT_1:3, NEWTON:64;
i mod m <> 0
proof
assume i mod m = 0 ; ::_thesis: contradiction
then 0 = i - ((i div m) * m) by A2, INT_1:def_10;
then m gcd xx = (m * 1) gcd (m * (((i div m) * a) + j)) by A17
.= m * (1 gcd (((i div m) * a) + j)) by A2, EULER_1:15
.= m * 1 by Lm3
.= m ;
hence contradiction by A2, A15, INT_2:def_3; ::_thesis: verum
end;
then A19: im >= 1 by NAT_1:14;
A20: i = ((i div m) * m) + (i mod m) by A2, NEWTON:66;
then reconsider ij = ((i mod m) * a) + ((((i div m) * a) + j) * m) as Element of NAT by A17;
A21: im <= m by A2, NEWTON:65;
A22: ij mod m = (im * a) mod m by EULER_1:12;
then m,im are_relative_prime by A2, A15, A18, A17, A20, Th4;
then im in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } by A19, A21;
hence x in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } by A14, A18, A17, A20, A22; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } or y in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } )
assume y in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } ; ::_thesis: y in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) }
then ex yy being Element of NAT st
( y = yy & ex u being Element of NAT st
( yy = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) ) ;
hence y in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } by A5; ::_thesis: verum
end;
A23: for xi, xj being Nat st xi in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } & xj in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } & xi <> xj holds
(a * xi) mod m <> (a * xj) mod m
proof
let xi, xj be Nat; ::_thesis: ( xi in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } & xj in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } & xi <> xj implies (a * xi) mod m <> (a * xj) mod m )
assume that
A24: xi in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } and
A25: xj in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } and
A26: xi <> xj ; ::_thesis: (a * xi) mod m <> (a * xj) mod m
set tm = (a * xi) mod m;
set sm = (a * xj) mod m;
assume A27: (a * xi) mod m = (a * xj) mod m ; ::_thesis: contradiction
consider s being Element of NAT such that
A28: s = xj and
m,s are_relative_prime and
A29: ( s >= 1 & s <= m ) by A25;
A30: (a * xj) mod m = (a * s) - (m * ((a * s) div m)) by A2, A28, NEWTON:63;
consider t being Element of NAT such that
A31: t = xi and
m,t are_relative_prime and
A32: ( t >= 1 & t <= m ) by A24;
(a * xi) mod m = (a * t) - (m * ((a * t) div m)) by A2, A31, NEWTON:63;
then 0 = (a * (t - s)) - (m * (((a * t) div m) - ((a * s) div m))) by A27, A30;
then A33: m divides a * (t - s) by INT_1:def_3;
reconsider m = m, c = t - s as Integer ;
( 1 - m <= c & c <= m - 1 ) by A32, A29, XREAL_1:13;
then t - s = 0 by A3, A33, Lm4, INT_2:25;
hence contradiction by A26, A31, A28; ::_thesis: verum
end;
reconsider FX = Sgm { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } as FinSequence of NAT ;
reconsider FYY = a * FX as FinSequence of NAT ;
reconsider FY = FYY mod m as FinSequence of NAT ;
A34: { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } c= Seg m
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } or x in Seg m )
assume x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ; ::_thesis: x in Seg m
then ex xx being Element of NAT st
( x = xx & m,xx are_relative_prime & xx >= 1 & xx <= m ) ;
hence x in Seg m by FINSEQ_1:1; ::_thesis: verum
end;
then reconsider X = { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } as finite set ;
dom FYY = Seg (len FYY) by FINSEQ_1:def_3
.= Seg (len FX) by NEWTON:2 ;
then A35: dom FX = dom FYY by FINSEQ_1:def_3;
A36: dom FY = Seg (len FY) by FINSEQ_1:def_3
.= Seg (len FYY) by Def1
.= Seg (len FX) by NEWTON:2 ;
then A37: dom FX = dom FY by FINSEQ_1:def_3;
A38: rng FY = { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) }
proof
thus rng FY c= { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } :: according to XBOOLE_0:def_10 ::_thesis: { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } c= rng FY
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng FY or x in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } )
assume x in rng FY ; ::_thesis: x in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) }
then consider y being set such that
A39: y in dom FY and
A40: x = FY . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A39;
FX . y in rng FX by A37, A39, FUNCT_1:def_3;
then A41: FX . y in X by A34, FINSEQ_1:def_13;
y in dom FX by A36, A39, FINSEQ_1:def_3;
then FY . y = (FYY . y) mod m by A35, Def1
.= (a * (FX . y)) mod m by RVSUM_1:44 ;
hence x in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } by A40, A41; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } or y in rng FY )
assume y in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } ; ::_thesis: y in rng FY
then consider yy being Element of NAT such that
A42: y = yy and
A43: ex u being Element of NAT st
( yy = (a * u) mod m & u in X ) ;
consider uu being Element of NAT such that
A44: yy = (a * uu) mod m and
A45: uu in X by A43;
uu in rng FX by A34, A45, FINSEQ_1:def_13;
then consider xx being set such that
A46: xx in dom FX and
A47: uu = FX . xx by FUNCT_1:def_3;
reconsider xx = xx as Element of NAT by A46;
FY . xx = (FYY . xx) mod m by A35, A46, Def1
.= y by A42, A44, A47, RVSUM_1:44 ;
hence y in rng FY by A37, A46, FUNCT_1:def_3; ::_thesis: verum
end;
A48: FY is one-to-one
proof
A49: FX is one-to-one by A34, FINSEQ_3:92;
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom FY or not x2 in dom FY or not FY . x1 = FY . x2 or x1 = x2 )
assume that
A50: x1 in dom FY and
A51: x2 in dom FY and
A52: FY . x1 = FY . x2 ; ::_thesis: x1 = x2
A53: x2 in dom FX by A36, A51, FINSEQ_1:def_3;
reconsider x2 = x2 as Element of NAT by A51;
A54: x1 in dom FX by A36, A50, FINSEQ_1:def_3;
reconsider x1 = x1 as Element of NAT by A50;
A55: ( FX . x1 in rng FX & FX . x2 in rng FX ) by A37, A50, A51, FUNCT_1:def_3;
A56: FY . x2 = (FYY . x2) mod m by A35, A53, Def1
.= (a * (FX . x2)) mod m by RVSUM_1:44 ;
FY . x1 = (FYY . x1) mod m by A35, A54, Def1
.= (a * (FX . x1)) mod m by RVSUM_1:44 ;
then ( not FX . x1 in X or not FX . x2 in X or not FX . x1 <> FX . x2 ) by A23, A52, A56;
hence x1 = x2 by A34, A54, A53, A55, A49, FINSEQ_1:def_13, FUNCT_1:def_4; ::_thesis: verum
end;
for x being set holds card (Coim (FX,x)) = card (Coim (FY,x))
proof
let x be set ; ::_thesis: card (Coim (FX,x)) = card (Coim (FY,x))
now__::_thesis:_card_(Coim_(FX,x))_=_card_(Coim_(FY,x))
percases ( x in X or not x in X ) ;
supposeA57: x in X ; ::_thesis: card (Coim (FX,x)) = card (Coim (FY,x))
A58: FX is one-to-one by A34, FINSEQ_3:92;
x in rng FX by A34, A57, FINSEQ_1:def_13;
then A59: len (FX - {x}) = (len FX) - 1 by A58, FINSEQ_3:90;
A60: ( (len (FX - {x})) - (len (FX - {x})) = ((len FX) - (card (FX " {x}))) - (len (FX - {x})) & len (FY - {x}) = (len FY) - (card (FY " {x})) ) by FINSEQ_3:59;
len (FY - {x}) = (len FY) - 1 by A13, A38, A48, A57, FINSEQ_3:90;
hence card (Coim (FX,x)) = card (Coim (FY,x)) by A59, A60; ::_thesis: verum
end;
suppose not x in X ; ::_thesis: card (Coim (FX,x)) = card (Coim (FY,x))
then ( not x in rng FX & FY " {x} = {} ) by A13, A34, A38, FINSEQ_1:def_13, FUNCT_1:72;
hence card (Coim (FX,x)) = card (Coim (FY,x)) by FUNCT_1:72; ::_thesis: verum
end;
end;
end;
hence card (Coim (FX,x)) = card (Coim (FY,x)) ; ::_thesis: verum
end;
then A61: FX,FY are_fiberwise_equipotent by CLASSES1:def_9;
then A62: len FX = len FY by RFINSEQ:3;
A63: (Product FY) mod m = ((a |^ (len FY)) * (Product FX)) mod m
proof
defpred S1[ Nat] means ( $1 <= len FY implies (Product (FY | $1)) mod m = ((a |^ (len (FY | $1))) * (Product (FX | $1))) mod m );
FY | (len FY) = FY | (Seg (len FY)) by FINSEQ_1:def_15;
then A64: FY = FY | (len FY) by FINSEQ_2:20;
A65: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
now__::_thesis:_(_S1[n]_implies_S1[n_+_1]_)
percases ( n + 1 <= len FY or n + 1 > len FY ) ;
supposeA66: n + 1 <= len FY ; ::_thesis: ( S1[n] implies S1[n + 1] )
then len (FX | (n + 1)) = n + 1 by A62, FINSEQ_1:59;
then A67: FX | (n + 1) = ((FX | (n + 1)) | n) ^ <*((FX | (n + 1)) . (n + 1))*> by RFINSEQ:7;
assume A68: S1[n] ; ::_thesis: S1[n + 1]
0 + 1 <= n + 1 by NAT_1:13;
then A69: n + 1 in dom FY by A66, FINSEQ_3:25;
A70: (FY | (n + 1)) . (n + 1) = FY . (n + 1) by FINSEQ_3:112;
A71: (FX | (n + 1)) . (n + 1) = FX . (n + 1) by FINSEQ_3:112;
A72: n <= n + 1 by NAT_1:11;
then A73: len (FY | n) = n by A66, FINSEQ_1:59, XXREAL_0:2;
A74: (FX | (n + 1)) | n = FX | n by A72, FINSEQ_5:77;
A75: (FY | (n + 1)) | n = FY | n by A72, FINSEQ_5:77;
A76: len (FY | (n + 1)) = n + 1 by A66, FINSEQ_1:59;
then FY | (n + 1) = ((FY | (n + 1)) | n) ^ <*((FY | (n + 1)) . (n + 1))*> by RFINSEQ:7;
then (Product (FY | (n + 1))) mod m = ((Product (FY | n)) * (FY . (n + 1))) mod m by A75, A70, RVSUM_1:96
.= ((((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * ((FY . (n + 1)) mod m)) mod m by A66, A68, A72, Th9, XXREAL_0:2
.= ((((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * (((FYY . (n + 1)) mod m) mod m)) mod m by A37, A35, A69, Def1
.= ((((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * (((a * FX) . (n + 1)) mod m)) mod m by Th5
.= (((a |^ (len (FY | n))) * (Product (FX | n))) * ((a * FX) . (n + 1))) mod m by Th9
.= (((a |^ n) * (Product (FX | n))) * (a * (FX . (n + 1)))) mod m by A73, RVSUM_1:44
.= (((a |^ n) * a) * ((Product (FX | n)) * (FX . (n + 1)))) mod m
.= ((a |^ (len (FY | (n + 1)))) * ((Product (FX | n)) * (FX . (n + 1)))) mod m by A76, NEWTON:6
.= ((a |^ (len (FY | (n + 1)))) * (Product (FX | (n + 1)))) mod m by A67, A74, A71, RVSUM_1:96 ;
hence S1[n + 1] ; ::_thesis: verum
end;
suppose n + 1 > len FY ; ::_thesis: ( S1[n] implies S1[n + 1] )
hence ( S1[n] implies S1[n + 1] ) ; ::_thesis: verum
end;
end;
end;
hence ( S1[n] implies S1[n + 1] ) ; ::_thesis: verum
end;
FX | (len FX) = FX | (Seg (len FX)) by FINSEQ_1:def_15;
then A77: FX = FX | (len FY) by A62, FINSEQ_2:20;
A78: S1[ 0 ] by NEWTON:4, RVSUM_1:94;
for n being Nat holds S1[n] from NAT_1:sch_2(A78, A65);
hence (Product FY) mod m = ((a |^ (len FY)) * (Product FX)) mod m by A64, A77; ::_thesis: verum
end;
A79: Product FX,m are_relative_prime
proof
defpred S1[ Nat] means ( $1 <= len FX implies Product (FX | $1),m are_relative_prime );
A80: FX | (len FX) = FX by FINSEQ_1:58;
A81: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
now__::_thesis:_(_S1[n]_implies_S1[n_+_1]_)
percases ( len FX >= n + 1 or len FX < n + 1 ) ;
supposeA82: len FX >= n + 1 ; ::_thesis: ( S1[n] implies S1[n + 1] )
reconsider FF = FX | (n + 1) as FinSequence of NAT ;
reconsider ff = FF . (n + 1) as Element of NAT ;
len FF = n + 1 by A82, FINSEQ_1:59;
then A83: FF = (FF | n) ^ <*ff*> by RFINSEQ:7;
reconsider a = Product (FF | n), b = ff, m9 = m as Integer ;
A84: n <= n + 1 by NAT_1:11;
0 + 1 <= n + 1 by XREAL_1:6;
then ( (FX | (n + 1)) . (n + 1) = FX . (n + 1) & n + 1 in dom FX ) by A82, FINSEQ_3:25, FINSEQ_3:112;
then A85: (FX | (n + 1)) . (n + 1) in rng FX by FUNCT_1:def_3;
rng FX = X by A34, FINSEQ_1:def_13;
then A86: ex p being Element of NAT st
( ff = p & m,p are_relative_prime & p >= 1 & p <= m ) by A85;
assume S1[n] ; ::_thesis: S1[n + 1]
then a,m9 are_relative_prime by A82, A84, FINSEQ_5:77, XXREAL_0:2;
then a * b,m9 are_relative_prime by A86, INT_2:26;
hence S1[n + 1] by A83, RVSUM_1:96; ::_thesis: verum
end;
suppose len FX < n + 1 ; ::_thesis: ( S1[n] implies S1[n + 1] )
hence ( S1[n] implies S1[n + 1] ) ; ::_thesis: verum
end;
end;
end;
hence ( S1[n] implies S1[n + 1] ) ; ::_thesis: verum
end;
(Product (FX | 0)) gcd m = 1 by NEWTON:51, RVSUM_1:94;
then A87: S1[ 0 ] by INT_2:def_3;
for n being Nat holds S1[n] from NAT_1:sch_2(A87, A81);
hence Product FX,m are_relative_prime by A80; ::_thesis: verum
end;
len FX = card X by A34, FINSEQ_3:39
.= Euler m by EULER_1:def_1 ;
then A88: len FY = Euler m by A61, RFINSEQ:3;
(Product FX) mod m = (Product FY) mod m by A61, Th10;
hence (a |^ (Euler m)) mod m = 1 by A2, A63, A88, A4, A79, Th12; ::_thesis: verum
end;
theorem :: EULER_2:19
for a, m being Nat st a <> 0 & m is prime & a,m are_relative_prime holds
(a |^ m) mod m = a mod m
proof
let a, m be Nat; ::_thesis: ( a <> 0 & m is prime & a,m are_relative_prime implies (a |^ m) mod m = a mod m )
assume that
A1: a <> 0 and
A2: m is prime and
A3: a,m are_relative_prime ; ::_thesis: (a |^ m) mod m = a mod m
A4: m > 1 by A2, INT_2:def_4;
then m - 1 > 1 - 1 by XREAL_1:9;
then reconsider mm = m - 1 as Element of NAT by INT_1:3;
Euler m = m - 1 by A2, EULER_1:20;
then ((a |^ mm) mod m) * a = 1 * a by A1, A3, A4, Th18;
then ( mm + 1 = m & ((a |^ mm) * a) mod m = a mod m ) by Th7;
hence (a |^ m) mod m = a mod m by NEWTON:6; ::_thesis: verum
end;