POLYEQ

:: POLYEQ_1 semantic presentation

begin

definition

let a, b, x be ( ( complex ) ( complex ) number ) ;

func Polynom (a,b,x) -> ( ( ) ( ) set ) equals :: POLYEQ_1:def 1
(a : ( ( ) ( ) set ) * x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + b : ( ( V21() V30(a : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) ) ) ( V21() V30(a : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) ) ) M2(K6(K7(a : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ;

end;

registration

let a, b, x be ( ( complex ) ( complex ) number ) ;

cluster Polynom (a : ( ( complex ) ( complex ) set ) ,b : ( ( complex ) ( complex ) set ) ,x : ( ( complex ) ( complex ) set ) ) : ( ( ) ( ) set ) -> complex ;

end;

registration

let a, b, x be ( ( real ) ( complex real ext-real ) number ) ;

cluster Polynom (a : ( ( real ) ( complex real ext-real ) set ) ,b : ( ( real ) ( complex real ext-real ) set ) ,x : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex ) set ) -> real ;

end;

definition

let a, b, x be ( ( ) ( complex real ext-real ) Real) ;
:: original: Polynom
redefine func Polynom (a,b,x) -> ( ( ) ( complex real ext-real ) Real) ;

end;

theorem :: POLYEQ_1:1

for a, b, x being ( ( complex ) ( complex ) number ) st a : ( ( complex ) ( complex ) 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 ) )) )) & Polynom (a : ( ( complex ) ( complex ) number ) ,b : ( ( complex ) ( complex ) number ) ,x : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) 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 : ( ( complex ) ( complex ) number ) = - (b : ( ( complex ) ( complex ) number ) / a : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) set ) ;

theorem :: POLYEQ_1:2

for x being ( ( complex ) ( complex ) number ) holds Polynom (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 ) )) )) ,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 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) 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 :: POLYEQ_1:3

for b being ( ( complex ) ( complex ) number ) st b : ( ( complex ) ( complex ) 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 ) )) )) holds
for x being ( ( complex ) ( complex ) number ) holds not Polynom (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 : ( ( complex ) ( complex ) number ) ,x : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) 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 ) )) )) ;

definition

let a, b, c, x be ( ( complex ) ( complex ) number ) ;

func Polynom (a,b,c,x) -> ( ( ) ( ) set ) equals :: POLYEQ_1:def 2
((a : ( ( real ) ( complex real ext-real ) set ) * (x : ( ( ) ( ) set ) ^2) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (b : ( ( real ) ( complex real ext-real ) set ) * x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + c : ( ( real ) ( complex real ext-real ) set ) : ( ( ) ( ) set ) ;

end;

registration

let a, b, c, x be ( ( real ) ( complex real ext-real ) number ) ;

cluster Polynom (a : ( ( real ) ( complex real ext-real ) set ) ,b : ( ( real ) ( complex real ext-real ) set ) ,c : ( ( real ) ( complex real ext-real ) set ) ,x : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( ) set ) -> real ;

end;

registration

let a, b, c, x be ( ( complex ) ( complex ) number ) ;

cluster Polynom (a : ( ( complex ) ( complex ) set ) ,b : ( ( complex ) ( complex ) set ) ,c : ( ( complex ) ( complex ) set ) ,x : ( ( complex ) ( complex ) set ) ) : ( ( ) ( ) set ) -> complex ;

end;

definition

let a, b, c, x be ( ( ) ( complex real ext-real ) Real) ;
:: original: Polynom
redefine func Polynom (a,b,c,x) -> ( ( ) ( complex real ext-real ) Real) ;

end;

theorem :: POLYEQ_1:4

for a, b, c, a9, b9, c9 being ( ( complex ) ( complex ) number ) st ( for x being ( ( real ) ( complex real ext-real ) number ) holds Polynom (a : ( ( complex ) ( complex ) number ) ,b : ( ( complex ) ( complex ) number ) ,c : ( ( complex ) ( complex ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex ) set ) = Polynom (a9 : ( ( complex ) ( complex ) number ) ,b9 : ( ( complex ) ( complex ) number ) ,c9 : ( ( complex ) ( complex ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex ) set ) ) holds
( a : ( ( complex ) ( complex ) number ) = a9 : ( ( complex ) ( complex ) number ) & b : ( ( complex ) ( complex ) number ) = b9 : ( ( complex ) ( complex ) number ) & c : ( ( complex ) ( complex ) number ) = c9 : ( ( complex ) ( complex ) number ) ) ;

theorem :: POLYEQ_1:5

for a, b, c 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 ) )) )) & delta (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( 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 x being ( ( real ) ( complex real ext-real ) number ) holds
( not Polynom (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( 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 ) )) )) or x : ( ( real ) ( complex real ext-real ) number ) = ((- b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (delta (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( 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 ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) or x : ( ( real ) ( complex real ext-real ) number ) = ((- b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (delta (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( 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 ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) ;

theorem :: POLYEQ_1:6

for a, b, c, x being ( ( complex ) ( complex ) number ) st a : ( ( complex ) ( complex ) 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 ) )) )) & delta (a : ( ( complex ) ( complex ) number ) ,b : ( ( complex ) ( complex ) number ) ,c : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) 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 : ( ( complex ) ( complex ) number ) ,b : ( ( complex ) ( complex ) number ) ,c : ( ( complex ) ( complex ) number ) ,x : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) 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 : ( ( complex ) ( complex ) number ) = - (b : ( ( complex ) ( complex ) number ) / (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 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) set ) ;

theorem :: POLYEQ_1:7

for a, b, c being ( ( real ) ( complex real ext-real ) number ) st delta (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( 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 x being ( ( real ) ( complex real ext-real ) number ) holds not Polynom (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( 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 ) )) )) ;

theorem :: POLYEQ_1:8

for x being ( ( real ) ( complex real ext-real ) number )
for b, c being ( ( complex ) ( complex ) number ) st b : ( ( complex ) ( complex ) 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 (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 : ( ( complex ) ( complex ) number ) ,c : ( ( complex ) ( complex ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex ) 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 ) = - (c : ( ( complex ) ( complex ) number ) / b : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) set ) ;

theorem :: POLYEQ_1:9

for x being ( ( complex ) ( complex ) number ) holds Polynom (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 ) )) )) ,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 ) )) )) ,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 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) 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 :: POLYEQ_1:10

