REAL is V57() V58() V59() V63() set
NAT is V57() V58() V59() V60() V61() V62() V63() Element of bool REAL
bool REAL is set
COMPLEX is V57() V63() set
omega is V57() V58() V59() V60() V61() V62() V63() set
bool omega is set
bool NAT is set
RAT is V57() V58() V59() V60() V63() set
INT is V57() V58() V59() V60() V61() V63() set
1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
0 is ext-real non positive non negative empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() V63() Element of NAT
2 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
3 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
n is ext-real non negative ordinal natural V14() V15() integer set
n -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 3 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
1 -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n -' 1) + n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
0 + n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) - 3 is ext-real V14() V15() integer Element of REAL
n - 1 is ext-real V14() V15() integer Element of REAL
(2 * n) - 1 is ext-real V14() V15() integer Element of REAL
((2 * n) - 1) - 1 is ext-real V14() V15() integer Element of REAL
(2 * n) - 2 is ext-real V14() V15() integer Element of REAL
((2 * n) - 2) - 1 is ext-real V14() V15() integer Element of REAL
n is ext-real non negative ordinal natural V14() V15() integer set
n -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
1 * (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) - 2 is ext-real V14() V15() integer Element of REAL
n - 1 is ext-real V14() V15() integer Element of REAL
n is ext-real non negative ordinal natural V14() V15() integer set
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
n + n is ext-real non negative ordinal natural V14() V15() integer set
n + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n + n) - 1 is ext-real V14() V15() integer Element of REAL
(n + 1) - 1 is ext-real V14() V15() integer Element of REAL
1 * 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
n is ext-real non negative ordinal natural V14() V15() integer set
n -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n -' 2) + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
n -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n -' 1) -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((n -' 1) -' 1) + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
4 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
n is ext-real non negative ordinal natural V14() V15() integer set
4 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(4 * n) * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((4 * n) * n) - (2 * n) is ext-real V14() V15() integer Element of REAL
n + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((4 * n) * n) - (2 * n)) / (n + 1) is ext-real V14() V15() Element of REAL
a is ext-real non negative non trivial ordinal natural V14() V15() integer set
4 * a is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(4 * a) * a is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * a is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((4 * a) * a) - (2 * a) is ext-real V14() V15() integer Element of REAL
a + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((4 * a) * a) - (2 * a)) / (a + 1) is ext-real V14() V15() Element of REAL
4 * (a + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(4 * (a + 1)) * (a + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * (a + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((4 * (a + 1)) * (a + 1)) - (2 * (a + 1)) is ext-real V14() V15() integer Element of REAL
(a + 1) + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((4 * (a + 1)) * (a + 1)) - (2 * (a + 1))) / ((a + 1) + 1) is ext-real V14() V15() Element of REAL
1 / (a + 1) is ext-real non negative V14() V15() Element of REAL
(((4 * a) * a) - (2 * a)) * (1 / (a + 1)) is ext-real V14() V15() Element of REAL
((((4 * a) * a) - (2 * a)) * (1 / (a + 1))) * (a + 1) is ext-real V14() V15() Element of REAL
1 * (a + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((4 * a) * a) - (2 * a)) - (a + 1) is ext-real V14() V15() integer Element of REAL
3 * a is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((4 * a) * a) - (3 * a) is ext-real V14() V15() integer Element of REAL
(((4 * a) * a) - (3 * a)) - 1 is ext-real V14() V15() integer Element of REAL
8 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
8 * a is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(8 * a) + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((((4 * a) * a) - (3 * a)) - 1) + ((8 * a) + 1) is ext-real V14() V15() integer Element of REAL
0 + 0 is ext-real non positive non negative empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(a + 1) + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((4 * (a + 1)) * (a + 1)) - (2 * (a + 1))) - ((a + 1) + 1) is ext-real V14() V15() integer Element of REAL
((((4 * (a + 1)) * (a + 1)) - (2 * (a + 1))) - ((a + 1) + 1)) + ((a + 1) + 1) is ext-real V14() V15() integer Element of REAL
0 + ((a + 1) + 1) is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((4 * (a + 1)) * (a + 1)) - (2 * (a + 1))) / ((a + 1) + 1) is ext-real V14() V15() Element of REAL
((a + 1) + 1) / ((a + 1) + 1) is ext-real non negative V14() V15() Element of REAL
4 * 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(4 * 2) * 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((4 * 2) * 2) - (2 * 2) is ext-real V14() V15() integer Element of REAL
2 + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((4 * 2) * 2) - (2 * 2)) / (2 + 1) is ext-real V14() V15() Element of REAL
n is ext-real non negative ordinal natural V14() V15() integer set
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 2) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) !) * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
n + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((((2 * n) -' 2) !) * n) * (n + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 1) + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) - 1 is ext-real V14() V15() integer Element of REAL
2 - 1 is ext-real V14() V15() integer Element of REAL
((2 * n) -' 2) + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 1) -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 1) -' 1) + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) !) * ((2 * n) -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((((2 * n) -' 2) !) * ((2 * n) -' 1)) * (2 * n) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 1) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 1) !) * (2 * n) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
0 * n is ext-real non positive non negative empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() V63() Element of NAT
n + n is ext-real non negative ordinal natural V14() V15() integer set
n is ext-real non negative ordinal natural V14() V15() integer set
n + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
3 / (n + 1) is ext-real non negative V14() V15() Element of REAL
2 - (3 / (n + 1)) is ext-real V14() V15() Element of REAL
2 * (2 - (3 / (n + 1))) is ext-real V14() V15() Element of REAL
4 / 2 is ext-real non negative V14() V15() Element of REAL
(2 * (2 - (3 / (n + 1)))) / 2 is ext-real V14() V15() Element of REAL
2 - 2 is ext-real V14() V15() integer Element of REAL
(2 - (3 / (n + 1))) - 2 is ext-real V14() V15() Element of REAL
- (3 / (n + 1)) is ext-real non positive V14() V15() Element of REAL
- (- (3 / (n + 1))) is ext-real non negative V14() V15() Element of REAL
- (- (- (3 / (n + 1)))) is ext-real non positive V14() V15() Element of REAL
n is ext-real non negative ordinal natural V14() V15() integer set
n -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 2) choose (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) choose (n -' 1)) / n is ext-real non negative V14() V15() Element of REAL
n is ext-real non negative ordinal natural V14() V15() integer set
(n) is ext-real V14() V15() Element of REAL
n -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 2) choose (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) choose (n -' 1)) / n is ext-real non negative V14() V15() Element of REAL
((2 * n) -' 2) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n -' 1) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
n ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((n -' 1) !) * (n !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) !) / (((n -' 1) !) * (n !)) is ext-real non negative V14() V15() Element of REAL
2 * 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n -' 1) + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 2) - (n -' 1) is ext-real V14() V15() integer set
n - 1 is ext-real V14() V15() integer Element of REAL
((2 * n) -' 2) - (n - 1) is ext-real V14() V15() integer Element of REAL
(2 * n) - 2 is ext-real V14() V15() integer Element of REAL
((2 * n) - 2) - (n - 1) is ext-real V14() V15() integer Element of REAL
((n -' 1) !) * ((n -' 1) !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) !) / (((n -' 1) !) * ((n -' 1) !)) is ext-real non negative V14() V15() Element of REAL
(((n -' 1) !) * ((n -' 1) !)) * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) !) / ((((n -' 1) !) * ((n -' 1) !)) * n) is ext-real non negative V14() V15() Element of REAL
((n -' 1) !) * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((n -' 1) !) * (((n -' 1) !) * n) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) !) / (((n -' 1) !) * (((n -' 1) !) * n)) is ext-real non negative V14() V15() Element of REAL
n is ext-real non negative ordinal natural V14() V15() integer set
(n) is ext-real V14() V15() Element of REAL
n -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 2) choose (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) choose (n -' 1)) / n is ext-real non negative V14() V15() Element of REAL
(2 * n) -' 3 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 3) choose (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
4 * (((2 * n) -' 3) choose (n -' 1)) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 1) choose (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1)) is ext-real V14() V15() integer Element of REAL
2 * 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) - 2 is ext-real V14() V15() integer Element of REAL
1 + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) - 3 is ext-real V14() V15() integer Element of REAL
((2 * n) -' 3) + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 3) - (n -' 1) is ext-real V14() V15() integer set
n - 1 is ext-real V14() V15() integer Element of REAL
((2 * n) -' 3) - (n - 1) is ext-real V14() V15() integer Element of REAL
((2 * n) - 3) - (n - 1) is ext-real V14() V15() integer Element of REAL
n - 2 is ext-real V14() V15() integer Element of REAL
n -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 3) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n -' 1) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n -' 2) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((n -' 1) !) * ((n -' 2) !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 3) !) / (((n -' 1) !) * ((n -' 2) !)) is ext-real non negative V14() V15() Element of REAL
4 * (((2 * n) -' 3) !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(4 * (((2 * n) -' 3) !)) / (((n -' 1) !) * ((n -' 2) !)) is ext-real non negative V14() V15() Element of REAL
(n -' 2) + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n -' 1) + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
1 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) - 1 is ext-real V14() V15() integer Element of REAL
((2 * n) -' 2) + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 1) - (n -' 1) is ext-real V14() V15() integer set
((2 * n) -' 1) - (n - 1) is ext-real V14() V15() integer Element of REAL
((2 * n) -' 1) - n is ext-real V14() V15() integer set
(((2 * n) -' 1) - n) + 1 is ext-real V14() V15() integer Element of REAL
((2 * n) - 1) - n is ext-real V14() V15() integer Element of REAL
(((2 * n) - 1) - n) + 1 is ext-real V14() V15() integer Element of REAL
((2 * n) -' 1) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
n ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((n -' 1) !) * (n !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 1) !) / (((n -' 1) !) * (n !)) is ext-real non negative V14() V15() Element of REAL
((2 * n) -' 2) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) !) * ((2 * n) -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((((2 * n) -' 2) !) * ((2 * n) -' 1)) / (((n -' 1) !) * (n !)) is ext-real non negative V14() V15() Element of REAL
n * (n - 1) is ext-real V14() V15() integer Element of REAL
(n * (n - 1)) * (4 * (((2 * n) -' 3) !)) is ext-real V14() V15() integer Element of REAL
(n * (n - 1)) * (((n -' 1) !) * ((n -' 2) !)) is ext-real V14() V15() integer Element of REAL
((n * (n - 1)) * (4 * (((2 * n) -' 3) !))) / ((n * (n - 1)) * (((n -' 1) !) * ((n -' 2) !))) is ext-real V14() V15() Element of REAL
(n - 1) * n is ext-real V14() V15() integer Element of REAL
((n - 1) * n) * (4 * (((2 * n) -' 3) !)) is ext-real V14() V15() integer Element of REAL
n * ((n -' 1) !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n - 1) * (n * ((n -' 1) !)) is ext-real V14() V15() integer Element of REAL
((n - 1) * (n * ((n -' 1) !))) * ((n -' 2) !) is ext-real V14() V15() integer Element of REAL
(((n - 1) * n) * (4 * (((2 * n) -' 3) !))) / (((n - 1) * (n * ((n -' 1) !))) * ((n -' 2) !)) is ext-real V14() V15() Element of REAL
(n - 1) * (n !) is ext-real V14() V15() integer Element of REAL
((n - 1) * (n !)) * ((n -' 2) !) is ext-real V14() V15() integer Element of REAL
(((n - 1) * n) * (4 * (((2 * n) -' 3) !))) / (((n - 1) * (n !)) * ((n -' 2) !)) is ext-real V14() V15() Element of REAL
(n -' 1) * ((n -' 2) !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n !) * ((n -' 1) * ((n -' 2) !)) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((n - 1) * n) * (4 * (((2 * n) -' 3) !))) / ((n !) * ((n -' 1) * ((n -' 2) !))) is ext-real V14() V15() Element of REAL
((2 * n) -' 2) * (((2 * n) -' 3) !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) * (((2 * n) -' 2) * (((2 * n) -' 3) !)) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n !) * ((n -' 1) !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) * (((2 * n) -' 2) * (((2 * n) -' 3) !))) / ((n !) * ((n -' 1) !)) is ext-real non negative V14() V15() Element of REAL
(2 * n) * (((2 * n) -' 2) !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) * (((2 * n) -' 2) !)) / ((n !) * ((n -' 1) !)) is ext-real non negative V14() V15() Element of REAL
((2 * n) * (((2 * n) -' 2) !)) - ((((2 * n) -' 2) !) * ((2 * n) -' 1)) is ext-real V14() V15() integer Element of REAL
(((2 * n) * (((2 * n) -' 2) !)) - ((((2 * n) -' 2) !) * ((2 * n) -' 1))) / ((n !) * ((n -' 1) !)) is ext-real V14() V15() Element of REAL
(0) is ext-real V14() V15() Element of REAL
0 -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * 0 is ext-real non positive non negative empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() V63() Element of NAT
(2 * 0) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * 0) -' 2) choose (0 -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * 0) -' 2) choose (0 -' 1)) / 0 is ext-real non positive non negative empty V14() V15() V57() V58() V59() V60() V61() V62() V63() Element of REAL
(1) is ext-real V14() V15() Element of REAL
1 -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * 1) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * 1) -' 2) choose (1 -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * 1) -' 2) choose (1 -' 1)) / 1 is ext-real non negative V14() V15() Element of REAL
((2 * 1) -' 2) choose 0 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2) is ext-real V14() V15() Element of REAL
2 -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * 2) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * 2) -' 2) choose (2 -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * 2) -' 2) choose (2 -' 1)) / 2 is ext-real non negative V14() V15() Element of REAL
4 -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
4 - 2 is ext-real V14() V15() integer Element of REAL
2 - 1 is ext-real V14() V15() integer Element of REAL
2 / 2 is ext-real non negative V14() V15() Element of REAL
n is ext-real non negative ordinal natural V14() V15() integer set
(n) is ext-real V14() V15() Element of REAL
n -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 2) choose (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) choose (n -' 1)) / n is ext-real non negative V14() V15() Element of REAL
(2 * n) -' 3 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 3) choose (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
4 * (((2 * n) -' 3) choose (n -' 1)) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 1) choose (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1)) is ext-real V14() V15() integer Element of REAL
n is ext-real non negative ordinal natural V14() V15() integer set
n + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((n + 1)) is ext-real V14() V15() Element of REAL
(n + 1) -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * (n + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * (n + 1)) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * (n + 1)) -' 2) choose ((n + 1) -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * (n + 1)) -' 2) choose ((n + 1) -' 1)) / (n + 1) is ext-real non negative V14() V15() Element of REAL
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
n ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n + 1) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n !) * ((n + 1) !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) !) / ((n !) * ((n + 1) !)) is ext-real non negative V14() V15() Element of REAL
(2 * n) - n is ext-real V14() V15() integer Element of REAL
a is ext-real non negative ordinal natural V14() V15() integer set
1 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) choose n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n !) * (n !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) !) / ((n !) * (n !)) is ext-real non negative V14() V15() Element of REAL
(2 * n) + 2 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) + 2) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((n !) * (n !)) * (n + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) !) / (((n !) * (n !)) * (n + 1)) is ext-real non negative V14() V15() Element of REAL
(n !) * (n + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n !) * ((n !) * (n + 1)) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) !) / ((n !) * ((n !) * (n + 1))) is ext-real non negative V14() V15() Element of REAL
n is ext-real non negative ordinal natural V14() V15() integer set
n + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((n + 1)) is ext-real V14() V15() Element of REAL
(n + 1) -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * (n + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * (n + 1)) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * (n + 1)) -' 2) choose ((n + 1) -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * (n + 1)) -' 2) choose ((n + 1) -' 1)) / (n + 1) is ext-real non negative V14() V15() Element of REAL
(n) is ext-real V14() V15() Element of REAL
n -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 2) choose (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) choose (n -' 1)) / n is ext-real non negative V14() V15() Element of REAL
((2 * n) -' 2) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
n ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n + 1) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n !) * ((n + 1) !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) !) / ((n !) * ((n + 1) !)) is ext-real non negative V14() V15() Element of REAL
(n -' 1) + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) !) * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((((2 * n) -' 2) !) * n) * (n + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((((2 * n) -' 2) !) * n) * (n + 1)) / ((n !) * ((n + 1) !)) is ext-real non negative V14() V15() Element of REAL
(n -' 1) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
n * ((n -' 1) !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n * ((n -' 1) !)) * ((n + 1) !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((((2 * n) -' 2) !) * n) * (n + 1)) / ((n * ((n -' 1) !)) * ((n + 1) !)) is ext-real non negative V14() V15() Element of REAL
(((2 * n) -' 2) !) * (n + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
n * ((((2 * n) -' 2) !) * (n + 1)) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((n -' 1) !) * ((n + 1) !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
n * (((n -' 1) !) * ((n + 1) !)) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n * ((((2 * n) -' 2) !) * (n + 1))) / (n * (((n -' 1) !) * ((n + 1) !))) is ext-real non negative V14() V15() Element of REAL
((((2 * n) -' 2) !) * (n + 1)) / (((n -' 1) !) * ((n + 1) !)) is ext-real non negative V14() V15() Element of REAL
(n + 1) * (n !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((n -' 1) !) * ((n + 1) * (n !)) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((((2 * n) -' 2) !) * (n + 1)) / (((n -' 1) !) * ((n + 1) * (n !))) is ext-real non negative V14() V15() Element of REAL
((n -' 1) !) * (n !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((n -' 1) !) * (n !)) * (n + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((((2 * n) -' 2) !) * (n + 1)) / ((((n -' 1) !) * (n !)) * (n + 1)) is ext-real non negative V14() V15() Element of REAL
(((2 * n) -' 2) !) / (((n -' 1) !) * (n !)) is ext-real non negative V14() V15() Element of REAL
0 * (n !) is ext-real non positive non negative empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() V63() Element of NAT
n is ext-real non negative ordinal natural V14() V15() integer set
(n) is ext-real V14() V15() Element of REAL
n -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 2) choose (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) choose (n -' 1)) / n is ext-real non negative V14() V15() Element of REAL
n + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((n + 1)) is ext-real V14() V15() Element of REAL
(n + 1) -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * (n + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * (n + 1)) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * (n + 1)) -' 2) choose ((n + 1) -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * (n + 1)) -' 2) choose ((n + 1) -' 1)) / (n + 1) is ext-real non negative V14() V15() Element of REAL
n is ext-real non negative ordinal natural V14() V15() integer set
(n) is ext-real V14() V15() Element of REAL
n -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 2) choose (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) choose (n -' 1)) / n is ext-real non negative V14() V15() Element of REAL
n is ext-real non negative ordinal natural V14() V15() integer set
(n) is ext-real V14() V15() Element of REAL
n -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 2) choose (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) choose (n -' 1)) / n is ext-real non negative V14() V15() Element of REAL
n is ext-real non negative ordinal natural V14() V15() integer set
n + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((n + 1)) is ext-real V14() V15() Element of REAL
(n + 1) -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * (n + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * (n + 1)) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * (n + 1)) -' 2) choose ((n + 1) -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * (n + 1)) -' 2) choose ((n + 1) -' 1)) / (n + 1) is ext-real non negative V14() V15() Element of REAL
3 / (n + 1) is ext-real non negative V14() V15() Element of REAL
2 - (3 / (n + 1)) is ext-real V14() V15() Element of REAL
2 * (2 - (3 / (n + 1))) is ext-real V14() V15() Element of REAL
(n) is ext-real V14() V15() Element of REAL
n -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 2) choose (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) choose (n -' 1)) / n is ext-real non negative V14() V15() Element of REAL
(2 * (2 - (3 / (n + 1)))) * (n) is ext-real V14() V15() Element of REAL
1 + 0 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
n - 1 is ext-real V14() V15() integer Element of REAL
2 * (n - 1) is ext-real V14() V15() integer Element of REAL
(2 * n) - (2 * 1) is ext-real V14() V15() integer Element of REAL
(n -' 1) + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((n -' 1) + 1)) is ext-real V14() V15() Element of REAL
((n -' 1) + 1) -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * ((n -' 1) + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * ((n -' 1) + 1)) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * ((n -' 1) + 1)) -' 2) choose (((n -' 1) + 1) -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * ((n -' 1) + 1)) -' 2) choose (((n -' 1) + 1) -' 1)) / ((n -' 1) + 1) is ext-real non negative V14() V15() Element of REAL
(2 * (n -' 1)) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n -' 1) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((n -' 1) + 1) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((n -' 1) !) * (((n -' 1) + 1) !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * (n -' 1)) !) / (((n -' 1) !) * (((n -' 1) + 1) !)) is ext-real non negative V14() V15() Element of REAL
((2 * n) -' 2) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
n ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((n -' 1) !) * (n !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) !) / (((n -' 1) !) * (n !)) is ext-real non negative V14() V15() Element of REAL
1 * 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) - 1 is ext-real V14() V15() integer Element of REAL
(2 * (n + 1)) / (n + 1) is ext-real non negative V14() V15() Element of REAL
((2 * (n + 1)) / (n + 1)) - (3 / (n + 1)) is ext-real V14() V15() Element of REAL
2 * (((2 * (n + 1)) / (n + 1)) - (3 / (n + 1))) is ext-real V14() V15() Element of REAL
(2 * (n + 1)) - 3 is ext-real V14() V15() integer Element of REAL
((2 * (n + 1)) - 3) / (n + 1) is ext-real V14() V15() Element of REAL
2 * (((2 * (n + 1)) - 3) / (n + 1)) is ext-real V14() V15() Element of REAL
2 * ((2 * n) - 1) is ext-real V14() V15() integer Element of REAL
(2 * ((2 * n) - 1)) / (n + 1) is ext-real V14() V15() Element of REAL
((2 * n) -' 1) * 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 1) * 2) * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
n * (n + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((((2 * n) -' 1) * 2) * n) / (n * (n + 1)) is ext-real non negative V14() V15() Element of REAL
((2 * n) -' 1) * (2 * n) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 1) * (2 * n)) / (n * (n + 1)) is ext-real non negative V14() V15() Element of REAL
((2 * n) -' 1) + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 2) + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n + 1) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n !) * ((n + 1) !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) !) / ((n !) * ((n + 1) !)) is ext-real non negative V14() V15() Element of REAL
((2 * n) -' 1) ! is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 1) !) * (2 * n) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((((2 * n) -' 1) !) * (2 * n)) / ((n !) * ((n + 1) !)) is ext-real non negative V14() V15() Element of REAL
(((2 * n) -' 2) !) * ((2 * n) -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((((2 * n) -' 2) !) * ((2 * n) -' 1)) * (2 * n) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((((2 * n) -' 2) !) * ((2 * n) -' 1)) * (2 * n)) / ((n !) * ((n + 1) !)) is ext-real non negative V14() V15() Element of REAL
(n !) * (n + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n !) * ((n !) * (n + 1)) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((((2 * n) -' 2) !) * ((2 * n) -' 1)) * (2 * n)) / ((n !) * ((n !) * (n + 1))) is ext-real non negative V14() V15() Element of REAL
((n -' 1) !) * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((n -' 1) !) * n) * (n + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n !) * ((((n -' 1) !) * n) * (n + 1)) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((((2 * n) -' 2) !) * ((2 * n) -' 1)) * (2 * n)) / ((n !) * ((((n -' 1) !) * n) * (n + 1))) is ext-real non negative V14() V15() Element of REAL
(((2 * n) -' 2) !) * (((2 * n) -' 1) * (2 * n)) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(n !) * ((n -' 1) !) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((n !) * ((n -' 1) !)) * (n * (n + 1)) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((((2 * n) -' 2) !) * (((2 * n) -' 1) * (2 * n))) / (((n !) * ((n -' 1) !)) * (n * (n + 1))) is ext-real non negative V14() V15() Element of REAL
(n) * ((((2 * n) -' 1) * (2 * n)) / (n * (n + 1))) is ext-real V14() V15() Element of REAL
n is ext-real non negative ordinal natural V14() V15() integer set
(n) is ext-real V14() V15() Element of REAL
n -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 2) choose (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) choose (n -' 1)) / n is ext-real non negative V14() V15() Element of REAL
n is ext-real non negative ordinal natural V14() V15() integer set
(n) is ext-real non negative ordinal natural V14() V15() integer Element of REAL
n -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 2) choose (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) choose (n -' 1)) / n is ext-real non negative V14() V15() Element of REAL
a is ext-real positive non negative non empty ordinal natural V14() V15() integer set
(a) is ext-real non negative ordinal natural V14() V15() integer Element of REAL
a -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * a is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * a) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * a) -' 2) choose (a -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * a) -' 2) choose (a -' 1)) / a is ext-real non negative V14() V15() Element of REAL
a + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((a + 1)) is ext-real non negative ordinal natural V14() V15() integer Element of REAL
(a + 1) -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * (a + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * (a + 1)) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * (a + 1)) -' 2) choose ((a + 1) -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * (a + 1)) -' 2) choose ((a + 1) -' 1)) / (a + 1) is ext-real non negative V14() V15() Element of REAL
n is ext-real positive non negative non empty ordinal natural V14() V15() integer set
(n) is ext-real non negative ordinal natural V14() V15() integer Element of REAL
n -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 2) choose (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) choose (n -' 1)) / n is ext-real non negative V14() V15() Element of REAL
n is ext-real non negative ordinal natural V14() V15() integer set
(n) is ext-real non negative ordinal natural V14() V15() integer Element of REAL
n -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * n is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * n) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * n) -' 2) choose (n -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * n) -' 2) choose (n -' 1)) / n is ext-real non negative V14() V15() Element of REAL
4 * (n) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
n + 1 is ext-real positive non negative non empty ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((n + 1)) is ext-real positive non negative non empty ordinal natural V14() V15() integer Element of REAL
(n + 1) -' 1 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
2 * (n + 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * (n + 1)) -' 2 is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * (n + 1)) -' 2) choose ((n + 1) -' 1) is ext-real non negative ordinal natural V14() V15() integer V46() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * (n + 1)) -' 2) choose ((n + 1) -' 1)) / (n + 1) is ext-real non negative V14() V15() Element of REAL
3 / (n + 1) is ext-real non negative V14() V15() Element of REAL
2 - (3 / (n + 1)) is ext-real V14() V15() Element of REAL
2 * (2 - (3 / (n + 1))) is ext-real V14() V15() Element of REAL
(2 * (2 - (3 / (n + 1)))) * (n) is ext-real V14() V15() Element of REAL