let t be Real; :: thesis: for n being Nat
for e being Element of F_Real st 1 <= n & e = 2 * (cos t) holds
ex p being INT -valued monic Polynomial of F_Real st
( eval (p,e) = 2 * (cos (n * t)) & deg p = n & ( n = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( n = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )
let n be Nat; :: thesis: for e being Element of F_Real st 1 <= n & e = 2 * (cos t) holds
ex p being INT -valued monic Polynomial of F_Real st
( eval (p,e) = 2 * (cos (n * t)) & deg p = n & ( n = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( n = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )
let e be Element of F_Real; :: thesis: ( 1 <= n & e = 2 * (cos t) implies ex p being INT -valued monic Polynomial of F_Real st
( eval (p,e) = 2 * (cos (n * t)) & deg p = n & ( n = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( n = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) ) )
assume that
A1: 1 <= n and
A2: e = 2 * (cos t) ; :: thesis: ex p being INT -valued monic Polynomial of F_Real st
( eval (p,e) = 2 * (cos (n * t)) & deg p = n & ( n = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( n = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )
defpred S₁[ Nat] means ( 1 <= $1 implies ex p being INT -valued monic Polynomial of F_Real st
( eval (p,e) = 2 * (cos ($1 * t)) & deg p = $1 & ( $1 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( $1 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) ) );
A3: S₁[1]

proof

assume 1 <= 1 ; :: thesis: ex p being INT -valued monic Polynomial of F_Real st
( eval (p,e) = 2 * (cos (1 * t)) & deg p = 1 & ( 1 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( 1 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )
reconsider p = <%(0. F_Real),(1. F_Real)%> as INT -valued monic Polynomial of F_Real ;
take p ; :: thesis: ( eval (p,e) = 2 * (cos (1 * t)) & deg p = 1 & ( 1 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( 1 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )
thus eval (p,e) = 2 * (cos (1 * t)) by A2, POLYNOM5:48; :: thesis: ( deg p = 1 & ( 1 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( 1 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )
len p = 2 by POLYNOM5:40;
hence deg p = 1 ; :: thesis: ( ( 1 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( 1 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )
thus ( ( 1 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( 1 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) ) ; :: thesis: verum

end;

A4: S₁[2]

proof

assume 1 <= 2 ; :: thesis: ex p being INT -valued monic Polynomial of F_Real st
( eval (p,e) = 2 * (cos (2 * t)) & deg p = 2 & ( 2 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( 2 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )
reconsider r = - 2 as Element of F_Real by XREAL_0:def 1;
reconsider p = <%r,(0. F_Real),(1. F_Real)%> as INT -valued monic Polynomial of F_Real ;
take p ; :: thesis: ( eval (p,e) = 2 * (cos (2 * t)) & deg p = 2 & ( 2 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( 2 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )
cos (2 * t) = (2 * ((cos t) ^2)) - 1 by SIN_COS5:7;
hence 2 * (cos (2 * t)) = (r + ((0. F_Real) * e)) + (((1. F_Real) * e) * e) by A2
.= eval (p,e) by Th36 ;
:: thesis: ( deg p = 2 & ( 2 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( 2 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )
len p = 3 by Th26;
hence deg p = 2 ; :: thesis: ( ( 2 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( 2 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )
thus ( ( 2 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( 2 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) ) ; :: thesis: verum

end;

A5: for k being non zero Nat st S₁[k] & S₁[k + 1] holds
S₁[k + 2]

proof

let k be non zero Nat; :: thesis: ( S₁[k] & S₁[k + 1] implies S₁[k + 2] )
assume that
A6: S₁[k] and
A7: S₁[k + 1] and
1 <= k + 2 ; :: thesis: ex p being INT -valued monic Polynomial of F_Real st
( eval (p,e) = 2 * (cos ((k + 2) * t)) & deg p = k + 2 & ( k + 2 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( k + 2 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )

per cases ( k + 2 = 1 or k + 2 = 2 or ( k + 2 <> 1 & k + 2 <> 2 ) ) ;

suppose k + 2 = 1 ; :: thesis: ex p being INT -valued monic Polynomial of F_Real st
( eval (p,e) = 2 * (cos ((k + 2) * t)) & deg p = k + 2 & ( k + 2 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( k + 2 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )

then k = - 1 ;
hence ex p being INT -valued monic Polynomial of F_Real st
( eval (p,e) = 2 * (cos ((k + 2) * t)) & deg p = k + 2 & ( k + 2 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( k + 2 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) ) ; :: thesis: verum

end;

suppose k + 2 = 2 ; :: thesis: ex p being INT -valued monic Polynomial of F_Real st
( eval (p,e) = 2 * (cos ((k + 2) * t)) & deg p = k + 2 & ( k + 2 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( k + 2 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )

hence ex p being INT -valued monic Polynomial of F_Real st
( eval (p,e) = 2 * (cos ((k + 2) * t)) & deg p = k + 2 & ( k + 2 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( k + 2 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) ) ; :: thesis: verum

end;

suppose A8: ( k + 2 <> 1 & k + 2 <> 2 ) ; :: thesis: ex p being INT -valued monic Polynomial of F_Real st
( eval (p,e) = 2 * (cos ((k + 2) * t)) & deg p = k + 2 & ( k + 2 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( k + 2 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )

A9: 0 + 1 <= k by NAT_1:13;
then consider p2 being INT -valued monic Polynomial of F_Real such that
A10: eval (p2,e) = 2 * (cos (k * t)) and
A11: deg p2 = k by A6;
consider p1 being INT -valued monic Polynomial of F_Real such that
A12: eval (p1,e) = 2 * (cos ((k + 1) * t)) and
A13: deg p1 = k + 1 by A7, A9, NAT_1:13;
set f = <%(0. F_Real),(1. F_Real)%>;
set p = (<%(0. F_Real),(1. F_Real)%> *' p1) - p2;
p1 is non-zero ;
then A14: len (<%(0. F_Real),(1. F_Real)%> *' p1) = (len p1) + 1 by UPROOTS:38;
then A15: deg (<%(0. F_Real),(1. F_Real)%> *' p1) > deg p2 by A11, A13, XREAL_1:8;
then reconsider p = (<%(0. F_Real),(1. F_Real)%> *' p1) - p2 as INT -valued monic Polynomial of F_Real by Th46;
take p ; :: thesis: ( eval (p,e) = 2 * (cos ((k + 2) * t)) & deg p = k + 2 & ( k + 2 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( k + 2 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )
A16: eval ((<%(0. F_Real),(1. F_Real)%> *' p1),e) = (eval (<%(0. F_Real),(1. F_Real)%>,e)) * (eval (p1,e)) by POLYNOM4:24;
(cos ((k + 2) * t)) + (cos (k * t)) = 2 * ((cos ((((k + 2) * t) + (k * t)) / 2)) * (cos ((((k + 2) * t) - (k * t)) / 2))) by SIN_COS4:17
.= (cos t) * (2 * (cos ((k * t) + t))) ;
then ((2 * (cos t)) * (2 * (cos ((k * t) + t)))) - (2 * (cos (k * t))) = 2 * (cos ((k + 2) * t)) ;
hence 2 * (cos ((k + 2) * t)) = (eval ((<%(0. F_Real),(1. F_Real)%> *' p1),e)) - (eval (p2,e)) by A2, A10, A12, A16, POLYNOM5:48
.= eval (p,e) by POLYNOM4:21 ;
:: thesis: ( deg p = k + 2 & ( k + 2 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( k + 2 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )
thus deg p = k + 2 by A13, A14, A15, Th41; :: thesis: ( ( k + 2 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( k + 2 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )
thus ( ( k + 2 = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( k + 2 = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) ) by A8; :: thesis: verum

end;

end;

end;

for k being non zero Nat holds S₁[k] from FIB_NUM2:sch 1(A3, A4, A5);
hence ex p being INT -valued monic Polynomial of F_Real st
( eval (p,e) = 2 * (cos (n * t)) & deg p = n & ( n = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( n = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) ) by A1; :: thesis: verum