series_4.miz



    begin

    reserve n for Nat,

a,b,c,d for Real,

s for Real_Sequence;

    

     Lm1: 4 = (2 |^ 2) & ((a + b) |^ 2) = (((a |^ 2) + ((2 * a) * b)) + (b |^ 2))

    proof

      

       A1: ((a + b) |^ (1 + 1)) = (((a + b) |^ 1) * (a + b)) by NEWTON: 6

      .= ((a + b) * (a + b))

      .= (((a * a) + (a * b)) + ((a * b) + (b * b)))

      .= (((a * a) + (a * b)) + ((a * b) + (b |^ 2))) by WSIERP_1: 1

      .= (((a |^ 2) + (a * b)) + ((a * b) + (b |^ 2))) by WSIERP_1: 1

      .= (((a |^ 2) + (2 * (a * b))) + (b |^ 2));

      (2 |^ 2) = (2 * 2) by WSIERP_1: 1

      .= 4;

      hence thesis by A1;

    end;

    

     Lm2: ((((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ 2) = ((((1 / 4) |^ (n + 1)) + (4 |^ (n + 1))) + 2)

    proof

      ((((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ (1 + 1)) = (((((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ 1) * (((1 / 2) |^ (n + 1)) + (2 |^ (n + 1)))) by NEWTON: 6

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

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

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

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

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

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

      .= ((((1 / 4) |^ (n + 1)) + 1) + ((1 |^ (n + 1)) + (4 |^ (n + 1))))

      .= ((((1 / 4) |^ (n + 1)) + 1) + (1 + (4 |^ (n + 1))))

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

      hence thesis;

    end;

    

     Lm3: ((((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ 2) = ((((1 / 9) |^ (n + 1)) + (9 |^ (n + 1))) + 2)

    proof

      ((((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ (1 + 1)) = (((((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ 1) * (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1)))) by NEWTON: 6

      .= ((((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) * (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))))

      .= (((((1 / 3) |^ (n + 1)) * ((1 / 3) |^ (n + 1))) + (((1 / 3) |^ (n + 1)) * (3 |^ (n + 1)))) + (((3 |^ (n + 1)) * ((1 / 3) |^ (n + 1))) + ((3 |^ (n + 1)) * (3 |^ (n + 1)))))

      .= (((((1 / 3) * (1 / 3)) |^ (n + 1)) + (((1 / 3) |^ (n + 1)) * (3 |^ (n + 1)))) + (((3 |^ (n + 1)) * ((1 / 3) |^ (n + 1))) + ((3 |^ (n + 1)) * (3 |^ (n + 1))))) by NEWTON: 7

      .= ((((((1 / 3) * 1) / 3) |^ (n + 1)) + (((1 / 3) * 3) |^ (n + 1))) + (((3 |^ (n + 1)) * ((1 / 3) |^ (n + 1))) + ((3 |^ (n + 1)) * (3 |^ (n + 1))))) by NEWTON: 7

      .= ((((((1 / 3) * 1) / 3) |^ (n + 1)) + (((1 / 3) * 3) |^ (n + 1))) + (((3 * (1 / 3)) |^ (n + 1)) + ((3 |^ (n + 1)) * (3 |^ (n + 1))))) by NEWTON: 7

      .= ((((((1 / 3) * 1) / 3) |^ (n + 1)) + (((1 / 3) * 3) |^ (n + 1))) + (((3 * (1 / 3)) |^ (n + 1)) + ((3 * 3) |^ (n + 1)))) by NEWTON: 7

      .= ((((1 / 9) |^ (n + 1)) + 1) + ((1 |^ (n + 1)) + (9 |^ (n + 1))))

      .= ((((1 / 9) |^ (n + 1)) + 1) + (1 + (9 |^ (n + 1))))

      .= ((((1 / 9) |^ (n + 1)) + 2) + (9 |^ (n + 1)));

      hence thesis;

    end;

    

     Lm4: ((a - b) * (a + b)) = ((a |^ 2) - (b |^ 2))

    proof

      ((a - b) * (a + b)) = ((a * a) - (b * b))

      .= ((a |^ 2) - (b * b)) by WSIERP_1: 1

      .= ((a |^ 2) - (b |^ 2)) by WSIERP_1: 1;

      hence thesis;

    end;

    

     Lm5: ((a - b) |^ 2) = (((a |^ 2) - ((2 * a) * b)) + (b |^ 2))

    proof

      ((a - b) |^ (1 + 1)) = (((a - b) |^ 1) * (a - b)) by NEWTON: 6

      .= ((a - b) * (a - b))

      .= (((a * a) - (a * b)) - ((a * b) - (b * b)))

      .= (((a * a) - (a * b)) - ((a * b) - (b |^ 2))) by WSIERP_1: 1

      .= (((a |^ 2) - (a * b)) - ((a * b) - (b |^ 2))) by WSIERP_1: 1

      .= (((a |^ 2) - (2 * (a * b))) + (b |^ 2));

      hence thesis;

    end;

    

     Lm6: a <> 1 implies (((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1))) = (((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a)))

    proof

      assume a <> 1;

      then

       A1: (1 - a) <> 0 ;

      

      then (((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1))) = (((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - (((1 - a) * (n * (a |^ (n + 1)))) / ((1 - a) * (1 - a)))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1))) by XCMPLX_1: 91

      .= (((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - (((1 - a) * (n * (a |^ (n + 1)))) / ((1 - a) |^ 2))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1))) by WSIERP_1: 1

      .= (((((a - (a * (a |^ n))) - ((n * (a |^ (n + 1))) - ((n * (a |^ (n + 1))) * a))) / ((1 - a) |^ 2)) + (n * (a |^ (n + 1)))) + (a |^ (n + 1))) by XCMPLX_1: 120

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

      .= (((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * (((1 - a) / (1 - a)) * 1))) by A1, XCMPLX_1: 60

      .= (((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * (((1 - a) / (1 - a)) * ((1 - a) / (1 - a))))) by A1, XCMPLX_1: 60

      .= (((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * (((1 - a) * (1 - a)) / ((1 - a) * (1 - a))))) by XCMPLX_1: 76

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

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

      .= (((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * ((((1 |^ 2) - ((2 * 1) * a)) + (a |^ 2)) / ((1 - a) * (1 - a))))) by Lm5

      .= (((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * ((((1 |^ 2) - ((2 * 1) * a)) + (a |^ 2)) / ((1 - a) |^ 2)))) by WSIERP_1: 1

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

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

      .= (((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) + (((((n * (a |^ (n + 1))) * 1) - (((n * (a |^ (n + 1))) * 2) * a)) + ((n * (a |^ (n + 1))) * (a |^ 2))) + ((((a |^ (n + 1)) * 1) - (((a |^ (n + 1)) * 2) * a)) + ((a |^ (n + 1)) * (a |^ 2))))) / ((1 - a) |^ 2)) by XCMPLX_1: 62

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

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

      .= (((a - ((a |^ (n + 1)) * a)) - (((n + 1) * (a |^ (n + 1))) * (a - (a * a)))) / ((1 - a) |^ 2)) by WSIERP_1: 1

      .= (((a - ((a |^ (n + 1)) * a)) / ((1 - a) |^ 2)) - (((((n + 1) * (a |^ (n + 1))) * a) * (1 - a)) / ((1 - a) |^ 2))) by XCMPLX_1: 120

      .= (((a - ((a |^ (n + 1)) * a)) / ((1 - a) |^ 2)) - (((((n + 1) * (a |^ (n + 1))) * a) * (1 - a)) / ((1 - a) * (1 - a)))) by WSIERP_1: 1

      .= (((a - ((a |^ (n + 1)) * a)) / ((1 - a) |^ 2)) - ((((((n + 1) * (a |^ (n + 1))) * a) / (1 - a)) * (1 - a)) / (1 - a))) by XCMPLX_1: 83

      .= (((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * ((a |^ (n + 1)) * a)) / (1 - a))) by A1, XCMPLX_1: 87

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

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

      hence thesis;

    end;

    

     Lm7: (1 / ((2 -Root (n + 2)) + (2 -Root (n + 1)))) = ((2 -Root (n + 2)) - (2 -Root (n + 1)))

    proof

      ((n + 1) + 1) > (n + 1) by NAT_1: 13;

      then (2 -Root (n + 2)) > (2 -Root (n + 1)) by PREPOWER: 28;

      then ((2 -Root (n + 2)) - (2 -Root (n + 1))) > ((2 -Root (n + 1)) - (2 -Root (n + 1))) by XREAL_1: 9;

      

      then ((1 / ((2 -Root (n + 2)) + (2 -Root (n + 1)))) * 1) = ((1 * ((2 -Root (n + 2)) - (2 -Root (n + 1)))) / (((2 -Root (n + 2)) - (2 -Root (n + 1))) * ((2 -Root (n + 2)) + (2 -Root (n + 1))))) by XCMPLX_1: 91

      .= (((2 -Root (n + 2)) - (2 -Root (n + 1))) / (((2 -Root (n + 2)) |^ 2) - ((2 -Root (n + 1)) |^ 2))) by Lm4

      .= (((2 -Root (n + 2)) - (2 -Root (n + 1))) / ((n + 2) - ((2 -Root (n + 1)) |^ 2))) by PREPOWER: 19

      .= (((2 -Root (n + 2)) - (2 -Root (n + 1))) / ((n + 2) - (n + 1))) by PREPOWER: 19

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

      hence thesis;

    end;

    theorem :: SERIES_4:1

    

     Th1: (((a + b) + c) |^ 2) = ((((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c))

    proof

      (((a + b) + c) |^ (1 + 1)) = ((((a + b) + c) |^ 1) * ((a + b) + c)) by NEWTON: 6

      .= (((a + b) + c) * ((a + b) + c))

      .= (((((a * a) + (a * b)) + (a * c)) + (((a * b) + (b * b)) + (b * c))) + (((a * c) + (c * b)) + (c * c)))

      .= (((((a * a) + (a * b)) + (a * c)) + (((a * b) + (b |^ 2)) + (b * c))) + (((a * c) + (c * b)) + (c * c))) by WSIERP_1: 1

      .= (((((a |^ 2) + (a * b)) + (a * c)) + (((a * b) + (b |^ 2)) + (b * c))) + (((a * c) + (c * b)) + (c * c))) by WSIERP_1: 1

      .= (((((a |^ 2) + (a * b)) + (a * c)) + (((a * b) + (b |^ 2)) + (b * c))) + (((a * c) + (c * b)) + (c |^ 2))) by WSIERP_1: 1

      .= ((((((a |^ 2) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c)) + (b |^ 2));

      hence thesis;

    end;

    theorem :: SERIES_4:2

    

     Th2: ((a + b) |^ 3) = ((((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) + (b |^ 3))

    proof

      ((a + b) |^ (2 + 1)) = (((a + b) |^ 2) * (a + b)) by NEWTON: 6

      .= ((((a |^ 2) + ((2 * a) * b)) + (b |^ 2)) * (a + b)) by Lm1

      .= (((((a |^ 2) * a) + ((a |^ 2) * b)) + ((((2 * a) * b) * a) + (((2 * a) * b) * b))) + (((b |^ 2) * a) + ((b |^ 2) * b)))

      .= (((((a |^ 2) * a) + ((a |^ 2) * b)) + ((((2 * a) * b) * a) + (((2 * a) * b) * b))) + (((b |^ 2) * a) + (b |^ (2 + 1)))) by NEWTON: 6

      .= ((((a |^ 3) + ((a |^ 2) * b)) + (((2 * (a * a)) * b) + (((2 * a) * b) * b))) + (((b |^ 2) * a) + (b |^ 3))) by NEWTON: 6

      .= ((((a |^ 3) + ((a |^ 2) * b)) + (((2 * ((a |^ 1) * a)) * b) + (((2 * a) * b) * b))) + (((b |^ 2) * a) + (b |^ 3)))

      .= ((((a |^ 3) + ((a |^ 2) * b)) + (((2 * (a |^ (1 + 1))) * b) + (((2 * a) * b) * b))) + (((b |^ 2) * a) + (b |^ 3))) by NEWTON: 6

      .= ((((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((2 * (b * b)) * a)) + (((b |^ 2) * a) + (b |^ 3)))

      .= ((((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((2 * ((b |^ 1) * b)) * a)) + (((b |^ 2) * a) + (b |^ 3)))

      .= ((((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((2 * (b |^ (1 + 1))) * a)) + (((b |^ 2) * a) + (b |^ 3))) by NEWTON: 6

      .= ((((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) + (b |^ 3));

      hence thesis;

    end;

    theorem :: SERIES_4:3

    (((a - b) + c) |^ 2) = ((((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) + ((2 * a) * c)) - ((2 * b) * c))

    proof

      (((a - b) + c) |^ (1 + 1)) = ((((a - b) + c) |^ 1) * ((a - b) + c)) by NEWTON: 6

      .= (((a - b) + c) * ((a - b) + c))

      .= (((((a * a) - (a * b)) + (a * c)) - (((a * b) - (b * b)) + (b * c))) + (((a * c) - (c * b)) + (c * c)))

      .= (((((a * a) - (a * b)) + (a * c)) - (((a * b) - (b |^ 2)) + (b * c))) + (((a * c) - (c * b)) + (c * c))) by WSIERP_1: 1

      .= (((((a |^ 2) - (a * b)) + (a * c)) - (((a * b) - (b |^ 2)) + (b * c))) + (((a * c) - (c * b)) + (c * c))) by WSIERP_1: 1

      .= (((((a |^ 2) - (a * b)) + (a * c)) - (((a * b) - (b |^ 2)) + (b * c))) + (((a * c) - (c * b)) + (c |^ 2))) by WSIERP_1: 1

      .= ((((((a |^ 2) + (c |^ 2)) - ((2 * a) * b)) + ((2 * a) * c)) - ((2 * b) * c)) + (b |^ 2));

      hence thesis;

    end;

    theorem :: SERIES_4:4

    (((a - b) - c) |^ 2) = ((((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) - ((2 * a) * c)) + ((2 * b) * c))

    proof

      (((a - b) - c) |^ (1 + 1)) = ((((a - b) - c) |^ 1) * ((a - b) - c)) by NEWTON: 6

      .= (((a - b) - c) * ((a - b) - c))

      .= (((((a * a) - (a * b)) - (a * c)) - (((a * b) - (b * b)) - (b * c))) - (((a * c) - (c * b)) - (c * c)))

      .= (((((a * a) - (a * b)) - (a * c)) - (((a * b) - (b |^ 2)) - (b * c))) - (((a * c) - (c * b)) - (c * c))) by WSIERP_1: 1

      .= (((((a |^ 2) - (a * b)) - (a * c)) - (((a * b) - (b |^ 2)) - (b * c))) - (((a * c) - (c * b)) - (c * c))) by WSIERP_1: 1

      .= (((((a |^ 2) - (a * b)) - (a * c)) - (((a * b) - (b |^ 2)) - (b * c))) - (((a * c) - (c * b)) - (c |^ 2))) by WSIERP_1: 1

      .= ((((((a |^ 2) + (c |^ 2)) - ((2 * a) * b)) - ((2 * a) * c)) + ((2 * b) * c)) + (b |^ 2));

      hence thesis;

    end;

    theorem :: SERIES_4:5

    ((a - b) |^ 3) = ((((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) - (b |^ 3))

    proof

      ((a - b) |^ (2 + 1)) = (((a - b) |^ 2) * (a - b)) by NEWTON: 6

      .= ((((a |^ 2) - ((2 * a) * b)) + (b |^ 2)) * (a - b)) by Lm5

      .= (((((a |^ 2) * a) - ((a |^ 2) * b)) - ((((2 * a) * b) * a) - (((2 * a) * b) * b))) + (((b |^ 2) * a) - ((b |^ 2) * b)))

      .= (((((a |^ 2) * a) - ((a |^ 2) * b)) - ((((2 * a) * b) * a) - (((2 * a) * b) * b))) + (((b |^ 2) * a) - (b |^ (2 + 1)))) by NEWTON: 6

      .= ((((a |^ 3) - ((a |^ 2) * b)) - (((2 * (a * a)) * b) - (((2 * a) * b) * b))) + (((b |^ 2) * a) - (b |^ 3))) by NEWTON: 6

      .= ((((a |^ 3) - ((a |^ 2) * b)) - (((2 * ((a |^ 1) * a)) * b) - (((2 * a) * b) * b))) + (((b |^ 2) * a) - (b |^ 3)))

      .= ((((a |^ 3) - ((a |^ 2) * b)) - (((2 * (a |^ (1 + 1))) * b) - (((2 * a) * b) * b))) + (((b |^ 2) * a) - (b |^ 3))) by NEWTON: 6

      .= (((((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((2 * (b * b)) * a)) + ((b |^ 2) * a)) - (b |^ 3))

      .= (((((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((2 * ((b |^ 1) * b)) * a)) + ((b |^ 2) * a)) - (b |^ 3))

      .= (((((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((2 * (b |^ (1 + 1))) * a)) + ((b |^ 2) * a)) - (b |^ 3)) by NEWTON: 6

      .= ((((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) - (b |^ 3));

      hence thesis;

    end;

    theorem :: SERIES_4:6

    ((a + b) |^ 4) = (((((a |^ 4) + ((4 * (a |^ 3)) * b)) + ((6 * (a |^ 2)) * (b |^ 2))) + ((4 * (b |^ 3)) * a)) + (b |^ 4))

    proof

      ((a + b) |^ (3 + 1)) = (((a + b) |^ 3) * (a + b)) by NEWTON: 6

      .= (((((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) + (b |^ 3)) * (a + b)) by Th2

      .= ((((((a |^ 3) * a) + ((a |^ 3) * b)) + ((((3 * (a |^ 2)) * b) * a) + (((3 * (a |^ 2)) * b) * b))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + ((b |^ 3) * b)))

      .= ((((((a |^ 3) * a) + ((a |^ 3) * b)) + ((((3 * (a |^ 2)) * b) * a) + (((3 * (a |^ 2)) * b) * b))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ (3 + 1)))) by NEWTON: 6

      .= (((((a |^ 4) + ((a |^ 3) * b)) + (((3 * ((a |^ 2) * a)) * b) + (((3 * (a |^ 2)) * b) * b))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4))) by NEWTON: 6

      .= (((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ (2 + 1))) * b) + (((3 * (a |^ 2)) * b) * b))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4))) by NEWTON: 6

      .= (((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b * b)))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4)))

      .= (((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * ((b |^ 1) * b)))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4)))

      .= (((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b |^ (1 + 1))))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4))) by NEWTON: 6

      .= (((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b |^ 2)))) + (((3 * (b |^ 2)) * (a * a)) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4)))

      .= (((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b |^ 2)))) + (((3 * (b |^ 2)) * ((a |^ 1) * a)) + (((3 * (b |^ 2)) * b) * a))) + (((b |^ 3) * a) + (b |^ 4)))

      .= (((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b |^ 2)))) + (((3 * (b |^ 2)) * (a |^ (1 + 1))) + ((3 * ((b |^ 2) * b)) * a))) + (((b |^ 3) * a) + (b |^ 4))) by NEWTON: 6

      .= (((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b |^ 2)))) + (((3 * (b |^ 2)) * (a |^ 2)) + ((3 * (b |^ (2 + 1))) * a))) + (((b |^ 3) * a) + (b |^ 4))) by NEWTON: 6

      .= (((((a |^ 4) + ((4 * (a |^ 3)) * b)) + ((6 * (a |^ 2)) * (b |^ 2))) + ((4 * (b |^ 3)) * a)) + (b |^ 4));

      hence thesis;

    end;

    theorem :: SERIES_4:7

    ((((a + b) + c) + d) |^ 2) = (((((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + (d |^ 2)) + ((((2 * a) * b) + ((2 * a) * c)) + ((2 * a) * d))) + (((2 * b) * c) + ((2 * b) * d))) + ((2 * c) * d))

    proof

      ((((a + b) + c) + d) |^ (1 + 1)) = (((((a + b) + c) + d) |^ 1) * (((a + b) + c) + d)) by NEWTON: 6

      .= ((((a + b) + c) + d) * (((a + b) + c) + d))

      .= (((((((a * a) + (a * b)) + (a * c)) + (a * d)) + ((((a * b) + (b * b)) + (b * c)) + (b * d))) + ((((a * c) + (c * b)) + (c * c)) + (c * d))) + ((((a * d) + (d * b)) + (d * c)) + (d * d)))

      .= (((((((a * a) + (a * b)) + (a * c)) + (a * d)) + ((((a * b) + (b |^ 2)) + (b * c)) + (b * d))) + ((((a * c) + (c * b)) + (c * c)) + (c * d))) + ((((a * d) + (d * b)) + (d * c)) + (d * d))) by WSIERP_1: 1

      .= (((((((a |^ 2) + (a * b)) + (a * c)) + (a * d)) + ((((a * b) + (b |^ 2)) + (b * c)) + (b * d))) + ((((a * c) + (c * b)) + (c * c)) + (c * d))) + ((((a * d) + (d * b)) + (d * c)) + (d * d))) by WSIERP_1: 1

      .= (((((((a |^ 2) + (a * b)) + (a * c)) + (a * d)) + ((((a * b) + (b |^ 2)) + (b * c)) + (b * d))) + ((((a * c) + (c * b)) + (c |^ 2)) + (c * d))) + ((((a * d) + (d * b)) + (d * c)) + (d * d))) by WSIERP_1: 1

      .= (((((((a |^ 2) + (a * b)) + (a * c)) + (a * d)) + ((((a * b) + (b |^ 2)) + (b * c)) + (b * d))) + ((((a * c) + (c * b)) + (c |^ 2)) + (c * d))) + ((((a * d) + (d * b)) + (d * c)) + (d |^ 2))) by WSIERP_1: 1

      .= (((((((a |^ 2) + (c |^ 2)) + (b |^ 2)) + (d |^ 2)) + ((((2 * a) * b) + ((2 * a) * c)) + ((2 * a) * d))) + (((2 * b) * c) + ((2 * b) * d))) + ((2 * c) * d));

      hence thesis;

    end;

    theorem :: SERIES_4:8

    (((a + b) + c) |^ 3) = (((((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + (((3 * (a |^ 2)) * b) + ((3 * (a |^ 2)) * c))) + (((3 * (b |^ 2)) * a) + ((3 * (b |^ 2)) * c))) + (((3 * (c |^ 2)) * a) + ((3 * (c |^ 2)) * b))) + (((6 * a) * b) * c))

    proof

      (((a + b) + c) |^ (2 + 1)) = ((((a + b) + c) |^ 2) * ((a + b) + c)) by NEWTON: 6

      .= (((((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c)) * ((a + b) + c)) by Th1

      .= (((((((((a |^ 2) * a) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + ((b |^ 2) * b)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + ((c |^ 2) * c))) + (((((2 * a) * b) * a) + (((2 * a) * b) * b)) + (((2 * a) * b) * c))) + (((((2 * a) * c) * a) + (((2 * a) * c) * b)) + (((2 * a) * c) * c))) + (((((2 * b) * c) * a) + (((2 * b) * c) * b)) + (((2 * b) * c) * c)))

      .= ((((((((a |^ (2 + 1)) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + ((b |^ 2) * b)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + ((c |^ 2) * c))) + (((((2 * a) * b) * a) + (((2 * a) * b) * b)) + (((2 * a) * b) * c))) + (((((2 * a) * c) * a) + (((2 * a) * c) * b)) + (((2 * a) * c) * c))) + (((((2 * b) * c) * a) + (((2 * b) * c) * b)) + (((2 * b) * c) * c))) by NEWTON: 6

      .= ((((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ (2 + 1))) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + ((c |^ 2) * c))) + (((((2 * a) * b) * a) + (((2 * a) * b) * b)) + (((2 * a) * b) * c))) + (((((2 * a) * c) * a) + (((2 * a) * c) * b)) + (((2 * a) * c) * c))) + (((((2 * b) * c) * a) + (((2 * b) * c) * b)) + (((2 * b) * c) * c))) by NEWTON: 6

      .= ((((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a * a)) * b) + ((2 * a) * (b * b))) + (((2 * a) * b) * c))) + ((((2 * (a * a)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c)))) by NEWTON: 6

      .= ((((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * ((a |^ 1) * a)) * b) + ((2 * a) * (b * b))) + (((2 * a) * b) * c))) + ((((2 * (a * a)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c))))

      .= ((((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ (1 + 1))) * b) + ((2 * a) * (b * b))) + (((2 * a) * b) * c))) + ((((2 * (a * a)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c)))) by NEWTON: 6

      .= ((((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * ((b |^ 1) * b))) + (((2 * a) * b) * c))) + ((((2 * (a * a)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c))))

      .= ((((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * (b |^ (1 + 1)))) + (((2 * a) * b) * c))) + ((((2 * (a * a)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c)))) by NEWTON: 6

      .= ((((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * (b |^ 2))) + (((2 * a) * b) * c))) + ((((2 * (a |^ 2)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c)))) by WSIERP_1: 1

      .= ((((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * (b |^ 2))) + (((2 * a) * b) * c))) + ((((2 * (a |^ 2)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c |^ 2)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c)))) by WSIERP_1: 1

      .= ((((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * (b |^ 2))) + (((2 * a) * b) * c))) + ((((2 * (a |^ 2)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c |^ 2)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c |^ 2)))) by WSIERP_1: 1

      .= ((((((((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + (((b |^ 2) * a) + ((b |^ 2) * c))) + (((c |^ 2) * a) + ((c |^ 2) * b))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * (b |^ 2))) + (((2 * a) * b) * c))) + ((((2 * (a |^ 2)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c |^ 2)))) + (((((2 * b) * c) * a) + ((2 * (b |^ 2)) * c)) + ((2 * (c |^ 2)) * b))) by WSIERP_1: 1

      .= (((((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + (((3 * (a |^ 2)) * b) + ((3 * (a |^ 2)) * c))) + (((3 * (b |^ 2)) * a) + ((3 * (b |^ 2)) * c))) + (((3 * (c |^ 2)) * a) + ((3 * (c |^ 2)) * b))) + (((6 * a) * b) * c));

      hence thesis;

    end;

    theorem :: SERIES_4:9

    a <> 0 implies ((((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 2) = ((((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2)

    proof

      assume

       A1: a <> 0 ;

      ((((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ (1 + 1)) = (((((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 1) * (((1 / a) |^ (n + 1)) + (a |^ (n + 1)))) by NEWTON: 6

      .= ((((1 / a) |^ (n + 1)) + (a |^ (n + 1))) * (((1 / a) |^ (n + 1)) + (a |^ (n + 1))))

      .= (((((1 / a) |^ (n + 1)) * ((1 / a) |^ (n + 1))) + (((1 / a) |^ (n + 1)) * (a |^ (n + 1)))) + (((a |^ (n + 1)) * ((1 / a) |^ (n + 1))) + ((a |^ (n + 1)) * (a |^ (n + 1)))))

      .= (((((1 / a) * (1 / a)) |^ (n + 1)) + (((1 / a) |^ (n + 1)) * (a |^ (n + 1)))) + (((a |^ (n + 1)) * ((1 / a) |^ (n + 1))) + ((a |^ (n + 1)) * (a |^ (n + 1))))) by NEWTON: 7

      .= (((((1 / a) * (1 / a)) |^ (n + 1)) + (((1 / a) * a) |^ (n + 1))) + (((a |^ (n + 1)) * ((1 / a) |^ (n + 1))) + ((a |^ (n + 1)) * (a |^ (n + 1))))) by NEWTON: 7

      .= (((((1 / a) * (1 / a)) |^ (n + 1)) + (((1 / a) * a) |^ (n + 1))) + (((a * (1 / a)) |^ (n + 1)) + ((a |^ (n + 1)) * (a |^ (n + 1))))) by NEWTON: 7

      .= (((((1 / a) * (1 / a)) |^ (n + 1)) + (((1 / a) * a) |^ (n + 1))) + (((a * (1 / a)) |^ (n + 1)) + ((a * a) |^ (n + 1)))) by NEWTON: 7

      .= (((((1 / a) * (1 / a)) |^ (n + 1)) + (1 |^ (n + 1))) + ((((1 / a) * a) |^ (n + 1)) + ((a * a) |^ (n + 1)))) by A1, XCMPLX_1: 106

      .= (((((1 / a) * (1 / a)) |^ (n + 1)) + (1 |^ (n + 1))) + ((1 |^ (n + 1)) + ((a * a) |^ (n + 1)))) by A1, XCMPLX_1: 106

      .= (((((1 / a) * (1 / a)) |^ (n + 1)) + 1) + ((1 |^ (n + 1)) + ((a * a) |^ (n + 1))))

      .= (((((1 / a) * (1 / a)) |^ (n + 1)) + 1) + (1 + ((a * a) |^ (n + 1))))

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

      .= (((((1 / a) * (1 / a)) |^ (n + 1)) + ((a |^ 2) |^ (n + 1))) + 2) by WSIERP_1: 1

      .= (((((1 / a) * (1 / a)) |^ (n + 1)) + (a |^ (2 * (n + 1)))) + 2) by NEWTON: 9

      .= (((((1 / a) |^ 2) |^ (n + 1)) + (a |^ ((2 * n) + 2))) + 2) by WSIERP_1: 1

      .= ((((1 / a) |^ (2 * (n + 1))) + (a |^ ((2 * n) + 2))) + 2) by NEWTON: 9

      .= ((((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2);

      hence thesis;

    end;

    theorem :: SERIES_4:10

    (a <> 1 & for n holds (s . n) = (a |^ n)) implies (( Partial_Sums s) . n) = ((1 - (a |^ (n + 1))) / (1 - a))

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) = ((1 - (a |^ ($1 + 1))) / (1 - a));

      assume a <> 1;

      then

       A1: (1 - a) <> 0 ;

      assume

       A2: for n holds (s . n) = (a |^ n);

      

       A3: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume (( Partial_Sums s) . n) = ((1 - (a |^ (n + 1))) / (1 - a));

        

        hence (( Partial_Sums s) . (n + 1)) = (((1 - (a |^ (n + 1))) / (1 - a)) + (s . (n + 1))) by SERIES_1:def 1

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

        .= (((1 - (a |^ (n + 1))) / (1 - a)) + ((a |^ (n + 1)) * ((1 - a) / (1 - a)))) by A1, XCMPLX_1: 60

        .= (((1 - (a |^ (n + 1))) / (1 - a)) + (((a |^ (n + 1)) * (1 - a)) / (1 - a))) by XCMPLX_1: 74

        .= (((1 - (a |^ (n + 1))) + ((a |^ (n + 1)) - ((a |^ (n + 1)) * a))) / (1 - a)) by XCMPLX_1: 62

        .= (((1 - (a |^ (n + 1))) + ((a |^ (n + 1)) - (a |^ ((n + 1) + 1)))) / (1 - a)) by NEWTON: 6

        .= ((1 - (a |^ ((n + 1) + 1))) / (1 - a));

      end;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1

      .= (a |^ 0 ) by A2

      .= 1 by NEWTON: 4

      .= ((1 - a) / (1 - a)) by A1, XCMPLX_1: 60

      .= ((1 - (a |^ ( 0 + 1))) / (1 - a));

      then

       A4: X[ 0 ];

      for n holds X[n] from NAT_1:sch 2( A4, A3);

      hence thesis;

    end;

    theorem :: SERIES_4:11

    (a <> 1 & a <> 0 & for n holds (s . n) = ((1 / a) |^ n)) implies for n holds (( Partial_Sums s) . n) = ((((1 / a) |^ n) - a) / (1 - a))

    proof

      assume that

       A1: a <> 1 and

       A2: a <> 0 ;

      defpred X[ Nat] means (( Partial_Sums s) . $1) = ((((1 / a) |^ $1) - a) / (1 - a));

      assume

       A3: for n holds (s . n) = ((1 / a) |^ n);

      

       A4: (1 - a) <> 0 by A1;

      

       A5: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume (( Partial_Sums s) . n) = ((((1 / a) |^ n) - a) / (1 - a));

        

        hence (( Partial_Sums s) . (n + 1)) = (((((1 / a) |^ n) - a) / (1 - a)) + (s . (n + 1))) by SERIES_1:def 1

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

        .= (((((1 / a) |^ n) - a) / (1 - a)) + (((1 / a) |^ (n + 1)) * ((1 - a) / (1 - a)))) by A4, XCMPLX_1: 60

        .= (((((1 / a) |^ n) - a) / (1 - a)) + ((((1 / a) |^ (n + 1)) * (1 - a)) / (1 - a))) by XCMPLX_1: 74

        .= (((((1 / a) |^ n) - a) + ((((1 / a) |^ (n + 1)) * 1) - (((1 / a) |^ (n + 1)) * a))) / (1 - a)) by XCMPLX_1: 62

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

        .= ((((((1 / a) |^ n) - a) + ((1 / a) |^ (n + 1))) - ((((1 / a) |^ n) * (1 / a)) * a)) / (1 - a)) by NEWTON: 6

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

        .= ((((((1 / a) |^ n) - a) + ((1 / a) |^ (n + 1))) - (((1 / a) |^ n) * 1)) / (1 - a)) by A2, XCMPLX_1: 106

        .= ((((1 / a) |^ (n + 1)) - a) / (1 - a));

      end;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1

      .= ((1 / a) |^ 0 ) by A3

      .= 1 by NEWTON: 4

      .= ((1 - a) / (1 - a)) by A4, XCMPLX_1: 60

      .= ((((1 / a) |^ 0 ) - a) / (1 - a)) by NEWTON: 4;

      then

       A6: X[ 0 ];

      for n holds X[n] from NAT_1:sch 2( A6, A5);

      hence thesis;

    end;

    theorem :: SERIES_4:12

    (for n holds (s . n) = (((10 |^ n) + (2 * n)) + 1)) implies (( Partial_Sums s) . n) = ((((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2))

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) = ((((10 |^ ($1 + 1)) / 9) - (1 / 9)) + (($1 + 1) |^ 2));

      assume

       A1: for n holds (s . n) = (((10 |^ n) + (2 * n)) + 1);

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume (( Partial_Sums s) . n) = ((((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2));

        

        then (( Partial_Sums s) . (n + 1)) = (((((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2)) + (s . (n + 1))) by SERIES_1:def 1

        .= (((((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2)) + (((10 |^ (n + 1)) + (2 * (n + 1))) + 1)) by A1

        .= (((((10 |^ (n + 1)) * 10) / 9) - (1 / 9)) + ((((n + 1) |^ 2) + (2 * n)) + 3))

        .= (((((10 |^ (n + 1)) * 10) / 9) - (1 / 9)) + (((((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2)) + (2 * n)) + 3)) by Lm1

        .= (((((10 |^ (n + 1)) * 10) / 9) - (1 / 9)) + (((((n |^ 2) + (2 * n)) + 1) + (2 * n)) + 3))

        .= (((((10 |^ (n + 1)) * 10) / 9) - (1 / 9)) + (((n |^ 2) + ((2 * n) * 2)) + (2 |^ 2))) by Lm1

        .= (((((10 |^ (n + 1)) * 10) / 9) - (1 / 9)) + ((n + 2) |^ 2)) by Lm1

        .= ((((10 |^ ((n + 1) + 1)) / 9) - (1 / 9)) + ((n + 2) |^ 2)) by NEWTON: 6;

        hence thesis;

      end;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1

      .= (((10 |^ 0 ) + (2 * 0 )) + 1) by A1

      .= (((10 / 9) - (1 / 9)) + 1) by NEWTON: 4

      .= ((((10 |^ ( 0 + 1)) / 9) - (1 / 9)) + 1)

      .= ((((10 |^ ( 0 + 1)) / 9) - (1 / 9)) + (( 0 + 1) |^ 2));

      then

       A3: X[ 0 ];

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

      hence thesis;

    end;

    theorem :: SERIES_4:13

    (for n holds (s . n) = (((2 * n) - 1) + ((1 / 2) |^ n))) implies (( Partial_Sums s) . n) = (((n |^ 2) + 1) - ((1 / 2) |^ n))

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) = ((($1 |^ 2) + 1) - ((1 / 2) |^ $1));

      assume

       A1: for n holds (s . n) = (((2 * n) - 1) + ((1 / 2) |^ n));

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume (( Partial_Sums s) . n) = (((n |^ 2) + 1) - ((1 / 2) |^ n));

        

        then (( Partial_Sums s) . (n + 1)) = ((((n |^ 2) + 1) - ((1 / 2) |^ n)) + (s . (n + 1))) by SERIES_1:def 1

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

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

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

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

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

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

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

        .= ((((n + 1) |^ 2) + 1) - ((1 / 2) |^ (n + 1))) by Lm1;

        hence thesis;

      end;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1

      .= (((2 * 0 ) - 1) + ((1 / 2) |^ 0 )) by A1

      .= (( - 1) + 1) by NEWTON: 4

      .= ((1 - 1) + ( 0 |^ 2)) by NEWTON: 11

      .= ((1 - ((1 / 2) |^ 0 )) + ( 0 |^ 2)) by NEWTON: 4;

      then

       A3: X[ 0 ];

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

      hence thesis;

    end;

    theorem :: SERIES_4:14

    (for n holds (s . n) = (n * ((1 / 2) |^ n))) implies (( Partial_Sums s) . n) = (2 - ((2 + n) * ((1 / 2) |^ n)))

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) = (2 - ((2 + $1) * ((1 / 2) |^ $1)));

      assume

       A1: for n holds (s . n) = (n * ((1 / 2) |^ n));

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume (( Partial_Sums s) . n) = (2 - ((2 + n) * ((1 / 2) |^ n)));

        

        then (( Partial_Sums s) . (n + 1)) = ((2 - ((2 + n) * ((1 / 2) |^ n))) + (s . (n + 1))) by SERIES_1:def 1

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

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

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

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

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

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

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

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

        hence thesis;

      end;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1

      .= ( 0 * ((1 / 2) |^ 0 )) by A1

      .= (2 - ((2 + 0 ) * 1))

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

      then

       A3: X[ 0 ];

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

      hence thesis;

    end;

    theorem :: SERIES_4:15

    (for n holds (s . n) = ((((1 / 2) |^ n) + (2 |^ n)) |^ 2)) implies for n holds (( Partial_Sums s) . n) = (((( - (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3)

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) = (((( - (((1 / 4) |^ $1) / 3)) + ((4 |^ ($1 + 1)) / 3)) + (2 * $1)) + 3);

      assume

       A1: for n holds (s . n) = ((((1 / 2) |^ n) + (2 |^ n)) |^ 2);

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume (( Partial_Sums s) . n) = (((( - (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3);

        

        then (( Partial_Sums s) . (n + 1)) = ((((( - (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3) + (s . (n + 1))) by SERIES_1:def 1

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

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

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

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

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

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

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

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

        hence thesis;

      end;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1

      .= ((((1 / 2) |^ 0 ) + (2 |^ 0 )) |^ 2) by A1

      .= ((1 + (2 |^ 0 )) |^ 2) by NEWTON: 4

      .= ((1 + 1) |^ 2) by NEWTON: 4

      .= (((( - (1 / 3)) + (4 / 3)) + (2 * 0 )) + 3) by Lm1

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

      .= (((( - (((1 / 4) |^ 0 ) / 3)) + ((4 |^ ( 0 + 1)) / 3)) + (2 * 0 )) + 3);

      then

       A3: X[ 0 ];

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

      hence thesis;

    end;

    theorem :: SERIES_4:16

    (for n holds (s . n) = ((((1 / 3) |^ n) + (3 |^ n)) |^ 2)) implies for n holds (( Partial_Sums s) . n) = (((( - (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3)

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) = (((( - (((1 / 9) |^ $1) / 8)) + ((9 |^ ($1 + 1)) / 8)) + (2 * $1)) + 3);

      assume

       A1: for n holds (s . n) = ((((1 / 3) |^ n) + (3 |^ n)) |^ 2);

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume (( Partial_Sums s) . n) = (((( - (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3);

        

        then (( Partial_Sums s) . (n + 1)) = ((((( - (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3) + (s . (n + 1))) by SERIES_1:def 1

        .= ((((( - (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3) + ((((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ 2)) by A1

        .= ((((( - (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3) + ((((1 / 9) |^ (n + 1)) + (9 |^ (n + 1))) + 2)) by Lm3

        .= (((((( - (((1 / 9) |^ n) / 8)) + ((1 / 9) |^ (n + 1))) + ((9 |^ (n + 1)) / 8)) + (9 |^ (n + 1))) + (2 * (n + 1))) + 3)

        .= (((((( - (((1 / 9) |^ n) / 8)) + (((1 / 9) |^ n) * (1 / 9))) + ((9 |^ (n + 1)) / 8)) + (9 |^ (n + 1))) + (2 * (n + 1))) + 3) by NEWTON: 6

        .= ((((( - ((((1 / 9) |^ n) * (1 / 9)) / 8)) + ((9 |^ (n + 1)) / 8)) + (9 |^ (n + 1))) + (2 * (n + 1))) + 3)

        .= ((((( - (((1 / 9) |^ (n + 1)) / 8)) + ((9 |^ (n + 1)) / 8)) + (9 |^ (n + 1))) + (2 * (n + 1))) + 3) by NEWTON: 6

        .= (((( - (((1 / 9) |^ (n + 1)) / 8)) + (((9 |^ (n + 1)) * 9) / 8)) + (2 * (n + 1))) + 3)

        .= (((( - (((1 / 9) |^ (n + 1)) / 8)) + ((9 |^ ((n + 1) + 1)) / 8)) + (2 * (n + 1))) + 3) by NEWTON: 6;

        hence thesis;

      end;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1

      .= ((((1 / 3) |^ 0 ) + (3 |^ 0 )) |^ 2) by A1

      .= ((1 + (3 |^ 0 )) |^ 2) by NEWTON: 4

      .= ((1 + 1) |^ 2) by NEWTON: 4

      .= (((( - (1 / 8)) + (9 / 8)) + (2 * 0 )) + 3) by Lm1

      .= (((( - (((1 / 9) |^ 0 ) / 8)) + (9 / 8)) + (2 * 0 )) + 3) by NEWTON: 4

      .= (((( - (((1 / 9) |^ 0 ) / 8)) + ((9 |^ ( 0 + 1)) / 8)) + (2 * 0 )) + 3);

      then

       A3: X[ 0 ];

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

      hence thesis;

    end;

    theorem :: SERIES_4:17

    (for n holds (s . n) = (n * (2 |^ n))) implies for n holds (( Partial_Sums s) . n) = (((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2)

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) = ((($1 * (2 |^ ($1 + 1))) - (2 |^ ($1 + 1))) + 2);

      assume

       A1: for n holds (s . n) = (n * (2 |^ n));

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume (( Partial_Sums s) . n) = (((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2);

        

        then (( Partial_Sums s) . (n + 1)) = ((((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2) + (s . (n + 1))) by SERIES_1:def 1

        .= ((((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2) + ((n + 1) * (2 |^ (n + 1)))) by A1

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

        .= ((n * (2 |^ ((n + 1) + 1))) + 2) by NEWTON: 6;

        hence thesis;

      end;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1

      .= ( 0 * (2 |^ 0 )) by A1

      .= ((( 0 * (2 |^ ( 0 + 1))) - 2) + 2)

      .= ((( 0 * (2 |^ ( 0 + 1))) - (2 |^ ( 0 + 1))) + 2);

      then

       A3: X[ 0 ];

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

      hence thesis;

    end;

    theorem :: SERIES_4:18

    (for n holds (s . n) = (((2 * n) + 1) * (3 |^ n))) implies for n holds (( Partial_Sums s) . n) = ((n * (3 |^ (n + 1))) + 1)

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) = (($1 * (3 |^ ($1 + 1))) + 1);

      assume

       A1: for n holds (s . n) = (((2 * n) + 1) * (3 |^ n));

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume (( Partial_Sums s) . n) = ((n * (3 |^ (n + 1))) + 1);

        

        then (( Partial_Sums s) . (n + 1)) = (((n * (3 |^ (n + 1))) + 1) + (s . (n + 1))) by SERIES_1:def 1

        .= (((n * (3 |^ (n + 1))) + 1) + (((2 * (n + 1)) + 1) * (3 |^ (n + 1)))) by A1

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

        .= (((n + 1) * (3 |^ ((n + 1) + 1))) + 1) by NEWTON: 6;

        hence thesis;

      end;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1

      .= (((2 * 0 ) + 1) * (3 |^ 0 )) by A1

      .= (( 0 * (3 |^ ( 0 + 1))) + 1) by NEWTON: 4;

      then

       A3: X[ 0 ];

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

      hence thesis;

    end;

    theorem :: SERIES_4:19

    (a <> 1 & for n holds (s . n) = (n * (a |^ n))) implies for n holds (( Partial_Sums s) . n) = (((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a)))

    proof

      assume that

       A1: a <> 1 and

       A2: for n holds (s . n) = (n * (a |^ n));

      defpred X[ Nat] means (( Partial_Sums s) . $1) = (((a * (1 - (a |^ $1))) / ((1 - a) |^ 2)) - (($1 * (a |^ ($1 + 1))) / (1 - a)));

      

       A3: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume (( Partial_Sums s) . n) = (((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a)));

        

        then (( Partial_Sums s) . (n + 1)) = ((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (s . (n + 1))) by SERIES_1:def 1

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

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

        .= (((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a))) by A1, Lm6;

        hence thesis;

      end;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1

      .= ( 0 * (a |^ 0 )) by A2

      .= ((((1 - 1) * a) / ((1 - a) |^ 2)) - (( 0 * (a |^ ( 0 + 1))) / (1 - a)))

      .= ((((1 - (a |^ 0 )) * a) / ((1 - a) |^ 2)) - (( 0 * (a |^ ( 0 + 1))) / (1 - a))) by NEWTON: 4;

      then

       A4: X[ 0 ];

      for n holds X[n] from NAT_1:sch 2( A4, A3);

      hence thesis;

    end;

    theorem :: SERIES_4:20

    (for n holds (s . n) = (1 / ((2 -Root (n + 1)) + (2 -Root n)))) implies (( Partial_Sums s) . n) = (2 -Root (n + 1))

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) = (2 -Root ($1 + 1));

      assume

       A1: for n holds (s . n) = (1 / ((2 -Root (n + 1)) + (2 -Root n)));

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume (( Partial_Sums s) . n) = (2 -Root (n + 1));

        

        then (( Partial_Sums s) . (n + 1)) = ((2 -Root (n + 1)) + (s . (n + 1))) by SERIES_1:def 1

        .= ((2 -Root (n + 1)) + (1 / ((2 -Root ((n + 1) + 1)) + (2 -Root (n + 1))))) by A1

        .= ((2 -Root (n + 1)) + ((2 -Root (n + 2)) - (2 -Root (n + 1)))) by Lm7

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

        hence thesis;

      end;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1

      .= (1 / ((2 -Root ( 0 + 1)) + (2 -Root 0 ))) by A1

      .= (1 / ((2 -Root ( 0 + 1)) + 0 )) by PREPOWER:def 2

      .= (1 / 1) by PREPOWER: 20

      .= (2 -Root ( 0 + 1)) by PREPOWER: 20;

      then

       A3: X[ 0 ];

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

      hence thesis;

    end;

    theorem :: SERIES_4:21

    (for n holds (s . n) = ((2 |^ n) + ((1 / 2) |^ n))) implies for n holds (( Partial_Sums s) . n) = (((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1)

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) = (((2 |^ ($1 + 1)) - ((1 / 2) |^ $1)) + 1);

      assume

       A1: for n holds (s . n) = ((2 |^ n) + ((1 / 2) |^ n));

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume (( Partial_Sums s) . n) = (((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1);

        

        then (( Partial_Sums s) . (n + 1)) = ((((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1) + (s . (n + 1))) by SERIES_1:def 1

        .= ((((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1) + ((2 |^ (n + 1)) + ((1 / 2) |^ (n + 1)))) by A1

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

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

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

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

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

        .= ((( - ((1 / 2) |^ (n + 1))) + 1) + (2 |^ ((n + 1) + 1))) by NEWTON: 6;

        hence thesis;

      end;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1

      .= ((2 |^ 0 ) + ((1 / 2) |^ 0 )) by A1

      .= (1 + ((1 / 2) |^ 0 )) by NEWTON: 4

      .= ((2 - 1) + 1) by NEWTON: 4

      .= (((2 |^ ( 0 + 1)) - 1) + 1)

      .= (((2 |^ ( 0 + 1)) - ((1 / 2) |^ 0 )) + 1) by NEWTON: 4;

      then

       A3: X[ 0 ];

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

      hence thesis;

    end;

    theorem :: SERIES_4:22

    (for n holds (s . n) = (((n ! ) * n) + (n / ((n + 1) ! )))) implies for n st n >= 1 holds (( Partial_Sums s) . n) = (((n + 1) ! ) - (1 / ((n + 1) ! )))

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) = ((($1 + 1) ! ) - (1 / (($1 + 1) ! )));

      assume

       A1: for n holds (s . n) = (((n ! ) * n) + (n / ((n + 1) ! )));

      

      then

       A2: (s . 0 ) = ((( 0 ! ) * 0 ) + ( 0 / (( 0 + 1) ! )))

      .= 0 ;

      

       A3: for n be Nat st n >= 1 & X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        assume that n >= 1 and

         A4: (( Partial_Sums s) . n) = (((n + 1) ! ) - (1 / ((n + 1) ! )));

        (( Partial_Sums s) . (n + 1)) = ((((n + 1) ! ) - (1 / ((n + 1) ! ))) + (s . (n + 1))) by A4, SERIES_1:def 1

        .= ((((n + 1) ! ) - (1 / ((n + 1) ! ))) + ((((n + 1) ! ) * (n + 1)) + ((n + 1) / (((n + 1) + 1) ! )))) by A1

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

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

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

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

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

        .= ((((n + 1) + 1) ! ) - (1 / (((n + 1) + 1) ! ))) by NEWTON: 15;

        hence thesis;

      end;

      (( Partial_Sums s) . (1 + 0 )) = ((( Partial_Sums s) . 0 ) + (s . (1 + 0 ))) by SERIES_1:def 1

      .= ( 0 + (s . 1)) by A2, SERIES_1:def 1

      .= (((1 ! ) * 1) + (1 / ((1 + 1) ! ))) by A1

      .= (((((1 + 1) ! ) - 1) + 1) - (1 / ((1 + 1) ! ))) by NEWTON: 13, NEWTON: 14;

      then

       A5: X[1];

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

      hence thesis;

    end;

    theorem :: SERIES_4:23

    (a <> 1 & for n st n >= 1 holds (s . n) = ((a / (a - 1)) |^ n) & (s . 0 ) = 0 ) implies for n st n >= 1 holds (( Partial_Sums s) . n) = (a * (((a / (a - 1)) |^ n) - 1))

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) = (a * (((a / (a - 1)) |^ $1) - 1));

      assume a <> 1;

      then

       A1: (a - 1) <> 0 ;

      assume

       A2: for n st n >= 1 holds (s . n) = ((a / (a - 1)) |^ n) & (s . 0 ) = 0 ;

      

       A3: for n be Nat st n >= 1 & X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        assume that n >= 1 and

         A4: (( Partial_Sums s) . n) = (a * (((a / (a - 1)) |^ n) - 1));

        

         A5: (n + 1) >= 1 by NAT_1: 11;

        (( Partial_Sums s) . (n + 1)) = ((a * (((a / (a - 1)) |^ n) - 1)) + (s . (n + 1))) by A4, SERIES_1:def 1

        .= (((a * ((a / (a - 1)) |^ n)) - a) + ((a / (a - 1)) |^ (n + 1))) by A2, A5

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

        .= (((a * ((a / (a - 1)) |^ n)) + (((a / (a - 1)) |^ n) * (a / (a - 1)))) - a) by NEWTON: 6

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

        .= ((((a / (a - 1)) |^ n) * ((a * 1) + (a * (1 / (a - 1))))) - a) by XCMPLX_1: 99

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

        .= ((((a / (a - 1)) |^ n) * (a * (((a - 1) / (a - 1)) + (1 / (a - 1))))) - a) by A1, XCMPLX_1: 60

        .= ((((a / (a - 1)) |^ n) * (a * (((a - 1) + 1) / (a - 1)))) - a) by XCMPLX_1: 62

        .= ((a * (((a / (a - 1)) |^ n) * (a / (a - 1)))) - a)

        .= ((a * ((a / (a - 1)) |^ (n + 1))) - a) by NEWTON: 6

        .= (a * (((a / (a - 1)) |^ (n + 1)) - 1));

        hence thesis;

      end;

      (( Partial_Sums s) . ( 0 + 1)) = ((( Partial_Sums s) . 0 ) + (s . ( 0 + 1))) by SERIES_1:def 1

      .= ((s . 0 ) + (s . 1)) by SERIES_1:def 1

      .= ( 0 + (s . 1)) by A2

      .= ( 0 + ((a / (a - 1)) |^ 1)) by A2

      .= (((a / (a - 1)) + a) - a)

      .= (((a * (1 / (a - 1))) + (a * 1)) - a) by XCMPLX_1: 99

      .= (((a * (1 / (a - 1))) + (a * ((a - 1) / (a - 1)))) - a) by A1, XCMPLX_1: 60

      .= ((a * ((1 / (a - 1)) + ((a - 1) / (a - 1)))) - a)

      .= ((a * ((1 + (a - 1)) / (a - 1))) - a) by XCMPLX_1: 62

      .= (a * ((a / (a - 1)) - 1))

      .= (a * (((a / (a - 1)) |^ 1) - 1));

      then

       A6: X[1];

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

      hence thesis;

    end;

    theorem :: SERIES_4:24

    (for n st n >= 1 holds (s . n) = ((2 |^ n) * (((3 * n) - 1) / 4)) & (s . 0 ) = 0 ) implies for n st n >= 1 holds (( Partial_Sums s) . n) = (((2 |^ n) * (((3 * n) - 4) / 2)) + 2)

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) = (((2 |^ $1) * (((3 * $1) - 4) / 2)) + 2);

      assume

       A1: for n st n >= 1 holds (s . n) = ((2 |^ n) * (((3 * n) - 1) / 4)) & (s . 0 ) = 0 ;

      

       A2: for n be Nat st n >= 1 & X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        assume that n >= 1 and

         A3: (( Partial_Sums s) . n) = (((2 |^ n) * (((3 * n) - 4) / 2)) + 2);

        

         A4: (n + 1) >= 1 by NAT_1: 11;

        (( Partial_Sums s) . (n + 1)) = ((((2 |^ n) * (((3 * n) - 4) / 2)) + 2) + (s . (n + 1))) by A3, SERIES_1:def 1

        .= ((((2 |^ n) * (((3 * n) - 4) / 2)) + 2) + ((2 |^ (n + 1)) * (((3 * (n + 1)) - 1) / 4))) by A1, A4

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

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

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

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

        hence thesis;

      end;

      (( Partial_Sums s) . (1 + 0 )) = ((( Partial_Sums s) . 0 ) + (s . (1 + 0 ))) by SERIES_1:def 1

      .= ((s . 0 ) + (s . 1)) by SERIES_1:def 1

      .= ( 0 + (s . 1)) by A1

      .= ((2 |^ 1) * (((3 * 1) - 1) / 4)) by A1

      .= (2 * (1 / 2))

      .= ((((3 - 4) / 2) * 2) + 2)

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

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

      then

       A5: X[1];

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

      hence thesis;

    end;

    theorem :: SERIES_4:25

    (for n holds (s . n) = ((n + 1) / (n + 2))) implies (( Partial_Product s) . n) = (1 / (n + 2))

    proof

      defpred X[ Nat] means (( Partial_Product s) . $1) = (1 / ($1 + 2));

      assume

       A1: for n holds (s . n) = ((n + 1) / (n + 2));

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume (( Partial_Product s) . n) = (1 / (n + 2));

        

        then (( Partial_Product s) . (n + 1)) = ((1 / (n + 2)) * (s . (n + 1))) by SERIES_3:def 1

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

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

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

        hence thesis;

      end;

      (( Partial_Product s) . 0 ) = (s . 0 ) by SERIES_3:def 1

      .= (( 0 + 1) / ( 0 + 2)) by A1

      .= (1 / ( 0 + 2));

      then

       A3: X[ 0 ];

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

      hence thesis;

    end;

    theorem :: SERIES_4:26

    (for n holds (s . n) = (1 / (n + 1))) implies (( Partial_Product s) . n) = (1 / ((n + 1) ! ))

    proof

      defpred X[ Nat] means (( Partial_Product s) . $1) = (1 / (($1 + 1) ! ));

      assume

       A1: for n holds (s . n) = (1 / (n + 1));

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume (( Partial_Product s) . n) = (1 / ((n + 1) ! ));

        

        then (( Partial_Product s) . (n + 1)) = ((1 / ((n + 1) ! )) * (s . (n + 1))) by SERIES_3:def 1

        .= ((1 / ((n + 1) ! )) * (1 / ((n + 1) + 1))) by A1

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

        .= (1 / (((n + 1) ! ) * ((n + 1) + 1))) by XCMPLX_1: 78

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

        hence thesis;

      end;

      (( Partial_Product s) . 0 ) = (s . 0 ) by SERIES_3:def 1

      .= (1 / (( 0 + 1) ! )) by A1, NEWTON: 13;

      then

       A3: X[ 0 ];

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

      hence thesis;

    end;

    theorem :: SERIES_4:27

    (for n st n >= 1 holds (s . n) = n & (s . 0 ) = 1) implies for n st n >= 1 holds (( Partial_Product s) . n) = (n ! )

    proof

      defpred X[ Nat] means (( Partial_Product s) . $1) = ($1 ! );

      assume

       A1: for n st n >= 1 holds (s . n) = n & (s . 0 ) = 1;

      

       A2: for n be Nat st n >= 1 & X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        assume that n >= 1 and

         A3: (( Partial_Product s) . n) = (n ! );

        

         A4: (n + 1) >= 1 by NAT_1: 11;

        (( Partial_Product s) . (n + 1)) = ((( Partial_Product s) . n) * (s . (n + 1))) by SERIES_3:def 1

        .= ((n ! ) * (n + 1)) by A1, A3, A4

        .= ((n + 1) ! ) by NEWTON: 15;

        hence thesis;

      end;

      (( Partial_Product s) . (1 + 0 )) = ((( Partial_Product s) . 0 ) * (s . (1 + 0 ))) by SERIES_3:def 1

      .= ((s . 0 ) * (s . (1 + 0 ))) by SERIES_3:def 1

      .= (1 * (s . 1)) by A1

      .= (1 ! ) by A1, NEWTON: 13;

      then

       A5: X[1];

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

      hence thesis;

    end;

    theorem :: SERIES_4:28

    (for n st n >= 1 holds (s . n) = (a / n) & (s . 0 ) = 1) implies for n st n >= 1 holds (( Partial_Product s) . n) = ((a |^ n) / (n ! ))

    proof

      defpred X[ Nat] means (( Partial_Product s) . $1) = ((a |^ $1) / ($1 ! ));

      assume

       A1: for n st n >= 1 holds (s . n) = (a / n) & (s . 0 ) = 1;

      

       A2: for n be Nat st n >= 1 & X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        assume that n >= 1 and

         A3: (( Partial_Product s) . n) = ((a |^ n) / (n ! ));

        

         A4: (n + 1) >= 1 by NAT_1: 11;

        (( Partial_Product s) . (n + 1)) = ((( Partial_Product s) . n) * (s . (n + 1))) by SERIES_3:def 1

        .= (((a |^ n) / (n ! )) * (a / (n + 1))) by A1, A3, A4

        .= (((a |^ n) * a) / ((n ! ) * (n + 1))) by XCMPLX_1: 76

        .= ((a |^ (n + 1)) / ((n ! ) * (n + 1))) by NEWTON: 6

        .= ((a |^ (n + 1)) / ((n + 1) ! )) by NEWTON: 15;

        hence thesis;

      end;

      (( Partial_Product s) . (1 + 0 )) = ((( Partial_Product s) . 0 ) * (s . (1 + 0 ))) by SERIES_3:def 1

      .= ((s . 0 ) * (s . (1 + 0 ))) by SERIES_3:def 1

      .= (1 * (s . 1)) by A1

      .= ((1 * a) / 1) by A1

      .= ((a |^ 1) / (1 ! )) by NEWTON: 13;

      then

       A5: X[1];

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

      hence thesis;

    end;

    theorem :: SERIES_4:29

    (for n st n >= 1 holds (s . n) = a & (s . 0 ) = 1) implies for n st n >= 1 holds (( Partial_Product s) . n) = (a |^ n)

    proof

      defpred X[ Nat] means (( Partial_Product s) . $1) = (a |^ $1);

      assume

       A1: for n st n >= 1 holds (s . n) = a & (s . 0 ) = 1;

      

       A2: for n be Nat st n >= 1 & X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        assume that n >= 1 and

         A3: (( Partial_Product s) . n) = (a |^ n);

        

         A4: (n + 1) >= 1 by NAT_1: 11;

        (( Partial_Product s) . (n + 1)) = ((( Partial_Product s) . n) * (s . (n + 1))) by SERIES_3:def 1

        .= ((a |^ n) * a) by A1, A3, A4

        .= (a |^ (n + 1)) by NEWTON: 6;

        hence thesis;

      end;

      (( Partial_Product s) . (1 + 0 )) = ((( Partial_Product s) . 0 ) * (s . (1 + 0 ))) by SERIES_3:def 1

      .= ((s . 0 ) * (s . (1 + 0 ))) by SERIES_3:def 1

      .= (1 * (s . 1)) by A1

      .= (1 * a) by A1

      .= (a |^ 1);

      then

       A5: X[1];

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

      hence thesis;

    end;

    theorem :: SERIES_4:30

    (for n st n >= 2 holds (s . n) = (1 - (1 / (n |^ 2))) & (s . 0 ) = 1 & (s . 1) = 1) implies for n st n >= 2 holds (( Partial_Product s) . n) = ((n + 1) / (2 * n))

    proof

      defpred X[ Nat] means (( Partial_Product s) . $1) = (($1 + 1) / (2 * $1));

      assume

       A1: for n st n >= 2 holds (s . n) = (1 - (1 / (n |^ 2))) & (s . 0 ) = 1 & (s . 1) = 1;

      

       A2: for n be Nat st n >= 2 & X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        assume that

         A3: n >= 2 and

         A4: (( Partial_Product s) . n) = ((n + 1) / (2 * n));

        

         A5: (n + 1) > (1 + 1) by A3, NAT_1: 13;

        ((n + 1) * (n + 1)) <> 0 ;

        then

         A6: ((n + 1) |^ 2) <> 0 by WSIERP_1: 1;

        (( Partial_Product s) . (n + 1)) = ((( Partial_Product s) . n) * (s . (n + 1))) by SERIES_3:def 1

        .= (((n + 1) / (2 * n)) * (1 - (1 / ((n + 1) |^ 2)))) by A1, A4, A5

        .= (((n + 1) / (2 * n)) * ((((n + 1) |^ 2) / ((n + 1) |^ 2)) - (1 / ((n + 1) |^ 2)))) by A6, XCMPLX_1: 60

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

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

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

        .= (((n + 1) * (n * (n + 2))) / ((2 * n) * ((n + 1) |^ 2))) by XCMPLX_1: 76

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

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

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

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

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

        .= ((1 * 1) * ((n + 2) / (2 * (n + 1)))) by A3, XCMPLX_1: 60

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

        hence thesis;

      end;

      (( Partial_Product s) . (1 + 1)) = ((( Partial_Product s) . (1 + 0 )) * (s . 2)) by SERIES_3:def 1

      .= (((( Partial_Product s) . 0 ) * (s . 1)) * (s . 2)) by SERIES_3:def 1

      .= (((s . 0 ) * (s . 1)) * (s . 2)) by SERIES_3:def 1

      .= ((1 * (s . 1)) * (s . 2)) by A1

      .= ((1 * 1) * (s . 2)) by A1

      .= (1 - (1 / 4)) by A1, Lm1

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

      then

       A7: X[2];

      for n be Nat st n >= 2 holds X[n] from NAT_1:sch 8( A7, A2);

      hence thesis;

    end;