:: by Kenichi Arai and Hiroyuki Okazaki

::

:: Received April 7, 2009

:: Copyright (c) 2009-2017 Association of Mizar Users

:: 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 )

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

for p being Nat holds

( p is Safe iff ex sgp being Prime st (2 * sgp) + 1 = p );

registration

ex b_{1} being Prime st b_{1} is Safe
end;

cluster non empty V9() V10() V11() V15() V16() V19() V20() integer dim-like prime finite cardinal ext-real positive non negative Safe for set ;

existence ex b

proof end;

definition
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 );

for p being Nat holds

( p is Sophie_Germain iff (2 * p) + 1 is Prime );

registration

ex b_{1} being Prime st b_{1} is Sophie_Germain
end;

cluster non empty V9() V10() V11() V15() V16() V19() V20() integer dim-like prime finite cardinal ext-real positive non negative Sophie_Germain for set ;

existence ex b

proof end;

Lm1: for p being Nat st p > 2 holds

(2 * p) + 1 > 5

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

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 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 )

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 ) ) )

( 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;

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: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

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

ex q being Safe Prime st (Mersenne p) mod q = q - 2

proof end;

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

a > 1

proof end;

:: Other theorems

theorem :: GR_CY_3:32

for a, x being Nat

for p being Prime st a,p are_coprime & a,x * x are_congruent_mod p holds

x,p are_coprime

for p being Prime st a,p are_coprime & a,x * x are_congruent_mod p holds

x,p are_coprime

proof end;

theorem :: GR_CY_3:33

for a, x being Integer

for p being Prime st a,p are_coprime & a,x * x are_congruent_mod p holds

x,p are_coprime

for p being Prime st a,p are_coprime & a,x * x are_congruent_mod p holds

x,p are_coprime

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

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 )

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;

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 "

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

for G being finite Subgroup of MultGroup F holds G is cyclic Group

proof end;