:: Properties of Primes and Multiplicative Group of a Field
:: by Kenichi Arai and Hiroyuki Okazaki
::
:: Received April 7, 2009
:: Copyright (c) 2009-2012 Association of Mizar Users


begin

:: Safe Prime & Sophie_Germain Prime & Mersenne number
theorem Th1: :: GR_CY_3:1
for p, q being Prime
for k being Nat holds
( not k divides p * q or k = 1 or k = p or k = q or k = p * q )
proofend;

definition
let p be Nat;
attrp is Safe  means :Def1: :: GR_CY_3:def 1
 ex sgp being Prime st (2 * sgp) + 1 = p;
end;

:: deftheorem Def1 defines Safe GR_CY_3:def_1_:_
 for p being Nat holds
( p is Safe iff ex sgp being Prime st (2 * sgp) + 1 = p );

registration
cluster non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal Safe for set ;
existence
 ex b1 being Prime st b1 is Safe
proofend;
end;

theorem Th2: :: GR_CY_3:2
for p being Safe Prime holds p >= 5
proofend;

theorem Th3: :: GR_CY_3:3
for p being Safe Prime holds p mod 2 = 1
proofend;

theorem Th4: :: GR_CY_3:4
for p being Safe Prime st p <> 7 holds
p mod 3 = 2
proofend;

theorem Th5: :: GR_CY_3:5
for p being Safe Prime st p <> 5 holds
p mod 4 = 3
proofend;

theorem :: GR_CY_3:6
for p being Safe Prime st p <> 7 holds
p mod 6 = 5
proofend;

theorem :: GR_CY_3:7
for p being Safe Prime st p > 7 holds
p mod 12 = 11
proofend;

theorem :: GR_CY_3:8
for p being Safe Prime holds
( not p > 5 or p mod 8 = 3 or p mod 8 = 7 )
proofend;

definition
let p be Nat;
attrp is Sophie_Germain  means :Def2: :: GR_CY_3:def 2
(2 * p) + 1 is Prime;
end;

:: deftheorem Def2 defines Sophie_Germain GR_CY_3:def_2_:_
 for p being Nat holds
( p is Sophie_Germain iff (2 * p) + 1 is Prime );

registration
cluster non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal Sophie_Germain for set ;
existence
 ex b1 being Prime st b1 is Sophie_Germain
proofend;
end;

theorem :: GR_CY_3:9
for p being Sophie_Germain Prime holds
( not p > 2 or p mod 4 = 1 or p mod 4 = 3 )
proofend;

theorem Th10: :: GR_CY_3:10
for p being Safe Prime ex q being Sophie_Germain Prime st p = (2 * q) + 1
proofend;

Lm1:  for p being Nat st p > 2 holds
(2 * p) + 1 > 5
proofend;

theorem Th11: :: GR_CY_3:11
for p being Safe Prime ex q being Sophie_Germain Prime st Euler p = 2 * q
proofend;

theorem :: GR_CY_3:12
for p1, p2 being Safe Prime
for N being Nat st p1 <> p2 &amp; N = p1 * p2 holds
ex q1, q2 being Sophie_Germain Prime st Euler N = (4 * q1) * q2
proofend;

theorem Th13: :: GR_CY_3:13
for p being Safe Prime ex q being Sophie_Germain Prime st card (Z/Z* p) = 2 * q
proofend;

theorem Th14: :: GR_CY_3:14
for G being finite cyclic Group
for n, m being Nat st card G = n * m holds
ex a being Element of G st
( ord a = n &amp; gr {a} is strict Subgroup of G )
proofend;

theorem :: GR_CY_3:15
for p being Safe Prime ex q being Sophie_Germain Prime ex H1, H2, Hq, H2q being strict Subgroup of Z/Z* p st
( card H1 = 1 &amp; card H2 = 2 &amp; card Hq = q &amp; card H2q = 2 * q &amp; ( for H being strict Subgroup of Z/Z* p holds
( H = H1 or H = H2 or H = Hq or H = H2q ) ) )
proofend;

definition
let n be Nat;
func Mersenne n ->  Nat equals :: GR_CY_3:def 3
(2 |^ n) - 1;
correctness
coherence
(2 |^ n) - 1 is Nat;
by NAT_1:21, PREPOWER:11;
end;

:: deftheorem  defines Mersenne GR_CY_3:def_3_:_
 for n being Nat holds Mersenne n = (2 |^ n) - 1;

Lm2:  2 |^ 2 = 4
proofend;

Lm3:  2 |^ 3 = 8
proofend;

Lm4:  2 |^ 4 = 16
proofend;

Lm5:  2 |^ 8 = 256
proofend;

theorem :: GR_CY_3:16
Mersenne 0 = 0
proofend;

