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