begin
theorem
for
c,
a,
b being ( ( ) (
complex real ext-real )
Real) holds
( not
c : ( ( ) (
complex real ext-real )
Real)
/ a : ( ( ) (
complex real ext-real )
Real) : ( ( ) (
complex real ext-real )
set )
< 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) or (
((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) (
complex real ext-real )
set )
/ (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) (
complex real ext-real )
set ) : ( ( ) (
complex real ext-real )
set )
> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) &
((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) (
complex real ext-real )
set )
/ (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) (
complex real ext-real )
set ) : ( ( ) (
complex real ext-real )
set )
< 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) ) or (
((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) (
complex real ext-real )
set )
/ (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) (
complex real ext-real )
set ) : ( ( ) (
complex real ext-real )
set )
< 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) &
((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) (
complex real ext-real )
set )
/ (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) (
complex real ext-real )
set ) : ( ( ) (
complex real ext-real )
set )
> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) ) ) ;
theorem
for
a,
b,
c,
x being ( ( ) (
complex real ext-real )
Real)
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) st
a : ( ( ) (
complex real ext-real )
Real)
<> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) &
n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) is
odd &
delta (
a : ( ( ) (
complex real ext-real )
Real) ,
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( )
set ) )
>= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) &
Polynom (
a : ( ( ) (
complex real ext-real )
Real) ,
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ,
(x : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( )
set ) )
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) & not
x : ( ( ) (
complex real ext-real )
Real)
= n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) )
-root (((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set ) : ( (
real ) (
complex real ext-real )
set ) holds
x : ( ( ) (
complex real ext-real )
Real)
= n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) )
-root (((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set ) : ( (
real ) (
complex real ext-real )
set ) ;
theorem
for
a,
b,
c,
x being ( ( ) (
complex real ext-real )
Real)
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) st
a : ( ( ) (
complex real ext-real )
Real)
<> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) &
b : ( ( ) (
complex real ext-real )
Real)
/ a : ( ( ) (
complex real ext-real )
Real) : ( ( ) (
complex real ext-real )
set )
< 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) &
c : ( ( ) (
complex real ext-real )
Real)
/ a : ( ( ) (
complex real ext-real )
Real) : ( ( ) (
complex real ext-real )
set )
> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) &
n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) is
even &
n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) )
>= 1 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) &
delta (
a : ( ( ) (
complex real ext-real )
Real) ,
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( )
set ) )
>= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) &
Polynom (
a : ( ( ) (
complex real ext-real )
Real) ,
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ,
(x : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( )
set ) )
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) & not
x : ( ( ) (
complex real ext-real )
Real)
= n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) )
-root (((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set ) : ( (
real ) (
complex real ext-real )
set ) & not
x : ( ( ) (
complex real ext-real )
Real)
= - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( (
real ) (
complex real ext-real )
set ) : ( (
complex ) (
complex real ext-real )
set ) & not
x : ( ( ) (
complex real ext-real )
Real)
= n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) )
-root (((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set ) : ( (
real ) (
complex real ext-real )
set ) holds
x : ( ( ) (
complex real ext-real )
Real)
= - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( (
real ) (
complex real ext-real )
set ) : ( (
complex ) (
complex real ext-real )
set ) ;
theorem
for
a,
b,
c,
x being ( ( ) (
complex real ext-real )
Real) st
a : ( ( ) (
complex real ext-real )
Real)
<> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) &
(((b : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) + ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) * b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (5 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
- ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) * c : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) (
complex real ext-real )
set ) : ( ( ) (
complex real ext-real )
set )
> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) &
Polynom (
a : ( ( ) (
complex real ext-real )
Real) ,
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ,
b : ( ( ) (
complex real ext-real )
Real) ,
a : ( ( ) (
complex real ext-real )
Real) ,
x : ( ( ) (
complex real ext-real )
Real) ) : ( ( ) (
complex real ext-real )
set )
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) holds
for
y1,
y2 being ( ( ) (
complex real ext-real )
Real) st
y1 : ( ( ) (
complex real ext-real )
Real)
= ((a : ( ( ) ( complex real ext-real ) Real) - b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) + (sqrt ((((b : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) + ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) * b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (5 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) - ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) * c : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
/ (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) (
complex real ext-real )
set ) : ( ( ) (
complex real ext-real )
set ) &
y2 : ( ( ) (
complex real ext-real )
Real)
= ((a : ( ( ) ( complex real ext-real ) Real) - b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) - (sqrt ((((b : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) + ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) * b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (5 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) - ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) * c : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
/ (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) (
complex real ext-real )
set ) : ( ( ) (
complex real ext-real )
set ) & not
x : ( ( ) (
complex real ext-real )
Real)
= - 1 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
complex ) ( non
zero complex real ext-real non
positive V33() )
set ) & not
x : ( ( ) (
complex real ext-real )
Real)
= (y1 : ( ( ) ( complex real ext-real ) Real) + (sqrt (delta (1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(- y1 : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) ,1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
/ 2 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real )
set ) & not
x : ( ( ) (
complex real ext-real )
Real)
= (y2 : ( ( ) ( complex real ext-real ) Real) + (sqrt (delta (1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(- y2 : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) ,1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
/ 2 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real )
set ) & not
x : ( ( ) (
complex real ext-real )
Real)
= (y1 : ( ( ) ( complex real ext-real ) Real) - (sqrt (delta (1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(- y1 : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) ,1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
/ 2 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real )
set ) holds
x : ( ( ) (
complex real ext-real )
Real)
= (y2 : ( ( ) ( complex real ext-real ) Real) - (sqrt (delta (1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(- y2 : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) ,1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
/ 2 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative V33() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real )
set ) ;