:: 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 b₁ being Prime st b₁ 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 b₁ being Prime st b₁ 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;