newton.miz



    begin

    reserve i,j,k,n,m,l,s,t for Nat;

    reserve a,b for Real;

    reserve F,G,H for FinSequence of REAL ;

    theorem :: NEWTON:1

    

     Th1: n >= 1 implies ( Seg n) = (( {1} \/ { k where k be Element of NAT : 1 < k & k < n }) \/ {n})

    proof

      assume

       A1: n >= 1;

      

       A2: (( {1} \/ { k where k be Element of NAT : 1 < k & k < n }) \/ {n}) c= ( Seg n)

      proof

        let d be object;

        

         A3: { k where k be Element of NAT : 1 < k & k < n } c= ( Seg n)

        proof

          let d be object;

          assume d in { k where k be Element of NAT : 1 < k & k < n };

          then ex k be Element of NAT st d = k & 1 < k & k < n;

          hence thesis;

        end;

        1 in ( Seg n) by A1;

        then {1} c= ( Seg n) by ZFMISC_1: 31;

        then

         A4: ( {1} \/ { k where k be Element of NAT : 1 < k & k < n }) c= ( Seg n) by A3, XBOOLE_1: 8;

        n in ( Seg n) by A1;

        then {n} c= ( Seg n) by ZFMISC_1: 31;

        then (( {1} \/ { k where k be Element of NAT : 1 < k & k < n }) \/ {n}) c= ( Seg n) by A4, XBOOLE_1: 8;

        hence thesis;

      end;

      ( Seg n) c= (( {1} \/ { k where k be Element of NAT : 1 < k & k < n }) \/ {n})

      proof

        let d be object;

        assume

         A5: d in ( Seg n);

        per cases by A1, XXREAL_0: 1;

          suppose

           A6: n > 1;

          reconsider l = d as Element of NAT by A5;

          

           A7: l <= n by A5, FINSEQ_1: 1;

          1 <= l by A5, FINSEQ_1: 1;

          then 1 = l or 1 < l & l < n or l = n or 1 = n by A7, XXREAL_0: 1;

          then d in {1} or d in { k where k be Element of NAT : 1 < k & k < n } or d in {n} by A6, TARSKI:def 1;

          then d in ( {1} \/ { k where k be Element of NAT : 1 < k & k < n }) or d in {n} by XBOOLE_0:def 3;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose n = 1;

          hence thesis by A5, FINSEQ_1: 2, XBOOLE_0:def 3;

        end;

      end;

      hence thesis by A2;

    end;

    theorem :: NEWTON:2

    

     Th2: ( len (a * F)) = ( len F)

    proof

      reconsider G = F as Element of (( len F) -tuples_on REAL ) by FINSEQ_2: 92;

      ( len (a * G)) = ( len G) by CARD_1:def 7;

      hence thesis;

    end;

    theorem :: NEWTON:3

    ( dom G) = ( dom (a * G)) by VALUED_1:def 5;

    registration

      let x be Complex, n be natural Number;

      cluster (n |-> x) -> complex-valued;

      coherence ;

    end

    definition

      let x be Complex, n be natural Number;

      :: NEWTON:def1

      func x |^ n -> number equals ( Product (n |-> x));

      coherence by TARSKI: 1;

    end

    registration

      let x be Real, n be natural Number;

      cluster (x |^ n) -> real;

      coherence ;

    end

    reserve z for Complex;

    registration

      let z be Complex, n be natural Number;

      cluster (z |^ n) -> complex;

      coherence ;

    end

    theorem :: NEWTON:4

    (z |^ 0 ) = 1 by RVSUM_1: 94;

    theorem :: NEWTON:5

    

     Th5: (z |^ 1) = z

    proof

      

      thus (z |^ 1) = ( Product <*z*>) by FINSEQ_2: 59

      .= z;

    end;

    registration

      let a be Complex;

      reduce (a |^ 1) to a;

      reducibility by Th5;

    end

    theorem :: NEWTON:6

    

     Th6: (z |^ (s + 1)) = ((z |^ s) * z)

    proof

      

      thus (z |^ (s + 1)) = ( Product ((s |-> z) ^ <*z*>)) by FINSEQ_2: 60

      .= ((z |^ s) * z) by RVSUM_1: 96;

    end;

    registration

      let x,n be natural Number;

      cluster (x |^ n) -> natural;

      coherence

      proof

        

         A0: n is Nat by TARSKI: 1;

        defpred P[ Nat] means (x |^ $1) is natural;

        

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

        proof

          let a be Nat;

          assume P[a];

          then

          reconsider b = (x |^ a) as Nat;

          (x |^ (a + 1)) = (b * x) by Th6;

          hence thesis;

        end;

        

         A2: P[ 0 ] by RVSUM_1: 94;

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

        hence thesis by A0;

      end;

    end

    reserve x,y for Complex;

    reserve r,s,t for natural Number;

    theorem :: NEWTON:7

    ((x * y) |^ s) = ((x |^ s) * (y |^ s))

    proof

      reconsider x, y as Element of COMPLEX by XCMPLX_0:def 2;

      ((x |^ s) * (y |^ s)) = ( Product (s |-> (x * y))) by RVSUM_1: 113;

      hence thesis;

    end;

    theorem :: NEWTON:8

    

     Th8: (x |^ (s + t)) = ((x |^ s) * (x |^ t))

    proof

      reconsider x as Element of COMPLEX by XCMPLX_0:def 2;

      ((x |^ s) * (x |^ t)) = ( Product ((s + t) |-> x)) by RVSUM_1: 111;

      hence thesis;

    end;

    theorem :: NEWTON:9

    ((x |^ s) |^ t) = (x |^ (s * t))

    proof

      reconsider x as Element of COMPLEX by XCMPLX_0:def 2;

      (x |^ (s * t)) = ( Product (t |-> (x |^ s))) by RVSUM_1: 112;

      hence thesis;

    end;

    theorem :: NEWTON:10

    

     Th10: (1 |^ s) = 1

    proof

      

       A0: s is Nat by TARSKI: 1;

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

       A1:

      now

        let s be Nat;

        assume P[s];

        then (1 |^ (s + 1)) = (1 * 1) by Th6;

        hence P[(s + 1)];

      end;

      

       A2: P[ 0 ] by RVSUM_1: 94;

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

      hence thesis by A0;

    end;

    registration

      let n be Nat;

      reduce (1 |^ n) to 1;

      reducibility by Th10;

    end

    theorem :: NEWTON:11

    

     Th11: s >= 1 implies ( 0 |^ s) = 0

    proof

      

       A0: s is Nat by TARSKI: 1;

      defpred P[ Nat] means ( 0 |^ $1) = 0 ;

       A1:

      now

        let n be Nat;

        assume n >= 1 & P[n];

        ( 0 |^ (n + 1)) = (( 0 |^ n) * 0 ) by Th6

        .= 0 ;

        hence P[(n + 1)];

      end;

      

       A2: P[1];

      for n be Nat st n >= 1 holds P[n] from NAT_1:sch 8( A2, A1);

      hence thesis by A0;

    end;

    registration

      let n be natural Number;

      cluster ( idseq n) -> natural-valued;

      coherence

      proof

        reconsider n as Nat by TARSKI: 1;

        ( Seg n) is natural-membered;

        hence thesis;

      end;

    end

    definition

      let n be natural Number;

      :: NEWTON:def2

      func n ! -> number equals ( Product ( idseq n));

      coherence by TARSKI: 1;

    end

    registration

      let n be natural Number;

      cluster (n ! ) -> real;

      coherence ;

    end

    theorem :: NEWTON:12

    

     Th12: ( 0 ! ) = 1 by RVSUM_1: 94;

    theorem :: NEWTON:13

    (1 ! ) = 1 by FINSEQ_2: 50;

    theorem :: NEWTON:14

    (2 ! ) = 2

    proof

      

      thus (2 ! ) = (1 * 2) by FINSEQ_2: 52, RVSUM_1: 99

      .= 2;

    end;

    theorem :: NEWTON:15

    

     Th15: ((s + 1) ! ) = ((s ! ) * (s + 1))

    proof

      ( idseq (s + 1)) = (( idseq s) ^ <*(s + 1)*>) by FINSEQ_2: 51;

      hence thesis by RVSUM_1: 96;

    end;

    theorem :: NEWTON:16

    

     Th16: (s ! ) is Element of NAT

    proof

      

       A0: s is Nat by TARSKI: 1;

      defpred P[ Nat] means ($1 ! ) is Element of NAT ;

       A1:

      now

        let s be Nat;

        assume P[s];

        then

        reconsider k = (s ! ) as Element of NAT ;

        ((s + 1) ! ) = ((s + 1) * k) by Th15;

        hence P[(s + 1)];

      end;

      

       A2: P[ 0 ] by RVSUM_1: 94;

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

      hence thesis by A0;

    end;

    registration

      let n be natural Number;

      cluster (n ! ) -> natural;

      coherence by Th16;

    end

    theorem :: NEWTON:17

    

     Th17: (s ! ) > 0

    proof

      

       A0: s is Nat by TARSKI: 1;

      defpred P[ Nat] means ($1 ! ) > 0 ;

       A1:

      now

        let s be Nat;

        assume P[s];

        then ((s + 1) * (s ! )) > ((s + 1) * 0 );

        hence P[(s + 1)] by Th15;

      end;

      

       A2: P[ 0 ] by RVSUM_1: 94;

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

      hence thesis by A0;

    end;

    registration

      let n be natural Number;

      cluster (n ! ) -> positive;

      coherence by Th17;

    end

    theorem :: NEWTON:18

    ((s ! ) * (t ! )) <> 0 ;

    definition

      let k,n be natural Number;

      :: NEWTON:def3

      func n choose k -> number means

      : Def3: for l be Nat st l = (n - k) holds it = ((n ! ) / ((k ! ) * (l ! ))) if n >= k

      otherwise it = 0 ;

      consistency ;

      existence

      proof

        thus n >= k implies ex r1 be set st for l be Nat st l = (n - k) holds r1 = ((n ! ) / ((k ! ) * (l ! )))

        proof

          assume n >= k;

          then

          reconsider m = (n - k) as Element of NAT by INT_1: 5;

          take ((n ! ) / ((k ! ) * (m ! )));

          thus thesis;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let r1,r2 be set;

        thus n >= k & (for l be Nat st l = (n - k) holds r1 = ((n ! ) / ((k ! ) * (l ! )))) & (for l be Nat st l = (n - k) holds r2 = ((n ! ) / ((k ! ) * (l ! )))) implies r1 = r2

        proof

          assume n >= k;

          then

          reconsider m = (n - k) as Element of NAT by INT_1: 5;

          assume that

           A1: for l be Nat st l = (n - k) holds r1 = ((n ! ) / ((k ! ) * (l ! ))) and

           A2: for l be Nat st l = (n - k) holds r2 = ((n ! ) / ((k ! ) * (l ! )));

          r1 = ((n ! ) / ((k ! ) * (m ! ))) by A1;

          hence thesis by A2;

        end;

        thus thesis;

      end;

    end

    registration

      let k,n be natural Number;

      cluster (n choose k) -> real;

      coherence

      proof

        per cases ;

          suppose

           A1: n >= k;

          then

          reconsider l = (n - k) as Element of NAT by INT_1: 5;

          (n choose k) = ((n ! ) / ((k ! ) * (l ! ))) by A1, Def3;

          hence thesis;

        end;

          suppose n < k;

          hence thesis by Def3;

        end;

      end;

    end

    theorem :: NEWTON:19

    

     Th19: (s choose 0 ) = 1

    proof

      reconsider m = (s - 0 ) as Element of NAT by ORDINAL1:def 12;

      m = s;

      

      then (s choose 0 ) = ((s ! ) / (1 * (s ! ))) by Def3, Th12

      .= 1 by XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: NEWTON:20

    

     Th20: s >= t & r = (s - t) implies (s choose t) = (s choose r)

    proof

      assume

       A1: s >= t;

      (t - s) >= ( 0 - s) by XREAL_1: 9;

      then

       A2: ( - ( - s)) >= ( - (t - s)) by XREAL_1: 24;

      assume

       A3: r = (s - t);

      then t = (s - r);

      then (s choose r) = ((s ! ) / ((r ! ) * (t ! ))) by A2, Def3;

      hence thesis by A1, A3, Def3;

    end;

    theorem :: NEWTON:21

    

     Th21: (s choose s) = 1

    proof

      reconsider m = (s - s) as Element of NAT by INT_1: 5;

      m = 0 ;

      then (s choose s) = (s choose 0 ) by Th20;

      hence thesis by Th19;

    end;

    theorem :: NEWTON:22

    

     Th22: ((t + 1) choose (s + 1)) = ((t choose (s + 1)) + (t choose s))

    proof

      per cases by XXREAL_0: 1;

        suppose

         A1: s < t;

        thus ((t + 1) choose (s + 1)) = ((t choose (s + 1)) + (t choose s))

        proof

          reconsider m1 = (t - s) as Element of NAT by A1, INT_1: 5;

          

           A2: (s + 1) <= t by A1, NAT_1: 13;

          then

          reconsider m2 = (t - (s + 1)) as Element of NAT by INT_1: 5;

          

           A3: (s + 1) <= (t + 1) by A1, XREAL_1: 6;

          then

          reconsider m = ((t + 1) - (s + 1)) as Element of NAT by INT_1: 5;

          (t choose (s + 1)) = ((t ! ) / (((s + 1) ! ) * (m2 ! ))) by A2, Def3;

          

          then

           A4: ((t choose (s + 1)) + (t choose s)) = (((t ! ) / (((s + 1) ! ) * (m2 ! ))) + ((t ! ) / ((s ! ) * (m1 ! )))) by A1, Def3

          .= ((((t ! ) * ((s ! ) * (m1 ! ))) + ((t ! ) * (((s + 1) ! ) * (m2 ! )))) / ((((s + 1) ! ) * (m2 ! )) * ((s ! ) * (m1 ! )))) by XCMPLX_1: 116

          .= ((((t ! ) * ((s ! ) * (m1 ! ))) + ((t ! ) * (((s ! ) * (s + 1)) * (m2 ! )))) / ((((s + 1) ! ) * (m2 ! )) * ((s ! ) * (m1 ! )))) by Th15

          .= (((s ! ) * ((t ! ) * ((m1 ! ) + ((s + 1) * (m2 ! ))))) / ((s ! ) * ((m1 ! ) * (((s + 1) ! ) * (m2 ! )))))

          .= (((t ! ) * (((m2 + 1) ! ) + ((s + 1) * (m2 ! )))) / ((m1 ! ) * (((s + 1) ! ) * (m2 ! )))) by XCMPLX_1: 91

          .= (((t ! ) * (((m2 ! ) * (m2 + 1)) + ((m2 ! ) * (s + 1)))) / ((m1 ! ) * (((s + 1) ! ) * (m2 ! )))) by Th15

          .= (((m2 ! ) * ((t ! ) * ((m2 + 1) + (s + 1)))) / ((m2 ! ) * (((s + 1) ! ) * (m1 ! ))))

          .= (((t ! ) * (t - (s - (s + 1)))) / (((s + 1) ! ) * (m1 ! ))) by XCMPLX_1: 91

          .= (((t + 1) ! ) / (((s + 1) ! ) * (m1 ! ))) by Th15;

          m = m1;

          hence thesis by A4, A3, Def3;

        end;

      end;

        suppose

         A5: s = t;

        then s < (t + 1) by NAT_1: 13;

        then

         A6: (t choose (s + 1)) = 0 by A5, Def3;

        ((t + 1) choose (s + 1)) = 1 by A5, Th21;

        hence thesis by A5, A6, Th21;

      end;

        suppose

         A7: s > t;

        then (s + 1) > (t + 1) by XREAL_1: 8;

        then

         A8: ((t + 1) choose (s + 1)) = 0 by Def3;

        

         A9: (s + 1) > (t + 0 ) by A7, XREAL_1: 8;

        (t choose s) = 0 by A7, Def3;

        hence thesis by A9, A8, Def3;

      end;

    end;

    theorem :: NEWTON:23

    

     Th23: s >= 1 implies (s choose 1) = s

    proof

      

       A0: s is Nat by TARSKI: 1;

      defpred P[ Nat] means ($1 choose 1) = $1;

       A1:

      now

        let n be Nat;

        assume that n >= 1 and

         A2: P[n];

        ((n + 1) choose 1) = ((n + 1) choose ( 0 + 1))

        .= (n + (n choose 0 )) by A2, Th22

        .= (n + 1) by Th19;

        hence P[(n + 1)];

      end;

      

       A3: P[1] by Th21;

      for n be Nat st n >= 1 holds P[n] from NAT_1:sch 8( A3, A1);

      hence thesis by A0;

    end;

    theorem :: NEWTON:24

    s >= 1 & t = (s - 1) implies (s choose t) = s

    proof

      assume that

       A1: s >= 1 and

       A2: t = (s - 1);

      (s choose t) = (s choose 1) by A1, A2, Th20;

      hence thesis by A1, Th23;

    end;

    theorem :: NEWTON:25

    

     Th25: (s choose r) is Element of NAT

    proof

      

       A0: s is Nat by TARSKI: 1;

      defpred P[ Nat] means for r holds ($1 choose r) is Element of NAT ;

      

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

      proof

        let s be Nat;

        assume

         A2: P[s];

        

         A3: for r st r <> 0 holds ((s + 1) choose r) is Element of NAT

        proof

          let r;

          assume

           A4: r <> 0 ;

          ((s + 1) choose r) is Element of NAT

          proof

            consider t be Nat such that

             A5: r = (t + 1) by A4, NAT_1: 6;

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

            reconsider m1 = (s choose t), m2 = (s choose (t + 1)) as Element of NAT by A2;

            (m1 + m2) = ((s choose t) + (s choose (t + 1)));

            hence thesis by A5, Th22;

          end;

          hence thesis;

        end;

        let r;

        r = 0 or r <> 0 ;

        hence thesis by A3, Th19;

      end;

      

       A6: P[ 0 ]

      proof

        let r;

        r = 0 or r > 0 ;

        hence thesis by Def3, Th19;

      end;

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

      hence thesis by A0;

    end;

    theorem :: NEWTON:26

    for m, F st m <> 0 & ( len F) = m & (for i, l st i in ( dom F) & l = ((n + i) - 1) holds (F . i) = (l choose n)) holds ( Sum F) = ((n + m) choose (n + 1))

    proof

      defpred P[ Nat] means for F st $1 <> 0 & ( len F) = $1 & (for i, l st i in ( dom F) & l = ((n + i) - 1) holds (F . i) = (l choose n)) holds ( Sum F) = ((n + $1) choose (n + 1));

      

       A1: for m st P[m] holds P[(m + 1)]

      proof

        let m;

        assume

         A2: P[m];

        let F;

        assume that (m + 1) <> 0 and

         A3: ( len F) = (m + 1) and

         A4: for i, l st i in ( dom F) & l = ((n + i) - 1) holds (F . i) = (l choose n);

        consider G be FinSequence of REAL , x be Element of REAL such that

         A5: F = (G ^ <*x*>) by A3, FINSEQ_2: 19;

        

         A6: (m + 1) = (( len G) + 1) by A3, A5, FINSEQ_2: 16;

        per cases ;

          suppose

           A7: m = 0 ;

          

           A8: n = ((n + 1) - 1);

          reconsider c = (n choose n) as Element of REAL by XREAL_0:def 1;

          

           A9: ( dom F) = ( Seg 1) by A3, A7, FINSEQ_1:def 3;

          then 1 in ( dom F);

          then (F . 1) = (n choose n) by A4, A8;

          

          hence ( Sum F) = ( Sum <*c*>) by A9, FINSEQ_1:def 8

          .= (n choose n) by FINSOP_1: 11

          .= 1 by Th21

          .= ((n + (m + 1)) choose (n + 1)) by A7, Th21;

        end;

          suppose

           A10: m <> 0 ;

          

           A11: (n + m) = ((n + (m + 1)) - 1);

          

           A12: for i, l st i in ( dom G) & l = ((n + i) - 1) holds (G . i) = (l choose n)

          proof

            

             A13: ( dom G) c= ( dom F) by A5, FINSEQ_1: 26;

            let i, l;

            assume that

             A14: i in ( dom G) and

             A15: l = ((n + i) - 1);

            (G . i) = (F . i) by A5, A14, FINSEQ_1:def 7;

            hence thesis by A4, A14, A15, A13;

          end;

          ( dom F) = ( Seg (m + 1)) by A3, FINSEQ_1:def 3;

          

          then

           A16: ((n + m) choose n) = ((G ^ <*x*>) . (( len G) + 1)) by A4, A5, A6, A11, FINSEQ_1: 4

          .= x by FINSEQ_1: 42;

          

          thus ( Sum F) = (( Sum G) + x) by A5, RVSUM_1: 74

          .= (((n + m) choose (n + 1)) + ((n + m) choose n)) by A2, A6, A10, A12, A16

          .= (((n + m) + 1) choose (n + 1)) by Th22

          .= ((n + (m + 1)) choose (n + 1));

        end;

      end;

      

       A17: P[ 0 ];

      thus for m holds P[m] from NAT_1:sch 2( A17, A1);

    end;

    registration

      let k,n be natural Number;

      cluster (n choose k) -> natural;

      coherence by Th25;

    end

    definition

      let k,n be Nat;

      :: original: choose

      redefine

      func n choose k -> Element of NAT ;

      coherence by ORDINAL1:def 12;

    end

    definition

      let a,b be Real;

      let n be natural Number;

      :: NEWTON:def4

      func (a,b) In_Power n -> FinSequence of REAL means

      : Def4: ( len it ) = (n + 1) & for i,l,m be Nat st i in ( dom it ) & m = (i - 1) & l = (n - m) holds (it . i) = (((n choose m) * (a |^ l)) * (b |^ m));

      existence

      proof

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

        defpred P[ Nat, object] means for l,m be Nat st m = ($1 - 1) & l = (n - m) holds $2 = (((n choose m) * (a |^ l)) * (b |^ m));

        

         A1: for k be Nat st k in ( Seg (n + 1)) holds ex x be object st P[k, x]

        proof

          let k be Nat;

          assume

           A2: k in ( Seg (n + 1));

          then k >= 1 by FINSEQ_1: 1;

          then

          reconsider m1 = (k - 1) as Element of NAT by INT_1: 5;

          k <= (n + 1) by A2, FINSEQ_1: 1;

          then (k - 1) <= ((n + 1) - 1) by XREAL_1: 9;

          then

          reconsider l1 = (n - m1) as Element of NAT by INT_1: 5;

          take (((n choose m1) * (a |^ l1)) * (b |^ m1));

          thus thesis;

        end;

        consider p be FinSequence such that

         A3: ( dom p) = ( Seg (n + 1)) and

         A4: for k be Nat st k in ( Seg (n + 1)) holds P[k, (p . k)] from FINSEQ_1:sch 1( A1);

        ( rng p) c= REAL

        proof

          let x be object;

          assume x in ( rng p);

          then

          consider y be object such that

           A5: y in ( dom p) and

           A6: x = (p . y) by FUNCT_1:def 3;

          reconsider y as Element of NAT by A5;

          y >= 1 by A3, A5, FINSEQ_1: 1;

          then

          reconsider m1 = (y - 1) as Element of NAT by INT_1: 5;

          y <= (n + 1) by A3, A5, FINSEQ_1: 1;

          then (y - 1) <= ((n + 1) - 1) by XREAL_1: 9;

          then

          reconsider l1 = (n - m1) as Element of NAT by INT_1: 5;

          (p . y) = (((n choose m1) * (a |^ l1)) * (b |^ m1)) by A3, A4, A5;

          then

          reconsider x as Real by A6;

          x in REAL by XREAL_0:def 1;

          hence thesis;

        end;

        then

        reconsider p as FinSequence of REAL by FINSEQ_1:def 4;

        take p;

        thus thesis by A3, A4, FINSEQ_1:def 3;

      end;

      uniqueness

      proof

        let G, H;

        assume that

         A7: ( len G) = (n + 1) and

         A8: for i,l,m be Nat st i in ( dom G) & m = (i - 1) & l = (n - m) holds (G . i) = (((n choose m) * (a |^ l)) * (b |^ m));

        assume that

         A9: ( len H) = (n + 1) and

         A10: for i,l,m be Nat st i in ( dom H) & m = (i - 1) & l = (n - m) holds (H . i) = (((n choose m) * (a |^ l)) * (b |^ m));

        for i st i in ( dom G) holds (G . i) = (H . i)

        proof

          let i;

          assume

           A11: i in ( dom G);

          then

           A12: i in ( Seg (n + 1)) by A7, FINSEQ_1:def 3;

          then i >= 1 by FINSEQ_1: 1;

          then

          reconsider m = (i - 1) as Element of NAT by INT_1: 5;

          i <= (n + 1) by A12, FINSEQ_1: 1;

          then (i - 1) <= ((n + 1) - 1) by XREAL_1: 9;

          then

          reconsider l = (n - m) as Element of NAT by INT_1: 5;

          i in ( dom H) by A9, A12, FINSEQ_1:def 3;

          then (H . i) = (((n choose m) * (a |^ l)) * (b |^ m)) by A10;

          hence thesis by A8, A11;

        end;

        hence thesis by A7, A9, FINSEQ_2: 9;

      end;

    end

    theorem :: NEWTON:27

    

     Th27: ((a,b) In_Power 0 ) = <*1*>

    proof

      set F = ((a,b) In_Power 0 );

      

       A1: ( len F) = ( 0 + 1) by Def4

      .= 1;

      then

       A2: ( dom F) = {1} by FINSEQ_1: 2, FINSEQ_1:def 3;

      then 1 in ( dom F) by TARSKI:def 1;

      then

      consider i be set such that

       A3: i in ( dom F);

      reconsider i as Element of NAT by A3;

      

       A4: i = 1 by A2, A3, TARSKI:def 1;

      then

      reconsider m1 = (i - 1) as Element of NAT by INT_1: 5;

      reconsider l1 = ( 0 - m1) as Element of NAT by A4;

      1 in ( dom ((a,b) In_Power 0 )) by A2, TARSKI:def 1;

      

      then (F . 1) = ((( 0 choose 0 ) * (a |^ l1)) * (b |^ m1)) by A4, Def4

      .= ((1 * (a |^ 0 )) * (b |^ 0 )) by A4, Th21

      .= 1 by RVSUM_1: 94;

      hence thesis by A1, FINSEQ_1: 40;

    end;

    theorem :: NEWTON:28

    

     Th28: (((a,b) In_Power s) . 1) = (a |^ s)

    proof

      reconsider m1 = (1 - 1) as Element of NAT by INT_1: 5;

      reconsider l1 = (s - m1) as Nat;

      ( len ((a,b) In_Power s)) = (s + 1) by Def4;

      then

       A1: ( dom ((a,b) In_Power s)) = ( Seg (s + 1)) by FINSEQ_1:def 3;

      (s + 1) >= ( 0 + 1) by XREAL_1: 6;

      then 1 in ( dom ((a,b) In_Power s)) by A1;

      

      then (((a,b) In_Power s) . 1) = (((s choose 0 ) * (a |^ l1)) * (b |^ m1)) by Def4

      .= ((1 * (a |^ l1)) * (b |^ m1)) by Th19

      .= (a |^ s) by RVSUM_1: 94;

      hence thesis;

    end;

    theorem :: NEWTON:29

    

     Th29: (((a,b) In_Power s) . (s + 1)) = (b |^ s)

    proof

      reconsider m1 = ((s + 1) - 1) as Element of NAT by INT_1: 5, NAT_1: 12;

      reconsider l1 = (s - m1) as Element of NAT by INT_1: 5;

      ( len ((a,b) In_Power s)) = (s + 1) by Def4;

      then ( dom ((a,b) In_Power s)) = ( Seg (s + 1)) by FINSEQ_1:def 3;

      then (s + 1) in ( dom ((a,b) In_Power s)) by FINSEQ_1: 4;

      

      then (((a,b) In_Power s) . (s + 1)) = (((s choose s) * (a |^ l1)) * (b |^ m1)) by Def4

      .= ((1 * (a |^ l1)) * (b |^ m1)) by Th21

      .= (1 * (b |^ m1)) by RVSUM_1: 94

      .= (b |^ s);

      hence thesis;

    end;

    theorem :: NEWTON:30

    

     Th30: ((a + b) |^ s) = ( Sum ((a,b) In_Power s))

    proof

      

       A0: s is Nat by TARSKI: 1;

      defpred P[ Nat] means ((a + b) |^ $1) = ( Sum ((a,b) In_Power $1));

      

       A1: for n st P[n] holds P[(n + 1)]

      proof

        reconsider a, b as Element of REAL by XREAL_0:def 1;

        let n;

        reconsider G1 = ((a * ((a,b) In_Power n)) ^ <*( In ( 0 , REAL ))*>) as FinSequence of REAL ;

        set G2 = ( <*( In ( 0 , REAL ))*> ^ (b * ((a,b) In_Power n)));

        assume P[n];

        

        then

         A2: ((a + b) |^ (n + 1)) = ((a + b) * ( Sum ((a,b) In_Power n))) by Th6

        .= ((a * ( Sum ((a,b) In_Power n))) + (b * ( Sum ((a,b) In_Power n))))

        .= (( Sum (a * ((a,b) In_Power n))) + (b * ( Sum ((a,b) In_Power n)))) by RVSUM_1: 87

        .= (( Sum (a * ((a,b) In_Power n))) + ( Sum (b * ((a,b) In_Power n)))) by RVSUM_1: 87;

        ( len G2) = (( len <* 0 *>) + ( len (b * ((a,b) In_Power n)))) by FINSEQ_1: 22

        .= (1 + ( len (b * ((a,b) In_Power n)))) by FINSEQ_1: 40

        .= (1 + ( len ((a,b) In_Power n))) by Th2

        .= ((n + 1) + 1) by Def4;

        then

        reconsider F2 = G2 as Element of (((n + 1) + 1) -tuples_on REAL ) by FINSEQ_2: 92;

        ( len G1) = (( len (a * ((a,b) In_Power n))) + ( len <* 0 *>)) by FINSEQ_1: 22

        .= (( len (a * ((a,b) In_Power n))) + 1) by FINSEQ_1: 40

        .= (( len ((a,b) In_Power n)) + 1) by Th2

        .= ((n + 1) + 1) by Def4;

        then

        reconsider F1 = G1 as Element of (((n + 1) + 1) -tuples_on REAL ) by FINSEQ_2: 92;

        

         A3: ( Sum F2) = ( 0 + ( Sum (b * ((a,b) In_Power n)))) by RVSUM_1: 76

        .= ( Sum (b * ((a,b) In_Power n)));

        ( Sum F1) = (( Sum (a * ((a,b) In_Power n))) + 0 ) by RVSUM_1: 74

        .= ( Sum (a * ((a,b) In_Power n)));

        then

         A4: ( Sum (G1 + G2)) = (( Sum (a * ((a,b) In_Power n))) + ( Sum (b * ((a,b) In_Power n)))) by A3, RVSUM_1: 89;

        set F = (F1 + F2);

        

         A5: ( len F2) = ((n + 1) + 1) by CARD_1:def 7;

        

         A6: ( len F) = ((n + 1) + 1) by CARD_1:def 7;

        

         A7: ( len F1) = ((n + 1) + 1) by CARD_1:def 7;

        

         A8: for i st i in ( dom ((a,b) In_Power (n + 1))) holds (F . i) = (((a,b) In_Power (n + 1)) . i)

        proof

          let i;

          assume

           A9: i in ( dom ((a,b) In_Power (n + 1)));

          set r2 = (F2 /. i);

          set r1 = (F1 /. i);

          set r = (((a,b) In_Power n) /. i);

          

           A10: ( len ((a,b) In_Power (n + 1))) = ((n + 1) + 1) by Def4;

          then

           A11: i in ( Seg ((n + 1) + 1)) by A9, FINSEQ_1:def 3;

          then

           A12: i in ( dom F1) by A7, FINSEQ_1:def 3;

          

           A13: i in ( dom F2) by A5, A11, FINSEQ_1:def 3;

          

           A14: i in {1} implies (F . i) = (((a,b) In_Power (n + 1)) . i)

          proof

            (n + 1) >= ( 0 + 1) by XREAL_1: 6;

            then 1 in ( Seg (n + 1));

            then 1 in ( Seg ( len ((a,b) In_Power n))) by Def4;

            then

             A15: 1 in ( dom ((a,b) In_Power n)) by FINSEQ_1:def 3;

            then

             A16: 1 in ( dom (a * ((a,b) In_Power n))) by VALUED_1:def 5;

            assume i in {1};

            then

             A17: i = 1 by TARSKI:def 1;

            then

             A18: r = (((a,b) In_Power n) . 1) by A15, PARTFUN1:def 6;

            r = (((a,b) In_Power n) . i) by A17, A15, PARTFUN1:def 6;

            then

             A19: r = (a |^ n) by A17, Th28;

            

             A20: r1 = (((a * ((a,b) In_Power n)) ^ <* 0 *>) . 1) by A12, A17, PARTFUN1:def 6

            .= ((a * ((a,b) In_Power n)) . 1) by A16, FINSEQ_1:def 7

            .= (a * (a |^ n)) by A18, A19, RVSUM_1: 44

            .= (a |^ (n + 1)) by Th6;

            

             A21: r2 = (F2 . i) by A13, PARTFUN1:def 6;

            

             A22: r1 = (F1 . i) by A12, PARTFUN1:def 6;

            r2 = (( <* 0 *> ^ (b * ((a,b) In_Power n))) . 1) by A13, A17, PARTFUN1:def 6

            .= 0 by FINSEQ_1: 41;

            

            then (F . i) = (r1 + 0 ) by A22, A21, RVSUM_1: 11

            .= (((a,b) In_Power (n + 1)) . i) by A17, A20, Th28;

            hence thesis;

          end;

          i >= 1 by A11, FINSEQ_1: 1;

          then

          reconsider j = (i - 1) as Element of NAT by INT_1: 5;

          set x = (((a,b) In_Power n) /. j);

          

           A23: i = (j + 1);

          

           A24: i in ( dom F) by A6, A11, FINSEQ_1:def 3;

          

           A25: i in { k where k be Element of NAT : k > 1 & k < ((n + 1) + 1) } implies (F . i) = (((a,b) In_Power (n + 1)) . i)

          proof

            assume i in { k where k be Element of NAT : 1 < k & k < ((n + 1) + 1) };

            then

             A26: ex k be Element of NAT st k = i & 1 < k & k < ((n + 1) + 1);

            then

            reconsider m1 = (i - 1) as Element of NAT by INT_1: 5;

            

             A27: r1 = (((a * ((a,b) In_Power n)) ^ <* 0 *>) . i) by A12, PARTFUN1:def 6;

            1 <= j by A23, A26, NAT_1: 13;

            then

            reconsider m2 = (j - 1) as Element of NAT by INT_1: 5;

            

             A28: j <= (n + 1) by A23, A26, XREAL_1: 6;

            then (j - 1) <= ((n + 1) - 1) by XREAL_1: 9;

            then

            reconsider l2 = (n - m2) as Element of NAT by INT_1: 5;

            1 <= j by A23, A26, NAT_1: 13;

            then j in ( Seg (n + 1)) by A28;

            then j in ( Seg ( len ((a,b) In_Power n))) by Def4;

            then

             A29: j in ( dom ((a,b) In_Power n)) by FINSEQ_1:def 3;

            then

             A30: x = (((a,b) In_Power n) . j) by PARTFUN1:def 6;

            

             A31: i <= (n + 1) by A26, NAT_1: 13;

            then i in ( Seg (n + 1)) by A26;

            then i in ( Seg ( len ((a,b) In_Power n))) by Def4;

            then

             A32: i in ( dom ((a,b) In_Power n)) by FINSEQ_1:def 3;

            then

             A33: r = (((a,b) In_Power n) . i) by PARTFUN1:def 6;

            i in ( dom (a * ((a,b) In_Power n))) by A32, VALUED_1:def 5;

            

            then

             A34: r1 = ((a * ((a,b) In_Power n)) . i) by A27, FINSEQ_1:def 7

            .= (a * r) by A33, RVSUM_1: 44;

            (i - 1) <= ((n + 1) - 1) by A31, XREAL_1: 9;

            then

            reconsider l1 = (n - m1) as Element of NAT by INT_1: 5;

            

             A35: (l1 + 1) = ((n + 1) - (m2 + 1));

            

             A36: j in ( dom (b * ((a,b) In_Power n))) by A29, VALUED_1:def 5;

            

             A37: r2 = (( <* 0 *> ^ (b * ((a,b) In_Power n))) . i) by A13, PARTFUN1:def 6;

            

            then r2 = (( <* 0 *> ^ (b * ((a,b) In_Power n))) . (( len <* 0 *>) + j)) by A23, FINSEQ_1: 40

            .= ((b * ((a,b) In_Power n)) . j) by A36, FINSEQ_1:def 7

            .= (b * x) by A30, RVSUM_1: 44;

            

            then (F . i) = ((a * r) + (b * x)) by A24, A27, A37, A34, VALUED_1:def 1

            .= ((a * (((a |^ l1) * (n choose m1)) * (b |^ m1))) + (b * x)) by A32, A33, Def4

            .= (((a * (a |^ l1)) * ((n choose m1) * (b |^ m1))) + (b * x))

            .= (((a |^ (l1 + 1)) * ((n choose m1) * (b |^ m1))) + (b * x)) by Th6

            .= (((a |^ (l1 + 1)) * ((n choose m1) * (b |^ m1))) + (b * ((b |^ m2) * ((n choose m2) * (a |^ l2))))) by A29, A30, Def4

            .= (((a |^ (l1 + 1)) * ((n choose m1) * (b |^ m1))) + ((b * (b |^ m2)) * ((n choose m2) * (a |^ l2))))

            .= (((a |^ (l1 + 1)) * ((n choose (m2 + 1)) * (b |^ (m2 + 1)))) + ((b |^ (m2 + 1)) * ((n choose m2) * (a |^ l2)))) by Th6

            .= ((((n choose (m2 + 1)) + (n choose m2)) * (a |^ (l1 + 1))) * (b |^ (m2 + 1)))

            .= ((((n + 1) choose (m2 + 1)) * (a |^ (l1 + 1))) * (b |^ (m2 + 1))) by Th22

            .= (((a,b) In_Power (n + 1)) . i) by A9, A35, Def4;

            hence thesis;

          end;

          

           A38: i in {((n + 1) + 1)} implies (F . i) = (((a,b) In_Power (n + 1)) . i)

          proof

            assume

             A39: i in {((n + 1) + 1)};

            then

             A40: i = ((n + 1) + 1) by TARSKI:def 1;

            

             A41: j = (((n + 1) + 1) - 1) by A39, TARSKI:def 1

            .= (n + 1);

            (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

            then j in ( Seg ( len ((a,b) In_Power n))) by A41, Def4;

            then

             A42: j in ( dom ((a,b) In_Power n)) by FINSEQ_1:def 3;

            

            then

             A43: x = (((a,b) In_Power n) . (n + 1)) by A41, PARTFUN1:def 6

            .= (b |^ n) by Th29;

            

             A44: x = (((a,b) In_Power n) . j) by A42, PARTFUN1:def 6;

            

             A45: j in ( dom (b * ((a,b) In_Power n))) by A42, VALUED_1:def 5;

            

             A46: r2 = (( <* 0 *> ^ (b * ((a,b) In_Power n))) . ((1 + n) + 1)) by A13, A40, PARTFUN1:def 6

            .= (( <* 0 *> ^ (b * ((a,b) In_Power n))) . (( len <* 0 *>) + j)) by A41, FINSEQ_1: 39

            .= ((b * ((a,b) In_Power n)) . j) by A45, FINSEQ_1:def 7

            .= (b * (b |^ n)) by A44, A43, RVSUM_1: 44

            .= (b |^ (n + 1)) by Th6;

            

             A47: r2 = (F2 . i) by A13, PARTFUN1:def 6;

            (n + 1) = ( len ((a,b) In_Power n)) by Def4

            .= ( len (a * ((a,b) In_Power n))) by Th2;

            

            then

             A48: r1 = (((a * ((a,b) In_Power n)) ^ <* 0 *>) . (( len (a * ((a,b) In_Power n))) + 1)) by A12, A40, PARTFUN1:def 6

            .= 0 by FINSEQ_1: 42;

            r1 = (F1 . i) by A12, PARTFUN1:def 6;

            

            then (F . i) = ( 0 + r2) by A48, A47, RVSUM_1: 11

            .= (((a,b) In_Power (n + 1)) . i) by A40, A46, Th29;

            hence thesis;

          end;

           A49:

          now

            assume i in (( {1} \/ { k where k be Element of NAT : 1 < k & k < ((n + 1) + 1) }) \/ {((n + 1) + 1)});

            then i in ( {1} \/ { k where k be Element of NAT : 1 < k & k < ((n + 1) + 1) }) or i in {((n + 1) + 1)} by XBOOLE_0:def 3;

            hence thesis by A14, A25, A38, XBOOLE_0:def 3;

          end;

          ( dom ((a,b) In_Power (n + 1))) = ( Seg ((n + 1) + 1)) by A10, FINSEQ_1:def 3;

          hence thesis by A9, A49, Th1, NAT_1: 12;

        end;

        ( len ((a,b) In_Power (n + 1))) = ( len F) by A6, Def4;

        hence thesis by A2, A4, A8, FINSEQ_2: 9;

      end;

      ((a + b) |^ 0 ) = ( Sum <*( In (1, REAL ))*>) by FINSOP_1: 11, RVSUM_1: 94

      .= ( Sum ((a,b) In_Power 0 )) by Th27;

      then

       A50: P[ 0 ];

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

      hence thesis by A0;

    end;

    definition

      let n be natural Number;

      :: NEWTON:def5

      func Newton_Coeff n -> FinSequence of REAL means

      : Def5: ( len it ) = (n + 1) & for i,k be Nat st i in ( dom it ) & k = (i - 1) holds (it . i) = (n choose k);

      existence

      proof

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

        defpred P[ Nat, object] means for s st s = ($1 - 1) holds $2 = (n choose s);

        

         A1: for l be Nat st l in ( Seg (n + 1)) holds ex x be object st P[l, x]

        proof

          let l be Nat;

          assume l in ( Seg (n + 1));

          then l >= 1 by FINSEQ_1: 1;

          then

          reconsider k = (l - 1) as Element of NAT by INT_1: 5;

          set x = (n choose k);

          take x;

          thus thesis;

        end;

        consider F be FinSequence such that

         A2: ( dom F) = ( Seg (n + 1)) & for l be Nat st l in ( Seg (n + 1)) holds P[l, (F . l)] from FINSEQ_1:sch 1( A1);

        ( rng F) c= REAL

        proof

          let x be object;

          assume x in ( rng F);

          then

          consider y be object such that

           A3: y in ( dom F) and

           A4: x = (F . y) by FUNCT_1:def 3;

          reconsider y as Element of NAT by A3;

          y >= 1 by A2, A3, FINSEQ_1: 1;

          then

          reconsider m1 = (y - 1) as Element of NAT by INT_1: 5;

          (F . y) = (n choose m1) by A2, A3;

          then

          reconsider x as Real by A4;

          x in REAL by XREAL_0:def 1;

          hence thesis;

        end;

        then

        reconsider F as FinSequence of REAL by FINSEQ_1:def 4;

        take F;

        thus thesis by A2, FINSEQ_1:def 3;

      end;

      uniqueness

      proof

        let G, H;

        assume that

         A5: ( len G) = (n + 1) and

         A6: for i,m be Nat st i in ( dom G) & m = (i - 1) holds (G . i) = (n choose m);

        assume that

         A7: ( len H) = (n + 1) and

         A8: for i,m be Nat st i in ( dom H) & m = (i - 1) holds (H . i) = (n choose m);

        for i st i in ( dom G) holds (G . i) = (H . i)

        proof

          let i;

          assume

           A9: i in ( dom G);

          then

           A10: i in ( Seg (n + 1)) by A5, FINSEQ_1:def 3;

          then i >= 1 by FINSEQ_1: 1;

          then

          reconsider m = (i - 1) as Element of NAT by INT_1: 5;

          i in ( dom H) by A7, A10, FINSEQ_1:def 3;

          then (H . i) = (n choose m) by A8;

          hence thesis by A6, A9;

        end;

        hence thesis by A5, A7, FINSEQ_2: 9;

      end;

    end

    theorem :: NEWTON:31

    

     Th31: ( Newton_Coeff s) = ((1,1) In_Power s)

    proof

      

       A1: for i st i in ( dom ( Newton_Coeff s)) holds (( Newton_Coeff s) . i) = (((1,1) In_Power s) . i)

      proof

        let i;

        assume

         A2: i in ( dom ( Newton_Coeff s));

        

         A3: ( dom ( Newton_Coeff s)) = ( Seg ( len ( Newton_Coeff s))) by FINSEQ_1:def 3

        .= ( Seg (s + 1)) by Def5;

        then i >= 1 by A2, FINSEQ_1: 1;

        then

        reconsider m1 = (i - 1) as Element of NAT by INT_1: 5;

        i <= (s + 1) by A2, A3, FINSEQ_1: 1;

        then ((s + 1) - 1) >= (i - 1) by XREAL_1: 9;

        then

        reconsider l1 = (s - m1) as Element of NAT by INT_1: 5;

        ( dom ( Newton_Coeff s)) = ( Seg ( len ((1,1) In_Power s))) by A3, Def4

        .= ( dom ((1,1) In_Power s)) by FINSEQ_1:def 3;

        

        then (((1,1) In_Power s) . i) = (((s choose m1) * (1 |^ l1)) * (1 |^ m1)) by A2, Def4

        .= (( Newton_Coeff s) . i) by A2, Def5;

        hence thesis;

      end;

      ( len ( Newton_Coeff s)) = (s + 1) by Def5

      .= ( len ((1,1) In_Power s)) by Def4;

      hence thesis by A1, FINSEQ_2: 9;

    end;

    theorem :: NEWTON:32

    (2 |^ s) = ( Sum ( Newton_Coeff s))

    proof

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

      .= ( Sum ((1,1) In_Power s)) by Th30

      .= ( Sum ( Newton_Coeff s)) by Th31;

      hence thesis;

    end;

    begin

    theorem :: NEWTON:33

    

     Th33: l >= 1 implies (k * l) >= k

    proof

      assume

       A1: l >= 1;

      for k holds (k * l) >= k

      proof

        defpred P[ Nat] means ($1 * l) >= $1;

        

         A2: for k st P[k] holds P[(k + 1)]

        proof

          let k;

          

           A3: ((k + 1) * l) = ((k * l) + (1 * l));

          

           A4: (k + l) >= (k + 1) by A1, XREAL_1: 7;

          assume (k * l) >= k;

          then ((k + 1) * l) >= (k + l) by A3, XREAL_1: 7;

          hence ((k + 1) * l) >= (k + 1) by A4, XXREAL_0: 2;

        end;

        

         A5: P[ 0 ];

        thus for k holds P[k] from NAT_1:sch 2( A5, A2);

      end;

      hence thesis;

    end;

    theorem :: NEWTON:34

    

     Th34: l >= 1 & n >= (k * l) implies n >= k

    proof

      assume that

       A1: l >= 1 and

       A2: n >= (k * l);

      (k * l) >= k by A1, Th33;

      hence thesis by A2, XXREAL_0: 2;

    end;

    definition

      let n;

      :: original: !

      redefine

      func n ! -> Element of NAT ;

      coherence by Th16;

    end

    theorem :: NEWTON:35

    

     Th35: l <> 0 implies l divides (l ! )

    proof

      assume l <> 0 ;

      then

      consider n be Nat such that

       A1: l = (n + 1) by NAT_1: 6;

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

      ((n + 1) ! ) = ((n + 1) * (n ! )) by Th15;

      hence thesis by A1, NAT_D:def 3;

    end;

    theorem :: NEWTON:36

    n <> 0 implies ((n + 1) / n) > 1

    proof

      assume

       A1: n <> 0 ;

      ((n + 1) / n) = ((n / n) + (1 / n)) by XCMPLX_1: 62

      .= (1 + (1 / n)) by A1, XCMPLX_1: 60;

      hence thesis by A1, XREAL_1: 29;

    end;

    theorem :: NEWTON:37

    

     Th37: (k / (k + 1)) < 1

    proof

      m < (m + 1) by XREAL_1: 29;

      hence thesis by XREAL_1: 189;

    end;

    theorem :: NEWTON:38

    

     Th38: (l ! ) >= l

    proof

      defpred P[ Nat] means ($1 ! ) >= $1;

      

       A1: for l st P[l] holds P[(l + 1)]

      proof

        let l;

        assume

         A2: (l ! ) >= l;

        

         A3: ((l ! ) * (l + 1)) = ((l + 1) ! ) by Th15;

        l = 0 & ((l + 1) ! ) >= (l + 1) or l >= 1 & ((l + 1) ! ) >= (l + 1)

        proof

          per cases by NAT_1: 14;

            case l = 0 ;

            hence thesis by FINSEQ_2: 50;

          end;

            case

             A4: l >= 1;

            ((l + 1) ! ) >= ((l + 1) * l) by A2, A3, XREAL_1: 64;

            hence thesis by A4, Th34;

          end;

        end;

        hence thesis;

      end;

      

       A5: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: NEWTON:39

    

     Th39: m <> 1 & m divides n implies not m divides (n + 1)

    proof

      assume that

       A1: m <> 1 and

       A2: m divides n and

       A3: m divides (n + 1);

      consider t be Nat such that

       A4: n = (m * t) by A2, NAT_D:def 3;

      consider s be Nat such that

       A5: (n + 1) = (m * s) by A3, NAT_D:def 3;

      t <= s

      proof

        ((n + 1) * t) = ((m * s) * t) by A5

        .= (n * s) by A4;

        

        then

         A6: t = ((n * s) / (n + 1)) by XCMPLX_1: 89

        .= (s * (n / (n + 1))) by XCMPLX_1: 74;

        assume

         A7: t > s;

        s > 0 by A5;

        hence contradiction by A7, A6, Th37, XREAL_1: 157;

      end;

      then

      reconsider r = (s - t) as Element of NAT by INT_1: 5;

      1 = ((m * s) - (m * t)) by A4, A5;

      then 1 = (m * r);

      hence contradiction by A1, NAT_1: 15;

    end;

    theorem :: NEWTON:40

    

     Th40: j <> 0 implies j divides ((j + k) ! )

    proof

      defpred P[ Nat] means for j st j <> 0 holds j divides ((j + $1) ! );

      

       A1: for k st P[k] holds P[(k + 1)]

      proof

        let k;

        assume

         A2: for j st j <> 0 holds j divides ((j + k) ! );

        let j;

        assume j <> 0 ;

        then j divides (((j + k) ! ) * ((j + k) + 1)) by A2, NAT_D: 9;

        hence thesis by Th15;

      end;

      

       A3: P[ 0 ] by Th35;

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

      hence thesis;

    end;

    theorem :: NEWTON:41

    

     Th41: j <= l & j <> 0 implies j divides (l ! )

    proof

      assume that

       A1: j <= l and

       A2: j <> 0 ;

      ex k be Nat st l = (j + k) by A1, NAT_1: 10;

      hence thesis by A2, Th40;

    end;

    theorem :: NEWTON:42

    j <> 1 & j <> 0 & j divides ((l ! ) + 1) implies j > l by Th39, Th41;

    theorem :: NEWTON:43

    (m lcm (n lcm k)) = ((m lcm n) lcm k)

    proof

      set M = (n lcm k);

      set K = (m lcm M);

      set N = (m lcm n);

      set L = (N lcm k);

      

       A1: m divides K by NAT_D:def 4;

      

       A2: M divides K by NAT_D:def 4;

      n divides M by NAT_D:def 4;

      then n divides K by A2, NAT_D: 4;

      then

       A3: N divides K by A1, NAT_D:def 4;

      k divides M by NAT_D:def 4;

      then k divides K by A2, NAT_D: 4;

      then

       A4: L divides K by A3, NAT_D:def 4;

      

       A5: N divides L by NAT_D:def 4;

      

       A6: k divides L by NAT_D:def 4;

      n divides N by NAT_D:def 4;

      then n divides L by A5, NAT_D: 4;

      then

       A7: M divides L by A6, NAT_D:def 4;

      m divides N by NAT_D:def 4;

      then m divides L by A5, NAT_D: 4;

      then K divides L by A7, NAT_D:def 4;

      hence thesis by A4, NAT_D: 5;

    end;

    theorem :: NEWTON:44

    

     Th44: m divides n iff (m lcm n) = n

    proof

      thus m divides n implies (m lcm n) = n

      proof

        set M = (m lcm n);

        assume m divides n;

        then

         A1: M divides n by NAT_D:def 4;

        n divides M by NAT_D:def 4;

        hence thesis by A1, NAT_D: 5;

      end;

      thus thesis by NAT_D:def 4;

    end;

    theorem :: NEWTON:45

    n divides m & k divides m iff (n lcm k) divides m

    proof

      (n lcm k) divides m implies n divides m & k divides m

      proof

        set M = (n lcm k);

        

         A1: n divides M by NAT_D:def 4;

        

         A2: k divides M by NAT_D:def 4;

        assume (n lcm k) divides m;

        hence thesis by A1, A2, NAT_D: 4;

      end;

      hence thesis by NAT_D:def 4;

    end;

    theorem :: NEWTON:46

    (m lcm 1) = m

    proof

      set M = (m lcm 1);

      1 divides m by NAT_D: 6;

      then

       A1: M divides m by NAT_D:def 4;

      m divides M by NAT_D:def 4;

      hence thesis by A1, NAT_D: 5;

    end;

    theorem :: NEWTON:47

    

     Th47: (m lcm n) divides (m * n)

    proof

      set s = (m * n);

      

       A1: n divides s by NAT_D: 9;

      m divides s by NAT_D: 9;

      hence thesis by A1, NAT_D:def 4;

    end;

    theorem :: NEWTON:48

    (m gcd (n gcd k)) = ((m gcd n) gcd k)

    proof

      set M = (n gcd k);

      set K = (m gcd M);

      set N = (m gcd n);

      set L = (N gcd k);

      

       A1: K divides M by NAT_D:def 5;

      

       A2: K divides m by NAT_D:def 5;

      M divides n by NAT_D:def 5;

      then K divides n by A1, NAT_D: 4;

      then

       A3: K divides N by A2, NAT_D:def 5;

      

       A4: L divides N by NAT_D:def 5;

      

       A5: L divides k by NAT_D:def 5;

      N divides n by NAT_D:def 5;

      then L divides n by A4, NAT_D: 4;

      then

       A6: L divides M by A5, NAT_D:def 5;

      N divides m by NAT_D:def 5;

      then L divides m by A4, NAT_D: 4;

      then

       A7: L divides K by A6, NAT_D:def 5;

      M divides k by NAT_D:def 5;

      then K divides k by A1, NAT_D: 4;

      then K divides L by A3, NAT_D:def 5;

      hence thesis by A7, NAT_D: 5;

    end;

    theorem :: NEWTON:49

    

     Th49: n divides m implies (n gcd m) = n

    proof

      set N = (n gcd m);

      assume n divides m;

      then

       A1: n divides N by NAT_D:def 5;

      N divides n by NAT_D:def 5;

      hence thesis by A1, NAT_D: 5;

    end;

    theorem :: NEWTON:50

    m divides n & m divides k iff m divides (n gcd k)

    proof

      m divides (n gcd k) implies m divides n & m divides k

      proof

        set M = (n gcd k);

        

         A1: M divides n by NAT_D:def 5;

        

         A2: M divides k by NAT_D:def 5;

        assume m divides (n gcd k);

        hence thesis by A1, A2, NAT_D: 4;

      end;

      hence thesis by NAT_D:def 5;

    end;

    theorem :: NEWTON:51

    (m gcd 1) = 1

    proof

      set M = (m gcd 1);

      

       A1: 1 divides M by NAT_D: 6;

      M divides 1 by NAT_D:def 5;

      hence thesis by A1, NAT_D: 5;

    end;

    theorem :: NEWTON:52

    (m gcd 0 ) = m

    proof

      set M = (m gcd 0 );

      m divides 0 by NAT_D: 6;

      then

       A1: m divides M by NAT_D:def 5;

      M divides m by NAT_D:def 5;

      hence thesis by A1, NAT_D: 5;

    end;

    theorem :: NEWTON:53

    

     Th53: ((m gcd n) lcm n) = n

    proof

      set M = (m gcd n);

      M divides n by NAT_D:def 5;

      hence thesis by Th44;

    end;

    theorem :: NEWTON:54

    

     Th54: (m gcd (m lcm n)) = m

    proof

      set M = (m lcm n);

      m divides M by NAT_D:def 4;

      hence thesis by Th49;

    end;

    theorem :: NEWTON:55

    (m gcd (m lcm n)) = ((n gcd m) lcm m)

    proof

      (m gcd (m lcm n)) = m by Th54;

      hence thesis by Th53;

    end;

    theorem :: NEWTON:56

    m divides n implies (m gcd k) divides (n gcd k)

    proof

      set M = (m gcd k);

      

       A1: M divides k by NAT_D:def 5;

      assume

       A2: m divides n;

      M divides m by NAT_D:def 5;

      then M divides n by A2, NAT_D: 4;

      hence thesis by A1, NAT_D:def 5;

    end;

    theorem :: NEWTON:57

    m divides n implies (k gcd m) divides (k gcd n)

    proof

      set M = (k gcd m);

      

       A1: M divides k by NAT_D:def 5;

      assume

       A2: m divides n;

      M divides m by NAT_D:def 5;

      then M divides n by A2, NAT_D: 4;

      hence thesis by A1, NAT_D:def 5;

    end;

    theorem :: NEWTON:58

    

     Th58: for m,n be Integer holds n > 0 implies (n gcd m) > 0

    proof

      let m,n be Integer;

      assume that

       A1: n > 0 and

       A2: (n gcd m) <= 0 ;

      

       A3: (n gcd m) divides n by INT_2:def 2;

      (n gcd m) = 0 or (n gcd m) < 0 by A2;

      then ex r be Integer st n = ( 0 * r) by A3, INT_1:def 3;

      hence contradiction by A1;

    end;

    theorem :: NEWTON:59

    m > 0 & n > 0 implies (m lcm n) > 0

    proof

      assume that

       A1: m > 0 and

       A2: n > 0 and

       A3: (m lcm n) <= 0 ;

      

       A4: (m lcm n) divides (m * n) by Th47;

      (m lcm n) = 0 or (m lcm n) < 0 by A3;

      then ex r be Nat st (m * n) = ( 0 * r) by A4, NAT_D:def 3;

      hence contradiction by A1, A2;

    end;

    theorem :: NEWTON:60

    ((n gcd m) lcm (n gcd k)) divides (n gcd (m lcm k))

    proof

      set M = (m lcm k);

      set N = (n gcd k);

      set P = (n gcd m);

      set L = (P lcm N);

      

       A1: N divides k by NAT_D:def 5;

      k divides M by NAT_D:def 4;

      then

       A2: N divides M by A1, NAT_D: 4;

      

       A3: P divides m by NAT_D:def 5;

      m divides M by NAT_D:def 4;

      then P divides M by A3, NAT_D: 4;

      then

       A4: L divides M by A2, NAT_D:def 4;

      

       A5: P divides n by NAT_D:def 5;

      N divides n by NAT_D:def 5;

      then L divides n by A5, NAT_D:def 4;

      hence thesis by A4, NAT_D:def 5;

    end;

    theorem :: NEWTON:61

    m divides l implies (m lcm (n gcd l)) divides ((m lcm n) gcd l)

    proof

      set M = (m lcm n);

      set K = (M gcd l);

      set N = (n gcd l);

      

       A1: m divides M by NAT_D:def 4;

      

       A2: N divides n by NAT_D:def 5;

      

       A3: N divides l by NAT_D:def 5;

      n divides M by NAT_D:def 4;

      then N divides M by A2, NAT_D: 4;

      then

       A4: N divides K by A3, NAT_D:def 5;

      assume m divides l;

      then m divides K by A1, NAT_D:def 5;

      hence thesis by A4, NAT_D:def 4;

    end;

    theorem :: NEWTON:62

    (n gcd m) divides (n lcm m)

    proof

      

       A1: n divides (n lcm m) by NAT_D:def 4;

      (n gcd m) divides n by NAT_D:def 5;

      hence thesis by A1, NAT_D: 4;

    end;

    reserve p,q for natural Number;

    reserve i0,i,i1,i2,i4 for Integer;

    theorem :: NEWTON:63

     0 < m implies (n mod m) = (n - (m * (n div m)))

    proof

      reconsider z1 = (m * (n div m)), z2 = (n mod m) as Integer;

      assume m > 0 ;

      then (n - z1) = ((z1 + z2) - z1) by NAT_D: 2;

      hence thesis;

    end;

    theorem :: NEWTON:64

    i2 >= 0 implies (i1 mod i2) >= 0 by INT_1: 57;

    theorem :: NEWTON:65

    i2 > 0 implies (i1 mod i2) < i2 by INT_1: 58;

    theorem :: NEWTON:66

    i2 <> 0 implies i1 = (((i1 div i2) * i2) + (i1 mod i2)) by INT_1: 59;

    ::$Notion-Name

    theorem :: NEWTON:67

    ex i, i1 st ((i * m) + (i1 * n)) = (m gcd n) by NAT_D: 68;

    definition

      :: NEWTON:def6

      func SetPrimes -> Subset of NAT means

      : Def6: for n be Nat holds n in it iff n is prime;

      existence

      proof

        defpred P[ Nat] means $1 is prime;

        consider X be Subset of NAT such that

         A1: for n be Element of NAT holds n in X iff P[n] from SUBSET_1:sch 3;

        take X;

        let n be Nat;

        thus n in X implies n is prime by A1;

        assume

         A2: n is prime;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let A,B be Subset of NAT such that

         A3: for n be Nat holds n in A iff n is prime and

         A4: for n be Nat holds n in B iff n is prime;

        thus A c= B by A3, A4;

        let x be object;

        assume

         A5: x in B;

        then

        reconsider x as Element of NAT ;

        x is prime by A4, A5;

        hence thesis by A3;

      end;

    end

    registration

      cluster prime for Element of NAT ;

      existence by INT_2: 28;

      cluster prime for Nat;

      existence by INT_2: 28;

    end

    definition

      mode Prime is prime Nat;

    end

    reserve x for set;

    definition

      let p be natural Number;

      :: NEWTON:def7

      func SetPrimenumber p -> Subset of NAT means

      : Def7: for q be Nat holds q in it iff q < p & q is prime;

      existence

      proof

        defpred P[ Nat] means $1 < p & $1 is prime;

        consider X be Subset of NAT such that

         A1: for q be Element of NAT holds q in X iff P[q] from SUBSET_1:sch 3;

        take X;

        let q be Nat;

        thus q in X implies q < p & q is prime by A1;

        assume that

         A2: q < p and

         A3: q is prime;

        q in NAT by ORDINAL1:def 12;

        hence thesis by A1, A2, A3;

      end;

      uniqueness

      proof

        let A,B be Subset of NAT such that

         A4: for q be Nat holds q in A iff q < p & q is prime and

         A5: for q be Nat holds q in B iff q < p & q is prime;

        thus A c= B

        proof

          let x be object;

          assume

           A6: x in A;

          then

          reconsider x as Element of NAT ;

          

           A7: x is prime by A4, A6;

          x < p by A4, A6;

          hence thesis by A5, A7;

        end;

        let x be object;

        assume

         A8: x in B;

        then

        reconsider x as Element of NAT ;

        

         A9: x is prime by A5, A8;

        x < p by A5, A8;

        hence thesis by A4, A9;

      end;

    end

    theorem :: NEWTON:68

    

     Th68: ( SetPrimenumber p) c= SetPrimes

    proof

      let x be object;

      assume

       A1: x in ( SetPrimenumber p);

      then

      reconsider x9 = x as Element of NAT ;

      x9 is prime by A1, Def7;

      hence thesis by Def6;

    end;

    theorem :: NEWTON:69

    p <= q implies ( SetPrimenumber p) c= ( SetPrimenumber q)

    proof

      assume

       A1: p <= q;

      let x be object;

      assume

       A2: x in ( SetPrimenumber p);

      then

      reconsider x9 = x as Element of NAT ;

      x9 < p by A2, Def7;

      then

       A3: x9 < q by A1, XXREAL_0: 2;

      x9 is prime by A2, Def7;

      hence thesis by A3, Def7;

    end;

    theorem :: NEWTON:70

    

     Th70: ( SetPrimenumber p) c= ( Seg p)

    proof

      let x be object;

      assume

       A1: x in ( SetPrimenumber p);

      then

      reconsider q = x as Element of NAT ;

      q is prime by A1, Def7;

      then

       A2: 1 <= q by INT_2:def 4;

      q < p by A1, Def7;

      hence thesis by A2;

    end;

    theorem :: NEWTON:71

    

     Th71: ( SetPrimenumber p) is finite

    proof

      ( SetPrimenumber p) c= ( Seg p) by Th70;

      hence thesis;

    end;

    registration

      let n be natural Number;

      cluster ( SetPrimenumber n) -> finite;

      coherence by Th71;

    end

    reserve p for Prime;

    theorem :: NEWTON:72

    

     Th72: ex p st p > l

    proof

      reconsider two = 2 as Prime by INT_2: 28;

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

      l = 0 & (ex p st p is prime & p > l) or l = 1 & (ex p st p is prime & p > l) or 2 <= l & ex p st p is prime & p > l

      proof

        l <= 2 implies l = 0 or ... or l = 2;

        per cases ;

          case

           A1: l = 0 ;

          take two;

          thus thesis by A1;

        end;

          case

           A2: l = 1;

          take two;

          thus thesis by A2;

        end;

          case

           A3: 2 <= l;

          l <= (l ! ) by Th38;

          then 2 <= (l ! ) by A3, XXREAL_0: 2;

          then (2 + 0 ) <= ((l ! ) + 1) by XREAL_1: 7;

          then

          consider j be Element of NAT such that

           A4: j is prime and

           A5: j divides ((l ! ) + 1) by INT_2: 31;

          reconsider j9 = j as Prime by A4;

          take j9;

          

           A6: j <> 0 by A4, INT_2:def 4;

          j <> 1 by A4, INT_2:def 4;

          hence thesis by A5, A6, Th39, Th41;

        end;

      end;

      hence thesis;

    end;

    

     Lm1: ( SetPrimenumber 2) = {}

    proof

      assume ( SetPrimenumber 2) <> {} ;

      then

      consider x be object such that

       A1: x in ( SetPrimenumber 2) by XBOOLE_0:def 1;

      reconsider x as Nat by A1;

      

       A2: x is prime by A1, Def7;

      x < (1 + 1) by A1, Def7;

      then x <= 1 by NAT_1: 13;

      then 0 is prime or 1 is prime by A2, NAT_1: 25;

      hence contradiction by INT_2:def 4;

    end;

    registration

      cluster SetPrimes -> non empty;

      coherence by Def6, INT_2: 28;

    end

    registration

      cluster ( SetPrimenumber 2) -> empty;

      coherence by Lm1;

    end

    theorem :: NEWTON:73

    ( SetPrimenumber m) c= ( Seg m)

    proof

      let x be object;

      assume

       A1: x in ( SetPrimenumber m);

      then

      reconsider x as Element of NAT ;

      x is prime by A1, Def7;

      then

       A2: 1 <= x by INT_2:def 4;

      x < m by A1, Def7;

      hence thesis by A2;

    end;

    theorem :: NEWTON:74

    k >= m implies not k in ( SetPrimenumber m) by Def7;

    theorem :: NEWTON:75

    (( SetPrimenumber n) \/ {n}) is finite;

    theorem :: NEWTON:76

    

     Th76: for f be Prime, g be Nat st f < g holds (( SetPrimenumber f) \/ {f}) c= ( SetPrimenumber g)

    proof

      let f be Prime, g be Nat;

      assume

       A1: f < g;

      let x be object;

      assume

       A2: x in (( SetPrimenumber f) \/ {f});

      then

      reconsider x as Nat;

      per cases by A2, XBOOLE_0:def 3;

        suppose

         A3: x in ( SetPrimenumber f);

        then x < f by Def7;

        then

         A4: x < g by A1, XXREAL_0: 2;

        x is prime by A3, Def7;

        hence thesis by A4, Def7;

      end;

        suppose x in {f};

        then x = f by TARSKI:def 1;

        hence thesis by A1, Def7;

      end;

    end;

    theorem :: NEWTON:77

    k >= m implies not k in ( SetPrimenumber m) by Def7;

    

     Lm2: ( SetPrimenumber n) = { k where k be Element of NAT : k < n & k is prime }

    proof

      thus ( SetPrimenumber n) c= { k where k be Element of NAT : k < n & k is prime }

      proof

        let x be object;

        assume

         A1: x in ( SetPrimenumber n);

        then

        reconsider x as Element of NAT ;

        

         A2: x is prime by A1, Def7;

        x < n by A1, Def7;

        hence thesis by A2;

      end;

      let x be object;

      assume x in { k where k be Element of NAT : k < n & k is prime };

      then ex k be Element of NAT st x = k & k < n & k is prime;

      hence thesis by Def7;

    end;

    definition

      let n be Nat;

      :: NEWTON:def8

      func primenumber n -> prime Element of NAT means

      : Def8: n = ( card ( SetPrimenumber it ));

      existence

      proof

        defpred P1[ Nat] means ex m st $1 = ( card ( SetPrimenumber m)) & m is Prime;

        

         A1: for n st P1[n] holds P1[(n + 1)]

        proof

          let n;

          given m such that

           A2: n = ( card ( SetPrimenumber m)) and

           A3: m is Prime;

          defpred P[ Nat] means $1 is prime & $1 > m;

          

           A4: not m in ( SetPrimenumber m) by Def7;

          

           A5: ex k be Nat st P[k]

          proof

            ex p st p > m by Th72;

            hence thesis;

          end;

          consider k be Nat such that

           A6: P[k] & for l be Nat st P[l] holds k <= l from NAT_1:sch 5( A5);

          take k;

          

           A7: ( SetPrimenumber k) c= (( SetPrimenumber m) \/ {m})

          proof

            let s be object;

            assume

             A8: s in ( SetPrimenumber k);

            then

            reconsider s as Element of NAT ;

            

             A9: s is prime by A8, Def7;

            s < k by A8, Def7;

            then

             A10: s <= m by A6, A9;

            per cases by A10, XXREAL_0: 1;

              suppose s = m;

              then s in {m} by TARSKI:def 1;

              hence thesis by XBOOLE_0:def 3;

            end;

              suppose

               A11: s < m;

              

               A12: ( SetPrimenumber m) c= (( SetPrimenumber m) \/ {m}) by XBOOLE_1: 7;

              s in ( SetPrimenumber m) by A9, A11, Def7;

              hence thesis by A12;

            end;

          end;

          (( SetPrimenumber m) \/ {m}) c= ( SetPrimenumber k) by A3, A6, Th76;

          then ( SetPrimenumber k) = (( SetPrimenumber m) \/ {m}) by A7;

          hence (n + 1) = ( card ( SetPrimenumber k)) by A2, A4, CARD_2: 41;

          thus thesis by A6;

        end;

        ( SetPrimenumber 2) = { k where k be Element of NAT : k < 2 & k is prime } by Lm2;

        then

         A13: P1[ 0 ] by CARD_1: 27, INT_2: 28;

        for n holds P1[n] from NAT_1:sch 2( A13, A1);

        then

        consider m such that

         A14: n = ( card ( SetPrimenumber m)) and

         A15: m is Prime;

        m in NAT by ORDINAL1:def 12;

        hence thesis by A14, A15;

      end;

      uniqueness

      proof

        let f,g be prime Element of NAT ;

        assume that

         A16: n = ( card ( SetPrimenumber f)) and

         A17: n = ( card ( SetPrimenumber g));

        assume

         A18: f <> g;

        f < g & (n + 1) <= n or g < f & (n + 1) <= n

        proof

          per cases by A18, XXREAL_0: 1;

            case

             A19: f < g;

            

             A20: not f in ( SetPrimenumber f) by Def7;

            ( card (( SetPrimenumber f) \/ {f})) <= ( card ( SetPrimenumber g)) by A19, Th76, NAT_1: 43;

            hence thesis by A16, A17, A20, CARD_2: 41;

          end;

            case

             A21: g < f;

            

             A22: not g in ( SetPrimenumber g) by Def7;

            ( card (( SetPrimenumber g) \/ {g})) <= ( card ( SetPrimenumber f)) by A21, Th76, NAT_1: 43;

            hence thesis by A16, A17, A22, CARD_2: 41;

          end;

        end;

        hence contradiction by NAT_1: 13;

      end;

    end

    theorem :: NEWTON:78

    ( SetPrimenumber n) = { k where k be Element of NAT : k < n & k is prime } by Lm2;

    ::$Notion-Name

    theorem :: NEWTON:79

    

     Th79: SetPrimes is infinite

    proof

      assume

       A1: SetPrimes is finite;

      then

      reconsider SP = SetPrimes as finite set;

      consider n be Nat such that

       A2: ( SetPrimes ,( Seg n)) are_equipotent by A1, FINSEQ_1: 56;

      ( card SetPrimes ) = ( card ( Seg n)) by A2, CARD_1: 5;

      then ( card SetPrimes ) = ( card n) by FINSEQ_1: 55;

      then

       A3: ( card SP) = n;

      set p = ( primenumber (n + 1));

      set SPp = ( SetPrimenumber p);

      

       A4: (n + 1) = ( card ( SetPrimenumber p)) by Def8;

      ( card SPp) <= ( card SP) by Th68, NAT_1: 43;

      hence contradiction by A3, A4, NAT_1: 13;

    end;

    registration

      cluster SetPrimes -> non empty infinite;

      coherence by Th79;

    end

    reserve i for Nat;

    theorem :: NEWTON:80

    i is prime implies for m,n be Nat holds i divides (m * n) implies i divides m or i divides n

    proof

      defpred P[ Nat] means $1 is prime & ex m,n be Nat st $1 divides (m * n) & not $1 divides m & not $1 divides n;

      assume

       A1: i is prime;

      given m,n be Nat such that

       A2: i divides (m * n) and

       A3: not (i divides m or i divides n);

      

       A4: ex i be Nat st P[i] by A1, A2, A3;

      consider p9 be Nat such that

       A5: P[p9] and

       A6: for p1 be Nat st P[p1] holds p9 <= p1 from NAT_1:sch 5( A4);

      defpred Q[ Nat] means ex n be Nat st p9 divides ($1 * n) & not p9 divides $1 & not p9 divides n;

      

       A7: ex i be Nat st Q[i] by A5;

      consider m be Nat such that

       A8: Q[m] and

       A9: for m1 be Nat st Q[m1] holds m <= m1 from NAT_1:sch 5( A7);

      

       A10: m > 0 by A8;

      consider n be Nat such that

       A11: p9 divides (m * n) and

       A12: not p9 divides m and

       A13: not p9 divides n by A8;

      

       A14: m < p9

      proof

        set m1 = (m mod p9);

        assume

         A15: m >= p9;

        

         A16: p9 > 0 by A5, INT_2:def 4;

        then m = ((p9 * (m div p9)) + m1) by NAT_D: 2;

        then

         A17: (m * n) = (((p9 * (m div p9)) * n) + (m1 * n));

        m1 < p9 by A16, NAT_D: 1;

        then

         A18: m1 < m by A15, XXREAL_0: 2;

        

         A19: p9 divides (p9 * (m div p9)) by NAT_D:def 3;

        p9 divides (p9 * ((m div p9) * n)) by NAT_D:def 3;

        then

         A20: p9 divides (m1 * n) by A11, A17, NAT_D: 10;

        m = ((p9 * (m div p9)) + m1) by A16, NAT_D: 2;

        then not p9 divides m1 by A12, A19, NAT_D: 8;

        hence contradiction by A9, A13, A18, A20;

      end;

      

       A21: m < 2

      proof

        assume m >= 2;

        then

        consider p1 be Element of NAT such that

         A22: p1 is prime and

         A23: p1 divides m by INT_2: 31;

        

         A24: p1 > 1 by A22, INT_2:def 4;

        

         A25: not p1 divides p9

        proof

          assume p1 divides p9;

          then p1 = 1 or p1 = p9 by A5, INT_2:def 4;

          hence contradiction by A8, A22, A23, INT_2:def 4;

        end;

        p1 <= m by A10, A23, NAT_D: 7;

        then

         A26: not p9 <= p1 by A14, XXREAL_0: 2;

        

         A27: p1 <> 0 by A22, INT_2:def 4;

        consider k be Nat such that

         A28: (m * n) = (p9 * k) by A11, NAT_D:def 3;

        p1 divides (p9 * k) by A23, A28, NAT_D: 9;

        then p1 divides k by A6, A22, A26, A25;

        then

        consider k1 be Nat such that

         A29: k = (p1 * k1) by NAT_D:def 3;

        consider m1 be Nat such that

         A30: m = (p1 * m1) by A23, NAT_D:def 3;

        

         A31: m1 > 0 by A8, A30;

        

         A32: m1 <> m

        proof

          assume m1 = m;

          then m = (1 * m1);

          hence contradiction by A24, A30, A31, XREAL_1: 68;

        end;

        m1 divides m by A30, NAT_D:def 3;

        then m1 <= m by A10, NAT_D: 7;

        then

         A33: m1 < m by A32, XXREAL_0: 1;

        ((p9 * k1) * p1) = (p1 * (m1 * n)) by A28, A29, A30;

        then (m1 * n) = (p9 * k1) by A27, XCMPLX_1: 5;

        then

         A34: p9 divides (m1 * n) by NAT_D:def 3;

         not p9 divides m1 by A12, A30, NAT_D: 9;

        hence contradiction by A9, A13, A33, A34;

      end;

      m >= 2

      proof

        

         A35: m >= ( 0 + 1) by A10, NAT_1: 13;

        assume

         A36: m < 2;

        then m <= (1 + 1);

        then m = 1 by A36, A35, NAT_1: 9;

        hence contradiction by A11, A13;

      end;

      hence thesis by A21;

    end;

    theorem :: NEWTON:81

    for x be Complex holds (x |^ 2) = (x * x) & (x ^2 ) = (x |^ 2)

    proof

      let x be Complex;

      

      thus (x * x) = ((x |^ 1) * x)

      .= (x |^ (1 + 1)) by Th6

      .= (x |^ 2);

      hence thesis;

    end;

    theorem :: NEWTON:82

    (m qua Integer div n) = (m div n) & (m qua Integer mod n) = (m mod n);

    reserve x for Real;

    theorem :: NEWTON:83

    x > 0 implies (x |^ k) > 0

    proof

      defpred P[ Nat] means for x st x > 0 holds (x |^ $1) > 0 ;

      

       A1: for k holds P[k] implies P[(k + 1)]

      proof

        let k such that

         A2: for x st x > 0 holds (x |^ k) > 0 ;

        let x;

        

         A3: (x |^ (k + 1)) = (x * (x |^ k)) by Th6;

        assume

         A4: x > 0 ;

        then (x |^ k) > 0 by A2;

        hence thesis by A4, A3;

      end;

      

       A5: P[ 0 ] by RVSUM_1: 94;

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

      hence thesis;

    end;

    theorem :: NEWTON:84

    n > 0 implies ( 0 |^ n) = 0

    proof

      assume n > 0 ;

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

      hence thesis by Th11;

    end;

    definition

      let m,n be Element of NAT ;

      :: original: |^

      redefine

      func m |^ n -> Element of NAT ;

      coherence by ORDINAL1:def 12;

    end

    defpred P[ Nat] means for i st 2 <= i holds (i |^ $1) >= ($1 + 1);

    

     Lm3: P[ 0 ] by RVSUM_1: 94;

    

     Lm4: for n st P[n] holds P[(n + 1)]

    proof

      let n;

      assume

       A0: P[n];

      let i such that

       A4: 2 <= i;

      (i |^ n) >= (n + 1) by A0, A4;

      then

       A2: (i * (i |^ n)) >= (i * (n + 1)) by XREAL_1: 64;

      

       A1: (i |^ (n + 1)) = (i * (i |^ n)) by Th6;

      

       A3: (2 + n) <= (i + n) by A4, XREAL_1: 6;

      1 <= i by A4, XXREAL_0: 2;

      then (i * n) >= n by XREAL_1: 151;

      then ((i * n) + i) >= (n + i) by XREAL_1: 6;

      then (i * (i |^ n)) >= (n + i) by A2, XXREAL_0: 2;

      hence thesis by A1, A3, XXREAL_0: 2;

    end;

    theorem :: NEWTON:85

    

     Th85: 2 <= i implies (i |^ n) >= (n + 1)

    proof

      for n holds P[n] from NAT_1:sch 2( Lm3, Lm4);

      hence thesis;

    end;

    theorem :: NEWTON:86

    2 <= i implies (i |^ n) > n

    proof

      assume 2 <= i;

      then (i |^ n) >= (n + 1) by Th85;

      hence thesis by NAT_1: 13;

    end;

    reserve k for Nat;

    scheme :: NEWTON:sch1

    Euklides9 { F( Nat) -> Element of NAT , G( Nat) -> Element of NAT , a() -> Element of NAT , b() -> Element of NAT } :

ex k st F(k) = (a() gcd b()) & G(k) = 0

      provided

       A1: 0 < b()

       and

       A2: b() < a()

       and

       A3: F(0) = a()

       and

       A4: G(0) = b()

       and

       A5: for k st G(k) > 0 holds F(+) = G(k) & G(+) = (F(k) mod G(k));

      deffunc F( Nat, set) = ( IFEQ ($2, 0 , 0 ,G($1)));

      consider q be sequence of NAT such that

       A6: (q . 0 ) = a() and

       A7: for i be Nat holds (q . (i + 1)) = F(i,.) from NAT_1:sch 12;

      deffunc Q( Nat) = (q . $1);

      (q . ( 0 + 1)) = ( IFEQ ((q . 0 ), 0 , 0 ,G(0))) by A7

      .= G(0) by A2, A6, FUNCOP_1:def 8;

      then

       A8: Q(0) = a() & Q() = b() by A4, A6;

      

       A9: for k st (q . k) qua Element of NAT > 0 holds (q . k) = F(k)

      proof

        let k such that

         A10: (q . k) qua Element of NAT > 0 ;

        now

          per cases ;

            case k = 0 ;

            hence thesis by A3, A6;

          end;

            case k <> 0 ;

            then

            consider i be Nat such that

             A11: k = (i + 1) by NAT_1: 6;

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

             A12:

            now

              assume

               A13: (q . i) qua Element of NAT = 0 ;

              (q . k) = ( IFEQ ((q . i), 0 , 0 ,G(i))) by A7, A11

              .= 0 by A13, FUNCOP_1:def 8;

              hence contradiction by A10;

            end;

            (q . k) = ( IFEQ ((q . i), 0 , 0 ,G(i))) by A7, A11

            .= G(i) by A12, FUNCOP_1:def 8;

            hence thesis by A5, A10, A11;

          end;

        end;

        hence thesis;

      end;

      

       A14: for k holds Q(+) = ( Q(k) mod Q(+))

      proof

        let k;

        now

          per cases ;

            case

             A15: (q . (k + 1)) <> 0 ;

             A16:

            now

              

               A17: (q . k) = 0 or (q . k) <> 0 ;

              assume

               A18: G(k) = 0 ;

              (q . (k + 1)) = ( IFEQ ((q . k), 0 , 0 ,G(k))) by A7

              .= 0 by A18, A17, FUNCOP_1:def 8;

              hence contradiction by A15;

            end;

            

             A19: (q . (k + (1 + 1))) = (q . ((k + 1) + 1))

            .= ( IFEQ ((q . (k + 1)), 0 , 0 ,G(+))) by A7

            .= G(+) by A15, FUNCOP_1:def 8

            .= (F(k) mod G(k)) by A5, A16;

             A20:

            now

              assume

               A21: (q . k) = 0 ;

              (q . (k + 1)) = ( IFEQ ((q . k), 0 , 0 ,G(k))) by A7

              .= 0 by A21, FUNCOP_1:def 8;

              hence contradiction by A15;

            end;

            (q . (k + 1)) = ( IFEQ ((q . k), 0 , 0 ,G(k))) by A7

            .= G(k) by A20, FUNCOP_1:def 8;

            hence thesis by A9, A19, A20;

          end;

            case

             A22: (q . (k + 1)) = 0 ;

            

            thus (q . (k + 2)) = (q . ((k + 1) + 1))

            .= ( IFEQ ((q . (k + 1)), 0 , 0 ,G(+))) by A7

            .= 0 by A22, FUNCOP_1:def 8

            .= ((q . k) mod (q . (k + 1))) by A22, NAT_D:def 2;

          end;

        end;

        hence thesis;

      end;

      

       A23: 0 < b() & b() < a() by A1, A2;

      consider k such that

       A24: Q(k) = (a() gcd b()) & Q(+) = 0 from NAT_D:sch 1( A23, A8, A14);

      take k;

      thus F(k) = (a() gcd b()) by A1, A9, A24, Th58;

      (a() gcd b()) > 0 by A1, Th58;

      

      hence G(k) = ( IFEQ ((q . k), 0 , 0 ,G(k))) by A24, FUNCOP_1:def 8

      .= 0 by A7, A24;

    end;

    reserve k,n,n1,n2,m1,m2 for Nat;

    theorem :: NEWTON:87

    

     Th87: r <> 0 or n = 0 iff (r |^ n) <> 0

    proof

      defpred P[ Nat] means r <> 0 or $1 = 0 iff (r |^ $1) <> 0 ;

      

       A1: P[k] implies P[(k + 1)]

      proof

        assume

         A2: P[k];

        (r |^ (k + 1)) = ((r |^ k) * r) by Th6;

        hence thesis by A2;

      end;

      

       A3: P[ 0 ] by RVSUM_1: 94;

       P[k] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    

     Lm5: ((2 |^ n1) * ((2 * m1) + 1)) = ((2 |^ n2) * ((2 * m2) + 1)) implies n1 <= n2

    proof

      assume

       A1: ((2 |^ n1) * ((2 * m1) + 1)) = ((2 |^ n2) * ((2 * m2) + 1));

      assume

       A2: n1 > n2;

      then

      consider n be Nat such that

       A3: n1 = (n2 + n) by NAT_1: 10;

      n <> 0 by A2, A3;

      then

      consider k be Nat such that

       A4: n = (k + 1) by NAT_1: 6;

      

       A5: (2 |^ n2) <> 0 by Th87;

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

      (2 |^ n1) = ((2 |^ n2) * (2 |^ (k + 1))) by A3, A4, Th8;

      then ((2 |^ n1) * ((2 * m1) + 1)) = ((2 |^ n2) * ((2 |^ (k + 1)) * ((2 * m1) + 1)));

      then ((2 |^ (k + 1)) * ((2 * m1) + 1)) = ((2 * m2) + 1) by A1, A5, XCMPLX_1: 5;

      

      then ((2 * m2) + 1) = (((2 |^ k) * (2 |^ 1)) * ((2 * m1) + 1)) by Th8

      .= (2 * ((2 |^ k) * ((2 * m1) + 1)));

      then

       A6: 2 divides ((2 * m2) + 1) by NAT_D:def 3;

      2 divides (2 * m2) by NAT_D:def 3;

      hence contradiction by A6, NAT_D: 7, NAT_D: 10;

    end;

    theorem :: NEWTON:88

    ((2 |^ n1) * ((2 * m1) + 1)) = ((2 |^ n2) * ((2 * m2) + 1)) implies n1 = n2 & m1 = m2

    proof

      

       A1: (2 |^ n1) <> 0 by Th87;

      assume

       A2: ((2 |^ n1) * ((2 * m1) + 1)) = ((2 |^ n2) * ((2 * m2) + 1));

      then

       A3: n2 <= n1 by Lm5;

      n1 <= n2 by A2, Lm5;

      hence n1 = n2 by A3, XXREAL_0: 1;

      then ((2 * m1) + 1) = ((2 * m2) + 1) by A2, A1, XCMPLX_1: 5;

      hence thesis;

    end;

    theorem :: NEWTON:89

    k <= n implies (m |^ k) divides (m |^ n)

    proof

      assume k <= n;

      then

      consider t be Nat such that

       A1: n = (k + t) by NAT_1: 10;

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

      (m |^ n) = ((m |^ k) * (m |^ t)) by A1, Th8;

      hence thesis by NAT_D:def 3;

    end;