:: GR_CY_3 semantic presentation
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
let p, q be Prime; ::_thesis: for k being Nat holds
( not k divides p * q or k = 1 or k = p or k = q or k = p * q )
let k be Nat; ::_thesis: ( not k divides p * q or k = 1 or k = p or k = q or k = p * q )
assume A1: k divides p * q ; ::_thesis: ( k = 1 or k = p or k = q or k = p * q )
percases ( k,p are_relative_prime or k gcd p = p ) by PEPIN:2;
suppose k,p are_relative_prime ; ::_thesis: ( k = 1 or k = p or k = q or k = p * q )
then k divides q by A1, PEPIN:3;
hence ( k = 1 or k = p or k = q or k = p * q ) by INT_2:def_4; ::_thesis: verum
end;
suppose k gcd p = p ; ::_thesis: ( k = 1 or k = p or k = q or k = p * q )
then p divides k by NAT_D:def_5;
then consider l being Nat such that
A2: k = p * l by NAT_D:def_3;
consider m being Nat such that
A3: k * m = p * q by A1, NAT_D:def_3;
p * (l * m) = p * q by A2, A3;
then l * m = q by XCMPLX_1:5;
then l divides q by NAT_D:def_3;
then ( l = 1 or l = q ) by INT_2:def_4;
hence ( k = 1 or k = p or k = q or k = p * q ) by A2; ::_thesis: verum
end;
end;
end;
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
proof
reconsider p = 5 as Prime by PEPIN:59;
reconsider sgp = 2 as Prime by INT_2:28;
take p ; ::_thesis: p is Safe
p = (2 * sgp) + 1 ;
hence p is Safe by Def1; ::_thesis: verum
end;
end;
theorem Th2: :: GR_CY_3:2
for p being Safe Prime holds p >= 5
proof
let p be Safe Prime; ::_thesis: p >= 5
consider q being Prime such that
A1: (2 * q) + 1 = p by Def1;
q > 1 by INT_2:def_4;
then q >= 1 + 1 by NAT_1:13;
then 2 * q >= 2 * 2 by XREAL_1:64;
then (2 * q) + 1 >= 4 + 1 by XREAL_1:7;
hence p >= 5 by A1; ::_thesis: verum
end;
theorem Th3: :: GR_CY_3:3
for p being Safe Prime holds p mod 2 = 1
proof
let p be Safe Prime; ::_thesis: p mod 2 = 1
p >= 4 + 1 by Th2;
then p > 4 by NAT_1:13;
then p > 4 - 2 by XREAL_1:51;
then p is odd by PEPIN:17;
hence p mod 2 = 1 by NAT_2:22; ::_thesis: verum
end;
theorem Th4: :: GR_CY_3:4
for p being Safe Prime st p <> 7 holds
p mod 3 = 2
proof
let p be Safe Prime; ::_thesis: ( p <> 7 implies p mod 3 = 2 )
set k = p mod 3;
consider q being Prime such that
A1: (2 * q) + 1 = p by Def1;
assume A2: p <> 7 ; ::_thesis: p mod 3 = 2
A3: now__::_thesis:_(_not_p_mod_3_=_0_&_not_p_mod_3_=_1_)
assume A4: ( p mod 3 = 0 or p mod 3 = 1 ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( p mod 3 = 0 or p mod 3 = 1 ) by A4;
suppose p mod 3 = 0 ; ::_thesis: contradiction
then 3 divides p by INT_1:62;
then 3 = p by INT_2:def_4;
hence contradiction by Th2; ::_thesis: verum
end;
supposeA5: p mod 3 = 1 ; ::_thesis: contradiction
2,3 are_relative_prime by INT_2:28, INT_2:30, PEPIN:41;
then A6: 2 gcd 3 = 1 by INT_2:def_3;
3 divides ((2 * q) + 1) - 1 by A1, A5, PEPIN:8;
then 3 divides q by A6, WSIERP_1:29;
then 3 = q by INT_2:def_4;
hence contradiction by A2, A1; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
p mod 3 < 2 + 1 by NAT_D:62;
then p mod 3 <= 0 + 2 by NAT_1:13;
hence p mod 3 = 2 by A3, NAT_1:26; ::_thesis: verum
end;
theorem Th5: :: GR_CY_3:5
for p being Safe Prime st p <> 5 holds
p mod 4 = 3
proof
let p be Safe Prime; ::_thesis: ( p <> 5 implies p mod 4 = 3 )
set k = p mod 4;
consider q being Prime such that
A1: (2 * q) + 1 = p by Def1;
assume A2: p <> 5 ; ::_thesis: p mod 4 = 3
A3: now__::_thesis:_(_not_p_mod_4_=_0_&_not_p_mod_4_=_1_&_not_p_mod_4_=_2_)
assume A4: ( p mod 4 = 0 or p mod 4 = 1 or p mod 4 = 2 ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( p mod 4 = 0 or p mod 4 = 1 or p mod 4 = 2 ) by A4;
suppose p mod 4 = 0 ; ::_thesis: contradiction
then 4 divides p by INT_1:62;
hence contradiction by INT_2:29, INT_2:def_4; ::_thesis: verum
end;
suppose p mod 4 = 1 ; ::_thesis: contradiction
then ((p div 4) * 4) + 1 = (2 * q) + 1 by A1, INT_1:59;
then q = (p div 4) * 2 ;
then 2 divides q by INT_1:def_3;
then 2 = q by INT_2:def_4;
hence contradiction by A2, A1; ::_thesis: verum
end;
suppose p mod 4 = 2 ; ::_thesis: contradiction
then p = ((p div 4) * 4) + 2 by INT_1:59
.= (((p div 4) * 2) + 1) * 2 ;
then 2 divides p by INT_1:def_3;
then 2 = p by INT_2:def_4;
hence contradiction by Th2; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
p mod 4 < 3 + 1 by NAT_D:62;
then p mod 4 <= 0 + 3 by NAT_1:13;
hence p mod 4 = 3 by A3, NAT_1:27; ::_thesis: verum
end;
theorem :: GR_CY_3:6
for p being Safe Prime st p <> 7 holds
p mod 6 = 5
proof
let p be Safe Prime; ::_thesis: ( p <> 7 implies p mod 6 = 5 )
assume A1: p <> 7 ; ::_thesis: p mod 6 = 5
A2: (4 * p) mod 6 = (2 * (2 * p)) mod (2 * 3)
.= 2 * ((2 * p) mod 3) by INT_4:20
.= 2 * (((2 mod 3) * (p mod 3)) mod 3) by NAT_D:67
.= 2 * ((2 * (p mod 3)) mod 3) by NAT_D:24
.= 2 * ((2 * 2) mod 3) by A1, Th4
.= 2 * ((1 + (3 * 1)) mod 3)
.= 2 * (1 mod 3) by NAT_D:61
.= 2 * 1 by PEPIN:5 ;
A3: (3 * p) mod 6 = (3 * p) mod (3 * 2)
.= 3 * (p mod 2) by INT_4:20
.= 3 * 1 by Th3 ;
p mod 6 = (p + (6 * p)) mod 6 by NAT_D:61
.= ((3 * p) + (4 * p)) mod 6
.= ((3 * 1) + (2 * 1)) mod 6 by A3, A2, NAT_D:66
.= 5 by NAT_D:24 ;
hence p mod 6 = 5 ; ::_thesis: verum
end;
theorem :: GR_CY_3:7
for p being Safe Prime st p > 7 holds
p mod 12 = 11
proof
let p be Safe Prime; ::_thesis: ( p > 7 implies p mod 12 = 11 )
assume A1: p > 7 ; ::_thesis: p mod 12 = 11
then p > 7 - 2 by XREAL_1:51;
then A2: p mod 4 = 3 by Th5;
A3: (9 * p) mod 12 = (3 * (3 * p)) mod (3 * 4)
.= 3 * ((3 * p) mod 4) by INT_4:20
.= 3 * (((3 mod 4) * (p mod 4)) mod 4) by NAT_D:67
.= 3 * ((3 * 3) mod 4) by A2, NAT_D:24
.= 3 * ((1 + (4 * 2)) mod 4)
.= 3 * (1 mod 4) by NAT_D:61
.= 3 * 1 by PEPIN:5 ;
A4: (4 * p) mod 12 = (4 * p) mod (4 * 3)
.= 4 * (p mod 3) by INT_4:20
.= 4 * 2 by A1, Th4 ;
p mod 12 = (p + (12 * p)) mod 12 by NAT_D:61
.= ((4 * p) + (9 * p)) mod 12
.= ((4 * 2) + (3 * 1)) mod 12 by A4, A3, NAT_D:66
.= 11 by NAT_D:24 ;
hence p mod 12 = 11 ; ::_thesis: verum
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
8 = 2 * 4 ;
then A1: 2 divides 8 by NAT_D:def_3;
let p be Safe Prime; ::_thesis: ( not p > 5 or p mod 8 = 3 or p mod 8 = 7 )
set k = p mod 8;
consider q being Prime such that
A2: (2 * q) + 1 = p by Def1;
assume A3: p > 5 ; ::_thesis: ( p mod 8 = 3 or p mod 8 = 7 )
A4: now__::_thesis:_(_not_p_mod_8_=_0_&_not_p_mod_8_=_1_&_not_p_mod_8_=_2_&_not_p_mod_8_=_4_&_not_p_mod_8_=_5_&_not_p_mod_8_=_6_)
assume A5: ( p mod 8 = 0 or p mod 8 = 1 or p mod 8 = 2 or p mod 8 = 4 or p mod 8 = 5 or p mod 8 = 6 ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( p mod 8 = 0 or p mod 8 = 1 or p mod 8 = 2 or p mod 8 = 4 or p mod 8 = 5 or p mod 8 = 6 ) by A5;
suppose p mod 8 = 0 ; ::_thesis: contradiction
then 8 divides p by INT_1:62;
then 2 divides p by A1, INT_2:9;
then 2 = p by INT_2:def_4;
hence contradiction by Th2; ::_thesis: verum
end;
suppose p mod 8 = 1 ; ::_thesis: contradiction
then ((p div 8) * 8) + 1 = (2 * q) + 1 by A2, INT_1:59;
then q = (p div 8) * 4 ;
then 4 divides q by INT_1:def_3;
hence contradiction by INT_2:29, INT_2:def_4; ::_thesis: verum
end;
suppose p mod 8 = 2 ; ::_thesis: contradiction
then p = ((p div 8) * 8) + 2 by INT_1:59
.= (((p div 8) * 4) + 1) * 2 ;
then 2 divides p by INT_1:def_3;
then 2 = p by INT_2:def_4;
hence contradiction by Th2; ::_thesis: verum
end;
suppose p mod 8 = 4 ; ::_thesis: contradiction
then p = ((p div 8) * 8) + 4 by INT_1:59
.= (((p div 8) * 4) + 2) * 2 ;
then 2 divides p by INT_1:def_3;
then 2 = p by INT_2:def_4;
hence contradiction by Th2; ::_thesis: verum
end;
suppose p mod 8 = 5 ; ::_thesis: contradiction
then ((p div 8) * 8) + 5 = (2 * q) + 1 by A2, INT_1:59;
then q = (((p div 8) * 2) + 1) * 2 ;
then 2 divides q by INT_1:def_3;
then 2 = q by INT_2:def_4;
hence contradiction by A3, A2; ::_thesis: verum
end;
suppose p mod 8 = 6 ; ::_thesis: contradiction
then p = ((p div 8) * 8) + 6 by INT_1:59
.= (((p div 8) * 4) + 3) * 2 ;
then 2 divides p by INT_1:def_3;
then 2 = p by INT_2:def_4;
hence contradiction by Th2; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
p mod 8 < 7 + 1 by NAT_D:62;
then p mod 8 <= 0 + 7 by NAT_1:13;
hence ( p mod 8 = 3 or p mod 8 = 7 ) by A4, NAT_1:31; ::_thesis: verum
end;
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
proof
reconsider p = 5 as Prime by PEPIN:59;
reconsider sgp = 2 as Prime by INT_2:28;
take sgp ; ::_thesis: sgp is Sophie_Germain
p = (2 * sgp) + 1 ;
hence sgp is Sophie_Germain by Def2; ::_thesis: verum
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
let p be Sophie_Germain Prime; ::_thesis: ( not p > 2 or p mod 4 = 1 or p mod 4 = 3 )
set k = p mod 4;
assume A1: p > 2 ; ::_thesis: ( p mod 4 = 1 or p mod 4 = 3 )
A2: now__::_thesis:_(_not_p_mod_4_=_0_&_not_p_mod_4_=_2_)
assume A3: ( p mod 4 = 0 or p mod 4 = 2 ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( p mod 4 = 0 or p mod 4 = 2 ) by A3;
suppose p mod 4 = 0 ; ::_thesis: contradiction
then 4 divides p by INT_1:62;
hence contradiction by INT_2:29, INT_2:def_4; ::_thesis: verum
end;
suppose p mod 4 = 2 ; ::_thesis: contradiction
then p = ((p div 4) * 4) + 2 by INT_1:59
.= (((p div 4) * 2) + 1) * 2 ;
then 2 divides p by INT_1:def_3;
hence contradiction by A1, INT_2:def_4; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
p mod 4 < 3 + 1 by NAT_D:62;
then p mod 4 <= 0 + 3 by NAT_1:13;
hence ( p mod 4 = 1 or p mod 4 = 3 ) by A2, NAT_1:27; ::_thesis: verum
end;
theorem Th10: :: GR_CY_3:10
for p being Safe Prime ex q being Sophie_Germain Prime st p = (2 * q) + 1
proof
let p be Safe Prime; ::_thesis: ex q being Sophie_Germain Prime st p = (2 * q) + 1
consider q being Prime such that
A1: (2 * q) + 1 = p by Def1;
q is Sophie_Germain Prime by A1, Def2;
hence ex q being Sophie_Germain Prime st p = (2 * q) + 1 by A1; ::_thesis: verum
end;
Lm1: for p being Nat st p > 2 holds
(2 * p) + 1 > 5
proof
let p be Nat; ::_thesis: ( p > 2 implies (2 * p) + 1 > 5 )
assume p > 2 ; ::_thesis: (2 * p) + 1 > 5
then 2 * p > 2 * 2 by XREAL_1:68;
then (2 * p) + 1 > 4 + 1 by XREAL_1:8;
hence (2 * p) + 1 > 5 ; ::_thesis: verum
end;
theorem Th11: :: GR_CY_3:11
for p being Safe Prime ex q being Sophie_Germain Prime st Euler p = 2 * q
proof
let p be Safe Prime; ::_thesis: ex q being Sophie_Germain Prime st Euler p = 2 * q
A1: Euler p = p - 1 by EULER_1:20;
ex q being Sophie_Germain Prime st p = (2 * q) + 1 by Th10;
hence ex q being Sophie_Germain Prime st Euler p = 2 * q by A1; ::_thesis: verum
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
let p1, p2 be Safe Prime; ::_thesis: for N being Nat st p1 <> p2 & N = p1 * p2 holds
ex q1, q2 being Sophie_Germain Prime st Euler N = (4 * q1) * q2
let N be Nat; ::_thesis: ( p1 <> p2 & N = p1 * p2 implies ex q1, q2 being Sophie_Germain Prime st Euler N = (4 * q1) * q2 )
assume that
A1: p1 <> p2 and
A2: N = p1 * p2 ; ::_thesis: ex q1, q2 being Sophie_Germain Prime st Euler N = (4 * q1) * q2
A3: p2 > 1 by INT_2:def_4;
consider q2 being Sophie_Germain Prime such that
A4: Euler p2 = 2 * q2 by Th11;
consider q1 being Sophie_Germain Prime such that
A5: Euler p1 = 2 * q1 by Th11;
p1 > 1 by INT_2:def_4;
then Euler N = (Euler p1) * (Euler p2) by A1, A2, A3, EULER_1:21, INT_2:30
.= (4 * q1) * q2 by A5, A4 ;
hence ex q1, q2 being Sophie_Germain Prime st Euler N = (4 * q1) * q2 ; ::_thesis: verum
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
let p be Safe Prime; ::_thesis: ex q being Sophie_Germain Prime st card (Z/Z* p) = 2 * q
consider q being Sophie_Germain Prime such that
A1: (2 * q) + 1 = p by Th10;
p - 1 = 2 * q by A1;
hence ex q being Sophie_Germain Prime st card (Z/Z* p) = 2 * q by INT_7:23; ::_thesis: verum
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
let G be finite cyclic Group; ::_thesis: 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 )
let n, m be Nat; ::_thesis: ( card G = n * m implies ex a being Element of G st
( ord a = n & gr {a} is strict Subgroup of G ) )
consider g being Element of G such that
A1: ord g = card G by GR_CY_1:19;
A2: m in NAT by ORDINAL1:def_12;
A3: n in NAT by ORDINAL1:def_12;
assume card G = n * m ; ::_thesis: ex a being Element of G st
( ord a = n & gr {a} is strict Subgroup of G )
then ord (g |^ m) = n by A1, A2, A3, INT_7:30;
then consider a being Element of G such that
A4: ord a = n ;
take a ; ::_thesis: ( ord a = n & gr {a} is strict Subgroup of G )
thus ( ord a = n & gr {a} is strict Subgroup of G ) by A4; ::_thesis: verum
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
let p be Safe Prime; ::_thesis: 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 ) ) )
consider q being Sophie_Germain Prime such that
A1: card (Z/Z* p) = 2 * q by Th13;
A2: Z/Z* p is cyclic Group by INT_7:31;
then consider a being Element of (Z/Z* p) such that
A3: ord a = 2 and
gr {a} is strict Subgroup of Z/Z* p by A1, Th14;
consider b being Element of (Z/Z* p) such that
A4: ord b = q and
gr {b} is strict Subgroup of Z/Z* p by A1, A2, Th14;
A5: card (gr {b}) = q by A4, GR_CY_1:7;
card ((1). (Z/Z* p)) = 1 by GROUP_2:69;
then consider H1 being strict Subgroup of Z/Z* p such that
A6: card H1 = 1 ;
Z/Z* p is strict Subgroup of Z/Z* p by GROUP_2:54;
then consider H2q being strict Subgroup of Z/Z* p such that
A7: card H2q = 2 * q by A1;
card (gr {a}) = 2 by A3, GR_CY_1:7;
then consider H2, Hq being strict Subgroup of Z/Z* p such that
A8: card H2 = 2 and
A9: card Hq = q by A5;
take q ; ::_thesis: 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 ) ) )
take H1 ; ::_thesis: ex 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 ) ) )
take H2 ; ::_thesis: ex 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 ) ) )
take Hq ; ::_thesis: ex 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 ) ) )
take H2q ; ::_thesis: ( 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 ) ) )
now__::_thesis:_for_H_being_strict_Subgroup_of_Z/Z*_p_holds_
(_H_=_H1_or_H_=_H2_or_H_=_Hq_or_H_=_H2q_)
let H be strict Subgroup of Z/Z* p; ::_thesis: ( H = H1 or H = H2 or H = Hq or H = H2q )
consider G1 being strict Subgroup of Z/Z* p such that
card G1 = card H and
A10: for G2 being strict Subgroup of Z/Z* p st card G2 = card H holds
G2 = G1 by A1, A2, GROUP_2:148, GR_CY_2:22;
A11: G1 = H by A10;
now__::_thesis:_(_H_=_H1_or_H_=_H2_or_H_=_Hq_or_H_=_H2q_)
percases ( card H = 1 or card H = 2 or card H = q or card H = 2 * q ) by A1, Th1, GROUP_2:148, INT_2:28;
suppose card H = 1 ; ::_thesis: ( H = H1 or H = H2 or H = Hq or H = H2q )
hence ( H = H1 or H = H2 or H = Hq or H = H2q ) by A6, A10, A11; ::_thesis: verum
end;
suppose card H = 2 ; ::_thesis: ( H = H1 or H = H2 or H = Hq or H = H2q )
hence ( H = H1 or H = H2 or H = Hq or H = H2q ) by A8, A10, A11; ::_thesis: verum
end;
suppose card H = q ; ::_thesis: ( H = H1 or H = H2 or H = Hq or H = H2q )
hence ( H = H1 or H = H2 or H = Hq or H = H2q ) by A9, A10, A11; ::_thesis: verum
end;
suppose card H = 2 * q ; ::_thesis: ( H = H1 or H = H2 or H = Hq or H = H2q )
hence ( H = H1 or H = H2 or H = Hq or H = H2q ) by A7, A10, A11; ::_thesis: verum
end;
end;
end;
hence ( H = H1 or H = H2 or H = Hq or H = H2q ) ; ::_thesis: verum
end;
hence ( 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 ) ) ) by A7, A8, A9, A6; ::_thesis: verum
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:11;
end;
:: deftheorem defines Mersenne GR_CY_3:def_3_:_
for n being Nat holds Mersenne n = (2 |^ n) - 1;
Lm2: 2 |^ 2 = 4
proof
2 |^ 2 = 2 |^ (1 + 1)
.= (2 |^ 1) * 2 by NEWTON:6
.= 2 * 2 by NEWTON:5 ;
hence 2 |^ 2 = 4 ; ::_thesis: verum
end;
Lm3: 2 |^ 3 = 8
proof
2 |^ 3 = 2 |^ (2 + 1)
.= 4 * 2 by Lm2, NEWTON:6 ;
hence 2 |^ 3 = 8 ; ::_thesis: verum
end;
Lm4: 2 |^ 4 = 16
proof
2 |^ 4 = 2 |^ (2 + 2)
.= 4 * 4 by Lm2, NEWTON:8 ;
hence 2 |^ 4 = 16 ; ::_thesis: verum
end;
Lm5: 2 |^ 8 = 256
proof
2 |^ 8 = 2 |^ (4 + 4)
.= 16 * 16 by Lm4, NEWTON:8 ;
hence 2 |^ 8 = 256 ; ::_thesis: verum
end;
theorem :: GR_CY_3:16
Mersenne 0 = 0
proof
thus Mersenne 0 = 1 - 1 by NEWTON:4
.= 0 ; ::_thesis: verum
end;
theorem :: GR_CY_3:17
Mersenne 1 = 1
proof
thus Mersenne 1 = 2 - 1 by NEWTON:5
.= 1 ; ::_thesis: verum
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
thus Mersenne 5 = (2 |^ (3 + 2)) - 1
.= ((2 |^ 3) * (2 |^ 2)) - 1 by NEWTON:8
.= 31 by Lm2, Lm3 ; ::_thesis: verum
end;
theorem :: GR_CY_3:21
Mersenne 7 = 127
proof
thus Mersenne 7 = (2 |^ (4 + 3)) - 1
.= ((2 |^ 4) * (2 |^ 3)) - 1 by NEWTON:8
.= 127 by Lm3, Lm4 ; ::_thesis: verum
end;
theorem :: GR_CY_3:22
Mersenne 11 = 23 * 89
proof
thus Mersenne 11 = (2 |^ (8 + 3)) - 1
.= ((2 |^ 8) * (2 |^ 3)) - 1 by NEWTON:8
.= 23 * 89 by Lm3, Lm5 ; ::_thesis: verum
end;
theorem :: GR_CY_3:23
for p being Prime st p <> 2 holds
(Mersenne p) mod (2 * p) = 1
proof
let p be Prime; ::_thesis: ( p <> 2 implies (Mersenne p) mod (2 * p) = 1 )
assume A1: p <> 2 ; ::_thesis: (Mersenne p) mod (2 * p) = 1
p > 1 by INT_2:def_4;
then 2 * p > 2 * 1 by XREAL_1:68;
then A2: 2 * p > 2 - 1 by XREAL_1:51;
(Mersenne p) mod (2 * p) = ((2 * (2 |^ (p -' 1))) - 1) mod (2 * p) by PEPIN:26
.= (((2 * (2 |^ (p -' 1))) mod (2 * p)) - (1 mod (2 * p))) mod (2 * p) by INT_6:7
.= ((2 * ((2 |^ (p -' 1)) mod p)) - (1 mod (2 * p))) mod (2 * p) by INT_4:20
.= ((2 * 1) - (1 mod (2 * p))) mod (2 * p) by A1, INT_2:28, INT_2:30, PEPIN:37
.= ((2 * 1) - 1) mod (2 * p) by A2, PEPIN:5 ;
hence (Mersenne p) mod (2 * p) = 1 by A2, PEPIN:5; ::_thesis: verum
end;
theorem :: GR_CY_3:24
for p being Prime st p <> 2 holds
(Mersenne p) mod 8 = 7
proof
let p be Prime; ::_thesis: ( p <> 2 implies (Mersenne p) mod 8 = 7 )
A1: p > 1 by INT_2:def_4;
then A2: p >= 1 + 1 by NAT_1:13;
assume p <> 2 ; ::_thesis: (Mersenne p) mod 8 = 7
then p > 2 + 0 by A2, XXREAL_0:1;
then p - 2 > 2 - 2 by XREAL_1:14;
then A3: p -' 2 > 0 by A2, XREAL_1:233;
A4: p -' 1 > 0 by A1, NAT_D:49;
(Mersenne p) mod 8 = ((2 * (2 |^ (p -' 1))) - 1) mod 8 by PEPIN:26
.= (((2 * (2 |^ (p -' 1))) mod (2 * 4)) - (1 mod 8)) mod 8 by INT_6:7
.= ((2 * ((2 |^ (p -' 1)) mod 4)) - (1 mod 8)) mod 8 by INT_4:20
.= ((2 * ((2 * (2 |^ ((p -' 1) -' 1))) mod (2 * 2))) - (1 mod 8)) mod 8 by A4, PEPIN:26
.= ((2 * ((2 * (2 |^ (p -' 2))) mod (2 * 2))) - (1 mod 8)) mod 8 by NAT_D:45
.= ((2 * (2 * ((2 |^ (p -' 2)) mod 2))) - (1 mod 8)) mod 8 by INT_4:20
.= ((4 * ((2 |^ (p -' 2)) mod 2)) - 1) mod 8 by PEPIN:5
.= ((4 * 0) - 1) mod 8 by A3, PEPIN:36
.= ((- 1) + (8 * 1)) mod 8 by NAT_D:61
.= 7 by NAT_D:24 ;
hence (Mersenne p) mod 8 = 7 ; ::_thesis: verum
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
let p be Sophie_Germain Prime; ::_thesis: ( p > 2 & p mod 4 = 3 implies ex q being Safe Prime st q divides Mersenne p )
assume that
A1: p > 2 and
A2: p mod 4 = 3 ; ::_thesis: ex q being Safe Prime st q divides Mersenne p
set q = (2 * p) + 1;
A3: (2 * p) + 1 is Safe Prime by Def1, Def2;
(2 * p) + 1 > 5 by A1, Lm1;
then A4: (2 * p) + 1 > 5 - 3 by XREAL_1:51;
then 2,(2 * p) + 1 are_relative_prime by A3, INT_2:28, INT_2:30;
then A5: 2 gcd ((2 * p) + 1) = 1 by INT_2:def_3;
p = ((p div 4) * 4) + 3 by A2, INT_1:59;
then (2 * p) + 1 = ((p div 4) * 8) + 7 ;
then ((2 * p) + 1) mod 8 = 7 mod 8 by NAT_D:21
.= 7 by NAT_D:24 ;
then 2 is_quadratic_residue_mod (2 * p) + 1 by A3, A4, INT_5:43;
then ((2 |^ ((((2 * p) + 1) -' 1) div 2)) - 1) mod ((2 * p) + 1) = 0 by A3, A4, A5, INT_5:20;
then ((2 |^ ((2 * p) div 2)) - 1) mod ((2 * p) + 1) = 0 by NAT_D:34;
then ((2 |^ p) - 1) mod ((2 * p) + 1) = 0 by NAT_D:18;
then (2 * p) + 1 divides (2 |^ p) - 1 by INT_1:62;
hence ex q being Safe Prime st q divides Mersenne p by A3; ::_thesis: verum
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
let p be Sophie_Germain Prime; ::_thesis: ( p > 2 & p mod 4 = 1 implies ex q being Safe Prime st (Mersenne p) mod q = q - 2 )
assume that
A1: p > 2 and
A2: p mod 4 = 1 ; ::_thesis: ex q being Safe Prime st (Mersenne p) mod q = q - 2
set q = (2 * p) + 1;
A3: (2 * p) + 1 is Safe Prime by Def1, Def2;
A4: (2 * p) + 1 > 5 by A1, Lm1;
then A5: (2 * p) + 1 > 5 - 3 by XREAL_1:51;
then 2,(2 * p) + 1 are_relative_prime by A3, INT_2:28, INT_2:30;
then A6: 2 gcd ((2 * p) + 1) = 1 by INT_2:def_3;
p = ((p div 4) * 4) + 1 by A2, INT_1:59;
then (2 * p) + 1 = ((p div 4) * 8) + 3 ;
then ((2 * p) + 1) mod 8 = 3 mod 8 by NAT_D:21
.= 3 by NAT_D:24 ;
then not 2 is_quadratic_residue_mod (2 * p) + 1 by A3, A5, INT_5:44;
then (2 |^ ((((2 * p) + 1) -' 1) div 2)) mod ((2 * p) + 1) = ((2 * p) + 1) - 1 by A3, A5, A6, INT_5:19;
then A7: (2 |^ ((2 * p) div 2)) mod ((2 * p) + 1) = ((2 * p) + 1) - 1 by NAT_D:34;
A8: (2 * p) + 1 > 5 - 4 by A4, XREAL_1:51;
then (2 * p) + 1 >= 1 + 1 by NAT_1:13;
then A9: ((2 * p) + 1) - 2 is Nat by NAT_1:21;
(Mersenne p) mod ((2 * p) + 1) = (((2 |^ p) mod ((2 * p) + 1)) - (1 mod ((2 * p) + 1))) mod ((2 * p) + 1) by INT_6:7
.= ((((2 * p) + 1) - 1) - (1 mod ((2 * p) + 1))) mod ((2 * p) + 1) by A7, NAT_D:18
.= ((((2 * p) + 1) - 1) - 1) mod ((2 * p) + 1) by A8, PEPIN:5
.= ((2 * p) + 1) - 2 by A9, NAT_D:24, XREAL_1:44 ;
hence ex q being Safe Prime st (Mersenne p) mod q = q - 2 by A3; ::_thesis: verum
end;
theorem Th27: :: GR_CY_3:27
for a, n being Nat st a > 1 holds
a - 1 divides (a |^ n) - 1
proof
let a, n be Nat; ::_thesis: ( a > 1 implies a - 1 divides (a |^ n) - 1 )
A1: (2 |^ n) - 1 is Nat by NAT_1:21, PREPOWER:11;
assume a > 1 ; ::_thesis: a - 1 divides (a |^ n) - 1
then A2: a >= 1 + 1 by NAT_1:13;
percases ( a = 2 or a > 2 ) by A2, XXREAL_0:1;
supposeA3: a = 2 ; ::_thesis: a - 1 divides (a |^ n) - 1
then ((a |^ n) - 1) mod (a - 1) = 0 by A1, RADIX_2:1;
hence a - 1 divides (a |^ n) - 1 by A3, INT_1:62; ::_thesis: verum
end;
supposeA4: a > 2 ; ::_thesis: a - 1 divides (a |^ n) - 1
then A5: a - 1 > 2 - 1 by XREAL_1:9;
A6: a - 1 is Nat by A4, NAT_1:20;
a mod (a - 1) = (a + ((a - 1) * (- 1))) mod (a - 1) by NAT_D:61
.= 1 by A5, PEPIN:5 ;
then A7: (a |^ n) mod (a - 1) = 1 by A5, A6, PEPIN:35;
((a |^ n) - 1) mod (a - 1) = (((a |^ n) mod (a - 1)) - (1 mod (a - 1))) mod (a - 1) by INT_6:7
.= (1 - 1) mod (a - 1) by A5, A7, PEPIN:5
.= 0 by A6, NAT_D:26 ;
hence a - 1 divides (a |^ n) - 1 by A5, A6, INT_1:62; ::_thesis: verum
end;
end;
end;
Lm6: for a, p being Nat st p > 1 & (a |^ p) - 1 is Prime holds
a > 1
proof
let a, p be Nat; ::_thesis: ( p > 1 & (a |^ p) - 1 is Prime implies a > 1 )
assume that
A1: p > 1 and
A2: (a |^ p) - 1 is Prime ; ::_thesis: a > 1
A3: now__::_thesis:_(_not_a_=_0_&_not_a_=_1_)
assume A4: ( a = 0 or a = 1 ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( a = 0 or a = 1 ) by A4;
suppose a = 0 ; ::_thesis: contradiction
then (a |^ p) - 1 = 0 - 1 by A1, NEWTON:84;
hence contradiction by A2; ::_thesis: verum
end;
suppose a = 1 ; ::_thesis: contradiction
then (a |^ p) - 1 = 1 - 1 by NEWTON:10;
hence contradiction by A2, INT_2:def_4; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
assume a <= 1 ; ::_thesis: contradiction
hence contradiction by A3, NAT_1:25; ::_thesis: verum
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
let a, p be Nat; ::_thesis: ( p > 1 & (a |^ p) - 1 is Prime implies ( a = 2 & p is Prime ) )
assume that
A1: p > 1 and
A2: (a |^ p) - 1 is Prime ; ::_thesis: ( a = 2 & p is Prime )
now__::_thesis:_(_a_=_2_&_p_is_Prime_)
A3: a > 1 by A1, A2, Lm6;
then A4: a >= 1 + 1 by NAT_1:13;
p >= 1 + 1 by A1, NAT_1:13;
then a < a |^ p by A3, PREPOWER:13;
then A5: a - 1 < (a |^ p) - 1 by XREAL_1:9;
now__::_thesis:_not_a_>_2
assume A6: a > 2 ; ::_thesis: contradiction
then A7: a - 1 > 2 - 1 by XREAL_1:9;
A8: a - 1 is Element of NAT by A6, NAT_1:20;
a - 1 divides (a |^ p) - 1 by A1, A2, Lm6, Th27;
hence contradiction by A2, A5, A7, A8, NAT_4:12; ::_thesis: verum
end;
hence a = 2 by A4, XXREAL_0:1; ::_thesis: p is Prime
assume p is not Prime ; ::_thesis: contradiction
then consider n being Element of NAT such that
A9: n divides p and
A10: 1 < n and
A11: n < p by A1, NAT_4:12;
consider q being Nat such that
A12: p = n * q by A9, NAT_D:def_3;
1 + 1 <= n by A10, NAT_1:13;
then 2 < 2 |^ n by PREPOWER:13;
then A13: 2 + 1 <= 2 |^ n by NAT_1:13;
2 |^ n <= a |^ n by A4, PREPOWER:9;
then 2 + 1 <= a |^ n by A13, XXREAL_0:2;
then 2 < a |^ n by NAT_1:13;
then A14: 2 - 1 < (a |^ n) - 1 by XREAL_1:9;
a >= 0 + 1 by A1, A2, Lm6;
then A15: (a |^ n) - 1 is Element of NAT by NAT_1:21, PREPOWER:11;
a |^ n < a |^ p by A3, A11, PEPIN:66;
then A16: (a |^ n) - 1 < (a |^ p) - 1 by XREAL_1:9;
(a |^ n) - 1 divides ((a |^ n) |^ q) - 1 by A3, A10, Th27, PEPIN:25;
then (a |^ n) - 1 divides (a |^ p) - 1 by A12, NEWTON:9;
hence contradiction by A2, A16, A15, A14, NAT_4:12; ::_thesis: verum
end;
hence ( a = 2 & p is Prime ) ; ::_thesis: verum
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
let a be Integer; ::_thesis: for x, n being Nat holds (a |^ x) mod n = ((a mod n) |^ x) mod n
let x, n be Nat; ::_thesis: (a |^ x) mod n = ((a mod n) |^ x) mod n
defpred S1[ Nat] means (a |^ $1) mod n = ((a mod n) |^ $1) mod n;
A1: for x being Nat st S1[x] holds
S1[x + 1]
proof
let x be Nat; ::_thesis: ( S1[x] implies S1[x + 1] )
A2: (a |^ (x + 1)) mod n = ((a |^ x) * a) mod n by NEWTON:6
.= (((a |^ x) mod n) * (a mod n)) mod n by NAT_D:67 ;
A3: ((a mod n) |^ (x + 1)) mod n = (((a mod n) |^ x) * (a mod n)) mod n by NEWTON:6
.= ((((a mod n) |^ x) mod n) * ((a mod n) mod n)) mod n by NAT_D:67
.= ((((a mod n) |^ x) mod n) * (a mod n)) mod n by NAT_D:65 ;
assume (a |^ x) mod n = ((a mod n) |^ x) mod n ; ::_thesis: S1[x + 1]
hence S1[x + 1] by A2, A3; ::_thesis: verum
end;
a |^ 0 = 1 by NEWTON:4;
then A4: S1[ 0 ] by NEWTON:4;
for n being Nat holds S1[n] from NAT_1:sch_2(A4, A1);
hence (a |^ x) mod n = ((a mod n) |^ x) mod n ; ::_thesis: verum
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
let x, y, n be Integer; ::_thesis: ( x,n are_relative_prime & x,y are_congruent_mod n implies y,n are_relative_prime )
assume that
A1: x,n are_relative_prime and
A2: x,y are_congruent_mod n and
A3: not y,n are_relative_prime ; ::_thesis: contradiction
consider z being Integer such that
A4: n * z = x - y by A2, INT_1:def_5;
set gcdyn = y gcd n;
A5: y gcd n divides y by INT_2:21;
A6: y gcd n divides n by INT_2:21;
y gcd n divides n * z by INT_2:2, INT_2:21;
then y gcd n divides (n * z) + y by A5, WSIERP_1:4;
then y gcd n divides x gcd n by A4, A6, INT_2:22;
then y gcd n divides 1 by A1, INT_2:def_3;
then A7: ( y gcd n = 1 or y gcd n = - 1 ) by INT_2:13;
0 <= y gcd n ;
hence contradiction by A3, A7, INT_2:def_3; ::_thesis: verum
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
let a, x be Nat; ::_thesis: for p being Prime st a,p are_relative_prime & a,x * x are_congruent_mod p holds
x,p are_relative_prime
let p be Prime; ::_thesis: ( a,p are_relative_prime & a,x * x are_congruent_mod p implies x,p are_relative_prime )
assume that
A1: a,p are_relative_prime and
A2: a,x * x are_congruent_mod p ; ::_thesis: x,p are_relative_prime
assume not x,p are_relative_prime ; ::_thesis: contradiction
then x gcd p = p by PEPIN:2;
then p divides x by NAT_D:def_5;
then A3: p divides x * x by NAT_D:9;
x * x,p are_relative_prime by A1, A2, Th31;
then (x * x) gcd p = 1 by INT_2:def_3;
then p divides 1 by A3, NAT_D:def_5;
then p = 1 by INT_2:13;
hence contradiction by INT_2:def_4; ::_thesis: verum
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
let a, x be Integer; ::_thesis: for p being Prime st a,p are_relative_prime & a,x * x are_congruent_mod p holds
x,p are_relative_prime
let p be Prime; ::_thesis: ( a,p are_relative_prime & a,x * x are_congruent_mod p implies x,p are_relative_prime )
assume that
A1: a,p are_relative_prime and
A2: a,x * x are_congruent_mod p ; ::_thesis: x,p are_relative_prime
x * x,p are_relative_prime by A1, A2, Th31;
then A3: (x * x) gcd p = 1 by INT_2:def_3;
assume A4: not x,p are_relative_prime ; ::_thesis: contradiction
A5: x gcd p divides p by INT_2:21;
A6: x gcd p >= 0 ;
x gcd p divides x * x by INT_2:2, INT_2:21;
then ( x gcd p = 1 or x gcd p = - 1 ) by A3, A5, INT_2:13, INT_2:22;
hence contradiction by A4, A6, INT_2:def_3; ::_thesis: verum
end;
Lm7: for n being Nat
for a being Integer st n <> 0 holds
a mod n,a are_congruent_mod n
proof
let n be Nat; ::_thesis: for a being Integer st n <> 0 holds
a mod n,a are_congruent_mod n
let a be Integer; ::_thesis: ( n <> 0 implies a mod n,a are_congruent_mod n )
A1: (a mod n) mod n = a mod n by NAT_D:65;
assume n <> 0 ; ::_thesis: a mod n,a are_congruent_mod n
hence a mod n,a are_congruent_mod n by A1, NAT_D:64; ::_thesis: verum
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
let n be Nat; ::_thesis: for a being Integer st n <> 0 holds
ex an being Nat st an,a are_congruent_mod n
let a be Integer; ::_thesis: ( n <> 0 implies ex an being Nat st an,a are_congruent_mod n )
assume A1: n <> 0 ; ::_thesis: ex an being Nat st an,a are_congruent_mod n
reconsider an = a mod n as Element of NAT by INT_1:3, INT_1:57;
take an ; ::_thesis: an,a are_congruent_mod n
thus an,a are_congruent_mod n by A1, Lm7; ::_thesis: verum
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
let a, b, n, x be Nat; ::_thesis: ( a,b are_congruent_mod n & n <> 0 implies a |^ x,b |^ x are_congruent_mod n )
assume that
A1: a,b are_congruent_mod n and
A2: n <> 0 ; ::_thesis: a |^ x,b |^ x are_congruent_mod n
A3: (a |^ x) mod n = ((a mod n) |^ x) mod n by PEPIN:12;
(b |^ x) mod n = ((b mod n) |^ x) mod n by PEPIN:12;
then (b |^ x) mod n = ((a mod n) |^ x) mod n by A1, NAT_D:64;
hence a |^ x,b |^ x are_congruent_mod n by A2, A3, NAT_D:64; ::_thesis: verum
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
let a, b be Integer; ::_thesis: for n, x being Nat st a,b are_congruent_mod n & n <> 0 holds
a |^ x,b |^ x are_congruent_mod n
let n, x be Nat; ::_thesis: ( a,b are_congruent_mod n & n <> 0 implies a |^ x,b |^ x are_congruent_mod n )
assume that
A1: a,b are_congruent_mod n and
A2: n <> 0 ; ::_thesis: a |^ x,b |^ x are_congruent_mod n
consider an being Nat such that
A3: an,a are_congruent_mod n by A2, Lm8;
b mod n >= 0 by A2, NAT_D:62;
then b mod n is Element of NAT by INT_1:3;
then consider nb being Nat such that
A4: nb = b mod n ;
reconsider ai = an as Integer ;
A5: ai,b are_congruent_mod n by A1, A3, INT_1:15;
reconsider bi = nb as Integer ;
b mod n = (b mod n) mod n by NAT_D:65;
then b,bi are_congruent_mod n by A2, A4, NAT_D:64;
then an,nb are_congruent_mod n by A5, INT_1:15;
then an |^ x,nb |^ x are_congruent_mod n by A2, Lm9;
then A6: (an |^ x) mod n = (nb |^ x) mod n by NAT_D:64;
A7: (b |^ x) mod n = ((b mod n) |^ x) mod n by Th30;
A8: (a |^ x) mod n = ((a mod n) |^ x) mod n by Th30;
an mod n = a mod n by A3, NAT_D:64;
then ((a mod n) |^ x) mod n = ((b mod n) |^ x) mod n by A4, A6, PEPIN:12;
hence a |^ x,b |^ x are_congruent_mod n by A2, A8, A7, NAT_D:64; ::_thesis: verum
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
let a be Integer; ::_thesis: 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 )
let n be Prime; ::_thesis: ( not (a * a) mod n = 1 or a,1 are_congruent_mod n or a, - 1 are_congruent_mod n )
reconsider cLa = a mod n as Integer ;
n > 1 by INT_2:def_4;
then A1: 1 mod n = 1 by PEPIN:5;
assume A2: (a * a) mod n = 1 ; ::_thesis: ( a,1 are_congruent_mod n or a, - 1 are_congruent_mod n )
then (cLa * cLa) mod n = 1 by NAT_D:67;
then cLa * cLa,1 are_congruent_mod n by A1, NAT_D:64;
then n divides (cLa * cLa) - 1 by INT_2:15;
then A3: n divides (cLa + 1) * (cLa - 1) ;
0 = n * 0 ;
then A4: n divides 0 by INT_1:def_3;
A5: a mod n <> 0
proof
assume A6: a mod n = 0 ; ::_thesis: contradiction
(a * a) mod n = ((a mod n) * (a mod n)) mod n by NAT_D:67
.= 0 by A4, A6, INT_1:62 ;
hence contradiction by A2; ::_thesis: verum
end;
cLa >= 0 by NAT_D:62;
then 0 + 1 <= cLa by A5, INT_1:7;
then A7: cLa - 1 is Element of NAT by INT_1:5;
cLa mod n = a mod n by NAT_D:65;
then A8: a,cLa are_congruent_mod n by NAT_D:64;
a mod n >= 0 by NAT_D:62;
then cLa + 1 is Element of NAT by INT_1:3;
then ( n divides cLa - (- 1) or n divides cLa - 1 ) by A7, A3, NEWTON:80;
then ( cLa, - 1 are_congruent_mod n or cLa,1 are_congruent_mod n ) by INT_2:15;
hence ( a,1 are_congruent_mod n or a, - 1 are_congruent_mod n ) by A8, INT_1:15; ::_thesis: verum
end;
begin
theorem :: GR_CY_3:36
for p being Prime holds Z/Z* p = MultGroup (INT.Ring p)
proof
let p be Prime; ::_thesis: Z/Z* p = MultGroup (INT.Ring p)
A1: 0 in Segm p by NAT_1:44;
then A2: (Segm p) \ {0} = NonZero (INT.Ring p) by FUNCT_7:def_1
.= the carrier of (MultGroup (INT.Ring p)) by UNIROOTS:def_1 ;
A3: 1 < p by INT_2:def_4;
then A4: the multF of (Z/Z* p) = (multint p) || ((Segm p) \ {0}) by INT_7:def_2
.= the multF of (MultGroup (INT.Ring p)) by A2, UNIROOTS:def_1 ;
0 = In (0,(Segm p)) by A1, FUNCT_7:def_1;
then the carrier of (Z/Z* p) = NonZero (INT.Ring p) by A3, INT_7:def_2
.= the carrier of (MultGroup (INT.Ring p)) by UNIROOTS:def_1 ;
hence Z/Z* p = MultGroup (INT.Ring p) by A4; ::_thesis: verum
end;
registration
let F be commutative Skew-Field;
cluster MultGroup F -> commutative ;
coherence
MultGroup F is commutative
proof
let x, y be Element of (MultGroup F); :: according to GROUP_1:def_12 ::_thesis: x * y = y * x
x in the carrier of (MultGroup F) ;
then x in NonZero F by UNIROOTS:def_1;
then reconsider x1 = x as Element of F ;
y in the carrier of (MultGroup F) ;
then y in NonZero F by UNIROOTS:def_1;
then reconsider y1 = y as Element of F ;
x * y = x1 * y1 by UNIROOTS:16
.= y * x by UNIROOTS:16 ;
hence x * y = y * x ; ::_thesis: verum
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
let F be commutative Skew-Field; ::_thesis: for x being Element of (MultGroup F)
for x1 being Element of F st x = x1 holds
x " = x1 "
let h be Element of (MultGroup F); ::_thesis: for x1 being Element of F st h = x1 holds
h " = x1 "
let hp be Element of F; ::_thesis: ( h = hp implies h " = hp " )
assume A1: h = hp ; ::_thesis: h " = hp "
set hpd = hp " ;
h in the carrier of (MultGroup F) ;
then h in NonZero F by UNIROOTS:def_1;
then not h in {(0. F)} by XBOOLE_0:def_5;
then A2: h <> 0. F by TARSKI:def_1;
then hp * (hp ") = 1. F by A1, VECTSP_1:def_10;
then hp " <> 0. F by VECTSP_1:6;
then not hp " in {(0. F)} by TARSKI:def_1;
then hp " in NonZero F by XBOOLE_0:def_5;
then reconsider g = hp " as Element of (MultGroup F) by UNIROOTS:def_1;
A3: 1_ F = 1_ (MultGroup F) by UNIROOTS:17;
g * h = (hp ") * hp by A1, UNIROOTS:16
.= 1_ (MultGroup F) by A1, A2, A3, VECTSP_1:def_10 ;
hence h " = hp " by GROUP_1:def_5; ::_thesis: verum
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
let F be commutative Skew-Field; ::_thesis: 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) ) )
let G be Subgroup of MultGroup F; ::_thesis: 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) ) )
let n be Nat; ::_thesis: ( 0 < n implies 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) ) ) )
reconsider n0 = n as Element of NAT by ORDINAL1:def_12;
set f = (<%(0. F),(1_ F)%> `^ n0) - (1_. F);
A1: now__::_thesis:_for_x,_xn_being_Element_of_F
for_xz_being_Element_of_G_st_x_=_xz_&_xn_=_xz_|^_n_holds_
eval_(((<%(0._F),(1__F)%>_`^_n0)_-_(1_._F)),x)_=_xn_-_(1__F)
let x, xn be Element of F; ::_thesis: for xz being Element of G st x = xz & xn = xz |^ n holds
eval (((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x) = xn - (1_ F)
let xz be Element of G; ::_thesis: ( x = xz & xn = xz |^ n implies eval (((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x) = xn - (1_ F) )
assume that
A2: x = xz and
A3: xn = xz |^ n ; ::_thesis: eval (((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x) = xn - (1_ F)
the carrier of G c= the carrier of (MultGroup F) by GROUP_2:def_5;
then reconsider xxz = xz as Element of (MultGroup F) by TARSKI:def_3;
A4: xn = xxz |^ n0 by A3, GROUP_4:1
.= (power F) . (x,n0) by A2, UNIROOTS:29 ;
thus eval (((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x) = (eval ((<%(0. F),(1_ F)%> `^ n0),x)) - (eval ((1_. F),x)) by POLYNOM4:21
.= (eval ((<%(0. F),(1_ F)%> `^ n0),x)) - (1_ F) by POLYNOM4:18
.= ((power F) . ((eval (<%(0. F),(1_ F)%>,x)),n0)) - (1_ F) by POLYNOM5:22
.= xn - (1_ F) by A4, POLYNOM5:48 ; ::_thesis: verum
end;
assume 0 < n ; ::_thesis: 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) ) )
then A5: 0 + 1 < n + 1 by XREAL_1:8;
len (1_. F) = 1 by POLYNOM4:4;
then A6: len (- (1_. F)) = 1 by POLYNOM4:8;
len <%(0. F),(1_ F)%> = 2 by POLYNOM5:40;
then len (<%(0. F),(1_ F)%> `^ n0) = ((n * 2) - n) + 1 by POLYNOM5:23
.= n + 1 ;
then len ((<%(0. F),(1_ F)%> `^ n0) - (1_. F)) = max ((n + 1),1) by A5, A6, POLYNOM4:7
.= n + 1 by A5, XXREAL_0:def_10 ;
then deg ((<%(0. F),(1_ F)%> `^ n0) - (1_. F)) = n ;
hence 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) ) ) by A1; ::_thesis: verum
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
let F be commutative Skew-Field; ::_thesis: 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})
let G be Subgroup of MultGroup F; ::_thesis: 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})
let a, b be Element of G; ::_thesis: for n being Nat st G is finite & 0 < n & ord a = n & b |^ n = 1_ G holds
b is Element of (gr {a})
let n be Nat; ::_thesis: ( G is finite & 0 < n & ord a = n & b |^ n = 1_ G implies b is Element of (gr {a}) )
assume that
A1: G is finite and
A2: 0 < n and
A3: ord a = n and
A4: b |^ n = 1_ G ; ::_thesis: b is Element of (gr {a})
consider f being Polynomial of F such that
A5: deg f = n and
A6: 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) by A2, Lm10;
assume A7: b is not Element of (gr {a}) ; ::_thesis: contradiction
A8: the carrier of G c= the carrier of (MultGroup F) by GROUP_2:def_5;
A9: for x being Element of G st x |^ n = 1_ G holds
x in Roots f
proof
let x1 be Element of G; ::_thesis: ( x1 |^ n = 1_ G implies x1 in Roots f )
A10: 1_ F = 1_ (MultGroup F) by UNIROOTS:17;
x1 in the carrier of G ;
then x1 in the carrier of (MultGroup F) by A8;
then x1 in NonZero F by UNIROOTS:def_1;
then reconsider x3 = x1 as Element of F ;
assume A11: x1 |^ n = 1_ G ; ::_thesis: x1 in Roots f
then A12: x1 |^ n = 1. F by A10, GROUP_2:44;
reconsider x2 = x1 |^ n as Element of F by A11, A10, GROUP_2:44;
eval (f,x3) = x2 - (1. F) by A6
.= 0. F by A12, RLVECT_1:15 ;
then x3 is_a_root_of f by POLYNOM5:def_6;
hence x1 in Roots f by POLYNOM5:def_9; ::_thesis: verum
end;
A13: the carrier of (gr {a}) c= Roots f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (gr {a}) or x in Roots f )
assume A14: x in the carrier of (gr {a}) ; ::_thesis: x in Roots f
the carrier of (gr {a}) c= the carrier of G by GROUP_2:def_5;
then reconsider x1 = x as Element of G by A14;
x1 in gr {a} by A14, STRUCT_0:def_5;
then consider j being Integer such that
A15: x1 = a |^ j by GR_CY_1:5;
x1 |^ n = a |^ (j * n) by A15, GROUP_1:35
.= (a |^ n) |^ j by GROUP_1:35
.= (1_ G) |^ j by A3, GROUP_1:41
.= 1_ G by GROUP_1:31 ;
hence x in Roots f by A9; ::_thesis: verum
end;
b in Roots f by A4, A9;
then {b} c= Roots f by ZFMISC_1:31;
then A16: the carrier of (gr {a}) \/ {b} c= Roots f by A13, XBOOLE_1:8;
reconsider gra = gr {a} as finite Group by A1;
A17: n = card gra by A1, A3, GR_CY_1:7
.= card the carrier of (gr {a}) ;
then reconsider XX = the carrier of (gr {a}) as finite set ;
consider m, n0 being Element of NAT such that
A18: n0 = deg f and
A19: m = card (Roots f) and
A20: m <= n0 by A5, INT_7:27;
card ( the carrier of (gr {a}) \/ {b}) = card (XX \/ {b})
.= n0 + 1 by A7, A5, A18, A17, CARD_2:41 ;
then card (n0 + 1) c= card m by A19, A16, CARD_1:11;
then n0 + 1 <= m by NAT_1:40;
hence contradiction by A20, NAT_1:16, XXREAL_0:2; ::_thesis: verum
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
let F be commutative Skew-Field; ::_thesis: for G being finite Subgroup of MultGroup F holds G is cyclic Group
let G be finite Subgroup of MultGroup F; ::_thesis: G is cyclic Group
set a = the Element of G;
defpred S1[ Nat, Element of G, Element of G] means ord $2 < ord $3;
assume G is not cyclic Group ; ::_thesis: contradiction
then A1: for x being Element of G holds not ord x = card G by GR_CY_1:19;
A2: for x being Element of G holds ord x < card G
proof
let x be Element of G; ::_thesis: ord x < card G
ord x <= card G by GR_CY_1:8, NAT_D:7;
hence ord x < card G by A1, XXREAL_0:1; ::_thesis: verum
end;
A3: for n being Element of NAT
for x being Element of G ex y being Element of G st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Element of G ex y being Element of G st S1[n,x,y]
let x be Element of G; ::_thesis: ex y being Element of G st S1[n,x,y]
set n = ord x;
ord x < card G by A2;
then A4: card (gr {x}) <> card G by GR_CY_1:7;
the carrier of (gr {x}) c= the carrier of G by GROUP_2:def_5;
then the carrier of (gr {x}) c< the carrier of G by A4, XBOOLE_0:def_8;
then the carrier of G \ the carrier of (gr {x}) <> {} by XBOOLE_1:105;
then consider z being set such that
A5: z in the carrier of G \ the carrier of (gr {x}) by XBOOLE_0:def_1;
reconsider z = z as Element of G by A5;
set m = ord z;
set l = (ord z) lcm (ord x);
ord x divides (ord z) lcm (ord x) by INT_2:def_1;
then consider j being Integer such that
A6: (ord z) lcm (ord x) = (ord x) * j by INT_1:def_3;
A7: 1 <= card (gr {x}) by GROUP_1:45;
then A8: 1 <= ord x by GR_CY_1:7;
then ((ord z) lcm (ord x)) / (ord x) = j by A6, XCMPLX_1:89;
then A9: j is Element of NAT by INT_1:3;
not ord z divides ord x
proof
assume ord z divides ord x ; ::_thesis: contradiction
then consider j being Integer such that
A10: ord x = (ord z) * j by INT_1:def_3;
A11: 0 < ord x by A7, GR_CY_1:7;
z |^ (ord x) = (z |^ (ord z)) |^ j by A10, GROUP_1:35
.= (1_ G) |^ j by GROUP_1:41
.= 1_ G by GROUP_1:31 ;
then z is Element of (gr {x}) by A11, Lm11;
hence contradiction by A5, XBOOLE_0:def_5; ::_thesis: verum
end;
then A12: ord x <> (ord z) lcm (ord x) by INT_2:def_1;
A13: 1 <= card (gr {z}) by GROUP_1:45;
then A14: ord z <> 0 by GR_CY_1:7;
1 <= ord z by A13, GR_CY_1:7;
then consider m0, n0 being Element of NAT such that
A15: (ord z) lcm (ord x) = n0 * m0 and
A16: n0 gcd m0 = 1 and
A17: n0 divides ord x and
A18: m0 divides ord z and
A19: n0 <> 0 and
A20: m0 <> 0 by A8, INT_7:17;
ex u being Integer st ord z = m0 * u by A18, INT_1:def_3;
then (ord z) / m0 is Integer by A20, XCMPLX_1:89;
then reconsider d2 = (ord z) / m0 as Element of NAT by INT_1:3;
ex j being Integer st ord x = n0 * j by A17, INT_1:def_3;
then (ord x) / n0 is Integer by A19, XCMPLX_1:89;
then reconsider d1 = (ord x) / n0 as Element of NAT by INT_1:3;
set y = (x |^ d1) * (z |^ d2);
ord z = d2 * m0 by A20, XCMPLX_1:87;
then A21: ord (z |^ d2) = m0 by INT_7:30;
ord x <> 0 by A7, GR_CY_1:7;
then j <> 0 by A14, A6, INT_2:4;
then (ord x) * 1 <= (ord x) * j by A9, NAT_1:14, XREAL_1:64;
then A22: ord x < (ord z) lcm (ord x) by A12, A6, XXREAL_0:1;
ord x = d1 * n0 by A19, XCMPLX_1:87;
then ord (x |^ d1) = n0 by INT_7:30;
then ord ((x |^ d1) * (z |^ d2)) = m0 * n0 by A16, A21, INT_7:25;
hence ex y being Element of G st ord x < ord y by A15, A22; ::_thesis: verum
end;
consider f being Function of NAT, the carrier of G such that
A23: ( f . 0 = the Element of G & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A3);
deffunc H1( Element of NAT ) -> Element of NAT = ord (f . $1);
consider g being Function of NAT,NAT such that
A24: for k being Element of NAT holds g . k = H1(k) from FUNCT_2:sch_4();
A25: now__::_thesis:_for_k_being_Element_of_NAT_holds_g_._k_<_g_._(k_+_1)
let k be Element of NAT ; ::_thesis: g . k < g . (k + 1)
A26: g . (k + 1) = ord (f . (k + 1)) by A24;
g . k = ord (f . k) by A24;
hence g . k < g . (k + 1) by A23, A26; ::_thesis: verum
end;
A27: for k, m being Element of NAT holds g . k < g . ((k + 1) + m)
proof
let k be Element of NAT ; ::_thesis: for m being Element of NAT holds g . k < g . ((k + 1) + m)
defpred S2[ Element of NAT ] means g . k < g . ((k + 1) + $1);
A28: now__::_thesis:_for_m_being_Element_of_NAT_st_S2[m]_holds_
S2[m_+_1]
let m be Element of NAT ; ::_thesis: ( S2[m] implies S2[m + 1] )
assume A29: S2[m] ; ::_thesis: S2[m + 1]
g . ((k + 1) + m) < g . (((k + 1) + m) + 1) by A25;
hence S2[m + 1] by A29, XXREAL_0:2; ::_thesis: verum
end;
A30: S2[ 0 ] by A25;
for m being Element of NAT holds S2[m] from NAT_1:sch_1(A30, A28);
hence for m being Element of NAT holds g . k < g . ((k + 1) + m) ; ::_thesis: verum
end;
A31: for k, m being Element of NAT st k < m holds
g . k < g . m
proof
let k, m be Element of NAT ; ::_thesis: ( k < m implies g . k < g . m )
assume A32: k < m ; ::_thesis: g . k < g . m
then m - k is Element of NAT by INT_1:5;
then reconsider mk = m - k as Nat ;
m - k <> 0 by A32;
then consider n0 being Nat such that
A33: mk = n0 + 1 by NAT_1:6;
reconsider n = n0 as Element of NAT by ORDINAL1:def_12;
m = (k + 1) + n by A33;
hence g . k < g . m by A27; ::_thesis: verum
end;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_NAT_&_x2_in_NAT_&_g_._x1_=_g_._x2_holds_
x2_=_x1
let x1, x2 be set ; ::_thesis: ( x1 in NAT & x2 in NAT & g . x1 = g . x2 implies x2 = x1 )
assume that
A34: x1 in NAT and
A35: x2 in NAT and
A36: g . x1 = g . x2 ; ::_thesis: x2 = x1
reconsider xx1 = x1, xx2 = x2 as Element of NAT by A34, A35;
A37: xx2 <= xx1 by A31, A36;
xx1 <= xx2 by A31, A36;
hence x2 = x1 by A37, XXREAL_0:1; ::_thesis: verum
end;
then g is one-to-one by FUNCT_2:19;
then dom g, rng g are_equipotent by WELLORD2:def_4;
then card (dom g) = card (rng g) by CARD_1:5;
then A38: card (rng g) = card NAT by FUNCT_2:def_1;
rng g c= Segm (card G)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in Segm (card G) )
assume y in rng g ; ::_thesis: y in Segm (card G)
then consider x being set such that
A39: x in NAT and
A40: y = g . x by FUNCT_2:11;
reconsider x = x as Element of NAT by A39;
reconsider gg = g . x as Element of NAT ;
g . x = ord (f . x) by A24;
then gg < card G by A2;
hence y in Segm (card G) by A40, NAT_1:44; ::_thesis: verum
end;
hence contradiction by A38; ::_thesis: verum
end;