REAL is set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL
bool REAL is set
COMPLEX is set
omega is non empty epsilon-transitive epsilon-connected ordinal set
bool omega is set
bool NAT is set
[:NAT,REAL:] is set
bool [:NAT,REAL:] is set
K99(REAL,REAL,NAT,NAT) is Element of bool [:REAL,REAL:]
[:REAL,REAL:] is set
bool [:REAL,REAL:] is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative integer set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative integer set
Fib 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
Fib 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
sqrt 0 is V11() real ext-real Element of REAL
sqrt 1 is V11() real ext-real Element of REAL
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
sqrt 4 is V11() real ext-real Element of REAL
tau is non empty V11() real ext-real positive non negative set
5 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer 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
tau_bar is non empty V11() real ext-real non positive negative set
1 - (sqrt 5) is V11() real ext-real set
(1 - (sqrt 5)) / 2 is V11() real ext-real Element of COMPLEX
Lucas 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
Lucas 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
Lucas 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
Lucas 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
Lucas 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
7 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
- 1 is non empty V11() real ext-real non positive negative integer set
Fib 2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
Fib 4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
- s5 is V11() real ext-real non positive integer set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
(- 1) to_power n is V11() real ext-real set
(- 1) |^ n is V11() real ext-real set
s5 * ((- 1) to_power n) is V11() real ext-real set
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
- s5 is V11() real ext-real non positive integer set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
(- 1) to_power n is V11() real ext-real set
(- 1) |^ n is V11() real ext-real set
s5 * ((- 1) to_power n) is V11() real ext-real set
- (s5 * ((- 1) to_power n)) is V11() real ext-real set
s5 is V11() real ext-real set
n is V11() real ext-real set
s5 / n is V11() real ext-real Element of COMPLEX
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
(s5 / n) to_power k is V11() real ext-real set
(s5 / n) |^ k is V11() real ext-real set
s5 to_power k is V11() real ext-real set
s5 |^ k is V11() real ext-real set
n to_power k is V11() real ext-real set
n |^ k is V11() real ext-real set
(s5 to_power k) / (n to_power k) is V11() real ext-real Element of COMPLEX
1 / n is V11() real ext-real Element of COMPLEX
s5 * (1 / n) is V11() real ext-real set
(s5 * (1 / n)) |^ k is V11() real ext-real set
(1 / n) |^ k is V11() real ext-real set
(s5 to_power k) * ((1 / n) |^ k) is V11() real ext-real set
1 / (n |^ k) is V11() real ext-real Element of COMPLEX
(s5 to_power k) * (1 / (n |^ k)) is V11() real ext-real set
(s5 to_power k) / (n |^ k) is V11() real ext-real Element of COMPLEX
s5 is V11() real ext-real set
n is V11() real ext-real integer set
k is V11() real ext-real integer set
n + k is V11() real ext-real integer set
s5 to_power (n + k) is V11() real ext-real set
s5 to_power n is V11() real ext-real set
s5 to_power k is V11() real ext-real set
(s5 to_power n) * (s5 to_power k) is V11() real ext-real set
s5 #Z n is V11() real ext-real set
(s5 #Z n) * (s5 to_power k) is V11() real ext-real set
s5 #Z k is V11() real ext-real set
(s5 #Z n) * (s5 #Z k) is V11() real ext-real set
s5 #Z (n + k) is V11() real ext-real set
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
n is V11() real ext-real set
- n is V11() real ext-real set
(- n) to_power s5 is V11() real ext-real set
(- n) |^ s5 is V11() real ext-real set
n to_power s5 is V11() real ext-real set
n |^ s5 is V11() real ext-real set
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
n is V11() real ext-real set
- n is V11() real ext-real set
(- n) to_power s5 is V11() real ext-real set
(- n) |^ s5 is V11() real ext-real set
n to_power s5 is V11() real ext-real set
n |^ s5 is V11() real ext-real set
- (n to_power s5) is V11() real ext-real set
tau * tau_bar is non empty V11() real ext-real non positive negative set
1 ^2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
1 * 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
(sqrt 5) ^2 is V11() real ext-real Element of REAL
(sqrt 5) * (sqrt 5) is V11() real ext-real set
(1 ^2) - ((sqrt 5) ^2) is V11() real ext-real set
((1 ^2) - ((sqrt 5) ^2)) / 4 is V11() real ext-real Element of COMPLEX
1 - 5 is V11() real ext-real integer set
(1 - 5) / 4 is V11() real ext-real Element of COMPLEX
tau_bar / tau is non empty V11() real ext-real non positive negative Element of COMPLEX
(sqrt 5) - 3 is V11() real ext-real set
((sqrt 5) - 3) / 2 is V11() real ext-real Element of COMPLEX
- (sqrt 5) is V11() real ext-real set
(- 1) + 1 is V11() real ext-real integer set
(- (sqrt 5)) + 1 is V11() real ext-real set
(1 - (sqrt 5)) * 2 is V11() real ext-real set
(1 + (sqrt 5)) * 2 is V11() real ext-real set
((1 - (sqrt 5)) * 2) / ((1 + (sqrt 5)) * 2) is V11() real ext-real Element of COMPLEX
(1 - (sqrt 5)) / (1 + (sqrt 5)) is V11() real ext-real Element of COMPLEX
(1 - (sqrt 5)) * (1 - (sqrt 5)) is V11() real ext-real set
(1 + (sqrt 5)) * (1 - (sqrt 5)) is V11() real ext-real set
((1 - (sqrt 5)) * (1 - (sqrt 5))) / ((1 + (sqrt 5)) * (1 - (sqrt 5))) is V11() real ext-real Element of COMPLEX
2 * (sqrt 5) is V11() real ext-real set
1 - (2 * (sqrt 5)) is V11() real ext-real set
(sqrt 5) ^2 is V11() real ext-real Element of REAL
(sqrt 5) * (sqrt 5) is V11() real ext-real set
(1 - (2 * (sqrt 5))) + ((sqrt 5) ^2) is V11() real ext-real set
1 ^2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
1 * 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
(1 ^2) - ((sqrt 5) ^2) is V11() real ext-real set
((1 - (2 * (sqrt 5))) + ((sqrt 5) ^2)) / ((1 ^2) - ((sqrt 5) ^2)) is V11() real ext-real Element of COMPLEX
(1 - (2 * (sqrt 5))) + 5 is V11() real ext-real set
((1 - (2 * (sqrt 5))) + 5) / ((1 ^2) - ((sqrt 5) ^2)) is V11() real ext-real Element of COMPLEX
6 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
6 - (2 * (sqrt 5)) is V11() real ext-real set
(1 ^2) - 5 is V11() real ext-real integer set
(6 - (2 * (sqrt 5))) / ((1 ^2) - 5) is V11() real ext-real Element of COMPLEX
3 - (sqrt 5) is V11() real ext-real set
2 * (3 - (sqrt 5)) is V11() real ext-real set
- 2 is non empty V11() real ext-real non positive negative integer set
(- 2) * 2 is non empty V11() real ext-real non positive negative integer even set
(2 * (3 - (sqrt 5))) / ((- 2) * 2) is V11() real ext-real Element of COMPLEX
tau / tau_bar is non empty V11() real ext-real non positive negative Element of COMPLEX
- 3 is non empty V11() real ext-real non positive negative integer set
(- 3) - (sqrt 5) is V11() real ext-real set
((- 3) - (sqrt 5)) / 2 is V11() real ext-real Element of COMPLEX
(1 + (sqrt 5)) * 2 is V11() real ext-real set
(1 - (sqrt 5)) * 2 is V11() real ext-real set
((1 + (sqrt 5)) * 2) / ((1 - (sqrt 5)) * 2) is V11() real ext-real Element of COMPLEX
(1 + (sqrt 5)) / (1 - (sqrt 5)) is V11() real ext-real Element of COMPLEX
(1 + (sqrt 5)) * (1 + (sqrt 5)) is V11() real ext-real set
(1 - (sqrt 5)) * (1 + (sqrt 5)) is V11() real ext-real set
((1 + (sqrt 5)) * (1 + (sqrt 5))) / ((1 - (sqrt 5)) * (1 + (sqrt 5))) is V11() real ext-real Element of COMPLEX
(sqrt 5) ^2 is V11() real ext-real Element of REAL
(sqrt 5) * (sqrt 5) is V11() real ext-real set
1 - ((sqrt 5) ^2) is V11() real ext-real set
((1 + (sqrt 5)) * (1 + (sqrt 5))) / (1 - ((sqrt 5) ^2)) is V11() real ext-real Element of COMPLEX
1 - 5 is V11() real ext-real integer set
((1 + (sqrt 5)) * (1 + (sqrt 5))) / (1 - 5) is V11() real ext-real Element of COMPLEX
2 * (sqrt 5) is V11() real ext-real set
1 + (2 * (sqrt 5)) is V11() real ext-real set
(1 + (2 * (sqrt 5))) + ((sqrt 5) ^2) is V11() real ext-real set
- 4 is non empty V11() real ext-real non positive negative integer set
((1 + (2 * (sqrt 5))) + ((sqrt 5) ^2)) / (- 4) is V11() real ext-real Element of COMPLEX
(1 + (2 * (sqrt 5))) + 5 is V11() real ext-real set
((1 + (2 * (sqrt 5))) + 5) / (- 4) is V11() real ext-real Element of COMPLEX
tau to_power 2 is V11() real ext-real set
tau |^ 2 is V11() real ext-real set
3 + (sqrt 5) is V11() real ext-real set
(3 + (sqrt 5)) / 2 is V11() real ext-real Element of COMPLEX
((1 + (sqrt 5)) / 2) ^2 is V11() real ext-real Element of COMPLEX
((1 + (sqrt 5)) / 2) * ((1 + (sqrt 5)) / 2) is V11() real ext-real set
1 ^2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
1 * 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
2 * 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer even set
(2 * 1) * (sqrt 5) is V11() real ext-real set
(1 ^2) + ((2 * 1) * (sqrt 5)) is V11() real ext-real set
(sqrt 5) ^2 is V11() real ext-real Element of REAL
(sqrt 5) * (sqrt 5) is V11() real ext-real set
((1 ^2) + ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2) is V11() real ext-real set
(((1 ^2) + ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2)) / 4 is V11() real ext-real Element of COMPLEX
2 * (sqrt 5) is V11() real ext-real set
1 + (2 * (sqrt 5)) is V11() real ext-real set
(1 + (2 * (sqrt 5))) + 5 is V11() real ext-real set
((1 + (2 * (sqrt 5))) + 5) / 4 is V11() real ext-real Element of COMPLEX
2 * (3 + (sqrt 5)) is V11() real ext-real set
2 * 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer even set
(2 * (3 + (sqrt 5))) / (2 * 2) is V11() real ext-real Element of COMPLEX
tau_bar to_power 2 is V11() real ext-real set
tau_bar |^ 2 is V11() real ext-real set
3 - (sqrt 5) is V11() real ext-real set
(3 - (sqrt 5)) / 2 is V11() real ext-real Element of COMPLEX
((1 - (sqrt 5)) / 2) ^2 is V11() real ext-real Element of COMPLEX
((1 - (sqrt 5)) / 2) * ((1 - (sqrt 5)) / 2) is V11() real ext-real set
1 ^2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
1 * 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
2 * 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer even set
(2 * 1) * (sqrt 5) is V11() real ext-real set
(1 ^2) - ((2 * 1) * (sqrt 5)) is V11() real ext-real set
(sqrt 5) ^2 is V11() real ext-real Element of REAL
(sqrt 5) * (sqrt 5) is V11() real ext-real set
((1 ^2) - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2) is V11() real ext-real set
(((1 ^2) - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2)) / 4 is V11() real ext-real Element of COMPLEX
2 * (sqrt 5) is V11() real ext-real set
1 - (2 * (sqrt 5)) is V11() real ext-real set
(1 - (2 * (sqrt 5))) + 5 is V11() real ext-real set
((1 - (2 * (sqrt 5))) + 5) / 4 is V11() real ext-real Element of COMPLEX
2 * (3 - (sqrt 5)) is V11() real ext-real set
2 * 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer even set
(2 * (3 - (sqrt 5))) / (2 * 2) is V11() real ext-real Element of COMPLEX
tau_bar to_power 3 is V11() real ext-real set
tau_bar |^ 3 is V11() real ext-real set
2 - (sqrt 5) is V11() real ext-real set
(sqrt 5) - (sqrt 5) is V11() real ext-real set
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
((1 - (sqrt 5)) / 2) to_power (2 + 1) is V11() real ext-real set
((1 - (sqrt 5)) / 2) |^ (2 + 1) is V11() real ext-real set
((1 - (sqrt 5)) / 2) to_power 2 is V11() real ext-real set
((1 - (sqrt 5)) / 2) |^ 2 is V11() real ext-real set
((1 - (sqrt 5)) / 2) to_power 1 is V11() real ext-real set
((1 - (sqrt 5)) / 2) |^ 1 is V11() real ext-real set
(((1 - (sqrt 5)) / 2) to_power 2) * (((1 - (sqrt 5)) / 2) to_power 1) is V11() real ext-real set
(((1 - (sqrt 5)) / 2) to_power 2) * ((1 - (sqrt 5)) / 2) is V11() real ext-real set
((1 - (sqrt 5)) / 2) ^2 is V11() real ext-real Element of COMPLEX
((1 - (sqrt 5)) / 2) * ((1 - (sqrt 5)) / 2) is V11() real ext-real set
(((1 - (sqrt 5)) / 2) ^2) * ((1 - (sqrt 5)) / 2) is V11() real ext-real Element of COMPLEX
2 * 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer even set
(2 * 1) * (sqrt 5) is V11() real ext-real set
1 - ((2 * 1) * (sqrt 5)) is V11() real ext-real set
(sqrt 5) ^2 is V11() real ext-real Element of REAL
(sqrt 5) * (sqrt 5) is V11() real ext-real set
(1 - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2) is V11() real ext-real set
((1 - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2)) * (1 - (sqrt 5)) is V11() real ext-real set
8 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
(((1 - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2)) * (1 - (sqrt 5))) / 8 is V11() real ext-real Element of COMPLEX
2 * (sqrt 5) is V11() real ext-real set
1 - (2 * (sqrt 5)) is V11() real ext-real set
(1 - (2 * (sqrt 5))) + 5 is V11() real ext-real set
((1 - (2 * (sqrt 5))) + 5) * (1 - (sqrt 5)) is V11() real ext-real set
(((1 - (2 * (sqrt 5))) + 5) * (1 - (sqrt 5))) / 8 is V11() real ext-real Element of COMPLEX
6 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
8 * (sqrt 5) is V11() real ext-real set
6 - (8 * (sqrt 5)) is V11() real ext-real set
2 * ((sqrt 5) ^2) is V11() real ext-real set
(6 - (8 * (sqrt 5))) + (2 * ((sqrt 5) ^2)) is V11() real ext-real set
((6 - (8 * (sqrt 5))) + (2 * ((sqrt 5) ^2))) / 8 is V11() real ext-real Element of COMPLEX
2 * 5 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer even set
(6 - (8 * (sqrt 5))) + (2 * 5) is V11() real ext-real set
((6 - (8 * (sqrt 5))) + (2 * 5)) / 8 is V11() real ext-real Element of COMPLEX
6 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
tau_bar to_power 6 is V11() real ext-real set
tau_bar |^ 6 is V11() real ext-real set
9 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
4 * (sqrt 5) is V11() real ext-real set
9 - (4 * (sqrt 5)) is V11() real ext-real set
3 * 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer even set
tau_bar to_power (3 * 2) is V11() real ext-real set
tau_bar |^ (3 * 2) is V11() real ext-real set
(2 - (sqrt 5)) to_power 2 is V11() real ext-real set
(2 - (sqrt 5)) |^ 2 is V11() real ext-real set
(2 - (sqrt 5)) ^2 is V11() real ext-real set
(2 - (sqrt 5)) * (2 - (sqrt 5)) is V11() real ext-real set
2 ^2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
2 * 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer even set
(2 * 2) * (sqrt 5) is V11() real ext-real set
(2 ^2) - ((2 * 2) * (sqrt 5)) is V11() real ext-real set
(sqrt 5) ^2 is V11() real ext-real Element of REAL
(sqrt 5) * (sqrt 5) is V11() real ext-real set
((2 ^2) - ((2 * 2) * (sqrt 5))) + ((sqrt 5) ^2) is V11() real ext-real set
4 - (4 * (sqrt 5)) is V11() real ext-real set
(4 - (4 * (sqrt 5))) + 5 is V11() real ext-real set
abs tau_bar is non empty V11() real ext-real positive non negative Element of REAL
3 ^2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
3 * 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
sqrt (3 ^2) is V11() real ext-real set
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
(2 + 1) - 1 is V11() real ext-real integer set
(sqrt 5) - 1 is V11() real ext-real set
- ((sqrt 5) - 1) is V11() real ext-real set
- 2 is non empty V11() real ext-real non positive negative integer set
(- 2) / 2 is non empty V11() real ext-real non positive negative Element of COMPLEX
abs (- 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of REAL
abs 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative integer Element of REAL
(abs (- 1)) + (abs 0) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
- (- 1) is non empty V11() real ext-real positive non negative integer set
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
1 / (sqrt 5) is V11() real ext-real Element of COMPLEX
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
(abs tau_bar) to_power s5 is V11() real ext-real set
(abs tau_bar) |^ s5 is V11() real ext-real set
((abs tau_bar) to_power s5) * (1 / (sqrt 5)) is V11() real ext-real set
1 / 2 is non empty V11() real ext-real positive non negative Element of COMPLEX
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
(abs tau_bar) to_power s5 is V11() real ext-real set
(abs tau_bar) |^ s5 is V11() real ext-real set
((abs tau_bar) to_power s5) * (1 / (sqrt 5)) is V11() real ext-real set
(sqrt 5) / 2 is V11() real ext-real Element of COMPLEX
2 / 2 is non empty V11() real ext-real positive non negative Element of COMPLEX
1 to_power s5 is V11() real ext-real set
1 |^ s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
(sqrt 5) / 1 is V11() real ext-real Element of COMPLEX
((sqrt 5) / 2) / ((sqrt 5) / 1) is V11() real ext-real Element of COMPLEX
((abs tau_bar) to_power s5) / ((sqrt 5) / 1) is V11() real ext-real Element of COMPLEX
1 * (sqrt 5) is V11() real ext-real set
2 * (sqrt 5) is V11() real ext-real set
(1 * (sqrt 5)) / (2 * (sqrt 5)) is V11() real ext-real Element of COMPLEX
((abs tau_bar) to_power s5) / (sqrt 5) is V11() real ext-real Element of COMPLEX
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
n is non empty V11() real ext-real set
n to_power s5 is V11() real ext-real set
n |^ s5 is V11() real ext-real set
- n is non empty V11() real ext-real set
(- n) to_power s5 is V11() real ext-real set
(- n) |^ s5 is V11() real ext-real set
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
n is V11() real ext-real set
n to_power s5 is V11() real ext-real set
n |^ s5 is V11() real ext-real set
- n is V11() real ext-real set
- (- n) is V11() real ext-real set
(- (- n)) to_power s5 is V11() real ext-real set
(- (- n)) |^ s5 is V11() real ext-real set
(- n) to_power s5 is V11() real ext-real set
(- n) |^ s5 is V11() real ext-real set
- ((- n) to_power s5) is V11() real ext-real set
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
tau_bar to_power s5 is V11() real ext-real set
tau_bar |^ s5 is V11() real ext-real set
s5 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
(abs tau_bar) to_power 2 is V11() real ext-real Element of REAL
(abs tau_bar) |^ 2 is V11() real ext-real set
- tau_bar is non empty V11() real ext-real positive non negative set
(- tau_bar) to_power 2 is V11() real ext-real set
(- tau_bar) |^ 2 is V11() real ext-real set
(- tau_bar) ^2 is V11() real ext-real set
(- tau_bar) * (- tau_bar) is non empty V11() real ext-real positive non negative set
1 ^2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
1 * 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
2 * 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer even set
(2 * 1) * (sqrt 5) is V11() real ext-real set
(1 ^2) - ((2 * 1) * (sqrt 5)) is V11() real ext-real set
(sqrt 5) ^2 is V11() real ext-real Element of REAL
(sqrt 5) * (sqrt 5) is V11() real ext-real set
((1 ^2) - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2) is V11() real ext-real set
(((1 ^2) - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2)) / 4 is V11() real ext-real Element of COMPLEX
2 * (sqrt 5) is V11() real ext-real set
1 - (2 * (sqrt 5)) is V11() real ext-real set
(1 - (2 * (sqrt 5))) + 5 is V11() real ext-real set
((1 - (2 * (sqrt 5))) + 5) / 4 is V11() real ext-real Element of COMPLEX
- 2 is non empty V11() real ext-real non positive negative integer set
- (sqrt 5) is V11() real ext-real set
(- 2) + 3 is V11() real ext-real integer set
(- (sqrt 5)) + 3 is V11() real ext-real set
(abs tau_bar) to_power 2 is V11() real ext-real set
n is non trivial epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
(abs tau_bar) to_power n is V11() real ext-real set
(abs tau_bar) |^ n is V11() real ext-real set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
(abs tau_bar) to_power (n + 1) is V11() real ext-real set
(abs tau_bar) |^ (n + 1) is V11() real ext-real set
(1 / 2) * (abs tau_bar) is non empty V11() real ext-real positive non negative set
((abs tau_bar) to_power n) * (abs tau_bar) is V11() real ext-real set
(abs tau_bar) to_power 1 is V11() real ext-real Element of REAL
(abs tau_bar) |^ 1 is V11() real ext-real set
((abs tau_bar) to_power n) * ((abs tau_bar) to_power 1) is V11() real ext-real set
(1 / 2) * 1 is non empty V11() real ext-real positive non negative set
n is non trivial epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
tau_bar to_power n is V11() real ext-real set
tau_bar |^ n is V11() real ext-real set
(abs tau_bar) to_power n is V11() real ext-real set
(abs tau_bar) |^ n is V11() real ext-real set
abs (tau_bar to_power n) is V11() real ext-real non negative Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
k is V11() real ext-real set
k to_power n is V11() real ext-real set
k |^ n is V11() real ext-real set
k to_power s5 is V11() real ext-real set
k |^ s5 is V11() real ext-real set
s5 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
n + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
s5 - n is V11() real ext-real integer set
(k to_power s5) - (k to_power n) is V11() real ext-real set
tb is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
tb + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
k to_power (tb + n) is V11() real ext-real set
k |^ (tb + n) is V11() real ext-real set
(k to_power (tb + n)) - (k to_power n) is V11() real ext-real set
k to_power tb is V11() real ext-real set
k |^ tb is V11() real ext-real set
(k to_power tb) * (k to_power n) is V11() real ext-real set
1 * (k to_power n) is V11() real ext-real set
((k to_power tb) * (k to_power n)) - (1 * (k to_power n)) is V11() real ext-real set
(k to_power tb) - 1 is V11() real ext-real set
((k to_power tb) - 1) * (k to_power n) is V11() real ext-real set
abs k is V11() real ext-real non negative Element of REAL
abs 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of REAL
1 to_power tb is V11() real ext-real set
1 |^ tb is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
(abs k) to_power tb is V11() real ext-real set
(abs k) |^ tb is V11() real ext-real set
abs (k to_power tb) is V11() real ext-real non negative Element of REAL
1 - 1 is V11() real ext-real integer set
0 + (k to_power n) is V11() real ext-real set
((k to_power s5) - (k to_power n)) + (k to_power n) is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
tau_bar to_power n is V11() real ext-real set
tau_bar |^ n is V11() real ext-real set
tau_bar to_power s5 is V11() real ext-real set
tau_bar |^ s5 is V11() real ext-real set
s5 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
n + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
s5 - n is V11() real ext-real integer set
(tau_bar to_power s5) - (tau_bar to_power n) is V11() real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
k + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
tau_bar to_power (k + n) is V11() real ext-real set
tau_bar |^ (k + n) is V11() real ext-real set
(tau_bar to_power (k + n)) - (tau_bar to_power n) is V11() real ext-real set
tau_bar to_power k is V11() real ext-real set
tau_bar |^ k is V11() real ext-real set
(tau_bar to_power k) * (tau_bar to_power n) is V11() real ext-real set
1 * (tau_bar to_power n) is V11() real ext-real set
((tau_bar to_power k) * (tau_bar to_power n)) - (1 * (tau_bar to_power n)) is V11() real ext-real set
(tau_bar to_power k) - 1 is V11() real ext-real set
((tau_bar to_power k) - 1) * (tau_bar to_power n) is V11() real ext-real set
1 to_power k is V11() real ext-real set
1 |^ k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
(abs tau_bar) to_power k is V11() real ext-real set
(abs tau_bar) |^ k is V11() real ext-real set
abs (tau_bar to_power k) is V11() real ext-real non negative Element of REAL
1 - 1 is V11() real ext-real integer set
0 + (tau_bar to_power n) is V11() real ext-real set
((tau_bar to_power s5) - (tau_bar to_power n)) + (tau_bar to_power n) is V11() real ext-real set
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
tau_bar to_power s5 is V11() real ext-real set
tau_bar |^ s5 is V11() real ext-real set
tau_bar to_power n is V11() real ext-real set
tau_bar |^ n is V11() real ext-real set
s5 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
n + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
s5 - n is V11() real ext-real integer set
(tau_bar to_power s5) - (tau_bar to_power n) is V11() real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
k + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
tau_bar to_power (k + n) is V11() real ext-real set
tau_bar |^ (k + n) is V11() real ext-real set
(tau_bar to_power (k + n)) - (tau_bar to_power n) is V11() real ext-real set
tau_bar to_power k is V11() real ext-real set
tau_bar |^ k is V11() real ext-real set
(tau_bar to_power k) * (tau_bar to_power n) is V11() real ext-real set
1 * (tau_bar to_power n) is V11() real ext-real set
((tau_bar to_power k) * (tau_bar to_power n)) - (1 * (tau_bar to_power n)) is V11() real ext-real set
(tau_bar to_power k) - 1 is V11() real ext-real set
((tau_bar to_power k) - 1) * (tau_bar to_power n) is V11() real ext-real set
n - n is V11() real ext-real integer set
1 - 1 is V11() real ext-real integer set
0 + (tau_bar to_power n) is V11() real ext-real set
((tau_bar to_power s5) - (tau_bar to_power n)) + (tau_bar to_power n) is V11() real ext-real set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
s5 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
Lucas n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
Lucas s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
n + k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
tb is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
Lucas tb is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
tb + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
Lucas (tb + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
tb - 0 is V11() real ext-real integer set
tb is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
tb + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
tk is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
Lucas tk is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
tk + (tb + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
Lucas (tk + (tb + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
tk + tb is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
tn is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
Lucas (tk + tb) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
(tk + tb) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
Lucas ((tk + tb) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
tk is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
Lucas tk is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
tk + (tb + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
Lucas (tk + (tb + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
tk is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
Lucas tk is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
tb is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
tk + tb is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
Lucas (tk + tb) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
tau_bar ^2 is V11() real ext-real set
tau_bar * tau_bar is non empty V11() real ext-real positive non negative set
(sqrt 5) + 3 is V11() real ext-real set
- (sqrt 5) is V11() real ext-real set
(- (sqrt 5)) + 3 is V11() real ext-real set
((sqrt 5) + 3) / 2 is V11() real ext-real Element of COMPLEX
((- (sqrt 5)) + 3) / 2 is V11() real ext-real Element of COMPLEX
tau ^2 is V11() real ext-real set
tau * tau is non empty V11() real ext-real positive non negative set
3 ^2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
3 * 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
sqrt (3 ^2) is V11() real ext-real set
3 - 3 is V11() real ext-real integer set
s5 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
tau to_power s5 is V11() real ext-real set
tau |^ s5 is V11() real ext-real set
tau_bar to_power s5 is V11() real ext-real set
tau_bar |^ s5 is V11() real ext-real set
s5 - 0 is V11() real ext-real integer set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
2 * k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer even set
(tau to_power 2) to_power k is V11() real ext-real set
(tau to_power 2) |^ k is V11() real ext-real set
(tau ^2) to_power k is V11() real ext-real set
(tau ^2) |^ k is V11() real ext-real set
(tau_bar to_power 2) to_power k is V11() real ext-real set
(tau_bar to_power 2) |^ k is V11() real ext-real set
(tau_bar ^2) to_power k is V11() real ext-real set
(tau_bar ^2) |^ k is V11() real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
2 * k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer even set
(2 * k) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer non even set
tau to_power (2 * k) is V11() real ext-real set
tau |^ (2 * k) is V11() real ext-real set
(tau / tau_bar) to_power (2 * k) is V11() real ext-real set
(tau / tau_bar) |^ (2 * k) is V11() real ext-real set
(tau / tau_bar) to_power 2 is V11() real ext-real set
(tau / tau_bar) |^ 2 is V11() real ext-real set
((tau / tau_bar) to_power 2) to_power k is V11() real ext-real set
((tau / tau_bar) to_power 2) |^ k is V11() real ext-real set
(tau / tau_bar) ^2 is V11() real ext-real Element of COMPLEX
(tau / tau_bar) * (tau / tau_bar) is non empty V11() real ext-real positive non negative set
((tau / tau_bar) ^2) to_power k is V11() real ext-real set
((tau / tau_bar) ^2) |^ k is V11() real ext-real set
tau_bar to_power (2 * k) is V11() real ext-real set
tau_bar |^ (2 * k) is V11() real ext-real set
(tau_bar to_power 2) to_power k is V11() real ext-real set
(tau_bar to_power 2) |^ k is V11() real ext-real set
(tau_bar ^2) to_power k is V11() real ext-real set
(tau_bar ^2) |^ k is V11() real ext-real set
(tau_bar / tau) * (((- 3) - (sqrt 5)) / 2) is V11() real ext-real Element of COMPLEX
((tau / tau_bar) to_power (2 * k)) * (((- 3) - (sqrt 5)) / 2) is V11() real ext-real set
((tau / tau_bar) to_power (2 * k)) * (tau / tau_bar) is V11() real ext-real set
(tau to_power (2 * k)) / (tau_bar to_power (2 * k)) is V11() real ext-real Element of COMPLEX
((tau to_power (2 * k)) / (tau_bar to_power (2 * k))) * (tau / tau_bar) is V11() real ext-real Element of COMPLEX
1 / (tau_bar to_power (2 * k)) is V11() real ext-real Element of COMPLEX
(tau to_power (2 * k)) * (1 / (tau_bar to_power (2 * k))) is V11() real ext-real set
((tau to_power (2 * k)) * (1 / (tau_bar to_power (2 * k)))) * (tau / tau_bar) is V11() real ext-real set
1 * (tau_bar to_power (2 * k)) is V11() real ext-real set
(((tau to_power (2 * k)) * (1 / (tau_bar to_power (2 * k)))) * (tau / tau_bar)) * (tau_bar to_power (2 * k)) is V11() real ext-real set
(tau to_power (2 * k)) * (tau / tau_bar) is V11() real ext-real set
(tau_bar to_power (2 * k)) * (1 / (tau_bar to_power (2 * k))) is V11() real ext-real set
((tau to_power (2 * k)) * (tau / tau_bar)) * ((tau_bar to_power (2 * k)) * (1 / (tau_bar to_power (2 * k)))) is V11() real ext-real set
(tau_bar to_power (2 * k)) / (tau_bar to_power (2 * k)) is V11() real ext-real Element of COMPLEX
((tau to_power (2 * k)) * (tau / tau_bar)) * ((tau_bar to_power (2 * k)) / (tau_bar to_power (2 * k))) is V11() real ext-real set
((tau to_power (2 * k)) * (tau / tau_bar)) * 1 is V11() real ext-real set
1 / tau_bar is non empty V11() real ext-real non positive negative Element of COMPLEX
tau * (1 / tau_bar) is non empty V11() real ext-real non positive negative set
(tau to_power (2 * k)) * (tau * (1 / tau_bar)) is V11() real ext-real set
((tau to_power (2 * k)) * (tau * (1 / tau_bar))) * 1 is V11() real ext-real set
(((tau to_power (2 * k)) * (tau * (1 / tau_bar))) * 1) * tau_bar is V11() real ext-real set
(tau_bar to_power (2 * k)) * tau_bar is V11() real ext-real set
(tau to_power (2 * k)) * tau is V11() real ext-real set
(1 / tau_bar) * 1 is non empty V11() real ext-real non positive negative set
((1 / tau_bar) * 1) * tau_bar is non empty V11() real ext-real positive non negative set
((tau to_power (2 * k)) * tau) * (((1 / tau_bar) * 1) * tau_bar) is V11() real ext-real set
tau_bar / tau_bar is non empty V11() real ext-real positive non negative Element of COMPLEX
((tau to_power (2 * k)) * tau) * (tau_bar / tau_bar) is V11() real ext-real set
((tau to_power (2 * k)) * tau) * 1 is V11() real ext-real set
tau_bar to_power 1 is V11() real ext-real set
tau_bar |^ 1 is V11() real ext-real set
(tau_bar to_power (2 * k)) * (tau_bar to_power 1) is V11() real ext-real set
tau_bar to_power ((2 * k) + 1) is V11() real ext-real set
tau_bar |^ ((2 * k) + 1) is V11() real ext-real set
tau to_power 1 is V11() real ext-real set
tau |^ 1 is V11() real ext-real set
(tau to_power (2 * k)) * (tau to_power 1) is V11() real ext-real set
- (1 / 2) is non empty V11() real ext-real non positive negative Element of COMPLEX
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
tau_bar to_power s5 is V11() real ext-real set
tau_bar |^ s5 is V11() real ext-real set
s5 - 0 is V11() real ext-real integer set
s5 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
2 * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer even set
0 ^2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
0 * 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
tau_bar to_power n is V11() real ext-real set
tau_bar |^ n is V11() real ext-real set
(tau_bar to_power n) to_power 2 is V11() real ext-real set
(tau_bar to_power n) |^ 2 is V11() real ext-real set
(tau_bar to_power n) ^2 is V11() real ext-real set
(tau_bar to_power n) * (tau_bar to_power n) is V11() real ext-real set
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
5 / 2 is non empty V11() real ext-real positive non negative Element of COMPLEX
(5 / 2) ^2 is V11() real ext-real Element of COMPLEX
(5 / 2) * (5 / 2) is non empty V11() real ext-real positive non negative set
sqrt ((5 / 2) ^2) is V11() real ext-real set
2 * (5 / 2) is non empty V11() real ext-real positive non negative set
2 * (sqrt 5) is V11() real ext-real set
- (2 * (sqrt 5)) is V11() real ext-real set
- 5 is non empty V11() real ext-real non positive negative integer set
(- (2 * (sqrt 5))) + 4 is V11() real ext-real set
(- 5) + 4 is V11() real ext-real integer set
2 * (2 - (sqrt 5)) is V11() real ext-real set
(2 * (2 - (sqrt 5))) / 2 is V11() real ext-real Element of COMPLEX
(- 1) / 2 is non empty V11() real ext-real non positive negative Element of COMPLEX
- (1 / (sqrt 5)) is V11() real ext-real Element of COMPLEX
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
tau_bar to_power s5 is V11() real ext-real set
tau_bar |^ s5 is V11() real ext-real set
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
2 * 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer even set
2 * (sqrt 5) is V11() real ext-real set
4 - 5 is V11() real ext-real integer set
(2 * (sqrt 5)) - 5 is V11() real ext-real set
(sqrt 5) ^2 is V11() real ext-real Element of REAL
(sqrt 5) * (sqrt 5) is V11() real ext-real set
(2 * (sqrt 5)) - ((sqrt 5) ^2) is V11() real ext-real set
(- 1) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(2 - (sqrt 5)) * (sqrt 5) is V11() real ext-real set
((2 - (sqrt 5)) * (sqrt 5)) / (sqrt 5) is V11() real ext-real Element of COMPLEX
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
tau_bar to_power s5 is V11() real ext-real set
tau_bar |^ s5 is V11() real ext-real set
7 / 3 is non empty V11() real ext-real positive non negative Element of COMPLEX
(7 / 3) ^2 is V11() real ext-real Element of COMPLEX
(7 / 3) * (7 / 3) is non empty V11() real ext-real positive non negative set
sqrt ((7 / 3) ^2) is V11() real ext-real set
3 * (sqrt 5) is V11() real ext-real set
(7 / 3) * 3 is non empty V11() real ext-real positive non negative set
(3 * (sqrt 5)) - 5 is V11() real ext-real set
7 - 5 is V11() real ext-real integer set
(sqrt 5) ^2 is V11() real ext-real Element of REAL
(sqrt 5) * (sqrt 5) is V11() real ext-real set
(3 * (sqrt 5)) - ((sqrt 5) ^2) is V11() real ext-real set
(3 * (sqrt 5)) - ((sqrt 5) * (sqrt 5)) is V11() real ext-real set
((3 * (sqrt 5)) - ((sqrt 5) * (sqrt 5))) / 2 is V11() real ext-real Element of COMPLEX
2 / 2 is non empty V11() real ext-real positive non negative Element of COMPLEX
((3 - (sqrt 5)) / 2) * (sqrt 5) is V11() real ext-real set
(((3 - (sqrt 5)) / 2) * (sqrt 5)) / (sqrt 5) is V11() real ext-real Element of COMPLEX
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
tau_bar to_power s5 is V11() real ext-real set
tau_bar |^ s5 is V11() real ext-real set
(tau_bar to_power s5) / (sqrt 5) is V11() real ext-real Element of COMPLEX
((tau_bar to_power s5) / (sqrt 5)) + (1 / 2) is V11() real ext-real Element of COMPLEX
abs ((1 - (sqrt 5)) / 2) is V11() real ext-real non negative Element of REAL
- ((1 - (sqrt 5)) / 2) is V11() real ext-real Element of COMPLEX
(abs ((1 - (sqrt 5)) / 2)) to_power s5 is V11() real ext-real set
(abs ((1 - (sqrt 5)) / 2)) |^ s5 is V11() real ext-real set
((abs ((1 - (sqrt 5)) / 2)) to_power s5) * (1 / (sqrt 5)) is V11() real ext-real set
((1 - (sqrt 5)) / 2) to_power s5 is V11() real ext-real set
((1 - (sqrt 5)) / 2) |^ s5 is V11() real ext-real set
(((1 - (sqrt 5)) / 2) to_power s5) * (1 / (sqrt 5)) is V11() real ext-real set
((((1 - (sqrt 5)) / 2) to_power s5) * (1 / (sqrt 5))) + (1 / 2) is V11() real ext-real set
(1 / 2) + (1 / 2) is non empty V11() real ext-real positive non negative Element of COMPLEX
- (((1 - (sqrt 5)) / 2) to_power s5) is V11() real ext-real set
(- (((1 - (sqrt 5)) / 2) to_power s5)) * (1 / (sqrt 5)) is V11() real ext-real set
- ((((1 - (sqrt 5)) / 2) to_power s5) * (1 / (sqrt 5))) is V11() real ext-real set
(((1 - (sqrt 5)) / 2) to_power s5) / (sqrt 5) is V11() real ext-real Element of COMPLEX
- ((((1 - (sqrt 5)) / 2) to_power s5) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
- (- ((((1 - (sqrt 5)) / 2) to_power s5) / (sqrt 5))) is V11() real ext-real Element of COMPLEX
0 + (1 / 2) is non empty V11() real ext-real positive non negative set
((((1 - (sqrt 5)) / 2) to_power s5) / (sqrt 5)) + (1 / 2) is V11() real ext-real Element of COMPLEX
(- (1 / 2)) + (1 / 2) is V11() real ext-real Element of COMPLEX
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
tau to_power s5 is V11() real ext-real set
tau |^ s5 is V11() real ext-real set
(tau to_power s5) / (sqrt 5) is V11() real ext-real Element of COMPLEX
((tau to_power s5) / (sqrt 5)) + (1 / 2) is V11() real ext-real Element of COMPLEX
[\(((tau to_power s5) / (sqrt 5)) + (1 / 2))/] is V11() real ext-real integer set
Fib s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
tau_bar to_power s5 is V11() real ext-real set
tau_bar |^ s5 is V11() real ext-real set
(tau to_power s5) - (tau_bar to_power s5) is V11() real ext-real set
((tau to_power s5) - (tau_bar to_power s5)) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(((tau to_power s5) - (tau_bar to_power s5)) / (sqrt 5)) + (1 / 2) is V11() real ext-real Element of COMPLEX
((((tau to_power s5) - (tau_bar to_power s5)) / (sqrt 5)) + (1 / 2)) - (1 / 2) is V11() real ext-real Element of COMPLEX
(tau_bar to_power s5) / (sqrt 5) is V11() real ext-real Element of COMPLEX
((tau to_power s5) / (sqrt 5)) - ((tau_bar to_power s5) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
(((tau to_power s5) / (sqrt 5)) - ((tau_bar to_power s5) / (sqrt 5))) + (1 / 2) is V11() real ext-real Element of COMPLEX
((((tau to_power s5) / (sqrt 5)) - ((tau_bar to_power s5) / (sqrt 5))) + (1 / 2)) - (1 / 2) is V11() real ext-real Element of COMPLEX
((tau_bar to_power s5) / (sqrt 5)) + (1 / 2) is V11() real ext-real Element of COMPLEX
(((tau to_power s5) / (sqrt 5)) + (1 / 2)) - (((tau_bar to_power s5) / (sqrt 5)) + (1 / 2)) is V11() real ext-real Element of COMPLEX
(((tau_bar to_power s5) / (sqrt 5)) + (1 / 2)) + (Fib s5) is V11() real ext-real set
0 + (Fib s5) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
1 - (1 / 2) is V11() real ext-real set
(((tau_bar to_power s5) / (sqrt 5)) + (1 / 2)) - (1 / 2) is V11() real ext-real Element of COMPLEX
- ((tau_bar to_power s5) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
(- ((tau_bar to_power s5) / (sqrt 5))) + ((tau to_power s5) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
(- (1 / 2)) + ((tau to_power s5) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
(((tau to_power s5) / (sqrt 5)) + (1 / 2)) - 1 is V11() real ext-real set
s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
tau to_power s5 is V11() real ext-real set
tau |^ s5 is V11() real ext-real set
(tau to_power s5) / (sqrt 5) is V11() real ext-real Element of COMPLEX
((tau to_power s5) / (sqrt 5)) - (1 / 2) is V11() real ext-real Element of COMPLEX
[/(((tau to_power s5) / (sqrt 5)) - (1 / 2))\] is V11() real ext-real integer set
Fib s5 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
tau_bar to_power s5 is V11() real ext-real set
tau_bar |^ s5 is V11() real ext-real set
(sqrt 5) / 2 is V11() real ext-real Element of COMPLEX
(tau_bar to_power s5) / (sqrt 5) is V11() real ext-real Element of COMPLEX
((sqrt 5) / 2) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(sqrt 5) / (sqrt 5) is V11() real ext-real Element of COMPLEX
((sqrt 5) / (sqrt 5)) / 2 is V11() real ext-real Element of COMPLEX
- ((tau_bar to_power s5) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
(- (1 / 2)) + ((tau to_power s5) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
(- ((tau_bar to_power s5) / (sqrt 5))) + ((tau to_power s5) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
((tau to_power s5) / (sqrt 5)) - ((tau_bar to_power s5) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
(tau to_power s5) - (tau_bar to_power s5) is V11() real ext-real set
((tau to_power s5) - (tau_bar to_power s5)) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(((tau to_power s5) / (sqrt 5)) - (1 / 2)) + 1 is V11() real ext-real set
s5 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
tau / (sqrt 5) is V11() real ext-real Element of COMPLEX
(tau / (sqrt 5)) - (1 / 2) is V11() real ext-real Element of COMPLEX
((tau / (sqrt 5)) - (1 / 2)) + 1 is V11() real ext-real set
((1 + (sqrt 5)) / 2) / (sqrt 5) is V11() real ext-real Element of COMPLEX
1 - (1 / 2) is V11() real ext-real set
(((1 + (sqrt 5)) / 2) / (sqrt 5)) + (1 - (1 / 2)) is V11() real ext-real set
(1 + (sqrt 5)) / (sqrt 5) is V11() real ext-real Element of COMPLEX
((1 + (sqrt 5)) / (sqrt 5)) / 2 is V11() real ext-real Element of COMPLEX
(((1 + (sqrt 5)) / (sqrt 5)) / 2) + (1 / 2) is V11() real ext-real Element of COMPLEX
((1 + (sqrt 5)) / (sqrt 5)) + 1 is V11() real ext-real set
(((1 + (sqrt 5)) / (sqrt 5)) + 1) / 2 is V11() real ext-real Element of COMPLEX
(sqrt 5) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(1 / (sqrt 5)) + ((sqrt 5) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
((1 / (sqrt 5)) + ((sqrt 5) / (sqrt 5))) + 1 is V11() real ext-real set
(((1 / (sqrt 5)) + ((sqrt 5) / (sqrt 5))) + 1) / 2 is V11() real ext-real Element of COMPLEX
(1 / (sqrt 5)) + 1 is V11() real ext-real set
((1 / (sqrt 5)) + 1) + 1 is V11() real ext-real set
(((1 / (sqrt 5)) + 1) + 1) / 2 is V11() real ext-real Element of COMPLEX
(1 / (sqrt 5)) / 2 is V11() real ext-real Element of COMPLEX
2 / 2 is non empty V11() real ext-real positive non negative Element of COMPLEX
((1 / (sqrt 5)) / 2) + (2 / 2) is V11() real ext-real Element of COMPLEX
((1 / (sqrt 5)) / 2) + 1 is V11() real ext-real set
(sqrt 5) / 2 is V11() real ext-real Element of COMPLEX
- ((sqrt 5) / 2) is V11() real ext-real Element of COMPLEX
(tau_bar to_power s5) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(- ((sqrt 5) / 2)) / (sqrt 5) is V11() real ext-real Element of COMPLEX
((sqrt 5) / 2) / (sqrt 5) is V11() real ext-real Element of COMPLEX
- (((sqrt 5) / 2) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
(sqrt 5) / (sqrt 5) is V11() real ext-real Element of COMPLEX
((sqrt 5) / (sqrt 5)) / 2 is V11() real ext-real Element of COMPLEX
- (((sqrt 5) / (sqrt 5)) / 2) is V11() real ext-real Element of COMPLEX
- (- (1 / 2)) is non empty V11() real ext-real positive non negative Element of COMPLEX
- ((tau_bar to_power s5) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
(1 / 2) + ((tau to_power s5) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
(- ((tau_bar to_power s5) / (sqrt 5))) + ((tau to_power s5) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
((tau to_power s5) / (sqrt 5)) - ((tau_bar to_power s5) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
(tau to_power s5) - (tau_bar to_power s5) is V11() real ext-real set
((tau to_power s5) - (tau_bar to_power s5)) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(1 - (sqrt 5)) ^2 is V11() real ext-real set
(1 - (sqrt 5)) * (1 - (sqrt 5)) is V11() real ext-real set
(1 - (sqrt 5)) to_power 2 is V11() real ext-real set
(1 - (sqrt 5)) |^ 2 is V11() real ext-real set
2 * (sqrt 5) is V11() real ext-real set
2 * 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer even set
- 2 is non empty V11() real ext-real non positive negative integer set
- (2 * (sqrt 5)) is V11() real ext-real set
(- 2) + 6 is V11() real ext-real integer set
(- (2 * (sqrt 5))) + 6 is V11() real ext-real set
1 - (2 * (sqrt 5)) is V11() real ext-real set
(1 - (2 * (sqrt 5))) + 5 is V11() real ext-real set
1 ^2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
1 * 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
(2 * 1) * (sqrt 5) is V11() real ext-real set
(1 ^2) - ((2 * 1) * (sqrt 5)) is V11() real ext-real set
(sqrt 5) ^2 is V11() real ext-real Element of REAL
(sqrt 5) * (sqrt 5) is V11() real ext-real set
((1 ^2) - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2) is V11() real ext-real set
2 ^2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
2 * 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer even set
2 to_power 2 is V11() real ext-real Element of REAL
2 |^ 2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
2 * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer even set
tau to_power (2 * n) is V11() real ext-real set
tau |^ (2 * n) is V11() real ext-real set
(tau to_power (2 * n)) / (sqrt 5) is V11() real ext-real Element of COMPLEX
[\((tau to_power (2 * n)) / (sqrt 5))/] is V11() real ext-real integer set
Fib (2 * n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
((tau to_power (2 * n)) / (sqrt 5)) - 1 is V11() real ext-real set
2 to_power (2 * n) is V11() real ext-real set
2 |^ (2 * n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
(2 to_power 2) to_power n is V11() real ext-real set
(2 to_power 2) |^ n is V11() real ext-real set
((1 - (sqrt 5)) to_power 2) to_power n is V11() real ext-real set
((1 - (sqrt 5)) to_power 2) |^ n is V11() real ext-real set
(1 - (sqrt 5)) to_power (2 * n) is V11() real ext-real set
(1 - (sqrt 5)) |^ (2 * n) is V11() real ext-real set
(2 to_power (2 * n)) / (2 to_power (2 * n)) is V11() real ext-real Element of COMPLEX
((1 - (sqrt 5)) to_power (2 * n)) / (2 to_power (2 * n)) is V11() real ext-real Element of COMPLEX
tau_bar to_power (2 * n) is V11() real ext-real set
tau_bar |^ (2 * n) is V11() real ext-real set
(sqrt 5) / (sqrt 5) is V11() real ext-real Element of COMPLEX
(tau_bar to_power (2 * n)) / (sqrt 5) is V11() real ext-real Element of COMPLEX
- ((tau_bar to_power (2 * n)) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
(- ((tau_bar to_power (2 * n)) / (sqrt 5))) + ((tau to_power (2 * n)) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
(- 1) + ((tau to_power (2 * n)) / (sqrt 5)) is V11() real ext-real set
((tau to_power (2 * n)) / (sqrt 5)) - ((tau_bar to_power (2 * n)) / (sqrt 5)) is V11() real ext-real Element of COMPLEX
(tau to_power (2 * n)) - (tau_bar to_power (2 * n)) is V11() real ext-real set
((tau to_power (2 * n)) - (tau_bar to_power (2 * n))) / (sqrt 5) is V11() real ext-real Element of COMPLEX
tau_bar to_power (2 * n) is V11() real ext-real set
tau_bar |^ (2 * n) is V11() real ext-real set
(tau_bar to_power 2) |^ n is V11() real ext-real set
(tau_bar ^2) to_power n is V11() real ext-real set
(tau_bar ^2) |^ n is V11() real ext-real set
0 + ((tau to_power (2 * n)) / (sqrt 5)) is V11() real ext-real set
(