begin
theorem
for
a,
c,
e,
x being ( (
real ) (
complex real ext-real )
number ) st
a : ( (
real ) (
complex real ext-real )
number )
<> 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) &
e : ( (
real ) (
complex real ext-real )
number )
<> 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) &
(c : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) (
complex real ext-real )
set )
- ((4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * e : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set ) : ( ( ) (
complex real ext-real )
set )
> 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) &
Polynom (
a : ( (
real ) (
complex real ext-real )
number ) ,
0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) ,
c : ( (
real ) (
complex real ext-real )
number ) ,
0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) ,
e : ( (
real ) (
complex real ext-real )
number ) ,
x : ( (
real ) (
complex real ext-real )
number ) ) : ( ( ) (
complex real ext-real )
set )
= 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) holds
(
x : ( (
real ) (
complex real ext-real )
number )
<> 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) & (
x : ( (
real ) (
complex real ext-real )
number )
= sqrt (((- c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (delta (a : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) ,e : ( ( real ) ( complex real ext-real ) number ) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
M2(
COMPLEX : ( ( ) (
V33()
V39() )
set ) )) : ( (
real ) (
complex real ext-real )
set ) or
x : ( (
real ) (
complex real ext-real )
number )
= sqrt (((- c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (delta (a : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) ,e : ( ( real ) ( complex real ext-real ) number ) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
M2(
COMPLEX : ( ( ) (
V33()
V39() )
set ) )) : ( (
real ) (
complex real ext-real )
set ) or
x : ( (
real ) (
complex real ext-real )
number )
= - (sqrt (((- c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (delta (a : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) ,e : ( ( real ) ( complex real ext-real ) number ) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) ) : ( (
real ) (
complex real ext-real )
set ) : ( (
complex ) (
complex real ext-real )
set ) or
x : ( (
real ) (
complex real ext-real )
number )
= - (sqrt (((- c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (delta (a : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) ,e : ( ( real ) ( complex real ext-real ) number ) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) ) : ( (
real ) (
complex real ext-real )
set ) : ( (
complex ) (
complex real ext-real )
set ) ) ) ;
theorem
for
a,
b,
c,
x,
y being ( (
real ) (
complex real ext-real )
number ) st
a : ( (
real ) (
complex real ext-real )
number )
<> 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) &
y : ( (
real ) (
complex real ext-real )
number )
= x : ( (
real ) (
complex real ext-real )
number )
+ (1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) / x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
M2(
COMPLEX : ( ( ) (
V33()
V39() )
set ) )) : ( ( ) (
complex real ext-real )
set ) &
Polynom (
a : ( (
real ) (
complex real ext-real )
number ) ,
b : ( (
real ) (
complex real ext-real )
number ) ,
c : ( (
real ) (
complex real ext-real )
number ) ,
b : ( (
real ) (
complex real ext-real )
number ) ,
a : ( (
real ) (
complex real ext-real )
number ) ,
x : ( (
real ) (
complex real ext-real )
number ) ) : ( ( ) (
complex real ext-real )
set )
= 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) holds
(
x : ( (
real ) (
complex real ext-real )
number )
<> 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) &
(((a : ( ( real ) ( complex real ext-real ) number ) * (y : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (b : ( ( real ) ( complex real ext-real ) number ) * y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set )
- (2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set ) : ( ( ) (
complex real ext-real )
set )
= 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) ) ;
theorem
for
a,
b,
c,
x,
y being ( (
real ) (
complex real ext-real )
number ) st
a : ( (
real ) (
complex real ext-real )
number )
<> 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) &
((b : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) - ((4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
+ (8 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * (a : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set ) : ( ( ) (
complex real ext-real )
set )
> 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) &
y : ( (
real ) (
complex real ext-real )
number )
= x : ( (
real ) (
complex real ext-real )
number )
+ (1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) / x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
M2(
COMPLEX : ( ( ) (
V33()
V39() )
set ) )) : ( ( ) (
complex real ext-real )
set ) &
Polynom (
a : ( (
real ) (
complex real ext-real )
number ) ,
b : ( (
real ) (
complex real ext-real )
number ) ,
c : ( (
real ) (
complex real ext-real )
number ) ,
b : ( (
real ) (
complex real ext-real )
number ) ,
a : ( (
real ) (
complex real ext-real )
number ) ,
x : ( (
real ) (
complex real ext-real )
number ) ) : ( ( ) (
complex real ext-real )
set )
= 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) holds
for
y1,
y2 being ( (
real ) (
complex real ext-real )
number ) st
y1 : ( (
real ) (
complex real ext-real )
number )
= ((- b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (((b : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) - ((4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (8 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * (a : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
/ (2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set ) : ( ( ) (
complex real ext-real )
M2(
COMPLEX : ( ( ) (
V33()
V39() )
set ) )) &
y2 : ( (
real ) (
complex real ext-real )
number )
= ((- b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (((b : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) - ((4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (8 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * (a : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
/ (2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set ) : ( ( ) (
complex real ext-real )
M2(
COMPLEX : ( ( ) (
V33()
V39() )
set ) )) holds
(
x : ( (
real ) (
complex real ext-real )
number )
<> 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) & (
x : ( (
real ) (
complex real ext-real )
number )
= (y1 : ( ( real ) ( complex real ext-real ) number ) + (sqrt (delta (1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ,(- y1 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) ,1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
/ 2 : ( ( ) ( non
zero natural complex real ext-real positive V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) : ( ( ) (
complex real ext-real )
M2(
COMPLEX : ( ( ) (
V33()
V39() )
set ) )) or
x : ( (
real ) (
complex real ext-real )
number )
= (y2 : ( ( real ) ( complex real ext-real ) number ) + (sqrt (delta (1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ,(- y2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) ,1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
/ 2 : ( ( ) ( non
zero natural complex real ext-real positive V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) : ( ( ) (
complex real ext-real )
M2(
COMPLEX : ( ( ) (
V33()
V39() )
set ) )) or
x : ( (
real ) (
complex real ext-real )
number )
= (y1 : ( ( real ) ( complex real ext-real ) number ) - (sqrt (delta (1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ,(- y1 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) ,1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
/ 2 : ( ( ) ( non
zero natural complex real ext-real positive V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) : ( ( ) (
complex real ext-real )
M2(
COMPLEX : ( ( ) (
V33()
V39() )
set ) )) or
x : ( (
real ) (
complex real ext-real )
number )
= (y2 : ( ( real ) ( complex real ext-real ) number ) - (sqrt (delta (1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ,(- y2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) ,1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
/ 2 : ( ( ) ( non
zero natural complex real ext-real positive V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) : ( ( ) (
complex real ext-real )
M2(
COMPLEX : ( ( ) (
V33()
V39() )
set ) )) ) ) ;
theorem
for
x,
y being ( (
real ) (
complex real ext-real )
number ) st
x : ( (
real ) (
complex real ext-real )
number )
+ y : ( (
real ) (
complex real ext-real )
number ) : ( ( ) (
complex real ext-real )
set )
<> 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) holds
(x : ( ( real ) ( complex real ext-real ) number ) + y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set )
|^ 4 : ( ( ) ( non
zero natural complex real ext-real positive V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) : ( ( ) (
complex real ext-real )
set )
= ((((x : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) + (((3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * (y : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (y : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set )
+ ((((x : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) + (((3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * (y : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (y : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set ) : ( ( ) (
complex real ext-real )
set ) ;
theorem
for
x,
y being ( (
real ) (
complex real ext-real )
number ) st
x : ( (
real ) (
complex real ext-real )
number )
+ y : ( (
real ) (
complex real ext-real )
number ) : ( ( ) (
complex real ext-real )
set )
<> 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) holds
(x : ( ( real ) ( complex real ext-real ) number ) + y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set )
|^ 4 : ( ( ) ( non
zero natural complex real ext-real positive V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) : ( ( ) (
complex real ext-real )
set )
= ((x : ( ( real ) ( complex real ext-real ) number ) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) + ((((4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((6 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * (y : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * (y : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
+ (y : ( ( real ) ( complex real ext-real ) number ) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) (
complex real ext-real )
set ) : ( ( ) (
complex real ext-real )
set ) ;
theorem
for
a1,
a2,
a3,
a4,
a5,
b1,
b2,
b3,
b4,
b5 being ( (
real ) (
complex real ext-real )
number ) st ( for
x being ( (
real ) (
complex real ext-real )
number ) holds
Polynom (
a1 : ( (
real ) (
complex real ext-real )
number ) ,
a2 : ( (
real ) (
complex real ext-real )
number ) ,
a3 : ( (
real ) (
complex real ext-real )
number ) ,
a4 : ( (
real ) (
complex real ext-real )
number ) ,
a5 : ( (
real ) (
complex real ext-real )
number ) ,
x : ( (
real ) (
complex real ext-real )
number ) ) : ( ( ) (
complex real ext-real )
set )
= Polynom (
b1 : ( (
real ) (
complex real ext-real )
number ) ,
b2 : ( (
real ) (
complex real ext-real )
number ) ,
b3 : ( (
real ) (
complex real ext-real )
number ) ,
b4 : ( (
real ) (
complex real ext-real )
number ) ,
b5 : ( (
real ) (
complex real ext-real )
number ) ,
x : ( (
real ) (
complex real ext-real )
number ) ) : ( ( ) (
complex real ext-real )
set ) ) holds
(
a5 : ( (
real ) (
complex real ext-real )
number )
= b5 : ( (
real ) (
complex real ext-real )
number ) &
((a1 : ( ( real ) ( complex real ext-real ) number ) - a2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + a3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set )
- a4 : ( (
real ) (
complex real ext-real )
number ) : ( ( ) (
complex real ext-real )
set )
= ((b1 : ( ( real ) ( complex real ext-real ) number ) - b2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + b3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set )
- b4 : ( (
real ) (
complex real ext-real )
number ) : ( ( ) (
complex real ext-real )
set ) &
((a1 : ( ( real ) ( complex real ext-real ) number ) + a2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + a3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set )
+ a4 : ( (
real ) (
complex real ext-real )
number ) : ( ( ) (
complex real ext-real )
set )
= ((b1 : ( ( real ) ( complex real ext-real ) number ) + b2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + b3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set )
+ b4 : ( (
real ) (
complex real ext-real )
number ) : ( ( ) (
complex real ext-real )
set ) ) ;
theorem
for
a1,
a2,
a3,
a4,
a5,
b1,
b2,
b3,
b4,
b5 being ( (
real ) (
complex real ext-real )
number ) st ( for
x being ( (
real ) (
complex real ext-real )
number ) holds
Polynom (
a1 : ( (
real ) (
complex real ext-real )
number ) ,
a2 : ( (
real ) (
complex real ext-real )
number ) ,
a3 : ( (
real ) (
complex real ext-real )
number ) ,
a4 : ( (
real ) (
complex real ext-real )
number ) ,
a5 : ( (
real ) (
complex real ext-real )
number ) ,
x : ( (
real ) (
complex real ext-real )
number ) ) : ( ( ) (
complex real ext-real )
set )
= Polynom (
b1 : ( (
real ) (
complex real ext-real )
number ) ,
b2 : ( (
real ) (
complex real ext-real )
number ) ,
b3 : ( (
real ) (
complex real ext-real )
number ) ,
b4 : ( (
real ) (
complex real ext-real )
number ) ,
b5 : ( (
real ) (
complex real ext-real )
number ) ,
x : ( (
real ) (
complex real ext-real )
number ) ) : ( ( ) (
complex real ext-real )
set ) ) holds
(
a1 : ( (
real ) (
complex real ext-real )
number )
- b1 : ( (
real ) (
complex real ext-real )
number ) : ( ( ) (
complex real ext-real )
set )
= b3 : ( (
real ) (
complex real ext-real )
number )
- a3 : ( (
real ) (
complex real ext-real )
number ) : ( ( ) (
complex real ext-real )
set ) &
a2 : ( (
real ) (
complex real ext-real )
number )
- b2 : ( (
real ) (
complex real ext-real )
number ) : ( ( ) (
complex real ext-real )
set )
= b4 : ( (
real ) (
complex real ext-real )
number )
- a4 : ( (
real ) (
complex real ext-real )
number ) : ( ( ) (
complex real ext-real )
set ) ) ;
theorem
for
a1,
a2,
a3,
a4,
a5,
b1,
b2,
b3,
b4,
b5 being ( (
real ) (
complex real ext-real )
number ) st ( for
x being ( (
real ) (
complex real ext-real )
number ) holds
Polynom (
a1 : ( (
real ) (
complex real ext-real )
number ) ,
a2 : ( (
real ) (
complex real ext-real )
number ) ,
a3 : ( (
real ) (
complex real ext-real )
number ) ,
a4 : ( (
real ) (
complex real ext-real )
number ) ,
a5 : ( (
real ) (
complex real ext-real )
number ) ,
x : ( (
real ) (
complex real ext-real )
number ) ) : ( ( ) (
complex real ext-real )
set )
= Polynom (
b1 : ( (
real ) (
complex real ext-real )
number ) ,
b2 : ( (
real ) (
complex real ext-real )
number ) ,
b3 : ( (
real ) (
complex real ext-real )
number ) ,
b4 : ( (
real ) (
complex real ext-real )
number ) ,
b5 : ( (
real ) (
complex real ext-real )
number ) ,
x : ( (
real ) (
complex real ext-real )
number ) ) : ( ( ) (
complex real ext-real )
set ) ) holds
(
a1 : ( (
real ) (
complex real ext-real )
number )
= b1 : ( (
real ) (
complex real ext-real )
number ) &
a2 : ( (
real ) (
complex real ext-real )
number )
= b2 : ( (
real ) (
complex real ext-real )
number ) &
a3 : ( (
real ) (
complex real ext-real )
number )
= b3 : ( (
real ) (
complex real ext-real )
number ) &
a4 : ( (
real ) (
complex real ext-real )
number )
= b4 : ( (
real ) (
complex real ext-real )
number ) &
a5 : ( (
real ) (
complex real ext-real )
number )
= b5 : ( (
real ) (
complex real ext-real )
number ) ) ;
theorem
for
a1,
a2,
a3,
a4,
a5,
x,
x1,
x2,
x3,
x4 being ( (
real ) (
complex real ext-real )
number ) st
a1 : ( (
real ) (
complex real ext-real )
number )
<> 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) & ( for
x being ( (
real ) (
complex real ext-real )
number ) holds
Polynom (
a1 : ( (
real ) (
complex real ext-real )
number ) ,
a2 : ( (
real ) (
complex real ext-real )
number ) ,
a3 : ( (
real ) (
complex real ext-real )
number ) ,
a4 : ( (
real ) (
complex real ext-real )
number ) ,
a5 : ( (
real ) (
complex real ext-real )
number ) ,
x : ( (
real ) (
complex real ext-real )
number ) ) : ( ( ) (
complex real ext-real )
set )
= Four0 (
a1 : ( (
real ) (
complex real ext-real )
number ) ,
x1 : ( (
real ) (
complex real ext-real )
number ) ,
x2 : ( (
real ) (
complex real ext-real )
number ) ,
x3 : ( (
real ) (
complex real ext-real )
number ) ,
x4 : ( (
real ) (
complex real ext-real )
number ) ,
x : ( (
real ) (
complex real ext-real )
number ) ) : ( ( ) (
complex real ext-real )
set ) ) holds
(((((a1 : ( ( real ) ( complex real ext-real ) number ) * (x : ( ( real ) ( complex real ext-real ) number ) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (a2 : ( ( real ) ( complex real ext-real ) number ) * (x : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (a3 : ( ( real ) ( complex real ext-real ) number ) * (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (a4 : ( ( real ) ( complex real ext-real ) number ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + a5 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set )
/ a1 : ( (
real ) (
complex real ext-real )
number ) : ( ( ) (
complex real ext-real )
M2(
COMPLEX : ( ( ) (
V33()
V39() )
set ) ))
= (((((x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) - (((x1 : ( ( real ) ( complex real ext-real ) number ) + x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * ((x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((((x1 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + (x2 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) - (((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
- ((((x : ( ( real ) ( complex real ext-real ) number ) - x1 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) - x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) - x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set ) : ( ( ) (
complex real ext-real )
set ) ;
theorem
for
a1,
a2,
a3,
a4,
a5,
x,
x1,
x2,
x3,
x4 being ( (
real ) (
complex real ext-real )
number ) st
a1 : ( (
real ) (
complex real ext-real )
number )
<> 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) & ( for
x being ( (
real ) (
complex real ext-real )
number ) holds
Polynom (
a1 : ( (
real ) (
complex real ext-real )
number ) ,
a2 : ( (
real ) (
complex real ext-real )
number ) ,
a3 : ( (
real ) (
complex real ext-real )
number ) ,
a4 : ( (
real ) (
complex real ext-real )
number ) ,
a5 : ( (
real ) (
complex real ext-real )
number ) ,
x : ( (
real ) (
complex real ext-real )
number ) ) : ( ( ) (
complex real ext-real )
set )
= Four0 (
a1 : ( (
real ) (
complex real ext-real )
number ) ,
x1 : ( (
real ) (
complex real ext-real )
number ) ,
x2 : ( (
real ) (
complex real ext-real )
number ) ,
x3 : ( (
real ) (
complex real ext-real )
number ) ,
x4 : ( (
real ) (
complex real ext-real )
number ) ,
x : ( (
real ) (
complex real ext-real )
number ) ) : ( ( ) (
complex real ext-real )
set ) ) holds
(((((a1 : ( ( real ) ( complex real ext-real ) number ) * (x : ( ( real ) ( complex real ext-real ) number ) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (a2 : ( ( real ) ( complex real ext-real ) number ) * (x : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (a3 : ( ( real ) ( complex real ext-real ) number ) * (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (a4 : ( ( real ) ( complex real ext-real ) number ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + a5 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set )
/ a1 : ( (
real ) (
complex real ext-real )
number ) : ( ( ) (
complex real ext-real )
M2(
COMPLEX : ( ( ) (
V33()
V39() )
set ) ))
= ((((x : ( ( real ) ( complex real ext-real ) number ) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) - ((((x1 : ( ( real ) ( complex real ext-real ) number ) + x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((((((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + (x1 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (x1 : ( ( real ) ( complex real ext-real ) number ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((x2 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + (x2 : ( ( real ) ( complex real ext-real ) number ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (x3 : ( ( real ) ( complex real ext-real ) number ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) - ((((((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + ((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((x1 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((x2 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
+ (((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set ) : ( ( ) (
complex real ext-real )
set ) ;
theorem
for
a1,
a2,
a3,
a4,
a5,
x1,
x2,
x3,
x4 being ( (
real ) (
complex real ext-real )
number ) st
a1 : ( (
real ) (
complex real ext-real )
number )
<> 0 : ( ( ) (
natural complex real ext-real V33()
V34()
V35()
V36()
V37()
V38()
V40()
V53() )
M3(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ,
NAT : ( ( ) (
V33()
V34()
V35()
V36()
V37()
V38()
V39() )
M2(
K6(
REAL : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) : ( ( ) ( )
set ) )) )) & ( for
x being ( (
real ) (
complex real ext-real )
number ) holds
Polynom (
a1 : ( (
real ) (
complex real ext-real )
number ) ,
a2 : ( (
real ) (
complex real ext-real )
number ) ,
a3 : ( (
real ) (
complex real ext-real )
number ) ,
a4 : ( (
real ) (
complex real ext-real )
number ) ,
a5 : ( (
real ) (
complex real ext-real )
number ) ,
x : ( (
real ) (
complex real ext-real )
number ) ) : ( ( ) (
complex real ext-real )
set )
= Four0 (
a1 : ( (
real ) (
complex real ext-real )
number ) ,
x1 : ( (
real ) (
complex real ext-real )
number ) ,
x2 : ( (
real ) (
complex real ext-real )
number ) ,
x3 : ( (
real ) (
complex real ext-real )
number ) ,
x4 : ( (
real ) (
complex real ext-real )
number ) ,
x : ( (
real ) (
complex real ext-real )
number ) ) : ( ( ) (
complex real ext-real )
set ) ) holds
(
a2 : ( (
real ) (
complex real ext-real )
number )
/ a1 : ( (
real ) (
complex real ext-real )
number ) : ( ( ) (
complex real ext-real )
M2(
COMPLEX : ( ( ) (
V33()
V39() )
set ) ))
= - (((x1 : ( ( real ) ( complex real ext-real ) number ) + x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set ) : ( (
complex ) (
complex real ext-real )
set ) &
a3 : ( (
real ) (
complex real ext-real )
number )
/ a1 : ( (
real ) (
complex real ext-real )
number ) : ( ( ) (
complex real ext-real )
M2(
COMPLEX : ( ( ) (
V33()
V39() )
set ) ))
= ((((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + (x1 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (x1 : ( ( real ) ( complex real ext-real ) number ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((x2 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + (x2 : ( ( real ) ( complex real ext-real ) number ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set )
+ (x3 : ( ( real ) ( complex real ext-real ) number ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set ) : ( ( ) (
complex real ext-real )
set ) &
a4 : ( (
real ) (
complex real ext-real )
number )
/ a1 : ( (
real ) (
complex real ext-real )
number ) : ( ( ) (
complex real ext-real )
M2(
COMPLEX : ( ( ) (
V33()
V39() )
set ) ))
= - (((((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + ((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((x1 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((x2 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) (
complex real ext-real )
set ) : ( (
complex ) (
complex real ext-real )
set ) &
a5 : ( (
real ) (
complex real ext-real )
number )
/ a1 : ( (
real ) (
complex real ext-real )
number ) : ( ( ) (
complex real ext-real )
M2(
COMPLEX : ( ( ) (
V33()
V39() )
set ) ))
= ((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) (
complex real ext-real )
set )
* x4 : ( (
real ) (
complex real ext-real )
number ) : ( ( ) (
complex real ext-real )
set ) ) ;