:: ASYMPT_1 semantic presentation

REAL is non empty V49() V50() V51() V55() V56() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V49() V50() V51() V52() V53() V54() V55() Element of K19(REAL)
K19(REAL) is non empty set
COMPLEX is non empty V49() V55() V56() set
RAT is non empty V49() V50() V51() V52() V55() V56() set
INT is non empty V49() V50() V51() V52() V53() V55() V56() set
omega is non empty epsilon-transitive epsilon-connected ordinal V49() V50() V51() V52() V53() V54() V55() set
K19(omega) is non empty set
K19(NAT) is non empty set
K20(REAL,REAL) is non empty V35() V36() V37() set
K19(K20(REAL,REAL)) is non empty set
K20(NAT,REAL) is non empty V35() V36() V37() set
K19(K20(NAT,REAL)) is non empty set
K20(COMPLEX,COMPLEX) is non empty V35() set
K19(K20(COMPLEX,COMPLEX)) is non empty set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is non empty V35() set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K20(K20(REAL,REAL),REAL) is non empty V35() V36() V37() set
K19(K20(K20(REAL,REAL),REAL)) is non empty set
K20(RAT,RAT) is V5( RAT ) non empty V35() V36() V37() set
K19(K20(RAT,RAT)) is non empty set
K20(K20(RAT,RAT),RAT) is V5( RAT ) non empty V35() V36() V37() set
K19(K20(K20(RAT,RAT),RAT)) is non empty set
K20(INT,INT) is V5( RAT ) V5( INT ) non empty V35() V36() V37() set
K19(K20(INT,INT)) is non empty set
K20(K20(INT,INT),INT) is V5( RAT ) V5( INT ) non empty V35() V36() V37() set
K19(K20(K20(INT,INT),INT)) is non empty set
K20(NAT,NAT) is V5( RAT ) V5( INT ) non empty V35() V36() V37() V38() set
K20(K20(NAT,NAT),NAT) is V5( RAT ) V5( INT ) non empty V35() V36() V37() V38() set
K19(K20(K20(NAT,NAT),NAT)) is non empty set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
0 is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V25() real ext-real non positive non negative integer V48() V49() V50() V51() V52() V53() V54() V55() FinSequence-membered Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
{} is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V25() real ext-real non positive non negative integer V49() V50() V51() V52() V53() V54() V55() FinSequence-membered set
- 1 is V25() real ext-real non positive integer Element of REAL
sqrt 0 is V25() real ext-real Element of REAL
2 to_power 3 is V25() real ext-real Element of REAL
2 |^ 3 is set
8 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 to_power 4 is V25() real ext-real Element of REAL
2 |^ 4 is set
16 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 to_power 5 is V25() real ext-real Element of REAL
2 |^ 5 is set
32 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
6 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 to_power 6 is V25() real ext-real Element of REAL
2 |^ 6 is set
64 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
0 ! is V25() real ext-real Element of REAL
1 ! is V25() real ext-real Element of REAL
2 ! is V25() real ext-real Element of REAL
Funcs (NAT,REAL) is functional non empty FUNCTION_DOMAIN of NAT , REAL
c is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
2 to_power c is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 |^ c is set
c + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 to_power (c + 1) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 |^ (c + 1) is set
(c + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 to_power 1 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 |^ 1 is set
(2 to_power c) * (2 to_power 1) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(2 to_power c) * 2 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(2 to_power c) + (2 to_power c) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(c + 1) + (2 to_power c) is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 to_power x is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 |^ x is set
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(x + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(x + 1) + (2 to_power x) is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 to_power 2 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 |^ 2 is set
2 ^2 is V25() real ext-real Element of REAL
2 * 2 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
c is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
2 to_power c is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 |^ c is set
c + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
12 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
36 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
c is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
log (2,c) is V25() real ext-real Element of REAL
(log (2,c)) ^2 is V25() real ext-real Element of REAL
(log (2,c)) * (log (2,c)) is V25() real ext-real set
((log (2,c)) ^2) + 36 is V25() real ext-real Element of REAL
c is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
c . 0 is V25() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
c . x is V25() real ext-real Element of REAL
log (2,x) is V25() real ext-real Element of REAL
(log (2,x)) ^2 is V25() real ext-real Element of REAL
(log (2,x)) * (log (2,x)) is V25() real ext-real set
((log (2,x)) ^2) + 36 is V25() real ext-real Element of REAL
c is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
c . 0 is V25() real ext-real Element of REAL
c is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
c . 0 is V25() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
c . x is V25() real ext-real Element of REAL
log (2,x) is V25() real ext-real Element of REAL
(log (2,x)) ^2 is V25() real ext-real Element of REAL
(log (2,x)) * (log (2,x)) is V25() real ext-real set
((log (2,x)) ^2) + 36 is V25() real ext-real Element of REAL
0 + 0 is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V25() real ext-real non positive non negative integer V48() V49() V50() V51() V52() V53() V54() V55() FinSequence-membered Element of NAT
f is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
f . 0 is V25() real ext-real Element of REAL
e is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
N0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
e . N0 is V25() real ext-real Element of REAL
log (2,2) is V25() real ext-real Element of REAL
log (2,N0) is V25() real ext-real Element of REAL
N0 to_power 3 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
N0 |^ 3 is set
(N0 to_power 3) * (log (2,N0)) is V25() real ext-real Element of REAL
(N0 to_power 3) * 0 is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V25() real ext-real non positive non negative integer V48() V49() V50() V51() V52() V53() V54() V55() FinSequence-membered Element of NAT
2 ^2 is V25() real ext-real Element of REAL
2 * 2 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
2 to_power 2 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 |^ 2 is set
log (2,4) is V25() real ext-real Element of REAL
log (2,2) is V25() real ext-real Element of REAL
2 * (log (2,2)) is V25() real ext-real Element of REAL
2 * 1 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
7 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
x is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() eventually-nonnegative eventually-positive eventually-nonzero Element of K19(K20(NAT,REAL))
N0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
N0 ^2 is V25() real ext-real set
N0 * N0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
7 * (N0 ^2) is V25() real ext-real Element of REAL
x . N0 is V25() real ext-real Element of REAL
N0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(N0 + 1) ^2 is V25() real ext-real set
(N0 + 1) * (N0 + 1) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
7 * ((N0 + 1) ^2) is V25() real ext-real Element of REAL
x . (N0 + 1) is V25() real ext-real Element of REAL
log (2,(N0 + 1)) is V25() real ext-real Element of REAL
(log (2,(N0 + 1))) ^2 is V25() real ext-real Element of REAL
(log (2,(N0 + 1))) * (log (2,(N0 + 1))) is V25() real ext-real set
((log (2,(N0 + 1))) ^2) + 36 is V25() real ext-real Element of REAL
2 to_power N0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 |^ N0 is set
N0 + 0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
log (2,(2 to_power N0)) is V25() real ext-real Element of REAL
log (2,N0) is V25() real ext-real set
N0 * (log (2,2)) is V25() real ext-real Element of REAL
N0 * 1 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
14 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
14 * N0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 * (log (2,N0)) is V25() real ext-real Element of REAL
7 * 2 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(7 * 2) * N0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
((7 * 2) * N0) + 7 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(2 * (log (2,N0))) + 1 is V25() real ext-real Element of REAL
(log (2,N0)) ^2 is V25() real ext-real set
(log (2,N0)) * (log (2,N0)) is V25() real ext-real set
2 * N0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
7 * (2 * N0) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(7 * (2 * N0)) + 7 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
((log (2,N0)) ^2) + ((7 * (2 * N0)) + 7) is V25() real ext-real Element of REAL
((log (2,N0)) ^2) + ((2 * (log (2,N0))) + 1) is V25() real ext-real Element of REAL
N0 + N0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
log (2,(N0 + N0)) is V25() real ext-real set
log (2,(2 * N0)) is V25() real ext-real Element of REAL
(log (2,N0)) + (log (2,2)) is V25() real ext-real Element of REAL
(log (2,(N0 + N0))) ^2 is V25() real ext-real set
(log (2,(N0 + N0))) * (log (2,(N0 + N0))) is V25() real ext-real set
(log (2,N0)) + 1 is V25() real ext-real Element of REAL
((log (2,N0)) + 1) ^2 is V25() real ext-real Element of REAL
((log (2,N0)) + 1) * ((log (2,N0)) + 1) is V25() real ext-real set
((log (2,N0)) ^2) + (2 * (log (2,N0))) is V25() real ext-real Element of REAL
(((log (2,N0)) ^2) + (2 * (log (2,N0)))) + 1 is V25() real ext-real Element of REAL
(((log (2,N0)) ^2) + ((7 * (2 * N0)) + 7)) + 36 is V25() real ext-real Element of REAL
((log (2,(N0 + N0))) ^2) + 36 is V25() real ext-real Element of REAL
4 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(N0 + 1) ^2 is V25() real ext-real Element of REAL
7 * ((N0 + 1) ^2) is V25() real ext-real Element of REAL
7 * 1 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(7 * (2 * N0)) + (7 * 1) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(7 * (N0 ^2)) + ((7 * (2 * N0)) + (7 * 1)) is V25() real ext-real Element of REAL
(x . N0) + ((7 * (2 * N0)) + (7 * 1)) is V25() real ext-real Element of REAL
((log (2,N0)) ^2) + 36 is V25() real ext-real Element of REAL
x . 4 is V25() real ext-real Element of REAL
(2 ^2) + 36 is V25() real ext-real Element of REAL
40 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
4 ^2 is V25() real ext-real set
4 * 4 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
7 * (4 ^2) is V25() real ext-real Element of REAL
N0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
N0 ^2 is V25() real ext-real Element of REAL
N0 * N0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
7 * (N0 ^2) is V25() real ext-real Element of REAL
x . N0 is V25() real ext-real Element of REAL
log (2,3) is V25() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
f . t is V25() real ext-real Element of REAL
t to_power 2 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
t |^ 2 is set
t to_power 3 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
t |^ 3 is set
log (2,t) is V25() real ext-real Element of REAL
(t to_power 3) * (log (2,t)) is V25() real ext-real Element of REAL
(t to_power 2) * 1 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
12 * ((t to_power 3) * (log (2,t))) is V25() real ext-real Element of REAL
5 * (t to_power 2) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
12 * (t to_power 3) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(12 * (t to_power 3)) * (log (2,t)) is V25() real ext-real Element of REAL
t ^2 is V25() real ext-real Element of REAL
t * t is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
5 * (t ^2) is V25() real ext-real Element of REAL
(5 * (t ^2)) + 0 is V25() real ext-real Element of REAL
((12 * (t to_power 3)) * (log (2,t))) - (5 * (t ^2)) is V25() real ext-real Element of REAL
- (5 * (t ^2)) is V25() real ext-real set
((12 * (t to_power 3)) * (log (2,t))) + (- (5 * (t ^2))) is V25() real ext-real set
(log (2,t)) ^2 is V25() real ext-real Element of REAL
(log (2,t)) * (log (2,t)) is V25() real ext-real set
(((12 * (t to_power 3)) * (log (2,t))) - (5 * (t ^2))) + ((log (2,t)) ^2) is V25() real ext-real Element of REAL
0 + 0 is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V25() real ext-real non positive non negative integer V48() V49() V50() V51() V52() V53() V54() V55() FinSequence-membered Element of NAT
((((12 * (t to_power 3)) * (log (2,t))) - (5 * (t ^2))) + ((log (2,t)) ^2)) + 36 is V25() real ext-real Element of REAL
t is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() eventually-nonnegative eventually-positive eventually-nonzero Element of K19(K20(NAT,REAL))
N0 is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() eventually-nonnegative eventually-positive eventually-nonzero Element of K19(K20(NAT,REAL))
Big_Oh N0 is functional non empty FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V1() V4( NAT ) V5( REAL ) Function-like V14( NAT ) quasi_total V35() V36() V37() Element of Funcs (NAT,REAL) : ex b₂ being V25() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (N0 . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
d is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
d to_power 3 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
d |^ 3 is set
12 * (d to_power 3) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
log (2,d) is V25() real ext-real Element of REAL
(12 * (d to_power 3)) * (log (2,d)) is V25() real ext-real Element of REAL
d ^2 is V25() real ext-real Element of REAL
d * d is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
5 * (d ^2) is V25() real ext-real Element of REAL
((12 * (d to_power 3)) * (log (2,d))) - (5 * (d ^2)) is V25() real ext-real Element of REAL
- (5 * (d ^2)) is V25() real ext-real set
((12 * (d to_power 3)) * (log (2,d))) + (- (5 * (d ^2))) is V25() real ext-real set
d is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
d . 0 is V25() real ext-real Element of REAL
N1 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
d . N1 is V25() real ext-real Element of REAL
N1 to_power 3 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
N1 |^ 3 is set
12 * (N1 to_power 3) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
log (2,N1) is V25() real ext-real Element of REAL
(12 * (N1 to_power 3)) * (log (2,N1)) is V25() real ext-real Element of REAL
N1 ^2 is V25() real ext-real Element of REAL
N1 * N1 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
5 * (N1 ^2) is V25() real ext-real Element of REAL
((12 * (N1 to_power 3)) * (log (2,N1))) - (5 * (N1 ^2)) is V25() real ext-real Element of REAL
- (5 * (N1 ^2)) is V25() real ext-real set
((12 * (N1 to_power 3)) * (log (2,N1))) + (- (5 * (N1 ^2))) is V25() real ext-real set
d is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
d . 0 is V25() real ext-real Element of REAL
d is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
d . 0 is V25() real ext-real Element of REAL
log (2,3) is V25() real ext-real Element of REAL
N1 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
d . N1 is V25() real ext-real Element of REAL
N1 to_power 2 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
N1 |^ 2 is set
N1 to_power 3 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
N1 |^ 3 is set
log (2,N1) is V25() real ext-real Element of REAL
(N1 to_power 3) * (log (2,N1)) is V25() real ext-real Element of REAL
(N1 to_power 2) * 1 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
12 * ((N1 to_power 3) * (log (2,N1))) is V25() real ext-real Element of REAL
5 * (N1 to_power 2) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
12 * (N1 to_power 3) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(12 * (N1 to_power 3)) * (log (2,N1)) is V25() real ext-real Element of REAL
N1 ^2 is V25() real ext-real Element of REAL
N1 * N1 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
5 * (N1 ^2) is V25() real ext-real Element of REAL
(5 * (N1 ^2)) + 0 is V25() real ext-real Element of REAL
((12 * (N1 to_power 3)) * (log (2,N1))) - (5 * (N1 ^2)) is V25() real ext-real Element of REAL
- (5 * (N1 ^2)) is V25() real ext-real set
((12 * (N1 to_power 3)) * (log (2,N1))) + (- (5 * (N1 ^2))) is V25() real ext-real set
N1 is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() eventually-nonnegative eventually-positive eventually-nonzero Element of K19(K20(NAT,REAL))
max (N1,x) is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() eventually-nonnegative eventually-positive eventually-nonzero Element of K19(K20(NAT,REAL))
N is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
N1 . n is V25() real ext-real Element of REAL
n ^2 is V25() real ext-real Element of REAL
n * n is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
7 * (n ^2) is V25() real ext-real Element of REAL
n to_power 3 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
n |^ 3 is set
n to_power 2 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
n |^ 2 is set
log (2,n) is V25() real ext-real Element of REAL
(n to_power 3) * (log (2,n)) is V25() real ext-real Element of REAL
(n to_power 2) * 1 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
12 * ((n to_power 3) * (log (2,n))) is V25() real ext-real Element of REAL
12 * (n to_power 2) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
12 * (n to_power 3) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(12 * (n to_power 3)) * (log (2,n)) is V25() real ext-real Element of REAL
12 * (n ^2) is V25() real ext-real Element of REAL
5 * (n ^2) is V25() real ext-real Element of REAL
((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) is V25() real ext-real Element of REAL
- (5 * (n ^2)) is V25() real ext-real set
((12 * (n to_power 3)) * (log (2,n))) + (- (5 * (n ^2))) is V25() real ext-real set
(12 * (n ^2)) - (5 * (n ^2)) is V25() real ext-real Element of REAL
(12 * (n ^2)) + (- (5 * (n ^2))) is V25() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
N1 . n is V25() real ext-real Element of REAL
x . n is V25() real ext-real Element of REAL
n ^2 is V25() real ext-real Element of REAL
n * n is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
7 * (n ^2) is V25() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(max (N1,x)) . n is V25() real ext-real Element of REAL
N1 . n is V25() real ext-real Element of REAL
x . n is V25() real ext-real Element of REAL
max ((N1 . n),(x . n)) is V25() real ext-real Element of REAL
max (4,N) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(max (N1,x)) . n is V25() real ext-real Element of REAL
N1 . n is V25() real ext-real Element of REAL
n to_power 3 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
n |^ 3 is set
12 * (n to_power 3) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
log (2,n) is V25() real ext-real Element of REAL
(12 * (n to_power 3)) * (log (2,n)) is V25() real ext-real Element of REAL
n ^2 is V25() real ext-real Element of REAL
n * n is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
5 * (n ^2) is V25() real ext-real Element of REAL
((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) is V25() real ext-real Element of REAL
- (5 * (n ^2)) is V25() real ext-real set
((12 * (n to_power 3)) * (log (2,n))) + (- (5 * (n ^2))) is V25() real ext-real set
((12 * (n to_power 3)) * (log (2,n))) - 0 is V25() real ext-real Element of REAL
- 0 is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V25() real ext-real non positive non negative integer V49() V50() V51() V52() V53() V54() V55() FinSequence-membered set
((12 * (n to_power 3)) * (log (2,n))) + (- 0) is V25() real ext-real set
(n to_power 3) * (log (2,n)) is V25() real ext-real Element of REAL
12 * ((n to_power 3) * (log (2,n))) is V25() real ext-real Element of REAL
N0 . n is V25() real ext-real Element of REAL
12 * (N0 . n) is V25() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
t . n is V25() real ext-real Element of REAL
N1 . n is V25() real ext-real Element of REAL
x . n is V25() real ext-real Element of REAL
(N1 . n) + (x . n) is V25() real ext-real Element of REAL
n to_power 3 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
n |^ 3 is set
12 * (n to_power 3) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
log (2,n) is V25() real ext-real Element of REAL
(12 * (n to_power 3)) * (log (2,n)) is V25() real ext-real Element of REAL
n ^2 is V25() real ext-real Element of REAL
n * n is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
5 * (n ^2) is V25() real ext-real Element of REAL
((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) is V25() real ext-real Element of REAL
- (5 * (n ^2)) is V25() real ext-real set
((12 * (n to_power 3)) * (log (2,n))) + (- (5 * (n ^2))) is V25() real ext-real set
(log (2,n)) ^2 is V25() real ext-real Element of REAL
(log (2,n)) * (log (2,n)) is V25() real ext-real set
((log (2,n)) ^2) + 36 is V25() real ext-real Element of REAL
(((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + (((log (2,n)) ^2) + 36) is V25() real ext-real Element of REAL
(((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + ((log (2,n)) ^2) is V25() real ext-real Element of REAL
((((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + ((log (2,n)) ^2)) + 36 is V25() real ext-real Element of REAL
Big_Oh t is functional non empty FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V1() V4( NAT ) V5( REAL ) Function-like V14( NAT ) quasi_total V35() V36() V37() Element of Funcs (NAT,REAL) : ex b₂ being V25() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (t . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
N1 + x is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() eventually-nonnegative Element of K19(K20(NAT,REAL))
Big_Oh (N1 + x) is functional non empty FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V1() V4( NAT ) V5( REAL ) Function-like V14( NAT ) quasi_total V35() V36() V37() Element of Funcs (NAT,REAL) : ex b₂ being V25() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * ((N1 + x) . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
Big_Oh (max (N1,x)) is functional non empty FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V1() V4( NAT ) V5( REAL ) Function-like V14( NAT ) quasi_total V35() V36() V37() Element of Funcs (NAT,REAL) : ex b₂ being V25() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * ((max (N1,x)) . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
c is V25() real ext-real logbase Element of REAL
x is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
[/c\] is V25() real ext-real integer set
log (c,c) is V25() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
log (c,e) is V25() real ext-real Element of REAL
e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
N0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
e + 0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
log (c,N0) is V25() real ext-real Element of REAL
x . N0 is V25() real ext-real Element of REAL
c is V25() real ext-real logbase Element of REAL
x is V25() real ext-real logbase Element of REAL
f is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
e is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
t is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() eventually-nonnegative eventually-positive eventually-nonzero Element of K19(K20(NAT,REAL))
Big_Oh t is functional non empty FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V1() V4( NAT ) V5( REAL ) Function-like V14( NAT ) quasi_total V35() V36() V37() Element of Funcs (NAT,REAL) : ex b₂ being V25() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (t . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
N0 is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() eventually-nonnegative eventually-positive eventually-nonzero Element of K19(K20(NAT,REAL))
Big_Oh N0 is functional non empty FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V1() V4( NAT ) V5( REAL ) Function-like V14( NAT ) quasi_total V35() V36() V37() Element of Funcs (NAT,REAL) : ex b₂ being V25() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (N0 . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
d is set
N1 is V1() V4( NAT ) V5( REAL ) Function-like V14( NAT ) quasi_total V35() V36() V37() Element of Funcs (NAT,REAL)
b is V25() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
b is V25() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
N + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
g9 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
t . g9 is V25() real ext-real Element of REAL
log (c,g9) is V25() real ext-real Element of REAL
log (c,x) is V25() real ext-real Element of REAL
log (x,g9) is V25() real ext-real Element of REAL
(log (c,x)) * (log (x,g9)) is V25() real ext-real Element of REAL
N + 0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
N1 . g9 is V25() real ext-real Element of REAL
b * (t . g9) is V25() real ext-real Element of REAL
b * (log (c,x)) is V25() real ext-real Element of REAL
(b * (log (c,x))) * (log (x,g9)) is V25() real ext-real Element of REAL
N0 . g9 is V25() real ext-real Element of REAL
(b * (log (c,x))) * (N0 . g9) is V25() real ext-real Element of REAL
log (c,1) is V25() real ext-real Element of REAL
b * 0 is V25() real ext-real Element of REAL
n is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
N1 is V1() V4( NAT ) V5( REAL ) Function-like V14( NAT ) quasi_total V35() V36() V37() Element of Funcs (NAT,REAL)
b is V25() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
b is V25() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
N + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
g9 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
N0 . g9 is V25() real ext-real Element of REAL
log (x,g9) is V25() real ext-real Element of REAL
log (x,c) is V25() real ext-real Element of REAL
log (c,g9) is V25() real ext-real Element of REAL
(log (x,c)) * (log (c,g9)) is V25() real ext-real Element of REAL
N + 0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
N1 . g9 is V25() real ext-real Element of REAL
b * (N0 . g9) is V25() real ext-real Element of REAL
b * (log (x,c)) is V25() real ext-real Element of REAL
(b * (log (x,c))) * (log (c,g9)) is V25() real ext-real Element of REAL
t . g9 is V25() real ext-real Element of REAL
(b * (log (x,c))) * (t . g9) is V25() real ext-real Element of REAL
log (x,1) is V25() real ext-real Element of REAL
b * 0 is V25() real ext-real Element of REAL
n is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
c is V25() real ext-real Element of REAL
x is V25() real ext-real Element of REAL
f is V25() real ext-real Element of REAL
e is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
N0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
e . N0 is V25() real ext-real Element of REAL
x * N0 is V25() real ext-real Element of REAL
(x * N0) + f is V25() real ext-real Element of REAL
c to_power ((x * N0) + f) is V25() real ext-real Element of REAL
e is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
N0 is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
t is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
e . t is V25() real ext-real Element of REAL
x * t is V25() real ext-real Element of REAL
(x * t) + f is V25() real ext-real Element of REAL
c to_power ((x * t) + f) is V25() real ext-real Element of REAL
N0 . t is V25() real ext-real Element of REAL
c is non empty V25() real ext-real positive non negative Element of REAL
x is V25() real ext-real Element of REAL
f is V25() real ext-real Element of REAL
(c,x,f) is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
N0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(c,x,f) . N0 is V25() real ext-real Element of REAL
x * N0 is V25() real ext-real Element of REAL
(x * N0) + f is V25() real ext-real Element of REAL
c to_power ((x * N0) + f) is V25() real ext-real Element of REAL
c is V25() real ext-real Element of REAL
f is V25() real ext-real Element of REAL
x is V25() real ext-real Element of REAL
c to_power x is V25() real ext-real Element of REAL
log (f,c) is V25() real ext-real Element of REAL
x * (log (f,c)) is V25() real ext-real Element of REAL
f to_power (x * (log (f,c))) is V25() real ext-real Element of REAL
log (f,(c to_power x)) is V25() real ext-real Element of REAL
x is non empty V25() real ext-real positive non negative Element of REAL
c is non empty V25() real ext-real positive non negative Element of REAL
(x,1,0) is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() eventually-nonnegative eventually-positive eventually-nonzero Element of K19(K20(NAT,REAL))
(c,1,0) is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() eventually-nonnegative eventually-positive eventually-nonzero Element of K19(K20(NAT,REAL))
Big_Oh (c,1,0) is functional non empty FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V1() V4( NAT ) V5( REAL ) Function-like V14( NAT ) quasi_total V35() V36() V37() Element of Funcs (NAT,REAL) : ex b₂ being V25() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * ((c,1,0) . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
log (2,x) is V25() real ext-real Element of REAL
log (2,c) is V25() real ext-real Element of REAL
(log (2,x)) - (log (2,c)) is V25() real ext-real Element of REAL
- (log (2,c)) is V25() real ext-real set
(log (2,x)) + (- (log (2,c))) is V25() real ext-real set
t is V1() V4( NAT ) V5( REAL ) Function-like V14( NAT ) quasi_total V35() V36() V37() Element of Funcs (NAT,REAL)
d is V25() real ext-real Element of REAL
N1 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
d is V25() real ext-real Element of REAL
N1 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
log (2,d) is V25() real ext-real Element of REAL
(log (2,d)) / ((log (2,x)) - (log (2,c))) is V25() real ext-real Element of REAL
((log (2,x)) - (log (2,c))) " is V25() real ext-real set
(log (2,d)) * (((log (2,x)) - (log (2,c))) ") is V25() real ext-real set
[/((log (2,d)) / ((log (2,x)) - (log (2,c))))\] is V25() real ext-real integer set
max (N1,[/((log (2,d)) / ((log (2,x)) - (log (2,c))))\]) is V25() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(n + 1) * (log (2,c)) is V25() real ext-real Element of REAL
2 to_power ((n + 1) * (log (2,c))) is V25() real ext-real Element of REAL
(log (2,c)) + 0 is V25() real ext-real Element of REAL
n + 0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(n + 1) * ((log (2,x)) - (log (2,c))) is V25() real ext-real Element of REAL
((log (2,d)) / ((log (2,x)) - (log (2,c)))) * ((log (2,x)) - (log (2,c))) is V25() real ext-real Element of REAL
2 to_power ((n + 1) * ((log (2,x)) - (log (2,c)))) is V25() real ext-real Element of REAL
2 to_power (log (2,d)) is V25() real ext-real Element of REAL
(n + 1) * (log (2,x)) is V25() real ext-real Element of REAL
((n + 1) * (log (2,x))) - ((n + 1) * (log (2,c))) is V25() real ext-real Element of REAL
- ((n + 1) * (log (2,c))) is V25() real ext-real set
((n + 1) * (log (2,x))) + (- ((n + 1) * (log (2,c)))) is V25() real ext-real set
2 to_power (((n + 1) * (log (2,x))) - ((n + 1) * (log (2,c)))) is V25() real ext-real Element of REAL
2 to_power ((n + 1) * (log (2,x))) is V25() real ext-real Element of REAL
(2 to_power ((n + 1) * (log (2,x)))) / (2 to_power ((n + 1) * (log (2,c)))) is V25() real ext-real Element of REAL
(2 to_power ((n + 1) * (log (2,c)))) " is V25() real ext-real set
(2 to_power ((n + 1) * (log (2,x)))) * ((2 to_power ((n + 1) * (log (2,c)))) ") is V25() real ext-real set
((2 to_power ((n + 1) * (log (2,x)))) / (2 to_power ((n + 1) * (log (2,c))))) * (2 to_power ((n + 1) * (log (2,c)))) is V25() real ext-real Element of REAL
d * (2 to_power ((n + 1) * (log (2,c)))) is V25() real ext-real Element of REAL
x to_power (n + 1) is V25() real ext-real Element of REAL
x |^ (n + 1) is set
c to_power (n + 1) is V25() real ext-real Element of REAL
c |^ (n + 1) is set
d * (c to_power (n + 1)) is V25() real ext-real Element of REAL
(x,1,0) . (n + 1) is V25() real ext-real Element of REAL
(c,1,0) . (n + 1) is V25() real ext-real Element of REAL
d * ((c,1,0) . (n + 1)) is V25() real ext-real Element of REAL
1 * (n + 1) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(1 * (n + 1)) + 0 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
x to_power ((1 * (n + 1)) + 0) is V25() real ext-real Element of REAL
x |^ ((1 * (n + 1)) + 0) is set
c is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
log (2,c) is V25() real ext-real Element of REAL
c is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
c . 0 is V25() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
c . x is V25() real ext-real Element of REAL
log (2,x) is V25() real ext-real Element of REAL
c is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
c . 0 is V25() real ext-real Element of REAL
x is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
x . 0 is V25() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
c . f is V25() real ext-real Element of REAL
x . f is V25() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
c . f is V25() real ext-real Element of REAL
log (2,f) is V25() real ext-real Element of REAL
x . f is V25() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
() is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
c is V25() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
x to_power c is V25() real ext-real Element of REAL
x is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
x . 0 is V25() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
x . f is V25() real ext-real Element of REAL
f to_power c is V25() real ext-real Element of REAL
x is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
x . 0 is V25() real ext-real Element of REAL
f is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
f . 0 is V25() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
x . e is V25() real ext-real Element of REAL
f . e is V25() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
x . e is V25() real ext-real Element of REAL
e to_power c is V25() real ext-real Element of REAL
f . e is V25() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
() . x is V25() real ext-real Element of REAL
log (2,2) is V25() real ext-real Element of REAL
log (2,x) is V25() real ext-real Element of REAL
c is V25() real ext-real Element of REAL
(c) is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
f is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(c) . f is V25() real ext-real Element of REAL
f to_power c is V25() real ext-real Element of REAL
c is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
x is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
c /" x is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
x " is V1() V4( NAT ) Function-like V14( NAT ) V35() V36() V37() set
c (#) (x ") is V1() V4( NAT ) Function-like V14( NAT ) V35() V36() V37() set
f is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(c /" x) . f is V25() real ext-real Element of REAL
c . f is V25() real ext-real Element of REAL
x . f is V25() real ext-real Element of REAL
(c . f) / (x . f) is V25() real ext-real Element of REAL
(x . f) " is V25() real ext-real set
(c . f) * ((x . f) ") is V25() real ext-real set
x " is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() Element of K19(K20(NAT,REAL))
(x ") . f is V25() real ext-real Element of REAL
(c . f) * ((x ") . f) is V25() real ext-real Element of REAL
(x . f) " is V25() real ext-real Element of REAL
(c . f) * ((x . f) ") is V25() real ext-real Element of REAL
c is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() eventually-nonnegative Element of K19(K20(NAT,REAL))
x is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() eventually-nonnegative Element of K19(K20(NAT,REAL))
Big_Oh x is functional non empty FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V1() V4( NAT ) V5( REAL ) Function-like V14( NAT ) quasi_total V35() V36() V37() Element of Funcs (NAT,REAL) : ex b₂ being V25() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (x . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
Big_Oh c is functional non empty FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V1() V4( NAT ) V5( REAL ) Function-like V14( NAT ) quasi_total V35() V36() V37() Element of Funcs (NAT,REAL) : ex b₂ being V25() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (c . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
c is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() eventually-nonnegative Element of K19(K20(NAT,REAL))
Big_Oh c is functional non empty FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V1() V4( NAT ) V5( REAL ) Function-like V14( NAT ) quasi_total V35() V36() V37() Element of Funcs (NAT,REAL) : ex b₂ being V25() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (c . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
x is V1() V4( NAT ) V5( REAL ) Function-like non empty V14( NAT ) quasi_total V35() V36() V37() eventually-nonnegative Element of K19(K20(NAT,REAL))
Big_Oh x is functional non empty FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V1() V4( NAT ) V5( REAL ) Function-like V14( NAT ) quasi_total V35() V36() V37() Element of Funcs (NAT,REAL) : ex b₂ being V25() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (x . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
Big_Omega x is functional non empty FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V1() V4( NAT ) V5( REAL ) Function-like V14( NAT ) quasi_total V35() V36() V37() Element of Funcs (NAT,REAL) : ex b₂ being V25() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (x . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
f is set
e is V1() V4( NAT ) V5( REAL ) Function-like V14( NAT ) quasi_total V35() V36() V37() Element of Funcs (NAT,REAL)
N0 is V25() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
N0 is V25() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
d is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
N1 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
e . N1 is V25() real ext-real Element of REAL
d is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
d is V25() real ext-real Element of REAL
N1 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
c is V25() real ext-real set
x is V25() real ext-real set
f is V25() real ext-real set
c to_power f is V25() real ext-real set
x to_power f is V25() real ext-real set
c is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer set
2 to_power c is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 |^ c is set
2 * c is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(2 * c) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
c + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 to_power (c + 1) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 |^ (c + 1) is set
2 * (c + 1) is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
(2 * (c + 1)) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V25() real ext-real positive non negative integer V48() V49() V50() V51() V52() V53() V54() Element of NAT
2 to_power 1 is epsilon-transitive epsilon-connected ordinal natural V25() real ext-real non negative integer V48() V49() V50() V51() V52()