numpoly1.miz



    begin

    scheme :: NUMPOLY1:sch1

    LNatRealSeq { F( set) -> Real } :

(ex seq be Real_Sequence st for n be Nat holds (seq . n) = F(n)) & (for seq1,seq2 be Real_Sequence st (for n be Nat holds (seq1 . n) = F(n)) & (for n be Nat holds (seq2 . n) = F(n)) holds seq1 = seq2);

      consider seq be Real_Sequence such that

       A1: for n be Nat holds (seq . n) = F(n) from SEQ_1:sch 1;

      thus ex seq be Real_Sequence st for n be Nat holds (seq . n) = F(n) by A1;

      let seq1,seq2 be Real_Sequence;

      assume that

       A2: for n be Nat holds (seq1 . n) = F(n) and

       A3: for n be Nat holds (seq2 . n) = F(n);

      let n be Element of NAT ;

      

      thus (seq1 . n) = F(n) by A2

      .= (seq2 . n) by A3;

    end;

    theorem :: NUMPOLY1:1

    

     Th1: for n,a be non zero Nat holds 1 <= (a * n)

    proof

      let n,a be non zero Nat;

      ( 0 + 1) <= (a * n) by NAT_1: 13;

      hence thesis;

    end;

    

     Lm1: for n be Integer holds (n * (n - 1)) is even

    proof

      let n be Integer;

      per cases ;

        suppose n is even;

        hence thesis;

      end;

        suppose n is odd;

        hence thesis;

      end;

    end;

    

     Lm2: for n be Integer holds (n * (n + 1)) is even

    proof

      let n be Integer;

      per cases ;

        suppose n is even;

        hence thesis;

      end;

        suppose n is odd;

        hence thesis;

      end;

    end;

    registration

      let n be Integer;

      cluster (n * (n - 1)) -> even;

      coherence by Lm1;

      cluster (n * (n + 1)) -> even;

      coherence by Lm2;

    end

    theorem :: NUMPOLY1:2

    

     Th2: for n be even Integer holds (n / 2) is Integer

    proof

      let n be even Integer;

      consider j be Integer such that

       A1: n = (2 * j) by ABIAN: 11;

      thus thesis by A1;

    end;

    registration

      let n be even Nat;

      cluster (n / 2) -> natural;

      coherence

      proof

        ex k be Nat st n = (2 * k) by ABIAN:def 2;

        hence thesis;

      end;

    end

    registration

      let n be odd Nat;

      cluster (n - 1) -> natural;

      coherence by CHORD: 2;

    end

    registration

      let n be odd Nat;

      cluster (n - 1) -> even;

      coherence ;

    end

    reserve n,s for Nat;

    theorem :: NUMPOLY1:3

    

     Th3: (n mod 5) = 0 or ... or (n mod 5) = 4

    proof

      (n mod 5) < (4 + 1) by NAT_D: 1;

      then (n mod 5) <= 4 by NAT_1: 13;

      hence thesis;

    end;

    theorem :: NUMPOLY1:4

    

     Th4: for k be Nat st k <> 0 holds (n,(n mod k)) are_congruent_mod k

    proof

      let k be Nat;

      assume k <> 0 ;

      then ((n mod k) - 0 ) = (n - ((n div k) * k)) by INT_1:def 10;

      then k divides (n - (n mod k)) by INT_1:def 3;

      hence thesis by INT_1:def 4;

    end;

    theorem :: NUMPOLY1:5

    

     Th5: (n, 0 ) are_congruent_mod 5 or ... or (n,4) are_congruent_mod 5

    proof

      (n mod 5) = 0 or ... or (n mod 5) = 4 by Th3;

      hence thesis by Th4;

    end;

    theorem :: NUMPOLY1:6

    

     Th6: not (((n * n) + n),4) are_congruent_mod 5

    proof

      assume (((n * n) + n),4) are_congruent_mod 5;

      then

       A1: (4,((n * n) + n)) are_congruent_mod 5 by INT_1: 14;

      (n, 0 ) are_congruent_mod 5 or ... or (n,4) are_congruent_mod 5 by Th5;

      per cases ;

        suppose

         A2: (n, 0 ) are_congruent_mod 5;

        then ((n * n),( 0 * 0 )) are_congruent_mod 5 by INT_1: 18;

        then (((n * n) + n),( 0 + 0 )) are_congruent_mod 5 by A2, INT_1: 16;

        then 5 divides (4 - 0 ) by INT_1:def 4, A1, INT_1: 15;

        hence thesis by NAT_D: 7;

      end;

        suppose

         A3: (n,1) are_congruent_mod 5;

        then ((n * n),(1 * 1)) are_congruent_mod 5 by INT_1: 18;

        then (((n * n) + n),(1 + 1)) are_congruent_mod 5 by A3, INT_1: 16;

        then 5 divides (4 - 2) by INT_1:def 4, A1, INT_1: 15;

        hence thesis by NAT_D: 7;

      end;

        suppose

         A4: (n,2) are_congruent_mod 5;

        then ((n * n),(2 * 2)) are_congruent_mod 5 by INT_1: 18;

        then (((n * n) + n),(4 + 2)) are_congruent_mod 5 by A4, INT_1: 16;

        then (6,((n * n) + n)) are_congruent_mod 5 by INT_1: 14;

        then ((6 - 5),((n * n) + n)) are_congruent_mod 5 by INT_1: 22;

        then (((n * n) + n),1) are_congruent_mod 5 by INT_1: 14;

        then 5 divides (4 - 1) by INT_1:def 4, A1, INT_1: 15;

        then 5 <= 3 by NAT_D: 7;

        hence thesis;

      end;

        suppose

         A5: (n,3) are_congruent_mod 5;

        then ((n * n),(3 * 3)) are_congruent_mod 5 by INT_1: 18;

        then (((n * n) + n),(9 + 3)) are_congruent_mod 5 by A5, INT_1: 16;

        then (12,((n * n) + n)) are_congruent_mod 5 by INT_1: 14;

        then ((12 - 5),((n * n) + n)) are_congruent_mod 5 by INT_1: 22;

        then ((7 - 5),((n * n) + n)) are_congruent_mod 5 by INT_1: 22;

        then (((n * n) + n),2) are_congruent_mod 5 by INT_1: 14;

        then 5 divides (4 - 2) by INT_1:def 4, A1, INT_1: 15;

        hence thesis by NAT_D: 7;

      end;

        suppose

         A6: (n,4) are_congruent_mod 5;

        then ((n * n),(4 * 4)) are_congruent_mod 5 by INT_1: 18;

        then (((n * n) + n),(16 + 4)) are_congruent_mod 5 by A6, INT_1: 16;

        then (20,((n * n) + n)) are_congruent_mod 5 by INT_1: 14;

        then ((20 - 5),((n * n) + n)) are_congruent_mod 5 by INT_1: 22;

        then ((15 - 5),((n * n) + n)) are_congruent_mod 5 by INT_1: 22;

        then ((10 - 5),((n * n) + n)) are_congruent_mod 5 by INT_1: 22;

        then ((5 - 5),((n * n) + n)) are_congruent_mod 5 by INT_1: 22;

        then (((n * n) + n), 0 ) are_congruent_mod 5 by INT_1: 14;

        then 5 divides (4 - 0 ) by INT_1:def 4, A1, INT_1: 15;

        hence thesis by NAT_D: 7;

      end;

    end;

    theorem :: NUMPOLY1:7

    

     Th7: not (((n * n) + n),3) are_congruent_mod 5

    proof

      assume (((n * n) + n),3) are_congruent_mod 5;

      then

       A1: (3,((n * n) + n)) are_congruent_mod 5 by INT_1: 14;

      (n, 0 ) are_congruent_mod 5 or ... or (n,4) are_congruent_mod 5 by Th5;

      per cases ;

        suppose

         A2: (n, 0 ) are_congruent_mod 5;

        then ((n * n),( 0 * 0 )) are_congruent_mod 5 by INT_1: 18;

        then (((n * n) + n),( 0 + 0 )) are_congruent_mod 5 by A2, INT_1: 16;

        then 5 divides (3 - 0 ) by INT_1:def 4, A1, INT_1: 15;

        hence thesis by NAT_D: 7;

      end;

        suppose

         A3: (n,1) are_congruent_mod 5;

        then ((n * n),(1 * 1)) are_congruent_mod 5 by INT_1: 18;

        then (((n * n) + n),(1 + 1)) are_congruent_mod 5 by A3, INT_1: 16;

        then 5 divides (3 - 2) by INT_1:def 4, A1, INT_1: 15;

        then 5 <= 1 by NAT_D: 7;

        hence thesis;

      end;

        suppose

         A4: (n,2) are_congruent_mod 5;

        then ((n * n),(2 * 2)) are_congruent_mod 5 by INT_1: 18;

        then (((n * n) + n),(4 + 2)) are_congruent_mod 5 by A4, INT_1: 16;

        then (6,((n * n) + n)) are_congruent_mod 5 by INT_1: 14;

        then ((6 - 5),((n * n) + n)) are_congruent_mod 5 by INT_1: 22;

        then (((n * n) + n),1) are_congruent_mod 5 by INT_1: 14;

        then 5 divides (3 - 1) by INT_1:def 4, A1, INT_1: 15;

        then 5 <= 2 by NAT_D: 7;

        hence thesis;

      end;

        suppose

         A5: (n,3) are_congruent_mod 5;

        then ((n * n),(3 * 3)) are_congruent_mod 5 by INT_1: 18;

        then (((n * n) + n),(9 + 3)) are_congruent_mod 5 by A5, INT_1: 16;

        then (12,((n * n) + n)) are_congruent_mod 5 by INT_1: 14;

        then ((12 - 5),((n * n) + n)) are_congruent_mod 5 by INT_1: 22;

        then ((7 - 5),((n * n) + n)) are_congruent_mod 5 by INT_1: 22;

        then (((n * n) + n),2) are_congruent_mod 5 by INT_1: 14;

        then 5 divides (3 - 2) by INT_1:def 4, A1, INT_1: 15;

        then 5 <= 1 by NAT_D: 7;

        hence thesis;

      end;

        suppose

         A6: (n,4) are_congruent_mod 5;

        then ((n * n),(4 * 4)) are_congruent_mod 5 by INT_1: 18;

        then (((n * n) + n),(16 + 4)) are_congruent_mod 5 by A6, INT_1: 16;

        then (20,((n * n) + n)) are_congruent_mod 5 by INT_1: 14;

        then ((20 - 5),((n * n) + n)) are_congruent_mod 5 by INT_1: 22;

        then ((15 - 5),((n * n) + n)) are_congruent_mod 5 by INT_1: 22;

        then ((10 - 5),((n * n) + n)) are_congruent_mod 5 by INT_1: 22;

        then ((5 - 5),((n * n) + n)) are_congruent_mod 5 by INT_1: 22;

        then (((n * n) + n), 0 ) are_congruent_mod 5 by INT_1: 14;

        then 5 divides (3 - 0 ) by INT_1:def 4, A1, INT_1: 15;

        hence thesis by NAT_D: 7;

      end;

    end;

    theorem :: NUMPOLY1:8

    

     Th8: (n mod 10) = 0 or ... or (n mod 10) = 9

    proof

      (n mod 10) < (9 + 1) by NAT_D: 1;

      then (n mod 10) <= 9 by NAT_1: 13;

      hence thesis;

    end;

    theorem :: NUMPOLY1:9

    

     Th9: (n, 0 ) are_congruent_mod 10 or ... or (n,9) are_congruent_mod 10

    proof

      (n mod 10) = 0 or ... or (n mod 10) = 9 by Th8;

      hence thesis by Th4;

    end;

    registration

      cluster non trivial -> 2 _or_greater for Nat;

      coherence by EC_PF_2:def 1, NAT_2: 29;

      cluster 2 _or_greater -> non trivial for Nat;

      coherence

      proof

        let n be Nat;

        assume n is 2 _or_greater;

        then n <> 0 & n <> 1 by EC_PF_2:def 1;

        hence thesis by NAT_2:def 1;

      end;

    end

    registration

      cluster 4 _or_greater -> 3 _or_greater non zero for Nat;

      coherence

      proof

        let n be Nat;

        assume n is 4 _or_greater;

        then n >= 4 by EC_PF_2:def 1;

        hence thesis by EC_PF_2:def 1, XXREAL_0: 2;

      end;

    end

    registration

      cluster 4 _or_greater -> non trivial for Nat;

      coherence

      proof

        let n be Nat;

        assume n is 4 _or_greater;

        then n <> 1 & n <> 0 by EC_PF_2:def 1;

        hence thesis by NAT_2:def 1;

      end;

    end

    registration

      cluster 4 _or_greater for Nat;

      existence by EC_PF_2:def 1;

      cluster 3 _or_greater for Nat;

      existence by EC_PF_2:def 1;

    end

    begin

    definition

      let n be Nat;

      :: NUMPOLY1:def1

      func Triangle n -> Real equals ( Sum ( idseq n));

      coherence ;

    end

    definition

      let n be object;

      :: NUMPOLY1:def2

      attr n is triangular means

      : Def2: ex k be Nat st n = ( Triangle k);

    end

    registration

      let n be zero number;

      cluster ( Triangle n) -> zero;

      coherence by RVSUM_1: 72;

    end

    theorem :: NUMPOLY1:10

    

     Th10: ( Triangle (n + 1)) = (( Triangle n) + (n + 1))

    proof

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

      

       A1: P[ 0 ] by FINSEQ_2: 50, RVSUM_1: 73;

      

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

      proof

        let k be Nat such that P[k];

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

        (((( Triangle (k + 1)) + k) + 1) + 1) = (((( Sum (( idseq k1) ^ <*(k1 + 1)*>)) + k) + 1) + 1) by FINSEQ_2: 51

        .= (( Sum (( idseq k1) ^ <*(k1 + 1)*>)) + ((k + 1) + 1))

        .= (( Sum ( idseq (k1 + 1))) + ((k1 + 1) + 1)) by FINSEQ_2: 51

        .= ( Sum (( idseq (k1 + 1)) ^ <*((k1 + 1) + 1)*>)) by RVSUM_1: 74

        .= ( Triangle ((k + 1) + 1)) by FINSEQ_2: 51;

        hence thesis;

      end;

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

      hence thesis;

    end;

    theorem :: NUMPOLY1:11

    

     Th11: ( Triangle 1) = 1 by FINSEQ_2: 50, RVSUM_1: 73;

    theorem :: NUMPOLY1:12

    

     Th12: ( Triangle 2) = 3

    proof

      

      thus ( Triangle 2) = (1 + 2) by RVSUM_1: 77, FINSEQ_2: 52

      .= 3;

    end;

    theorem :: NUMPOLY1:13

    

     Th13: ( Triangle 3) = 6

    proof

      

      thus ( Triangle 3) = ((1 + 2) + 3) by RVSUM_1: 78, FINSEQ_2: 53

      .= 6;

    end;

    theorem :: NUMPOLY1:14

    

     Th14: ( Triangle 4) = 10

    proof

      

      thus ( Triangle 4) = (( Triangle 3) + (3 + 1)) by Th10

      .= 10 by Th13;

    end;

    theorem :: NUMPOLY1:15

    

     Th15: ( Triangle 5) = 15

    proof

      

      thus ( Triangle 5) = (( Triangle 4) + (4 + 1)) by Th10

      .= 15 by Th14;

    end;

    theorem :: NUMPOLY1:16

    

     Th16: ( Triangle 6) = 21

    proof

      

      thus ( Triangle 6) = (( Triangle 5) + (5 + 1)) by Th10

      .= 21 by Th15;

    end;

    theorem :: NUMPOLY1:17

    

     Th17: ( Triangle 7) = 28

    proof

      

      thus ( Triangle 7) = (( Triangle 6) + (6 + 1)) by Th10

      .= 28 by Th16;

    end;

    theorem :: NUMPOLY1:18

    

     Th18: ( Triangle 8) = 36

    proof

      

      thus ( Triangle 8) = (( Triangle 7) + (7 + 1)) by Th10

      .= 36 by Th17;

    end;

    theorem :: NUMPOLY1:19

    

     Th19: ( Triangle n) = ((n * (n + 1)) / 2)

    proof

      defpred P[ Nat] means ( Triangle $1) = (($1 * ($1 + 1)) / 2);

      

       A1: P[ 0 ];

      

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

      proof

        let k be Nat such that

         A3: P[k];

        ( Triangle (k + 1)) = (( Triangle k) + (k + 1)) by Th10

        .= (((k + 1) * (k + 2)) / 2) by A3;

        hence thesis;

      end;

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

      hence thesis;

    end;

    theorem :: NUMPOLY1:20

    

     Th20: ( Triangle n) >= 0

    proof

      

       A1: ( Triangle n) = ((n * (n + 1)) / 2) by Th19;

      thus thesis by A1;

    end;

    registration

      let n be Nat;

      cluster ( Triangle n) -> non negative;

      coherence by Th20;

    end

    registration

      let n be non zero Nat;

      cluster ( Triangle n) -> positive;

      coherence

      proof

        ((n * (n + 1)) / 2) > 0 ;

        hence thesis by Th19;

      end;

    end

    registration

      let n be Nat;

      cluster ( Triangle n) -> natural;

      coherence

      proof

        ( Triangle n) = ((n * (n + 1)) / 2) by Th19;

        hence thesis;

      end;

    end

    

     Lm3: ( 0 - 1) < 0 ;

    theorem :: NUMPOLY1:21

    

     Th21: ( Triangle (n -' 1)) = ((n * (n - 1)) / 2)

    proof

      per cases ;

        suppose n <> 0 ;

        then

         A1: 1 <= (1 * n) by Th1;

        ( Triangle (n -' 1)) = (((n -' 1) * ((n -' 1) + 1)) / 2) by Th19

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

        hence thesis by XREAL_1: 233, A1;

      end;

        suppose

         A2: n = 0 ;

        

        then ( Triangle (n -' 1)) = ( Triangle 0 ) by XREAL_0:def 2, Lm3

        .= ((n * (n - 1)) / 2) by A2;

        hence thesis;

      end;

    end;

    registration

      cluster triangular -> natural for number;

      coherence ;

    end

    registration

      cluster triangular non zero for number;

      existence

      proof

        reconsider a = ( Triangle 1) as number by TARSKI: 1;

        take a;

        thus thesis;

      end;

    end

    theorem :: NUMPOLY1:22

    

     Th22: for n be triangular number holds not (n,7) are_congruent_mod 10

    proof

      let n be triangular number;

      consider k be Nat such that

       A1: n = ( Triangle k) by Def2;

      

       A2: (4 * 5) = 20;

      

       A3: n = ((k * (k + 1)) / 2) by A1, Th19;

      assume (n,7) are_congruent_mod 10;

      then ((((k * (k + 1)) / 2) * 2),(7 * 2)) are_congruent_mod (10 * 2) by A3, INT_4: 10;

      then ((k * (k + 1)),14) are_congruent_mod 5 by A2, INT_1: 20;

      then (14,(k * (k + 1))) are_congruent_mod 5 by INT_1: 14;

      then ((14 - 5),(k * (k + 1))) are_congruent_mod 5 by INT_1: 22;

      then ((9 - 5),(k * (k + 1))) are_congruent_mod 5 by INT_1: 22;

      then (4,((k * k) + k)) are_congruent_mod 5;

      hence thesis by Th6, INT_1: 14;

    end;

    theorem :: NUMPOLY1:23

    

     Th23: for n be triangular number holds not (n,9) are_congruent_mod 10

    proof

      let n be triangular number;

      consider k be Nat such that

       A1: n = ( Triangle k) by Def2;

      

       A2: (4 * 5) = 20;

      

       A3: n = ((k * (k + 1)) / 2) by A1, Th19;

      assume (n,9) are_congruent_mod 10;

      then ((((k * (k + 1)) / 2) * 2),(9 * 2)) are_congruent_mod (10 * 2) by A3, INT_4: 10;

      then ((k * (k + 1)),18) are_congruent_mod 5 by A2, INT_1: 20;

      then (18,(k * (k + 1))) are_congruent_mod 5 by INT_1: 14;

      then ((18 - 5),(k * (k + 1))) are_congruent_mod 5 by INT_1: 22;

      then ((13 - 5),(k * (k + 1))) are_congruent_mod 5 by INT_1: 22;

      then ((8 - 5),(k * (k + 1))) are_congruent_mod 5 by INT_1: 22;

      then (3,((k * k) + k)) are_congruent_mod 5;

      hence thesis by Th7, INT_1: 14;

    end;

    theorem :: NUMPOLY1:24

    

     Th24: for n be triangular number holds not (n,2) are_congruent_mod 10

    proof

      let n be triangular number;

      consider k be Nat such that

       A1: n = ( Triangle k) by Def2;

      

       A2: (4 * 5) = 20;

      

       A3: n = ((k * (k + 1)) / 2) by A1, Th19;

      assume (n,2) are_congruent_mod 10;

      then ((((k * (k + 1)) / 2) * 2),(2 * 2)) are_congruent_mod (10 * 2) by A3, INT_4: 10;

      then ((k * (k + 1)),4) are_congruent_mod 5 by A2, INT_1: 20;

      then (4,((k * k) + k)) are_congruent_mod 5 by INT_1: 14;

      hence thesis by Th6, INT_1: 14;

    end;

    theorem :: NUMPOLY1:25

    

     Th25: for n be triangular number holds not (n,4) are_congruent_mod 10

    proof

      let n be triangular number;

      consider k be Nat such that

       A1: n = ( Triangle k) by Def2;

      

       A2: (4 * 5) = 20;

      

       A3: n = ((k * (k + 1)) / 2) by A1, Th19;

      assume (n,4) are_congruent_mod 10;

      then ((((k * (k + 1)) / 2) * 2),(4 * 2)) are_congruent_mod (10 * 2) by A3, INT_4: 10;

      then ((k * (k + 1)),8) are_congruent_mod 5 by A2, INT_1: 20;

      then (8,(k * (k + 1))) are_congruent_mod 5 by INT_1: 14;

      then ((8 - 5),(k * (k + 1))) are_congruent_mod 5 by INT_1: 22;

      then (3,((k * k) + k)) are_congruent_mod 5;

      hence thesis by Th7, INT_1: 14;

    end;

    theorem :: NUMPOLY1:26

    for n be triangular number holds (n, 0 ) are_congruent_mod 10 or (n,1) are_congruent_mod 10 or (n,3) are_congruent_mod 10 or (n,5) are_congruent_mod 10 or (n,6) are_congruent_mod 10 or (n,8) are_congruent_mod 10

    proof

      let n be triangular number;

      (n, 0 ) are_congruent_mod 10 or ... or (n,9) are_congruent_mod 10 by Th9;

      per cases ;

        suppose (n, 0 ) are_congruent_mod 10;

        hence thesis;

      end;

        suppose (n,1) are_congruent_mod 10;

        hence thesis;

      end;

        suppose (n,2) are_congruent_mod 10;

        hence thesis by Th24;

      end;

        suppose (n,3) are_congruent_mod 10;

        hence thesis;

      end;

        suppose (n,4) are_congruent_mod 10;

        hence thesis by Th25;

      end;

        suppose (n,5) are_congruent_mod 10;

        hence thesis;

      end;

        suppose (n,6) are_congruent_mod 10;

        hence thesis;

      end;

        suppose (n,7) are_congruent_mod 10;

        hence thesis by Th22;

      end;

        suppose (n,8) are_congruent_mod 10;

        hence thesis;

      end;

        suppose (n,9) are_congruent_mod 10;

        hence thesis by Th23;

      end;

    end;

    begin

    definition

      let s,n be natural Number;

      :: NUMPOLY1:def3

      func Polygon (s,n) -> Integer equals ((((n ^2 ) * (s - 2)) - (n * (s - 4))) / 2);

      coherence

      proof

        ((n * (n - 1)) * (s - 2)) is even;

        then (((n * (s - 2)) * (n - 1)) / 2) is Integer by Th2;

        then ((((n * (s - 2)) * (n - 1)) / 2) + n) is Integer;

        hence thesis;

      end;

    end

    theorem :: NUMPOLY1:27

    

     Th27: s >= 2 implies ( Polygon (s,n)) is natural

    proof

      assume s >= 2;

      then

       A1: (s - 2) >= (2 - 2) by XREAL_1: 9;

      per cases ;

        suppose n = 0 ;

        hence thesis;

      end;

        suppose n > 0 ;

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

        then (n - 1) >= (1 - 1) by XREAL_1: 9;

        then ((((n * (s - 2)) * (n - 1)) / 2) + n) >= 0 by A1;

        hence ( Polygon (s,n)) in NAT by INT_1: 3;

      end;

    end;

    theorem :: NUMPOLY1:28

    ( Polygon (s,n)) = ((((n * (s - 2)) * (n - 1)) / 2) + n);

    definition

      let s be Nat;

      let x be object;

      :: NUMPOLY1:def4

      attr x is s -gonal means

      : Def4: ex n be Nat st x = ( Polygon (s,n));

    end

    definition

      let x be object;

      :: NUMPOLY1:def5

      attr x is polygonal means ex s be Nat st x is s -gonal;

    end

    theorem :: NUMPOLY1:29

    ( Polygon (s,1)) = 1;

    theorem :: NUMPOLY1:30

    ( Polygon (s,2)) = s;

    registration

      let s be Nat;

      cluster s -gonal for number;

      existence

      proof

        reconsider a = ( Polygon (s,2)) as number;

        take a;

        thus thesis;

      end;

    end

    registration

      let s be non zero Nat;

      cluster non zeros -gonal for number;

      existence

      proof

        reconsider a = ( Polygon (s,2)) as number;

        take a;

        thus thesis;

      end;

    end

    registration

      let s be Nat;

      cluster s -gonal -> real for number;

      coherence ;

    end

    registration

      let s be non trivial Nat;

      cluster s -gonal -> natural for number;

      coherence by EC_PF_2:def 1, Th27;

    end

    theorem :: NUMPOLY1:31

    (( Polygon (s,(n + 1))) - ( Polygon (s,n))) = (((s - 2) * n) + 1);

    definition

      let s be Nat, x be s -gonal number;

      :: NUMPOLY1:def6

      func IndexPoly (s,x) -> Real equals (((( sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2 ))) + s) - 4) / ((2 * s) - 4));

      coherence ;

    end

    theorem :: NUMPOLY1:32

    for s be non zero Nat, x be non zeros -gonal number st x = ( Polygon (s,n)) holds ((((8 * s) - 16) * x) + ((s - 4) ^2 )) = ((((2 * n) * (s - 2)) - (s - 4)) ^2 );

    theorem :: NUMPOLY1:33

    for s be non zero Nat, x be non zeros -gonal number st s >= 4 holds ((((8 * s) - 16) * x) + ((s - 4) ^2 )) is square

    proof

      let s be non zero Nat, x be non zeros -gonal number;

      assume

       A1: s >= 4;

      consider n be Nat such that

       A2: x = ( Polygon (s,n)) by Def4;

      

       A3: ((((8 * s) - 16) * x) + ((s - 4) ^2 )) = ((((2 * n) * (s - 2)) - (s - 4)) ^2 ) by A2;

      n <> 0 by A2;

      then

       A4: (2 * n) >= 1 by Th1;

      s >= ( 0 + 4) by A1;

      then

       A5: (s - 4) >= 0 by XREAL_1: 19;

      (s - 2) >= (s - 4) by XREAL_1: 13;

      then ((2 * n) * (s - 2)) >= ( 0 + (1 * (s - 4))) by A4, A5, XREAL_1: 66;

      then (((2 * n) * (s - 2)) - (s - 4)) in NAT by INT_1: 3, XREAL_1: 19;

      hence thesis by A3;

    end;

    theorem :: NUMPOLY1:34

    

     Th34: for s be non zero Nat, x be non zeros -gonal number st s >= 4 holds ( IndexPoly (s,x)) in NAT

    proof

      let s be non zero Nat, x be non zeros -gonal number;

      assume

       A1: s >= 4;

      consider n be Nat such that

       A2: x = ( Polygon (s,n)) by Def4;

      

       A3: ((((8 * s) - 16) * x) + ((s - 4) ^2 )) = ((((2 * n) * (s - 2)) - (s - 4)) ^2 ) by A2;

      

       A4: (s - 2) <> 0 by A1;

      n <> 0 by A2;

      then

       A5: (2 * n) >= 1 by Th1;

      s >= ( 0 + 4) by A1;

      then

       A6: (s - 4) >= 0 by XREAL_1: 19;

      (s - 2) >= (s - 4) by XREAL_1: 13;

      then

       A7: ((2 * n) * (s - 2)) >= ( 0 + (1 * (s - 4))) by A5, A6, XREAL_1: 66;

      ( IndexPoly (s,x)) = ((((((2 * n) * (s - 2)) - (s - 4)) + s) - 4) / ((2 * s) - 4)) by SQUARE_1: 22, A7, A3, XREAL_1: 19

      .= (((2 * n) * (s - 2)) / (2 * (s - 2)))

      .= ((2 * n) / 2) by A4, XCMPLX_1: 91

      .= n;

      hence thesis by ORDINAL1:def 12;

    end;

    theorem :: NUMPOLY1:35

    

     Th35: for s be non trivial Nat, x be s -gonal number holds 0 <= ((((8 * s) - 16) * x) + ((s - 4) ^2 ))

    proof

      let s be non trivial Nat;

      let x be s -gonal number;

      (s - 2) >= (2 - 2) by XREAL_1: 9, NAT_2: 29;

      then (8 * (s - 2)) >= 0 ;

      hence thesis;

    end;

    theorem :: NUMPOLY1:36

    

     Th36: for n be odd Nat st s >= 2 holds n divides ( Polygon (s,n))

    proof

      let n be odd Nat;

      assume

       A1: s >= 2;

      

       A2: ( Polygon (s,n)) = ((((n * (s - 2)) * (n - 1)) / 2) + n);

      

       A3: (s - 0 ) >= 2 by A1;

      then (s - 2) >= 0 by XREAL_1: 11;

      then

       A4: ((n * (s - 2)) * (n - 1)) in NAT by INT_1: 3;

      reconsider k = (((n * (s - 2)) * (n - 1)) / 2) as Nat by A4;

      

       A5: (s - 2) in NAT by INT_1: 3, A3, XREAL_1: 11;

      k = (n * ((s - 2) * ((n - 1) / 2)));

      then n divides k by NAT_D:def 3, A5;

      hence thesis by A2, NAT_D: 8;

    end;

    begin

    ::$Notion-Name

    definition

      let s,n be Nat;

      :: NUMPOLY1:def7

      func CenterPolygon (s,n) -> Integer equals ((((s * n) / 2) * (n - 1)) + 1);

      coherence

      proof

        ((n * (n - 1)) / 2) is Integer by Th2;

        then ((s * ((n / 2) * (n - 1))) + 1) is Integer;

        hence thesis;

      end;

    end

    registration

      let s be Nat;

      let n be non zero Nat;

      cluster ( CenterPolygon (s,n)) -> natural;

      coherence

      proof

        (n - 0 ) >= 1 by NAT_1: 14;

        then (n - 1) >= 0 by XREAL_1: 11;

        hence thesis by INT_1: 3;

      end;

    end

    theorem :: NUMPOLY1:37

    ( CenterPolygon ( 0 ,n)) = 1;

    theorem :: NUMPOLY1:38

    ( CenterPolygon (s, 0 )) = 1;

    theorem :: NUMPOLY1:39

    ( CenterPolygon (s,n)) = ((s * ( Triangle (n -' 1))) + 1)

    proof

      ( CenterPolygon (s,n)) = ((s * ((n * (n - 1)) / 2)) + 1)

      .= ((s * ( Triangle (n -' 1))) + 1) by Th21;

      hence thesis;

    end;

    begin

    theorem :: NUMPOLY1:40

    

     Th40: ( Triangle n) = ( Polygon (3,n))

    proof

      ( Polygon (3,n)) = ((n * (n + 1)) / 2);

      hence thesis by Th19;

    end;

    theorem :: NUMPOLY1:41

    

     Th41: for n be odd Nat holds n divides ( Triangle n)

    proof

      let n be odd Nat;

      n divides ( Polygon (3,n)) by Th36;

      hence thesis by Th40;

    end;

    theorem :: NUMPOLY1:42

    

     Th42: ( Triangle n) <= ( Triangle (n + 1))

    proof

      ( Triangle (n + 1)) = (( Triangle n) + (n + 1)) by Th10;

      hence thesis by NAT_1: 16;

    end;

    theorem :: NUMPOLY1:43

    for k be Nat st k <= n holds ( Triangle k) <= ( Triangle n)

    proof

      let k be Nat;

      assume k <= n;

      then

      consider i be Nat such that

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

      defpred P[ Nat] means for n be Nat holds ( Triangle n) <= ( Triangle (n + $1));

      

       A2: P[ 0 ];

      

       A3: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A4: P[k];

        let n be Nat;

        

         A5: ( Triangle n) <= ( Triangle (n + k)) by A4;

        ( Triangle (n + k)) <= ( Triangle ((n + k) + 1)) by Th42;

        hence thesis by A5, XXREAL_0: 2;

      end;

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

      hence thesis by A1;

    end;

    theorem :: NUMPOLY1:44

    

     Th44: n <= ( Triangle n)

    proof

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

      

       A1: P[ 0 ];

      

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

      proof

        let k be Nat;

        assume P[k];

        ( Triangle (k + 1)) = (( Triangle k) + (k + 1)) by Th10;

        hence thesis by NAT_1: 11;

      end;

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

      hence thesis;

    end;

    theorem :: NUMPOLY1:45

    

     Th45: for n be non trivial Nat holds n < ( Triangle n)

    proof

      let n be non trivial Nat;

      defpred P[ Nat] means $1 < ( Triangle $1);

      

       A1: P[2] by Th12;

      

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

      proof

        let k be non trivial Nat;

        assume P[k];

        ( Triangle (k + 1)) = (( Triangle k) + (k + 1)) by Th10;

        hence thesis by NAT_1: 16;

      end;

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

      hence thesis;

    end;

    theorem :: NUMPOLY1:46

    

     Th46: n <> 2 implies ( Triangle n) is non prime

    proof

      assume

       A1: n <> 2;

      assume

       A2: ( Triangle n) is prime;

      then

       A3: n <> 1 by Th11, INT_2:def 4;

      n <> 0 by A2, INT_2:def 4;

      then

       A4: n is non trivial by NAT_2:def 1, A3;

      per cases ;

        suppose n is odd;

        then n = 1 or n = ( Triangle n) by INT_2:def 4, A2, Th41;

        hence thesis by Th45, A4, Th11;

      end;

        suppose n is even;

        then

        consider k be Nat such that

         A5: n = (2 * k) by ABIAN:def 2;

        

         A6: k <> 0 by A2, INT_2:def 4, A5;

        

         A7: ( Triangle n) = ((n * (n + 1)) / 2) by Th19

        .= (k * (n + 1)) by A5;

        then k divides ( Triangle n) by NAT_D:def 3;

        per cases by INT_2:def 4, A2;

          suppose k = 1;

          hence thesis by A1, A5;

        end;

          suppose

           A8: k = ( Triangle n);

          1 = (k / k) by A6, XCMPLX_1: 60

          .= (n + 1) by A6, XCMPLX_1: 89, A7, A8;

          then n = 0 ;

          hence thesis by INT_2:def 4, A2;

        end;

      end;

    end;

    registration

      let n be 3 _or_greater Nat;

      cluster ( Triangle n) -> non prime;

      coherence

      proof

        n <> 2 by EC_PF_2:def 1;

        hence thesis by Th46;

      end;

    end

    registration

      cluster triangular -> non prime for 4 _or_greater Nat;

      coherence

      proof

        let n be 4 _or_greater Nat;

        assume n is triangular;

        then

        consider k be Nat such that

         A1: n = ( Triangle k);

        k <> 2 by A1, EC_PF_2:def 1, Th12;

        hence thesis by A1, Th46;

      end;

    end

    registration

      let s be 4 _or_greater non zero Nat, x be non zeros -gonal number;

      cluster ( IndexPoly (s,x)) -> natural;

      coherence by Th34, EC_PF_2:def 1;

    end

    theorem :: NUMPOLY1:47

    for s be 4 _or_greater Nat, x be non zeros -gonal number st s <> 2 holds ( Polygon (s,( IndexPoly (s,x)))) = x

    proof

      let s be 4 _or_greater Nat, x be non zeros -gonal number;

      assume s <> 2;

      then

       A1: (s - 2) <> 0 ;

      

       A2: 0 <= ((((8 * s) - 16) * x) + ((s - 4) ^2 )) by Th35;

      set qq = ( sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2 )));

      set w = ( IndexPoly (s,x));

      

       A3: ((w ^2 ) * (s - 2)) = (((((qq + s) - 4) ^2 ) / (((2 * s) - 4) ^2 )) * (s - 2)) by XCMPLX_1: 76

      .= (((((qq + s) - 4) ^2 ) / ((4 * (s - 2)) * (s - 2))) * (s - 2))

      .= ((((qq ^2 ) + ((s - 4) ^2 )) + ((2 * qq) * (s - 4))) / (4 * (s - 2))) by XCMPLX_1: 92, A1;

      

       A4: (w * (s - 4)) = ((((qq + s) - 4) * (s - 4)) / ((2 * s) - 4)) by XCMPLX_1: 74

      .= ((2 * ((qq * (s - 4)) + ((s - 4) ^2 ))) / (2 * (2 * (s - 2)))) by XCMPLX_1: 91

      .= ((2 * ((qq * (s - 4)) + ((s - 4) ^2 ))) / (4 * (s - 2)));

      

       A5: (qq ^2 ) = ((((8 * s) - 16) * x) + ((s - 4) ^2 )) by SQUARE_1:def 2, A2;

      ( Polygon (s,w)) = ((((((qq ^2 ) + ((s - 4) ^2 )) + ((2 * qq) * (s - 4))) - (2 * ((qq * (s - 4)) + ((s - 4) ^2 )))) / (4 * (s - 2))) / 2) by XCMPLX_1: 120, A3, A4

      .= (((((qq ^2 ) + ((s - 4) ^2 )) + ((2 * qq) * (s - 4))) - (2 * ((qq * (s - 4)) + ((s - 4) ^2 )))) / ((4 * (s - 2)) * 2)) by XCMPLX_1: 78

      .= x by A1, XCMPLX_1: 89, A5;

      hence thesis;

    end;

    theorem :: NUMPOLY1:48

    36 is square triangular

    proof

      

       A1: (6 ^2 ) = 36;

      ( Triangle 8) = (((8 + 1) * 8) / 2) by Th19

      .= 36;

      hence thesis by A1;

    end;

    registration

      let n be Nat;

      cluster ( Polygon (3,n)) -> natural;

      coherence

      proof

        ( Triangle n) = ( Polygon (3,n)) by Th40;

        hence thesis;

      end;

    end

    registration

      let n be Nat;

      cluster ( Polygon (3,n)) -> triangular;

      coherence

      proof

        ( Triangle n) = ( Polygon (3,n)) by Th40;

        hence thesis;

      end;

    end

    theorem :: NUMPOLY1:49

    

     Th49: ( Polygon (s,n)) = (((s - 2) * ( Triangle (n -' 1))) + n)

    proof

      ( Polygon (s,n)) = (((s - 2) * ((n * (n - 1)) / 2)) + n)

      .= (((s - 2) * ( Triangle (n -' 1))) + n) by Th21;

      hence thesis;

    end;

    theorem :: NUMPOLY1:50

    ( Polygon (s,n)) = (((s - 3) * ( Triangle (n -' 1))) + ( Triangle n))

    proof

      (((s - 3) * ( Triangle (n -' 1))) + ( Triangle n)) = (((s - 3) * ((n * (n - 1)) / 2)) + ( Triangle n)) by Th21

      .= (((s - 3) * ((n * (n - 1)) / 2)) + ((n * (n + 1)) / 2)) by Th19;

      hence thesis;

    end;

    theorem :: NUMPOLY1:51

    ( Polygon ( 0 ,n)) = (n * (2 - n));

    theorem :: NUMPOLY1:52

    ( Polygon (1,n)) = ((n * (3 - n)) / 2);

    theorem :: NUMPOLY1:53

    ( Polygon (2,n)) = n;

    registration

      let s be non trivial Nat, n be Nat;

      cluster ( Polygon (s,n)) -> natural;

      coherence

      proof

        s >= ( 0 + 2) by NAT_2: 29;

        then

         A1: (s - 2) >= 0 by XREAL_1: 19;

        ( Polygon (s,n)) = (((s - 2) * ( Triangle (n -' 1))) + n) by Th49;

        hence thesis by INT_1: 3, A1;

      end;

    end

    registration

      let n be Nat;

      cluster ( Polygon (4,n)) -> square;

      coherence ;

    end

    registration

      cluster 3 -gonal -> triangular for Nat;

      coherence ;

      cluster triangular -> 3 -gonal for Nat;

      coherence

      proof

        let x be Nat;

        assume x is triangular;

        then

        consider n be Nat such that

         A1: x = ( Triangle n);

        x = ( Polygon (3,n)) by A1, Th40;

        hence thesis;

      end;

      cluster 4 -gonal -> square for Nat;

      coherence ;

      cluster square -> 4 -gonal for Nat;

      coherence

      proof

        let x be Nat;

        assume x is square;

        then

        consider n be Nat such that

         A2: x = (n ^2 ) by PYTHTRIP:def 3;

        x = ( Polygon (4,n)) by A2;

        hence thesis;

      end;

    end

    theorem :: NUMPOLY1:54

    (( Triangle (n -' 1)) + ( Triangle n)) = (n ^2 )

    proof

      per cases ;

        suppose n <> 0 ;

        then

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

        ( Triangle (n -' 1)) = (((n - 1) * ((n - 1) + 1)) / 2) by Th19, A1;

        

        then (( Triangle (n -' 1)) + ( Triangle n)) = ((((n - 1) * ((n + 1) - 1)) / 2) + ((n * (n + 1)) / 2)) by Th19

        .= (n ^2 );

        hence thesis;

      end;

        suppose

         A2: n = 0 ;

        

        then (( Triangle (n -' 1)) + ( Triangle n)) = (( Triangle ( 0 -' 1)) + ( Triangle 0 ))

        .= (n ^2 ) by A2, XREAL_0:def 2, Lm3;

        hence thesis;

      end;

    end;

    theorem :: NUMPOLY1:55

    

     Th55: (( Triangle n) + ( Triangle (n + 1))) = ((n + 1) ^2 )

    proof

      ( Triangle n) = ((n * (n + 1)) / 2) by Th19;

      

      then (( Triangle n) + ( Triangle (n + 1))) = (((n * (n + 1)) / 2) + (((n + 1) * ((n + 1) + 1)) / 2)) by Th19

      .= ((n + 1) ^2 );

      hence thesis;

    end;

    registration

      let n be Nat;

      cluster (( Triangle n) + ( Triangle (n + 1))) -> square;

      coherence

      proof

        (( Triangle n) + ( Triangle (n + 1))) = ((n + 1) ^2 ) by Th55;

        hence thesis;

      end;

    end

    theorem :: NUMPOLY1:56

    for n be non trivial Nat holds ((1 / 3) * ( Triangle ((3 * n) -' 1))) = ((n * ((3 * n) - 1)) / 2)

    proof

      let n be non trivial Nat;

      

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

      ( Triangle ((3 * n) -' 1)) = ((((3 * n) - 1) * (((3 * n) - 1) + 1)) / 2) by A1, Th19;

      hence thesis;

    end;

    theorem :: NUMPOLY1:57

    for n be non zero Nat holds ( Triangle ((2 * n) -' 1)) = ((n * ((4 * n) - 2)) / 2)

    proof

      let n be non zero Nat;

      

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

      ( Triangle ((2 * n) -' 1)) = ((((2 * n) - 1) * (((2 * n) - 1) + 1)) / 2) by A1, Th19;

      hence thesis;

    end;

    definition

      let n,k be Nat;

      :: NUMPOLY1:def8

      func NPower (n,k) -> FinSequence of REAL means

      : Def8: ( dom it ) = ( Seg k) & for i be Nat st i in ( dom it ) holds (it . i) = (i |^ n);

      existence

      proof

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

        deffunc f( Nat) = ( In (($1 |^ n), REAL ));

        consider e be FinSequence of REAL such that

         A1: ( len e) = k1 & for i be Nat st i in ( dom e) holds (e . i) = f(i) from FINSEQ_2:sch 1;

        take e;

        thus ( dom e) = ( Seg k) by FINSEQ_1:def 3, A1;

        let i be Nat;

        assume

         A2: i in ( dom e);

         f(i) = (i |^ n);

        hence thesis by A2, A1;

      end;

      uniqueness

      proof

        deffunc f( Nat) = ($1 |^ n);

        let e1,e2 be FinSequence of REAL such that

         A3: ( dom e1) = ( Seg k) & for i be Nat st i in ( dom e1) holds (e1 . i) = f(i) and

         A4: ( dom e2) = ( Seg k) & for i be Nat st i in ( dom e2) holds (e2 . i) = f(i);

        for i be Nat st i in ( dom e1) holds (e1 . i) = (e2 . i)

        proof

          let i be Nat;

          assume

           A5: i in ( dom e1);

          

          hence (e1 . i) = f(i) by A3

          .= (e2 . i) by A5, A3, A4;

        end;

        hence thesis by A3, A4, FINSEQ_1: 13;

      end;

    end

    theorem :: NUMPOLY1:58

    

     Th58: for k be Nat holds ( NPower (n,(k + 1))) = (( NPower (n,k)) ^ <*((k + 1) |^ n)*>)

    proof

      let k be Nat;

      

       A1: ( dom ( NPower (n,(k + 1)))) = ( dom (( NPower (n,k)) ^ <*((k + 1) |^ n)*>))

      proof

        ( Seg ( len ( NPower (n,k)))) = ( dom ( NPower (n,k))) by FINSEQ_1:def 3

        .= ( Seg k) by Def8;

        then

         A2: ( len ( NPower (n,k))) = k by FINSEQ_1: 6;

        

         A3: ( len <*((k + 1) |^ n)*>) = 1 by FINSEQ_1: 40;

        ( dom (( NPower (n,k)) ^ <*((k + 1) |^ n)*>)) = ( Seg (( len ( NPower (n,k))) + ( len <*((k + 1) |^ n)*>))) by FINSEQ_1:def 7

        .= ( dom ( NPower (n,(k + 1)))) by Def8, A3, A2;

        hence thesis;

      end;

      for l be Nat st l in ( dom ( NPower (n,(k + 1)))) holds (( NPower (n,(k + 1))) . l) = ((( NPower (n,k)) ^ <*((k + 1) |^ n)*>) . l)

      proof

        let l be Nat;

        assume

         A4: l in ( dom ( NPower (n,(k + 1))));

        then l in ( Seg (k + 1)) by Def8;

        then

         A5: 1 <= l & l <= (k + 1) by FINSEQ_1: 1;

        set NP = ((( NPower (n,k)) ^ <*((k + 1) |^ n)*>) . l);

        ((( NPower (n,k)) ^ <*((k + 1) |^ n)*>) . l) = (l |^ n)

        proof

          per cases by A5, NAT_1: 8;

            suppose l <= k;

            then l in ( Seg k) by A5, FINSEQ_1: 1;

            then

             A6: l in ( dom ( NPower (n,k))) by Def8;

            

            then NP = (( NPower (n,k)) . l) by FINSEQ_1:def 7

            .= (l |^ n) by Def8, A6;

            hence thesis;

          end;

            suppose

             A7: l = (k + 1);

            ( Seg k) = ( dom ( NPower (n,k))) by Def8

            .= ( Seg ( len ( NPower (n,k)))) by FINSEQ_1:def 3;

            then k = ( len ( NPower (n,k))) by FINSEQ_1: 6;

            hence thesis by A7, FINSEQ_1: 42;

          end;

        end;

        hence thesis by Def8, A4;

      end;

      hence thesis by A1, FINSEQ_1: 13;

    end;

    registration

      let n be Nat;

      reduce ( Sum ( NPower (n, 0 ))) to 0 ;

      reducibility

      proof

        ( dom ( NPower (n, 0 ))) = ( Seg 0 ) by Def8

        .= {} ;

        hence thesis by RVSUM_1: 72, RELAT_1: 41;

      end;

    end

    theorem :: NUMPOLY1:59

    (( Triangle n) |^ 2) = ( Sum ( NPower (3,n)))

    proof

      defpred P[ Nat] means (( Triangle $1) |^ 2) = ( Sum ( NPower (3,$1)));

      

       A1: P[ 0 ]

      proof

        

        thus (( Triangle 0 ) |^ 2) = ( 0 * 0 ) by NEWTON: 81

        .= ( Sum ( NPower (3, 0 )));

      end;

      

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

      proof

        let k be Nat such that

         A3: P[k];

        reconsider k1 = (k + 1) as Element of REAL by XREAL_0:def 1;

        (( Triangle (k + 1)) |^ 2) = ((((k + 1) * ((k + 1) + 1)) / 2) |^ 2) by Th19

        .= ((((k + 1) * (k + 2)) / 2) * (((k + 1) * (k + 2)) / 2)) by NEWTON: 81

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

        .= (((((k + 1) |^ 2) * (k + 2)) * (k + 2)) / (2 * 2)) by NEWTON: 81

        .= ((((k + 1) |^ 2) * (((k * k) + (4 * k)) + 4)) / (2 * 2))

        .= ((((k + 1) |^ 2) * (((k |^ 2) + (4 * k)) + 4)) / (2 * 2)) by NEWTON: 81

        .= ((((((k + 1) |^ 2) * (k |^ 2)) / 4) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4))

        .= ((((((k + 1) * k) |^ 2) / (2 * 2)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4)) by NEWTON: 7

        .= ((((((k + 1) * k) |^ 2) / (2 |^ 2)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4)) by NEWTON: 81

        .= ((((((k + 1) |^ 2) * (k |^ 2)) / (2 |^ 2)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4)) by NEWTON: 7

        .= ((((((k + 1) * (k + 1)) * (k |^ 2)) / (2 |^ 2)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4)) by NEWTON: 81

        .= ((((((k + 1) * (k + 1)) * (k * k)) / (2 |^ 2)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4)) by NEWTON: 81

        .= (((((((k + 1) * (k + 1)) * k) * k) / (2 * 2)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4)) by NEWTON: 81

        .= ((((((k + 1) * k) / 2) * (((k + 1) * k) / 2)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4))

        .= (((( Triangle k) * (((k + 1) * k) / 2)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4)) by Th19

        .= (((( Triangle k) * ( Triangle k)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4)) by Th19

        .= (((( Triangle k) |^ 2) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4)) by NEWTON: 81

        .= (( Sum ( NPower (3,k))) + (((k + 1) |^ 2) * (k + 1))) by A3

        .= (( Sum ( NPower (3,k))) + (((k + 1) * (k + 1)) * (k + 1))) by NEWTON: 81

        .= (( Sum ( NPower (3,k))) + ((k + 1) |^ 3)) by POLYEQ_3: 27

        .= ( Sum (( NPower (3,k)) ^ <*(k1 |^ 3)*>)) by RVSUM_1: 74

        .= ( Sum ( NPower (3,(k + 1)))) by Th58;

        hence thesis;

      end;

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

      hence thesis;

    end;

    theorem :: NUMPOLY1:60

    for n be non trivial Nat holds (( Triangle n) + (( Triangle (n -' 1)) * ( Triangle (n + 1)))) = (( Triangle n) |^ 2)

    proof

      let n be non trivial Nat;

      

       A1: ( Triangle n) = ((n * (n + 1)) / 2) by Th19;

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

      then

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

      

       A3: ( Triangle (n -' 1)) = (((n -' 1) * ((n -' 1) + 1)) / 2) by Th19

      .= (((n - 1) * n) / 2) by A2;

      ( Triangle (n + 1)) = (((n + 1) * ((n + 1) + 1)) / 2) by Th19

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

      

      then (( Triangle n) + (( Triangle (n -' 1)) * ( Triangle (n + 1)))) = (( Triangle n) * ( Triangle n)) by A1, A3

      .= (( Triangle n) |^ 2) by NEWTON: 81;

      hence thesis;

    end;

    theorem :: NUMPOLY1:61

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

    proof

      

       A1: ( Triangle (n + 1)) = (((n + 1) * ((n + 1) + 1)) / 2) by Th19

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

      

       A2: ((n + 1) |^ 2) = ((n + 1) * (n + 1)) by NEWTON: 81;

      ((( Triangle n) |^ 2) + (( Triangle (n + 1)) |^ 2)) = ((((n * (n + 1)) / 2) |^ 2) + (( Triangle (n + 1)) |^ 2)) by Th19

      .= ((((n * (n + 1)) / 2) * ((n * (n + 1)) / 2)) + ((((n + 1) * (n + 2)) / 2) |^ 2)) by NEWTON: 81, A1

      .= ((((n * (n + 1)) / 2) * ((n * (n + 1)) / 2)) + ((((n + 1) * (n + 2)) / 2) * (((n + 1) * (n + 2)) / 2))) by NEWTON: 81

      .= ((((n + 1) |^ 2) * (((n + 1) |^ 2) + 1)) / 2) by A2

      .= ( Triangle ((n + 1) |^ 2)) by Th19;

      hence thesis;

    end;

    theorem :: NUMPOLY1:62

    ((( Triangle (n + 1)) |^ 2) - (( Triangle n) |^ 2)) = ((n + 1) |^ 3)

    proof

      

       A1: ( Triangle (n + 1)) = (((n + 1) * ((n + 1) + 1)) / 2) by Th19

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

      

       A2: ((n + 1) |^ 3) = (((n + 1) * (n + 1)) * (n + 1)) by POLYEQ_3: 27

      .= (((((n * n) * n) + ((3 * n) * n)) + (3 * n)) + 1);

      

       A3: ((n + 1) * (n + 1)) = ((n + 1) |^ 2) by NEWTON: 81;

      ((( Triangle (n + 1)) |^ 2) - (( Triangle n) |^ 2)) = (((((n + 1) * (n + 2)) / 2) |^ 2) - (((n * (n + 1)) / 2) |^ 2)) by Th19, A1

      .= (((((n + 1) * (n + 2)) / 2) * (((n + 1) * (n + 2)) / 2)) - (((n * (n + 1)) / 2) |^ 2)) by NEWTON: 81

      .= ((((((n + 1) * (n + 1)) * (n + 2)) * (n + 2)) / 4) - (((n * (n + 1)) / 2) |^ 2))

      .= ((((((n + 1) |^ 2) * (n + 2)) * (n + 2)) / 4) - (((n * (n + 1)) / 2) |^ 2)) by NEWTON: 81

      .= ((((((n + 1) |^ 2) * (n + 2)) * (n + 2)) / 4) - (((n * (n + 1)) / 2) * ((n * (n + 1)) / 2))) by NEWTON: 81

      .= ((((((n + 1) |^ 2) * (n + 2)) * (n + 2)) / 4) - ((((n * n) * (n + 1)) * (n + 1)) / 4))

      .= ((((((n + 1) |^ 2) * (n + 2)) * (n + 2)) / 4) - ((((n |^ 2) * (n + 1)) * (n + 1)) / 4)) by NEWTON: 81

      .= ((((n + 1) |^ 2) * (((((n * n) + (2 * n)) + (2 * n)) + 4) - (n |^ 2))) / 4) by A3

      .= ((((n + 1) |^ 2) * (((((n |^ 2) + (2 * n)) + (2 * n)) + 4) - (n |^ 2))) / 4) by NEWTON: 81

      .= (((n + 1) |^ 2) * (n + 1))

      .= (((n + 1) * (n + 1)) * (n + 1)) by NEWTON: 81

      .= ((n + 1) |^ 3) by A2;

      hence thesis;

    end;

    theorem :: NUMPOLY1:63

    for n be non zero Nat holds ((3 * ( Triangle n)) + ( Triangle (n -' 1))) = ( Triangle (2 * n))

    proof

      let n be non zero Nat;

      

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

      

       A2: ( Triangle (n -' 1)) = (((n - 1) * ((n - 1) + 1)) / 2) by A1, Th19;

      ((3 * ( Triangle n)) + ( Triangle (n -' 1))) = ((3 * ((n * (n + 1)) / 2)) + (((n - 1) * ((n - 1) + 1)) / 2)) by A2, Th19

      .= (((2 * n) * ((2 * n) + 1)) / 2)

      .= ( Triangle (2 * n)) by Th19;

      hence thesis;

    end;

    theorem :: NUMPOLY1:64

    ((3 * ( Triangle n)) + ( Triangle (n + 1))) = ( Triangle ((2 * n) + 1))

    proof

      

       A1: ( Triangle n) = ((n * (n + 1)) / 2) by Th19;

      

       A2: ( Triangle (n + 1)) = (((n + 1) * ((n + 1) + 1)) / 2) by Th19

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

      ( Triangle ((2 * n) + 1)) = ((((2 * n) + 1) * (((2 * n) + 1) + 1)) / 2) by Th19

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

      hence thesis by A1, A2;

    end;

    theorem :: NUMPOLY1:65

    for n be non zero Nat holds ((( Triangle (n -' 1)) + (6 * ( Triangle n))) + ( Triangle (n + 1))) = ((8 * ( Triangle n)) + 1)

    proof

      let n be non zero Nat;

      

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

      

       A2: ( Triangle (n -' 1)) = (((n - 1) * ((n - 1) + 1)) / 2) by A1, Th19;

      

       A3: ( Triangle n) = ((n * (n + 1)) / 2) by Th19;

      ( Triangle (n + 1)) = (((n + 1) * ((n + 1) + 1)) / 2) by Th19

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

      hence thesis by A3, A2;

    end;

    theorem :: NUMPOLY1:66

    for n be non zero Nat holds (( Triangle n) + ( Triangle (n -' 1))) = ((((1 + (2 * n)) - 1) * n) / 2)

    proof

      let n be non zero Nat;

      

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

      

       A2: ( Triangle (n -' 1)) = (((n - 1) * ((n - 1) + 1)) / 2) by A1, Th19;

      (( Triangle n) + ( Triangle (n -' 1))) = (((n * (n + 1)) / 2) + ( Triangle (n -' 1))) by Th19

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

      hence thesis;

    end;

    theorem :: NUMPOLY1:67

    

     Th67: (1 + (9 * ( Triangle n))) = ( Triangle ((3 * n) + 1))

    proof

      

       A1: ( Triangle n) = ((n * (n + 1)) / 2) by Th19;

      ( Triangle ((3 * n) + 1)) = ((((3 * n) + 1) * (((3 * n) + 1) + 1)) / 2) by Th19

      .= (1 + (9 * ( Triangle n))) by A1;

      hence thesis;

    end;

    theorem :: NUMPOLY1:68

    for m be Nat holds ( Triangle (n + m)) = ((( Triangle n) + ( Triangle m)) + (n * m))

    proof

      let m be Nat;

      ( Triangle (n + m)) = (((n + m) * ((n + m) + 1)) / 2) by Th19

      .= ((((n * (n + 1)) / 2) + ((m * (m + 1)) / 2)) + (n * m))

      .= ((( Triangle n) + ((m * (m + 1)) / 2)) + (n * m)) by Th19

      .= ((( Triangle n) + ( Triangle m)) + (n * m)) by Th19;

      hence thesis;

    end;

    theorem :: NUMPOLY1:69

    for n,m be non trivial Nat holds ((( Triangle n) * ( Triangle m)) + (( Triangle (n -' 1)) * ( Triangle (m -' 1)))) = ( Triangle (n * m))

    proof

      let n,m be non trivial Nat;

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

      then

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

      ( 0 + 1) <= m by NAT_1: 13;

      then

       A2: (m -' 1) = (m - 1) by XREAL_1: 233;

      

       A3: ( Triangle (n -' 1)) = (((n - 1) * ((n - 1) + 1)) / 2) by A1, Th19;

      

       A4: ( Triangle (m -' 1)) = (((m - 1) * ((m - 1) + 1)) / 2) by A2, Th19;

      

       A5: ( Triangle (n * m)) = (((n * m) * ((n * m) + 1)) / 2) by Th19;

      ((( Triangle n) * ( Triangle m)) + (( Triangle (n -' 1)) * ( Triangle (m -' 1)))) = ((((n * (n + 1)) / 2) * ( Triangle m)) + (( Triangle (n -' 1)) * ( Triangle (m -' 1)))) by Th19

      .= ((((n * (n + 1)) / 2) * ((m * (m + 1)) / 2)) + ((((n - 1) * ((n - 1) + 1)) / 2) * (((m - 1) * ((m - 1) + 1)) / 2))) by A4, A3, Th19

      .= (((((n * n) + n) / 2) * (((m * m) + m) / 2)) + ((((n * n) - n) / 2) * (((m * m) - m) / 2)))

      .= (((((n |^ 2) + n) / 2) * (((m * m) + m) / 2)) + ((((n * n) - n) / 2) * (((m * m) - m) / 2))) by NEWTON: 81

      .= (((((n |^ 2) + n) / 2) * (((m |^ 2) + m) / 2)) + ((((n * n) - n) / 2) * (((m * m) - m) / 2))) by NEWTON: 81

      .= (((((n |^ 2) + n) / 2) * (((m |^ 2) + m) / 2)) + ((((n |^ 2) - n) / 2) * (((m * m) - m) / 2))) by NEWTON: 81

      .= (((((n |^ 2) + n) / 2) * (((m |^ 2) + m) / 2)) + ((((n |^ 2) - n) / 2) * (((m |^ 2) - m) / 2))) by NEWTON: 81

      .= ((((n |^ 2) * (m |^ 2)) + (n * m)) / 2)

      .= ((((n * n) * (m |^ 2)) + (n * m)) / 2) by NEWTON: 81

      .= ((((n * n) * (m * m)) + (n * m)) / 2) by NEWTON: 81

      .= ( Triangle (n * m)) by A5;

      hence thesis;

    end;

    begin

    definition

      let s be Nat;

      :: NUMPOLY1:def9

      func PolygonalNumbers s -> set equals the set of all ( Polygon (s,n)) where n be Nat;

      coherence ;

    end

    definition

      let s be non trivial Nat;

      :: original: PolygonalNumbers

      redefine

      func PolygonalNumbers s -> Subset of NAT ;

      coherence

      proof

         the set of all ( Polygon (s,n)) where n be Nat c= NAT

        proof

          let x be object;

          assume x in the set of all ( Polygon (s,n)) where n be Nat;

          then ex n be Nat st x = ( Polygon (s,n));

          hence thesis by ORDINAL1:def 12;

        end;

        hence thesis;

      end;

    end

    

     Lm4: for s be non trivial Nat holds ( PolygonalNumbers s) is Subset of NAT ;

    definition

      :: NUMPOLY1:def10

      func TriangularNumbers -> Subset of NAT equals ( PolygonalNumbers 3);

      coherence

      proof

        3 is non trivial by NAT_2:def 1;

        hence thesis by Lm4;

      end;

      :: NUMPOLY1:def11

      func SquareNumbers -> Subset of NAT equals ( PolygonalNumbers 4);

      coherence

      proof

        4 is non trivial by NAT_2:def 1;

        hence thesis by Lm4;

      end;

    end

    registration

      let s be non trivial Nat;

      cluster ( PolygonalNumbers s) -> non empty;

      coherence

      proof

        

         A1: ( Polygon (s, 0 )) is set;

        ( Polygon (s,n)) in ( PolygonalNumbers s);

        hence thesis by A1, XBOOLE_0:def 1;

      end;

    end

    registration

      cluster TriangularNumbers -> non empty;

      coherence

      proof

        3 is non trivial by NAT_2:def 1;

        hence thesis;

      end;

      cluster SquareNumbers -> non empty;

      coherence

      proof

        4 is non trivial by NAT_2:def 1;

        hence thesis;

      end;

    end

    registration

      cluster -> triangular for Element of TriangularNumbers ;

      coherence

      proof

        let x be Element of TriangularNumbers ;

        x in TriangularNumbers by SUBSET_1:def 1;

        then ex n be Nat st x = ( Polygon (3,n));

        hence thesis;

      end;

      cluster -> square for Element of SquareNumbers ;

      coherence

      proof

        let x be Element of SquareNumbers ;

        x in SquareNumbers by SUBSET_1:def 1;

        then ex n be Nat st x = ( Polygon (4,n));

        hence thesis;

      end;

    end

    theorem :: NUMPOLY1:70

    

     Th70: for x be number holds x in TriangularNumbers iff x is triangular

    proof

      let x be number;

      thus x in TriangularNumbers implies x is triangular;

      assume x is triangular;

      then

      consider n be Nat such that

       A1: x = ( Triangle n);

      x = ( Polygon (3,n)) by A1, Th40;

      hence thesis;

    end;

    theorem :: NUMPOLY1:71

    

     Th71: for x be number holds x in SquareNumbers iff x is square

    proof

      let x be number;

      thus x in SquareNumbers implies x is square;

      assume x is square;

      then

      consider n be Nat such that

       A1: x = (n ^2 ) by PYTHTRIP:def 3;

      x = ( Polygon (4,n)) by A1;

      hence thesis;

    end;

    begin

    theorem :: NUMPOLY1:72

    

     Th72: ((n + 1) choose 2) = ((n * (n + 1)) / 2)

    proof

      per cases ;

        suppose

         A1: n <> 0 ;

        then

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

        

         A3: (n + 1) >= (1 + 1) by NAT_1: 14, A1, XREAL_1: 6;

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

        .= ((n + 1) - 2);

        

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

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

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

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

        .= ((n * (n + 1)) / 2) by XCMPLX_1: 91;

        hence thesis;

      end;

        suppose n = 0 ;

        hence thesis by NEWTON:def 3;

      end;

    end;

    theorem :: NUMPOLY1:73

    ( Triangle n) = ((n + 1) choose 2)

    proof

      ((n + 1) choose 2) = ((n * (n + 1)) / 2) by Th72;

      hence thesis by Th19;

    end;

    theorem :: NUMPOLY1:74

    

     Th74: for n be non zero Nat st n is even perfect holds n is triangular

    proof

      let n be non zero Nat;

      assume n is even perfect;

      then

      consider p be Nat such that

       A1: ((2 |^ p) -' 1) is prime & n = ((2 |^ (p -' 1)) * ((2 |^ p) -' 1)) by NAT_5: 39;

      set p1 = ( Mersenne p);

      

       A2: p <> 0

      proof

        assume p = 0 ;

        

        then ((2 |^ p) -' 1) = (1 -' 1) by NEWTON: 4

        .= 0 by XREAL_1: 232;

        hence thesis by A1;

      end;

      

       A3: n = ((2 |^ (p -' 1)) * p1) by A1, XREAL_0:def 2;

      

       A4: (p -' 1) = (p - 1) by XREAL_1: 233, A2, NAT_1: 14;

      ((2 to_power p) / (2 to_power 1)) = ((p1 + 1) / 2);

      then

       A5: (2 to_power (p -' 1)) = ((p1 + 1) / 2) by A4, POWER: 29;

      ((p1 * (p1 + 1)) / 2) = ( Triangle p1) by Th19;

      hence thesis by A3, A5;

    end;

    registration

      let n be non zero Nat;

      cluster ( Mersenne n) -> non zero;

      coherence

      proof

        assume ( Mersenne n) = 0 ;

        then ( log (2,(2 to_power n))) = 0 by POWER: 51;

        then (n * ( log (2,2))) = 0 by POWER: 55;

        then (n * 1) = 0 by POWER: 52;

        hence thesis;

      end;

    end

    definition

      let n be number;

      :: NUMPOLY1:def12

      attr n is mersenne means

      : Def12: ex p be Nat st n = ( Mersenne p);

    end

    registration

      cluster mersenne for Prime;

      existence

      proof

        reconsider p = ( Mersenne 2) as Prime by PEPIN: 41, GR_CY_3: 18;

        p is mersenne;

        hence thesis;

      end;

      cluster non prime for Nat;

      existence by INT_2: 29;

    end

    registration

      cluster mersenne non prime for Nat;

      existence

      proof

        set p = ( Mersenne 11);

        reconsider p as non prime Nat by INT_2:def 4, GR_CY_3: 22, NAT_D: 9;

        p is mersenne;

        hence thesis;

      end;

    end

    registration

      cluster -> non zero for Prime;

      coherence by INT_2:def 4;

    end

    registration

      let n be mersenne Prime;

      cluster ( Triangle n) -> perfect;

      coherence

      proof

        reconsider n0 = ( Triangle n) as non zero Nat by TARSKI: 1;

        consider p be Nat such that

         A1: n = ( Mersenne p) by Def12;

        (2 to_power p) > 0 by POWER: 34;

        then (2 |^ p) >= ( 0 + 1) by NAT_1: 13;

        then

         A2: ((2 |^ p) -' 1) = ((2 |^ p) - 1) by XREAL_0:def 2, XREAL_1: 19;

        

         A3: (p -' 1) = (p - 1) by XREAL_1: 233, A1, GR_CY_3: 16, NAT_1: 14;

        reconsider p1 = ( Mersenne p) as Nat;

        ((2 to_power p) / (2 to_power 1)) = ((p1 + 1) / 2);

        then (2 to_power (p -' 1)) = ((p1 + 1) / 2) by A3, POWER: 29;

        then (p1 * (2 |^ (p -' 1))) = ((p1 * (p1 + 1)) / 2);

        then n0 is perfect by NAT_5: 38, A2, A1, Th19;

        hence thesis;

      end;

    end

    registration

      cluster even perfect -> triangular for non zero Nat;

      coherence by Th74;

    end

    theorem :: NUMPOLY1:75

    

     Th75: ((8 * ( Triangle n)) + 1) = (((2 * n) + 1) ^2 )

    proof

      (8 * ( Triangle n)) = (8 * ((n * (n + 1)) / 2)) by Th19

      .= (4 * ((n ^2 ) + n));

      hence thesis;

    end;

    theorem :: NUMPOLY1:76

    

     Th76: n is triangular implies ((8 * n) + 1) is square

    proof

      assume n is triangular;

      then

      consider k be Nat such that

       A1: n = ( Triangle k);

      ((8 * ( Triangle k)) + 1) = (((2 * k) + 1) ^2 ) by Th75;

      hence ((8 * n) + 1) is square by A1;

    end;

    theorem :: NUMPOLY1:77

    

     Th77: n is triangular implies ((9 * n) + 1) is triangular

    proof

      assume n is triangular;

      then

      consider k be Nat such that

       A1: n = ( Triangle k);

      (1 + (9 * ( Triangle k))) = ( Triangle ((3 * k) + 1)) by Th67;

      hence thesis by A1;

    end;

    theorem :: NUMPOLY1:78

    

     Th78: ( Triangle n) is triangular square implies ( Triangle ((4 * n) * (n + 1))) is triangular square

    proof

      assume ( Triangle n) is triangular square;

      then ((n * (n + 1)) / 2) is triangular square by Th19;

      then

      consider k be Nat such that

       A1: ((n * (n + 1)) / 2) = (k ^2 ) by PYTHTRIP:def 3;

      ( Triangle ((4 * n) * (n + 1))) = (((8 * (k ^2 )) * ((8 * (k ^2 )) + 1)) / 2) by Th19, A1

      .= ((4 * (k ^2 )) * (((4 * n) * (n + 1)) + 1)) by A1

      .= (((2 * k) * ((2 * n) + 1)) ^2 );

      hence thesis;

    end;

    registration

      cluster TriangularNumbers -> infinite;

      coherence

      proof

        set T = TriangularNumbers ;

        for m be Element of NAT holds ex n be Element of NAT st n >= m & n in T

        proof

          let m be Element of NAT ;

          reconsider w = ( Triangle m) as Nat by TARSKI: 1;

          

           A1: w is triangular;

          reconsider n = ((9 * w) + 1) as Element of NAT by ORDINAL1:def 12;

          take n;

          

           A2: w >= m by Th44;

          (9 * w) >= (1 * w) by XREAL_1: 64;

          then ((9 * w) + 1) > w by NAT_1: 13;

          hence n >= m by A2, XXREAL_0: 2;

          thus thesis by Th70, A1, Th77;

        end;

        hence thesis by PYTHTRIP: 9;

      end;

      cluster SquareNumbers -> infinite;

      coherence

      proof

        set T = SquareNumbers ;

        for m be Element of NAT holds ex n be Element of NAT st n >= m & n in T

        proof

          let m be Element of NAT ;

          reconsider w = ( Triangle m) as Nat by TARSKI: 1;

          

           A3: w is triangular;

          reconsider n = ((8 * w) + 1) as Element of NAT by ORDINAL1:def 12;

          take n;

          

           A4: w >= m by Th44;

          (8 * w) >= (1 * w) by XREAL_1: 64;

          then ((8 * w) + 1) > w by NAT_1: 13;

          hence n >= m by A4, XXREAL_0: 2;

          thus thesis by Th71, A3, Th76;

        end;

        hence thesis by PYTHTRIP: 9;

      end;

    end

    registration

      cluster triangular square non zero for Nat;

      existence

      proof

        reconsider a = ( Triangle 1) as Nat by TARSKI: 1;

        take a;

        1 = (1 ^2 );

        then ( Triangle 1) is triangular square by FINSEQ_2: 50, RVSUM_1: 73;

        hence thesis;

      end;

    end

    theorem :: NUMPOLY1:79

    

     Th79: 0 is triangular square

    proof

       0 = ( 0 ^2 );

      then ( Triangle 0 ) is triangular square;

      hence thesis;

    end;

    registration

      cluster zero -> triangular square for number;

      coherence by Th79;

    end

    theorem :: NUMPOLY1:80

    

     Th80: 1 is triangular square

    proof

      1 = (1 ^2 );

      hence thesis by Th11;

    end;

    ::$Notion-Name

    theorem :: NUMPOLY1:81

    36 is triangular square

    proof

      ( Triangle ((4 * 1) * (1 + 1))) is triangular square by Th11, Th80, Th78;

      hence thesis by Th18;

    end;

    theorem :: NUMPOLY1:82

    1225 is triangular square

    proof

      

       A1: (35 ^2 ) = 1225;

      ( Triangle 49) = ((49 * (49 + 1)) / 2) by Th19

      .= 1225;

      hence thesis by A1;

    end;

    registration

      let n be triangular Nat;

      cluster ((9 * n) + 1) -> triangular;

      coherence by Th77;

    end

    registration

      let n be triangular Nat;

      cluster ((8 * n) + 1) -> square;

      coherence by Th76;

    end

    begin

    registration

      let a be Real;

      reduce ( lim ( seq_const a)) to a;

      reducibility

      proof

        (( seq_const a) . 1) = a by SEQ_1: 57;

        hence thesis by SEQ_4: 25;

      end;

    end

    definition

      :: NUMPOLY1:def13

      func ReciTriangRS -> Real_Sequence means

      : Def13: for i be Nat holds (it . i) = (1 / ( Triangle i));

      correctness

      proof

        deffunc F( Nat) = (1 / ( Triangle $1));

        thus (ex seq be Real_Sequence st for n be Nat holds (seq . n) = F(n)) & (for seq1,seq2 be Real_Sequence st (for n be Nat holds (seq1 . n) = F(n)) & (for n be Nat holds (seq2 . n) = F(n)) holds seq1 = seq2) from LNatRealSeq;

      end;

    end

    registration

      reduce ( ReciTriangRS . 0 ) to 0 ;

      reducibility

      proof

        

        thus ( ReciTriangRS . 0 ) = (1 / ( Triangle 0 )) by Def13

        .= 0 ;

      end;

    end

    theorem :: NUMPOLY1:83

    

     Th83: (1 / ( Triangle n)) = (2 / (n * (n + 1)))

    proof

      (1 / ( Triangle n)) = (1 / ((n * (n + 1)) / 2)) by Th19

      .= (2 / (n * (n + 1))) by XCMPLX_1: 57;

      hence thesis;

    end;

    theorem :: NUMPOLY1:84

    

     Th84: (( Partial_Sums ReciTriangRS ) . n) = (2 - (2 / (n + 1)))

    proof

      defpred P[ Nat] means (( Partial_Sums ReciTriangRS ) . $1) = (2 - (2 / ($1 + 1)));

      

       A1: P[ 0 ]

      proof

        ( ReciTriangRS . 0 ) = 0 ;

        hence thesis by SERIES_1:def 1;

      end;

      

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

      proof

        let k be Nat such that

         A3: P[k];

        

         A4: ( ReciTriangRS . (k + 1)) = (1 / ( Triangle (k + 1))) by Def13

        .= (2 / ((k + 1) * ((k + 1) + 1))) by Th83

        .= (2 / (((k * k) + (3 * k)) + 2));

        

         A5: ((k + 2) / (k + 2)) = 1 by XCMPLX_1: 60;

        

         A6: ((k + 1) / (k + 1)) = 1 by XCMPLX_1: 60;

        (( Partial_Sums ReciTriangRS ) . (k + 1)) = (((2 * ((k + 2) / (k + 2))) - ((2 / (k + 1)) * 1)) + (2 / ((k + 1) * (k + 2)))) by A5, A3, A4, SERIES_1:def 1

        .= ((((2 * (k + 2)) / (k + 2)) - ((2 / (k + 1)) * ((k + 2) / (k + 2)))) + (2 / ((k + 1) * (k + 2)))) by XCMPLX_1: 74, A5

        .= (((((2 * (k + 2)) / (k + 2)) * ((k + 1) / (k + 1))) - ((2 * (k + 2)) / ((k + 1) * (k + 2)))) + (2 / ((k + 1) * (k + 2)))) by A6, XCMPLX_1: 76

        .= (((((2 * (k + 2)) * (k + 1)) / ((k + 2) * (k + 1))) - ((2 * (k + 2)) / ((k + 1) * (k + 2)))) + (2 / ((k + 1) * (k + 2)))) by XCMPLX_1: 76

        .= (((((((2 * k) * k) + (6 * k)) + 4) - ((2 * k) + 4)) / ((k + 2) * (k + 1))) + (2 / ((k + 1) * (k + 2)))) by XCMPLX_1: 120

        .= (((((((2 * k) * k) + (6 * k)) + 4) - ((2 * k) + 4)) + 2) / ((k + 2) * (k + 1))) by XCMPLX_1: 62

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

        .= (((2 * (k + 2)) - 2) / (k + 2)) by XCMPLX_1: 91

        .= (((2 * (k + 2)) / (k + 2)) - (2 / (k + 2))) by XCMPLX_1: 120

        .= (2 - (2 / (k + 2))) by XCMPLX_1: 89;

        hence thesis;

      end;

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

      hence thesis;

    end;

    definition

      :: NUMPOLY1:def14

      func SumsReciTriang -> Real_Sequence means

      : Def14: for n be Nat holds (it . n) = (2 - (2 / (n + 1)));

      correctness

      proof

        deffunc F( Nat) = (2 - (2 / ($1 + 1)));

        thus (ex seq be Real_Sequence st for n be Nat holds (seq . n) = F(n)) & (for seq1,seq2 be Real_Sequence st (for n be Nat holds (seq1 . n) = F(n)) & (for n be Nat holds (seq2 . n) = F(n)) holds seq1 = seq2) from LNatRealSeq;

      end;

      let a,b be Real;

      :: NUMPOLY1:def15

      func geo-seq (a,b) -> Real_Sequence means

      : Def15: for n be Nat holds (it . n) = (a / (n + b));

      correctness

      proof

        deffunc F( Nat) = (a / ($1 + b));

        thus (ex seq be Real_Sequence st for n be Nat holds (seq . n) = F(n)) & (for seq1,seq2 be Real_Sequence st (for n be Nat holds (seq1 . n) = F(n)) & (for n be Nat holds (seq2 . n) = F(n)) holds seq1 = seq2) from LNatRealSeq;

      end;

    end

    theorem :: NUMPOLY1:85

    

     Th85: for a,b be Real holds ( geo-seq (a,b)) is convergent & ( lim ( geo-seq (a,b))) = 0

    proof

      let a,b be Real;

      for k be Nat holds (( geo-seq (a,b)) . k) = (a / (k + b)) by Def15;

      hence thesis by SEQ_4: 31;

    end;

    theorem :: NUMPOLY1:86

    

     Th86: SumsReciTriang = (( seq_const 2) + ( - ( geo-seq (2,1))))

    proof

      for k be Nat holds ( SumsReciTriang . k) = ((( seq_const 2) . k) + (( - ( geo-seq (2,1))) . k))

      proof

        let k be Nat;

        

         A1: ( SumsReciTriang . k) = (2 - (2 / (k + 1))) by Def14;

        

         A2: (( seq_const 2) . k) = 2 by SEQ_1: 57;

        ( - (( geo-seq (2,1)) . k)) = (( - ( geo-seq (2,1))) . k) by VALUED_1: 8;

        then (( - ( geo-seq (2,1))) . k) = ( - (2 / (k + 1))) by Def15;

        hence thesis by A1, A2;

      end;

      hence thesis by SEQ_1: 7;

    end;

    theorem :: NUMPOLY1:87

    

     Th87: SumsReciTriang is convergent & ( lim SumsReciTriang ) = 2

    proof

      

       A1: ( seq_const 2) is convergent & ( lim ( seq_const 2)) = 2;

      

       A2: ( geo-seq (2,1)) is convergent by Th85;

      

       A3: ( lim ( geo-seq (2,1))) = 0 by Th85;

      

       A4: ( lim ( - ( geo-seq (2,1)))) = ( - ( lim ( geo-seq (2,1)))) by SEQ_2: 10, Th85

      .= 0 by A3;

      ( lim SumsReciTriang ) = (2 + 0 ) by SEQ_2: 6, A1, A2, Th86, A4;

      hence thesis by Th86, A2;

    end;

    theorem :: NUMPOLY1:88

    ( Partial_Sums ReciTriangRS ) = SumsReciTriang by Th84, Def14;

    ::$Notion-Name

    theorem :: NUMPOLY1:89

    ( Sum ReciTriangRS ) = 2 by Th84, Def14, Th87;