let
n
be
even
Nat
;
:: thesis:
for
x
being
Element
of
F_Real
holds
eval
(
(
npoly
(
F_Real
,
n
)
)
,
x
)
>
0.
F_Real
let
x
be
Element
of
F_Real
;
:: thesis:
eval
(
(
npoly
(
F_Real
,
n
)
)
,
x
)
>
0.
F_Real
per
cases
(
n
=
0
or not
n
is
zero
)
;
suppose
n
=
0
;
:: thesis:
eval
(
(
npoly
(
F_Real
,
n
)
)
,
x
)
>
0.
F_Real
hence
eval
(
(
npoly
(
F_Real
,
n
)
)
,
x
)
>
0.
F_Real
by
lem1e
;
:: thesis:
verum
end;
suppose
S
: not
n
is
zero
;
:: thesis:
eval
(
(
npoly
(
F_Real
,
n
)
)
,
x
)
>
0.
F_Real
(
x
|^
n
)
+
1
>=
(
0.
F_Real
)
+
1
by
XX
,
XREAL_1:6
;
then
(
x
|^
n
)
+
(
1.
F_Real
)
>=
1 ;
hence
eval
(
(
npoly
(
F_Real
,
n
)
)
,
x
)
>
0.
F_Real
by
lem1a
,
S
;
:: thesis:
verum
end;
end;