let x, y be Real; ( x + y <> 0 implies (x + y) |^ 4 = ((x |^ 4) + ((((4 * y) * (x |^ 3)) + ((6 * (y ^2)) * (x ^2))) + ((4 * (y |^ 3)) * x))) + (y |^ 4) )
set g = (((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x;
set h = (((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y;
set p = y |^ 3;
set q = x |^ 3;
set u = x |^ 4;
set v = y |^ 4;
A1:
(((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x = (((x |^ 3) * x) + ((((3 * y) * (x ^2)) + ((3 * (y ^2)) * x)) * x)) + ((y |^ 3) * x)
;
A2:
y |^ 3 = (y ^2) * y
by Th4;
assume
x + y <> 0
; (x + y) |^ 4 = ((x |^ 4) + ((((4 * y) * (x |^ 3)) + ((6 * (y ^2)) * (x ^2))) + ((4 * (y |^ 3)) * x))) + (y |^ 4)
then A3:
(x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y)
by Th5;
(((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y =
(((x |^ 3) * y) + ((((3 * y) * (x ^2)) + ((3 * (y ^2)) * x)) * y)) + ((y |^ 3) * y)
.=
(((x |^ 3) * y) + ((((3 * y) * (x ^2)) + ((3 * (y ^2)) * x)) * y)) + (y |^ 4)
by Th4
;
then (x + y) |^ 4 =
(((x |^ 4) + (((3 * y) * ((x ^2) * x)) - ((- ((3 * (y ^2)) * x)) * x))) + ((y |^ 3) * x)) + ((((x |^ 3) * y) + ((((3 * y) * (x ^2)) + ((3 * (y ^2)) * x)) * y)) + (y |^ 4))
by A3, A1, Th4
.=
(((x |^ 4) + (((3 * y) * (x |^ 3)) - (- ((3 * (y ^2)) * (x ^2))))) + ((y |^ 3) * x)) + ((((x |^ 3) * y) + ((((3 * y) * (x ^2)) + ((3 * (y ^2)) * x)) * y)) + (y |^ 4))
by Th4
.=
(((x |^ 4) + ((3 * y) * (x |^ 3))) + (((3 * (y ^2)) * (x ^2)) + ((y |^ 3) * x))) + ((((x |^ 3) * y) + (((3 * (y ^2)) * (x ^2)) + (((3 * (y ^2)) * x) * y))) + (y |^ 4))
;
hence
(x + y) |^ 4 = ((x |^ 4) + ((((4 * y) * (x |^ 3)) + ((6 * (y ^2)) * (x ^2))) + ((4 * (y |^ 3)) * x))) + (y |^ 4)
by A2; verum