let p be Polynomial of F_Real; :: thesis: poly_diff (Leading-Monomial p) = (0_. F_Real) +* (((len p) -' 2),((p . ((len p) -' 1)) * ((len p) -' 1)))
set l = Leading-Monomial p;
set m = (len p) -' 1;
set k = (len p) -' 2;
reconsider a = (p . ((len p) -' 1)) * ((len p) -' 1) as Element of F_Real by XREAL_0:def 1;
set f = (0_. F_Real) +* (((len p) -' 2),a);
poly_diff (Leading-Monomial p) = (0_. F_Real) +* (((len p) -' 2),a)
proof
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (poly_diff (Leading-Monomial p)) . n = ((0_. F_Real) +* (((len p) -' 2),a)) . n
A1: (poly_diff (Leading-Monomial p)) . n = ((Leading-Monomial p) . (n + 1)) * (n + 1) by Def5;
A2: dom (0_. F_Real) = NAT ;
per cases ( len p = 0 or len p = 1 or len p > 1 ) by NAT_1:53;
suppose A3: ( len p = 0 or len p = 1 ) ; :: thesis: (poly_diff (Leading-Monomial p)) . n = ((0_. F_Real) +* (((len p) -' 2),a)) . n
1 - 1 >= 0 ;
then A4: 1 -' 1 = 0 by XREAL_0:def 2;
1 - 2 < 0 ;
then A5: (len p) -' 2 = 0 by A3, XREAL_0:def 2;
0 -' 1 = 0 ;
then A6: (Leading-Monomial p) . (n + 1) = 0. F_Real by A3, A4, POLYNOM4:def 1;
now :: thesis: ((0_. F_Real) +* (((len p) -' 2),a)) . n = 0. F_Real
per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: ((0_. F_Real) +* (((len p) -' 2),a)) . n = 0. F_Real
hence ((0_. F_Real) +* (((len p) -' 2),a)) . n = 0. F_Real by A2, A3, A4, A5, FUNCT_7:31; :: thesis: verum
end;
suppose n <> 0 ; :: thesis: ((0_. F_Real) +* (((len p) -' 2),a)) . n = 0. F_Real
hence ((0_. F_Real) +* (((len p) -' 2),a)) . n = (0_. F_Real) . n by A5, FUNCT_7:32
.= 0. F_Real ;
:: thesis: verum
end;
end;
end;
hence (poly_diff (Leading-Monomial p)) . n = ((0_. F_Real) +* (((len p) -' 2),a)) . n by A1, A6; :: thesis: verum
end;
suppose A7: len p > 1 ; :: thesis: (poly_diff (Leading-Monomial p)) . n = ((0_. F_Real) +* (((len p) -' 2),a)) . n
then A8: (len p) - 1 > 1 - 1 by XREAL_1:14;
per cases ( (len p) -' 1 = n + 1 or (len p) -' 1 <> n + 1 ) ;
suppose A9: (len p) -' 1 = n + 1 ; :: thesis: (poly_diff (Leading-Monomial p)) . n = ((0_. F_Real) +* (((len p) -' 2),a)) . n
then A10: (Leading-Monomial p) . (n + 1) = p . ((len p) -' 1) by POLYNOM4:def 1;
(len p) -' 2 = ((len p) -' 1) -' 1 by NAT_D:45;
then ((len p) -' 2) + 1 = n + 1 by A9, NAT_D:34;
hence (poly_diff (Leading-Monomial p)) . n = ((0_. F_Real) +* (((len p) -' 2),a)) . n by A1, A2, A9, A10, FUNCT_7:31; :: thesis: verum
end;
suppose A11: (len p) -' 1 <> n + 1 ; :: thesis: (poly_diff (Leading-Monomial p)) . n = ((0_. F_Real) +* (((len p) -' 2),a)) . n
then A12: (Leading-Monomial p) . (n + 1) = 0. F_Real by POLYNOM4:def 1;
A13: (len p) - 2 <> n by A8, A11, XREAL_0:def 2;
(len p) - 2 > 1 - 2 by A7, XREAL_1:14;
then (len p) - 2 >= (- 1) + 1 by INT_1:7;
then (len p) -' 2 = (len p) - 2 by XREAL_0:def 2;
hence ((0_. F_Real) +* (((len p) -' 2),a)) . n = (0_. F_Real) . n by A13, FUNCT_7:32
.= (poly_diff (Leading-Monomial p)) . n by A1, A12 ;
:: thesis: verum
end;
end;
end;
end;
end;
hence poly_diff (Leading-Monomial p) = (0_. F_Real) +* (((len p) -' 2),((p . ((len p) -' 1)) * ((len p) -' 1))) ; :: thesis: verum