for c being ( ( complex ) ( complex ) number ) st c : ( ( complex ) ( complex ) 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 ) )) )) holds
for x being ( ( complex ) ( complex ) number ) holds not Polynom (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 ) )) )) ,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 : ( ( complex ) ( complex ) number ) ,x : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) 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 ) )) )) ;

definition

let a, x, x1, x2 be ( ( complex ) ( complex ) number ) ;

func Quard (a,x1,x2,x) -> ( ( ) ( ) set ) equals :: POLYEQ_1:def 3
a : ( ( complex ) ( complex ) set ) * ((x : ( ( complex ) ( complex ) set ) - x1 : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) * (x : ( ( complex ) ( complex ) set ) - x2 : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex ) set ) ;

end;

registration

let a, x, x1, x2 be ( ( real ) ( complex real ext-real ) number ) ;

cluster Quard (a : ( ( real ) ( complex real ext-real ) set ) ,x1 : ( ( real ) ( complex real ext-real ) set ) ,x2 : ( ( real ) ( complex real ext-real ) set ) ,x : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( ) set ) -> real ;

end;

definition

let a, x, x1, x2 be ( ( ) ( complex real ext-real ) Real) ;
:: original: Quard
redefine func Quard (a,x1,x2,x) -> ( ( ) ( complex real ext-real ) Real) ;

end;

theorem :: POLYEQ_1:11

for x1, x2 being ( ( real ) ( complex real ext-real ) number )
for a, b, c being ( ( complex ) ( complex ) number ) st a : ( ( complex ) ( complex ) 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 (a : ( ( complex ) ( complex ) number ) ,b : ( ( complex ) ( complex ) number ) ,c : ( ( complex ) ( complex ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex ) set ) = Quard (a : ( ( complex ) ( complex ) number ) ,x1 : ( ( real ) ( complex real ext-real ) number ) ,x2 : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( ) set ) ) holds
( b : ( ( complex ) ( complex ) number ) / a : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = - (x1 : ( ( real ) ( complex real ext-real ) number ) + x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) & c : ( ( complex ) ( complex ) number ) / a : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) ) ;

begin

definition

let a, b, c, d, x be ( ( complex ) ( complex ) number ) ;

