:: FIB_NUM semantic presentation

REAL is V1() V2() V56() V68() V69() V70() V74() V80() set
NAT is V68() V69() V70() V71() V72() V73() V74() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V1() V2() V56() V68() V74() V80() set
omega is V68() V69() V70() V71() V72() V73() V74() set
K6(omega) is set
K6(NAT) is set
RAT is V1() V2() V56() V68() V69() V70() V71() V74() V80() set
INT is V1() V2() V56() V68() V69() V70() V71() V72() V74() V80() set
K7(COMPLEX,COMPLEX) is complex-valued set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is V20( RAT ) complex-valued ext-real-valued real-valued set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V20( RAT ) complex-valued ext-real-valued real-valued set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K7(K7(NAT,NAT),NAT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(NAT,NAT),NAT)) is set
1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
0 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib 0 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib 1 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
2 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
4 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
sqrt 4 is V11() real ext-real Element of REAL
K7(NAT,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(NAT,REAL)) is set
0 " is V11() real ext-real non negative set
F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F gcd f is ordinal natural V11() real ext-real non negative V33() set
f + F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F gcd (f + F) is ordinal natural V11() real ext-real non negative V33() set
F is ordinal natural V11() real ext-real non negative V33() set
f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F gcd f is ordinal natural V11() real ext-real non negative V33() set
f2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f * f2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F gcd (f * f2) is ordinal natural V11() real ext-real non negative V33() set
F gcd f2 is ordinal natural V11() real ext-real non negative V33() set
f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F gcd f is ordinal natural V11() real ext-real non negative V33() set
f2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f * f2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F gcd (f * f2) is ordinal natural V11() real ext-real non negative V33() set
F gcd f2 is ordinal natural V11() real ext-real non negative V33() set
f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F gcd f is ordinal natural V11() real ext-real non negative V33() set
f2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f * f2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F gcd (f * f2) is ordinal natural V11() real ext-real non negative V33() set
F gcd f2 is ordinal natural V11() real ext-real non negative V33() set
1 + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
g is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
g1 is ordinal natural V11() real ext-real non negative V33() set
g * g1 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
g2 is ordinal natural V11() real ext-real non negative V33() set
g * g2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
h is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
h + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
h * (1 + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
h * g is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
h + h is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
h gcd f is ordinal natural V11() real ext-real non negative V33() set
n is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
h gcd n is ordinal natural V11() real ext-real non negative V33() set
g * (h gcd n) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
g * h is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f * n is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
g * (f * n) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(g * h) gcd (g * (f * n)) is ordinal natural V11() real ext-real non negative V33() set
h gcd (f * n) is ordinal natural V11() real ext-real non negative V33() set
g * (h gcd (f * n)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F gcd f is ordinal natural V11() real ext-real non negative V33() set
f2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f * f2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F gcd (f * f2) is ordinal natural V11() real ext-real non negative V33() set
F gcd f2 is ordinal natural V11() real ext-real non negative V33() set
F is V11() real ext-real set
1 / F is V11() real ext-real Element of COMPLEX
F " is V11() real ext-real set
1 * (F ") is V11() real ext-real set
f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
1 / (1 / F) is V11() real ext-real Element of COMPLEX
(1 / F) " is V11() real ext-real set
1 * ((1 / F) ") is V11() real ext-real set
1 / (F ") is V11() real ext-real Element of COMPLEX
(F ") " is V11() real ext-real set
1 * ((F ") ") is V11() real ext-real set
1 / f is V11() real ext-real non negative Element of COMPLEX
f " is V11() real ext-real non negative set
1 * (f ") is V11() real ext-real non negative set
F is ordinal natural V11() real ext-real non negative V33() set
f is ordinal natural V11() real ext-real non negative V33() set
f + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(f + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f + 2 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(f + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
0 + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F is ordinal natural V11() real ext-real non negative V33() set
f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
max (f,f2) is ordinal natural V11() real ext-real non negative V33() set
g is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
g1 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
max (g,g1) is ordinal natural V11() real ext-real non negative V33() set
F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
max (F,f) is ordinal natural V11() real ext-real non negative V33() set
0 + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(0 + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib 2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
1 + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(1 + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
3 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
1 + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (1 + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F is ordinal natural V11() real ext-real non negative V33() set
F + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (F + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(F + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib ((F + 1) + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F + 2 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(F + 2) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib ((F + 2) + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
1 + (F + 1) is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F + (F + 1) is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(F + 2) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib ((F + 2) + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(F + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib ((F + 1) + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib ((F + 1) + 1)) + (Fib (F + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (F + 1)) + (F + 1) is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
0 + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (0 + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (F + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(F + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib ((F + 1) + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (F + 1)) + (Fib F) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (F + 1)) + 0 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (0 + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f + (F + 1) is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (f + (F + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f + F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(f + F) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (f + F) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f + F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (f + F) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib f2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f2 + 0 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (f2 + 0) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f2 is ordinal natural V11() real ext-real non negative V33() set
f + f2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f1 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f + f1 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (F + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
0 + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (0 + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F is ordinal natural V11() real ext-real non negative V33() set
F + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
0 + (F + 1) is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (0 + (F + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib F) * (Fib 0) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (F + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (F + 1)) * (Fib (0 + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
((Fib F) * (Fib 0)) + ((Fib (F + 1)) * (Fib (0 + 1))) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F is ordinal natural V11() real ext-real non negative V33() set
Fib F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (F + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(F + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib ((F + 1) + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F + 2 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (F + 2) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(F + 2) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib ((F + 2) + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f is ordinal natural V11() real ext-real non negative V33() set
f + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(F + 2) + (f + 1) is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib ((F + 2) + (f + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib f) * (Fib (F + 2)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (f + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (f + 1)) * (Fib ((F + 2) + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
((Fib f) * (Fib (F + 2))) + ((Fib (f + 1)) * (Fib ((F + 2) + 1))) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(F + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
((F + 1) + 1) + (f + 1) is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (((F + 1) + 1) + (f + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F + (f + 1) is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(F + (f + 1)) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
((F + (f + 1)) + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (((F + (f + 1)) + 1) + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (F + (f + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(F + 1) + (f + 1) is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib ((F + 1) + (f + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (F + (f + 1))) + (Fib ((F + 1) + (f + 1))) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib f) * (Fib F) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (f + 1)) * (Fib (F + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib f) * (Fib (F + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib ((F + 1) + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (f + 1)) * (Fib ((F + 1) + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
((Fib f) * (Fib F)) + ((Fib (f + 1)) * (Fib (F + 1))) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
((Fib f) * (Fib (F + 1))) + ((Fib (f + 1)) * (Fib ((F + 1) + 1))) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(((Fib f) * (Fib F)) + ((Fib (f + 1)) * (Fib (F + 1)))) + (((Fib f) * (Fib (F + 1))) + ((Fib (f + 1)) * (Fib ((F + 1) + 1)))) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
((Fib f) * (Fib F)) + ((Fib f) * (Fib (F + 1))) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
((Fib (f + 1)) * (Fib (F + 1))) + ((Fib (f + 1)) * (Fib ((F + 1) + 1))) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(((Fib f) * (Fib F)) + ((Fib f) * (Fib (F + 1)))) + (((Fib (f + 1)) * (Fib (F + 1))) + ((Fib (f + 1)) * (Fib ((F + 1) + 1)))) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (F + 1)) + (Fib ((F + 1) + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (f + 1)) * ((Fib (F + 1)) + (Fib ((F + 1) + 1))) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
((F + 1) + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (((F + 1) + 1) + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (f + 1)) * (Fib (((F + 1) + 1) + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib F) + (Fib (F + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib f) * ((Fib F) + (Fib (F + 1))) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib f) * (Fib ((F + 1) + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
1 + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (1 + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F is ordinal natural V11() real ext-real non negative V33() set
F + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
1 + (F + 1) is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (1 + (F + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib F) * (Fib 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (F + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (F + 1)) * (Fib (1 + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
((Fib F) * (Fib 1)) + ((Fib (F + 1)) * (Fib (1 + 1))) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (F + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib F) gcd (Fib (F + 1)) is ordinal natural V11() real ext-real non negative V33() set
(F + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib ((F + 1) + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (F + 1)) gcd (Fib ((F + 1) + 1)) is ordinal natural V11() real ext-real non negative V33() set
(Fib (F + 1)) + (Fib F) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (F + 1)) gcd ((Fib (F + 1)) + (Fib F)) is ordinal natural V11() real ext-real non negative V33() set
Fib (0 + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib 0) gcd (Fib (0 + 1)) is ordinal natural V11() real ext-real non negative V33() set
F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib F) gcd (Fib f) is ordinal natural V11() real ext-real non negative V33() set
F gcd f is ordinal natural V11() real ext-real non negative V33() set
Fib (F gcd f) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f2 is ordinal natural V11() real ext-real non negative V33() set
f + f2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f1 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
g is ordinal natural V11() real ext-real non negative V33() set
g + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
g1 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
g1 + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (g1 + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (f + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (g1 + 1)) * (Fib (f + 1)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib g1 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib g1) * (Fib f) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
((Fib (g1 + 1)) * (Fib (f + 1))) + ((Fib g1) * (Fib f)) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib f1 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (f + 1)) * (Fib f1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib f) gcd ((Fib (f + 1)) * (Fib f1)) is ordinal natural V11() real ext-real non negative V33() set
(Fib f) gcd (Fib (f + 1)) is ordinal natural V11() real ext-real non negative V33() set
(Fib f) gcd (Fib f1) is ordinal natural V11() real ext-real non negative V33() set
f gcd f1 is ordinal natural V11() real ext-real non negative V33() set
F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib f is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib F) gcd (Fib f) is ordinal natural V11() real ext-real non negative V33() set
F gcd f is ordinal natural V11() real ext-real non negative V33() set
Fib (F gcd f) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib f) gcd (Fib F) is ordinal natural V11() real ext-real non negative V33() set
f gcd F is ordinal natural V11() real ext-real non negative V33() set
Fib (f gcd F) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F is V11() real ext-real set
F ^2 is V11() real ext-real set
F * F is V11() real ext-real set
f is V11() real ext-real set
f * (F ^2) is V11() real ext-real set
2 * f is V11() real ext-real set
f2 is V11() real ext-real set
f2 * F is V11() real ext-real set
(f * (F ^2)) + (f2 * F) is V11() real ext-real set
- f2 is V11() real ext-real set
f1 is V11() real ext-real set
delta (f,f2,f1) is V11() real ext-real set
((f * (F ^2)) + (f2 * F)) + f1 is V11() real ext-real set
sqrt (delta (f,f2,f1)) is V11() real ext-real set
(- f2) - (sqrt (delta (f,f2,f1))) is V11() real ext-real set
- (sqrt (delta (f,f2,f1))) is V11() real ext-real set
(- f2) + (- (sqrt (delta (f,f2,f1)))) is V11() real ext-real set
((- f2) - (sqrt (delta (f,f2,f1)))) / (2 * f) is V11() real ext-real Element of COMPLEX
(2 * f) " is V11() real ext-real set
((- f2) - (sqrt (delta (f,f2,f1)))) * ((2 * f) ") is V11() real ext-real set
(- f2) + (sqrt (delta (f,f2,f1))) is V11() real ext-real set
((- f2) + (sqrt (delta (f,f2,f1)))) / (2 * f) is V11() real ext-real Element of COMPLEX
((- f2) + (sqrt (delta (f,f2,f1)))) * ((2 * f) ") is V11() real ext-real set
F - (((- f2) - (sqrt (delta (f,f2,f1)))) / (2 * f)) is V11() real ext-real set
- (((- f2) - (sqrt (delta (f,f2,f1)))) / (2 * f)) is V11() real ext-real set
F + (- (((- f2) - (sqrt (delta (f,f2,f1)))) / (2 * f))) is V11() real ext-real set
f * (F - (((- f2) - (sqrt (delta (f,f2,f1)))) / (2 * f))) is V11() real ext-real set
F - (((- f2) + (sqrt (delta (f,f2,f1)))) / (2 * f)) is V11() real ext-real set
- (((- f2) + (sqrt (delta (f,f2,f1)))) / (2 * f)) is V11() real ext-real set
F + (- (((- f2) + (sqrt (delta (f,f2,f1)))) / (2 * f))) is V11() real ext-real set
(f * (F - (((- f2) - (sqrt (delta (f,f2,f1)))) / (2 * f)))) * (F - (((- f2) + (sqrt (delta (f,f2,f1)))) / (2 * f))) is V11() real ext-real set
5 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
sqrt 5 is V11() real ext-real Element of REAL
1 + (sqrt 5) is V11() real ext-real set
(1 + (sqrt 5)) / 2 is V11() real ext-real Element of COMPLEX
2 " is V11() real ext-real positive non negative set
(1 + (sqrt 5)) * (2 ") is V11() real ext-real set
() is V11() real ext-real set
1 - (sqrt 5) is V11() real ext-real set
- (sqrt 5) is V11() real ext-real set
1 + (- (sqrt 5)) is V11() real ext-real set
(1 - (sqrt 5)) / 2 is V11() real ext-real Element of COMPLEX
(1 - (sqrt 5)) * (2 ") is V11() real ext-real set
() is V11() real ext-real set
() ^2 is V11() real ext-real set
() * () is V11() real ext-real set
() + 1 is V11() real ext-real set
() ^2 is V11() real ext-real set
() * () is V11() real ext-real set
() + 1 is V11() real ext-real set
- 1 is V11() real ext-real non positive V33() set
delta (1,(- 1),(- 1)) is V11() real ext-real set
(- 1) ^2 is V11() real ext-real set
(- 1) * (- 1) is V11() real ext-real non negative V33() set
4 * 1 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(4 * 1) * (- 1) is V11() real ext-real non positive V33() set
((- 1) ^2) - ((4 * 1) * (- 1)) is V11() real ext-real set
- ((4 * 1) * (- 1)) is V11() real ext-real non negative V33() set
((- 1) ^2) + (- ((4 * 1) * (- 1))) is V11() real ext-real set
- (- 1) is V11() real ext-real non negative V33() set
sqrt (delta (1,(- 1),(- 1))) is V11() real ext-real set
(- (- 1)) - (sqrt (delta (1,(- 1),(- 1)))) is V11() real ext-real set
- (sqrt (delta (1,(- 1),(- 1)))) is V11() real ext-real set
(- (- 1)) + (- (sqrt (delta (1,(- 1),(- 1))))) is V11() real ext-real set
2 * 1 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
((- (- 1)) - (sqrt (delta (1,(- 1),(- 1))))) / (2 * 1) is V11() real ext-real Element of COMPLEX
(2 * 1) " is V11() real ext-real non negative set
((- (- 1)) - (sqrt (delta (1,(- 1),(- 1))))) * ((2 * 1) ") is V11() real ext-real set
F is V11() real ext-real set
F ^2 is V11() real ext-real set
F * F is V11() real ext-real set
F + 1 is V11() real ext-real set
1 * (F ^2) is V11() real ext-real set
(- 1) * F is V11() real ext-real set
(1 * (F ^2)) + ((- 1) * F) is V11() real ext-real set
((1 * (F ^2)) + ((- 1) * F)) + (- 1) is V11() real ext-real set
3 ^2 is V11() real ext-real Element of REAL
3 * 3 is ordinal natural V11() real ext-real non negative V33() set
9 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
sqrt 9 is V11() real ext-real Element of REAL
2 / 2 is V11() real ext-real non negative Element of COMPLEX
2 * (2 ") is V11() real ext-real non negative set
0 + (sqrt 5) is V11() real ext-real set
0 * 2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(1 - (sqrt 5)) / 1 is V11() real ext-real Element of COMPLEX
1 " is V11() real ext-real positive non negative set
(1 - (sqrt 5)) * (1 ") is V11() real ext-real set
0 * 1 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
abs () is V11() real ext-real Element of REAL
3 - 1 is V11() real ext-real V33() set
- 1 is V11() real ext-real non positive V33() set
3 + (- 1) is V11() real ext-real V33() set
(sqrt 5) - 1 is V11() real ext-real set
(sqrt 5) + (- 1) is V11() real ext-real set
2 / 2 is V11() real ext-real non negative Element of COMPLEX
2 * (2 ") is V11() real ext-real non negative set
((sqrt 5) - 1) / 2 is V11() real ext-real Element of COMPLEX
((sqrt 5) - 1) * (2 ") is V11() real ext-real set
- ((1 - (sqrt 5)) / 2) is V11() real ext-real Element of COMPLEX
() to_power 1 is V11() real ext-real set
() to_power 0 is V11() real ext-real set
() to_power 0 is V11() real ext-real set
(() to_power 0) - (() to_power 0) is V11() real ext-real set
- (() to_power 0) is V11() real ext-real set
(() to_power 0) + (- (() to_power 0)) is V11() real ext-real set
((() to_power 0) - (() to_power 0)) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(sqrt 5) " is V11() real ext-real set
((() to_power 0) - (() to_power 0)) * ((sqrt 5) ") is V11() real ext-real set
1 - 1 is V11() real ext-real V33() set
- 1 is V11() real ext-real non positive V33() set
1 + (- 1) is V11() real ext-real V33() set
(1 - 1) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(1 - 1) * ((sqrt 5) ") is V11() real ext-real set
F is ordinal natural V11() real ext-real non negative V33() set
Fib F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
() to_power F is V11() real ext-real set
() to_power F is V11() real ext-real set
(() to_power F) - (() to_power F) is V11() real ext-real set
- (() to_power F) is V11() real ext-real set
(() to_power F) + (- (() to_power F)) is V11() real ext-real set
((() to_power F) - (() to_power F)) / (sqrt 5) is V11() real ext-real Element of COMPLEX
((() to_power F) - (() to_power F)) * ((sqrt 5) ") is V11() real ext-real set
F + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (F + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
() to_power (F + 1) is V11() real ext-real set
() to_power (F + 1) is V11() real ext-real set
(() to_power (F + 1)) - (() to_power (F + 1)) is V11() real ext-real set
- (() to_power (F + 1)) is V11() real ext-real set
(() to_power (F + 1)) + (- (() to_power (F + 1))) is V11() real ext-real set
((() to_power (F + 1)) - (() to_power (F + 1))) / (sqrt 5) is V11() real ext-real Element of COMPLEX
((() to_power (F + 1)) - (() to_power (F + 1))) * ((sqrt 5) ") is V11() real ext-real set
F + 2 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (F + 2) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
() to_power (F + 2) is V11() real ext-real set
() to_power (F + 2) is V11() real ext-real set
(() to_power (F + 2)) - (() to_power (F + 2)) is V11() real ext-real set
- (() to_power (F + 2)) is V11() real ext-real set
(() to_power (F + 2)) + (- (() to_power (F + 2))) is V11() real ext-real set
((() to_power (F + 2)) - (() to_power (F + 2))) / (sqrt 5) is V11() real ext-real Element of COMPLEX
((() to_power (F + 2)) - (() to_power (F + 2))) * ((sqrt 5) ") is V11() real ext-real set
() |^ (F + 2) is V11() real ext-real set
() |^ F is V11() real ext-real set
() |^ (1 + 1) is V11() real ext-real set
(() |^ F) * (() |^ (1 + 1)) is V11() real ext-real set
() |^ 1 is V11() real ext-real set
() * (() |^ 1) is V11() real ext-real set
(() |^ F) * (() * (() |^ 1)) is V11() real ext-real set
(() |^ F) * (() + 1) is V11() real ext-real set
(() |^ F) * () is V11() real ext-real set
(() |^ F) * 1 is V11() real ext-real set
((() |^ F) * ()) + ((() |^ F) * 1) is V11() real ext-real set
() |^ (F + 1) is V11() real ext-real set
(() |^ (F + 1)) + ((() |^ F) * 1) is V11() real ext-real set
(() to_power (F + 1)) + (() |^ F) is V11() real ext-real set
(() to_power F) + (() to_power (F + 1)) is V11() real ext-real set
() to_power 2 is V11() real ext-real set
(() to_power 2) * (() to_power F) is V11() real ext-real set
(() to_power F) * (() + 1) is V11() real ext-real set
(() to_power F) * () is V11() real ext-real set
(() to_power F) * 1 is V11() real ext-real set
((() to_power F) * ()) + ((() to_power F) * 1) is V11() real ext-real set
() to_power 1 is V11() real ext-real set
(() to_power F) * (() to_power 1) is V11() real ext-real set
((() to_power F) * (() to_power 1)) + (() to_power F) is V11() real ext-real set
(() to_power F) + (() to_power (F + 1)) is V11() real ext-real set
(F + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib ((F + 1) + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(((() to_power F) - (() to_power F)) / (sqrt 5)) + (((() to_power (F + 1)) - (() to_power (F + 1))) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
() - () is V11() real ext-real set
- () is V11() real ext-real set
() + (- ()) is V11() real ext-real set
() to_power 1 is V11() real ext-real set
(() to_power 1) - (() to_power 1) is V11() real ext-real set
- (() to_power 1) is V11() real ext-real set
(() to_power 1) + (- (() to_power 1)) is V11() real ext-real set
((() to_power 1) - (() to_power 1)) / (sqrt 5) is V11() real ext-real Element of COMPLEX
((() to_power 1) - (() to_power 1)) * ((sqrt 5) ") is V11() real ext-real set
(sqrt 5) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(sqrt 5) * ((sqrt 5) ") is V11() real ext-real set
F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f is V11() real ext-real set
abs f is V11() real ext-real Element of REAL
f |^ F is V11() real ext-real set
abs (f |^ F) is V11() real ext-real Element of REAL
f2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f |^ f2 is V11() real ext-real set
abs (f |^ f2) is V11() real ext-real Element of REAL
f2 + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f |^ (f2 + 1) is V11() real ext-real set
abs (f |^ (f2 + 1)) is V11() real ext-real Element of REAL
(f |^ f2) * f is V11() real ext-real set
abs ((f |^ f2) * f) is V11() real ext-real Element of REAL
(abs (f |^ f2)) * (abs f) is V11() real ext-real set
f |^ 0 is V11() real ext-real set
abs (f |^ 0) is V11() real ext-real Element of REAL
abs 1 is V11() real ext-real V67() Element of REAL
F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
() to_power F is V11() real ext-real set
(() to_power F) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(sqrt 5) " is V11() real ext-real set
(() to_power F) * ((sqrt 5) ") is V11() real ext-real set
abs ((() to_power F) / (sqrt 5)) is V11() real ext-real Element of REAL
abs (() to_power F) is V11() real ext-real Element of REAL
() |^ F is V11() real ext-real set
abs (() |^ F) is V11() real ext-real Element of REAL
abs ((() to_power F) * ((sqrt 5) ")) is V11() real ext-real Element of REAL
abs ((sqrt 5) ") is V11() real ext-real Element of REAL
(abs (() to_power F)) * (abs ((sqrt 5) ")) is V11() real ext-real set
1 / 2 is V11() real ext-real non negative Element of COMPLEX
1 * (2 ") is V11() real ext-real non negative set
1 / (sqrt 5) is V11() real ext-real Element of COMPLEX
1 * ((sqrt 5) ") is V11() real ext-real set
F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib F is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
() to_power F is V11() real ext-real set
(() to_power F) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(sqrt 5) " is V11() real ext-real set
(() to_power F) * ((sqrt 5) ") is V11() real ext-real set
(Fib F) - ((() to_power F) / (sqrt 5)) is V11() real ext-real set
- ((() to_power F) / (sqrt 5)) is V11() real ext-real set
(Fib F) + (- ((() to_power F) / (sqrt 5))) is V11() real ext-real set
abs ((Fib F) - ((() to_power F) / (sqrt 5))) is V11() real ext-real Element of REAL
() to_power F is V11() real ext-real set
(() to_power F) - (() to_power F) is V11() real ext-real set
- (() to_power F) is V11() real ext-real set
(() to_power F) + (- (() to_power F)) is V11() real ext-real set
((() to_power F) - (() to_power F)) / (sqrt 5) is V11() real ext-real Element of COMPLEX
((() to_power F) - (() to_power F)) * ((sqrt 5) ") is V11() real ext-real set
(() to_power F) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(() to_power F) * ((sqrt 5) ") is V11() real ext-real set
((() to_power F) / (sqrt 5)) - ((() to_power F) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
- ((() to_power F) / (sqrt 5)) is V11() real ext-real set
((() to_power F) / (sqrt 5)) + (- ((() to_power F) / (sqrt 5))) is V11() real ext-real set
- ((Fib F) - ((() to_power F) / (sqrt 5))) is V11() real ext-real set
abs (- ((Fib F) - ((() to_power F) / (sqrt 5)))) is V11() real ext-real Element of REAL
f is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
F is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
F /" f is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f " is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
F (#) (f ") is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
f2 is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f /" f2 is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f2 " is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
f (#) (f2 ") is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(F /" f) (#) (f /" f2) is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
F /" f2 is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
F (#) (f2 ") is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
g2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
((F /" f) (#) (f /" f2)) . g2 is V11() real ext-real Element of REAL
(F /" f2) . g2 is V11() real ext-real Element of REAL
F . g2 is V11() real ext-real Element of REAL
f . g2 is V11() real ext-real Element of REAL
(f . g2) " is V11() real ext-real set
f2 . g2 is V11() real ext-real Element of REAL
(f2 . g2) " is V11() real ext-real set
(f /" f2) . g2 is V11() real ext-real Element of REAL
f2 " is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f2 ") . g2 is V11() real ext-real Element of REAL
(f . g2) * ((f2 ") . g2) is V11() real ext-real set
(f . g2) * ((f2 . g2) ") is V11() real ext-real set
(F . g2) * ((f2 ") . g2) is V11() real ext-real set
(F . g2) * ((f2 . g2) ") is V11() real ext-real set
((f . g2) ") * (f . g2) is V11() real ext-real set
1 / (f . g2) is V11() real ext-real Element of COMPLEX
1 * ((f . g2) ") is V11() real ext-real set
(1 / (f . g2)) * (f . g2) is V11() real ext-real set
(F /" f) . g2 is V11() real ext-real Element of REAL
f " is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f ") . g2 is V11() real ext-real Element of REAL
(F . g2) * ((f ") . g2) is V11() real ext-real set
(F . g2) * ((f . g2) ") is V11() real ext-real set
((F . g2) * ((f . g2) ")) * ((f . g2) * ((f2 . g2) ")) is V11() real ext-real set
(((f . g2) ") * (f . g2)) * (F . g2) is V11() real ext-real set
((((f . g2) ") * (f . g2)) * (F . g2)) * ((f2 . g2) ") is V11() real ext-real set
F is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
F /" f is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f " is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
F (#) (f ") is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
f2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(F /" f) . f2 is V11() real ext-real Element of REAL
F . f2 is V11() real ext-real Element of REAL
f . f2 is V11() real ext-real Element of REAL
(F . f2) / (f . f2) is V11() real ext-real Element of COMPLEX
(f . f2) " is V11() real ext-real set
(F . f2) * ((f . f2) ") is V11() real ext-real set
f " is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f ") . f2 is V11() real ext-real Element of REAL
(F . f2) * ((f ") . f2) is V11() real ext-real set
F is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim F is V11() real ext-real Element of REAL
f is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f ^\ 2 is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of f
f ^\ 1 is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of f
(f ^\ 1) ^\ 1 is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of f ^\ 1
f ^\ (1 + 1) is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of f
g is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(f ^\ 2) . g is V11() real ext-real Element of REAL
g + 2 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f . (g + 2) is V11() real ext-real Element of REAL
g + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(g + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib ((g + 1) + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(f ^\ 2) /" (f ^\ 2) is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f ^\ 2) " is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(f ^\ 2) (#) ((f ^\ 2) ") is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
g is ordinal natural V11() real ext-real non negative V33() set
((f ^\ 2) /" (f ^\ 2)) . g is V11() real ext-real Element of REAL
(f ^\ 2) . g is V11() real ext-real Element of REAL
((f ^\ 2) . g) " is V11() real ext-real set
((f ^\ 2) . g) * (((f ^\ 2) . g) ") is V11() real ext-real set
1 / ((f ^\ 2) . g) is V11() real ext-real Element of COMPLEX
1 * (((f ^\ 2) . g) ") is V11() real ext-real set
((f ^\ 2) . g) * (1 / ((f ^\ 2) . g)) is V11() real ext-real set
f /" f is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f " is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
f (#) (f ") is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(f /" f) ^\ 2 is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of f /" f
((f ^\ 2) /" (f ^\ 2)) . 0 is V11() real ext-real Element of REAL
lim ((f ^\ 2) /" (f ^\ 2)) is V11() real ext-real Element of REAL
lim (f /" f) is V11() real ext-real Element of REAL
g is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
g is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
g ^\ 1 is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of g
g2 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
g . g2 is V11() real ext-real Element of REAL
(sqrt 5) " is V11() real ext-real set
() |^ g2 is V11() real ext-real set
() to_power g2 is V11() real ext-real set
(() to_power g2) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(() to_power g2) * ((sqrt 5) ") is V11() real ext-real set
(() |^ g2) * ((sqrt 5) ") is V11() real ext-real set
(f ^\ 2) /" (f ^\ 1) is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f ^\ 1) " is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(f ^\ 2) (#) ((f ^\ 1) ") is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(f ^\ 2) /" (g ^\ 1) is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(g ^\ 1) " is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(f ^\ 2) (#) ((g ^\ 1) ") is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(g ^\ 1) /" (f ^\ 1) is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(g ^\ 1) (#) ((f ^\ 1) ") is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
((f ^\ 2) /" (g ^\ 1)) (#) ((g ^\ 1) /" (f ^\ 1)) is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(g ^\ 1) ^\ 1 is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of g ^\ 1
h is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(f ^\ 1) . h is V11() real ext-real Element of REAL
h + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f . (h + 1) is V11() real ext-real Element of REAL
Fib (h + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
((g ^\ 1) ^\ 1) /" (f ^\ 2) is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((g ^\ 1) ^\ 1) (#) ((f ^\ 2) ") is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
h is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(((g ^\ 1) ^\ 1) /" (f ^\ 2)) . h is V11() real ext-real Element of REAL
((g ^\ 1) ^\ 1) . h is V11() real ext-real Element of REAL
(f ^\ 2) . h is V11() real ext-real Element of REAL
((f ^\ 2) . h) " is V11() real ext-real set
(((g ^\ 1) ^\ 1) . h) * (((f ^\ 2) . h) ") is V11() real ext-real set
g ^\ (1 + 1) is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of g
g /" f is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
g (#) (f ") is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(g /" f) ^\ 2 is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of g /" f
h is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(f ^\ 1) . h is V11() real ext-real Element of REAL
h + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (h + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f . (h + 1) is V11() real ext-real Element of REAL
(f ^\ 1) /" f is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f ^\ 1) (#) (f ") is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
h is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
F . h is V11() real ext-real Element of REAL
((f ^\ 1) /" f) . h is V11() real ext-real Element of REAL
(f ^\ 1) . h is V11() real ext-real Element of REAL
f . h is V11() real ext-real Element of REAL
((f ^\ 1) . h) / (f . h) is V11() real ext-real Element of COMPLEX
(f . h) " is V11() real ext-real set
((f ^\ 1) . h) * ((f . h) ") is V11() real ext-real set
h + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (h + 1) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (h + 1)) / (f . h) is V11() real ext-real Element of COMPLEX
(Fib (h + 1)) * ((f . h) ") is V11() real ext-real set
Fib h is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(Fib (h + 1)) / (Fib h) is V11() real ext-real non negative Element of COMPLEX
(Fib h) " is V11() real ext-real non negative set
(Fib (h + 1)) * ((Fib h) ") is V11() real ext-real non negative set
F ^\ 1 is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of F
((g ^\ 1) ^\ 1) /" (g ^\ 1) is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((g ^\ 1) ^\ 1) (#) ((g ^\ 1) ") is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(g ^\ 1) /" g is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
g " is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(g ^\ 1) (#) (g ") is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
((g ^\ 1) /" g) ^\ 1 is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (g ^\ 1) /" g
h is ordinal natural V11() real ext-real non negative V33() set
((g ^\ 1) /" g) . h is V11() real ext-real Element of REAL
g . h is V11() real ext-real Element of REAL
() to_power h is V11() real ext-real set
(() to_power h) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(sqrt 5) " is V11() real ext-real set
(() to_power h) * ((sqrt 5) ") is V11() real ext-real set
() |^ h is V11() real ext-real set
(() |^ h) * ((sqrt 5) ") is V11() real ext-real set
(g ^\ 1) . h is V11() real ext-real Element of REAL
h + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
g . (h + 1) is V11() real ext-real Element of REAL
() to_power (h + 1) is V11() real ext-real set
(() to_power (h + 1)) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(() to_power (h + 1)) * ((sqrt 5) ") is V11() real ext-real set
() |^ (h + 1) is V11() real ext-real set
(() |^ (h + 1)) * ((sqrt 5) ") is V11() real ext-real set
() * (() |^ h) is V11() real ext-real set
(() * (() |^ h)) * ((sqrt 5) ") is V11() real ext-real set
() * (g . h) is V11() real ext-real set
(g . h) " is V11() real ext-real set
(() * (g . h)) * ((g . h) ") is V11() real ext-real set
(g . h) * ((g . h) ") is V11() real ext-real set
() * ((g . h) * ((g . h) ")) is V11() real ext-real set
() * 1 is V11() real ext-real set
f " is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
h is V11() real ext-real set
n is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
1 / n is V11() real ext-real non negative Element of COMPLEX
n " is V11() real ext-real non negative set
1 * (n ") is V11() real ext-real non negative set
n + 2 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
m is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(f ") . m is V11() real ext-real Element of REAL
((f ") . m) - 0 is V11() real ext-real set
- 0 is V11() real ext-real non positive V33() set
((f ") . m) + (- 0) is V11() real ext-real set
abs (((f ") . m) - 0) is V11() real ext-real Element of REAL
n + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
(n + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib (n + 2) is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
Fib m is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f . m is V11() real ext-real Element of REAL
(f . m) " is V11() real ext-real set
n + 0 is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
1 / (n + 1) is V11() real ext-real non negative Element of COMPLEX
(n + 1) " is V11() real ext-real positive non negative set
1 * ((n + 1) ") is V11() real ext-real non negative set
abs ((f . m) ") is V11() real ext-real Element of REAL
1 / (f . m) is V11() real ext-real Element of COMPLEX
1 * ((f . m) ") is V11() real ext-real set
lim (f ") is V11() real ext-real Element of REAL
h is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
h is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
n is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
f . n is V11() real ext-real Element of REAL
g . n is V11() real ext-real Element of REAL
h . n is V11() real ext-real Element of REAL
(g . n) - (h . n) is V11() real ext-real set
- (h . n) is V11() real ext-real set
(g . n) + (- (h . n)) is V11() real ext-real set
Fib n is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
() to_power n is V11() real ext-real set
() to_power n is V11() real ext-real set
(() to_power n) - (() to_power n) is V11() real ext-real set
- (() to_power n) is V11() real ext-real set
(() to_power n) + (- (() to_power n)) is V11() real ext-real set
((() to_power n) - (() to_power n)) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(sqrt 5) " is V11() real ext-real set
((() to_power n) - (() to_power n)) * ((sqrt 5) ") is V11() real ext-real set
(() to_power n) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(() to_power n) * ((sqrt 5) ") is V11() real ext-real set
(() to_power n) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(() to_power n) * ((sqrt 5) ") is V11() real ext-real set
((() to_power n) / (sqrt 5)) - ((() to_power n) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
- ((() to_power n) / (sqrt 5)) is V11() real ext-real set
((() to_power n) / (sqrt 5)) + (- ((() to_power n) / (sqrt 5))) is V11() real ext-real set
(g . n) - ((() to_power n) / (sqrt 5)) is V11() real ext-real set
(g . n) + (- ((() to_power n) / (sqrt 5))) is V11() real ext-real set
n is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
g . n is V11() real ext-real Element of REAL
f . n is V11() real ext-real Element of REAL
h . n is V11() real ext-real Element of REAL
(f . n) + (h . n) is V11() real ext-real set
(g . n) - (h . n) is V11() real ext-real set
- (h . n) is V11() real ext-real set
(g . n) + (- (h . n)) is V11() real ext-real set
f + h is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
h /" f is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
h (#) (f ") is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(f /" f) + (h /" f) is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
n is ordinal natural V11() real ext-real non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
h . n is V11() real ext-real Element of REAL
abs (h . n) is V11() real ext-real Element of REAL
() to_power n is V11() real ext-real set
(() to_power n) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(sqrt 5) " is V11() real ext-real set
(() to_power n) * ((sqrt 5) ") is V11() real ext-real set
((g ^\ 1) /" g) . 0 is V11() real ext-real Element of REAL
lim ((g ^\ 1) /" g) is V11() real ext-real Element of REAL
lim (((g ^\ 1) ^\ 1) /" (g ^\ 1)) is V11() real ext-real Element of REAL
(g /" f) ^\ 1 is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of g /" f
lim (h /" f) is V11() real ext-real Element of REAL
lim (g /" f) is V11() real ext-real Element of REAL
1 + 0 is V1() ordinal natural V11() real ext-real positive non negative V33() V67() V68() V69() V70() V71() V72() V73() Element of NAT
lim (((g ^\ 1) ^\ 1) /" (f ^\ 2)) is V11() real ext-real Element of REAL
(((g ^\ 1) ^\ 1) /" (f ^\ 2)) " is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f ^\ 2) /" ((g ^\ 1) ^\ 1) is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((g ^\ 1) ^\ 1) " is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
(f ^\ 2) (#) (((g ^\ 1) ^\ 1) ") is V16() V19( NAT ) V21() V26( NAT ) complex-valued ext-real-valued real-valued set
((f ^\ 2) /" ((g ^\ 1) ^\ 1)) (#) (((g ^\ 1) ^\ 1) /" (g ^\ 1)) is V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim ((((g ^\ 1) ^\ 1) /" (f ^\ 2)) ") is V11() real ext-real Element of REAL
1 " is V11() real ext-real positive non negative set
lim ((f ^\ 2) /" ((g ^\ 1) ^\ 1)) is V11() real ext-real Element of REAL
lim ((f ^\ 2) /" (g ^\ 1)) is V11() real ext-real Element of REAL
1 * () is V11() real ext-real set
lim ((g ^\ 1) /" (f ^\ 1)) is V11() real ext-real Element of REAL
lim ((f ^\ 2) /" (f ^\ 1)) is V11() real ext-real Element of REAL
() * 1 is V11() real ext-real set