let n be Nat; for a being Real st a <> 1 holds
((((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))
let a be Real; ( 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)) )
assume
a <> 1
; ((((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))
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
((((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))
; verum