gr_cy_3.miz



    begin

    theorem :: GR_CY_3:1

    

     Th1: for p,q be Prime, k be Nat st k divides (p * q) holds k = 1 or k = p or k = q or k = (p * q)

    proof

      let p,q be Prime, k be Nat;

      assume

       A1: k divides (p * q);

      per cases by PEPIN: 2;

        suppose (k,p) are_coprime ;

        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;

      end;

        suppose (k gcd p) = p;

        then p divides k by NAT_D:def 5;

        then

        consider l be Nat such that

         A2: k = (p * l) by NAT_D:def 3;

        consider m be 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;

      end;

    end;

    definition

      let p be Nat;

      :: GR_CY_3:def1

      attr p is Safe means

      : Def1: ex sgp be Prime st ((2 * sgp) + 1) = p;

    end

    registration

      cluster Safe for Prime;

      existence

      proof

        reconsider p = 5 as Prime by PEPIN: 59;

        reconsider sgp = 2 as Prime by INT_2: 28;

        take p;

        p = ((2 * sgp) + 1);

        hence thesis;

      end;

    end

    theorem :: GR_CY_3:2

    

     Th2: for p be Safe Prime holds p >= 5

    proof

      let p be Safe Prime;

      consider q be 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 thesis by A1;

    end;

    theorem :: GR_CY_3:3

    

     Th3: for p be Safe Prime holds (p mod 2) = 1

    proof

      let p be Safe Prime;

      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 thesis by NAT_2: 22;

    end;

    theorem :: GR_CY_3:4

    

     Th4: for p be Safe Prime st p <> 7 holds (p mod 3) = 2

    proof

      let p be Safe Prime;

      set k = (p mod 3);

      consider q be Prime such that

       A1: ((2 * q) + 1) = p by Def1;

      assume

       A2: p <> 7;

       A3:

      now

        assume

         A4: k = 0 or k = 1;

        now

          per cases by A4;

            suppose k = 0 ;

            then 3 divides p by INT_1: 62;

            then 3 = p by INT_2:def 4;

            hence contradiction by Th2;

          end;

            suppose

             A5: k = 1;

            (2,3) are_coprime 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;

          end;

        end;

        hence contradiction;

      end;

      k < (2 + 1) by NAT_D: 62;

      then k <= ( 0 + 2) by NAT_1: 13;

      then k = 0 or ... or k = 2;

      hence thesis by A3;

    end;

    theorem :: GR_CY_3:5

    

     Th5: for p be Safe Prime st p <> 5 holds (p mod 4) = 3

    proof

      let p be Safe Prime;

      set k = (p mod 4);

      consider q be Prime such that

       A1: ((2 * q) + 1) = p by Def1;

      assume

       A2: p <> 5;

       A3:

      now

        assume

         A4: k = 0 or k = 1 or k = 2;

        now

          per cases by A4;

            suppose k = 0 ;

            then 4 divides p by INT_1: 62;

            hence contradiction by INT_2: 29, INT_2:def 4;

          end;

            suppose k = 1;

            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;

          end;

            suppose k = 2;

            

            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;

          end;

        end;

        hence contradiction;

      end;

      k < (3 + 1) by NAT_D: 62;

      then k <= ( 0 + 3) by NAT_1: 13;

      then k = 0 or ... or k = 3;

      hence thesis by A3;

    end;

    theorem :: GR_CY_3:6

    for p be Safe Prime st p <> 7 holds (p mod 6) = 5

    proof

      let p be Safe Prime;

      assume

       A1: p <> 7;

      

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

    end;

    theorem :: GR_CY_3:7

    for p be Safe Prime st p > 7 holds (p mod 12) = 11

    proof

      let p be Safe Prime;

      assume

       A1: p > 7;

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

    end;

    theorem :: GR_CY_3:8

    for p be Safe Prime st p > 5 holds (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;

      set k = (p mod 8);

      consider q be Prime such that

       A2: ((2 * q) + 1) = p by Def1;

      assume

       A3: p > 5;

       A4:

      now

        assume

         A5: (k = 0 or ... or k = 2) or (k = 4 or ... or k = 6);

        now

          per cases by A5;

            suppose k = 0 ;

            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;

          end;

            suppose k = 1;

            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;

          end;

            suppose k = 2;

            

            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;

          end;

            suppose k = 4;

            

            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;

          end;

            suppose k = 5;

            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;

          end;

            suppose k = 6;

            

            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;

          end;

        end;

        hence contradiction;

      end;

      k < (7 + 1) by NAT_D: 62;

      then k <= ( 0 + 7) by NAT_1: 13;

      then k = 0 or ... or k = 7;

      hence thesis by A4;

    end;

    definition

      let p be Nat;

      :: GR_CY_3:def2

      attr p is Sophie_Germain means

      : Def2: ((2 * p) + 1) is Prime;

    end

    registration

      cluster Sophie_Germain for Prime;

      existence

      proof

        reconsider p = 5 as Prime by PEPIN: 59;

        reconsider sgp = 2 as Prime by INT_2: 28;

        take sgp;

        p = ((2 * sgp) + 1);

        hence thesis;

      end;

    end

    theorem :: GR_CY_3:9

    for p be Sophie_Germain Prime st p > 2 holds (p mod 4) = 1 or (p mod 4) = 3

    proof

      let p be Sophie_Germain Prime;

      set k = (p mod 4);

      assume

       A1: p > 2;

       A2:

      now

        assume

         A3: k = 0 or k = 2;

        now

          per cases by A3;

            suppose k = 0 ;

            then 4 divides p by INT_1: 62;

            hence contradiction by INT_2: 29, INT_2:def 4;

          end;

            suppose k = 2;

            

            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;

          end;

        end;

        hence contradiction;

      end;

      k < (3 + 1) by NAT_D: 62;

      then k <= ( 0 + 3) by NAT_1: 13;

      then k = 0 or ... or k = 3;

      hence thesis by A2;

    end;

    theorem :: GR_CY_3:10

    

     Th10: for p be Safe Prime holds ex q be Sophie_Germain Prime st p = ((2 * q) + 1)

    proof

      let p be Safe Prime;

      consider q be Prime such that

       A1: ((2 * q) + 1) = p by Def1;

      q is Sophie_Germain Prime by A1, Def2;

      hence thesis by A1;

    end;

    

     Lm1: for p be Nat st p > 2 holds ((2 * p) + 1) > 5

    proof

      let p be Nat;

      assume p > 2;

      then (2 * p) > (2 * 2) by XREAL_1: 68;

      then ((2 * p) + 1) > (4 + 1) by XREAL_1: 8;

      hence thesis;

    end;

    theorem :: GR_CY_3:11

    

     Th11: for p be Safe Prime holds ex q be Sophie_Germain Prime st ( Euler p) = (2 * q)

    proof

      let p be Safe Prime;

      

       A1: ( Euler p) = (p - 1) by EULER_1: 20;

      ex q be Sophie_Germain Prime st p = ((2 * q) + 1) by Th10;

      hence thesis by A1;

    end;

    theorem :: GR_CY_3:12

    for p1,p2 be Safe Prime, N be Nat st p1 <> p2 & N = (p1 * p2) holds ex q1,q2 be Sophie_Germain Prime st ( Euler N) = ((4 * q1) * q2)

    proof

      let p1,p2 be Safe Prime, N be Nat;

      assume that

       A1: p1 <> p2 and

       A2: N = (p1 * p2);

      

       A3: p2 > 1 by INT_2:def 4;

      consider q2 be Sophie_Germain Prime such that

       A4: ( Euler p2) = (2 * q2) by Th11;

      consider q1 be 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 thesis;

    end;

    theorem :: GR_CY_3:13

    

     Th13: for p be Safe Prime holds ex q be Sophie_Germain Prime st ( card ( Z/Z* p)) = (2 * q)

    proof

      let p be Safe Prime;

      consider q be Sophie_Germain Prime such that

       A1: ((2 * q) + 1) = p by Th10;

      (p - 1) = (2 * q) by A1;

      hence thesis by INT_7: 23;

    end;

    theorem :: GR_CY_3:14

    

     Th14: for G be cyclic finite Group, n,m be Nat st ( card G) = (n * m) holds ex a be Element of G st ( ord a) = n & ( gr {a}) is strict Subgroup of G

    proof

      let G be cyclic finite Group;

      let n,m be Nat;

      consider g be 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);

      then ( ord (g |^ m)) = n by A1, A2, A3, INT_7: 30;

      then

      consider a be Element of G such that

       A4: ( ord a) = n;

      take a;

      thus thesis by A4;

    end;

    theorem :: GR_CY_3:15

    for p be Safe Prime holds ex q be Sophie_Germain Prime, H1,H2,Hq,H2q be strict Subgroup of ( Z/Z* p) st ( card H1) = 1 & ( card H2) = 2 & ( card Hq) = q & ( card H2q) = (2 * q) & for H be strict Subgroup of ( Z/Z* p) holds H = H1 or H = H2 or H = Hq or H = H2q

    proof

      let p be Safe Prime;

      consider q be 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 be 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 be 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 be 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 be 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 be strict Subgroup of ( Z/Z* p) such that

       A8: ( card H2) = 2 and

       A9: ( card Hq) = q by A5;

      take q, H1, H2, Hq, H2q;

      now

        let H be strict Subgroup of ( Z/Z* p);

        consider G1 be strict Subgroup of ( Z/Z* p) such that ( card G1) = ( card H) and

         A10: for G2 be 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

          per cases by A1, Th1, GROUP_2: 148, INT_2: 28;

            suppose ( card H) = 1;

            hence H = H1 or H = H2 or H = Hq or H = H2q by A6, A10, A11;

          end;

            suppose ( card H) = 2;

            hence H = H1 or H = H2 or H = Hq or H = H2q by A8, A10, A11;

          end;

            suppose ( card H) = q;

            hence H = H1 or H = H2 or H = Hq or H = H2q by A9, A10, A11;

          end;

            suppose ( card H) = (2 * q);

            hence H = H1 or H = H2 or H = Hq or H = H2q by A7, A10, A11;

          end;

        end;

        hence H = H1 or H = H2 or H = Hq or H = H2q;

      end;

      hence thesis by A7, A8, A9, A6;

    end;

    definition

      let n be Nat;

      :: GR_CY_3:def3

      func Mersenne (n) -> Nat equals ((2 |^ n) - 1);

      correctness by NAT_1: 21, PREPOWER: 11;

    end

    

     Lm2: (2 |^ 2) = 4

    proof

      (2 |^ 2) = (2 |^ (1 + 1))

      .= ((2 |^ 1) * 2) by NEWTON: 6

      .= (2 * 2);

      hence thesis;

    end;

    

     Lm3: (2 |^ 3) = 8

    proof

      (2 |^ 3) = (2 |^ (2 + 1))

      .= (4 * 2) by Lm2, NEWTON: 6;

      hence thesis;

    end;

    

     Lm4: (2 |^ 4) = 16

    proof

      (2 |^ 4) = (2 |^ (2 + 2))

      .= (4 * 4) by Lm2, NEWTON: 8;

      hence thesis;

    end;

    

     Lm5: (2 |^ 8) = 256

    proof

      (2 |^ 8) = (2 |^ (4 + 4))

      .= (16 * 16) by Lm4, NEWTON: 8;

      hence thesis;

    end;

    theorem :: GR_CY_3:16

    ( Mersenne 0 ) = 0

    proof

      

      thus ( Mersenne 0 ) = (1 - 1) by NEWTON: 4

      .= 0 ;

    end;

    theorem :: GR_CY_3:17

    ( Mersenne 1) = 1;

    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;

    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;

    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;

    end;

    theorem :: GR_CY_3:23

    for p be Prime st p <> 2 holds (( Mersenne p) mod (2 * p)) = 1

    proof

      let p be Prime;

      assume

       A1: p <> 2;

      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 thesis by A2, PEPIN: 5;

    end;

    theorem :: GR_CY_3:24

    for p be Prime st p <> 2 holds (( Mersenne p) mod 8) = 7

    proof

      let p be Prime;

      

       A1: p > 1 by INT_2:def 4;

      then

       A2: p >= (1 + 1) by NAT_1: 13;

      assume p <> 2;

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

    end;

    theorem :: GR_CY_3:25

    for p be Sophie_Germain Prime st p > 2 & (p mod 4) = 3 holds ex q be Safe Prime st q divides ( Mersenne p)

    proof

      let p be Sophie_Germain Prime;

      assume that

       A1: p > 2 and

       A2: (p mod 4) = 3;

      set q = ((2 * p) + 1);

      

       A3: q is Safe Prime by Def1, Def2;

      q > 5 by A1, Lm1;

      then

       A4: q > (5 - 3) by XREAL_1: 51;

      then (2,q) are_coprime by A3, INT_2: 28, INT_2: 30;

      then

       A5: (2 gcd q) = 1 by INT_2:def 3;

      p = (((p div 4) * 4) + 3) by A2, INT_1: 59;

      then q = (((p div 4) * 8) + 7);

      

      then (q mod 8) = (7 mod 8) by NAT_D: 21

      .= 7 by NAT_D: 24;

      then 2 is_quadratic_residue_mod q by A3, A4, INT_5: 43;

      then (((2 |^ ((((2 * p) + 1) -' 1) div 2)) - 1) mod q) = 0 by A3, A4, A5, INT_5: 20;

      then (((2 |^ ((2 * p) div 2)) - 1) mod q) = 0 by NAT_D: 34;

      then (((2 |^ p) - 1) mod q) = 0 by NAT_D: 18;

      then q divides ((2 |^ p) - 1) by INT_1: 62;

      hence thesis by A3;

    end;

    theorem :: GR_CY_3:26

    for p be Sophie_Germain Prime st p > 2 & (p mod 4) = 1 holds ex q be Safe Prime st (( Mersenne p) mod q) = (q - 2)

    proof

      let p be Sophie_Germain Prime;

      assume that

       A1: p > 2 and

       A2: (p mod 4) = 1;

      set q = ((2 * p) + 1);

      

       A3: q is Safe Prime by Def1, Def2;

      

       A4: q > 5 by A1, Lm1;

      then

       A5: q > (5 - 3) by XREAL_1: 51;

      then (2,q) are_coprime by A3, INT_2: 28, INT_2: 30;

      then

       A6: (2 gcd q) = 1 by INT_2:def 3;

      p = (((p div 4) * 4) + 1) by A2, INT_1: 59;

      then q = (((p div 4) * 8) + 3);

      

      then (q mod 8) = (3 mod 8) by NAT_D: 21

      .= 3 by NAT_D: 24;

      then not 2 is_quadratic_residue_mod q by A3, A5, INT_5: 44;

      then ((2 |^ ((((2 * p) + 1) -' 1) div 2)) mod q) = (q - 1) by A3, A5, A6, INT_5: 19;

      then

       A7: ((2 |^ ((2 * p) div 2)) mod q) = (q - 1) by NAT_D: 34;

      

       A8: q > (5 - 4) by A4, XREAL_1: 51;

      then q >= (1 + 1) by NAT_1: 13;

      then

       A9: (q - 2) is Nat by NAT_1: 21;

      (( Mersenne p) mod q) = ((((2 |^ p) mod q) - (1 mod q)) mod q) by INT_6: 7

      .= (((q - 1) - (1 mod q)) mod q) by A7, NAT_D: 18

      .= (((q - 1) - 1) mod q) by A8, PEPIN: 5

      .= (q - 2) by A9, NAT_D: 24, XREAL_1: 44;

      hence thesis by A3;

    end;

    theorem :: GR_CY_3:27

    

     Th27: for a,n be Nat st a > 1 holds (a - 1) divides ((a |^ n) - 1)

    proof

      let a,n be Nat;

      

       A1: ((2 |^ n) - 1) is Nat by NAT_1: 21, PREPOWER: 11;

      assume a > 1;

      then

       A2: a >= (1 + 1) by NAT_1: 13;

      per cases by A2, XXREAL_0: 1;

        suppose

         A3: a = 2;

        then (((a |^ n) - 1) mod (a - 1)) = 0 by A1, RADIX_2: 1;

        hence thesis by A3, INT_1: 62;

      end;

        suppose

         A4: a > 2;

        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 thesis by A5, A6, INT_1: 62;

      end;

    end;

    

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

    proof

      let a,p be Nat;

      assume that

       A1: p > 1 and

       A2: ((a |^ p) - 1) is Prime;

       A3:

      now

        assume

         A4: a = 0 or a = 1;

        now

          per cases by A4;

            suppose a = 0 ;

            then ((a |^ p) - 1) = ( 0 - 1) by A1, NEWTON: 84;

            hence contradiction by A2;

          end;

            suppose a = 1;

            then ((a |^ p) - 1) = (1 - 1);

            hence contradiction by A2, INT_2:def 4;

          end;

        end;

        hence contradiction;

      end;

      assume a <= 1;

      hence contradiction by A3, NAT_1: 25;

    end;

    theorem :: GR_CY_3:28

    

     Th28: for a,p be Nat st p > 1 & ((a |^ p) - 1) is Prime holds a = 2 & p is Prime

    proof

      let a,p be Nat;

      assume that

       A1: p > 1 and

       A2: ((a |^ p) - 1) is Prime;

      now

        

         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

          assume

           A6: a > 2;

          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;

        end;

        hence a = 2 by A4, XXREAL_0: 1;

        assume not p is Prime;

        then

        consider n be Element of NAT such that

         A9: n divides p and

         A10: 1 < n and

         A11: n < p by A1, NAT_4: 12;

        consider q be 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;

      end;

      hence thesis;

    end;

    theorem :: GR_CY_3:29

    for p be Nat st p > 1 & ( Mersenne p) is Prime holds p is Prime by Th28;

    theorem :: GR_CY_3:30

    

     Th30: for a be Integer, x,n be Nat holds ((a |^ x) mod n) = (((a mod n) |^ x) mod n)

    proof

      let a be Integer;

      let x,n be Nat;

      defpred P[ Nat] means ((a |^ $1) mod n) = (((a mod n) |^ $1) mod n);

      

       A1: for x be Nat st P[x] holds P[(x + 1)]

      proof

        let x be Nat;

        

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

        hence thesis by A2, A3;

      end;

      (a |^ 0 ) = 1 by NEWTON: 4;

      then

       A4: P[ 0 ] by NEWTON: 4;

      for n be Nat holds P[n] from NAT_1:sch 2( A4, A1);

      hence thesis;

    end;

    theorem :: GR_CY_3:31

    

     Th31: for x,y,n be Integer st (x,n) are_coprime & (x,y) are_congruent_mod n holds (y,n) are_coprime

    proof

      let x,y,n be Integer;

      assume that

       A1: (x,n) are_coprime and

       A2: (x,y) are_congruent_mod n and

       A3: not (y,n) are_coprime ;

      consider z be Integer such that

       A4: (n * z) = (x - y) by A2, INT_1:def 5;

      set gcdyn = (y gcd n);

      

       A5: gcdyn divides y by INT_2: 21;

      

       A6: gcdyn divides n by INT_2: 21;

      gcdyn divides (n * z) by INT_2: 2, INT_2: 21;

      then gcdyn divides ((n * z) + y) by A5, WSIERP_1: 4;

      then gcdyn divides (x gcd n) by A4, A6, INT_2: 22;

      then gcdyn divides 1 by A1, INT_2:def 3;

      then

       A7: gcdyn = 1 or gcdyn = ( - 1) by INT_2: 13;

       0 <= gcdyn;

      hence contradiction by A3, A7, INT_2:def 3;

    end;

    theorem :: GR_CY_3:32

    for a,x be Nat, p be Prime st (a,p) are_coprime & (a,(x * x)) are_congruent_mod p holds (x,p) are_coprime

    proof

      let a,x be Nat;

      let p be Prime;

      assume that

       A1: (a,p) are_coprime and

       A2: (a,(x * x)) are_congruent_mod p;

      assume not (x,p) are_coprime ;

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

    end;

    theorem :: GR_CY_3:33

    for a,x be Integer, p be Prime st (a,p) are_coprime & (a,(x * x)) are_congruent_mod p holds (x,p) are_coprime

    proof

      let a,x be Integer;

      let p be Prime;

      assume that

       A1: (a,p) are_coprime and

       A2: (a,(x * x)) are_congruent_mod p;

      ((x * x),p) are_coprime by A1, A2, Th31;

      then

       A3: ((x * x) gcd p) = 1 by INT_2:def 3;

      assume

       A4: not (x,p) are_coprime ;

      

       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;

    end;

    

     Lm7: for n be Nat, a be Integer st n <> 0 holds ((a mod n),a) are_congruent_mod n

    proof

      let n be Nat;

      let a be Integer;

      

       A1: ((a mod n) mod n) = (a mod n) by NAT_D: 65;

      assume n <> 0 ;

      hence thesis by A1, NAT_D: 64;

    end;

    

     Lm8: for n be Nat, a be Integer st n <> 0 holds ex an be Nat st (an,a) are_congruent_mod n

    proof

      let n be Nat;

      let a be Integer;

      assume

       A1: n <> 0 ;

      reconsider an = (a mod n) as Element of NAT by INT_1: 3, INT_1: 57;

      take an;

      thus thesis by A1, Lm7;

    end;

    

     Lm9: for a,b,n,x be 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;

      assume that

       A1: (a,b) are_congruent_mod n and

       A2: n <> 0 ;

      

       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 thesis by A2, A3, NAT_D: 64;

    end;

    theorem :: GR_CY_3:34

    for a,b be Integer, n,x be 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;

      let n,x be Nat;

      assume that

       A1: (a,b) are_congruent_mod n and

       A2: n <> 0 ;

      consider an be 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 be 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 thesis by A2, A8, A7, NAT_D: 64;

    end;

    theorem :: GR_CY_3:35

    for a be Integer, n be Prime st ((a * a) mod n) = 1 holds (a,1) are_congruent_mod n or (a,( - 1)) are_congruent_mod n

    proof

      let a be Integer;

      let n be Prime;

      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;

      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 ;

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

      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 thesis by A8, INT_1: 15;

    end;

    begin

    theorem :: GR_CY_3:36

    for p be Prime holds ( Z/Z* p) = ( MultGroup ( INT.Ring p))

    proof

      let p be Prime;

      

       A1: 0 in ( Segm p) by NAT_1: 44;

      

      then

       A2: (( Segm p) \ { 0 }) = ( NonZero ( INT.Ring p)) by SUBSET_1:def 8

      .= 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, SUBSET_1:def 8;

      

      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;

    end;

    registration

      let F be commutative Skew-Field;

      cluster ( MultGroup F) -> commutative;

      coherence

      proof

        let x,y be Element of ( MultGroup F);

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

      end;

    end

    theorem :: GR_CY_3:37

    for F be commutative Skew-Field, x be Element of ( MultGroup F), x1 be Element of F st x = x1 holds (x " ) = (x1 " )

    proof

      let F be commutative Skew-Field, h be Element of ( MultGroup F), hp be Element of F;

      assume

       A1: 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 * hpd) = ( 1. F) by A1, VECTSP_1:def 10;

      then hpd <> ( 0. F);

      then not hpd in {( 0. F)} by TARSKI:def 1;

      then hpd in ( NonZero F) by XBOOLE_0:def 5;

      then

      reconsider g = hpd as Element of ( MultGroup F) by UNIROOTS:def 1;

      

       A3: ( 1_ F) = ( 1_ ( MultGroup F)) by UNIROOTS: 17;

      (g * h) = (hpd * hp) by A1, UNIROOTS: 16

      .= ( 1_ ( MultGroup F)) by A1, A2, A3, VECTSP_1:def 10;

      hence thesis by GROUP_1:def 5;

    end;

    

     Lm10: for F be commutative Skew-Field, G be Subgroup of ( MultGroup F), n be Nat st 0 < n holds ex f be Polynomial of F st ( deg f) = n & for x,xn be Element of F, xz be Element of G st x = xz & xn = (xz |^ n) holds ( eval (f,x)) = (xn - ( 1. F))

    proof

      let F be commutative Skew-Field, G be Subgroup of ( MultGroup F), n be Nat;

      reconsider n0 = n as Element of NAT by ORDINAL1:def 12;

      set f = (( <%( 0. F), ( 1_ F)%> `^ n0) - ( 1_. F));

       A1:

      now

        let x,xn be Element of F, xz be Element of G;

        assume that

         A2: x = xz and

         A3: xn = (xz |^ n);

        the carrier of G c= the carrier of ( MultGroup F) by GROUP_2:def 5;

        then

        reconsider xxz = xz as Element of ( MultGroup F);

        

         A4: xn = (xxz |^ n0) by A3, GROUP_4: 1

        .= (( power F) . (x,n0)) by A2, UNIROOTS: 29;

        

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

      end;

      assume 0 < n;

      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 f) = ( max ((n + 1),1)) by A5, A6, POLYNOM4: 7

      .= (n + 1) by A5, XXREAL_0:def 10;

      then ( deg f) = n;

      hence thesis by A1;

    end;

    

     Lm11: for F be commutative Skew-Field, G be Subgroup of ( MultGroup F), a,b be Element of G, n be 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, G be Subgroup of ( MultGroup F), a,b be Element of G, n be Nat;

      assume that

       A1: G is finite and

       A2: 0 < n and

       A3: ( ord a) = n and

       A4: (b |^ n) = ( 1_ G);

      consider f be Polynomial of F such that

       A5: ( deg f) = n and

       A6: for x,xn be Element of F, xz be Element of G st x = xz & xn = (xz |^ n) holds ( eval (f,x)) = (xn - ( 1. F)) by A2, Lm10;

      assume

       A7: not b is Element of ( gr {a});

      

       A8: the carrier of G c= the carrier of ( MultGroup F) by GROUP_2:def 5;

      

       A9: for x be Element of G st (x |^ n) = ( 1_ G) holds x in ( Roots f)

      proof

        let x1 be Element of G;

        

         A10: ( 1_ F) = ( 1_ ( MultGroup F)) by UNIROOTS: 17;

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

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

        hence x1 in ( Roots f) by POLYNOM5:def 10;

      end;

      

       A13: the carrier of ( gr {a}) c= ( Roots f)

      proof

        let x be object;

        assume

         A14: x in the carrier of ( gr {a});

        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;

        then

        consider j be 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;

      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 be 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 ( Segm (n0 + 1))) c= ( card ( Segm 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;

    end;

    theorem :: GR_CY_3:38

    for F be commutative Skew-Field, G be finite Subgroup of ( MultGroup F) holds G is cyclic Group

    proof

      let F be commutative Skew-Field, G be finite Subgroup of ( MultGroup F);

      set a = the Element of G;

      defpred P[ Nat, Element of G, Element of G] means ( ord $2) < ( ord $3);

      assume not G is cyclic Group;

      then

       A1: not ex x be Element of G st ( ord x) = ( card G) by GR_CY_1: 19;

      

       A2: for x be Element of G holds ( ord x) < ( card G)

      proof

        let x be Element of G;

        ( ord x) <= ( card G) by GR_CY_1: 8, NAT_D: 7;

        hence thesis by A1, XXREAL_0: 1;

      end;

      

       A3: for n be Nat holds for x be Element of G holds ex y be Element of G st P[n, x, y]

      proof

        let n be Nat, x be Element of G;

        set n = ( ord x);

        n < ( 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 be object such that

         A5: z in (the carrier of G \ the carrier of ( gr {x})) by XBOOLE_0:def 1;

        reconsider z as Element of G by A5;

        set m = ( ord z);

        set l = (m lcm n);

        n divides (m lcm n) by INT_2:def 1;

        then

        consider j be Integer such that

         A6: l = (n * j) by INT_1:def 3;

        

         A7: 1 <= ( card ( gr {x})) by GROUP_1: 45;

        then

         A8: 1 <= n by GR_CY_1: 7;

        then (l / n) = j by A6, XCMPLX_1: 89;

        then

         A9: j is Element of NAT by INT_1: 3;

         not m divides n

        proof

          assume m divides n;

          then

          consider j be Integer such that

           A10: n = (m * j) by INT_1:def 3;

          

           A11: 0 < n by A7, GR_CY_1: 7;

          (z |^ n) = ((z |^ m) |^ 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;

        end;

        then

         A12: n <> l by INT_2:def 1;

        

         A13: 1 <= ( card ( gr {z})) by GROUP_1: 45;

        then

         A14: m <> 0 by GR_CY_1: 7;

        1 <= m by A13, GR_CY_1: 7;

        then

        consider m0,n0 be Element of NAT such that

         A15: l = (n0 * m0) and

         A16: (n0 gcd m0) = 1 and

         A17: n0 divides n and

         A18: m0 divides m and

         A19: n0 <> 0 and

         A20: m0 <> 0 by A8, INT_7: 17;

        ex u be Integer st m = (m0 * u) by A18, INT_1:def 3;

        then (m / m0) is Integer by A20, XCMPLX_1: 89;

        then

        reconsider d2 = (m / m0) as Element of NAT by INT_1: 3;

        ex j be Integer st n = (n0 * j) by A17, INT_1:def 3;

        then (n / n0) is Integer by A19, XCMPLX_1: 89;

        then

        reconsider d1 = (n / n0) as Element of NAT by INT_1: 3;

        set y = ((x |^ d1) * (z |^ d2));

        m = (d2 * m0) by A20, XCMPLX_1: 87;

        then

         A21: ( ord (z |^ d2)) = m0 by INT_7: 30;

        n <> 0 by A7, GR_CY_1: 7;

        then j <> 0 by A14, A6, INT_2: 4;

        then (n * 1) <= (n * j) by A9, NAT_1: 14, XREAL_1: 64;

        then

         A22: n < l by A12, A6, XXREAL_0: 1;

        n = (d1 * n0) by A19, XCMPLX_1: 87;

        then ( ord (x |^ d1)) = n0 by INT_7: 30;

        then ( ord y) = (m0 * n0) by A16, A21, INT_7: 25;

        hence ex y be Element of G st n < ( ord y) by A15, A22;

      end;

      consider f be sequence of the carrier of G such that

       A23: (f . 0 ) = a & for n be Nat holds P[n, (f . n) qua Element of G, (f . (n + 1)) qua Element of G] from RECDEF_1:sch 2( A3);

      deffunc F( Nat) = ( ord (f . $1));

      consider g be sequence of NAT such that

       A24: for k be Element of NAT holds (g . k) = F(k) from FUNCT_2:sch 4;

      

       A25: for k be Nat holds (g . k) = F(k)

      proof

        let k be Nat;

        k in NAT by ORDINAL1:def 12;

        hence thesis by A24;

      end;

       A26:

      now

        let k be Nat;

        

         A27: (g . (k + 1)) = ( ord (f . (k + 1))) by A25;

        (g . k) = ( ord (f . k)) by A25;

        hence (g . k) < (g . (k + 1)) by A23, A27;

      end;

      

       A28: for k,m be Element of NAT holds (g . k) < (g . ((k + 1) + m))

      proof

        let k be Element of NAT ;

        defpred P[ Nat] means (g . k) < (g . ((k + 1) + $1));

         A29:

        now

          let m be Nat;

          assume

           A30: P[m];

          (g . ((k + 1) + m)) < (g . (((k + 1) + m) + 1)) by A26;

          hence P[(m + 1)] by A30, XXREAL_0: 2;

        end;

        

         A31: P[ 0 ] by A26;

        for m be Nat holds P[m] from NAT_1:sch 2( A31, A29);

        hence thesis;

      end;

      

       A32: for k,m be Element of NAT st k < m holds (g . k) < (g . m)

      proof

        let k,m be Element of NAT ;

        assume

         A33: k < m;

        then (m - k) is Element of NAT by INT_1: 5;

        then

        reconsider mk = (m - k) as Nat;

        (m - k) <> 0 by A33;

        then

        consider n0 be Nat such that

         A34: mk = (n0 + 1) by NAT_1: 6;

        reconsider n = n0 as Element of NAT by ORDINAL1:def 12;

        m = ((k + 1) + n) by A34;

        hence thesis by A28;

      end;

      now

        let x1,x2 be object;

        assume that

         A35: x1 in NAT and

         A36: x2 in NAT and

         A37: (g . x1) = (g . x2);

        reconsider xx1 = x1, xx2 = x2 as Element of NAT by A35, A36;

        

         A38: xx2 <= xx1 by A32, A37;

        xx1 <= xx2 by A32, A37;

        hence x2 = x1 by A38, XXREAL_0: 1;

      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

       A39: ( card ( rng g)) = ( card NAT ) by FUNCT_2:def 1;

      ( rng g) c= ( Segm ( card G))

      proof

        let y be object;

        assume y in ( rng g);

        then

        consider x be object such that

         A40: x in NAT and

         A41: y = (g . x) by FUNCT_2: 11;

        reconsider x as Element of NAT by A40;

        reconsider gg = (g . x) as Element of NAT ;

        (g . x) = ( ord (f . x)) by A25;

        then gg < ( card G) by A2;

        hence y in ( Segm ( card G)) by A41, NAT_1: 44;

      end;

      hence contradiction by A39;

    end;