theorem :: GR_CY_3:17
Mersenne 1 = 1
proofend;

theorem :: GR_CY_3:18
Mersenne 2 = 3 by Lm2;

theorem :: GR_CY_3:19
Mersenne 3 = 7 by Lm3;

theorem :: GR_CY_3:20
Mersenne 5 = 31
proofend;

theorem :: GR_CY_3:21
Mersenne 7 = 127
proofend;

theorem :: GR_CY_3:22
Mersenne 11 = 23 * 89
proofend;

theorem :: GR_CY_3:23
for p being Prime st p <> 2 holds
(Mersenne p) mod (2 * p) = 1
proofend;

theorem :: GR_CY_3:24
for p being Prime st p <> 2 holds
(Mersenne p) mod 8 = 7
proofend;

theorem :: GR_CY_3:25
for p being Sophie_Germain Prime st p > 2 &amp; p mod 4 = 3 holds
ex q being Safe Prime st q divides Mersenne p
proofend;

theorem :: GR_CY_3:26
for p being Sophie_Germain Prime st p > 2 &amp; p mod 4 = 1 holds
ex q being Safe Prime st (Mersenne p) mod q = q - 2
proofend;

theorem Th27: :: GR_CY_3:27
for a, n being Nat st a > 1 holds
a - 1 divides (a |^ n) - 1
proofend;

Lm6:  for a, p being Nat st p > 1 &amp; (a |^ p) - 1 is Prime holds
a > 1
proofend;

theorem Th28: :: GR_CY_3:28
for a, p being Nat st p > 1 &amp; (a |^ p) - 1 is Prime holds
( a = 2 &amp; p is Prime )
proofend;

theorem :: GR_CY_3:29
for p being Nat st p > 1 &amp; Mersenne p is Prime holds
p is Prime by Th28;

:: Other theorems
theorem Th30: :: GR_CY_3:30
for a being Integer
for x, n being Nat holds (a |^ x) mod n = ((a mod n) |^ x) mod n
proofend;

theorem Th31: :: GR_CY_3:31
for x, y, n being Integer st x,n are_relative_prime &amp; x,y are_congruent_mod n holds
y,n are_relative_prime
proofend;

theorem :: GR_CY_3:32
for a, x being Nat
for p being Prime st a,p are_relative_prime &amp; a,x * x are_congruent_mod p holds
x,p are_relative_prime
proofend;

theorem :: GR_CY_3:33
for a, x being Integer
for p being Prime st a,p are_relative_prime &amp; a,x * x are_congruent_mod p holds
x,p are_relative_prime
proofend;

Lm7:  for n being Nat
for a being Integer st n <> 0 holds
a mod n,a are_congruent_mod n
proofend;

Lm8:  for n being Nat
for a being Integer st n <> 0 holds
ex an being Nat st an,a are_congruent_mod n
proofend;

Lm9:  for a, b, n, x being Nat st a,b are_congruent_mod n &amp; n <> 0 holds
a |^ x,b |^ x are_congruent_mod n
proofend;

theorem :: GR_CY_3:34
for a, b being Integer
for n, x being Nat st a,b are_congruent_mod n &amp; n <> 0 holds
a |^ x,b |^ x are_congruent_mod n
proofend;

theorem :: GR_CY_3:35
for a being Integer
for n being Prime holds
( not (a * a) mod n = 1 or a,1 are_congruent_mod n or a, - 1 are_congruent_mod n )
proofend;

begin

theorem :: GR_CY_3:36
for p being Prime holds Z/Z* p = MultGroup (INT.Ring p)
proofend;

registration
let F be commutative Skew-Field;
cluster MultGroup F ->  commutative ;
coherence
 MultGroup F is commutative
proofend;
end;

theorem :: GR_CY_3:37
for F being commutative Skew-Field
for x being Element of (MultGroup F)
for x1 being Element of F st x = x1 holds
x " = x1 "
proofend;

Lm10:  for F being commutative Skew-Field
for G being Subgroup of MultGroup F
for n being Nat st 0 < n holds
ex f being Polynomial of F st
( deg f = n &amp; ( for x, xn being Element of F
for xz being Element of G st x = xz &amp; xn = xz |^ n holds
eval (f,x) = xn - (1. F) ) )
proofend;

Lm11:  for F being commutative Skew-Field
for G being Subgroup of MultGroup F
for a, b being Element of G
for n being Nat st G is finite &amp; 0 < n &amp; ord a = n &amp; b |^ n = 1_ G holds
b is Element of (gr {a})
proofend;

theorem :: GR_CY_3:38
for F being commutative Skew-Field
for G being finite Subgroup of MultGroup F holds G is cyclic Group
proofend;