:: FDIFF_3 semantic presentation

REAL is V11() V12() V49() V51() V71() V72() V73() V77() V99() V100() V102() set
NAT is V11() epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V97() V99() Element of K19(REAL)
K19(REAL) is set
COMPLEX is V11() V12() V49() V51() V71() V77() set
omega is V11() epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V97() V99() set
K19(omega) is set
K20(NAT,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
K19(K19(REAL)) is set
0 is set
the V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V51() V55() V71() V72() V73() V74() V75() V76() V77() V99() V100() V101() V102() set is V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V51() V55() V71() V72() V73() V74() V75() V76() V77() V99() V100() V101() V102() set
1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V91() V92() V97() V99() Element of NAT
{0,1} is V51() set
K20(REAL,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) is set
RAT is V11() V12() V49() V51() V71() V72() V73() V74() V77() set
INT is V11() V12() V49() V51() V71() V72() V73() V74() V75() V77() set
K20(COMPLEX,COMPLEX) is complex-valued set
K19(K20(COMPLEX,COMPLEX)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(K20(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is V5( RAT ) complex-valued ext-real-valued real-valued set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is V5( RAT ) complex-valued ext-real-valued real-valued set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
K20(K20(NAT,NAT),NAT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
K19(K20(K20(NAT,NAT),NAT)) is set
K19(NAT) is set
0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
{0} is V51() V71() V72() V73() V74() V75() V76() V99() V100() V101() set
K19(K20(NAT,NAT)) is set
2 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V91() V92() V97() V99() Element of NAT
-infty is V11() non real ext-real non positive negative set
+infty is V11() non real ext-real positive non negative set
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
{x0} is V51() V71() V72() V73() V99() V100() V101() set
N is V30() real ext-real Element of REAL
x0 - N is V30() real ext-real Element of REAL
[.(x0 - N),x0.] is V71() V72() V73() V102() Element of K19(REAL)
NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant V11() total quasi_total complex-valued ext-real-valued real-valued convergent Element of K19(K20(NAT,REAL))
g1 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- N is V30() real ext-real Element of REAL
q1 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
q2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
q2 + 2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
N / (q2 + 2) is V30() real ext-real Element of REAL
- 0 is V30() real ext-real Element of REAL
- (N / (q2 + 2)) is V30() real ext-real Element of REAL
(- N) / (q2 + 2) is V30() real ext-real Element of REAL
q1 . q2 is V30() real ext-real Element of REAL
q2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
q1 . q2 is V30() real ext-real Element of REAL
lim q1 is V30() real ext-real Element of REAL
q2 is V1() non-zero V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() constant V11() total quasi_total complex-valued ext-real-valued real-valued convergent Element of K19(K20(NAT,REAL))
rng r is V71() V72() V73() Element of K19(REAL)
q2 + r is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (q2 + r) is V71() V72() V73() Element of K19(REAL)
h1 is set
h1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
r . h1 is V30() real ext-real Element of REAL
h1 is set
r . 0 is V30() real ext-real Element of REAL
h1 is set
h1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
(q2 + r) . h1 is V30() real ext-real Element of REAL
h1 + 2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
N * (h1 + 2) is V30() real ext-real Element of REAL
N * 1 is V30() real ext-real Element of REAL
(h1 + 2) " is V30() real ext-real Element of REAL
(N * (h1 + 2)) * ((h1 + 2) ") is V30() real ext-real Element of REAL
N * ((h1 + 2) ") is V30() real ext-real Element of REAL
(h1 + 2) * ((h1 + 2) ") is V30() real ext-real Element of REAL
N * ((h1 + 2) * ((h1 + 2) ")) is V30() real ext-real Element of REAL
N / (h1 + 2) is V30() real ext-real Element of REAL
x0 - (N / (h1 + 2)) is V30() real ext-real Element of REAL
- (N / (h1 + 2)) is V30() real ext-real Element of REAL
x0 + (- (N / (h1 + 2))) is V30() real ext-real Element of REAL
(- N) / (h1 + 2) is V30() real ext-real Element of REAL
x0 + ((- N) / (h1 + 2)) is V30() real ext-real Element of REAL
x0 - 0 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( x0 - N <= b₁ & b₁ <= x0 ) } is set
q2 . h1 is V30() real ext-real Element of REAL
r . h1 is V30() real ext-real Element of REAL
(q2 . h1) + (r . h1) is V30() real ext-real Element of REAL
((- N) / (h1 + 2)) + (r . h1) is V30() real ext-real Element of REAL
h1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
q2 . h1 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
{x0} is V51() V71() V72() V73() V99() V100() V101() set
N is V30() real ext-real Element of REAL
x0 + N is V30() real ext-real Element of REAL
[.x0,(x0 + N).] is V71() V72() V73() V102() Element of K19(REAL)
NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant V11() total quasi_total complex-valued ext-real-valued real-valued convergent Element of K19(K20(NAT,REAL))
g1 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
q1 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
q2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
q2 + 2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
N / (q2 + 2) is V30() real ext-real Element of REAL
q1 . q2 is V30() real ext-real Element of REAL
q2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
q1 . q2 is V30() real ext-real Element of REAL
lim q1 is V30() real ext-real Element of REAL
q2 is V1() non-zero V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() constant V11() total quasi_total complex-valued ext-real-valued real-valued convergent Element of K19(K20(NAT,REAL))
rng r is V71() V72() V73() Element of K19(REAL)
q2 + r is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (q2 + r) is V71() V72() V73() Element of K19(REAL)
h1 is set
h1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
r . h1 is V30() real ext-real Element of REAL
h1 is set
r . 0 is V30() real ext-real Element of REAL
h1 is set
h1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
(q2 + r) . h1 is V30() real ext-real Element of REAL
h1 + 2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
N * (h1 + 2) is V30() real ext-real Element of REAL
N * 1 is V30() real ext-real Element of REAL
(h1 + 2) " is V30() real ext-real Element of REAL
(N * (h1 + 2)) * ((h1 + 2) ") is V30() real ext-real Element of REAL
N * ((h1 + 2) ") is V30() real ext-real Element of REAL
(h1 + 2) * ((h1 + 2) ") is V30() real ext-real Element of REAL
N * ((h1 + 2) * ((h1 + 2) ")) is V30() real ext-real Element of REAL
N / (h1 + 2) is V30() real ext-real Element of REAL
x0 + (N / (h1 + 2)) is V30() real ext-real Element of REAL
x0 + 0 is V30() real ext-real Element of REAL
{ b₁ where b₁ is V30() real ext-real Element of REAL : ( x0 <= b₁ & b₁ <= x0 + N ) } is set
q2 . h1 is V30() real ext-real Element of REAL
r . h1 is V30() real ext-real Element of REAL
(q2 . h1) + (r . h1) is V30() real ext-real Element of REAL
(N / (h1 + 2)) + (r . h1) is V30() real ext-real Element of REAL
(N / (h1 + 2)) + x0 is V30() real ext-real Element of REAL
h1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
q2 . h1 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
{x0} is V51() V71() V72() V73() V99() V100() V101() set
N is V1() non-zero V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
N " is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
g1 is V1() non-zero V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
g1 " is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() constant V11() total quasi_total complex-valued ext-real-valued real-valued convergent Element of K19(K20(NAT,REAL))
rng r is V71() V72() V73() Element of K19(REAL)
N + r is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (N + r) is V71() V72() V73() Element of K19(REAL)
g1 + r is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (g1 + r) is V71() V72() V73() Element of K19(REAL)
f /* (N + r) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* r is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (N + r)) - (f /* r) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (f /* r) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
K116(1) is V30() real ext-real non positive set
K116(1) (#) (f /* r) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(f /* (N + r)) + (- (f /* r)) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(N ") (#) ((f /* (N + r)) - (f /* r)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((N ") (#) ((f /* (N + r)) - (f /* r))) is V30() real ext-real Element of REAL
f /* (g1 + r) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (g1 + r)) - (f /* r) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (g1 + r)) + (- (f /* r)) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(g1 ") (#) ((f /* (g1 + r)) - (f /* r)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((g1 ") (#) ((f /* (g1 + r)) - (f /* r))) is V30() real ext-real Element of REAL
q1 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
q2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
h1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
2 * h1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
(2 * h1) + 1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
q1 . (2 * h1) is V30() real ext-real Element of REAL
N . h1 is V30() real ext-real Element of REAL
q1 . q2 is V30() real ext-real Element of REAL
q1 . ((2 * h1) + 1) is V30() real ext-real Element of REAL
g1 . h1 is V30() real ext-real Element of REAL
q1 . q2 is V30() real ext-real Element of REAL
q1 . q2 is V30() real ext-real Element of REAL
q1 . q2 is V30() real ext-real Element of REAL
lim g1 is V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V51() V55() V71() V72() V73() V74() V75() V76() V77() V99() V100() V101() V102() Element of REAL
lim N is V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V51() V55() V71() V72() V73() V74() V75() V76() V77() V99() V100() V101() V102() Element of REAL
lim q1 is V30() real ext-real Element of REAL
h1 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
h1 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
q2 is V1() non-zero V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
q2 + r is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (q2 + r) is V71() V72() V73() Element of K19(REAL)
h2 is set
c2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
(q2 + r) . c2 is V30() real ext-real Element of REAL
c2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
2 * c2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
(2 * c2) + 1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
q2 . c2 is V30() real ext-real Element of REAL
r . c2 is V30() real ext-real Element of REAL
(q2 . c2) + (r . c2) is V30() real ext-real Element of REAL
N . c2 is V30() real ext-real Element of REAL
r . (2 * c2) is V30() real ext-real Element of REAL
(N . c2) + (r . (2 * c2)) is V30() real ext-real Element of REAL
r . c2 is V30() real ext-real Element of REAL
(N . c2) + (r . c2) is V30() real ext-real Element of REAL
(N + r) . c2 is V30() real ext-real Element of REAL
g1 . c2 is V30() real ext-real Element of REAL
r . ((2 * c2) + 1) is V30() real ext-real Element of REAL
(g1 . c2) + (r . ((2 * c2) + 1)) is V30() real ext-real Element of REAL
r . c2 is V30() real ext-real Element of REAL
(g1 . c2) + (r . c2) is V30() real ext-real Element of REAL
(g1 + r) . c2 is V30() real ext-real Element of REAL
h2 is V1() V4( NAT ) V5( NAT ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
q2 " is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* (q2 + r) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (q2 + r)) - (f /* r) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (q2 + r)) + (- (f /* r)) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(q2 ") (#) ((f /* (q2 + r)) - (f /* r)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) * h2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued subsequence of (q2 ") (#) ((f /* (q2 + r)) - (f /* r))
h2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
(((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) * h2) . h2 is V30() real ext-real Element of REAL
h2 . h2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) . (h2 . h2) is V30() real ext-real Element of REAL
2 * h2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
(2 * h2) + 1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) . ((2 * h2) + 1) is V30() real ext-real Element of REAL
(q2 ") . ((2 * h2) + 1) is V30() real ext-real Element of REAL
((f /* (q2 + r)) - (f /* r)) . ((2 * h2) + 1) is V30() real ext-real Element of REAL
((q2 ") . ((2 * h2) + 1)) * (((f /* (q2 + r)) - (f /* r)) . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
(f /* (q2 + r)) . ((2 * h2) + 1) is V30() real ext-real Element of REAL
(f /* r) . ((2 * h2) + 1) is V30() real ext-real Element of REAL
((f /* (q2 + r)) . ((2 * h2) + 1)) - ((f /* r) . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
((q2 ") . ((2 * h2) + 1)) * (((f /* (q2 + r)) . ((2 * h2) + 1)) - ((f /* r) . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
q2 . ((2 * h2) + 1) is V30() real ext-real Element of REAL
(q2 . ((2 * h2) + 1)) " is V30() real ext-real Element of REAL
((q2 . ((2 * h2) + 1)) ") * (((f /* (q2 + r)) . ((2 * h2) + 1)) - ((f /* r) . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
g1 . h2 is V30() real ext-real Element of REAL
(g1 . h2) " is V30() real ext-real Element of REAL
((g1 . h2) ") * (((f /* (q2 + r)) . ((2 * h2) + 1)) - ((f /* r) . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
(g1 ") . h2 is V30() real ext-real Element of REAL
((g1 ") . h2) * (((f /* (q2 + r)) . ((2 * h2) + 1)) - ((f /* r) . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
(q2 + r) . ((2 * h2) + 1) is V30() real ext-real Element of REAL
f . ((q2 + r) . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
(f . ((q2 + r) . ((2 * h2) + 1))) - ((f /* r) . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
((g1 ") . h2) * ((f . ((q2 + r) . ((2 * h2) + 1))) - ((f /* r) . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
r . ((2 * h2) + 1) is V30() real ext-real Element of REAL
(q2 . ((2 * h2) + 1)) + (r . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
f . ((q2 . ((2 * h2) + 1)) + (r . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
(f . ((q2 . ((2 * h2) + 1)) + (r . ((2 * h2) + 1)))) - ((f /* r) . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
((g1 ") . h2) * ((f . ((q2 . ((2 * h2) + 1)) + (r . ((2 * h2) + 1)))) - ((f /* r) . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
(g1 . h2) + (r . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
f . ((g1 . h2) + (r . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
(f . ((g1 . h2) + (r . ((2 * h2) + 1)))) - ((f /* r) . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
((g1 ") . h2) * ((f . ((g1 . h2) + (r . ((2 * h2) + 1)))) - ((f /* r) . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
r . h2 is V30() real ext-real Element of REAL
(g1 . h2) + (r . h2) is V30() real ext-real Element of REAL
f . ((g1 . h2) + (r . h2)) is V30() real ext-real Element of REAL
(f . ((g1 . h2) + (r . h2))) - ((f /* r) . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
((g1 ") . h2) * ((f . ((g1 . h2) + (r . h2))) - ((f /* r) . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
(g1 + r) . h2 is V30() real ext-real Element of REAL
f . ((g1 + r) . h2) is V30() real ext-real Element of REAL
(f . ((g1 + r) . h2)) - ((f /* r) . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
((g1 ") . h2) * ((f . ((g1 + r) . h2)) - ((f /* r) . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
(f /* (g1 + r)) . h2 is V30() real ext-real Element of REAL
((f /* (g1 + r)) . h2) - ((f /* r) . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
((g1 ") . h2) * (((f /* (g1 + r)) . h2) - ((f /* r) . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
f . (r . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
((f /* (g1 + r)) . h2) - (f . (r . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
((g1 ") . h2) * (((f /* (g1 + r)) . h2) - (f . (r . ((2 * h2) + 1)))) is V30() real ext-real Element of REAL
f . (r . h2) is V30() real ext-real Element of REAL
((f /* (g1 + r)) . h2) - (f . (r . h2)) is V30() real ext-real Element of REAL
((g1 ") . h2) * (((f /* (g1 + r)) . h2) - (f . (r . h2))) is V30() real ext-real Element of REAL
(f /* r) . h2 is V30() real ext-real Element of REAL
((f /* (g1 + r)) . h2) - ((f /* r) . h2) is V30() real ext-real Element of REAL
((g1 ") . h2) * (((f /* (g1 + r)) . h2) - ((f /* r) . h2)) is V30() real ext-real Element of REAL
((f /* (g1 + r)) - (f /* r)) . h2 is V30() real ext-real Element of REAL
((g1 ") . h2) * (((f /* (g1 + r)) - (f /* r)) . h2) is V30() real ext-real Element of REAL
((g1 ") (#) ((f /* (g1 + r)) - (f /* r))) . h2 is V30() real ext-real Element of REAL
h2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
c2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
2 * c2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
(2 * c2) + 1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
q2 . (2 * c2) is V30() real ext-real Element of REAL
N . c2 is V30() real ext-real Element of REAL
q2 . h2 is V30() real ext-real Element of REAL
q2 . ((2 * c2) + 1) is V30() real ext-real Element of REAL
g1 . c2 is V30() real ext-real Element of REAL
q2 . h2 is V30() real ext-real Element of REAL
q2 . h2 is V30() real ext-real Element of REAL
q2 . h2 is V30() real ext-real Element of REAL
h2 is V1() V4( NAT ) V5( NAT ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) * h2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued subsequence of (q2 ") (#) ((f /* (q2 + r)) - (f /* r))
c2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
(((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) * h2) . c2 is V30() real ext-real Element of REAL
h2 . c2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) . (h2 . c2) is V30() real ext-real Element of REAL
2 * c2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) . (2 * c2) is V30() real ext-real Element of REAL
(q2 ") . (2 * c2) is V30() real ext-real Element of REAL
((f /* (q2 + r)) - (f /* r)) . (2 * c2) is V30() real ext-real Element of REAL
((q2 ") . (2 * c2)) * (((f /* (q2 + r)) - (f /* r)) . (2 * c2)) is V30() real ext-real Element of REAL
(f /* (q2 + r)) . (2 * c2) is V30() real ext-real Element of REAL
(f /* r) . (2 * c2) is V30() real ext-real Element of REAL
((f /* (q2 + r)) . (2 * c2)) - ((f /* r) . (2 * c2)) is V30() real ext-real Element of REAL
((q2 ") . (2 * c2)) * (((f /* (q2 + r)) . (2 * c2)) - ((f /* r) . (2 * c2))) is V30() real ext-real Element of REAL
q2 . (2 * c2) is V30() real ext-real Element of REAL
(q2 . (2 * c2)) " is V30() real ext-real Element of REAL
((q2 . (2 * c2)) ") * (((f /* (q2 + r)) . (2 * c2)) - ((f /* r) . (2 * c2))) is V30() real ext-real Element of REAL
N . c2 is V30() real ext-real Element of REAL
(N . c2) " is V30() real ext-real Element of REAL
((N . c2) ") * (((f /* (q2 + r)) . (2 * c2)) - ((f /* r) . (2 * c2))) is V30() real ext-real Element of REAL
(N ") . c2 is V30() real ext-real Element of REAL
((N ") . c2) * (((f /* (q2 + r)) . (2 * c2)) - ((f /* r) . (2 * c2))) is V30() real ext-real Element of REAL
(q2 + r) . (2 * c2) is V30() real ext-real Element of REAL
f . ((q2 + r) . (2 * c2)) is V30() real ext-real Element of REAL
(f . ((q2 + r) . (2 * c2))) - ((f /* r) . (2 * c2)) is V30() real ext-real Element of REAL
((N ") . c2) * ((f . ((q2 + r) . (2 * c2))) - ((f /* r) . (2 * c2))) is V30() real ext-real Element of REAL
r . (2 * c2) is V30() real ext-real Element of REAL
(q2 . (2 * c2)) + (r . (2 * c2)) is V30() real ext-real Element of REAL
f . ((q2 . (2 * c2)) + (r . (2 * c2))) is V30() real ext-real Element of REAL
(f . ((q2 . (2 * c2)) + (r . (2 * c2)))) - ((f /* r) . (2 * c2)) is V30() real ext-real Element of REAL
((N ") . c2) * ((f . ((q2 . (2 * c2)) + (r . (2 * c2)))) - ((f /* r) . (2 * c2))) is V30() real ext-real Element of REAL
(N . c2) + (r . (2 * c2)) is V30() real ext-real Element of REAL
f . ((N . c2) + (r . (2 * c2))) is V30() real ext-real Element of REAL
(f . ((N . c2) + (r . (2 * c2)))) - ((f /* r) . (2 * c2)) is V30() real ext-real Element of REAL
((N ") . c2) * ((f . ((N . c2) + (r . (2 * c2)))) - ((f /* r) . (2 * c2))) is V30() real ext-real Element of REAL
r . c2 is V30() real ext-real Element of REAL
(N . c2) + (r . c2) is V30() real ext-real Element of REAL
f . ((N . c2) + (r . c2)) is V30() real ext-real Element of REAL
(f . ((N . c2) + (r . c2))) - ((f /* r) . (2 * c2)) is V30() real ext-real Element of REAL
((N ") . c2) * ((f . ((N . c2) + (r . c2))) - ((f /* r) . (2 * c2))) is V30() real ext-real Element of REAL
(N + r) . c2 is V30() real ext-real Element of REAL
f . ((N + r) . c2) is V30() real ext-real Element of REAL
(f . ((N + r) . c2)) - ((f /* r) . (2 * c2)) is V30() real ext-real Element of REAL
((N ") . c2) * ((f . ((N + r) . c2)) - ((f /* r) . (2 * c2))) is V30() real ext-real Element of REAL
(f /* (N + r)) . c2 is V30() real ext-real Element of REAL
((f /* (N + r)) . c2) - ((f /* r) . (2 * c2)) is V30() real ext-real Element of REAL
((N ") . c2) * (((f /* (N + r)) . c2) - ((f /* r) . (2 * c2))) is V30() real ext-real Element of REAL
f . (r . (2 * c2)) is V30() real ext-real Element of REAL
((f /* (N + r)) . c2) - (f . (r . (2 * c2))) is V30() real ext-real Element of REAL
((N ") . c2) * (((f /* (N + r)) . c2) - (f . (r . (2 * c2)))) is V30() real ext-real Element of REAL
f . (r . c2) is V30() real ext-real Element of REAL
((f /* (N + r)) . c2) - (f . (r . c2)) is V30() real ext-real Element of REAL
((N ") . c2) * (((f /* (N + r)) . c2) - (f . (r . c2))) is V30() real ext-real Element of REAL
(f /* r) . c2 is V30() real ext-real Element of REAL
((f /* (N + r)) . c2) - ((f /* r) . c2) is V30() real ext-real Element of REAL
((N ") . c2) * (((f /* (N + r)) . c2) - ((f /* r) . c2)) is V30() real ext-real Element of REAL
((f /* (N + r)) - (f /* r)) . c2 is V30() real ext-real Element of REAL
((N ") . c2) * (((f /* (N + r)) - (f /* r)) . c2) is V30() real ext-real Element of REAL
((N ") (#) ((f /* (N + r)) - (f /* r))) . c2 is V30() real ext-real Element of REAL
lim ((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V71() V72() V73() Element of K19(REAL)
x0 is V30() real ext-real Element of REAL
{x0} is V51() V71() V72() V73() V99() V100() V101() set
N is V1() non-zero V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
N " is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
g1 is V1() non-zero V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
g1 " is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() constant V11() total quasi_total complex-valued ext-real-valued real-valued convergent Element of K19(K20(NAT,REAL))
rng r is V71() V72() V73() Element of K19(REAL)
N + r is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (N + r) is V71() V72() V73() Element of K19(REAL)
g1 + r is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (g1 + r) is V71() V72() V73() Element of K19(REAL)
f /* (N + r) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* r is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (N + r)) - (f /* r) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (f /* r) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
K116(1) is V30() real ext-real non positive set
K116(1) (#) (f /* r) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(f /* (N + r)) + (- (f /* r)) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(N ") (#) ((f /* (N + r)) - (f /* r)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((N ") (#) ((f /* (N + r)) - (f /* r))) is V30() real ext-real Element of REAL
f /* (g1 + r) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (g1 + r)) - (f /* r) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (g1 + r)) + (- (f /* r)) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(g1 ") (#) ((f /* (g1 + r)) - (f /* r)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((g1 ") (#) ((f /* (g1 + r)) - (f /* r))) is V30() real ext-real Element of REAL
q1 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
q2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
h1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
2 * h1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
(2 * h1) + 1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
q1 . q2 is V30() real ext-real Element of REAL
N . h1 is V30() real ext-real Element of REAL
q1 . q2 is V30() real ext-real Element of REAL
g1 . h1 is V30() real ext-real Element of REAL
q1 . q2 is V30() real ext-real Element of REAL
q1 . q2 is V30() real ext-real Element of REAL
lim g1 is V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V51() V55() V71() V72() V73() V74() V75() V76() V77() V99() V100() V101() V102() Element of REAL
lim N is V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V51() V55() V71() V72() V73() V74() V75() V76() V77() V99() V100() V101() V102() Element of REAL
lim q1 is V30() real ext-real Element of REAL
h1 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
h1 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
q2 is V1() non-zero V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
q2 + r is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (q2 + r) is V71() V72() V73() Element of K19(REAL)
h2 is set
c2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
(q2 + r) . c2 is V30() real ext-real Element of REAL
c2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
2 * c2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
(2 * c2) + 1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
q2 . (2 * c2) is V30() real ext-real Element of REAL
r . (2 * c2) is V30() real ext-real Element of REAL
(q2 . (2 * c2)) + (r . (2 * c2)) is V30() real ext-real Element of REAL
N . c2 is V30() real ext-real Element of REAL
(N . c2) + (r . (2 * c2)) is V30() real ext-real Element of REAL
r . c2 is V30() real ext-real Element of REAL
(N . c2) + (r . c2) is V30() real ext-real Element of REAL
(N + r) . c2 is V30() real ext-real Element of REAL
q2 . ((2 * c2) + 1) is V30() real ext-real Element of REAL
r . ((2 * c2) + 1) is V30() real ext-real Element of REAL
(q2 . ((2 * c2) + 1)) + (r . ((2 * c2) + 1)) is V30() real ext-real Element of REAL
g1 . c2 is V30() real ext-real Element of REAL
(g1 . c2) + (r . ((2 * c2) + 1)) is V30() real ext-real Element of REAL
r . c2 is V30() real ext-real Element of REAL
(g1 . c2) + (r . c2) is V30() real ext-real Element of REAL
(g1 + r) . c2 is V30() real ext-real Element of REAL
h2 is V1() V4( NAT ) V5( NAT ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
q2 " is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* (q2 + r) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (q2 + r)) - (f /* r) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (q2 + r)) + (- (f /* r)) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(q2 ") (#) ((f /* (q2 + r)) - (f /* r)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) * h2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued subsequence of (q2 ") (#) ((f /* (q2 + r)) - (f /* r))
h2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
(((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) * h2) . h2 is V30() real ext-real Element of REAL
h2 . h2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) . (h2 . h2) is V30() real ext-real Element of REAL
2 * h2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
(2 * h2) + 1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) . ((2 * h2) + 1) is V30() real ext-real Element of REAL
(q2 ") . ((2 * h2) + 1) is V30() real ext-real Element of REAL
((f /* (q2 + r)) - (f /* r)) . ((2 * h2) + 1) is V30() real ext-real Element of REAL
((q2 ") . ((2 * h2) + 1)) * (((f /* (q2 + r)) - (f /* r)) . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
q2 . ((2 * h2) + 1) is V30() real ext-real Element of REAL
(q2 . ((2 * h2) + 1)) " is V30() real ext-real Element of REAL
((q2 . ((2 * h2) + 1)) ") * (((f /* (q2 + r)) - (f /* r)) . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
g1 . h2 is V30() real ext-real Element of REAL
(g1 . h2) " is V30() real ext-real Element of REAL
((g1 . h2) ") * (((f /* (q2 + r)) - (f /* r)) . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
(g1 ") . h2 is V30() real ext-real Element of REAL
((g1 ") . h2) * (((f /* (q2 + r)) - (f /* r)) . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
(f /* (q2 + r)) . ((2 * h2) + 1) is V30() real ext-real Element of REAL
(f /* r) . ((2 * h2) + 1) is V30() real ext-real Element of REAL
((f /* (q2 + r)) . ((2 * h2) + 1)) - ((f /* r) . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
((g1 ") . h2) * (((f /* (q2 + r)) . ((2 * h2) + 1)) - ((f /* r) . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
(q2 + r) . ((2 * h2) + 1) is V30() real ext-real Element of REAL
f . ((q2 + r) . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
(f . ((q2 + r) . ((2 * h2) + 1))) - ((f /* r) . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
((g1 ") . h2) * ((f . ((q2 + r) . ((2 * h2) + 1))) - ((f /* r) . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
r . ((2 * h2) + 1) is V30() real ext-real Element of REAL
f . (r . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
(f . ((q2 + r) . ((2 * h2) + 1))) - (f . (r . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
((g1 ") . h2) * ((f . ((q2 + r) . ((2 * h2) + 1))) - (f . (r . ((2 * h2) + 1)))) is V30() real ext-real Element of REAL
(q2 . ((2 * h2) + 1)) + (r . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
f . ((q2 . ((2 * h2) + 1)) + (r . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
(f . ((q2 . ((2 * h2) + 1)) + (r . ((2 * h2) + 1)))) - (f . (r . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
((g1 ") . h2) * ((f . ((q2 . ((2 * h2) + 1)) + (r . ((2 * h2) + 1)))) - (f . (r . ((2 * h2) + 1)))) is V30() real ext-real Element of REAL
(g1 . h2) + (r . ((2 * h2) + 1)) is V30() real ext-real Element of REAL
f . ((g1 . h2) + (r . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
(f . ((g1 . h2) + (r . ((2 * h2) + 1)))) - (f . (r . ((2 * h2) + 1))) is V30() real ext-real Element of REAL
((g1 ") . h2) * ((f . ((g1 . h2) + (r . ((2 * h2) + 1)))) - (f . (r . ((2 * h2) + 1)))) is V30() real ext-real Element of REAL
r . h2 is V30() real ext-real Element of REAL
f . (r . h2) is V30() real ext-real Element of REAL
(f . ((g1 . h2) + (r . ((2 * h2) + 1)))) - (f . (r . h2)) is V30() real ext-real Element of REAL
((g1 ") . h2) * ((f . ((g1 . h2) + (r . ((2 * h2) + 1)))) - (f . (r . h2))) is V30() real ext-real Element of REAL
(g1 . h2) + (r . h2) is V30() real ext-real Element of REAL
f . ((g1 . h2) + (r . h2)) is V30() real ext-real Element of REAL
(f . ((g1 . h2) + (r . h2))) - (f . (r . h2)) is V30() real ext-real Element of REAL
((g1 ") . h2) * ((f . ((g1 . h2) + (r . h2))) - (f . (r . h2))) is V30() real ext-real Element of REAL
(g1 + r) . h2 is V30() real ext-real Element of REAL
f . ((g1 + r) . h2) is V30() real ext-real Element of REAL
(f . ((g1 + r) . h2)) - (f . (r . h2)) is V30() real ext-real Element of REAL
((g1 ") . h2) * ((f . ((g1 + r) . h2)) - (f . (r . h2))) is V30() real ext-real Element of REAL
(f /* (g1 + r)) . h2 is V30() real ext-real Element of REAL
((f /* (g1 + r)) . h2) - (f . (r . h2)) is V30() real ext-real Element of REAL
((g1 ") . h2) * (((f /* (g1 + r)) . h2) - (f . (r . h2))) is V30() real ext-real Element of REAL
(f /* r) . h2 is V30() real ext-real Element of REAL
((f /* (g1 + r)) . h2) - ((f /* r) . h2) is V30() real ext-real Element of REAL
((g1 ") . h2) * (((f /* (g1 + r)) . h2) - ((f /* r) . h2)) is V30() real ext-real Element of REAL
((f /* (g1 + r)) - (f /* r)) . h2 is V30() real ext-real Element of REAL
((g1 ") . h2) * (((f /* (g1 + r)) - (f /* r)) . h2) is V30() real ext-real Element of REAL
((g1 ") (#) ((f /* (g1 + r)) - (f /* r))) . h2 is V30() real ext-real Element of REAL
h2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
q2 . h2 is V30() real ext-real Element of REAL
c2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
2 * c2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
(2 * c2) + 1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
N . c2 is V30() real ext-real Element of REAL
g1 . c2 is V30() real ext-real Element of REAL
h2 is V1() V4( NAT ) V5( NAT ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) * h2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued subsequence of (q2 ") (#) ((f /* (q2 + r)) - (f /* r))
c2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
(((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) * h2) . c2 is V30() real ext-real Element of REAL
h2 . c2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) . (h2 . c2) is V30() real ext-real Element of REAL
2 * c2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) . (2 * c2) is V30() real ext-real Element of REAL
(q2 ") . (2 * c2) is V30() real ext-real Element of REAL
((f /* (q2 + r)) - (f /* r)) . (2 * c2) is V30() real ext-real Element of REAL
((q2 ") . (2 * c2)) * (((f /* (q2 + r)) - (f /* r)) . (2 * c2)) is V30() real ext-real Element of REAL
q2 . (2 * c2) is V30() real ext-real Element of REAL
(q2 . (2 * c2)) " is V30() real ext-real Element of REAL
((q2 . (2 * c2)) ") * (((f /* (q2 + r)) - (f /* r)) . (2 * c2)) is V30() real ext-real Element of REAL
N . c2 is V30() real ext-real Element of REAL
(N . c2) " is V30() real ext-real Element of REAL
((N . c2) ") * (((f /* (q2 + r)) - (f /* r)) . (2 * c2)) is V30() real ext-real Element of REAL
(N ") . c2 is V30() real ext-real Element of REAL
((N ") . c2) * (((f /* (q2 + r)) - (f /* r)) . (2 * c2)) is V30() real ext-real Element of REAL
(f /* (q2 + r)) . (2 * c2) is V30() real ext-real Element of REAL
(f /* r) . (2 * c2) is V30() real ext-real Element of REAL
((f /* (q2 + r)) . (2 * c2)) - ((f /* r) . (2 * c2)) is V30() real ext-real Element of REAL
((N ") . c2) * (((f /* (q2 + r)) . (2 * c2)) - ((f /* r) . (2 * c2))) is V30() real ext-real Element of REAL
(q2 + r) . (2 * c2) is V30() real ext-real Element of REAL
f . ((q2 + r) . (2 * c2)) is V30() real ext-real Element of REAL
(f . ((q2 + r) . (2 * c2))) - ((f /* r) . (2 * c2)) is V30() real ext-real Element of REAL
((N ") . c2) * ((f . ((q2 + r) . (2 * c2))) - ((f /* r) . (2 * c2))) is V30() real ext-real Element of REAL
r . (2 * c2) is V30() real ext-real Element of REAL
f . (r . (2 * c2)) is V30() real ext-real Element of REAL
(f . ((q2 + r) . (2 * c2))) - (f . (r . (2 * c2))) is V30() real ext-real Element of REAL
((N ") . c2) * ((f . ((q2 + r) . (2 * c2))) - (f . (r . (2 * c2)))) is V30() real ext-real Element of REAL
(q2 . (2 * c2)) + (r . (2 * c2)) is V30() real ext-real Element of REAL
f . ((q2 . (2 * c2)) + (r . (2 * c2))) is V30() real ext-real Element of REAL
(f . ((q2 . (2 * c2)) + (r . (2 * c2)))) - (f . (r . (2 * c2))) is V30() real ext-real Element of REAL
((N ") . c2) * ((f . ((q2 . (2 * c2)) + (r . (2 * c2)))) - (f . (r . (2 * c2)))) is V30() real ext-real Element of REAL
(N . c2) + (r . (2 * c2)) is V30() real ext-real Element of REAL
f . ((N . c2) + (r . (2 * c2))) is V30() real ext-real Element of REAL
(f . ((N . c2) + (r . (2 * c2)))) - (f . (r . (2 * c2))) is V30() real ext-real Element of REAL
((N ") . c2) * ((f . ((N . c2) + (r . (2 * c2)))) - (f . (r . (2 * c2)))) is V30() real ext-real Element of REAL
r . c2 is V30() real ext-real Element of REAL
f . (r . c2) is V30() real ext-real Element of REAL
(f . ((N . c2) + (r . (2 * c2)))) - (f . (r . c2)) is V30() real ext-real Element of REAL
((N ") . c2) * ((f . ((N . c2) + (r . (2 * c2)))) - (f . (r . c2))) is V30() real ext-real Element of REAL
(N . c2) + (r . c2) is V30() real ext-real Element of REAL
f . ((N . c2) + (r . c2)) is V30() real ext-real Element of REAL
(f . ((N . c2) + (r . c2))) - (f . (r . c2)) is V30() real ext-real Element of REAL
((N ") . c2) * ((f . ((N . c2) + (r . c2))) - (f . (r . c2))) is V30() real ext-real Element of REAL
(N + r) . c2 is V30() real ext-real Element of REAL
f . ((N + r) . c2) is V30() real ext-real Element of REAL
(f . ((N + r) . c2)) - (f . (r . c2)) is V30() real ext-real Element of REAL
((N ") . c2) * ((f . ((N + r) . c2)) - (f . (r . c2))) is V30() real ext-real Element of REAL
(f /* (N + r)) . c2 is V30() real ext-real Element of REAL
((f /* (N + r)) . c2) - (f . (r . c2)) is V30() real ext-real Element of REAL
((N ") . c2) * (((f /* (N + r)) . c2) - (f . (r . c2))) is V30() real ext-real Element of REAL
(f /* r) . c2 is V30() real ext-real Element of REAL
((f /* (N + r)) . c2) - ((f /* r) . c2) is V30() real ext-real Element of REAL
((N ") . c2) * (((f /* (N + r)) . c2) - ((f /* r) . c2)) is V30() real ext-real Element of REAL
((f /* (N + r)) - (f /* r)) . c2 is V30() real ext-real Element of REAL
((N ") . c2) * (((f /* (N + r)) - (f /* r)) . c2) is V30() real ext-real Element of REAL
((N ") (#) ((f /* (N + r)) - (f /* r))) . c2 is V30() real ext-real Element of REAL
lim ((q2 ") (#) ((f /* (q2 + r)) - (f /* r))) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x0 is V30() real ext-real Element of REAL
left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)
K220(-infty,x0) is V97() V98() V102() set
dom f is V71() V72() V73() Element of K19(REAL)
(left_open_halfline x0) /\ (dom f) is V71() V72() V73() Element of K19(REAL)
f . x0 is V30() real ext-real Element of REAL
NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant V11() total quasi_total complex-valued ext-real-valued real-valued convergent Element of K19(K20(NAT,REAL))
g1 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng g1 is V71() V72() V73() Element of K19(REAL)
lim g1 is V30() real ext-real Element of REAL
f /* g1 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* g1) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
x0 - r is V30() real ext-real Element of REAL
[.(x0 - r),x0.] is V71() V72() V73() V102() Element of K19(REAL)
q1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
N is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
q2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
g1 - N is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- N is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
K116(1) is V30() real ext-real non positive set
K116(1) (#) N is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
g1 + (- N) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
N ^\ q1 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total complex-valued ext-real-valued real-valued subsequence of N
h1 is V1() V4( NAT ) V5( REAL ) V6() constant V11() total quasi_total complex-valued ext-real-valued real-valued convergent Element of K19(K20(NAT,REAL))
rng h1 is V71() V72() V73() Element of K19(REAL)
{x0} is V51() V71() V72() V73() V99() V100() V101() set
h1 is set
h2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
(N ^\ q1) . h2 is V30() real ext-real Element of REAL
h2 + q1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V71() V72() V73() V74() V75() V76() V91() V92() V99() Element of NAT
N . (h2 + q1) is