let a, b, c be positive Real; (((((((2 * (a ^2)) * (sqrt (b * c))) * 2) * (b ^2)) * (sqrt (a * c))) * 2) * (c ^2)) * (sqrt (a * b)) = (((2 * a) * b) * c) |^ 3
(((((((2 * (a ^2)) * (sqrt (b * c))) * 2) * (b ^2)) * (sqrt (a * c))) * 2) * (c ^2)) * (sqrt (a * b)) =
(((((((2 ^2) * 2) * (a ^2)) * (b ^2)) * (c ^2)) * (sqrt (b * c))) * (sqrt (a * c))) * (sqrt (a * b))
.=
(((((((2 |^ 2) * 2) * (a ^2)) * (b ^2)) * (c ^2)) * (sqrt (b * c))) * (sqrt (a * c))) * (sqrt (a * b))
by NEWTON:81
.=
((((((2 |^ (2 + 1)) * (a ^2)) * (b ^2)) * (c ^2)) * (sqrt (b * c))) * (sqrt (a * c))) * (sqrt (a * b))
by NEWTON:6
.=
(((((2 |^ 3) * (a ^2)) * (b ^2)) * (c ^2)) * ((sqrt (b * c)) * (sqrt (a * c)))) * (sqrt (a * b))
.=
(((((2 |^ 3) * (a ^2)) * (b ^2)) * (c ^2)) * (sqrt ((b * c) * (a * c)))) * (sqrt (a * b))
by SQUARE_1:29
.=
((((2 |^ 3) * (a ^2)) * (b ^2)) * (c ^2)) * ((sqrt (((b * c) * a) * c)) * (sqrt (a * b)))
.=
((((2 |^ 3) * (a ^2)) * (b ^2)) * (c ^2)) * (sqrt ((((b * c) * a) * c) * (a * b)))
by SQUARE_1:29
.=
((((2 |^ 3) * (a ^2)) * (b ^2)) * (c ^2)) * (sqrt (((a * b) * c) ^2))
.=
((((2 |^ 3) * (a ^2)) * (b ^2)) * (c ^2)) * ((a * b) * c)
by SQUARE_1:22
.=
(((2 |^ 3) * ((a ^2) * a)) * ((b ^2) * b)) * ((c ^2) * c)
.=
(((2 |^ 3) * ((a |^ 2) * a)) * ((b ^2) * b)) * ((c ^2) * c)
by NEWTON:81
.=
(((2 |^ 3) * ((a |^ 2) * a)) * ((b |^ 2) * b)) * ((c ^2) * c)
by NEWTON:81
.=
(((2 |^ 3) * ((a |^ 2) * a)) * ((b |^ 2) * b)) * ((c |^ 2) * c)
by NEWTON:81
.=
(((2 |^ 3) * (a |^ (2 + 1))) * ((b |^ 2) * b)) * ((c |^ 2) * c)
by NEWTON:6
.=
(((2 |^ 3) * (a |^ 3)) * (b |^ 3)) * ((c |^ 2) * c)
by NEWTON:6
.=
(((2 |^ 3) * (a |^ 3)) * (b |^ 3)) * (c |^ (2 + 1))
by NEWTON:6
.=
(((2 * a) |^ 3) * (b |^ 3)) * (c |^ 3)
by NEWTON:7
.=
(((2 * a) * b) |^ 3) * (c |^ 3)
by NEWTON:7
.=
(((2 * a) * b) * c) |^ 3
by NEWTON:7
;
hence
(((((((2 * (a ^2)) * (sqrt (b * c))) * 2) * (b ^2)) * (sqrt (a * c))) * 2) * (c ^2)) * (sqrt (a * b)) = (((2 * a) * b) * c) |^ 3
; verum