:: Properties of Primes and Multiplicative Group of a Field :: by Kenichi Arai and Hiroyuki Okazaki :: :: Received April 7, 2009 :: Copyright (c) 2009-2018 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;