:: Properties of Primes and Multiplicative Group of a Field
:: by Kenichi Arai and Hiroyuki Okazaki
::
:: Received April 7, 2009
:: Copyright (c) 2009 Association of Mizar Users
theorem LMPQ: :: 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 )
:: deftheorem defASP 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 );
theorem SP1: :: GR_CY_3:2
theorem SPM1: :: GR_CY_3:3
theorem SPM2: :: GR_CY_3:4
theorem SPM3: :: GR_CY_3:5
theorem :: GR_CY_3:6
theorem :: GR_CY_3:7
theorem :: GR_CY_3:8
:: deftheorem defSGP defines Sophie_Germain GR_CY_3:def 2 :
theorem :: GR_CY_3:9
theorem SGSP0: :: GR_CY_3:10
SGSP2:
for p being Nat st p > 2 holds
(2 * p) + 1 > 5
theorem SGSP3: :: GR_CY_3:11
theorem :: GR_CY_3:12
theorem SF1: :: GR_CY_3:13
theorem SF2: :: GR_CY_3:14
theorem :: GR_CY_3:15
:: deftheorem defines Mersenne GR_CY_3:def 3 :
MSLm1:
2 |^ 2 = 4
MSLm2:
2 |^ 3 = 8
MSLm3:
2 |^ 4 = 16
MSLm4:
2 |^ 8 = 256
theorem :: GR_CY_3:16
theorem :: GR_CY_3:17
theorem :: GR_CY_3:18
theorem :: GR_CY_3:19
theorem :: GR_CY_3:20
theorem :: GR_CY_3:21
theorem :: GR_CY_3:22
theorem :: GR_CY_3:23
theorem :: GR_CY_3:24
theorem :: GR_CY_3:25
theorem :: GR_CY_3:26
theorem LmST1: :: GR_CY_3:27
LmST2:
for a, p being Nat st p > 1 & (a |^ p) - 1 is Prime holds
a > 1
theorem LmST3: :: GR_CY_3:28
theorem :: GR_CY_3:29
theorem INTPOW: :: GR_CY_3:30
theorem THP: :: GR_CY_3:31
theorem :: GR_CY_3:32
theorem :: GR_CY_3:33
Lmmod1:
for n being Nat
for a being Integer st n <> 0 holds
a mod n,a are_congruent_mod n
Lmmod2:
for n being Nat
for a being Integer st n <> 0 holds
ex an being Nat st an,a are_congruent_mod n
Lmsm1:
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
theorem :: GR_CY_3:34
theorem :: GR_CY_3:35
theorem :: GR_CY_3:36
theorem :: GR_CY_3:37
LM0X62a:
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) ) )
LM0X62:
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})
theorem :: GR_CY_3:38