let y, h be real number ; :: thesis: (y + h) |^ 3 = ((y |^ 3) + (((3 * h) * (y ^2 )) + ((3 * (h ^2 )) * y))) + (h |^ 3)
A1: (y + h) |^ 3 = (y + h) |^ (2 + 1) ;
A2: (y + h) |^ 3 = ((y + h) |^ (1 + 1)) * (y + h) by A1, NEWTON:11
.= (((y + h) |^ 1) * (y + h)) * (y + h) by NEWTON:11
.= ((y + h) |^ 1) * ((y + h) ^2 )
.= ((y + h) to_power 1) * (((y ^2 ) + ((2 * y) * h)) + (h ^2 )) by POWER:46
.= (y + h) * (((y ^2 ) + ((2 * y) * h)) + (h ^2 )) by POWER:30
.= ((y * (y ^2 )) + (((3 * h) * (y ^2 )) + (((2 + 1) * (h ^2 )) * y))) + (h * (h ^2 )) ;
y |^ 3 = y |^ (2 + 1)
.= (y |^ (1 + 1)) * y by NEWTON:11
.= ((y |^ 1) * y) * y by NEWTON:11
.= (y |^ 1) * (y ^2 ) ;
then A3: y |^ 3 = (y to_power 1) * (y ^2 ) by POWER:46;
h |^ 3 = h |^ (2 + 1)
.= (h |^ (1 + 1)) * h by NEWTON:11
.= ((h |^ 1) * h) * h by NEWTON:11
.= (h |^ 1) * (h ^2 )
.= (h to_power 1) * (h ^2 ) by POWER:46
.= h * (h ^2 ) by POWER:30 ;
hence (y + h) |^ 3 = ((y |^ 3) + (((3 * h) * (y ^2 )) + ((3 * (h ^2 )) * y))) + (h |^ 3) by A2, A3, POWER:30; :: thesis: verum