:: Properties of Primes and Multiplicative Group of a Field
:: by Kenichi Arai and Hiroyuki Okazaki
::
:: Received April 7, 2009
:: Copyright (c) 2009-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, NEWTON, NAT_1, ARYTM_3, RELAT_1, INT_2, XXREAL_0, INT_1,
ARYTM_1, ABIAN, CARD_1, EULER_1, INT_7, GRAPH_1, FINSET_1, GROUP_1,
SUBSET_1, GROUP_4, STRUCT_0, GROUP_2, INT_5, UNIROOTS, INT_3, XBOOLE_0,
ALGSTR_0, BINOP_2, REALSET1, FUNCT_7, BINOP_1, VECTSP_2, SUPINF_2,
MESFUNC1, POLYNOM1, HURWITZ, POLYNOM2, AFINSQ_1, POLYNOM5, POLYNOM3,
TARSKI, FUNCT_1, FINSEQ_1, GR_CY_3;
notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, CARD_1, DOMAIN_1, ORDINAL1,
NUMBERS, XCMPLX_0, INT_1, INT_2, NAT_D, XXREAL_0, RELAT_1, FUNCT_1,
FUNCT_2, FUNCT_7, BINOP_1, NAT_1, GROUP_2, STRUCT_0, ALGSTR_0, GROUP_1,
GROUP_4, VFUNCT_1, GR_CY_1, VECTSP_1, VECTSP_2, ALGSEQ_1, POLYNOM3,
POLYNOM4, POLYNOM5, NEWTON, EULER_1, INT_3, HURWITZ, REALSET1, INT_5,
INT_7, ABIAN, UNIROOTS;
constructors REAL_1, NAT_D, EUCLID, REALSET1, GROUP_4, GR_CY_1, INT_3,
BINARITH, POLYNOM4, POLYNOM5, WELLORD2, ALGSTR_1, HURWITZ, UPROOTS,
INT_5, EULER_1, INT_7, ABIAN, UNIROOTS, RELSET_1, VFUNCT_1, ALGSEQ_1,
BINOP_1;
registrations XBOOLE_0, STRUCT_0, XREAL_0, ORDINAL1, NAT_1, INT_1, GROUP_2,
FINSET_1, GR_CY_1, VECTSP_1, INT_3, XXREAL_0, RELAT_1, CARD_1, ALGSTR_1,
POLYNOM3, POLYNOM4, POLYNOM5, WSIERP_1, NEWTON, INT_7, VFUNCT_1, FUNCT_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions GROUP_1, TARSKI;
equalities STRUCT_0, GROUP_1, INT_3, POLYNOM3, HURWITZ, INT_7, ORDINAL1;
expansions STRUCT_0, TARSKI;
theorems TARSKI, XBOOLE_0, ZFMISC_1, ORDINAL1, FUNCT_2, VECTSP_1, INT_1,
RLVECT_1, GR_CY_1, NAT_1, INT_2, PEPIN, NAT_D, XCMPLX_1, WSIERP_1,
CARD_1, GROUP_1, GROUP_2, 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, SUBSET_1;
schemes NAT_1, FUNCT_2, RECDEF_1;
begin :: Properties of Primes
:: Safe Prime & Sophie_Germain Prime & Mersenne number
theorem Th1:
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_coprime;
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 4;
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 4;
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
:Def1:
ex sgp be Prime st 2*sgp+1 = p;
end;
registration
cluster Safe for Prime;
existence
proof
reconsider p = 5 as Prime by PEPIN:59;
reconsider sgp = 2 as Prime by INT_2:28;
take p;
p = 2*sgp+1;
hence thesis;
end;
end;
theorem Th2:
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 Def1;
q > 1 by INT_2:def 4;
then q >= 1+1 by NAT_1:13;
then 2*q >= 2*2 by XREAL_1:64;
then 2*q+1 >= 4+1 by XREAL_1:7;
hence thesis by A1;
end;
theorem Th3:
for p be Safe Prime holds p mod 2 = 1
proof
let p be Safe Prime;
p >= 4+1 by Th2;
then p > 4 by NAT_1:13;
then p > 4-2 by XREAL_1:51;
then p is odd by PEPIN:17;
hence thesis by NAT_2:22;
end;
theorem Th4:
for p be Safe Prime st p <> 7 holds p mod 3 = 2
proof
let p be Safe Prime;
set k = p mod 3;
consider q be Prime such that
A1: 2*q+1 = p by Def1;
assume
A2: p <> 7;
A3: now
assume
A4: k = 0 or k = 1;
now
per cases by A4;
suppose
k = 0;
then 3 divides p by INT_1:62;
then 3 = p by INT_2:def 4;
hence contradiction by Th2;
end;
suppose
A5: k = 1;
2,3 are_coprime by INT_2:28,30,PEPIN:41;
then
A6: 2 gcd 3 = 1 by INT_2:def 3;
3 divides (2*q+1-1) by A1,A5,PEPIN:8;
then 3 divides q by A6,WSIERP_1:29;
then 3 = q by INT_2:def 4;
hence contradiction by A2,A1;
end;
end;
hence contradiction;
end;
k < 2+1 by NAT_D:62;
then k <=0+2 by NAT_1:13;
then k = 0 or ... or k = 2;
hence thesis by A3;
end;
theorem Th5:
for p be Safe Prime st p <> 5 holds p mod 4 = 3
proof
let p be Safe Prime;
set k = p mod 4;
consider q be Prime such that
A1: 2*q+1 = p by Def1;
assume
A2: p <> 5;
A3: 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:62;
hence contradiction by INT_2:29,def 4;
end;
suppose
k = 1;
then (p div 4)*4+1 = 2*q+1 by A1,INT_1:59;
then q = (p div 4)*2;
then 2 divides q by INT_1:def 3;
then 2 = q by INT_2:def 4;
hence contradiction by A2,A1;
end;
suppose
k=2;
then p = (p div 4)*4+2 by INT_1:59
.=((p div 4)*2+1)*2;
then 2 divides p by INT_1:def 3;
then 2 = p by INT_2:def 4;
hence contradiction by Th2;
end;
end;
hence contradiction;
end;
k < 3+1 by NAT_D:62;
then k <= 0+3 by NAT_1:13;
then k = 0 or ... or k = 3;
hence thesis by A3;
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: 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 NAT_D:67
.= 2*((2*(p mod 3)) mod 3) by NAT_D:24
.= 2*((2*2) mod 3) by A1,Th4
.= 2*((1+3*1) mod 3)
.= 2*(1 mod 3) by NAT_D:61
.= 2*1 by PEPIN:5;
A3: 3*p mod 6 = 3*p mod 3*2 .= 3*(p mod 2) by INT_4:20
.= 3*1 by Th3;
p mod 6 = (p+6*p) mod 6 by NAT_D:61
.= (3*p+4*p) mod 6
.= (3*1+2*1) mod 6 by A3,A2,NAT_D:66
.= 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:51;
then
A2: p mod 4 = 3 by Th5;
A3: 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 NAT_D:67
.= 3*((3 * 3) mod 4) by A2,NAT_D:24
.= 3*((1+4*2) mod 4)
.= 3*(1 mod 4) by NAT_D:61
.= 3*1 by PEPIN:5;
A4: 4*p mod 12 = 4*p mod 4*3 .= 4*(p mod 3) by INT_4:20
.= 4*2 by A1,Th4;
p mod 12 = (p+12*p) mod 12 by NAT_D:61
.= (4*p+9*p) mod 12
.= (4*2+3*1) mod 12 by A4,A3,NAT_D:66
.= 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
8 = 2*4;
then
A1: 2 divides 8 by NAT_D:def 3;
let p be Safe Prime;
set k = p mod 8;
consider q be Prime such that
A2: 2*q+1 = p by Def1;
assume
A3: p > 5;
A4: now
assume
A5: (k = 0 or ... or k = 2) or (k = 4 or ... or k = 6);
now
per cases by A5;
suppose
k = 0;
then 8 divides p by INT_1:62;
then 2 divides p by A1,INT_2:9;
then 2 = p by INT_2:def 4;
hence contradiction by Th2;
end;
suppose
k=1;
then (p div 8)*8+1 = 2*q+1 by A2,INT_1:59;
then q = (p div 8)*4;
then 4 divides q by INT_1:def 3;
hence contradiction by INT_2:29,def 4;
end;
suppose
k=2;
then p = (p div 8)*8+2 by INT_1:59
.=((p div 8)*4+1)*2;
then 2 divides p by INT_1:def 3;
then 2 = p by INT_2:def 4;
hence contradiction by Th2;
end;
suppose
k = 4;
then p=(p div 8)*8+4 by INT_1:59
.=((p div 8)*4+2)*2;
then 2 divides p by INT_1:def 3;
then 2 = p by INT_2:def 4;
hence contradiction by Th2;
end;
suppose
k = 5;
then (p div 8)*8+5 = 2*q+1 by A2,INT_1:59;
then q = ((p div 8)*2+1)*2;
then 2 divides q by INT_1:def 3;
then 2 = q by INT_2:def 4;
hence contradiction by A3,A2;
end;
suppose
k = 6;
then p=(p div 8)*8+6 by INT_1:59
.= ((p div 8)*4+3)*2;
then 2 divides p by INT_1:def 3;
then 2 = p by INT_2:def 4;
hence contradiction by Th2;
end;
end;
hence contradiction;
end;
k < 7+1 by NAT_D:62;
then k <= 0+7 by NAT_1:13;
then k = 0 or ... or k = 7;
hence thesis by A4;
end;
definition
let p be Nat;
attr p is Sophie_Germain means
:Def2:
2*p+1 is Prime;
end;
registration
cluster Sophie_Germain for Prime;
existence
proof
reconsider p = 5 as Prime by PEPIN:59;
reconsider sgp = 2 as Prime by INT_2:28;
take sgp;
p = 2*sgp+1;
hence thesis;
end;
end;
theorem
for p be Prime st p > 2 holds p mod 4 = 1 or p mod 4 = 3
proof
let p be Prime;
set k = p mod 4;
assume
A1: p > 2;
A2: now
assume
A3: k = 0 or k = 2;
now
per cases by A3;
suppose
k = 0;
then 4 divides p by INT_1:62;
hence contradiction by INT_2:29,def 4;
end;
suppose
k = 2;
then p = (p div 4)*4+2 by INT_1:59
.= ((p div 4)*2+1)*2;
then 2 divides p by INT_1:def 3;
hence contradiction by A1,INT_2:def 4;
end;
end;
hence contradiction;
end;
k < 3+1 by NAT_D:62;
then k <= 0+3 by NAT_1:13;
then k = 0 or ... or k = 3;
hence thesis by A2;
end;
theorem Th10:
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 Def1;
q is Sophie_Germain Prime by A1,Def2;
hence thesis by A1;
end;
Lm1: 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:68;
then 2*p+1 > 4+1 by XREAL_1:8;
hence thesis;
end;
theorem Th11:
for p be Safe Prime ex q be Sophie_Germain Prime st Euler p = 2*q
proof
let p be Safe Prime;
A1: Euler p = p-1 by EULER_1:20;
ex q be Sophie_Germain Prime st p = 2*q+1 by Th10;
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 that
A1: p1 <> p2 and
A2: N = p1*p2;
consider q2 be Sophie_Germain Prime such that
A4: Euler p2 = 2*q2 by Th11;
consider q1 be Sophie_Germain Prime such that
A5: Euler p1 = 2*q1 by Th11;
Euler N = Euler p1 * Euler p2 by A1,A2,EULER_1:21,INT_2:30
.= 4*q1*q2 by A5,A4;
hence thesis;
end;
theorem Th13:
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 Th10;
p-1 =2*q by A1;
hence thesis by INT_7:23;
end;
theorem Th14:
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;
consider g be Element of G such that
A1: ord g = card G by GR_CY_1:19;
A2: m in NAT by ORDINAL1:def 12;
A3: n in NAT by ORDINAL1:def 12;
assume card G = n*m;
then ord (g|^m) = n by A1,A2,A3,INT_7:30;
then consider a be Element of G such that
A4: ord a = n;
take a;
thus thesis by A4;
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 Th13;
A2: Z/Z*(p) is cyclic Group by INT_7:31;
then consider a being Element of (Z/Z*(p)) such that
A3: ord a = 2 and
gr {a} is strict Subgroup of (Z/Z*(p)) by A1,Th14;
consider b being Element of (Z/Z*(p)) such that
A4: ord b = q and
gr {b} is strict Subgroup of (Z/Z*(p)) by A1,A2,Th14;
A5: card gr {b} = q by A4,GR_CY_1:7;
card (1).Z/Z*(p) = 1 by GROUP_2:69;
then consider H1 be strict Subgroup of Z/Z*(p) such that
A6: card H1 = 1;
Z/Z*(p) is strict Subgroup of Z/Z*(p) by GROUP_2:54;
then consider H2q be strict Subgroup of Z/Z*(p) such that
A7: card H2q = 2*q by A1;
card gr {a} = 2 by A3,GR_CY_1:7;
then consider H2,Hq be strict Subgroup of Z/Z*(p) such that
A8: card H2 = 2 and
A9: card Hq = q by A5;
take q,H1,H2,Hq,H2q;
now
let H be strict Subgroup of Z/Z*(p);
consider G1 be strict Subgroup of Z/Z*(p) such that
card G1 = card H and
A10: for G2 being strict Subgroup of Z/Z*(p) st card G2 = card H holds
G2 = G1 by A1,A2,GROUP_2:148,GR_CY_2:22;
A11: G1 = H by A10;
now
per cases by A1,Th1,GROUP_2:148,INT_2:28;
suppose
card H = 1;
hence H = H1 or H = H2 or H = Hq or H = H2q by A6,A10,A11;
end;
suppose
card H = 2;
hence H = H1 or H = H2 or H = Hq or H = H2q by A8,A10,A11;
end;
suppose
card H = q;
hence H = H1 or H = H2 or H = Hq or H = H2q by A9,A10,A11;
end;
suppose
card H = 2*q;
hence H = H1 or H = H2 or H = Hq or H = H2q by A7,A10,A11;
end;
end;
hence H = H1 or H = H2 or H = Hq or H = H2q;
end;
hence thesis by A7,A8,A9,A6;
end;
definition
let n be Nat;
func Mersenne(n) -> Nat equals
2|^n-1;
correctness by NAT_1:21,PREPOWER:11;
end;
Lm2: 2|^2 = 4
proof
2|^2 = 2|^(1+1) .= 2|^1*2 by NEWTON:6
.= 2*2;
hence thesis;
end;
Lm3: 2|^3 = 8
proof
2|^3 = 2|^(2+1) .= 4*2 by Lm2,NEWTON:6;
hence thesis;
end;
Lm4: 2|^4 = 16
proof
2|^4 = 2|^(2+2) .= 4*4 by Lm2,NEWTON:8;
hence thesis;
end;
Lm5: 2|^8 = 256
proof
2|^8 = 2|^(4+4) .= 16*16 by Lm4,NEWTON:8;
hence thesis;
end;
theorem
Mersenne(0) = 0
proof
thus Mersenne(0) = 1-1 by NEWTON:4
.= 0;
end;
theorem
Mersenne(1) = 1;
theorem
Mersenne(2) = 3 by Lm2;
theorem
Mersenne(3) = 7 by Lm3;
theorem
Mersenne(5) = 31
proof
thus Mersenne(5) = 2|^(3+2)-1 .= 2|^3*2|^2-1 by NEWTON:8
.= 31 by Lm2,Lm3;
end;
theorem
Mersenne(7) = 127
proof
thus Mersenne(7) = 2|^(4+3)-1 .= 2|^4*2|^3-1 by NEWTON:8
.= 127 by Lm3,Lm4;
end;
theorem
Mersenne(11) = 23*89
proof
thus Mersenne(11) = 2|^(8+3)-1 .= 2|^8*2|^3-1 by NEWTON:8
.= 23*89 by Lm3,Lm5;
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 4;
then 2*p > 2*1 by XREAL_1:68;
then
A2: 2*p > 2-1 by XREAL_1:51;
Mersenne(p) mod 2*p = 2*2|^(p-'1)-1 mod 2*p by PEPIN:26
.= ((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 A1,INT_2:28,30,PEPIN:37
.= (2*1-1) mod 2*p by A2,PEPIN:5;
hence thesis by A2,PEPIN:5;
end;
theorem
for p be Prime st p <> 2 holds Mersenne(p) mod 8 = 7
proof
let p be Prime;
A1: p > 1 by INT_2:def 4;
then
A2: p >= 1+1 by NAT_1:13;
assume p <> 2;
then p > 2 + 0 by A2,XXREAL_0:1;
then p-2 > 2-2 by XREAL_1:14;
then
A3: p-'2 > 0 by A2,XREAL_1:233;
A4: p-'1 > 0 by A1,NAT_D:49;
Mersenne(p) mod 8 = 2*2|^(p-'1)-1 mod 8 by PEPIN:26
.= ((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 A4,PEPIN:26
.= (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 A3,PEPIN:36
.= (-1+8*1) mod 8 by NAT_D:61
.= 7 by NAT_D:24;
hence thesis;
end;
theorem
for p be Sophie_Germain Prime st p > 2 & p mod 4 = 3
ex q be Safe Prime st q divides Mersenne(p)
proof
let p be Sophie_Germain Prime;
assume that
A1: p > 2 and
A2: p mod 4 = 3;
set q = 2*p+1;
A3: q is Safe Prime by Def1,Def2;
q > 5 by A1,Lm1;
then
A4: q > 5-3 by XREAL_1:51;
then 2,q are_coprime by A3,INT_2:28,30;
then
A5: 2 gcd q = 1 by INT_2:def 3;
p = (p div 4)*4+3 by A2,INT_1:59;
then q = (p div 4)*8+7;
then q mod 8 = 7 mod 8 by NAT_D:21
.= 7 by NAT_D:24;
then 2 is_quadratic_residue_mod q by A3,A4,INT_5:43;
then (2|^((2*p+1-'1) div 2)-1) mod q = 0 by A3,A4,A5,INT_5:20;
then (2|^((2*p) div 2)-1) mod q = 0 by NAT_D:34;
then (2|^p-1) mod q = 0;
then q divides 2|^p-1 by INT_1:62;
hence thesis by A3;
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 that
A1: p > 2 and
A2: p mod 4 = 1;
set q = 2*p+1;
A3: q is Safe Prime by Def1,Def2;
A4: q > 5 by A1,Lm1;
then
A5: q > 5-3 by XREAL_1:51;
then 2,q are_coprime by A3,INT_2:28,30;
then
A6: 2 gcd q = 1 by INT_2:def 3;
p = (p div 4)*4+1 by A2,INT_1:59;
then q = (p div 4)*8+3;
then q mod 8 = 3 mod 8 by NAT_D:21
.= 3 by NAT_D:24;
then not 2 is_quadratic_residue_mod q by A3,A5,INT_5:44;
then 2|^((2*p+1-'1) div 2) mod q = q-1 by A3,A5,A6,INT_5:19;
then
A7: 2|^((2*p) div 2) mod q = q-1 by NAT_D:34;
A8: q > 5-4 by A4,XREAL_1:51;
then q >= 1+1 by NAT_1:13;
then
A9: 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 A7
.= ((q-1)-1) mod q by A8,PEPIN:5
.= q-2 by A9,NAT_D:24,XREAL_1:44;
hence thesis by A3;
end;
theorem Th27:
for a,n be Nat holds a-1 divides a|^n-1
proof
let a,n be Nat;
A1: 2|^n-1 is Nat by NAT_1:21,PREPOWER:11;
per cases;
suppose a <= 1;
then a = 0 or a = 1 by NAT_1:25;
hence thesis by INT_2:12;
end;
suppose a > 1;
then
A2: a >= 1+1 by NAT_1:13;
per cases by A2,XXREAL_0:1;
suppose
A3: a = 2;
then a|^n-1 mod (a-1) = 0;
hence thesis by A3,INT_1:62;
end;
suppose
A4: a > 2;
then
A5: a-1 > 2-1 by XREAL_1:9;
A6: a-1 is Nat by A4,NAT_1:20;
a mod (a-1) = (a+(a-1)*(-1)) mod (a-1) by NAT_D:61
.= 1 by A5,PEPIN:5;
then
A7: (a|^n) mod (a-1) = 1 by A5,A6,PEPIN:35;
(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 A5,A7,PEPIN:5
.= 0 by A6,NAT_D:26;
hence thesis by A5,INT_1:62;
end;
end;
end;
Lm6: for a,p be Nat st p > 1 & a|^p-1 is Prime holds a > 1
proof
let a,p be Nat;
assume that
A1: p > 1 and
A2: a|^p-1 is Prime;
A3: now
assume
A4: a = 0 or a = 1;
now
per cases by A4;
suppose
a = 0;
then a|^p-1 = 0-1 by A1,NEWTON:84;
hence contradiction by A2;
end;
suppose
a = 1;
then a|^p-1 = 1-1;
hence contradiction by A2,INT_2:def 4;
end;
end;
hence contradiction;
end;
assume a <= 1;
hence contradiction by A3,NAT_1:25;
end;
theorem Th28:
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 that
A0: p <> 1 and
A2: a|^p-1 is Prime;
A1: now
assume p <= 1;
then p = 0 by A0,NAT_1:25;
then a|^p-1 = 1-1 by NEWTON:4;
hence contradiction by A2,INT_2:def 4;
end;
now
A3: a > 1 by A1,A2,Lm6;
then
A4: a >= 1+1 by NAT_1:13;
p >= 1+1 by A1,NAT_1:13;
then a < a|^p by A3,PREPOWER:13;
then
A5: a-1 < a|^p-1 by XREAL_1:9;
now
assume
A6: a > 2;
then
A7: a-1 > 2-1 by XREAL_1:9;
A8: a-1 is Element of NAT by A6,NAT_1:20;
a-1 divides a|^p-1 by Th27;
hence contradiction by A2,A5,A7,A8,NAT_4:12;
end;
hence a = 2 by A4,XXREAL_0:1;
assume not p is Prime;
then consider n be Element of NAT such that
A9: n divides p and
A10: 1 < n and
A11: n < p by A1,NAT_4:12;
consider q be Nat such that
A12: p = n*q by A9,NAT_D:def 3;
1+1 <= n by A10,NAT_1:13;
then 2 < 2|^n by PREPOWER:13;
then
A13: 2+1 <= 2|^n by NAT_1:13;
2|^n <= a|^n by A4,PREPOWER:9;
then 2+1 <= a|^n by A13,XXREAL_0:2;
then 2 < a|^n by NAT_1:13;
then
A14: 2-1 < a|^n-1 by XREAL_1:9;
a >= 0+1 by A1,A2,Lm6;
then
A15: a|^n-1 is Element of NAT by NAT_1:21,PREPOWER:11;
a|^n < a|^p by A3,A11,PEPIN:66;
then
A16: a|^n-1 < a|^p-1 by XREAL_1:9;
a|^n-1 divides (a|^n)|^q-1 by Th27;
then a|^n-1 divides a|^p-1 by A12,NEWTON:9;
hence contradiction by A2,A16,A15,A14,NAT_4:12;
end;
hence thesis;
end;
theorem
for p be Nat st p <> 1 & Mersenne(p) is Prime holds p is Prime by Th28;
:: Other theorems
theorem Th30:
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: for x be Nat st P[x] holds P[x+1]
proof
let x be Nat;
A2: a|^(x+1) mod n = (a|^x)*a mod n by NEWTON:6
.= (a|^x mod n)*(a mod n) mod n by NAT_D:67;
A3: (a mod n)|^(x+1) mod n = ((a mod n)|^x)*(a mod n) mod n by NEWTON:6
.= ((a mod n)|^x mod n)*((a mod n) mod n) mod n by NAT_D:67
.= ((a mod n)|^x mod n)*(a mod n) mod n by NAT_D:65;
assume a|^x mod n = (a mod n)|^x mod n;
hence thesis by A2,A3;
end;
a|^0 = 1 by NEWTON:4;
then
A4: P[0] by NEWTON:4;
for n be Nat holds P[n] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
theorem Th31:
for x,y,n be Integer st
x,n are_coprime & x,y are_congruent_mod n holds y,n are_coprime
proof
let x,y,n be Integer;
assume that
A1: x,n are_coprime and
A2: x,y are_congruent_mod n and
A3: not y,n are_coprime;
consider z be Integer such that
A4: n*z = x-y by A2,INT_1:def 5;
set gcdyn = y gcd n;
A5: gcdyn divides y by INT_2:21;
A6: gcdyn divides n by INT_2:21;
gcdyn divides n*z by INT_2:2,21;
then gcdyn divides n*z+y by A5,WSIERP_1:4;
then gcdyn divides (x gcd n) by A4,A6,INT_2:22;
then gcdyn divides 1 by A1,INT_2:def 3;
then
A7: gcdyn = 1 or gcdyn = -1 by INT_2:13;
0 <= gcdyn;
hence contradiction by A3,A7,INT_2:def 3;
end;
::$CT
theorem
for a,x be Integer, p be Prime st
a,p are_coprime & a,x*x are_congruent_mod p holds x,p are_coprime
proof
let a,x be Integer;
let p be Prime;
assume that
A1: a,p are_coprime and
A2: a,x*x are_congruent_mod p;
x*x,p are_coprime by A1,A2,Th31;
then
A3: x*x gcd p = 1 by INT_2:def 3;
assume
A4: not x,p are_coprime;
A5: (x gcd p) divides p by INT_2:21;
A6: x gcd p >= 0;
(x gcd p) divides (x*x) by INT_2:2,21;
then (x gcd p) = 1 or (x gcd p) = -1 by A3,A5,INT_2:13,22;
hence contradiction by A4,A6,INT_2:def 3;
end;
Lm7: 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;
A1: (a mod n) mod n = a mod n by NAT_D:65;
assume n <> 0;
hence thesis by A1,NAT_D:64;
end;
Lm8: 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:3;
take an;
thus thesis by A1,Lm7;
end;
Lm9: 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 that
A1: a,b are_congruent_mod n and
A2: n <> 0;
A3: (a|^x) mod n = ((a mod n)|^x) mod n by PEPIN:12;
(b|^x) mod n = ((b mod n)|^x) mod n by PEPIN:12;
then (b|^x) mod n = ((a mod n)|^x) mod n by A1,NAT_D:64;
hence thesis by A2,A3,NAT_D:64;
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 that
A1: a,b are_congruent_mod n and
A2: n <> 0;
consider an be Nat such that
A3: an,a are_congruent_mod n by A2,Lm8;
b mod n >= 0;
b mod n is Element of NAT by INT_1:3;
then consider nb be Nat such that
A4: nb = b mod n;
reconsider ai = an as Integer;
A5: ai,b are_congruent_mod n by A1,A3,INT_1:15;
reconsider bi = nb as Integer;
b mod n = (b mod n) mod n by NAT_D:65;
then b,bi are_congruent_mod n by A2,A4,NAT_D:64;
then an,nb are_congruent_mod n by A5,INT_1:15;
then an|^x,nb|^x are_congruent_mod n by A2,Lm9;
then
A6: (an|^x mod n) = (nb|^x mod n) by NAT_D:64;
A7: b|^x mod n = (b mod n)|^x mod n by Th30;
A8: a|^x mod n = (a mod n)|^x mod n by Th30;
an mod n = a mod n by A3,NAT_D:64;
then (a mod n)|^x mod n = (b mod n)|^x mod n by A4,A6,PEPIN:12;
hence thesis by A2,A8,A7,NAT_D:64;
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;
reconsider cLa = a mod n as Integer;
n > 1 by INT_2:def 4;
then
A1: 1 mod n = 1 by PEPIN:5;
assume
A2: a*a mod n = 1;
then cLa*cLa mod n = 1 by NAT_D:67;
then cLa*cLa,1 are_congruent_mod n by A1,NAT_D:64;
then n divides cLa*cLa-1 by INT_2:15;
then
A3: n divides (cLa+1)*(cLa-1);
0 = n*0;
then
A4: n divides 0 by INT_1:def 3;
A5: a mod n <> 0
proof
assume
A6: a mod n = 0;
a*a mod n = (a mod n)*(a mod n) mod n by NAT_D:67
.= 0 by A4,A6,INT_1:62;
hence contradiction by A2;
end;
cLa >= 0;
0+1 <= cLa by A5,INT_1:7;
then
A7: cLa-1 is Element of NAT by INT_1:5;
cLa mod n = a mod n by NAT_D:65;
then
A8: a,cLa are_congruent_mod n by NAT_D:64;
a mod n >= 0;
cLa+1 is Element of NAT by INT_1:3;
n divides (cLa-(-1)) or n divides (cLa-1) by A7,A3,NEWTON:80;
then cLa,(-1) are_congruent_mod n or cLa,1 are_congruent_mod n by INT_2:15;
hence thesis by A8,INT_1:15;
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 NAT_1:44;
then
A2: Segm(p) \ {0} = NonZero INT.Ring p by SUBSET_1:def 8
.= the carrier of MultGroup (INT.Ring(p)) by UNIROOTS:def 1;
A3: 1 < p by INT_2:def 4;
then
A4: the multF of Z/Z*(p) = (multint p) || (Segm(p) \ {0}) by INT_7:def 2
.= the multF of MultGroup (INT.Ring(p)) by A2,UNIROOTS:def 1;
0 = In (0,Segm(p)) by A1,SUBSET_1:def 8;
then the carrier of (Z/Z*(p)) = NonZero INT.Ring p by A3,INT_7:def 2
.= the carrier of MultGroup (INT.Ring(p)) by UNIROOTS:def 1;
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;
then x in NonZero F by UNIROOTS:def 1;
then reconsider x1 = x as Element of F;
y in the carrier of MultGroup F;
then y in NonZero F by UNIROOTS:def 1;
then reconsider y1 = y as Element of F;
x*y = x1*y1 by UNIROOTS:16
.= y*x by UNIROOTS:16;
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;
set hpd = 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;
then hp*hpd = 1.F by A1,VECTSP_1:def 10;
then hpd <> 0.F;
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;
A3: 1_F = 1_MultGroup F by UNIROOTS:17;
g * h = hpd*hp by A1,UNIROOTS:16
.= 1_(MultGroup (F)) by A1,A2,A3,VECTSP_1:def 10;
hence thesis by GROUP_1:def 5;
end;
Lm10: 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;
reconsider n0 = n as Element of NAT by ORDINAL1:def 12;
set f = (<%0.F, 1_(F)%>)`^n0-1_.(F);
A1: now
let x,xn be Element of F, xz be Element of G;
assume that
A2: x = xz and
A3: 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);
A4: xn = xxz|^n0 by A3,GROUP_4:1
.=(power F).(x,n0) by A2,UNIROOTS:29;
thus eval(f,x) = eval((<%0.F,1_(F)%>)`^n0,x)-eval(1_.(F),x) by POLYNOM4:21
.= eval((<%0.F,1_(F)%>)`^n0,x)-1_F by POLYNOM4:18
.= (power F).(eval(<%0.F,1_(F)%>,x),n0)-1_F by POLYNOM5:22
.= xn-1_F by A4,POLYNOM5:48;
end;
assume 0 < n;
then
A5: 0+1 < n+1 by XREAL_1:8;
len(1_.(F)) = 1 by POLYNOM4:4;
then
A6: len(-1_.(F)) = 1 by POLYNOM4:8;
len <%0.F,1_(F)%> = 2 by POLYNOM5:40;
then len((<%0.F,1_(F)%>)`^n0) = n*2-n+1 by POLYNOM5:23
.= n+1;
then len (f) = max(n+1,1) by A5,A6,POLYNOM4:7
.= n+1 by A5,XXREAL_0:def 10;
then deg f = n;
hence thesis by A1;
end;
Lm11: 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 that
A1: G is finite and
A2: 0 < n and
A3: ord a = n and
A4: b |^n = 1_G;
consider f be Polynomial of F such that
A5: deg f = n and
A6: 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 A2,Lm10;
assume
A7: not b is Element of gr {a};
A8: the carrier of G c= the carrier of MultGroup (F) by GROUP_2:def 5;
A9: for x be Element of G st x|^n = 1_G holds x in Roots(f)
proof
let x1 be Element of G;
A10: 1_F = 1_MultGroup F by UNIROOTS:17;
x1 in the carrier of MultGroup (F) by A8;
then x1 in NonZero F by UNIROOTS:def 1;
then reconsider x3 = x1 as Element of F;
assume
A11: x1|^n = 1_G;
then
A12: x1|^n = 1.F by A10,GROUP_2:44;
reconsider x2 = x1|^n as Element of F by A11,A10,GROUP_2:44;
eval(f,x3) = x2-1.F by A6
.=0.F by A12,RLVECT_1:15;
then x3 is_a_root_of f by POLYNOM5:def 7;
hence x1 in Roots(f) by POLYNOM5:def 10;
end;
A13: the carrier of gr {a} c= Roots(f)
proof
let x be object;
assume
A14: 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 A14;
x1 in gr {a} by A14;
then consider j be Integer such that
A15: x1 = a|^j by GR_CY_1:5;
x1|^n = a|^(j*n) by A15,GROUP_1:35
.= (a|^n)|^j by GROUP_1:35
.= (1_G)|^j by A3,GROUP_1:41
.= 1_G by GROUP_1:31;
hence x in Roots(f) by A9;
end;
b in Roots(f) by A4,A9;
then {b} c= Roots(f) by ZFMISC_1:31;
then
A16: (the carrier of gr {a}) \/ {b} c= Roots(f) by A13,XBOOLE_1:8;
reconsider gra = gr {a} as finite Group by A1;
A17: n = card gra by A1,A3,GR_CY_1:7
.= card (the carrier of gr {a});
then reconsider XX = the carrier of gr {a} as finite set;
consider m,n0 be Element of NAT such that
A18: n0 = deg f and
A19: m = card(Roots(f)) and
A20: m <= n0 by A5,INT_7:27;
card ((the carrier of gr {a}) \/ {b}) = card ( XX \/ {b} )
.= n0+1 by A7,A5,A18,A17,CARD_2:41;
then card Segm(n0+1) c= card Segm m by A19,A16,CARD_1:11;
then n0+1 <= m by NAT_1:40;
hence contradiction by A20,NAT_1:16,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);
set a = the Element of G;
defpred P[Nat,Element of G,Element of G] means ord $2 < ord $3;
assume not G is cyclic Group;
then
A1: not ex x be Element of G st ord x = card (G) by GR_CY_1:19;
A2: for x be Element of G holds ord x < card (G)
proof
let x be Element of G;
ord x <= card (G) by GR_CY_1:8,NAT_D:7;
hence thesis by A1,XXREAL_0:1;
end;
A3: for n being Nat for x being Element of G ex y being Element
of G st P[n,x,y]
proof
let n be Nat, x be Element of G;
set n = ord x;
n < card G by A2;
then
A4: card gr {x} <> card G by GR_CY_1:7;
the carrier of (gr {x}) c= the carrier of G by GROUP_2:def 5;
then the carrier of (gr {x}) c< the carrier of G by A4,XBOOLE_0:def 8;
then (the carrier of G) \ (the carrier of (gr {x})) <> {} by XBOOLE_1:105;
then consider z be object such that
A5: z in (the carrier of G) \ (the carrier of (gr {x})) by XBOOLE_0:def 1;
reconsider z as Element of G by A5;
set m = ord z;
set l = m lcm n;
n divides (m lcm n) by INT_2:def 1;
then consider j be Integer such that
A6: l = n*j by INT_1:def 3;
A7: 1 <= card gr {x} by GROUP_1:45;
then
A8: 1 <= n by GR_CY_1:7;
then l/n = j by A6,XCMPLX_1:89;
then
A9: j is Element of NAT by INT_1:3;
not m divides n
proof
assume m divides n;
then consider j be Integer such that
A10: n = m*j by INT_1:def 3;
A11: 0 < n by A7,GR_CY_1:7;
z|^n = (z|^m)|^j by A10,GROUP_1:35
.= (1_(G))|^j by GROUP_1:41
.= 1_(G) by GROUP_1:31;
then z is Element of gr {x} by A11,Lm11;
hence contradiction by A5,XBOOLE_0:def 5;
end;
then
A12: n <> l by INT_2:def 1;
A13: 1 <= card gr {z} by GROUP_1:45;
then
A14: m <> 0 by GR_CY_1:7;
1 <= m by A13,GR_CY_1:7;
then consider m0,n0 be Element of NAT such that
A15: l = n0*m0 and
A16: n0 gcd m0 = 1 and
A17: n0 divides n and
A18: m0 divides m and
A19: n0 <> 0 and
A20: m0 <> 0 by A8,INT_7:17;
ex u be Integer st m = m0* u by A18,INT_1:def 3;
then m/m0 is Integer by A20,XCMPLX_1:89;
then reconsider d2 = m/m0 as Element of NAT by INT_1:3;
ex j be Integer st n = n0*j by A17,INT_1:def 3;
then n/n0 is Integer by A19,XCMPLX_1:89;
then reconsider d1 = n/n0 as Element of NAT by INT_1:3;
set y = (x|^d1)*(z|^d2);
m = d2*m0 by A20,XCMPLX_1:87;
then
A21: ord (z|^d2) = m0 by INT_7:30;
n <> 0 by A7,GR_CY_1:7;
then j <> 0 by A14,A6,INT_2:4;
then n*1 <= n*j by A9,NAT_1:14,XREAL_1:64;
then
A22: n < l by A12,A6,XXREAL_0:1;
n = d1*n0 by A19,XCMPLX_1:87;
then ord (x|^d1) = n0 by INT_7:30;
then ord y = m0*n0 by A16,A21,INT_7:25;
hence ex y be Element of G st n < ord y by A15,A22;
end;
consider f being sequence of the carrier of G such that
A23: f.0 = a & for n being Nat holds P[n,f.n qua Element of G
,f.(n+1)
qua Element of G] from
RECDEF_1:sch 2(A3);
deffunc F(Nat) = ord (f.$1);
consider g be sequence of NAT such that
A24: for k be Element of NAT holds g.k=F(k) from FUNCT_2:sch 4;
A25: for k be Nat holds g.k=F(k)
proof let k be Nat;
k in NAT by ORDINAL1:def 12;
hence thesis by A24;
end;
A26: now
let k be Nat;
A27: g.(k+1) = ord (f.(k+1)) by A25;
g.k = ord (f.k) by A25;
hence g.k < g.(k+1) by A23,A27;
end;
A28: for k,m be Element of NAT holds g.k < g.(k+1+m)
proof
let k be Element of NAT;
defpred P[Nat] means g.k < g.(k+1+$1);
A29: now
let m be Nat;
assume
A30: P[m];
g.(k+1+m) < g.((k+1+m) + 1) by A26;
hence P[m+1] by A30,XXREAL_0:2;
end;
A31: P[0] by A26;
for m be Nat holds P[m] from NAT_1:sch 2(A31,A29);
hence thesis;
end;
A32: for k,m be Element of NAT st k < m holds g.k < g.m
proof
let k, m be Element of NAT;
assume
A33: k < m;
then m-k is Element of NAT by INT_1:5;
then reconsider mk = m-k as Nat;
m-k <> 0 by A33;
then consider n0 be Nat such that
A34: mk = n0+1 by NAT_1:6;
reconsider n = n0 as Element of NAT by ORDINAL1:def 12;
m = k+1+n by A34;
hence thesis by A28;
end;
now
let x1,x2 be object;
assume that
A35: x1 in NAT and
A36: x2 in NAT and
A37: g.x1 = g.x2;
reconsider xx1 = x1,xx2 = x2 as Element of NAT by A35,A36;
A38: xx2 <= xx1 by A32,A37;
xx1 <= xx2 by A32,A37;
hence x2 = x1 by A38,XXREAL_0:1;
end;
then g is one-to-one by FUNCT_2:19;
then dom g, rng g are_equipotent by WELLORD2:def 4;
then card dom g = card rng g by CARD_1:5;
then
A39: card rng g = card NAT by FUNCT_2:def 1;
rng g c= Segm card G
proof
let y be object;
assume y in rng g;
then consider x be object such that
A40: x in NAT and
A41: y=g.x by FUNCT_2:11;
reconsider x as Element of NAT by A40;
reconsider gg = g.x as Element of NAT;
g.x = ord (f.x) by A25;
then gg < card G by A2;
hence y in Segm(card G) by A41,NAT_1:44;
end;
hence contradiction by A39;
end;