numeral1.miz



    begin

    theorem :: NUMERAL1:1

    

     Th1: for k,l,m be Nat holds ((k (#) (l GeoSeq )) | m) is XFinSequence of NAT

    proof

      let k,l,m be Nat;

      set g = ((k (#) (l GeoSeq )) | m);

      

       A1: ( dom (k (#) (l GeoSeq ))) = NAT by FUNCT_2:def 1;

      then m in ( dom (k (#) (l GeoSeq ))) by ORDINAL1:def 12;

      then m c= ( dom (k (#) (l GeoSeq ))) by A1, ORDINAL1:def 2;

      then ( dom g) = m by RELAT_1: 62;

      then

      reconsider g9 = g as XFinSequence by ORDINAL1:def 7;

      ( rng g9) c= NAT

      proof

        let a be object;

        assume a in ( rng g9);

        then

        consider o be object such that

         A2: o in ( dom g) and

         A3: a = (g . o) by FUNCT_1:def 3;

        o in ( dom (k (#) (l GeoSeq ))) by A2, RELAT_1: 57;

        then

        reconsider o as Element of NAT ;

        

         A4: (k * (l |^ o)) in NAT by ORDINAL1:def 12;

        (g . o) = ((k (#) (l GeoSeq )) . o) by A2, FUNCT_1: 47

        .= (k * ((l GeoSeq ) . o)) by SEQ_1: 9

        .= (k * (l |^ o)) by PREPOWER:def 1;

        hence thesis by A3, A4;

      end;

      hence thesis by RELAT_1:def 19;

    end;

    theorem :: NUMERAL1:2

    

     Th2: for d be XFinSequence of NAT , n be Nat 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 NAT , n be Nat 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 NAT_D: 6;

      end;

        suppose

         A2: ( len d) > 0 ;

        then

        consider f be sequence of NAT such that

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

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

         A5: ( addnat "**" 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)) = ( addnat . ((f . k),(d . (k + 1)))) by A4, A8

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

            hence thesis by A7, A8, A9, NAT_1: 13, NAT_D: 8;

          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 ( len d)) by A2, NAT_1: 44;

        then

         A11: P[ 0 ] by A1, A3;

        

         A12: ( addnat "**" d) = ( Sum d) by AFINSQ_2: 51;

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

        hence thesis by A5, A10, A12;

      end;

    end;

    theorem :: NUMERAL1:3

    

     Th3: for d,e be XFinSequence of NAT , n be Nat 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 NAT , n be Nat 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 NAT ] means for e be XFinSequence of NAT 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 NAT , l be Element of NAT st P[p] holds P[(p ^ <%l%>)]

      proof

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

        assume

         A3: P[p];

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

        proof

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

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

          let e be XFinSequence of NAT ;

          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 NAT st Q[k, x];

          consider p9 be XFinSequence of NAT 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 < ( len p9) by AFINSQ_1: 86;

            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 k < 1 by NAT_1: 44;

            then

             A12: k = 0 by 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) by AFINSQ_1: 36

            .= ( <%(l mod n)%> . k) by A12;

          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;

          

          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) by NAT_D: 22

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

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

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

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

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

        end;

      end;

      

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

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

      hence thesis by A1;

    end;

    begin

    definition

      let d be XFinSequence of NAT ;

      let b be Nat;

      :: NUMERAL1:def1

      func value (d,b) -> Nat means

      : Def1: ex d9 be XFinSequence of NAT st (( dom d9) = ( dom d) & for i be Nat st i in ( dom d9) holds (d9 . i) = ((d . i) * (b |^ i))) & it = ( Sum d9);

      existence

      proof

        deffunc F( Nat) = ((d . $1) * (b |^ $1));

        consider d9 be XFinSequence such that

         A1: ( len d9) = ( len d) & for i be Nat st i in ( len d) holds (d9 . i) = F(i) from AFINSQ_1:sch 2;

        ( rng d9) c= NAT

        proof

          let a be object;

          assume a in ( rng d9);

          then

          consider i be object such that

           A2: i in ( dom d9) and

           A3: (d9 . i) = a by FUNCT_1:def 3;

          reconsider i as Element of NAT by A2;

          a = F(i) by A1, A2, A3;

          hence thesis by ORDINAL1:def 12;

        end;

        then

        reconsider d9 as XFinSequence of NAT by RELAT_1:def 19;

        take ( Sum d9);

        thus thesis by A1;

      end;

      uniqueness

      proof

        let k,l be Nat;

        given k9 be XFinSequence of NAT such that

         A4: ( dom k9) = ( dom d) and

         A5: for i be Nat st i in ( dom k9) holds (k9 . i) = ((d . i) * (b |^ i)) and

         A6: k = ( Sum k9);

        given l9 be XFinSequence of NAT such that

         A7: ( dom l9) = ( dom d) and

         A8: for i be Nat st i in ( dom l9) holds (l9 . i) = ((d . i) * (b |^ i)) and

         A9: l = ( Sum l9);

        now

          let i be Nat;

          assume

           A10: i in ( dom d);

          

          hence (k9 . i) = ((d . i) * (b |^ i)) by A4, A5

          .= (l9 . i) by A7, A8, A10;

        end;

        hence thesis by A4, A6, A7, A9, AFINSQ_1: 8;

      end;

    end

    definition

      let n,b be Nat;

      assume

       A1: b > 1;

      ::$Notion-Name

      :: NUMERAL1:def2

      func digits (n,b) -> XFinSequence of NAT means

      : Def2: ( value (it ,b)) = n & (it . (( len it ) - 1)) <> 0 & for i be Nat st i in ( dom it ) holds 0 <= (it . i) & (it . i) < b if n <> 0

      otherwise it = <% 0 %>;

      consistency ;

      existence

      proof

        reconsider d = <% 0 %> as XFinSequence of NAT ;

        reconsider N = n, B = b as Element of NAT by ORDINAL1:def 12;

        thus n <> 0 implies ex d be XFinSequence of NAT st ( value (d,b)) = n & (d . (( len d) - 1)) <> 0 & for i be Nat st i in ( dom d) holds 0 <= (d . i) & (d . i) < b

        proof

          deffunc G( Nat, Element of NAT ) = ($2 div B);

          consider f be sequence of NAT such that

           A2: (f . 0 ) = N & for i be Nat holds (f . (i + 1)) = G(i,) from NAT_1:sch 12;

          defpred R[ Nat] means (f . $1) = 0 ;

          defpred Q[ Nat] means ex i be Nat st (f . i) = $1;

          

           A3: for k be Nat st k <> 0 & Q[k] holds ex l be Nat st l < k & Q[l]

          proof

            let k be Nat;

            assume that

             A4: k <> 0 and

             A5: Q[k];

            take l = (k div b);

            thus l < k by A1, A4, INT_1: 56;

            consider i be Nat such that

             A6: (f . i) = k by A5;

            take (i + 1);

            thus thesis by A2, A6;

          end;

          

           A7: ex k be Nat st Q[k] by A2;

           Q[ 0 ] from NAT_1:sch 7( A7, A3);

          then

           A8: ex l be Nat st R[l];

          consider l be Nat such that

           A9: R[l] & for i be Nat st R[i] holds l <= i from NAT_1:sch 5( A8);

          assume n <> 0 ;

          then

          consider m be Nat such that

           A10: (m + 1) = l by A2, A9, NAT_1: 6;

          reconsider m as Element of NAT by ORDINAL1:def 12;

          ( dom f) = NAT by FUNCT_2:def 1;

          then (m + 1) c= ( dom f) by ORDINAL1:def 2;

          then ( dom (f | (m + 1))) = (m + 1) by RELAT_1: 62;

          then

          reconsider g = (f | (m + 1)) as XFinSequence of NAT by ORDINAL1:def 7;

          defpred P[ Nat, Nat] means $2 = ((g . $1) mod b);

          

           A11: for i be Nat st i in ( Segm (m + 1)) holds ex x be Element of NAT st P[i, x];

          consider d be XFinSequence of NAT such that

           A12: ( dom d) = ( Segm (m + 1)) & for i be Nat st i in ( Segm (m + 1)) holds P[i, (d . i)] from STIRL2_1:sch 5( A11);

           A13:

          now

            let i be Nat such that l <= i;

            assume R[i];

            then (f . (i + 1)) = ( 0 div b) by A2;

            hence R[(i + 1)] by NAT_2: 2;

          end;

          

           A14: R[l] by A9;

          

           A15: for i be Nat st l <= i holds R[i] from NAT_1:sch 8( A14, A13);

           A16:

          now

            let i be Element of NAT ;

            assume m < i;

            then l <= i by A10, NAT_1: 13;

            hence (f . i) = 0 by A15;

          end;

          deffunc F( Nat) = ((d . $1) * (b |^ $1));

          consider d9 be XFinSequence such that

           A17: ( len d9) = ( len d) & for i be Nat st i in ( len d) holds (d9 . i) = F(i) from AFINSQ_1:sch 2;

          ( rng d9) c= NAT

          proof

            let a be object;

            assume a in ( rng d9);

            then

            consider i be object such that

             A18: i in ( dom d9) and

             A19: (d9 . i) = a by FUNCT_1:def 3;

            reconsider i as Element of NAT by A18;

            a = F(i) by A17, A18, A19;

            hence thesis by ORDINAL1:def 12;

          end;

          then

          reconsider d9 as XFinSequence of NAT by RELAT_1:def 19;

          consider s be sequence of NAT such that

           A20: (s . 0 ) = (d9 . 0 ) and

           A21: for i be Nat st (i + 1) < ( len d9) holds (s . (i + 1)) = ( addnat . ((s . i),(d9 . (i + 1)))) and

           A22: ( addnat "**" d9) = (s . (( len d9) - 1)) by A12, A17, AFINSQ_2:def 8;

          defpred I[ Nat] means $1 < ( len d9) implies (s . $1) = (n - ((f . ($1 + 1)) * (b |^ ($1 + 1))));

           A23:

          now

            let i be Nat;

            assume

             A24: I[i];

            now

              assume

               A25: (i + 1) < ( len d9);

              then

               A26: (i + 1) in ( dom d9) by AFINSQ_1: 86;

              

              thus (s . (i + 1)) = ( addnat . ((s . i),(d9 . (i + 1)))) by A21, A25

              .= ((n - ((f . (i + 1)) * (b |^ (i + 1)))) + (d9 . (i + 1))) by A24, A25, BINOP_2:def 23, NAT_1: 13

              .= ((n - ((f . (i + 1)) * (b |^ (i + 1)))) + ((d . (i + 1)) * (b |^ (i + 1)))) by A17, A26

              .= ((n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((g . (i + 1)) mod b) * (b |^ (i + 1)))) by A12, A17, A26

              .= ((n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) mod b) * (b |^ (i + 1)))) by A12, A17, A26, FUNCT_1: 49

              .= ((n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) - (b * ((f . (i + 1)) div B))) * (b |^ (i + 1)))) by A1, NEWTON: 63

              .= ((n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) - (b * (f . ((i + 1) + 1)))) * (b |^ (i + 1)))) by A2

              .= ((n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) * (b |^ (i + 1))) - ((f . ((i + 1) + 1)) * (b * (b |^ (i + 1))))))

              .= ((n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) * (b |^ (i + 1))) - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1))))) by NEWTON: 6

              .= (n - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1))));

            end;

            hence I[(i + 1)];

          end;

          reconsider ld = (( len d9) - 1) as Element of NAT by A12, A17;

          

           A27: 0 in ( Segm (m + 1)) by NAT_1: 44;

          

          then (d9 . 0 ) = ((d . 0 ) * (b |^ 0 )) by A12, A17

          .= (((g . 0 ) mod b) * (b |^ 0 )) by A12, A27

          .= (((f . 0 ) mod b) * (b |^ 0 )) by A27, FUNCT_1: 49

          .= ((n mod b) * 1) by A2, NEWTON: 4

          .= (N - (B * (N div B))) by A1, NEWTON: 63

          .= (n - ((n div b) * (b |^ 1)))

          .= (n - ((f . ( 0 qua Nat + 1)) * (b |^ ( 0 qua Nat + 1)))) by A2;

          then

           A28: I[ 0 ] by A20;

          for i be Nat holds I[i] from NAT_1:sch 2( A28, A23);

          

          then (s . ld) = (n - ((f . (m + 1)) * (b |^ (m + 1)))) by A12, A17, XREAL_1: 44

          .= n by A9, A10;

          then

           A29: n = ( Sum d9) by A22, AFINSQ_2: 51;

          m < l by A10, NAT_1: 13;

          then

           A30: (f . m) <> 0 by A9;

          take d;

          thus ( value (d,b)) = n by A17, A29, Def1;

          m in ( Segm (m + 1)) by NAT_1: 45;

          then

           A31: (g . m) = (f . m) by FUNCT_1: 49;

          then m < (m + 1) & (f . (m + 1)) = ((g . m) div b) by A2, NAT_1: 13;

          then

           A32: ((g . m) div b) = 0 by A16;

          (d . (( len d) - 1)) = ((g . m) mod b) by A12, NAT_1: 45

          .= (g . m) by A1, A32, NAT_2: 12, NAT_D: 24;

          hence (d . (( len d) - 1)) <> 0 by A30, A31;

          let i be Nat;

          assume i in ( dom d);

          then (d . i) = ((g . i) mod b) by A12;

          hence thesis by A1, NAT_D: 1;

        end;

        assume n = 0 ;

        take d;

        thus thesis;

      end;

      uniqueness

      proof

        reconsider b1 = (b - 1) as Element of NAT by A1, NAT_1: 20;

        let d,e be XFinSequence of NAT ;

        thus n <> 0 & (( value (d,b)) = n & (d . (( len d) - 1)) <> 0 & for i be Nat st i in ( dom d) holds 0 <= (d . i) & (d . i) < b) & (( value (e,b)) = n & (e . (( len e) - 1)) <> 0 & for i be Nat st i in ( dom e) holds 0 <= (e . i) & (e . i) < b) implies d = e

        proof

          ( log (2,b)) > ( log (2,1)) by A1, POWER: 57;

          then

           A33: ( log (2,b)) > 0 by POWER: 51;

          ( log (2,b)) > ( log (2,1)) by A1, POWER: 57;

          then

           A34: ( log (2,b)) > 0 by POWER: 51;

          

           A35: (1 - b) <> 0 by A1;

          

           A36: (1 - b) <> 0 by A1;

          reconsider g = ((b1 (#) (b GeoSeq )) | ( len d)) as XFinSequence of NAT by Th1;

          assume

           A37: n <> 0 ;

          assume that

           A38: ( value (d,b)) = n and

           A39: (d . (( len d) - 1)) <> 0 and

           A40: for i be Nat st i in ( dom d) holds 0 <= (d . i) & (d . i) < b;

          consider D be XFinSequence of NAT such that

           A41: ( dom D) = ( dom d) and

           A42: for i be Nat st i in ( dom D) holds (D . i) = ((d . i) * (b |^ i)) and

           A43: n = ( Sum D) by A38, Def1;

          ( dom d) <> {} by A39, FUNCT_1:def 2;

          then

           A44: ( len D) > 0 by A41;

          

           A45: (( len d) - 1) in ( dom d) by A39, FUNCT_1:def 2;

          then

          reconsider k = (( len d) - 1) as Element of NAT ;

          

           A46: (1 * (b |^ k)) <= ((d . k) * (b |^ k)) by A39, NAT_1: 4, NAT_1: 14;

          

           A47: (b |^ k) > 0 by A1, PREPOWER: 6;

          (D . k) = ((d . k) * (b |^ k)) by A41, A42, A45;

          then ((d . k) * (b |^ k)) <= n by A41, A43, A45, A44, AFINSQ_2: 61;

          then (b |^ k) <= n by A46, XXREAL_0: 2;

          then ( log (2,(b to_power k))) <= ( log (2,n)) by A47, PRE_FF: 10;

          then (k * ( log (2,b))) <= ( log (2,n)) by A1, POWER: 55;

          then ((k * ( log (2,b))) / ( log (2,b))) <= (( log (2,n)) / ( log (2,b))) by A34, XREAL_1: 72;

          then

           A48: k <= (( log (2,n)) / ( log (2,b))) by A34, XCMPLX_1: 89;

          g = (((b - 1) (#) (b GeoSeq )) | (k + 1));

          

          then

           A49: ( Sum g) = (( Partial_Sums ((b - 1) (#) (b GeoSeq ))) . k) by AFINSQ_2: 56

          .= (((b - 1) (#) ( Partial_Sums (b GeoSeq ))) . k) by SERIES_1: 9

          .= ((b - 1) * (( Partial_Sums (b GeoSeq )) . k)) by SEQ_1: 9

          .= ((b - 1) * ((1 - (b to_power (k + 1))) / (1 - b))) by A1, SERIES_1: 22

          .= ( - ((1 - b) * ((1 - (b |^ (k + 1))) / (1 - b))))

          .= ( - (1 - (b |^ (k + 1)))) by A36, XCMPLX_1: 87

          .= ((b |^ (k + 1)) - 1);

          

           A50: ( dom ((b - 1) (#) (b GeoSeq ))) = NAT by FUNCT_2:def 1;

          then

           A51: ( len D) = ( len g) by A41, RELAT_1: 62;

          ( len d) c= ( dom ((b - 1) (#) (b GeoSeq ))) by A50, ORDINAL1:def 2;

          then

           A52: ( dom g) = ( len d) by RELAT_1: 62;

          

           A53: for i be Nat st i in ( dom D) holds (D . i) <= (g . i)

          proof

            let i be Nat;

            reconsider I = i as Element of NAT by ORDINAL1:def 12;

            assume

             A54: i in ( dom D);

            then

             A55: (D . i) = ((d . i) * (b |^ i)) by A42;

            (d . i) < (b1 + 1) by A40, A41, A54;

            then

             A56: (d . i) <= b1 by NAT_1: 13;

            (g . I) = (((b - 1) (#) (b GeoSeq )) . I) by A41, A52, A54, FUNCT_1: 47

            .= ((b - 1) * ((b GeoSeq ) . I)) by SEQ_1: 9

            .= (b1 * (b |^ I)) by PREPOWER:def 1;

            hence thesis by A56, A55, XREAL_1: 64;

          end;

          assume that

           A57: ( value (e,b)) = n and

           A58: (e . (( len e) - 1)) <> 0 and

           A59: for i be Nat st i in ( dom e) holds 0 <= (e . i) & (e . i) < b;

          consider E be XFinSequence of NAT such that

           A60: ( dom E) = ( dom e) and

           A61: for i be Nat st i in ( dom E) holds (E . i) = ((e . i) * (b |^ i)) and

           A62: n = ( Sum E) by A57, Def1;

          

           A63: (( len e) - 1) in ( dom e) by A58, FUNCT_1:def 2;

          then

          reconsider l = (( len e) - 1) as Element of NAT ;

          

           A64: (1 * (b |^ l)) <= ((e . l) * (b |^ l)) by A58, NAT_1: 4, NAT_1: 14;

          reconsider g = ((b1 (#) (b GeoSeq )) | ( len e)) as XFinSequence of NAT by Th1;

          g = (((b - 1) (#) (b GeoSeq )) | (l + 1));

          

          then

           A65: ( Sum g) = (( Partial_Sums ((b - 1) (#) (b GeoSeq ))) . l) by AFINSQ_2: 56

          .= (((b - 1) (#) ( Partial_Sums (b GeoSeq ))) . l) by SERIES_1: 9

          .= ((b - 1) * (( Partial_Sums (b GeoSeq )) . l)) by SEQ_1: 9

          .= ((b - 1) * ((1 - (b to_power (l + 1))) / (1 - b))) by A1, SERIES_1: 22

          .= ( - ((1 - b) * ((1 - (b |^ (l + 1))) / (1 - b))))

          .= ( - (1 - (b |^ (l + 1)))) by A35, XCMPLX_1: 87

          .= ((b |^ (l + 1)) - 1);

          ( dom E) <> {} by A58, A60, FUNCT_1:def 2;

          then

           A66: ( len E) > 0 ;

          

           A67: ( dom ((b - 1) (#) (b GeoSeq ))) = NAT by FUNCT_2:def 1;

          then ( len e) c= ( dom ((b - 1) (#) (b GeoSeq ))) by ORDINAL1:def 2;

          then

           A68: ( dom g) = ( len e) by RELAT_1: 62;

          

           A69: for i be Nat st i in ( dom E) holds (E . i) <= (g . i)

          proof

            let i be Nat;

            reconsider I = i as Element of NAT by ORDINAL1:def 12;

            assume

             A70: i in ( dom E);

            then

             A71: (E . i) = ((e . i) * (b |^ i)) by A61;

            (e . i) < (b1 + 1) by A59, A60, A70;

            then

             A72: (e . i) <= b1 by NAT_1: 13;

            (g . I) = (((b - 1) (#) (b GeoSeq )) . I) by A60, A68, A70, FUNCT_1: 47

            .= ((b - 1) * ((b GeoSeq ) . I)) by SEQ_1: 9

            .= (b1 * (b |^ I)) by PREPOWER:def 1;

            hence thesis by A72, A71, XREAL_1: 64;

          end;

          

           A73: (b |^ l) > 0 by A1, PREPOWER: 6;

          (E . l) = ((e . l) * (b |^ l)) by A60, A61, A63;

          then ((e . l) * (b |^ l)) <= n by A60, A62, A63, A66, AFINSQ_2: 61;

          then (b |^ l) <= n by A64, XXREAL_0: 2;

          then ( log (2,(b to_power l))) <= ( log (2,n)) by A73, PRE_FF: 10;

          then (l * ( log (2,b))) <= ( log (2,n)) by A1, POWER: 55;

          then ((l * ( log (2,b))) / ( log (2,b))) <= (( log (2,n)) / ( log (2,b))) by A33, XREAL_1: 72;

          then

           A74: l <= (( log (2,n)) / ( log (2,b))) by A33, XCMPLX_1: 89;

          ( len E) = ( len g) by A60, A67, RELAT_1: 62;

          then n < (((b |^ (l + 1)) - 1) + 1) by A62, A65, A69, AFINSQ_2: 57, XREAL_1: 39;

          then ( log (2,n)) < ( log (2,(b to_power (l + 1)))) by A37, POWER: 57;

          then ( log (2,n)) < ((l + 1) * ( log (2,b))) by A1, POWER: 55;

          then (( log (2,n)) / ( log (2,b))) < (((l + 1) * ( log (2,b))) / ( log (2,b))) by A33, XREAL_1: 74;

          then (( log (2,n)) / ( log (2,b))) < (l + 1) by A33, XCMPLX_1: 89;

          then k < (l + 1) by A48, XXREAL_0: 2;

          then

           A75: k <= l by NAT_1: 13;

          n < (((b |^ (k + 1)) - 1) + 1) by A43, A49, A51, A53, AFINSQ_2: 57, XREAL_1: 39;

          then ( log (2,n)) < ( log (2,(b to_power (k + 1)))) by A37, POWER: 57;

          then ( log (2,n)) < ((k + 1) * ( log (2,b))) by A1, POWER: 55;

          then (( log (2,n)) / ( log (2,b))) < (((k + 1) * ( log (2,b))) / ( log (2,b))) by A34, XREAL_1: 74;

          then (( log (2,n)) / ( log (2,b))) < (k + 1) by A34, XCMPLX_1: 89;

          then l < (k + 1) by A74, XXREAL_0: 2;

          then l <= k by NAT_1: 13;

          then

           A76: k = l by A75, XXREAL_0: 1;

          now

            let a be object;

            assume

             A77: a in ( dom d);

            then

            reconsider o = a as Element of NAT ;

            o < (k + 1) by A77, AFINSQ_1: 86;

            then

             A78: o <= k by NAT_1: 13;

            

             A79: o < ( len d) by A77, AFINSQ_1: 86;

            then

            reconsider oo = (( len d) - o) as Element of NAT by NAT_1: 21;

            per cases by A78, XXREAL_0: 1;

              suppose

               A80: o = 0 & o = k;

              then ( len E) = 1 by A60, A76;

              

              then

               A81: E = <%(E . 0 )%> by AFINSQ_1: 34

              .= <%((e . 0 ) * (b |^ 0 ))%> by A60, A61, A76, A77, A80

              .= <%((e . 0 ) * 1)%> by NEWTON: 4;

              ( len D) = 1 by A41, A80;

              

              then D = <%(D . 0 )%> by AFINSQ_1: 34

              .= <%((d . 0 ) * (b |^ 0 ))%> by A41, A42, A77, A80

              .= <%((d . 0 ) * 1)%> by NEWTON: 4;

              

              hence (d . a) = n by A43, A80, AFINSQ_2: 53

              .= (e . a) by A62, A80, A81, AFINSQ_2: 53;

            end;

              suppose

               A82: o = 0 & o < k;

              reconsider co = ( <%> NAT ) as XFinSequence of NAT ;

              ( Sum co) = 0 ;

              then

               A83: (( Sum co) div (b |^ o)) = 0 by NAT_2: 2;

              set d9 = D;

              D = (co ^ d9);

              then

               A84: n = (( Sum co) + ( Sum d9)) by A43, AFINSQ_2: 55;

              reconsider bo = (b |^ o) as Element of NAT by ORDINAL1:def 12;

              

               A85: bo <> 0 by A1, PREPOWER: 5;

               A86:

              now

                let k be Nat;

                assume k in ( dom <%(D . o)%>);

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

                then k < 1 by NAT_1: 44;

                then k = 0 by NAT_1: 14;

                hence (d9 . k) = ( <%(D . o)%> . k) by A82;

              end;

              reconsider o1 = (o + 1) as Element of NAT ;

              o1 <= k by A82, NAT_1: 13;

              then

               A87: o1 < ( len d) by XREAL_1: 147;

              reconsider oo1 = (( len d) - o1) as Element of NAT by A82;

              defpred P[ Nat, set] means $2 = (D . ($1 + o1));

              reconsider do1 = (D | o1) as XFinSequence of NAT ;

              

               A88: for u be Nat st u in ( Segm oo1) holds ex x be Element of NAT st P[u, x];

              consider d91 be XFinSequence of NAT such that

               A89: ( dom d91) = ( Segm oo1) & for x be Nat st x in ( Segm oo1) holds P[x, (d91 . x)] from STIRL2_1:sch 5( A88);

              

               A90: ( len d) = ( len D) by A41;

              then

               A91: ( len do1) = o1 by A87, AFINSQ_1: 11;

              then

               A92: ( dom D) = (( len do1) + ( len d91)) by A41, A89;

              now

                let k be Nat;

                reconsider K = k as Element of NAT by ORDINAL1:def 12;

                assume

                 A93: k in ( dom d91);

                then k < ( len d91) by AFINSQ_1: 86;

                then (o1 + k) < ( len D) by A91, A92, XREAL_1: 8;

                then (o1 + k) in ( dom D) by AFINSQ_1: 86;

                then (D . (o1 + k)) = ((d . (o1 + k)) * (b |^ (o1 + k))) by A42;

                

                then (d91 . K) = ((d . (o1 + k)) * (b |^ (o1 + k))) by A89, A93

                .= ((d . (o1 + k)) * ((b |^ o1) * (b |^ k))) by NEWTON: 8

                .= (((d . (o1 + k)) * (b |^ k)) * (b |^ o1));

                hence (b |^ o1) divides (d91 . k) by NAT_D:def 3;

              end;

              then

               A94: (b |^ o1) divides ( Sum d91) by Th2;

               A95:

              now

                let k be Nat;

                assume

                 A96: k in ( dom d91);

                

                thus (d9 . (( len <%(D . o)%>) + k)) = (D . (( len do1) + k)) by A82, A91, AFINSQ_1: 33

                .= (d91 . k) by A89, A91, A96;

              end;

              ( dom d9) = (1 + ( dom d91)) by A41, A82, A89

              .= (( len <%(D . o)%>) + ( len d91)) by AFINSQ_1: 34;

              then d9 = ( <%(D . o)%> ^ d91) by A86, A95, AFINSQ_1:def 3;

              then

               A97: ( Sum d9) = (( Sum <%(D . o)%>) + ( Sum d91)) by AFINSQ_2: 55;

              (for x be Nat st x in ( dom do1) holds (D . x) = (do1 . x)) & for x be Nat st x in ( dom d91) holds (D . (( len do1) + x)) = (d91 . x) by A89, A91, FUNCT_1: 47;

              then D = (do1 ^ d91) by A92, AFINSQ_1:def 3;

              then

               A98: n = (( Sum do1) + ( Sum d91)) by A43, AFINSQ_2: 55;

              reconsider bo1 = (b |^ o1) as Element of NAT by ORDINAL1:def 12;

              consider ok1 be Nat such that

               A99: (ok1 + 1) = o1;

              now

                let k be Nat;

                reconsider K = k as Element of NAT by ORDINAL1:def 12;

                assume k in ( dom d9);

                

                then (d9 . K) = ((d . (o + k)) * (b |^ (o + k))) by A42, A82

                .= ((d . (o + k)) * ((b |^ o) * (b |^ k))) by NEWTON: 8

                .= (((d . (o + k)) * (b |^ k)) * (b |^ o));

                hence (b |^ o) divides (d9 . k) by NAT_D:def 3;

              end;

              then

               A100: (b |^ o) divides ( Sum d9) by Th2;

              then (( Sum d9) mod (b |^ o)) = 0 by A85, PEPIN: 6;

              then (n div (b |^ o)) = ((( Sum d9) div (b |^ o)) + (( Sum co) div (b |^ o))) by A84, NAT_D: 19;

              then

               A101: ((n div (b |^ o)) * (b |^ o)) = ( Sum d9) by A83, A100, NAT_D: 3;

              reconsider co = ( <%> NAT ) as XFinSequence of NAT ;

              ( Sum co) = 0 ;

              then

               A102: (( Sum co) div (b |^ o)) = 0 by NAT_2: 2;

              set d9 = E;

              E = (co ^ d9);

              then

               A103: n = (( Sum co) + ( Sum d9)) by A62, AFINSQ_2: 55;

              reconsider bo = (b |^ o) as Element of NAT by ORDINAL1:def 12;

              

               A104: bo <> 0 by A1, PREPOWER: 5;

              reconsider ok1 as Element of NAT by ORDINAL1:def 12;

              reconsider g1 = ((b1 (#) (b GeoSeq )) | (ok1 + 1)) as XFinSequence of NAT by Th1;

              

               A105: (1 - b) <> 0 by A1;

              ( dom ((b - 1) (#) (b GeoSeq ))) = NAT by FUNCT_2:def 1;

              then

               A106: o1 c= ( dom ((b - 1) (#) (b GeoSeq ))) by ORDINAL1:def 2;

              then

               A107: ( len do1) = ( len g1) by A91, A99, RELAT_1: 62;

              

               A108: ( dom g1) = o1 by A99, A106, RELAT_1: 62;

              

               A109: for i be Nat st i in ( dom do1) holds (do1 . i) <= (g1 . i)

              proof

                let i be Nat;

                reconsider I = i as Element of NAT by ORDINAL1:def 12;

                assume

                 A110: i in ( dom do1);

                then i in o1 by A87, A90, AFINSQ_1: 11;

                

                then

                 A111: (g1 . I) = (((b - 1) (#) (b GeoSeq )) . I) by A108, FUNCT_1: 47

                .= ((b - 1) * ((b GeoSeq ) . I)) by SEQ_1: 9

                .= (b1 * (b |^ I)) by PREPOWER:def 1;

                

                 A112: ( dom do1) c= ( dom D) by RELAT_1: 60;

                then (d . i) < (b1 + 1) by A40, A41, A110;

                then

                 A113: (d . i) <= b1 by NAT_1: 13;

                (do1 . i) = (D . i) by A110, FUNCT_1: 47

                .= ((d . i) * (b |^ i)) by A42, A110, A112;

                hence thesis by A111, A113, XREAL_1: 64;

              end;

              ( Sum g1) = (( Partial_Sums ((b - 1) (#) (b GeoSeq ))) . ok1) by AFINSQ_2: 56

              .= (((b - 1) (#) ( Partial_Sums (b GeoSeq ))) . ok1) by SERIES_1: 9

              .= ((b - 1) * (( Partial_Sums (b GeoSeq )) . ok1)) by SEQ_1: 9

              .= ((b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b))) by A1, SERIES_1: 22

              .= ( - ((1 - b) * ((1 - (b |^ o1)) / (1 - b)))) by A99

              .= ( - (1 - (b |^ o1))) by A105, XCMPLX_1: 87

              .= ((b |^ o1) - 1);

              then ( Sum do1) < (((b |^ o1) - 1) + 1) by A107, A109, AFINSQ_2: 57, XREAL_1: 145;

              then

               A114: (( Sum do1) div (b |^ o1)) = 0 by NAT_D: 27;

              bo1 <> 0 by A1, PREPOWER: 5;

              then (( Sum d91) mod (b |^ o1)) = 0 by A94, PEPIN: 6;

              then (n div (b |^ o1)) = ((( Sum d91) div (b |^ o1)) + (( Sum do1) div (b |^ o1))) by A98, NAT_D: 19;

              then ((n div (b |^ o1)) * (b |^ o1)) = ( Sum d91) by A114, A94, NAT_D: 3;

              then (D . o) = (((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1))) by A101, A97, AFINSQ_2: 53;

              then ((d . o) * (b |^ o)) = (((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1))) by A41, A42, A77;

              then ((d . o) * (b |^ o)) = (((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * ((b |^ o) * (b |^ 1)))) by NEWTON: 8;

              then ((d . o) * (b |^ o)) = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * (b |^ 1))));

              then (((b |^ o) * (d . o)) / (b |^ o)) = (((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o));

              then

               A115: (d . o) = (((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o)) by A85, XCMPLX_1: 89;

              reconsider o1 = (o + 1) as Element of NAT ;

              reconsider do1 = (E | o1) as XFinSequence of NAT ;

              

               A116: ( len e) = ( len E) by A60;

              now

                let k be Nat;

                reconsider K = k as Element of NAT by ORDINAL1:def 12;

                assume k in ( dom d9);

                

                then (d9 . K) = ((e . (o + k)) * (b |^ (o + k))) by A61, A82

                .= ((e . (o + k)) * ((b |^ o) * (b |^ k))) by NEWTON: 8

                .= (((e . (o + k)) * (b |^ k)) * (b |^ o));

                hence (b |^ o) divides (d9 . k) by NAT_D:def 3;

              end;

              then

               A117: (b |^ o) divides ( Sum d9) by Th2;

              then (( Sum d9) mod (b |^ o)) = 0 by A104, PEPIN: 6;

              then (n div (b |^ o)) = ((( Sum d9) div (b |^ o)) + (( Sum co) div (b |^ o))) by A103, NAT_D: 19;

              then

               A118: ((n div (b |^ o)) * (b |^ o)) = ( Sum d9) by A102, A117, NAT_D: 3;

               A119:

              now

                let k be Nat;

                assume k in ( dom <%(E . o)%>);

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

                then k < 1 by NAT_1: 44;

                then k = 0 by NAT_1: 14;

                hence (d9 . k) = ( <%(E . o)%> . k) by A82;

              end;

              reconsider oo1 = (( len d) - o1) as Element of NAT by A82;

              defpred P[ Nat, set] means $2 = (E . ($1 + o1));

              

               A120: for u be Nat st u in ( Segm oo1) holds ex x be Element of NAT st P[u, x];

              consider d91 be XFinSequence of NAT such that

               A121: ( dom d91) = ( Segm oo1) & for x be Nat st x in ( Segm oo1) holds P[x, (d91 . x)] from STIRL2_1:sch 5( A120);

              o1 <= k by A82, NAT_1: 13;

              then

               A122: o1 < ( len d) by XREAL_1: 147;

              then

               A123: ( len do1) = o1 by A76, A116, AFINSQ_1: 11;

               A124:

              now

                let k be Nat;

                assume

                 A125: k in ( dom d91);

                

                thus (d9 . (( len <%(E . o)%>) + k)) = (E . (( len do1) + k)) by A82, A123, AFINSQ_1: 33

                .= (d91 . k) by A121, A123, A125;

              end;

              reconsider bo1 = (b |^ o1) as Element of NAT by ORDINAL1:def 12;

              consider ok1 be Nat such that

               A126: (ok1 + 1) = o1;

              

               A127: ( dom E) = (( len do1) + ( len d91)) by A60, A76, A121, A123;

              now

                let k be Nat;

                reconsider K = k as Element of NAT by ORDINAL1:def 12;

                assume

                 A128: k in ( dom d91);

                then k < ( len d91) by AFINSQ_1: 86;

                then (o1 + k) < ( len E) by A123, A127, XREAL_1: 8;

                then (o1 + k) in ( dom E) by AFINSQ_1: 86;

                then (E . (o1 + k)) = ((e . (o1 + k)) * (b |^ (o1 + k))) by A61;

                

                then (d91 . K) = ((e . (o1 + k)) * (b |^ (o1 + k))) by A121, A128

                .= ((e . (o1 + k)) * ((b |^ o1) * (b |^ k))) by NEWTON: 8

                .= (((e . (o1 + k)) * (b |^ k)) * (b |^ o1));

                hence (b |^ o1) divides (d91 . k) by NAT_D:def 3;

              end;

              then

               A129: (b |^ o1) divides ( Sum d91) by Th2;

              reconsider ok1 as Element of NAT by ORDINAL1:def 12;

              reconsider g1 = ((b1 (#) (b GeoSeq )) | (ok1 + 1)) as XFinSequence of NAT by Th1;

              

               A130: (1 - b) <> 0 by A1;

              ( dom ((b - 1) (#) (b GeoSeq ))) = NAT by FUNCT_2:def 1;

              then

               A131: o1 c= ( dom ((b - 1) (#) (b GeoSeq ))) by ORDINAL1:def 2;

              then

               A132: ( len do1) = ( len g1) by A123, A126, RELAT_1: 62;

              

               A133: ( dom g1) = o1 by A126, A131, RELAT_1: 62;

              

               A134: for i be Nat st i in ( dom do1) holds (do1 . i) <= (g1 . i)

              proof

                let i be Nat;

                reconsider I = i as Element of NAT by ORDINAL1:def 12;

                assume

                 A135: i in ( dom do1);

                then i in o1 by A76, A122, A116, AFINSQ_1: 11;

                

                then

                 A136: (g1 . I) = (((b - 1) (#) (b GeoSeq )) . I) by A133, FUNCT_1: 47

                .= ((b - 1) * ((b GeoSeq ) . I)) by SEQ_1: 9

                .= (b1 * (b |^ I)) by PREPOWER:def 1;

                

                 A137: ( dom do1) c= ( dom E) by RELAT_1: 60;

                then (e . i) < (b1 + 1) by A59, A60, A135;

                then

                 A138: (e . i) <= b1 by NAT_1: 13;

                (do1 . i) = (E . i) by A135, FUNCT_1: 47

                .= ((e . i) * (b |^ i)) by A61, A135, A137;

                hence thesis by A136, A138, XREAL_1: 64;

              end;

              ( Sum g1) = (( Partial_Sums ((b - 1) (#) (b GeoSeq ))) . ok1) by AFINSQ_2: 56

              .= (((b - 1) (#) ( Partial_Sums (b GeoSeq ))) . ok1) by SERIES_1: 9

              .= ((b - 1) * (( Partial_Sums (b GeoSeq )) . ok1)) by SEQ_1: 9

              .= ((b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b))) by A1, SERIES_1: 22

              .= ( - ((1 - b) * ((1 - (b |^ o1)) / (1 - b)))) by A126

              .= ( - (1 - (b |^ o1))) by A130, XCMPLX_1: 87

              .= ((b |^ o1) - 1);

              then ( Sum do1) < (((b |^ o1) - 1) + 1) by A132, A134, AFINSQ_2: 57, XREAL_1: 145;

              then

               A139: (( Sum do1) div (b |^ o1)) = 0 by NAT_D: 27;

              (for x be Nat st x in ( dom do1) holds (E . x) = (do1 . x)) & for x be Nat st x in ( dom d91) holds (E . (( len do1) + x)) = (d91 . x) by A121, A123, FUNCT_1: 47;

              then E = (do1 ^ d91) by A127, AFINSQ_1:def 3;

              then

               A140: n = (( Sum do1) + ( Sum d91)) by A62, AFINSQ_2: 55;

              bo1 <> 0 by A1, PREPOWER: 5;

              then (( Sum d91) mod (b |^ o1)) = 0 by A129, PEPIN: 6;

              then (n div (b |^ o1)) = ((( Sum d91) div (b |^ o1)) + (( Sum do1) div (b |^ o1))) by A140, NAT_D: 19;

              then

               A141: ((n div (b |^ o1)) * (b |^ o1)) = ( Sum d91) by A139, A129, NAT_D: 3;

              ( dom d9) = (1 + ( dom d91)) by A60, A76, A82, A121

              .= (( len <%(E . o)%>) + ( len d91)) by AFINSQ_1: 34;

              then d9 = ( <%(E . o)%> ^ d91) by A119, A124, AFINSQ_1:def 3;

              then ( Sum d9) = (( Sum <%(E . o)%>) + ( Sum d91)) by AFINSQ_2: 55;

              then (E . o) = (((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1))) by A118, A141, AFINSQ_2: 53;

              then ((e . o) * (b |^ o)) = (((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1))) by A60, A61, A76, A77;

              then ((e . o) * (b |^ o)) = (((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * ((b |^ o) * (b |^ 1)))) by NEWTON: 8;

              then ((e . o) * (b |^ o)) = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * (b |^ 1))));

              then (((b |^ o) * (e . o)) / (b |^ o)) = (((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o));

              hence (d . a) = (e . a) by A115, A104, XCMPLX_1: 89;

            end;

              suppose

               A142: o > 0 & o = k;

              set d9 = <%(D . o)%>;

              reconsider co = (D | o) as XFinSequence of NAT ;

              

               A143: ( len d) = ( len D) by A41;

              then

               A144: ( len co) = o by A79, AFINSQ_1: 11;

              

               A145: ( len d9) = oo by A142, AFINSQ_1: 34;

              then

               A146: ( dom D) = (( len co) + ( len d9)) by A41, A144;

              

               A147: for x be Nat st x in ( dom d9) holds (D . (( len co) + x)) = (d9 . x)

              proof

                let x be Nat;

                assume x in ( dom d9);

                then x < 1 by A142, A145, AFINSQ_1: 86;

                then x = 0 by NAT_1: 14;

                hence thesis by A144;

              end;

              now

                let k be Nat;

                reconsider K = k as Element of NAT by ORDINAL1:def 12;

                assume

                 A148: k in ( dom d9);

                then k < ( len d9) by AFINSQ_1: 86;

                then (o + k) < ( len D) by A144, A146, XREAL_1: 8;

                then (o + k) in ( dom D) by AFINSQ_1: 86;

                then (D . (o + k)) = ((d . (o + k)) * (b |^ (o + k))) by A42;

                

                then (d9 . K) = ((d . (o + k)) * (b |^ (o + k))) by A144, A147, A148

                .= ((d . (o + k)) * ((b |^ o) * (b |^ k))) by NEWTON: 8

                .= (((d . (o + k)) * (b |^ k)) * (b |^ o));

                hence (b |^ o) divides (d9 . k) by NAT_D:def 3;

              end;

              then

               A149: (b |^ o) divides ( Sum d9) by Th2;

              reconsider bo = (b |^ o) as Element of NAT by ORDINAL1:def 12;

              

               A150: (1 - b) <> 0 by A1;

              consider ok be Nat such that

               A151: (ok + 1) = o by A142, NAT_1: 6;

              reconsider ok as Element of NAT by ORDINAL1:def 12;

              reconsider g = ((b1 (#) (b GeoSeq )) | (ok + 1)) as XFinSequence of NAT by Th1;

              

               A152: ( Sum g) = (( Partial_Sums ((b - 1) (#) (b GeoSeq ))) . ok) by AFINSQ_2: 56

              .= (((b - 1) (#) ( Partial_Sums (b GeoSeq ))) . ok) by SERIES_1: 9

              .= ((b - 1) * (( Partial_Sums (b GeoSeq )) . ok)) by SEQ_1: 9

              .= ((b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b))) by A1, SERIES_1: 22

              .= ( - ((1 - b) * ((1 - (b |^ o)) / (1 - b)))) by A151

              .= ( - (1 - (b |^ o))) by A150, XCMPLX_1: 87

              .= ((b |^ o) - 1);

              consider ok be Nat such that

               A153: (ok + 1) = o by A142, NAT_1: 6;

              ( dom ((b - 1) (#) (b GeoSeq ))) = NAT by FUNCT_2:def 1;

              then

               A154: o c= ( dom ((b - 1) (#) (b GeoSeq ))) by ORDINAL1:def 2;

              then

               A155: ( dom g) = o by A151, RELAT_1: 62;

              

               A156: for i be Nat st i in ( dom co) holds (co . i) <= (g . i)

              proof

                let i be Nat;

                reconsider I = i as Element of NAT by ORDINAL1:def 12;

                assume

                 A157: i in ( dom co);

                then i in o by A79, A143, AFINSQ_1: 11;

                

                then

                 A158: (g . I) = (((b - 1) (#) (b GeoSeq )) . I) by A155, FUNCT_1: 47

                .= ((b - 1) * ((b GeoSeq ) . I)) by SEQ_1: 9

                .= (b1 * (b |^ I)) by PREPOWER:def 1;

                

                 A159: ( dom co) c= ( dom D) by RELAT_1: 60;

                then (d . i) < (b1 + 1) by A40, A41, A157;

                then

                 A160: (d . i) <= b1 by NAT_1: 13;

                (co . i) = (D . i) by A157, FUNCT_1: 47

                .= ((d . i) * (b |^ i)) by A42, A157, A159;

                hence thesis by A158, A160, XREAL_1: 64;

              end;

              ( len co) = ( len g) by A144, A151, A154, RELAT_1: 62;

              then ( Sum co) < (((b |^ o) - 1) + 1) by A152, A156, AFINSQ_2: 57, XREAL_1: 145;

              then

               A161: (( Sum co) div (b |^ o)) = 0 by NAT_D: 27;

              for x be Nat st x in ( dom co) holds (D . x) = (co . x) by FUNCT_1: 47;

              then D = (co ^ d9) by A146, A147, AFINSQ_1:def 3;

              then

               A162: n = (( Sum co) + ( Sum d9)) by A43, AFINSQ_2: 55;

              

               A163: bo <> 0 by A1, PREPOWER: 5;

              then (( Sum d9) mod (b |^ o)) = 0 by A149, PEPIN: 6;

              then (n div (b |^ o)) = ((( Sum d9) div (b |^ o)) + (( Sum co) div (b |^ o))) by A162, NAT_D: 19;

              then ((n div (b |^ o)) * (b |^ o)) = ( Sum d9) by A161, A149, NAT_D: 3;

              then (D . o) = ((n div (b |^ o)) * (b |^ o)) by AFINSQ_2: 53;

              then (((d . o) * (b |^ o)) / (b |^ o)) = (((n div (b |^ o)) * (b |^ o)) / (b |^ o)) by A41, A42, A77;

              then

               A164: (d . o) = (((n div (b |^ o)) * (b |^ o)) / (b |^ o)) by A163, XCMPLX_1: 89;

              set d9 = <%(E . o)%>;

              reconsider co = (E | o) as XFinSequence of NAT ;

              

               A165: ( len e) = ( len E) by A60;

              then

               A166: ( len co) = o by A76, A79, AFINSQ_1: 11;

              

               A167: ( len d9) = oo by A142, AFINSQ_1: 34;

              then

               A168: ( dom E) = (( len co) + ( len d9)) by A60, A76, A166;

              

               A169: for x be Nat st x in ( dom d9) holds (E . (( len co) + x)) = (d9 . x)

              proof

                let x be Nat;

                assume x in ( dom d9);

                then x < 1 by A142, A167, AFINSQ_1: 86;

                then x = 0 by NAT_1: 14;

                hence thesis by A166;

              end;

              now

                let k be Nat;

                reconsider K = k as Element of NAT by ORDINAL1:def 12;

                assume

                 A170: k in ( dom d9);

                then k < ( len d9) by AFINSQ_1: 86;

                then (o + k) < ( len E) by A166, A168, XREAL_1: 8;

                then (o + k) in ( dom E) by AFINSQ_1: 86;

                then (E . (o + k)) = ((e . (o + k)) * (b |^ (o + k))) by A61;

                

                then (d9 . K) = ((e . (o + k)) * (b |^ (o + k))) by A166, A169, A170

                .= ((e . (o + k)) * ((b |^ o) * (b |^ k))) by NEWTON: 8

                .= (((e . (o + k)) * (b |^ k)) * (b |^ o));

                hence (b |^ o) divides (d9 . k) by NAT_D:def 3;

              end;

              then

               A171: (b |^ o) divides ( Sum d9) by Th2;

              reconsider ok as Element of NAT by ORDINAL1:def 12;

              reconsider g = ((b1 (#) (b GeoSeq )) | (ok + 1)) as XFinSequence of NAT by Th1;

              reconsider bo = (b |^ o) as Element of NAT by ORDINAL1:def 12;

              

               A172: (1 - b) <> 0 by A1;

              ( dom ((b - 1) (#) (b GeoSeq ))) = NAT by FUNCT_2:def 1;

              then

               A173: o c= ( dom ((b - 1) (#) (b GeoSeq ))) by ORDINAL1:def 2;

              then

               A174: ( len co) = ( len g) by A166, A153, RELAT_1: 62;

              

               A175: ( dom g) = o by A153, A173, RELAT_1: 62;

              

               A176: for i be Nat st i in ( dom co) holds (co . i) <= (g . i)

              proof

                let i be Nat;

                reconsider I = i as Element of NAT by ORDINAL1:def 12;

                assume

                 A177: i in ( dom co);

                then i in o by A76, A79, A165, AFINSQ_1: 11;

                

                then

                 A178: (g . I) = (((b - 1) (#) (b GeoSeq )) . I) by A175, FUNCT_1: 47

                .= ((b - 1) * ((b GeoSeq ) . I)) by SEQ_1: 9

                .= (b1 * (b |^ I)) by PREPOWER:def 1;

                

                 A179: ( dom co) c= ( dom E) by RELAT_1: 60;

                then (e . i) < (b1 + 1) by A59, A60, A177;

                then

                 A180: (e . i) <= b1 by NAT_1: 13;

                (co . i) = (E . i) by A177, FUNCT_1: 47

                .= ((e . i) * (b |^ i)) by A61, A177, A179;

                hence thesis by A178, A180, XREAL_1: 64;

              end;

              ( Sum g) = (( Partial_Sums ((b - 1) (#) (b GeoSeq ))) . ok) by AFINSQ_2: 56

              .= (((b - 1) (#) ( Partial_Sums (b GeoSeq ))) . ok) by SERIES_1: 9

              .= ((b - 1) * (( Partial_Sums (b GeoSeq )) . ok)) by SEQ_1: 9

              .= ((b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b))) by A1, SERIES_1: 22

              .= ( - ((1 - b) * ((1 - (b |^ o)) / (1 - b)))) by A153

              .= ( - (1 - (b |^ o))) by A172, XCMPLX_1: 87

              .= ((b |^ o) - 1);

              then ( Sum co) < (((b |^ o) - 1) + 1) by A174, A176, AFINSQ_2: 57, XREAL_1: 145;

              then

               A181: (( Sum co) div (b |^ o)) = 0 by NAT_D: 27;

              for x be Nat st x in ( dom co) holds (E . x) = (co . x) by FUNCT_1: 47;

              then E = (co ^ d9) by A168, A169, AFINSQ_1:def 3;

              then

               A182: n = (( Sum co) + ( Sum d9)) by A62, AFINSQ_2: 55;

              

               A183: bo <> 0 by A1, PREPOWER: 5;

              then (( Sum d9) mod (b |^ o)) = 0 by A171, PEPIN: 6;

              then (n div (b |^ o)) = ((( Sum d9) div (b |^ o)) + (( Sum co) div (b |^ o))) by A182, NAT_D: 19;

              then ((n div (b |^ o)) * (b |^ o)) = ( Sum d9) by A181, A171, NAT_D: 3;

              then (E . o) = ((n div (b |^ o)) * (b |^ o)) by AFINSQ_2: 53;

              then (((e . o) * (b |^ o)) / (b |^ o)) = (((n div (b |^ o)) * (b |^ o)) / (b |^ o)) by A60, A61, A76, A77;

              hence (d . a) = (e . a) by A164, A183, XCMPLX_1: 89;

            end;

              suppose

               A184: o > 0 & o < k;

              reconsider o1 = (o + 1) as Element of NAT ;

              

               A185: o1 <= k by A184, NAT_1: 13;

              then

               A186: o1 < ( len d) by XREAL_1: 147;

              reconsider bo1 = (b |^ o1) as Element of NAT by ORDINAL1:def 12;

              reconsider do1 = (D | o1) as XFinSequence of NAT ;

              reconsider bo = (b |^ o) as Element of NAT by ORDINAL1:def 12;

              defpred P[ Nat, set] means $2 = (D . ($1 + o));

              consider ok1 be Nat such that

               A187: (ok1 + 1) = o1;

              reconsider ok1 as Element of NAT by ORDINAL1:def 12;

              reconsider g1 = ((b1 (#) (b GeoSeq )) | (ok1 + 1)) as XFinSequence of NAT by Th1;

              

               A188: ( len d) = ( len D) by A41;

              then

               A189: ( len do1) = o1 by A186, AFINSQ_1: 11;

              ( dom ((b - 1) (#) (b GeoSeq ))) = NAT by FUNCT_2:def 1;

              then

               A190: o1 c= ( dom ((b - 1) (#) (b GeoSeq ))) by ORDINAL1:def 2;

              then

               A191: ( len do1) = ( len g1) by A189, A187, RELAT_1: 62;

              

               A192: ( dom g1) = o1 by A187, A190, RELAT_1: 62;

              

               A193: for i be Nat st i in ( dom do1) holds (do1 . i) <= (g1 . i)

              proof

                let i be Nat;

                reconsider I = i as Element of NAT by ORDINAL1:def 12;

                assume

                 A194: i in ( dom do1);

                then i in o1 by A186, A188, AFINSQ_1: 11;

                

                then

                 A195: (g1 . I) = (((b - 1) (#) (b GeoSeq )) . I) by A192, FUNCT_1: 47

                .= ((b - 1) * ((b GeoSeq ) . I)) by SEQ_1: 9

                .= (b1 * (b |^ I)) by PREPOWER:def 1;

                

                 A196: ( dom do1) c= ( dom D) by RELAT_1: 60;

                then (d . i) < (b1 + 1) by A40, A41, A194;

                then

                 A197: (d . i) <= b1 by NAT_1: 13;

                (do1 . i) = (D . i) by A194, FUNCT_1: 47

                .= ((d . i) * (b |^ i)) by A42, A194, A196;

                hence thesis by A195, A197, XREAL_1: 64;

              end;

              k < ( len d) by XREAL_1: 147;

              then

              reconsider oo1 = (( len d) - o1) as Element of NAT by A185, NAT_1: 21, XXREAL_0: 2;

              

               A198: for u be Nat st u in ( Segm oo) holds ex x be Element of NAT st P[u, x];

              consider d9 be XFinSequence of NAT such that

               A199: ( dom d9) = ( Segm oo) & for x be Nat st x in ( Segm oo) holds P[x, (d9 . x)] from STIRL2_1:sch 5( A198);

               A200:

              now

                let k be Nat;

                assume k in ( dom <%(D . o)%>);

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

                then k < 1 by NAT_1: 44;

                then

                 A201: k = 0 by NAT_1: 14;

                then ( len d9) > k by A79, XREAL_1: 50, A199;

                then k in ( dom d9) by A199, NAT_1: 44;

                

                hence (d9 . k) = (D . (k + o)) by A199

                .= ( <%(D . o)%> . k) by A201;

              end;

              defpred P[ Nat, set] means $2 = (D . ($1 + o1));

              

               A202: for u be Nat st u in ( Segm oo1) holds ex x be Element of NAT st P[u, x];

              consider d91 be XFinSequence of NAT such that

               A203: ( dom d91) = ( Segm oo1) & for x be Nat st x in ( Segm oo1) holds P[x, (d91 . x)] from STIRL2_1:sch 5( A202);

              reconsider co = (D | o) as XFinSequence of NAT ;

              

               A204: ( len d) = ( len D) by A41;

              then

               A205: ( len co) = o by A79, AFINSQ_1: 11;

              then

               A206: ( dom D) = (( len co) + ( len d9)) by A41, A199;

              now

                let k be Nat;

                reconsider K = k as Element of NAT by ORDINAL1:def 12;

                assume

                 A207: k in ( dom d9);

                then k < ( len d9) by AFINSQ_1: 86;

                then (o + k) < ( len D) by A205, A206, XREAL_1: 8;

                then (o + k) in ( dom D) by AFINSQ_1: 86;

                then (D . (o + k)) = ((d . (o + k)) * (b |^ (o + k))) by A42;

                

                then (d9 . K) = ((d . (o + k)) * (b |^ (o + k))) by A199, A207

                .= ((d . (o + k)) * ((b |^ o) * (b |^ k))) by NEWTON: 8

                .= (((d . (o + k)) * (b |^ k)) * (b |^ o));

                hence (b |^ o) divides (d9 . k) by NAT_D:def 3;

              end;

              then

               A208: (b |^ o) divides ( Sum d9) by Th2;

              (for x be Nat st x in ( dom co) holds (D . x) = (co . x)) & for x be Nat st x in ( dom d9) holds (D . (( len co) + x)) = (d9 . x) by A199, A205, FUNCT_1: 47;

              then D = (co ^ d9) by A206, AFINSQ_1:def 3;

              then

               A209: n = (( Sum co) + ( Sum d9)) by A43, AFINSQ_2: 55;

              consider ok be Nat such that

               A210: (ok + 1) = o by A184, NAT_1: 6;

              reconsider ok as Element of NAT by ORDINAL1:def 12;

              reconsider g = ((b1 (#) (b GeoSeq )) | (ok + 1)) as XFinSequence of NAT by Th1;

              

               A211: (1 - b) <> 0 by A1;

              

               A212: ( Sum g) = (( Partial_Sums ((b - 1) (#) (b GeoSeq ))) . ok) by AFINSQ_2: 56

              .= (((b - 1) (#) ( Partial_Sums (b GeoSeq ))) . ok) by SERIES_1: 9

              .= ((b - 1) * (( Partial_Sums (b GeoSeq )) . ok)) by SEQ_1: 9

              .= ((b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b))) by A1, SERIES_1: 22

              .= ( - ((1 - b) * ((1 - (b |^ o)) / (1 - b)))) by A210

              .= ( - (1 - (b |^ o))) by A211, XCMPLX_1: 87

              .= ((b |^ o) - 1);

              ( dom ((b - 1) (#) (b GeoSeq ))) = NAT by FUNCT_2:def 1;

              then

               A213: o c= ( dom ((b - 1) (#) (b GeoSeq ))) by ORDINAL1:def 2;

              then

               A214: ( dom g) = o by A210, RELAT_1: 62;

              

               A215: for i be Nat st i in ( dom co) holds (co . i) <= (g . i)

              proof

                let i be Nat;

                reconsider I = i as Element of NAT by ORDINAL1:def 12;

                assume

                 A216: i in ( dom co);

                then i in o by A79, A204, AFINSQ_1: 11;

                

                then

                 A217: (g . I) = (((b - 1) (#) (b GeoSeq )) . I) by A214, FUNCT_1: 47

                .= ((b - 1) * ((b GeoSeq ) . I)) by SEQ_1: 9

                .= (b1 * (b |^ I)) by PREPOWER:def 1;

                

                 A218: ( dom co) c= ( dom D) by RELAT_1: 60;

                then (d . i) < (b1 + 1) by A40, A41, A216;

                then

                 A219: (d . i) <= b1 by NAT_1: 13;

                (co . i) = (D . i) by A216, FUNCT_1: 47

                .= ((d . i) * (b |^ i)) by A42, A216, A218;

                hence thesis by A217, A219, XREAL_1: 64;

              end;

               A220:

              now

                let k be Nat;

                assume

                 A221: k in ( dom d91);

                then k < ( len d91) by A203, NAT_1: 44;

                then (k + 1) < (oo1 + 1) by XREAL_1: 8, A203;

                then (k + 1) < ( len d9) by A199;

                then

                 A222: (k + 1) in ( dom d9) by A199, NAT_1: 44;

                

                thus (d9 . (( len <%(D . o)%>) + k)) = (d9 . (1 + k)) by AFINSQ_1: 33

                .= (D . (( len co) + (k + 1))) by A199, A205, A222

                .= (D . (( len do1) + k)) by A205, A189

                .= (d91 . k) by A203, A189, A221;

              end;

              ( dom d9) = (1 + ( dom d91)) by A199, A203

              .= (( len <%(D . o)%>) + ( len d91)) by AFINSQ_1: 34;

              then d9 = ( <%(D . o)%> ^ d91) by A200, A220, AFINSQ_1:def 3;

              then

               A223: ( Sum d9) = (( Sum <%(D . o)%>) + ( Sum d91)) by AFINSQ_2: 55;

              defpred P[ Nat, set] means $2 = (E . ($1 + o));

              

               A224: (1 - b) <> 0 by A1;

              consider ok be Nat such that

               A225: (ok + 1) = o by A184, NAT_1: 6;

              

               A226: ( dom D) = (( len do1) + ( len d91)) by A41, A203, A189;

              now

                let k be Nat;

                reconsider K = k as Element of NAT by ORDINAL1:def 12;

                assume

                 A227: k in ( dom d91);

                then k < ( len d91) by AFINSQ_1: 86;

                then (o1 + k) < ( len D) by A189, A226, XREAL_1: 8;

                then (o1 + k) in ( dom D) by AFINSQ_1: 86;

                then (D . (o1 + k)) = ((d . (o1 + k)) * (b |^ (o1 + k))) by A42;

                

                then (d91 . K) = ((d . (o1 + k)) * (b |^ (o1 + k))) by A203, A227

                .= ((d . (o1 + k)) * ((b |^ o1) * (b |^ k))) by NEWTON: 8

                .= (((d . (o1 + k)) * (b |^ k)) * (b |^ o1));

                hence (b |^ o1) divides (d91 . k) by NAT_D:def 3;

              end;

              then

               A228: (b |^ o1) divides ( Sum d91) by Th2;

              ( len co) = ( len g) by A205, A210, A213, RELAT_1: 62;

              then ( Sum co) < (((b |^ o) - 1) + 1) by A212, A215, AFINSQ_2: 57, XREAL_1: 145;

              then

               A229: (( Sum co) div (b |^ o)) = 0 by NAT_D: 27;

              

               A230: (1 - b) <> 0 by A1;

              ( Sum g1) = (( Partial_Sums ((b - 1) (#) (b GeoSeq ))) . ok1) by AFINSQ_2: 56

              .= (((b - 1) (#) ( Partial_Sums (b GeoSeq ))) . ok1) by SERIES_1: 9

              .= ((b - 1) * (( Partial_Sums (b GeoSeq )) . ok1)) by SEQ_1: 9

              .= ((b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b))) by A1, SERIES_1: 22

              .= ( - ((1 - b) * ((1 - (b |^ o1)) / (1 - b)))) by A187

              .= ( - (1 - (b |^ o1))) by A230, XCMPLX_1: 87

              .= ((b |^ o1) - 1);

              then ( Sum do1) < (((b |^ o1) - 1) + 1) by A191, A193, AFINSQ_2: 57, XREAL_1: 145;

              then

               A231: (( Sum do1) div (b |^ o1)) = 0 by NAT_D: 27;

              (for x be Nat st x in ( dom do1) holds (D . x) = (do1 . x)) & for x be Nat st x in ( dom d91) holds (D . (( len do1) + x)) = (d91 . x) by A203, A189, FUNCT_1: 47;

              then D = (do1 ^ d91) by A226, AFINSQ_1:def 3;

              then

               A232: n = (( Sum do1) + ( Sum d91)) by A43, AFINSQ_2: 55;

              bo1 <> 0 by A1, PREPOWER: 5;

              then (( Sum d91) mod (b |^ o1)) = 0 by A228, PEPIN: 6;

              then (n div (b |^ o1)) = ((( Sum d91) div (b |^ o1)) + (( Sum do1) div (b |^ o1))) by A232, NAT_D: 19;

              then

               A233: ((n div (b |^ o1)) * (b |^ o1)) = ( Sum d91) by A231, A228, NAT_D: 3;

              

               A234: bo <> 0 by A1, PREPOWER: 5;

              then (( Sum d9) mod (b |^ o)) = 0 by A208, PEPIN: 6;

              then (n div (b |^ o)) = ((( Sum d9) div (b |^ o)) + (( Sum co) div (b |^ o))) by A209, NAT_D: 19;

              then ((n div (b |^ o)) * (b |^ o)) = ( Sum d9) & ( Sum <%(D . o)%>) = (D . o) by A229, A208, AFINSQ_2: 53, NAT_D: 3;

              then ((d . o) * (b |^ o)) = (((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1))) by A41, A42, A77, A233, A223;

              then ((d . o) * (b |^ o)) = (((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * ((b |^ o) * (b |^ 1)))) by NEWTON: 8;

              then ((d . o) * (b |^ o)) = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * (b |^ 1))));

              then (((b |^ o) * (d . o)) / (b |^ o)) = (((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o));

              then

               A235: (d . o) = (((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o)) by A234, XCMPLX_1: 89;

              reconsider o1 = (o + 1) as Element of NAT ;

              

               A236: o1 <= k by A184, NAT_1: 13;

              then

               A237: o1 < ( len d) by XREAL_1: 147;

              reconsider ok as Element of NAT by ORDINAL1:def 12;

              reconsider g = ((b1 (#) (b GeoSeq )) | (ok + 1)) as XFinSequence of NAT by Th1;

              

               A238: (1 - b) <> 0 by A1;

              reconsider bo1 = (b |^ o1) as Element of NAT by ORDINAL1:def 12;

              reconsider do1 = (E | o1) as XFinSequence of NAT ;

              reconsider bo = (b |^ o) as Element of NAT by ORDINAL1:def 12;

              consider ok1 be Nat such that

               A239: (ok1 + 1) = o1;

              reconsider ok1 as Element of NAT by ORDINAL1:def 12;

              reconsider g1 = ((b1 (#) (b GeoSeq )) | (ok1 + 1)) as XFinSequence of NAT by Th1;

              

               A240: ( len e) = ( len E) by A60;

              then

               A241: ( len do1) = o1 by A76, A237, AFINSQ_1: 11;

              ( dom ((b - 1) (#) (b GeoSeq ))) = NAT by FUNCT_2:def 1;

              then

               A242: o1 c= ( dom ((b - 1) (#) (b GeoSeq ))) by ORDINAL1:def 2;

              then

               A243: ( len do1) = ( len g1) by A241, A239, RELAT_1: 62;

              

               A244: ( dom g1) = o1 by A239, A242, RELAT_1: 62;

              

               A245: for i be Nat st i in ( dom do1) holds (do1 . i) <= (g1 . i)

              proof

                let i be Nat;

                reconsider I = i as Element of NAT by ORDINAL1:def 12;

                assume

                 A246: i in ( dom do1);

                then i in o1 by A76, A237, A240, AFINSQ_1: 11;

                

                then

                 A247: (g1 . I) = (((b - 1) (#) (b GeoSeq )) . I) by A244, FUNCT_1: 47

                .= ((b - 1) * ((b GeoSeq ) . I)) by SEQ_1: 9

                .= (b1 * (b |^ I)) by PREPOWER:def 1;

                

                 A248: ( dom do1) c= ( dom E) by RELAT_1: 60;

                then (e . i) < (b1 + 1) by A59, A60, A246;

                then

                 A249: (e . i) <= b1 by NAT_1: 13;

                (do1 . i) = (E . i) by A246, FUNCT_1: 47

                .= ((e . i) * (b |^ i)) by A61, A246, A248;

                hence thesis by A247, A249, XREAL_1: 64;

              end;

              ( Sum g1) = (( Partial_Sums ((b - 1) (#) (b GeoSeq ))) . ok1) by AFINSQ_2: 56

              .= (((b - 1) (#) ( Partial_Sums (b GeoSeq ))) . ok1) by SERIES_1: 9

              .= ((b - 1) * (( Partial_Sums (b GeoSeq )) . ok1)) by SEQ_1: 9

              .= ((b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b))) by A1, SERIES_1: 22

              .= ( - ((1 - b) * ((1 - (b |^ o1)) / (1 - b)))) by A239

              .= ( - (1 - (b |^ o1))) by A238, XCMPLX_1: 87

              .= ((b |^ o1) - 1);

              then ( Sum do1) < (((b |^ o1) - 1) + 1) by A243, A245, AFINSQ_2: 57, XREAL_1: 145;

              then

               A250: (( Sum do1) div (b |^ o1)) = 0 by NAT_D: 27;

              k < ( len d) by XREAL_1: 147;

              then

              reconsider oo1 = (( len d) - o1) as Element of NAT by A236, NAT_1: 21, XXREAL_0: 2;

              

               A251: for u be Nat st u in ( Segm oo) holds ex x be Element of NAT st P[u, x];

              consider d9 be XFinSequence of NAT such that

               A252: ( dom d9) = ( Segm oo) & for x be Nat st x in ( Segm oo) holds P[x, (d9 . x)] from STIRL2_1:sch 5( A251);

               A253:

              now

                let k be Nat;

                assume k in ( dom <%(E . o)%>);

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

                then k < 1 by NAT_1: 44;

                then

                 A254: k = 0 by NAT_1: 14;

                oo > 0 by A79, XREAL_1: 50;

                then k < ( len d9) by A252, A254;

                then k in ( dom d9) by A252, NAT_1: 44;

                

                hence (d9 . k) = (E . (k + o)) by A252

                .= ( <%(E . o)%> . k) by A254;

              end;

              defpred P[ Nat, set] means $2 = (E . ($1 + o1));

              

               A255: for u be Nat st u in ( Segm oo1) holds ex x be Element of NAT st P[u, x];

              consider d91 be XFinSequence of NAT such that

               A256: ( dom d91) = ( Segm oo1) & for x be Nat st x in ( Segm oo1) holds P[x, (d91 . x)] from STIRL2_1:sch 5( A255);

              

               A257: ( dom E) = (( len do1) + ( len d91)) by A60, A76, A256, A241;

              now

                let k be Nat;

                reconsider K = k as Element of NAT by ORDINAL1:def 12;

                assume

                 A258: k in ( dom d91);

                then k < ( len d91) by AFINSQ_1: 86;

                then (o1 + k) < ( len E) by A241, A257, XREAL_1: 8;

                then (o1 + k) in ( dom E) by AFINSQ_1: 86;

                then (E . (o1 + k)) = ((e . (o1 + k)) * (b |^ (o1 + k))) by A61;

                

                then (d91 . K) = ((e . (o1 + k)) * (b |^ (o1 + k))) by A256, A258

                .= ((e . (o1 + k)) * ((b |^ o1) * (b |^ k))) by NEWTON: 8

                .= (((e . (o1 + k)) * (b |^ k)) * (b |^ o1));

                hence (b |^ o1) divides (d91 . k) by NAT_D:def 3;

              end;

              then

               A259: (b |^ o1) divides ( Sum d91) by Th2;

              (for x be Nat st x in ( dom do1) holds (E . x) = (do1 . x)) & for x be Nat st x in ( dom d91) holds (E . (( len do1) + x)) = (d91 . x) by A256, A241, FUNCT_1: 47;

              then E = (do1 ^ d91) by A257, AFINSQ_1:def 3;

              then

               A260: n = (( Sum do1) + ( Sum d91)) by A62, AFINSQ_2: 55;

              bo1 <> 0 by A1, PREPOWER: 5;

              then (( Sum d91) mod (b |^ o1)) = 0 by A259, PEPIN: 6;

              then (n div (b |^ o1)) = ((( Sum d91) div (b |^ o1)) + (( Sum do1) div (b |^ o1))) by A260, NAT_D: 19;

              then

               A261: ((n div (b |^ o1)) * (b |^ o1)) = ( Sum d91) by A250, A259, NAT_D: 3;

              reconsider co = (E | o) as XFinSequence of NAT ;

              

               A262: ( len e) = ( len E) by A60;

              then

               A263: ( len co) = o by A76, A79, AFINSQ_1: 11;

              then

               A264: ( dom E) = (( len co) + ( len d9)) by A60, A76, A252;

              now

                let k be Nat;

                reconsider K = k as Element of NAT by ORDINAL1:def 12;

                assume

                 A265: k in ( dom d9);

                then k < ( len d9) by AFINSQ_1: 86;

                then (o + k) < ( len E) by A263, A264, XREAL_1: 8;

                then (o + k) in ( dom E) by AFINSQ_1: 86;

                then (E . (o + k)) = ((e . (o + k)) * (b |^ (o + k))) by A61;

                

                then (d9 . K) = ((e . (o + k)) * (b |^ (o + k))) by A252, A265

                .= ((e . (o + k)) * ((b |^ o) * (b |^ k))) by NEWTON: 8

                .= (((e . (o + k)) * (b |^ k)) * (b |^ o));

                hence (b |^ o) divides (d9 . k) by NAT_D:def 3;

              end;

              then

               A266: (b |^ o) divides ( Sum d9) by Th2;

              ( dom ((b - 1) (#) (b GeoSeq ))) = NAT by FUNCT_2:def 1;

              then

               A267: o c= ( dom ((b - 1) (#) (b GeoSeq ))) by ORDINAL1:def 2;

              then

               A268: ( len co) = ( len g) by A263, A225, RELAT_1: 62;

              

               A269: ( dom g) = o by A225, A267, RELAT_1: 62;

              

               A270: for i be Nat st i in ( dom co) holds (co . i) <= (g . i)

              proof

                let i be Nat;

                reconsider I = i as Element of NAT by ORDINAL1:def 12;

                assume

                 A271: i in ( dom co);

                then i in o by A76, A79, A262, AFINSQ_1: 11;

                

                then

                 A272: (g . I) = (((b - 1) (#) (b GeoSeq )) . I) by A269, FUNCT_1: 47

                .= ((b - 1) * ((b GeoSeq ) . I)) by SEQ_1: 9

                .= (b1 * (b |^ I)) by PREPOWER:def 1;

                

                 A273: ( dom co) c= ( dom E) by RELAT_1: 60;

                then (e . i) < (b1 + 1) by A59, A60, A271;

                then

                 A274: (e . i) <= b1 by NAT_1: 13;

                (co . i) = (E . i) by A271, FUNCT_1: 47

                .= ((e . i) * (b |^ i)) by A61, A271, A273;

                hence thesis by A272, A274, XREAL_1: 64;

              end;

              ( Sum g) = (( Partial_Sums ((b - 1) (#) (b GeoSeq ))) . ok) by AFINSQ_2: 56

              .= (((b - 1) (#) ( Partial_Sums (b GeoSeq ))) . ok) by SERIES_1: 9

              .= ((b - 1) * (( Partial_Sums (b GeoSeq )) . ok)) by SEQ_1: 9

              .= ((b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b))) by A1, SERIES_1: 22

              .= ( - ((1 - b) * ((1 - (b |^ o)) / (1 - b)))) by A225

              .= ( - (1 - (b |^ o))) by A224, XCMPLX_1: 87

              .= ((b |^ o) - 1);

              then ( Sum co) < (((b |^ o) - 1) + 1) by A268, A270, AFINSQ_2: 57, XREAL_1: 145;

              then

               A275: (( Sum co) div (b |^ o)) = 0 by NAT_D: 27;

               A276:

              now

                let k be Nat;

                assume

                 A277: k in ( dom d91);

                then k < ( len d91) by A256, NAT_1: 44;

                then (k + 1) < (oo1 + 1) by XREAL_1: 8, A256;

                then

                 A278: (k + 1) in ( Segm oo) by NAT_1: 44;

                

                thus (d9 . (( len <%(E . o)%>) + k)) = (d9 . (1 + k)) by AFINSQ_1: 33

                .= (E . (( len co) + (k + 1))) by A252, A263, A278

                .= (E . (( len do1) + k)) by A263, A241

                .= (d91 . k) by A256, A241, A277;

              end;

              ( dom d9) = (1 + ( dom d91)) by A252, A256

              .= (( len <%(E . o)%>) + ( len d91)) by AFINSQ_1: 34;

              then d9 = ( <%(E . o)%> ^ d91) by A253, A276, AFINSQ_1:def 3;

              then

               A279: ( Sum d9) = (( Sum <%(E . o)%>) + ( Sum d91)) by AFINSQ_2: 55;

              (for x be Nat st x in ( dom co) holds (E . x) = (co . x)) & for x be Nat st x in ( dom d9) holds (E . (( len co) + x)) = (d9 . x) by A252, A263, FUNCT_1: 47;

              then E = (co ^ d9) by A264, AFINSQ_1:def 3;

              then

               A280: n = (( Sum co) + ( Sum d9)) by A62, AFINSQ_2: 55;

              

               A281: bo <> 0 by A1, PREPOWER: 5;

              then (( Sum d9) mod (b |^ o)) = 0 by A266, PEPIN: 6;

              then (n div (b |^ o)) = ((( Sum d9) div (b |^ o)) + (( Sum co) div (b |^ o))) by A280, NAT_D: 19;

              then ((n div (b |^ o)) * (b |^ o)) = ( Sum d9) by A275, A266, NAT_D: 3;

              then (E . o) = (((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1))) by A261, A279, AFINSQ_2: 53;

              then ((e . o) * (b |^ o)) = (((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1))) by A60, A61, A76, A77;

              then ((e . o) * (b |^ o)) = (((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * ((b |^ o) * (b |^ 1)))) by NEWTON: 8;

              then ((e . o) * (b |^ o)) = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * (b |^ 1))));

              then (((b |^ o) * (e . o)) / (b |^ o)) = (((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o));

              hence (d . a) = (e . a) by A235, A281, XCMPLX_1: 89;

            end;

          end;

          hence thesis by A76, FUNCT_1: 2;

        end;

        assume that n = 0 and

         A282: d = <% 0 %> & e = <% 0 %>;

        thus thesis by A282;

      end;

    end

    theorem :: NUMERAL1:4

    

     Th4: for n,b be Nat st b > 1 holds ( len ( digits (n,b))) >= 1

    proof

      let n,b be Nat;

      assume

       A1: b > 1;

      per cases ;

        suppose n = 0 ;

        then ( digits (n,b)) = <% 0 %> by A1, Def2;

        hence thesis by AFINSQ_1: 33;

      end;

        suppose n <> 0 ;

        then (( digits (n,b)) . (( len ( digits (n,b))) - 1)) <> 0 by A1, Def2;

        then (( len ( digits (n,b))) - 1) in ( dom ( digits (n,b))) by FUNCT_1:def 2;

        hence thesis by NAT_1: 14;

      end;

    end;

    theorem :: NUMERAL1:5

    

     Th5: for n,b be Nat st b > 1 holds ( value (( digits (n,b)),b)) = n

    proof

      let n,b be Nat;

      assume

       A1: b > 1;

      per cases ;

        suppose n <> 0 ;

        hence thesis by A1, Def2;

      end;

        suppose

         A2: n = 0 ;

        then

         A3: ( digits (n,b)) = <% 0 %> by A1, Def2;

        now

          let i be Nat;

          assume i in ( dom <% 0 %>);

          then i in { 0 } by AFINSQ_1:def 4, CARD_1: 49;

          then

           A4: i = 0 by TARSKI:def 1;

          

          hence ( <% 0 %> . i) = ( 0 * (b |^ i))

          .= ((( digits (n,b)) . i) * (b |^ i)) by A3, A4;

        end;

        then ( value (( digits (n,b)),b)) = ( Sum <% 0 %>) by A3, Def1;

        hence thesis by A2, AFINSQ_2: 53;

      end;

    end;

    begin

    theorem :: NUMERAL1:6

    

     Th6: for n,k be Nat st k = ((10 |^ n) - 1) holds 9 divides k

    proof

      defpred P[ Nat] means ex k be Nat st k = ((10 |^ $1) - 1) & 9 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 |^ k) - 1) and

         A3: 9 divides l;

        consider m be Nat such that

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

        

         A5: 9 divides (9 * ((m * 10) + 1)) by NAT_D:def 3;

        ((10 |^ (k + 1)) - 1) = ((((9 * m) + 1) * 10) - 1) by A2, A4, NEWTON: 6

        .= (9 * ((m * 10) + 1));

        hence P[(k + 1)] by A5;

      end;

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

      .= 0 ;

      then

       A6: P[ 0 ] by NAT_D: 6;

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

      then

       A7: ex l be Nat st l = ((10 |^ n) - 1) & 9 divides l;

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

      hence thesis by A7;

    end;

    theorem :: NUMERAL1:7

    for n,b be Nat st b > 1 holds b divides n iff (( digits (n,b)) . 0 ) = 0

    proof

      let n,b be Nat;

      reconsider B = b as Element of NAT by ORDINAL1:def 12;

      consider d be XFinSequence of NAT such that ( dom d) = ( dom ( digits (n,b))) and

       A1: for i be Nat st i in ( dom d) holds (d . i) = ((( digits (n,b)) . i) * (b |^ i)) and

       A2: ( value (( digits (n,b)),b)) = ( Sum d) by Def1;

      assume

       A3: b > 1;

      thus b divides n implies (( digits (n,b)) . 0 ) = 0

      proof

        

         A4: ( len ( digits (n,b))) >= 1 by A3, Th4;

        assume

         A5: b divides n;

        consider d be XFinSequence of NAT such that

         A6: ( dom d) = ( dom ( digits (n,b))) and

         A7: for i be Nat st i in ( dom d) holds (d . i) = ((( digits (n,b)) . i) * (b |^ i)) and

         A8: ( value (( digits (n,b)),b)) = ( Sum d) by Def1;

        per cases by A4, XXREAL_0: 1;

          suppose

           A9: ( len ( digits (n,b))) = 1;

          

           A10: b divides ( Sum d) by A3, A5, A8, Th5;

          

           A11: 0 in ( dom ( digits (n,b))) by A9, AFINSQ_1: 86;

          ( len d) = 1 by A6, A9;

          then d = <%(d . 0 )%> by AFINSQ_1: 34;

          

          then ( Sum d) = (d . 0 ) by AFINSQ_2: 53

          .= ((( digits (n,b)) . 0 ) * (b |^ 0 )) by A6, A7, A11;

          then

           A12: b divides ((( digits (n,b)) . 0 ) * 1) by A10, NEWTON: 4;

          per cases ;

            suppose n = 0 ;

            then ( digits (n,b)) = <% 0 %> by A3, Def2;

            hence thesis;

          end;

            suppose n <> 0 ;

            then (( digits (n,b)) . 0 ) < b by A3, A11, Def2;

            hence thesis by A12, NAT_D: 7;

          end;

        end;

          suppose

           A13: ( len ( digits (n,b))) > 1;

          then

          reconsider k = (( len ( digits (n,b))) - 1) as Element of NAT by NAT_1: 21;

          defpred P[ Nat, set] means $2 = (d . ($1 + 1));

           A14:

          now

            let l be Nat;

            assume l in ( dom <%(d . 0 )%>);

            then l in ( Segm 1) by AFINSQ_1:def 4;

            then l < 1 by NAT_1: 44;

            then l = 0 by NAT_1: 14;

            hence (d . l) = ( <%(d . 0 )%> . l);

          end;

          

           A15: for u be Nat st u in ( Segm k) holds ex x be Element of NAT st P[u, x];

          consider d9 be XFinSequence of NAT such that

           A16: ( dom d9) = ( Segm k) & for x be Nat st x in ( Segm k) holds P[x, (d9 . x)] from STIRL2_1:sch 5( A15);

          now

            let i be Nat;

            assume

             A17: i in ( dom d9);

            then i < ( len d9) by A16, NAT_1: 44;

            then (i + 1) < (k + 1) by XREAL_1: 8, A16;

            then

             A18: (i + 1) in ( dom d) by A6, AFINSQ_1: 86;

            (d9 . i) = (d . (i + 1)) by A16, A17

            .= ((( digits (n,b)) . (i + 1)) * (b |^ (i + 1))) by A7, A18

            .= ((( digits (n,b)) . (i + 1)) * ((b |^ i) * b)) by NEWTON: 6

            .= (b * ((( digits (n,b)) . (i + 1)) * (b |^ i)));

            hence b divides (d9 . i) by NAT_D:def 3;

          end;

          then b divides ( Sum d9) by Th2;

          then

           A19: (( Sum d9) mod B) = 0 by A3, PEPIN: 6;

           A20:

          now

            let l be Nat;

            

             A21: (( len <%(d . 0 )%>) + l) = (l + 1) by AFINSQ_1: 34;

            assume l in ( dom d9);

            hence (d . (( len <%(d . 0 )%>) + l)) = (d9 . l) by A16, A21;

          end;

          

           A22: 0 in ( dom ( digits (n,b))) by A13, AFINSQ_1: 86;

          ( dom d) = (k + 1) by A6

          .= (( len <%(d . 0 )%>) + ( len d9)) by A16, AFINSQ_1: 33;

          then d = ( <%(d . 0 )%> ^ d9) by A14, A20, AFINSQ_1:def 3;

          then ( Sum d) = (( Sum <%(d . 0 )%>) + ( Sum d9)) by AFINSQ_2: 55;

          then n = (( Sum <%(d . 0 )%>) + ( Sum d9)) by A3, A8, Th5;

          then n = ((d . 0 ) + ( Sum d9)) by AFINSQ_2: 53;

          then (((d . 0 ) + ( Sum d9)) mod B) = 0 by A3, A5, PEPIN: 6;

          then ((d . 0 ) mod b) = 0 by A19, NAT_D: 17;

          then B divides (d . 0 ) by A3, PEPIN: 6;

          then b divides ((( digits (n,b)) . 0 ) * (b |^ 0 )) by A6, A7, A22;

          then

           A23: b divides ((( digits (n,b)) . 0 ) * 1) by NEWTON: 4;

          per cases ;

            suppose n = 0 ;

            then ( digits (n,b)) = <% 0 %> by A3, Def2;

            hence thesis;

          end;

            suppose n <> 0 ;

            then (( digits (n,b)) . 0 ) < b by A3, A22, Def2;

            hence thesis by A23, NAT_D: 7;

          end;

        end;

      end;

      assume

       A24: (( digits (n,b)) . 0 ) = 0 ;

      now

        let i be Nat;

        assume

         A25: i in ( dom d);

        per cases ;

          suppose i = 0 ;

          

          then (d . i) = ((( digits (n,b)) . 0 ) * (b |^ 0 )) by A1, A25

          .= ((( digits (n,b)) . 0 ) * 1) by NEWTON: 4;

          hence b divides (d . i) by A24, NAT_D: 6;

        end;

          suppose i > 0 ;

          then

          consider j be Nat such that

           A26: (j + 1) = i by NAT_1: 6;

          (d . i) = ((( digits (n,b)) . i) * (b |^ (j + 1))) by A1, A25, A26

          .= ((( digits (n,b)) . i) * ((b |^ j) * b)) by NEWTON: 6

          .= (b * ((( digits (n,b)) . i) * (b |^ j)));

          hence b divides (d . i) by NAT_D:def 3;

        end;

      end;

      then b divides ( value (( digits (n,b)),b)) by A2, Th2;

      hence thesis by A3, Th5;

    end;

    theorem :: NUMERAL1:8

    for n be Nat holds 2 divides n iff 2 divides (( digits (n,10)) . 0 )

    proof

      let n be Nat;

      consider d be XFinSequence of NAT such that ( dom d) = ( dom ( digits (n,10))) and

       A1: for i be Nat st i in ( dom d) holds (d . i) = ((( digits (n,10)) . i) * (10 |^ i)) and

       A2: ( value (( digits (n,10)),10)) = ( Sum d) by Def1;

      thus 2 divides n implies 2 divides (( digits (n,10)) . 0 )

      proof

        

         A3: ( len ( digits (n,10))) >= 1 by Th4;

        assume

         A4: 2 divides n;

        consider d be XFinSequence of NAT such that

         A5: ( dom d) = ( dom ( digits (n,10))) and

         A6: for i be Nat st i in ( dom d) holds (d . i) = ((( digits (n,10)) . i) * (10 |^ i)) and

         A7: ( value (( digits (n,10)),10)) = ( Sum d) by Def1;

        per cases by A3, XXREAL_0: 1;

          suppose

           A8: ( len ( digits (n,10))) = 1;

          then

           A9: 0 in ( dom ( digits (n,10))) by AFINSQ_1: 86;

          

           A10: 2 divides ( Sum d) by A4, A7, Th5;

          ( len d) = 1 by A5, A8;

          then d = <%(d . 0 )%> by AFINSQ_1: 34;

          

          then ( Sum d) = (d . 0 ) by AFINSQ_2: 53

          .= ((( digits (n,10)) . 0 ) * (10 |^ 0 )) by A5, A6, A9;

          then 2 divides ((( digits (n,10)) . 0 ) * 1) by A10, NEWTON: 4;

          hence thesis;

        end;

          suppose

           A11: ( len ( digits (n,10))) > 1;

          then

          reconsider k = (( len ( digits (n,10))) - 1) as Element of NAT by NAT_1: 21;

          defpred P[ Nat, set] means $2 = (d . ($1 + 1));

           A12:

          now

            let l be Nat;

            assume l in ( dom <%(d . 0 )%>);

            then l in ( Segm 1) by AFINSQ_1:def 4;

            then l < 1 by NAT_1: 44;

            then l = 0 by NAT_1: 14;

            hence (d . l) = ( <%(d . 0 )%> . l);

          end;

          

           A13: for u be Nat st u in ( Segm k) holds ex x be Element of NAT st P[u, x];

          consider d9 be XFinSequence of NAT such that

           A14: ( dom d9) = ( Segm k) & for x be Nat st x in ( Segm k) holds P[x, (d9 . x)] from STIRL2_1:sch 5( A13);

          now

            let i be Nat;

            assume

             A15: i in ( dom d9);

            then i < ( len d9) by A14, NAT_1: 44;

            then (i + 1) < (k + 1) by XREAL_1: 8, A14;

            then

             A16: (i + 1) in ( dom d) by A5, AFINSQ_1: 86;

            (d9 . i) = (d . (i + 1)) by A14, A15

            .= ((( digits (n,10)) . (i + 1)) * (10 |^ (i + 1))) by A6, A16

            .= ((( digits (n,10)) . (i + 1)) * ((10 |^ i) * 10)) by NEWTON: 6

            .= (2 * (((( digits (n,10)) . (i + 1)) * (10 |^ i)) * 5));

            hence 2 divides (d9 . i) by NAT_D:def 3;

          end;

          then 2 divides ( Sum d9) by Th2;

          then

           A17: (( Sum d9) mod 2) = 0 by PEPIN: 6;

           A18:

          now

            let l be Nat;

            

             A19: (( len <%(d . 0 )%>) + l) = (l + 1) by AFINSQ_1: 34;

            assume l in ( dom d9);

            hence (d . (( len <%(d . 0 )%>) + l)) = (d9 . l) by A14, A19;

          end;

          ( dom d) = (k + 1) by A5

          .= (( len <%(d . 0 )%>) + ( len d9)) by A14, AFINSQ_1: 33;

          then d = ( <%(d . 0 )%> ^ d9) by A12, A18, AFINSQ_1:def 3;

          then ( Sum d) = (( Sum <%(d . 0 )%>) + ( Sum d9)) by AFINSQ_2: 55;

          then n = (( Sum <%(d . 0 )%>) + ( Sum d9)) by A7, Th5;

          then n = ((d . 0 ) + ( Sum d9)) by AFINSQ_2: 53;

          then (((d . 0 ) + ( Sum d9)) mod 2) = 0 by A4, PEPIN: 6;

          then ((d . 0 ) mod 2) = 0 by A17, NAT_D: 17;

          then

           A20: 2 divides (d . 0 ) by PEPIN: 6;

           0 in ( dom ( digits (n,10))) by A11, AFINSQ_1: 86;

          then 2 divides ((( digits (n,10)) . 0 ) * (10 |^ 0 )) by A5, A6, A20;

          then 2 divides ((( digits (n,10)) . 0 ) * 1) by NEWTON: 4;

          hence thesis;

        end;

      end;

      assume

       A21: 2 divides (( digits (n,10)) . 0 );

      now

        let i be Nat;

        assume

         A22: i in ( dom d);

        per cases ;

          suppose i = 0 ;

          

          then (d . i) = ((( digits (n,10)) . 0 ) * (10 |^ 0 )) by A1, A22

          .= ((( digits (n,10)) . 0 ) * 1) by NEWTON: 4;

          hence 2 divides (d . i) by A21;

        end;

          suppose i > 0 ;

          then

          consider j be Nat such that

           A23: (j + 1) = i by NAT_1: 6;

          (d . i) = ((( digits (n,10)) . i) * (10 |^ (j + 1))) by A1, A22, A23

          .= ((( digits (n,10)) . i) * ((10 |^ j) * 10)) by NEWTON: 6

          .= (2 * (((( digits (n,10)) . i) * (10 |^ j)) * 5));

          hence 2 divides (d . i) by NAT_D:def 3;

        end;

      end;

      then 2 divides ( value (( digits (n,10)),10)) by A2, Th2;

      hence thesis by Th5;

    end;

    ::$Notion-Name

    theorem :: NUMERAL1:9

    for n be Nat holds 3 divides n iff 3 divides ( Sum ( digits (n,10)))

    proof

      let n be Nat;

      consider p be XFinSequence of NAT such that

       A1: ( dom p) = ( dom ( digits (n,10))) and

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

       A3: ( value (( digits (n,10)),10)) = ( Sum p) by Def1;

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

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

      

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

      consider p9 be XFinSequence of NAT such that

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

       A6:

      now

        let i be Nat;

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

        reconsider dz as Element of NAT by ORDINAL1:def 12;

        3 divides (3 * 3) & 9 divides dz by Th6, NAT_D:def 3;

        then 3 divides dz by NAT_D: 4;

        then 3 divides ((( digits (n,10)) . i) * dz) by NAT_D: 9;

        then

         A7: (((( digits (n,10)) . i) * dz) mod 3) = 0 by PEPIN: 6;

        assume

         A8: i in ( dom p);

        

        hence (p9 . i) = ((p . i) mod 3) by A5

        .= (((( digits (n,10)) . i) * (dz + 1)) mod 3) by A2, A8

        .= ((((( digits (n,10)) . i) * dz) + (( digits (n,10)) . i)) mod 3)

        .= (( 0 qua Nat + (( digits (n,10)) . i)) mod 3) by A7, NAT_D: 22

        .= ((( digits (n,10)) . i) mod 3);

      end;

      thus 3 divides n implies 3 divides ( Sum ( digits (n,10)))

      proof

        assume 3 divides n;

        then 3 divides ( Sum p) by A3, Th5;

        then (( Sum p) mod 3) = 0 by PEPIN: 6;

        then (( Sum p9) mod 3) = 0 by A5, Th3;

        then (( Sum ( digits (n,10))) mod 3) = 0 by A1, A5, A6, Th3;

        hence thesis by PEPIN: 6;

      end;

      assume 3 divides ( Sum ( digits (n,10)));

      then (( Sum ( digits (n,10))) mod 3) = 0 by PEPIN: 6;

      then (( Sum p9) mod 3) = 0 by A1, A5, A6, Th3;

      then (( Sum p) mod 3) = 0 by A5, Th3;

      then 3 divides ( Sum p) by PEPIN: 6;

      hence thesis by A3, Th5;

    end;

    theorem :: NUMERAL1:10

    for n be Nat holds 5 divides n iff 5 divides (( digits (n,10)) . 0 )

    proof

      let n be Nat;

      consider d be XFinSequence of NAT such that ( dom d) = ( dom ( digits (n,10))) and

       A1: for i be Nat st i in ( dom d) holds (d . i) = ((( digits (n,10)) . i) * (10 |^ i)) and

       A2: ( value (( digits (n,10)),10)) = ( Sum d) by Def1;

      thus 5 divides n implies 5 divides (( digits (n,10)) . 0 )

      proof

        

         A3: ( len ( digits (n,10))) >= 1 by Th4;

        assume

         A4: 5 divides n;

        consider d be XFinSequence of NAT such that

         A5: ( dom d) = ( dom ( digits (n,10))) and

         A6: for i be Nat st i in ( dom d) holds (d . i) = ((( digits (n,10)) . i) * (10 |^ i)) and

         A7: ( value (( digits (n,10)),10)) = ( Sum d) by Def1;

        per cases by A3, XXREAL_0: 1;

          suppose

           A8: ( len ( digits (n,10))) = 1;

          then

           A9: 0 in ( dom ( digits (n,10))) by AFINSQ_1: 86;

          

           A10: 5 divides ( Sum d) by A4, A7, Th5;

          ( len d) = 1 by A5, A8;

          then d = <%(d . 0 )%> by AFINSQ_1: 34;

          

          then ( Sum d) = (d . 0 ) by AFINSQ_2: 53

          .= ((( digits (n,10)) . 0 ) * (10 |^ 0 )) by A5, A6, A9;

          then 5 divides ((( digits (n,10)) . 0 ) * 1) by A10, NEWTON: 4;

          hence thesis;

        end;

          suppose

           A11: ( len ( digits (n,10))) > 1;

          then

          reconsider k = (( len ( digits (n,10))) - 1) as Element of NAT by NAT_1: 21;

          defpred P[ Nat, set] means $2 = (d . ($1 + 1));

           A12:

          now

            let l be Nat;

            assume l in ( dom <%(d . 0 )%>);

            then l in ( Segm 1) by AFINSQ_1:def 4;

            then l < 1 by NAT_1: 44;

            then l = 0 by NAT_1: 14;

            hence (d . l) = ( <%(d . 0 )%> . l);

          end;

          

           A13: for u be Nat st u in ( Segm k) holds ex x be Element of NAT st P[u, x];

          consider d9 be XFinSequence of NAT such that

           A14: ( dom d9) = ( Segm k) & for x be Nat st x in ( Segm k) holds P[x, (d9 . x)] from STIRL2_1:sch 5( A13);

          now

            let i be Nat;

            assume

             A15: i in ( dom d9);

            then i < ( len d9) by A14, NAT_1: 44;

            then (i + 1) < (k + 1) by XREAL_1: 8, A14;

            then

             A16: (i + 1) in ( dom d) by A5, AFINSQ_1: 86;

            (d9 . i) = (d . (i + 1)) by A14, A15

            .= ((( digits (n,10)) . (i + 1)) * (10 |^ (i + 1))) by A6, A16

            .= ((( digits (n,10)) . (i + 1)) * ((10 |^ i) * 10)) by NEWTON: 6

            .= (5 * (((( digits (n,10)) . (i + 1)) * (10 |^ i)) * 2));

            hence 5 divides (d9 . i) by NAT_D:def 3;

          end;

          then 5 divides ( Sum d9) by Th2;

          then

           A17: (( Sum d9) mod 5) = 0 by PEPIN: 6;

           A18:

          now

            let l be Nat;

            

             A19: (( len <%(d . 0 )%>) + l) = (l + 1) by AFINSQ_1: 34;

            assume l in ( dom d9);

            hence (d . (( len <%(d . 0 )%>) + l)) = (d9 . l) by A14, A19;

          end;

          ( dom d) = (k + 1) by A5

          .= (( len <%(d . 0 )%>) + ( len d9)) by A14, AFINSQ_1: 33;

          then d = ( <%(d . 0 )%> ^ d9) by A12, A18, AFINSQ_1:def 3;

          then ( Sum d) = (( Sum <%(d . 0 )%>) + ( Sum d9)) by AFINSQ_2: 55;

          then n = (( Sum <%(d . 0 )%>) + ( Sum d9)) by A7, Th5;

          then n = ((d . 0 ) + ( Sum d9)) by AFINSQ_2: 53;

          then (((d . 0 ) + ( Sum d9)) mod 5) = 0 by A4, PEPIN: 6;

          then ((d . 0 ) mod 5) = 0 by A17, NAT_D: 17;

          then

           A20: 5 divides (d . 0 ) by PEPIN: 6;

           0 in ( dom ( digits (n,10))) by A11, AFINSQ_1: 86;

          then 5 divides ((( digits (n,10)) . 0 ) * (10 |^ 0 )) by A5, A6, A20;

          then 5 divides ((( digits (n,10)) . 0 ) * 1) by NEWTON: 4;

          hence thesis;

        end;

      end;

      assume

       A21: 5 divides (( digits (n,10)) . 0 );

      now

        let i be Nat;

        assume

         A22: i in ( dom d);

        per cases ;

          suppose i = 0 ;

          

          then (d . i) = ((( digits (n,10)) . 0 ) * (10 |^ 0 )) by A1, A22

          .= ((( digits (n,10)) . 0 ) * 1) by NEWTON: 4;

          hence 5 divides (d . i) by A21;

        end;

          suppose i > 0 ;

          then

          consider j be Nat such that

           A23: (j + 1) = i by NAT_1: 6;

          (d . i) = ((( digits (n,10)) . i) * (10 |^ (j + 1))) by A1, A22, A23

          .= ((( digits (n,10)) . i) * ((10 |^ j) * 10)) by NEWTON: 6

          .= (5 * (((( digits (n,10)) . i) * (10 |^ j)) * 2));

          hence 5 divides (d . i) by NAT_D:def 3;

        end;

      end;

      then 5 divides ( value (( digits (n,10)),10)) by A2, Th2;

      hence thesis by Th5;

    end;