let t be Real; 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; 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; ( 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)
; 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 S1[ 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:
S1[1]
proof
assume
1
<= 1
;
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
;
( 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;
( 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
;
( ( 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)%> ) ) )
;
verum
end;
A4:
S1[2]
proof
assume
1
<= 2
;
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
;
( 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
;
( 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
;
( ( 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)%> ) ) )
;
verum
end;
A5:
for k being non zero Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be non
zero Nat;
( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that A6:
S1[
k]
and A7:
S1[
k + 1]
and
1
<= k + 2
;
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 A8:
(
k + 2
<> 1 &
k + 2
<> 2 )
;
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
;
( 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
;
( 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;
( ( 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;
verum end; end;
end;
for k being non zero Nat holds S1[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; verum