REAL is non empty non trivial complex-membered ext-real-membered real-membered V56() non finite non bounded_below non bounded_above V71() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() non finite left_end bounded_below cardinal limit_cardinal Element of bool REAL
bool REAL is non empty non trivial non finite set
COMPLEX is non empty non trivial complex-membered V56() non finite set
RAT is non empty non trivial complex-membered ext-real-membered real-membered rational-membered V56() non finite set
INT is non empty non trivial complex-membered ext-real-membered real-membered rational-membered integer-membered V56() non finite set
[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial complex-valued non finite set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial complex-valued non finite set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:REAL,REAL:] is Relation-like non empty non trivial complex-valued ext-real-valued real-valued non finite set
bool [:REAL,REAL:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial complex-valued ext-real-valued real-valued non finite set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial complex-valued ext-real-valued real-valued non finite set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial complex-valued ext-real-valued real-valued non finite set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial complex-valued ext-real-valued real-valued non finite set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial complex-valued ext-real-valued real-valued non finite set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial complex-valued ext-real-valued real-valued natural-valued non finite set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial complex-valued ext-real-valued real-valued natural-valued non finite set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() finite finite-yielding V61() bounded_below bounded_above real-bounded V71() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() finite finite-yielding V61() bounded_below bounded_above real-bounded V71() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() finite finite-yielding V61() bounded_below bounded_above real-bounded V71() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() non finite left_end bounded_below cardinal limit_cardinal set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
ExtREAL is non empty ext-real-membered V71() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite left_end right_end bounded_below bounded_above real-bounded cardinal Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() finite finite-yielding V61() bounded_below bounded_above real-bounded V71() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite left_end right_end bounded_below bounded_above real-bounded cardinal Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite left_end right_end bounded_below bounded_above real-bounded cardinal Element of NAT
[:NAT,REAL:] is Relation-like non empty non trivial complex-valued ext-real-valued real-valued non finite set
bool [:NAT,REAL:] is non empty non trivial non finite set
bool [:NAT,NAT:] is non empty non trivial non finite set
dom {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() finite finite-yielding V61() bounded_below bounded_above real-bounded V71() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
rng {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty trivial Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() finite finite-yielding V61() bounded_below bounded_above real-bounded V71() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
|.0.| is complex real ext-real V49() Element of REAL
Re 0 is complex real ext-real Element of REAL
(Re 0) ^2 is complex real ext-real Element of REAL
(Re 0) * (Re 0) is complex real ext-real set
Im 0 is complex real ext-real Element of REAL
(Im 0) ^2 is complex real ext-real Element of REAL
(Im 0) * (Im 0) is complex real ext-real set
((Re 0) ^2) + ((Im 0) ^2) is complex real ext-real Element of REAL
sqrt (((Re 0) ^2) + ((Im 0) ^2)) is complex real ext-real Element of REAL
sqrt 0 is complex real ext-real Element of REAL
compcomplex is Relation-like COMPLEX -defined COMPLEX -valued Function-like non empty total V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
addcomplex is Relation-like [:COMPLEX,COMPLEX:] -defined COMPLEX -valued Function-like non empty total V18([:COMPLEX,COMPLEX:], COMPLEX ) complex-valued commutative associative V79( COMPLEX ) Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
diffcomplex is Relation-like [:COMPLEX,COMPLEX:] -defined COMPLEX -valued Function-like non empty total V18([:COMPLEX,COMPLEX:], COMPLEX ) complex-valued Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
multcomplex is Relation-like [:COMPLEX,COMPLEX:] -defined COMPLEX -valued Function-like non empty total V18([:COMPLEX,COMPLEX:], COMPLEX ) complex-valued commutative associative V79( COMPLEX ) Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
the_unity_wrt addcomplex is complex Element of COMPLEX
the_unity_wrt multcomplex is complex Element of COMPLEX
card {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() finite finite-yielding V61() bounded_below bounded_above real-bounded V71() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
R is complex-membered ext-real-membered real-membered Element of bool REAL
r0 is complex-membered ext-real-membered real-membered Element of bool REAL
r1 is complex real ext-real set
t is complex real ext-real set
r1 is complex real ext-real set
t is complex real ext-real Element of REAL
t is complex real ext-real set
m is complex real ext-real set
R is complex real ext-real set
r0 is complex-membered ext-real-membered real-membered Element of bool REAL
r1 is complex-membered ext-real-membered real-membered Element of bool REAL
t is complex real ext-real set
t is complex real ext-real set
t + R is complex real ext-real Element of REAL
t + 0 is complex real ext-real Element of REAL
t is complex real ext-real set
t is complex real ext-real set
t is complex real ext-real set
t - R is complex real ext-real Element of REAL
m is complex real ext-real set
m + R is complex real ext-real Element of REAL
(t - R) + R is complex real ext-real Element of REAL
- 0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() finite finite-yielding V61() bounded_below bounded_above real-bounded V71() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of REAL
- R is complex real ext-real Element of REAL
t + 0 is complex real ext-real Element of REAL
t + (- R) is complex real ext-real Element of REAL
m is complex real ext-real set
R is complex real ext-real set
r0 is complex real ext-real set
r0 + 1 is complex real ext-real Element of REAL
r0 is complex real ext-real set
r1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
R is complex-membered ext-real-membered real-membered Element of bool REAL
r0 is complex real ext-real set
r1 is complex real ext-real set
r1 is complex real ext-real set
t is complex real ext-real set
abs r0 is complex real ext-real Element of REAL
Re r0 is complex real ext-real Element of REAL
(Re r0) ^2 is complex real ext-real Element of REAL
(Re r0) * (Re r0) is complex real ext-real set
Im r0 is complex real ext-real Element of REAL
(Im r0) ^2 is complex real ext-real Element of REAL
(Im r0) * (Im r0) is complex real ext-real set
((Re r0) ^2) + ((Im r0) ^2) is complex real ext-real Element of REAL
sqrt (((Re r0) ^2) + ((Im r0) ^2)) is complex real ext-real Element of REAL
abs r1 is complex real ext-real Element of REAL
Re r1 is complex real ext-real Element of REAL
(Re r1) ^2 is complex real ext-real Element of REAL
(Re r1) * (Re r1) is complex real ext-real set
Im r1 is complex real ext-real Element of REAL
(Im r1) ^2 is complex real ext-real Element of REAL
(Im r1) * (Im r1) is complex real ext-real set
((Re r1) ^2) + ((Im r1) ^2) is complex real ext-real Element of REAL
sqrt (((Re r1) ^2) + ((Im r1) ^2)) is complex real ext-real Element of REAL
(abs r0) + (abs r1) is complex real ext-real Element of REAL
((abs r0) + (abs r1)) + 1 is complex real ext-real Element of REAL
t is complex real ext-real Element of REAL
t is complex real ext-real set
abs t is complex real ext-real Element of REAL
Re t is complex real ext-real Element of REAL
(Re t) ^2 is complex real ext-real Element of REAL
(Re t) * (Re t) is complex real ext-real set
Im t is complex real ext-real Element of REAL
(Im t) ^2 is complex real ext-real Element of REAL
(Im t) * (Im t) is complex real ext-real set
((Re t) ^2) + ((Im t) ^2) is complex real ext-real Element of REAL
sqrt (((Re t) ^2) + ((Im t) ^2)) is complex real ext-real Element of REAL
t + 0 is complex real ext-real Element of REAL
- (abs r1) is complex real ext-real Element of REAL
- (abs r0) is complex real ext-real Element of REAL
(- (abs r0)) + (- (abs r1)) is complex real ext-real Element of REAL
0 + t is complex real ext-real Element of REAL
(- (abs r0)) - (abs r1) is complex real ext-real Element of REAL
- 1 is complex real ext-real non positive V48() V49() Element of INT
((- (abs r0)) - (abs r1)) + (- 1) is complex real ext-real Element of REAL
((- (abs r0)) - (abs r1)) - 1 is complex real ext-real Element of REAL
- (((abs r0) + (abs r1)) + 1) is complex real ext-real Element of REAL
r0 is complex real ext-real set
- r0 is complex real ext-real Element of REAL
r1 is ext-real set
t is complex real ext-real set
abs t is complex real ext-real Element of REAL
Re t is complex real ext-real Element of REAL
(Re t) ^2 is complex real ext-real Element of REAL
(Re t) * (Re t) is complex real ext-real set
Im t is complex real ext-real Element of REAL
(Im t) ^2 is complex real ext-real Element of REAL
(Im t) * (Im t) is complex real ext-real set
((Re t) ^2) + ((Im t) ^2) is complex real ext-real Element of REAL
sqrt (((Re t) ^2) + ((Im t) ^2)) is complex real ext-real Element of REAL
- (abs t) is complex real ext-real Element of REAL
r1 is ext-real set
t is complex real ext-real set
abs t is complex real ext-real Element of REAL
Re t is complex real ext-real Element of REAL
(Re t) ^2 is complex real ext-real Element of REAL
(Re t) * (Re t) is complex real ext-real set
Im t is complex real ext-real Element of REAL
(Im t) ^2 is complex real ext-real Element of REAL
(Im t) * (Im t) is complex real ext-real set
((Re t) ^2) + ((Im t) ^2) is complex real ext-real Element of REAL
sqrt (((Re t) ^2) + ((Im t) ^2)) is complex real ext-real Element of REAL
R is complex real ext-real set
{R} is non empty trivial complex-membered ext-real-membered real-membered finite left_end right_end bounded_below bounded_above real-bounded 1 -element set
r0 is set
R is complex-membered ext-real-membered real-membered set
r0 is complex real ext-real set
r1 is complex real ext-real set
r1 is complex-membered ext-real-membered real-membered Element of bool REAL
t is complex real ext-real set
t is complex real ext-real set
t is complex real ext-real set
t is complex real ext-real Element of REAL
m is complex real ext-real Element of REAL
m is complex real ext-real set
m - m is complex real ext-real Element of REAL
f1 is complex real ext-real set
m - (m - m) is complex real ext-real Element of REAL
(m - m) - (m - m) is complex real ext-real Element of REAL
m is complex real ext-real set
f1 is complex real ext-real set
m - f1 is complex real ext-real Element of REAL
R is complex real ext-real set
r0 is complex real ext-real set
r1 is complex-membered ext-real-membered real-membered set
R - r0 is complex real ext-real Element of REAL
R - (R - r0) is complex real ext-real Element of REAL
t is complex real ext-real set
r0 - R is complex real ext-real Element of REAL
r0 - (r0 - R) is complex real ext-real Element of REAL
t is complex real ext-real set
R is complex-membered ext-real-membered real-membered set
r0 is complex real ext-real set
r1 is complex real ext-real set
r1 is complex-membered ext-real-membered real-membered Element of bool REAL
t is complex-membered ext-real-membered real-membered Element of bool REAL
t is complex real ext-real set
m is complex real ext-real set
t is complex real ext-real set
m is complex real ext-real Element of REAL
m is complex real ext-real Element of REAL
f1 is complex real ext-real set
m + f1 is complex real ext-real Element of REAL
f2 is complex real ext-real set
(m + f1) - m is complex real ext-real Element of REAL
m - m is complex real ext-real Element of REAL
f1 is complex real ext-real set
f2 is complex real ext-real set
m + f2 is complex real ext-real Element of REAL
R is complex real ext-real set
r0 is complex real ext-real set
r1 is complex-membered ext-real-membered real-membered set
R - r0 is complex real ext-real Element of REAL
r0 + (R - r0) is complex real ext-real Element of REAL
t is complex real ext-real set
r0 - R is complex real ext-real Element of REAL
R + (r0 - R) is complex real ext-real Element of REAL
t is complex real ext-real set
R is complex-membered ext-real-membered real-membered set
r0 is complex real ext-real set
r1 is complex real ext-real set
R is complex-membered ext-real-membered real-membered set
r0 is complex real ext-real set
r1 is complex real ext-real set
R is complex real ext-real set
r0 is non empty complex-membered ext-real-membered real-membered set
(r0) is complex real ext-real set
r1 is complex real ext-real set
R + r1 is complex real ext-real Element of REAL
r1 is ext-real set
R is non empty complex-membered ext-real-membered real-membered set
(R) is complex real ext-real set
r0 is complex real ext-real set
r1 is complex real ext-real set
r0 - r1 is complex real ext-real Element of REAL
r0 + r1 is complex real ext-real Element of REAL
r1 is ext-real set
R is non empty complex-membered ext-real-membered real-membered bounded_below set
(R) is complex real ext-real set
inf R is complex real ext-real set
r0 is complex real ext-real set
r1 is ext-real set
r0 is complex real ext-real set
R is non empty complex-membered ext-real-membered real-membered bounded_above set
(R) is complex real ext-real set
sup R is complex real ext-real set
r0 is complex real ext-real set
r1 is ext-real set
r0 is complex real ext-real set
R is complex-membered ext-real-membered real-membered Element of bool REAL
(R) is complex real ext-real set
(R) is complex real ext-real set
R is complex real ext-real set
(R) is non empty trivial complex-membered ext-real-membered real-membered finite left_end right_end bounded_below bounded_above real-bounded 1 -element Element of bool REAL
((R)) is complex real ext-real Element of REAL
inf (R) is complex real ext-real set
r0 is complex real ext-real set
(r0) is non empty trivial complex-membered ext-real-membered real-membered finite left_end right_end bounded_below bounded_above real-bounded 1 -element Element of bool REAL
((r0)) is complex real ext-real Element of REAL
sup (r0) is complex real ext-real set
R is complex real ext-real set
(R) is non empty trivial complex-membered ext-real-membered real-membered finite left_end right_end bounded_below bounded_above real-bounded 1 -element Element of bool REAL
((R)) is complex real ext-real Element of REAL
inf (R) is complex real ext-real set
((R)) is complex real ext-real Element of REAL
sup (R) is complex real ext-real set
R is complex-membered ext-real-membered real-membered Element of bool REAL
(R) is complex real ext-real Element of REAL
(R) is complex real ext-real Element of REAL
r0 is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded set
(r0) is complex real ext-real set
inf r0 is complex real ext-real set
(r0) is complex real ext-real set
sup r0 is complex real ext-real set
R is complex-membered ext-real-membered real-membered Element of bool REAL
(R) is complex real ext-real Element of REAL
(R) is complex real ext-real Element of REAL
r0 is complex real ext-real set
r1 is complex real ext-real set
r0 is complex real ext-real Element of REAL
r1 is set
t is set
(r0) is non empty trivial complex-membered ext-real-membered real-membered finite left_end right_end bounded_below bounded_above real-bounded 1 -element Element of bool REAL
R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
abs R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
r0 is complex real ext-real set
r1 is complex real ext-real Element of REAL
abs r1 is complex real ext-real Element of REAL
Re r1 is complex real ext-real Element of REAL
(Re r1) ^2 is complex real ext-real Element of REAL
(Re r1) * (Re r1) is complex real ext-real set
Im r1 is complex real ext-real Element of REAL
(Im r1) ^2 is complex real ext-real Element of REAL
(Im r1) * (Im r1) is complex real ext-real set
((Re r1) ^2) + ((Im r1) ^2) is complex real ext-real Element of REAL
sqrt (((Re r1) ^2) + ((Im r1) ^2)) is complex real ext-real Element of REAL
t is complex real ext-real Element of REAL
t is complex real ext-real set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
f1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
(abs R) . f1 is complex real ext-real Element of REAL
((abs R) . f1) - t is complex real ext-real Element of REAL
abs (((abs R) . f1) - t) is complex real ext-real Element of REAL
Re (((abs R) . f1) - t) is complex real ext-real Element of REAL
(Re (((abs R) . f1) - t)) ^2 is complex real ext-real Element of REAL
(Re (((abs R) . f1) - t)) * (Re (((abs R) . f1) - t)) is complex real ext-real set
Im (((abs R) . f1) - t) is complex real ext-real Element of REAL
(Im (((abs R) . f1) - t)) ^2 is complex real ext-real Element of REAL
(Im (((abs R) . f1) - t)) * (Im (((abs R) . f1) - t)) is complex real ext-real set
((Re (((abs R) . f1) - t)) ^2) + ((Im (((abs R) . f1) - t)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (((abs R) . f1) - t)) ^2) + ((Im (((abs R) . f1) - t)) ^2)) is complex real ext-real Element of REAL
R . f1 is complex real ext-real Element of REAL
r1 - (R . f1) is complex real ext-real Element of REAL
abs (r1 - (R . f1)) is complex real ext-real Element of REAL
Re (r1 - (R . f1)) is complex real ext-real Element of REAL
(Re (r1 - (R . f1))) ^2 is complex real ext-real Element of REAL
(Re (r1 - (R . f1))) * (Re (r1 - (R . f1))) is complex real ext-real set
Im (r1 - (R . f1)) is complex real ext-real Element of REAL
(Im (r1 - (R . f1))) ^2 is complex real ext-real Element of REAL
(Im (r1 - (R . f1))) * (Im (r1 - (R . f1))) is complex real ext-real set
((Re (r1 - (R . f1))) ^2) + ((Im (r1 - (R . f1))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (r1 - (R . f1))) ^2) + ((Im (r1 - (R . f1))) ^2)) is complex real ext-real Element of REAL
(R . f1) - r1 is complex real ext-real Element of REAL
- ((R . f1) - r1) is complex real ext-real Element of REAL
abs (- ((R . f1) - r1)) is complex real ext-real Element of REAL
Re (- ((R . f1) - r1)) is complex real ext-real Element of REAL
(Re (- ((R . f1) - r1))) ^2 is complex real ext-real Element of REAL
(Re (- ((R . f1) - r1))) * (Re (- ((R . f1) - r1))) is complex real ext-real set
Im (- ((R . f1) - r1)) is complex real ext-real Element of REAL
(Im (- ((R . f1) - r1))) ^2 is complex real ext-real Element of REAL
(Im (- ((R . f1) - r1))) * (Im (- ((R . f1) - r1))) is complex real ext-real set
((Re (- ((R . f1) - r1))) ^2) + ((Im (- ((R . f1) - r1))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (- ((R . f1) - r1))) ^2) + ((Im (- ((R . f1) - r1))) ^2)) is complex real ext-real Element of REAL
abs ((R . f1) - r1) is complex real ext-real Element of REAL
Re ((R . f1) - r1) is complex real ext-real Element of REAL
(Re ((R . f1) - r1)) ^2 is complex real ext-real Element of REAL
(Re ((R . f1) - r1)) * (Re ((R . f1) - r1)) is complex real ext-real set
Im ((R . f1) - r1) is complex real ext-real Element of REAL
(Im ((R . f1) - r1)) ^2 is complex real ext-real Element of REAL
(Im ((R . f1) - r1)) * (Im ((R . f1) - r1)) is complex real ext-real set
((Re ((R . f1) - r1)) ^2) + ((Im ((R . f1) - r1)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((R . f1) - r1)) ^2) + ((Im ((R . f1) - r1)) ^2)) is complex real ext-real Element of REAL
abs (R . f1) is complex real ext-real Element of REAL
Re (R . f1) is complex real ext-real Element of REAL
(Re (R . f1)) ^2 is complex real ext-real Element of REAL
(Re (R . f1)) * (Re (R . f1)) is complex real ext-real set
Im (R . f1) is complex real ext-real Element of REAL
(Im (R . f1)) ^2 is complex real ext-real Element of REAL
(Im (R . f1)) * (Im (R . f1)) is complex real ext-real set
((Re (R . f1)) ^2) + ((Im (R . f1)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (R . f1)) ^2) + ((Im (R . f1)) ^2)) is complex real ext-real Element of REAL
t - (abs (R . f1)) is complex real ext-real Element of REAL
(abs (R . f1)) - t is complex real ext-real Element of REAL
- (abs ((R . f1) - r1)) is complex real ext-real Element of REAL
- (t - (abs (R . f1))) is complex real ext-real Element of REAL
abs ((abs (R . f1)) - t) is complex real ext-real Element of REAL
Re ((abs (R . f1)) - t) is complex real ext-real Element of REAL
(Re ((abs (R . f1)) - t)) ^2 is complex real ext-real Element of REAL
(Re ((abs (R . f1)) - t)) * (Re ((abs (R . f1)) - t)) is complex real ext-real set
Im ((abs (R . f1)) - t) is complex real ext-real Element of REAL
(Im ((abs (R . f1)) - t)) ^2 is complex real ext-real Element of REAL
(Im ((abs (R . f1)) - t)) * (Im ((abs (R . f1)) - t)) is complex real ext-real set
((Re ((abs (R . f1)) - t)) ^2) + ((Im ((abs (R . f1)) - t)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((abs (R . f1)) - t)) ^2) + ((Im ((abs (R . f1)) - t)) ^2)) is complex real ext-real Element of REAL
(abs R) . f1 is complex real ext-real Element of REAL
((abs R) . f1) - t is complex real ext-real Element of REAL
abs (((abs R) . f1) - t) is complex real ext-real Element of REAL
Re (((abs R) . f1) - t) is complex real ext-real Element of REAL
(Re (((abs R) . f1) - t)) ^2 is complex real ext-real Element of REAL
(Re (((abs R) . f1) - t)) * (Re (((abs R) . f1) - t)) is complex real ext-real set
Im (((abs R) . f1) - t) is complex real ext-real Element of REAL
(Im (((abs R) . f1) - t)) ^2 is complex real ext-real Element of REAL
(Im (((abs R) . f1) - t)) * (Im (((abs R) . f1) - t)) is complex real ext-real set
((Re (((abs R) . f1) - t)) ^2) + ((Im (((abs R) . f1) - t)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (((abs R) . f1) - t)) ^2) + ((Im (((abs R) . f1) - t)) ^2)) is complex real ext-real Element of REAL
R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued bounded_above bounded_below bounded convergent Element of bool [:NAT,REAL:]
abs R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
r0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
abs R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim (abs R) is complex real ext-real Element of REAL
lim R is complex real ext-real Element of REAL
abs (lim R) is complex real ext-real Element of REAL
Re (lim R) is complex real ext-real Element of REAL
(Re (lim R)) ^2 is complex real ext-real Element of REAL
(Re (lim R)) * (Re (lim R)) is complex real ext-real set
Im (lim R) is complex real ext-real Element of REAL
(Im (lim R)) ^2 is complex real ext-real Element of REAL
(Im (lim R)) * (Im (lim R)) is complex real ext-real set
((Re (lim R)) ^2) + ((Im (lim R)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (lim R)) ^2) + ((Im (lim R)) ^2)) is complex real ext-real Element of REAL
r0 is complex real ext-real set
r1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
R . t is complex real ext-real Element of REAL
(lim R) - (R . t) is complex real ext-real Element of REAL
abs ((lim R) - (R . t)) is complex real ext-real Element of REAL
Re ((lim R) - (R . t)) is complex real ext-real Element of REAL
(Re ((lim R) - (R . t))) ^2 is complex real ext-real Element of REAL
(Re ((lim R) - (R . t))) * (Re ((lim R) - (R . t))) is complex real ext-real set
Im ((lim R) - (R . t)) is complex real ext-real Element of REAL
(Im ((lim R) - (R . t))) ^2 is complex real ext-real Element of REAL
(Im ((lim R) - (R . t))) * (Im ((lim R) - (R . t))) is complex real ext-real set
((Re ((lim R) - (R . t))) ^2) + ((Im ((lim R) - (R . t))) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((lim R) - (R . t))) ^2) + ((Im ((lim R) - (R . t))) ^2)) is complex real ext-real Element of REAL
(R . t) - (lim R) is complex real ext-real Element of REAL
- ((R . t) - (lim R)) is complex real ext-real Element of REAL
abs (- ((R . t) - (lim R))) is complex real ext-real Element of REAL
Re (- ((R . t) - (lim R))) is complex real ext-real Element of REAL
(Re (- ((R . t) - (lim R)))) ^2 is complex real ext-real Element of REAL
(Re (- ((R . t) - (lim R)))) * (Re (- ((R . t) - (lim R)))) is complex real ext-real set
Im (- ((R . t) - (lim R))) is complex real ext-real Element of REAL
(Im (- ((R . t) - (lim R)))) ^2 is complex real ext-real Element of REAL
(Im (- ((R . t) - (lim R)))) * (Im (- ((R . t) - (lim R)))) is complex real ext-real set
((Re (- ((R . t) - (lim R)))) ^2) + ((Im (- ((R . t) - (lim R)))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (- ((R . t) - (lim R)))) ^2) + ((Im (- ((R . t) - (lim R)))) ^2)) is complex real ext-real Element of REAL
abs ((R . t) - (lim R)) is complex real ext-real Element of REAL
Re ((R . t) - (lim R)) is complex real ext-real Element of REAL
(Re ((R . t) - (lim R))) ^2 is complex real ext-real Element of REAL
(Re ((R . t) - (lim R))) * (Re ((R . t) - (lim R))) is complex real ext-real set
Im ((R . t) - (lim R)) is complex real ext-real Element of REAL
(Im ((R . t) - (lim R))) ^2 is complex real ext-real Element of REAL
(Im ((R . t) - (lim R))) * (Im ((R . t) - (lim R))) is complex real ext-real set
((Re ((R . t) - (lim R))) ^2) + ((Im ((R . t) - (lim R))) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((R . t) - (lim R))) ^2) + ((Im ((R . t) - (lim R))) ^2)) is complex real ext-real Element of REAL
abs (R . t) is complex real ext-real Element of REAL
Re (R . t) is complex real ext-real Element of REAL
(Re (R . t)) ^2 is complex real ext-real Element of REAL
(Re (R . t)) * (Re (R . t)) is complex real ext-real set
Im (R . t) is complex real ext-real Element of REAL
(Im (R . t)) ^2 is complex real ext-real Element of REAL
(Im (R . t)) * (Im (R . t)) is complex real ext-real set
((Re (R . t)) ^2) + ((Im (R . t)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (R . t)) ^2) + ((Im (R . t)) ^2)) is complex real ext-real Element of REAL
(abs (lim R)) - (abs (R . t)) is complex real ext-real Element of REAL
(abs (R . t)) - (abs (lim R)) is complex real ext-real Element of REAL
- (abs ((R . t) - (lim R))) is complex real ext-real Element of REAL
- ((abs (lim R)) - (abs (R . t))) is complex real ext-real Element of REAL
abs ((abs (R . t)) - (abs (lim R))) is complex real ext-real Element of REAL
Re ((abs (R . t)) - (abs (lim R))) is complex real ext-real Element of REAL
(Re ((abs (R . t)) - (abs (lim R)))) ^2 is complex real ext-real Element of REAL
(Re ((abs (R . t)) - (abs (lim R)))) * (Re ((abs (R . t)) - (abs (lim R)))) is complex real ext-real set
Im ((abs (R . t)) - (abs (lim R))) is complex real ext-real Element of REAL
(Im ((abs (R . t)) - (abs (lim R)))) ^2 is complex real ext-real Element of REAL
(Im ((abs (R . t)) - (abs (lim R)))) * (Im ((abs (R . t)) - (abs (lim R)))) is complex real ext-real set
((Re ((abs (R . t)) - (abs (lim R)))) ^2) + ((Im ((abs (R . t)) - (abs (lim R)))) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((abs (R . t)) - (abs (lim R)))) ^2) + ((Im ((abs (R . t)) - (abs (lim R)))) ^2)) is complex real ext-real Element of REAL
(abs R) . t is complex real ext-real Element of REAL
((abs R) . t) - (abs (lim R)) is complex real ext-real Element of REAL
abs (((abs R) . t) - (abs (lim R))) is complex real ext-real Element of REAL
Re (((abs R) . t) - (abs (lim R))) is complex real ext-real Element of REAL
(Re (((abs R) . t) - (abs (lim R)))) ^2 is complex real ext-real Element of REAL
(Re (((abs R) . t) - (abs (lim R)))) * (Re (((abs R) . t) - (abs (lim R)))) is complex real ext-real set
Im (((abs R) . t) - (abs (lim R))) is complex real ext-real Element of REAL
(Im (((abs R) . t) - (abs (lim R)))) ^2 is complex real ext-real Element of REAL
(Im (((abs R) . t) - (abs (lim R)))) * (Im (((abs R) . t) - (abs (lim R)))) is complex real ext-real set
((Re (((abs R) . t) - (abs (lim R)))) ^2) + ((Im (((abs R) . t) - (abs (lim R)))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (((abs R) . t) - (abs (lim R)))) ^2) + ((Im (((abs R) . t) - (abs (lim R)))) ^2)) is complex real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
abs R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim (abs R) is complex real ext-real Element of REAL
lim R is complex real ext-real Element of REAL
r0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
R . r0 is complex real ext-real Element of REAL
abs (R . r0) is complex real ext-real Element of REAL
Re (R . r0) is complex real ext-real Element of REAL
(Re (R . r0)) ^2 is complex real ext-real Element of REAL
(Re (R . r0)) * (Re (R . r0)) is complex real ext-real set
Im (R . r0) is complex real ext-real Element of REAL
(Im (R . r0)) ^2 is complex real ext-real Element of REAL
(Im (R . r0)) * (Im (R . r0)) is complex real ext-real set
((Re (R . r0)) ^2) + ((Im (R . r0)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (R . r0)) ^2) + ((Im (R . r0)) ^2)) is complex real ext-real Element of REAL
- (abs (R . r0)) is complex real ext-real Element of REAL
(abs R) . r0 is complex real ext-real Element of REAL
- ((abs R) . r0) is complex real ext-real Element of REAL
- (abs R) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- 1 is complex real ext-real non positive set
(- 1) (#) (abs R) is Relation-like NAT -defined Function-like non empty total complex-valued ext-real-valued real-valued set
(- (abs R)) . r0 is complex real ext-real Element of REAL
lim (- (abs R)) is complex real ext-real Element of REAL
- (lim (abs R)) is complex real ext-real Element of REAL
R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
r0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
r1 is complex real ext-real set
t is complex real ext-real set
t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
R . m is complex real ext-real Element of REAL
(R . m) - r1 is complex real ext-real Element of REAL
abs ((R . m) - r1) is complex real ext-real Element of REAL
Re ((R . m) - r1) is complex real ext-real Element of REAL
(Re ((R . m) - r1)) ^2 is complex real ext-real Element of REAL
(Re ((R . m) - r1)) * (Re ((R . m) - r1)) is complex real ext-real set
Im ((R . m) - r1) is complex real ext-real Element of REAL
(Im ((R . m) - r1)) ^2 is complex real ext-real Element of REAL
(Im ((R . m) - r1)) * (Im ((R . m) - r1)) is complex real ext-real set
((Re ((R . m) - r1)) ^2) + ((Im ((R . m) - r1)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((R . m) - r1)) ^2) + ((Im ((R . m) - r1)) ^2)) is complex real ext-real Element of REAL
f1 is Relation-like NAT -defined NAT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]
r0 * f1 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of r0
f1 . m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
R . m is complex real ext-real Element of REAL
r0 . (f1 . m) is complex real ext-real Element of REAL
R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim R is complex real ext-real Element of REAL
r0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim r0 is complex real ext-real Element of REAL
r1 is Relation-like NAT -defined NAT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]
r0 * r1 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of r0
t is complex real ext-real set
t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
r1 . m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
R . m is complex real ext-real Element of REAL
r0 . (r1 . m) is complex real ext-real Element of REAL
(R . m) - (lim r0) is complex real ext-real Element of REAL
abs ((R . m) - (lim r0)) is complex real ext-real Element of REAL
Re ((R . m) - (lim r0)) is complex real ext-real Element of REAL
(Re ((R . m) - (lim r0))) ^2 is complex real ext-real Element of REAL
(Re ((R . m) - (lim r0))) * (Re ((R . m) - (lim r0))) is complex real ext-real set
Im ((R . m) - (lim r0)) is complex real ext-real Element of REAL
(Im ((R . m) - (lim r0))) ^2 is complex real ext-real Element of REAL
(Im ((R . m) - (lim r0))) * (Im ((R . m) - (lim r0))) is complex real ext-real set
((Re ((R . m) - (lim r0))) ^2) + ((Im ((R . m) - (lim r0))) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((R . m) - (lim r0))) ^2) + ((Im ((R . m) - (lim r0))) ^2)) is complex real ext-real Element of REAL
R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
r0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
r1 is complex real ext-real set
t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
t is complex real ext-real set
m is complex real ext-real set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
f1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
f2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
R . f2 is complex real ext-real Element of REAL
(R . f2) - r1 is complex real ext-real Element of REAL
abs ((R . f2) - r1) is complex real ext-real Element of REAL
Re ((R . f2) - r1) is complex real ext-real Element of REAL
(Re ((R . f2) - r1)) ^2 is complex real ext-real Element of REAL
(Re ((R . f2) - r1)) * (Re ((R . f2) - r1)) is complex real ext-real set
Im ((R . f2) - r1) is complex real ext-real Element of REAL
(Im ((R . f2) - r1)) ^2 is complex real ext-real Element of REAL
(Im ((R . f2) - r1)) * (Im ((R . f2) - r1)) is complex real ext-real set
((Re ((R . f2) - r1)) ^2) + ((Im ((R . f2) - r1)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((R . f2) - r1)) ^2) + ((Im ((R . f2) - r1)) ^2)) is complex real ext-real Element of REAL
r0 . f2 is complex real ext-real Element of REAL
(r0 . f2) - t is complex real ext-real Element of REAL
abs ((r0 . f2) - t) is complex real ext-real Element of REAL
Re ((r0 . f2) - t) is complex real ext-real Element of REAL
(Re ((r0 . f2) - t)) ^2 is complex real ext-real Element of REAL
(Re ((r0 . f2) - t)) * (Re ((r0 . f2) - t)) is complex real ext-real set
Im ((r0 . f2) - t) is complex real ext-real Element of REAL
(Im ((r0 . f2) - t)) ^2 is complex real ext-real Element of REAL
(Im ((r0 . f2) - t)) * (Im ((r0 . f2) - t)) is complex real ext-real set
((Re ((r0 . f2) - t)) ^2) + ((Im ((r0 . f2) - t)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((r0 . f2) - t)) ^2) + ((Im ((r0 . f2) - t)) ^2)) is complex real ext-real Element of REAL
f1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
f2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
r0 . f2 is complex real ext-real Element of REAL
R . f2 is complex real ext-real Element of REAL
(r0 . f2) - t is complex real ext-real Element of REAL
abs ((r0 . f2) - t) is complex real ext-real Element of REAL
Re ((r0 . f2) - t) is complex real ext-real Element of REAL
(Re ((r0 . f2) - t)) ^2 is complex real ext-real Element of REAL
(Re ((r0 . f2) - t)) * (Re ((r0 . f2) - t)) is complex real ext-real set
Im ((r0 . f2) - t) is complex real ext-real Element of REAL
(Im ((r0 . f2) - t)) ^2 is complex real ext-real Element of REAL
(Im ((r0 . f2) - t)) * (Im ((r0 . f2) - t)) is complex real ext-real set
((Re ((r0 . f2) - t)) ^2) + ((Im ((r0 . f2) - t)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((r0 . f2) - t)) ^2) + ((Im ((r0 . f2) - t)) ^2)) is complex real ext-real Element of REAL
f1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
f2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim R is complex real ext-real Element of REAL
r0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim r0 is complex real ext-real Element of REAL
r1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
r1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
t is complex real ext-real set
t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
R . m is complex real ext-real Element of REAL
(R . m) - (lim R) is complex real ext-real Element of REAL
abs ((R . m) - (lim R)) is complex real ext-real Element of REAL
Re ((R . m) - (lim R)) is complex real ext-real Element of REAL
(Re ((R . m) - (lim R))) ^2 is complex real ext-real Element of REAL
(Re ((R . m) - (lim R))) * (Re ((R . m) - (lim R))) is complex real ext-real set
Im ((R . m) - (lim R)) is complex real ext-real Element of REAL
(Im ((R . m) - (lim R))) ^2 is complex real ext-real Element of REAL
(Im ((R . m) - (lim R))) * (Im ((R . m) - (lim R))) is complex real ext-real set
((Re ((R . m) - (lim R))) ^2) + ((Im ((R . m) - (lim R))) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((R . m) - (lim R))) ^2) + ((Im ((R . m) - (lim R))) ^2)) is complex real ext-real Element of REAL
r0 . m is complex real ext-real Element of REAL
(r0 . m) - (lim R) is complex real ext-real Element of REAL
abs ((r0 . m) - (lim R)) is complex real ext-real Element of REAL
Re ((r0 . m) - (lim R)) is complex real ext-real Element of REAL
(Re ((r0 . m) - (lim R))) ^2 is complex real ext-real Element of REAL
(Re ((r0 . m) - (lim R))) * (Re ((r0 . m) - (lim R))) is complex real ext-real set
Im ((r0 . m) - (lim R)) is complex real ext-real Element of REAL
(Im ((r0 . m) - (lim R))) ^2 is complex real ext-real Element of REAL
(Im ((r0 . m) - (lim R))) * (Im ((r0 . m) - (lim R))) is complex real ext-real set
((Re ((r0 . m) - (lim R))) ^2) + ((Im ((r0 . m) - (lim R))) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((r0 . m) - (lim R))) ^2) + ((Im ((r0 . m) - (lim R))) ^2)) is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
r0 . m is complex real ext-real Element of REAL
R . m is complex real ext-real Element of REAL
(r0 . m) - (lim R) is complex real ext-real Element of REAL
abs ((r0 . m) - (lim R)) is complex real ext-real Element of REAL
Re ((r0 . m) - (lim R)) is complex real ext-real Element of REAL
(Re ((r0 . m) - (lim R))) ^2 is complex real ext-real Element of REAL
(Re ((r0 . m) - (lim R))) * (Re ((r0 . m) - (lim R))) is complex real ext-real set
Im ((r0 . m) - (lim R)) is complex real ext-real Element of REAL
(Im ((r0 . m) - (lim R))) ^2 is complex real ext-real Element of REAL
(Im ((r0 . m) - (lim R))) * (Im ((r0 . m) - (lim R))) is complex real ext-real set
((Re ((r0 . m) - (lim R))) ^2) + ((Im ((r0 . m) - (lim R))) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((r0 . m) - (lim R))) ^2) + ((Im ((r0 . m) - (lim R))) ^2)) is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
the Relation-like NAT -defined REAL -valued Function-like constant non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued non-decreasing non-increasing bounded_above bounded_below bounded convergent Element of bool [:NAT,REAL:] is Relation-like NAT -defined REAL -valued Function-like constant non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued non-decreasing non-increasing bounded_above bounded_below bounded convergent Element of bool [:NAT,REAL:]
R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued bounded_above bounded_below bounded convergent Element of bool [:NAT,REAL:]
r0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
R ^\ r0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of R
r1 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
r0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
r0 ^\ R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of r0
lim (r0 ^\ R) is complex real ext-real Element of REAL
lim r0 is complex real ext-real Element of REAL
R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
r0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
r0 ^\ R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of r0
r1 is complex real ext-real set
t is complex real ext-real set
t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
t + R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
r0 . m is complex real ext-real Element of REAL
(r0 . m) - r1 is complex real ext-real Element of REAL
abs ((r0 . m) - r1) is complex real ext-real Element of REAL
Re ((r0 . m) - r1) is complex real ext-real Element of REAL
(Re ((r0 . m) - r1)) ^2 is complex real ext-real Element of REAL
(Re ((r0 . m) - r1)) * (Re ((r0 . m) - r1)) is complex real ext-real set
Im ((r0 . m) - r1) is complex real ext-real Element of REAL
(Im ((r0 . m) - r1)) ^2 is complex real ext-real Element of REAL
(Im ((r0 . m) - r1)) * (Im ((r0 . m) - r1)) is complex real ext-real set
((Re ((r0 . m) - r1)) ^2) + ((Im ((r0 . m) - r1)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((r0 . m) - r1)) ^2) + ((Im ((r0 . m) - r1)) ^2)) is complex real ext-real Element of REAL
f1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative finite cardinal set
(t + R) + f1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
m - R is complex real ext-real V48() V49() Element of INT
f2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
t + f2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
(t + f2) + R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
- R is complex real ext-real non positive V48() V49() Element of INT
((t + f2) + R) + (- R) is complex real ext-real V48() V49() Element of INT
f1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
f1 + R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT
(r0 ^\ R) . f1 is complex real ext-real Element of REAL
((r0