catalan1.miz



    begin

    theorem :: CATALAN1:1

    

     Th1: for n be Nat st n > 1 holds (n -' 1) <= ((2 * n) -' 3)

    proof

      let n be Nat;

      assume

       A1: n > 1;

      then (n -' 1) > (1 -' 1) by NAT_D: 57;

      then

       A2: ((n -' 1) + n) > ( 0 + n) by XREAL_1: 6;

      (2 * 1) < (2 * n) by A1, XREAL_1: 68;

      then (2 + 1) <= (2 * n) by NAT_1: 13;

      then

       A3: ((2 * n) -' 3) = ((2 * n) - 3) by XREAL_1: 233;

      (n -' 1) = (n - 1) by A1, XREAL_1: 233;

      then (((2 * n) - 1) - 1) > (n - 1) by A2, XREAL_1: 9;

      then (((2 * n) - 2) - 1) >= (n - 1) by INT_1: 52;

      hence thesis by A1, A3, XREAL_1: 233;

    end;

    theorem :: CATALAN1:2

    

     Th2: for n be Nat st n >= 1 holds (n -' 1) <= ((2 * n) -' 2)

    proof

      let n be Nat;

      assume

       A1: n >= 1;

      then (2 * 1) <= (2 * n) by XREAL_1: 64;

      then

       A2: (1 * (n -' 1)) <= (2 * (n -' 1)) & ((2 * n) -' 2) = ((2 * n) - 2) by XREAL_1: 64, XREAL_1: 233;

      (n -' 1) = (n - 1) by A1, XREAL_1: 233;

      hence thesis by A2;

    end;

    theorem :: CATALAN1:3

    

     Th3: for n be Nat st n > 1 holds n < ((2 * n) -' 1)

    proof

      let n be Nat;

      assume

       A1: n > 1;

      then (n + n) > (n + 1) by XREAL_1: 6;

      then

       A2: ((n + n) - 1) > ((n + 1) - 1) by XREAL_1: 9;

      (1 * 2) < (2 * n) by A1, XREAL_1: 68;

      hence thesis by A2, XREAL_1: 233, XXREAL_0: 2;

    end;

    theorem :: CATALAN1:4

    

     Th4: for n be Nat st n > 1 holds ((n -' 2) + 1) = (n -' 1)

    proof

      let n be Nat;

      assume n > 1;

      then

       A1: (n -' 1) >= 1 by NAT_D: 49;

      ((n -' 2) + 1) = (((n -' 1) -' 1) + 1) by NAT_D: 45

      .= (n -' 1) by A1, XREAL_1: 235;

      hence thesis;

    end;

    theorem :: CATALAN1:5

    for n be Nat st n > 1 holds ((((4 * n) * n) - (2 * n)) / (n + 1)) > 1

    proof

      defpred P[ Nat] means ((((4 * $1) * $1) - (2 * $1)) / ($1 + 1)) > 1;

      let n be Nat;

      

       A1: for k be non trivial Nat st P[k] holds P[(k + 1)]

      proof

        let k be non trivial Nat such that

         A2: P[k];

        set k1 = (k + 1);

        ((((4 * k) * k) - (2 * k)) / (k + 1)) = ((((4 * k) * k) - (2 * k)) * (1 / (k + 1))) by XCMPLX_1: 99;

        then (((((4 * k) * k) - (2 * k)) * (1 / (k + 1))) * (k + 1)) > (1 * (k + 1)) by A2, XREAL_1: 68;

        then (((4 * k) * k) - (2 * k)) > (1 * (k + 1)) by XCMPLX_1: 109;

        then ((((4 * k) * k) - (2 * k)) - (k + 1)) > 0 by XREAL_1: 50;

        then (((((4 * k) * k) - (3 * k)) - 1) + ((8 * k) + 1)) > ( 0 + 0 );

        then (((((4 * k1) * k1) - (2 * k1)) - (k1 + 1)) + (k1 + 1)) > ( 0 + (k1 + 1)) by XREAL_1: 8;

        then ((((4 * k1) * k1) - (2 * k1)) / (k1 + 1)) > ((k1 + 1) / (k1 + 1)) by XREAL_1: 74;

        hence thesis by XCMPLX_1: 60;

      end;

      assume n > 1;

      then

       A3: n is non trivial by NAT_2: 28;

      

       A4: P[2];

      for k be non trivial Nat holds P[k] from NAT_2:sch 2( A4, A1);

      hence thesis by A3;

    end;

    theorem :: CATALAN1:6

    

     Th6: for n be Nat st n > 1 holds (((((2 * n) -' 2) ! ) * n) * (n + 1)) < ((2 * n) ! )

    proof

      let n be Nat;

      assume

       A1: n > 1;

      then

       A2: (2 * 1) < (2 * n) by XREAL_1: 68;

      then

       A3: (((2 * n) -' 1) + 1) = (2 * n) by XREAL_1: 235, XXREAL_0: 2;

      (2 - 1) < ((2 * n) - 1) by A2, XREAL_1: 9;

      then

       A4: 1 < ((2 * n) -' 1) by A2, XREAL_1: 233, XXREAL_0: 2;

      (((2 * n) -' 2) + 1) = ((((2 * n) -' 1) -' 1) + 1) by NAT_D: 45

      .= ((2 * n) -' 1) by A4, XREAL_1: 235;

      

      then

       A5: (((((2 * n) -' 2) ! ) * ((2 * n) -' 1)) * (2 * n)) = ((((2 * n) -' 1) ! ) * (2 * n)) by NEWTON: 15

      .= ((2 * n) ! ) by A3, NEWTON: 15;

      (((2 * n) -' 2) ! ) > 0 by NEWTON: 17;

      then

       A6: ((((2 * n) -' 2) ! ) * n) > ( 0 * n) & ((((2 * n) -' 2) ! ) * n) < ((((2 * n) -' 2) ! ) * ((2 * n) -' 1)) by A1, Th3, XREAL_1: 68;

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

      hence thesis by A5, A6, XREAL_1: 98;

    end;

    theorem :: CATALAN1:7

    

     Th7: for n be Nat holds (2 * (2 - (3 / (n + 1)))) < 4

    proof

      let n be Nat;

      assume (2 * (2 - (3 / (n + 1)))) >= 4;

      then ((2 * (2 - (3 / (n + 1)))) / 2) >= (4 / 2) by XREAL_1: 72;

      then ((2 - (3 / (n + 1))) - 2) >= (2 - 2) by XREAL_1: 9;

      then ( - ( - ( - (3 / (n + 1))))) >= 0 ;

      hence thesis by XREAL_1: 139;

    end;

    begin

    definition

      let n be Nat;

      :: CATALAN1:def1

      func Catalan (n) -> Real equals ((((2 * n) -' 2) choose (n -' 1)) / n);

      coherence ;

    end

    theorem :: CATALAN1:8

    

     Th8: for n be Nat st n > 1 holds ( Catalan n) = ((((2 * n) -' 2) ! ) / (((n -' 1) ! ) * (n ! )))

    proof

      let n be Nat;

      assume

       A1: n > 1;

      then

       A2: (2 * 1) <= (2 * n) by XREAL_1: 64;

      

       A3: ((n -' 1) + 1) = n by A1, XREAL_1: 235;

      

       A4: (n -' 1) <= ((2 * n) -' 2) by A1, Th2;

      (((2 * n) -' 2) - (n -' 1)) = (((2 * n) -' 2) - (n - 1)) by A1, XREAL_1: 233

      .= (((2 * n) - 2) - (n - 1)) by A2, XREAL_1: 233

      .= (n -' 1) by A1, XREAL_1: 233;

      then (((2 * n) -' 2) choose (n -' 1)) = ((((2 * n) -' 2) ! ) / (((n -' 1) ! ) * ((n -' 1) ! ))) by A4, NEWTON:def 3;

      

      then ( Catalan n) = ((((2 * n) -' 2) ! ) / ((((n -' 1) ! ) * ((n -' 1) ! )) * n)) by XCMPLX_1: 78

      .= ((((2 * n) -' 2) ! ) / (((n -' 1) ! ) * (((n -' 1) ! ) * n)))

      .= ((((2 * n) -' 2) ! ) / (((n -' 1) ! ) * (n ! ))) by A3, NEWTON: 15;

      hence thesis;

    end;

    theorem :: CATALAN1:9

    

     Th9: for n be Nat st n > 1 holds ( Catalan n) = ((4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1)))

    proof

      let n be Nat;

      assume

       A1: n > 1;

      then

       A2: (n -' 1) <= ((2 * n) -' 3) by Th1;

      

       A3: (2 * 1) <= (2 * n) by A1, XREAL_1: 64;

      then

       A4: ((2 * n) -' 2) = ((2 * n) - 2) by XREAL_1: 233;

      

       A5: (1 + 1) <= n by A1, NAT_1: 13;

      then

       A6: (2 * 2) <= (2 * n) by XREAL_1: 64;

      then ((2 * n) -' 3) = ((2 * n) - 3) by XREAL_1: 233, XXREAL_0: 2;

      

      then

       A7: (((2 * n) -' 3) + 1) = ((2 * n) - 2)

      .= ((2 * n) -' 2) by A3, XREAL_1: 233;

      (((2 * n) -' 3) - (n -' 1)) = (((2 * n) -' 3) - (n - 1)) by A1, XREAL_1: 233

      .= (((2 * n) - 3) - (n - 1)) by A6, XREAL_1: 233, XXREAL_0: 2

      .= (n - 2)

      .= (n -' 2) by A5, XREAL_1: 233;

      then (((2 * n) -' 3) choose (n -' 1)) = ((((2 * n) -' 3) ! ) / (((n -' 1) ! ) * ((n -' 2) ! ))) by A2, NEWTON:def 3;

      then

       A8: (4 * (((2 * n) -' 3) choose (n -' 1))) = ((4 * (((2 * n) -' 3) ! )) / (((n -' 1) ! ) * ((n -' 2) ! ))) by XCMPLX_1: 74;

      

       A9: ((n -' 2) + 1) = (n -' 1) by A1, Th4;

      

       A10: (n -' 1) = (n - 1) by A1, XREAL_1: 233;

      then

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

      

       A12: (1 * n) < (2 * n) by A1, XREAL_1: 68;

      then

       A13: ((2 * n) -' 1) = ((2 * n) - 1) by A1, XREAL_1: 233, XXREAL_0: 2;

      1 < (2 * n) by A1, A12, XXREAL_0: 2;

      then

       A14: (((2 * n) -' 2) + 1) = ((2 * n) -' 1) by Th4;

      1 < (2 * n) by A1, A12, XXREAL_0: 2;

      then

       A15: (n -' 1) < ((2 * n) -' 1) by A12, NAT_D: 57;

      (((2 * n) -' 1) - (n -' 1)) = (((2 * n) -' 1) - (n - 1)) by A1, XREAL_1: 233

      .= ((((2 * n) -' 1) - n) + 1)

      .= ((((2 * n) - 1) - n) + 1) by A1, A12, XREAL_1: 233, XXREAL_0: 2

      .= n;

      then (((2 * n) -' 1) choose (n -' 1)) = ((((2 * n) -' 1) ! ) / (((n -' 1) ! ) * (n ! ))) by A15, NEWTON:def 3;

      then

       A16: (((2 * n) -' 1) choose (n -' 1)) = (((((2 * n) -' 2) ! ) * ((2 * n) -' 1)) / (((n -' 1) ! ) * (n ! ))) by A14, NEWTON: 15;

      (n - 1) > 0 by A1, XREAL_1: 50;

      

      then (4 * (((2 * n) -' 3) choose (n -' 1))) = (((n * (n - 1)) * (4 * (((2 * n) -' 3) ! ))) / ((n * (n - 1)) * (((n -' 1) ! ) * ((n -' 2) ! )))) by A1, A8, XCMPLX_1: 6, XCMPLX_1: 91

      .= ((((n - 1) * n) * (4 * (((2 * n) -' 3) ! ))) / (((n - 1) * (n * ((n -' 1) ! ))) * ((n -' 2) ! )))

      .= ((((n - 1) * n) * (4 * (((2 * n) -' 3) ! ))) / (((n - 1) * (n ! )) * ((n -' 2) ! ))) by A11, NEWTON: 15

      .= ((((n - 1) * n) * (4 * (((2 * n) -' 3) ! ))) / ((n ! ) * ((n -' 1) * ((n -' 2) ! )))) by A10

      .= (((2 * n) * (((2 * n) -' 2) * (((2 * n) -' 3) ! ))) / ((n ! ) * ((n -' 1) ! ))) by A4, A9, NEWTON: 15

      .= (((2 * n) * (((2 * n) -' 2) ! )) / ((n ! ) * ((n -' 1) ! ))) by A7, NEWTON: 15;

      

      then ((4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1))) = ((((2 * n) * (((2 * n) -' 2) ! )) - ((((2 * n) -' 2) ! ) * ((2 * n) -' 1))) / ((n ! ) * ((n -' 1) ! ))) by A16, XCMPLX_1: 120

      .= ( Catalan n) by A1, A13, Th8;

      hence thesis;

    end;

    theorem :: CATALAN1:10

    ( Catalan 0 ) = 0 ;

    theorem :: CATALAN1:11

    

     Th11: ( Catalan 1) = 1

    proof

      ( Catalan 1) = (((2 * 1) -' 2) choose 0 ) by XREAL_1: 232

      .= 1 by NEWTON: 19;

      hence thesis;

    end;

    theorem :: CATALAN1:12

    

     Th12: ( Catalan 2) = 1

    proof

      

       A1: (4 -' 2) = (4 - 2) by XREAL_1: 233

      .= 2;

      (2 -' 1) = (2 - 1) by XREAL_1: 233

      .= 1;

      

      then ( Catalan 2) = (2 / 2) by A1, NEWTON: 23

      .= 1;

      hence thesis;

    end;

    theorem :: CATALAN1:13

    

     Th13: for n be Nat holds ( Catalan n) is Integer

    proof

      let n be Nat;

      per cases by NAT_1: 25;

        suppose n = 0 ;

        hence thesis;

      end;

        suppose n = 1;

        hence thesis;

      end;

        suppose n > 1;

        then ( Catalan n) = ((4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1))) by Th9;

        hence thesis;

      end;

    end;

    theorem :: CATALAN1:14

    

     Th14: for k be Nat holds ( Catalan (k + 1)) = (((2 * k) ! ) / ((k ! ) * ((k + 1) ! )))

    proof

      let k be Nat;

      reconsider l = ((2 * k) - k) as Nat;

      l = k & (1 * k) <= (2 * k) by XREAL_1: 64;

      then

       A1: ((2 * k) choose k) = (((2 * k) ! ) / ((k ! ) * (k ! ))) by NEWTON:def 3;

      (((2 * k) + 2) -' 2) = (2 * k) & ((k + 1) -' 1) = k by NAT_D: 34;

      

      then ( Catalan (k + 1)) = (((2 * k) ! ) / (((k ! ) * (k ! )) * (k + 1))) by A1, XCMPLX_1: 78

      .= (((2 * k) ! ) / ((k ! ) * ((k ! ) * (k + 1))))

      .= (((2 * k) ! ) / ((k ! ) * ((k + 1) ! ))) by NEWTON: 15;

      hence thesis;

    end;

    theorem :: CATALAN1:15

    

     Th15: for n be Nat st n > 1 holds ( Catalan n) < ( Catalan (n + 1))

    proof

      let n be Nat;

      set a = (((2 * n) -' 2) ! );

      set b = ((2 * n) ! );

      

       A1: ( Catalan (n + 1)) = (((2 * n) ! ) / ((n ! ) * ((n + 1) ! ))) by Th14;

      assume

       A2: n > 1;

      then ((n -' 1) + 1) = n by XREAL_1: 235;

      

      then

       A3: (((a * n) * (n + 1)) / ((n ! ) * ((n + 1) ! ))) = (((a * n) * (n + 1)) / ((n * ((n -' 1) ! )) * ((n + 1) ! ))) by NEWTON: 15

      .= ((n * (a * (n + 1))) / (n * (((n -' 1) ! ) * ((n + 1) ! ))))

      .= ((a * (n + 1)) / (((n -' 1) ! ) * ((n + 1) ! ))) by A2, XCMPLX_1: 91

      .= ((a * (n + 1)) / (((n -' 1) ! ) * ((n + 1) * (n ! )))) by NEWTON: 15

      .= ((a * (n + 1)) / ((((n -' 1) ! ) * (n ! )) * (n + 1)))

      .= (a / (((n -' 1) ! ) * (n ! ))) by XCMPLX_1: 91;

      (n ! ) > 0 & ((n + 1) ! ) > 0 by NEWTON: 17;

      then ((n ! ) * ((n + 1) ! )) > ( 0 * (n ! )) by XREAL_1: 68;

      then (((a * n) * (n + 1)) / ((n ! ) * ((n + 1) ! ))) < (b / ((n ! ) * ((n + 1) ! ))) by A2, Th6, XREAL_1: 74;

      hence thesis by A2, A1, A3, Th8;

    end;

    theorem :: CATALAN1:16

    

     Th16: for n be Nat holds ( Catalan n) <= ( Catalan (n + 1))

    proof

      let n be Nat;

      per cases by NAT_1: 25;

        suppose n = 0 ;

        hence thesis;

      end;

        suppose n = 1;

        hence thesis by Th11, Th12;

      end;

        suppose n > 1;

        hence thesis by Th15;

      end;

    end;

    theorem :: CATALAN1:17

    for n be Nat holds ( Catalan n) >= 0 ;

    theorem :: CATALAN1:18

    

     Th18: for n be Nat holds ( Catalan n) is Element of NAT

    proof

      let n be Nat;

      ( Catalan n) is Integer by Th13;

      hence thesis by INT_1: 3;

    end;

    theorem :: CATALAN1:19

    

     Th19: for n be Nat st n > 0 holds ( Catalan (n + 1)) = ((2 * (2 - (3 / (n + 1)))) * ( Catalan n))

    proof

      let n be Nat;

      assume

       A1: n > 0 ;

      then

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

      

      then

       A3: (2 * (n -' 1)) = (2 * (n - 1)) by XREAL_1: 233

      .= ((2 * n) - (2 * 1))

      .= ((2 * n) -' 2) by A2, XREAL_1: 64, XREAL_1: 233;

      

       A4: ( Catalan n) = ( Catalan ((n -' 1) + 1)) by A2, XREAL_1: 235

      .= (((2 * (n -' 1)) ! ) / (((n -' 1) ! ) * (((n -' 1) + 1) ! ))) by Th14

      .= ((((2 * n) -' 2) ! ) / (((n -' 1) ! ) * (n ! ))) by A2, A3, XREAL_1: 235;

      

       A5: ((n -' 1) + 1) = n by A2, XREAL_1: 235;

      

       A6: (1 * 2) <= (2 * n) by A2, XREAL_1: 64;

      then

       A7: ((2 * n) -' 1) = ((2 * n) - 1) by XREAL_1: 233, XXREAL_0: 2;

      

       A8: (2 * (2 - (3 / (n + 1)))) = (2 * (((2 * (n + 1)) / (n + 1)) - (3 / (n + 1)))) by XCMPLX_1: 89

      .= (2 * (((2 * (n + 1)) - 3) / (n + 1))) by XCMPLX_1: 120

      .= ((2 * ((2 * n) - 1)) / (n + 1)) by XCMPLX_1: 74

      .= (((((2 * n) -' 1) * 2) * n) / (n * (n + 1))) by A1, A7, XCMPLX_1: 91

      .= ((((2 * n) -' 1) * (2 * n)) / (n * (n + 1)));

      

       A9: (((2 * n) -' 1) + 1) = (2 * n) by A6, XREAL_1: 235, XXREAL_0: 2;

      1 < (2 * n) by A6, XXREAL_0: 2;

      then

       A10: (((2 * n) -' 2) + 1) = ((2 * n) -' 1) by Th4;

      ( Catalan (n + 1)) = (((2 * n) ! ) / ((n ! ) * ((n + 1) ! ))) by Th14

      .= (((((2 * n) -' 1) ! ) * (2 * n)) / ((n ! ) * ((n + 1) ! ))) by A9, NEWTON: 15

      .= ((((((2 * n) -' 2) ! ) * ((2 * n) -' 1)) * (2 * n)) / ((n ! ) * ((n + 1) ! ))) by A10, NEWTON: 15

      .= ((((((2 * n) -' 2) ! ) * ((2 * n) -' 1)) * (2 * n)) / ((n ! ) * ((n ! ) * (n + 1)))) by NEWTON: 15

      .= ((((((2 * n) -' 2) ! ) * ((2 * n) -' 1)) * (2 * n)) / ((n ! ) * ((((n -' 1) ! ) * n) * (n + 1)))) by A5, NEWTON: 15

      .= (((((2 * n) -' 2) ! ) * (((2 * n) -' 1) * (2 * n))) / (((n ! ) * ((n -' 1) ! )) * (n * (n + 1))))

      .= (( Catalan n) * ((((2 * n) -' 1) * (2 * n)) / (n * (n + 1)))) by A4, XCMPLX_1: 76;

      hence thesis by A8;

    end;

    registration

      let n be Nat;

      cluster ( Catalan n) -> natural;

      coherence by Th18;

    end

    theorem :: CATALAN1:20

    

     Th20: for n be Nat st n > 0 holds ( Catalan n) > 0

    proof

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

      let n be Nat;

      assume

       A1: n > 0 ;

      

       A2: for n be non zero Nat st P[n] holds P[(n + 1)] by Th16;

      

       A3: P[1] by Th11;

      for n be non zero Nat holds P[n] from NAT_1:sch 10( A3, A2);

      hence thesis by A1;

    end;

    registration

      let n be non zero Nat;

      cluster ( Catalan n) -> non zero;

      coherence by Th20;

    end

    theorem :: CATALAN1:21

    for n be Nat st n > 0 holds ( Catalan (n + 1)) < (4 * ( Catalan n))

    proof

      let n be Nat;

      assume

       A1: n > 0 ;

      then ( Catalan (n + 1)) = ((2 * (2 - (3 / (n + 1)))) * ( Catalan n)) by Th19;

      hence thesis by A1, Th7, XREAL_1: 68;

    end;