REAL is V11() V45() V46() V47() V51() V52() set
NAT is V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() Element of K19(REAL)
K19(REAL) is set
COMPLEX is V11() V45() V51() V52() set
RAT is V11() V45() V46() V47() V48() V51() V52() set
INT is V11() V45() V46() V47() V48() V49() V51() V52() set
omega is V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() set
K19(omega) is set
K19(NAT) is set
K20(NAT,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
K20(NAT,COMPLEX) is complex-valued set
K19(K20(NAT,COMPLEX)) is set
1 is V11() epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
0 is set
the Function-like functional V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() set is Function-like functional V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() set
0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
|.0.| is V22() real ext-real V44() Element of REAL
Re 0 is V22() real ext-real Element of REAL
K266((Re 0)) is V22() real ext-real Element of REAL
Im 0 is V22() real ext-real Element of REAL
K266((Im 0)) is V22() real ext-real Element of REAL
K266((Re 0)) + K266((Im 0)) is V22() real ext-real Element of REAL
K268((K266((Re 0)) + K266((Im 0)))) is V22() real ext-real Element of REAL
0c is V22() Element of COMPLEX
K20(COMPLEX,COMPLEX) is complex-valued set
K19(K20(COMPLEX,COMPLEX)) is set
0 " is V22() real ext-real non negative set
2 is V11() epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
K19(COMPLEX) is set
K20(NAT,NAT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
K19(K20(NAT,NAT)) is set
cs is V1() V4( NAT ) V5( REAL ) Function-like V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
cf is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
cs is V22() real ext-real set
cf is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
cf is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
x0 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
cf . f is V22() set
x0 . f is V22() set
cf . f is V22() Element of COMPLEX
f + cs is V22() real ext-real Element of REAL
1 / (f + cs) is V22() real ext-real Element of REAL
(f + cs) " is V22() real ext-real set
1 * ((f + cs) ") is V22() real ext-real set
x0 . f is V22() Element of COMPLEX
cs is V22() real ext-real set
(cs) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
x0 is V22() Element of COMPLEX
f is V22() real ext-real Element of REAL
f " is V22() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
L is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
R is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(cs) . R is V22() set
((cs) . R) - x0 is V22() set
- x0 is V22() set
((cs) . R) + (- x0) is V22() set
|.(((cs) . R) - x0).| is V22() real ext-real Element of REAL
Re (((cs) . R) - x0) is V22() real ext-real Element of REAL
K266((Re (((cs) . R) - x0))) is V22() real ext-real Element of REAL
Im (((cs) . R) - x0) is V22() real ext-real Element of REAL
K266((Im (((cs) . R) - x0))) is V22() real ext-real Element of REAL
K266((Re (((cs) . R) - x0))) + K266((Im (((cs) . R) - x0))) is V22() real ext-real Element of REAL
K268((K266((Re (((cs) . R) - x0))) + K266((Im (((cs) . R) - x0))))) is V22() real ext-real Element of REAL
L + cs is V22() real ext-real Element of REAL
R + cs is V22() real ext-real Element of REAL
1 / (R + cs) is V22() real ext-real Element of REAL
(R + cs) " is V22() real ext-real set
1 * ((R + cs) ") is V22() real ext-real set
1 / (L + cs) is V22() real ext-real Element of REAL
(L + cs) " is V22() real ext-real set
1 * ((L + cs) ") is V22() real ext-real set
(cs) . R is V22() Element of COMPLEX
N + cs is V22() real ext-real Element of REAL
(f ") + 0 is V22() real ext-real Element of REAL
1 / (f ") is V22() real ext-real Element of REAL
(f ") " is V22() real ext-real set
1 * ((f ") ") is V22() real ext-real set
1 / (N + cs) is V22() real ext-real Element of REAL
(N + cs) " is V22() real ext-real set
1 * ((N + cs) ") is V22() real ext-real set
((cs) . R) - x0 is V22() Element of COMPLEX
((cs) . R) + (- x0) is V22() set
abs (((cs) . R) - x0) is V22() real ext-real Element of REAL
Re (((cs) . R) - x0) is V22() real ext-real Element of REAL
K266((Re (((cs) . R) - x0))) is V22() real ext-real Element of REAL
Im (((cs) . R) - x0) is V22() real ext-real Element of REAL
K266((Im (((cs) . R) - x0))) is V22() real ext-real Element of REAL
K266((Re (((cs) . R) - x0))) + K266((Im (((cs) . R) - x0))) is V22() real ext-real Element of REAL
K268((K266((Re (((cs) . R) - x0))) + K266((Im (((cs) . R) - x0))))) is V22() real ext-real Element of REAL
cs is V11() V22() real ext-real positive non negative set
(cs) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
cs is V22() real ext-real set
(cs) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim (cs) is V22() Element of COMPLEX
x0 is V22() real ext-real Element of REAL
x0 " is V22() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
L is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
N + cs is V22() real ext-real Element of REAL
L + cs is V22() real ext-real Element of REAL
1 / (L + cs) is V22() real ext-real Element of REAL
(L + cs) " is V22() real ext-real set
1 * ((L + cs) ") is V22() real ext-real set
1 / (N + cs) is V22() real ext-real Element of REAL
(N + cs) " is V22() real ext-real set
1 * ((N + cs) ") is V22() real ext-real set
(cs) . L is V22() Element of COMPLEX
f + cs is V22() real ext-real Element of REAL
(x0 ") + 0 is V22() real ext-real Element of REAL
1 / (x0 ") is V22() real ext-real Element of REAL
(x0 ") " is V22() real ext-real set
1 * ((x0 ") ") is V22() real ext-real set
1 / (f + cs) is V22() real ext-real Element of REAL
(f + cs) " is V22() real ext-real set
1 * ((f + cs) ") is V22() real ext-real set
((cs) . L) - 0c is V22() Element of COMPLEX
- 0c is V22() set
((cs) . L) + (- 0c) is V22() set
abs (((cs) . L) - 0c) is V22() real ext-real Element of REAL
Re (((cs) . L) - 0c) is V22() real ext-real Element of REAL
K266((Re (((cs) . L) - 0c))) is V22() real ext-real Element of REAL
Im (((cs) . L) - 0c) is V22() real ext-real Element of REAL
K266((Im (((cs) . L) - 0c))) is V22() real ext-real Element of REAL
K266((Re (((cs) . L) - 0c))) + K266((Im (((cs) . L) - 0c))) is V22() real ext-real Element of REAL
K268((K266((Re (((cs) . L) - 0c))) + K266((Im (((cs) . L) - 0c))))) is V22() real ext-real Element of REAL
cs is V11() V22() real ext-real positive non negative set
(cs) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent Element of K19(K20(NAT,COMPLEX))
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
x0 + cs is V11() V22() real ext-real positive non negative Element of REAL
1 / (x0 + cs) is V11() V22() real ext-real positive non negative Element of REAL
(x0 + cs) " is V11() V22() real ext-real positive non negative set
1 * ((x0 + cs) ") is V11() V22() real ext-real positive non negative set
(cs) . x0 is V22() Element of COMPLEX
lim (cs) is V22() Element of COMPLEX
(1) is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
cs is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
NAT --> 0c is V1() V4( NAT ) V5( COMPLEX ) Function-like constant V11() total T-Sequence-like quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
cs is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
cf is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
cf . x0 is V22() Element of COMPLEX
f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
cf . f is V22() Element of COMPLEX
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
cf . x0 is V22() Element of COMPLEX
f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
cf . f is V22() Element of COMPLEX
cf is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
x0 is V1() V4( NAT ) V5( NAT ) Function-like V11() total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
cf * x0 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(cf * x0) . f is V22() Element of COMPLEX
x0 . f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative Element of REAL
cf . (x0 . f) is V22() Element of COMPLEX
dom (cf * x0) is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
COMPLEX --> 0c is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like constant V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
cf is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
f " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
x0 /* f is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f ") (#) (x0 /* f) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((f ") (#) (x0 /* f)) is V22() Element of COMPLEX
dom x0 is V45() Element of K19(COMPLEX)
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
rng f is V45() Element of K19(COMPLEX)
((f ") (#) (x0 /* f)) . N is V22() Element of COMPLEX
(f ") . N is V22() Element of COMPLEX
(x0 /* f) . N is V22() Element of COMPLEX
((f ") . N) * ((x0 /* f) . N) is V22() Element of COMPLEX
f . N is V22() Element of COMPLEX
x0 /. (f . N) is V22() Element of COMPLEX
x0 . (f . N) is V22() Element of COMPLEX
((f ") . N) * (x0 /. (f . N)) is V22() Element of COMPLEX
((f ") . N) * 0c is V22() Element of COMPLEX
((f ") (#) (x0 /* f)) . 0 is V22() Element of COMPLEX
1r is V22() Element of COMPLEX
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom x0 is V45() Element of K19(COMPLEX)
f is set
f is V22() Element of COMPLEX
x0 /. f is V22() Element of COMPLEX
1r * f is V22() Element of COMPLEX
x0 . f is V22() set
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
x0 + f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
N is V22() Element of COMPLEX
L is V22() Element of COMPLEX
R is V22() Element of COMPLEX
(x0 + f) /. R is V22() Element of COMPLEX
(x0 + f) . R is V22() Element of COMPLEX
x0 /. R is V22() Element of COMPLEX
x0 . R is V22() Element of COMPLEX
f /. R is V22() Element of COMPLEX
f . R is V22() Element of COMPLEX
(x0 /. R) + (f /. R) is V22() Element of COMPLEX
L * R is V22() Element of COMPLEX
(L * R) + (f /. R) is V22() Element of COMPLEX
N * R is V22() Element of COMPLEX
(L * R) + (N * R) is V22() Element of COMPLEX
L + N is V22() Element of COMPLEX
(L + N) * R is V22() Element of COMPLEX
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
x0 - f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
- f is V1() V4( COMPLEX ) Function-like total complex-valued set
- 1 is V11() V22() real ext-real non positive negative set
(- 1) (#) f is V1() V4( COMPLEX ) Function-like total complex-valued set
x0 + (- f) is V1() V4( COMPLEX ) Function-like total complex-valued set
N is V22() Element of COMPLEX
L is V22() Element of COMPLEX
R is V22() Element of COMPLEX
(x0 - f) /. R is V22() Element of COMPLEX
(x0 - f) . R is V22() Element of COMPLEX
x0 /. R is V22() Element of COMPLEX
x0 . R is V22() Element of COMPLEX
f /. R is V22() Element of COMPLEX
f . R is V22() Element of COMPLEX
(x0 /. R) - (f /. R) is V22() Element of COMPLEX
- (f /. R) is V22() set
(x0 /. R) + (- (f /. R)) is V22() set
L * R is V22() Element of COMPLEX
(L * R) - (f /. R) is V22() Element of COMPLEX
(L * R) + (- (f /. R)) is V22() set
N * R is V22() Element of COMPLEX
(L * R) - (N * R) is V22() Element of COMPLEX
- (N * R) is V22() set
(L * R) + (- (N * R)) is V22() set
L - N is V22() Element of COMPLEX
- N is V22() set
L + (- N) is V22() set
(L - N) * R is V22() Element of COMPLEX
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
x0 is V22() Element of COMPLEX
x0 (#) f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
N is V22() Element of COMPLEX
L is V22() Element of COMPLEX
(x0 (#) f) /. L is V22() Element of COMPLEX
(x0 (#) f) . L is V22() Element of COMPLEX
f /. L is V22() Element of COMPLEX
f . L is V22() Element of COMPLEX
x0 * (f /. L) is V22() Element of COMPLEX
N * L is V22() Element of COMPLEX
x0 * (N * L) is V22() Element of COMPLEX
x0 * N is V22() Element of COMPLEX
(x0 * N) * L is V22() Element of COMPLEX
L is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
x0 + f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
N is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
N " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(x0 + f) /* N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(N ") (#) ((x0 + f) /* N) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
x0 /* N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f /* N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(x0 /* N) + (f /* N) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(N ") (#) ((x0 /* N) + (f /* N)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(N ") (#) (x0 /* N) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(N ") (#) (f /* N) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((N ") (#) (x0 /* N)) + ((N ") (#) (f /* N)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((N ") (#) (x0 /* N)) is V22() Element of COMPLEX
lim ((N ") (#) ((x0 + f) /* N)) is V22() Element of COMPLEX
lim ((N ") (#) (f /* N)) is V22() Element of COMPLEX
(lim ((N ") (#) (x0 /* N))) + (lim ((N ") (#) (f /* N))) is V22() Element of COMPLEX
N is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
x0 - f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
- f is V1() V4( COMPLEX ) Function-like total complex-valued set
(- 1) (#) f is V1() V4( COMPLEX ) Function-like total complex-valued set
x0 + (- f) is V1() V4( COMPLEX ) Function-like total complex-valued set
N is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
N " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(x0 - f) /* N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(N ") (#) ((x0 - f) /* N) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
x0 /* N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f /* N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(x0 /* N) - (f /* N) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- (f /* N) is V1() V4( NAT ) Function-like total complex-valued set
(- 1) (#) (f /* N) is V1() V4( NAT ) Function-like total complex-valued set
(x0 /* N) + (- (f /* N)) is V1() V4( NAT ) Function-like total complex-valued set
(N ") (#) ((x0 /* N) - (f /* N)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(N ") (#) (x0 /* N) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(N ") (#) (f /* N) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((N ") (#) (x0 /* N)) - ((N ") (#) (f /* N)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- ((N ") (#) (f /* N)) is V1() V4( NAT ) Function-like total complex-valued set
(- 1) (#) ((N ") (#) (f /* N)) is V1() V4( NAT ) Function-like total complex-valued set
((N ") (#) (x0 /* N)) + (- ((N ") (#) (f /* N))) is V1() V4( NAT ) Function-like total complex-valued set
lim ((N ") (#) (x0 /* N)) is V22() Element of COMPLEX
lim ((N ") (#) (f /* N)) is V22() Element of COMPLEX
lim ((N ") (#) ((x0 - f) /* N)) is V22() Element of COMPLEX
0c - 0c is V22() Element of COMPLEX
- 0c is V22() set
0c + (- 0c) is V22() set
N is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
x0 (#) f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
L is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
L " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
R is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(L ") . R is V22() Element of COMPLEX
L . R is V22() Element of COMPLEX
(L . R) " is V22() Element of COMPLEX
Re (L . R) is V22() real ext-real Element of REAL
K266((Re (L . R))) is V22() real ext-real Element of REAL
Im (L . R) is V22() real ext-real Element of REAL
K266((Im (L . R))) is V22() real ext-real Element of REAL
K266((Re (L . R))) + K266((Im (L . R))) is V22() real ext-real Element of REAL
(Re (L . R)) / (K266((Re (L . R))) + K266((Im (L . R)))) is V22() real ext-real Element of REAL
(K266((Re (L . R))) + K266((Im (L . R)))) " is V22() real ext-real set
(Re (L . R)) * ((K266((Re (L . R))) + K266((Im (L . R)))) ") is V22() real ext-real set
- (Im (L . R)) is V22() real ext-real Element of REAL
(- (Im (L . R))) / (K266((Re (L . R))) + K266((Im (L . R)))) is V22() real ext-real Element of REAL
(- (Im (L . R))) * ((K266((Re (L . R))) + K266((Im (L . R)))) ") is V22() real ext-real set
K278() is V22() Element of COMPLEX
((- (Im (L . R))) / (K266((Re (L . R))) + K266((Im (L . R))))) * K278() is V22() set
((Re (L . R)) / (K266((Re (L . R))) + K266((Im (L . R))))) + (((- (Im (L . R))) / (K266((Re (L . R))) + K266((Im (L . R))))) * K278()) is V22() set
N is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
N " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(x0 (#) f) /* N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(N ") (#) ((x0 (#) f) /* N) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
x0 /* N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f /* N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(x0 /* N) (#) (f /* N) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((x0 /* N) (#) (f /* N)) /" N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
N " is V1() V4( NAT ) Function-like total complex-valued set
((x0 /* N) (#) (f /* N)) (#) (N ") is V1() V4( NAT ) Function-like total complex-valued set
((x0 /* N) (#) (f /* N)) (#) (N ") is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
N (#) (N ") is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(((x0 /* N) (#) (f /* N)) (#) (N ")) /" (N (#) (N ")) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(N (#) (N ")) " is V1() V4( NAT ) Function-like total complex-valued set
(((x0 /* N) (#) (f /* N)) (#) (N ")) (#) ((N (#) (N ")) ") is V1() V4( NAT ) Function-like total complex-valued set
(N ") " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((N ") ") (#) (N ") is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(((x0 /* N) (#) (f /* N)) (#) (N ")) (#) (((N ") ") (#) (N ")) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(N ") (#) (f /* N) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(x0 /* N) (#) ((N ") (#) (f /* N)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(N (#) (N ")) (#) ((x0 /* N) (#) ((N ") (#) (f /* N))) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(N (#) (N ")) (#) (x0 /* N) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((N (#) (N ")) (#) (x0 /* N)) (#) ((N ") (#) (f /* N)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(N ") (#) (x0 /* N) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
N (#) ((N ") (#) (x0 /* N)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(N (#) ((N ") (#) (x0 /* N))) (#) ((N ") (#) (f /* N)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((N ") (#) (x0 /* N)) is V22() Element of COMPLEX
lim N is V22() Element of COMPLEX
lim (N (#) ((N ") (#) (x0 /* N))) is V22() Element of COMPLEX
0 * 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
lim ((N ") (#) (f /* N)) is V22() Element of COMPLEX
lim ((N ") (#) ((x0 (#) f) /* N)) is V22() Element of COMPLEX
0c * 0c is V22() Element of COMPLEX
N is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
x0 is V22() Element of COMPLEX
x0 (#) f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
N is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
N " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(x0 (#) f) /* N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(N ") (#) ((x0 (#) f) /* N) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f /* N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
x0 (#) (f /* N) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(N ") (#) (x0 (#) (f /* N)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(N ") (#) (f /* N) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
x0 (#) ((N ") (#) (f /* N)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((N ") (#) (f /* N)) is V22() Element of COMPLEX
lim ((N ") (#) ((x0 (#) f) /* N)) is V22() Element of COMPLEX
x0 * 0c is V22() Element of COMPLEX
N is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
x0 (#) f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
N is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
L is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
L " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
N /* L is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(L ") (#) (N /* L) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((L ") (#) (N /* L)) is V22() Element of COMPLEX
R is V22() Element of COMPLEX
a is V22() Element of COMPLEX
s1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
L . s1 is V22() Element of COMPLEX
(x0 (#) f) /* L is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(L ") (#) ((x0 (#) f) /* L) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((L ") (#) ((x0 (#) f) /* L)) . s1 is V22() Element of COMPLEX
(L ") . s1 is V22() Element of COMPLEX
((x0 (#) f) /* L) . s1 is V22() Element of COMPLEX
((L ") . s1) * (((x0 (#) f) /* L) . s1) is V22() Element of COMPLEX
(x0 (#) f) /. (L . s1) is V22() Element of COMPLEX
(x0 (#) f) . (L . s1) is V22() Element of COMPLEX
((L ") . s1) * ((x0 (#) f) /. (L . s1)) is V22() Element of COMPLEX
x0 /. (L . s1) is V22() Element of COMPLEX
x0 . (L . s1) is V22() Element of COMPLEX
f /. (L . s1) is V22() Element of COMPLEX
f . (L . s1) is V22() Element of COMPLEX
(x0 /. (L . s1)) * (f /. (L . s1)) is V22() Element of COMPLEX
((L ") . s1) * ((x0 /. (L . s1)) * (f /. (L . s1))) is V22() Element of COMPLEX
((L ") . s1) * (x0 /. (L . s1)) is V22() Element of COMPLEX
(((L ") . s1) * (x0 /. (L . s1))) * (f /. (L . s1)) is V22() Element of COMPLEX
(L . s1) " is V22() Element of COMPLEX
Re (L . s1) is V22() real ext-real Element of REAL
K266((Re (L . s1))) is V22() real ext-real Element of REAL
Im (L . s1) is V22() real ext-real Element of REAL
K266((Im (L . s1))) is V22() real ext-real Element of REAL
K266((Re (L . s1))) + K266((Im (L . s1))) is V22() real ext-real Element of REAL
(Re (L . s1)) / (K266((Re (L . s1))) + K266((Im (L . s1)))) is V22() real ext-real Element of REAL
(K266((Re (L . s1))) + K266((Im (L . s1)))) " is V22() real ext-real set
(Re (L . s1)) * ((K266((Re (L . s1))) + K266((Im (L . s1)))) ") is V22() real ext-real set
- (Im (L . s1)) is V22() real ext-real Element of REAL
(- (Im (L . s1))) / (K266((Re (L . s1))) + K266((Im (L . s1)))) is V22() real ext-real Element of REAL
(- (Im (L . s1))) * ((K266((Re (L . s1))) + K266((Im (L . s1)))) ") is V22() real ext-real set
K278() is V22() Element of COMPLEX
((- (Im (L . s1))) / (K266((Re (L . s1))) + K266((Im (L . s1))))) * K278() is V22() set
((Re (L . s1)) / (K266((Re (L . s1))) + K266((Im (L . s1))))) + (((- (Im (L . s1))) / (K266((Re (L . s1))) + K266((Im (L . s1))))) * K278()) is V22() set
((L . s1) ") * (x0 /. (L . s1)) is V22() Element of COMPLEX
(((L . s1) ") * (x0 /. (L . s1))) * (f /. (L . s1)) is V22() Element of COMPLEX
(L . s1) * R is V22() Element of COMPLEX
((L . s1) ") * ((L . s1) * R) is V22() Element of COMPLEX
(((L . s1) ") * ((L . s1) * R)) * (f /. (L . s1)) is V22() Element of COMPLEX
((L . s1) ") * (L . s1) is V22() Element of COMPLEX
(((L . s1) ") * (L . s1)) * R is V22() Element of COMPLEX
((((L . s1) ") * (L . s1)) * R) * (f /. (L . s1)) is V22() Element of COMPLEX
1r is V22() Element of COMPLEX
1r * R is V22() Element of COMPLEX
(1r * R) * (f /. (L . s1)) is V22() Element of COMPLEX
a * (L . s1) is V22() Element of COMPLEX
R * (a * (L . s1)) is V22() Element of COMPLEX
R * a is V22() Element of COMPLEX
(R * a) * (L . s1) is V22() Element of COMPLEX
(R * a) (#) L is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent Element of K19(K20(NAT,COMPLEX))
((R * a) (#) L) . s1 is V22() Element of COMPLEX
lim L is V22() Element of COMPLEX
(R * a) * 0c is V22() Element of COMPLEX
L is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
x0 (#) f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
N is V22() Element of COMPLEX
L is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
L " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(x0 (#) f) /* L is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(L ") (#) ((x0 (#) f) /* L) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
x0 /* L is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f /* L is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(x0 /* L) (#) (f /* L) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(L ") (#) ((x0 /* L) (#) (f /* L)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(L ") (#) (x0 /* L) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((L ") (#) (x0 /* L)) (#) (f /* L) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
R is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(f /* L) . R is V22() Element of COMPLEX
L . R is V22() Element of COMPLEX
f /. (L . R) is V22() Element of COMPLEX
f . (L . R) is V22() Element of COMPLEX
N * (L . R) is V22() Element of COMPLEX
N (#) L is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent Element of K19(K20(NAT,COMPLEX))
(N (#) L) . R is V22() Element of COMPLEX
lim L is V22() Element of COMPLEX
lim (f /* L) is V22() Element of COMPLEX
N * 0c is V22() Element of COMPLEX
lim ((L ") (#) (x0 /* L)) is V22() Element of COMPLEX
lim ((L ") (#) ((x0 (#) f) /* L)) is V22() Element of COMPLEX
0c * 0c is V22() Element of COMPLEX
L is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f (#) x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
N is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
x0 is V22() set
{ b1 where b1 is V22() set : not 1 <= |.(b1 - x0).| } is set
N is set
L is V22() set
L - x0 is V22() set
- x0 is V22() set
L + (- x0) is V22() set
|.(L - x0).| is V22() real ext-real Element of REAL
Re (L - x0) is V22() real ext-real Element of REAL
K266((Re (L - x0))) is V22() real ext-real Element of REAL
Im (L - x0) is V22() real ext-real Element of REAL
K266((Im (L - x0))) is V22() real ext-real Element of REAL
K266((Re (L - x0))) + K266((Im (L - x0))) is V22() real ext-real Element of REAL
K268((K266((Re (L - x0))) + K266((Im (L - x0))))) is V22() real ext-real Element of REAL
x0 is V22() Element of COMPLEX
f is V22() real ext-real set
{ b1 where b1 is V22() set : not f <= |.(b1 - x0).| } is set
L is set
R is V22() set
R - x0 is V22() set
- x0 is V22() set
R + (- x0) is V22() set
|.(R - x0).| is V22() real ext-real Element of REAL
Re (R - x0) is V22() real ext-real Element of REAL
K266((Re (R - x0))) is V22() real ext-real Element of REAL
Im (R - x0) is V22() real ext-real Element of REAL
K266((Im (R - x0))) is V22() real ext-real Element of REAL
K266((Re (R - x0))) + K266((Im (R - x0))) is V22() real ext-real Element of REAL
K268((K266((Re (R - x0))) + K266((Im (R - x0))))) is V22() real ext-real Element of REAL
x0 is V22() Element of COMPLEX
f is V45() (x0)
N is V22() real ext-real Element of REAL
{ b1 where b1 is V22() set : not N <= |.(b1 - x0).| } is set
x0 - x0 is V22() Element of COMPLEX
- x0 is V22() set
x0 + (- x0) is V22() set
|.(x0 - x0).| is V22() real ext-real Element of REAL
Re (x0 - x0) is V22() real ext-real Element of REAL
K266((Re (x0 - x0))) is V22() real ext-real Element of REAL
Im (x0 - x0) is V22() real ext-real Element of REAL
K266((Im (x0 - x0))) is V22() real ext-real Element of REAL
K266((Re (x0 - x0))) + K266((Im (x0 - x0))) is V22() real ext-real Element of REAL
K268((K266((Re (x0 - x0))) + K266((Im (x0 - x0))))) is V22() real ext-real Element of REAL
x0 is V22() set
f is V45() (x0)
N is V45() (x0)
L is V22() real ext-real Element of REAL
{ b1 where b1 is V22() set : not L <= |.(b1 - x0).| } is set
R is V22() real ext-real Element of REAL
{ b1 where b1 is V22() set : not R <= |.(b1 - x0).| } is set
min (L,R) is V22() real ext-real set
{ b1 where b1 is V22() set : not min (L,R) <= |.(b1 - x0).| } is set
s1 is set
M is V22() set
M - x0 is V22() set
- x0 is V22() set
M + (- x0) is V22() set
|.(M - x0).| is V22() real ext-real Element of REAL
Re (M - x0) is V22() real ext-real Element of REAL
K266((Re (M - x0))) is V22() real ext-real Element of REAL
Im (M - x0) is V22() real ext-real Element of REAL
K266((Im (M - x0))) is V22() real ext-real Element of REAL
K266((Re (M - x0))) + K266((Im (M - x0))) is V22() real ext-real Element of REAL
K268((K266((Re (M - x0))) + K266((Im (M - x0))))) is V22() real ext-real Element of REAL
s1 is set
M is V22() set
M - x0 is V22() set
- x0 is V22() set
M + (- x0) is V22() set
|.(M - x0).| is V22() real ext-real Element of REAL
Re (M - x0) is V22() real ext-real Element of REAL
K266((Re (M - x0))) is V22() real ext-real Element of REAL
Im (M - x0) is V22() real ext-real Element of REAL
K266((Im (M - x0))) is V22() real ext-real Element of REAL
K266((Re (M - x0))) + K266((Im (M - x0))) is V22() real ext-real Element of REAL
K268((K266((Re (M - x0))) + K266((Im (M - x0))))) is V22() real ext-real Element of REAL
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f is V22() set
dom x0 is V45() Element of K19(COMPLEX)
1r is V22() Element of COMPLEX
x0 /. f is V22() Element of COMPLEX
N is V45() (f)
L is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
L is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
a is V22() Element of COMPLEX
L /. 1r is V22() Element of COMPLEX
L . 1r is V22() Element of COMPLEX
a * 1r is V22() Element of COMPLEX
(2) is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
L is V22() Element of COMPLEX
R is V22() Element of COMPLEX
a is V45() (f)
s1 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
s1 /. 1r is V22() Element of COMPLEX
s1 . 1r is V22() Element of COMPLEX
M is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
a is V45() (f)
s1 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
s1 /. 1r is V22() Element of COMPLEX
s1 . 1r is V22() Element of COMPLEX
M is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
s1 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
s1 /. 1r is V22() Element of COMPLEX
s1 . 1r is V22() Element of COMPLEX
M is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
p is V22() Element of COMPLEX
m is V45() (f)
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m /. 1r is V22() Element of COMPLEX
m . 1r is V22() Element of COMPLEX
n is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m is V45() (f)
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m /. 1r is V22() Element of COMPLEX
m . 1r is V22() Element of COMPLEX
n is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m /. 1r is V22() Element of COMPLEX
m . 1r is V22() Element of COMPLEX
n is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
y1 is V22() Element of COMPLEX
R17 is V45() (f)
R16 is V22() real ext-real Element of REAL
{ b1 where b1 is V22() set : not R16 <= |.(b1 - f).| } is set
R18 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
R16 (#) R18 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
R13 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(R16 (#) R18) . R13 is V22() Element of COMPLEX
R18 . R13 is V22() Element of COMPLEX
R16 * (R18 . R13) is V22() set
R13 + 2 is V11() epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
1 / (R13 + 2) is V11() V22() real ext-real positive non negative Element of REAL
(R13 + 2) " is V11() V22() real ext-real positive non negative set
1 * ((R13 + 2) ") is V11() V22() real ext-real positive non negative set
R16 * (1 / (R13 + 2)) is V22() real ext-real Element of REAL
R16 / (R13 + 2) is V22() real ext-real Element of REAL
R16 * ((R13 + 2) ") is V22() real ext-real set
R13 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(R16 (#) R18) . R13 is V22() Element of COMPLEX
R13 + 2 is V11() epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
R16 / (R13 + 2) is V22() real ext-real Element of REAL
(R13 + 2) " is V11() V22() real ext-real positive non negative set
R16 * ((R13 + 2) ") is V22() real ext-real set
lim R18 is V22() Element of COMPLEX
lim (R16 (#) R18) is V22() Element of COMPLEX
R16 * 0 is V22() real ext-real Element of REAL
R13 is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
L is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
R13 . L is V22() Element of COMPLEX
L + 2 is V11() epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
R16 / (L + 2) is V22() real ext-real Element of REAL
(L + 2) " is V11() V22() real ext-real positive non negative set
R16 * ((L + 2) ") is V22() real ext-real set
R15 is V22() set
f + R15 is V22() set
R19 is V22() set
R19 - f is V22() set
- f is V22() set
R19 + (- f) is V22() set
L + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(L + 1) + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
0 + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
R16 / 1 is V22() real ext-real Element of REAL
1 " is V11() V22() real ext-real positive non negative set
R16 * (1 ") is V22() real ext-real set
(f + R15) - f is V22() set
(f + R15) + (- f) is V22() set
|.((f + R15) - f).| is V22() real ext-real Element of REAL
Re ((f + R15) - f) is V22() real ext-real Element of REAL
K266((Re ((f + R15) - f))) is V22() real ext-real Element of REAL
Im ((f + R15) - f) is V22() real ext-real Element of REAL
K266((Im ((f + R15) - f))) is V22() real ext-real Element of REAL
K266((Re ((f + R15) - f))) + K266((Im ((f + R15) - f))) is V22() real ext-real Element of REAL
K268((K266((Re ((f + R15) - f))) + K266((Im ((f + R15) - f))))) is V22() real ext-real Element of REAL
p * 1r is V22() Element of COMPLEX
L is V22() set
x0 /. L is V22() Element of COMPLEX
(x0 /. L) - (x0 /. f) is V22() Element of COMPLEX
- (x0 /. f) is V22() set
(x0 /. L) + (- (x0 /. f)) is V22() set
L - f is V22() set
- f is V22() set
L + (- f) is V22() set
s1 /. (L - f) is V22() Element of COMPLEX
M /. (L - f) is V22() Element of COMPLEX
(s1 /. (L - f)) + (M /. (L - f)) is V22() Element of COMPLEX
m /. (L - f) is V22() Element of COMPLEX
n /. (L - f) is V22() Element of COMPLEX
(m /. (L - f)) + (n /. (L - f)) is V22() Element of COMPLEX
R19 is V22() Element of COMPLEX
R15 is V22() Element of COMPLEX
R19 - R15 is V22() Element of COMPLEX
- R15 is V22() set
R19 + (- R15) is V22() set
p * (R19 - R15) is V22() Element of COMPLEX
M /. (R19 - R15) is V22() Element of COMPLEX
M . (R19 - R15) is V22() Element of COMPLEX
(p * (R19 - R15)) + (M /. (R19 - R15)) is V22() Element of COMPLEX
m /. (R19 - R15) is V22() Element of COMPLEX
m . (R19 - R15) is V22() Element of COMPLEX
n /. (R19 - R15) is V22() Element of COMPLEX
n . (R19 - R15) is V22() Element of COMPLEX
(m /. (R19 - R15)) + (n /. (R19 - R15)) is V22() Element of COMPLEX
(p * 1r) * (L - f) is V22() set
((p * 1r) * (L - f)) + (M /. (L - f)) is V22() set
y1 * 1r is V22() Element of COMPLEX
(y1 * 1r) * (L - f) is V22() set
((y1 * 1r) * (L - f)) + (n /. (L - f)) is V22() set
L * (L - f) is V22() set
(L * (L - f)) + (M /. (L - f)) is V22() set
R * (L - f) is V22() set
(R * (L - f)) + (n /. (L - f)) is V22() set
dom n is V45() Element of K19(COMPLEX)
rng R13 is V45() Element of K19(COMPLEX)
dom M is V45() Element of K19(COMPLEX)
L is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
R13 . L is V22() Element of COMPLEX
L * (R13 . L) is V22() Element of COMPLEX
M /. (R13 . L) is V22() Element of COMPLEX
M . (R13 . L) is V22() Element of COMPLEX
(L * (R13 . L)) + (M /. (R13 . L)) is V22() Element of COMPLEX
R * (R13 . L) is V22() Element of COMPLEX
n /. (R13 . L) is V22() Element of COMPLEX
n . (R13 . L) is V22() Element of COMPLEX
(R * (R13 . L)) + (n /. (R13 . L)) is V22() Element of COMPLEX
R15 is V22() set
R15 - f is V22() set
R15 + (- f) is V22() set
(L * (R13 . L)) / (R13 . L) is V22() Element of COMPLEX
(R13 . L) " is V22() set
Re (R13 . L) is V22() real ext-real Element of REAL
K266((Re (R13 . L))) is V22() real ext-real Element of REAL
Im (R13 . L) is V22() real ext-real Element of REAL
K266((Im (R13 . L))) is V22() real ext-real Element of REAL
K266((Re (R13 . L))) + K266((Im (R13 . L))) is V22() real ext-real Element of REAL
(Re (R13 . L)) / (K266((Re (R13 . L))) + K266((Im (R13 . L)))) is V22() real ext-real Element of REAL
- (Im (R13 . L)) is V22() real ext-real Element of REAL
(- (Im (R13 . L))) / (K266((Re (R13 . L))) + K266((Im (R13 . L)))) is V22() real ext-real Element of REAL
K278() is V22() Element of COMPLEX
((- (Im (R13 . L))) / (K266((Re (R13 . L))) + K266((Im (R13 . L))))) * K278() is V22() set
((Re (R13 . L)) / (K266((Re (R13 . L))) + K266((Im (R13 . L))))) + (((- (Im (R13 . L))) / (K266((Re (R13 . L))) + K266((Im (R13 . L))))) * K278()) is V22() set
(L * (R13 . L)) * ((R13 . L) ") is V22() set
(M /. (R13 . L)) / (R13 . L) is V22() Element of COMPLEX
(M /. (R13 . L)) * ((R13 . L) ") is V22() set
((L * (R13 . L)) / (R13 . L)) + ((M /. (R13 . L)) / (R13 . L)) is V22() Element of COMPLEX
((R * (R13 . L)) + (n /. (R13 . L))) / (R13 . L) is V22() Element of COMPLEX
((R * (R13 . L)) + (n /. (R13 . L))) * ((R13 . L) ") is V22() set
(R * (R13 . L)) / (R13 . L) is V22() Element of COMPLEX
(R * (R13 . L)) * ((R13 . L) ") is V22() set
(R13 . L) / (R13 . L) is V22() Element of COMPLEX
(R13 . L) * ((R13 . L) ") is V22() set
R * ((R13 . L) / (R13 . L)) is V22() Element of COMPLEX
R * 1 is V22() set
(n /. (R13 . L)) / (R13 . L) is V22() Element of COMPLEX
(n /. (R13 . L)) * ((R13 . L) ") is V22() set
R13 " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(R13 ") . L is V22() Element of COMPLEX
(n /. (R13 . L)) * ((R13 ") . L) is V22() Element of COMPLEX
n /* R13 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(n /* R13) . L is V22() Element of COMPLEX
((n /* R13) . L) * ((R13 ") . L) is V22() Element of COMPLEX
(R13 ") (#) (n /* R13) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((R13 ") (#) (n /* R13)) . L is V22() Element of COMPLEX
L * ((R13 . L) / (R13 . L)) is V22() Element of COMPLEX
L * 1 is V22() set
(M /. (R13 . L)) * ((R13 ") . L) is V22() Element of COMPLEX
M /* R13 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(M /* R13) . L is V22() Element of COMPLEX
((M /* R13) . L) * ((R13 ") . L) is V22() Element of COMPLEX
(R13 ") (#) (M /* R13) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((R13 ") (#) (M /* R13)) . L is V22() Element of COMPLEX
L - R is V22() Element of COMPLEX
- R is V22() set
L + (- R) is V22() set
- (((R13 ") (#) (M /* R13)) . L) is V22() Element of COMPLEX
(((R13 ") (#) (n /* R13)) . L) + (- (((R13 ") (#) (M /* R13)) . L)) is V22() Element of COMPLEX
- ((R13 ") (#) (M /* R13)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1) (#) ((R13 ") (#) (M /* R13)) is V1() V4( NAT ) Function-like total complex-valued set
(- ((R13 ") (#) (M /* R13))) . L is V22() Element of COMPLEX
(((R13 ") (#) (n /* R13)) . L) + ((- ((R13 ") (#) (M /* R13))) . L) is V22() Element of COMPLEX
((R13 ") (#) (n /* R13)) + (- ((R13 ") (#) (M /* R13))) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(((R13 ") (#) (n /* R13)) + (- ((R13 ") (#) (M /* R13)))) . L is V22() Element of COMPLEX
((R13 ") (#) (n /* R13)) - ((R13 ") (#) (M /* R13)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- ((R13 ") (#) (M /* R13)) is V1() V4( NAT ) Function-like total complex-valued set
((R13 ") (#) (n /* R13)) + (- ((R13 ") (#) (M /* R13))) is V1() V4( NAT ) Function-like total complex-valued set
(((R13 ") (#) (n /* R13)) - ((R13 ") (#) (M /* R13))) . 1 is V22() Element of COMPLEX
lim (((R13 ") (#) (n /* R13)) - ((R13 ") (#) (M /* R13))) is V22() Element of COMPLEX
lim ((R13 ") (#) (n /* R13)) is V22() Element of COMPLEX
lim ((R13 ") (#) (M /* R13)) is V22() Element of COMPLEX
0 - 0 is V22() real ext-real Element of REAL
- 0 is V22() real ext-real non positive set
0 + (- 0) is V22() real ext-real set
x0 is set
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V45() Element of K19(COMPLEX)
x0 is V45() Element of K19(COMPLEX)
x0 ` is V45() Element of K19(COMPLEX)
K17(COMPLEX,x0) is V45() set
f is V22() set
{ b1 where b1 is V22() set : not 1 / (a1 + 1) <= |.(b1 - f).| } is set
N is V22() real ext-real Element of REAL
{ b1 where b1 is V22() set : not N <= |.(b1 - f).| } is set
R is set
a is V22() set
a - f is V22() set
- f is V22() set
a + (- f) is V22() set
|.(a - f).| is V22() real ext-real Element of REAL
Re (a - f) is V22() real ext-real Element of REAL
K266((Re (a - f))) is V22() real ext-real Element of REAL
Im (a - f) is V22() real ext-real Element of REAL
K266((Im (a - f))) is V22() real ext-real Element of REAL
K266((Re (a - f))) + K266((Im (a - f))) is V22() real ext-real Element of REAL
K268((K266((Re (a - f))) + K266((Im (a - f))))) is V22() real ext-real Element of REAL
s1 is V22() Element of COMPLEX
M is V22() Element of COMPLEX
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
N + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
1 / (N + 1) is V11() V22() real ext-real positive non negative Element of REAL
(N + 1) " is V11() V22() real ext-real positive non negative set
1 * ((N + 1) ") is V11() V22() real ext-real positive non negative set
{ b1 where b1 is V22() set : not 1 / (N + 1) <= |.(b1 - f).| } is set
N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng N is V45() Element of K19(COMPLEX)
L is set
dom N is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
R is set
N . R is V22() set
a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
N . a is V22() Element of COMPLEX
L is V22() real ext-real Element of REAL
L " is V22() real ext-real Element of REAL
R is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
s1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
a + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
s1 + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
1 / (s1 + 1) is V11() V22() real ext-real positive non negative Element of REAL
(s1 + 1) " is V11() V22() real ext-real positive non negative set
1 * ((s1 + 1) ") is V11() V22() real ext-real positive non negative set
1 / (a + 1) is V11() V22() real ext-real positive non negative Element of REAL
(a + 1) " is V11() V22() real ext-real positive non negative set
1 * ((a + 1) ") is V11() V22() real ext-real positive non negative set
N . s1 is V22() Element of COMPLEX
{ b1 where b1 is V22() set : not 1 / (s1 + 1) <= |.(b1 - f).| } is set
(N . s1) - f is V22() set
(N . s1) + (- f) is V22() set
|.((N . s1) - f).| is V22() real ext-real Element of REAL
Re ((N . s1) - f) is V22() real ext-real Element of REAL
K266((Re ((N . s1) - f))) is V22() real ext-real Element of REAL
Im ((N . s1) - f) is V22() real ext-real Element of REAL
K266((Im ((N . s1) - f))) is V22() real ext-real Element of REAL
K266((Re ((N . s1) - f))) + K266((Im ((N . s1) - f))) is V22() real ext-real Element of REAL
K268((K266((Re ((N . s1) - f))) + K266((Im ((N . s1) - f))))) is V22() real ext-real Element of REAL
M is V22() set
M - f is V22() set
M + (- f) is V22() set
|.(M - f).| is V22() real ext-real Element of REAL
Re (M - f) is V22() real ext-real Element of REAL
K266((Re (M - f))) is V22() real ext-real Element of REAL
Im (M - f) is V22() real ext-real Element of REAL
K266((Im (M - f))) is V22() real ext-real Element of REAL
K266((Re (M - f))) + K266((Im (M - f))) is V22() real ext-real Element of REAL
K268((K266((Re (M - f))) + K266((Im (M - f))))) is V22() real ext-real Element of REAL
(L ") + 0 is V22() real ext-real Element of REAL
1 / (L ") is V22() real ext-real Element of REAL
(L ") " is V22() real ext-real set
1 * ((L ") ") is V22() real ext-real set
lim N is V22() Element of COMPLEX
COMPLEX \ x0 is V45() Element of K19(COMPLEX)
x0 is V45() Element of K19(COMPLEX)
f is V22() set
N is V45() (f)
L is V22() real ext-real Element of REAL
{ b1 where b1 is V22() set : not L <= |.(b1 - f).| } is set
x0 is V45() Element of K19(COMPLEX)
x0 ` is V45() Element of K19(COMPLEX)
K17(COMPLEX,x0) is V45() set
f is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng f is V45() Element of K19(COMPLEX)
lim f is V22() Element of COMPLEX
N is V45() ( lim f)
L is V22() real ext-real Element of REAL
{ b1 where b1 is V22() set : not L <= |.(b1 - (lim f)).| } is set
R is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
dom f is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
f . R is V22() Element of COMPLEX
(f . R) - (lim f) is V22() Element of COMPLEX
- (lim f) is V22() set
(f . R) + (- (lim f)) is V22() set
|.((f . R) - (lim f)).| is V22() real ext-real Element of REAL
Re ((f . R) - (lim f)) is V22() real ext-real Element of REAL
K266((Re ((f . R) - (lim f)))) is V22() real ext-real Element of REAL
Im ((f . R) - (lim f)) is V22() real ext-real Element of REAL
K266((Im ((f . R) - (lim f)))) is V22() real ext-real Element of REAL
K266((Re ((f . R) - (lim f)))) + K266((Im ((f . R) - (lim f)))) is V22() real ext-real Element of REAL
K268((K266((Re ((f . R) - (lim f)))) + K266((Im ((f . R) - (lim f)))))) is V22() real ext-real Element of REAL
x0 is V45() Element of K19(COMPLEX)
f is V22() set
N is V45() Element of K19(COMPLEX)
x0 is V45() Element of K19(COMPLEX)
f is V22() Element of COMPLEX
N is V22() real ext-real Element of REAL
{ b1 where b1 is V22() set : not N <= |.(b1 - f).| } is set
L is V45() Element of K19(COMPLEX)
R is V22() set
R - f is V22() set
- f is V22() set
R + (- f) is V22() set
|.(R - f).| is V22() real ext-real Element of REAL
Re (R - f) is V22() real ext-real Element of REAL
K266((Re (R - f))) is V22() real ext-real Element of REAL
Im (R - f) is V22() real ext-real Element of REAL
K266((Im (R - f))) is V22() real ext-real Element of REAL
K266((Re (R - f))) + K266((Im (R - f))) is V22() real ext-real Element of REAL
K268((K266((Re (R - f))) + K266((Im (R - f))))) is V22() real ext-real Element of REAL
N - |.(R - f).| is V22() real ext-real Element of REAL
- |.(R - f).| is V22() real ext-real set
N + (- |.(R - f).|) is V22() real ext-real set
(N - |.(R - f).|) / 2 is V22() real ext-real Element of REAL
2 " is V11() V22() real ext-real positive non negative set
(N - |.(R - f).|) * (2 ") is V22() real ext-real set
a is V22() real ext-real Element of REAL
{ b1 where b1 is V22() set : not a <= |.(b1 - R).| } is set
M is V22() set
M - f is V22() set
M + (- f) is V22() set
|.(M - f).| is V22() real ext-real Element of REAL
Re (M - f) is V22() real ext-real Element of REAL
K266((Re (M - f))) is V22() real ext-real Element of REAL
Im (M - f) is V22() real ext-real Element of REAL
K266((Im (M - f))) is V22() real ext-real Element of REAL
K266((Re (M - f))) + K266((Im (M - f))) is V22() real ext-real Element of REAL
K268((K266((Re (M - f))) + K266((Im (M - f))))) is V22() real ext-real Element of REAL
(N - |.(R - f).|) + |.(R - f).| is V22() real ext-real Element of REAL
a + |.(R - f).| is V22() real ext-real Element of REAL
M is V45() (R)
p is set
m is V22() set
m - R is V22() set
- R is V22() set
m + (- R) is V22() set
|.(m - R).| is V22() real ext-real Element of REAL
Re (m - R) is V22() real ext-real Element of REAL
K266((Re (m - R))) is V22() real ext-real Element of REAL
Im (m - R) is V22() real ext-real Element of REAL
K266((Im (m - R))) is V22() real ext-real Element of REAL
K266((Re (m - R))) + K266((Im (m - R))) is V22() real ext-real Element of REAL
K268((K266((Re (m - R))) + K266((Im (m - R))))) is V22() real ext-real Element of REAL
|.(m - R).| + |.(R - f).| is V22() real ext-real Element of REAL
m - f is V22() set
m + (- f) is V22() set
|.(m - f).| is V22() real ext-real Element of REAL
Re (m - f) is V22() real ext-real Element of REAL
K266((Re (m - f))) is V22() real ext-real Element of REAL
Im (m - f) is V22() real ext-real Element of REAL
K266((Im (m - f))) is V22() real ext-real Element of REAL
K266((Re (m - f))) + K266((Im (m - f))) is V22() real ext-real Element of REAL
K268((K266((Re (m - f))) + K266((Im (m - f))))) is V22() real ext-real Element of REAL
x0 is V45() Element of K19(COMPLEX)
f is V22() Element of COMPLEX
N is V22() real ext-real Element of REAL
{ b1 where b1 is V22() set : |.(b1 - f).| <= N } is set
L is V45() Element of K19(COMPLEX)
NAT --> N is V1() V4( NAT ) V5( REAL ) Function-like constant V11() total T-Sequence-like quasi_total complex-valued ext-real-valued real-valued bounded_above bounded_below bounded convergent Element of K19(K20(NAT,REAL))
NAT --> f is V1() V4( NAT ) V5( COMPLEX ) Function-like constant V11() total T-Sequence-like quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
s1 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng s1 is V45() Element of K19(COMPLEX)
lim s1 is V22() Element of COMPLEX
a is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
s1 - a is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- a is V1() V4( NAT ) Function-like total complex-valued set
(- 1) (#) a is V1() V4( NAT ) Function-like total complex-valued set
s1 + (- a) is V1() V4( NAT ) Function-like total complex-valued set
lim (s1 - a) is V22() Element of COMPLEX
lim a is V22() Element of COMPLEX
(lim s1) - (lim a) is V22() Element of COMPLEX
- (lim a) is V22() set
(lim s1) + (- (lim a)) is V22() set
|.(s1 - a).| is V1() V4( NAT ) V5( REAL ) Function-like V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
p is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
|.(s1 - a).| . p is V22() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(s1 - a) . m is V22() Element of COMPLEX
s1 . m is V22() Element of COMPLEX
- a is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(- a) . m is V22() Element of COMPLEX
(s1 . m) + ((- a) . m) is V22() Element of COMPLEX
a . m is V22() Element of COMPLEX
(s1 . m) - (a . m) is V22() Element of COMPLEX
- (a . m) is V22() set
(s1 . m) + (- (a . m)) is V22() set
(s1 . m) - f is V22() Element of COMPLEX
- f is V22() set
(s1 . m) + (- f) is V22() set
(s1 - a) . p is V22() Element of COMPLEX
s1 . p is V22() Element of COMPLEX
(s1 . p) - f is V22() Element of COMPLEX
(s1 . p) + (- f) is V22() set
dom s1 is V45() V46() V47() V48() V49() V50() Element of K19(NAT)
m is V22() set
m - f is V22() set
m + (- f) is V22() set
|.(m - f).| is V22() real ext-real Element of REAL
Re (m - f) is V22() real ext-real Element of REAL
K266((Re (m - f))) is V22() real ext-real Element of REAL
Im (m - f) is V22() real ext-real Element of REAL
K266((Im (m - f))) is V22() real ext-real Element of REAL
K266((Re (m - f))) + K266((Im (m - f))) is V22() real ext-real Element of REAL
K268((K266((Re (m - f))) + K266((Im (m - f))))) is V22() real ext-real Element of REAL
lim |.(s1 - a).| is V22() real ext-real Element of REAL
|.(lim (s1 - a)).| is V22() real ext-real Element of REAL
Re (lim (s1 - a)) is V22() real ext-real Element of REAL
K266((Re (lim (s1 - a)))) is V22() real ext-real Element of REAL
Im (lim (s1 - a)) is V22() real ext-real Element of REAL
K266((Im (lim (s1 - a)))) is V22() real ext-real Element of REAL
K266((Re (lim (s1 - a)))) + K266((Im (lim (s1 - a)))) is V22() real ext-real Element of REAL
K268((K266((Re (lim (s1 - a)))) + K266((Im (lim (s1 - a)))))) is V22() real ext-real Element of REAL
p is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent Element of K19(K20(NAT,COMPLEX))
|.p.| is V1() V4( NAT ) V5( REAL ) Function-like V11() total quasi_total complex-valued ext-real-valued real-valued bounded_above bounded_below bounded convergent Element of K19(K20(NAT,REAL))
R is V1() V4( NAT ) V5( REAL ) Function-like V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
|.p.| . m is V22() real ext-real Element of REAL
R . m is V22() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
a . m is V22() Element of COMPLEX
lim R is V22() real ext-real Element of REAL
R . 0 is V22() real ext-real Element of REAL
lim |.p.| is V22() real ext-real Element of REAL
(lim s1) - f is V22() Element of COMPLEX
- f is V22() set
(lim s1) + (- f) is V22() set
|.((lim s1) - f).| is V22() real ext-real Element of REAL
Re ((lim s1) - f) is V22() real ext-real Element of REAL
K266((Re ((lim s1) - f))) is V22() real ext-real Element of REAL
Im ((lim s1) - f) is V22() real ext-real Element of REAL
K266((Im ((lim s1) - f))) is V22() real ext-real Element of REAL
K266((Re ((lim s1) - f))) + K266((Im ((lim s1) - f))) is V22() real ext-real Element of REAL
K268((K266((Re ((lim s1) - f))) + K266((Im ((lim s1) - f))))) is V22() real ext-real Element of REAL
{ b1 where b1 is V22() set : not 1 <= |.(b1 - 0c).| } is set
x0 is V45() Element of K19(COMPLEX)
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom x0 is V45() Element of K19(COMPLEX)
f is V45() () Element of K19(COMPLEX)
N is V22() Element of COMPLEX
x0 | f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom (x0 | f) is V45() Element of K19(COMPLEX)
(x0 | f) /. N is V22() Element of COMPLEX
L is V45() (N)
x0 /. N is V22() Element of COMPLEX
(dom x0) /\ f is V45() Element of K19(COMPLEX)
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
a is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
a is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
s1 is V22() Element of COMPLEX
x0 /. s1 is V22() Element of COMPLEX
(x0 /. s1) - (x0 /. N) is V22() Element of COMPLEX
- (x0 /. N) is V22() set
(x0 /. s1) + (- (x0 /. N)) is V22() set
s1 - N is V22() set
- N is V22() set
s1 + (- N) is V22() set
R /. (s1 - N) is V22() Element of COMPLEX
a /. (s1 - N) is V22() Element of COMPLEX
(R /. (s1 - N)) + (a /. (s1 - N)) is V22() Element of COMPLEX
(x0 | f) /. s1 is V22() Element of COMPLEX
((x0 | f) /. s1) - ((x0 | f) /. N) is V22() Element of COMPLEX
- ((x0 | f) /. N) is V22() set
((x0 | f) /. s1) + (- ((x0 | f) /. N)) is V22() set
s1 - N is V22() Element of COMPLEX
R /. (s1 - N) is V22() Element of COMPLEX
R . (s1 - N) is V22() Element of COMPLEX
a /. (s1 - N) is V22() Element of COMPLEX
a . (s1 - N) is V22() Element of COMPLEX
(R /. (s1 - N)) + (a /. (s1 - N)) is V22() Element of COMPLEX
(x0 /. s1) - ((x0 | f) /. N) is V22() Element of COMPLEX
(x0 /. s1) + (- ((x0 | f) /. N)) is V22() set
x0 | f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
N is V22() Element of COMPLEX
dom (x0 | f) is V45() Element of K19(COMPLEX)
L is V45() (N)
x0 /. N is V22() Element of COMPLEX
R is V45() (N)
a is V45() (N)
(x0 | f) /. N is V22() Element of COMPLEX
(dom x0) /\ f is V45() Element of K19(COMPLEX)
s1 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
M is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
s1 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
M is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
p is V22() Element of COMPLEX
(x0 | f) /. p is V22() Element of COMPLEX
((x0 | f) /. p) - ((x0 | f) /. N) is V22() Element of COMPLEX
- ((x0 | f) /. N) is V22() set
((x0 | f) /. p) + (- ((x0 | f) /. N)) is V22() set
p - N is V22() set
- N is V22() set
p + (- N) is V22() set
s1 /. (p - N) is V22() Element of COMPLEX
M /. (p - N) is V22() Element of COMPLEX
(s1 /. (p - N)) + (M /. (p - N)) is V22() Element of COMPLEX
x0 /. p is V22() Element of COMPLEX
(x0 /. p) - (x0 /. N) is V22() Element of COMPLEX
- (x0 /. N) is V22() set
(x0 /. p) + (- (x0 /. N)) is V22() set
p - N is V22() Element of COMPLEX
s1 /. (p - N) is V22() Element of COMPLEX
s1 . (p - N) is V22() Element of COMPLEX
M /. (p - N) is V22() Element of COMPLEX
M . (p - N) is V22() Element of COMPLEX
(s1 /. (p - N)) + (M /. (p - N)) is V22() Element of COMPLEX
((x0 | f) /. p) - (x0 /. N) is V22() Element of COMPLEX
((x0 | f) /. p) + (- (x0 /. N)) is V22() set
x0 is V45() Element of K19(COMPLEX)
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V45() Element of K19(COMPLEX)
N is V22() set
f | x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom (f | x0) is V45() Element of K19(COMPLEX)
(f | x0) /. N is V22() Element of COMPLEX
L is V45() (N)
(dom f) /\ x0 is V45() Element of K19(COMPLEX)
R is V45() (N)
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f is set
N is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom N is V45() Element of K19(COMPLEX)
L is set
L is set
L is V22() Element of COMPLEX
N . L is V22() set
(x0,L) is V22() Element of COMPLEX
N /. L is V22() Element of COMPLEX
L is V22() Element of COMPLEX
N /. L is V22() Element of COMPLEX
(x0,L) is V22() Element of COMPLEX
N is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom N is V45() Element of K19(COMPLEX)
L is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom L is V45() Element of K19(COMPLEX)
R is V22() Element of COMPLEX
N /. R is V22() Element of COMPLEX
(x0,R) is V22() Element of COMPLEX
L /. R is V22() Element of COMPLEX
cf is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom cf is V45() Element of K19(COMPLEX)
f is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
rng f is V45() Element of K19(COMPLEX)
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
f " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
cf /* f is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f ") (#) (cf /* f) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((f ") (#) (cf /* f)) . N is V22() Element of COMPLEX
(f ") . N is V22() Element of COMPLEX
(cf /* f) . N is V22() Element of COMPLEX
((f ") . N) * ((cf /* f) . N) is V22() Element of COMPLEX
f . N is V22() Element of COMPLEX
cf /. (f . N) is V22() Element of COMPLEX
cf . (f . N) is V22() Element of COMPLEX
((f ") . N) * (cf /. (f . N)) is V22() Element of COMPLEX
((f ") . N) * 0c is V22() Element of COMPLEX
((f ") (#) (cf /* f)) . 0 is V22() Element of COMPLEX
lim ((f ") (#) (cf /* f)) is V22() Element of COMPLEX
L is V22() Element of COMPLEX
cf /. L is V22() Element of COMPLEX
cf . L is V22() Element of COMPLEX
0c * L is V22() Element of COMPLEX
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom R is V45() Element of K19(COMPLEX)
rng R is V45() Element of K19(COMPLEX)
a is V45() () Element of K19(COMPLEX)
(R,a) is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
s1 is V22() Element of COMPLEX
{s1} is V45() set
M is V22() Element of COMPLEX
R . M is V22() set
R /. M is V22() Element of COMPLEX
M is V22() Element of COMPLEX
p is V45() (M)
R /. M is V22() Element of COMPLEX
L is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m is V22() Element of COMPLEX
R /. m is V22() Element of COMPLEX
(R /. m) - (R /. M) is V22() Element of COMPLEX
- (R /. M) is V22() set
(R /. m) + (- (R /. M)) is V22() set
m - M is V22() Element of COMPLEX
- M is V22() set
m + (- M) is V22() set
L /. (m - M) is V22() Element of COMPLEX
L . (m - M) is V22() Element of COMPLEX
f /. (m - M) is V22() Element of COMPLEX
f . (m - M) is V22() Element of COMPLEX
(L /. (m - M)) + (f /. (m - M)) is V22() Element of COMPLEX
s1 - (R /. M) is V22() Element of COMPLEX
s1 + (- (R /. M)) is V22() set
s1 - s1 is V22() Element of COMPLEX
- s1 is V22() set
s1 + (- s1) is V22() set
(L /. (m - M)) + 0c is V22() Element of COMPLEX
M is V22() Element of COMPLEX
(R,a) /. M is V22() Element of COMPLEX
R /. M is V22() Element of COMPLEX
p is V45() (M)
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
p is V45() (M)
m is V22() Element of COMPLEX
R /. m is V22() Element of COMPLEX
(R /. m) - (R /. M) is V22() Element of COMPLEX
- (R /. M) is V22() set
(R /. m) + (- (R /. M)) is V22() set
m - M is V22() Element of COMPLEX
- M is V22() set
m + (- M) is V22() set
L /. (m - M) is V22() Element of COMPLEX
L . (m - M) is V22() Element of COMPLEX
f /. (m - M) is V22() Element of COMPLEX
f . (m - M) is V22() Element of COMPLEX
(L /. (m - M)) + (f /. (m - M)) is V22() Element of COMPLEX
s1 - (R /. M) is V22() Element of COMPLEX
s1 + (- (R /. M)) is V22() set
s1 - s1 is V22() Element of COMPLEX
- s1 is V22() set
s1 + (- s1) is V22() set
(L /. (m - M)) + 0c is V22() Element of COMPLEX
(R,M) is V22() Element of COMPLEX
L /. 1r is V22() Element of COMPLEX
L . 1r is V22() Element of COMPLEX
x0 is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
x0 ^\ f is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of x0
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(x0 ^\ f) . N is V22() Element of COMPLEX
N + f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
x0 . (N + f) is V22() Element of COMPLEX
x0 is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
x0 ^\ f is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of x0
lim x0 is V22() Element of COMPLEX
lim (x0 ^\ f) is V22() Element of COMPLEX
N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
f is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f ^\ x0 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of f
N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f + N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f + N) ^\ x0 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of f + N
N ^\ x0 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of N
(f ^\ x0) + (N ^\ x0) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
L is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
((f + N) ^\ x0) . L is V22() Element of COMPLEX
L + x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(f + N) . (L + x0) is V22() Element of COMPLEX
f . (L + x0) is V22() Element of COMPLEX
N . (L + x0) is V22() Element of COMPLEX
(f . (L + x0)) + (N . (L + x0)) is V22() Element of COMPLEX
(f ^\ x0) . L is V22() Element of COMPLEX
((f ^\ x0) . L) + (N . (L + x0)) is V22() Element of COMPLEX
(N ^\ x0) . L is V22() Element of COMPLEX
((f ^\ x0) . L) + ((N ^\ x0) . L) is V22() Element of COMPLEX
((f ^\ x0) + (N ^\ x0)) . L is V22() Element of COMPLEX
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
f is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f ^\ x0 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of f
N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f - N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- N is V1() V4( NAT ) Function-like total complex-valued set
(- 1) (#) N is V1() V4( NAT ) Function-like total complex-valued set
f + (- N) is V1() V4( NAT ) Function-like total complex-valued set
(f - N) ^\ x0 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of f - N
N ^\ x0 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of N
(f ^\ x0) - (N ^\ x0) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- (N ^\ x0) is V1() V4( NAT ) Function-like total complex-valued set
(- 1) (#) (N ^\ x0) is V1() V4( NAT ) Function-like total complex-valued set
(f ^\ x0) + (- (N ^\ x0)) is V1() V4( NAT ) Function-like total complex-valued set
L is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
((f - N) ^\ x0) . L is V22() Element of COMPLEX
- N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f + (- N) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
L + x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(f + (- N)) . (L + x0) is V22() Element of COMPLEX
f . (L + x0) is V22() Element of COMPLEX
(- N) . (L + x0) is V22() Element of COMPLEX
(f . (L + x0)) + ((- N) . (L + x0)) is V22() Element of COMPLEX
N . (L + x0) is V22() Element of COMPLEX
- (N . (L + x0)) is V22() Element of COMPLEX
(f . (L + x0)) + (- (N . (L + x0))) is V22() Element of COMPLEX
(f ^\ x0) . L is V22() Element of COMPLEX
((f ^\ x0) . L) - (N . (L + x0)) is V22() Element of COMPLEX
- (N . (L + x0)) is V22() set
((f ^\ x0) . L) + (- (N . (L + x0))) is V22() set
(N ^\ x0) . L is V22() Element of COMPLEX
- ((N ^\ x0) . L) is V22() Element of COMPLEX
((f ^\ x0) . L) + (- ((N ^\ x0) . L)) is V22() Element of COMPLEX
- (N ^\ x0) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(- (N ^\ x0)) . L is V22() Element of COMPLEX
((f ^\ x0) . L) + ((- (N ^\ x0)) . L) is V22() Element of COMPLEX
((f ^\ x0) - (N ^\ x0)) . L is V22() Element of COMPLEX
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
f is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f ") ^\ x0 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of f "
f ^\ x0 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of f
(f ^\ x0) " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
((f ") ^\ x0) . N is V22() Element of COMPLEX
N + x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(f ") . (N + x0) is V22() Element of COMPLEX
f . (N + x0) is V22() Element of COMPLEX
(f . (N + x0)) " is V22() Element of COMPLEX
Re (f . (N + x0)) is V22() real ext-real Element of REAL
K266((Re (f . (N + x0)))) is V22() real ext-real Element of REAL
Im (f . (N + x0)) is V22() real ext-real Element of REAL
K266((Im (f . (N + x0)))) is V22() real ext-real Element of REAL
K266((Re (f . (N + x0)))) + K266((Im (f . (N + x0)))) is V22() real ext-real Element of REAL
(Re (f . (N + x0))) / (K266((Re (f . (N + x0)))) + K266((Im (f . (N + x0))))) is V22() real ext-real Element of REAL
(K266((Re (f . (N + x0)))) + K266((Im (f . (N + x0))))) " is V22() real ext-real set
(Re (f . (N + x0))) * ((K266((Re (f . (N + x0)))) + K266((Im (f . (N + x0))))) ") is V22() real ext-real set
- (Im (f . (N + x0))) is V22() real ext-real Element of REAL
(- (Im (f . (N + x0)))) / (K266((Re (f . (N + x0)))) + K266((Im (f . (N + x0))))) is V22() real ext-real Element of REAL
(- (Im (f . (N + x0)))) * ((K266((Re (f . (N + x0)))) + K266((Im (f . (N + x0))))) ") is V22() real ext-real set
K278() is V22() Element of COMPLEX
((- (Im (f . (N + x0)))) / (K266((Re (f . (N + x0)))) + K266((Im (f . (N + x0)))))) * K278() is V22() set
((Re (f . (N + x0))) / (K266((Re (f . (N + x0)))) + K266((Im (f . (N + x0)))))) + (((- (Im (f . (N + x0)))) / (K266((Re (f . (N + x0)))) + K266((Im (f . (N + x0)))))) * K278()) is V22() set
(f ^\ x0) . N is V22() Element of COMPLEX
((f ^\ x0) . N) " is V22() Element of COMPLEX
Re ((f ^\ x0) . N) is V22() real ext-real Element of REAL
K266((Re ((f ^\ x0) . N))) is V22() real ext-real Element of REAL
Im ((f ^\ x0) . N) is V22() real ext-real Element of REAL
K266((Im ((f ^\ x0) . N))) is V22() real ext-real Element of REAL
K266((Re ((f ^\ x0) . N))) + K266((Im ((f ^\ x0) . N))) is V22() real ext-real Element of REAL
(Re ((f ^\ x0) . N)) / (K266((Re ((f ^\ x0) . N))) + K266((Im ((f ^\ x0) . N)))) is V22() real ext-real Element of REAL
(K266((Re ((f ^\ x0) . N))) + K266((Im ((f ^\ x0) . N)))) " is V22() real ext-real set
(Re ((f ^\ x0) . N)) * ((K266((Re ((f ^\ x0) . N))) + K266((Im ((f ^\ x0) . N)))) ") is V22() real ext-real set
- (Im ((f ^\ x0) . N)) is V22() real ext-real Element of REAL
(- (Im ((f ^\ x0) . N))) / (K266((Re ((f ^\ x0) . N))) + K266((Im ((f ^\ x0) . N)))) is V22() real ext-real Element of REAL
(- (Im ((f ^\ x0) . N))) * ((K266((Re ((f ^\ x0) . N))) + K266((Im ((f ^\ x0) . N)))) ") is V22() real ext-real set
((- (Im ((f ^\ x0) . N))) / (K266((Re ((f ^\ x0) . N))) + K266((Im ((f ^\ x0) . N))))) * K278() is V22() set
((Re ((f ^\ x0) . N)) / (K266((Re ((f ^\ x0) . N))) + K266((Im ((f ^\ x0) . N))))) + (((- (Im ((f ^\ x0) . N))) / (K266((Re ((f ^\ x0) . N))) + K266((Im ((f ^\ x0) . N))))) * K278()) is V22() set
((f ^\ x0) ") . N is V22() Element of COMPLEX
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
f is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f ^\ x0 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of f
N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f (#) N is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f (#) N) ^\ x0 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of f (#) N
N ^\ x0 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of N
(f ^\ x0) (#) (N ^\ x0) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
L is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
((f (#) N) ^\ x0) . L is V22() Element of COMPLEX
L + x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(f (#) N) . (L + x0) is V22() Element of COMPLEX
f . (L + x0) is V22() Element of COMPLEX
N . (L + x0) is V22() Element of COMPLEX
(f . (L + x0)) * (N . (L + x0)) is V22() Element of COMPLEX
(f ^\ x0) . L is V22() Element of COMPLEX
((f ^\ x0) . L) * (N . (L + x0)) is V22() Element of COMPLEX
(N ^\ x0) . L is V22() Element of COMPLEX
((f ^\ x0) . L) * ((N ^\ x0) . L) is V22() Element of COMPLEX
((f ^\ x0) (#) (N ^\ x0)) . L is V22() Element of COMPLEX
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom x0 is V45() Element of K19(COMPLEX)
f is V22() set
{f} is V45() set
(x0,f) is V22() Element of COMPLEX
N is V45() (f)
x0 /. f is V22() Element of COMPLEX
L is V45() (f)
R is V45() (f)
a is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
a " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
s1 is V1() V4( NAT ) V5( COMPLEX ) Function-like constant V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng s1 is V12() V45() Element of K19(COMPLEX)
a + s1 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng (a + s1) is V45() Element of K19(COMPLEX)
x0 /* (a + s1) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
x0 /* s1 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(x0 /* (a + s1)) - (x0 /* s1) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- (x0 /* s1) is V1() V4( NAT ) Function-like total complex-valued set
(- 1) (#) (x0 /* s1) is V1() V4( NAT ) Function-like total complex-valued set
(x0 /* (a + s1)) + (- (x0 /* s1)) is V1() V4( NAT ) Function-like total complex-valued set
(a ") (#) ((x0 /* (a + s1)) - (x0 /* s1)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((a ") (#) ((x0 /* (a + s1)) - (x0 /* s1))) is V22() Element of COMPLEX
M is V22() real ext-real Element of REAL
{ b1 where b1 is V22() set : not M <= |.(b1 - f).| } is set
f - f is V22() set
- f is V22() set
f + (- f) is V22() set
|.(f - f).| is V22() real ext-real Element of REAL
Re (f - f) is V22() real ext-real Element of REAL
K266((Re (f - f))) is V22() real ext-real Element of REAL
Im (f - f) is V22() real ext-real Element of REAL
K266((Im (f - f))) is V22() real ext-real Element of REAL
K266((Re (f - f))) + K266((Im (f - f))) is V22() real ext-real Element of REAL
K268((K266((Re (f - f))) + K266((Im (f - f))))) is V22() real ext-real Element of REAL
p is set
lim s1 is V22() Element of COMPLEX
lim a is V22() Element of COMPLEX
lim (a + s1) is V22() Element of COMPLEX
0 + f is V22() set
p is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
s1 ^\ p is V1() V4( NAT ) V5( COMPLEX ) Function-like constant V11() total quasi_total complex-valued subsequence of s1
rng (s1 ^\ p) is V12() V45() Element of K19(COMPLEX)
(a + s1) ^\ p is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of a + s1
rng ((a + s1) ^\ p) is V45() Element of K19(COMPLEX)
m is set
m is set
m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
((a + s1) ^\ p) . m is V22() Element of COMPLEX
p + 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
p + m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(a + s1) . (p + m) is V22() Element of COMPLEX
((a + s1) . (p + m)) - f is V22() set
((a + s1) . (p + m)) + (- f) is V22() set
|.(((a + s1) . (p + m)) - f).| is V22() real ext-real Element of REAL
Re (((a + s1) . (p + m)) - f) is V22() real ext-real Element of REAL
K266((Re (((a + s1) . (p + m)) - f))) is V22() real ext-real Element of REAL
Im (((a + s1) . (p + m)) - f) is V22() real ext-real Element of REAL
K266((Im (((a + s1) . (p + m)) - f))) is V22() real ext-real Element of REAL
K266((Re (((a + s1) . (p + m)) - f))) + K266((Im (((a + s1) . (p + m)) - f))) is V22() real ext-real Element of REAL
K268((K266((Re (((a + s1) . (p + m)) - f))) + K266((Im (((a + s1) . (p + m)) - f))))) is V22() real ext-real Element of REAL
(((a + s1) ^\ p) . m) - f is V22() set
(((a + s1) ^\ p) . m) + (- f) is V22() set
|.((((a + s1) ^\ p) . m) - f).| is V22() real ext-real Element of REAL
Re ((((a + s1) ^\ p) . m) - f) is V22() real ext-real Element of REAL
K266((Re ((((a + s1) ^\ p) . m) - f))) is V22() real ext-real Element of REAL
Im ((((a + s1) ^\ p) . m) - f) is V22() real ext-real Element of REAL
K266((Im ((((a + s1) ^\ p) . m) - f))) is V22() real ext-real Element of REAL
K266((Re ((((a + s1) ^\ p) . m) - f))) + K266((Im ((((a + s1) ^\ p) . m) - f))) is V22() real ext-real Element of REAL
K268((K266((Re ((((a + s1) ^\ p) . m) - f))) + K266((Im ((((a + s1) ^\ p) . m) - f))))) is V22() real ext-real Element of REAL
n is V22() set
p is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
s1 ^\ p is V1() V4( NAT ) V5( COMPLEX ) Function-like constant V11() total quasi_total complex-valued subsequence of s1
rng (s1 ^\ p) is V12() V45() Element of K19(COMPLEX)
(a + s1) ^\ p is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of a + s1
rng ((a + s1) ^\ p) is V45() Element of K19(COMPLEX)
p is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
s1 ^\ p is V1() V4( NAT ) V5( COMPLEX ) Function-like constant V11() total quasi_total complex-valued subsequence of s1
rng (s1 ^\ p) is V12() V45() Element of K19(COMPLEX)
(a + s1) ^\ p is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of a + s1
rng ((a + s1) ^\ p) is V45() Element of K19(COMPLEX)
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
n is set
a ^\ p is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) subsequence of a
m /* (a ^\ p) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
m /* (a ^\ p) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(m /* (a ^\ p)) + (m /* (a ^\ p)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(a ^\ p) " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((m /* (a ^\ p)) + (m /* (a ^\ p))) (#) ((a ^\ p) ") is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim (((m /* (a ^\ p)) + (m /* (a ^\ p))) (#) ((a ^\ p) ")) is V22() Element of COMPLEX
m /. 1r is V22() Element of COMPLEX
m . 1r is V22() Element of COMPLEX
(m /* (a ^\ p)) (#) ((a ^\ p) ") is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
n is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((a ^\ p) ") (#) (m /* (a ^\ p)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim (((a ^\ p) ") (#) (m /* (a ^\ p))) is V22() Element of COMPLEX
y1 is V22() real ext-real Element of REAL
R18 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
R17 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
R16 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
n . R16 is V22() Element of COMPLEX
(n . R16) - (m /. 1r) is V22() Element of COMPLEX
- (m /. 1r) is V22() set
(n . R16) + (- (m /. 1r)) is V22() set
abs ((n . R16) - (m /. 1r)) is V22() real ext-real Element of REAL
Re ((n . R16) - (m /. 1r)) is V22() real ext-real Element of REAL
K266((Re ((n . R16) - (m /. 1r)))) is V22() real ext-real Element of REAL
Im ((n . R16) - (m /. 1r)) is V22() real ext-real Element of REAL
K266((Im ((n . R16) - (m /. 1r)))) is V22() real ext-real Element of REAL
K266((Re ((n . R16) - (m /. 1r)))) + K266((Im ((n . R16) - (m /. 1r)))) is V22() real ext-real Element of REAL
K268((K266((Re ((n . R16) - (m /. 1r)))) + K266((Im ((n . R16) - (m /. 1r)))))) is V22() real ext-real Element of REAL
((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R16 is V22() Element of COMPLEX
(m /. 1r) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R16) is V22() Element of COMPLEX
((m /. 1r) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R16)) - (m /. 1r) is V22() Element of COMPLEX
((m /. 1r) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R16)) + (- (m /. 1r)) is V22() set
abs (((m /. 1r) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R16)) - (m /. 1r)) is V22() real ext-real Element of REAL
Re (((m /. 1r) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R16)) - (m /. 1r)) is V22() real ext-real Element of REAL
K266((Re (((m /. 1r) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R16)) - (m /. 1r)))) is V22() real ext-real Element of REAL
Im (((m /. 1r) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R16)) - (m /. 1r)) is V22() real ext-real Element of REAL
K266((Im (((m /. 1r) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R16)) - (m /. 1r)))) is V22() real ext-real Element of REAL
K266((Re (((m /. 1r) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R16)) - (m /. 1r)))) + K266((Im (((m /. 1r) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R16)) - (m /. 1r)))) is V22() real ext-real Element of REAL
K268((K266((Re (((m /. 1r) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R16)) - (m /. 1r)))) + K266((Im (((m /. 1r) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R16)) - (m /. 1r)))))) is V22() real ext-real Element of REAL
(((a ^\ p) ") (#) (m /* (a ^\ p))) . R16 is V22() Element of COMPLEX
((((a ^\ p) ") (#) (m /* (a ^\ p))) . R16) - 0c is V22() Element of COMPLEX
- 0c is V22() set
((((a ^\ p) ") (#) (m /* (a ^\ p))) . R16) + (- 0c) is V22() set
abs (((((a ^\ p) ") (#) (m /* (a ^\ p))) . R16) - 0c) is V22() real ext-real Element of REAL
Re (((((a ^\ p) ") (#) (m /* (a ^\ p))) . R16) - 0c) is V22() real ext-real Element of REAL
K266((Re (((((a ^\ p) ") (#) (m /* (a ^\ p))) . R16) - 0c))) is V22() real ext-real Element of REAL
Im (((((a ^\ p) ") (#) (m /* (a ^\ p))) . R16) - 0c) is V22() real ext-real Element of REAL
K266((Im (((((a ^\ p) ") (#) (m /* (a ^\ p))) . R16) - 0c))) is V22() real ext-real Element of REAL
K266((Re (((((a ^\ p) ") (#) (m /* (a ^\ p))) . R16) - 0c))) + K266((Im (((((a ^\ p) ") (#) (m /* (a ^\ p))) . R16) - 0c))) is V22() real ext-real Element of REAL
K268((K266((Re (((((a ^\ p) ") (#) (m /* (a ^\ p))) . R16) - 0c))) + K266((Im (((((a ^\ p) ") (#) (m /* (a ^\ p))) . R16) - 0c))))) is V22() real ext-real Element of REAL
y1 is V22() Element of COMPLEX
y1 * 1r is V22() Element of COMPLEX
R18 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(a ^\ p) . R18 is V22() Element of COMPLEX
(((m /* (a ^\ p)) + (m /* (a ^\ p))) (#) ((a ^\ p) ")) . R18 is V22() Element of COMPLEX
((m /* (a ^\ p)) + (m /* (a ^\ p))) . R18 is V22() Element of COMPLEX
((a ^\ p) ") . R18 is V22() Element of COMPLEX
(((m /* (a ^\ p)) + (m /* (a ^\ p))) . R18) * (((a ^\ p) ") . R18) is V22() Element of COMPLEX
(m /* (a ^\ p)) . R18 is V22() Element of COMPLEX
(m /* (a ^\ p)) . R18 is V22() Element of COMPLEX
((m /* (a ^\ p)) . R18) + ((m /* (a ^\ p)) . R18) is V22() Element of COMPLEX
(((m /* (a ^\ p)) . R18) + ((m /* (a ^\ p)) . R18)) * (((a ^\ p) ") . R18) is V22() Element of COMPLEX
((m /* (a ^\ p)) . R18) * (((a ^\ p) ") . R18) is V22() Element of COMPLEX
((m /* (a ^\ p)) . R18) * (((a ^\ p) ") . R18) is V22() Element of COMPLEX
(((m /* (a ^\ p)) . R18) * (((a ^\ p) ") . R18)) + (((m /* (a ^\ p)) . R18) * (((a ^\ p) ") . R18)) is V22() Element of COMPLEX
((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R18 is V22() Element of COMPLEX
(((m /* (a ^\ p)) . R18) * (((a ^\ p) ") . R18)) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R18) is V22() Element of COMPLEX
((a ^\ p) . R18) " is V22() Element of COMPLEX
Re ((a ^\ p) . R18) is V22() real ext-real Element of REAL
K266((Re ((a ^\ p) . R18))) is V22() real ext-real Element of REAL
Im ((a ^\ p) . R18) is V22() real ext-real Element of REAL
K266((Im ((a ^\ p) . R18))) is V22() real ext-real Element of REAL
K266((Re ((a ^\ p) . R18))) + K266((Im ((a ^\ p) . R18))) is V22() real ext-real Element of REAL
(Re ((a ^\ p) . R18)) / (K266((Re ((a ^\ p) . R18))) + K266((Im ((a ^\ p) . R18)))) is V22() real ext-real Element of REAL
(K266((Re ((a ^\ p) . R18))) + K266((Im ((a ^\ p) . R18)))) " is V22() real ext-real set
(Re ((a ^\ p) . R18)) * ((K266((Re ((a ^\ p) . R18))) + K266((Im ((a ^\ p) . R18)))) ") is V22() real ext-real set
- (Im ((a ^\ p) . R18)) is V22() real ext-real Element of REAL
(- (Im ((a ^\ p) . R18))) / (K266((Re ((a ^\ p) . R18))) + K266((Im ((a ^\ p) . R18)))) is V22() real ext-real Element of REAL
(- (Im ((a ^\ p) . R18))) * ((K266((Re ((a ^\ p) . R18))) + K266((Im ((a ^\ p) . R18)))) ") is V22() real ext-real set
K278() is V22() Element of COMPLEX
((- (Im ((a ^\ p) . R18))) / (K266((Re ((a ^\ p) . R18))) + K266((Im ((a ^\ p) . R18))))) * K278() is V22() set
((Re ((a ^\ p) . R18)) / (K266((Re ((a ^\ p) . R18))) + K266((Im ((a ^\ p) . R18))))) + (((- (Im ((a ^\ p) . R18))) / (K266((Re ((a ^\ p) . R18))) + K266((Im ((a ^\ p) . R18))))) * K278()) is V22() set
((m /* (a ^\ p)) . R18) * (((a ^\ p) . R18) ") is V22() Element of COMPLEX
(((m /* (a ^\ p)) . R18) * (((a ^\ p) . R18) ")) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R18) is V22() Element of COMPLEX
m /. ((a ^\ p) . R18) is V22() Element of COMPLEX
m . ((a ^\ p) . R18) is V22() Element of COMPLEX
(m /. ((a ^\ p) . R18)) * (((a ^\ p) . R18) ") is V22() Element of COMPLEX
((m /. ((a ^\ p) . R18)) * (((a ^\ p) . R18) ")) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R18) is V22() Element of COMPLEX
y1 * ((a ^\ p) . R18) is V22() Element of COMPLEX
(y1 * ((a ^\ p) . R18)) * (((a ^\ p) . R18) ") is V22() Element of COMPLEX
((y1 * ((a ^\ p) . R18)) * (((a ^\ p) . R18) ")) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R18) is V22() Element of COMPLEX
((a ^\ p) . R18) * (((a ^\ p) . R18) ") is V22() Element of COMPLEX
y1 * (((a ^\ p) . R18) * (((a ^\ p) . R18) ")) is V22() Element of COMPLEX
(y1 * (((a ^\ p) . R18) * (((a ^\ p) . R18) "))) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R18) is V22() Element of COMPLEX
(y1 * 1r) + (((m /* (a ^\ p)) (#) ((a ^\ p) ")) . R18) is V22() Element of COMPLEX
n . R18 is V22() Element of COMPLEX
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
((a + s1) ^\ p) . n is V22() Element of COMPLEX
x0 /. (((a + s1) ^\ p) . n) is V22() Element of COMPLEX
(s1 ^\ p) . n is V22() Element of COMPLEX
x0 /. ((s1 ^\ p) . n) is V22() Element of COMPLEX
(x0 /. (((a + s1) ^\ p) . n)) - (x0 /. ((s1 ^\ p) . n)) is V22() Element of COMPLEX
- (x0 /. ((s1 ^\ p) . n)) is V22() set
(x0 /. (((a + s1) ^\ p) . n)) + (- (x0 /. ((s1 ^\ p) . n))) is V22() set
(a ^\ p) . n is V22() Element of COMPLEX
m /. ((a ^\ p) . n) is V22() Element of COMPLEX
m . ((a ^\ p) . n) is V22() Element of COMPLEX
m /. ((a ^\ p) . n) is V22() Element of COMPLEX
m . ((a ^\ p) . n) is V22() Element of COMPLEX
(m /. ((a ^\ p) . n)) + (m /. ((a ^\ p) . n)) is V22() Element of COMPLEX
(((a + s1) ^\ p) . n) - ((s1 ^\ p) . n) is V22() Element of COMPLEX
- ((s1 ^\ p) . n) is V22() set
(((a + s1) ^\ p) . n) + (- ((s1 ^\ p) . n)) is V22() set
n + p is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(a + s1) . (n + p) is V22() Element of COMPLEX
((a + s1) . (n + p)) - ((s1 ^\ p) . n) is V22() Element of COMPLEX
((a + s1) . (n + p)) + (- ((s1 ^\ p) . n)) is V22() set
a . (n + p) is V22() Element of COMPLEX
s1 . (n + p) is V22() Element of COMPLEX
(a . (n + p)) + (s1 . (n + p)) is V22() Element of COMPLEX
((a . (n + p)) + (s1 . (n + p))) - ((s1 ^\ p) . n) is V22() Element of COMPLEX
((a . (n + p)) + (s1 . (n + p))) + (- ((s1 ^\ p) . n)) is V22() set
((a ^\ p) . n) + (s1 . (n + p)) is V22() Element of COMPLEX
(((a ^\ p) . n) + (s1 . (n + p))) - ((s1 ^\ p) . n) is V22() Element of COMPLEX
(((a ^\ p) . n) + (s1 . (n + p))) + (- ((s1 ^\ p) . n)) is V22() set
((a ^\ p) . n) + ((s1 ^\ p) . n) is V22() Element of COMPLEX
(((a ^\ p) . n) + ((s1 ^\ p) . n)) - ((s1 ^\ p) . n) is V22() Element of COMPLEX
(((a ^\ p) . n) + ((s1 ^\ p) . n)) + (- ((s1 ^\ p) . n)) is V22() set
n is set
n is set
x0 /* ((a + s1) ^\ p) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
x0 /* (s1 ^\ p) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(x0 /* ((a + s1) ^\ p)) - (x0 /* (s1 ^\ p)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- (x0 /* (s1 ^\ p)) is V1() V4( NAT ) Function-like total complex-valued set
(- 1) (#) (x0 /* (s1 ^\ p)) is V1() V4( NAT ) Function-like total complex-valued set
(x0 /* ((a + s1) ^\ p)) + (- (x0 /* (s1 ^\ p))) is V1() V4( NAT ) Function-like total complex-valued set
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
((x0 /* ((a + s1) ^\ p)) - (x0 /* (s1 ^\ p))) . n is V22() Element of COMPLEX
(x0 /* ((a + s1) ^\ p)) . n is V22() Element of COMPLEX
(x0 /* (s1 ^\ p)) . n is V22() Element of COMPLEX
((x0 /* ((a + s1) ^\ p)) . n) - ((x0 /* (s1 ^\ p)) . n) is V22() Element of COMPLEX
- ((x0 /* (s1 ^\ p)) . n) is V22() set
((x0 /* ((a + s1) ^\ p)) . n) + (- ((x0 /* (s1 ^\ p)) . n)) is V22() set
((a + s1) ^\ p) . n is V22() Element of COMPLEX
x0 /. (((a + s1) ^\ p) . n) is V22() Element of COMPLEX
(x0 /. (((a + s1) ^\ p) . n)) - ((x0 /* (s1 ^\ p)) . n) is V22() Element of COMPLEX
(x0 /. (((a + s1) ^\ p) . n)) + (- ((x0 /* (s1 ^\ p)) . n)) is V22() set
(s1 ^\ p) . n is V22() Element of COMPLEX
x0 /. ((s1 ^\ p) . n) is V22() Element of COMPLEX
(x0 /. (((a + s1) ^\ p) . n)) - (x0 /. ((s1 ^\ p) . n)) is V22() Element of COMPLEX
- (x0 /. ((s1 ^\ p) . n)) is V22() set
(x0 /. (((a + s1) ^\ p) . n)) + (- (x0 /. ((s1 ^\ p) . n))) is V22() set
(a ^\ p) . n is V22() Element of COMPLEX
m /. ((a ^\ p) . n) is V22() Element of COMPLEX
m . ((a ^\ p) . n) is V22() Element of COMPLEX
m /. ((a ^\ p) . n) is V22() Element of COMPLEX
m . ((a ^\ p) . n) is V22() Element of COMPLEX
(m /. ((a ^\ p) . n)) + (m /. ((a ^\ p) . n)) is V22() Element of COMPLEX
(m /* (a ^\ p)) . n is V22() Element of COMPLEX
((m /* (a ^\ p)) . n) + (m /. ((a ^\ p) . n)) is V22() Element of COMPLEX
(m /* (a ^\ p)) . n is V22() Element of COMPLEX
((m /* (a ^\ p)) . n) + ((m /* (a ^\ p)) . n) is V22() Element of COMPLEX
((m /* (a ^\ p)) + (m /* (a ^\ p))) . n is V22() Element of COMPLEX
((x0 /* ((a + s1) ^\ p)) - (x0 /* (s1 ^\ p))) (#) ((a ^\ p) ") is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(x0 /* (a + s1)) ^\ p is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of x0 /* (a + s1)
((x0 /* (a + s1)) ^\ p) - (x0 /* (s1 ^\ p)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((x0 /* (a + s1)) ^\ p) + (- (x0 /* (s1 ^\ p))) is V1() V4( NAT ) Function-like total complex-valued set
(((x0 /* (a + s1)) ^\ p) - (x0 /* (s1 ^\ p))) (#) ((a ^\ p) ") is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(x0 /* s1) ^\ p is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of x0 /* s1
((x0 /* (a + s1)) ^\ p) - ((x0 /* s1) ^\ p) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- ((x0 /* s1) ^\ p) is V1() V4( NAT ) Function-like total complex-valued set
(- 1) (#) ((x0 /* s1) ^\ p) is V1() V4( NAT ) Function-like total complex-valued set
((x0 /* (a + s1)) ^\ p) + (- ((x0 /* s1) ^\ p)) is V1() V4( NAT ) Function-like total complex-valued set
(((x0 /* (a + s1)) ^\ p) - ((x0 /* s1) ^\ p)) (#) ((a ^\ p) ") is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((x0 /* (a + s1)) - (x0 /* s1)) ^\ p is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of (x0 /* (a + s1)) - (x0 /* s1)
(((x0 /* (a + s1)) - (x0 /* s1)) ^\ p) (#) ((a ^\ p) ") is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(a ") ^\ p is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of a "
(((x0 /* (a + s1)) - (x0 /* s1)) ^\ p) (#) ((a ") ^\ p) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((x0 /* (a + s1)) - (x0 /* s1)) (#) (a ") is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(((x0 /* (a + s1)) - (x0 /* s1)) (#) (a ")) ^\ p is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of ((x0 /* (a + s1)) - (x0 /* s1)) (#) (a ")
n is V22() Element of COMPLEX
x0 /. n is V22() Element of COMPLEX
(x0 /. n) - (x0 /. f) is V22() Element of COMPLEX
- (x0 /. f) is V22() set
(x0 /. n) + (- (x0 /. f)) is V22() set
n - f is V22() set
n + (- f) is V22() set
m /. (n - f) is V22() Element of COMPLEX
m /. (n - f) is V22() Element of COMPLEX
(m /. (n - f)) + (m /. (n - f)) is V22() Element of COMPLEX
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
x0 + f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
N is V22() Element of COMPLEX
((x0 + f),N) is V22() Element of COMPLEX
(x0,N) is V22() Element of COMPLEX
(f,N) is V22() Element of COMPLEX
(x0,N) + (f,N) is V22() Element of COMPLEX
dom x0 is V45() Element of K19(COMPLEX)
x0 /. N is V22() Element of COMPLEX
L is V45() (N)
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
a is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
a is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
dom f is V45() Element of K19(COMPLEX)
f /. N is V22() Element of COMPLEX
s1 is V45() (N)
M is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
p is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
M is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
p is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
a + p is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R + M is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
n is V45() (N)
n /\ n is V45() Element of K19(COMPLEX)
(dom x0) /\ (dom f) is V45() Element of K19(COMPLEX)
dom (x0 + f) is V45() Element of K19(COMPLEX)
y1 is V22() Element of COMPLEX
(x0 + f) /. y1 is V22() Element of COMPLEX
(x0 + f) /. N is V22() Element of COMPLEX
((x0 + f) /. y1) - ((x0 + f) /. N) is V22() Element of COMPLEX
- ((x0 + f) /. N) is V22() set
((x0 + f) /. y1) + (- ((x0 + f) /. N)) is V22() set
x0 /. y1 is V22() Element of COMPLEX
f /. y1 is V22() Element of COMPLEX
(x0 /. y1) + (f /. y1) is V22() Element of COMPLEX
((x0 /. y1) + (f /. y1)) - ((x0 + f) /. N) is V22() Element of COMPLEX
((x0 /. y1) + (f /. y1)) + (- ((x0 + f) /. N)) is V22() set
(x0 /. N) + (f /. N) is V22() Element of COMPLEX
((x0 /. y1) + (f /. y1)) - ((x0 /. N) + (f /. N)) is V22() Element of COMPLEX
- ((x0 /. N) + (f /. N)) is V22() set
((x0 /. y1) + (f /. y1)) + (- ((x0 /. N) + (f /. N))) is V22() set
(x0 /. y1) - (x0 /. N) is V22() Element of COMPLEX
- (x0 /. N) is V22() set
(x0 /. y1) + (- (x0 /. N)) is V22() set
(f /. y1) - (f /. N) is V22() Element of COMPLEX
- (f /. N) is V22() set
(f /. y1) + (- (f /. N)) is V22() set
((x0 /. y1) - (x0 /. N)) + ((f /. y1) - (f /. N)) is V22() Element of COMPLEX
y1 - N is V22() Element of COMPLEX
- N is V22() set
y1 + (- N) is V22() set
R /. (y1 - N) is V22() Element of COMPLEX
R . (y1 - N) is V22() Element of COMPLEX
a /. (y1 - N) is V22() Element of COMPLEX
a . (y1 - N) is V22() Element of COMPLEX
(R /. (y1 - N)) + (a /. (y1 - N)) is V22() Element of COMPLEX
((R /. (y1 - N)) + (a /. (y1 - N))) + ((f /. y1) - (f /. N)) is V22() Element of COMPLEX
M /. (y1 - N) is V22() Element of COMPLEX
M . (y1 - N) is V22() Element of COMPLEX
p /. (y1 - N) is V22() Element of COMPLEX
p . (y1 - N) is V22() Element of COMPLEX
(M /. (y1 - N)) + (p /. (y1 - N)) is V22() Element of COMPLEX
((R /. (y1 - N)) + (a /. (y1 - N))) + ((M /. (y1 - N)) + (p /. (y1 - N))) is V22() Element of COMPLEX
(R /. (y1 - N)) + (M /. (y1 - N)) is V22() Element of COMPLEX
(a /. (y1 - N)) + (p /. (y1 - N)) is V22() Element of COMPLEX
((R /. (y1 - N)) + (M /. (y1 - N))) + ((a /. (y1 - N)) + (p /. (y1 - N))) is V22() Element of COMPLEX
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m /. (y1 - N) is V22() Element of COMPLEX
m . (y1 - N) is V22() Element of COMPLEX
(m /. (y1 - N)) + ((a /. (y1 - N)) + (p /. (y1 - N))) is V22() Element of COMPLEX
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m /. (y1 - N) is V22() Element of COMPLEX
m . (y1 - N) is V22() Element of COMPLEX
(m /. (y1 - N)) + (m /. (y1 - N)) is V22() Element of COMPLEX
m /. 1r is V22() Element of COMPLEX
m . 1r is V22() Element of COMPLEX
R /. 1r is V22() Element of COMPLEX
R . 1r is V22() Element of COMPLEX
M /. 1r is V22() Element of COMPLEX
M . 1r is V22() Element of COMPLEX
(R /. 1r) + (M /. 1r) is V22() Element of COMPLEX
(x0,N) + (M /. 1r) is V22() Element of COMPLEX
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
x0 - f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
- f is V1() V4( COMPLEX ) Function-like complex-valued set
(- 1) (#) f is V1() V4( COMPLEX ) Function-like complex-valued set
x0 + (- f) is V1() V4( COMPLEX ) Function-like complex-valued set
N is V22() Element of COMPLEX
((x0 - f),N) is V22() Element of COMPLEX
(x0,N) is V22() Element of COMPLEX
(f,N) is V22() Element of COMPLEX
(x0,N) - (f,N) is V22() Element of COMPLEX
- (f,N) is V22() set
(x0,N) + (- (f,N)) is V22() set
dom x0 is V45() Element of K19(COMPLEX)
x0 /. N is V22() Element of COMPLEX
L is V45() (N)
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
a is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
a is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
dom f is V45() Element of K19(COMPLEX)
f /. N is V22() Element of COMPLEX
s1 is V45() (N)
M is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
p is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
M is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
p is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
a - p is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
- p is V1() V4( COMPLEX ) Function-like total complex-valued set
(- 1) (#) p is V1() V4( COMPLEX ) Function-like total complex-valued set
a + (- p) is V1() V4( COMPLEX ) Function-like total complex-valued set
R - M is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
- M is V1() V4( COMPLEX ) Function-like total complex-valued set
(- 1) (#) M is V1() V4( COMPLEX ) Function-like total complex-valued set
R + (- M) is V1() V4( COMPLEX ) Function-like total complex-valued set
n is V45() (N)
n /\ n is V45() Element of K19(COMPLEX)
(dom x0) /\ (dom f) is V45() Element of K19(COMPLEX)
dom (x0 - f) is V45() Element of K19(COMPLEX)
y1 is V22() Element of COMPLEX
(x0 - f) /. y1 is V22() Element of COMPLEX
(x0 - f) /. N is V22() Element of COMPLEX
((x0 - f) /. y1) - ((x0 - f) /. N) is V22() Element of COMPLEX
- ((x0 - f) /. N) is V22() set
((x0 - f) /. y1) + (- ((x0 - f) /. N)) is V22() set
x0 /. y1 is V22() Element of COMPLEX
f /. y1 is V22() Element of COMPLEX
(x0 /. y1) - (f /. y1) is V22() Element of COMPLEX
- (f /. y1) is V22() set
(x0 /. y1) + (- (f /. y1)) is V22() set
((x0 /. y1) - (f /. y1)) - ((x0 - f) /. N) is V22() Element of COMPLEX
((x0 /. y1) - (f /. y1)) + (- ((x0 - f) /. N)) is V22() set
(x0 /. N) - (f /. N) is V22() Element of COMPLEX
- (f /. N) is V22() set
(x0 /. N) + (- (f /. N)) is V22() set
((x0 /. y1) - (f /. y1)) - ((x0 /. N) - (f /. N)) is V22() Element of COMPLEX
- ((x0 /. N) - (f /. N)) is V22() set
((x0 /. y1) - (f /. y1)) + (- ((x0 /. N) - (f /. N))) is V22() set
(x0 /. y1) - (x0 /. N) is V22() Element of COMPLEX
- (x0 /. N) is V22() set
(x0 /. y1) + (- (x0 /. N)) is V22() set
(f /. y1) - (f /. N) is V22() Element of COMPLEX
(f /. y1) + (- (f /. N)) is V22() set
((x0 /. y1) - (x0 /. N)) - ((f /. y1) - (f /. N)) is V22() Element of COMPLEX
- ((f /. y1) - (f /. N)) is V22() set
((x0 /. y1) - (x0 /. N)) + (- ((f /. y1) - (f /. N))) is V22() set
y1 - N is V22() Element of COMPLEX
- N is V22() set
y1 + (- N) is V22() set
R /. (y1 - N) is V22() Element of COMPLEX
R . (y1 - N) is V22() Element of COMPLEX
a /. (y1 - N) is V22() Element of COMPLEX
a . (y1 - N) is V22() Element of COMPLEX
(R /. (y1 - N)) + (a /. (y1 - N)) is V22() Element of COMPLEX
((R /. (y1 - N)) + (a /. (y1 - N))) - ((f /. y1) - (f /. N)) is V22() Element of COMPLEX
((R /. (y1 - N)) + (a /. (y1 - N))) + (- ((f /. y1) - (f /. N))) is V22() set
M /. (y1 - N) is V22() Element of COMPLEX
M . (y1 - N) is V22() Element of COMPLEX
p /. (y1 - N) is V22() Element of COMPLEX
p . (y1 - N) is V22() Element of COMPLEX
(M /. (y1 - N)) + (p /. (y1 - N)) is V22() Element of COMPLEX
((R /. (y1 - N)) + (a /. (y1 - N))) - ((M /. (y1 - N)) + (p /. (y1 - N))) is V22() Element of COMPLEX
- ((M /. (y1 - N)) + (p /. (y1 - N))) is V22() set
((R /. (y1 - N)) + (a /. (y1 - N))) + (- ((M /. (y1 - N)) + (p /. (y1 - N)))) is V22() set
(R /. (y1 - N)) - (M /. (y1 - N)) is V22() Element of COMPLEX
- (M /. (y1 - N)) is V22() set
(R /. (y1 - N)) + (- (M /. (y1 - N))) is V22() set
(a /. (y1 - N)) - (p /. (y1 - N)) is V22() Element of COMPLEX
- (p /. (y1 - N)) is V22() set
(a /. (y1 - N)) + (- (p /. (y1 - N))) is V22() set
((R /. (y1 - N)) - (M /. (y1 - N))) + ((a /. (y1 - N)) - (p /. (y1 - N))) is V22() Element of COMPLEX
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m /. (y1 - N) is V22() Element of COMPLEX
m . (y1 - N) is V22() Element of COMPLEX
(m /. (y1 - N)) + ((a /. (y1 - N)) - (p /. (y1 - N))) is V22() Element of COMPLEX
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m /. (y1 - N) is V22() Element of COMPLEX
m . (y1 - N) is V22() Element of COMPLEX
(m /. (y1 - N)) + (m /. (y1 - N)) is V22() Element of COMPLEX
m /. 1r is V22() Element of COMPLEX
m . 1r is V22() Element of COMPLEX
R /. 1r is V22() Element of COMPLEX
R . 1r is V22() Element of COMPLEX
M /. 1r is V22() Element of COMPLEX
M . 1r is V22() Element of COMPLEX
(R /. 1r) - (M /. 1r) is V22() Element of COMPLEX
- (M /. 1r) is V22() set
(R /. 1r) + (- (M /. 1r)) is V22() set
(x0,N) - (M /. 1r) is V22() Element of COMPLEX
(x0,N) + (- (M /. 1r)) is V22() set
x0 is V22() Element of COMPLEX
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
x0 (#) f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
N is V22() Element of COMPLEX
((x0 (#) f),N) is V22() Element of COMPLEX
(f,N) is V22() Element of COMPLEX
x0 * (f,N) is V22() Element of COMPLEX
dom f is V45() Element of K19(COMPLEX)
f /. N is V22() Element of COMPLEX
L is V45() (N)
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
a is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
a is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
x0 (#) a is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
x0 (#) R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
dom (x0 (#) f) is V45() Element of K19(COMPLEX)
p is V22() Element of COMPLEX
(x0 (#) f) /. p is V22() Element of COMPLEX
(x0 (#) f) /. N is V22() Element of COMPLEX
((x0 (#) f) /. p) - ((x0 (#) f) /. N) is V22() Element of COMPLEX
- ((x0 (#) f) /. N) is V22() set
((x0 (#) f) /. p) + (- ((x0 (#) f) /. N)) is V22() set
f /. p is V22() Element of COMPLEX
x0 * (f /. p) is V22() Element of COMPLEX
(x0 * (f /. p)) - ((x0 (#) f) /. N) is V22() Element of COMPLEX
(x0 * (f /. p)) + (- ((x0 (#) f) /. N)) is V22() set
x0 * (f /. N) is V22() Element of COMPLEX
(x0 * (f /. p)) - (x0 * (f /. N)) is V22() Element of COMPLEX
- (x0 * (f /. N)) is V22() set
(x0 * (f /. p)) + (- (x0 * (f /. N))) is V22() set
(f /. p) - (f /. N) is V22() Element of COMPLEX
- (f /. N) is V22() set
(f /. p) + (- (f /. N)) is V22() set
x0 * ((f /. p) - (f /. N)) is V22() Element of COMPLEX
p - N is V22() Element of COMPLEX
- N is V22() set
p + (- N) is V22() set
R /. (p - N) is V22() Element of COMPLEX
R . (p - N) is V22() Element of COMPLEX
a /. (p - N) is V22() Element of COMPLEX
a . (p - N) is V22() Element of COMPLEX
(R /. (p - N)) + (a /. (p - N)) is V22() Element of COMPLEX
x0 * ((R /. (p - N)) + (a /. (p - N))) is V22() Element of COMPLEX
x0 * (R /. (p - N)) is V22() Element of COMPLEX
x0 * (a /. (p - N)) is V22() Element of COMPLEX
(x0 * (R /. (p - N))) + (x0 * (a /. (p - N))) is V22() Element of COMPLEX
M is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
M /. (p - N) is V22() Element of COMPLEX
M . (p - N) is V22() Element of COMPLEX
(M /. (p - N)) + (x0 * (a /. (p - N))) is V22() Element of COMPLEX
s1 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
s1 /. (p - N) is V22() Element of COMPLEX
s1 . (p - N) is V22() Element of COMPLEX
(M /. (p - N)) + (s1 /. (p - N)) is V22() Element of COMPLEX
M /. 1r is V22() Element of COMPLEX
M . 1r is V22() Element of COMPLEX
R /. 1r is V22() Element of COMPLEX
R . 1r is V22() Element of COMPLEX
x0 * (R /. 1r) is V22() Element of COMPLEX
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
x0 (#) f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
N is V22() Element of COMPLEX
((x0 (#) f),N) is V22() Element of COMPLEX
f /. N is V22() Element of COMPLEX
(x0,N) is V22() Element of COMPLEX
(f /. N) * (x0,N) is V22() Element of COMPLEX
x0 /. N is V22() Element of COMPLEX
(f,N) is V22() Element of COMPLEX
(x0 /. N) * (f,N) is V22() Element of COMPLEX
((f /. N) * (x0,N)) + ((x0 /. N) * (f,N)) is V22() Element of COMPLEX
dom f is V45() Element of K19(COMPLEX)
L is V45() (N)
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
a is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
a is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
(x0 /. N) (#) a is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
(x0 /. N) (#) R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
dom x0 is V45() Element of K19(COMPLEX)
p is V45() (N)
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
(f /. N) (#) m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
(f /. N) (#) m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
a (#) m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m (#) a is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m (#) R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m (#) R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
n is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
s1 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
n + s1 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
y1 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
M is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
y1 + M is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R13 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R14 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R13 + R14 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R16 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R17 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R16 + R17 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R19 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R18 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R19 + R18 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R15 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R20 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R15 + R20 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
N is V45() (N)
N /\ N is V45() Element of K19(COMPLEX)
(dom x0) /\ (dom f) is V45() Element of K19(COMPLEX)
dom (x0 (#) f) is V45() Element of K19(COMPLEX)
x is V22() Element of COMPLEX
x0 /. x is V22() Element of COMPLEX
(x0 /. x) - (x0 /. N) is V22() Element of COMPLEX
- (x0 /. N) is V22() set
(x0 /. x) + (- (x0 /. N)) is V22() set
((x0 /. x) - (x0 /. N)) + (x0 /. N) is V22() Element of COMPLEX
x - N is V22() Element of COMPLEX
- N is V22() set
x + (- N) is V22() set
m /. (x - N) is V22() Element of COMPLEX
m . (x - N) is V22() Element of COMPLEX
m /. (x - N) is V22() Element of COMPLEX
m . (x - N) is V22() Element of COMPLEX
(m /. (x - N)) + (m /. (x - N)) is V22() Element of COMPLEX
((m /. (x - N)) + (m /. (x - N))) + (x0 /. N) is V22() Element of COMPLEX
(x0 (#) f) /. x is V22() Element of COMPLEX
(x0 (#) f) /. N is V22() Element of COMPLEX
((x0 (#) f) /. x) - ((x0 (#) f) /. N) is V22() Element of COMPLEX
- ((x0 (#) f) /. N) is V22() set
((x0 (#) f) /. x) + (- ((x0 (#) f) /. N)) is V22() set
f /. x is V22() Element of COMPLEX
(x0 /. x) * (f /. x) is V22() Element of COMPLEX
((x0 /. x) * (f /. x)) - ((x0 (#) f) /. N) is V22() Element of COMPLEX
((x0 /. x) * (f /. x)) + (- ((x0 (#) f) /. N)) is V22() set
(x0 /. x) * (f /. N) is V22() Element of COMPLEX
- ((x0 /. x) * (f /. N)) is V22() Element of COMPLEX
((x0 /. x) * (f /. x)) + (- ((x0 /. x) * (f /. N))) is V22() Element of COMPLEX
(((x0 /. x) * (f /. x)) + (- ((x0 /. x) * (f /. N)))) + ((x0 /. x) * (f /. N)) is V22() Element of COMPLEX
(x0 /. N) * (f /. N) is V22() Element of COMPLEX
((((x0 /. x) * (f /. x)) + (- ((x0 /. x) * (f /. N)))) + ((x0 /. x) * (f /. N))) - ((x0 /. N) * (f /. N)) is V22() Element of COMPLEX
- ((x0 /. N) * (f /. N)) is V22() set
((((x0 /. x) * (f /. x)) + (- ((x0 /. x) * (f /. N)))) + ((x0 /. x) * (f /. N))) + (- ((x0 /. N) * (f /. N))) is V22() set
(f /. x) - (f /. N) is V22() Element of COMPLEX
- (f /. N) is V22() set
(f /. x) + (- (f /. N)) is V22() set
(x0 /. x) * ((f /. x) - (f /. N)) is V22() Element of COMPLEX
((x0 /. x) - (x0 /. N)) * (f /. N) is V22() Element of COMPLEX
((x0 /. x) * ((f /. x) - (f /. N))) + (((x0 /. x) - (x0 /. N)) * (f /. N)) is V22() Element of COMPLEX
((m /. (x - N)) + (m /. (x - N))) * (f /. N) is V22() Element of COMPLEX
((x0 /. x) * ((f /. x) - (f /. N))) + (((m /. (x - N)) + (m /. (x - N))) * (f /. N)) is V22() Element of COMPLEX
(f /. N) * (m /. (x - N)) is V22() Element of COMPLEX
(m /. (x - N)) * (f /. N) is V22() Element of COMPLEX
((f /. N) * (m /. (x - N))) + ((m /. (x - N)) * (f /. N)) is V22() Element of COMPLEX
((x0 /. x) * ((f /. x) - (f /. N))) + (((f /. N) * (m /. (x - N))) + ((m /. (x - N)) * (f /. N))) is V22() Element of COMPLEX
y1 /. (x - N) is V22() Element of COMPLEX
y1 . (x - N) is V22() Element of COMPLEX
(f /. N) * (m /. (x - N)) is V22() Element of COMPLEX
(y1 /. (x - N)) + ((f /. N) * (m /. (x - N))) is V22() Element of COMPLEX
((x0 /. x) * ((f /. x) - (f /. N))) + ((y1 /. (x - N)) + ((f /. N) * (m /. (x - N)))) is V22() Element of COMPLEX
(((m /. (x - N)) + (m /. (x - N))) + (x0 /. N)) * ((f /. x) - (f /. N)) is V22() Element of COMPLEX
n /. (x - N) is V22() Element of COMPLEX
n . (x - N) is V22() Element of COMPLEX
(y1 /. (x - N)) + (n /. (x - N)) is V22() Element of COMPLEX
((((m /. (x - N)) + (m /. (x - N))) + (x0 /. N)) * ((f /. x) - (f /. N))) + ((y1 /. (x - N)) + (n /. (x - N))) is V22() Element of COMPLEX
R /. (x - N) is V22() Element of COMPLEX
R . (x - N) is V22() Element of COMPLEX
a /. (x - N) is V22() Element of COMPLEX
a . (x - N) is V22() Element of COMPLEX
(R /. (x - N)) + (a /. (x - N)) is V22() Element of COMPLEX
(((m /. (x - N)) + (m /. (x - N))) + (x0 /. N)) * ((R /. (x - N)) + (a /. (x - N))) is V22() Element of COMPLEX
((((m /. (x - N)) + (m /. (x - N))) + (x0 /. N)) * ((R /. (x - N)) + (a /. (x - N)))) + ((y1 /. (x - N)) + (n /. (x - N))) is V22() Element of COMPLEX
((m /. (x - N)) + (m /. (x - N))) * ((R /. (x - N)) + (a /. (x - N))) is V22() Element of COMPLEX
(x0 /. N) * (R /. (x - N)) is V22() Element of COMPLEX
(x0 /. N) * (a /. (x - N)) is V22() Element of COMPLEX
((x0 /. N) * (R /. (x - N))) + ((x0 /. N) * (a /. (x - N))) is V22() Element of COMPLEX
(((m /. (x - N)) + (m /. (x - N))) * ((R /. (x - N)) + (a /. (x - N)))) + (((x0 /. N) * (R /. (x - N))) + ((x0 /. N) * (a /. (x - N)))) is V22() Element of COMPLEX
((((m /. (x - N)) + (m /. (x - N))) * ((R /. (x - N)) + (a /. (x - N)))) + (((x0 /. N) * (R /. (x - N))) + ((x0 /. N) * (a /. (x - N))))) + ((y1 /. (x - N)) + (n /. (x - N))) is V22() Element of COMPLEX
M /. (x - N) is V22() Element of COMPLEX
M . (x - N) is V22() Element of COMPLEX
(M /. (x - N)) + ((x0 /. N) * (a /. (x - N))) is V22() Element of COMPLEX
(((m /. (x - N)) + (m /. (x - N))) * ((R /. (x - N)) + (a /. (x - N)))) + ((M /. (x - N)) + ((x0 /. N) * (a /. (x - N)))) is V22() Element of COMPLEX
((((m /. (x - N)) + (m /. (x - N))) * ((R /. (x - N)) + (a /. (x - N)))) + ((M /. (x - N)) + ((x0 /. N) * (a /. (x - N))))) + ((y1 /. (x - N)) + (n /. (x - N))) is V22() Element of COMPLEX
s1 /. (x - N) is V22() Element of COMPLEX
s1 . (x - N) is V22() Element of COMPLEX
(M /. (x - N)) + (s1 /. (x - N)) is V22() Element of COMPLEX
(((m /. (x - N)) + (m /. (x - N))) * ((R /. (x - N)) + (a /. (x - N)))) + ((M /. (x - N)) + (s1 /. (x - N))) is V22() Element of COMPLEX
((((m /. (x - N)) + (m /. (x - N))) * ((R /. (x - N)) + (a /. (x - N)))) + ((M /. (x - N)) + (s1 /. (x - N)))) + ((y1 /. (x - N)) + (n /. (x - N))) is V22() Element of COMPLEX
(n /. (x - N)) + (s1 /. (x - N)) is V22() Element of COMPLEX
(y1 /. (x - N)) + ((n /. (x - N)) + (s1 /. (x - N))) is V22() Element of COMPLEX
(M /. (x - N)) + ((y1 /. (x - N)) + ((n /. (x - N)) + (s1 /. (x - N)))) is V22() Element of COMPLEX
(((m /. (x - N)) + (m /. (x - N))) * ((R /. (x - N)) + (a /. (x - N)))) + ((M /. (x - N)) + ((y1 /. (x - N)) + ((n /. (x - N)) + (s1 /. (x - N))))) is V22() Element of COMPLEX
R13 /. (x - N) is V22() Element of COMPLEX
R13 . (x - N) is V22() Element of COMPLEX
(y1 /. (x - N)) + (R13 /. (x - N)) is V22() Element of COMPLEX
(M /. (x - N)) + ((y1 /. (x - N)) + (R13 /. (x - N))) is V22() Element of COMPLEX
(((m /. (x - N)) + (m /. (x - N))) * ((R /. (x - N)) + (a /. (x - N)))) + ((M /. (x - N)) + ((y1 /. (x - N)) + (R13 /. (x - N)))) is V22() Element of COMPLEX
(y1 /. (x - N)) + (M /. (x - N)) is V22() Element of COMPLEX
((y1 /. (x - N)) + (M /. (x - N))) + (R13 /. (x - N)) is V22() Element of COMPLEX
(((m /. (x - N)) + (m /. (x - N))) * ((R /. (x - N)) + (a /. (x - N)))) + (((y1 /. (x - N)) + (M /. (x - N))) + (R13 /. (x - N))) is V22() Element of COMPLEX
(m /. (x - N)) * (R /. (x - N)) is V22() Element of COMPLEX
(m /. (x - N)) * (a /. (x - N)) is V22() Element of COMPLEX
((m /. (x - N)) * (R /. (x - N))) + ((m /. (x - N)) * (a /. (x - N))) is V22() Element of COMPLEX
(m /. (x - N)) * ((R /. (x - N)) + (a /. (x - N))) is V22() Element of COMPLEX
(((m /. (x - N)) * (R /. (x - N))) + ((m /. (x - N)) * (a /. (x - N)))) + ((m /. (x - N)) * ((R /. (x - N)) + (a /. (x - N)))) is V22() Element of COMPLEX
L is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
L /. (x - N) is V22() Element of COMPLEX
L . (x - N) is V22() Element of COMPLEX
(L /. (x - N)) + (R13 /. (x - N)) is V22() Element of COMPLEX
((((m /. (x - N)) * (R /. (x - N))) + ((m /. (x - N)) * (a /. (x - N)))) + ((m /. (x - N)) * ((R /. (x - N)) + (a /. (x - N))))) + ((L /. (x - N)) + (R13 /. (x - N))) is V22() Element of COMPLEX
R14 /. (x - N) is V22() Element of COMPLEX
R14 . (x - N) is V22() Element of COMPLEX
(a /. (x - N)) * (m /. (x - N)) is V22() Element of COMPLEX
(R14 /. (x - N)) + ((a /. (x - N)) * (m /. (x - N))) is V22() Element of COMPLEX
((R14 /. (x - N)) + ((a /. (x - N)) * (m /. (x - N)))) + ((m /. (x - N)) * ((R /. (x - N)) + (a /. (x - N)))) is V22() Element of COMPLEX
(((R14 /. (x - N)) + ((a /. (x - N)) * (m /. (x - N)))) + ((m /. (x - N)) * ((R /. (x - N)) + (a /. (x - N))))) + ((L /. (x - N)) + (R13 /. (x - N))) is V22() Element of COMPLEX
R18 /. (x - N) is V22() Element of COMPLEX
R18 . (x - N) is V22() Element of COMPLEX
(R14 /. (x - N)) + (R18 /. (x - N)) is V22() Element of COMPLEX
(m /. (x - N)) * (R /. (x - N)) is V22() Element of COMPLEX
(m /. (x - N)) * (a /. (x - N)) is V22() Element of COMPLEX
((m /. (x - N)) * (R /. (x - N))) + ((m /. (x - N)) * (a /. (x - N))) is V22() Element of COMPLEX
((R14 /. (x - N)) + (R18 /. (x - N))) + (((m /. (x - N)) * (R /. (x - N))) + ((m /. (x - N)) * (a /. (x - N)))) is V22() Element of COMPLEX
(((R14 /. (x - N)) + (R18 /. (x - N))) + (((m /. (x - N)) * (R /. (x - N))) + ((m /. (x - N)) * (a /. (x - N))))) + ((L /. (x - N)) + (R13 /. (x - N))) is V22() Element of COMPLEX
R16 /. (x - N) is V22() Element of COMPLEX
R16 . (x - N) is V22() Element of COMPLEX
(R16 /. (x - N)) + ((m /. (x - N)) * (a /. (x - N))) is V22() Element of COMPLEX
((R14 /. (x - N)) + (R18 /. (x - N))) + ((R16 /. (x - N)) + ((m /. (x - N)) * (a /. (x - N)))) is V22() Element of COMPLEX
(((R14 /. (x - N)) + (R18 /. (x - N))) + ((R16 /. (x - N)) + ((m /. (x - N)) * (a /. (x - N))))) + ((L /. (x - N)) + (R13 /. (x - N))) is V22() Element of COMPLEX
R17 /. (x - N) is V22() Element of COMPLEX
R17 . (x - N) is V22() Element of COMPLEX
(R16 /. (x - N)) + (R17 /. (x - N)) is V22() Element of COMPLEX
((R14 /. (x - N)) + (R18 /. (x - N))) + ((R16 /. (x - N)) + (R17 /. (x - N))) is V22() Element of COMPLEX
(((R14 /. (x - N)) + (R18 /. (x - N))) + ((R16 /. (x - N)) + (R17 /. (x - N)))) + ((L /. (x - N)) + (R13 /. (x - N))) is V22() Element of COMPLEX
R19 /. (x - N) is V22() Element of COMPLEX
R19 . (x - N) is V22() Element of COMPLEX
((R14 /. (x - N)) + (R18 /. (x - N))) + (R19 /. (x - N)) is V22() Element of COMPLEX
(((R14 /. (x - N)) + (R18 /. (x - N))) + (R19 /. (x - N))) + ((L /. (x - N)) + (R13 /. (x - N))) is V22() Element of COMPLEX
(R19 /. (x - N)) + (R18 /. (x - N)) is V22() Element of COMPLEX
(R14 /. (x - N)) + ((R19 /. (x - N)) + (R18 /. (x - N))) is V22() Element of COMPLEX
((R14 /. (x - N)) + ((R19 /. (x - N)) + (R18 /. (x - N)))) + ((L /. (x - N)) + (R13 /. (x - N))) is V22() Element of COMPLEX
R20 /. (x - N) is V22() Element of COMPLEX
R20 . (x - N) is V22() Element of COMPLEX
(R14 /. (x - N)) + (R20 /. (x - N)) is V22() Element of COMPLEX
((L /. (x - N)) + (R13 /. (x - N))) + ((R14 /. (x - N)) + (R20 /. (x - N))) is V22() Element of COMPLEX
(R13 /. (x - N)) + (R14 /. (x - N)) is V22() Element of COMPLEX
((R13 /. (x - N)) + (R14 /. (x - N))) + (R20 /. (x - N)) is V22() Element of COMPLEX
(L /. (x - N)) + (((R13 /. (x - N)) + (R14 /. (x - N))) + (R20 /. (x - N))) is V22() Element of COMPLEX
R15 /. (x - N) is V22() Element of COMPLEX
R15 . (x - N) is V22() Element of COMPLEX
(R15 /. (x - N)) + (R20 /. (x - N)) is V22() Element of COMPLEX
(L /. (x - N)) + ((R15 /. (x - N)) + (R20 /. (x - N))) is V22() Element of COMPLEX
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R /. (x - N) is V22() Element of COMPLEX
R . (x - N) is V22() Element of COMPLEX
(L /. (x - N)) + (R /. (x - N)) is V22() Element of COMPLEX
L /. 1r is V22() Element of COMPLEX
L . 1r is V22() Element of COMPLEX
y1 /. 1r is V22() Element of COMPLEX
y1 . 1r is V22() Element of COMPLEX
M /. 1r is V22() Element of COMPLEX
M . 1r is V22() Element of COMPLEX
(y1 /. 1r) + (M /. 1r) is V22() Element of COMPLEX
m /. 1r is V22() Element of COMPLEX
m . 1r is V22() Element of COMPLEX
(f /. N) * (m /. 1r) is V22() Element of COMPLEX
((f /. N) * (m /. 1r)) + (M /. 1r) is V22() Element of COMPLEX
R /. 1r is V22() Element of COMPLEX
R . 1r is V22() Element of COMPLEX
(x0 /. N) * (R /. 1r) is V22() Element of COMPLEX
((f /. N) * (m /. 1r)) + ((x0 /. N) * (R /. 1r)) is V22() Element of COMPLEX
((f /. N) * (x0,N)) + ((x0 /. N) * (R /. 1r)) is V22() Element of COMPLEX
cf is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
id COMPLEX is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like one-to-one V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
N is V22() Element of COMPLEX
f /. N is V22() Element of COMPLEX
1r * N is V22() Element of COMPLEX
dom cf is V45() Element of K19(COMPLEX)
R is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
L is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
rng L is V45() Element of K19(COMPLEX)
L " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
cf /* L is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(L ") (#) (cf /* L) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((L ") (#) (cf /* L)) . R is V22() Element of COMPLEX
(L ") . R is V22() Element of COMPLEX
(cf /* L) . R is V22() Element of COMPLEX
((L ") . R) * ((cf /* L) . R) is V22() Element of COMPLEX
L . R is V22() Element of COMPLEX
cf /. (L . R) is V22() Element of COMPLEX
cf . (L . R) is V22() Element of COMPLEX
((L ") . R) * (cf /. (L . R)) is V22() Element of COMPLEX
((L ") . R) * 0c is V22() Element of COMPLEX
((L ") (#) (cf /* L)) . 0 is V22() Element of COMPLEX
lim ((L ") (#) (cf /* L)) is V22() Element of COMPLEX
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom R is V45() Element of K19(COMPLEX)
a is V45() () Element of K19(COMPLEX)
R | a is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
id a is V1() V4(a) V5(a) Function-like one-to-one total quasi_total complex-valued Element of K19(K20(a,a))
K20(a,a) is complex-valued set
K19(K20(a,a)) is set
(R,a) is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
s1 is V22() set
(R | a) . s1 is V22() set
R . s1 is V22() set
R /. s1 is V22() Element of COMPLEX
s1 is V22() Element of COMPLEX
M is V45() (s1)
R /. s1 is V22() Element of COMPLEX
N is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
L is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
p is V22() Element of COMPLEX
R /. p is V22() Element of COMPLEX
(R /. p) - (R /. s1) is V22() Element of COMPLEX
- (R /. s1) is V22() set
(R /. p) + (- (R /. s1)) is V22() set
p - s1 is V22() Element of COMPLEX
- s1 is V22() set
p + (- s1) is V22() set
N /. (p - s1) is V22() Element of COMPLEX
N . (p - s1) is V22() Element of COMPLEX
L /. (p - s1) is V22() Element of COMPLEX
L . (p - s1) is V22() Element of COMPLEX
(N /. (p - s1)) + (L /. (p - s1)) is V22() Element of COMPLEX
p - (R /. s1) is V22() Element of COMPLEX
p + (- (R /. s1)) is V22() set
(N /. (p - s1)) + 0c is V22() Element of COMPLEX
s1 is V22() Element of COMPLEX
(R,a) /. s1 is V22() Element of COMPLEX
M is V45() (s1)
R /. s1 is V22() Element of COMPLEX
p is V45() (s1)
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
p is V45() (s1)
m is V45() (s1)
m is V22() Element of COMPLEX
R /. m is V22() Element of COMPLEX
(R /. m) - (R /. s1) is V22() Element of COMPLEX
- (R /. s1) is V22() set
(R /. m) + (- (R /. s1)) is V22() set
m - s1 is V22() Element of COMPLEX
- s1 is V22() set
m + (- s1) is V22() set
N /. (m - s1) is V22() Element of COMPLEX
N . (m - s1) is V22() Element of COMPLEX
L /. (m - s1) is V22() Element of COMPLEX
L . (m - s1) is V22() Element of COMPLEX
(N /. (m - s1)) + (L /. (m - s1)) is V22() Element of COMPLEX
m - (R /. s1) is V22() Element of COMPLEX
m + (- (R /. s1)) is V22() set
(N /. (m - s1)) + 0c is V22() Element of COMPLEX
(R,s1) is V22() Element of COMPLEX
N /. 1r is V22() Element of COMPLEX
N . 1r is V22() Element of COMPLEX
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
x0 + f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom (x0 + f) is V45() Element of K19(COMPLEX)
N is V45() () Element of K19(COMPLEX)
((x0 + f),N) is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
L is V22() Element of COMPLEX
L is V22() Element of COMPLEX
((x0 + f),N) /. L is V22() Element of COMPLEX
((x0 + f),L) is V22() Element of COMPLEX
(x0,L) is V22() Element of COMPLEX
(f,L) is V22() Element of COMPLEX
(x0,L) + (f,L) is V22() Element of COMPLEX
L is V22() Element of COMPLEX
((x0 + f),N) /. L is V22() Element of COMPLEX
(x0,L) is V22() Element of COMPLEX
(f,L) is V22() Element of COMPLEX
(x0,L) + (f,L) is V22() Element of COMPLEX
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
x0 - f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
- f is V1() V4( COMPLEX ) Function-like complex-valued set
(- 1) (#) f is V1() V4( COMPLEX ) Function-like complex-valued set
x0 + (- f) is V1() V4( COMPLEX ) Function-like complex-valued set
dom (x0 - f) is V45() Element of K19(COMPLEX)
N is V45() () Element of K19(COMPLEX)
((x0 - f),N) is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
L is V22() Element of COMPLEX
L is V22() Element of COMPLEX
((x0 - f),N) /. L is V22() Element of COMPLEX
((x0 - f),L) is V22() Element of COMPLEX
(x0,L) is V22() Element of COMPLEX
(f,L) is V22() Element of COMPLEX
(x0,L) - (f,L) is V22() Element of COMPLEX
- (f,L) is V22() set
(x0,L) + (- (f,L)) is V22() set
L is V22() Element of COMPLEX
((x0 - f),N) /. L is V22() Element of COMPLEX
(x0,L) is V22() Element of COMPLEX
(f,L) is V22() Element of COMPLEX
(x0,L) - (f,L) is V22() Element of COMPLEX
- (f,L) is V22() set
(x0,L) + (- (f,L)) is V22() set
x0 is V22() Element of COMPLEX
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
x0 (#) f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom (x0 (#) f) is V45() Element of K19(COMPLEX)
N is V45() () Element of K19(COMPLEX)
((x0 (#) f),N) is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
L is V22() Element of COMPLEX
L is V22() Element of COMPLEX
((x0 (#) f),N) /. L is V22() Element of COMPLEX
((x0 (#) f),L) is V22() Element of COMPLEX
(f,L) is V22() Element of COMPLEX
x0 * (f,L) is V22() Element of COMPLEX
L is V22() Element of COMPLEX
((x0 (#) f),N) /. L is V22() Element of COMPLEX
(f,L) is V22() Element of COMPLEX
x0 * (f,L) is V22() Element of COMPLEX
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
x0 (#) f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom (x0 (#) f) is V45() Element of K19(COMPLEX)
N is V45() () Element of K19(COMPLEX)
((x0 (#) f),N) is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
L is V22() Element of COMPLEX
L is V22() Element of COMPLEX
((x0 (#) f),N) /. L is V22() Element of COMPLEX
((x0 (#) f),L) is V22() Element of COMPLEX
f /. L is V22() Element of COMPLEX
(x0,L) is V22() Element of COMPLEX
(f /. L) * (x0,L) is V22() Element of COMPLEX
x0 /. L is V22() Element of COMPLEX
(f,L) is V22() Element of COMPLEX
(x0 /. L) * (f,L) is V22() Element of COMPLEX
((f /. L) * (x0,L)) + ((x0 /. L) * (f,L)) is V22() Element of COMPLEX
L is V22() Element of COMPLEX
((x0 (#) f),N) /. L is V22() Element of COMPLEX
f /. L is V22() Element of COMPLEX
(x0,L) is V22() Element of COMPLEX
(f /. L) * (x0,L) is V22() Element of COMPLEX
x0 /. L is V22() Element of COMPLEX
(f,L) is V22() Element of COMPLEX
(x0 /. L) * (f,L) is V22() Element of COMPLEX
((f /. L) * (x0,L)) + ((x0 /. L) * (f,L)) is V22() Element of COMPLEX
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom x0 is V45() Element of K19(COMPLEX)
f is V45() () Element of K19(COMPLEX)
x0 | f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
(x0,f) is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
cf is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom cf is V45() Element of K19(COMPLEX)
R is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
L is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
rng L is V45() Element of K19(COMPLEX)
L " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
cf /* L is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(L ") (#) (cf /* L) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((L ") (#) (cf /* L)) . R is V22() Element of COMPLEX
(L ") . R is V22() Element of COMPLEX
(cf /* L) . R is V22() Element of COMPLEX
((L ") . R) * ((cf /* L) . R) is V22() Element of COMPLEX
L . R is V22() Element of COMPLEX
cf /. (L . R) is V22() Element of COMPLEX
cf . (L . R) is V22() Element of COMPLEX
((L ") . R) * (cf /. (L . R)) is V22() Element of COMPLEX
((L ") . R) * 0c is V22() Element of COMPLEX
((L ") (#) (cf /* L)) . 0 is V22() Element of COMPLEX
lim ((L ") (#) (cf /* L)) is V22() Element of COMPLEX
a is V22() Element of COMPLEX
cf /. a is V22() Element of COMPLEX
cf . a is V22() Element of COMPLEX
0c * a is V22() Element of COMPLEX
f /\ (dom x0) is V45() Element of K19(COMPLEX)
s1 is V22() Element of COMPLEX
M is V22() Element of COMPLEX
p is V45() (M)
x0 /. M is V22() Element of COMPLEX
a is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
L is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m is V22() Element of COMPLEX
x0 /. m is V22() Element of COMPLEX
(x0 /. m) - (x0 /. M) is V22() Element of COMPLEX
- (x0 /. M) is V22() set
(x0 /. m) + (- (x0 /. M)) is V22() set
m - M is V22() Element of COMPLEX
- M is V22() set
m + (- M) is V22() set
a /. (m - M) is V22() Element of COMPLEX
a . (m - M) is V22() Element of COMPLEX
L /. (m - M) is V22() Element of COMPLEX
L . (m - M) is V22() Element of COMPLEX
(a /. (m - M)) + (L /. (m - M)) is V22() Element of COMPLEX
s1 - (x0 /. M) is V22() Element of COMPLEX
s1 + (- (x0 /. M)) is V22() set
s1 - s1 is V22() Element of COMPLEX
- s1 is V22() set
s1 + (- s1) is V22() set
(a /. (m - M)) + 0c is V22() Element of COMPLEX
M is V22() Element of COMPLEX
(x0,f) /. M is V22() Element of COMPLEX
p is V45() (M)
x0 /. M is V22() Element of COMPLEX
m is V22() Element of COMPLEX
x0 /. m is V22() Element of COMPLEX
(x0 /. m) - (x0 /. M) is V22() Element of COMPLEX
- (x0 /. M) is V22() set
(x0 /. m) + (- (x0 /. M)) is V22() set
m - M is V22() Element of COMPLEX
- M is V22() set
m + (- M) is V22() set
a /. (m - M) is V22() Element of COMPLEX
a . (m - M) is V22() Element of COMPLEX
L /. (m - M) is V22() Element of COMPLEX
L . (m - M) is V22() Element of COMPLEX
(a /. (m - M)) + (L /. (m - M)) is V22() Element of COMPLEX
s1 - (x0 /. M) is V22() Element of COMPLEX
s1 + (- (x0 /. M)) is V22() set
s1 - s1 is V22() Element of COMPLEX
- s1 is V22() set
s1 + (- s1) is V22() set
(a /. (m - M)) + 0c is V22() Element of COMPLEX
(x0,M) is V22() Element of COMPLEX
a /. 1r is V22() Element of COMPLEX
a . 1r is V22() Element of COMPLEX
x0 is V22() Element of COMPLEX
f is V22() Element of COMPLEX
N is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom N is V45() Element of K19(COMPLEX)
L is V45() () Element of K19(COMPLEX)
(N,L) is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
cf is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom cf is V45() Element of K19(COMPLEX)
s1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
a is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
rng a is V45() Element of K19(COMPLEX)
a " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
cf /* a is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(a ") (#) (cf /* a) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((a ") (#) (cf /* a)) . s1 is V22() Element of COMPLEX
(a ") . s1 is V22() Element of COMPLEX
(cf /* a) . s1 is V22() Element of COMPLEX
((a ") . s1) * ((cf /* a) . s1) is V22() Element of COMPLEX
a . s1 is V22() Element of COMPLEX
cf /. (a . s1) is V22() Element of COMPLEX
cf . (a . s1) is V22() Element of COMPLEX
((a ") . s1) * (cf /. (a . s1)) is V22() Element of COMPLEX
((a ") . s1) * 0c is V22() Element of COMPLEX
((a ") (#) (cf /* a)) . 0 is V22() Element of COMPLEX
lim ((a ") (#) (cf /* a)) is V22() Element of COMPLEX
s1 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(COMPLEX,COMPLEX))
M is V22() Element of COMPLEX
s1 /. M is V22() Element of COMPLEX
s1 . M is V22() Element of COMPLEX
x0 * M is V22() Element of COMPLEX
p is V22() Element of COMPLEX
m is V45() (p)
N /. p is V22() Element of COMPLEX
M is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
a is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m is V22() Element of COMPLEX
N /. m is V22() Element of COMPLEX
(N /. m) - (N /. p) is V22() Element of COMPLEX
- (N /. p) is V22() set
(N /. m) + (- (N /. p)) is V22() set
m - p is V22() Element of COMPLEX
- p is V22() set
m + (- p) is V22() set
M /. (m - p) is V22() Element of COMPLEX
M . (m - p) is V22() Element of COMPLEX
a /. (m - p) is V22() Element of COMPLEX
a . (m - p) is V22() Element of COMPLEX
(M /. (m - p)) + (a /. (m - p)) is V22() Element of COMPLEX
x0 * m is V22() Element of COMPLEX
(x0 * m) + f is V22() Element of COMPLEX
((x0 * m) + f) - (N /. p) is V22() Element of COMPLEX
((x0 * m) + f) + (- (N /. p)) is V22() set
x0 * p is V22() Element of COMPLEX
(x0 * p) + f is V22() Element of COMPLEX
((x0 * m) + f) - ((x0 * p) + f) is V22() Element of COMPLEX
- ((x0 * p) + f) is V22() set
((x0 * m) + f) + (- ((x0 * p) + f)) is V22() set
x0 * (m - p) is V22() Element of COMPLEX
(x0 * (m - p)) + 0c is V22() Element of COMPLEX
(M /. (m - p)) + 0c is V22() Element of COMPLEX
p is V22() Element of COMPLEX
(N,L) /. p is V22() Element of COMPLEX
m is V45() (p)
N /. p is V22() Element of COMPLEX
m is V22() Element of COMPLEX
N /. m is V22() Element of COMPLEX
(N /. m) - (N /. p) is V22() Element of COMPLEX
- (N /. p) is V22() set
(N /. m) + (- (N /. p)) is V22() set
m - p is V22() Element of COMPLEX
- p is V22() set
m + (- p) is V22() set
M /. (m - p) is V22() Element of COMPLEX
M . (m - p) is V22() Element of COMPLEX
a /. (m - p) is V22() Element of COMPLEX
a . (m - p) is V22() Element of COMPLEX
(M /. (m - p)) + (a /. (m - p)) is V22() Element of COMPLEX
x0 * m is V22() Element of COMPLEX
(x0 * m) + f is V22() Element of COMPLEX
((x0 * m) + f) - (N /. p) is V22() Element of COMPLEX
((x0 * m) + f) + (- (N /. p)) is V22() set
x0 * p is V22() Element of COMPLEX
(x0 * p) + f is V22() Element of COMPLEX
((x0 * m) + f) - ((x0 * p) + f) is V22() Element of COMPLEX
- ((x0 * p) + f) is V22() set
((x0 * m) + f) + (- ((x0 * p) + f)) is V22() set
x0 * (m - p) is V22() Element of COMPLEX
(x0 * (m - p)) + 0c is V22() Element of COMPLEX
(M /. (m - p)) + 0c is V22() Element of COMPLEX
(N,p) is V22() Element of COMPLEX
M /. 1r is V22() Element of COMPLEX
M . 1r is V22() Element of COMPLEX
x0 * 1r is V22() Element of COMPLEX
x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f is V22() Element of COMPLEX
dom x0 is V45() Element of K19(COMPLEX)
x0 /. f is V22() Element of COMPLEX
N is V45() (f)
L is V22() real ext-real Element of REAL
{ b1 where b1 is V22() set : not L <= |.(b1 - f).| } is set
NAT --> f is V1() V4( NAT ) V5( COMPLEX ) Function-like constant V11() total T-Sequence-like quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
a is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng a is V45() Element of K19(COMPLEX)
lim a is V22() Element of COMPLEX
s1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
R is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim R is V22() Element of COMPLEX
R . 0 is V22() Element of COMPLEX
M is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
a - R is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- R is V1() V4( NAT ) Function-like total complex-valued set
(- 1) (#) R is V1() V4( NAT ) Function-like total complex-valued set
a + (- R) is V1() V4( NAT ) Function-like total complex-valued set
lim M is V22() Element of COMPLEX
lim (a - R) is V22() Element of COMPLEX
f - f is V22() Element of COMPLEX
- f is V22() set
f + (- f) is V22() set
M ^\ s1 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of M
lim (M ^\ s1) is V22() Element of COMPLEX
R ^\ s1 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of R
m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
M . m is V22() Element of COMPLEX
a . m is V22() Element of COMPLEX
R . m is V22() Element of COMPLEX
(a . m) - (R . m) is V22() Element of COMPLEX
- (R . m) is V22() set
(a . m) + (- (R . m)) is V22() set
m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(M ^\ s1) . m is V22() Element of COMPLEX
m + s1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
M . (m + s1) is V22() Element of COMPLEX
m is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
p is V1() V4( NAT ) V5( COMPLEX ) Function-like constant V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
m + p is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
x0 /* (m + p) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
x0 /* p is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(x0 /* (m + p)) - (x0 /* p) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- (x0 /* p) is V1() V4( NAT ) Function-like total complex-valued set
(- 1) (#) (x0 /* p) is V1() V4( NAT ) Function-like total complex-valued set
(x0 /* (m + p)) + (- (x0 /* p)) is V1() V4( NAT ) Function-like total complex-valued set
((x0 /* (m + p)) - (x0 /* p)) + (x0 /* p) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(((x0 /* (m + p)) - (x0 /* p)) + (x0 /* p)) . m is V22() Element of COMPLEX
((x0 /* (m + p)) - (x0 /* p)) . m is V22() Element of COMPLEX
(x0 /* p) . m is V22() Element of COMPLEX
(((x0 /* (m + p)) - (x0 /* p)) . m) + ((x0 /* p) . m) is V22() Element of COMPLEX
(x0 /* (m + p)) . m is V22() Element of COMPLEX
((x0 /* (m + p)) . m) - ((x0 /* p) . m) is V22() Element of COMPLEX
- ((x0 /* p) . m) is V22() set
((x0 /* (m + p)) . m) + (- ((x0 /* p) . m)) is V22() set
(((x0 /* (m + p)) . m) - ((x0 /* p) . m)) + ((x0 /* p) . m) is V22() Element of COMPLEX
m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(m + p) . m is V22() Element of COMPLEX
(a - R) + R is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((a - R) + R) ^\ s1 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of (a - R) + R
(((a - R) + R) ^\ s1) . m is V22() Element of COMPLEX
m + s1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
((a - R) + R) . (m + s1) is V22() Element of COMPLEX
(a - R) . (m + s1) is V22() Element of COMPLEX
R . (m + s1) is V22() Element of COMPLEX
((a - R) . (m + s1)) + (R . (m + s1)) is V22() Element of COMPLEX
a . (m + s1) is V22() Element of COMPLEX
(a . (m + s1)) - (R . (m + s1)) is V22() Element of COMPLEX
- (R . (m + s1)) is V22() set
(a . (m + s1)) + (- (R . (m + s1))) is V22() set
((a . (m + s1)) - (R . (m + s1))) + (R . (m + s1)) is V22() Element of COMPLEX
a ^\ s1 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of a
(a ^\ s1) . m is V22() Element of COMPLEX
x0 /* (a ^\ s1) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
x0 /* a is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(x0 /* a) ^\ s1 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued subsequence of x0 /* a
rng p is V12() V45() Element of K19(COMPLEX)
{f} is V45() set
m is set
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(R ^\ s1) . n is V22() Element of COMPLEX
n + s1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
R . (n + s1) is V22() Element of COMPLEX
m is set
p . 0 is V22() Element of COMPLEX
0 + s1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
R . (0 + s1) is V22() Element of COMPLEX
m is V22() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
y1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(x0 /* p) . y1 is V22() Element of COMPLEX
((x0 /* p) . y1) - (x0 /. f) is V22() Element of COMPLEX
- (x0 /. f) is V22() set
((x0 /* p) . y1) + (- (x0 /. f)) is V22() set
|.(((x0 /* p) . y1) - (x0 /. f)).| is V22() real ext-real Element of REAL
Re (((x0 /* p) . y1) - (x0 /. f)) is V22() real ext-real Element of REAL
K266((Re (((x0 /* p) . y1) - (x0 /. f)))) is V22() real ext-real Element of REAL
Im (((x0 /* p) . y1) - (x0 /. f)) is V22() real ext-real Element of REAL
K266((Im (((x0 /* p) . y1) - (x0 /. f)))) is V22() real ext-real Element of REAL
K266((Re (((x0 /* p) . y1) - (x0 /. f)))) + K266((Im (((x0 /* p) . y1) - (x0 /. f)))) is V22() real ext-real Element of REAL
K268((K266((Re (((x0 /* p) . y1) - (x0 /. f)))) + K266((Im (((x0 /* p) . y1) - (x0 /. f)))))) is V22() real ext-real Element of REAL
p . y1 is V22() Element of COMPLEX
x0 /. (p . y1) is V22() Element of COMPLEX
(x0 /. (p . y1)) - (x0 /. f) is V22() Element of COMPLEX
(x0 /. (p . y1)) + (- (x0 /. f)) is V22() set
|.((x0 /. (p . y1)) - (x0 /. f)).| is V22() real ext-real Element of REAL
Re ((x0 /. (p . y1)) - (x0 /. f)) is V22() real ext-real Element of REAL
K266((Re ((x0 /. (p . y1)) - (x0 /. f)))) is V22() real ext-real Element of REAL
Im ((x0 /. (p . y1)) - (x0 /. f)) is V22() real ext-real Element of REAL
K266((Im ((x0 /. (p . y1)) - (x0 /. f)))) is V22() real ext-real Element of REAL
K266((Re ((x0 /. (p . y1)) - (x0 /. f)))) + K266((Im ((x0 /. (p . y1)) - (x0 /. f)))) is V22() real ext-real Element of REAL
K268((K266((Re ((x0 /. (p . y1)) - (x0 /. f)))) + K266((Im ((x0 /. (p . y1)) - (x0 /. f)))))) is V22() real ext-real Element of REAL
y1 + s1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
R . (y1 + s1) is V22() Element of COMPLEX
x0 /. (R . (y1 + s1)) is V22() Element of COMPLEX
(x0 /. (R . (y1 + s1))) - (x0 /. f) is V22() Element of COMPLEX
(x0 /. (R . (y1 + s1))) + (- (x0 /. f)) is V22() set
|.((x0 /. (R . (y1 + s1))) - (x0 /. f)).| is V22() real ext-real Element of REAL
Re ((x0 /. (R . (y1 + s1))) - (x0 /. f)) is V22() real ext-real Element of REAL
K266((Re ((x0 /. (R . (y1 + s1))) - (x0 /. f)))) is V22() real ext-real Element of REAL
Im ((x0 /. (R . (y1 + s1))) - (x0 /. f)) is V22() real ext-real Element of REAL
K266((Im ((x0 /. (R . (y1 + s1))) - (x0 /. f)))) is V22() real ext-real Element of REAL
K266((Re ((x0 /. (R . (y1 + s1))) - (x0 /. f)))) + K266((Im ((x0 /. (R . (y1 + s1))) - (x0 /. f)))) is V22() real ext-real Element of REAL
K268((K266((Re ((x0 /. (R . (y1 + s1))) - (x0 /. f)))) + K266((Im ((x0 /. (R . (y1 + s1))) - (x0 /. f)))))) is V22() real ext-real Element of REAL
(x0 /. f) - (x0 /. f) is V22() Element of COMPLEX
(x0 /. f) + (- (x0 /. f)) is V22() set
|.((x0 /. f) - (x0 /. f)).| is V22() real ext-real Element of REAL
Re ((x0 /. f) - (x0 /. f)) is V22() real ext-real Element of REAL
K266((Re ((x0 /. f) - (x0 /. f)))) is V22() real ext-real Element of REAL
Im ((x0 /. f) - (x0 /. f)) is V22() real ext-real Element of REAL
K266((Im ((x0 /. f) - (x0 /. f)))) is V22() real ext-real Element of REAL
K266((Re ((x0 /. f) - (x0 /. f)))) + K266((Im ((x0 /. f) - (x0 /. f)))) is V22() real ext-real Element of REAL
K268((K266((Re ((x0 /. f) - (x0 /. f)))) + K266((Im ((x0 /. f) - (x0 /. f)))))) is V22() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
m . m is V22() Element of COMPLEX
m " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(m ") (#) ((x0 /* (m + p)) - (x0 /* p)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
m (#) ((m ") (#) ((x0 /* (m + p)) - (x0 /* p))) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(m (#) ((m ") (#) ((x0 /* (m + p)) - (x0 /* p)))) . m is V22() Element of COMPLEX
((m ") (#) ((x0 /* (m + p)) - (x0 /* p))) . m is V22() Element of COMPLEX
(m . m) * (((m ") (#) ((x0 /* (m + p)) - (x0 /* p))) . m) is V22() Element of COMPLEX
(m ") . m is V22() Element of COMPLEX
((x0 /* (m + p)) - (x0 /* p)) . m is V22() Element of COMPLEX
((m ") . m) * (((x0 /* (m + p)) - (x0 /* p)) . m) is V22() Element of COMPLEX
(m . m) * (((m ") . m) * (((x0 /* (m + p)) - (x0 /* p)) . m)) is V22() Element of COMPLEX
(m . m) " is V22() Element of COMPLEX
Re (m . m) is V22() real ext-real Element of REAL
K266((Re (m . m))) is V22() real ext-real Element of REAL
Im (m . m) is V22() real ext-real Element of REAL
K266((Im (m . m))) is V22() real ext-real Element of REAL
K266((Re (m . m))) + K266((Im (m . m))) is V22() real ext-real Element of REAL
(Re (m . m)) / (K266((Re (m . m))) + K266((Im (m . m)))) is V22() real ext-real Element of REAL
(K266((Re (m . m))) + K266((Im (m . m)))) " is V22() real ext-real set
(Re (m . m)) * ((K266((Re (m . m))) + K266((Im (m . m)))) ") is V22() real ext-real set
- (Im (m . m)) is V22() real ext-real Element of REAL
(- (Im (m . m))) / (K266((Re (m . m))) + K266((Im (m . m)))) is V22() real ext-real Element of REAL
(- (Im (m . m))) * ((K266((Re (m . m))) + K266((Im (m . m)))) ") is V22() real ext-real set
K278() is V22() Element of COMPLEX
((- (Im (m . m))) / (K266((Re (m . m))) + K266((Im (m . m))))) * K278() is V22() set
((Re (m . m)) / (K266((Re (m . m))) + K266((Im (m . m))))) + (((- (Im (m . m))) / (K266((Re (m . m))) + K266((Im (m . m))))) * K278()) is V22() set
((m . m) ") * (((x0 /* (m + p)) - (x0 /* p)) . m) is V22() Element of COMPLEX
(m . m) * (((m . m) ") * (((x0 /* (m + p)) - (x0 /* p)) . m)) is V22() Element of COMPLEX
(m . m) * ((m . m) ") is V22() Element of COMPLEX
((m . m) * ((m . m) ")) * (((x0 /* (m + p)) - (x0 /* p)) . m) is V22() Element of COMPLEX
1 * (((x0 /* (m + p)) - (x0 /* p)) . m) is V22() set
rng (m + p) is V45() Element of K19(COMPLEX)
m is set
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(m + p) . n is V22() Element of COMPLEX
(((a - R) + R) ^\ s1) . n is V22() Element of COMPLEX
n + s1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
((a - R) + R) . (n + s1) is V22() Element of COMPLEX
(a - R) . (n + s1) is V22() Element of COMPLEX
R . (n + s1) is V22() Element of COMPLEX
((a - R) . (n + s1)) + (R . (n + s1)) is V22() Element of COMPLEX
a . (n + s1) is V22() Element of COMPLEX
(a . (n + s1)) - (R . (n + s1)) is V22() Element of COMPLEX
- (R . (n + s1)) is V22() set
(a . (n + s1)) + (- (R . (n + s1))) is V22() set
((a . (n + s1)) - (R . (n + s1))) + (R . (n + s1)) is V22() Element of COMPLEX
s1 + n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
a . (s1 + n) is V22() Element of COMPLEX
((m + p) . n) - f is V22() Element of COMPLEX
((m + p) . n) + (- f) is V22() set
|.(((m + p) . n) - f).| is V22() real ext-real Element of REAL
Re (((m + p) . n) - f) is V22() real ext-real Element of REAL
K266((Re (((m + p) . n) - f))) is V22() real ext-real Element of REAL
Im (((m + p) . n) - f) is V22() real ext-real Element of REAL
K266((Im (((m + p) . n) - f))) is V22() real ext-real Element of REAL
K266((Re (((m + p) . n) - f))) + K266((Im (((m + p) . n) - f))) is V22() real ext-real Element of REAL
K268((K266((Re (((m + p) . n) - f))) + K266((Im (((m + p) . n) - f))))) is V22() real ext-real Element of REAL
y1 is V22() set
lim (m (#) ((m ") (#) ((x0 /* (m + p)) - (x0 /* p)))) is V22() Element of COMPLEX
lim ((m ") (#) ((x0 /* (m + p)) - (x0 /* p))) is V22() Element of COMPLEX
0c * (lim ((m ") (#) ((x0 /* (m + p)) - (x0 /* p)))) is V22() Element of COMPLEX
lim (((x0 /* (m + p)) - (x0 /* p)) + (x0 /* p)) is V22() Element of COMPLEX
lim (x0 /* p) is V22() Element of COMPLEX
0c + (lim (x0 /* p)) is V22() Element of COMPLEX
lim (x0 /* a) is V22() Element of COMPLEX
x0 is set
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V45() Element of K19(COMPLEX)
f | x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
N is V22() Element of COMPLEX
dom (f | x0) is V45() Element of K19(COMPLEX)
x0 is set
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
N is V45() () Element of K19(COMPLEX)
f | x0 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V45() Element of K19(COMPLEX)
f | N is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
L is V22() Element of COMPLEX
dom (f | N) is V45() Element of K19(COMPLEX)
R is V45() (L)
dom (f | x0) is V45() Element of K19(COMPLEX)
(f | x0) /. L is V22() Element of COMPLEX
a is V45() (L)
s1 is V45() (L)
(f | N) /. L is V22() Element of COMPLEX
(dom f) /\ x0 is V45() Element of K19(COMPLEX)
(dom f) /\ N is V45() Element of K19(COMPLEX)
M is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
p is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
M is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
p is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
m is V22() Element of COMPLEX
(f | N) /. m is V22() Element of COMPLEX
((f | N) /. m) - ((f | N) /. L) is V22() Element of COMPLEX
- ((f | N) /. L) is V22() set
((f | N) /. m) + (- ((f | N) /. L)) is V22() set
m - L is V22() set
- L is V22() set
m + (- L) is V22() set
M /. (m - L) is V22() Element of COMPLEX
p /. (m - L) is V22() Element of COMPLEX
(M /. (m - L)) + (p /. (m - L)) is V22() Element of COMPLEX
(f | x0) /. m is V22() Element of COMPLEX
((f | x0) /. m) - ((f | x0) /. L) is V22() Element of COMPLEX
- ((f | x0) /. L) is V22() set
((f | x0) /. m) + (- ((f | x0) /. L)) is V22() set
m - L is V22() Element of COMPLEX
M /. (m - L) is V22() Element of COMPLEX
M . (m - L) is V22() Element of COMPLEX
p /. (m - L) is V22() Element of COMPLEX
p . (m - L) is V22() Element of COMPLEX
(M /. (m - L)) + (p /. (m - L)) is V22() Element of COMPLEX
f /. L is V22() Element of COMPLEX
((f | x0) /. m) - (f /. L) is V22() Element of COMPLEX
- (f /. L) is V22() set
((f | x0) /. m) + (- (f /. L)) is V22() set
f /. m is V22() Element of COMPLEX
(f /. m) - (f /. L) is V22() Element of COMPLEX
(f /. m) + (- (f /. L)) is V22() set
(f /. m) - ((f | N) /. L) is V22() Element of COMPLEX
(f /. m) + (- ((f | N) /. L)) is V22() set
x0 is V22() Element of COMPLEX
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V45() Element of K19(COMPLEX)
f /. x0 is V22() Element of COMPLEX
N is V45() (x0)
L is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
L is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued () Element of K19(K20(COMPLEX,COMPLEX))
R /. 0c is V22() Element of COMPLEX
R . 0c is V22() Element of COMPLEX
a is V22() Element of COMPLEX
(f /. x0) - (f /. x0) is V22() Element of COMPLEX
- (f /. x0) is V22() set
(f /. x0) + (- (f /. x0)) is V22() set
x0 - x0 is V22() Element of COMPLEX
- x0 is V22() set
x0 + (- x0) is V22() set
L /. (x0 - x0) is V22() Element of COMPLEX
L . (x0 - x0) is V22() Element of COMPLEX
R /. (x0 - x0) is V22() Element of COMPLEX
R . (x0 - x0) is V22() Element of COMPLEX
(L /. (x0 - x0)) + (R /. (x0 - x0)) is V22() Element of COMPLEX
a * 0c is V22() Element of COMPLEX
(a * 0c) + (R /. 0c) is V22() Element of COMPLEX
s1 is V1() non-empty V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued bounded convergent ( 0 ) Element of K19(K20(NAT,COMPLEX))
s1 " is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
R /* s1 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(s1 ") (#) (R /* s1) is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
M is V22() real ext-real Element of REAL
lim s1 is V22() Element of COMPLEX
|.s1.| is V1() V4( NAT ) V5( REAL ) Function-like V11() total quasi_total complex-valued ext-real-valued real-valued bounded_above bounded_below bounded convergent Element of K19(K20(NAT,REAL))
lim |.s1.| is V22() real ext-real Element of REAL
M (#) |.s1.| is V1() V4( NAT ) V5( REAL ) Function-like V11() total quasi_total complex-valued ext-real-valued real-valued bounded_above bounded_below bounded convergent Element of K19(K20(NAT,REAL))
lim (M (#) |.s1.|) is V22() real ext-real Element of REAL
M * |.0.| is V22() real ext-real Element of REAL
M * 0 is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(M (#) |.s1.|) . n is V22() real ext-real Element of REAL
((M (#) |.s1.|) . n) - 0 is V22() real ext-real Element of REAL
- 0 is V22() real ext-real non positive set
((M (#) |.s1.|) . n) + (- 0) is V22() real ext-real set
abs (((M (#) |.s1.|) . n) - 0) is V22() real ext-real Element of REAL
Re (((M (#) |.s1.|) . n) - 0) is V22() real ext-real Element of REAL
K266((Re (((M (#) |.s1.|) . n) - 0))) is V22() real ext-real Element of REAL
Im (((M (#) |.s1.|) . n) - 0) is V22() real ext-real Element of REAL
K266((Im (((M (#) |.s1.|) . n) - 0))) is V22() real ext-real Element of REAL
K266((Re (((M (#) |.s1.|) . n) - 0))) + K266((Im (((M (#) |.s1.|) . n) - 0))) is V22() real ext-real Element of REAL
K268((K266((Re (((M (#) |.s1.|) . n) - 0))) + K266((Im (((M (#) |.s1.|) . n) - 0))))) is V22() real ext-real Element of REAL
((s1 ") (#) (R /* s1)) . n is V22() Element of COMPLEX
|.(((s1 ") (#) (R /* s1)) . n).| is V22() real ext-real Element of REAL
Re (((s1 ") (#) (R /* s1)) . n) is V22() real ext-real Element of REAL
K266((Re (((s1 ") (#) (R /* s1)) . n))) is V22() real ext-real Element of REAL
Im (((s1 ") (#) (R /* s1)) . n) is V22() real ext-real Element of REAL
K266((Im (((s1 ") (#) (R /* s1)) . n))) is V22() real ext-real Element of REAL
K266((Re (((s1 ") (#) (R /* s1)) . n))) + K266((Im (((s1 ") (#) (R /* s1)) . n))) is V22() real ext-real Element of REAL
K268((K266((Re (((s1 ") (#) (R /* s1)) . n))) + K266((Im (((s1 ") (#) (R /* s1)) . n))))) is V22() real ext-real Element of REAL
(s1 ") . n is V22() Element of COMPLEX
(R /* s1) . n is V22() Element of COMPLEX
((s1 ") . n) * ((R /* s1) . n) is V22() Element of COMPLEX
|.(((s1 ") . n) * ((R /* s1) . n)).| is V22() real ext-real Element of REAL
Re (((s1 ") . n) * ((R /* s1) . n)) is V22() real ext-real Element of REAL
K266((Re (((s1 ") . n) * ((R /* s1) . n)))) is V22() real ext-real Element of REAL
Im (((s1 ") . n) * ((R /* s1) . n)) is V22() real ext-real Element of REAL
K266((Im (((s1 ") . n) * ((R /* s1) . n)))) is V22() real ext-real Element of REAL
K266((Re (((s1 ") . n) * ((R /* s1) . n)))) + K266((Im (((s1 ") . n) * ((R /* s1) . n)))) is V22() real ext-real Element of REAL
K268((K266((Re (((s1 ") . n) * ((R /* s1) . n)))) + K266((Im (((s1 ") . n) * ((R /* s1) . n)))))) is V22() real ext-real Element of REAL
s1 . n is V22() Element of COMPLEX
(s1 . n) " is V22() Element of COMPLEX
Re (s1 . n) is V22() real ext-real Element of REAL
K266((Re (s1 . n))) is V22() real ext-real Element of REAL
Im (s1 . n) is V22() real ext-real Element of REAL
K266((Im (s1 . n))) is V22() real ext-real Element of REAL
K266((Re (s1 . n))) + K266((Im (s1 . n))) is V22() real ext-real Element of REAL
(Re (s1 . n)) / (K266((Re (s1 . n))) + K266((Im (s1 . n)))) is V22() real ext-real Element of REAL
(K266((Re (s1 . n))) + K266((Im (s1 . n)))) " is V22() real ext-real set
(Re (s1 . n)) * ((K266((Re (s1 . n))) + K266((Im (s1 . n)))) ") is V22() real ext-real set
- (Im (s1 . n)) is V22() real ext-real Element of REAL
(- (Im (s1 . n))) / (K266((Re (s1 . n))) + K266((Im (s1 . n)))) is V22() real ext-real Element of REAL
(- (Im (s1 . n))) * ((K266((Re (s1 . n))) + K266((Im (s1 . n)))) ") is V22() real ext-real set
K278() is V22() Element of COMPLEX
((- (Im (s1 . n))) / (K266((Re (s1 . n))) + K266((Im (s1 . n))))) * K278() is V22() set
((Re (s1 . n)) / (K266((Re (s1 . n))) + K266((Im (s1 . n))))) + (((- (Im (s1 . n))) / (K266((Re (s1 . n))) + K266((Im (s1 . n))))) * K278()) is V22() set
((s1 . n) ") * ((R /* s1) . n) is V22() Element of COMPLEX
|.(((s1 . n) ") * ((R /* s1) . n)).| is V22() real ext-real Element of REAL
Re (((s1 . n) ") * ((R /* s1) . n)) is V22() real ext-real Element of REAL
K266((Re (((s1 . n) ") * ((R /* s1) . n)))) is V22() real ext-real Element of REAL
Im (((s1 . n) ") * ((R /* s1) . n)) is V22() real ext-real Element of REAL
K266((Im (((s1 . n) ") * ((R /* s1) . n)))) is V22() real ext-real Element of REAL
K266((Re (((s1 . n) ") * ((R /* s1) . n)))) + K266((Im (((s1 . n) ") * ((R /* s1) . n)))) is V22() real ext-real Element of REAL
K268((K266((Re (((s1 . n) ") * ((R /* s1) . n)))) + K266((Im (((s1 . n) ") * ((R /* s1) . n)))))) is V22() real ext-real Element of REAL
|.(s1 . n).| is V22() real ext-real Element of REAL
K268((K266((Re (s1 . n))) + K266((Im (s1 . n))))) is V22() real ext-real Element of REAL
|.(s1 . n).| * |.(((s1 . n) ") * ((R /* s1) . n)).| is V22() real ext-real Element of REAL
M * |.(s1 . n).| is V22() real ext-real Element of REAL
(s1 . n) * (((s1 . n) ") * ((R /* s1) . n)) is V22() Element of COMPLEX
|.((s1 . n) * (((s1 . n) ") * ((R /* s1) . n))).| is V22() real ext-real Element of REAL
Re ((s1 . n) * (((s1 . n) ") * ((R /* s1) . n))) is V22() real ext-real Element of REAL
K266((Re ((s1 . n) * (((s1 . n) ") * ((R /* s1) . n))))) is V22() real ext-real Element of REAL
Im ((s1 . n) * (((s1 . n) ") * ((R /* s1) . n))) is V22() real ext-real Element of REAL
K266((Im ((s1 . n) * (((s1 . n) ") * ((R /* s1) . n))))) is V22() real ext-real Element of REAL
K266((Re ((s1 . n) * (((s1 . n) ") * ((R /* s1) . n))))) + K266((Im ((s1 . n) * (((s1 . n) ") * ((R /* s1) . n))))) is V22() real ext-real Element of REAL
K268((K266((Re ((s1 . n) * (((s1 . n) ") * ((R /* s1) . n))))) + K266((Im ((s1 . n) * (((s1 . n) ") * ((R /* s1) . n))))))) is V22() real ext-real Element of REAL
(s1 . n) * ((s1 . n) ") is V22() Element of COMPLEX
((s1 . n) * ((s1 . n) ")) * ((R /* s1) . n) is V22() Element of COMPLEX
|.(((s1 . n) * ((s1 . n) ")) * ((R /* s1) . n)).| is V22() real ext-real Element of REAL
Re (((s1 . n) * ((s1 . n) ")) * ((R /* s1) . n)) is V22() real ext-real Element of REAL
K266((Re (((s1 . n) * ((s1 . n) ")) * ((R /* s1) . n)))) is V22() real ext-real Element of REAL
Im (((s1 . n) * ((s1 . n) ")) * ((R /* s1) . n)) is V22() real ext-real Element of REAL
K266((Im (((s1 . n) * ((s1 . n) ")) * ((R /* s1) . n)))) is V22() real ext-real Element of REAL
K266((Re (((s1 . n) * ((s1 . n) ")) * ((R /* s1) . n)))) + K266((Im (((s1 . n) * ((s1 . n) ")) * ((R /* s1) . n)))) is V22() real ext-real Element of REAL
K268((K266((Re (((s1 . n) * ((s1 . n) ")) * ((R /* s1) . n)))) + K266((Im (((s1 . n) * ((s1 . n) ")) * ((R /* s1) . n)))))) is V22() real ext-real Element of REAL
1r * ((R /* s1) . n) is V22() Element of COMPLEX
|.(1r * ((R /* s1) . n)).| is V22() real ext-real Element of REAL
Re (1r * ((R /* s1) . n)) is V22() real ext-real Element of REAL
K266((Re (1r * ((R /* s1) . n)))) is V22() real ext-real Element of REAL
Im (1r * ((R /* s1) . n)) is V22() real ext-real Element of REAL
K266((Im (1r * ((R /* s1) . n)))) is V22() real ext-real Element of REAL
K266((Re (1r * ((R /* s1) . n)))) + K266((Im (1r * ((R /* s1) . n)))) is V22() real ext-real Element of REAL
K268((K266((Re (1r * ((R /* s1) . n)))) + K266((Im (1r * ((R /* s1) . n)))))) is V22() real ext-real Element of REAL
|.((R /* s1) . n).| is V22() real ext-real Element of REAL
Re ((R /* s1) . n) is V22() real ext-real Element of REAL
K266((Re ((R /* s1) . n))) is V22() real ext-real Element of REAL
Im ((R /* s1) . n) is V22() real ext-real Element of REAL
K266((Im ((R /* s1) . n))) is V22() real ext-real Element of REAL
K266((Re ((R /* s1) . n))) + K266((Im ((R /* s1) . n))) is V22() real ext-real Element of REAL
K268((K266((Re ((R /* s1) . n))) + K266((Im ((R /* s1) . n))))) is V22() real ext-real Element of REAL
|.s1.| . n is V22() real ext-real Element of REAL
M * (|.s1.| . n) is V22() real ext-real Element of REAL
((R /* s1) . n) - 0c is V22() Element of COMPLEX
- 0c is V22() set
((R /* s1) . n) + (- 0c) is V22() set
|.(((R /* s1) . n) - 0c).| is V22() real ext-real Element of REAL
Re (((R /* s1) . n) - 0c) is V22() real ext-real Element of REAL
K266((Re (((R /* s1) . n) - 0c))) is V22() real ext-real Element of REAL
Im (((R /* s1) . n) - 0c) is V22() real ext-real Element of REAL
K266((Im (((R /* s1) . n) - 0c))) is V22() real ext-real Element of REAL
K266((Re (((R /* s1) . n) - 0c))) + K266((Im (((R /* s1) . n) - 0c))) is V22() real ext-real Element of REAL
K268((K266((Re (((R /* s1) . n) - 0c))) + K266((Im (((R /* s1) . n) - 0c))))) is V22() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
(R /* s1) . n is V22() Element of COMPLEX
((R /* s1) . n) - 0c is V22() Element of COMPLEX
((R /* s1) . n) + (- 0c) is V22() set
|.(((R /* s1) . n) - 0c).| is V22() real ext-real Element of REAL
Re (((R /* s1) . n) - 0c) is V22() real ext-real Element of REAL
K266((Re (((R /* s1) . n) - 0c))) is V22() real ext-real Element of REAL
Im (((R /* s1) . n) - 0c) is V22() real ext-real Element of REAL
K266((Im (((R /* s1) . n) - 0c))) is V22() real ext-real Element of REAL
K266((Re (((R /* s1) . n) - 0c))) + K266((Im (((R /* s1) . n) - 0c))) is V22() real ext-real Element of REAL
K268((K266((Re (((R /* s1) . n) - 0c))) + K266((Im (((R /* s1) . n) - 0c))))) is V22() real ext-real Element of REAL
lim (R /* s1) is V22() Element of COMPLEX
s1 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng s1 is V45() Element of K19(COMPLEX)
dom R is V45() Element of K19(COMPLEX)
lim s1 is V22() Element of COMPLEX
R /* s1 is V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim (R /* s1) is V22() Element of COMPLEX