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