:: Basic Properties of Primitive Root and Order Function
:: by Na Ma and Xiquan Liang
::
:: Received August 6, 2012
:: Copyright (c) 2012 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, INT_1, NAT_1, SUBSET_1, EQREL_1, EULER_1, FINSEQ_1,
INT_4, MEMBER_1, TARSKI, REAL_1, ARYTM_3, FUNCT_1, RELAT_1, FINSET_1,
CARD_1, XBOOLE_0, ARYTM_1, INT_2, XXREAL_0, COMPLEX1, NEWTON, SQUARE_1,
PARTFUN1, INT_8, PEPIN, INT_5, POLYEQ_3, ABIAN, CARD_3, ORDINAL4,
CFUNCT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, NUMBERS, ORDINAL1, XXREAL_0,
XCMPLX_0, XREAL_0, INT_1, NAT_1, INT_2, NAT_D, FUNCT_1, FINSEQ_1,
RELSET_1, EULER_1, TREES_4, EQREL_1, PARTFUN1, FINSET_1, WSIERP_1,
NEWTON, MEMBER_1, ABIAN, PEPIN, INT_4, INT_5, POLYEQ_3;
constructors EULER_1, WSIERP_1, PEPIN, NAT_3, NAT_D, INTEGRA2, RELSET_1,
ABIAN, INT_4, INT_5, POLYEQ_3;
registrations RELAT_1, FINSEQ_1, CARD_1, NAT_1, INT_1, MEMBERED, FINSET_1,
SEQM_3, NEWTON, NAT_3, XXREAL_0, NUMBERS, XBOOLE_0, XREAL_0, ORDINAL1,
VALUED_0, ABIAN, MEMBER_1, XCMPLX_0, WSIERP_1, INT_4;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, SQUARE_1, FINSEQ_1, EULER_1, POLYEQ_3, XBOOLE_0;
theorems ORDINAL1, NAT_1, NAT_2, INT_1, INT_2, FINSEQ_1, CARD_2, INT_5,
EULER_1, EULER_2, NEWTON, XCMPLX_1, XREAL_1, RELAT_1, ABIAN, STIRL2_1,
XXREAL_0, NAT_D, PEPIN, NAT_4, WSIERP_1, FINSEQ_3, INT_4, PYTHTRIP,
ABSVALUE, FINSEQ_2, FINSEQ_4, FUNCT_1, MEMBER_1, FINSEQ_5, XBOOLE_1,
XREAL_0, SEQ_2, XBOOLE_0, EQREL_1, NUMBERS, RVSUM_1;
schemes NAT_1, FINSEQ_1, FINSEQ_2;
begin
reserve i,s,t,m,n,k for Nat,
c,d,e for Element of NAT,
fn for FinSequence of NAT,
x,y for Integer;
definition ::: should be moved to EULER_1
let m be Nat;
func RelPrimes(m) -> set equals
{k where k is Element of NAT:m,k are_relative_prime & 1<=k & k<=m};
correctness;
end;
theorem TH13:
RelPrimes(m) c= Seg m
proof
let x be element;
assume x in RelPrimes(m);
then ex k be Element of NAT st
k = x & m,k are_relative_prime & k >= 1 & k <= m;
hence x in Seg m;
end;
definition
let m be Nat;
redefine func RelPrimes(m) -> Subset of NAT;
coherence
proof
RelPrimes(m) c= Seg m by TH13;
hence thesis by XBOOLE_1:1;
end;
end;
registration
let m be Nat;
cluster RelPrimes(m) -> finite;
coherence
proof
RelPrimes(m) c= Seg m by TH13;
hence thesis;
end;
end;
theorem
1<=m implies RelPrimes(m) <> {}
proof
assume A1:1<=m;
m gcd 1 = 1 by NEWTON:51;
then m,1 are_relative_prime by INT_2:def 3;
then 1 in RelPrimes(m) by A1;
hence thesis;
end;
theorem Th21:
for X being Subset of INT, a being Integer holds x in a ** X iff ex y
being Integer st y in X & x = a * y
proof
let X be Subset of INT, a be Integer;
hereby
assume x in a ** X;
then consider z being Complex such that
A2: x = a * z and
A1: z in X by MEMBER_1:195;
reconsider z as Integer by A1;
take z;
thus z in X & x = a * z by A1,A2;
end;
given y being Integer such that
A3: y in X & x = a * y;
thus thesis by MEMBER_1:193,A3;
end;
theorem Th30:
ex r be Nat st (1+s)|^t = 1 + t*s + (t choose 2)*s^2+r*s^3
proof
defpred P[Nat] means
ex r be Nat st (1+s)|^$1 = 1 + $1*s + ($1 choose 2)*s^2+r*s^3;
A2: for t be Nat st P[t] holds P[t+1]
proof let t be Nat;
assume P[t];
then consider r1 be Nat such that
A3: (1+s)|^t = 1 + t*s + (t choose 2)*s^2 + r1*s^3;
(1+s)|^(t+1)
= (1 + t*s + (t choose 2)*s^2 + r1*s^3)*(1+s) by A3,NEWTON:6
.= 1+(t+1)*s +(t+(t choose 2))*s^2+r1*s^3+(t choose 2)*s^2*s+r1*s^3*s
.= 1+(t+1)*s +(t+t*(t-1)/2)*s^2+r1*s^3+(t choose 2)*s^2*s
+r1*s^3*s by STIRL2_1:51
.= 1+(t+1)*s +(t+1)*((t+1)-1)/2*s^2+r1*s^3+(t choose 2)*s^2*s+r1*s^3*s
.=1+(t+1)*s +((t+1) choose 2)*s^2+r1*s^3+(t choose 2)*s^3+r1*s^3*s
by STIRL2_1:51
.= 1+(t+1)*s +((t+1) choose 2)*s^2+(r1+(t choose 2)+r1*s)*s^3;
hence thesis;
end;
A1:P[0]
proof
reconsider z = 0 as Element of NAT;
take r = 0;
1 + z *s + (z choose 2) *s^2+r *s^3 = 1 + z *s + z *s^2+r *s^3
by NEWTON:def 3
.= (1+s)|^z by NEWTON:4;
hence thesis;
end;
for t be Nat holds P[t] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th1:
n>1 & i,n are_relative_prime implies i <> 0
proof
assume A1:n>1 & i,n are_relative_prime;
assume i = 0;
then i gcd n > 1 by A1,NEWTON:52;
hence contradiction by A1,INT_2:def 3;
end;
theorem Th12:
for a,b be Integer,m be Nat st a*b mod m = 1 & a mod m = 1
holds b mod m = 1
proof let a,b be Integer,m be Nat;
assume A1:a*b mod m = 1 & a mod m = 1;
then A2:m <> 0 by INT_1:def 10;
then a mod m = 1 mod m by A1,PEPIN:5,INT_1:58;
then a*b,1*b are_congruent_mod m by INT_4:11,A2,NAT_D:64;
hence thesis by A1,NAT_D:64;
end;
Lm2:
for x be Integer holds 2 divides x*(x+1)
proof let x be Integer;
per cases;
suppose x is even;
hence thesis by ABIAN:def 1;
end;
suppose x is odd;
then consider y be Integer such that A2:x = 2*y+1 by ABIAN:1;
x*(x+1) = 2*((2*y+1)*(y+1)) by A2;
hence thesis by INT_1:def 3;
end;
end;
theorem Th22:
for x be odd Integer,k be Nat st k>=3 holds x|^(2|^(k-'2)) mod 2|^k = 1
proof let x be odd Integer,k be Nat;
assume A1: k>=3;
defpred X[Nat] means x|^(2|^($1-'2)) mod 2|^$1 = 1;
consider y be Integer such that A2: x = 2*y+1 by ABIAN:1;
A3: X[3]
proof
3-'2 = 3-2 by XREAL_1:233
.= 1;
then A4:x|^(2|^(3-'2)) mod 2|^3
= x|^2 mod 2|^3 by NEWTON:5
.= x^2 mod 2|^3 by NEWTON:81;
A5: x^2-1 = 2^2*(y*(y+1)) by A2;
2 divides y*(y+1) by Lm2;
then 2^2*2 divides (x^2-1) by A5,INT_4:7;
then 2|^2*2 divides (x^2-1) by NEWTON:81;
then 2|^(2+1) divides (x^2-1) by NEWTON:6;then
A6: x^2,1 are_congruent_mod 2|^3 by INT_2:15;
2*2*2>1;
then 2|^2*2>1 by NEWTON:81;
then 2|^(2+1)>1 by NEWTON:6;
hence thesis by A4,A6,PEPIN:39;
end;
A7: for k be Nat st k>=3 & X[k] holds X[k+1]
proof let k be Nat;
assume A8:k>=3 & X[k];
A10: k>0 & k>1 & k>2 by A8,XXREAL_0:2;
B:k-'3+1=k+1-'3 by A8,NAT_D:38
.=k+1-3 by A8,NAT_D:37
.=k-2;
k-'2 = k-2 by A10,XREAL_1:233;
then A16:x|^(2|^(k-'2)) = x|^(2|^(k-'3)*2) by B,NEWTON:6
.= x|^2|^(2|^(k-'3)) by NEWTON:9
.= x^2|^(2|^(k-'3)) by NEWTON:81;
2|^k > 1 by A8,PEPIN:25;
then x|^(2|^(k-'2)),1 are_congruent_mod 2|^k by A8,A16,PEPIN:39;
then consider t be Integer such that
A11: x|^(2|^(k-'2)) - 1 = 2|^k * t by INT_1:def 3,INT_2:15;
(x|^(2|^(k-'2)))^2 = (x|^(2|^(k-'2)))|^2 by NEWTON:81
.= x|^(2|^(k-'2)*2) by NEWTON:9 .= x|^(2|^((k-'2)+1)) by NEWTON:6;
then A12: x|^(2|^((k-'2)+1)) = (t*2|^k + 1)^2 by A11
.= t^2*(2|^k)^2 + 2*(t*2|^k) + 1
.= t^2*(2|^k)|^2 + 2*(t*2|^k) + 1 by NEWTON:81
.= t^2*(2|^(2*k)) + 2*2|^k*t + 1 by NEWTON:9
.= (t^2*(2|^(2*k)) + 2|^(k+1)*t) + 1 by NEWTON:6;
k+k>k+1 by A10,XREAL_1:8;
then
A13: 2|^(k+1) divides t^2*(2|^(2*k)) by NAT_D:9,PEPIN:31;
2|^(k+1) divides 2|^(k+1)*t by INT_2:2;then
A14: 2|^(k+1) divides (t^2*(2|^(2*k)) + 2|^(k+1)*t) by A13,WSIERP_1:4;
A17: (t^2*(2|^(2*k)) + 2|^(k+1)*t) mod 2|^(k+1) = 0 by A14,INT_1:62;
x|^(2|^((k+1)-'2)) mod 2|^(k+1)
= x|^(2|^((k-'2)+1)) mod 2|^(k+1) by NAT_D:38,A10
.= (((t^2*(2|^(2*k)) + 2|^(k+1)*t) mod 2|^(k+1)) + (1 mod 2|^(k+1)))
mod 2|^(k+1) by A12,NAT_D:66
.= 1 mod 2|^(k+1) by A17,NAT_D:65
.= 1 by PEPIN:5,25;
hence thesis;
end;
for k be Nat st k>=3 holds X[k] from NAT_1:sch 8(A3,A7);
hence thesis by A1;
end;
reserve p for Prime;
Lm:k <= n implies m |^ k divides m |^ n by NEWTON:89;
theorem Th19:
m>=1 implies Euler(p|^m) = p|^m - p|^(m-'1)
proof assume A0: m >= 1;
set X = {k where k is Element of NAT :
p|^m,k are_relative_prime & k >= 1 & k <= p|^m};
set X1 = {k where k is Element of NAT :
not p|^m,k are_relative_prime & k >= 1 & k <= p|^m};
set X2 = {k where k is Element of NAT :
not p,k are_relative_prime & k >= 1 & k <= p|^m};
set X3 = {k where k is Element of NAT :
p divides k & k >= 1 & k <= p|^m};
reconsider w = p|^(m-'1) as Element of NAT by ORDINAL1:def 12;
A8: X1 = X2
proof thus X1 c= X2
proof let a be element;
assume a in X1;
then consider b be Element of NAT such that
A3: b = a & not p|^m,b are_relative_prime & b >= 1 & b <= p|^m;
not p,b are_relative_prime by A3,WSIERP_1:10;
hence thesis by A3;
end;
let a be element;
assume a in X2;
then consider k be Element of NAT such that
A5: k = a & not p,k are_relative_prime & k >= 1 & k <= p|^m;
p gcd k = p by A5,PEPIN:2;then
A6: p divides k by NAT_D:def 5;
p|^1 divides p|^m by A0,NEWTON:89;then
A7: p divides p|^m by NEWTON:5;
now assume p|^m,k are_relative_prime;
then p = 1 by A6,A7,PYTHTRIP:def 1;
hence contradiction by INT_2:def 4;
end;
hence thesis by A5;
end;
A9: X2 = X3
proof thus X2 c= X3
proof let x be element;
assume x in X2;
then consider k be Element of NAT such that
A11: x = k & not p,k are_relative_prime & k >= 1 & k <= p|^m;
p gcd k = p by A11,PEPIN:2;
then p divides k by NAT_D:def 5;
hence thesis by A11;
end;
let x be element;
assume x in X3;
then consider k be Element of NAT such that
A12: x = k & p divides k & k >= 1 & k <= p|^m;
p gcd k = p by A12,NEWTON:49;
then p gcd k > 1 by INT_2:def 4;
then not p,k are_relative_prime by INT_2:def 3;
hence thesis by A12;
end;
X3 c= Seg(p|^m)
proof
let x be element;
assume x in X3;
then ex k be Element of NAT st
k = x & p divides k & k >= 1 & k <= p|^m;
hence x in Seg(p|^m);
end;
then reconsider X1,X2,X3 as finite Subset of NAT by A8,A9,XBOOLE_1:1;
deffunc F(Nat) = $1 * p;
consider f be FinSequence such that
A13:len f = w & for d be Nat st d in dom f holds f.d = F(d)
from FINSEQ_1:sch 2;
A14: rng f = X3
proof thus rng f c= X3
proof let a be element;
assume a in rng f;
then consider s be Nat such that
A16: s in dom f & f.s = a by FINSEQ_2:10;
A17: a = s * p by A16,A13;then
reconsider a as Element of NAT by ORDINAL1:def 12;
A18: p divides a by A17,NAT_D:def 3;
s in Seg w by A16,A13,FINSEQ_1:def 3;
then A19:s >= 1 & s <= w by FINSEQ_1:1;
p > 1 by INT_2:def 4;
then A20:s * p >= 1*1 by A19,XREAL_1:66;
s * p <= w * p by A19,XREAL_1:66;
then A:s * p <= p|^((m-'1) + 1) by NEWTON:6;
p|^((m-'1) + 1)=p|^(m + 1-'1 ) by A0,NAT_D:38
.=p|^m by NAT_D:34;
hence thesis by A17,A18,A20,A;
end;
let a be element;
assume a in X3;
then consider k be Element of NAT such that
A21: a = k & p divides k & k >= 1 & k <= p|^m;
consider t be Nat such that A22:k = p * t by A21,NAT_D:def 3;
t <> 0 by A22,A21;
then A23:t >= 1 by NAT_1:14;
p|^m = p|^(m + 1 -' 1) by NAT_D:34
.=p|^(m-'1+1) by A0,NAT_D:38
.=p|^(m-'1) * p by NEWTON:6;
then p * t / p <= p|^(m-'1) * p / p by XREAL_1:72,A21,A22;
then t <= w * p / p by XCMPLX_1:89;
then t <= w by XCMPLX_1:89;
then t in Seg w by A23;then
A24: t in dom f by A13,FINSEQ_1:def 3;
f.t = t * p by A24,A13;
hence thesis by A21,A22,A24,FUNCT_1:3;
end;
for a,b be set st a in dom f & b in dom f & f.a = f.b holds a = b
proof let a,b be set;
assume A25:a in dom f & b in dom f & f.a = f.b;
then reconsider a,b as Element of NAT;
f.a = a * p & f.b = b * p by A25,A13;
hence thesis by A25,XCMPLX_1:5;
end;
then f is one-to-one by FUNCT_1:def 4; then
A26:w = card X1 by A8,A9,A13,A14,FINSEQ_4:62;
A27: X1 c= Seg(p|^m)
proof let x be element;
assume x in X1;
then consider k be Element of NAT such that
A28: x = k & not p|^m,k are_relative_prime & k >= 1 & k <= p|^m;
thus thesis by A28;
end;
A38: X c= Seg(p|^m)
proof let x be element;
assume x in X;
then consider k be Element of NAT such that
A29: x = k & p|^m,k are_relative_prime & k >= 1 & k <= p|^m;
thus thesis by A29;
end;
then A30:X1 \/ X c= Seg(p|^m) by A27,XBOOLE_1:8;
reconsider X as finite Subset of NAT by A38,XBOOLE_1:1;
Seg(p|^m) c= X1 \/ X
proof let x be element;
assume A31:x in Seg(p|^m);
then reconsider x as Element of NAT;
A32: x >= 1 & x <= p|^m by A31,FINSEQ_1:1;
per cases;
suppose p|^m,x are_relative_prime;
then x in X by A32;
hence thesis by XBOOLE_0:def 3;
end;
suppose not p|^m,x are_relative_prime;
then x in X1 by A32;
hence thesis by XBOOLE_0:def 3;
end;
end;
then A33: X1 \/ X = Seg(p|^m) by A30,XBOOLE_0:def 10;
not ex x being set st x in X1 /\ X
proof assume ex x be set st x in X1 /\ X;
then consider x be set such that A34: x in X1 /\ X;
A35: x in X1 & x in X by A34,XBOOLE_0:def 4;
then consider k1 be Element of NAT such that
A36: x = k1 & not p|^m,k1 are_relative_prime & k1 >= 1 & k1 <= p|^m;
consider k2 be Element of NAT such that
A37: x = k2 & p|^m,k2 are_relative_prime & k2 >= 1 & k2 <= p|^m by A35;
thus contradiction by A36,A37;
end;
then X1 /\ X = {} by XBOOLE_0:def 1;
then X1 misses X by XBOOLE_0:def 7;
then card X1 + card X = card Seg(p|^m) by A33,CARD_2:40;
then w + card X = p|^m by A26,FINSEQ_1:57;
hence thesis;
end;
theorem
n>1 & i,n are_relative_prime implies order(i,n) divides Euler n
proof
assume
A1:n>1 & i,n are_relative_prime;
(i |^ Euler n) mod n = 1 by Th1,A1,EULER_2:18;
hence thesis by A1,PEPIN:47;
end;
theorem Th3:
for i,n st n>1 & i,n are_relative_prime holds
i|^s,i|^t are_congruent_mod n iff s,t are_congruent_mod order(i,n)
proof let i,n;
assume A1:n>1 & i,n are_relative_prime;
A7:i <> 0 & n > 0 by A1,Th1;
set R = order(i,n);
reconsider RR = R as Element of NAT;
thus i|^s,i|^t are_congruent_mod n implies s,t are_congruent_mod R
proof
assume B1:i|^s,i|^t are_congruent_mod n;
A4: i gcd n = 1 by A1,INT_2:def 3;
per cases by XXREAL_0:1;
suppose s = t;
hence thesis by INT_1:11;
end;
suppose s > t;
then consider l be Nat such that A2: s = t + l by NAT_1:10;
n divides (i|^s - i|^t) by B1,INT_2:15;
then n divides (i|^t * i|^l - i|^t * 1) by A2,NEWTON:8;
then A3:n divides (i|^t * (i|^l - 1));
reconsider ll = i|^l - 1 as Element of NAT by NAT_1:21,14,A7;
A8: n gcd i|^t = 1 by A4,A7,NAT_4:10;
n divides ll by A3,A8,WSIERP_1:30;
then i|^l,1 are_congruent_mod n by INT_2:15;
then i|^l mod n = 1 mod n by NAT_D:64 .= 1 by A1,PEPIN:5;
then R divides (s - t) by A2,A1,PEPIN:47;
hence thesis by INT_2:15;
end;
suppose s < t;
then consider l be Nat such that A10:t = s + l by NAT_1:10;
i|^t,i|^s are_congruent_mod n by B1,INT_1:14;
then n divides (i|^t - i|^s) by INT_2:15;
then n divides (i|^s * i|^l - i|^s * 1) by A10,NEWTON:8;
then A13:n divides (i|^s * (i|^l - 1));
A11: n gcd i|^s = 1 by A4,A7,NAT_4:10;
reconsider ll = i|^l - 1 as Element of NAT by NAT_1:21,14,A7;
n divides ll by A11,A13,WSIERP_1:30;
then i|^l,1 are_congruent_mod n by INT_2:15;
then i|^l mod n = 1 mod n by NAT_D:64
.= 1 by A1,PEPIN:5;
then R divides (t - s) by A1,A10,PEPIN:47;
then t,s are_congruent_mod R by INT_2:15;
hence thesis by INT_1:14;
end;
end;
assume B2:s,t are_congruent_mod R;
B9:R > 0 by A1,PEPIN:def 2;
then B3:s = (s div R) * R + (s mod R) &
t = (t div R) * R + (t mod R) by NEWTON:66;
then B4:i|^s = i|^ (R * (s div R)) * i|^(s mod R) by NEWTON:8
.= i|^R|^(s div R) * i|^(s mod R) by NEWTON:9;
B5:i|^R mod n = 1 by A1,PEPIN:def 2
.= 1 mod n by A1,PEPIN:5;
then (i|^R|^(s div R)) mod n = 1|^(s div R) mod n by INT_4:8
.= 1 mod n by NEWTON:10;
then i|^R|^(s div R),1 are_congruent_mod n by A1,NAT_D:64;
then i|^R|^(s div R)*i|^(s mod R),1*i|^(s mod R) are_congruent_mod n
by INT_4:11;
then B6:i|^s mod n = i|^(s mod R) mod n by B4,NAT_D:64;
B7:i|^t = i|^ (R * (t div R)) * i|^(t mod R) by NEWTON:8,B3
.= i|^R|^(t div R) * i|^(t mod R) by NEWTON:9;
i|^R|^(t div R) mod n = 1|^(t div R) mod n by B5,INT_4:8
.= 1 mod n by NEWTON:10;
then i|^R|^(t div R),1 are_congruent_mod n by A1,NAT_D:64;
then i|^R|^(t div R)*i|^(t mod R),1*i|^(t mod R) are_congruent_mod n
by INT_4:11;
then B8:i|^t mod n = i|^(t mod R) mod n by B7,NAT_D:64;
s mod R = (s mod R) mod R & t mod R = (t mod R) mod R by EULER_2:5;
then B10:s,(s mod R) are_congruent_mod R
& t,(t mod R) are_congruent_mod R by B9,NAT_D:64;
then t,(s mod R) are_congruent_mod R by B2,PEPIN:40;
then (s mod R),(t mod R) are_congruent_mod R by B10,PEPIN:40;
then B11:R divides ((s mod R)-(t mod R)) by INT_2:15;
now assume (s mod R)<>(t mod R);
then (s mod R)-(t mod R)<>0;
then |.R.| <= |.((s mod R)-(t mod R)).| by B11,INT_4:6;
then B12:R <= |.((s mod R)-(t mod R)).| by ABSVALUE:def 1;
reconsider sR = s mod RR, tR = t mod RR as Element of REAL
by XREAL_0:def 1;
reconsider rR = -R as Element of REAL by XREAL_0:def 1;
S: sR < RR & sR >= 0 & tR < RR & tR >= 0 by B9,NAT_D:1;
sR - tR <= sR by XREAL_1:43; then
T: sR - tR < RR by S,XXREAL_0:2;
V: (-1)*tR > (-1)*RR by XREAL_1:69,S;
sR + -tR >= -tR by XREAL_1:31; then
sR + -tR > rR by XXREAL_0:2,V;
hence contradiction by B12,SEQ_2:1,T;
end;
hence thesis by A1,B6,B8,NAT_D:64;
end;
theorem
for i,n st n>1 & i,n are_relative_prime holds
i|^s,1 are_congruent_mod n iff order(i,n) divides s
proof let i,n;
assume A1:n>1 & i,n are_relative_prime;
thus i|^s,1 are_congruent_mod n implies order(i,n) divides s
proof assume i|^s,1 are_congruent_mod n;
then i|^s,i|^0 are_congruent_mod n by NEWTON:4;
then s,0 are_congruent_mod order(i,n) by A1,Th3;
then order(i,n) divides (s-0) by INT_2:15;
hence thesis;
end;
assume order(i,n) divides s;
then order(i,n) divides (s-0);
then s,0 are_congruent_mod order(i,n) by INT_2:15;
then i|^s,i|^0 are_congruent_mod n by A1,Th3;
hence thesis by NEWTON:4;
end;
theorem
n>1 & i,n are_relative_prime & len fn = order(i,n) &
(for d st d in dom fn holds fn.d =i|^(d-'1))
implies (for d,e st d in dom fn & e in dom fn & d<>e
holds not fn.d,fn.e are_congruent_mod n)
proof assume A1:n>1 & i,n are_relative_prime & len fn = order(i,n) &
(for d st d in dom fn holds fn.d = i|^(d-'1));
then A0:i <> 0 & n <> 0 by Th1;
A9:i gcd n = 1 by A1,INT_2:def 3;
assume ex d,e st d in dom fn & e in dom fn & d<>e &
fn.d,fn.e are_congruent_mod n;
then consider d,e such that
A2: d in dom fn & e in dom fn & d<>e & fn.d,fn.e are_congruent_mod n;
A4: d>=1 & d<=order(i,n) & e>=1 & e<=order(i,n) by A2,A1,FINSEQ_3:25;
then d-'1+1=d+1-'1 by NAT_D:38
.=d+1-1 by NAT_D:37
.=d-1+1; then
AA: d-'1=d-1;
e-'1+1=e+1-'1 by NAT_D:38,A4
.=e+1-1 by NAT_D:37
.=e-1+1; then
A5: d-1=d-'1 & e-1=e-'1 by AA;
per cases by A2,XXREAL_0:1;
suppose d > e;
then A6: e-'1 < d-'1 by A5,XREAL_1:9;
then consider k be Nat such that A7:d-'1=(e-'1)+k by NAT_1:10;
reconsider ll = i|^k - 1 as Element of NAT by A0,NAT_1:21,14;
A8: i|^(d-'1) - i|^(e-'1)
= i|^(e-'1) * i|^k - i|^(e-'1) * 1 by A7,NEWTON:8
.= i|^(e-'1) * ll;
A10: i|^(e-'1) gcd n = 1 by A0,A9,NAT_4:10;
i|^(d-'1),fn.e are_congruent_mod n by A1,A2;
then i|^(d-'1),i|^(e-'1) are_congruent_mod n by A1,A2;
then n divides i|^(d-'1) - i|^(e-'1) by INT_2:15;
then n divides ll by A8,A10,WSIERP_1:30;
then i|^k,1 are_congruent_mod n by INT_2:15;
then A13:i|^k mod n = 1 mod n by NAT_D:64
.= 1 by A1,PEPIN:5;
A14: (d-'1)-(e-'1)>0 by A6,XREAL_1:50;
A15: order(i,n) <= k by A14,A7,NAT_D:7,A1,A13,PEPIN:47;
d-e <= order(i,n)-1 by A4,XREAL_1:13;
hence contradiction by A5,A7,A15,XXREAL_0:2,XREAL_1:146;
end;
suppose e > d;
then A17:e-'1 > d-'1 by A5,XREAL_1:9;
then consider k be Nat such that A18:e-'1=(d-'1)+k by NAT_1:10;
reconsider ll = i|^k - 1 as Element of NAT by A0,NAT_1:21,14;
A19: i|^(e-'1) - i|^(d-'1)
= i|^(d-'1) * i|^k - i|^(d-'1) * 1 by A18,NEWTON:8
.= i|^(d-'1) * ll;
A20: i|^(d-'1) gcd n = 1 by A0,A9,NAT_4:10;
i|^(d-'1),fn.e are_congruent_mod n by A1,A2;
then i|^(d-'1),i|^(e-'1) are_congruent_mod n by A1,A2;
then i|^(e-'1),i|^(d-'1) are_congruent_mod n by INT_1:14;
then n divides (i|^(e-'1) - i|^(d-'1)) by INT_2:15;
then n divides ll by A19,A20,WSIERP_1:30;
then i|^k,1 are_congruent_mod n by INT_2:15;
then A21:i|^k mod n = 1 mod n by NAT_D:64
.= 1 by A1,PEPIN:5;
A22: (e-'1)-(d-'1)>0 by A17,XREAL_1:50;
A23: order(i,n) <= k by A18,A22,NAT_D:7,A1,A21,PEPIN:47;
e-d <= order(i,n)-1 by A4,XREAL_1:13;
hence contradiction by A18,A23,A5,XXREAL_0:2,XREAL_1:146;
end;
end;
theorem
n>1 & i,n are_relative_prime & len fn = order(i,n) &
(for d st d in dom fn holds fn.d = i|^(d-'1))
implies (for d st d in dom fn holds fn.d|^order(i,n) mod n = 1)
proof
assume
A1:n>1 & i,n are_relative_prime & len fn = order(i,n) &
(for d st d in dom fn holds fn.d = i|^(d-'1));
set K = order(i,n);
let d;
assume d in dom fn;
then A:fn.d = i|^(d -' 1) by A1;
A2:fn.d|^order(i,n) mod n
= i|^(K*(d-'1)) mod n by NEWTON:9,A
.= i|^K|^(d-'1) mod n by NEWTON:9;
i|^order(i,n) mod n = 1 by A1,PEPIN:def 2
.= 1 mod n by A1,PEPIN:5;
then (i|^K|^(d-'1)) mod n = 1|^(d-'1) mod n by INT_4:8
.= 1 mod n by NEWTON:10
.= 1 by A1,PEPIN:5;
hence thesis by A2;
end;
theorem Th6:
n>1 & i,n are_relative_prime
implies order(i|^s,n) = order(i,n) div (order(i,n) gcd s)
proof assume A1:n>1 & i,n are_relative_prime;
then A0:i <> 0 & n <> 0 by Th1;
i gcd n = 1 by A1,INT_2:def 3;then
i|^s gcd n = 1 by A0,NAT_4:10;then
A7:i|^s,n are_relative_prime by INT_2:def 3;
A3:order(i,n) > 0 by A1,PEPIN:def 2;
set K1 = order(i,n) gcd s,
K2 = order(i,n) div K1;
per cases;
suppose B1:s = 0;
then K1 = order(i,n) by NEWTON:52;
then B2:K2 = 1 by A3,NAT_2:3;
i|^s = 1 by B1,NEWTON:4;
hence thesis by A1,B2,PEPIN:46;
end;
suppose B:s > 0;
K1 divides order(i,n) & K1 divides s by NAT_D:def 5; then
A4: order(i,n) = K2 * K1 & s = (s div K1) * K1 by NAT_D:3; then
A12:K2 <> 0 & K1 <> 0 & (s div K1) <> 0 by A1,B,PEPIN:def 2;
A14: K2,(s div K1) are_relative_prime by A4,A12,EULER_1:6;
s * K2 = (s div K1) * order(i,n) by A4;
then order(i,n) divides s * K2 by NAT_D:def 3;
then (i|^(s * K2)) mod n = 1 by A1,PEPIN:48;
then A6:(i|^s|^K2) mod n = 1 by NEWTON:9;
for k be Nat st k > 0 & (i|^s|^k) mod n = 1 holds 0 < K2 & K2 <= k
proof let k be Nat;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
assume A10:k > 0 & (i|^s|^k) mod n = 1;
then (i|^(s*k)) mod n = 1 by NEWTON:9;
then (K2 * K1) divides (((s div K1) * k1) * K1) by A4,A1,PEPIN:47;
then K2 divides ((s div K1) * k1) by A12,PYTHTRIP:7;
hence thesis by A12,A10,A14,PEPIN:3,NAT_D:7;
end;
hence thesis by A1,A7,A12,A6,PEPIN:def 2;
end;
end;
theorem
for i,n st n>1 & i,n are_relative_prime holds
order(i,n),s are_relative_prime iff order(i|^s,n) = order(i,n)
proof let i,n;
assume A1:n>1 & i,n are_relative_prime;
thus order(i,n),s are_relative_prime implies order(i|^s,n) = order(i,n)
proof assume order(i,n),s are_relative_prime;
then order(i,n) gcd s = 1 by INT_2:def 3;
then order(i,n) div (order(i,n) gcd s) = order(i,n) by NAT_2:4;
hence thesis by A1,Th6;
end;
assume order(i|^s,n) = order(i,n);
then A2:order(i,n) div (order(i,n) gcd s) = order(i,n) by A1,Th6;
set d = order(i,n) gcd s;
A3:d divides order(i,n) by NAT_D:def 5;
then A4:(order(i,n) div d)*1 = (order(i,n) div d)*d by A2,NAT_D:3;
A6:order(i,n)>0 by A1,PEPIN:def 2;
then A7:d<=order(i,n) by A3,NAT_D:7;
d<>0 by A6,INT_2:5;
then order(i,n) div d <> 0 by A7,NAT_2:13;
then d = 1 by A4,XCMPLX_1:5;
hence thesis by INT_2:def 3;
end;
theorem
n>1 & i,n are_relative_prime & order(i,n) = s*t
implies order(i|^s,n) = t
proof assume A1:n>1 & i,n are_relative_prime & order(i,n) = s*t;
then A8:i <> 0 by Th1;
A6:t <> 0 & s <> 0 by A1,PEPIN:def 2;
i gcd n = 1 by A1,INT_2:def 3;
then i|^s gcd n = 1 by A8,A1,NAT_4:10;
then A7:i|^s,n are_relative_prime by INT_2:def 3;
A4:i|^s|^t mod n = i|^order(i,n) mod n by A1,NEWTON:9
.=1 by A1,PEPIN:def 2;
A12: for k be Nat st k>0 & (i|^s|^k) mod n = 1 holds 0 < t & t <= k
proof let k be Nat;
assume A5:k>0 & (i|^s|^k) mod n = 1;
then A11:i|^(s*k) mod n = 1 by NEWTON:9;
reconsider t,s,k as Element of NAT by ORDINAL1:def 12;
t*s divides k*s by A11,A1,PEPIN:47;
then t divides k by A6,PYTHTRIP:7;
hence thesis by A6,A5,NAT_D:7;
end;
t is Element of NAT by ORDINAL1:def 12;
hence thesis by A1,A7,A6,A12,A4,PEPIN:def 2;
end;
theorem Th9:
n>1 & s,n are_relative_prime & t,n are_relative_prime &
order(s,n),order(t,n) are_relative_prime implies
order(s*t,n) = order(s,n)*order(t,n)
proof assume A1:n>1 & s,n are_relative_prime & t,n are_relative_prime &
order(s,n),order(t,n) are_relative_prime;
then s gcd n = 1 & t gcd n = 1 by INT_2:def 3; then
(s*t) gcd n = 1 by WSIERP_1:7;
then A2:(s*t),n are_relative_prime by INT_2:def 3;
set L = order(s,n)*order(t,n);
A10:((s*t)|^order(s*t,n)) mod n = 1 by A1,A2,PEPIN:def 2
.= 1 mod n by A1,PEPIN:5;
then ((s*t)|^order(s*t,n)|^order(s,n)) mod n = 1|^order(s,n) mod n
by INT_4:8;
then (s*t)|^(order(s*t,n) * order(s,n)) mod n
= 1|^order(s,n) mod n by NEWTON:9
.= 1 mod n by NEWTON:10 .= 1 by A1,PEPIN:5;
then (s*t)|^(order(s,n))|^order(s*t,n) mod n = 1 by NEWTON:9;
then (s|^order(s,n)*t|^order(s,n))|^order(s*t,n) mod n = 1 by NEWTON:7;then
A6:((s|^order(s,n))|^order(s*t,n) * (t|^order(s,n))|^order(s*t,n)) mod n = 1
by NEWTON:7;
s|^order(s,n) mod n = 1 by A1,PEPIN:def 2 .= 1 mod n by A1,PEPIN:5;
then (s|^order(s,n))|^order(s*t,n) mod n = 1|^order(s*t,n) mod n by INT_4:8
.= 1 mod n by NEWTON:10;
then (s|^order(s,n))|^order(s*t,n),1 are_congruent_mod n by A1,NAT_D:64;
then (s|^order(s,n))|^order(s*t,n)*(t|^order(s,n))|^order(s*t,n),
1*(t|^order(s,n))|^order(s*t,n) are_congruent_mod n by INT_4:11;
then (t|^order(s,n))|^order(s*t,n) mod n = 1 by A6,NAT_D:64;
then A7:t|^(order(s,n) * order(s*t,n)) mod n = 1 by NEWTON:9;
A8:order(t,n) divides order(s*t,n) by A1,A7,PEPIN:47,PEPIN:3;
((s*t)|^order(s*t,n))|^order(t,n) mod n = 1|^order(t,n) mod n
by A10,INT_4:8;
then (s*t)|^(order(s*t,n) * order(t,n)) mod n
= 1|^order(t,n) mod n by NEWTON:9
.= 1 mod n by NEWTON:10 .= 1 by A1,PEPIN:5;
then ((s*t)|^order(t,n))|^order(s*t,n) mod n = 1 by NEWTON:9;then
(s|^order(t,n)*t|^order(t,n))|^order(s*t,n) mod n = 1 by NEWTON:7;then
A11:((s|^order(t,n))|^order(s*t,n) * (t|^order(t,n))|^order(s*t,n)) mod n = 1
by NEWTON:7;
t|^order(t,n) mod n = 1 by A1,PEPIN:def 2 .= 1 mod n by A1,PEPIN:5;
then (t|^order(t,n))|^order(s*t,n) mod n = 1|^order(s*t,n) mod n by INT_4:8
.= 1 mod n by NEWTON:10;
then (t|^order(t,n))|^order(s*t,n),1 are_congruent_mod n by A1,NAT_D:64;
then (t|^order(t,n))|^order(s*t,n)*(s|^order(t,n))|^order(s*t,n),
1*(s|^order(t,n))|^order(s*t,n) are_congruent_mod n by INT_4:11;
then (s|^order(t,n))|^order(s*t,n) mod n = 1 by A11,NAT_D:64;
then s|^(order(t,n) * order(s*t,n)) mod n = 1 by NEWTON:9;
then order(s,n) divides order(s*t,n) by A1,PEPIN:3,47;
then A12:L divides order(s*t,n) by A8,A1,PEPIN:4;
order(s,n) divides L & order(t,n) divides L by NAT_D:def 3;
then s|^L mod n = 1 & t|^L mod n = 1 by A1,PEPIN:48;
then s|^L,1 are_congruent_mod n & t|^L,1 are_congruent_mod n by A1,PEPIN:39;
then (s|^L)*(t|^L),1*1 are_congruent_mod n by INT_1:18;
then (s*t)|^L,1 are_congruent_mod n by NEWTON:7;
then (s*t)|^L mod n = 1 mod n by NAT_D:64 .= 1 by A1,PEPIN:5;
then order(s*t,n) divides L by A1,A2,PEPIN:47;
hence thesis by A12,NAT_D:5;
end;
reserve fp,fr for FinSequence of NAT;
theorem
n>1 & s,n are_relative_prime & t,n are_relative_prime &
order(s*t,n) = order(s,n)*order(t,n) implies
order(s,n),order(t,n) are_relative_prime
proof assume A1:n>1 & s,n are_relative_prime & t,n are_relative_prime &
order(s*t,n) = order(s,n)*order(t,n);
then s gcd n = 1 & t gcd n = 1 by INT_2:def 3; then
s*t gcd n = 1 by WSIERP_1:7;
then A10:s*t,n are_relative_prime by INT_2:def 3;
set L = order(s,n) lcm order(t,n);
order(s,n)>0 & order(t,n)>0 by A1,PEPIN:def 2;
then B:L<>0 by INT_2:4;
order(s,n) divides order(s*t,n) & order(t,n) divides order(s*t,n)
by A1,NAT_D:def 3;
then A3:L divides order(s*t,n) by NAT_D:def 4;
A4:order(s,n) divides L & order(t,n) divides L by NAT_D:def 4;then
s|^(order(s,n) lcm order(t,n)) mod n = 1 by A1,PEPIN:48
.= 1 mod n by A1,PEPIN:5;
then A6:s|^(order(s,n) lcm order(t,n)),1 are_congruent_mod n by A1,NAT_D:64;
t|^L mod n = 1 by A1,A4,PEPIN:48 .= 1 mod n by A1,PEPIN:5;
then t|^L,1 are_congruent_mod n by A1,NAT_D:64;
then A:t|^(order(s,n) lcm order(t,n))*s|^(order(s,n) lcm order(t,n)),1*1
are_congruent_mod n by A6,INT_1:18;
set B=s*t;
B|^(order(s,n) lcm order(t,n)),1*1 are_congruent_mod n by A,NEWTON:7;
then BB:B|^(order(s,n) lcm order(t,n)) mod n = 1 mod n by NAT_D:64
.= 1 by A1,PEPIN:5;
order(B,n) divides L by BB,A1,A10,PEPIN:47;
then L = order(s,n)*order(t,n) by A1,A3,NAT_D:5;
then L*(order(s,n) gcd order(t,n)) = L*1 by NAT_D:29;
then order(s,n) gcd order(t,n) = 1 by B,XCMPLX_1:5;
hence thesis by INT_2:def 3;
end;
theorem
n>1 & s,n are_relative_prime & s*t mod n = 1
implies order(s,n)=order(t,n)
proof assume A1:n>1 & s,n are_relative_prime & s*t mod n = 1;
set f = t gcd n;
A8: now assume not t,n are_relative_prime;
then A2:f <> 1 by INT_2:def 3;
f <> 0 by A1,INT_2:5;
then A4:f > 1 by A2,NAT_1:25;
A5: n divides (s*t - 1) by A1,PEPIN:8;
A6: f divides t & f divides n by NAT_D:def 5;then
A7: f divides (s*t - 1) by A5,INT_2:9;
f divides s*t by A6,NAT_D:9;
hence contradiction by A4,A7,INT_5:2,NAT_D:7;
end;
A11:order(s,n)>0 by A1,PEPIN:def 2;
set M=s*t;
A15:M mod n = 1 mod n by A1,PEPIN:5;
then M|^order(s,n) mod n = 1|^order(s,n) mod n by INT_4:8
.= 1 mod n by NEWTON:10 .= 1 by A1,PEPIN:5;
then A12:(s|^order(s,n)*t|^order(s,n)) mod n = 1 by NEWTON:7;
s|^order(s,n) mod n = 1 by A1,PEPIN:def 2;then
A13:t|^order(s,n) mod n = 1 by A12,Th12;
for k be Nat st k > 0 & (t|^k) mod n = 1
holds 0 < order(s,n) & order(s,n) <= k
proof let k be Nat;
assume A14:k > 0 & (t|^k) mod n = 1;
k is Element of NAT by ORDINAL1:def 12;then
M|^k mod n = 1|^k mod n by A15,INT_4:8
.= 1 mod n by NEWTON:10 .= 1 by A1,PEPIN:5;
then (s|^k * t|^k) mod n = 1 by NEWTON:7;
then s|^k mod n = 1 by A14,Th12;
hence thesis by A1,A14,PEPIN:def 2;
end;
hence thesis by A13,A11,A8,A1,PEPIN:def 2;
end;
theorem Th13:
n>1 & m>1 & i,n are_relative_prime & m divides n
implies order(i,m) divides order(i,n)
proof
assume A1:n>1 & m>1 & i,n are_relative_prime & m divides n;
i gcd n = 1 by A1,INT_2:def 3;
then i gcd m = 1 by A1,WSIERP_1:16;
then A3:i,m are_relative_prime by INT_2:def 3;
(i|^order(i,n)) mod n = 1 by A1,PEPIN:def 2
.= 1 mod n by A1,PEPIN:5;
then i|^order(i,n),1 are_congruent_mod n by A1,NAT_D:64;
then n divides (i|^order(i,n) - 1) by INT_2:15;
then m divides (i|^order(i,n) - 1) by A1,INT_2:9;
then i|^order(i,n),1 are_congruent_mod m by INT_2:15;
then (i|^order(i,n)) mod m = 1 mod m by NAT_D:64
.= 1 by A1,PEPIN:5;
hence thesis by A1,A3,PEPIN:47;
end;
theorem
n>1 & m>1 & m,n are_relative_prime & i,m*n are_relative_prime
implies order(i,m*n) = order(i,m) lcm order(i,n)
proof
assume
A1: n>1 & m>1 & m,n are_relative_prime & i,m*n are_relative_prime;
then A2:m*n>1*1 by XREAL_1:98;
then i <> 0 by A1,Th1; then
A8: i>0;
set K = order(i,m) lcm order(i,n);
A3: m divides m*n & n divides m*n by NAT_D:def 3;then
order(i,m) divides order(i,m*n) & order(i,n) divides order(i,m*n)
by A1,A2,Th13;
then A4:K divides order(i,m*n) by NAT_D:def 4;
i gcd m*n = 1 by A1,INT_2:def 3;
then i gcd m = 1 & i gcd n = 1 by A3,WSIERP_1:16;then
A5: i,m are_relative_prime & i,n are_relative_prime by INT_2:def 3;
i|^K-1>=0 by NAT_1:14,XREAL_1:48,A8;
then A9:i|^K-1 is Element of NAT by INT_1:3;
order(i,m) divides K & order(i,n) divides K by NAT_D:def 4;
then (i|^K) mod m = 1 & (i|^K) mod n = 1 by A1,A5,PEPIN:48;
then (i|^K),1 are_congruent_mod m & (i|^K),1 are_congruent_mod n
by A1,PEPIN:39;
then m divides ((i|^K)-1) & n divides ((i|^K)-1) by INT_2:15;
then m*n divides ((i|^K)-1) by A1,A9,PEPIN:4;
then i|^K,1 are_congruent_mod m*n by INT_2:15;then
A10:i|^K mod m*n = 1 by A2,PEPIN:39;
order(i,m*n) divides K by A1,A2,A10,PEPIN:47;
hence thesis by A4,NAT_D:5;
end;
definition
let X be set,m be Nat;
pred X is_RRS_of m means :Def1:
ex fp be FinSequence of INT st
len fp = len(Sgm RelPrimes(m)) & (for d st d in dom fp holds
fp.d in Class(Cong m,(Sgm RelPrimes(m)).d)) & X = rng fp;
end;
theorem Th14:
RelPrimes(m) is_RRS_of m
proof
A0: RelPrimes(m) c= Seg m by TH13;
A1: rng Sgm RelPrimes(m) = RelPrimes(m) &
len Sgm RelPrimes(m) = len Sgm RelPrimes(m) by A0,FINSEQ_1:def 13;
rng Sgm RelPrimes(m) c= INT;
then A2:Sgm RelPrimes(m) is FinSequence of INT by FINSEQ_1:def 4;
for a be Nat st a in dom Sgm RelPrimes(m)
holds (Sgm RelPrimes(m)).a in Class(Cong(m),(Sgm RelPrimes(m)).a)
proof let a be Nat;
assume a in dom Sgm RelPrimes(m);
(Sgm RelPrimes(m)).a,(Sgm RelPrimes(m)).a are_congruent_mod m
by INT_1:11;
then [(Sgm RelPrimes(m)).a,(Sgm RelPrimes(m)).a] in Cong(m)
by INT_4:def 1;
hence thesis by EQREL_1:18;
end; then
for d st d in dom Sgm RelPrimes(m) holds (Sgm RelPrimes(m)).d
in Class(Cong m,(Sgm RelPrimes(m)).d);
hence thesis by A1,A2,Def1;
end;
theorem Th15:
d in dom Sgm RelPrimes(m) & e in dom Sgm RelPrimes(m)
& d<>e implies not (Sgm RelPrimes(m)).d,(Sgm RelPrimes(m)).e
are_congruent_mod m
proof
assume A1: d in dom Sgm RelPrimes(m) & e in dom Sgm RelPrimes(m) & d<>e;
A0: RelPrimes(m) c= Seg(m) by TH13;
rng Sgm RelPrimes(m) = RelPrimes(m) by A0,FINSEQ_1:def 13;
then A2:(Sgm RelPrimes(m)).d in RelPrimes(m) &
(Sgm RelPrimes(m)).e in RelPrimes(m) by A1,FUNCT_1:def 3;
then consider k1 be Element of NAT such that
A3: k1=(Sgm RelPrimes(m)).d & m,k1 are_relative_prime & k1>=1 & k1<=m;
consider k2 be Element of NAT such that
A4: k2=(Sgm RelPrimes(m)).e & m,k2 are_relative_prime & k2>=1 & k2<=m by A2;
A5:((Sgm RelPrimes(m)).d)-((Sgm RelPrimes(m)).e)<=m-1 &
1-m<=((Sgm RelPrimes(m)).d)-((Sgm RelPrimes(m)).e) by A3,A4,XREAL_1:13;
A6: m-1 0
by A1,FUNCT_1:def 4;
then |.m.| <= |.(((Sgm RelPrimes(m)).d)-((Sgm RelPrimes(m)).e)).|
by A9,INT_4:6;
hence contradiction by A8,ABSVALUE:def 1;
end;
hence thesis;
end;
theorem Th16:
for X be finite set st X is_RRS_of m holds card X = Euler m &
(for x,y be Integer st x in X & y in X & x<>y holds
not x,y are_congruent_mod m) & (for x be Integer st x in X holds
x,m are_relative_prime)
proof
let X be finite set;
assume X is_RRS_of m; then
consider fp be FinSequence of INT such that
A1:len fp = len(Sgm RelPrimes(m)) & (for d st d in dom fp holds
fp.d in Class(Cong m,(Sgm RelPrimes(m)).d)) & X = rng fp by Def1;
A11:dom fp = dom (Sgm RelPrimes(m)) by A1,FINSEQ_3:29;
for a,b be set st a in dom fp & b in dom fp & fp.a = fp.b holds a = b
proof let a,b be set;
assume A2:a in dom fp & b in dom fp & fp.a = fp.b;
reconsider a,b as Element of NAT by A2;
reconsider l=fp.a,ll=fp.b as Element of INT by A2,FINSEQ_2:11;
l in Class(Cong(m),(Sgm RelPrimes(m)).a) &
ll in Class(Cong(m),(Sgm RelPrimes(m)).b) by A1,A2;
then [(Sgm RelPrimes(m)).a,l] in Cong(m) &
[(Sgm RelPrimes(m)).b,ll] in Cong(m) by EQREL_1:18;
then A3:(Sgm RelPrimes(m)).a,l are_congruent_mod m
& (Sgm RelPrimes(m)).b,ll are_congruent_mod m by INT_4:def 1;
then l,(Sgm RelPrimes(m)).b are_congruent_mod m by A2,INT_1:14;
hence thesis by Th15,A2,A11,A3,INT_1:15;
end;
then A:fp is one-to-one by FUNCT_1:def 4;
C:RelPrimes(m) c= Seg m by TH13;
A7:card X = len(Sgm RelPrimes(m)) by A1,FINSEQ_4:62,A
.= Euler m by C,FINSEQ_3:39;
A20: for x,y be Integer st x in X & y in X & x<>y holds
not x,y are_congruent_mod m
proof let x,y be Integer;
assume A8:x in X & y in X & x<>y; then
consider d be Nat such that
A9: d in dom fp & fp.d = x by A1,FINSEQ_2:10;
consider e be Nat such that
A10: e in dom fp & fp.e = y by A1,A8,FINSEQ_2:10;
A12: d in dom Sgm RelPrimes(m) & e in dom Sgm RelPrimes(m)
by A9,A10,A1,FINSEQ_3:29;
reconsider d,e as Element of NAT by A9,A10;
fp.d in Class(Cong m,(Sgm RelPrimes(m)).d) &
fp.e in Class(Cong m,(Sgm RelPrimes(m)).e) by A9,A10,A1;then
[(Sgm RelPrimes(m)).d,fp.d] in Cong(m) &
[(Sgm RelPrimes(m)).e,fp.e] in Cong(m) by EQREL_1:18;
then A13:(Sgm RelPrimes(m)).d,fp.d are_congruent_mod m &
(Sgm RelPrimes(m)).e,fp.e are_congruent_mod m by INT_4:def 1;
now assume fp.d,fp.e are_congruent_mod m;
then (Sgm RelPrimes(m)).d,fp.e are_congruent_mod m by A13,INT_1:15;
then fp.e,(Sgm RelPrimes(m)).d are_congruent_mod m by INT_1:14;
hence contradiction by A12,A9,A10,A8,Th15,A13,INT_1:15;
end;
hence thesis by A9,A10;
end;
for x be Integer st x in X holds x,m are_relative_prime
proof let x be Integer;
assume x in X;
then consider d be Nat such that
A16: d in dom fp & fp.d = x by A1,FINSEQ_2:10;
reconsider d as Element of NAT by A16;
fp.d in Class(Cong m,(Sgm RelPrimes(m)).d) by A1,A16;
then [(Sgm RelPrimes(m)).d,fp.d] in Cong(m) by EQREL_1:18;
then (Sgm RelPrimes(m)).d,fp.d are_congruent_mod m by INT_4:def 1;
then A17:(Sgm RelPrimes(m)).d gcd m = fp.d gcd m by INT_4:14;
RelPrimes(m) c= Seg m by TH13;then
rng (Sgm RelPrimes(m)) = RelPrimes(m) by FINSEQ_1:def 13;
then (Sgm RelPrimes(m)).d in RelPrimes(m) by A11,A16,FUNCT_1:def 3;
then consider k be Element of NAT such that
A19: (Sgm RelPrimes(m)).d=k & m,k are_relative_prime & k>=1 & k<=m;
fp.d gcd m = 1 by A17,A19,INT_2:def 3;
hence thesis by A16, INT_2:def 3;
end;
hence thesis by A7,A20;
end;
Lm1:
for X be finite set st card X = 0 holds X = {};
theorem
{} is_RRS_of m iff m = 0
proof thus {} is_RRS_of m implies m = 0
proof assume {} is_RRS_of m;
then Euler m = card {} by Th16;
hence thesis by PEPIN:42;
end;
assume A1:m = 0;
reconsider fp=<*>INT as FinSequence of INT;
RelPrimes m c= Seg m by TH13; then
card RelPrimes(m) <= card Seg m by NAT_1:43;
then card RelPrimes(m) <= 0 by A1;
then card RelPrimes(m) = 0;
then A4:len Sgm RelPrimes(m) = len fp by Lm1,FINSEQ_3:43;
(for d st d in dom fp holds fp.d in Class(Cong(m),(Sgm RelPrimes(m)).d));
hence thesis by RELAT_1:38,A4,Def1;
end;
theorem Th18:
for X be finite Subset of INT
st ( 1y holds
not x,y are_congruent_mod m) & (for x be Integer st x in X holds
x,m are_relative_prime))
holds X is_RRS_of m
proof let X be finite Subset of INT;
assume A1:(1y holds
not x,y are_congruent_mod m) & (for x be Integer st x in X holds
x,m are_relative_prime));
then card X <> 0 by PEPIN:42;
then reconsider X as non empty finite Subset of INT;
set Y = RelPrimes(m);
C: Y c= Seg m by TH13;
reconsider Y as finite set;
m gcd 1 = 1 by NEWTON:51;
then m,1 are_relative_prime by INT_2:def 3;
then 1 in Y by A1;
then reconsider Y as non empty finite set;
reconsider Y as non empty finite Subset of INT
by NUMBERS:17,XBOOLE_1:1;
A41:Y is_RRS_of m by Th14;
defpred P[Nat,set] means $2 in Class(Cong m,(Sgm Y).$1);
A31:for a be Nat st a in Seg Euler m ex y being Element of X st P[a,y]
proof
let a be Nat;
assume A27:a in Seg Euler m;
consider fp being FinSequence such that
A7: len fp = Euler m & (for d st d in dom fp holds fp.d in X) &
fp is one-to-one by A1,INT_4:51;
for d be Nat st d in dom fp holds fp.d in X by A7;
then reconsider fp as FinSequence of X by FINSEQ_2:12;
A9: card(rng fp) = card X by A1,A7,FINSEQ_4:62;
rng fp c= X by FINSEQ_1:def 4;then
A10: rng fp = X by A9,CARD_2:102;
defpred PP[Nat,set] means fp.$1 in Class(Cong m,$2);
A18: for c be Nat st c in Seg Euler m ex r be Element of Y st PP[c,r]
proof let c be Nat;
assume c in Seg Euler m;
then c in dom fp by A7,FINSEQ_1:def 3;
then A11:fp.c,m are_relative_prime by A1,A7;
set r = fp.c mod m;
A17: fp.c mod m = ((fp.c div m)*m + r) mod m by A1,INT_1:59
.= r mod m by EULER_1:12;
then fp.c,r are_congruent_mod m by A1,NAT_D:64;
then A12:r gcd m = fp.c gcd m by INT_4:14 .= 1 by A11,INT_2:def 3;
then A13:r,m are_relative_prime by INT_2:def 3;
reconsider r as Element of NAT by INT_1:3,57;
reconsider zz = 0,j=1 as Real;
now assume r=0;
then |.m.| = 1 by A12,WSIERP_1:8;
hence contradiction by A1,ABSVALUE:def 1;
end;
then r-1>=0 by INT_1:52;
then A14:(r-1+j) >= zz+j by XREAL_1:7;
r<=m by A1,INT_1:58;
then A16:r in Y by A14,A13;
r,fp.c are_congruent_mod m by A17,A1,NAT_D:64;
then [r,fp.c] in Cong m by INT_4:def 1;
then fp.c in Class(Cong m,r) by EQREL_1:18;
hence thesis by A16;
end;
consider fr being FinSequence of Y such that
A19: dom fr = Seg Euler m & for c be Nat st c in Seg Euler m
holds PP[c,fr.c] from FINSEQ_1:sch 5(A18);
for x1,x2 be set
st x1 in dom fr & x2 in dom fr & fr.x1 = fr.x2 holds x1 = x2
proof let x1,x2 be set;
assume A21:x1 in dom fr & x2 in dom fr & fr.x1 = fr.x2;
then reconsider x1,x2 as Element of NAT;
fp.x1 in Class(Cong m,fr.x1) & fp.x2 in Class(Cong m,fr.x2) by A21,A19;
then [fr.x1,fp.x1] in Cong m & [fr.x2,fp.x2] in Cong m by EQREL_1:18;
then fr.x1,fp.x1 are_congruent_mod m & fr.x2,fp.x2 are_congruent_mod m
by INT_4:def 1;
then A22:fp.x1,fp.x2 are_congruent_mod m by A21,PEPIN:40;
A23: x1 in dom fp & x2 in dom fp by A21,A7,A19,FINSEQ_1:def 3;
then fp.x1 in X & fp.x2 in X by A10,FUNCT_1:def 3;
then fp.x1 = fp.x2 by A1,A22;
hence thesis by A23,A7,FUNCT_1:def 4;
end;
then fr is one-to-one by FUNCT_1:def 4;
then A25:card rng fr = len fr by FINSEQ_4:62
.= card Y by A19,FINSEQ_1:def 3;
rng fr c= Y by FINSEQ_1:def 4;
then A26:rng fr = Y by A25,CARD_2:102;
len Sgm Y = Euler m by C,FINSEQ_3:39;
then a in dom Sgm Y by A27,FINSEQ_1:def 3;
then (Sgm Y).a in rng(Sgm Y) by FUNCT_1:def 3;
then (Sgm Y).a in rng fr by A26,C,FINSEQ_1:def 13;
then consider i be Nat such that
A28:i in dom fr & fr.i=(Sgm Y).a by FINSEQ_2:10;
i in dom fp by A28,A7,A19,FINSEQ_1:def 3;
then fp.i is Element of X by A10,FUNCT_1:def 3;
hence thesis by A28,A19;
end;
consider f being FinSequence of X such that
A32: dom f = Seg Euler m & for a be Nat st a in Seg Euler m holds P[a,f.a]
from FINSEQ_1:sch 5(A31);
A33:len f = Euler m by A32,FINSEQ_1:def 3;
for a,b be set st a in dom f & b in dom f & f.a = f.b holds a = b
proof let a,b be set;
assume A34:a in dom f & b in dom f & f.a = f.b;
then reconsider a,b as Element of NAT;
f.a in Class(Cong m,(Sgm Y).a) & f.b in Class(Cong m,(Sgm Y).b)
by A34,A32;
then [(Sgm Y).a,f.a] in Cong m & [(Sgm Y).b,f.b] in Cong m
by EQREL_1:18;
then A35:(Sgm Y).a,f.a are_congruent_mod m
& (Sgm Y).b,f.b are_congruent_mod m by INT_4:def 1;
then f.b,(Sgm Y).b are_congruent_mod m by INT_1:14;
then A36:(Sgm Y).a,(Sgm Y).b are_congruent_mod m by A35,A34,INT_1:15;
now assume A37:a <> b;
len Sgm Y = Euler m by C,FINSEQ_3:39;then
A38: a in dom Sgm Y & b in dom Sgm Y by A34,A32,FINSEQ_1:def 3;
Sgm Y is one-to-one by C,FINSEQ_3:92;
then A39:(Sgm Y).a <> (Sgm Y).b by A37,A38,FUNCT_1:def 4;
(Sgm Y).a in rng(Sgm Y) & (Sgm Y).b in rng(Sgm Y)
by A38,FUNCT_1:def 3;
then (Sgm Y).a in Y & (Sgm Y).b in Y by C,FINSEQ_1:def 13;
hence contradiction by A36,A39,A41,Th16;
end;
hence thesis;
end;
then f is one-to-one by FUNCT_1:def 4;
then A42:card X = card(rng f) by A1,A33,FINSEQ_4:62;
A44:rng f c= X by FINSEQ_1:def 4;
take f;
thus thesis by C,A32,A33,A44,A42,CARD_2:102,FINSEQ_3:39;
end;
theorem
for X be finite Subset of INT,a be Integer st (m>1 &
a,m are_relative_prime & X is_RRS_of m) holds (a ** X) is_RRS_of m
proof let X be finite Subset of INT,a be Integer;
assume A1:m>1 & a,m are_relative_prime & X is_RRS_of m;
then A2:card X = Euler m & (for x,y be Integer st x in X & y in X & x<>y
holds not x,y are_congruent_mod m) & (for x be Integer st x in X
holds x,m are_relative_prime) by Th16;
A5: a ** X c= INT
proof let x be element;
assume A3: x in a ** X;
then reconsider m = x as Real;
consider y being Complex such that
A0: x = a * y and
A4: y in X by A3,MEMBER_1:195;
reconsider n = y as Integer by A4;
m = a * n by A0;
hence thesis by INT_1:def 2;
end;
a<>0 by A1,Th1;then
A6: card(a ** X) = Euler m by A2,INT_4:5;
A7: for x,y be Integer st x in (a ** X) & y in (a ** X) & x<>y holds
not x,y are_congruent_mod m
proof let x,y be Integer;
assume A8:x in (a ** X) & y in (a ** X) & x <> y;
then consider z1 be Integer such that A9:z1 in X & x=a*z1 by Th21;
consider z2 be Integer such that A10:z2 in X & y=a*z2 by A8,Th21;
not z1,z2 are_congruent_mod m by A9,A8,A10,A1,Th16;
hence thesis by A9,A10,A1,INT_4:9;
end;
for x be Integer st x in (a ** X) holds x,m are_relative_prime
proof let x be Integer;
assume x in (a ** X);
then consider y such that A13:y in X & x = a * y by Th21;
y,m are_relative_prime by A13,A1,Th16;
hence thesis by A13, A1,INT_2:26;
end;
hence thesis by A1,A5,A6,A7,Th18;
end;
definition let i,n;
pred i is_primitive_root_of n means :Def2:
order(i,n) = Euler n;
end;
theorem
n>1 & i,n are_relative_prime implies (i is_primitive_root_of n iff
for fn st len fn = Euler n &
(for d being Nat st d in dom fn holds fn.d = i|^d)
holds rng fn is_RRS_of n)
proof assume A1:n>1 & i,n are_relative_prime;
then A17:i <> 0 by Th1;
reconsider z = 0, j = 1 as Element of REAL by XREAL_0:def 1;
i - 1 >= 0 by A17,INT_1:52;then
A0:i - 1 + j >= z + j by XREAL_1:7;
A18:i gcd n = 1 by A1,INT_2:def 3;
thus i is_primitive_root_of n implies for fn st len fn = Euler n
& (for d being Nat st d in dom fn holds fn.d = i|^d) holds
rng fn is_RRS_of n
proof assume i is_primitive_root_of n;
then A2: order(i,n) = Euler n by Def2;
for fn st len fn = Euler n
& (for d be Nat st d in dom fn holds fn.d = i|^d) holds
rng fn is_RRS_of n
proof let fn;
assume A3:len fn = Euler n
& (for d being Nat st d in dom fn holds fn.d = i|^d);
fn is one-to-one
proof per cases by A0,XXREAL_0:1;
suppose
S: i = 1;
reconsider fn as FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;
fn = <*fn/.1*> by FINSEQ_5:14,A3,A2,A1,PEPIN:46,S;
hence thesis;
end;
suppose A7:i > 1;
for x1,x2 be set st x1 in dom fn & x2 in dom fn & fn.x1 = fn.x2
holds x1 = x2
proof let x1,x2 be set;
assume A8:x1 in dom fn & x2 in dom fn & fn.x1 = fn.x2;
then reconsider x1,x2 as Element of NAT;
i|^x1 = fn.x2 by A8,A3 .= i|^x2 by A8,A3;
hence thesis by A7,PEPIN:30;
end;
hence thesis by FUNCT_1:def 4;
end;
end;
then A9:card(rng fn) = Euler n by A3,FINSEQ_4:62;
A10: for x,y be Integer st x in rng fn & y in rng fn & x <> y
holds not x,y are_congruent_mod n
proof let x,y be Integer;
assume A11:x in rng fn & y in rng fn & x <> y
& x,y are_congruent_mod n;
then consider s such that
A12: s in dom fn & fn.s = x by FINSEQ_2:10;
consider t such that
A13: t in dom fn & fn.t = y by A11,FINSEQ_2:10;
A14: x = i|^s & y = i|^t by A12,A13,A3;
A19: 1 <= s & s <= order(i,n) & 1 <= t & t <= order(i,n)
by A12,A13,A2,A3,FINSEQ_3:25;
per cases by A11,A12,A13,XXREAL_0:1;
suppose s > t;
then A20:s - t > 0 by XREAL_1:50;
then reconsider k = s - t as Element of NAT by INT_1:3;
i|^s - i|^t = i|^(t+k) - i|^t .= i|^t*i|^k - i|^t*1 by NEWTON:8
.= i|^t * (i|^k - 1);
then A21:n divides (i|^t * (i|^k - 1)) by A14,A11,INT_2:15;
i|^t gcd n = 1 by A17,A18,A1,NAT_4:10;
then n divides (i|^k - 1) by A21,WSIERP_1:29;
then i|^k,1 are_congruent_mod n by INT_2:15;
then i|^k mod n = 1 mod n by NAT_D:64 .= 1 by A1,PEPIN:5;then
A23: order(i,n) <= k by A20,A1,PEPIN:47,NAT_D:7;
k <= order(i,n)-1 & order(i,n)-1 0 by XREAL_1:50;
then reconsider k = t - s as Element of NAT by INT_1:3;
A27: i|^t - i|^s = i|^(s+k) - i|^s .= i|^s*i|^k - i|^s*1 by NEWTON:8
.= i|^s * (i|^k - 1);
i|^t,i|^s are_congruent_mod n by A14,A11,INT_1:14;
then A25:n divides (i|^s * (i|^k - 1)) by A27,INT_2:15;
i|^s gcd n = 1 by A17,A18,A1,NAT_4:10;
then n divides (i|^k - 1) by A25,WSIERP_1:29;
then i|^k,1 are_congruent_mod n by INT_2:15;
then i|^k mod n = 1 mod n by NAT_D:64 .= 1 by A1,PEPIN:5;then
A26: order(i,n) <= k by A24,A1,PEPIN:47,NAT_D:7;
k <= order(i,n)-1 & order(i,n)-1y holds not x,y are_congruent_mod n) by Th16;
then A41:f is one-to-one by A32,FINSEQ_4:62;
B:Euler n <> 0 by A1,PEPIN:42;
then
A35:Euler n > 0;
A39:Euler n >= 1 by A1,PEPIN:42,NAT_1:14;
A36:(i |^ Euler n) mod n = 1 by A1,Th1,EULER_2:18;
for s st s > 0 & (i|^s) mod n = 1 holds 0 < Euler n & Euler n <= s
proof let s;
assume A37:s > 0 & (i|^s) mod n = 1;
now assume s < Euler n;
then A38:Euler n - s > 0 by XREAL_1:50;
then reconsider k = Euler n - s as Element of NAT by INT_1:3;
A43: k < Euler n & k >= 1 by A37,A38,XREAL_1:44,NAT_1:14;then
A40: k in dom f & Euler n in dom f by A32,A39,FINSEQ_3:25; then
A42: f.k in rng f & f.(Euler n) in rng f by FUNCT_1:3;
f.k <> f.(Euler n) by A40,A41,A43,FUNCT_1:def 4;
then not f.k,f.(Euler n) are_congruent_mod n by A42,A34,Th16;
then not i|^k,f.(Euler n) are_congruent_mod n by A40,A32;then
A44: not i|^k,i|^(Euler n) are_congruent_mod n by A40,A32;
i|^(Euler n),i|^s are_congruent_mod n by A37,A36,A1,NAT_D:64;
then A45:n divides (i|^(Euler n) - i|^s) by INT_2:15;
A46: i|^(Euler n) - i|^s = i|^(s+k)-i|^s
.= i|^s*i|^k - i|^s*1 by NEWTON:8
.= i|^s * (i|^k - 1);
i|^s gcd n = 1 by A17,A18,A1,NAT_4:10;then
A47: n divides (i|^k - 1) by A45,A46,WSIERP_1:29;
(i |^ Euler n) mod n = 1 mod n by A1,A36,PEPIN:5;
then i|^Euler n,1 are_congruent_mod n by A1,NAT_D:64;
then n divides (i|^Euler n - 1) by INT_2:15;
then n divides (i|^k - 1 - (i|^Euler n - 1)) by A47,INT_5:1;
then n divides (i|^k - i|^Euler n);
hence contradiction by A44,INT_2:15;
end;
hence thesis by B;
end;
then order(i,n) = Euler n by A1,A35,A36,PEPIN:def 2;
hence thesis by Def2;
end;
theorem
p>2 & i,p are_relative_prime & i is_primitive_root_of p
implies (for k be Nat holds not i|^(2*k+1) is_quadratic_residue_mod p)
proof
assume
A1:p>2 & i,p are_relative_prime & i is_primitive_root_of p;
A2:order(i,p) = Euler p by A1,Def2
.= p - 1 by EULER_1:20;
A3: p>1 by INT_2:def 4;then
a4: p-'1+1=p+1-'1 by NAT_D:38
.=p+1-1 by NAT_D:37
.=p-1+1;
now assume ex k be Nat st i|^(2*k+1) is_quadratic_residue_mod p;
then consider k be Nat such that
A5: i|^(2*k+1) is_quadratic_residue_mod p;
set L=2*k+1;
set Q=p-'1;
i|^(2*k+1),p are_relative_prime by A1,WSIERP_1:10;
then i|^(2*k+1) gcd p = 1 by INT_2:def 3;then
1 = i|^L|^(Q div 2) mod p by A1,A5,INT_5:17
.= i|^((2*k+1) * ((p-'1) div 2)) mod p by NEWTON:9
.= i|^(2*k*((p-'1) div 2)+1*((p-'1) div 2)) mod p
.= (i|^(2*k*((p-'1) div 2)) * i|^((p-'1) div 2)) mod p by NEWTON:8;
then A8:(i|^(2*k*((p-'1) div 2)) * i|^((p-'1) div 2)),1
are_congruent_mod p by A3,PEPIN:39;
p is odd by A1,PEPIN:17;
then 2 divides (p-'1) by PEPIN:22,a4;then
A10: p-'1 = 2*((p-'1) div 2) by NAT_D:3;
(i|^(p-'1)) mod p = 1 by A1,PEPIN:37;
then i|^Q|^k mod p = 1 by A3,PEPIN:35;
then i|^Q|^k,1 are_congruent_mod p by A3,PEPIN:39;
then i|^(k*(p-'1)),1 are_congruent_mod p by NEWTON:9;
then (i|^(k*(p-'1)) * i|^((p-'1) div 2)),(1*i|^((p-'1) div 2))
are_congruent_mod p by INT_4:11;
then i|^((p-'1) div 2),1 are_congruent_mod p by A8,A10,PEPIN:40;then
A9: i|^((p-'1) div 2) mod p = 1 by A3,PEPIN:39;
p-1 >= 2 by A1,INT_1:52; then
A13:(p-'1) div 2 >= 2 div 2 by a4,NAT_2:24;
A11:(p-'1) divides ((p-'1) div 2) by A9,A3,A1,A2,a4,PEPIN:47;
((p-'1) div 2) divides (p-'1) by A10,NAT_D:def 3;
then 2*((p-'1) div 2) = 1*((p-'1) div 2) by A10,A11,NAT_D:5;
hence contradiction by A13,PEPIN:44;
end;
hence thesis;
end;
theorem
for k be Nat st k>=3 holds (for m st m,2|^k are_relative_prime
holds not m is_primitive_root_of 2|^k)
proof let k be Nat;
assume A1:k>=3;
now assume ex m st m,2|^k are_relative_prime
& m is_primitive_root_of 2|^k;
then consider m such that
A2: m,2|^k are_relative_prime & m is_primitive_root_of 2|^k;
now assume m is even;
then A3:2 divides m by PEPIN:22;
2|^1 divides 2|^k by A1,XXREAL_0:2,NEWTON:89;
then 2 divides 2|^k by NEWTON:5;
hence contradiction by A2,A3,PYTHTRIP:def 1;
end;
then A4:m|^(2|^(k-'2)) mod 2|^k = 1 by A1,Th22;
A5: 2|^k > 1 by A1,PEPIN:25;
order(m,2|^k) <= 2|^(k-'2) by A2,A4,A5,PEPIN:def 2;
then A6:Euler(2|^k) <= 2|^(k-'2) by A2,Def2;
A7:k>1 by XXREAL_0:2,A1;
k = (k-'1)+1 by A7,XREAL_1:235;then
A9: Euler(2|^k) = 2|^((k-'1)+1) - 2|^(k-'1) by A1,XXREAL_0:2,Th19,INT_2:28
.= 2|^(k-'1)*2 - 2|^(k-'1)*1 by NEWTON:6
.= 2|^(k-'1);
k-'1= k-1-1+1 by A7,XREAL_1:233
.=k-2+1 .= (k-'2)+1 by A1,XXREAL_0:2,XREAL_1:233;
then 2|^(k-'2) * 2 <= 2|^(k-'2) by A6,A9,NEWTON:6;
then 2|^(k-'2)*2/(2|^(k-'2))<=2|^(k-'2)/(2|^(k-'2)) by XREAL_1:72;
then 2 <= 2|^(k-'2)/(2|^(k-'2)) by XCMPLX_1:89;
then 2 <= 1 by XCMPLX_1:60;
hence contradiction;
end;
hence thesis;
end;
theorem
p>2 & k>=2 & i,p are_relative_prime & i is_primitive_root_of p
& i|^(p-'1) mod p^2 <> 1 implies i|^(Euler(p|^(k-'1))) mod p|^k <> 1
proof assume A1:p>2 & k >= 2 & i,p are_relative_prime &
i is_primitive_root_of p & i|^(p-'1) mod p^2 <> 1;
A4: p>1 by INT_2:def 4;
defpred P[Nat] means i|^(Euler(p|^($1-'1))) mod p|^$1 <> 1;
A2: P[2]
proof 2-'1 = 2-1 by XREAL_1:233
.= 1;
then A3:i|^(Euler(p|^(2-'1))) mod p|^2
= i|^(Euler p) mod p|^2 by NEWTON:5;
Euler p = p - 1 by EULER_1:20
.= p-'1 by A4,XREAL_1:233;
hence thesis by A1,A3,NEWTON:81;
end;
A5: for k be Nat st k>=2 & P[k] holds P[k+1]
proof let k be Nat;
assume A6:k>=2 & P[k];
A7: i<>0 by A1,A4,Th1;
A8: i,p|^(k-'1) are_relative_prime by A1,WSIERP_1:10;
A9: k>1 & k>0 by A6,XXREAL_0:2;
then k-1>0 by XREAL_1:50;then
A16:k-'1>0 by A6,XXREAL_0:2,XREAL_1:233;then
A10:p|^(k-'1) > 1 by A4,PEPIN:25;
i|^(Euler(p|^(k-'1))) mod p|^(k-'1) = 1 by A7,A8,A16,A4,PEPIN:25,
EULER_2:18;
then i|^(Euler(p|^(k-'1))),1 are_congruent_mod p|^(k-'1) by A10,PEPIN:39;
then p|^(k-'1) divides (i|^(Euler(p|^(k-'1))) - 1) by INT_2:15;
then consider s be Integer such that
A11:i|^(Euler(p|^(k-'1))) - 1 = p|^(k-'1) * s by INT_1:def 3;
A14:p|^k > 1 by A4,A6,PEPIN:25;
A12:p|^(k-'1) * s >= 0 by A11,XREAL_1:48,NAT_1:14,A7;
s >= 0 by A12;
then reconsider s as Element of NAT by INT_1:3;
reconsider M=s^3 as Element of NAT by ORDINAL1:def 12;
A13:p|^(k-'1) is Element of NAT & p is Element of NAT by ORDINAL1:def 12;
A15: now assume p divides s;
then p|^(k-'1) * p divides p|^(k-'1) * s by A13,PYTHTRIP:7;
then A0:p|^(k-'1+1) divides p|^(k-'1) * s by NEWTON:6;
p|^(k-'1+1)=p|^(k+1-'1) by A9,NAT_D:38
.=p|^k by NAT_D:34;
then i|^(Euler(p|^(k-'1))),1 are_congruent_mod p|^k by INT_2:15,A0,A11;
hence contradiction by A6,A14,PEPIN:39;
end;
A17:k-'1>=1 by A16,NAT_1:14;
A19: Euler(p|^k) = p|^k - p|^(k-'1) by A6,XXREAL_0:2,Th19
.= p|^(k+1-'1) - p|^(k-'1) by NAT_D:34
.= p|^(k-'1+1) - p|^(k-'1) by A6,XXREAL_0:2,NAT_D:38
.= p|^(k-'1)*p - p|^(k-'1) by NEWTON:6
.= p|^(k-'1)*p - p|^(k-'1+1-'1) by NAT_D:34
.= p|^(k-'1)*p - p|^(k-'1-'1+1) by NAT_D:38,A16,NAT_1:14
.= p|^(k-'1)*p - p|^(k-'1-'1)*p by NEWTON:6
.= (p|^(k-'1) - p|^((k-'1)-'1)) * p
.= Euler(p|^(k-'1)) * p by A16,NAT_1:14,Th19;
consider t be Nat such that
A20:(1 + p|^(k-'1) * s)|^p
= 1+p*(p|^(k-'1)*s)+(p choose 2)*(p|^(k-'1)*s)^2+t*(p|^(k-'1)*s)^3 by Th30;
a: p is odd by A1,PEPIN:17;
A26:p-'1 = p-1 by A4,XREAL_1:233;
then 2 divides (p-'1) by a,PEPIN:22;
then (p-'1) mod 2 = 0 by PEPIN:6;
then A27:(p-'1) div 2 = (p-1)/2 by A26,PEPIN:63;
A21:(1 + p|^(k-'1) * s)|^p
=1+p*p|^(k-'1)*s+(p choose 2)*(p|^(k-'1)*s)^2+t*(p|^(k-'1)*s)^3 by A20
.=1+p|^(k-'1+1)*s+(p choose 2)*(p|^(k-'1)*s)^2+t*(p|^(k-'1)*s)^3
by NEWTON:6
.=1+p|^(k+1-'1)*s+(p choose 2)*(p|^(k-'1)*s)^2+t*(p|^(k-'1)*s)^3
by A9,NAT_D:38
.=1+p|^k*s+(p choose 2)*(p|^(k-'1)*s)^2+t*(p|^(k-'1)*s)^3 by NAT_D:34
.=1+p|^k*s+p*(p-1)/2*(p|^(k-'1)*s)^2+t*(p|^(k-'1)*s)^3 by STIRL2_1:51
.=1+p|^k*s+((p-'1) div 2)*(p|^(k-'1)*p)*p|^(k-'1)*s^2+t*(p|^(k-'1)*s)^3
by A27
.=1+p|^k*s+((p-'1) div 2)*p|^(k-'1+1)*p|^(k-'1)*s^2+t*(p|^(k-'1)*s)^3
by NEWTON:6
.=1+p|^k*s+((p-'1) div 2)*p|^(k+1-'1)*p|^(k-'1)*s^2+t*(p|^(k-'1)*s)^3
by NAT_D:38,A9
.=1+p|^k*s+((p-'1) div 2)*p|^k*p|^(k-'1)*s^2+t*(p|^(k-'1)*s)^3
by NAT_D:34
.=1+p|^k*s+((p-'1) div 2)*(p|^(k-'1)*p|^k)*s^2+t*(p|^(k-'1)*s)^3
.=1+p|^k*s+((p-'1) div 2)*p|^(k-'1+k)*s^2+t*(p|^(k-'1)*s)^3
by NEWTON:8
.=1+p|^k*s+((p-'1) div 2)*p|^(k+k-'1)*s^2+t*(p|^(k-'1)*s)^3
by A9, NAT_D:38
.=1+p|^k*s+((p-'1) div 2)*p|^(2*k-'1)*s^2
+t*(p|^(k-'1)*p|^(k-'1))*p|^(k-'1)*s^3
.=1+p|^k*s+((p-'1) div 2)*p|^(2*k-'1)*s^2
+t*p|^((k-'1)+(k-'1))*p|^(k-'1)*M by NEWTON:8
.=1+p|^k*s+((p-'1) div 2)*p|^(2*k-'1)*s^2
+t*(p|^((k-'1)+(k-'1))*p|^(k-'1))*M
.=1+p|^k*s+((p-'1) div 2)*p|^(2*k-'1)*s^2+t*p|^((k-'1)
+(k-'1)+(k-'1))*M by NEWTON:8
.=1+p|^k*s+((p-'1) div 2)*p|^(2*k-'1)*s^2+t*M*p|^(3*(k-'1));
k-'1+k>=1+k by A17,XREAL_1:6;
then A22:k+k-'1>=k+1 by A6,XXREAL_0:2,NAT_D:38;then
A23:p|^(k+1) divides (((p-'1) div 2)*s^2*p|^(2*k-'1)) by Lm,NAT_D:9;
k+2*k>=2+2*k by A6,XREAL_1:6;
then A24:3*k-3>=2*k+2-3 by XREAL_1:9;
2*k>2*1 by A9,XREAL_1:68;
then 2*k-'1=2*k-1 by XXREAL_0:2,XREAL_1:233;
then 3*(k-1)>=k+1 by A22,A24,XXREAL_0:2;
then 3*(k-'1)>=k+1 by A6,XXREAL_0:2,XREAL_1:233;
then p|^(k+1) divides (t*M*p|^(3*(k-'1))) by Lm,NAT_D:9;then
A28:p|^(k+1) divides (((p-'1) div 2)*p|^(2*k-'1)*s^2+t*M*p|^(3*(k-'1)))
by A23,NAT_D:8;
i|^(Euler(p|^k)) = (1 + p|^(k-'1) * s)|^p by A11,A19,NEWTON:9;
then A29:p|^(k+1) divides ((i|^(Euler(p|^k))-1)-p|^k*s) by A21,A28;
now assume A30:i|^(Euler(p|^((k+1)-'1))) mod p|^(k+1) = 1;
p|^(k+1)>1 by A4,PEPIN:25;
then i|^(Euler(p|^((k+1)-'1))),1 are_congruent_mod p|^(k+1)
by A30,PEPIN:39;
then p|^(k+1) divides (i|^(Euler(p|^((k+1)-'1)))-1) by INT_2:15;
then p|^(k+1) divides (i|^(Euler(p|^k))-1) by NAT_D:34;
then p|^(k+1) divides p|^k*s by A29,INT_5:2;then
A31: p|^k*p divides p|^k*s by NEWTON:6;
p|^k is Element of NAT by ORDINAL1:def 12;
hence contradiction by A15,A13,A31,PYTHTRIP:7;
end;
hence thesis;
end;
for k be Nat st k>=2 holds P[k] from NAT_1:sch 8(A2,A5);
hence thesis by A1;
end;
theorem
n>1 & len fp>=2 & (for d st d in dom fp holds fp.d,n are_relative_prime)
implies for fr st len fr = len fp & (for d st d in dom fr holds
fr.d = order(fp.d,n)) & (for d,e st d in dom fr & e in dom fr & d <> e
holds fr.d,fr.e are_relative_prime) holds order((Product fp),n) = Product fr
proof
defpred RP[FinSequence of NAT] means
for d st d in dom $1 holds $1.d,n are_relative_prime;
defpred CC[FinSequence of NAT] means
for fr st len fr = len $1 & (for d st d in dom fr holds
fr.d = order($1.d,n)) & (for d,e st d in dom fr & e in dom fr & d <> e
holds fr.d,fr.e are_relative_prime) holds order((Product $1),n) = Product fr;
defpred TH[FinSequence of NAT] means
(n>1 & len $1>=2 & RP[$1]) implies CC[$1];
A1:TH[<*>NAT qua FinSequence of NAT];
A2:for fp,c st TH[fp] holds TH[fp^<*c*>]
proof let fp,c; assume A3:TH[fp];
set fp1=fp^<*c*>;
TH[fp1]
proof
assume A4:n>1 & len fp1>=2 & RP[fp1];
A5: len fp1=len fp+1 by FINSEQ_2:16;
per cases by A4,XXREAL_0:1;
suppose A6:len fp1 = 2;
then fp1=<*(fp1.1),(fp1.2)*> by FINSEQ_1:44;
then A7:Product fp1=(fp1.1)*(fp1.2) by RVSUM_1:99;
dom fp1 = Seg 2 by A6,FINSEQ_1:def 3; then
A8: 1 in dom fp1 & 2 in dom fp1;then
A9: fp1.1,n are_relative_prime & fp1.2,n are_relative_prime by A4;
CC[fp1]
proof
let fr;
assume A10:len fr = len fp1 & (for d st d in dom fr holds
fr.d = order(fp1.d,n)) & (for d,e st d in dom fr & e in dom fr
& d<>e holds fr.d,fr.e are_relative_prime);
then A11:1 in dom fr & 2 in dom fr by A8,FINSEQ_3:29;
then fr.1,fr.2 are_relative_prime by A10;
then order(fp1.1,n),fr.2 are_relative_prime by A10,A11;then
A13: order(fp1.1,n),order(fp1.2,n) are_relative_prime by A10,A11;
fr=<*fr.1,fr.2*> by A6,A10,FINSEQ_1:44;
then Product fr = fr.1*fr.2 by RVSUM_1:99
.= order(fp1.1,n) * fr.2 by A10,A11
.= order(fp1.1,n)*order(fp1.2,n) by A10,A11;
hence thesis by A13,A4,A7,A9,Th9;
end;
hence thesis;
end;
suppose len fp1 > 2;
then len fp + 1 > 2 by FINSEQ_2:16;
then A14:len fp +1 -1 >= 2 by INT_1:52;
A29: RP[fp]
proof let d; assume A15:d in dom fp;
then fp1.d = fp.d by FINSEQ_1:def 7;
hence thesis by A4,A15,FINSEQ_2:15;
end;
CC[fp1]
proof
let fr;
assume A19:len fr = len fp1 & (for d st d in dom fr holds
fr.d = order(fp1.d,n)) & (for d,e st d in dom fr & e in dom fr
& d<>e holds fr.d,fr.e are_relative_prime);
then consider f be FinSequence of NAT,l be Element of NAT such that
A20: fr = f ^ <*l*> by FINSEQ_2:19;
A21: len f + 1 = len fp + 1 by A5,A19,A20,FINSEQ_2:16;
A22: for d st d in dom f holds f.d = order(fp.d,n)
proof let d; assume A23:d in dom f;
then A24:f.d = fr.d by A20,FINSEQ_1:def 7;
A27: d in dom fr by A23,A20,FINSEQ_2:15;
dom f = dom fp by A21,FINSEQ_3:29;
then fp.d = fp1.d by A23,FINSEQ_1:def 7;
hence thesis by A27,A19,A24;
end;
for d,e st d in dom f & e in dom f & d<>e
holds f.d,f.e are_relative_prime
proof let d,e; assume A25:d in dom f & e in dom f & d<>e;
then A26:f.d = fr.d & f.e = fr.e by A20,FINSEQ_1:def 7;
d in dom fr & e in dom fr by A25,A20,FINSEQ_2:15;
hence thesis by A25,A19,A26;
end;
then A28:order(Product fp,n)=Product f by A21,A22,A29,A3,A4,A14;
A30: for d be Nat st d in dom fp holds (fp.d) gcd n = 1
by A29,INT_2:def 3;
(Product fp) gcd n = 1 by A30,WSIERP_1:36;
then A31:(Product (fp)),n are_relative_prime by INT_2:def 3;
reconsider z = 0, j = 1 as Element of NAT;
len fp+j>=z+j by XREAL_1:7;then
(len fp+1) in dom fp1 by A5,FINSEQ_3:25;
then fp1.(len fp+1),n are_relative_prime by A4;
then A33:c,n are_relative_prime by FINSEQ_1:42;
len f+j >= z+j by XREAL_1:7;
then len fr >= j by A20,FINSEQ_2:16;
then A38:len fr in dom fr by FINSEQ_3:25;
then fr.(len fr)=order(fp1.(len fr),n) by A19
.=order(fp1.(len fp+1),n) by A19,FINSEQ_2:16
.=order(c,n) by FINSEQ_1:42;
then A34:fr.(len f+1) = order(c,n) by A20,FINSEQ_2:16;
A40: Product fp1 = Product fp * c & Product fr = Product f * l
by A20,RVSUM_1:96;
for d be Nat st d in dom f holds f.d gcd fr.(len f +1) = 1
proof let d be Nat; assume A35:d in dom f;
then A36:d in dom fr by A20,FINSEQ_2:15;
d<=len f by A35,FINSEQ_3:25;then
A39: d