:: GR_CY_3 semantic presentation

REAL is set
NAT is non empty V2() V4() V5() V6() non finite cardinal limit_cardinal Element of K6(REAL)
K6(REAL) is set
K677() is strict algebraic-closed doubleLoopStr
the carrier of K677() is set
COMPLEX is set
NAT is non empty V2() V4() V5() V6() non finite cardinal limit_cardinal set
K6(NAT) is V2() non finite set
K6(NAT) is V2() non finite set
1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
K7(1,1) is Relation-like finite set
K6(K7(1,1)) is finite V40() set
K7(K7(1,1),1) is Relation-like finite set
K6(K7(K7(1,1),1)) is finite V40() set
K7(K7(1,1),REAL) is Relation-like set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is Relation-like set
K7(K7(REAL,REAL),REAL) is Relation-like set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
K7(2,2) is Relation-like finite set
K7(K7(2,2),REAL) is Relation-like set
K6(K7(K7(2,2),REAL)) is set
RAT is set
INT is set
K6(K7(REAL,REAL)) is set
K339(2) is V159() L15()
the carrier of K339(2) is set
K480() is non empty strict Group-like associative commutative cyclic multMagma
the carrier of K480() is non empty V139() set
INT.Ring is non empty non degenerated V53() non finite left_add-cancelable right_add-cancelable right_complementable strict V147() V148() V149() unital associative commutative Euclidian V222() V223() V224() V225() V226() V227() V252() V253() V254() V255() domRing-like doubleLoopStr
addint is Relation-like Function-like V32(K7(INT,INT), INT ) Element of K6(K7(K7(INT,INT),INT))
K7(INT,INT) is Relation-like set
K7(K7(INT,INT),INT) is Relation-like set
K6(K7(K7(INT,INT),INT)) is set
multint is Relation-like Function-like V32(K7(INT,INT), INT ) Element of K6(K7(K7(INT,INT),INT))
In (1,INT) is V11() V12() integer ext-real Element of INT
0 is empty V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative Relation-like non-empty empty-yielding finite finite-yielding V40() cardinal {} -element Element of NAT
{} is empty V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative Relation-like non-empty empty-yielding finite finite-yielding V40() cardinal {} -element set
In (0,INT) is V11() V12() integer ext-real Element of INT
doubleLoopStr(# INT,addint,multint,(In (1,INT)),(In (0,INT)) #) is strict doubleLoopStr
the carrier of INT.Ring is non empty V2() non finite V139() set
K7( the carrier of INT.Ring,NAT) is V2() Relation-like non finite set
K6(K7( the carrier of INT.Ring,NAT)) is V2() non finite set
K7(COMPLEX,COMPLEX) is Relation-like set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is Relation-like set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(RAT,RAT) is Relation-like set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is Relation-like set
K6(K7(K7(RAT,RAT),RAT)) is set
K6(K7(INT,INT)) is set
K7(NAT,NAT) is V2() Relation-like non finite set
K7(K7(NAT,NAT),NAT) is V2() Relation-like non finite set
K6(K7(K7(NAT,NAT),NAT)) is V2() non finite set
K588() is set
K7(NAT,REAL) is Relation-like set
K6(K7(NAT,REAL)) is set
K313(1,NAT) is M11( NAT )
K7(NAT, the carrier of K677()) is Relation-like set
K6(K7(NAT, the carrier of K677())) is set
K6( the carrier of K677()) is set
3 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
7 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
4 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
5 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
6 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
- 1 is V11() V12() integer ext-real non positive set
{0} is non empty V2() finite V40() 1 -element Element of K6(NAT)
8 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
F * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
a gcd F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
F * f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
g is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
a * g is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
f * g is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
F * (f * g) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
a gcd F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
2 * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * G) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
2 * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * G) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
4 - 2 is V11() V12() integer ext-real set
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
a is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
2 * a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * a) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 gcd 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 * a) + 1) - 1 is V11() V12() integer ext-real set
2 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
0 + 2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
a is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
2 * a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * a) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F div 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 4) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 4) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 4) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F div 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 4) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 4) + 2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 4) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 2) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(((F div 4) * 2) + 1) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
0 + 3 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 6 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(4 * F) mod 6 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (2 * F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * (2 * F)) mod (2 * 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * F) mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((2 * F) mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 mod 3) * (F mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 mod 3) * (F mod 3)) mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (((2 mod 3) * (F mod 3)) mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (F mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * (F mod 3)) mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((2 * (F mod 3)) mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * 2) mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((2 * 2) mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 + (3 * 1) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(1 + (3 * 1)) mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((1 + (3 * 1)) mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (1 mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(3 * F) mod 6 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(3 * F) mod (3 * 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F mod 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * (F mod 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
6 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F + (6 * F) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F + (6 * F)) mod 6 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(3 * F) + (4 * F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((3 * F) + (4 * F)) mod 6 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(3 * 1) + (2 * 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((3 * 1) + (2 * 1)) mod 6 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
12 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
11 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 12 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
7 - 2 is V11() V12() integer ext-real set
F mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
9 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
9 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(9 * F) mod 12 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * (3 * F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(3 * (3 * F)) mod (3 * 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(3 * F) mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * ((3 * F) mod 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(3 mod 4) * (F mod 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((3 mod 4) * (F mod 4)) mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * (((3 mod 4) * (F mod 4)) mod 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(3 * 3) mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * ((3 * 3) mod 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 + (4 * 2) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(1 + (4 * 2)) mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * ((1 + (4 * 2)) mod 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * (1 mod 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(4 * F) mod 12 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 * 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(4 * F) mod (4 * 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 * (F mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
12 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F + (12 * F) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F + (12 * F)) mod 12 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(4 * F) + (9 * F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((4 * F) + (9 * F)) mod 12 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(4 * 2) + (3 * 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((4 * 2) + (3 * 1)) mod 12 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
a is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
2 * a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * a) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F div 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 8) * 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 8) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 8) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F div 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 8) * 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 8) + 2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 8) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 4) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(((F div 8) * 4) + 1) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F div 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 8) * 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 8) + 4 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 8) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 4) + 2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(((F div 8) * 4) + 2) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F div 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 8) * 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 8) + 5 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 8) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 2) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(((F div 8) * 2) + 1) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F div 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 8) * 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 8) + 6 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 8) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 4) + 3 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(((F div 8) * 4) + 3) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
7 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
0 + 7 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
2 * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * G) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F div 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 4) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 4) + 2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 4) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 2) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(((F div 4) * 2) + 1) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
0 + 3 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
2 * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * G) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * F) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
Euler F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F - 1 is V11() V12() integer ext-real set
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
2 * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * G) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
Euler a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
Euler G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
f is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
2 * f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
Euler F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
g is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
2 * g is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(Euler F) * (Euler G) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 * g is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(4 * g) * f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
Z/Z* F is non empty finite Group-like associative commutative multMagma
Segm0 F is non empty finite Element of K6(NAT)
multint0 F is Relation-like Function-like V28(K7((Segm0 F),(Segm0 F))) V32(K7((Segm0 F),(Segm0 F)), Segm0 F) finite Element of K6(K7(K7((Segm0 F),(Segm0 F)),(Segm0 F)))
K7((Segm0 F),(Segm0 F)) is Relation-like finite set
K7(K7((Segm0 F),(Segm0 F)),(Segm0 F)) is Relation-like finite set
K6(K7(K7((Segm0 F),(Segm0 F)),(Segm0 F))) is finite V40() set
multint F is Relation-like Function-like V28(K7((Segm F),(Segm F))) V32(K7((Segm F),(Segm F)), Segm F) Element of K6(K7(K7((Segm F),(Segm F)),(Segm F)))
Segm F is non empty V140() Element of K6(NAT)
K7((Segm F),(Segm F)) is Relation-like set
K7(K7((Segm F),(Segm F)),(Segm F)) is Relation-like set
K6(K7(K7((Segm F),(Segm F)),(Segm F))) is set
(multint F) || (Segm0 F) is set
multMagma(# (Segm0 F),(multint0 F) #) is strict multMagma
card (Z/Z* F) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of (Z/Z* F) is non empty finite set
card the carrier of (Z/Z* F) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
2 * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * G) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F - 1 is V11() V12() integer ext-real set
F is non empty finite Group-like associative commutative cyclic multMagma
card F is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of F is non empty finite set
card the carrier of F is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
G * a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
f is Element of the carrier of F
ord f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
f |^ a is Element of the carrier of F
power F is Relation-like Function-like V28(K7( the carrier of F,NAT)) V32(K7( the carrier of F,NAT), the carrier of F) Element of K6(K7(K7( the carrier of F,NAT), the carrier of F))
K7( the carrier of F,NAT) is V2() Relation-like non finite set
K7(K7( the carrier of F,NAT), the carrier of F) is V2() Relation-like non finite set
K6(K7(K7( the carrier of F,NAT), the carrier of F)) is V2() non finite set
(power F) . (f,a) is set
ord (f |^ a) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
g is Element of the carrier of F
ord g is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
{g} is non empty V2() finite 1 -element Element of K6( the carrier of F)
K6( the carrier of F) is finite V40() set
gr {g} is non empty finite strict Group-like associative commutative Subgroup of F
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
Z/Z* F is non empty finite Group-like associative commutative multMagma
Segm0 F is non empty finite Element of K6(NAT)
multint0 F is Relation-like Function-like V28(K7((Segm0 F),(Segm0 F))) V32(K7((Segm0 F),(Segm0 F)), Segm0 F) finite Element of K6(K7(K7((Segm0 F),(Segm0 F)),(Segm0 F)))
K7((Segm0 F),(Segm0 F)) is Relation-like finite set
K7(K7((Segm0 F),(Segm0 F)),(Segm0 F)) is Relation-like finite set
K6(K7(K7((Segm0 F),(Segm0 F)),(Segm0 F))) is finite V40() set
multint F is Relation-like Function-like V28(K7((Segm F),(Segm F))) V32(K7((Segm F),(Segm F)), Segm F) Element of K6(K7(K7((Segm F),(Segm F)),(Segm F)))
Segm F is non empty V140() Element of K6(NAT)
K7((Segm F),(Segm F)) is Relation-like set
K7(K7((Segm F),(Segm F)),(Segm F)) is Relation-like set
K6(K7(K7((Segm F),(Segm F)),(Segm F))) is set
(multint F) || (Segm0 F) is set
multMagma(# (Segm0 F),(multint0 F) #) is strict multMagma
card (Z/Z* F) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of (Z/Z* F) is non empty finite set
card the carrier of (Z/Z* F) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
2 * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
a is Element of the carrier of (Z/Z* F)
ord a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
{a} is non empty V2() finite 1 -element Element of K6( the carrier of (Z/Z* F))
K6( the carrier of (Z/Z* F)) is finite V40() set
gr {a} is non empty finite strict Group-like associative commutative Subgroup of Z/Z* F
f is Element of the carrier of (Z/Z* F)
ord f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
{f} is non empty V2() finite 1 -element Element of K6( the carrier of (Z/Z* F))
gr {f} is non empty finite strict Group-like associative commutative Subgroup of Z/Z* F
card (gr {f}) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of (gr {f}) is non empty finite set
card the carrier of (gr {f}) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
(1). (Z/Z* F) is non empty finite strict Group-like associative commutative cyclic Subgroup of Z/Z* F
card ((1). (Z/Z* F)) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of ((1). (Z/Z* F)) is non empty finite set
card the carrier of ((1). (Z/Z* F)) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
g is non empty finite strict Group-like associative commutative Subgroup of Z/Z* F
card g is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of g is non empty finite set
card the carrier of g is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
y is non empty finite strict Group-like associative commutative Subgroup of Z/Z* F
card y is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of y is non empty finite set
card the carrier of y is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
card (gr {a}) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of (gr {a}) is non empty finite set
card the carrier of (gr {a}) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
x is non empty finite strict Group-like associative commutative Subgroup of Z/Z* F
card x is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of x is non empty finite set
card the carrier of x is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
x is non empty finite strict Group-like associative commutative Subgroup of Z/Z* F
card x is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of x is non empty finite set
card the carrier of x is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
gg is non empty finite strict Group-like associative commutative Subgroup of Z/Z* F
card gg is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of gg is non empty finite set
card the carrier of gg is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
n is non empty finite strict Group-like associative commutative Subgroup of Z/Z* F
card n is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of n is non empty finite set
card the carrier of n is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
gg is non empty finite strict Group-like associative commutative Subgroup of Z/Z* F
F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ F) - 1 is V11() V12() integer ext-real set
2 |^ 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 |^ (1 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ 1) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 |^ (2 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
16 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 + 2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 |^ (2 + 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
256 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
4 + 4 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 |^ (4 + 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
16 * 16 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(0) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ 0 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ 0) - 1 is V11() V12() integer ext-real set
1 - 1 is V11() V12() integer ext-real set
(1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ 1) - 1 is V11() V12() integer ext-real set
2 - 1 is V11() V12() integer ext-real set
(2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ 2) - 1 is V11() V12() integer ext-real set
(3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ 3) - 1 is V11() V12() integer ext-real set
(5) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ 5 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ 5) - 1 is V11() V12() integer ext-real set
31 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
3 + 2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 |^ (3 + 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ (3 + 2)) - 1 is V11() V12() integer ext-real set
(2 |^ 3) * (2 |^ 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 |^ 3) * (2 |^ 2)) - 1 is V11() V12() integer ext-real set
(7) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ 7 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ 7) - 1 is V11() V12() integer ext-real set
127 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
4 + 3 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 |^ (4 + 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ (4 + 3)) - 1 is V11() V12() integer ext-real set
(2 |^ 4) * (2 |^ 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 |^ 4) * (2 |^ 3)) - 1 is V11() V12() integer ext-real set
(11) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ 11 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ 11) - 1 is V11() V12() integer ext-real set
23 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
89 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
23 * 89 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
8 + 3 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 |^ (8 + 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ (8 + 3)) - 1 is V11() V12() integer ext-real set
(2 |^ 8) * (2 |^ 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 |^ 8) * (2 |^ 3)) - 1 is V11() V12() integer ext-real set
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
(F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ F) - 1 is V11() V12() integer ext-real set
2 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F) mod (2 * F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 - 1 is V11() V12() integer ext-real set
F -' 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ (F -' 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (2 |^ (F -' 1)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * (2 |^ (F -' 1))) - 1 is V11() V12() integer ext-real set
((2 * (2 |^ (F -' 1))) - 1) mod (2 * F) is V11() V12() integer ext-real set
(2 * (2 |^ (F -' 1))) mod (2 * F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 mod (2 * F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 * (2 |^ (F -' 1))) mod (2 * F)) - (1 mod (2 * F)) is V11() V12() integer ext-real set
(((2 * (2 |^ (F -' 1))) mod (2 * F)) - (1 mod (2 * F))) mod (2 * F) is V11() V12() integer ext-real set
(2 |^ (F -' 1)) mod F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((2 |^ (F -' 1)) mod F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * ((2 |^ (F -' 1)) mod F)) - (1 mod (2 * F)) is V11() V12() integer ext-real set
((2 * ((2 |^ (F -' 1)) mod F)) - (1 mod (2 * F))) mod (2 * F) is V11() V12() integer ext-real set
(2 * 1) - (1 mod (2 * F)) is V11() V12() integer ext-real set
((2 * 1) - (1 mod (2 * F))) mod (2 * F) is V11() V12() integer ext-real set
(2 * 1) - 1 is V11() V12() integer ext-real set
((2 * 1) - 1) mod (2 * F) is V11() V12() integer ext-real set
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
(F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ F) - 1 is V11() V12() integer ext-real set
(F) mod 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 + 0 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F - 2 is V11() V12() integer ext-real set
2 - 2 is V11() V12() integer ext-real set
F -' 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F -' 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ (F -' 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (2 |^ (F -' 1)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * (2 |^ (F -' 1))) - 1 is V11() V12() integer ext-real set
((2 * (2 |^ (F -' 1))) - 1) mod 8 is V11() V12() integer ext-real set
2 * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * (2 |^ (F -' 1))) mod (2 * 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 mod 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 * (2 |^ (F -' 1))) mod (2 * 4)) - (1 mod 8) is V11() V12() integer ext-real set
(((2 * (2 |^ (F -' 1))) mod (2 * 4)) - (1 mod 8)) mod 8 is V11() V12() integer ext-real set
(2 |^ (F -' 1)) mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((2 |^ (F -' 1)) mod 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * ((2 |^ (F -' 1)) mod 4)) - (1 mod 8) is V11() V12() integer ext-real set
((2 * ((2 |^ (F -' 1)) mod 4)) - (1 mod 8)) mod 8 is V11() V12() integer ext-real set
(F -' 1) -' 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ ((F -' 1) -' 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (2 |^ ((F -' 1) -' 1)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * (2 |^ ((F -' 1) -' 1))) mod (2 * 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((2 * (2 |^ ((F -' 1) -' 1))) mod (2 * 2)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * ((2 * (2 |^ ((F -' 1) -' 1))) mod (2 * 2))) - (1 mod 8) is V11() V12() integer ext-real set
((2 * ((2 * (2 |^ ((F -' 1) -' 1))) mod (2 * 2))) - (1 mod 8)) mod 8 is V11() V12() integer ext-real set
2 |^ (F -' 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (2 |^ (F -' 2)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * (2 |^ (F -' 2))) mod (2 * 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((2 * (2 |^ (F -' 2))) mod (2 * 2)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * ((2 * (2 |^ (F -' 2))) mod (2 * 2))) - (1 mod 8) is V11() V12() integer ext-real set
((2 * ((2 * (2 |^ (F -' 2))) mod (2 * 2))) - (1 mod 8)) mod 8 is V11() V12() integer ext-real set
(2 |^ (F -' 2)) mod 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((2 |^ (F -' 2)) mod 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (2 * ((2 |^ (F -' 2)) mod 2)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * (2 * ((2 |^ (F -' 2)) mod 2))) - (1 mod 8) is V11() V12() integer ext-real set
((2 * (2 * ((2 |^ (F -' 2)) mod 2))) - (1 mod 8)) mod 8 is V11() V12() integer ext-real set
4 * ((2 |^ (F -' 2)) mod 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(4 * ((2 |^ (F -' 2)) mod 2)) - 1 is V11() V12() integer ext-real set
((4 * ((2 |^ (F -' 2)) mod 2)) - 1) mod 8 is V11() V12() integer ext-real set
4 * 0 is empty V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative Relation-like non-empty empty-yielding finite finite-yielding V40() cardinal {} -element Element of NAT
(4 * 0) - 1 is non empty V11() V12() integer ext-real non positive negative set
((4 * 0) - 1) mod 8 is V11() V12() integer ext-real set
8 * 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(- 1) + (8 * 1) is V11() V12() integer ext-real set
((- 1) + (8 * 1)) mod 8 is V11() V12() integer ext-real set
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ F) - 1 is V11() V12() integer ext-real set
2 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * F) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
5 - 3 is V11() V12() integer ext-real set
2 gcd ((2 * F) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F div 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 4) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 4) + 3 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 4) * 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 8) + 7 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
((2 * F) + 1) mod 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
7 mod 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 * F) + 1) -' 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(((2 * F) + 1) -' 1) div 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ ((((2 * F) + 1) -' 1) div 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ ((((2 * F) + 1) -' 1) div 2)) - 1 is V11() V12() integer ext-real set
((2 |^ ((((2 * F) + 1) -' 1) div 2)) - 1) mod ((2 * F) + 1) is V11() V12() integer ext-real set
(2 * F) div 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ ((2 * F) div 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ ((2 * F) div 2)) - 1 is V11() V12() integer ext-real set
((2 |^ ((2 * F) div 2)) - 1) mod ((2 * F) + 1) is V11() V12() integer ext-real set
((2 |^ F) - 1) mod ((2 * F) + 1) is V11() V12() integer ext-real set
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ F) - 1 is V11() V12() integer ext-real set
2 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * F) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
5 - 3 is V11() V12() integer ext-real set
2 gcd ((2 * F) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F div 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 4) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 4) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 4) * 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 8) + 3 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
((2 * F) + 1) mod 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 mod 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 * F) + 1) -' 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(((2 * F) + 1) -' 1) div 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ ((((2 * F) + 1) -' 1) div 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ ((((2 * F) + 1) -' 1) div 2)) mod ((2 * F) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 * F) + 1) - 1 is V11() V12() integer ext-real set
(2 * F) div 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ ((2 * F) div 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ ((2 * F) div 2)) mod ((2 * F) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
5 - 4 is V11() V12() integer ext-real set
1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
((2 * F) + 1) - 2 is V11() V12() integer ext-real set
(F) mod ((2 * F) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ F) mod ((2 * F) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 mod ((2 * F) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 |^ F) mod ((2 * F) + 1)) - (1 mod ((2 * F) + 1)) is V11() V12() integer ext-real set
(((2 |^ F) mod ((2 * F) + 1)) - (1 mod ((2 * F) + 1))) mod ((2 * F) + 1) is V11() V12() integer ext-real set
(((2 * F) + 1) - 1) - (1 mod ((2 * F) + 1)) is V11() V12() integer ext-real set
((((2 * F) + 1) - 1) - (1 mod ((2 * F) + 1))) mod ((2 * F) + 1) is V11() V12() integer ext-real set
(((2 * F) + 1) - 1) - 1 is V11() V12() integer ext-real set
((((2 * F) + 1) - 1) - 1) mod ((2 * F) + 1) is V11() V12() integer ext-real set
F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
F - 1 is V11() V12() integer ext-real set
G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
F |^ G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
(F |^ G) - 1 is V11() V12() integer ext-real set
2 |^ G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ G) - 1 is V11() V12() integer ext-real set
1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
((F |^ G) - 1) mod (F - 1) is V11() V12() integer ext-real set
2 - 1 is V11() V12() integer ext-real set
F mod (F - 1) is V11() V12() integer ext-real set
(F - 1) * (- 1) is V11() V12() integer ext-real set
F + ((F - 1) * (- 1)) is V11() V12() integer ext-real set
(F + ((F - 1) * (- 1))) mod (F - 1) is V11() V12() integer ext-real set
(F |^ G) mod (F - 1) is V11() V12() integer ext-real set
((F |^ G) - 1) mod (F - 1) is V11() V12() integer ext-real set
1 mod (F - 1) is V11() V12() integer ext-real set
((F |^ G) mod (F - 1)) - (1 mod (F - 1)) is V11() V12() integer ext-real set
(((F |^ G) mod (F - 1)) - (1 mod (F - 1))) mod (F - 1) is V11() V12() integer ext-real set
1 - 1 is V11() V12() integer ext-real set
(1 - 1) mod (F - 1) is V11() V12() integer ext-real set
G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
F |^ G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
(F |^ G) - 1 is V11() V12() integer ext-real set
0 - 1 is non empty V11() V12() integer ext-real non positive negative set
1 - 1 is V11() V12() integer ext-real