let n be Nat; :: thesis: for a being Real st a <> 0 holds
(((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 2 = (((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2
let a be Real; :: thesis: ( a <> 0 implies (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 2 = (((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2 )
assume A1: a <> 0 ; :: thesis: (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 2 = (((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2
(((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 (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 2 = (((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2 ; :: thesis: verum