numeral2.miz



    begin

    reserve n,k,b for Nat,

i for Integer;

    theorem :: NUMERAL2:1

    

     Th1: for f be non empty XFinSequence holds (f | 1) = <%(f . 0 )%>

    proof

      let f be non empty XFinSequence;

      

       A1: 0 in ( Segm ( 0 + 1)) by NAT_1: 45;

      ( len f) >= 1 by NAT_1: 14;

      then ( len (f | 1)) = 1 & ((f | 1) . 0 ) = (f . 0 ) by AFINSQ_1: 54, FUNCT_1: 49, A1;

      hence thesis by AFINSQ_1: 34;

    end;

    theorem :: NUMERAL2:2

    

     Th2: for f be non empty XFinSequence holds f = ( <%(f . 0 )%> ^ (f /^ 1))

    proof

      let f be non empty XFinSequence;

      

      thus f = ((f | 1) ^ (f /^ 1))

      .= ( <%(f . 0 )%> ^ (f /^ 1)) by Th1;

    end;

    theorem :: NUMERAL2:3

    

     Th3: for f be XFinSequence holds ( mid (f,2,( len f))) = (f /^ 1)

    proof

      let f be XFinSequence;

      

       A1: (2 - 1) >= 0 ;

      thus ( mid (f,2,( len f))) = (f /^ 1) by A1, XREAL_0:def 2;

    end;

    theorem :: NUMERAL2:4

    

     Th4: for X,Y be finite natural-membered set st X misses Y holds ( dom (( Sgm0 X) ^ ( Sgm0 Y))) = ( dom ( Sgm0 (X \/ Y)))

    proof

      let X,Y be finite natural-membered set such that

       A1: X misses Y;

      

      thus ( dom (( Sgm0 X) ^ ( Sgm0 Y))) = (( len ( Sgm0 X)) + ( len ( Sgm0 Y))) by AFINSQ_1:def 3

      .= (( card X) + ( len ( Sgm0 Y))) by AFINSQ_2: 20

      .= (( card X) + ( card Y)) by AFINSQ_2: 20

      .= ( card (X \/ Y)) by A1, CARD_2: 40

      .= ( len ( Sgm0 (X \/ Y))) by AFINSQ_2: 20

      .= ( dom ( Sgm0 (X \/ Y)));

    end;

    theorem :: NUMERAL2:5

    

     Th5: for X,Y be finite natural-membered set holds ( rng (( Sgm0 X) ^ ( Sgm0 Y))) = ( rng ( Sgm0 (X \/ Y)))

    proof

      let X,Y be finite natural-membered set;

      

      thus ( rng (( Sgm0 X) ^ ( Sgm0 Y))) = (( rng ( Sgm0 X)) \/ ( rng ( Sgm0 Y))) by AFINSQ_1: 26

      .= (X \/ ( rng ( Sgm0 Y))) by AFINSQ_2:def 4

      .= (X \/ Y) by AFINSQ_2:def 4

      .= ( rng ( Sgm0 (X \/ Y))) by AFINSQ_2:def 4;

    end;

    theorem :: NUMERAL2:6

    

     Th6: for F be XFinSequence holds for X be set holds ( dom ( SubXFinS (F,X))) = ( dom ( Sgm0 (X /\ ( dom F))))

    proof

      let F be XFinSequence;

      let X be set;

      ( len ( SubXFinS (F,X))) = ( card (X /\ ( Segm ( len F)))) by AFINSQ_2: 36

      .= ( card ( Sgm0 (X /\ ( dom F)))) by AFINSQ_2: 20;

      hence thesis;

    end;

    definition

      :: original: EvenNAT

      redefine

      :: NUMERAL2:def1

      func EvenNAT equals { n where n be Nat : n is even };

      compatibility

      proof

         EvenNAT = { n where n be Nat : n is even }

        proof

          thus EvenNAT c= { n where n be Nat : n is even }

          proof

            let m be object;

            assume m in EvenNAT ;

            then

            consider k be Nat such that

             A1: m = (2 * k) by FIB_NUM2:def 3;

            thus m in { n where n be Nat : n is even } by A1;

          end;

          thus { n where n be Nat : n is even } c= EvenNAT

          proof

            let m be object;

            assume m in { n where n be Nat : n is even };

            then

            consider n be Nat such that

             A2: n = m & n is even;

            consider k be Nat such that

             A3: n = (2 * k) by A2, ABIAN:def 2;

            thus m in EvenNAT by A2, A3, FIB_NUM2:def 3;

          end;

        end;

        hence thesis;

      end;

    end

    definition

      :: original: OddNAT

      redefine

      :: NUMERAL2:def2

      func OddNAT equals { n where n be Nat : n is odd };

      compatibility

      proof

         OddNAT = { n where n be Nat : n is odd }

        proof

          thus OddNAT c= { n where n be Nat : n is odd }

          proof

            let m be object;

            assume m in OddNAT ;

            then

            consider k be Element of NAT such that

             A1: m = ((2 * k) + 1) by FIB_NUM2:def 4;

            thus m in { n where n be Nat : n is odd } by A1;

          end;

          let m be object;

          assume m in { n where n be Nat : n is odd };

          then

          consider n be Nat such that

           A2: n = m & n is odd;

          consider k be Nat such that

           A3: n = ((2 * k) + 1) by A2, ABIAN: 9;

          k is Element of NAT by ORDINAL1:def 12;

          hence m in OddNAT by A2, A3, FIB_NUM2:def 4;

        end;

        hence thesis;

      end;

    end

    theorem :: NUMERAL2:7

    

     Th7: EvenNAT misses OddNAT

    proof

      thus ( EvenNAT /\ OddNAT ) c= {}

      proof

        let n be object;

        assume n in ( EvenNAT /\ OddNAT );

        then

         A1: n in EvenNAT & n in OddNAT by XBOOLE_0:def 4;

        consider e be Nat such that

         A2: e = n & e is even by A1;

        consider o be Nat such that

         A3: o = n & o is odd by A1;

        thus thesis by A2, A3;

      end;

      thus {} c= ( EvenNAT /\ OddNAT ) by XBOOLE_1: 2;

    end;

    theorem :: NUMERAL2:8

    

     Th8: ( EvenNAT \/ OddNAT ) = NAT

    proof

      thus ( EvenNAT \/ OddNAT ) c= NAT ;

      let n be object;

      assume

       A1: n in NAT & not n in ( EvenNAT \/ OddNAT );

      then

      reconsider n as Nat;

      n in NAT & not n in EvenNAT & not n in OddNAT by A1, XBOOLE_0:def 3;

      then not n is even & not n is odd;

      hence contradiction;

    end;

    registration

      let F be Sequence;

      let P be Permutation of ( dom F);

      cluster (F * P) -> Sequence-like;

      correctness

      proof

        per cases ;

          suppose ( rng F) is empty;

          then F = {} ;

          hence thesis;

        end;

          suppose

           A1: ( rng F) is non empty;

          

           A2: ( dom P) = ( dom F) by FUNCT_2: 52;

          F is Function of ( dom F), ( rng F) by FUNCT_2: 1;

          then ( dom (F * P)) = ( dom F) by A1, FUNCT_2: 123, A2;

          hence thesis by ORDINAL1:def 7;

        end;

      end;

    end

    theorem :: NUMERAL2:9

    

     Th9: for F be XFinSequence holds for X,Y be set st X misses Y holds ex P be Permutation of ( dom ( SubXFinS (F,(X \/ Y)))) st (( SubXFinS (F,(X \/ Y))) * P) = (( SubXFinS (F,X)) ^ ( SubXFinS (F,Y)))

    proof

      let F be XFinSequence;

      let X,Y be set such that

       A1: X misses Y;

      set A = (( Sgm0 (X /\ ( Segm ( len F)))) ^ ( Sgm0 (Y /\ ( Segm ( len F)))));

      set B = ( Sgm0 ((X \/ Y) /\ ( Segm ( len F))));

      

       A2: ( rng ( Sgm0 (X /\ ( Segm ( len F))))) = (X /\ ( len F)) & ( rng ( Sgm0 (Y /\ ( Segm ( len F))))) = (Y /\ ( len F)) by AFINSQ_2:def 4;

      then

      reconsider A as one-to-one Function by A1, XBOOLE_1: 76, CARD_FIN: 52;

      reconsider B as one-to-one Function;

      

       A3: ((X \/ Y) /\ ( len F)) = ((X /\ ( len F)) \/ (Y /\ ( len F))) by XBOOLE_1: 23;

      then

       A4: ( rng A) = ( rng B) by Th5;

      then

       A5: ( rng A) = ( dom (B " )) by FUNCT_1: 33;

      set P = ((B " ) * A);

      

       A6: ( dom P) = ( dom A) by A5, RELAT_1: 27

      .= ( dom B) by A3, A1, XBOOLE_1: 76, Th4

      .= ( dom ( SubXFinS (F,(X \/ Y)))) by Th6;

      

       A7: ( rng P) = ( rng (B " )) by A5, RELAT_1: 28

      .= ( dom B) by FUNCT_1: 33

      .= ( dom ( SubXFinS (F,(X \/ Y)))) by Th6;

      reconsider P as Function of ( dom ( SubXFinS (F,(X \/ Y)))), ( dom ( SubXFinS (F,(X \/ Y)))) by A6, A7, FUNCT_2: 2;

      ( card ( dom ( SubXFinS (F,(X \/ Y))))) = ( card ( dom ( SubXFinS (F,(X \/ Y)))));

      then P is onto by FINSEQ_4: 63;

      then

      reconsider P as Permutation of ( dom ( SubXFinS (F,(X \/ Y))));

      take P;

      

       A8: ( rng ( Sgm0 (X /\ ( Segm ( len F))))) c= ( len F) & ( rng ( Sgm0 (Y /\ ( Segm ( len F))))) c= ( len F) by A2, XBOOLE_1: 17;

      

      thus (( SubXFinS (F,(X \/ Y))) * P) = (F * (( Sgm0 ((X \/ Y) /\ ( Segm ( len F)))) * ((B " ) * A))) by RELAT_1: 36

      .= (F * ((( Sgm0 ((X \/ Y) /\ ( Segm ( len F)))) * (B " )) * A)) by RELAT_1: 36

      .= (F * (( id ( rng A)) * A)) by FUNCT_1: 39, A4

      .= (F * A) by RELAT_1: 54

      .= (( SubXFinS (F,X)) ^ ( SubXFinS (F,Y))) by A8, AFINSQ_2: 70;

    end;

    theorem :: NUMERAL2:10

    

     Th10: for cF be complex-valued XFinSequence holds for B1,B2 be set st B1 misses B2 holds ( Sum ( SubXFinS (cF,(B1 \/ B2)))) = (( Sum ( SubXFinS (cF,B1))) + ( Sum ( SubXFinS (cF,B2))))

    proof

      let cF be complex-valued XFinSequence;

      let B1,B2 be set such that

       A1: B1 misses B2;

      set O = ( SubXFinS (cF,(B1 \/ B2)));

      ( rng O) c= COMPLEX by VALUED_0:def 1;

      then

      reconsider O = ( SubXFinS (cF,(B1 \/ B2))) as XFinSequence of COMPLEX by RELAT_1:def 19;

      consider P be Permutation of ( dom O) such that

       A2: (O * P) = (( SubXFinS (cF,B1)) ^ ( SubXFinS (cF,B2))) by A1, Th9;

      ( Sum (O * P)) = (( Sum ( SubXFinS (cF,B1))) + ( Sum ( SubXFinS (cF,B2)))) by A2, AFINSQ_2: 55;

      hence thesis by AFINSQ_2: 45;

    end;

    theorem :: NUMERAL2:11

    

     Th11: for F be XFinSequence holds F = ( SubXFinS (F, NAT ))

    proof

      let F be XFinSequence;

      set SFN = ( Sgm0 (( len F) /\ NAT ));

      ( dom F) c= NAT ;

      then

       A1: (( len F) /\ NAT ) = ( len F) by XBOOLE_1: 28;

      

       A2: F is Function of ( dom F), ( rng F) by FUNCT_2: 1;

      ( rng ( id ( dom F))) c= NAT ;

      then

      reconsider idF = ( id ( dom F)) as XFinSequence of NAT by RELAT_1:def 19;

      

       A3: ( rng idF) = ( len F);

      now

        let l,m,k1,k2 be Nat;

        assume

         A4: l < m & m < ( len idF) & k1 = (idF . l) & k2 = (idF . m);

        then l < ( len idF) by XXREAL_0: 2;

        then k1 = l & k2 = m by A4, FUNCT_1: 18, AFINSQ_1: 66;

        hence k1 < k2 by A4;

      end;

      then ( id ( dom F)) = ( Sgm0 ( Segm ( len F))) by AFINSQ_2:def 4, A3;

      hence thesis by A1, FUNCT_2: 17, A2;

    end;

    theorem :: NUMERAL2:12

    

     Th12: for N,i be Nat st i in ( dom ( Sgm0 (N /\ EvenNAT ))) holds (( Sgm0 (N /\ EvenNAT )) . i) = (2 * i)

    proof

      defpred P[ Nat] means for i be Nat st i in ( dom ( Sgm0 ($1 /\ EvenNAT ))) holds (( Sgm0 ($1 /\ EvenNAT )) . i) = (2 * i);

      

       A1: P[ 0 ]

      proof

        let i be Nat;

        assume i in ( dom ( Sgm0 ( 0 /\ EvenNAT )));

        then i in ( len ( Sgm0 {} ));

        then i in ( card {} ) by AFINSQ_2: 20;

        hence thesis;

      end;

       A2:

      now

        let n be Nat;

        assume

         A3: P[n];

        thus P[(n + 1)]

        proof

          let i be Nat;

          assume

           A4: i in ( dom ( Sgm0 ((n + 1) /\ EvenNAT )));

          per cases ;

            suppose

             A5: n is even;

            

             A6: ((n + 1) /\ EvenNAT ) = ((n /\ EvenNAT ) \/ {n})

            proof

              thus ((n + 1) /\ EvenNAT ) c= ((n /\ EvenNAT ) \/ {n})

              proof

                let x be object;

                assume

                 A7: x in ((n + 1) /\ EvenNAT );

                then x in (n + 1) & x in EvenNAT by XBOOLE_0:def 4;

                then

                consider y be Nat such that

                 A8: y = x & y is even;

                y in ( Segm (n + 1)) & y in EvenNAT by A7, XBOOLE_0:def 4, A8;

                then (y < n or y = n) & y in EvenNAT by NAT_1: 44, NAT_1: 22;

                then (y in ( Segm n) & y in EvenNAT ) or y = n by NAT_1: 44;

                then y in (n /\ EvenNAT ) or y in {n} by XBOOLE_0:def 4, TARSKI:def 1;

                hence x in ((n /\ EvenNAT ) \/ {n}) by A8, XBOOLE_0:def 3;

              end;

              let x be object;

              assume x in ((n /\ EvenNAT ) \/ {n});

              per cases by XBOOLE_0:def 3;

                suppose

                 A9: x in (n /\ EvenNAT );

                ( Segm n) c= ( Segm (n + 1)) by NAT_1: 11, NAT_1: 39;

                then (n /\ EvenNAT ) c= ((n + 1) /\ EvenNAT ) by XBOOLE_1: 26;

                hence x in ((n + 1) /\ EvenNAT ) by A9;

              end;

                suppose x in {n};

                then x = n by TARSKI:def 1;

                then x in ( Segm (n + 1)) & x in EvenNAT by NAT_1: 45, A5;

                hence x in ((n + 1) /\ EvenNAT ) by XBOOLE_0:def 4;

              end;

            end;

            reconsider X = (n /\ EvenNAT ) as finite natural-membered set;

            reconsider Y = {n} as finite natural-membered set;

            

             A10: X <N< Y

            proof

              let a,b be Nat;

              assume a in X & b in Y;

              then a in ( Segm n) & b = n by XBOOLE_0:def 4, TARSKI:def 1;

              hence a < b by NAT_1: 44;

            end;

             not n in n;

            then not n in (n /\ EvenNAT ) by XBOOLE_0:def 4;

            then

             A11: ( card ((n + 1) /\ EvenNAT )) = (( card (n /\ EvenNAT )) + 1) by A6, CARD_2: 41;

            

             A12: i in ( Segm ( dom ( Sgm0 ((n + 1) /\ EvenNAT )))) by A4;

            then i < ( len ( Sgm0 ((n + 1) /\ EvenNAT ))) by NAT_1: 44;

            then i < (( card (n /\ EvenNAT )) + 1) by A11, AFINSQ_2: 20;

            then i < (( len ( Sgm0 X)) + 1) by AFINSQ_2: 20;

            per cases by NAT_1: 22;

              suppose

               A13: i < ( len ( Sgm0 X));

              then

               A14: i < ( Segm ( card ( Sgm0 (n /\ EvenNAT ))));

              

              thus (( Sgm0 ((n + 1) /\ EvenNAT )) . i) = (( Sgm0 (n /\ EvenNAT )) . i) by A10, A13, AFINSQ_2: 29, A6

              .= (2 * i) by A14, NAT_1: 44, A3;

            end;

              suppose

               A15: i = ( len ( Sgm0 X));

              

              then

               A16: (( Sgm0 ((n + 1) /\ EvenNAT )) . i) = (( Sgm0 Y) . 0 ) by AFINSQ_2: 32, A10, A6

              .= n by AFINSQ_2: 22;

              (( Sgm0 ((n + 1) /\ EvenNAT )) . i) in ( rng ( Sgm0 ((n + 1) /\ EvenNAT ))) by FUNCT_1: 3, A4;

              then (( Sgm0 ((n + 1) /\ EvenNAT )) . i) in ((n + 1) /\ EvenNAT ) by AFINSQ_2:def 4;

              then (( Sgm0 ((n + 1) /\ EvenNAT )) . i) in EvenNAT by XBOOLE_0:def 4;

              then

              consider r be Nat such that

               A17: r = (( Sgm0 ((n + 1) /\ EvenNAT )) . i) & r is even;

              consider j be Nat such that

               A18: r = (2 * j) by A17, ABIAN:def 2;

              per cases by XXREAL_0: 1;

                suppose

                 A19: j < i;

                then

                 A20: j < ( Segm ( card ( Sgm0 (n /\ EvenNAT )))) by A15;

                j < ( card ( Sgm0 ((n + 1) /\ EvenNAT ))) by A19, A12, NAT_1: 44, XXREAL_0: 2;

                then

                 A21: j in ( Segm ( dom ( Sgm0 ((n + 1) /\ EvenNAT )))) by NAT_1: 44;

                (( Sgm0 ((n + 1) /\ EvenNAT )) . j) = (( Sgm0 (n /\ EvenNAT )) . j) by A10, A19, A15, AFINSQ_2: 29, A6

                .= (( Sgm0 ((n + 1) /\ EvenNAT )) . i) by A20, NAT_1: 44, A3, A17, A18;

                hence (( Sgm0 ((n + 1) /\ EvenNAT )) . i) = (2 * i) by A21, A4, FUNCT_1:def 4, A19;

              end;

                suppose j = i;

                hence (( Sgm0 ((n + 1) /\ EvenNAT )) . i) = (2 * i) by A17, A18;

              end;

                suppose

                 A22: j > i;

                

                 A23: (2 * i) in EvenNAT ;

                (2 * i) < n & n < (n + 1) by A22, XREAL_1: 68, A17, A18, A16, NAT_1: 16;

                then (2 * i) < (n + 1) by XXREAL_0: 2;

                then (2 * i) in ( Segm (n + 1)) by NAT_1: 44;

                then (2 * i) in ((n + 1) /\ EvenNAT ) by A23, XBOOLE_0:def 4;

                then (2 * i) in ( rng ( Sgm0 ((n + 1) /\ EvenNAT ))) by AFINSQ_2:def 4;

                then

                consider l be object such that

                 A24: l in ( dom ( Sgm0 ((n + 1) /\ EvenNAT ))) & (( Sgm0 ((n + 1) /\ EvenNAT )) . l) = (2 * i) by FUNCT_1:def 3;

                reconsider l as Element of NAT by A24;

                l in ( Segm ( dom ( Sgm0 ((n + 1) /\ EvenNAT )))) by A24;

                then l < ( len ( Sgm0 ((n + 1) /\ EvenNAT ))) by NAT_1: 44;

                then l < (( card (n /\ EvenNAT )) + 1) by A11, AFINSQ_2: 20;

                then l < (( len ( Sgm0 X)) + 1) by AFINSQ_2: 20;

                per cases by NAT_1: 22;

                  suppose

                   A25: l < ( len ( Sgm0 X));

                  then

                   A26: l < ( Segm ( card ( Sgm0 (n /\ EvenNAT ))));

                  (( Sgm0 ((n + 1) /\ EvenNAT )) . l) = (( Sgm0 (n /\ EvenNAT )) . l) by A10, A25, AFINSQ_2: 29, A6

                  .= (2 * l) by A26, NAT_1: 44, A3;

                  then (2 * i) = (2 * l) by A24;

                  hence (( Sgm0 ((n + 1) /\ EvenNAT )) . i) = (2 * i) by A25, A15;

                end;

                  suppose l = ( len ( Sgm0 X));

                  hence (( Sgm0 ((n + 1) /\ EvenNAT )) . i) = (2 * i) by A15, A24;

                end;

              end;

            end;

          end;

            suppose

             A27: n is odd;

            ((n + 1) /\ EvenNAT ) = (n /\ EvenNAT )

            proof

              thus ((n + 1) /\ EvenNAT ) c= (n /\ EvenNAT )

              proof

                let x be object;

                assume x in ((n + 1) /\ EvenNAT );

                then

                 A28: x in ( Segm (n + 1)) & x in EvenNAT by XBOOLE_0:def 4;

                then

                consider y be Nat such that

                 A29: y = x & y is even;

                y < n by A28, A29, NAT_1: 44, A27, NAT_1: 22;

                then y in ( Segm n) & y in EvenNAT by A29, NAT_1: 44;

                hence x in (n /\ EvenNAT ) by A29, XBOOLE_0:def 4;

              end;

              ( Segm n) c= ( Segm (n + 1)) by NAT_1: 11, NAT_1: 39;

              hence (n /\ EvenNAT ) c= ((n + 1) /\ EvenNAT ) by XBOOLE_1: 26;

            end;

            hence (( Sgm0 ((n + 1) /\ EvenNAT )) . i) = (2 * i) by A4, A3;

          end;

        end;

      end;

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

      hence thesis;

    end;

    theorem :: NUMERAL2:13

    

     Th13: for N,i be Nat st i in ( dom ( Sgm0 (N /\ OddNAT ))) holds (( Sgm0 (N /\ OddNAT )) . i) = ((2 * i) + 1)

    proof

      defpred P[ Nat] means for i be Nat st i in ( dom ( Sgm0 ($1 /\ OddNAT ))) holds (( Sgm0 ($1 /\ OddNAT )) . i) = ((2 * i) + 1);

      

       A1: P[ 0 ]

      proof

        let i be Nat;

        assume i in ( dom ( Sgm0 ( 0 /\ OddNAT )));

        then i in ( len ( Sgm0 {} ));

        then i in ( card {} ) by AFINSQ_2: 20;

        hence thesis;

      end;

       A2:

      now

        let n be Nat;

        assume

         A3: P[n];

        thus P[(n + 1)]

        proof

          let i be Nat;

          assume

           A4: i in ( dom ( Sgm0 ((n + 1) /\ OddNAT )));

          per cases ;

            suppose

             A5: n is odd;

            

             A6: ((n + 1) /\ OddNAT ) = ((n /\ OddNAT ) \/ {n})

            proof

              thus ((n + 1) /\ OddNAT ) c= ((n /\ OddNAT ) \/ {n})

              proof

                let x be object;

                assume

                 A7: x in ((n + 1) /\ OddNAT );

                then x in (n + 1) & x in OddNAT by XBOOLE_0:def 4;

                then

                consider y be Nat such that

                 A8: y = x & y is odd;

                y in ( Segm (n + 1)) & y in OddNAT by A7, XBOOLE_0:def 4, A8;

                then (y < n or y = n) & y in OddNAT by NAT_1: 44, NAT_1: 22;

                then (y in ( Segm n) & y in OddNAT ) or y = n by NAT_1: 44;

                then y in (n /\ OddNAT ) or y in {n} by XBOOLE_0:def 4, TARSKI:def 1;

                hence x in ((n /\ OddNAT ) \/ {n}) by A8, XBOOLE_0:def 3;

              end;

              let x be object;

              assume x in ((n /\ OddNAT ) \/ {n});

              per cases by XBOOLE_0:def 3;

                suppose

                 A9: x in (n /\ OddNAT );

                ( Segm n) c= ( Segm (n + 1)) by NAT_1: 11, NAT_1: 39;

                then (n /\ OddNAT ) c= ((n + 1) /\ OddNAT ) by XBOOLE_1: 26;

                hence x in ((n + 1) /\ OddNAT ) by A9;

              end;

                suppose x in {n};

                then x = n by TARSKI:def 1;

                then x in ( Segm (n + 1)) & x in OddNAT by NAT_1: 45, A5;

                hence x in ((n + 1) /\ OddNAT ) by XBOOLE_0:def 4;

              end;

            end;

            reconsider X = (n /\ OddNAT ) as finite natural-membered set;

            reconsider Y = {n} as finite natural-membered set;

            

             A10: X <N< Y

            proof

              let a,b be Nat;

              assume a in X & b in Y;

              then a in ( Segm n) & b = n by XBOOLE_0:def 4, TARSKI:def 1;

              hence a < b by NAT_1: 44;

            end;

             not n in n;

            then not n in (n /\ OddNAT ) by XBOOLE_0:def 4;

            then

             A11: ( card ((n + 1) /\ OddNAT )) = (( card (n /\ OddNAT )) + 1) by A6, CARD_2: 41;

            

             A12: i in ( Segm ( dom ( Sgm0 ((n + 1) /\ OddNAT )))) by A4;

            then i < ( len ( Sgm0 ((n + 1) /\ OddNAT ))) by NAT_1: 44;

            then i < (( card (n /\ OddNAT )) + 1) by A11, AFINSQ_2: 20;

            then i < (( len ( Sgm0 X)) + 1) by AFINSQ_2: 20;

            per cases by NAT_1: 22;

              suppose

               A13: i < ( len ( Sgm0 X));

              then

               A14: i < ( Segm ( card ( Sgm0 (n /\ OddNAT ))));

              

              thus (( Sgm0 ((n + 1) /\ OddNAT )) . i) = (( Sgm0 (n /\ OddNAT )) . i) by A10, A13, AFINSQ_2: 29, A6

              .= ((2 * i) + 1) by A14, NAT_1: 44, A3;

            end;

              suppose

               A15: i = ( len ( Sgm0 X));

              

              then

               A16: (( Sgm0 ((n + 1) /\ OddNAT )) . i) = (( Sgm0 Y) . 0 ) by AFINSQ_2: 32, A10, A6

              .= n by AFINSQ_2: 22;

              (( Sgm0 ((n + 1) /\ OddNAT )) . i) in ( rng ( Sgm0 ((n + 1) /\ OddNAT ))) by FUNCT_1: 3, A4;

              then (( Sgm0 ((n + 1) /\ OddNAT )) . i) in ((n + 1) /\ OddNAT ) by AFINSQ_2:def 4;

              then (( Sgm0 ((n + 1) /\ OddNAT )) . i) in OddNAT by XBOOLE_0:def 4;

              then

              consider r be Nat such that

               A17: r = (( Sgm0 ((n + 1) /\ OddNAT )) . i) & r is odd;

              consider j be Nat such that

               A18: r = ((2 * j) + 1) by A17, ABIAN: 9;

              per cases by XXREAL_0: 1;

                suppose

                 A19: j < i;

                then

                 A20: j < ( Segm ( card ( Sgm0 (n /\ OddNAT )))) by A15;

                j < ( card ( Sgm0 ((n + 1) /\ OddNAT ))) by A19, A12, NAT_1: 44, XXREAL_0: 2;

                then

                 A21: j in ( Segm ( dom ( Sgm0 ((n + 1) /\ OddNAT )))) by NAT_1: 44;

                (( Sgm0 ((n + 1) /\ OddNAT )) . j) = (( Sgm0 (n /\ OddNAT )) . j) by A10, A19, A15, AFINSQ_2: 29, A6

                .= (( Sgm0 ((n + 1) /\ OddNAT )) . i) by A20, NAT_1: 44, A3, A17, A18;

                hence (( Sgm0 ((n + 1) /\ OddNAT )) . i) = ((2 * i) + 1) by A21, A4, FUNCT_1:def 4, A19;

              end;

                suppose j = i;

                hence (( Sgm0 ((n + 1) /\ OddNAT )) . i) = ((2 * i) + 1) by A17, A18;

              end;

                suppose j > i;

                then

                 A22: (2 * i) < (2 * j) by XREAL_1: 68;

                

                 A23: ((2 * i) + 1) in OddNAT ;

                ((2 * i) + 1) < n & n < (n + 1) by A22, XREAL_1: 8, A17, A18, A16, NAT_1: 16;

                then ((2 * i) + 1) < (n + 1) by XXREAL_0: 2;

                then ((2 * i) + 1) in ( Segm (n + 1)) by NAT_1: 44;

                then ((2 * i) + 1) in ((n + 1) /\ OddNAT ) by A23, XBOOLE_0:def 4;

                then ((2 * i) + 1) in ( rng ( Sgm0 ((n + 1) /\ OddNAT ))) by AFINSQ_2:def 4;

                then

                consider l be object such that

                 A24: l in ( dom ( Sgm0 ((n + 1) /\ OddNAT ))) & (( Sgm0 ((n + 1) /\ OddNAT )) . l) = ((2 * i) + 1) by FUNCT_1:def 3;

                reconsider l as Element of NAT by A24;

                l in ( Segm ( dom ( Sgm0 ((n + 1) /\ OddNAT )))) by A24;

                then l < ( len ( Sgm0 ((n + 1) /\ OddNAT ))) by NAT_1: 44;

                then l < (( card (n /\ OddNAT )) + 1) by A11, AFINSQ_2: 20;

                then l < (( len ( Sgm0 X)) + 1) by AFINSQ_2: 20;

                per cases by NAT_1: 22;

                  suppose

                   A25: l < ( len ( Sgm0 X));

                  then

                   A26: l < ( Segm ( card ( Sgm0 (n /\ OddNAT ))));

                  (( Sgm0 ((n + 1) /\ OddNAT )) . l) = (( Sgm0 (n /\ OddNAT )) . l) by A10, A25, AFINSQ_2: 29, A6

                  .= ((2 * l) + 1) by A26, NAT_1: 44, A3;

                  then ((2 * i) + 1) = ((2 * l) + 1) by A24;

                  hence (( Sgm0 ((n + 1) /\ OddNAT )) . i) = ((2 * i) + 1) by A25, A15;

                end;

                  suppose l = ( len ( Sgm0 X));

                  hence (( Sgm0 ((n + 1) /\ OddNAT )) . i) = ((2 * i) + 1) by A15, A24;

                end;

              end;

            end;

          end;

            suppose

             A27: n is even;

            ((n + 1) /\ OddNAT ) = (n /\ OddNAT )

            proof

              thus ((n + 1) /\ OddNAT ) c= (n /\ OddNAT )

              proof

                let x be object;

                assume x in ((n + 1) /\ OddNAT );

                then

                 A28: x in ( Segm (n + 1)) & x in OddNAT by XBOOLE_0:def 4;

                then

                consider y be Nat such that

                 A29: y = x & y is odd;

                y < n by A28, A29, NAT_1: 44, A27, NAT_1: 22;

                then y in ( Segm n) & y in OddNAT by A29, NAT_1: 44;

                hence x in (n /\ OddNAT ) by A29, XBOOLE_0:def 4;

              end;

              ( Segm n) c= ( Segm (n + 1)) by NAT_1: 11, NAT_1: 39;

              hence (n /\ OddNAT ) c= ((n + 1) /\ OddNAT ) by XBOOLE_1: 26;

            end;

            hence (( Sgm0 ((n + 1) /\ OddNAT )) . i) = ((2 * i) + 1) by A4, A3;

          end;

        end;

      end;

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

      hence thesis;

    end;

    begin

    theorem :: NUMERAL2:14

    

     Th14: for i,j be Integer holds ((i mod j) mod j) = (i mod j)

    proof

      let i,j be Integer;

      per cases ;

        suppose j <> 0 ;

        

        hence ((i mod j) mod j) = ((i - ((i div j) * j)) mod j) by INT_1:def 10

        .= ((i + (j * ( - (i div j)) qua Integer)) mod j)

        .= (i mod j) by NAT_D: 61;

      end;

        suppose

         A1: j = 0 ;

        

        hence ((i mod j) mod j) = 0 by INT_1:def 10

        .= (i mod j) by A1, INT_1:def 10;

      end;

    end;

    theorem :: NUMERAL2:15

    for i,j,k,l be Integer st (i mod l) = (j mod l) holds ((k + i) mod l) = ((k + j) mod l)

    proof

      let i,j,k,l be Integer;

      assume

       A1: (i mod l) = (j mod l);

      

      thus ((k + i) mod l) = (((k mod l) + (i mod l)) mod l) by NAT_D: 66

      .= ((k + j) mod l) by A1, NAT_D: 66;

    end;

    theorem :: NUMERAL2:16

    

     Th16: for d be XFinSequence of INT , n be Integer st for i be Nat st i in ( dom d) holds n divides (d . i) holds n divides ( Sum d)

    proof

      let d be XFinSequence of INT , n be Integer such that

       A1: for i be Nat st i in ( dom d) holds n divides (d . i);

      per cases ;

        suppose ( len d) = 0 ;

        then d = {} ;

        then ( Sum d) = 0 ;

        hence thesis by INT_2: 12;

      end;

        suppose

         A2: ( len d) > 0 ;

        then

        consider f be Function of NAT , INT such that

         A3: (f . 0 ) = (d . 0 ) and

         A4: for n be Nat st (n + 1) < ( len d) holds (f . (n + 1)) = ( addint . ((f . n),(d . (n + 1)))) and

         A5: ( addint "**" d) = (f . (( len d) - 1)) by AFINSQ_2:def 8;

        defpred P[ Nat] means $1 < ( len d) implies n divides (f . $1);

         A6:

        now

          let k be Nat;

          assume

           A7: P[k];

          thus P[(k + 1)]

          proof

            assume

             A8: (k + 1) < ( len d);

            then (k + 1) in ( Segm ( len d)) by NAT_1: 44;

            then

             A9: n divides (d . (k + 1)) by A1;

            (f . (k + 1)) = ( addint . ((f . k),(d . (k + 1)))) by A4, A8

            .= ((f . k) + (d . (k + 1))) by BINOP_2:def 20;

            hence thesis by A7, A8, A9, XREAL_1: 145, WSIERP_1: 4;

          end;

        end;

        reconsider ld = (( len d) - 1) as Element of NAT by A2, NAT_1: 20;

        

         A10: ld < ( len d) by XREAL_1: 147;

         0 in ( Segm ( dom d)) by NAT_1: 44, A2;

        then

         A11: P[ 0 ] by A1, A3;

        

         A12: ( addint "**" d) = ( Sum d) by AFINSQ_2: 50;

        for k be Nat holds P[k] from NAT_1:sch 2( A11, A6);

        hence thesis by A5, A10, A12;

      end;

    end;

    theorem :: NUMERAL2:17

    for d,e be XFinSequence of INT , n be Integer st ( dom d) = ( dom e) & for i be Nat st i in ( dom d) holds (e . i) = ((d . i) mod n) holds (( Sum d) mod n) = (( Sum e) mod n)

    proof

      let d,e be XFinSequence of INT , n be Integer such that

       A1: ( dom d) = ( dom e) & for i be Nat st i in ( dom d) holds (e . i) = ((d . i) mod n);

      defpred P[ XFinSequence of INT ] means for e be XFinSequence of INT st ( dom $1) = ( dom e) & for i be Nat st i in ( dom $1) holds (e . i) = (($1 . i) mod n) holds (( Sum $1) mod n) = (( Sum e) mod n);

      

       A2: for p be XFinSequence of INT , l be Element of INT st P[p] holds P[(p ^ <%l%>)]

      proof

        let p be XFinSequence of INT , l be Element of INT ;

        assume

         A3: P[p];

        thus P[(p ^ <%l%>)]

        proof

          reconsider dop = ( dom p) as Element of NAT by ORDINAL1:def 12;

          defpred Q[ set, Integer] means $2 = ((p . $1) mod n);

          let e be XFinSequence of INT ;

          assume that

           A4: ( dom (p ^ <%l%>)) = ( dom e) and

           A5: for i be Nat st i in ( dom (p ^ <%l%>)) holds (e . i) = (((p ^ <%l%>) . i) mod n);

          

           A6: for k be Nat st k in ( Segm dop) holds ex x be Element of INT st Q[k, x]

          proof

            let k be Nat;

            assume k in ( Segm dop);

            reconsider x = ((p . k) mod n) as Element of INT by INT_1:def 2;

            take x;

            thus thesis;

          end;

          consider p9 be XFinSequence of INT such that

           A7: ( dom p9) = ( Segm dop) & for k be Nat st k in ( Segm dop) holds Q[k, (p9 . k)] from STIRL2_1:sch 5( A6);

           A8:

          now

            let k be Nat;

            assume

             A9: k in ( dom p9);

            then k < ( Segm ( dom p9)) by NAT_1: 44;

            then k < (( len p) + 1) by A7, NAT_1: 13;

            then k < (( len p) + ( len <%l%>)) by AFINSQ_1: 33;

            then k in ( Segm (( len p) + ( len <%l%>))) by NAT_1: 44;

            then k in ( dom (p ^ <%l%>)) by AFINSQ_1:def 3;

            

            hence (e . k) = (((p ^ <%l%>) . k) mod n) by A5

            .= ((p . k) mod n) by A7, A9, AFINSQ_1:def 3

            .= (p9 . k) by A7, A9;

          end;

           A10:

          now

            let k be Nat;

            assume k in ( dom <%(l mod n)%>);

            then

             A11: k in ( Segm 1) by AFINSQ_1: 33;

            then

             A12: k = 0 by NAT_1: 44, NAT_1: 14;

            k in ( dom <%l%>) by A11, AFINSQ_1: 33;

            

            hence (e . (( len p9) + k)) = (((p ^ <%l%>) . ( len p)) mod n) by A5, A7, A12, AFINSQ_1: 23

            .= ( <%(l mod n)%> . k) by A12, AFINSQ_1: 36;

          end;

          ( dom e) = (( len p) + ( len <%l%>)) by A4, AFINSQ_1:def 3

          .= (( dom p) + 1) by AFINSQ_1: 33

          .= (( len p9) + ( len <%(l mod n)%>)) by A7, AFINSQ_1: 33;

          then

           A13: e = (p9 ^ <%(l mod n)%>) by A8, A10, AFINSQ_1:def 3;

          reconsider lmn = (l mod n) as Element of INT by INT_1:def 2;

          

          thus (( Sum (p ^ <%l%>)) mod n) = ((( Sum p) + ( Sum <%l%>)) mod n) by AFINSQ_2: 55

          .= ((( Sum p) + l) mod n) by AFINSQ_2: 53

          .= (((( Sum p) mod n) + (l mod n)) mod n) by NAT_D: 66

          .= (((( Sum p9) mod n) + (l mod n)) mod n) by A3, A7

          .= (((( Sum p9) mod n) + ((l mod n) mod n)) mod n) by Th14

          .= ((( Sum p9) + (l mod n)) mod n) by NAT_D: 66

          .= ((( Sum p9) + ( Sum <%lmn%>)) mod n) by AFINSQ_2: 53

          .= (( Sum e) mod n) by A13, AFINSQ_2: 55;

        end;

      end;

      

       A14: P[( <%> INT )] by AFINSQ_1: 15;

      for p be XFinSequence of INT holds P[p] from AFINSQ_2:sch 2( A14, A2);

      hence thesis by A1;

    end;

    theorem :: NUMERAL2:18

    

     Th18: for f,g be XFinSequence of NAT , i be Integer st ( dom f) = ( dom g) & for n be object st n in ( dom f) holds (f . n) = (i * (g . n)) holds ( Sum f) = (i * ( Sum g))

    proof

      let f,g be XFinSequence of NAT , i be Integer;

      assume ( dom f) = ( dom g) & for n be object st n in ( dom f) holds (f . n) = (i * (g . n));

      then f = (i (#) g) by VALUED_1:def 5;

      hence ( Sum f) = (i * ( Sum g)) by AFINSQ_2: 64;

    end;

    theorem :: NUMERAL2:19

    

     Th19: b > 1 implies n = ((b * ( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b))) + (( digits (n,b)) . 0 ))

    proof

      assume

       A1: b > 1;

      set d = ( digits (n,b));

      

       A2: ( len d) >= 1 by A1, NUMERAL1: 4;

      then

       A3: 0 in ( Segm ( dom d)) by NAT_1: 44;

      n = ( value (d,b)) by A1, NUMERAL1: 5;

      then

      consider d1 be XFinSequence of NAT such that

       A4: (( dom d1) = ( dom d) & for i be Nat st i in ( dom d1) holds (d1 . i) = ((d . i) * (b |^ i))) & n = ( Sum d1) by NUMERAL1:def 1;

      d1 <> {} by A4, A2;

      then d1 = ( <%(d1 . 0 )%> ^ (d1 /^ 1)) by Th2;

      

      then

       A5: n = (( Sum <%(d1 . 0 )%>) + ( Sum (d1 /^ 1))) by A4, AFINSQ_2: 55

      .= ((d1 . 0 ) + ( Sum (d1 /^ 1))) by AFINSQ_2: 53

      .= (( Sum (d1 /^ 1)) + ((d . 0 ) * (b |^ 0 ))) by A4, A3

      .= (( Sum (d1 /^ 1)) + ((d . 0 ) * 1)) by NEWTON: 4;

      consider e be XFinSequence of NAT such that

       A6: (( dom e) = ( dom (d /^ 1)) & for i be Nat st i in ( dom e) holds (e . i) = (((d /^ 1) . i) * (b |^ i))) & ( value ((d /^ 1),b)) = ( Sum e) by NUMERAL1:def 1;

      

       A7: ( dom (d1 /^ 1)) = ( len (d1 /^ 1))

      .= (( len d1) -' 1) by AFINSQ_2:def 2

      .= (( len d) -' 1) by A4

      .= ( len (d /^ 1)) by AFINSQ_2:def 2

      .= ( dom (d /^ 1));

      now

        let n1 be object;

        assume

         A8: n1 in ( dom e);

        then

        reconsider n = n1 as Nat;

        n in ( len (d /^ 1)) by A6, A8;

        then n in ( Segm (( len d) -' 1)) by AFINSQ_2:def 2;

        then (n + 1) < ((( len d) -' 1) + 1) by NAT_1: 44, XREAL_1: 8;

        then (n + 1) < ( len d) by XREAL_1: 235, A2;

        then

         A9: (n + 1) in ( Segm ( dom d)) by NAT_1: 44;

        

        thus ((d1 /^ 1) . n1) = (d1 . (n + 1)) by A7, A6, A8, AFINSQ_2:def 2

        .= ((d . (n + 1)) * (b |^ (n + 1))) by A4, A9

        .= ((d . (n + 1)) * ((b |^ n) * b)) by NEWTON: 6

        .= (b * ((d . (n + 1)) * (b |^ n)))

        .= (b * (((d /^ 1) . n) * (b |^ n))) by A8, A6, AFINSQ_2:def 2

        .= (b * (e . n1)) by A8, A6;

      end;

      then ( Sum (d1 /^ 1)) = (b * ( Sum e)) by A7, A6, Th18;

      hence thesis by Th3, A6, A5;

    end;

    theorem :: NUMERAL2:20

    

     Th20: for n,k be Nat st k = ((10 |^ (2 * n)) - 1) holds 11 divides k

    proof

      defpred P[ Nat] means ex k be Nat st k = ((10 |^ (2 * $1)) - 1) & 11 divides k;

      let n,k be Nat;

       A1:

      now

        let k be Nat;

        assume P[k];

        then

        consider l be Nat such that

         A2: l = ((10 |^ (2 * k)) - 1) and

         A3: 11 divides l;

        consider m be Nat such that

         A4: l = (11 * m) by A3, NAT_D:def 3;

        ((10 |^ (2 * (k + 1))) - 1) = ((10 |^ ((2 * k) + 2)) - 1)

        .= ((((11 * m) + 1) * (10 |^ (1 + 1))) - 1) by A2, A4, NEWTON: 8

        .= ((((11 * m) + 1) * ((10 |^ 1) * 10)) - 1) by NEWTON: 6

        .= ((((11 * m) + 1) * (10 * 10)) - 1)

        .= (11 * ((m * 100) + 9));

        hence P[(k + 1)] by NAT_D:def 3;

      end;

      ((10 |^ 0 ) - 1) = (1 - 1) by NEWTON: 4

      .= 0 ;

      then

       A5: P[ 0 ] by NAT_D: 6;

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

      then

       A6: ex l be Nat st l = ((10 |^ (2 * n)) - 1) & 11 divides l;

      assume k = ((10 |^ (2 * n)) - 1);

      hence thesis by A6;

    end;

    theorem :: NUMERAL2:21

    

     Th21: for n,k be Nat st k = ((10 |^ ((2 * n) + 1)) + 1) holds 11 divides k

    proof

      defpred P[ Nat] means ex k be Nat st k = ((10 |^ ((2 * $1) + 1)) + 1) & 11 divides k;

      let n,k be Nat;

       A1:

      now

        let k be Nat;

        assume P[k];

        then

        consider l be Nat such that

         A2: l = ((10 |^ ((2 * k) + 1)) + 1) and

         A3: 11 divides l;

        consider m be Nat such that

         A4: l = (11 * m) by A3, NAT_D:def 3;

        ((10 |^ ((2 * (k + 1)) + 1)) + 1) = ((10 |^ (((2 * k) + 1) + 2)) + 1)

        .= ((((11 * m) - 1) * (10 |^ (1 + 1))) + 1) by A2, A4, NEWTON: 8

        .= ((((11 * m) - 1) * ((10 |^ 1) * 10)) + 1) by NEWTON: 6

        .= ((((11 * m) - 1) * (10 * 10)) + 1)

        .= (11 * ((m * 100) - 9));

        hence P[(k + 1)] by INT_1:def 3;

      end;

      

       A5: P[ 0 ];

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

      then

       A6: ex l be Nat st l = ((10 |^ ((2 * n) + 1)) + 1) & 11 divides l;

      assume k = ((10 |^ ((2 * n) + 1)) + 1);

      hence thesis by A6;

    end;

    theorem :: NUMERAL2:22

    

     Th22: (7,10) are_coprime

    proof

      (2,7) are_coprime & (5,7) are_coprime by NAT_4: 26, EULER_1: 2;

      then ((2 * 5),7) are_coprime by INT_2: 26;

      hence thesis;

    end;

    

     Lm1: for n be Element of NAT st 1 < n & n < 5 & n is prime holds n = 2 or n = 3

    proof

      let n be Element of NAT ;

      assume that

       A1: 1 < n & n < 5 and

       A2: n is prime;

      (1 + 1) < (n + 1) & n < (4 + 1) by A1, XREAL_1: 6;

      then 2 <= n & n <= (2 + 1) or 3 <= n & n <= (3 + 1) by NAT_1: 13;

      hence thesis by A2, INT_2: 29, NAT_1: 9;

    end;

    

     Lm2: not 6 is prime & not 8 is prime & not 9 is prime & not 10 is prime & not 12 is prime & not 14 is prime & not 15 is prime & not 16 is prime & not 18 is prime & not 20 is prime & not 21 is prime & not 22 is prime & not 24 is prime & not 25 is prime & not 26 is prime & not 27 is prime & not 28 is prime

    proof

      6 = (2 * 3);

      then 2 divides 6 by NAT_D:def 3;

      hence not 6 is prime by INT_2:def 4;

      8 = (2 * 4);

      then 2 divides 8 by NAT_D:def 3;

      hence not 8 is prime by INT_2:def 4;

      9 = (3 * 3);

      then 3 divides 9 by NAT_D:def 3;

      hence not 9 is prime by INT_2:def 4;

      10 = (2 * 5);

      then 2 divides 10 by NAT_D:def 3;

      hence not 10 is prime by INT_2:def 4;

      12 = (2 * 6);

      then 2 divides 12 by NAT_D:def 3;

      hence not 12 is prime by INT_2:def 4;

      14 = (2 * 7);

      then 2 divides 14 by NAT_D:def 3;

      hence not 14 is prime by INT_2:def 4;

      15 = (3 * 5);

      then 3 divides 15 by NAT_D:def 3;

      hence not 15 is prime by INT_2:def 4;

      16 = (4 * 4);

      then 4 divides 16 by NAT_D:def 3;

      hence not 16 is prime by INT_2:def 4;

      18 = (2 * 9);

      then 2 divides 18 by NAT_D:def 3;

      hence not 18 is prime by INT_2:def 4;

      20 = (4 * 5);

      then 4 divides 20 by NAT_D:def 3;

      hence not 20 is prime by INT_2:def 4;

      21 = (3 * 7);

      then 3 divides 21 by NAT_D:def 3;

      hence not 21 is prime by INT_2:def 4;

      22 = (2 * 11);

      then 2 divides 22 by NAT_D:def 3;

      hence not 22 is prime by INT_2:def 4;

      24 = (4 * 6);

      then 4 divides 24 by NAT_D:def 3;

      hence not 24 is prime by INT_2:def 4;

      25 = (5 * 5);

      then 5 divides 25 by NAT_D:def 3;

      hence not 25 is prime by INT_2:def 4;

      26 = (2 * 13);

      then 2 divides 26 by NAT_D:def 3;

      hence not 26 is prime by INT_2:def 4;

      27 = (3 * 9);

      then 3 divides 27 by NAT_D:def 3;

      hence not 27 is prime by INT_2:def 4;

      28 = (4 * 7);

      then 4 divides 28 by NAT_D:def 3;

      hence thesis by INT_2:def 4;

    end;

    

     Lm3: for n be Element of NAT st 1 < n & n < 29 & n is prime holds n = 2 or n = 3 or n = 5 or n = 7 or n = 11 or n = 13 or n = 17 or n = 19 or n = 23

    proof

      let n be Element of NAT ;

      assume that

       A1: 1 < n and

       A2: n < 29 and

       A3: n is prime;

      

       A4: (1 + 1) < (n + 1) & n < (28 + 1) by A1, A2, XREAL_1: 6;

      per cases by A4, NAT_1: 13;

        suppose 2 <= n & n < 5;

        hence thesis by A1, A3, Lm1;

      end;

        suppose

         A5: 5 <= n & n <= (27 + 1);

        per cases by A5;

          suppose 5 <= n & n <= (12 + 1);

          then 5 <= n & n <= (5 + 1) or 6 <= n & n <= (6 + 1) or 7 <= n & n <= (7 + 1) or 8 <= n & n <= (8 + 1) or 9 <= n & n <= (9 + 1) or 10 <= n & n <= (10 + 1) or 11 <= n & n <= (11 + 1) or 12 <= n & n <= (12 + 1);

          hence thesis by A3, Lm2, NAT_1: 9;

        end;

          suppose 13 <= n & n <= (20 + 1);

          then 13 <= n & n <= (13 + 1) or 14 <= n & n <= (14 + 1) or 15 <= n & n <= (15 + 1) or 16 <= n & n <= (16 + 1) or 17 <= n & n <= (17 + 1) or 18 <= n & n <= (18 + 1) or 19 <= n & n <= (19 + 1) or 20 <= n & n <= (20 + 1);

          hence thesis by A3, Lm2, NAT_1: 9;

        end;

          suppose 21 <= n & n <= (27 + 1);

          then 21 <= n & n <= (21 + 1) or 22 <= n & n <= (22 + 1) or 23 <= n & n <= (23 + 1) or 24 <= n & n <= (24 + 1) or 25 <= n & n <= (25 + 1) or 26 <= n & n <= (26 + 1) or 27 <= n & n <= (27 + 1);

          hence thesis by A3, Lm2, NAT_1: 9;

        end;

      end;

    end;

    

     Lm4: for k be Element of NAT st k < 841 holds for n be Element of NAT st 1 < n & (n * n) <= k & n is prime holds n = 2 or n = 3 or n = 5 or n = 7 or n = 11 or n = 13 or n = 17 or n = 19 or n = 23

    proof

      let k be Element of NAT ;

      assume

       A1: k < 841;

      let n be Element of NAT ;

      assume that

       A2: 1 < n and

       A3: (n * n) <= k and

       A4: n is prime;

      (n * n) < (29 * 29) by A1, A3, XXREAL_0: 2;

      then n < 29 by NAT_4: 1;

      hence thesis by A2, A4, Lm3;

    end;

    theorem :: NUMERAL2:23

    

     Th23: 29 is prime

    proof

      now

        let n be Element of NAT ;

        29 = ((2 * 14) + 1);

        then

         A1: not 2 divides 29 by NAT_4: 9;

        29 = ((3 * 9) + 2);

        then

         A2: not 3 divides 29 by NAT_4: 9;

        29 = ((5 * 5) + 4);

        then

         A3: not 5 divides 29 by NAT_4: 9;

        29 = ((7 * 4) + 1);

        then

         A4: not 7 divides 29 by NAT_4: 9;

        29 = ((11 * 2) + 7);

        then

         A5: not 11 divides 29 by NAT_4: 9;

        29 = ((13 * 2) + 3);

        then

         A6: not 13 divides 29 by NAT_4: 9;

        29 = ((17 * 1) + 12);

        then

         A7: not 17 divides 29 by NAT_4: 9;

        29 = ((19 * 1) + 10);

        then

         A8: not 19 divides 29 by NAT_4: 9;

        29 = ((23 * 1) + 6);

        then

         A9: not 23 divides 29 by NAT_4: 9;

        assume 1 < n & (n * n) <= 29 & n is prime;

        hence not n divides 29 by A1, A2, A9, A8, A4, A3, A6, A5, A7, Lm4;

      end;

      hence thesis by NAT_4: 14;

    end;

    theorem :: NUMERAL2:24

    

     Th24: 31 is prime

    proof

      now

        let n be Element of NAT ;

        31 = ((2 * 15) + 1);

        then

         A1: not 2 divides 31 by NAT_4: 9;

        31 = ((3 * 10) + 1);

        then

         A2: not 3 divides 31 by NAT_4: 9;

        31 = ((5 * 6) + 1);

        then

         A3: not 5 divides 31 by NAT_4: 9;

        31 = ((7 * 4) + 3);

        then

         A4: not 7 divides 31 by NAT_4: 9;

        31 = ((11 * 2) + 9);

        then

         A5: not 11 divides 31 by NAT_4: 9;

        31 = ((13 * 2) + 5);

        then

         A6: not 13 divides 31 by NAT_4: 9;

        31 = ((17 * 1) + 14);

        then

         A7: not 17 divides 31 by NAT_4: 9;

        31 = ((19 * 1) + 12);

        then

         A8: not 19 divides 31 by NAT_4: 9;

        31 = ((23 * 1) + 8);

        then

         A9: not 23 divides 31 by NAT_4: 9;

        assume 1 < n & (n * n) <= 31 & n is prime;

        hence not n divides 31 by A1, A2, A9, A8, A4, A3, A6, A5, A7, Lm4;

      end;

      hence thesis by NAT_4: 14;

    end;

    theorem :: NUMERAL2:25

    

     Th25: 41 is prime

    proof

      now

        let n be Element of NAT ;

        41 = ((2 * 20) + 1);

        then

         A1: not 2 divides 41 by NAT_4: 9;

        41 = ((3 * 13) + 2);

        then

         A2: not 3 divides 41 by NAT_4: 9;

        41 = ((5 * 8) + 1);

        then

         A3: not 5 divides 41 by NAT_4: 9;

        41 = ((7 * 5) + 6);

        then

         A4: not 7 divides 41 by NAT_4: 9;

        41 = ((11 * 3) + 8);

        then

         A5: not 11 divides 41 by NAT_4: 9;

        41 = ((13 * 3) + 2);

        then

         A6: not 13 divides 41 by NAT_4: 9;

        41 = ((17 * 2) + 7);

        then

         A7: not 17 divides 41 by NAT_4: 9;

        41 = ((19 * 2) + 3);

        then

         A8: not 19 divides 41 by NAT_4: 9;

        41 = ((23 * 1) + 18);

        then

         A9: not 23 divides 41 by NAT_4: 9;

        assume 1 < n & (n * n) <= 41 & n is prime;

        hence not n divides 41 by A1, A2, A3, A4, A5, A6, A7, A8, A9, Lm4;

      end;

      hence thesis by NAT_4: 14;

    end;

    theorem :: NUMERAL2:26

    

     Th26: 47 is prime

    proof

      now

        let n be Element of NAT ;

        47 = ((2 * 23) + 1);

        then

         A1: not 2 divides 47 by NAT_4: 9;

        47 = ((3 * 15) + 2);

        then

         A2: not 3 divides 47 by NAT_4: 9;

        47 = ((5 * 9) + 2);

        then

         A3: not 5 divides 47 by NAT_4: 9;

        47 = ((7 * 6) + 5);

        then

         A4: not 7 divides 47 by NAT_4: 9;

        47 = ((11 * 4) + 3);

        then

         A5: not 11 divides 47 by NAT_4: 9;

        47 = ((13 * 3) + 8);

        then

         A6: not 13 divides 47 by NAT_4: 9;

        47 = ((17 * 2) + 13);

        then

         A7: not 17 divides 47 by NAT_4: 9;

        47 = ((19 * 2) + 9);

        then

         A8: not 19 divides 47 by NAT_4: 9;

        47 = ((23 * 2) + 1);

        then

         A9: not 23 divides 47 by NAT_4: 9;

        assume 1 < n & (n * n) <= 47 & n is prime;

        hence not n divides 47 by A1, A2, A3, A4, A5, A6, A7, A8, A9, Lm4;

      end;

      hence thesis by NAT_4: 14;

    end;

    theorem :: NUMERAL2:27

    

     Th27: 53 is prime

    proof

      now

        let n be Element of NAT ;

        53 = ((2 * 26) + 1);

        then

         A1: not 2 divides 53 by NAT_4: 9;

        53 = ((3 * 17) + 2);

        then

         A2: not 3 divides 53 by NAT_4: 9;

        53 = ((5 * 10) + 3);

        then

         A3: not 5 divides 53 by NAT_4: 9;

        53 = ((7 * 7) + 4);

        then

         A4: not 7 divides 53 by NAT_4: 9;

        53 = ((11 * 4) + 9);

        then

         A5: not 11 divides 53 by NAT_4: 9;

        53 = ((13 * 4) + 1);

        then

         A6: not 13 divides 53 by NAT_4: 9;

        53 = ((17 * 3) + 2);

        then

         A7: not 17 divides 53 by NAT_4: 9;

        53 = ((19 * 2) + 15);

        then

         A8: not 19 divides 53 by NAT_4: 9;

        53 = ((23 * 2) + 7);

        then

         A9: not 23 divides 53 by NAT_4: 9;

        assume 1 < n & (n * n) <= 53 & n is prime;

        hence not n divides 53 by A1, A2, A3, A4, A5, A6, A7, A8, A9, Lm4;

      end;

      hence thesis by NAT_4: 14;

    end;

    theorem :: NUMERAL2:28

    

     Th28: 59 is prime

    proof

      now

        let n be Element of NAT ;

        59 = ((2 * 29) + 1);

        then

         A1: not 2 divides 59 by NAT_4: 9;

        59 = ((3 * 19) + 2);

        then

         A2: not 3 divides 59 by NAT_4: 9;

        59 = ((5 * 11) + 4);

        then

         A3: not 5 divides 59 by NAT_4: 9;

        59 = ((7 * 8) + 3);

        then

         A4: not 7 divides 59 by NAT_4: 9;

        59 = ((11 * 5) + 4);

        then

         A5: not 11 divides 59 by NAT_4: 9;

        59 = ((13 * 4) + 7);

        then

         A6: not 13 divides 59 by NAT_4: 9;

        59 = ((17 * 3) + 8);

        then

         A7: not 17 divides 59 by NAT_4: 9;

        59 = ((19 * 3) + 2);

        then

         A8: not 19 divides 59 by NAT_4: 9;

        59 = ((23 * 2) + 13);

        then

         A9: not 23 divides 59 by NAT_4: 9;

        assume 1 < n & (n * n) <= 59 & n is prime;

        hence not n divides 59 by A1, A2, A3, A4, A5, A6, A7, A8, A9, Lm4;

      end;

      hence thesis by NAT_4: 14;

    end;

    theorem :: NUMERAL2:29

    

     Th29: 61 is prime

    proof

      now

        let n be Element of NAT ;

        61 = ((2 * 30) + 1);

        then

         A1: not 2 divides 61 by NAT_4: 9;

        61 = ((3 * 20) + 1);

        then

         A2: not 3 divides 61 by NAT_4: 9;

        61 = ((5 * 12) + 1);

        then

         A3: not 5 divides 61 by NAT_4: 9;

        61 = ((7 * 8) + 5);

        then

         A4: not 7 divides 61 by NAT_4: 9;

        61 = ((11 * 5) + 6);

        then

         A5: not 11 divides 61 by NAT_4: 9;

        61 = ((13 * 4) + 9);

        then

         A6: not 13 divides 61 by NAT_4: 9;

        61 = ((17 * 3) + 10);

        then

         A7: not 17 divides 61 by NAT_4: 9;

        61 = ((19 * 3) + 4);

        then

         A8: not 19 divides 61 by NAT_4: 9;

        61 = ((23 * 2) + 15);

        then

         A9: not 23 divides 61 by NAT_4: 9;

        assume 1 < n & (n * n) <= 61 & n is prime;

        hence not n divides 61 by A1, A2, A3, A4, A5, A6, A7, A8, A9, Lm4;

      end;

      hence thesis by NAT_4: 14;

    end;

    theorem :: NUMERAL2:30

    

     Th30: 67 is prime

    proof

      now

        let n be Element of NAT ;

        67 = ((2 * 33) + 1);

        then

         A1: not 2 divides 67 by NAT_4: 9;

        67 = ((3 * 22) + 1);

        then

         A2: not 3 divides 67 by NAT_4: 9;

        67 = ((5 * 13) + 2);

        then

         A3: not 5 divides 67 by NAT_4: 9;

        67 = ((7 * 9) + 4);

        then

         A4: not 7 divides 67 by NAT_4: 9;

        67 = ((11 * 6) + 1);

        then

         A5: not 11 divides 67 by NAT_4: 9;

        67 = ((13 * 5) + 2);

        then

         A6: not 13 divides 67 by NAT_4: 9;

        67 = ((17 * 3) + 16);

        then

         A7: not 17 divides 67 by NAT_4: 9;

        67 = ((19 * 3) + 10);

        then

         A8: not 19 divides 67 by NAT_4: 9;

        67 = ((23 * 2) + 21);

        then

         A9: not 23 divides 67 by NAT_4: 9;

        assume 1 < n & (n * n) <= 67 & n is prime;

        hence not n divides 67 by A1, A2, A3, A4, A5, A6, A7, A8, A9, Lm4;

      end;

      hence thesis by NAT_4: 14;

    end;

    theorem :: NUMERAL2:31

    

     Th31: 71 is prime

    proof

      now

        let n be Element of NAT ;

        71 = ((2 * 35) + 1);

        then

         A1: not 2 divides 71 by NAT_4: 9;

        71 = ((3 * 23) + 2);

        then

         A2: not 3 divides 71 by NAT_4: 9;

        71 = ((5 * 14) + 1);

        then

         A3: not 5 divides 71 by NAT_4: 9;

        71 = ((7 * 10) + 1);

        then

         A4: not 7 divides 71 by NAT_4: 9;

        71 = ((11 * 6) + 5);

        then

         A5: not 11 divides 71 by NAT_4: 9;

        71 = ((13 * 5) + 6);

        then

         A6: not 13 divides 71 by NAT_4: 9;

        71 = ((17 * 4) + 3);

        then

         A7: not 17 divides 71 by NAT_4: 9;

        71 = ((19 * 3) + 14);

        then

         A8: not 19 divides 71 by NAT_4: 9;

        71 = ((23 * 3) + 2);

        then

         A9: not 23 divides 71 by NAT_4: 9;

        assume 1 < n & (n * n) <= 71 & n is prime;

        hence not n divides 71 by A1, A2, A3, A4, A5, A6, A7, A8, A9, Lm4;

      end;

      hence thesis by NAT_4: 14;

    end;

    theorem :: NUMERAL2:32

    

     Th32: 73 is prime

    proof

      now

        let n be Element of NAT ;

        73 = ((2 * 36) + 1);

        then

         A1: not 2 divides 73 by NAT_4: 9;

        73 = ((3 * 24) + 1);

        then

         A2: not 3 divides 73 by NAT_4: 9;

        73 = ((5 * 14) + 3);

        then

         A3: not 5 divides 73 by NAT_4: 9;

        73 = ((7 * 10) + 3);

        then

         A4: not 7 divides 73 by NAT_4: 9;

        73 = ((11 * 6) + 7);

        then

         A5: not 11 divides 73 by NAT_4: 9;

        73 = ((13 * 5) + 8);

        then

         A6: not 13 divides 73 by NAT_4: 9;

        73 = ((17 * 4) + 5);

        then

         A7: not 17 divides 73 by NAT_4: 9;

        73 = ((19 * 3) + 16);

        then

         A8: not 19 divides 73 by NAT_4: 9;

        73 = ((23 * 3) + 4);

        then

         A9: not 23 divides 73 by NAT_4: 9;

        assume 1 < n & (n * n) <= 73 & n is prime;

        hence not n divides 73 by A1, A2, A3, A4, A5, A6, A7, A8, A9, Lm4;

      end;

      hence thesis by NAT_4: 14;

    end;

    theorem :: NUMERAL2:33

    

     Th33: 79 is prime

    proof

      now

        let n be Element of NAT ;

        79 = ((2 * 39) + 1);

        then

         A1: not 2 divides 79 by NAT_4: 9;

        79 = ((3 * 26) + 1);

        then

         A2: not 3 divides 79 by NAT_4: 9;

        79 = ((5 * 15) + 4);

        then

         A3: not 5 divides 79 by NAT_4: 9;

        79 = ((7 * 11) + 2);

        then

         A4: not 7 divides 79 by NAT_4: 9;

        79 = ((11 * 7) + 2);

        then

         A5: not 11 divides 79 by NAT_4: 9;

        79 = ((13 * 6) + 1);

        then

         A6: not 13 divides 79 by NAT_4: 9;

        79 = ((17 * 4) + 11);

        then

         A7: not 17 divides 79 by NAT_4: 9;

        79 = ((19 * 4) + 3);

        then

         A8: not 19 divides 79 by NAT_4: 9;

        79 = ((23 * 3) + 10);

        then

         A9: not 23 divides 79 by NAT_4: 9;

        assume 1 < n & (n * n) <= 79 & n is prime;

        hence not n divides 79 by A1, A2, A3, A4, A5, A6, A7, A8, A9, Lm4;

      end;

      hence thesis by NAT_4: 14;

    end;

    theorem :: NUMERAL2:34

    

     Th34: 89 is prime

    proof

      now

        let n be Element of NAT ;

        89 = ((2 * 44) + 1);

        then

         A1: not 2 divides 89 by NAT_4: 9;

        89 = ((3 * 29) + 2);

        then

         A2: not 3 divides 89 by NAT_4: 9;

        89 = ((5 * 17) + 4);

        then

         A3: not 5 divides 89 by NAT_4: 9;

        89 = ((7 * 12) + 5);

        then

         A4: not 7 divides 89 by NAT_4: 9;

        89 = ((11 * 8) + 1);

        then

         A5: not 11 divides 89 by NAT_4: 9;

        89 = ((13 * 6) + 11);

        then

         A6: not 13 divides 89 by NAT_4: 9;

        89 = ((17 * 5) + 4);

        then

         A7: not 17 divides 89 by NAT_4: 9;

        89 = ((19 * 4) + 13);

        then

         A8: not 19 divides 89 by NAT_4: 9;

        89 = ((23 * 3) + 20);

        then

         A9: not 23 divides 89 by NAT_4: 9;

        assume 1 < n & (n * n) <= 89 & n is prime;

        hence not n divides 89 by A1, A2, A3, A4, A5, A6, A7, A8, A9, Lm4;

      end;

      hence thesis by NAT_4: 14;

    end;

    theorem :: NUMERAL2:35

    

     Th35: 97 is prime

    proof

      now

        let n be Element of NAT ;

        97 = ((2 * 48) + 1);

        then

         A1: not 2 divides 97 by NAT_4: 9;

        97 = ((3 * 32) + 1);

        then

         A2: not 3 divides 97 by NAT_4: 9;

        97 = ((5 * 19) + 2);

        then

         A3: not 5 divides 97 by NAT_4: 9;

        97 = ((7 * 13) + 6);

        then

         A4: not 7 divides 97 by NAT_4: 9;

        97 = ((11 * 8) + 9);

        then

         A5: not 11 divides 97 by NAT_4: 9;

        97 = ((13 * 7) + 6);

        then

         A6: not 13 divides 97 by NAT_4: 9;

        97 = ((17 * 5) + 12);

        then

         A7: not 17 divides 97 by NAT_4: 9;

        97 = ((19 * 5) + 2);

        then

         A8: not 19 divides 97 by NAT_4: 9;

        97 = ((23 * 4) + 5);

        then

         A9: not 23 divides 97 by NAT_4: 9;

        assume 1 < n & (n * n) <= 97 & n is prime;

        hence not n divides 97 by A1, A2, A3, A4, A5, A6, A7, A8, A9, Lm4;

      end;

      hence thesis by NAT_4: 14;

    end;

    theorem :: NUMERAL2:36

    

     Th36: 101 is prime

    proof

      now

        let n be Element of NAT ;

        101 = ((2 * 50) + 1);

        then

         A1: not 2 divides 101 by NAT_4: 9;

        101 = ((3 * 33) + 2);

        then

         A2: not 3 divides 101 by NAT_4: 9;

        101 = ((5 * 20) + 1);

        then

         A3: not 5 divides 101 by NAT_4: 9;

        101 = ((7 * 14) + 3);

        then

         A4: not 7 divides 101 by NAT_4: 9;

        101 = ((11 * 9) + 2);

        then

         A5: not 11 divides 101 by NAT_4: 9;

        101 = ((13 * 7) + 10);

        then

         A6: not 13 divides 101 by NAT_4: 9;

        101 = ((17 * 5) + 16);

        then

         A7: not 17 divides 101 by NAT_4: 9;

        101 = ((19 * 5) + 6);

        then

         A8: not 19 divides 101 by NAT_4: 9;

        101 = ((23 * 4) + 9);

        then

         A9: not 23 divides 101 by NAT_4: 9;

        assume 1 < n & (n * n) <= 101 & n is prime;

        hence not n divides 101 by A1, A2, A3, A4, A5, A6, A7, A8, A9, Lm4;

      end;

      hence thesis by NAT_4: 14;

    end;

    begin

    theorem :: NUMERAL2:37

    

     Th37: for p be prime Nat, n,f,b be Nat st (ex k be Nat st ((b * f) + 1) = (p * k)) & b > 1 & (p,b) are_coprime holds p divides n iff p divides (( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b)) - (f * (( digits (n,b)) . 0 )))

    proof

      let p be prime Nat, n,f,b be Nat such that

       A1: ex k be Nat st ((b * f) + 1) = (p * k) and

       A2: b > 1 and

       A3: (p,b) are_coprime ;

      consider k be Nat such that

       A4: ((b * f) + 1) = (p * k) by A1;

      thus p divides n implies p divides (( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b)) - (f * (( digits (n,b)) . 0 )))

      proof

        assume p divides n;

        then

        consider i be Nat such that

         A5: n = (p * i) by NAT_D:def 3;

        

         A6: ((b * ( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b))) + (( digits (n,b)) . 0 )) = (p * i) by A2, A5, Th19;

        ((p * k) * (( digits (n,b)) . 0 )) = (((b * f) + 1) * (( digits (n,b)) . 0 )) by A4;

        then

         A7: ((b * (( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b)) - (f * (( digits (n,b)) . 0 )))) / b) = ((p * (i - (k * (( digits (n,b)) . 0 )))) / b) by A6;

        then (( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b)) - (f * (( digits (n,b)) . 0 ))) = ((p * (i - (k * (( digits (n,b)) . 0 )))) / b) by A2, XCMPLX_1: 89;

        then b divides (p * (i - (k * (( digits (n,b)) . 0 )))) by A2, WSIERP_1: 17;

        then

        consider j be Integer such that

         A8: (i - (k * (( digits (n,b)) . 0 ))) = (b * j) by A3, INT_2: 25, INT_1:def 3;

        (( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b)) - (f * (( digits (n,b)) . 0 ))) = ((p * (b * j)) / b) by A8, A7, A2, XCMPLX_1: 89

        .= ((p * j) * (b / b))

        .= ((p * j) * 1) by A2, XCMPLX_1: 60;

        hence p divides (( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b)) - (f * (( digits (n,b)) . 0 ))) by INT_1:def 3;

      end;

      assume p divides (( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b)) - (f * (( digits (n,b)) . 0 )));

      then

      consider i be Integer such that

       A9: (( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b)) - (f * (( digits (n,b)) . 0 ))) = (p * i) by INT_1:def 3;

      n = ((b * ((p * i) + (f * (( digits (n,b)) . 0 )))) + (( digits (n,b)) . 0 )) by A2, A9, Th19

      .= (((b * p) * i) + (((b * f) + 1) * (( digits (n,b)) . 0 )))

      .= (((b * p) * i) + ((p * k) * (( digits (n,b)) . 0 ))) by A4

      .= (p * ((b * i) + (k * (( digits (n,b)) . 0 ))));

      hence p divides n by INT_1:def 3;

    end;

    theorem :: NUMERAL2:38

    

     Th38: for p be prime Nat, n,f,b be Nat st (ex k be Nat st ((b * f) - 1) = (p * k)) & b > 1 & (p,b) are_coprime holds p divides n iff p divides (( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b)) + (f * (( digits (n,b)) . 0 )))

    proof

      let p be prime Nat, n,f,b be Nat such that

       A1: ex k be Nat st ((b * f) - 1) = (p * k) and

       A2: b > 1 and

       A3: (p,b) are_coprime ;

      consider k be Nat such that

       A4: ((b * f) - 1) = (p * k) by A1;

      thus p divides n implies p divides (( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b)) + (f * (( digits (n,b)) . 0 )))

      proof

        assume p divides n;

        then

        consider i be Nat such that

         A5: n = (p * i) by NAT_D:def 3;

        

         A6: ((b * ( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b))) + (( digits (n,b)) . 0 )) = (p * i) by A2, A5, Th19;

        ((p * k) * (( digits (n,b)) . 0 )) = (((b * f) - 1) * (( digits (n,b)) . 0 )) by A4;

        then

         A7: ((b * (( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b)) + (f * (( digits (n,b)) . 0 )))) / b) = ((p * (i + (k * (( digits (n,b)) . 0 )))) / b) by A6;

        then (( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b)) + (f * (( digits (n,b)) . 0 ))) = ((p * (i + (k * (( digits (n,b)) . 0 )))) / b) by A2, XCMPLX_1: 89;

        then b divides (p * (i + (k * (( digits (n,b)) . 0 )))) by A2, WSIERP_1: 17;

        then

        consider j be Integer such that

         A8: (i + (k * (( digits (n,b)) . 0 ))) = (b * j) by A3, INT_2: 25, INT_1:def 3;

        (( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b)) + (f * (( digits (n,b)) . 0 ))) = ((p * (b * j)) / b) by A8, A7, A2, XCMPLX_1: 89

        .= ((p * j) * (b / b))

        .= ((p * j) * 1) by A2, XCMPLX_1: 60;

        hence p divides (( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b)) + (f * (( digits (n,b)) . 0 ))) by INT_1:def 3;

      end;

      assume p divides (( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b)) + (f * (( digits (n,b)) . 0 )));

      then

      consider i be Integer such that

       A9: (( value (( mid (( digits (n,b)),2,( len ( digits (n,b))))),b)) + (f * (( digits (n,b)) . 0 ))) = (p * i) by INT_1:def 3;

      n = ((b * ((p * i) - (f * (( digits (n,b)) . 0 )))) + (( digits (n,b)) . 0 )) by A2, A9, Th19

      .= (((b * p) * i) - (((b * f) - 1) * (( digits (n,b)) . 0 )))

      .= (((b * p) * i) - ((p * k) * (( digits (n,b)) . 0 ))) by A4

      .= (p * ((b * i) - (k * (( digits (n,b)) . 0 ))));

      hence p divides n by INT_1:def 3;

    end;

    ::$Notion-Name

    theorem :: NUMERAL2:39

    

     Th39: 7 divides n iff 7 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) - (2 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 7 as prime Nat by NAT_4: 26;

      ((10 * 2) + 1) = (p * 3);

      hence thesis by Th37, Th22;

    end;

    theorem :: NUMERAL2:40

    7 divides n iff 7 divides (( value ((( digits (n,10)) /^ 1),10)) - (2 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th39;

    end;

    theorem :: NUMERAL2:41

    

     Th41: 11 divides n iff 11 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) - (( digits (n,10)) . 0 ))

    proof

      reconsider p = 11 as prime Nat by NAT_4: 27;

      

       A1: ((10 * 1) + 1) = (p * 1);

      (p,10) are_coprime by EULER_1: 2;

      then 11 divides n iff 11 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) - (1 * (( digits (n,10)) . 0 ))) by Th37, A1;

      hence thesis;

    end;

    theorem :: NUMERAL2:42

    11 divides n iff 11 divides (( value ((( digits (n,10)) /^ 1),10)) - (( digits (n,10)) . 0 ))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th41;

    end;

    ::$Notion-Name

    theorem :: NUMERAL2:43

    11 divides n iff 11 divides (( Sum ( SubXFinS (( digits (n,10)), EvenNAT ))) - ( Sum ( SubXFinS (( digits (n,10)), OddNAT ))))

    proof

      set d = ( digits (n,10));

      consider p be XFinSequence of NAT such that

       A1: ( dom p) = ( dom d) and

       A2: for i be Nat st i in ( dom p) holds (p . i) = ((d . i) * (10 |^ i)) and

       A3: ( value (d,10)) = ( Sum p) by NUMERAL1:def 1;

      set pe = ( SubXFinS (p, EvenNAT ));

      set po = ( SubXFinS (p, OddNAT ));

      

       A4: (( Sum pe) + ( Sum po)) = ( Sum ( SubXFinS (p, NAT ))) by Th10, Th7, Th8

      .= ( Sum p) by Th11;

      set de = ( SubXFinS (d, EvenNAT ));

      set dod = ( SubXFinS (d, OddNAT ));

      

       A5: ( dom pe) = ( dom ( Sgm0 ( EvenNAT /\ ( len d)))) by Th6, A1

      .= ( dom de) by Th6;

      

       A6: ( dom po) = ( dom ( Sgm0 ( OddNAT /\ ( len d)))) by Th6, A1

      .= ( dom dod) by Th6;

      

       A7: for i be Nat st i in ( dom de) holds (de . i) = (d . (2 * i))

      proof

        set se = ( Sgm0 ( EvenNAT /\ ( len d)));

        let i be Nat;

        assume

         A8: i in ( dom de);

        then

         A9: i in ( dom se) & (se . i) in ( dom d) by FUNCT_1: 11;

        

        thus (de . i) = (d . (se . i)) by A8, FUNCT_1: 12

        .= (d . (2 * i)) by A9, Th12;

      end;

      

       A10: for i be Nat st i in ( dom pe) holds (pe . i) = ((de . i) * (10 |^ (2 * i)))

      proof

        set se = ( Sgm0 ( EvenNAT /\ ( len p)));

        let i be Nat;

        assume

         A11: i in ( dom pe);

        then

         A12: i in ( dom se) & (se . i) in ( dom p) by FUNCT_1: 11;

        then

         A13: (se . i) = (2 * i) by Th12;

        

        thus (pe . i) = (p . (se . i)) by A11, FUNCT_1: 12

        .= ((d . (2 * i)) * (10 |^ (2 * i))) by A12, A13, A2

        .= ((de . i) * (10 |^ (2 * i))) by A12, A1, FUNCT_1: 11, A7;

      end;

      

       A14: for i be Nat st i in ( dom dod) holds (dod . i) = (d . ((2 * i) + 1))

      proof

        set so = ( Sgm0 ( OddNAT /\ ( len d)));

        let i be Nat;

        assume

         A15: i in ( dom dod);

        then

         A16: i in ( dom so) & (so . i) in ( dom d) by FUNCT_1: 11;

        

        thus (dod . i) = (d . (so . i)) by A15, FUNCT_1: 12

        .= (d . ((2 * i) + 1)) by A16, Th13;

      end;

      

       A17: for i be Nat st i in ( dom po) holds (po . i) = ((dod . i) * (10 |^ ((2 * i) + 1)))

      proof

        set so = ( Sgm0 ( OddNAT /\ ( len p)));

        let i be Nat;

        assume

         A18: i in ( dom po);

        then

         A19: i in ( dom so) & (so . i) in ( dom p) by FUNCT_1: 11;

        then

         A20: (so . i) = ((2 * i) + 1) by Th13;

        

        thus (po . i) = (p . (so . i)) by A18, FUNCT_1: 12

        .= ((d . ((2 * i) + 1)) * (10 |^ ((2 * i) + 1))) by A19, A20, A2

        .= ((dod . i) * (10 |^ ((2 * i) + 1))) by A19, A1, FUNCT_1: 11, A14;

      end;

      defpred E[ set, set] means $2 = ((pe . $1) - (de . $1));

      

       A21: for k be Nat st k in ( Segm ( dom pe)) holds ex x be Element of INT st E[k, x]

      proof

        let k be Nat;

        assume k in ( Segm ( dom pe));

        take ((pe . k) - (de . k));

        thus thesis by INT_1:def 2;

      end;

      consider pede be XFinSequence of INT such that

       A22: ( dom pede) = ( Segm ( dom pe)) & for k be Nat st k in ( Segm ( dom pe)) holds E[k, (pede . k)] from STIRL2_1:sch 5( A21);

      now

        let i be Nat;

        reconsider dz = ((10 |^ (2 * i)) - 1) as Nat by NAT_1: 20, NEWTON: 83;

        assume

         A23: i in ( dom pede);

        

        then (pede . i) = ((pe . i) - (de . i)) by A22

        .= (((de . i) * (10 |^ (2 * i))) - (de . i)) by A10, A23, A22

        .= ((de . i) * dz);

        hence 11 divides (pede . i) by Th20, NAT_D: 9;

      end;

      then 11 divides ( Sum pede) by Th16;

      then

       A24: (( Sum pede) mod 11) = 0 by INT_1: 62;

      

       A25: ( len pede) = ( len de) by A22, A5;

      

       A26: ( len pede) = ( len pe) by A22;

      

       A27: for i be Nat st i in ( dom pe) holds (pe . i) = ( addint . ((pede . i),(de . i)))

      proof

        let i be Nat;

        assume

         A28: i in ( dom pe);

        

        thus ( addint . ((pede . i),(de . i))) = ((pede . i) + (de . i)) by BINOP_2:def 20

        .= (((pe . i) - (de . i)) + (de . i)) by A28, A22

        .= (pe . i);

      end;

      

       A29: ( Sum pe) = ( addint "**" pe) by AFINSQ_2: 50

      .= ( addint "**" (pede ^ de)) by A25, A26, A27, AFINSQ_2: 46

      .= ( Sum (pede ^ de)) by AFINSQ_2: 50

      .= (( Sum pede) + ( Sum de)) by AFINSQ_2: 55;

      defpred O[ set, set] means $2 = ((po . $1) + (dod . $1));

      

       A30: for k be Nat st k in ( Segm ( dom po)) holds ex x be Element of NAT st O[k, x];

      consider podo be XFinSequence of NAT such that

       A31: ( dom podo) = ( Segm ( dom po)) & for k be Nat st k in ( Segm ( dom po)) holds O[k, (podo . k)] from STIRL2_1:sch 5( A30);

      now

        let i be Nat;

        reconsider dz = ((10 |^ (2 * i)) - 1) as Nat by NAT_1: 20, NEWTON: 83;

        assume

         A32: i in ( dom podo);

        

        then (podo . i) = ((po . i) + (dod . i)) by A31

        .= (((dod . i) * (10 |^ ((2 * i) + 1))) + (dod . i)) by A17, A32, A31

        .= ((dod . i) * ((10 |^ ((2 * i) + 1)) + 1));

        hence 11 divides (podo . i) by Th21, NAT_D: 9;

      end;

      then 11 divides ( Sum podo) by Th16;

      then

       A33: (( Sum podo) mod 11) = 0 by INT_1: 62;

      set mdo = (( - 1) (#) dod);

      

       A34: ( len podo) = ( len mdo) by A31, A6, VALUED_1:def 5;

      

       A35: ( len podo) = ( len po) by A31;

      

       A36: for i be Nat st i in ( dom po) holds (po . i) = ( addint . ((podo . i),(mdo . i)))

      proof

        let i be Nat;

        assume

         A37: i in ( dom po);

        then

         A38: i in ( dom mdo) by A6, VALUED_1:def 5;

        

        thus ( addint . ((podo . i),(mdo . i))) = ((podo . i) + (mdo . i)) by BINOP_2:def 20

        .= ((podo . i) + (( - 1) * (dod . i))) by A38, VALUED_1:def 5

        .= (((po . i) + (dod . i)) - (dod . i)) by A37, A31

        .= (po . i);

      end;

      

       A39: ( Sum po) = ( addint "**" po) by AFINSQ_2: 50

      .= ( addint "**" (podo ^ mdo)) by A34, A35, A36, AFINSQ_2: 46

      .= ( Sum (podo ^ mdo)) by AFINSQ_2: 50

      .= (( Sum podo) + ( Sum mdo)) by AFINSQ_2: 55

      .= (( Sum podo) + (( - 1) * ( Sum dod))) by AFINSQ_2: 64

      .= (( Sum podo) - ( Sum dod));

      thus 11 divides n implies 11 divides (( Sum de) - ( Sum dod))

      proof

        assume 11 divides n;

        then 11 divides ( Sum p) by A3, NUMERAL1: 5;

        

        then 0 = (((( Sum pede) + ( Sum podo)) + (( Sum de) - ( Sum dod))) mod 11) by INT_1: 62, A4, A29, A39

        .= ((((( Sum pede) + ( Sum podo)) mod 11) + ((( Sum de) - ( Sum dod)) mod 11)) mod 11) by NAT_D: 66

        .= (((((( Sum pede) mod 11) + (( Sum podo) mod 11)) mod 11) + ((( Sum de) - ( Sum dod)) mod 11)) mod 11) by NAT_D: 66

        .= (( 0 qua Integer + ((( Sum de) - ( Sum dod)) mod 11)) mod 11) by A24, A33, NAT_D: 26

        .= ((( Sum de) - ( Sum dod)) mod 11) by Th14;

        hence 11 divides (( Sum de) - ( Sum dod)) by INT_1: 62;

      end;

      thus 11 divides (( Sum de) - ( Sum dod)) implies 11 divides n

      proof

        assume 11 divides (( Sum de) - ( Sum dod));

        

        then 0 = ((( Sum de) - ( Sum dod)) mod 11) by INT_1: 62

        .= (( 0 qua Integer + ((( Sum de) - ( Sum dod)) mod 11)) mod 11) by Th14

        .= (((((( Sum pede) mod 11) + (( Sum podo) mod 11)) mod 11) + ((( Sum de) - ( Sum dod)) mod 11)) mod 11) by A24, A33, NAT_D: 26

        .= ((((( Sum pede) + ( Sum podo)) mod 11) + ((( Sum de) - ( Sum dod)) mod 11)) mod 11) by NAT_D: 66

        .= (((( Sum pede) + ( Sum podo)) + (( Sum de) - ( Sum dod))) mod 11) by NAT_D: 66

        .= (n mod 11) by A4, A29, A39, A3, NUMERAL1: 5;

        hence 11 divides n by INT_1: 62;

      end;

    end;

    ::$Notion-Name

    theorem :: NUMERAL2:44

    

     Th44: 13 divides n iff 13 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) + (4 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 13 as prime Nat by NAT_4: 28;

      

       A1: ((10 * 4) - 1) = (p * 3);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th38, A1;

    end;

    theorem :: NUMERAL2:45

    13 divides n iff 13 divides (( value ((( digits (n,10)) /^ 1),10)) + (4 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th44;

    end;

    theorem :: NUMERAL2:46

    

     Th46: 17 divides n iff 17 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) - (5 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 17 as prime Nat by PEPIN: 60;

      

       A1: ((10 * 5) + 1) = (p * 3);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th37, A1;

    end;

    theorem :: NUMERAL2:47

    17 divides n iff 17 divides (( value ((( digits (n,10)) /^ 1),10)) - (5 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th46;

    end;

    theorem :: NUMERAL2:48

    

     Th48: 19 divides n iff 19 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) + (2 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 19 as prime Nat by NAT_4: 29;

      

       A1: ((10 * 2) - 1) = (p * 1);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th38, A1;

    end;

    theorem :: NUMERAL2:49

    19 divides n iff 19 divides (( value ((( digits (n,10)) /^ 1),10)) + (2 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th48;

    end;

    theorem :: NUMERAL2:50

    

     Th50: 23 divides n iff 23 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) + (7 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 23 as prime Nat by NAT_4: 30;

      

       A1: ((10 * 7) - 1) = (p * 3);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th38, A1;

    end;

    theorem :: NUMERAL2:51

    23 divides n iff 23 divides (( value ((( digits (n,10)) /^ 1),10)) + (7 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th50;

    end;

    theorem :: NUMERAL2:52

    

     Th52: 29 divides n iff 29 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) + (3 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 29 as prime Nat by Th23;

      

       A1: ((10 * 3) - 1) = (p * 1);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th38, A1;

    end;

    theorem :: NUMERAL2:53

    29 divides n iff 29 divides (( value ((( digits (n,10)) /^ 1),10)) + (3 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th52;

    end;

    theorem :: NUMERAL2:54

    

     Th54: 31 divides n iff 31 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) - (3 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 31 as prime Nat by Th24;

      

       A1: ((10 * 3) + 1) = (p * 1);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th37, A1;

    end;

    theorem :: NUMERAL2:55

    31 divides n iff 31 divides (( value ((( digits (n,10)) /^ 1),10)) - (3 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th54;

    end;

    theorem :: NUMERAL2:56

    

     Th56: 37 divides n iff 37 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) - (11 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 37 as prime Nat by NAT_4: 31;

      

       A1: ((10 * 11) + 1) = (p * 3);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th37, A1;

    end;

    theorem :: NUMERAL2:57

    37 divides n iff 37 divides (( value ((( digits (n,10)) /^ 1),10)) - (11 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th56;

    end;

    theorem :: NUMERAL2:58

    

     Th58: 41 divides n iff 41 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) - (4 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 41 as prime Nat by Th25;

      

       A1: ((10 * 4) + 1) = (p * 1);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th37, A1;

    end;

    theorem :: NUMERAL2:59

    41 divides n iff 41 divides (( value ((( digits (n,10)) /^ 1),10)) - (4 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th58;

    end;

    theorem :: NUMERAL2:60

    

     Th60: 43 divides n iff 43 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) + (13 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 43 as prime Nat by NAT_4: 32;

      

       A1: ((10 * 13) - 1) = (p * 3);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th38, A1;

    end;

    theorem :: NUMERAL2:61

    43 divides n iff 43 divides (( value ((( digits (n,10)) /^ 1),10)) + (13 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th60;

    end;

    theorem :: NUMERAL2:62

    

     Th62: 47 divides n iff 47 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) - (14 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 47 as prime Nat by Th26;

      

       A1: ((10 * 14) + 1) = (p * 3);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th37, A1;

    end;

    theorem :: NUMERAL2:63

    47 divides n iff 47 divides (( value ((( digits (n,10)) /^ 1),10)) - (14 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th62;

    end;

    theorem :: NUMERAL2:64

    

     Th64: 53 divides n iff 53 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) + (16 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 53 as prime Nat by Th27;

      

       A1: ((10 * 16) - 1) = (p * 3);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th38, A1;

    end;

    theorem :: NUMERAL2:65

    53 divides n iff 53 divides (( value ((( digits (n,10)) /^ 1),10)) + (16 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th64;

    end;

    theorem :: NUMERAL2:66

    

     Th66: 59 divides n iff 59 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) + (6 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 59 as prime Nat by Th28;

      

       A1: ((10 * 6) - 1) = (p * 1);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th38, A1;

    end;

    theorem :: NUMERAL2:67

    59 divides n iff 59 divides (( value ((( digits (n,10)) /^ 1),10)) + (6 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th66;

    end;

    theorem :: NUMERAL2:68

    

     Th68: 61 divides n iff 61 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) - (6 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 61 as prime Nat by Th29;

      

       A1: ((10 * 6) + 1) = (p * 1);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th37, A1;

    end;

    theorem :: NUMERAL2:69

    61 divides n iff 61 divides (( value ((( digits (n,10)) /^ 1),10)) - (6 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th68;

    end;

    theorem :: NUMERAL2:70

    

     Th70: 67 divides n iff 67 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) - (20 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 67 as prime Nat by Th30;

      

       A1: ((10 * 20) + 1) = (p * 3);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th37, A1;

    end;

    theorem :: NUMERAL2:71

    67 divides n iff 67 divides (( value ((( digits (n,10)) /^ 1),10)) - (20 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th70;

    end;

    theorem :: NUMERAL2:72

    

     Th72: 71 divides n iff 71 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) - (7 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 71 as prime Nat by Th31;

      

       A1: ((10 * 7) + 1) = (p * 1);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th37, A1;

    end;

    theorem :: NUMERAL2:73

    71 divides n iff 71 divides (( value ((( digits (n,10)) /^ 1),10)) - (7 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th72;

    end;

    theorem :: NUMERAL2:74

    

     Th74: 73 divides n iff 73 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) + (22 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 73 as prime Nat by Th32;

      

       A1: ((10 * 22) - 1) = (p * 3);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th38, A1;

    end;

    theorem :: NUMERAL2:75

    73 divides n iff 73 divides (( value ((( digits (n,10)) /^ 1),10)) + (22 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th74;

    end;

    theorem :: NUMERAL2:76

    

     Th76: 79 divides n iff 79 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) + (8 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 79 as prime Nat by Th33;

      

       A1: ((10 * 8) - 1) = (p * 1);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th38, A1;

    end;

    theorem :: NUMERAL2:77

    79 divides n iff 79 divides (( value ((( digits (n,10)) /^ 1),10)) + (8 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th76;

    end;

    theorem :: NUMERAL2:78

    

     Th78: 83 divides n iff 83 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) + (25 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 83 as prime Nat by NAT_4: 33;

      

       A1: ((10 * 25) - 1) = (p * 3);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th38, A1;

    end;

    theorem :: NUMERAL2:79

    83 divides n iff 83 divides (( value ((( digits (n,10)) /^ 1),10)) + (25 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th78;

    end;

    theorem :: NUMERAL2:80

    

     Th80: 89 divides n iff 89 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) + (9 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 89 as prime Nat by Th34;

      

       A1: ((10 * 9) - 1) = (p * 1);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th38, A1;

    end;

    theorem :: NUMERAL2:81

    89 divides n iff 89 divides (( value ((( digits (n,10)) /^ 1),10)) + (9 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th80;

    end;

    theorem :: NUMERAL2:82

    

     Th82: 97 divides n iff 97 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) - (29 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 97 as prime Nat by Th35;

      

       A1: ((10 * 29) + 1) = (p * 3);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th37, A1;

    end;

    theorem :: NUMERAL2:83

    97 divides n iff 97 divides (( value ((( digits (n,10)) /^ 1),10)) - (29 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th82;

    end;

    theorem :: NUMERAL2:84

    

     Th84: 101 divides n iff 101 divides (( value (( mid (( digits (n,10)),2,( len ( digits (n,10))))),10)) - (10 * (( digits (n,10)) . 0 )))

    proof

      reconsider p = 101 as prime Nat by Th36;

      

       A1: ((10 * 10) + 1) = (p * 1);

      (p,10) are_coprime by EULER_1: 2;

      hence thesis by Th37, A1;

    end;

    theorem :: NUMERAL2:85

    101 divides n iff 101 divides (( value ((( digits (n,10)) /^ 1),10)) - (10 * (( digits (n,10)) . 0 )))

    proof

      (( digits (n,10)) /^ 1) = ( mid (( digits (n,10)),2,( len ( digits (n,10))))) by Th3;

      hence thesis by Th84;

    end;