:: REAL_3 semantic presentation

REAL is non zero V45() V70() V71() V72() V76() set
NAT is non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non zero V45() V70() V76() set
omega is non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() set
K6(omega) is set
K6(NAT) is set
RAT is non zero V45() V70() V71() V72() V73() V76() set
INT is non zero V45() V70() V71() V72() V73() V74() V76() set
K7(COMPLEX,COMPLEX) is V35() set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V35() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is V35() V36() V37() set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is V35() V36() V37() set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is RAT -valued V35() V36() V37() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is RAT -valued V35() V36() V37() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is RAT -valued INT -valued V35() V36() V37() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is RAT -valued INT -valued V35() V36() V37() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is RAT -valued INT -valued V35() V36() V37() V38() set
K7(K7(NAT,NAT),NAT) is RAT -valued INT -valued V35() V36() V37() V38() set
K6(K7(K7(NAT,NAT),NAT)) is set
K322() is set
1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer rational V70() V71() V72() V73() V74() V75() V76() Element of NAT
0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer rational V70() V71() V72() V73() V74() V75() V76() set
K7(NAT,REAL) is V35() V36() V37() set
K6(K7(NAT,REAL)) is set
2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
tau is complex real ext-real set
5 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
sqrt 5 is complex real ext-real Element of REAL
1 + (sqrt 5) is complex real ext-real set
(1 + (sqrt 5)) / 2 is complex real ext-real Element of COMPLEX
2 " is non zero complex real ext-real positive non negative rational set
(1 + (sqrt 5)) * (2 ") is complex real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
g - 1 is complex real ext-real integer rational Element of REAL
- 1 is complex real ext-real non positive integer rational set
g + (- 1) is complex real ext-real integer rational set
1 - 1 is complex real ext-real integer rational Element of REAL
1 + (- 1) is complex real ext-real integer rational set
g is complex real ext-real set
r is complex real ext-real set
g / r is complex real ext-real Element of COMPLEX
r " is complex real ext-real set
g * (r ") is complex real ext-real set
s1 is complex real ext-real set
(g / r) - s1 is complex real ext-real set
- s1 is complex real ext-real set
(g / r) + (- s1) is complex real ext-real set
s is complex real ext-real set
r * s1 is complex real ext-real set
(r * s1) + s is complex real ext-real set
1 / ((g / r) - s1) is complex real ext-real Element of REAL
((g / r) - s1) " is complex real ext-real set
1 * (((g / r) - s1) ") is complex real ext-real set
r / s is complex real ext-real Element of COMPLEX
s " is complex real ext-real set
r * (s ") is complex real ext-real set
g - (r * s1) is complex real ext-real set
- (r * s1) is complex real ext-real set
g + (- (r * s1)) is complex real ext-real set
(g - (r * s1)) / r is complex real ext-real Element of COMPLEX
(g - (r * s1)) * (r ") is complex real ext-real set
r * ((g - (r * s1)) / r) is complex real ext-real set
(r * s1) / r is complex real ext-real Element of COMPLEX
(r * s1) * (r ") is complex real ext-real set
(g / r) - ((r * s1) / r) is complex real ext-real Element of COMPLEX
- ((r * s1) / r) is complex real ext-real set
(g / r) + (- ((r * s1) / r)) is complex real ext-real set
r * ((g / r) - ((r * s1) / r)) is complex real ext-real set
1 * s is complex real ext-real Element of REAL
r * ((g / r) - s1) is complex real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
g div 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
g / 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer rational V70() V71() V72() V73() V74() V75() V76() set
0 " is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer rational V70() V71() V72() V73() V74() V75() V76() set
g * (0 ") is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer rational V70() V71() V72() V73() V74() V75() V76() set
[\(g / 0)/] is complex real ext-real integer rational set
g mod 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
0 div g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
0 / g is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer rational V70() V71() V72() V73() V74() V75() V76() set
g " is complex real ext-real non negative rational set
0 * (g ") is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer rational V70() V71() V72() V73() V74() V75() V76() set
[\(0 / g)/] is complex real ext-real integer rational set
0 mod g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
g is complex set
g - g is set
- g is complex set
g + (- g) is set
g / 0 is complex Element of COMPLEX
g * (0 ") is set
[\0/] is complex real ext-real integer rational set
g is complex real ext-real set
1 / g is complex real ext-real Element of REAL
g " is complex real ext-real set
1 * (g ") is complex real ext-real set
1 * (g ") is complex real ext-real Element of REAL
g * (g ") is complex real ext-real set
g is complex real ext-real integer rational set
g + 1 is complex real ext-real integer rational Element of REAL
r is complex real ext-real set
[\r/] is complex real ext-real integer rational set
(g + 1) - 1 is complex real ext-real integer rational Element of REAL
(g + 1) + (- 1) is complex real ext-real integer rational set
r - 1 is complex real ext-real Element of REAL
r + (- 1) is complex real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
g / r is complex real ext-real non negative rational Element of COMPLEX
r " is complex real ext-real non negative rational set
g * (r ") is complex real ext-real non negative rational set
[\(g / r)/] is complex real ext-real integer rational set
g div r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
g / r is complex real ext-real non negative rational set
[\(g / r)/] is complex real ext-real integer rational set
g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
g mod r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
g / r is complex real ext-real non negative rational Element of COMPLEX
r " is complex real ext-real non negative rational set
g * (r ") is complex real ext-real non negative rational set
g div r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
g / r is complex real ext-real non negative rational set
[\(g / r)/] is complex real ext-real integer rational set
s1 is complex real ext-real integer rational set
s1 div r is complex real ext-real integer rational set
s1 / r is complex real ext-real rational set
s1 * (r ") is complex real ext-real rational set
[\(s1 / r)/] is complex real ext-real integer rational set
(s1 div r) * r is complex real ext-real integer rational set
s1 - ((s1 div r) * r) is complex real ext-real integer rational set
- ((s1 div r) * r) is complex real ext-real integer rational set
s1 + (- ((s1 div r) * r)) is complex real ext-real integer rational set
g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
g / r is complex real ext-real non negative rational Element of COMPLEX
r " is complex real ext-real non negative rational set
g * (r ") is complex real ext-real non negative rational set
g div r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
g / r is complex real ext-real non negative rational set
[\(g / r)/] is complex real ext-real integer rational set
g mod r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
g + 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r * (g / r) is complex real ext-real non negative rational set
(r * (g / r)) + (g mod r) is complex real ext-real non negative rational set
(g mod r) - 0 is complex real ext-real non negative integer rational Element of REAL
- 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer rational V70() V71() V72() V73() V74() V75() V76() set
(g mod r) + (- 0) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
g - (r * (g / r)) is complex real ext-real rational set
- (r * (g / r)) is complex real ext-real non positive rational set
g + (- (r * (g / r))) is complex real ext-real rational set
g - g is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer rational V70() V71() V72() V73() V74() V75() V76() set
- g is complex real ext-real non positive integer rational set
g + (- g) is complex real ext-real integer rational set
g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
g / r is complex real ext-real non negative rational Element of COMPLEX
r " is complex real ext-real non negative rational set
g * (r ") is complex real ext-real non negative rational set
frac (g / r) is complex real ext-real Element of REAL
[\(g / r)/] is complex real ext-real integer rational set
(g / r) - [\(g / r)/] is complex real ext-real rational set
- [\(g / r)/] is complex real ext-real integer rational set
(g / r) + (- [\(g / r)/]) is complex real ext-real rational set
g mod r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g mod r) / r is complex real ext-real non negative rational Element of COMPLEX
(g mod r) * (r ") is complex real ext-real non negative rational set
frac 0 is complex real ext-real Element of REAL
0 - [\0/] is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer rational V70() V71() V72() V73() V74() V75() V76() set
- [\0/] is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer rational V70() V71() V72() V73() V74() V75() V76() set
0 + (- [\0/]) is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer rational V70() V71() V72() V73() V74() V75() V76() set
g div r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
g / r is complex real ext-real non negative rational set
[\(g / r)/] is complex real ext-real integer rational set
r * (g div r) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(r * (g div r)) + (g mod r) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g / r) + 0 is complex real ext-real non negative rational Element of REAL
(g div r) + ((g mod r) / r) is complex real ext-real non negative rational set
g is complex real ext-real rational set
s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r is complex real ext-real integer rational set
r / s1 is complex real ext-real rational Element of REAL
s1 " is complex real ext-real non negative rational set
r * (s1 ") is complex real ext-real rational set
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
s / s1 is complex real ext-real non negative rational Element of COMPLEX
s * (s1 ") is complex real ext-real non negative rational set
NAT --> 1 is non zero T-Sequence-like Relation-like NAT -defined NAT -valued RAT -valued INT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
K6(K7(NAT,NAT)) is set
dom (NAT --> 1) is epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() Element of K6(NAT)
r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(NAT --> 1) . r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r is non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
g is Relation-like Function-like set
dom g is set
r is set
g . r is set
r is set
rng g is set
s1 is set
g . s1 is set
r is set
g . r is set
K7(NAT,INT) is RAT -valued INT -valued V35() V36() V37() set
K6(K7(NAT,INT)) is set
g is Relation-like Function-like set
r is non zero Relation-like NAT -defined INT -valued Function-like V26( NAT ) V30( NAT , INT ) V35() V36() V37() Element of K6(K7(NAT,INT))
dom r is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
s1 is set
r . s1 is complex real ext-real integer rational Element of REAL
dom g is set
rng g is set
K6(K7(NAT,NAT)) is set
g is Relation-like Function-like set
dom g is set
r is set
g . r is set
rng g is set
r is set
s1 is set
g . s1 is set
g is Relation-like Function-like set
r is Relation-like Function-like set
g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
g mod r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r mod (g mod r) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
s3 is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
s3 . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
s3 . 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
n . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n . 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
n + 2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n . (n + 2) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n . n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(n . n) mod (n . (n + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
s3 is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
s3 . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
s3 . 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
n . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n . 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n1 is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
n1 . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n1 . 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n2 + 2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n1 . (n2 + 2) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n1 . n2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n2 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n1 . (n2 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(n1 . n2) mod (n1 . (n2 + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
n2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n2 + 2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n . (n2 + 2) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n . n2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n2 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n . (n2 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(n . n2) mod (n . (n2 + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n . 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
g div r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
g / r is complex real ext-real non negative rational set
r " is complex real ext-real non negative rational set
g * (r ") is complex real ext-real non negative rational set
[\(g / r)/] is complex real ext-real integer rational set
g mod r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r div (g mod r) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r / (g mod r) is complex real ext-real non negative rational set
(g mod r) " is complex real ext-real non negative rational set
r * ((g mod r) ") is complex real ext-real non negative rational set
[\(r / (g mod r))/] is complex real ext-real integer rational set
(g,r) is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
s3 is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
s3 . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
s3 . 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
n . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n . 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
n + 2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n . (n + 2) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((g,r) . n) div ((g,r) . (n + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((g,r) . n) / ((g,r) . (n + 1)) is complex real ext-real non negative rational set
((g,r) . (n + 1)) " is complex real ext-real non negative rational set
((g,r) . n) * (((g,r) . (n + 1)) ") is complex real ext-real non negative rational set
[\(((g,r) . n) / ((g,r) . (n + 1)))/] is complex real ext-real integer rational set
s3 is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
s3 . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
s3 . 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
n . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n . 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n1 is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
n1 . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n1 . 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n2 + 2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n1 . (n2 + 2) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . n2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
n2 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (n2 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((g,r) . n2) div ((g,r) . (n2 + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((g,r) . n2) / ((g,r) . (n2 + 1)) is complex real ext-real non negative rational set
((g,r) . (n2 + 1)) " is complex real ext-real non negative rational set
((g,r) . n2) * (((g,r) . (n2 + 1)) ") is complex real ext-real non negative rational set
[\(((g,r) . n2) / ((g,r) . (n2 + 1)))/] is complex real ext-real integer rational set
n is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
n2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n2 + 2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n . (n2 + 2) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . n2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
n2 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (n2 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((g,r) . n2) div ((g,r) . (n2 + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((g,r) . n2) / ((g,r) . (n2 + 1)) is complex real ext-real non negative rational set
((g,r) . (n2 + 1)) " is complex real ext-real non negative rational set
((g,r) . n2) * (((g,r) . (n2 + 1)) ") is complex real ext-real non negative rational set
[\(((g,r) . n2) / ((g,r) . (n2 + 1)))/] is complex real ext-real integer rational set
n . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n . 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
(g,r) is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
(g,r) . 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
(g,r) . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r div ((g,r) . 0) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r / ((g,r) . 0) is complex real ext-real non negative rational set
((g,r) . 0) " is complex real ext-real non negative rational set
r * (((g,r) . 0) ") is complex real ext-real non negative rational set
[\(r / ((g,r) . 0))/] is complex real ext-real integer rational set
g mod r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r div (g mod r) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r / (g mod r) is complex real ext-real non negative rational set
(g mod r) " is complex real ext-real non negative rational set
r * ((g mod r) ") is complex real ext-real non negative rational set
[\(r / (g mod r))/] is complex real ext-real integer rational set
g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
(g,r) is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
(g,r) . 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r mod ((g,r) . 0) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
g mod r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r mod (g mod r) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
(s1,s) is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
(s1,s) . g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
(s1,s) . r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
(s1,s) . n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
(s1,s) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
s mod ((s1,s) . 0) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
2 + 0 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . (0 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((s1,s) . 0) mod ((s1,s) . (0 + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n - 1 is complex real ext-real integer rational Element of REAL
n + (- 1) is complex real ext-real integer rational set
(s1,s) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
n + 2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . (n + 2) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((s1,s) . n) mod ((s1,s) . (n + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
n + 2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . (n + 2) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((s1,s) . n) mod ((s1,s) . (n + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
(g,r) is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
(g,r) . s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
s1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (s1 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (0 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
g mod r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r mod (g mod r) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
0 + 2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (0 + 2) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (0 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((g,r) . 0) mod ((g,r) . (0 + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
s1 - 1 is complex real ext-real integer rational Element of REAL
s1 + (- 1) is complex real ext-real integer rational set
s3 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
s3 + (1 + 1) is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (s3 + (1 + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . s3 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
s3 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (s3 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((g,r) . s3) mod ((g,r) . (s3 + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
(s1,s) is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
(s1,s) . g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
(s1,s) . r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
(s1,s) . n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
(s1,s) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
(g,r) is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
(g,r) is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
s1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (s1 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
(n + 1) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . ((n + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
(g,r) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(n + 1) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . ((n + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n + (1 + 1) is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (n + (1 + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((g,r) . n) div ((g,r) . (n + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((g,r) . n) / ((g,r) . (n + 1)) is complex real ext-real non negative rational set
((g,r) . (n + 1)) " is complex real ext-real non negative rational set
((g,r) . n) * (((g,r) . (n + 1)) ") is complex real ext-real non negative rational set
[\(((g,r) . n) / ((g,r) . (n + 1)))/] is complex real ext-real integer rational set
((g,r) . (n + 1)) * (((g,r) . n) div ((g,r) . (n + 1))) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((g,r) . n) mod ((g,r) . (n + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(((g,r) . (n + 1)) * (((g,r) . n) div ((g,r) . (n + 1)))) + (((g,r) . n) mod ((g,r) . (n + 1))) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n + 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (0 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
g mod r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (0 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r div ((g,r) . 0) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r / ((g,r) . 0) is complex real ext-real non negative rational set
((g,r) . 0) " is complex real ext-real non negative rational set
r * (((g,r) . 0) ") is complex real ext-real non negative rational set
[\(r / ((g,r) . 0))/] is complex real ext-real integer rational set
r div (g mod r) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r / (g mod r) is complex real ext-real non negative rational set
(g mod r) " is complex real ext-real non negative rational set
r * ((g mod r) ") is complex real ext-real non negative rational set
[\(r / (g mod r))/] is complex real ext-real integer rational set
(g mod r) * (r div (g mod r)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r mod (g mod r) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((g mod r) * (r div (g mod r))) + (r mod (g mod r)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
(g,r) is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
(g,r) is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
(g,r) . s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
s1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (s1 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
(g,r) . n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
(n + 1) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . ((n + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(n + 1) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . ((n + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n + (1 + 1) is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (n + (1 + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((g,r) . n) div ((g,r) . (n + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((g,r) . n) / ((g,r) . (n + 1)) is complex real ext-real non negative rational set
((g,r) . (n + 1)) " is complex real ext-real non negative rational set
((g,r) . n) * (((g,r) . (n + 1)) ") is complex real ext-real non negative rational set
[\(((g,r) . n) / ((g,r) . (n + 1)))/] is complex real ext-real integer rational set
(g,r) . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (0 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(g,r) . (0 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r div ((g,r) . 0) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
r / ((g,r) . 0) is complex real ext-real non negative rational set
((g,r) . 0) " is complex real ext-real non negative rational set
r * (((g,r) . 0) ") is complex real ext-real non negative rational set
[\(r / ((g,r) . 0))/] is complex real ext-real integer rational set
g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
(s1,s) is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
(s1,s) . g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
(s1,s) . r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
(s1,s) is non zero Relation-like NAT -defined NAT -valued Function-like V26( NAT ) V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
(s1,s) . n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
(s1,s) . n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
(s1,s) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . (0 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
2 + 0 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . (0 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((s1,s) . 0) div ((s1,s) . (0 + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((s1,s) . 0) / ((s1,s) . (0 + 1)) is complex real ext-real non negative rational set
((s1,s) . (0 + 1)) " is complex real ext-real non negative rational set
((s1,s) . 0) * (((s1,s) . (0 + 1)) ") is complex real ext-real non negative rational set
[\(((s1,s) . 0) / ((s1,s) . (0 + 1)))/] is complex real ext-real integer rational set
(s1,s) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
((s1,s) . 0) mod ((s1,s) . (0 + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n - 1 is complex real ext-real integer rational Element of REAL
n + (- 1) is complex real ext-real integer rational set
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set
n1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational Element of REAL
(s1,s) . (n + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
n1 + 2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . (n1 + 2) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() Element of NAT
(s1,s) . (n1 + 1) is epsilon-transitive epsilon-connected ordinal natural