:: 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 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
1 + 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
2 - 1 is V11() V12() integer ext-real set
a 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
a * f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ a 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
F |^ a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
(F |^ a) - 1 is V11() V12() integer ext-real set
0 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F |^ a) |^ f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
((F |^ a) |^ 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) 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 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 V11() V12() integer ext-real set
a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
(F |^ G) mod a is V11() V12() integer ext-real set
F mod a is V11() V12() integer ext-real set
(F mod a) |^ G is V11() V12() integer ext-real set
((F mod a) |^ G) mod a is V11() V12() integer ext-real set
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
F |^ f is V11() V12() integer ext-real set
(F |^ f) mod a is V11() V12() integer ext-real set
(F mod a) |^ f is V11() V12() integer ext-real set
((F mod a) |^ f) mod a is V11() V12() integer ext-real set
f + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F |^ (f + 1) is V11() V12() integer ext-real set
(F |^ (f + 1)) mod a is V11() V12() integer ext-real set
(F mod a) |^ (f + 1) is V11() V12() integer ext-real set
((F mod a) |^ (f + 1)) mod a is V11() V12() integer ext-real set
(F |^ f) * F is V11() V12() integer ext-real set
((F |^ f) * F) mod a is V11() V12() integer ext-real set
((F |^ f) mod a) * (F mod a) is V11() V12() integer ext-real set
(((F |^ f) mod a) * (F mod a)) mod a is V11() V12() integer ext-real set
((F mod a) |^ f) * (F mod a) is V11() V12() integer ext-real set
(((F mod a) |^ f) * (F mod a)) mod a is V11() V12() integer ext-real set
(F mod a) mod a is V11() V12() integer ext-real set
(((F mod a) |^ f) mod a) * ((F mod a) mod a) is V11() V12() integer ext-real set
((((F mod a) |^ f) mod a) * ((F mod a) mod a)) mod a is V11() V12() integer ext-real set
(((F mod a) |^ f) mod a) * (F mod a) is V11() V12() integer ext-real set
((((F mod a) |^ f) mod a) * (F mod a)) mod a is V11() V12() integer ext-real set
F |^ 0 is V11() V12() integer ext-real set
(F |^ 0) mod a is V11() V12() integer ext-real set
(F mod a) |^ 0 is V11() V12() integer ext-real set
((F mod a) |^ 0) mod a is V11() V12() integer ext-real set
F is V11() V12() integer ext-real set
a is V11() V12() integer ext-real set
G is V11() V12() integer ext-real set
F - G is V11() V12() integer ext-real set
f is V11() V12() integer ext-real set
a * f is V11() V12() integer ext-real set
G gcd a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
(a * f) + G is V11() V12() integer ext-real set
F gcd a 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
G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
G * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
a is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
G gcd a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(G * G) gcd a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F is V11() V12() integer ext-real set
G is V11() V12() integer ext-real set
G * G is V11() V12() integer ext-real set
a is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
(G * G) gcd a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
G gcd a 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
G is V11() V12() integer ext-real set
G mod F is V11() V12() integer ext-real set
(G mod F) mod F is V11() V12() integer ext-real set
F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
G is V11() V12() integer ext-real set
G mod F is V11() V12() integer ext-real set
a 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
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
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 |^ f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
(F |^ f) mod a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F mod a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F mod a) |^ f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
((F mod a) |^ f) mod a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(G |^ f) mod a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
G mod a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(G mod a) |^ f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
((G mod a) |^ f) mod a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F is V11() V12() integer ext-real set
G is V11() V12() integer ext-real set
a 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 |^ f is V11() V12() integer ext-real set
G |^ f is V11() V12() integer ext-real set
g is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
G mod a is V11() V12() integer ext-real set
y is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
x is V11() V12() integer ext-real set
(G mod a) mod a is V11() V12() integer ext-real set
x is V11() V12() integer ext-real set
g |^ f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
y |^ f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
(g |^ f) mod a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(y |^ f) mod a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(G |^ f) mod a is V11() V12() integer ext-real set
(G mod a) |^ f is V11() V12() integer ext-real set
((G mod a) |^ f) mod a is V11() V12() integer ext-real set
(F |^ f) mod a is V11() V12() integer ext-real set
F mod a is V11() V12() integer ext-real set
(F mod a) |^ f is V11() V12() integer ext-real set
((F mod a) |^ f) mod a is V11() V12() integer ext-real set
g mod a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F is V11() V12() integer ext-real set
F * F 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
(F * F) mod G is V11() V12() integer ext-real set
F mod G is V11() V12() integer ext-real set
1 mod G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
a is V11() V12() integer ext-real set
a * a is V11() V12() integer ext-real set
(a * a) mod G is V11() V12() integer ext-real set
(a * a) - 1 is V11() V12() integer ext-real set
a + 1 is V11() V12() integer ext-real set
a - 1 is V11() V12() integer ext-real set
(a + 1) * (a - 1) is V11() V12() integer ext-real set
G * 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
(F mod G) * (F mod G) is V11() V12() integer ext-real set
((F mod G) * (F mod G)) mod G is V11() V12() integer ext-real set
0 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
a mod G is V11() V12() integer ext-real set
a - (- 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
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
INT.Ring F is non empty non degenerated V53() left_add-cancelable right_add-cancelable right_complementable almost_left_invertible strict V147() V148() V149() unital associative commutative Euclidian V222() V223() V224() V225() V226() V227() V252() V253() V254() V255() domRing-like doubleLoopStr
addint 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)))
In (1,(Segm F)) is Element of Segm F
In (0,(Segm F)) is Element of Segm F
doubleLoopStr(# (Segm F),(addint F),(multint F),(In (1,(Segm F))),(In (0,(Segm F))) #) is strict doubleLoopStr
MultGroup (INT.Ring F) is non empty strict Group-like associative multMagma
(Segm F) \ {0} is Element of K6(NAT)
NonZero (INT.Ring F) is non empty Element of K6( the carrier of (INT.Ring F))
the carrier of (INT.Ring F) is non empty V2() set
K6( the carrier of (INT.Ring F)) is set
[#] (INT.Ring F) is non empty non proper Element of K6( the carrier of (INT.Ring F))
0. (INT.Ring F) is V55( INT.Ring F) Element of the carrier of (INT.Ring F)
the ZeroF of (INT.Ring F) is Element of the carrier of (INT.Ring F)
{(0. (INT.Ring F))} is non empty V2() finite 1 -element set
([#] (INT.Ring F)) \ {(0. (INT.Ring F))} is Element of K6( the carrier of (INT.Ring F))
the carrier of (MultGroup (INT.Ring F)) is non empty set
the multF of (Z/Z* F) is Relation-like Function-like V28(K7( the carrier of (Z/Z* F), the carrier of (Z/Z* F))) V32(K7( the carrier of (Z/Z* F), the carrier of (Z/Z* F)), the carrier of (Z/Z* F)) finite Element of K6(K7(K7( the carrier of (Z/Z* F), the carrier of (Z/Z* F)), the carrier of (Z/Z* F)))
the carrier of (Z/Z* F) is non empty finite set
K7( the carrier of (Z/Z* F), the carrier of (Z/Z* F)) is Relation-like finite set
K7(K7( the carrier of (Z/Z* F), the carrier of (Z/Z* F)), the carrier of (Z/Z* F)) is Relation-like finite set
K6(K7(K7( the carrier of (Z/Z* F), the carrier of (Z/Z* F)), the carrier of (Z/Z* F))) is finite V40() set
(multint F) || ((Segm F) \ {0}) is set
the multF of (MultGroup (INT.Ring F)) is Relation-like Function-like V28(K7( the carrier of (MultGroup (INT.Ring F)), the carrier of (MultGroup (INT.Ring F)))) V32(K7( the carrier of (MultGroup (INT.Ring F)), the carrier of (MultGroup (INT.Ring F))), the carrier of (MultGroup (INT.Ring F))) Element of K6(K7(K7( the carrier of (MultGroup (INT.Ring F)), the carrier of (MultGroup (INT.Ring F))), the carrier of (MultGroup (INT.Ring F))))
K7( the carrier of (MultGroup (INT.Ring F)), the carrier of (MultGroup (INT.Ring F))) is Relation-like set
K7(K7( the carrier of (MultGroup (INT.Ring F)), the carrier of (MultGroup (INT.Ring F))), the carrier of (MultGroup (INT.Ring F))) is Relation-like set
K6(K7(K7( the carrier of (MultGroup (INT.Ring F)), the carrier of (MultGroup (INT.Ring F))), the carrier of (MultGroup (INT.Ring F)))) is set
F is non empty non degenerated V53() left_add-cancelable right_add-cancelable right_complementable almost_left_invertible V147() V148() V149() unital associative commutative Euclidian V222() V223() V224() V225() V226() V227() V252() V253() V254() V255() domRing-like doubleLoopStr
MultGroup F is non empty strict Group-like associative multMagma
the carrier of (MultGroup F) is non empty set
G is Element of the carrier of (MultGroup F)
a is Element of the carrier of (MultGroup F)
G * a is Element of the carrier of (MultGroup F)
a * G is Element of the carrier of (MultGroup F)
NonZero F is non empty Element of K6( the carrier of F)
the carrier of F is non empty V2() set
K6( the carrier of F) is set
[#] F is non empty non proper Element of K6( the carrier of F)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{(0. F)} is non empty V2() finite 1 -element set
([#] F) \ {(0. F)} is Element of K6( the carrier of F)
f is Element of the carrier of F
g is Element of the carrier of F
f * g is Element of the carrier of F
F is non empty non degenerated V53() left_add-cancelable right_add-cancelable right_complementable almost_left_invertible V147() V148() V149() unital associative commutative Euclidian V222() V223() V224() V225() V226() V227() V252() V253() V254() V255() domRing-like doubleLoopStr
MultGroup F is non empty strict Group-like associative commutative multMagma
the carrier of (MultGroup F) is non empty set
the carrier of F is non empty V2() set
G is Element of the carrier of (MultGroup F)
G " is Element of the carrier of (MultGroup F)
a is Element of the carrier of F
a " is Element of the carrier of F
NonZero F is non empty Element of K6( the carrier of F)
K6( the carrier of F) is set
[#] F is non empty non proper Element of K6( the carrier of F)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{(0. F)} is non empty V2() finite 1 -element set
([#] F) \ {(0. F)} is Element of K6( the carrier of F)
{(0. F)} is non empty V2() finite 1 -element Element of K6( the carrier of F)
a * (a ") is Element of the carrier of F
1. F is V55(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
1_ F is Element of the carrier of F
1_ (MultGroup F) is Element of the carrier of (MultGroup F)
g is Element of the carrier of (MultGroup F)
g * G is Element of the carrier of (MultGroup F)
(a ") * a is Element of the carrier of F
F is non empty non degenerated V53() left_add-cancelable right_add-cancelable right_complementable almost_left_invertible V147() V148() V149() unital associative commutative Euclidian V222() V223() V224() V225() V226() V227() V252() V253() V254() V255() domRing-like doubleLoopStr
MultGroup F is non empty strict Group-like associative commutative multMagma
the carrier of F is non empty V2() set
K7(NAT, the carrier of F) is V2() Relation-like non finite set
K6(K7(NAT, the carrier of F)) is V2() non finite set
1. F is V55(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
G is non empty Group-like associative commutative Subgroup of MultGroup F
the carrier of G is non empty set
a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
1_ F is Element of the carrier of F
<%(0. F),(1_ F)%> is non empty Relation-like Function-like V28( NAT ) V32( NAT , the carrier of F) V221(F) Element of K6(K7(NAT, the carrier of F))
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
<%(0. F),(1_ F)%> `^ f is non empty Relation-like Function-like V28( NAT ) V32( NAT , the carrier of F) V221(F) Element of K6(K7(NAT, the carrier of F))
1_. F is non empty Relation-like Function-like V28( NAT ) V32( NAT , the carrier of F) V221(F) Element of K6(K7(NAT, the carrier of F))
0_. F is non empty Relation-like Function-like V28( NAT ) V32( NAT , the carrier of F) V221(F) with_roots Element of K6(K7(NAT, the carrier of F))
K548( the carrier of F,NAT,(0. F)) is non empty V8() Relation-like Function-like V28( NAT ) V32( NAT , the carrier of F) Element of K6(K7(NAT, the carrier of F))
K752(NAT, the carrier of F,(0_. F),0,(1. F)) is non empty Relation-like Function-like V28( NAT ) V32( NAT , the carrier of F) Element of K6(K7(NAT, the carrier of F))
(<%(0. F),(1_ F)%> `^ f) - (1_. F) is non empty Relation-like Function-like V28( NAT ) V32( NAT , the carrier of F) V221(F) Element of K6(K7(NAT, the carrier of F))
- (1_. F) is non empty Relation-like Function-like V28( NAT ) V32( NAT , the carrier of F) V221(F) Element of K6(K7(NAT, the carrier of F))
K654(F,(<%(0. F),(1_ F)%> `^ f),(- (1_. F))) is non empty Relation-like Function-like V28( NAT ) V32( NAT , the carrier of F) V221(F) Element of K6(K7(NAT, the carrier of F))
y is Element of the carrier of F
x is Element of the carrier of G
x is Element of the carrier of F
x |^ a is Element of the carrier of G
power G is Relation-like Function-like V28(K7( the carrier of G,NAT)) V32(K7( the carrier of G,NAT), the carrier of G) Element of K6(K7(K7( the carrier of G,NAT), the carrier of G))
K7( the carrier of G,NAT) is V2() Relation-like non finite set
K7(K7( the carrier of G,NAT), the carrier of G) is V2() Relation-like non finite set
K6(K7(K7( the carrier of G,NAT), the carrier of G)) is V2() non finite set
(power G) . (x,a) is set
the carrier of (MultGroup F) is non empty set
gg is Element of the carrier of (MultGroup F)
gg |^ f is Element of the carrier of (MultGroup F)
power (MultGroup F) is Relation-like Function-like V28(K7( the carrier of (MultGroup F),NAT)) V32(K7( the carrier of (MultGroup F),NAT), the carrier of (MultGroup F)) Element of K6(K7(K7( the carrier of (MultGroup F),NAT), the carrier of (MultGroup F)))
K7( the carrier of (MultGroup F),NAT) is V2() Relation-like non finite set
K7(K7( the carrier of (MultGroup F),NAT), the carrier of (MultGroup F)) is V2() Relation-like non finite set
K6(K7(K7( the carrier of (MultGroup F),NAT), the carrier of (MultGroup F))) is V2() non finite set
(power (MultGroup F)) . (gg,f) is set
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) . (y,f) is Element of the carrier of F
eval (((<%(0. F),(1_ F)%> `^ f) - (1_. F)),y) is Element of the carrier of F
eval ((<%(0. F),(1_ F)%> `^ f),y) is Element of the carrier of F
eval ((1_. F),y) is Element of the carrier of F
(eval ((<%(0. F),(1_ F)%> `^ f),y)) - (eval ((1_. F),y)) is Element of the carrier of F
(eval ((<%(0. F),(1_ F)%> `^ f),y)) - (1_ F) is Element of the carrier of F
eval (<%(0. F),(1_ F)%>,y) is Element of the carrier of F
(power F) . ((eval (<%(0. F),(1_ F)%>,y)),f) is Element of the carrier of F
((power F) . ((eval (<%(0. F),(1_ F)%>,y)),f)) - (1_ F) is Element of the carrier of F
x - (1_ F) is Element of the carrier of F
a + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
len (1_. F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
len (- (1_. F)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
len <%(0. F),(1_ F)%> is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
len (<%(0. F),(1_ F)%> `^ f) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
a * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(a * 2) - a is V11() V12() integer ext-real set
((a * 2) - a) + 1 is V11() V12() integer ext-real set
len ((<%(0. F),(1_ F)%> `^ f) - (1_. F)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
max ((a + 1),1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
deg ((<%(0. F),(1_ F)%> `^ f) - (1_. F)) is V11() V12() integer ext-real set
(len ((<%(0. F),(1_ F)%> `^ f) - (1_. F))) - 1 is V11() V12() integer ext-real set
F is non empty non degenerated V53() left_add-cancelable right_add-cancelable right_complementable almost_left_invertible V147() V148() V149() unital associative commutative Euclidian V222() V223() V224() V225() V226() V227() V252() V253() V254() V255() domRing-like doubleLoopStr
MultGroup F is non empty strict Group-like associative commutative multMagma
G is non empty Group-like associative commutative Subgroup of MultGroup F
the carrier of G is non empty set
1_ G is Element of the carrier of G
a is Element of the carrier of G
ord a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
f is Element of the carrier of G
{a} is non empty V2() finite 1 -element Element of K6( the carrier of G)
K6( the carrier of G) is set
gr {a} is non empty strict Group-like associative commutative Subgroup of G
the carrier of (gr {a}) is non empty set
g is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
f |^ g is Element of the carrier of G
power G is Relation-like Function-like V28(K7( the carrier of G,NAT)) V32(K7( the carrier of G,NAT), the carrier of G) Element of K6(K7(K7( the carrier of G,NAT), the carrier of G))
K7( the carrier of G,NAT) is V2() Relation-like non finite set
K7(K7( the carrier of G,NAT), the carrier of G) is V2() Relation-like non finite set
K6(K7(K7( the carrier of G,NAT), the carrier of G)) is V2() non finite set
(power G) . (f,g) is set
the carrier of F is non empty V2() set
K7(NAT, the carrier of F) is V2() Relation-like non finite set
K6(K7(NAT, the carrier of F)) is V2() non finite set
1. F is V55(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
y is non empty Relation-like Function-like V28( NAT ) V32( NAT , the carrier of F) V221(F) Element of K6(K7(NAT, the carrier of F))
deg y is V11() V12() integer ext-real set
len y is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(len y) - 1 is V11() V12() integer ext-real set
the carrier of (MultGroup F) is non empty set
Roots y is Element of K6( the carrier of F)
K6( the carrier of F) is set
x is Element of the carrier of G
x |^ g is Element of the carrier of G
(power G) . (x,g) is set
1_ F is Element of the carrier of F
1_ (MultGroup F) is Element of the carrier of (MultGroup F)
NonZero F is non empty Element of K6( the carrier of F)
[#] F is non empty non proper Element of K6( the carrier of F)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{(0. F)} is non empty V2() finite 1 -element set
([#] F) \ {(0. F)} is Element of K6( the carrier of F)
x is Element of the carrier of F
eval (y,x) is Element of the carrier of F
gg is Element of the carrier of F
gg - (1. F) is Element of the carrier of F
x is set
x is Element of the carrier of G
gg is V11() V12() integer ext-real set
a |^ gg is Element of the carrier of G
x |^ g is Element of the carrier of G
(power G) . (x,g) is set
gg * g is V11() V12() integer ext-real set
a |^ (gg * g) is Element of the carrier of G
a |^ g is Element of the carrier of G
(power G) . (a,g) is set
(a |^ g) |^ gg is Element of the carrier of G
(1_ G) |^ gg is Element of the carrier of G
{f} is non empty V2() finite 1 -element Element of K6( the carrier of G)
the carrier of (gr {a}) \/ {f} is non empty set
x is non empty finite Group-like associative multMagma
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
card the carrier of (gr {a}) is non empty V4() V5() V6() cardinal set
card (Roots y) is V4() V5() V6() cardinal set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
gg is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
card ( the carrier of (gr {a}) \/ {f}) is non empty V4() V5() V6() cardinal set
x is finite set
x \/ {f} is non empty finite set
card (x \/ {f}) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
n + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
card (n + 1) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
card gg is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F is non empty non degenerated V53() left_add-cancelable right_add-cancelable right_complementable almost_left_invertible V147() V148() V149() unital associative commutative Euclidian V222() V223() V224() V225() V226() V227() V252() V253() V254() V255() domRing-like doubleLoopStr
MultGroup F is non empty strict Group-like associative commutative multMagma
G is non empty finite Group-like associative commutative Subgroup of MultGroup F
the carrier of G is non empty finite set
the Element of the carrier of G is Element of the carrier of G
card G is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
card the carrier of G is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
f is Element of the carrier of G
ord f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
f is Element of the carrier of G
ord 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 Element of NAT
g is Element of the carrier of G
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 G)
K6( the carrier of G) is finite V40() set
gr {g} is non empty finite strict Group-like associative commutative Subgroup of G
card (gr {g}) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of (gr {g}) is non empty finite set
card the carrier of (gr {g}) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
the carrier of G \ the carrier of (gr {g}) is finite Element of K6( the carrier of G)
x is set
x is Element of the carrier of G
ord x is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(ord x) lcm (ord g) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
j is V11() V12() integer ext-real set
(ord g) * j is V11() V12() integer ext-real set
((ord x) lcm (ord g)) / (ord g) is V11() V12() ext-real non negative set
m0 is V11() V12() integer ext-real set
(ord x) * m0 is V11() V12() integer ext-real set
x |^ (ord g) is Element of the carrier of G
power G is Relation-like Function-like V28(K7( the carrier of G,NAT)) V32(K7( the carrier of G,NAT), the carrier of G) Element of K6(K7(K7( the carrier of G,NAT), the carrier of G))
K7( the carrier of G,NAT) is V2() Relation-like non finite set
K7(K7( the carrier of G,NAT), the carrier of G) is V2() Relation-like non finite set
K6(K7(K7( the carrier of G,NAT), the carrier of G)) is V2() non finite set
(power G) . (x,(ord g)) is set
x |^ (ord x) is Element of the carrier of G
(power G) . (x,(ord x)) is set
(x |^ (ord x)) |^ m0 is Element of the carrier of G
1_ G is Element of the carrier of G
(1_ G) |^ m0 is Element of the carrier of G
{x} is non empty V2() finite 1 -element Element of K6( the carrier of G)
gr {x} is non empty finite strict Group-like associative commutative Subgroup of G
card (gr {x}) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of (gr {x}) is non empty finite set
card the carrier of (gr {x}) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
n0 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
m0 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
n0 * m0 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
n0 gcd m0 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(ord x) / m0 is V11() V12() ext-real non negative set
d2 is V11() V12() integer ext-real set
m0 * d2 is V11() V12() integer ext-real set
(ord g) / n0 is V11() V12() ext-real non negative set
d1 is V11() V12() integer ext-real set
n0 * d1 is V11() V12() integer ext-real set
d1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
g |^ d1 is Element of the carrier of G
power G is Relation-like Function-like V28(K7( the carrier of G,NAT)) V32(K7( the carrier of G,NAT), the carrier of G) Element of K6(K7(K7( the carrier of G,NAT), the carrier of G))
K7( the carrier of G,NAT) is V2() Relation-like non finite set
K7(K7( the carrier of G,NAT), the carrier of G) is V2() Relation-like non finite set
K6(K7(K7( the carrier of G,NAT), the carrier of G)) is V2() non finite set
(power G) . (g,d1) is set
d2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
x |^ d2 is Element of the carrier of G
(power G) . (x,d2) is set
(g |^ d1) * (x |^ d2) is Element of the carrier of G
d2 * m0 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
ord (x |^ d2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(ord g) * 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
d1 * n0 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
ord (g |^ d1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
ord ((g |^ d1) * (x |^ d2)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
m0 * n0 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
K7(NAT, the carrier of G) is V2() Relation-like non finite set
K6(K7(NAT, the carrier of G)) is V2() non finite set
f is non empty Relation-like Function-like V28( NAT ) V32( NAT , the carrier of G) Element of K6(K7(NAT, the carrier of G))
f . 0 is Element of the carrier of G
K6(K7(NAT,NAT)) is V2() non finite set
g is non empty Relation-like Function-like V28( NAT ) V32( NAT , NAT ) Element of K6(K7(NAT,NAT))
y is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
y + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
g . (y + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
f . (y + 1) is Element of the carrier of G
ord (f . (y + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
g . y is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
f . y is Element of the carrier of G
ord (f . y) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
y is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
y + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
g . y is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
x is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(y + 1) + x is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
g . ((y + 1) + x) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((y + 1) + x) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
g . (((y + 1) + x) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
x + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(y + 1) + (x + 1) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
g . ((y + 1) + (x + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(y + 1) + 0 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
g . ((y + 1) + 0) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
x is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(y + 1) + x is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
g . ((y + 1) + x) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
x is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
y is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
g . x is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
g . y is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
x - y is V11() V12() integer ext-real set
x is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
gg is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
gg + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
y + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(y + 1) + n is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
y is set
x is set
g . y is set
g . x is set
gg is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
x is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
dom g is non empty set
rng g is non empty set
card (dom g) is non empty V4() V5() V6() cardinal set
card (rng g) is non empty V4() V5() V6() cardinal set
card NAT is non empty V2() V4() V5() V6() non finite cardinal set
Segm (card G) is non empty V140() Element of K6(NAT)
y is set
x is set
g . x is set
x is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
g . x is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
f . x is Element of the carrier of G
ord (f . x) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
gg is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT