:: POLYEQ_4 semantic presentation

begin

theorem :: POLYEQ_4:1
for b, a, c being ( ( ) ( complex real ext-real ) Real) st b : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & c : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) >= 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
( ((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & ((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: POLYEQ_4:2
for b, a, c being ( ( ) ( complex real ext-real ) Real) st b : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & c : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) >= 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
( ((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & ((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: POLYEQ_4:3
for c, a, b being ( ( ) ( complex real ext-real ) Real) holds
( not c : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) or ( ((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & ((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) or ( ((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & ((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ;

theorem :: POLYEQ_4:4
for a, x being ( ( ) ( complex real ext-real ) Real)
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st a : ( ( ) ( complex real ext-real ) Real) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) is even & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & x : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) = a : ( ( ) ( complex real ext-real ) Real) & not x : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) holds
x : ( ( ) ( complex real ext-real ) Real) = - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( complex ) ( complex real ext-real ) set ) ;

theorem :: POLYEQ_4:5
for a, b, x being ( ( ) ( complex real ext-real ) Real) st a : ( ( ) ( complex real ext-real ) Real) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & Polynom (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,x : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & not x : ( ( ) ( complex real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
x : ( ( ) ( complex real ext-real ) Real) = - (b : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) ;

theorem :: POLYEQ_4:6
for a, x being ( ( ) ( complex real ext-real ) Real) st a : ( ( ) ( complex real ext-real ) Real) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & Polynom (a : ( ( ) ( complex real ext-real ) Real) ,0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,x : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
x : ( ( ) ( complex real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

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

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

theorem :: POLYEQ_4:9
for a, b, x being ( ( ) ( complex real ext-real ) Real)
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st a : ( ( ) ( complex real ext-real ) Real) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) is odd & Polynom (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(x : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & not x : ( ( ) ( complex real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
x : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (- (b : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( complex ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) ;

theorem :: POLYEQ_4:10
for a, b, x being ( ( ) ( complex real ext-real ) Real)
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st a : ( ( ) ( complex real ext-real ) Real) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) is even & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & Polynom (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(x : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & not x : ( ( ) ( complex real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & not x : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (- (b : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( complex ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) holds
x : ( ( ) ( complex real ext-real ) Real) = - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (- (b : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( complex ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) ;

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

theorem :: POLYEQ_4:12
for a, b, x being ( ( ) ( complex real ext-real ) Real) st a : ( ( ) ( complex real ext-real ) Real) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & ((b : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) * b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) >= 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & Polynom (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,a : ( ( ) ( complex real ext-real ) Real) ,x : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & not x : ( ( ) ( complex real ext-real ) Real) = - 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non zero complex real ext-real non positive V33() ) set ) & not x : ( ( ) ( complex real ext-real ) Real) = ((a : ( ( ) ( complex real ext-real ) Real) - b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) + (sqrt (((b : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) * b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) holds
x : ( ( ) ( complex real ext-real ) Real) = ((a : ( ( ) ( complex real ext-real ) Real) - b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) - (sqrt (((b : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) * b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) - (3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * (a : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) ;

definition
let a, b, c, d, e, f, x be ( ( complex ) ( complex ) number ) ;
func Polynom (a,b,c,d,e,f,x) -> ( ( ) ( ) set ) equals :: POLYEQ_4:def 1
(((((a : ( ( ) ( ) set ) * (x : ( ( ) ( ) Element of K6(c : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) |^ 5 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (b : ( ( V21() V30(a : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) ) ) ( V21() V30(a : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) ) ) Element of K6(K7(a : ( ( ) ( ) set ) ,a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) * (x : ( ( ) ( ) Element of K6(c : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) |^ 4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (c : ( ( ) ( ) set ) * (x : ( ( ) ( ) Element of K6(c : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) |^ 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (d : ( ( ) ( ) set ) * (x : ( ( ) ( ) Element of K6(c : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ^2) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (e : ( ( complex ) ( complex ) set ) * x : ( ( ) ( ) Element of K6(c : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + f : ( ( complex ) ( complex ) set ) : ( ( ) ( ) set ) ;
end;

registration
let a, b, c, d, e, f, x be ( ( complex ) ( complex ) number ) ;
cluster Polynom (a : ( ( complex ) ( complex ) set ) ,b : ( ( complex ) ( complex ) set ) ,c : ( ( complex ) ( complex ) set ) ,d : ( ( complex ) ( complex ) set ) ,e : ( ( complex ) ( complex ) set ) ,f : ( ( complex ) ( complex ) set ) ,x : ( ( complex ) ( complex ) set ) ) : ( ( ) ( ) set ) -> complex ;
end;

registration
let a, b, c, d, e, f, x be ( ( real ) ( complex real ext-real ) number ) ;
cluster Polynom (a : ( ( real ) ( complex real ext-real ) set ) ,b : ( ( real ) ( complex real ext-real ) set ) ,c : ( ( real ) ( complex real ext-real ) set ) ,d : ( ( real ) ( complex real ext-real ) set ) ,e : ( ( real ) ( complex real ext-real ) set ) ,f : ( ( real ) ( complex real ext-real ) set ) ,x : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex ) set ) -> real ;
end;

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

theorem :: POLYEQ_4:14
for x, y, p, q being ( ( ) ( complex real ext-real ) Real) st x : ( ( ) ( complex real ext-real ) Real) + y : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) = p : ( ( ) ( complex real ext-real ) Real) & x : ( ( ) ( complex real ext-real ) Real) * y : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) = q : ( ( ) ( complex real ext-real ) Real) & (p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) >= 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & not ( x : ( ( ) ( complex real ext-real ) Real) = (p : ( ( ) ( complex real ext-real ) Real) + (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = (p : ( ( ) ( complex real ext-real ) Real) - (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) ) holds
( x : ( ( ) ( complex real ext-real ) Real) = (p : ( ( ) ( complex real ext-real ) Real) - (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = (p : ( ( ) ( complex real ext-real ) Real) + (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) ) ;

theorem :: POLYEQ_4:15
for x, y, p, q being ( ( ) ( complex real ext-real ) Real)
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st (x : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) + (y : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( complex real ext-real ) set ) = p : ( ( ) ( complex real ext-real ) Real) & (x : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) * (y : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( complex real ext-real ) set ) = q : ( ( ) ( complex real ext-real ) Real) & (p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) >= 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) is odd & not ( x : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) + (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) - (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) ) holds
( x : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) - (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) + (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) ) ;

theorem :: POLYEQ_4:16
for x, y, p, q being ( ( ) ( complex real ext-real ) Real)
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st (x : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) + (y : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( complex real ext-real ) set ) = p : ( ( ) ( complex real ext-real ) Real) & (x : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) * (y : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( complex real ext-real ) set ) = q : ( ( ) ( complex real ext-real ) Real) & (p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) >= 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & p : ( ( ) ( complex real ext-real ) Real) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & q : ( ( ) ( complex real ext-real ) Real) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) is even & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & not ( x : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) + (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) - (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) ) & not ( x : ( ( ) ( complex real ext-real ) Real) = - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) + (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) - (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) ) & not ( x : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) + (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) - (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) ) & not ( x : ( ( ) ( complex real ext-real ) Real) = - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) + (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) - (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) ) & not ( x : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) - (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) + (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) ) & not ( x : ( ( ) ( complex real ext-real ) Real) = - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) - (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) + (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) ) & not ( x : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) - (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) + (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) ) holds
( x : ( ( ) ( complex real ext-real ) Real) = - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) - (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((p : ( ( ) ( complex real ext-real ) Real) + (sqrt ((p : ( ( ) ( complex real ext-real ) Real) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (4 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) * q : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) ) ;

theorem :: POLYEQ_4:17
for x, y, a, b being ( ( ) ( complex real ext-real ) Real)
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st (x : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) + (y : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( complex real ext-real ) set ) = a : ( ( ) ( complex real ext-real ) Real) & (x : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) - (y : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( complex real ext-real ) set ) = b : ( ( ) ( complex real ext-real ) Real) & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) is even & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( ) ( complex real ext-real ) Real) + b : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( ) ( complex real ext-real ) Real) - b : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & not ( x : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((a : ( ( ) ( complex real ext-real ) Real) + b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((a : ( ( ) ( complex real ext-real ) Real) - b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) ) & not ( x : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((a : ( ( ) ( complex real ext-real ) Real) + b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((a : ( ( ) ( complex real ext-real ) Real) - b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) ) & not ( x : ( ( ) ( complex real ext-real ) Real) = - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((a : ( ( ) ( complex real ext-real ) Real) + b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((a : ( ( ) ( complex real ext-real ) Real) - b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) ) holds
( x : ( ( ) ( complex real ext-real ) Real) = - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((a : ( ( ) ( complex real ext-real ) Real) + b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root ((a : ( ( ) ( complex real ext-real ) Real) - b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) ) ;

theorem :: POLYEQ_4:18
for a, x, b, y, p being ( ( ) ( complex real ext-real ) Real)
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st (a : ( ( ) ( complex real ext-real ) Real) * (x : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) + (b : ( ( ) ( complex real ext-real ) Real) * (y : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) = p : ( ( ) ( complex real ext-real ) Real) & x : ( ( ) ( complex real ext-real ) Real) * y : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) is odd & a : ( ( ) ( complex real ext-real ) Real) * b : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & not ( x : ( ( ) ( complex real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & y : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (p : ( ( ) ( complex real ext-real ) Real) / b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) ) holds
( x : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (p : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: POLYEQ_4:19
for a, x, b, y, p being ( ( ) ( complex real ext-real ) Real)
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st (a : ( ( ) ( complex real ext-real ) Real) * (x : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) + (b : ( ( ) ( complex real ext-real ) Real) * (y : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) = p : ( ( ) ( complex real ext-real ) Real) & x : ( ( ) ( complex real ext-real ) Real) * y : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) is even & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & p : ( ( ) ( complex real ext-real ) Real) / b : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & p : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( ) ( complex real ext-real ) Real) * b : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & not ( x : ( ( ) ( complex real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & y : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (p : ( ( ) ( complex real ext-real ) Real) / b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) ) & not ( x : ( ( ) ( complex real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & y : ( ( ) ( complex real ext-real ) Real) = - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (p : ( ( ) ( complex real ext-real ) Real) / b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) ) & not ( x : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (p : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) holds
( x : ( ( ) ( complex real ext-real ) Real) = - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (p : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: POLYEQ_4:20
for a, x, p, y, q being ( ( ) ( complex real ext-real ) Real)
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st a : ( ( ) ( complex real ext-real ) Real) * (x : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( complex real ext-real ) set ) = p : ( ( ) ( complex real ext-real ) Real) & x : ( ( ) ( complex real ext-real ) Real) * y : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) = q : ( ( ) ( complex real ext-real ) Real) & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) is odd & p : ( ( ) ( complex real ext-real ) Real) * a : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
( x : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (p : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = q : ( ( ) ( complex real ext-real ) Real) * (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (a : ( ( ) ( complex real ext-real ) Real) / p : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) ) ;

theorem :: POLYEQ_4:21
for a, x, p, y, q being ( ( ) ( complex real ext-real ) Real)
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st a : ( ( ) ( complex real ext-real ) Real) * (x : ( ( ) ( complex real ext-real ) Real) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( complex real ext-real ) set ) = p : ( ( ) ( complex real ext-real ) Real) & x : ( ( ) ( complex real ext-real ) Real) * y : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) = q : ( ( ) ( complex real ext-real ) Real) & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) is even & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & p : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) set ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( ) ( complex real ext-real ) Real) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & not ( x : ( ( ) ( complex real ext-real ) Real) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (p : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) : ( ( real ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = q : ( ( ) ( complex real ext-real ) Real) * (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (a : ( ( ) ( complex real ext-real ) Real) / p : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) ) holds
( x : ( ( ) ( complex real ext-real ) Real) = - (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (p : ( ( ) ( complex real ext-real ) Real) / a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) & y : ( ( ) ( complex real ext-real ) Real) = - (q : ( ( ) ( complex real ext-real ) Real) * (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -root (a : ( ( ) ( complex real ext-real ) Real) / p : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) ) ;

theorem :: POLYEQ_4:22
for a, x being ( ( ) ( complex real ext-real ) Real) st a : ( ( ) ( complex real ext-real ) Real) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( ) ( complex real ext-real ) Real) <> 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( ) ( complex real ext-real ) Real) to_power x : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) = 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
x : ( ( ) ( complex real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POLYEQ_4:23
for a, x being ( ( ) ( complex real ext-real ) Real) st a : ( ( ) ( complex real ext-real ) Real) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( ) ( complex real ext-real ) Real) <> 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( ) ( complex real ext-real ) Real) to_power x : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) = a : ( ( ) ( complex real ext-real ) Real) holds
x : ( ( ) ( complex real ext-real ) Real) = 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POLYEQ_4:24
for a, b, x being ( ( ) ( complex real ext-real ) Real) st a : ( ( ) ( complex real ext-real ) Real) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( ) ( complex real ext-real ) Real) <> 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & x : ( ( ) ( complex real ext-real ) Real) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & log (a : ( ( ) ( complex real ext-real ) Real) ,x : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
x : ( ( ) ( complex real ext-real ) Real) = 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POLYEQ_4:25
for a, b, x being ( ( ) ( complex real ext-real ) Real) st a : ( ( ) ( complex real ext-real ) Real) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( ) ( complex real ext-real ) Real) <> 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & x : ( ( ) ( complex real ext-real ) Real) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & log (a : ( ( ) ( complex real ext-real ) Real) ,x : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( ) set ) ) = 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
x : ( ( ) ( complex real ext-real ) Real) = a : ( ( ) ( complex real ext-real ) Real) ;