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


begin

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 )
proof end;

definition
let p be Nat;
attr p 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 set ;
existence
ex b1 being Prime st b1 is Safe
proof end;
end;

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

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

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

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

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

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

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

definition
let p be Nat;
attr p 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 set ;
existence
ex b1 being Prime st b1 is Sophie_Germain
proof end;
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 )
proof end;

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

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

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

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

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

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 & gr {a} is strict Subgroup of G )
proof end;

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 & card H2 = 2 & card Hq = q & card H2q = 2 * q & ( for H being strict Subgroup of Z/Z* p holds
( H = H1 or H = H2 or H = Hq or H = H2q ) ) )
proof end;

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:19;
end;

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

Lm2: 2 |^ 2 = 4
proof end;

Lm3: 2 |^ 3 = 8
proof end;

Lm4: 2 |^ 4 = 16
proof end;

Lm5: 2 |^ 8 = 256
proof end;

theorem :: GR_CY_3:16
Mersenne 0 = 0
proof end;

theorem :: GR_CY_3:17
Mersenne 1 = 1
proof end;

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
proof end;

theorem :: GR_CY_3:21
Mersenne 7 = 127
proof end;

theorem :: GR_CY_3:22
Mersenne 11 = 23 * 89
proof end;

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

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

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

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

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

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

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

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

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
proof end;

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

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

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

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

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

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

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

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 )
proof end;

begin

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

registration
let F be commutative Skew-Field;
cluster MultGroup F -> commutative ;
coherence
MultGroup F is commutative
proof end;
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 "
proof end;

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 & ( for x, xn being Element of F
for xz being Element of G st x = xz & xn = xz |^ n holds
eval (f,x) = xn - (1. F) ) )
proof end;

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 & 0 < n & ord a = n & b |^ n = 1_ G holds
b is Element of (gr {a})
proof end;

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