func Polynom (a,b,c,d,x) -> ( ( ) ( ) set ) equals :: POLYEQ_1:def 4
(((a : ( ( real ) ( complex real ext-real ) set ) * (x : ( ( ) ( ) M2(b : ( ( real ) ( 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 ) )) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (b : ( ( real ) ( complex real ext-real ) set ) * (x : ( ( ) ( ) M2(b : ( ( real ) ( complex real ext-real ) set ) )) ^2) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (c : ( ( real ) ( complex real ext-real ) set ) * x : ( ( ) ( ) M2(b : ( ( real ) ( complex real ext-real ) set ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + d : ( ( real ) ( complex real ext-real ) set ) : ( ( ) ( ) set ) ;

end;

registration

let a, b, c, d, x be ( ( complex ) ( complex ) number ) ;

cluster Polynom (a : ( ( complex ) ( complex ) set ) ,b : ( ( complex ) ( complex ) set ) ,c : ( ( complex ) ( complex ) set ) ,d : ( ( complex ) ( complex ) set ) ,x : ( ( complex ) ( complex ) set ) ) : ( ( ) ( ) set ) -> complex ;

end;

registration

let a, b, c, d, x be ( ( real ) ( complex real ext-real ) number ) ;

cluster Polynom (a : ( ( real ) ( complex real ext-real ) set ) ,b : ( ( real ) ( complex real ext-real ) set ) ,c : ( ( real ) ( complex real ext-real ) set ) ,d : ( ( real ) ( complex real ext-real ) set ) ,x : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex ) set ) -> real ;

end;

definition

let a, b, c, d, x be ( ( ) ( complex real ext-real ) Real) ;
:: original: Polynom
redefine func Polynom (a,b,c,d,x) -> ( ( ) ( complex real ext-real ) Real) ;

end;

theorem :: POLYEQ_1:12

for a, b, c, d, a9, b9, c9, d9 being ( ( real ) ( complex real ext-real ) number ) st ( for x being ( ( real ) ( complex real ext-real ) number ) holds Polynom (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) ,d : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) = Polynom (a9 : ( ( real ) ( complex real ext-real ) number ) ,b9 : ( ( real ) ( complex real ext-real ) number ) ,c9 : ( ( real ) ( complex real ext-real ) number ) ,d9 : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) holds
( a : ( ( real ) ( complex real ext-real ) number ) = a9 : ( ( real ) ( complex real ext-real ) number ) & b : ( ( real ) ( complex real ext-real ) number ) = b9 : ( ( real ) ( complex real ext-real ) number ) & c : ( ( real ) ( complex real ext-real ) number ) = c9 : ( ( real ) ( complex real ext-real ) number ) & d : ( ( real ) ( complex real ext-real ) number ) = d9 : ( ( real ) ( complex real ext-real ) number ) ) ;

definition

let a, x, x1, x2, x3 be ( ( real ) ( complex real ext-real ) number ) ;

func Tri (a,x1,x2,x3,x) -> ( ( ) ( ) set ) equals :: POLYEQ_1:def 5
a : ( ( real ) ( complex real ext-real ) set ) * (((x : ( ( real ) ( complex real ext-real ) set ) - x1 : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) set ) - x2 : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) set ) - x3 : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) ;

end;

registration

let a, x, x1, x2, x3 be ( ( real ) ( complex real ext-real ) number ) ;

cluster Tri (a : ( ( real ) ( complex real ext-real ) set ) ,x1 : ( ( real ) ( complex real ext-real ) set ) ,x2 : ( ( real ) ( complex real ext-real ) set ) ,x3 : ( ( real ) ( complex real ext-real ) set ) ,x : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( ) set ) -> real ;

end;

definition

let a, x, x1, x2, x3 be ( ( ) ( complex real ext-real ) Real) ;
:: original: Tri
redefine func Tri (a,x1,x2,x3,x) -> ( ( ) ( complex real ext-real ) Real) ;

end;

theorem :: POLYEQ_1:13

for a, b, c, d, x1, x2, x3 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 ) )) )) & ( for x being ( ( real ) ( complex real ext-real ) number ) holds Polynom (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) ,d : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) = Tri (a : ( ( 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 ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) holds
( b : ( ( real ) ( complex real ext-real ) number ) / a : ( ( 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 ) + x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) & c : ( ( real ) ( complex real ext-real ) number ) / a : ( ( 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 ) + (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 ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) & d : ( ( real ) ( complex real ext-real ) number ) / a : ( ( 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 ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) ) ;

theorem :: POLYEQ_1:14

for y, h being ( ( real ) ( complex real ext-real ) number ) holds (y : ( ( real ) ( complex real ext-real ) number ) + h : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( 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 ) )) )) : ( ( ) ( 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 ) + (((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 ) )) )) * h : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * (y : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) * (h : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + (h : ( ( 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 ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ;

theorem :: POLYEQ_1:15

for a, b, c, d, 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 ) )) )) & Polynom (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) ,d : ( ( 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 a1, a2, a3, h, y being ( ( real ) ( complex real ext-real ) number ) st y : ( ( real ) ( complex real ext-real ) number ) = x : ( ( real ) ( complex real ext-real ) number ) + (b : ( ( 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) & h : ( ( real ) ( complex real ext-real ) number ) = - (b : ( ( 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) & a1 : ( ( real ) ( complex real ext-real ) number ) = b : ( ( real ) ( complex real ext-real ) number ) / a : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) & a2 : ( ( real ) ( complex real ext-real ) number ) = c : ( ( real ) ( complex real ext-real ) number ) / a : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) & a3 : ( ( real ) ( complex real ext-real ) number ) = d : ( ( real ) ( complex real ext-real ) number ) / a : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) holds
((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 ) + ((((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 ) )) )) * h : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + a1 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * (y : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) * (h : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) * (a1 : ( ( real ) ( complex real ext-real ) number ) * h : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + a2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + (((h : ( ( 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 ) + (a1 : ( ( real ) ( complex real ext-real ) number ) * (h : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((a2 : ( ( real ) ( complex real ext-real ) number ) * h : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + a3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 :: POLYEQ_1:16

for a, b, c, d, 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 ) )) )) & Polynom (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) ,d : ( ( 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 a1, a2, a3, h, y being ( ( real ) ( complex real ext-real ) number ) st y : ( ( real ) ( complex real ext-real ) number ) = x : ( ( real ) ( complex real ext-real ) number ) + (b : ( ( 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) & h : ( ( real ) ( complex real ext-real ) number ) = - (b : ( ( 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) & a1 : ( ( real ) ( complex real ext-real ) number ) = b : ( ( real ) ( complex real ext-real ) number ) / a : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) & a2 : ( ( real ) ( complex real ext-real ) number ) = c : ( ( real ) ( complex real ext-real ) number ) / a : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) & a3 : ( ( real ) ( complex real ext-real ) number ) = d : ( ( real ) ( complex real ext-real ) number ) / a : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) holds
(((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 ) + (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 ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) - (b : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) * (a : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) * ((b : ( ( 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * d : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) - (b : ( ( real ) ( complex real ext-real ) number ) * c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) * (a : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 :: POLYEQ_1:17

for y, a, c, b, d being ( ( real ) ( complex real ext-real ) number ) st (((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 ) + (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 ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) - (b : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) * (a : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) * ((b : ( ( 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * d : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) - (b : ( ( real ) ( complex real ext-real ) number ) * c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) * (a : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 p, q being ( ( real ) ( complex real ext-real ) number ) st p : ( ( 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) - (b : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) * (a : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) & q : ( ( real ) ( complex real ext-real ) number ) = (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 ) )) )) * ((b : ( ( 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * d : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) - (b : ( ( real ) ( complex real ext-real ) number ) * c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) * (a : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) holds
Polynom (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 ) )) )) ,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 ) )) )) ,p : ( ( real ) ( complex real ext-real ) number ) ,q : ( ( 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 ) )) )) ;

theorem :: POLYEQ_1:18

theorem :: POLYEQ_1:19

for p, q, y being ( ( real ) ( complex real ext-real ) number ) st Polynom (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 ) )) )) ,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 ) )) )) ,p : ( ( real ) ( complex real ext-real ) number ) ,q : ( ( 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
for u, v being ( ( real ) ( complex real ext-real ) number ) st y : ( ( real ) ( complex real ext-real ) number ) = u : ( ( real ) ( complex real ext-real ) number ) + v : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( 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 ) )) )) * v : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * u : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + p : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) & not 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 ) )) )) -root ((- (q : ( ( real ) ( complex real ext-real ) number ) / 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( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + (sqrt (((q : ( ( 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + ((p : ( ( 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 ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) -root ((- (q : ( ( real ) ( complex real ext-real ) number ) / 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( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) - (sqrt (((q : ( ( 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + ((p : ( ( 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 ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) & not 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 ) )) )) -root ((- (q : ( ( real ) ( complex real ext-real ) number ) / 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( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + (sqrt (((q : ( ( 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + ((p : ( ( 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 ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) -root ((- (q : ( ( real ) ( complex real ext-real ) number ) / 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( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + (sqrt (((q : ( ( 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + ((p : ( ( 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 ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) holds
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 ) )) )) -root ((- (q : ( ( real ) ( complex real ext-real ) number ) / 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( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) - (sqrt (((q : ( ( 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + ((p : ( ( 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 ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) -root ((- (q : ( ( real ) ( complex real ext-real ) number ) / 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( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) - (sqrt (((q : ( ( 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + ((p : ( ( 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 ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ;

theorem :: POLYEQ_1:20

for b, c, d, x being ( ( real ) ( complex real ext-real ) number ) st b : ( ( 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 ) )) )) & delta (b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) ,d : ( ( 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 ) )) )) & Polynom (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 ) ,c : ( ( real ) ( complex real ext-real ) number ) ,d : ( ( 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 ) )) )) & not x : ( ( real ) ( complex real ext-real ) number ) = ((- c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (delta (b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) ,d : ( ( 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 ) )) )) * b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) holds
x : ( ( real ) ( complex real ext-real ) number ) = ((- c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (delta (b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) ,d : ( ( 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 ) )) )) * b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ;

theorem :: POLYEQ_1:21

for a, p, c, q, d, 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 ) )) )) & p : ( ( real ) ( complex real ext-real ) number ) = c : ( ( real ) ( complex real ext-real ) number ) / a : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) & q : ( ( real ) ( complex real ext-real ) number ) = d : ( ( real ) ( complex real ext-real ) number ) / a : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) 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 ) ,d : ( ( 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 u, v being ( ( real ) ( complex real ext-real ) number ) st x : ( ( real ) ( complex real ext-real ) number ) = u : ( ( real ) ( complex real ext-real ) number ) + v : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( 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 ) )) )) * v : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * u : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + p : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) & not 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 ) )) )) -root ((- (d : ( ( real ) ( complex real ext-real ) number ) / (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 ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + (sqrt (((d : ( ( 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 ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + ((c : ( ( 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) -root ((- (d : ( ( real ) ( complex real ext-real ) number ) / (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 ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) - (sqrt (((d : ( ( 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 ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + ((c : ( ( 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) & not 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 ) )) )) -root ((- (d : ( ( real ) ( complex real ext-real ) number ) / (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 ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + (sqrt (((d : ( ( 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 ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + ((c : ( ( 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) -root ((- (d : ( ( real ) ( complex real ext-real ) number ) / (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 ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + (sqrt (((d : ( ( 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 ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + ((c : ( ( 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) holds
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 ) )) )) -root ((- (d : ( ( real ) ( complex real ext-real ) number ) / (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 ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) - (sqrt (((d : ( ( 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 ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + ((c : ( ( 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) -root ((- (d : ( ( real ) ( complex real ext-real ) number ) / (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 ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) - (sqrt (((d : ( ( 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 ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) + ((c : ( ( 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 ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) 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 ) )) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ;

theorem :: POLYEQ_1:22

for a, b, c, 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 ) )) )) & delta (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( 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 ) )) )) & Polynom (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,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 ) )) )) ,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 ) )) )) & not 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 ) )) )) & not x : ( ( real ) ( complex real ext-real ) number ) = ((- b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (delta (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( 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 ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) holds
x : ( ( real ) ( complex real ext-real ) number ) = ((- b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (delta (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( 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 ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ;

theorem :: POLYEQ_1:23

for a, c, 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 ) )) )) & c : ( ( real ) ( complex real ext-real ) number ) / a : ( ( 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 ) )) )) & 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 ) )) )) ,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 ) )) )) & not 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 ) )) )) & not x : ( ( real ) ( complex real ext-real ) number ) = sqrt (- (c : ( ( real ) ( complex real ext-real ) number ) / a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( complex ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) holds
x : ( ( real ) ( complex real ext-real ) number ) = - (sqrt (- (c : ( ( real ) ( complex real ext-real ) number ) / a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( complex ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) ;