:: Properties of Primes and Multiplicative Group of a Field
:: by Kenichi Arai and Hiroyuki Okazaki
::
:: Received April 7, 2009
:: Copyright (c) 2009 Association of Mizar Users
environ
vocabularies BOOLE, TARSKI, BINOP_1, INT_1, CARD_1, FUNCT_1, VECTSP_1,
RELAT_1, ARYTM_1, GR_CY_1, RLVECT_1, NAT_1, ARYTM_3, INT_2, NAT_LAT,
ALGSTR_0, INT_3, ARYTM, GROUP_1, GROUP_2, GROUP_4, INT_7, REALSET1,
FINSET_1, GRAPH_1, FINSEQ_1, POLYNOM1, POLYNOM2, ALGSEQ_1, POLYNOM3,
POLYNOM5, SQUARE_1, HURWITZ, GR_CY_3, EULER_1, INT_5, MATRIX_2, UNIROOTS,
FUNCT_7, VECTSP_2, STRUCT_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, FINSET_1, CARD_1,
DOMAIN_1, NUMBERS, XCMPLX_0, XREAL_0, INT_1, INT_2, NAT_1, NAT_D,
XXREAL_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_7, BINOP_1, GROUP_2,
STRUCT_0, ALGSTR_0, GROUP_1, GROUP_4, GR_CY_1, VECTSP_1, VECTSP_2,
BHSP_1, ALGSEQ_1, POLYNOM3, POLYNOM4, POLYNOM5, BINARITH, NEWTON,
EULER_1, INT_3, HURWITZ, REALSET1, PEPIN, INT_5, INT_7, ABIAN, UNIROOTS;
constructors REAL_1, NAT_D, NAT_3, PEPIN, EUCLID, REALSET1, GROUP_4, ARYTM_1,
ARYTM_0, GR_CY_1, INT_3, WSIERP_1, BINARITH, BHSP_1, POLYNOM2, POLYNOM4,
POLYNOM5, WELLORD2, ALGSTR_1, HURWITZ, UPROOTS, RECDEF_1, INT_5, GROUP_5,
EULER_1, INT_7, ABIAN, UNIROOTS, FUNCT_7, RELSET_1;
registrations XBOOLE_0, STRUCT_0, XREAL_0, ORDINAL1, NAT_1, INT_1, GROUP_1,
GROUP_2, FINSET_1, GR_CY_1, ALGSTR_0, VECTSP_1, INT_3, XXREAL_0,
SUBSET_1, RELAT_1, CARD_1, ALGSTR_1, POLYNOM3, POLYNOM4, POLYNOM5,
REALSET1, WSIERP_1, NEWTON, INT_5, ABIAN, UNIROOTS, FUNCT_7, INT_7;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions STRUCT_0, GROUP_1, INT_3, CARD_1, TARSKI, ALGSTR_0, REALSET1,
BINOP_1, POLYNOM3, HURWITZ, INT_7, SQUARE_1, UNIROOTS, FUNCT_7;
theorems TARSKI, XBOOLE_0, ZFMISC_1, ORDINAL1, FUNCT_2, VECTSP_1, INT_1,
RLVECT_1, GR_CY_1, FUNCT_7, NAT_1, INT_2, INT_3, PEPIN, NAT_D, XCMPLX_1,
WSIERP_1, CARD_1, GROUP_1, GROUP_2, STRUCT_0, WELLORD2, XREAL_1, NEWTON,
XXREAL_0, GROUP_4, POLYNOM4, POLYNOM5, CARD_2, EULER_1, XBOOLE_1, INT_7,
NAT_2, INT_4, INT_6, INT_5, NAT_4, RADIX_2, PREPOWER, UNIROOTS, GR_CY_2;
schemes NAT_1, FUNCT_2, RECDEF_1;
begin :: Properties of Primes
:: Safe Prime & Sophie_Germain Prime & Mersenne number
theorem LMPQ:
for p,q be Prime, k be Nat st k divides p*q
holds k = 1 or k = p or k = q or k = p*q
proof
let p,q be Prime, k be Nat;
assume
A1: k divides p*q;
per cases by PEPIN:2;
suppose k,p are_relative_prime;
then k divides q by A1,PEPIN:3;
hence k = 1 or k = p or k = q or k = p*q by INT_2:def 5;
end;
suppose k gcd p = p;
then p divides k by NAT_D:def 5;
then consider l be Nat such that
A2: k = p*l by NAT_D:def 3;
consider m be Nat such that
A3: k*m = p*q by A1,NAT_D:def 3;
p*(l*m) = p*q by A2,A3;
then l*m = q by XCMPLX_1:5;
then l divides q by NAT_D:def 3;
then l = 1 or l = q by INT_2:def 5;
hence k = 1 or k = p or k = q or k = p*q by A2;
end;
end;
definition let p be Nat;
attr p is Safe means :defASP:
ex sgp be Prime st 2*sgp+1 = p;
end;
registration
cluster Safe Prime;
existence
proof
reconsider sgp = 2 as Prime by INT_2:44;
reconsider p = 5 as Prime by PEPIN:64;
A1: p = 2*sgp+1;
take p;
thus thesis by A1,defASP;
end;
end;
theorem SP1:
for p be Safe Prime holds p >= 5
proof
let p be Safe Prime;
consider q be Prime such that
A1: 2*q+1 = p by defASP;
q > 1 by INT_2:def 5;
then q >= 1+1 by NAT_1:13;
then 2*q >= 2*2 by XREAL_1:66;
then 2*q+1 >= 4+1 by XREAL_1:9;
hence thesis by A1;
end;
theorem SPM1:
for p be Safe Prime holds p mod 2 = 1
proof
let p be Safe Prime;
p >= 4+1 by SP1;
then p > 4 by NAT_1:13;
then p > 4-2 by XREAL_1:53;
then p is odd by PEPIN:17;
hence thesis by NAT_2:24;
end;
theorem SPM2:
for p be Safe Prime st p <> 7 holds p mod 3 = 2
proof
let p be Safe Prime;
assume
A1: p <> 7;
consider q be Prime such that
A2: 2*q+1 = p by defASP;
set k = p mod 3;
0 <= k & k < 2+1 by INT_3:9; then
A3: 0 <= k & k <=0+2 by NAT_1:13;
now assume
A4: k = 0 or k = 1;
now per cases by A4;
suppose k = 0;
then 3 divides p by INT_1:89;
then 3 = p by INT_2:def 5;
hence contradiction by SP1;
end;
suppose k = 1; then
A5: 3 divides (2*q+1-1) by A2,PEPIN:8;
2,3 are_relative_prime by INT_2:44,47,PEPIN:44;
then 2 gcd 3 = 1 by INT_2:def 4;
then 3 divides q by A5,WSIERP_1:36;
then 3 = q by INT_2:def 5;
hence contradiction by A1,A2;
end;
end;
hence contradiction;
end;
hence thesis by A3,NAT_1:27;
end;
theorem SPM3:
for p be Safe Prime st p <> 5 holds p mod 4 = 3
proof
let p be Safe Prime;
assume
A1: p <> 5;
consider q be Prime such that
A2: 2*q+1 = p by defASP;
set k = p mod 4;
0 <= k & k < 3+1 by INT_3:9; then
A3: 0 <= k & k <= 0+3 by NAT_1:13;
now assume
A4: k = 0 or k = 1 or k = 2;
now per cases by A4;
suppose k = 0;
then 4 divides p by INT_1:89;
hence contradiction by INT_2:def 5,INT_2:46;
end;
suppose k = 1;
then (p div 4)*4+1 = 2*q+1 by A2,INT_1:86;
then q = (p div 4)*2;
then 2 divides q by INT_1:def 9;
then 2 = q by INT_2:def 5;
hence contradiction by A1,A2;
end;
suppose k=2;
then p = (p div 4)*4+2 by INT_1:86
.=((p div 4)*2+1)*2;
then 2 divides p by INT_1:def 9;
then 2 = p by INT_2:def 5;
hence contradiction by SP1;
end;
end;
hence contradiction;
end;
hence thesis by A3,NAT_1:28;
end;
theorem
for p be Safe Prime st p <> 7 holds p mod 6 = 5
proof
let p be Safe Prime;
assume
A1: p <> 7;
A2: 3*p mod 6 = 3*p mod 3*2
.= 3*(p mod 2) by INT_4:20
.= 3*1 by SPM1;
A3: 4*p mod 6 = 2*(2*p) mod 2*3
.= 2*((2*p) mod 3) by INT_4:20
.= 2*(((2 mod 3)*(p mod 3)) mod 3) by INT_3:15
.= 2*((2*(p mod 3)) mod 3) by NAT_D:24
.= 2*((2*2) mod 3) by SPM2,A1
.= 2*((1+3*1) mod 3)
.= 2*(1 mod 3) by INT_3:8
.= 2*1 by PEPIN:5;
p mod 6 = (p+6*p) mod 6 by INT_3:8
.= (3*p+4*p) mod 6
.= (3*1+2*1) mod 6 by A2,A3,INT_3:14
.= 5 by NAT_D:24;
hence thesis;
end;
theorem
for p be Safe Prime st p > 7 holds p mod 12 = 11
proof
let p be Safe Prime;
assume
A1: p > 7;
then p > 7-2 by XREAL_1:53; then
A2: p mod 4 = 3 by SPM3;
A3: 4*p mod 12 = 4*p mod 4*3
.= 4*(p mod 3) by INT_4:20
.= 4*2 by SPM2,A1;
A4: 9*p mod 12 = 3*(3*p) mod 3*4
.= 3*((3*p) mod 4) by INT_4:20
.= 3*(((3 mod 4)*(p mod 4)) mod 4) by INT_3:15
.= 3*((3 * 3) mod 4) by A2,NAT_D:24
.= 3*((1+4*2) mod 4)
.= 3*(1 mod 4) by INT_3:8
.= 3*1 by PEPIN:5;
p mod 12 = (p+12*p) mod 12 by INT_3:8
.= (4*p+9*p) mod 12
.= (4*2+3*1) mod 12 by A3,A4,INT_3:14
.= 11 by NAT_D:24;
hence thesis;
end;
theorem
for p be Safe Prime st p > 5 holds p mod 8 = 3 or p mod 8 = 7
proof
let p be Safe Prime;
assume
A1: p > 5;
consider q be Prime such that
A2: 2*q+1 = p by defASP;
8 = 2*4; then
A3: 2 divides 8 & 4 divides 8 by NAT_D:def 3;
set k = p mod 8;
0 <= k & k < 7+1 by INT_3:9; then
A4: 0 <= k & k <= 0+7 by NAT_1:13;
now assume A5: k = 0 or k = 1 or k = 2 or k = 4 or k = 5 or k = 6;
now per cases by A5;
suppose k = 0;
then 8 divides p by INT_1:89;
then 2 divides p by A3,INT_2:13;
then 2 = p by INT_2:def 5;
hence contradiction by SP1;
end;
suppose k=1;
then (p div 8)*8+1 = 2*q+1 by A2,INT_1:86;
then q = (p div 8)*4;
then 4 divides q by INT_1:def 9;
hence contradiction by INT_2:def 5,INT_2:46;
end;
suppose k=2;
then p = (p div 8)*8+2 by INT_1:86
.=((p div 8)*4+1)*2;
then 2 divides p by INT_1:def 9;
then 2 = p by INT_2:def 5;
hence contradiction by SP1;
end;
suppose k = 4;
then p=(p div 8)*8+4 by INT_1:86
.=((p div 8)*4+2)*2;
then 2 divides p by INT_1:def 9;
then 2 = p by INT_2:def 5;
hence contradiction by SP1;
end;
suppose k = 5;
then (p div 8)*8+5 = 2*q+1 by A2,INT_1:86;
then q = ((p div 8)*2+1)*2;
then 2 divides q by INT_1:def 9;
then 2 = q by INT_2:def 5;
hence contradiction by A1,A2;
end;
suppose k = 6;
then p=(p div 8)*8+6 by INT_1:86
.= ((p div 8)*4+3)*2;
then 2 divides p by INT_1:def 9;
then 2 = p by INT_2:def 5;
hence contradiction by SP1;
end;
end;
hence contradiction;
end;
hence thesis by A4,NAT_1:32;
end;
definition let p be Nat;
attr p is Sophie_Germain means :defSGP:
2*p+1 is Prime;
end;
registration
cluster Sophie_Germain Prime;
existence
proof
reconsider sgp = 2 as Prime by INT_2:44;
reconsider p = 5 as Prime by PEPIN:64;
A1: p = 2*sgp+1;
take sgp;
thus thesis by A1,defSGP;
end;
end;
theorem
for p be Sophie_Germain Prime st p > 2 holds p mod 4 = 1 or p mod 4 = 3
proof
let p be Sophie_Germain Prime;
assume
A1: p > 2;
set k = p mod 4;
0 <= k & k < 3+1 by INT_3:9; then
A2: 0 <= k & k <= 0+3 by NAT_1:13;
now assume
A3: k = 0 or k = 2;
now per cases by A3;
suppose k = 0;
then 4 divides p by INT_1:89;
hence contradiction by INT_2:def 5,INT_2:46;
end;
suppose k = 2;
then p = (p div 4)*4+2 by INT_1:86
.= ((p div 4)*2+1)*2;
then 2 divides p by INT_1:def 9;
hence contradiction by INT_2:def 5,A1;
end;
end;
hence contradiction;
end;
hence thesis by A2,NAT_1:28;
end;
theorem SGSP0:
for p be Safe Prime ex q be Sophie_Germain Prime st p = 2*q+1
proof
let p be Safe Prime;
consider q be Prime such that
A1: 2*q+1 = p by defASP;
q is Sophie_Germain Prime by A1,defSGP;
hence thesis by A1;
end;
SGSP2:
for p be Nat st p > 2 holds 2*p+1 > 5
proof
let p be Nat;
assume p > 2;
then 2*p > 2*2 by XREAL_1:70;
then 2*p+1 > 4+1 by XREAL_1:10;
hence thesis;
end;
theorem SGSP3:
for p be Safe Prime ex q be Sophie_Germain Prime st Euler p = 2*q
proof
let p be Safe Prime;
consider q be Sophie_Germain Prime such that
A1: p = 2*q+1 by SGSP0;
Euler p = p-1 by EULER_1:21;
hence thesis by A1;
end;
theorem
for p1,p2 be Safe Prime, N be Nat st p1 <> p2 & N = p1*p2
holds ex q1,q2 be Sophie_Germain Prime st Euler (N) = 4*q1*q2
proof
let p1,p2 be Safe Prime, N be Nat;
assume
A1: p1 <> p2 & N = p1*p2;
consider q1 be Sophie_Germain Prime such that
A2: Euler p1 = 2*q1 by SGSP3;
consider q2 be Sophie_Germain Prime such that
A3: Euler p2 = 2*q2 by SGSP3;
p1 > 1 & p2 > 1 by INT_2:def 5;
then Euler (N) = Euler p1 * Euler p2 by A1,INT_2:47,EULER_1:22
.= 4*q1*q2 by A2,A3;
hence thesis;
end;
theorem SF1:
for p be Safe Prime ex q be Sophie_Germain Prime st card (Z/Z*(p)) = 2*q
proof
let p be Safe Prime;
consider q be Sophie_Germain Prime such that
A1: 2*q+1 = p by SGSP0;
p-1 =2*q by A1;
hence thesis by INT_7:23;
end;
theorem SF2:
for G being cyclic finite Group, n,m being Nat st card G = n*m
ex a being Element of G st ord a = n & gr {a} is strict Subgroup of G
proof
let G be cyclic finite Group;
let n,m be Nat;
assume
A1: card G = n*m;
consider g be Element of G such that
A2: ord g = card G by GR_CY_1:43;
m in NAT & n in NAT by ORDINAL1:def 13; then
A4: ord (g|^m) = n by INT_7:30,A1,A2;
consider a be Element of G such that
A5: ord a = n by A4;
take a;
thus thesis by A5;
end;
theorem
for p be Safe Prime ex q be Sophie_Germain Prime,
H1,H2,Hq,H2q be strict Subgroup of (Z/Z*(p))
st card H1 = 1 & card H2 = 2 & card Hq = q & card H2q = 2*q
& for H be strict Subgroup of (Z/Z*(p))
holds H = H1 or H = H2 or H = Hq or H = H2q
proof
let p be Safe Prime;
consider q be Sophie_Germain Prime such that
A1: card (Z/Z*(p)) = 2*q by SF1;
A2: Z/Z*(p) is cyclic Group by INT_7:31;
Z/Z*(p) is strict Subgroup of Z/Z*(p) by GROUP_2:63;
then consider H2q be strict Subgroup of Z/Z*(p) such that
A3: card H2q = 2*q by A1;
consider a being Element of (Z/Z*(p)) such that
A5: ord a = 2 & gr {a} is strict Subgroup of (Z/Z*(p)) by A1,A2,SF2;
consider b being Element of (Z/Z*(p)) such that
a5: ord b = q & gr {b} is strict Subgroup of (Z/Z*(p)) by A1,A2,SF2;
card gr {a} = 2 & card gr {b} = q by a5,A5,GR_CY_1:27;
then consider H2,Hq be strict Subgroup of Z/Z*(p) such that
A6: card H2 = 2 & card Hq = q;
card (1).Z/Z*(p) = 1 by GROUP_2:81;
then consider H1 be strict Subgroup of Z/Z*(p) such that
A7: card H1 = 1;
A8: now let H be strict Subgroup of Z/Z*(p);
consider G1 be strict Subgroup of Z/Z*(p) such that
A9: card G1 = card H & for G2 being strict Subgroup of Z/Z*(p) st
card G2 = card H holds G2 = G1 by A2,GROUP_2:178,A1,GR_CY_2:28;
A10: G1 = H by A9;
now per cases by INT_2:44,A1,GROUP_2:178,LMPQ;
suppose card H = 1;
hence H = H1 or H = H2 or H = Hq or H = H2q by A7,A9,A10;
end;
suppose card H = 2;
hence H = H1 or H = H2 or H = Hq or H = H2q by A6,A9,A10;
end;
suppose card H = q;
hence H = H1 or H = H2 or H = Hq or H = H2q by A6,A9,A10;
end;
suppose card H = 2*q;
hence H = H1 or H = H2 or H = Hq or H = H2q by A3,A9,A10;
end;
end;
hence H = H1 or H = H2 or H = Hq or H = H2q;
end;
take q,H1,H2,Hq,H2q;
thus thesis by A3,A6,A7,A8;
end;
definition
let n be Nat;
func Mersenne(n) -> Nat equals
2|^n-1;
correctness by PREPOWER:19,NAT_1:21;
end;
MSLm1: 2|^2 = 4
proof
2|^2 = 2|^(1+1)
.= 2|^1*2 by NEWTON:11
.= 2*2 by NEWTON:10;
hence thesis;
end;
MSLm2: 2|^3 = 8
proof
2|^3 = 2|^(2+1)
.= 4*2 by MSLm1,NEWTON:11;
hence thesis;
end;
MSLm3: 2|^4 = 16
proof
2|^4 = 2|^(2+2)
.= 4*4 by MSLm1,NEWTON:13;
hence thesis;
end;
MSLm4: 2|^8 = 256
proof
2|^8 = 2|^(4+4)
.= 16*16 by MSLm3,NEWTON:13;
hence thesis;
end;
theorem
Mersenne(0) = 0
proof
thus Mersenne(0) = 1-1 by NEWTON:9
.= 0;
end;
theorem
Mersenne(1) = 1
proof
thus Mersenne(1) = 2-1 by NEWTON:10
.= 1;
end;
theorem
Mersenne(2) = 3 by MSLm1;
theorem
Mersenne(3) = 7 by MSLm2;
theorem
Mersenne(5) = 31
proof
thus Mersenne(5) = 2|^(3+2)-1
.= 2|^3*2|^2-1 by NEWTON:13
.= 31 by MSLm1,MSLm2;
end;
theorem
Mersenne(7) = 127
proof
thus Mersenne(7) = 2|^(4+3)-1
.= 2|^4*2|^3-1 by NEWTON:13
.= 127 by MSLm2,MSLm3;
end;
theorem
Mersenne(11) = 23*89
proof
thus Mersenne(11) = 2|^(8+3)-1
.= 2|^8*2|^3-1 by NEWTON:13
.= 23*89 by MSLm2,MSLm4;
end;
theorem
for p be Prime st p <> 2 holds Mersenne(p) mod 2*p = 1
proof
let p be Prime;
assume
A1: p <> 2;
p > 1 by INT_2:def 5;
then 2*p > 2*1 by XREAL_1:70; then
A2: 2*p > 2-1 by XREAL_1:53;
Mersenne(p) mod 2*p = 2*2|^(p-'1)-1 mod 2*p by PEPIN:27
.= ((2*2|^(p-'1) mod 2*p)-(1 mod 2*p)) mod 2*p by INT_6:7
.= (2*(2|^(p-'1) mod p)-(1 mod 2*p)) mod 2*p by INT_4:20
.= (2*1-(1 mod 2*p)) mod 2*p by PEPIN:38,INT_2:44,INT_2:47,A1
.= (2*1-1) mod 2*p by PEPIN:5,A2;
hence thesis by PEPIN:5,A2;
end;
theorem
for p be Prime st p <> 2 holds Mersenne(p) mod 8 = 7
proof
let p be Prime;
assume
A1: p <> 2;
A2: p > 1 by INT_2:def 5; then
A3: p >= 1+1 by NAT_1:13; then
A4: p > 2 + 0 by XXREAL_0:1,A1;
A5: p-'1 > 0 by A2,NAT_D:49;
p-2 > 2-2 by XREAL_1:16,A4; then
A6: p-'2 > 0 by A3,XREAL_1:235;
Mersenne(p) mod 8 = 2*2|^(p-'1)-1 mod 8 by PEPIN:27
.= ((2*2|^(p-'1) mod 2*4)-(1 mod 8)) mod 8 by INT_6:7
.= (2*(2|^(p-'1) mod 4)-(1 mod 8)) mod 8 by INT_4:20
.= (2*(2*2|^(p-'1-'1) mod 2*2)-(1 mod 8)) mod 8 by PEPIN:27,A5
.= (2*(2*2|^(p-'2) mod 2*2)-(1 mod 8)) mod 8 by NAT_D:45
.= (2*(2*( 2|^(p-'2) mod 2))-(1 mod 8)) mod 8 by INT_4:20
.= (4*(2|^(p-'2) mod 2)-1) mod 8 by PEPIN:5
.= (4*0-1) mod 8 by A6, PEPIN:37
.= (-1+8*1) mod 8 by INT_3:8
.= 7 by NAT_D:24;
hence thesis;
end;
theorem
for p be Sophie_Germain Prime st p > 2 & p mod 4 = 3
holds ex q be Safe Prime st q divides Mersenne(p)
proof
let p be Sophie_Germain Prime;
assume
A1: p > 2 & p mod 4 = 3;
set q = 2*p+1;
A2: q > 5 by A1,SGSP2;
B2: q is Safe Prime by defSGP,defASP;
A3: q mod 8 = 7
proof
p = (p div 4)*4+3 by A1,INT_1:86;
then q = (p div 4)*8+7;
then q mod 8 = 7 mod 8 by NAT_D:21
.= 7 by NAT_D:24;
hence thesis;
end;
A4: q > 5-3 by A2,XREAL_1:53; then
A5: 2 is_quadratic_residue_mod q by A3,INT_5:43,B2;
2,q are_relative_prime by INT_2:44,INT_2:47,A4,B2;
then 2 gcd q = 1 by INT_2:def 4;
then (2|^((2*p+1-'1) div 2)-1) mod q = 0 by A4,A5,INT_5:20,B2;
then (2|^((2*p) div 2)-1) mod q = 0 by NAT_D:34;
then (2|^p-1) mod q = 0 by NAT_D:18;
then q divides 2|^p-1 by INT_1:89;
hence thesis by B2;
end;
theorem
for p be Sophie_Germain Prime st p > 2 & p mod 4 = 1
holds ex q be Safe Prime st Mersenne(p) mod q = q-2
proof
let p be Sophie_Germain Prime;
assume
A1: p > 2 & p mod 4 = 1;
set q = 2*p+1;
B2: q is Safe Prime by defSGP,defASP;
A2: q > 5 by A1,SGSP2;
A3: q mod 8 = 3
proof
p = (p div 4)*4+1 by A1,INT_1:86;
then q = (p div 4)*8+3;
then q mod 8 = 3 mod 8 by NAT_D:21
.= 3 by NAT_D:24;
hence thesis;
end;
A4: q > 5-3 by A2,XREAL_1:53; then
A5: not 2 is_quadratic_residue_mod q by A3,INT_5:44,B2;
2,q are_relative_prime by INT_2:44,INT_2:47,A4,B2;
then 2 gcd q = 1 by INT_2:def 4;
then 2|^((2*p+1-'1) div 2) mod q = q-1 by A4,A5,INT_5:19,B2; then
A6: 2|^((2*p) div 2) mod q = q-1 by NAT_D:34;
A7: q > 5-4 by A2,XREAL_1:53; then
q >= 1+1 by NAT_1:13; then
A8: q-2 is Nat by NAT_1:21;
Mersenne(p) mod q = ((2|^p mod q)-(1 mod q)) mod q by INT_6:7
.= ((q-1)-(1 mod q)) mod q by A6,NAT_D:18
.= ((q-1)-1) mod q by PEPIN:5,A7
.= q-2 by NAT_D:24,XREAL_1:46,A8;
hence thesis by B2;
end;
theorem LmST1:
for a,n be Nat st a > 1 holds a-1 divides a|^n-1
proof
let a,n be Nat;
assume
A1: a > 1;
A2: 2|^n-1 is Nat by PREPOWER:19,NAT_1:21;
A3: a >= 1+1 by NAT_1:13,A1;
per cases by A3,XXREAL_0:1;
suppose
A4: a = 2;
then a|^n-1 mod (a-1) = 0 by RADIX_2:1,A2;
hence thesis by INT_1:89,A4;
end;
suppose
A5: a > 2; then
A6: a-1 > 2-1 by XREAL_1:11;
A7: a-1 is Nat by NAT_1:20,A5;
a mod (a-1) = (a+(a-1)*(-1)) mod (a-1) by INT_3:8
.= 1 by PEPIN:5,A6; then
A8: (a|^n) mod (a-1) = 1 by PEPIN:36,A6,A7;
(a|^n-1) mod (a-1) = ((a|^n mod (a-1))-(1 mod (a-1))) mod (a-1)
by INT_6:7
.= (1-1) mod (a-1) by PEPIN:5,A6,A8
.= 0 by NAT_D:26,A7;
hence thesis by INT_1:89,A6,A7;
end;
end;
LmST2:
for a,p be Nat st p > 1 & a|^p-1 is Prime holds a > 1
proof
let a,p be Nat;
assume
A1: p > 1 & a|^p-1 is Prime;
assume
A2: a <= 1;
now assume
A3: a = 0 or a = 1;
now per cases by A3;
suppose a = 0;
then a|^p-1 = 0-1 by A1,NEWTON:103;
hence contradiction by A1;
end;
suppose a = 1;
then a|^p-1 = 1-1 by NEWTON:15;
hence contradiction by INT_2:def 5,A1;
end;
end;
hence contradiction;
end;
hence contradiction by A2,NAT_1:26;
end;
theorem LmST3:
for a,p be Nat st p > 1 & a|^p-1 is Prime holds a = 2 & p is Prime
proof
let a,p be Nat;
assume
A1: p > 1 & a|^p-1 is Prime;
now
A2: a > 1 by A1,LmST2; then
A3: a >= 1+1 by NAT_1:13;
p >= 1+1 by NAT_1:13,A1;
then a < a|^p by A2,PREPOWER:21; then
A4: a-1 < a|^p-1 by XREAL_1:11;
now assume
A5: a > 2; then
A6: a-1 > 2-1 by XREAL_1:11;
A7: a-1 is Element of NAT by NAT_1:20,A5;
a-1 divides a|^p-1 by A1,LmST2,LmST1;
hence contradiction by A1,A4,A6,A7,NAT_4:12;
end;
hence a = 2 by XXREAL_0:1,A3;
assume
A8: not p is Prime;
consider n be Element of NAT such that
A9: n divides p & 1 < n & n < p by NAT_4:12,A1,A8;
consider q be Nat such that
A10: p = n*q by A9,NAT_D:def 3;
a|^n-1 divides (a|^n)|^q-1 by LmST1,PEPIN:26,A2,A9; then
A11: a|^n-1 divides a|^p-1 by NEWTON:14,A10;
a|^n < a|^p by A2,A9,PEPIN:71; then
A12: a|^n-1 < a|^p-1 by XREAL_1:11;
a >= 0+1 by A1,LmST2; then
A13: a|^n-1 is Element of NAT by PREPOWER:19,NAT_1:21;
1+1 <= n by NAT_1:13,A9;
then 2 < 2|^n by PREPOWER:21; then
A14: 2+1 <= 2|^n by NAT_1:13;
2|^n <= a|^n by A3,PREPOWER:17;
then 2+1 <= a|^n by A14,XXREAL_0:2;
then 2 < a|^n by NAT_1:13;
then 2-1 < a|^n-1 by XREAL_1:11;
hence contradiction by NAT_4:12,A1,A11,A12,A13;
end;
hence thesis;
end;
theorem
for p be Nat st p > 1 & Mersenne(p) is Prime holds p is Prime by LmST3;
:: Other theorems
theorem INTPOW:
for a be Integer,x,n be Nat holds a|^x mod n = (a mod n)|^x mod n
proof
let a be Integer;
let x, n be Nat;
defpred P[Nat] means a|^$1 mod n = (a mod n)|^$1 mod n;
A1: P[0]
proof
a|^0 = 1 & (a mod n)|^0 = 1 by NEWTON:9;
hence thesis;
end;
A2: for x be Nat st P[x] holds P[x+1]
proof
let x be Nat;
assume
A3: a|^x mod n = (a mod n)|^x mod n;
A4: a|^(x+1) mod n = (a|^x)*a mod n by NEWTON:11
.= (a|^x mod n)*(a mod n) mod n by INT_3:15;
(a mod n)|^(x+1) mod n = ((a mod n)|^x)*(a mod n) mod n by NEWTON:11
.= ((a mod n)|^x mod n)*((a mod n) mod n) mod n by INT_3:15
.= ((a mod n)|^x mod n)*(a mod n) mod n by INT_3:13;
hence thesis by A3,A4;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem THP:
for x,y,n be Integer st x,n are_relative_prime & x,y are_congruent_mod n
holds y,n are_relative_prime
proof
let x,y,n be Integer;
assume that
A1: x,n are_relative_prime and
A2: x,y are_congruent_mod n and
A3: not y,n are_relative_prime;
consider z be Integer such that
A4: n*z = x-y by A2,INT_1:def 3;
set gcdyn = y gcd n;
A6: gcdyn divides y by INT_2:31;
A7: gcdyn divides n by INT_2:32;
A8: gcdyn divides n*z by INT_2:32,INT_2:12;
A9: gcdyn divides n*z+y by A8,A6,WSIERP_1:9;
A10: gcdyn divides (x gcd n) by A4,A9,A7,INT_2:33;
A11: gcdyn divides 1 by A10,A1,INT_2:def 4;
A12: gcdyn = 1 or gcdyn = -1 by A11,INT_2:17;
0 <= gcdyn;
hence contradiction by A3,INT_2:def 4,A12;
end;
theorem
for a,x be Nat, p be Prime st a,p are_relative_prime
& a,x*x are_congruent_mod p holds x,p are_relative_prime
proof
let a,x be Nat;
let p be Prime;
assume
A1: a,p are_relative_prime & a,x*x are_congruent_mod p;
assume
A2: not x,p are_relative_prime;
reconsider ai = a, dpi = p, xx = x*x as Integer;
x*x,p are_relative_prime by A1,THP; then
A4: x*x gcd p = 1 by INT_2:def 4;
x gcd p = p by A2,PEPIN:2;
then p divides x by NAT_D:def 5;
then p divides x*x & p divides p by NAT_D:9;
then p divides 1 by A4, NAT_D:def 5;
then p = 1 by INT_2:17;
hence contradiction by INT_2:def 5;
end;
theorem
for a,x be Integer, p be Prime st a,p are_relative_prime
& a,x*x are_congruent_mod p holds x,p are_relative_prime
proof
let a,x be Integer;
let p be Prime;
assume
A1: a,p are_relative_prime & a,x*x are_congruent_mod p;
assume
A2: not x,p are_relative_prime;
x*x,p are_relative_prime by A1,THP; then
A4: x*x gcd p = 1 by INT_2:def 4;
A5: x gcd p <> 1 & x gcd p >= 0 by A2,INT_2:def 4;
(x gcd p) divides (x*x) & (x gcd p) divides p by INT_2:31,INT_2:12;
then (x gcd p) = 1 or (x gcd p) = -1 by INT_2:33,INT_2:17,A4;
hence contradiction by A5;
end;
Lmmod1:
for n be Nat, a be Integer st n <> 0 holds (a mod n),a are_congruent_mod n
proof
let n be Nat;
let a be Integer;
assume
A1: n <> 0;
(a mod n) mod n = a mod n by INT_3:13;
hence thesis by A1,INT_3:12;
end;
Lmmod2:
for n be Nat, a be Integer st n <> 0 ex an be Nat st an,a are_congruent_mod n
proof
let n be Nat;
let a be Integer;
assume
A1: n <> 0;
reconsider an = a mod n as Element of NAT by INT_1:16,INT_1:84;
take an;
thus thesis by A1,Lmmod1;
end;
Lmsm1:
for a,b,n,x be Nat st a,b are_congruent_mod n & n <> 0
holds a|^x,b|^x are_congruent_mod n
proof
let a,b,n,x be Nat;
assume
A1: a,b are_congruent_mod n & n <> 0;
(a|^x) mod n = ((a mod n)|^x) mod n
& (b|^x) mod n = ((b mod n)|^x) mod n by PEPIN:12;
then (a|^x) mod n = ((a mod n)|^x) mod n
& (b|^x) mod n = ((a mod n)|^x) mod n by A1,INT_3:12;
hence thesis by INT_3:12,A1;
end;
theorem
for a,b be Integer,n,x be Nat st a,b are_congruent_mod n & n <> 0
holds a|^x,b|^x are_congruent_mod n
proof
let a,b be Integer;
let n,x be Nat;
assume
A1: a,b are_congruent_mod n & n <> 0;
consider an be Nat such that
A2: an,a are_congruent_mod n by A1,Lmmod2;
reconsider ai = an as Integer;
A4: an mod n = a mod n by A2,INT_3:12;
A5: a|^x mod n = (a mod n)|^x mod n
& b|^x mod n = (b mod n)|^x mod n by INTPOW;
b mod n is Integer & b mod n >= 0 by A1,INT_3:9; then
A6: b mod n is Element of NAT by INT_1:16;
A7: b mod n = (b mod n) mod n by INT_3:13;
consider nb be Nat such that
A8: nb = b mod n by A6;
reconsider bi = nb as Integer;
A10: b,bi are_congruent_mod n by A1,A7,A8,INT_3:12;
ai,b are_congruent_mod n by A1,A2,INT_1:36;
then an,nb are_congruent_mod n by A10,INT_1:36;
then an|^x,nb|^x are_congruent_mod n by A1,Lmsm1; then
A11: (an|^x mod n) = (nb|^x mod n) by INT_3:12;
(a mod n)|^x mod n = (b mod n)|^x mod n by A4,A8,A11,PEPIN:12;
hence thesis by A1,INT_3:12,A5;
end;
theorem
for a be Integer, n be Prime st a*a mod n = 1
holds a,1 are_congruent_mod n or a,(-1) are_congruent_mod n
proof
let a be Integer;
let n be Prime;
A0: n > 1 by INT_2:def 5;
assume
A1: a*a mod n = 1;
0 = n*0; then
A2: n divides 0 by INT_1:def 9;
A3: 1 mod n = 1 by A0,PEPIN:5;
A4: a mod n <> 0
proof
assume
A5: a mod n = 0;
a*a mod n = (a mod n)*(a mod n) mod n by INT_3:15
.= 0 by A2,INT_1:89,A5;
hence contradiction by A1;
end;
reconsider cLa = a mod n as Integer;
cLa mod n = a mod n by INT_3:13; then
A7: a,cLa are_congruent_mod n by INT_3:12;
A8: cLa*cLa mod n = 1 by A1,INT_3:15;
A9: a mod n >= 0 & a mod n < n by INT_3:9;
cLa <> 0 & cLa >= 0 & cLa < n by A4,INT_3:9;
then 0+1 <= cLa & cLa < n by INT_1:20;
then cLa-1 is Element of NAT by INT_1:18;
then consider ax be Nat such that
A10: ax = cLa-1;
cLa+1 is Element of NAT by A9,INT_1:16;
then consider ay be Nat such that
A11: ay = cLa+1;
cLa*cLa,1 are_congruent_mod n by A3,A8,INT_3:12; then
A12: n divides cLa*cLa-1 by INT_2:19;
n divides (cLa+1)*(cLa-1) by A12;
then n divides (cLa-(-1)) or n divides (cLa-1) by A10,A11,NEWTON:98;
then cLa,(-1) are_congruent_mod n
or cLa,1 are_congruent_mod n by INT_2:19;
hence thesis by INT_1:36,A7;
end;
begin :: Multiplicative Group of a Field
theorem
for p be Prime holds Z/Z*(p) = MultGroup (INT.Ring(p))
proof
let p be Prime;
A1: 0 in Segm(p) by GR_CY_1:10;
A2: 1 < p by INT_2:def 5;
A3: 0 = In (0,Segm(p)) by A1,FUNCT_7:def 1;
A4: the carrier of (Z/Z*(p))
= NonZero INT.Ring p by A2,A3,INT_7:def 2
.= the carrier of MultGroup (INT.Ring(p)) by UNIROOTS:def 1;
A5: Segm(p) \ {0} = NonZero INT.Ring p
by A1,FUNCT_7:def 1
.= the carrier of MultGroup (INT.Ring(p)) by UNIROOTS:def 1;
the multF of Z/Z*(p) = (multint p) || (Segm(p) \ {0}) by INT_7:def 2,A2
.= the multF of MultGroup (INT.Ring(p)) by UNIROOTS:def 1,A5;
hence Z/Z*(p) = MultGroup (INT.Ring(p)) by A4;
end;
registration let F be commutative Skew-Field;
cluster MultGroup (F) -> commutative;
coherence
proof
let x,y be Element of MultGroup F;
x in the carrier of MultGroup F
& y in the carrier of MultGroup F; then
A1: x in NonZero F &
y in NonZero F by UNIROOTS: def 1;
then reconsider x1 = x as Element of F;
reconsider y1 = y as Element of F by A1;
x*y = x1*y1 by UNIROOTS:19
.= y*x by UNIROOTS:19;
hence thesis;
end;
end;
theorem
for F be commutative Skew-Field, x be Element of MultGroup (F),
x1 be Element of F st x = x1 holds x" = x1"
proof
let F be commutative Skew-Field,
h be Element of MultGroup (F),
hp be Element of F;
assume
A1: h = hp;
h in the carrier of MultGroup (F);
then h in NonZero F by UNIROOTS:def 1;
then not h in {0.F} by XBOOLE_0:def 5; then
A2: h <> 0.F by TARSKI:def 1;
set hpd = hp";
hp*hpd = 1.F by A1,A2,VECTSP_1:def 22; then
hpd <> 0.F by VECTSP_1:36;
then not hpd in {0.F} by TARSKI:def 1;
then hpd in NonZero F by XBOOLE_0:def 5;
then reconsider g = hpd as Element of MultGroup (F) by UNIROOTS:def 1;
A4: 1_F = 1_MultGroup F by UNIROOTS:20;
g * h = hpd*hp by A1,UNIROOTS:19
.= 1_(MultGroup (F)) by A1,A2,VECTSP_1:def 22,A4;
hence thesis by GROUP_1:def 6;
end;
LM0X62a:
for F be commutative Skew-Field, G be Subgroup of MultGroup (F),
n be Nat st 0 < n ex f be Polynomial of F st deg f = n &
for x,xn be Element of F, xz be Element of G st x = xz & xn = xz|^n
holds eval(f,x) = xn-1.F
proof
let F be commutative Skew-Field,
G be Subgroup of MultGroup (F), n be Nat;
assume 0 < n; then
A1: 0+1 < n+1 by XREAL_1:10;
reconsider n0 = n as Element of NAT by ORDINAL1:def 13;
set f = (<%0.F, 1_(F)%>)`^n0-1_.(F);
A2: now let x,xn be Element of F, xz be Element of G;
assume
A3: x = xz & xn = xz|^n;
the carrier of G c= the carrier of MultGroup (F) by GROUP_2:def 5;
then reconsider xxz = xz as Element of MultGroup (F) by TARSKI:def 3;
A4: xn = xxz|^n0 by GROUP_4:3,A3
.=(power F).(x,n0) by UNIROOTS:32,A3;
thus eval(f,x) = eval((<%0.F,1_(F)%>)`^n0,x)-eval(1_.(F),x)
by POLYNOM4:24
.= eval((<%0.F,1_(F)%>)`^n0,x)-1_F by POLYNOM4:21
.= (power F).(eval(<%0.F,1_(F)%>,x),n0)-1_F by POLYNOM5:23
.= xn-1_F by A4,POLYNOM5:49;
end;
A5: len <%0.F,1_(F)%> = 2 by POLYNOM5:41;
A6: len((<%0.F,1_(F)%>)`^n0) = n*2-n+1 by A5,POLYNOM5:24
.= n+1;
len(1_.(F)) = 1 by POLYNOM4:7; then
A7: len(-1_.(F)) = 1 by POLYNOM4:11;
len (f) = max(n+1,1) by A6,A7,POLYNOM4:10,A1
.= n+1 by XXREAL_0:def 10,A1;
then deg f = n;
hence thesis by A2;
end;
LM0X62:
for F be commutative Skew-Field, G be Subgroup of MultGroup (F),
a,b be Element of G, n be Nat st G is finite & 0 < n & ord a = n
& b |^n = 1_G holds b is Element of gr {a}
proof
let F be commutative Skew-Field, G be Subgroup of MultGroup (F),
a, b be Element of G, n be Nat;
assume
A1: G is finite & 0 < n & ord a = n & b |^n = 1_G;
assume
A2: not b is Element of gr {a};
A3: the carrier of G c= the carrier of MultGroup (F) by GROUP_2:def 5;
reconsider L = F as unital (non empty doubleLoopStr);
consider f be Polynomial of F such that
A4: deg f = n & for x,xn be Element of F, xz be Element of G st x = xz
& xn = xz|^n holds eval(f,x) = xn-1.F by A1,LM0X62a;
A5: for x be Element of G st x|^n = 1_G holds x in Roots(f)
proof
let x1 be Element of G;
assume
A6: x1|^n = 1_G;
x1 in the carrier of G;
then x1 in the carrier of MultGroup (F) by A3;
then x1 in NonZero F by UNIROOTS: def 1;
then reconsider x3 = x1 as Element of F;
A7: 1_F = 1_MultGroup F by UNIROOTS:20; then
A8: x1|^n = 1.F by GROUP_2:53,A6;
reconsider x2 = x1|^n as Element of F by GROUP_2:53,A6,A7;
eval(f,x3) = x2-1.F by A4
.=0.F by RLVECT_1:28,A8;
then x3 is_a_root_of f by POLYNOM5:def 6;
hence x1 in Roots(f) by POLYNOM5:def 9;
end;
A9: the carrier of gr {a} c= Roots(f)
proof
let x be set;
assume
A10: x in the carrier of gr {a};
the carrier of gr {a} c= the carrier of G by GROUP_2:def 5;
then reconsider x1=x as Element of G by A10;
x1 in gr {a} by A10,STRUCT_0:def 5;
then consider j be Integer such that
A11: x1 = a|^j by GR_CY_1:25;
x1|^n = a|^(j*n) by GROUP_1:67,A11
.= (a|^n)|^j by GROUP_1:67
.= (1_G)|^j by A1,GROUP_1:82
.= 1_G by GROUP_1:61;
hence x in Roots(f) by A5;
end;
reconsider RF = Roots(f) as finite set by INT_7:27,A4;
consider m,n0 be Element of NAT such that
A12: n0 = deg f & m = card(Roots(f)) & m <= n0 by INT_7:27,A4;
reconsider gra = gr {a} as finite Group by A1;
A13: n = card gra by GR_CY_1:27,A1
.= card (the carrier of gr {a});
b in Roots(f) by A1,A5;
then {b} c= Roots(f) by ZFMISC_1:37; then
A14: (the carrier of gr {a}) \/ {b} c= Roots(f) by A9,XBOOLE_1:8;
reconsider XX = the carrier of gr {a} as finite set by A13;
A15: card ((the carrier of gr {a}) \/ {b}) = card ( XX \/ {b} )
.= n0+1 by A4,A12,A13,CARD_2:54,A2;
card (n0+1) c= card(m) by CARD_1:27,A14,A15,A12;
then n0+1 <= m by NAT_1:41;
hence contradiction by NAT_1:16,A12,XXREAL_0:2;
end;
theorem
for F be commutative Skew-Field, G be finite Subgroup of MultGroup(F)
holds G is cyclic Group
proof
let F be commutative Skew-Field,
G be finite Subgroup of MultGroup(F);
assume not G is cyclic Group; then
A1: not ex x be Element of G st ord x = card (G) by GR_CY_1:43;
A2: for x be Element of G holds ord x < card (G)
proof
let x be Element of G;
ord x <= card (G) by NAT_D:7,GR_CY_1:28;
hence thesis by XXREAL_0:1,A1;
end;
consider a be Element of G;
defpred P[Nat,Element of G,Element of G] means ord $2 < ord $3;
A3: for n being Element of NAT for x being Element of G ex y being Element of G
st P[n,x,y]
proof
let n be Element of NAT, x be Element of G;
set n = ord x;
A4: n < card G by A2;
A5: the carrier of (gr {x}) c= the carrier of G by GROUP_2:def 5;
A6: card gr {x} <> card G by A4,GR_CY_1:27;
the carrier of (gr {x}) c< the carrier of G by XBOOLE_0:def 8,A5,A6;
then (the carrier of G) \ (the carrier of (gr {x})) <> {}
by XBOOLE_1:105;
then consider z be set such that
A7: z in (the carrier of G) \ (the carrier of (gr {x})) by XBOOLE_0:def 1;
reconsider z as Element of G by A7;
set m = ord z;
reconsider d = m gcd n as Nat;
reconsider H = gr {z } as strict Subgroup of G;
A16: 1 <= card gr {x} by GROUP_1:90; then
A17: 1 <= n by GR_CY_1:27;
A18: n <> 0 by A16,GR_CY_1:27;
A19: 1 <= card gr {z} by GROUP_1:90; then
A20: 1 <= m by GR_CY_1:27;
A21: m <> 0 by A19,GR_CY_1:27;
set l = m lcm n;
consider m0,n0 be Element of NAT such that
A22: l = n0*m0 & n0 gcd m0 = 1 & n0 divides n & m0 divides m
& n0 <> 0 & m0 <> 0 by INT_7:17,A17,A20;
consider j be Integer such that
A23: n = n0*j by A22,INT_1:def 9;
A24: n/n0 is Integer by A22,XCMPLX_1:90,A23;
reconsider d1 = n/n0 as Element of NAT by INT_1:16,A24;
consider u be Integer such that
A25: m = m0* u by A22,INT_1:def 9;
A26: m/m0 is Integer by A22,XCMPLX_1:90,A25;
reconsider d2 = m/m0 as Element of NAT by INT_1:16,A26;
set y = (x|^d1)*(z|^d2);
n = d1*n0 by A22,XCMPLX_1:88; then
A27: ord (x|^d1) = n0 by INT_7:30;
m = d2*m0 by A22,XCMPLX_1:88;
then ord (z|^d2) = m0 by INT_7:30; then
A28: ord y = m0*n0 by A27,INT_7:25,A22;
A29: not m divides n
proof
assume m divides n;
then consider j be Integer such that
A31: n = m*j by INT_1:def 9;
A32: z|^n = (z|^m)|^j by GROUP_1:67,A31
.= (1_(G))|^j by GROUP_1:82
.= 1_(G) by GROUP_1:61;
0 < n by A16,GR_CY_1:27;
then z is Element of gr {x} by A32,LM0X62;
hence contradiction by A7,XBOOLE_0:def 5;
end;
A33: n <> l by INT_2:def 2,A29;
A34: n divides (m lcm n) by INT_2:def 2;
consider j be Integer such that
A35: l = n*j by A34,INT_1:def 9;
A36: l/n = j by A17,A35,XCMPLX_1:90;
A37: j is Element of NAT by INT_1:16,A36;
j <> 0 by A18,A21,INT_2:4,A35;
then n*1 <= n*j by XREAL_1:66,A37,NAT_1:14;
then n < l by XXREAL_0:1,A35,A33;
hence ex y be Element of G st n < ord y by A28,A22;
end;
consider f being Function of NAT, the carrier of G such that
A38: f.0 = a & for n being Element of NAT holds P[n,f.n,f.(n+1)]
from RECDEF_1:sch 2(A3);
deffunc F(Element of NAT) = ord (f.$1);
consider g be Function of NAT, NAT such that
A39: for k be Element of NAT holds g.k=F(k) from FUNCT_2:sch 4;
A40: now let k be Element of NAT;
A41: g.k = ord (f.k) by A39;
g.(k+1) = ord (f.(k+1)) by A39;
hence g.k < g.(k+1) by A38,A41;
end;
A42: for k,m be Element of NAT holds g.k < g.(k+1+m)
proof
let k be Element of NAT;
defpred P[Element of NAT] means g.k < g.(k+1+$1);
A43: P[0] by A40;
A44: now let m be Element of NAT;
assume
A45: P[m];
g.(k+1+m) < g.((k+1+m) + 1) by A40;
hence P[m+1] by A45, XXREAL_0:2;
end;
for m be Element of NAT holds P[m] from NAT_1:sch 1(A43,A44);
hence thesis;
end;
A46: for k,m be Element of NAT st k < m holds g.k < g.m
proof
let k, m be Element of NAT;
assume
A47: k < m;
then m-k is Element of NAT by INT_1:18;
then reconsider mk = m-k as Nat;
m-k <> 0 by A47;
then consider n0 be Nat such that
A48: mk = n0+1 by NAT_1:6;
reconsider n = n0 as Element of NAT by ORDINAL1:def 13;
m = k+1+n by A48;
hence thesis by A42;
end;
g is one-to-one
proof
now let x1,x2 be set;
assume
A49: x1 in NAT & x2 in NAT & g.x1 = g.x2;
then reconsider xx1 = x1,xx2 = x2 as Element of NAT;
xx1 <= xx2 & xx2 <= xx1 by A46,A49;
hence x2 = x1 by XXREAL_0:1;
end;
hence thesis by FUNCT_2:25;
end;
then dom g, rng g are_equipotent by WELLORD2:def 4; then
A50: card dom g = card rng g by CARD_1:21;
A51: rng g c= Segm card G
proof
let y be set;
assume y in rng g;
then consider x be set such that
A52: x in NAT & y=g.x by FUNCT_2:17;
reconsider x as Element of NAT by A52;
reconsider gg = g.x as Element of NAT;
g.x = ord (f.x) by A39;
then gg < card G by A2;
hence y in Segm(card G) by A52,NAT_1:45;
end;
card rng g = card NAT by FUNCT_2:def 1,A50;
hence contradiction by A51;
end;