:: POLYEQ_5 semantic presentation

begin

theorem :: POLYEQ_5:1
for a being ( ( complex ) ( complex ) number ) holds a : ( ( complex ) ( complex ) number ) * a : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = a : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) set ) ;

theorem :: POLYEQ_5:2
for a being ( ( complex ) ( complex ) number ) holds (a : ( ( complex ) ( complex ) number ) * a : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * a : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = a : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) set ) ;

theorem :: POLYEQ_5:3
for a being ( ( complex ) ( complex ) number ) holds ((a : ( ( complex ) ( complex ) number ) * a : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * a : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * a : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = a : ( ( complex ) ( complex ) number ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) set ) ;

theorem :: POLYEQ_5:4
for a, b being ( ( complex ) ( complex ) number ) holds (a : ( ( complex ) ( complex ) number ) - b : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) set ) = ((a : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * b : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (b : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex ) set ) ;

theorem :: POLYEQ_5:5
for a, b being ( ( complex ) ( complex ) number ) holds (a : ( ( complex ) ( complex ) number ) - b : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) set ) = (((a : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - ((3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) * b : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + ((3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (b : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) * a : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) - (b : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex ) set ) ;

theorem :: POLYEQ_5:6
for a, b being ( ( complex ) ( complex ) number ) holds (a : ( ( complex ) ( complex ) number ) - b : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) set ) = ((((a : ( ( complex ) ( complex ) number ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) * b : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + ((6 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) * (b : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) - ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (b : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) * a : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (b : ( ( complex ) ( complex ) number ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex ) set ) ;

notation
let n be ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Nat) ;
let r be ( ( real ) ( complex real ext-real ) number ) ;
synonym n -real-root r for n -root r;
end;

definition
let n be ( ( non zero natural ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Nat) ;
let z be ( ( complex ) ( complex ) number ) ;
func n -root z -> ( ( complex ) ( complex ) number ) equals :: POLYEQ_5:def 1
(n : ( ( complex ) ( complex ) set ) -real-root |.z : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( real ) ( complex real ext-real ) set ) * ((cos ((Arg z : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) / n : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) + ((sin ((Arg z : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) / n : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;
end;

theorem :: POLYEQ_5:7
for z being ( ( complex ) ( complex ) number )
for n0 being ( ( non zero natural ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Nat) holds (n0 : ( ( non zero natural ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Nat) -root z : ( ( complex ) ( complex ) number ) ) : ( ( complex ) ( complex ) number ) |^ n0 : ( ( non zero natural ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Nat) : ( ( ) ( complex ) set ) = z : ( ( complex ) ( complex ) number ) ;

theorem :: POLYEQ_5:8
for n0 being ( ( non zero natural ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Nat)
for r being ( ( real ) ( complex real ext-real ) number ) st r : ( ( real ) ( complex real ext-real ) number ) >= 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
n0 : ( ( non zero natural ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Nat) -root r : ( ( real ) ( complex real ext-real ) number ) : ( ( complex ) ( complex ) number ) = n0 : ( ( non zero natural ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Nat) -real-root r : ( ( real ) ( complex real ext-real ) number ) : ( ( real ) ( complex real ext-real ) set ) ;

theorem :: POLYEQ_5:9
for z being ( ( complex ) ( complex ) number )
for n0 being ( ( non zero natural ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Nat)
for r being ( ( real ) ( complex real ext-real ) number ) st r : ( ( real ) ( complex real ext-real ) number ) > 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
n0 : ( ( non zero natural ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Nat) -root (z : ( ( complex ) ( complex ) number ) / r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( complex ) ( complex ) number ) = (n0 : ( ( non zero natural ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Nat) -root z : ( ( complex ) ( complex ) number ) ) : ( ( complex ) ( complex ) number ) / (n0 : ( ( non zero natural ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Nat) -root r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ;

theorem :: POLYEQ_5:10
for a, z being ( ( complex ) ( complex ) number ) holds
( z : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) set ) = a : ( ( complex ) ( complex ) number ) iff ( z : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) number ) or z : ( ( complex ) ( complex ) number ) = - (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( complex ) ( complex ) number ) ) : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) set ) ) ) ;

begin

theorem :: POLYEQ_5:11
for z, a1, s1, s2, a0 being ( ( complex ) ( complex ) number ) st a1 : ( ( complex ) ( complex ) number ) = - (s1 : ( ( complex ) ( complex ) number ) + s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) set ) & a0 : ( ( complex ) ( complex ) number ) = s1 : ( ( complex ) ( complex ) number ) * s2 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) holds
( ((z : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) + (a1 : ( ( complex ) ( complex ) number ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + a0 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) iff ( z : ( ( complex ) ( complex ) number ) = s1 : ( ( complex ) ( complex ) number ) or z : ( ( complex ) ( complex ) number ) = s2 : ( ( complex ) ( complex ) number ) ) ) ;

theorem :: POLYEQ_5:12
for z, a2, a1, a0 being ( ( complex ) ( complex ) number ) st a2 : ( ( complex ) ( complex ) number ) <> 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
( ((a2 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a1 : ( ( complex ) ( complex ) number ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + a0 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) iff ( z : ( ( complex ) ( complex ) number ) = (- (a1 : ( ( complex ) ( complex ) number ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) + ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (delta (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) )) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) number ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) or z : ( ( complex ) ( complex ) number ) = (- (a1 : ( ( complex ) ( complex ) number ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) - ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (delta (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) )) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) number ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) ) ;

begin

theorem :: POLYEQ_5:13
for z, a2, a1, a0, x, q, r being ( ( complex ) ( complex ) number ) st z : ( ( complex ) ( complex ) number ) = x : ( ( complex ) ( complex ) number ) - (a2 : ( ( complex ) ( complex ) number ) / 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) & q : ( ( complex ) ( complex ) number ) = ((3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (a2 : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 9 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & r : ( ( complex ) ( complex ) number ) = ((((9 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * a1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a2 : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) - (27 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 54 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) holds
( (((z : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) + (a2 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a1 : ( ( complex ) ( complex ) number ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + a0 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) iff ((x : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) + ((3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * x : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) - (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: POLYEQ_5:14
for z, a2, s1, s2, a1, a0, s3 being ( ( complex ) ( complex ) number ) st a2 : ( ( complex ) ( complex ) number ) = - ((s1 : ( ( complex ) ( complex ) number ) + s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) set ) & a1 : ( ( complex ) ( complex ) number ) = ((s1 : ( ( complex ) ( complex ) number ) * s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + (s1 : ( ( complex ) ( complex ) number ) * s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (s2 : ( ( complex ) ( complex ) number ) * s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex ) set ) & a0 : ( ( complex ) ( complex ) number ) = - ((s1 : ( ( complex ) ( complex ) number ) * s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) set ) holds
( (((z : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) + (a2 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a1 : ( ( complex ) ( complex ) number ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + a0 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) iff ( z : ( ( complex ) ( complex ) number ) = s1 : ( ( complex ) ( complex ) number ) or z : ( ( complex ) ( complex ) number ) = s2 : ( ( complex ) ( complex ) number ) or z : ( ( complex ) ( complex ) number ) = s3 : ( ( complex ) ( complex ) number ) ) ) ;

theorem :: POLYEQ_5:15
for z, a1, a2, a0, s1, s2, q, r, s being ( ( complex ) ( complex ) number ) st q : ( ( complex ) ( complex ) number ) = ((3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (a2 : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 9 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & q : ( ( complex ) ( complex ) number ) <> 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & r : ( ( complex ) ( complex ) number ) = ((((9 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * a1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a2 : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) - (27 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 54 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((q : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) + (r : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) number ) & s1 : ( ( complex ) ( complex ) number ) = 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (r : ( ( complex ) ( complex ) number ) + s : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) number ) & s2 : ( ( complex ) ( complex ) number ) = - (q : ( ( complex ) ( complex ) number ) / s1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) holds
( (((z : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) + (a2 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a1 : ( ( complex ) ( complex ) number ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + a0 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) iff ( z : ( ( complex ) ( complex ) number ) = (s1 : ( ( complex ) ( complex ) number ) + s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (a2 : ( ( complex ) ( complex ) number ) / 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) or z : ( ( complex ) ( complex ) number ) = ((- ((s1 : ( ( complex ) ( complex ) number ) + s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) - (a2 : ( ( complex ) ( complex ) number ) / 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) + ((((s1 : ( ( complex ) ( complex ) number ) - s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) or z : ( ( complex ) ( complex ) number ) = ((- ((s1 : ( ( complex ) ( complex ) number ) + s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) - (a2 : ( ( complex ) ( complex ) number ) / 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) - ((((s1 : ( ( complex ) ( complex ) number ) - s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) ) ;

theorem :: POLYEQ_5:16
for z, a1, a2, a0, s1, q, r being ( ( complex ) ( complex ) number ) st q : ( ( complex ) ( complex ) number ) = ((3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (a2 : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 9 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & q : ( ( complex ) ( complex ) number ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & r : ( ( complex ) ( complex ) number ) = ((((9 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * a1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a2 : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) - (27 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 54 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s1 : ( ( complex ) ( complex ) number ) = 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) number ) holds
( (((z : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) + (a2 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a1 : ( ( complex ) ( complex ) number ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + a0 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) iff ( z : ( ( complex ) ( complex ) number ) = s1 : ( ( complex ) ( complex ) number ) - (a2 : ( ( complex ) ( complex ) number ) / 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) or z : ( ( complex ) ( complex ) number ) = ((- (s1 : ( ( complex ) ( complex ) number ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) - (a2 : ( ( complex ) ( complex ) number ) / 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) + (((s1 : ( ( complex ) ( complex ) number ) * (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) or z : ( ( complex ) ( complex ) number ) = ((- (s1 : ( ( complex ) ( complex ) number ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) - (a2 : ( ( complex ) ( complex ) number ) / 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) - (((s1 : ( ( complex ) ( complex ) number ) * (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) ) ;

definition
let a0, a1, a2 be ( ( complex ) ( complex ) number ) ;
func 1_root_of_cubic (a0,a1,a2) -> ( ( complex ) ( complex ) number ) means :: POLYEQ_5:def 2
 ex r, s1 being ( ( complex ) ( complex ) number ) st
( r : ( ( complex ) ( complex ) number ) = ((((9 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) ) : ( ( ) ( complex real ext-real ) set ) - (27 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 54 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s1 : ( ( complex ) ( complex ) number ) = 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) number ) & it : ( ( ) ( ) set ) = s1 : ( ( complex ) ( complex ) number ) - (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) / 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) ) if (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) : ( ( ) ( complex real ext-real ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )
otherwise ex q, r, s, s1, s2 being ( ( complex ) ( complex ) number ) st
( q : ( ( complex ) ( complex ) number ) = ((3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 9 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) & r : ( ( complex ) ( complex ) number ) = ((((9 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) ) : ( ( ) ( complex real ext-real ) set ) - (27 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 54 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((q : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) + (r : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) number ) & s1 : ( ( complex ) ( complex ) number ) = 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (r : ( ( complex ) ( complex ) number ) + s : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) number ) & s2 : ( ( complex ) ( complex ) number ) = - (q : ( ( complex ) ( complex ) number ) / s1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & it : ( ( ) ( ) set ) = (s1 : ( ( complex ) ( complex ) number ) + s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) / 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) );
func 2_root_of_cubic (a0,a1,a2) -> ( ( complex ) ( complex ) number ) means :: POLYEQ_5:def 3
 ex r, s1 being ( ( complex ) ( complex ) number ) st
( r : ( ( complex ) ( complex ) number ) = ((((9 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) ) : ( ( ) ( complex real ext-real ) set ) - (27 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 54 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s1 : ( ( complex ) ( complex ) number ) = 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) number ) & it : ( ( ) ( ) set ) = ((- (s1 : ( ( complex ) ( complex ) number ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) - (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) / 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) + (((s1 : ( ( complex ) ( complex ) number ) * (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) if (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) : ( ( ) ( complex real ext-real ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )
otherwise ex q, r, s, s1, s2 being ( ( complex ) ( complex ) number ) st
( q : ( ( complex ) ( complex ) number ) = ((3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 9 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) & r : ( ( complex ) ( complex ) number ) = ((((9 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) ) : ( ( ) ( complex real ext-real ) set ) - (27 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 54 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((q : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) + (r : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) number ) & s1 : ( ( complex ) ( complex ) number ) = 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (r : ( ( complex ) ( complex ) number ) + s : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) number ) & s2 : ( ( complex ) ( complex ) number ) = - (q : ( ( complex ) ( complex ) number ) / s1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & it : ( ( ) ( ) set ) = ((- ((s1 : ( ( complex ) ( complex ) number ) + s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) - (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) / 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) + ((((s1 : ( ( complex ) ( complex ) number ) - s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) );
func 3_root_of_cubic (a0,a1,a2) -> ( ( complex ) ( complex ) number ) means :: POLYEQ_5:def 4
 ex r, s1 being ( ( complex ) ( complex ) number ) st
( r : ( ( complex ) ( complex ) number ) = ((((9 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) ) : ( ( ) ( complex real ext-real ) set ) - (27 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 54 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s1 : ( ( complex ) ( complex ) number ) = 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) number ) & it : ( ( ) ( ) set ) = ((- (s1 : ( ( complex ) ( complex ) number ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) - (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) / 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) - (((s1 : ( ( complex ) ( complex ) number ) * (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) if (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) : ( ( ) ( complex real ext-real ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )
otherwise ex q, r, s, s1, s2 being ( ( complex ) ( complex ) number ) st
( q : ( ( complex ) ( complex ) number ) = ((3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 9 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) & r : ( ( complex ) ( complex ) number ) = ((((9 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) ) : ( ( ) ( complex real ext-real ) set ) - (27 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 54 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((q : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) + (r : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) number ) & s1 : ( ( complex ) ( complex ) number ) = 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (r : ( ( complex ) ( complex ) number ) + s : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) number ) & s2 : ( ( complex ) ( complex ) number ) = - (q : ( ( complex ) ( complex ) number ) / s1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & it : ( ( ) ( ) set ) = ((- ((s1 : ( ( complex ) ( complex ) number ) + s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) - (a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) / 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) - ((((s1 : ( ( complex ) ( complex ) number ) - s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) );
end;

theorem :: POLYEQ_5:17
for a0, a1, a2 being ( ( complex ) ( complex ) number ) holds ((1_root_of_cubic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) + (2_root_of_cubic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + (3_root_of_cubic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = - a2 : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) set ) ;

theorem :: POLYEQ_5:18
for a0, a1, a2 being ( ( complex ) ( complex ) number ) holds (((1_root_of_cubic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) * (2_root_of_cubic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + ((1_root_of_cubic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) * (3_root_of_cubic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + ((2_root_of_cubic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) * (3_root_of_cubic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex ) set ) = a1 : ( ( complex ) ( complex ) number ) ;

theorem :: POLYEQ_5:19
for a0, a1, a2 being ( ( complex ) ( complex ) number ) holds ((1_root_of_cubic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) * (2_root_of_cubic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * (3_root_of_cubic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = - a0 : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) set ) ;

theorem :: POLYEQ_5:20
for z, a2, a1, a0, a3 being ( ( complex ) ( complex ) number ) st a3 : ( ( complex ) ( complex ) number ) <> 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
( (((a3 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a2 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a1 : ( ( complex ) ( complex ) number ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + a0 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) iff ( z : ( ( complex ) ( complex ) number ) = 1_root_of_cubic ((a0 : ( ( complex ) ( complex ) number ) / a3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a1 : ( ( complex ) ( complex ) number ) / a3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a2 : ( ( complex ) ( complex ) number ) / a3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( complex ) ( complex ) number ) or z : ( ( complex ) ( complex ) number ) = 2_root_of_cubic ((a0 : ( ( complex ) ( complex ) number ) / a3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a1 : ( ( complex ) ( complex ) number ) / a3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a2 : ( ( complex ) ( complex ) number ) / a3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( complex ) ( complex ) number ) or z : ( ( complex ) ( complex ) number ) = 3_root_of_cubic ((a0 : ( ( complex ) ( complex ) number ) / a3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a1 : ( ( complex ) ( complex ) number ) / a3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a2 : ( ( complex ) ( complex ) number ) / a3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( complex ) ( complex ) number ) ) ) ;

begin

theorem :: POLYEQ_5:21
for z, a2, a1, a0, x, a3, q, r, p being ( ( complex ) ( complex ) number ) st z : ( ( complex ) ( complex ) number ) = x : ( ( complex ) ( complex ) number ) - (a3 : ( ( complex ) ( complex ) number ) / 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) & p : ( ( complex ) ( complex ) number ) = ((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 32 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & q : ( ( complex ) ( complex ) number ) = (((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * a3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a3 : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & r : ( ( complex ) ( complex ) number ) = ((((256 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - ((64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * a1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + ((16 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) * a2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( complex ) ( complex ) number ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 1024 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) holds
( ((((z : ( ( complex ) ( complex ) number ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) + (a3 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a2 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a1 : ( ( complex ) ( complex ) number ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + a0 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) iff (((x : ( ( complex ) ( complex ) number ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) + ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * (x : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + ((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * x : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: POLYEQ_5:22
for z, s1, s2, a2, a1, a0, a3, s3, s4 being ( ( complex ) ( complex ) number ) st a3 : ( ( complex ) ( complex ) number ) = - (((s1 : ( ( complex ) ( complex ) number ) + s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + s4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) set ) & a2 : ( ( complex ) ( complex ) number ) = (((((s1 : ( ( complex ) ( complex ) number ) * s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + (s1 : ( ( complex ) ( complex ) number ) * s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (s1 : ( ( complex ) ( complex ) number ) * s4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (s2 : ( ( complex ) ( complex ) number ) * s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (s2 : ( ( complex ) ( complex ) number ) * s4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (s3 : ( ( complex ) ( complex ) number ) * s4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex ) set ) & a1 : ( ( complex ) ( complex ) number ) = - (((((s1 : ( ( complex ) ( complex ) number ) * s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + ((s1 : ( ( complex ) ( complex ) number ) * s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * s4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + ((s1 : ( ( complex ) ( complex ) number ) * s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * s4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + ((s2 : ( ( complex ) ( complex ) number ) * s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * s4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) set ) & a0 : ( ( complex ) ( complex ) number ) = ((s1 : ( ( complex ) ( complex ) number ) * s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * s4 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) holds
( ((((z : ( ( complex ) ( complex ) number ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) + (a3 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a2 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a1 : ( ( complex ) ( complex ) number ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + a0 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) iff ( z : ( ( complex ) ( complex ) number ) = s1 : ( ( complex ) ( complex ) number ) or z : ( ( complex ) ( complex ) number ) = s2 : ( ( complex ) ( complex ) number ) or z : ( ( complex ) ( complex ) number ) = s3 : ( ( complex ) ( complex ) number ) or z : ( ( complex ) ( complex ) number ) = s4 : ( ( complex ) ( complex ) number ) ) ) ;

theorem :: POLYEQ_5:23
for z, s1, s2, q, r, s3, p being ( ( complex ) ( complex ) number ) st q : ( ( complex ) ( complex ) number ) <> 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & s1 : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (1_root_of_cubic ((- (q : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ,((p : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ,(2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) )) : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) number ) & s2 : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (2_root_of_cubic ((- (q : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ,((p : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ,(2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) )) : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) number ) & s3 : ( ( complex ) ( complex ) number ) = - (q : ( ( complex ) ( complex ) number ) / (s1 : ( ( complex ) ( complex ) number ) * s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) holds
( (((z : ( ( complex ) ( complex ) number ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) + ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * (z : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + ((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) iff ( z : ( ( complex ) ( complex ) number ) = (s1 : ( ( complex ) ( complex ) number ) + s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + s3 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) or z : ( ( complex ) ( complex ) number ) = (s1 : ( ( complex ) ( complex ) number ) - s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - s3 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) or z : ( ( complex ) ( complex ) number ) = ((- s1 : ( ( complex ) ( complex ) number ) ) : ( ( complex ) ( complex ) set ) + s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - s3 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) or z : ( ( complex ) ( complex ) number ) = ((- s1 : ( ( complex ) ( complex ) number ) ) : ( ( complex ) ( complex ) set ) - s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + s3 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) ) ) ;

theorem :: POLYEQ_5:24
for z, a2, a1, a0, s1, s2, a3, q, r, s3, p being ( ( complex ) ( complex ) number ) st p : ( ( complex ) ( complex ) number ) = ((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 32 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & q : ( ( complex ) ( complex ) number ) = (((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * a3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a3 : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & q : ( ( complex ) ( complex ) number ) <> 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & r : ( ( complex ) ( complex ) number ) = ((((256 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - ((64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * a1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + ((16 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) * a2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( complex ) ( complex ) number ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 1024 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s1 : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (1_root_of_cubic ((- (q : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ,((p : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ,(2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) )) : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) number ) & s2 : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (2_root_of_cubic ((- (q : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ,((p : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ,(2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) )) : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) number ) & s3 : ( ( complex ) ( complex ) number ) = - (q : ( ( complex ) ( complex ) number ) / (s1 : ( ( complex ) ( complex ) number ) * s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) holds
( ((((z : ( ( complex ) ( complex ) number ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) + (a3 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a2 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a1 : ( ( complex ) ( complex ) number ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + a0 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) iff ( z : ( ( complex ) ( complex ) number ) = ((s1 : ( ( complex ) ( complex ) number ) + s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (a3 : ( ( complex ) ( complex ) number ) / 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) or z : ( ( complex ) ( complex ) number ) = ((s1 : ( ( complex ) ( complex ) number ) - s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (a3 : ( ( complex ) ( complex ) number ) / 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) or z : ( ( complex ) ( complex ) number ) = (((- s1 : ( ( complex ) ( complex ) number ) ) : ( ( complex ) ( complex ) set ) + s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (a3 : ( ( complex ) ( complex ) number ) / 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) or z : ( ( complex ) ( complex ) number ) = (((- s1 : ( ( complex ) ( complex ) number ) ) : ( ( complex ) ( complex ) set ) - s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (a3 : ( ( complex ) ( complex ) number ) / 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) ) ) ;

theorem :: POLYEQ_5:25
for z, a2, a1, a0, s1, a3, q, r, p being ( ( complex ) ( complex ) number ) st p : ( ( complex ) ( complex ) number ) = ((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 32 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & q : ( ( complex ) ( complex ) number ) = (((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * a3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a3 : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & q : ( ( complex ) ( complex ) number ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & r : ( ( complex ) ( complex ) number ) = ((((256 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - ((64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * a1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + ((16 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) * a2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( complex ) ( complex ) number ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) / 1024 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s1 : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) number ) holds
( ((((z : ( ( complex ) ( complex ) number ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) + (a3 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a2 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a1 : ( ( complex ) ( complex ) number ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + a0 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) iff ( z : ( ( complex ) ( complex ) number ) = (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (- (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (p : ( ( complex ) ( complex ) number ) - s1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ) : ( ( complex ) ( complex ) number ) - (a3 : ( ( complex ) ( complex ) number ) / 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) or z : ( ( complex ) ( complex ) number ) = (- (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (- (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (p : ( ( complex ) ( complex ) number ) - s1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ) : ( ( complex ) ( complex ) number ) ) : ( ( complex ) ( complex ) set ) - (a3 : ( ( complex ) ( complex ) number ) / 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) or z : ( ( complex ) ( complex ) number ) = (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (- (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (p : ( ( complex ) ( complex ) number ) + s1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ) : ( ( complex ) ( complex ) number ) - (a3 : ( ( complex ) ( complex ) number ) / 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) or z : ( ( complex ) ( complex ) number ) = (- (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (- (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (p : ( ( complex ) ( complex ) number ) + s1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ) : ( ( complex ) ( complex ) number ) ) : ( ( complex ) ( complex ) set ) - (a3 : ( ( complex ) ( complex ) number ) / 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) ) ) ;

definition
let a0, a1, a2, a3 be ( ( complex ) ( complex ) number ) ;
func 1_root_of_quartic (a0,a1,a2,a3) -> ( ( complex ) ( complex ) number ) means :: POLYEQ_5:def 5
 ex p, r, s1 being ( ( complex ) ( complex ) number ) st
( p : ( ( complex ) ( complex ) number ) = ((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 32 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & r : ( ( complex ) ( complex ) number ) = ((((256 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) - ((64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + ((16 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 1024 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s1 : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) number ) & it : ( ( ) ( ) Element of a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) = (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (- (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (p : ( ( complex ) ( complex ) number ) - s1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ) : ( ( complex ) ( complex ) number ) - (a3 : ( ( ) ( ) set ) / 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) ) if ((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) * a3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (a3 : ( ( ) ( ) set ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )
otherwise ex p, q, r, s1, s2, s3 being ( ( complex ) ( complex ) number ) st
( p : ( ( complex ) ( complex ) number ) = ((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 32 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & q : ( ( complex ) ( complex ) number ) = (((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) * a3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (a3 : ( ( ) ( ) set ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & r : ( ( complex ) ( complex ) number ) = ((((256 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) - ((64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + ((16 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 1024 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s1 : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (1_root_of_cubic ((- (q : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ,((p : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ,(2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) )) : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) number ) & s2 : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (2_root_of_cubic ((- (q : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ,((p : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ,(2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) )) : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) number ) & s3 : ( ( complex ) ( complex ) number ) = - (q : ( ( complex ) ( complex ) number ) / (s1 : ( ( complex ) ( complex ) number ) * s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & it : ( ( ) ( ) Element of a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) = ((s1 : ( ( complex ) ( complex ) number ) + s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (a3 : ( ( ) ( ) set ) / 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) );
func 2_root_of_quartic (a0,a1,a2,a3) -> ( ( complex ) ( complex ) number ) means :: POLYEQ_5:def 6
 ex p, r, s1 being ( ( complex ) ( complex ) number ) st
( p : ( ( complex ) ( complex ) number ) = ((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 32 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & r : ( ( complex ) ( complex ) number ) = ((((256 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) - ((64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + ((16 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 1024 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s1 : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) number ) & it : ( ( ) ( ) Element of a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) = (- (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (- (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (p : ( ( complex ) ( complex ) number ) - s1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ) : ( ( complex ) ( complex ) number ) ) : ( ( complex ) ( complex ) set ) - (a3 : ( ( ) ( ) set ) / 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) ) if ((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) * a3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (a3 : ( ( ) ( ) set ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )
otherwise ex p, q, r, s1, s2, s3 being ( ( complex ) ( complex ) number ) st
( p : ( ( complex ) ( complex ) number ) = ((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 32 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & q : ( ( complex ) ( complex ) number ) = (((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) * a3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (a3 : ( ( ) ( ) set ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & r : ( ( complex ) ( complex ) number ) = ((((256 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) - ((64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + ((16 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 1024 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s1 : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (1_root_of_cubic ((- (q : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ,((p : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ,(2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) )) : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) number ) & s2 : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (2_root_of_cubic ((- (q : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ,((p : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ,(2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) )) : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) number ) & s3 : ( ( complex ) ( complex ) number ) = - (q : ( ( complex ) ( complex ) number ) / (s1 : ( ( complex ) ( complex ) number ) * s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & it : ( ( ) ( ) Element of a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) = (((- s1 : ( ( complex ) ( complex ) number ) ) : ( ( complex ) ( complex ) set ) - s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (a3 : ( ( ) ( ) set ) / 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) );
func 3_root_of_quartic (a0,a1,a2,a3) -> ( ( complex ) ( complex ) number ) means :: POLYEQ_5:def 7
 ex p, r, s1 being ( ( complex ) ( complex ) number ) st
( p : ( ( complex ) ( complex ) number ) = ((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 32 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & r : ( ( complex ) ( complex ) number ) = ((((256 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) - ((64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + ((16 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 1024 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s1 : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) number ) & it : ( ( ) ( ) Element of a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) = (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (- (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (p : ( ( complex ) ( complex ) number ) + s1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ) : ( ( complex ) ( complex ) number ) - (a3 : ( ( ) ( ) set ) / 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) ) if ((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) * a3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (a3 : ( ( ) ( ) set ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )
otherwise ex p, q, r, s1, s2, s3 being ( ( complex ) ( complex ) number ) st
( p : ( ( complex ) ( complex ) number ) = ((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 32 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & q : ( ( complex ) ( complex ) number ) = (((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) * a3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (a3 : ( ( ) ( ) set ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & r : ( ( complex ) ( complex ) number ) = ((((256 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) - ((64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + ((16 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 1024 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s1 : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (1_root_of_cubic ((- (q : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ,((p : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ,(2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) )) : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) number ) & s2 : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (2_root_of_cubic ((- (q : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ,((p : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ,(2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) )) : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) number ) & s3 : ( ( complex ) ( complex ) number ) = - (q : ( ( complex ) ( complex ) number ) / (s1 : ( ( complex ) ( complex ) number ) * s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & it : ( ( ) ( ) Element of a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) = (((- s1 : ( ( complex ) ( complex ) number ) ) : ( ( complex ) ( complex ) set ) + s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (a3 : ( ( ) ( ) set ) / 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) );
func 4_root_of_quartic (a0,a1,a2,a3) -> ( ( complex ) ( complex ) number ) means :: POLYEQ_5:def 8
 ex p, r, s1 being ( ( complex ) ( complex ) number ) st
( p : ( ( complex ) ( complex ) number ) = ((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 32 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & r : ( ( complex ) ( complex ) number ) = ((((256 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) - ((64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + ((16 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 1024 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s1 : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( complex ) ( complex ) number ) & it : ( ( ) ( ) Element of a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) = (- (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (- (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (p : ( ( complex ) ( complex ) number ) + s1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ) : ( ( complex ) ( complex ) number ) ) : ( ( complex ) ( complex ) set ) - (a3 : ( ( ) ( ) set ) / 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) ) if ((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) * a3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (a3 : ( ( ) ( ) set ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )
otherwise ex p, q, r, s1, s2, s3 being ( ( complex ) ( complex ) number ) st
( p : ( ( complex ) ( complex ) number ) = ((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 32 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & q : ( ( complex ) ( complex ) number ) = (((8 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) - ((4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) set ) * a3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (a3 : ( ( ) ( ) set ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & r : ( ( complex ) ( complex ) number ) = ((((256 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a0 : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) - ((64 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) * a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + ((16 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) * a2 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a3 : ( ( ) ( ) set ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / 1024 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & s1 : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (1_root_of_cubic ((- (q : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ,((p : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ,(2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) )) : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) number ) & s2 : ( ( complex ) ( complex ) number ) = 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (2_root_of_cubic ((- (q : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( complex ) ( complex ) set ) ,((p : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) - r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ,(2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) )) : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) number ) & s3 : ( ( complex ) ( complex ) number ) = - (q : ( ( complex ) ( complex ) number ) / (s1 : ( ( complex ) ( complex ) number ) * s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) & it : ( ( ) ( ) Element of a1 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) = ((s1 : ( ( complex ) ( complex ) number ) - s2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - s3 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) - (a3 : ( ( ) ( ) set ) / 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( complex ) set ) );
end;

theorem :: POLYEQ_5:26
for a0, a1, a2, a3 being ( ( complex ) ( complex ) number ) holds (((1_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) + (2_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + (3_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + (4_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = - a3 : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) set ) ;

theorem :: POLYEQ_5:27
for a0, a1, a2, a3 being ( ( complex ) ( complex ) number ) holds ((((((1_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) * (2_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + ((1_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) * (3_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + ((1_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) * (4_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + ((2_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) * (3_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + ((2_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) * (4_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + ((3_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) * (4_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex ) set ) = a2 : ( ( complex ) ( complex ) number ) ;

theorem :: POLYEQ_5:28
for a0, a1, a2, a3 being ( ( complex ) ( complex ) number ) holds (((((1_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) * (2_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * (3_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) + (((1_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) * (2_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * (4_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (((1_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) * (3_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * (4_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (((2_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) * (3_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * (4_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex ) set ) = - a1 : ( ( complex ) ( complex ) number ) : ( ( complex ) ( complex ) set ) ;

theorem :: POLYEQ_5:29
for a0, a1, a2, a3 being ( ( complex ) ( complex ) number ) holds (((1_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) * (2_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * (3_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) * (4_root_of_quartic (a0 : ( ( complex ) ( complex ) number ) ,a1 : ( ( complex ) ( complex ) number ) ,a2 : ( ( complex ) ( complex ) number ) ,a3 : ( ( complex ) ( complex ) number ) )) : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = a0 : ( ( complex ) ( complex ) number ) ;

theorem :: POLYEQ_5:30
for z, a2, a1, a0, a3, a4 being ( ( complex ) ( complex ) number ) st a4 : ( ( complex ) ( complex ) number ) <> 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
( ((((a4 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a3 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a2 : ( ( complex ) ( complex ) number ) * (z : ( ( complex ) ( complex ) number ) |^ 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + (a1 : ( ( complex ) ( complex ) number ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) + a0 : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) iff ( z : ( ( complex ) ( complex ) number ) = 1_root_of_quartic ((a0 : ( ( complex ) ( complex ) number ) / a4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a1 : ( ( complex ) ( complex ) number ) / a4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a2 : ( ( complex ) ( complex ) number ) / a4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a3 : ( ( complex ) ( complex ) number ) / a4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( complex ) ( complex ) number ) or z : ( ( complex ) ( complex ) number ) = 2_root_of_quartic ((a0 : ( ( complex ) ( complex ) number ) / a4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a1 : ( ( complex ) ( complex ) number ) / a4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a2 : ( ( complex ) ( complex ) number ) / a4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a3 : ( ( complex ) ( complex ) number ) / a4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( complex ) ( complex ) number ) or z : ( ( complex ) ( complex ) number ) = 3_root_of_quartic ((a0 : ( ( complex ) ( complex ) number ) / a4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a1 : ( ( complex ) ( complex ) number ) / a4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a2 : ( ( complex ) ( complex ) number ) / a4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a3 : ( ( complex ) ( complex ) number ) / a4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( complex ) ( complex ) number ) or z : ( ( complex ) ( complex ) number ) = 4_root_of_quartic ((a0 : ( ( complex ) ( complex ) number ) / a4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a1 : ( ( complex ) ( complex ) number ) / a4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a2 : ( ( complex ) ( complex ) number ) / a4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ,(a3 : ( ( complex ) ( complex ) number ) / a4 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( complex ) ( complex ) number ) ) ) ;