:: Properties of Primes and Multiplicative Group of a Field
:: by Kenichi Arai and Hiroyuki Okazaki
::
:: Received April 7, 2009
:: Copyright (c) 2009-2017 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;
begin :: Properties of Primes
:: Safe Prime & Sophie_Germain Prime & Mersenne number
theorem :: GR_CY_3:1
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;
definition
let p be Nat;
attr p is Safe means
:: GR_CY_3:def 1
ex sgp be Prime st 2*sgp+1 = p;
end;
registration
cluster Safe for Prime;
end;
theorem :: GR_CY_3:2
for p be Safe Prime holds p >= 5;
theorem :: GR_CY_3:3
for p be Safe Prime holds p mod 2 = 1;
theorem :: GR_CY_3:4
for p be Safe Prime st p <> 7 holds p mod 3 = 2;
theorem :: GR_CY_3:5
for p be Safe Prime st p <> 5 holds p mod 4 = 3;
theorem :: GR_CY_3:6
for p be Safe Prime st p <> 7 holds p mod 6 = 5;
theorem :: GR_CY_3:7
for p be Safe Prime st p > 7 holds p mod 12 = 11;
theorem :: GR_CY_3:8
for p be Safe Prime st p > 5 holds p mod 8 = 3 or p mod 8 = 7;
definition
let p be Nat;
attr p is Sophie_Germain means
:: GR_CY_3:def 2
2*p+1 is Prime;
end;
registration
cluster Sophie_Germain for Prime;
end;
theorem :: GR_CY_3:9
for p be Sophie_Germain Prime st p > 2 holds p mod 4 = 1 or p mod 4 = 3;
theorem :: GR_CY_3:10
for p be Safe Prime ex q be Sophie_Germain Prime st p = 2*q+1;
theorem :: GR_CY_3:11
for p be Safe Prime ex q be Sophie_Germain Prime st Euler p = 2* q;
theorem :: GR_CY_3:12
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;
theorem :: GR_CY_3:13
for p be Safe Prime ex q be Sophie_Germain Prime st card (Z/Z*(p )) = 2*q;
theorem :: GR_CY_3:14
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;
theorem :: GR_CY_3:15
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;
definition
let n be Nat;
func Mersenne(n) -> Nat equals
:: GR_CY_3:def 3
2|^n-1;
end;
theorem :: GR_CY_3:16
Mersenne(0) = 0;
theorem :: GR_CY_3:17
Mersenne(1) = 1;
theorem :: GR_CY_3:18
Mersenne(2) = 3;
theorem :: GR_CY_3:19
Mersenne(3) = 7;
theorem :: GR_CY_3:20
Mersenne(5) = 31;
theorem :: GR_CY_3:21
Mersenne(7) = 127;
theorem :: GR_CY_3:22
Mersenne(11) = 23*89;
theorem :: GR_CY_3:23
for p be Prime st p <> 2 holds Mersenne(p) mod 2*p = 1;
theorem :: GR_CY_3:24
for p be Prime st p <> 2 holds Mersenne(p) mod 8 = 7;
theorem :: GR_CY_3:25
for p be Sophie_Germain Prime st p > 2 & p mod 4 = 3
ex q be Safe Prime st q divides Mersenne(p);
theorem :: GR_CY_3:26
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;
theorem :: GR_CY_3:27
for a,n be Nat st a > 1 holds a-1 divides a|^n-1;
theorem :: GR_CY_3:28
for a,p be Nat st p > 1 & a|^p-1 is Prime holds a = 2 & p is Prime;
theorem :: GR_CY_3:29
for p be Nat st p > 1 & Mersenne(p) is Prime holds p is Prime;
:: Other theorems
theorem :: GR_CY_3:30
for a be Integer,x,n be Nat holds a|^x mod n = (a mod n)|^x mod n;
theorem :: GR_CY_3:31
for x,y,n be Integer st x,n are_coprime & x,y
are_congruent_mod n holds y,n are_coprime;
theorem :: GR_CY_3:32
for a,x be Nat, p be Prime st a,p are_coprime & a,x*x
are_congruent_mod p holds x,p are_coprime;
theorem :: GR_CY_3:33
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;
theorem :: GR_CY_3:34
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;
theorem :: GR_CY_3:35
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;
begin :: Multiplicative Group of a Field
theorem :: GR_CY_3:36
for p be Prime holds Z/Z*(p) = MultGroup (INT.Ring(p));
registration
let F be commutative Skew-Field;
cluster MultGroup (F) -> commutative;
end;
theorem :: GR_CY_3:37
for F be commutative Skew-Field, x be Element of MultGroup (F), x1 be
Element of F st x = x1 holds x" = x1";
theorem :: GR_CY_3:38
for F be commutative Skew-Field, G be finite Subgroup of MultGroup(F)
holds G is cyclic Group;