:: SERIES_2 semantic presentation

REAL is V4() V45() V57() V58() V59() V63() set
NAT is V57() V58() V59() V60() V61() V62() V63() Element of K11(REAL)
K11(REAL) is set
COMPLEX is V4() V45() V57() V63() set
NAT is V57() V58() V59() V60() V61() V62() V63() set
K11(NAT) is set
K11(NAT) is set
RAT is V4() V45() V57() V58() V59() V60() V63() set
INT is V4() V45() V57() V58() V59() V60() V61() V63() set
K12(NAT,REAL) is V35() V36() V37() set
K11(K12(NAT,REAL)) is set
0 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
1 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
1 ! is ext-real positive natural V14() real Element of REAL
2 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 ! is ext-real positive natural V14() real Element of REAL
- 1 is ext-real V14() real set
a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(- 1) |^ a is ext-real V14() real set
abs ((- 1) |^ a) is ext-real V14() real Element of REAL
(- 1) to_power a is ext-real V14() real set
1 to_power a is ext-real V14() real set
(- 1) to_power a is ext-real V14() real set
1 to_power a is ext-real V14() real set
- (1 to_power a) is ext-real V14() real set
- (- 1) is ext-real V14() real set
3 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a is ext-real V14() real set
a |^ 3 is ext-real V14() real set
a * a is ext-real V14() real set
(a * a) * a is ext-real V14() real set
2 + 1 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a |^ (2 + 1) is ext-real V14() real set
a |^ 2 is ext-real V14() real set
(a |^ 2) * a is ext-real V14() real set
a is ext-real V14() real set
a |^ 3 is ext-real V14() real set
a |^ 2 is ext-real V14() real set
(a |^ 2) * a is ext-real V14() real set
2 + 1 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a |^ (2 + 1) is ext-real V14() real set
4 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 |^ 2 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a is ext-real V14() real set
a |^ 2 is ext-real V14() real set
2 * a is ext-real V14() real set
b is ext-real V14() real set
a + b is ext-real V14() real set
(a + b) |^ 2 is ext-real V14() real set
(2 * a) * b is ext-real V14() real set
(a |^ 2) + ((2 * a) * b) is ext-real V14() real set
b |^ 2 is ext-real V14() real set
((a |^ 2) + ((2 * a) * b)) + (b |^ 2) is ext-real V14() real set
1 + 1 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(a + b) |^ (1 + 1) is ext-real V14() real set
(a + b) |^ 1 is ext-real V14() real set
((a + b) |^ 1) * (a + b) is ext-real V14() real set
(a + b) * (a + b) is ext-real V14() real set
a * a is ext-real V14() real set
a * b is ext-real V14() real set
(a * a) + (a * b) is ext-real V14() real set
b * b is ext-real V14() real set
(a * b) + (b * b) is ext-real V14() real set
((a * a) + (a * b)) + ((a * b) + (b * b)) is ext-real V14() real set
(a * b) + (b |^ 2) is ext-real V14() real set
((a * a) + (a * b)) + ((a * b) + (b |^ 2)) is ext-real V14() real set
(a |^ 2) + (a * b) is ext-real V14() real set
((a |^ 2) + (a * b)) + ((a * b) + (b |^ 2)) is ext-real V14() real set
2 * (a * b) is ext-real V14() real set
(a |^ 2) + (2 * (a * b)) is ext-real V14() real set
((a |^ 2) + (2 * (a * b))) + (b |^ 2) is ext-real V14() real set
2 * 2 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a is ext-real V14() real set
a + 1 is ext-real V14() real set
(a + 1) |^ 3 is ext-real V14() real set
a |^ 3 is ext-real V14() real set
a |^ 2 is ext-real V14() real set
3 * (a |^ 2) is ext-real V14() real set
(a |^ 3) + (3 * (a |^ 2)) is ext-real V14() real set
3 * a is ext-real V14() real set
((a |^ 3) + (3 * (a |^ 2))) + (3 * a) is ext-real V14() real set
(((a |^ 3) + (3 * (a |^ 2))) + (3 * a)) + 1 is ext-real V14() real set
(a + 1) |^ 2 is ext-real V14() real set
((a + 1) |^ 2) * (a + 1) is ext-real V14() real set
2 * a is ext-real V14() real set
(2 * a) * 1 is ext-real V14() real set
(a |^ 2) + ((2 * a) * 1) is ext-real V14() real set
1 |^ 2 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((a |^ 2) + ((2 * a) * 1)) + (1 |^ 2) is ext-real V14() real set
(((a |^ 2) + ((2 * a) * 1)) + (1 |^ 2)) * (a + 1) is ext-real V14() real set
(a |^ 2) + (2 * a) is ext-real V14() real set
((a |^ 2) + (2 * a)) + 1 is ext-real V14() real set
(((a |^ 2) + (2 * a)) + 1) * (a + 1) is ext-real V14() real set
(a |^ 2) * a is ext-real V14() real set
(a |^ 2) * 1 is ext-real V14() real set
((a |^ 2) * a) + ((a |^ 2) * 1) is ext-real V14() real set
(2 * a) * a is ext-real V14() real set
((2 * a) * a) + (2 * a) is ext-real V14() real set
(((a |^ 2) * a) + ((a |^ 2) * 1)) + (((2 * a) * a) + (2 * a)) is ext-real V14() real set
1 * a is ext-real V14() real set
1 * 1 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(1 * a) + (1 * 1) is ext-real V14() real set
((((a |^ 2) * a) + ((a |^ 2) * 1)) + (((2 * a) * a) + (2 * a))) + ((1 * a) + (1 * 1)) is ext-real V14() real set
((2 * a) * a) + ((2 * a) * 1) is ext-real V14() real set
(((a |^ 2) * a) + ((a |^ 2) * 1)) + (((2 * a) * a) + ((2 * a) * 1)) is ext-real V14() real set
(1 |^ 2) * a is ext-real V14() real set
((1 |^ 2) * a) + 1 is ext-real V14() real set
((((a |^ 2) * a) + ((a |^ 2) * 1)) + (((2 * a) * a) + ((2 * a) * 1))) + (((1 |^ 2) * a) + 1) is ext-real V14() real set
2 + 1 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a |^ (2 + 1) is ext-real V14() real set
(a |^ (2 + 1)) + (a |^ 2) is ext-real V14() real set
((a |^ (2 + 1)) + (a |^ 2)) + (((2 * a) * a) + (2 * a)) is ext-real V14() real set
(((a |^ (2 + 1)) + (a |^ 2)) + (((2 * a) * a) + (2 * a))) + (((1 |^ 2) * a) + 1) is ext-real V14() real set
(a |^ 3) + (a |^ 2) is ext-real V14() real set
a * a is ext-real V14() real set
2 * (a * a) is ext-real V14() real set
(2 * (a * a)) + (2 * a) is ext-real V14() real set
((a |^ 3) + (a |^ 2)) + ((2 * (a * a)) + (2 * a)) is ext-real V14() real set
(1 * a) + 1 is ext-real V14() real set
(((a |^ 3) + (a |^ 2)) + ((2 * (a * a)) + (2 * a))) + ((1 * a) + 1) is ext-real V14() real set
a |^ 1 is ext-real V14() real set
(a |^ 1) * a is ext-real V14() real set
2 * ((a |^ 1) * a) is ext-real V14() real set
(2 * ((a |^ 1) * a)) + (2 * a) is ext-real V14() real set
((a |^ 3) + (a |^ 2)) + ((2 * ((a |^ 1) * a)) + (2 * a)) is ext-real V14() real set
(((a |^ 3) + (a |^ 2)) + ((2 * ((a |^ 1) * a)) + (2 * a))) + (a + 1) is ext-real V14() real set
1 + 1 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a |^ (1 + 1) is ext-real V14() real set
2 * (a |^ (1 + 1)) is ext-real V14() real set
(2 * (a |^ (1 + 1))) + (2 * a) is ext-real V14() real set
((a |^ 3) + (a |^ 2)) + ((2 * (a |^ (1 + 1))) + (2 * a)) is ext-real V14() real set
(((a |^ 3) + (a |^ 2)) + ((2 * (a |^ (1 + 1))) + (2 * a))) + (a + 1) is ext-real V14() real set
2 * (a |^ 2) is ext-real V14() real set
((a |^ 3) + (a |^ 2)) + (2 * (a |^ 2)) is ext-real V14() real set
(((a |^ 3) + (a |^ 2)) + (2 * (a |^ 2))) + (2 * a) is ext-real V14() real set
((((a |^ 3) + (a |^ 2)) + (2 * (a |^ 2))) + (2 * a)) + (a + 1) is ext-real V14() real set
30 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 * a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * a) + 1 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a * ((2 * a) + 1) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a |^ 2 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
3 * (a |^ 2) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
3 * a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(3 * (a |^ 2)) + (3 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((3 * (a |^ 2)) + (3 * a)) - 1 is ext-real V14() real set
(a * ((2 * a) + 1)) * (((3 * (a |^ 2)) + (3 * a)) - 1) is ext-real V14() real set
a + 1 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(a + 1) |^ 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((a + 1) |^ 3) * 30 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((a * ((2 * a) + 1)) * (((3 * (a |^ 2)) + (3 * a)) - 1)) + (((a + 1) |^ 3) * 30) is ext-real V14() real set
a + 2 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 * (a + 1) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * (a + 1)) + 1 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(a + 2) * ((2 * (a + 1)) + 1) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(a + 1) |^ 2 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
3 * ((a + 1) |^ 2) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
3 * (a + 1) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(3 * ((a + 1) |^ 2)) + (3 * (a + 1)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((3 * ((a + 1) |^ 2)) + (3 * (a + 1))) - 1 is ext-real V14() real set
((a + 2) * ((2 * (a + 1)) + 1)) * (((3 * ((a + 1) |^ 2)) + (3 * (a + 1))) - 1) is ext-real V14() real set
(2 * a) + 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(a + 2) * ((2 * a) + 3) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * a) * 1 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(a |^ 2) + ((2 * a) * 1) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
1 |^ 2 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((a |^ 2) + ((2 * a) * 1)) + (1 |^ 2) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
3 * (((a |^ 2) + ((2 * a) * 1)) + (1 |^ 2)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(3 * a) + 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(3 * (((a |^ 2) + ((2 * a) * 1)) + (1 |^ 2))) + ((3 * a) + 3) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((3 * (((a |^ 2) + ((2 * a) * 1)) + (1 |^ 2))) + ((3 * a) + 3)) - 1 is ext-real V14() real set
((a + 2) * ((2 * a) + 3)) * (((3 * (((a |^ 2) + ((2 * a) * 1)) + (1 |^ 2))) + ((3 * a) + 3)) - 1) is ext-real V14() real set
a * (2 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 * (2 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(a * (2 * a)) + (2 * (2 * a)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a * 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 * 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(a * 3) + (2 * 3) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((a * (2 * a)) + (2 * (2 * a))) + ((a * 3) + (2 * 3)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(a |^ 2) + (2 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((a |^ 2) + (2 * a)) + (1 |^ 2) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
3 * (((a |^ 2) + (2 * a)) + (1 |^ 2)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(3 * (((a |^ 2) + (2 * a)) + (1 |^ 2))) + (3 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((3 * (((a |^ 2) + (2 * a)) + (1 |^ 2))) + (3 * a)) + 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((3 * (((a |^ 2) + (2 * a)) + (1 |^ 2))) + (3 * a)) + 3) - 1 is ext-real V14() real set
(((a * (2 * a)) + (2 * (2 * a))) + ((a * 3) + (2 * 3))) * ((((3 * (((a |^ 2) + (2 * a)) + (1 |^ 2))) + (3 * a)) + 3) - 1) is ext-real V14() real set
((a |^ 2) + (2 * a)) + 1 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
3 * (((a |^ 2) + (2 * a)) + 1) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(3 * (((a |^ 2) + (2 * a)) + 1)) + (3 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((3 * (((a |^ 2) + (2 * a)) + 1)) + (3 * a)) + 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((3 * (((a |^ 2) + (2 * a)) + 1)) + (3 * a)) + 3) - 1 is ext-real V14() real set
(((a * (2 * a)) + (2 * (2 * a))) + ((a * 3) + (2 * 3))) * ((((3 * (((a |^ 2) + (2 * a)) + 1)) + (3 * a)) + 3) - 1) is ext-real V14() real set
a * a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(a * a) * 2 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 * 2 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * 2) * a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((a * a) * 2) + ((2 * 2) * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
6 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(a * 3) + 6 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((a * a) * 2) + ((2 * 2) * a)) + ((a * 3) + 6) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(a |^ 2) * 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
6 * a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((a |^ 2) * 3) + (6 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((a |^ 2) * 3) + (6 * a)) + 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((((a |^ 2) * 3) + (6 * a)) + 3) + (3 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((((a |^ 2) * 3) + (6 * a)) + 3) + (3 * a)) + 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((((((a |^ 2) * 3) + (6 * a)) + 3) + (3 * a)) + 3) - 1 is ext-real V14() real set
((((a * a) * 2) + ((2 * 2) * a)) + ((a * 3) + 6)) * (((((((a |^ 2) * 3) + (6 * a)) + 3) + (3 * a)) + 3) - 1) is ext-real V14() real set
2 * (a |^ 2) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
4 * a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * (a |^ 2)) + (4 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * (a |^ 2)) + (4 * a)) + ((a * 3) + 6) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(3 * (a |^ 2)) + (6 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((3 * (a |^ 2)) + (6 * a)) + 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((3 * (a |^ 2)) + (6 * a)) + 3) + (3 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((((3 * (a |^ 2)) + (6 * a)) + 3) + (3 * a)) + 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((((3 * (a |^ 2)) + (6 * a)) + 3) + (3 * a)) + 3) - 1 is ext-real V14() real set
(((2 * (a |^ 2)) + (4 * a)) + ((a * 3) + 6)) * ((((((3 * (a |^ 2)) + (6 * a)) + 3) + (3 * a)) + 3) - 1) is ext-real V14() real set
(a |^ 2) * (a |^ 2) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 * ((a |^ 2) * (a |^ 2)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * ((a |^ 2) * (a |^ 2))) * 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * (a |^ 2)) * a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
9 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * (a |^ 2)) * a) * 9 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * ((a |^ 2) * (a |^ 2))) * 3) + (((2 * (a |^ 2)) * a) * 9) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
10 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
10 * (a |^ 2) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * ((a |^ 2) * (a |^ 2))) * 3) + (((2 * (a |^ 2)) * a) * 9)) + (10 * (a |^ 2)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
7 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
7 * a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(7 * a) * (a |^ 2) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((7 * a) * (a |^ 2)) * 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(7 * a) * a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((7 * a) * a) * 9 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((7 * a) * (a |^ 2)) * 3) + (((7 * a) * a) * 9) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
35 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
35 * a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((((7 * a) * (a |^ 2)) * 3) + (((7 * a) * a) * 9)) + (35 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((((2 * ((a |^ 2) * (a |^ 2))) * 3) + (((2 * (a |^ 2)) * a) * 9)) + (10 * (a |^ 2))) + (((((7 * a) * (a |^ 2)) * 3) + (((7 * a) * a) * 9)) + (35 * a)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
6 * 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(6 * 3) * (a |^ 2) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
6 * 9 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(6 * 9) * a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((6 * 3) * (a |^ 2)) + ((6 * 9) * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((6 * 3) * (a |^ 2)) + ((6 * 9) * a)) + 30 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((((2 * ((a |^ 2) * (a |^ 2))) * 3) + (((2 * (a |^ 2)) * a) * 9)) + (10 * (a |^ 2))) + (((((7 * a) * (a |^ 2)) * 3) + (((7 * a) * a) * 9)) + (35 * a))) + ((((6 * 3) * (a |^ 2)) + ((6 * 9) * a)) + 30) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 + 2 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a |^ (2 + 2) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 * (a |^ (2 + 2)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * (a |^ (2 + 2))) * 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(a |^ 2) * a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 * ((a |^ 2) * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * ((a |^ 2) * a)) * 9 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * (a |^ (2 + 2))) * 3) + ((2 * ((a |^ 2) * a)) * 9) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * (a |^ (2 + 2))) * 3) + ((2 * ((a |^ 2) * a)) * 9)) + (10 * (a |^ 2)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a * (a |^ 2) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
7 * (a * (a |^ 2)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(7 * (a * (a |^ 2))) * 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
7 * (a * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(7 * (a * a)) * 9 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((7 * (a * (a |^ 2))) * 3) + ((7 * (a * a)) * 9) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((7 * (a * (a |^ 2))) * 3) + ((7 * (a * a)) * 9)) + (35 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((((2 * (a |^ (2 + 2))) * 3) + ((2 * ((a |^ 2) * a)) * 9)) + (10 * (a |^ 2))) + ((((7 * (a * (a |^ 2))) * 3) + ((7 * (a * a)) * 9)) + (35 * a)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
18 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
18 * (a |^ 2) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
54 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
54 * a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(18 * (a |^ 2)) + (54 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((18 * (a |^ 2)) + (54 * a)) + 30 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((((2 * (a |^ (2 + 2))) * 3) + ((2 * ((a |^ 2) * a)) * 9)) + (10 * (a |^ 2))) + ((((7 * (a * (a |^ 2))) * 3) + ((7 * (a * a)) * 9)) + (35 * a))) + (((18 * (a |^ 2)) + (54 * a)) + 30) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a |^ 4 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 * (a |^ 4) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * (a |^ 4)) * 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 + 1 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a |^ (2 + 1) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 * (a |^ (2 + 1)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * (a |^ (2 + 1))) * 9 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * (a |^ 4)) * 3) + ((2 * (a |^ (2 + 1))) * 9) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * (a |^ 4)) * 3) + ((2 * (a |^ (2 + 1))) * 9)) + (10 * (a |^ 2)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((((2 * (a |^ 4)) * 3) + ((2 * (a |^ (2 + 1))) * 9)) + (10 * (a |^ 2))) + ((((7 * (a * (a |^ 2))) * 3) + ((7 * (a * a)) * 9)) + (35 * a)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((((2 * (a |^ 4)) * 3) + ((2 * (a |^ (2 + 1))) * 9)) + (10 * (a |^ 2))) + ((((7 * (a * (a |^ 2))) * 3) + ((7 * (a * a)) * 9)) + (35 * a))) + (((18 * (a |^ 2)) + (54 * a)) + 30) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
6 * (a |^ 4) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a |^ 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 * (a |^ 3) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * (a |^ 3)) * 9 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(6 * (a |^ 4)) + ((2 * (a |^ 3)) * 9) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((6 * (a |^ 4)) + ((2 * (a |^ 3)) * 9)) + (10 * (a |^ 2)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
7 * (a |^ (2 + 1)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(7 * (a |^ (2 + 1))) * 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((7 * (a |^ (2 + 1))) * 3) + ((7 * (a * a)) * 9) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((7 * (a |^ (2 + 1))) * 3) + ((7 * (a * a)) * 9)) + (35 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((6 * (a |^ 4)) + ((2 * (a |^ 3)) * 9)) + (10 * (a |^ 2))) + ((((7 * (a |^ (2 + 1))) * 3) + ((7 * (a * a)) * 9)) + (35 * a)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((((6 * (a |^ 4)) + ((2 * (a |^ 3)) * 9)) + (10 * (a |^ 2))) + ((((7 * (a |^ (2 + 1))) * 3) + ((7 * (a * a)) * 9)) + (35 * a))) + (((18 * (a |^ 2)) + (54 * a)) + 30) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
18 * (a |^ 3) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(6 * (a |^ 4)) + (18 * (a |^ 3)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((6 * (a |^ 4)) + (18 * (a |^ 3))) + (10 * (a |^ 2)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
7 * (a |^ 3) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(7 * (a |^ 3)) * 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
7 * (a |^ 2) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(7 * (a |^ 2)) * 9 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((7 * (a |^ 3)) * 3) + ((7 * (a |^ 2)) * 9) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((7 * (a |^ 3)) * 3) + ((7 * (a |^ 2)) * 9)) + (35 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((6 * (a |^ 4)) + (18 * (a |^ 3))) + (10 * (a |^ 2))) + ((((7 * (a |^ 3)) * 3) + ((7 * (a |^ 2)) * 9)) + (35 * a)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((((6 * (a |^ 4)) + (18 * (a |^ 3))) + (10 * (a |^ 2))) + ((((7 * (a |^ 3)) * 3) + ((7 * (a |^ 2)) * 9)) + (35 * a))) + (((18 * (a |^ 2)) + (54 * a)) + 30) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
39 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
39 * (a |^ 3) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(6 * (a |^ 4)) + (39 * (a |^ 3)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
73 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
73 + 18 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(73 + 18) * (a |^ 2) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((6 * (a |^ 4)) + (39 * (a |^ 3))) + ((73 + 18) * (a |^ 2)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
89 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
89 * a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((6 * (a |^ 4)) + (39 * (a |^ 3))) + ((73 + 18) * (a |^ 2))) + (89 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((((6 * (a |^ 4)) + (39 * (a |^ 3))) + ((73 + 18) * (a |^ 2))) + (89 * a)) + 30 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 * (a * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * (a * a)) + a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * (a * a)) + a) * (((3 * (a |^ 2)) + (3 * a)) - 1) is ext-real V14() real set
(((2 * (a * a)) + a) * (((3 * (a |^ 2)) + (3 * a)) - 1)) + (((a + 1) |^ 3) * 30) is ext-real V14() real set
a |^ 1 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(a |^ 1) * a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 * ((a |^ 1) * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * ((a |^ 1) * a)) + a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * ((a |^ 1) * a)) + a) * (((3 * (a |^ 2)) + (3 * a)) - 1) is ext-real V14() real set
(((2 * ((a |^ 1) * a)) + a) * (((3 * (a |^ 2)) + (3 * a)) - 1)) + (((a + 1) |^ 3) * 30) is ext-real V14() real set
1 + 1 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a |^ (1 + 1) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
2 * (a |^ (1 + 1)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * (a |^ (1 + 1))) + a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * (a |^ (1 + 1))) + a) * (((3 * (a |^ 2)) + (3 * a)) - 1) is ext-real V14() real set
(((2 * (a |^ (1 + 1))) + a) * (((3 * (a |^ 2)) + (3 * a)) - 1)) + (((a + 1) |^ 3) * 30) is ext-real V14() real set
(a * (a |^ 2)) * 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * ((a |^ 2) * (a |^ 2))) * 3) + ((a * (a |^ 2)) * 3) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * ((a |^ 2) * a)) * 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(a * a) * 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * ((a |^ 2) * a)) * 3) + ((a * a) * 3) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * ((a |^ 2) * (a |^ 2))) * 3) + ((a * (a |^ 2)) * 3)) + (((2 * ((a |^ 2) * a)) * 3) + ((a * a) * 3)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * (a |^ 2)) + a is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((((2 * ((a |^ 2) * (a |^ 2))) * 3) + ((a * (a |^ 2)) * 3)) + (((2 * ((a |^ 2) * a)) * 3) + ((a * a) * 3))) - ((2 * (a |^ 2)) + a) is ext-real V14() real set
(((((2 * ((a |^ 2) * (a |^ 2))) * 3) + ((a * (a |^ 2)) * 3)) + (((2 * ((a |^ 2) * a)) * 3) + ((a * a) * 3))) - ((2 * (a |^ 2)) + a)) + (((a + 1) |^ 3) * 30) is ext-real V14() real set
((2 * (a |^ (2 + 2))) * 3) + ((a * (a |^ 2)) * 3) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * (a |^ (2 + 2))) * 3) + ((a * (a |^ 2)) * 3)) + (((2 * ((a |^ 2) * a)) * 3) + ((a * a) * 3)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((((2 * (a |^ (2 + 2))) * 3) + ((a * (a |^ 2)) * 3)) + (((2 * ((a |^ 2) * a)) * 3) + ((a * a) * 3))) - ((2 * (a |^ 2)) + a) is ext-real V14() real set
(((((2 * (a |^ (2 + 2))) * 3) + ((a * (a |^ 2)) * 3)) + (((2 * ((a |^ 2) * a)) * 3) + ((a * a) * 3))) - ((2 * (a |^ 2)) + a)) + (((a + 1) |^ 3) * 30) is ext-real V14() real set
((2 * (a |^ 4)) * 3) + ((a * (a |^ 2)) * 3) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(2 * (a |^ (2 + 1))) * 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * (a |^ (2 + 1))) * 3) + ((a * a) * 3) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * (a |^ 4)) * 3) + ((a * (a |^ 2)) * 3)) + (((2 * (a |^ (2 + 1))) * 3) + ((a * a) * 3)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((((2 * (a |^ 4)) * 3) + ((a * (a |^ 2)) * 3)) + (((2 * (a |^ (2 + 1))) * 3) + ((a * a) * 3))) - ((2 * (a |^ 2)) + a) is ext-real V14() real set
(((((2 * (a |^ 4)) * 3) + ((a * (a |^ 2)) * 3)) + (((2 * (a |^ (2 + 1))) * 3) + ((a * a) * 3))) - ((2 * (a |^ 2)) + a)) + (((a + 1) |^ 3) * 30) is ext-real V14() real set
(2 * (a |^ 3)) * 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((2 * (a |^ 3)) * 3) + ((a |^ 2) * 3) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((2 * (a |^ 4)) * 3) + ((a * (a |^ 2)) * 3)) + (((2 * (a |^ 3)) * 3) + ((a |^ 2) * 3)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((((2 * (a |^ 4)) * 3) + ((a * (a |^ 2)) * 3)) + (((2 * (a |^ 3)) * 3) + ((a |^ 2) * 3))) - ((2 * (a |^ 2)) + a) is ext-real V14() real set
(((((2 * (a |^ 4)) * 3) + ((a * (a |^ 2)) * 3)) + (((2 * (a |^ 3)) * 3) + ((a |^ 2) * 3))) - ((2 * (a |^ 2)) + a)) + (((a + 1) |^ 3) * 30) is ext-real V14() real set
(a |^ (2 + 1)) * 3 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(6 * (a |^ 4)) + ((a |^ (2 + 1)) * 3) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
6 * (a |^ 3) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(6 * (a |^ 3)) + ((a |^ 2) * 3) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((6 * (a |^ 4)) + ((a |^ (2 + 1)) * 3)) + ((6 * (a |^ 3)) + ((a |^ 2) * 3)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((6 * (a |^ 4)) + ((a |^ (2 + 1)) * 3)) + ((6 * (a |^ 3)) + ((a |^ 2) * 3))) - ((2 * (a |^ 2)) + a) is ext-real V14() real set
((((6 * (a |^ 4)) + ((a |^ (2 + 1)) * 3)) + ((6 * (a |^ 3)) + ((a |^ 2) * 3))) - ((2 * (a |^ 2)) + a)) + (((a + 1) |^ 3) * 30) is ext-real V14() real set
9 * (a |^ 3) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(6 * (a |^ 4)) + (9 * (a |^ 3)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
1 * (a |^ 2) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((6 * (a |^ 4)) + (9 * (a |^ 3))) + (1 * (a |^ 2)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((6 * (a |^ 4)) + (9 * (a |^ 3))) + (1 * (a |^ 2))) - a is ext-real V14() real set
(a |^ 3) + (3 * (a |^ 2)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((a |^ 3) + (3 * (a |^ 2))) + (3 * a) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(((a |^ 3) + (3 * (a |^ 2))) + (3 * a)) + 1 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((((a |^ 3) + (3 * (a |^ 2))) + (3 * a)) + 1) * 30 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((((6 * (a |^ 4)) + (9 * (a |^ 3))) + (1 * (a |^ 2))) - a) + (((((a |^ 3) + (3 * (a |^ 2))) + (3 * a)) + 1) * 30) is ext-real V14() real set
91 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
91 * (a |^ 2) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((6 * (a |^ 4)) + (39 * (a |^ 3))) + (91 * (a |^ 2)) is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
90 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
90 - 1 is ext-real V14() real set
(90 - 1) * a is ext-real V14() real set
(((6 * (a |^ 4)) + (39 * (a |^ 3))) + (91 * (a |^ 2))) + ((90 - 1) * a) is ext-real V14() real set
((((6 * (a |^ 4)) + (39 * (a |^ 3))) + (91 * (a |^ 2))) + ((90 - 1) * a)) + 30 is ext-real V14() real set
6 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
5 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
10 is ext-real positive V4() natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a is ext-real V14() real set
a + 1 is ext-real V14() real set
(a + 1) |^ 4 is ext-real V14() real set
a |^ 4 is ext-real V14() real set
a |^ 3 is ext-real V14() real set
4 * (a |^ 3) is ext-real V14() real set
(a |^ 4) + (4 * (a |^ 3)) is ext-real V14() real set
a |^ 2 is ext-real V14() real set
6 * (a |^ 2) is ext-real V14() real set
((a |^ 4) + (4 * (a |^ 3))) + (6 * (a |^ 2)) is ext-real V14() real set
4 * a is ext-real V14() real set
(((a |^ 4) + (4 * (a |^ 3))) + (6 * (a |^ 2))) + (4 * a) is ext-real V14() real set
((((a |^ 4) + (4 * (a |^ 3))) + (6 * (a |^ 2))) + (4 * a)) + 1 is ext-real V14() real set
(a + 1) |^ 5 is ext-real V14() real set
a |^ 5 is ext-real V14() real set
5 * (a |^ 4) is ext-real V14() real set
(a |^ 5) + (5 * (a |^ 4)) is ext-real V14() real set
10 * (a |^ 3) is ext-real V14() real set
((a |^ 5) + (5 * (a |^ 4))) + (10 * (a |^ 3)) is ext-real V14() real set
10 * (a |^ 2) is ext-real V14() real set
(((a |^ 5) + (5 * (a |^ 4))) + (10 * (a |^ 3))) + (10 * (a |^ 2)) is ext-real V14() real set
5 * a is ext-real V14() real set
((((a |^ 5) + (5 * (a |^ 4))) + (10 * (a |^ 3))) + (10 * (a |^ 2))) + (5 * a) is ext-real V14() real set
(((((a |^ 5) + (5 * (a |^ 4))) + (10 * (a |^ 3))) + (10 * (a |^ 2))) + (5 * a)) + 1 is ext-real V14() real set
3 + 1 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(a + 1) |^ (3 + 1) is ext-real V14() real set
(a + 1) |^ 3 is ext-real V14() real set
((a + 1) |^ 3) * (a + 1) is ext-real V14() real set
3 * (a |^ 2) is ext-real V14() real set
(a |^ 3) + (3 * (a |^ 2)) is ext-real V14() real set
3 * a is ext-real V14() real set
((a |^ 3) + (3 * (a |^ 2))) + (3 * a) is ext-real V14() real set
(((a |^ 3) + (3 * (a |^ 2))) + (3 * a)) + 1 is ext-real V14() real set
((((a |^ 3) + (3 * (a |^ 2))) + (3 * a)) + 1) * (a + 1) is ext-real V14() real set
(a |^ 3) * a is ext-real V14() real set
((a |^ 3) * a) + (a |^ 3) is ext-real V14() real set
(a |^ 2) * a is ext-real V14() real set
3 * ((a |^ 2) * a) is ext-real V14() real set
(3 * ((a |^ 2) * a)) + (3 * (a |^ 2)) is ext-real V14() real set
(((a |^ 3) * a) + (a |^ 3)) + ((3 * ((a |^ 2) * a)) + (3 * (a |^ 2))) is ext-real V14() real set
a * a is ext-real V14() real set
3 * (a * a) is ext-real V14() real set
(3 * (a * a)) + (3 * a) is ext-real V14() real set
((((a |^ 3) * a) + (a |^ 3)) + ((3 * ((a |^ 2) * a)) + (3 * (a |^ 2)))) + ((3 * (a * a)) + (3 * a)) is ext-real V14() real set
(((((a |^ 3) * a) + (a |^ 3)) + ((3 * ((a |^ 2) * a)) + (3 * (a |^ 2)))) + ((3 * (a * a)) + (3 * a))) + (a + 1) is ext-real V14() real set
a |^ (3 + 1) is ext-real V14() real set
(a |^ (3 + 1)) + (a |^ 3) is ext-real V14() real set
((a |^ (3 + 1)) + (a |^ 3)) + ((3 * ((a |^ 2) * a)) + (3 * (a |^ 2))) is ext-real V14() real set
(((a |^ (3 + 1)) + (a |^ 3)) + ((3 * ((a |^ 2) * a)) + (3 * (a |^ 2)))) + ((3 * (a * a)) + (3 * a)) is ext-real V14() real set
((((a |^ (3 + 1)) + (a |^ 3)) + ((3 * ((a |^ 2) * a)) + (3 * (a |^ 2)))) + ((3 * (a * a)) + (3 * a))) + (a + 1) is ext-real V14() real set
2 + 1 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
a |^ (2 + 1) is ext-real V14() real set
3 * (a |^ (2 + 1)) is ext-real V14() real set
(3 * (a |^ (2 + 1))) + (3 * (a |^ 2)) is ext-real V14() real set
((a |^ (3 + 1)) + (a |^ 3)) + ((3 * (a |^ (2 + 1))) + (3 * (a |^ 2))) is ext-real V14() real set
(((a |^ (3 + 1)) + (a |^ 3)) + ((3 * (a |^ (2 + 1))) + (3 * (a |^ 2)))) + ((3 * (a * a)) + (3 * a)) is ext-real V14() real set
((((a |^ (3 + 1)) + (a |^ 3)) + ((3 * (a |^ (2 + 1))) + (3 * (a |^ 2)))) + ((3 * (a * a)) + (3 * a))) + (a + 1) is ext-real V14() real set
(a |^ 4) + (a |^ 3) is ext-real V14() real set
3 * (a |^ 3) is ext-real V14() real set
(3 * (a |^ 3)) + (3 * (a |^ 2)) is ext-real V14() real set
((a |^ 4) + (a |^ 3)) + ((3 * (a |^ 3)) + (3 * (a |^ 2))) is ext-real V14() real set
(3 * (a |^ 2)) + (3 * a) is ext-real V14() real set
(((a |^ 4) + (a |^ 3)) + ((3 * (a |^ 3)) + (3 * (a |^ 2)))) + ((3 * (a |^ 2)) + (3 * a)) is ext-real V14() real set
((((a |^ 4) + (a |^ 3)) + ((3 * (a |^ 3)) + (3 * (a |^ 2)))) + ((3 * (a |^ 2)) + (3 * a))) + (a + 1) is ext-real V14() real set
3 + 2 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
(a + 1) |^ (3 + 2) is ext-real V14() real set
(a + 1) |^ 2 is ext-real V14() real set
((a + 1) |^ 3) * ((a + 1) |^ 2) is ext-real V14() real set
((((a |^ 3) + (3 * (a |^ 2))) + (3 * a)) + 1) * ((a + 1) |^ 2) is ext-real V14() real set
2 * a is ext-real V14() real set
(2 * a) * 1 is ext-real V14() real set
(a |^ 2) + ((2 * a) * 1) is ext-real V14() real set
1 |^ 2 is ext-real natural V14() real V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
((a |^ 2) + ((2 * a) * 1)) + (1 |^ 2) is ext-real V14() real set
((((a |^ 3) + (3 * (a |^ 2))) + (3 * a)) + 1) * (((a |^ 2) + ((2 * a) * 1)) + (1 |^ 2)) is ext-real V14() real set
(a |^ 2) + (2 * a) is ext-real V14() real set
((a |^ 2) + (2 * a)) + 1 is ext-real V14() real set
((((a |^ 3) + (3 * (a |^ 2))) + (3 * a)) + 1) * (((a |^ 2) + (2 * a)) + 1) is ext-real V14() real set
(a |^ 3) * (a |^ 2) is ext-real V14() real set
(2 * a) * (a |^ 3) is ext-real V14() real set
((a |^ 3) * (a |^ 2)) + ((2 * a) * (a |^ 3)) is ext-real V14() real set
(a |^ 3) * 1 is ext-real V14() real set
(((a |^ 3) * (a |^ 2)) + ((2 * a) * (a |^ 3))) + ((a |^ 3) * 1) is ext-real V14() real set
(3 * (a |^ 2)) * (a |^ 2) is ext-real V14() real set
(2 * a) * (3 * (a |^ 2)) is ext-real V14() real set
((3 * (a |^ 2)) * (a |^ 2)) + ((2 * a) * (3 * (a |^ 2))) is ext-real V14() real set
(3 * (a |^ 2)) * 1 is ext-real V14() real set
(((3 * (a |^ 2)) * (a |^ 2)) + ((2 * a) * (3 * (a |^ 2)))) + ((3 * (a |^ 2)) * 1) is ext-real V14() real set
((((a |^ 3) * (a |^ 2)) + ((2 * a) * (a |^ 3))) + ((a |^ 3) * 1)) + ((((3 * (a |^ 2)) * (a |^ 2)) + ((2 * a) * (3 * (a |^ 2)))) + ((3 * (a |^ 2)) * 1)) is ext-real V14() real set
(3 * a) * (a |^ 2) is ext-real V14() real set
(3 * a) * (2 * a) is ext-real V14() real set
((3 * a) * (a |^ 2)) + ((3 * a) * (2 * a)) is ext-real V14() real set
(3 * a) * 1 is ext-real V14() real set
(((3 * a) * (a |^ 2)) + ((3 * a) * (2 * a))) + ((3 * a) * 1) is ext-real V14() real set
(((((a |^ 3) * (a |^ 2)) + ((2 * a) * (a |^ 3))) + ((a |^ 3) * 1)) + ((((3 * (a |^ 2)) * (a |^ 2)) + ((2 * a) * (3 * (a |^ 2)))) + ((3 * (a |^ 2)) * 1))) + ((((3 * a) * (a |^ 2)) + ((3 * a) * (2 * a))) + ((3 * a) * 1)) is ext-real V14() real set
((((((a |^ 3) * (a |^ 2)) + ((2 * a) * (a |^ 3))) + ((a |^ 3) * 1)) + ((((3 * (a |^ 2)) * (a |^ 2)) + ((2 * a) * (3 * (a |^ 2)))) + ((3 * (a |^ 2)) * 1))) + ((((3 * a) * (a |^ 2)) + ((3 * a) * (2 * a))) + ((3 * a) * 1))) + (((a |^ 2) + (2 * a)) + 1) is ext-real V14() real set
a |^ (3 + 2) is ext-real V14() real set
a * (a |^ 3) is ext-real V14() real set
2 * (a * (a |^ 3)) is ext-real V14() real set
(a |^ (3 + 2)) + (2 * (a * (a |^ 3))) is ext-real V14() real set
((a |^ (3 + 2)) + (2 * (a * (a |^ 3)))) + (a |^ 3) is ext-real V14() real set
(a |^ 2) * (a |^ 2) is ext-real V14() real set
3 * ((a |^ 2) * (a |^ 2)) is ext-real V14() real set
a * (a |^ 2) is ext-real V14() real set
2 * (a * (a |^ 2)) is ext-real V14() real set
(2 * (a * (a |^ 2))) * 3 is ext-real V14() real set
(3 * ((a |^ 2) * (a |^ 2))) + ((2 * (a * (a |^ 2))) * 3) is ext-real V14() real set
((3 * ((a |^ 2) * (a |^ 2))) + ((2 * (a * (a |^ 2))) * 3)) + (3 * (a |^ 2)) is ext-real V14() real set
(((a |^ (3 + 2)) + (2 * (a * (a |^ 3)))) + (a |^ 3)) + (((3 * ((a |^ 2) * (a |^ 2))) + ((2 * (a * (a |^ 2))) * 3)) + (3 * (a |^ 2))) is ext-real V14() real set
3 * (a * (a |^ 2)) is ext-real V14() real set
(3 * (a * a)) * 2 is ext-real V14() real set
(3 * (a * (a |^ 2))) + ((3 * (a * a)) * 2) is ext-real V14() real set
((3 * (a * (a |^ 2))) + ((3 * (a * a)) * 2)) + (3 * a) is ext-real V14() real set
((((a |^ (3 + 2)) + (2 * (a * (a |^ 3)))) + (a |^ 3)) + (((3 * ((a |^ 2) * (a |^ 2))) + ((2 * (a * (a |^ 2))) * 3)) + (3 * (a |^ 2)))) + (((3 * (a * (a |^ 2))) + ((3 * (a * a)) * 2)) + (3 * a)) is ext-real V14() real set
(((((a |^ (3 + 2)) + (2 * (a * (a |^ 3)))) + (a |^ 3)) + (((3 * ((a |^ 2) * (a |^ 2))) + ((2 * (a * (a |^ 2))) * 3)) + (3 * (a |^ 2)))) + (((3 * (a * (a |^ 2))) + ((3 * (a * a)) * 2)) + (3 * a))) + (((a |^ 2) + (2 * a)) + 1) is ext-real