:: Basic Properties of Primitive Root and Order Function
:: by Na Ma and Xiquan Liang
::
:: Received August 6, 2012
:: Copyright (c) 2012-2026 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,
XCMPLX_0, NUMBER09;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, 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,
NEWTON, NAT_3, XXREAL_0, NUMBERS, XBOOLE_0, XREAL_0, ORDINAL1, VALUED_0,
ABIAN, MEMBER_1, XCMPLX_0, WSIERP_1, INT_4, VALUED_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities SQUARE_1, FINSEQ_1, EULER_1, POLYEQ_3;
expansions TARSKI, 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_coprime & 1 <= k & k <= m};
correctness;
end;
theorem Th1:
RelPrimes(m) c= Seg m
proof
let x be object;
assume x in RelPrimes(m);
then ex k be Element of NAT st
k = x & m,k are_coprime & k >= 1 & k <= m;
hence x in Seg m;
end;
registration
let m;
cluster RelPrimes(m) -> included_in_Seg;
coherence
proof
RelPrimes(m) c= Seg m by Th1;
hence thesis by FINSEQ_1:def 13;
end;
end;
definition
let m be Nat;
redefine func RelPrimes(m) -> Subset of NAT; :: redefines RelPrimes (INT_8, definition)
coherence
proof
RelPrimes(m) c= Seg m by Th1;
hence thesis by XBOOLE_1:1;
end;
end;
registration
let m be Nat;
cluster RelPrimes(m) -> finite;
coherence;
end;
theorem
1 <= m implies RelPrimes(m) <> {}
proof
assume A1:1<=m;
m gcd 1 = 1 by NEWTON:51;
then m,1 are_coprime by INT_2:def 3;
then 1 in RelPrimes(m) by A1;
hence thesis;
end;
theorem Th3:
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
A1: x = a * z and
A2: z in X by MEMBER_1:195;
reconsider z as Integer by A2;
take z;
thus z in X & x = a * z by A2,A1;
end;
thus thesis by MEMBER_1:193;
end;
theorem Th4:
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;
A1: 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
A2: (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 A2,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;
A3: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(A3,A1);
hence thesis;
end;
theorem Th5:
n>1 & i,n are_coprime implies i <> 0
proof
assume A1:n>1 & i,n are_coprime;
assume i = 0;
then i gcd n > 1 by A1,NEWTON:52;
hence contradiction by A1,INT_2:def 3;
end;
theorem Th6:
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;
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;
Lm1:
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 A1:x = 2*y+1 by ABIAN:1;
x*(x+1) = 2*((2*y+1)*(y+1)) by A1;
hence thesis by INT_1:def 3;
end;
end;
theorem Th7:
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
.= 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 Lm1;
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];
A9: k>0 & k>1 & k>2 by A8,XXREAL_0:2;
A10: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 A9,XREAL_1:233;
then A11:x|^(2|^(k-'2)) = x|^(2|^(k-'3)*2) by A10,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,A11,PEPIN:39;
then consider t be Integer such that
A12: 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 A13: x|^(2|^((k-'2)+1)) = (t*2|^k + 1)^2 by A12
.= 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 A9,XREAL_1:8;
then
A14: 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
A15: 2|^(k+1) divides (t^2*(2|^(2*k)) + 2|^(k+1)*t) by A14,WSIERP_1:4;
A16: (t^2*(2|^(2*k)) + 2|^(k+1)*t) mod 2|^(k+1) = 0 by A15,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,A9
.= (((t^2*(2|^(2*k)) + 2|^(k+1)*t) mod 2|^(k+1)) + (1 mod 2|^(k+1)))
mod 2|^(k+1) by A13,NAT_D:66
.= 1 mod 2|^(k+1) by A16,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;
Lm2:k <= n implies m |^ k divides m |^ n by NEWTON:89;
theorem Th8:
m>=1 implies Euler(p|^m) = p|^m - p|^(m-'1)
proof assume A1: m >= 1;
set X = {k where k is Element of NAT :
p|^m,k are_coprime & k >= 1 & k <= p|^m};
set X1 = {k where k is Element of NAT :
not p|^m,k are_coprime & k >= 1 & k <= p|^m};
set X2 = {k where k is Element of NAT :
not p,k are_coprime & 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;
A2: X1 = X2
proof thus X1 c= X2
proof let a be object;
assume a in X1;
then consider b be Element of NAT such that
A3: b = a & not p|^m,b are_coprime & b >= 1 & b <= p|^m;
not p,b are_coprime by A3,WSIERP_1:10;
hence thesis by A3;
end;
let a be object;
assume a in X2;
then consider k be Element of NAT such that
A4: k = a & not p,k are_coprime & k >= 1 & k <= p|^m;
p gcd k = p by A4,PEPIN:2;then
A5: p divides k by NAT_D:def 5;
p|^1 divides p|^m by A1,NEWTON:89;then
A6: p divides p|^m;
now assume p|^m,k are_coprime;
then p = 1 by A5,A6,PYTHTRIP:def 1;
hence contradiction by INT_2:def 4;
end;
hence thesis by A4;
end;
A7: X2 = X3
proof thus X2 c= X3
proof let x be object;
assume x in X2;
then consider k be Element of NAT such that
A8: x = k & not p,k are_coprime & k >= 1 & k <= p|^m;
p gcd k = p by A8,PEPIN:2;
then p divides k by NAT_D:def 5;
hence thesis by A8;
end;
let x be object;
assume x in X3;
then consider k be Element of NAT such that
A9: x = k & p divides k & k >= 1 & k <= p|^m;
p gcd k = p by A9,NEWTON:49;
then p gcd k > 1 by INT_2:def 4;
then not p,k are_coprime by INT_2:def 3;
hence thesis by A9;
end;
X3 c= Seg(p|^m)
proof
let x be object;
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 A2,A7,XBOOLE_1:1;
deffunc F(Nat) = $1 * p;
consider f be FinSequence such that
A10:len f = w & for d be Nat st d in dom f holds f.d = F(d)
from FINSEQ_1:sch 2;
A11: rng f = X3
proof thus rng f c= X3
proof let a be object;
assume a in rng f;
then consider s be Nat such that
A12: s in dom f & f.s = a by FINSEQ_2:10;
A13: a = s * p by A12,A10;then
reconsider a as Element of NAT by ORDINAL1:def 12;
A14: p divides a by A13,NAT_D:def 3;
s in Seg w by A12,A10,FINSEQ_1:def 3;
then A15:s >= 1 & s <= w by FINSEQ_1:1;
p > 1 by INT_2:def 4;
then A16:s * p >= 1*1 by A15,XREAL_1:66;
s * p <= w * p by A15,XREAL_1:66;
then A17:s * p <= p|^((m-'1) + 1) by NEWTON:6;
p|^((m-'1) + 1)=p|^(m + 1-'1 ) by A1,NAT_D:38
.=p|^m by NAT_D:34;
hence thesis by A13,A14,A16,A17;
end;
let a be object;
assume a in X3;
then consider k be Element of NAT such that
A18: a = k & p divides k & k >= 1 & k <= p|^m;
consider t be Nat such that A19:k = p * t by A18,NAT_D:def 3;
t <> 0 by A19,A18;
then A20:t >= 1 by NAT_1:14;
p|^m = p|^(m + 1 -' 1) by NAT_D:34
.=p|^(m-'1+1) by A1,NAT_D:38
.=p|^(m-'1) * p by NEWTON:6;
then p * t / p <= p|^(m-'1) * p / p by XREAL_1:72,A18,A19;
then t <= w * p / p by XCMPLX_1:89;
then t <= w by XCMPLX_1:89;
then t in Seg w by A20;then
A21: t in dom f by A10,FINSEQ_1:def 3;
f.t = t * p by A21,A10;
hence thesis by A18,A19,A21,FUNCT_1:3;
end;
for a,b be object st a in dom f & b in dom f & f.a = f.b holds a = b
proof let a,b be object;
assume A22: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 A22,A10;
hence thesis by A22,XCMPLX_1:5;
end;
then f is one-to-one by FUNCT_1:def 4; then
A23:w = card X1 by A2,A7,A10,A11,FINSEQ_4:62;
A24: X1 c= Seg(p|^m)
proof let x be object;
assume x in X1;
then consider k be Element of NAT such that
A25: x = k & not p|^m,k are_coprime & k >= 1 & k <= p|^m;
thus thesis by A25;
end;
A26: X c= Seg(p|^m)
proof let x be object;
assume x in X;
then consider k be Element of NAT such that
A27: x = k & p|^m,k are_coprime & k >= 1 & k <= p|^m;
thus thesis by A27;
end;
then A28:X1 \/ X c= Seg(p|^m) by A24,XBOOLE_1:8;
reconsider X as finite Subset of NAT by A26,XBOOLE_1:1;
Seg(p|^m) c= X1 \/ X
proof let x be object;
assume A29:x in Seg(p|^m);
then reconsider x as Element of NAT;
A30: x >= 1 & x <= p|^m by A29,FINSEQ_1:1;
per cases;
suppose p|^m,x are_coprime;
then x in X by A30;
hence thesis by XBOOLE_0:def 3;
end;
suppose not p|^m,x are_coprime;
then x in X1 by A30;
hence thesis by XBOOLE_0:def 3;
end;
end;
then A31: X1 \/ X = Seg(p|^m) by A28;
not ex x being object st x in X1 /\ X
proof
given x be object such that A32: x in X1 /\ X;
A33: x in X1 & x in X by A32,XBOOLE_0:def 4;
then consider k1 be Element of NAT such that
A34: x = k1 & not p|^m,k1 are_coprime & k1 >= 1 & k1 <= p|^m;
consider k2 be Element of NAT such that
A35: x = k2 & p|^m,k2 are_coprime & k2 >= 1 & k2 <= p|^m by A33;
thus contradiction by A34,A35;
end;
then X1 /\ X = {} by XBOOLE_0:def 1;
then X1 misses X;
then card X1 + card X = card Seg(p|^m) by A31,CARD_2:40;
then w + card X = p|^m by A23,FINSEQ_1:57;
hence thesis;
end;
theorem
n>1 & i,n are_coprime implies order(i,n) divides Euler n
proof
assume
A1:n>1 & i,n are_coprime;
(i |^ Euler n) mod n = 1 by Th5,A1,EULER_2:18;
hence thesis by A1,PEPIN:47;
end;
theorem Th10:
for i,n st n>1 & i,n are_coprime 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_coprime;
A2:i <> 0 & n > 0 by A1,Th5;
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 A3: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 A5: s = t + l by NAT_1:10;
n divides (i|^s - i|^t) by A3,INT_2:15;
then n divides (i|^t * i|^l - i|^t * 1) by A5,NEWTON:8;
then A6:n divides (i|^t * (i|^l - 1));
reconsider ll = i|^l - 1 as Element of NAT by NAT_1:21,14,A2;
A7: n gcd i|^t = 1 by A4,A2,NAT_4:10;
n divides ll by A6,A7,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 A5,A1,PEPIN:47;
hence thesis by INT_2:15;
end;
suppose s < t;
then consider l be Nat such that A8:t = s + l by NAT_1:10;
i|^t,i|^s are_congruent_mod n by A3,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 A8,NEWTON:8;
then A9:n divides (i|^s * (i|^l - 1));
A10: n gcd i|^s = 1 by A4,A2,NAT_4:10;
reconsider ll = i|^l - 1 as Element of NAT by NAT_1:21,14,A2;
n divides ll by A10,A9,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,A8,PEPIN:47;
then t,s are_congruent_mod R by INT_2:15;
hence thesis by INT_1:14;
end;
end;
assume A11:s,t are_congruent_mod R;
A12:R > 0 by A1,PEPIN:def 2;
then A13:s = (s div R) * R + (s mod R) &
t = (t div R) * R + (t mod R) by NEWTON:66;
then A14: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;
A15: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;
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 A16:i|^s mod n = i|^(s mod R) mod n by A14,NAT_D:64;
A17:i|^t = i|^ (R * (t div R)) * i|^(t mod R) by NEWTON:8,A13
.= 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 A15,INT_4:8
.= 1 mod n;
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 A18:i|^t mod n = i|^(t mod R) mod n by A17,NAT_D:64;
s mod R = (s mod R) mod R & t mod R = (t mod R) mod R by NAT_D:73;
then A19:s,(s mod R) are_congruent_mod R
& t,(t mod R) are_congruent_mod R by A12,NAT_D:64;
then t,(s mod R) are_congruent_mod R by A11,PEPIN:40;
then (s mod R),(t mod R) are_congruent_mod R by A19,PEPIN:40;
then A20: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 A20,INT_4:6;
then A21: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;
A22: sR < RR & sR >= 0 & tR < RR & tR >= 0 by A12,NAT_D:1;
sR - tR <= sR by XREAL_1:43; then
A23: sR - tR < RR by A22,XXREAL_0:2;
A24: (-1)*tR > (-1)*RR by XREAL_1:69,A22;
sR + -tR >= -tR by XREAL_1:31; then
sR + -tR > rR by XXREAL_0:2,A24;
hence contradiction by A21,SEQ_2:1,A23;
end;
hence thesis by A1,A16,A18,NAT_D:64;
end;
theorem
for i,n st n>1 & i,n are_coprime 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_coprime;
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,Th10;
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,Th10;
hence thesis by NEWTON:4;
end;
theorem
n>1 & i,n are_coprime & 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_coprime & len fn = order(i,n) &
(for d st d in dom fn holds fn.d = i|^(d-'1));
then A2:i <> 0 & n <> 0 by Th5;
A3: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
A4: d in dom fn & e in dom fn & d<>e & fn.d,fn.e are_congruent_mod n;
A5: d>=1 & d<=order(i,n) & e>=1 & e<=order(i,n) by A4,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
A6: d-'1=d-1;
e-'1+1=e+1-'1 by NAT_D:38,A5
.=e+1-1 by NAT_D:37
.=e-1+1; then
A7: d-1=d-'1 & e-1=e-'1 by A6;
per cases by A4,XXREAL_0:1;
suppose d > e;
then A8: e-'1 < d-'1 by A7,XREAL_1:9;
then consider k be Nat such that A9:d-'1=(e-'1)+k by NAT_1:10;
reconsider ll = i|^k - 1 as Element of NAT by A2,NAT_1:21,14;
A10: i|^(d-'1) - i|^(e-'1)
= i|^(e-'1) * i|^k - i|^(e-'1) * 1 by A9,NEWTON:8
.= i|^(e-'1) * ll;
A11: i|^(e-'1) gcd n = 1 by A2,A3,NAT_4:10;
i|^(d-'1),fn.e are_congruent_mod n by A1,A4;
then i|^(d-'1),i|^(e-'1) are_congruent_mod n by A1,A4;
then n divides i|^(d-'1) - i|^(e-'1) by INT_2:15;
then n divides ll by A10,A11,WSIERP_1:30;
then i|^k,1 are_congruent_mod n by INT_2:15;
then A12:i|^k mod n = 1 mod n by NAT_D:64
.= 1 by A1,PEPIN:5;
A13: (d-'1)-(e-'1)>0 by A8,XREAL_1:50;
A14: order(i,n) <= k by A13,A9,NAT_D:7,A1,A12,PEPIN:47;
d-e <= order(i,n)-1 by A5,XREAL_1:13;
hence contradiction by A7,A9,A14,XXREAL_0:2,XREAL_1:146;
end;
suppose e > d;
then A15:e-'1 > d-'1 by A7,XREAL_1:9;
then consider k be Nat such that A16:e-'1=(d-'1)+k by NAT_1:10;
reconsider ll = i|^k - 1 as Element of NAT by A2,NAT_1:21,14;
A17: i|^(e-'1) - i|^(d-'1)
= i|^(d-'1) * i|^k - i|^(d-'1) * 1 by A16,NEWTON:8
.= i|^(d-'1) * ll;
A18: i|^(d-'1) gcd n = 1 by A2,A3,NAT_4:10;
i|^(d-'1),fn.e are_congruent_mod n by A1,A4;
then i|^(d-'1),i|^(e-'1) are_congruent_mod n by A1,A4;
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 A17,A18,WSIERP_1:30;
then i|^k,1 are_congruent_mod n by INT_2:15;
then A19:i|^k mod n = 1 mod n by NAT_D:64
.= 1 by A1,PEPIN:5;
A20: (e-'1)-(d-'1)>0 by A15,XREAL_1:50;
A21: order(i,n) <= k by A16,A20,NAT_D:7,A1,A19,PEPIN:47;
e-d <= order(i,n)-1 by A5,XREAL_1:13;
hence contradiction by A16,A21,A7,XXREAL_0:2,XREAL_1:146;
end;
end;
theorem
n>1 & i,n are_coprime & 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_coprime & 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 A2:fn.d = i|^(d -' 1) by A1;
A3:fn.d|^order(i,n) mod n
= i|^(K*(d-'1)) mod n by NEWTON:9,A2
.= 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
.= 1 by A1,PEPIN:5;
hence thesis by A3;
end;
theorem Th14:
n>1 & i,n are_coprime
implies order(i|^s,n) = order(i,n) div (order(i,n) gcd s)
proof assume A1:n>1 & i,n are_coprime;
then A2:i <> 0 & n <> 0 by Th5;
i gcd n = 1 by A1,INT_2:def 3;then
i|^s gcd n = 1 by A2,NAT_4:10;then
A3:i|^s,n are_coprime by INT_2:def 3;
A4: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 A5:s = 0;
then K1 = order(i,n) by NEWTON:52;
then A6:K2 = 1 by A4,NAT_2:3;
i|^s = 1 by A5,NEWTON:4;
hence thesis by A1,A6,PEPIN:46;
end;
suppose A7:s > 0;
K1 divides order(i,n) & K1 divides s by NAT_D:def 5; then
A8: order(i,n) = K2 * K1 & s = (s div K1) * K1 by NAT_D:3; then
A9:K2 <> 0 & K1 <> 0 & (s div K1) <> 0 by A1,A7,PEPIN:def 2;
A10: K2,(s div K1) are_coprime by A8,A9,EULER_1:6;
s * K2 = (s div K1) * order(i,n) by A8;
then order(i,n) divides s * K2 by NAT_D:def 3;
then (i|^(s * K2)) mod n = 1 by A1,PEPIN:48;
then A11:(i|^s|^K2) mod n = 1 by NEWTON:9;
for k be Nat st k > 0 & (i|^s|^k) mod n = 1 holds K2 <= k
proof let k be Nat;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
assume A12: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 A8,A1,PEPIN:47;
then K2 divides ((s div K1) * k1) by A9,PYTHTRIP:7;
hence thesis by A12,A10,PEPIN:3,NAT_D:7;
end;
hence thesis by A1,A3,A9,A11,PEPIN:def 2;
end;
end;
theorem
for i,n st n>1 & i,n are_coprime holds
order(i,n),s are_coprime iff order(i|^s,n) = order(i,n)
proof let i,n;
assume A1:n>1 & i,n are_coprime;
thus order(i,n),s are_coprime implies order(i|^s,n) = order(i,n)
proof assume order(i,n),s are_coprime;
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);
hence thesis by A1,Th14;
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,Th14;
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;
A5:order(i,n)>0 by A1,PEPIN:def 2;
then A6:d<=order(i,n) by A3,NAT_D:7;
d<>0 by A5,INT_2:5;
then order(i,n) div d <> 0 by A6,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_coprime & order(i,n) = s*t
implies order(i|^s,n) = t
proof assume A1:n>1 & i,n are_coprime & order(i,n) = s*t;
then A2:i <> 0 by Th5;
A3: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 A2,A1,NAT_4:10;
then A4:i|^s,n are_coprime by INT_2:def 3;
A5:i|^s|^t mod n = i|^order(i,n) mod n by A1,NEWTON:9
.=1 by A1,PEPIN:def 2;
A6: for k be Nat st k>0 & (i|^s|^k) mod n = 1 holds t <= k
proof let k be Nat;
assume A7:k>0 & (i|^s|^k) mod n = 1;
then A8: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 A8,A1,PEPIN:47;
then t divides k by A3,PYTHTRIP:7;
hence thesis by A7,NAT_D:7;
end;
t is Element of NAT by ORDINAL1:def 12;
hence thesis by A1,A4,A3,A6,A5,PEPIN:def 2;
end;
theorem Th17:
n>1 & s,n are_coprime & t,n are_coprime &
order(s,n),order(t,n) are_coprime implies
order(s*t,n) = order(s,n)*order(t,n)
proof assume A1:n>1 & s,n are_coprime & t,n are_coprime &
order(s,n),order(t,n) are_coprime;
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_coprime by INT_2:def 3;
set L = order(s,n)*order(t,n);
A3:((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 .= 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
A4:((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;
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 A4,NAT_D:64;
then A5:t|^(order(s,n) * order(s*t,n)) mod n = 1 by NEWTON:9;
A6:order(t,n) divides order(s*t,n) by A1,A5,PEPIN:47,PEPIN:3;
((s*t)|^order(s*t,n))|^order(t,n) mod n = 1|^order(t,n) mod n
by A3,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 .= 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
A7:((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;
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 A7,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 A8:L divides order(s*t,n) by A6,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 A8,NAT_D:5;
end;
reserve fp,fr for FinSequence of NAT;
theorem
n>1 & s,n are_coprime & t,n are_coprime &
order(s*t,n) = order(s,n)*order(t,n) implies
order(s,n),order(t,n) are_coprime
proof assume A1:n>1 & s,n are_coprime & t,n are_coprime &
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 A2:s*t,n are_coprime 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 A3: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 A4:L divides order(s*t,n) by NAT_D:def 4;
A5: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,A5,PEPIN:48 .= 1 mod n by A1,PEPIN:5;
then t|^L,1 are_congruent_mod n by A1,NAT_D:64;
then A7: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 A7,NEWTON:7;
then A8: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 A8,A1,A2,PEPIN:47;
then L = order(s,n)*order(t,n) by A1,A4,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 A3,XCMPLX_1:5;
hence thesis by INT_2:def 3;
end;
theorem
n>1 & s,n are_coprime & s*t mod n = 1
implies order(s,n)=order(t,n)
proof assume A1:n>1 & s,n are_coprime & s*t mod n = 1;
set f = t gcd n;
A2: now assume not t,n are_coprime;
then A3:f <> 1 by INT_2:def 3;
f <> 0 by A1,INT_2:5;
then A4:f > 1 by A3,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;
A8:order(s,n)>0 by A1,PEPIN:def 2;
set M=s*t;
A9: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 .= 1 by A1,PEPIN:5;
then A10:(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
A11:t|^order(s,n) mod n = 1 by A10,Th6;
for k be Nat st k > 0 & (t|^k) mod n = 1 holds order(s,n) <= k
proof let k be Nat;
assume A12:k > 0 & (t|^k) mod n = 1;
M|^k mod n = 1|^k mod n by A9,INT_4:8
.= 1 mod n .= 1 by A1,PEPIN:5;
then (s|^k * t|^k) mod n = 1 by NEWTON:7;
then s|^k mod n = 1 by A12,Th6;
hence thesis by A1,A12,PEPIN:def 2;
end;
hence thesis by A11,A8,A2,A1,PEPIN:def 2;
end;
theorem Th20:
n>1 & m>1 & i,n are_coprime & m divides n
implies order(i,m) divides order(i,n)
proof
assume A1:n>1 & m>1 & i,n are_coprime & m divides n;
i gcd n = 1 by A1,INT_2:def 3;
then i gcd m = 1 by A1,WSIERP_1:16;
then A2:i,m are_coprime 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,A2,PEPIN:47;
end;
theorem
n>1 & m>1 & m,n are_coprime & i,m*n are_coprime
implies order(i,m*n) = order(i,m) lcm order(i,n)
proof
assume
A1: n>1 & m>1 & m,n are_coprime & i,m*n are_coprime;
then A2:m*n>1*1 by XREAL_1:98;
then i <> 0 by A1,Th5; then
A3: i>0;
set K = order(i,m) lcm order(i,n);
A4: 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,Th20;
then A5: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 A4,WSIERP_1:16;then
A6: i,m are_coprime & i,n are_coprime by INT_2:def 3;
i|^K-1>=0 by NAT_1:14,XREAL_1:48,A3;
then A7: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,A6,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,A7,PEPIN:4;
then i|^K,1 are_congruent_mod m*n by INT_2:15;then
A8:i|^K mod m*n = 1 by A2,PEPIN:39;
order(i,m*n) divides K by A1,A2,A8,PEPIN:47;
hence thesis by A5,NAT_D:5;
end;
definition
let X be set,m be Nat;
pred X is_RRS_of m means
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 Th22:
RelPrimes(m) is_RRS_of m
proof
A2: rng Sgm RelPrimes(m) = RelPrimes(m) &
len Sgm RelPrimes(m) = len Sgm RelPrimes(m) by FINSEQ_1:def 14;
rng Sgm RelPrimes(m) c= INT by RELAT_1:def 19;
then A3: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 A2,A3;
end;
theorem Th23:
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;
rng Sgm RelPrimes(m) = RelPrimes(m) by FINSEQ_1:def 14;
then A3:(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
A4: k1=(Sgm RelPrimes(m)).d & m,k1 are_coprime & k1>=1 & k1<=m;
consider k2 be Element of NAT such that
A5: k2=(Sgm RelPrimes(m)).e & m,k2 are_coprime & k2>=1 & k2<=m by A3;
A6:((Sgm RelPrimes(m)).d)-((Sgm RelPrimes(m)).e)<=m-1 &
1-m<=((Sgm RelPrimes(m)).d)-((Sgm RelPrimes(m)).e) by A4,A5,XREAL_1:13;
A7: m-1<m by XREAL_1:146;
A8: ((Sgm RelPrimes(m)).d)-((Sgm RelPrimes(m)).e)<m
by A6,XXREAL_0:2,XREAL_1:146;
-m < -(m-1) by A7,XREAL_1:24;
then -m<((Sgm RelPrimes(m)).d)-((Sgm RelPrimes(m)).e)
by A6,XXREAL_0:2; then
A9: |.(((Sgm RelPrimes(m)).d)-((Sgm RelPrimes(m)).e)).|<m by A8,SEQ_2:1;
now assume (Sgm RelPrimes(m)).d,(Sgm RelPrimes(m)).e are_congruent_mod m;
then A10:m divides (((Sgm RelPrimes(m)).d)-((Sgm RelPrimes(m)).e))
by INT_2:15;
Sgm RelPrimes(m) is one-to-one by FINSEQ_3:92;
then ((Sgm RelPrimes(m)).d)-((Sgm RelPrimes(m)).e) <> 0
by A1,FUNCT_1:def 4;
then |.m.| <= |.(((Sgm RelPrimes(m)).d)-((Sgm RelPrimes(m)).e)).|
by A10,INT_4:6;
hence contradiction by A9,ABSVALUE:def 1;
end;
hence thesis;
end;
theorem Th24:
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_coprime)
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;
A2:dom fp = dom (Sgm RelPrimes(m)) by A1,FINSEQ_3:29;
for a,b be object st a in dom fp & b in dom fp & fp.a = fp.b holds a = b
proof let a,b be object;
assume A3:a in dom fp & b in dom fp & fp.a = fp.b;
reconsider a,b as Element of NAT by A3;
reconsider l=fp.a,ll=fp.b as Element of INT by A3,FINSEQ_2:11;
l in Class(Cong(m),(Sgm RelPrimes(m)).a) &
ll in Class(Cong(m),(Sgm RelPrimes(m)).b) by A1,A3;
then [(Sgm RelPrimes(m)).a,l] in Cong(m) &
[(Sgm RelPrimes(m)).b,ll] in Cong(m) by EQREL_1:18;
then A4:(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 A3,INT_1:14;
hence thesis by Th23,A3,A2,A4,INT_1:15;
end;
then A5:fp is one-to-one by FUNCT_1:def 4;
A7:card X = len(Sgm RelPrimes(m)) by A1,FINSEQ_4:62,A5
.= Euler m by FINSEQ_3:39;
A8: 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 A9:x in X & y in X & x<>y; then
consider d be Nat such that
A10: d in dom fp & fp.d = x by A1,FINSEQ_2:10;
consider e be Nat such that
A11: e in dom fp & fp.e = y by A1,A9,FINSEQ_2:10;
A12: d in dom Sgm RelPrimes(m) & e in dom Sgm RelPrimes(m)
by A10,A11,A1,FINSEQ_3:29;
reconsider d,e as Element of NAT by A10,A11;
fp.d in Class(Cong m,(Sgm RelPrimes(m)).d) &
fp.e in Class(Cong m,(Sgm RelPrimes(m)).e) by A10,A11,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,A10,A11,A9,Th23,A13,INT_1:15;
end;
hence thesis by A10,A11;
end;
for x be Integer st x in X holds x,m are_coprime
proof let x be Integer;
assume x in X;
then consider d be Nat such that
A14: d in dom fp & fp.d = x by A1,FINSEQ_2:10;
reconsider d as Element of NAT by A14;
fp.d in Class(Cong m,(Sgm RelPrimes(m)).d) by A1,A14;
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 A15:(Sgm RelPrimes(m)).d gcd m = fp.d gcd m by WSIERP_1:43;
rng (Sgm RelPrimes(m)) = RelPrimes(m) by FINSEQ_1:def 14;
then (Sgm RelPrimes(m)).d in RelPrimes(m) by A2,A14,FUNCT_1:def 3;
then consider k be Element of NAT such that
A16: (Sgm RelPrimes(m)).d=k & m,k are_coprime & k>=1 & k<=m;
fp.d gcd m = 1 by A15,A16,INT_2:def 3;
hence thesis by A14, INT_2:def 3;
end;
hence thesis by A7,A8;
end;
Lm3:
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 Th24;
hence thesis by PEPIN:42;
end;
assume A1:m = 0;
reconsider fp=<*>INT as FinSequence of INT;
RelPrimes m c= Seg m by Th1; then
card RelPrimes(m) <= card Seg m by NAT_1:43;
then card RelPrimes(m) <= 0 by A1;
then card RelPrimes(m) = 0;
then A2:len Sgm RelPrimes(m) = len fp by Lm3,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,A2;
end;
theorem Th26:
for X be finite Subset of INT
st ( 1<m & 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_coprime))
holds X is_RRS_of m
proof let X be finite Subset of INT;
assume A1:(1<m & 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_coprime));
then card X <> 0 by PEPIN:42;
then reconsider X as non empty finite Subset of INT;
set Y = RelPrimes(m);
reconsider Y as finite set;
m gcd 1 = 1 by NEWTON:51;
then m,1 are_coprime 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;
A3:Y is_RRS_of m by Th22;
defpred P[Nat,set] means $2 in Class(Cong m,(Sgm Y).$1);
A4: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 A5:a in Seg Euler m;
consider fp being FinSequence such that
A6: 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 A6;
then reconsider fp as FinSequence of X by FINSEQ_2:12;
A7: card(rng fp) = card X by A1,A6,FINSEQ_4:62;
rng fp c= X by FINSEQ_1:def 4;then
A8: rng fp = X by A7,CARD_2:102;
defpred PP[Nat,set] means fp.$1 in Class(Cong m,$2);
A9: 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 A6,FINSEQ_1:def 3;
then A10:fp.c,m are_coprime by A1,A6;
set r = fp.c mod m;
A11: fp.c mod m = ((fp.c div m)*m + r) mod m by A1,INT_1:59
.= r mod m by NAT_D:61;
then fp.c,r are_congruent_mod m by A1,NAT_D:64;
then A12:r gcd m = fp.c gcd m by WSIERP_1:43
.= 1 by A10,INT_2:def 3;
then A13:r,m are_coprime by INT_2:def 3;
reconsider r as Element of NAT by INT_1:3;
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 A15:r in Y by A14,A13;
r,fp.c are_congruent_mod m by A11,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 A15;
end;
consider fr being FinSequence of Y such that
A16: 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(A9);
for x1,x2 be object
st x1 in dom fr & x2 in dom fr & fr.x1 = fr.x2 holds x1 = x2
proof let x1,x2 be object;
assume A17: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 A17,A16;
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 A18:fp.x1,fp.x2 are_congruent_mod m by A17,PEPIN:40;
A19: x1 in dom fp & x2 in dom fp by A17,A6,A16,FINSEQ_1:def 3;
then fp.x1 in X & fp.x2 in X by A8,FUNCT_1:def 3;
then fp.x1 = fp.x2 by A1,A18;
hence thesis by A19,A6,FUNCT_1:def 4;
end;
then fr is one-to-one by FUNCT_1:def 4;
then A20:card rng fr = len fr by FINSEQ_4:62
.= card Y by A16,FINSEQ_1:def 3;
rng fr c= Y by FINSEQ_1:def 4;
then A21:rng fr = Y by A20,CARD_2:102;
len Sgm Y = Euler m by FINSEQ_3:39;
then a in dom Sgm Y by A5,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 A21,FINSEQ_1:def 14;
then consider i be Nat such that
A22:i in dom fr & fr.i=(Sgm Y).a by FINSEQ_2:10;
i in dom fp by A22,A6,A16,FINSEQ_1:def 3;
then fp.i is Element of X by A8,FUNCT_1:def 3;
hence thesis by A22,A16;
end;
consider f being FinSequence of X such that
A23: 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(A4);
A24:len f = Euler m by A23,FINSEQ_1:def 3;
for a,b be object st a in dom f & b in dom f & f.a = f.b holds a = b
proof let a,b be object;
assume A25: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 A25,A23;
then [(Sgm Y).a,f.a] in Cong m & [(Sgm Y).b,f.b] in Cong m
by EQREL_1:18;
then A26:(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 A27:(Sgm Y).a,(Sgm Y).b are_congruent_mod m by A26,A25,INT_1:15;
now assume A28:a <> b;
len Sgm Y = Euler m by FINSEQ_3:39;then
A29: a in dom Sgm Y & b in dom Sgm Y by A25,A23,FINSEQ_1:def 3;
Sgm Y is one-to-one by FINSEQ_3:92;
then A30:(Sgm Y).a <> (Sgm Y).b by A28,A29,FUNCT_1:def 4;
(Sgm Y).a in rng(Sgm Y) & (Sgm Y).b in rng(Sgm Y)
by A29,FUNCT_1:def 3;
then (Sgm Y).a in Y & (Sgm Y).b in Y by FINSEQ_1:def 14;
hence contradiction by A27,A30,A3,Th24;
end;
hence thesis;
end;
then f is one-to-one by FUNCT_1:def 4;
then A31:card X = card(rng f) by A1,A24,FINSEQ_4:62;
A32:rng f c= X by FINSEQ_1:def 4;
take f;
thus thesis by A23,A24,A32,A31,CARD_2:102,FINSEQ_3:39;
end;
theorem
for X be finite Subset of INT,a be Integer st (m>1 &
a,m are_coprime & 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_coprime & 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_coprime) by Th24;
A3: a ** X c= INT
by INT_1:def 2;
a<>0 by A1,Th5;then
A4: card(a ** X) = Euler m by A2,INT_4:5;
A5: 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 A6:x in (a ** X) & y in (a ** X) & x <> y;
then consider z1 be Integer such that A7:z1 in X & x=a*z1 by Th3;
consider z2 be Integer such that A8:z2 in X & y=a*z2 by A6,Th3;
not z1,z2 are_congruent_mod m by A7,A6,A8,A1,Th24;
hence thesis by A7,A8,A1,INT_4:9;
end;
for x be Integer st x in (a ** X) holds x,m are_coprime
proof let x be Integer;
assume x in (a ** X);
then consider y such that A9:y in X & x = a * y by Th3;
y,m are_coprime by A9,A1,Th24;
hence thesis by A9, A1,INT_2:26;
end;
hence thesis by A1,A3,A4,A5,Th26;
end;
definition let i,n;
pred i is_primitive_root_of n means
order(i,n) = Euler n;
end;
theorem
n>1 & i,n are_coprime 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_coprime;
then A2:i <> 0 by Th5;
reconsider z = 0, j = 1 as Element of REAL by XREAL_0:def 1;
i - 1 >= 0 by A2,INT_1:52;then
A3:i - 1 + j >= z + j by XREAL_1:7;
A4: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 A5: order(i,n) = Euler n;
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 A6: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 A3,XXREAL_0:1;
suppose
A7: i = 1;
reconsider fn as FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;
fn = <*fn.1*> by FINSEQ_5:14,A6,A5,A1,PEPIN:46,A7;
hence thesis;
end;
suppose A8:i > 1;
for x1,x2 be object st x1 in dom fn & x2 in dom fn & fn.x1 = fn.x2
holds x1 = x2
proof let x1,x2 be object;
assume A9: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 A9,A6 .= i|^x2 by A9,A6;
hence thesis by A8,PEPIN:30;
end;
hence thesis by FUNCT_1:def 4;
end;
end;
then A10:card(rng fn) = Euler n by A6,FINSEQ_4:62;
A11: 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 A12:x in rng fn & y in rng fn & x <> y
& x,y are_congruent_mod n;
then consider s such that
A13: s in dom fn & fn.s = x by FINSEQ_2:10;
consider t such that
A14: t in dom fn & fn.t = y by A12,FINSEQ_2:10;
A15: x = i|^s & y = i|^t by A13,A14,A6;
A16: 1 <= s & s <= order(i,n) & 1 <= t & t <= order(i,n)
by A13,A14,A5,A6,FINSEQ_3:25;
per cases by A12,A13,A14,XXREAL_0:1;
suppose s > t;
then A17: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 A18:n divides (i|^t * (i|^k - 1)) by A15,A12,INT_2:15;
i|^t gcd n = 1 by A2,A4,A1,NAT_4:10;
then n divides (i|^k - 1) by A18,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
A19: order(i,n) <= k by A17,A1,PEPIN:47,NAT_D:7;
k <= order(i,n)-1 & order(i,n)-1<order(i,n) by A16,XREAL_1:13,146;
hence contradiction by A19,XXREAL_0:2;
end;
suppose s < t;
then A20:t - s > 0 by XREAL_1:50;
then reconsider k = t - s as Element of NAT by INT_1:3;
A21: 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 A15,A12,INT_1:14;
then A22:n divides (i|^s * (i|^k - 1)) by A21,INT_2:15;
i|^s gcd n = 1 by A2,A4,A1,NAT_4:10;
then n divides (i|^k - 1) by A22,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<order(i,n) by A16,XREAL_1:13,146;
hence contradiction by A23,XXREAL_0:2;
end;
end;
A24: for x be Integer st x in rng fn holds x,n are_coprime
proof let x be Integer;
assume x in rng fn;
then consider s such that
A25: s in dom fn & fn.s = x by FINSEQ_2:10;
A26: x = i|^s by A25,A6;
i|^s gcd n = 1 by A2,A4,A1,NAT_4:10;
hence thesis by A26,INT_2:def 3;
end;
rng fn c= INT by RELAT_1:def 19;
hence thesis by A1,A10,A11,A24,Th26;
end;
hence thesis;
end;
assume A27: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;
deffunc G(Nat) = i|^$1;
consider f be FinSequence such that
A28:len f = Euler n & for d being Nat st d in dom f holds f.d=G(d)
from FINSEQ_1:sch 2;
for s st s in dom f holds f.s in NAT
proof let s;
assume A29:s in dom f;
f.s = i|^s by A28,A29;
hence thesis by ORDINAL1:def 12;
end;
then reconsider f as FinSequence of NAT by FINSEQ_2:12;
A30:rng f is_RRS_of n by A28,A27;then
card rng f = Euler n & (for x,y be Integer st x in rng f
& y in rng f & x<>y holds not x,y are_congruent_mod n) by Th24;
then A31:f is one-to-one by A28,FINSEQ_4:62;
Euler n <> 0 by A1,PEPIN:42;
then
A33:Euler n > 0;
A34:Euler n >= 1 by A1,PEPIN:42,NAT_1:14;
A35:(i |^ Euler n) mod n = 1 by A1,Th5,EULER_2:18;
for s st s > 0 & (i|^s) mod n = 1 holds Euler n <= s
proof let s;
assume A36:s > 0 & (i|^s) mod n = 1;
now assume s < Euler n;
then A37:Euler n - s > 0 by XREAL_1:50;
then reconsider k = Euler n - s as Element of NAT by INT_1:3;
A38: k < Euler n & k >= 1 by A36,A37,XREAL_1:44,NAT_1:14;then
A39: k in dom f & Euler n in dom f by A28,A34,FINSEQ_3:25; then
A40: f.k in rng f & f.(Euler n) in rng f by FUNCT_1:3;
f.k <> f.(Euler n) by A39,A31,A38,FUNCT_1:def 4;
then not f.k,f.(Euler n) are_congruent_mod n by A40,A30,Th24;
then not i|^k,f.(Euler n) are_congruent_mod n by A39,A28;then
A41: not i|^k,i|^(Euler n) are_congruent_mod n by A39,A28;
i|^(Euler n),i|^s are_congruent_mod n by A36,A35,A1,NAT_D:64;
then A42:n divides (i|^(Euler n) - i|^s) by INT_2:15;
A43: 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 A2,A4,A1,NAT_4:10;then
A44: n divides (i|^k - 1) by A42,A43,WSIERP_1:29;
(i |^ Euler n) mod n = 1 mod n by A1,A35,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 A44,INT_5:1;
then n divides (i|^k - i|^Euler n);
hence contradiction by A41,INT_2:15;
end;
hence thesis;
end;
then order(i,n) = Euler n by A1,A33,A35,PEPIN:def 2;
hence thesis;
end;
theorem
p>2 & i,p are_coprime & 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_coprime & i is_primitive_root_of p;
A2:order(i,p) = Euler p by A1
.= 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;
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_coprime 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 A6:(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
A7: 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 A6,A7,PEPIN:40;then
A8: i|^((p-'1) div 2) mod p = 1 by A3,PEPIN:39;
p-1 >= 2 by A1,INT_1:52; then
A9:(p-'1) div 2 >= 2 div 2 by A4,NAT_2:24;
A10:(p-'1) divides ((p-'1) div 2) by A8,A3,A1,A2,A4,PEPIN:47;
((p-'1) div 2) divides (p-'1) by A7,NAT_D:def 3;
then 2*((p-'1) div 2) = 1*((p-'1) div 2) by A7,A10,NAT_D:5;
hence contradiction by A9,PEPIN:44;
end;
theorem
for k be Nat st k>=3 holds
for m st m,2|^k are_coprime 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_coprime
& m is_primitive_root_of 2|^k;
then consider m such that
A2: m,2|^k are_coprime & 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;
hence contradiction by A2,A3,PYTHTRIP:def 1;
end;
then A4:m|^(2|^(k-'2)) mod 2|^k = 1 by A1,Th7;
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;
A7:k>1 by XXREAL_0:2,A1;
k = (k-'1)+1 by A7,XREAL_1:235;then
A8: Euler(2|^k) = 2|^((k-'1)+1) - 2|^(k-'1) by A1,XXREAL_0:2,Th8,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,A8,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_coprime & 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_coprime &
i is_primitive_root_of p & i|^(p-'1) mod p^2 <> 1;
A2: p>1 by INT_2:def 4;
defpred P[Nat] means i|^(Euler(p|^($1-'1))) mod p|^$1 <> 1;
A3: P[2]
proof 2-'1 = 2-1 by XREAL_1:233
.= 1;
then A4:i|^(Euler(p|^(2-'1))) mod p|^2
= i|^(Euler p) mod p|^2;
Euler p = p - 1 by EULER_1:20
.= p-'1 by A2,XREAL_1:233;
hence thesis by A1,A4,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,A2,Th5;
A8: i,p|^(k-'1) are_coprime by A1,WSIERP_1:10;
A9: k>1 & k>0 by A6,XXREAL_0:2;
then k-1>0 by XREAL_1:50;then
A10:k-'1>0 by A6,XXREAL_0:2,XREAL_1:233;then
A11:p|^(k-'1) > 1 by A2,PEPIN:25;
i|^(Euler(p|^(k-'1))) mod p|^(k-'1) = 1 by A7,A8,A10,A2,PEPIN:25,
EULER_2:18;
then i|^(Euler(p|^(k-'1))),1 are_congruent_mod p|^(k-'1) by A11,PEPIN:39;
then p|^(k-'1) divides (i|^(Euler(p|^(k-'1))) - 1) by INT_2:15;
then consider s be Integer such that
A12:i|^(Euler(p|^(k-'1))) - 1 = p|^(k-'1) * s by INT_1:def 3;
A13:p|^k > 1 by A2,A6,PEPIN:25;
A14:p|^(k-'1) * s >= 0 by A12,XREAL_1:48,NAT_1:14,A7;
s >= 0 by A14;
then reconsider s as Element of NAT by INT_1:3;
reconsider M=s^3 as Element of NAT by ORDINAL1:def 12;
A16: now assume p divides s;
then p|^(k-'1) * p divides p|^(k-'1) * s by PYTHTRIP:7;
then A17: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,A17,A12;
hence contradiction by A6,A13,PEPIN:39;
end;
A18:k-'1>=1 by A10,NAT_1:14;
A19: Euler(p|^k) = p|^k - p|^(k-'1) by A6,XXREAL_0:2,Th8
.= 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,A10,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 A10,NAT_1:14,Th8;
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 Th4;
A21: p is odd by A1,PEPIN:17;
A22:p-'1 = p-1 by A2,XREAL_1:233;
then 2 divides (p-'1) by A21,PEPIN:22;
then (p-'1) mod 2 = 0 by PEPIN:6;
then A23:(p-'1) div 2 = (p-1)/2 by A22,PEPIN:63;
A24:(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 A23
.=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 A18,XREAL_1:6;
then A25:k+k-'1>=k+1 by A6,XXREAL_0:2,NAT_D:38;then
A26:p|^(k+1) divides (((p-'1) div 2)*s^2*p|^(2*k-'1)) by Lm2,NAT_D:9;
k+2*k>=2+2*k by A6,XREAL_1:6;
then A27: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 A25,A27,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 Lm2,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 A26,NAT_D:8;
i|^(Euler(p|^k)) = (1 + p|^(k-'1) * s)|^p by A12,A19,NEWTON:9;
then A29:p|^(k+1) divides ((i|^(Euler(p|^k))-1)-p|^k*s) by A24,A28;
now assume A30:i|^(Euler(p|^((k+1)-'1))) mod p|^(k+1) = 1;
p|^(k+1)>1 by A2,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
p|^k*p divides p|^k*s by NEWTON:6;
hence contradiction by A16,PYTHTRIP:7;
end;
hence thesis;
end;
for k be Nat st k>=2 holds P[k] from NAT_1:sch 8(A3,A5);
hence thesis by A1;
end;
theorem
n>1 & len fp>=2 & (for d st d in dom fp holds fp.d,n are_coprime)
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_coprime) 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_coprime;
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_coprime) 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_coprime & fp1.2,n are_coprime 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_coprime);
then A11:1 in dom fr & 2 in dom fr by A8,FINSEQ_3:29;
then fr.1,fr.2 are_coprime by A10;
then order(fp1.1,n),fr.2 are_coprime by A10,A11;then
A12: order(fp1.1,n),order(fp1.2,n) are_coprime 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 A12,A4,A7,A9,Th17;
end;
hence thesis;
end;
suppose len fp1 > 2;
then len fp + 1 > 2 by FINSEQ_2:16;
then A13:len fp +1 -1 >= 2 by INT_1:52;
A14: 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 A16: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_coprime);
then consider f be FinSequence of NAT,l be Element of NAT such that
A17: fr = f ^ <*l*> by FINSEQ_2:19;
A18: len f + 1 = len fp + 1 by A5,A16,A17,FINSEQ_2:16;
A19: for d st d in dom f holds f.d = order(fp.d,n)
proof let d; assume A20:d in dom f;
then A21:f.d = fr.d by A17,FINSEQ_1:def 7;
A22: d in dom fr by A20,A17,FINSEQ_2:15;
dom f = dom fp by A18,FINSEQ_3:29;
then fp.d = fp1.d by A20,FINSEQ_1:def 7;
hence thesis by A22,A16,A21;
end;
for d,e st d in dom f & e in dom f & d<>e
holds f.d,f.e are_coprime
proof let d,e; assume A23:d in dom f & e in dom f & d<>e;
then A24:f.d = fr.d & f.e = fr.e by A17,FINSEQ_1:def 7;
d in dom fr & e in dom fr by A23,A17,FINSEQ_2:15;
hence thesis by A23,A16,A24;
end;
then A25:order(Product fp,n)=Product f by A18,A19,A14,A3,A4,A13;
A26: for d be Nat st d in dom fp holds (fp.d) gcd n = 1
by A14,INT_2:def 3;
(Product fp) gcd n = 1 by A26,WSIERP_1:36;
then A27:(Product (fp)),n are_coprime 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_coprime by A4;
then A28:c,n are_coprime by FINSEQ_1:42;
len f+j >= z+j by XREAL_1:7;
then len fr >= j by A17,FINSEQ_2:16;
then A29:len fr in dom fr by FINSEQ_3:25;
then fr.(len fr)=order(fp1.(len fr),n) by A16
.=order(fp1.(len fp+1),n) by A16,FINSEQ_2:16
.=order(c,n) by FINSEQ_1:42;
then A30:fr.(len f+1) = order(c,n) by A17,FINSEQ_2:16;
A31: Product fp1 = Product fp * c & Product fr = Product f * l
by A17,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 A32:d in dom f;
then A33:d in dom fr by A17,FINSEQ_2:15;
d<=len f by A32,FINSEQ_3:25;then
A34: d<len f+1 by XREAL_1:145;
(len f+1) in dom fr by A17,A29,FINSEQ_2:16;
then fr.d,fr.(len f+1) are_coprime by A16,A33,A34;
then f.d,fr.(len f+1) are_coprime
by A17,A32,FINSEQ_1:def 7;
hence thesis by INT_2:def 3;
end;
then Product f gcd (fr.(len f +1)) = 1 by WSIERP_1:36;
then Product f,order(c,n) are_coprime by A30,INT_2:def 3;
then order(Product fp*c,n)=order(Product fp,n)*order(c,n)
by A4,A28,A27,A25,Th17;
hence order(Product fp1,n)=Product fr by A31,A30,A17,A25,FINSEQ_1:42;
end;
hence thesis;
end;
end;
hence thesis;
end;
for fp being FinSequence of NAT holds TH[fp] from FINSEQ_2:sch 2(A1,A2);
hence thesis;
end;