:: QUATERNI semantic presentation

REAL is non empty V45() V46() V47() V51() V52() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() Element of bool REAL
bool REAL is non empty set
omega is non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() set
RAT+ is set
{} is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set
RAT is non empty V45() V46() V47() V48() V51() V52() set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
{ [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of omega : verum } is set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of omega : verum } is Element of bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) }
bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is non empty set
( { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of omega : verum } ) \/ omega is non empty set
bool RAT+ is non empty set
bool (bool RAT+) is non empty set
DEDEKIND_CUTS is Element of bool (bool RAT+)
REAL+ is set
COMPLEX is non empty V45() V51() V52() set
INT is non empty V45() V46() V47() V48() V49() V51() V52() set
{{}} is non empty V45() V46() V47() V48() V49() V50() set
[:{{}},REAL+:] is Relation-like set
REAL+ \/ [:{{}},REAL+:] is set
[{},{}] is set
{{},{}} is non empty V45() V46() V47() V48() V49() V50() set
{{{},{}},{{}}} is non empty set
{[{},{}]} is Relation-like non empty set
(REAL+ \/ [:{{}},REAL+:]) \ {[{},{}]} is Element of bool (REAL+ \/ [:{{}},REAL+:])
bool (REAL+ \/ [:{{}},REAL+:]) is non empty set
{{},1} is non empty V45() V46() V47() V48() V49() V50() set
Funcs ({{},1},REAL) is functional non empty FUNCTION_DOMAIN of {{},1}, REAL
{ b₁ where b₁ is Relation-like {{},1} -defined REAL -valued Function-like V14({{},1}) quasi_total V33() V34() V35() Element of Funcs ({{},1},REAL) : b₁ . 1 = {} } is set
(Funcs ({{},1},REAL)) \ { b₁ where b₁ is Relation-like {{},1} -defined REAL -valued Function-like V14({{},1}) quasi_total V33() V34() V35() Element of Funcs ({{},1},REAL) : b₁ . 1 = {} } is Element of bool (Funcs ({{},1},REAL))
bool (Funcs ({{},1},REAL)) is non empty set
((Funcs ({{},1},REAL)) \ { b₁ where b₁ is Relation-like {{},1} -defined REAL -valued Function-like V14({{},1}) quasi_total V33() V34() V35() Element of Funcs ({{},1},REAL) : b₁ . 1 = {} } ) \/ REAL is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
[:2,REAL:] is Relation-like non empty V33() V34() V35() set
bool [:2,REAL:] is non empty set
0 is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V43() V44() V45() V46() V47() V48() V49() V50() V51() Element of NAT
{0,1} is non empty V45() V46() V47() V48() V49() V50() set
{ b₁ where b₁ is Element of bool RAT+ : for b₂ being Element of RAT+ holds
( not b₂ in b₁ or ( ( for b₃ being Element of RAT+ holds
( not b₃ <=' b₂ or b₃ in b₁ ) ) & ex b₃ being Element of RAT+ st
( b₃ in b₁ & not b₃ <=' b₂ ) ) ) } is set
{RAT+} is non empty set
{ b₁ where b₁ is Element of bool RAT+ : for b₂ being Element of RAT+ holds
( not b₂ in b₁ or ( ( for b₃ being Element of RAT+ holds
( not b₃ <=' b₂ or b₃ in b₁ ) ) & ex b₃ being Element of RAT+ st
( b₃ in b₁ & not b₃ <=' b₂ ) ) ) } \ {RAT+} is Element of bool { b₁ where b₁ is Element of bool RAT+ : for b₂ being Element of RAT+ holds
( not b₂ in b₁ or ( ( for b₃ being Element of RAT+ holds
( not b₃ <=' b₂ or b₃ in b₁ ) ) & ex b₃ being Element of RAT+ st
( b₃ in b₁ & not b₃ <=' b₂ ) ) ) }
bool { b₁ where b₁ is Element of bool RAT+ : for b₂ being Element of RAT+ holds
( not b₂ in b₁ or ( ( for b₃ being Element of RAT+ holds
( not b₃ <=' b₂ or b₃ in b₁ ) ) & ex b₃ being Element of RAT+ st
( b₃ in b₁ & not b₃ <=' b₂ ) ) ) } is non empty set
RAT+ \/ DEDEKIND_CUTS is set
{} is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of RAT+
{ { b₂ where b₂ is Element of RAT+ : not b₁ <=' b₂ } where b₁ is Element of RAT+ : not b₁ = {} } is set
(RAT+ \/ DEDEKIND_CUTS) \ { { b₂ where b₂ is Element of RAT+ : not b₁ <=' b₂ } where b₁ is Element of RAT+ : not b₁ = {} } is Element of bool (RAT+ \/ DEDEKIND_CUTS)
bool (RAT+ \/ DEDEKIND_CUTS) is non empty set
sqrt 0 is complex real ext-real Element of REAL
sqrt 1 is complex real ext-real Element of REAL
4 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
{{},1,2,3} is non empty set
Funcs (4,REAL) is functional non empty FUNCTION_DOMAIN of 4, REAL
{ b₁ where b₁ is Relation-like 4 -defined REAL -valued Function-like V14(4) quasi_total V33() V34() V35() Element of Funcs (4,REAL) : ( b₁ . 2 = 0 & b₁ . 3 = 0 ) } is set
(Funcs (4,REAL)) \ { b₁ where b₁ is Relation-like 4 -defined REAL -valued Function-like V14(4) quasi_total V33() V34() V35() Element of Funcs (4,REAL) : ( b₁ . 2 = 0 & b₁ . 3 = 0 ) } is Element of bool (Funcs (4,REAL))
bool (Funcs (4,REAL)) is non empty set
((Funcs (4,REAL)) \ { b₁ where b₁ is Relation-like 4 -defined REAL -valued Function-like V14(4) quasi_total V33() V34() V35() Element of Funcs (4,REAL) : ( b₁ . 2 = 0 & b₁ . 3 = 0 ) } ) \/ COMPLEX is non empty set
() is set
z is set
z2 is set
m3 is set
m4 is set
(z,z2) --> (m3,m4) is Relation-like Function-like set
m1 is set
m2 is set
n1 is set
n2 is set
(m1,m2) --> (n1,n2) is Relation-like Function-like set
((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set
z is set
z2 is set
m1 is set
m2 is set
m3 is set
m4 is set
n1 is set
n2 is set
(z,z2,m1,m2,m3,m4,n1,n2) is set
(z,z2) --> (m3,m4) is Relation-like Function-like set
(m1,m2) --> (n1,n2) is Relation-like Function-like set
((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set
z is set
z2 is set
m1 is set
m2 is set
{z,z2,m1,m2} is non empty set
m3 is set
m4 is set
n1 is set
n2 is set
(z,z2,m1,m2,m3,m4,n1,n2) is Relation-like Function-like set
(z,z2) --> (m3,m4) is Relation-like Function-like set
(m1,m2) --> (n1,n2) is Relation-like Function-like set
((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set
dom (z,z2,m1,m2,m3,m4,n1,n2) is set
dom ((z,z2) --> (m3,m4)) is set
{z,z2} is non empty set
dom ((m1,m2) --> (n1,n2)) is set
{m1,m2} is non empty set
(dom ((z,z2) --> (m3,m4))) \/ (dom ((m1,m2) --> (n1,n2))) is set
z is set
z2 is set
m1 is set
m2 is set
m3 is set
m4 is set
n1 is set
n2 is set
(z,z2,m1,m2,m3,m4,n1,n2) is Relation-like Function-like set
(z,z2) --> (m3,m4) is Relation-like Function-like set
(m1,m2) --> (n1,n2) is Relation-like Function-like set
((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set
rng (z,z2,m1,m2,m3,m4,n1,n2) is set
{m3,m4,n1,n2} is non empty set
rng ((z,z2) --> (m3,m4)) is set
{m3,m4} is non empty set
rng ((m1,m2) --> (n1,n2)) is set
{n1,n2} is non empty set
(rng ((z,z2) --> (m3,m4))) \/ (rng ((m1,m2) --> (n1,n2))) is set
{m3,m4} \/ {n1,n2} is non empty set
rng (((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2))) is set
z is set
z2 is set
m1 is set
m2 is set
m3 is set
m4 is set
n1 is set
n2 is set
(z,z2,m1,m2,m3,m4,n1,n2) is Relation-like Function-like set
(z,z2) --> (m3,m4) is Relation-like Function-like set
(m1,m2) --> (n1,n2) is Relation-like Function-like set
((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set
(z,z2,m1,m2,m3,m4,n1,n2) . z is set
(z,z2,m1,m2,m3,m4,n1,n2) . z2 is set
(z,z2,m1,m2,m3,m4,n1,n2) . m1 is set
(z,z2,m1,m2,m3,m4,n1,n2) . m2 is set
((z,z2) --> (m3,m4)) . z is set
((z,z2) --> (m3,m4)) . z2 is set
((m1,m2) --> (n1,n2)) . m1 is set
((m1,m2) --> (n1,n2)) . m2 is set
dom ((m1,m2) --> (n1,n2)) is set
{m1,m2} is non empty set
z is set
z2 is set
m1 is set
m2 is set
m3 is set
m4 is set
n1 is set
n2 is set
{m3,m4,n1,n2} is non empty set
(z,z2,m1,m2,m3,m4,n1,n2) is Relation-like Function-like set
(z,z2) --> (m3,m4) is Relation-like Function-like set
(m1,m2) --> (n1,n2) is Relation-like Function-like set
((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set
rng (z,z2,m1,m2,m3,m4,n1,n2) is set
n4 is set
dom (z,z2,m1,m2,m3,m4,n1,n2) is set
{z,z2,m1,m2} is non empty set
(z,z2,m1,m2,m3,m4,n1,n2) . z is set
(z,z2,m1,m2,m3,m4,n1,n2) . z2 is set
(z,z2,m1,m2,m3,m4,n1,n2) . m1 is set
(z,z2,m1,m2,m3,m4,n1,n2) . m2 is set
z is set
z2 is set
m1 is set
m2 is set
m3 is set
m4 is set
n1 is set
n2 is set
(z,z2,m1,m2,m3,m4,n1,n2) is Relation-like Function-like set
(z,z2) --> (m3,m4) is Relation-like Function-like set
(m1,m2) --> (n1,n2) is Relation-like Function-like set
((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set
rng (z,z2,m1,m2,m3,m4,n1,n2) is set
{m3,m4,n1,n2} is non empty set
z is set
z2 is set
m1 is set
m2 is set
{z,z2,m1,m2} is non empty set
m3 is set
m4 is set
z is non empty set
z2 is set
m1 is set
m2 is set
m3 is set
m4 is Element of z
n1 is Element of z
n2 is Element of z
n3 is Element of z
(z2,m1,m2,m3,m4,n1,n2,n3) is Relation-like Function-like set
(z2,m1) --> (m4,n1) is Relation-like Function-like set
(m2,m3) --> (n2,n3) is Relation-like Function-like set
((z2,m1) --> (m4,n1)) +* ((m2,m3) --> (n2,n3)) is Relation-like Function-like set
{z2,m1,m2,m3} is non empty set
[:{z2,m1,m2,m3},z:] is Relation-like non empty set
bool [:{z2,m1,m2,m3},z:] is non empty set
(z2,m1) --> (m4,n1) is Relation-like {z2,m1} -defined z -valued Function-like non empty V14({z2,m1}) quasi_total Element of bool [:{z2,m1},z:]
{z2,m1} is non empty set
[:{z2,m1},z:] is Relation-like non empty set
bool [:{z2,m1},z:] is non empty set
(m2,m3) --> (n2,n3) is Relation-like {m2,m3} -defined z -valued Function-like non empty V14({m2,m3}) quasi_total Element of bool [:{m2,m3},z:]
{m2,m3} is non empty set
[:{m2,m3},z:] is Relation-like non empty set
bool [:{m2,m3},z:] is non empty set
rng (z2,m1,m2,m3,m4,n1,n2,n3) is set
rng ((z2,m1) --> (m4,n1)) is non empty Element of bool z
bool z is non empty set
rng ((m2,m3) --> (n2,n3)) is non empty Element of bool z
(rng ((z2,m1) --> (m4,n1))) \/ (rng ((m2,m3) --> (n2,n3))) is non empty Element of bool z
dom (z2,m1,m2,m3,m4,n1,n2,n3) is set
(NAT,0,1,2,3,0,0,1,0) is Relation-like {0,1,2,3} -defined NAT -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() V36() Element of bool [:{0,1,2,3},NAT:]
{0,1,2,3} is non empty set
[:{0,1,2,3},NAT:] is Relation-like RAT -valued INT -valued non empty V33() V34() V35() V36() set
bool [:{0,1,2,3},NAT:] is non empty set
(0,1) --> (0,0) is Relation-like NAT -defined Function-like set
(2,3) --> (1,0) is Relation-like NAT -defined Function-like set
((0,1) --> (0,0)) +* ((2,3) --> (1,0)) is Relation-like NAT -defined Function-like set
(NAT,0,1,2,3,0,0,0,1) is Relation-like {0,1,2,3} -defined NAT -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() V36() Element of bool [:{0,1,2,3},NAT:]
(2,3) --> (0,1) is Relation-like NAT -defined Function-like set
((0,1) --> (0,0)) +* ((2,3) --> (0,1)) is Relation-like NAT -defined Function-like set
() is set
() is set
<i> is set
(0,1) --> (0,1) is Relation-like NAT -defined {0,1} -defined REAL -valued Function-like non empty V14({0,1}) quasi_total V33() V34() V35() Element of bool [:{0,1},REAL:]
[:{0,1},REAL:] is Relation-like non empty V33() V34() V35() set
bool [:{0,1},REAL:] is non empty set
[*0,1*] is complex Element of COMPLEX
z2 is Relation-like 4 -defined REAL -valued Function-like V14(4) quasi_total V33() V34() V35() Element of Funcs (4,REAL)
z2 . 2 is complex real ext-real Element of REAL
z2 . 3 is complex real ext-real Element of REAL
z2 is complex real ext-real Element of REAL
m1 is complex real ext-real Element of REAL
m2 is complex real ext-real Element of REAL
m3 is complex real ext-real Element of REAL
(REAL,0,1,2,3,z2,m1,m2,m3) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]
[:{0,1,2,3},REAL:] is Relation-like non empty V33() V34() V35() set
bool [:{0,1,2,3},REAL:] is non empty set
(0,1) --> (z2,m1) is Relation-like NAT -defined Function-like set
(2,3) --> (m2,m3) is Relation-like NAT -defined Function-like set
((0,1) --> (z2,m1)) +* ((2,3) --> (m2,m3)) is Relation-like NAT -defined Function-like set
z2 is Relation-like 4 -defined REAL -valued Function-like V14(4) quasi_total V33() V34() V35() Element of Funcs (4,REAL)
z2 . 2 is complex real ext-real Element of REAL
z2 . 3 is complex real ext-real Element of REAL
z2 is complex real ext-real Element of REAL
m1 is complex real ext-real Element of REAL
m2 is complex real ext-real Element of REAL
m3 is complex real ext-real Element of REAL
(REAL,0,1,2,3,z2,m1,m2,m3) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]
[:{0,1,2,3},REAL:] is Relation-like non empty V33() V34() V35() set
bool [:{0,1,2,3},REAL:] is non empty set
(0,1) --> (z2,m1) is Relation-like NAT -defined Function-like set
(2,3) --> (m2,m3) is Relation-like NAT -defined Function-like set
((0,1) --> (z2,m1)) +* ((2,3) --> (m2,m3)) is Relation-like NAT -defined Function-like set
z is Element of ()
m1 is complex real ext-real set
m2 is complex real ext-real set
z is complex real ext-real set
z2 is complex real ext-real set
(0,1,2,3,z,z2,m1,m2) is Relation-like Function-like set
(0,1) --> (z,z2) is Relation-like NAT -defined Function-like set
(2,3) --> (m1,m2) is Relation-like NAT -defined Function-like set
((0,1) --> (z,z2)) +* ((2,3) --> (m1,m2)) is Relation-like NAT -defined Function-like set
m3 is complex real ext-real Element of REAL
m4 is complex real ext-real Element of REAL
[*m3,m4*] is complex Element of COMPLEX
n4 is () Element of ()
m3 is complex real ext-real Element of REAL
m4 is complex real ext-real Element of REAL
n1 is complex real ext-real Element of REAL
n2 is complex real ext-real Element of REAL
(REAL,0,1,2,3,m3,m4,n1,n2) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]
[:{0,1,2,3},REAL:] is Relation-like non empty V33() V34() V35() set
bool [:{0,1,2,3},REAL:] is non empty set
(0,1) --> (m3,m4) is Relation-like NAT -defined Function-like set
(2,3) --> (n1,n2) is Relation-like NAT -defined Function-like set
((0,1) --> (m3,m4)) +* ((2,3) --> (n1,n2)) is Relation-like NAT -defined Function-like set
n4 is Relation-like 4 -defined REAL -valued Function-like V14(4) quasi_total V33() V34() V35() Element of Funcs (4,REAL)
n4 . 2 is complex real ext-real Element of REAL
n4 . 3 is complex real ext-real Element of REAL
n4 is () Element of ()
n1 is complex real ext-real Element of REAL
n2 is complex real ext-real Element of REAL
m3 is () Element of ()
[*n1,n2*] is complex Element of COMPLEX
n3 is complex real ext-real Element of REAL
n4 is complex real ext-real Element of REAL
m4 is () Element of ()
[*n3,n4*] is complex Element of COMPLEX
b1 is () Element of ()
b2 is () Element of ()
z is complex real ext-real Element of REAL
z2 is complex real ext-real Element of REAL
(z,z2,0,0) is () Element of ()
[*z,z2*] is complex Element of COMPLEX
m1 is complex real ext-real Element of REAL
m2 is complex real ext-real Element of REAL
[*m1,m2*] is complex Element of COMPLEX
z is set
z2 is set
m1 is set
m2 is set
{z,z2,m1,m2} is non empty set
m3 is set
m4 is set
n1 is set
n2 is set
(z,z2,m1,m2,m3,m4,n1,n2) is Relation-like Function-like set
(z,z2) --> (m3,m4) is Relation-like Function-like set
(m1,m2) --> (n1,n2) is Relation-like Function-like set
((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set
n3 is Relation-like Function-like set
dom n3 is set
n3 . z is set
n3 . z2 is set
n3 . m1 is set
n3 . m2 is set
dom ((z,z2) --> (m3,m4)) is set
{z,z2} is non empty set
dom ((m1,m2) --> (n1,n2)) is set
{m1,m2} is non empty set
(dom ((z,z2) --> (m3,m4))) \/ (dom ((m1,m2) --> (n1,n2))) is set
b2 is set
n3 . b2 is set
((m1,m2) --> (n1,n2)) . b2 is set
((z,z2) --> (m3,m4)) . b2 is set
z is () set
z2 is complex real ext-real Element of REAL
m1 is complex real ext-real Element of REAL
[*z2,m1*] is complex Element of COMPLEX
(z2,m1,0,0) is () Element of ()
z2 is Relation-like Function-like set
dom z2 is set
rng z2 is set
z2 . 0 is set
z2 . 1 is set
z2 . 2 is set
z2 . 3 is set
m1 is complex real ext-real Element of REAL
m2 is complex real ext-real Element of REAL
m3 is complex real ext-real Element of REAL
m4 is complex real ext-real Element of REAL
(REAL,0,1,2,3,m1,m2,m3,m4) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]
[:{0,1,2,3},REAL:] is Relation-like non empty V33() V34() V35() set
bool [:{0,1,2,3},REAL:] is non empty set
(0,1) --> (m1,m2) is Relation-like NAT -defined Function-like set
(2,3) --> (m3,m4) is Relation-like NAT -defined Function-like set
((0,1) --> (m1,m2)) +* ((2,3) --> (m3,m4)) is Relation-like NAT -defined Function-like set
(m1,m2,m3,m4) is () Element of ()
(REAL,0,1,2,3,m1,m2,m3,m4) . 2 is complex real ext-real Element of REAL
(REAL,0,1,2,3,m1,m2,m3,m4) . 3 is complex real ext-real Element of REAL
z is set
z2 is set
m1 is set
m2 is set
m3 is set
[z,m3] is set
{z,m3} is non empty set
{z} is non empty set
{{z,m3},{z}} is non empty set
m4 is set
[z2,m4] is set
{z2,m4} is non empty set
{z2} is non empty set
{{z2,m4},{z2}} is non empty set
n1 is set
[m1,n1] is set
{m1,n1} is non empty set
{m1} is non empty set
{{m1,n1},{m1}} is non empty set
n2 is set
(z,z2,m1,m2,m3,m4,n1,n2) is Relation-like Function-like set
(z,z2) --> (m3,m4) is Relation-like Function-like set
(m1,m2) --> (n1,n2) is Relation-like Function-like set
((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set
[m2,n2] is set
{m2,n2} is non empty set
{m2} is non empty set
{{m2,n2},{m2}} is non empty set
{[z,m3],[z2,m4],[m1,n1],[m2,n2]} is non empty set
dom ((z,z2) --> (m3,m4)) is set
{z,z2} is non empty set
dom ((m1,m2) --> (n1,n2)) is set
{m1,m2} is non empty set
((z,z2) --> (m3,m4)) \/ ((m1,m2) --> (n1,n2)) is Relation-like set
{[z,m3],[z2,m4]} is Relation-like non empty set
{[z,m3],[z2,m4]} \/ ((m1,m2) --> (n1,n2)) is Relation-like non empty set
{[m1,n1],[m2,n2]} is Relation-like non empty set
{[z,m3],[z2,m4]} \/ {[m1,n1],[m2,n2]} is Relation-like non empty set
z is set
z2 is set
[z,z2] is set
{z,z2} is non empty set
{z} is non empty set
{{z,z2},{z}} is non empty set
m1 is set
{m1} is non empty set
z is Element of bool RAT+
z2 is Element of RAT+
m1 is Element of RAT+
m1 + m1 is Element of RAT+
m2 is Element of RAT+
m2 + m2 is Element of RAT+
m3 is Element of RAT+
m3 + m3 is Element of RAT+
z2 + {} is Element of RAT+
z2 + z2 is Element of RAT+
m1 + {} is Element of RAT+
m2 + {} is Element of RAT+
z is complex real ext-real Element of REAL
z2 is complex real ext-real Element of REAL
m1 is complex real ext-real Element of REAL
m2 is complex real ext-real Element of REAL
(REAL,0,1,2,3,z,z2,m1,m2) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]
[:{0,1,2,3},REAL:] is Relation-like non empty V33() V34() V35() set
bool [:{0,1,2,3},REAL:] is non empty set
(0,1) --> (z,z2) is Relation-like NAT -defined Function-like set
(2,3) --> (m1,m2) is Relation-like NAT -defined Function-like set
((0,1) --> (z,z2)) +* ((2,3) --> (m1,m2)) is Relation-like NAT -defined Function-like set
[0,z] is set
{0,z} is non empty V45() V46() V47() set
{0} is non empty V45() V46() V47() V48() V49() V50() set
{{0,z},{0}} is non empty set
[1,z2] is set
{1,z2} is non empty V45() V46() V47() set
{1} is non empty V45() V46() V47() V48() V49() V50() set
{{1,z2},{1}} is non empty set
[2,m1] is set
{2,m1} is non empty V45() V46() V47() set
{2} is non empty V45() V46() V47() V48() V49() V50() set
{{2,m1},{2}} is non empty set
[3,m2] is set
{3,m2} is non empty V45() V46() V47() set
{3} is non empty V45() V46() V47() V48() V49() V50() set
{{3,m2},{3}} is non empty set
{[0,z],[1,z2],[2,m1],[3,m2]} is non empty set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is set
m4 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
[m4,n1] is set
{m4,n1} is non empty V45() V46() V47() V48() V49() V50() set
{m4} is non empty V45() V46() V47() V48() V49() V50() set
{{m4,n1},{m4}} is non empty set
{{m4}} is non empty set
{ [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT : verum } is set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT : verum } is Element of bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT : ( b₁,b₂ are_relative_prime & not b₂ = {} ) }
bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is non empty set
n1 is set
[0,n1] is set
{0,n1} is non empty set
{{0,n1},{0}} is non empty set
n2 is set
[1,n2] is set
{1,n2} is non empty set
{{1,n2},{1}} is non empty set
n3 is set
[2,n3] is set
{2,n3} is non empty set
{{2,n3},{2}} is non empty set
n4 is set
[3,n4] is set
{3,n4} is non empty set
{{3,n4},{3}} is non empty set
{[0,n1],[1,n2],[2,n3],[3,n4]} is non empty set
b1 is Element of bool RAT+
b2 is Element of RAT+
b3 is Element of RAT+
b2 is Element of RAT+
b3 is Element of RAT+
b4 is Element of RAT+
a3 is Element of RAT+
a4 is Element of RAT+
{{}} is non empty V45() V46() V47() V48() V49() V50() set
[:{{}},REAL+:] is Relation-like set
n1 is set
n2 is set
[n1,n2] is set
{n1,n2} is non empty set
{n1} is non empty set
{{n1,n2},{n1}} is non empty set
{0,n2} is non empty set
{0,n2} is non empty set
z is complex real ext-real Element of REAL
z2 is complex real ext-real Element of REAL
m1 is complex real ext-real Element of REAL
m2 is complex real ext-real Element of REAL
(REAL,0,1,2,3,z,z2,m1,m2) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]
[:{0,1,2,3},REAL:] is Relation-like non empty V33() V34() V35() set
bool [:{0,1,2,3},REAL:] is non empty set
(0,1) --> (z,z2) is Relation-like NAT -defined Function-like set
(2,3) --> (m1,m2) is Relation-like NAT -defined Function-like set
((0,1) --> (z,z2)) +* ((2,3) --> (m1,m2)) is Relation-like NAT -defined Function-like set
Funcs ({0,1},REAL) is functional non empty FUNCTION_DOMAIN of {0,1}, REAL
dom (REAL,0,1,2,3,z,z2,m1,m2) is non empty Element of bool {0,1,2,3}
bool {0,1,2,3} is non empty set
{2,3} is non empty V45() V46() V47() V48() V49() V50() set
{0,1} \/ {2,3} is non empty V45() V46() V47() V48() V49() V50() set
{ b₁ where b₁ is Relation-like {0,1} -defined REAL -valued Function-like V14({0,1}) quasi_total V33() V34() V35() Element of Funcs ({0,1},REAL) : b₁ . 1 = 0 } is set
(Funcs ({0,1},REAL)) \ { b₁ where b₁ is Relation-like {0,1} -defined REAL -valued Function-like V14({0,1}) quasi_total V33() V34() V35() Element of Funcs ({0,1},REAL) : b₁ . 1 = 0 } is Element of bool (Funcs ({0,1},REAL))
bool (Funcs ({0,1},REAL)) is non empty set
z is set
z2 is set
m1 is set
m2 is set
m3 is set
m4 is set
n1 is set
n2 is set
(z,z2,m1,m2,m3,m4,n1,n2) is Relation-like Function-like set
(z,z2) --> (m3,m4) is Relation-like Function-like set
(m1,m2) --> (n1,n2) is Relation-like Function-like set
((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set
n3 is set
n4 is set
b1 is set
b2 is set
(z,z2,m1,m2,n3,n4,b1,b2) is Relation-like Function-like set
(z,z2) --> (n3,n4) is Relation-like Function-like set
(m1,m2) --> (b1,b2) is Relation-like Function-like set
((z,z2) --> (n3,n4)) +* ((m1,m2) --> (b1,b2)) is Relation-like Function-like set
(z,z2,m1,m2,m3,m4,n1,n2) . z is set
(z,z2,m1,m2,m3,m4,n1,n2) . z2 is set
(z,z2,m1,m2,m3,m4,n1,n2) . m1 is set
(z,z2,m1,m2,m3,m4,n1,n2) . m2 is set
z is complex real ext-real Element of REAL
z2 is complex real ext-real Element of REAL
m1 is complex real ext-real Element of REAL
m2 is complex real ext-real Element of REAL
(z,z2,m1,m2) is () Element of ()
m3 is complex real ext-real Element of REAL
m4 is complex real ext-real Element of REAL
n1 is complex real ext-real Element of REAL
n2 is complex real ext-real Element of REAL
(m3,m4,n1,n2) is () Element of ()
[*z,z2*] is complex Element of COMPLEX
(REAL,0,1,2,3,m3,m4,n1,n2) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]
[:{0,1,2,3},REAL:] is Relation-like non empty V33() V34() V35() set
bool [:{0,1,2,3},REAL:] is non empty set
(0,1) --> (m3,m4) is Relation-like NAT -defined Function-like set
(2,3) --> (n1,n2) is Relation-like NAT -defined Function-like set
((0,1) --> (m3,m4)) +* ((2,3) --> (n1,n2)) is Relation-like NAT -defined Function-like set
[*m3,m4*] is complex Element of COMPLEX
(REAL,0,1,2,3,z,z2,m1,m2) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]
[:{0,1,2,3},REAL:] is Relation-like non empty V33() V34() V35() set
bool [:{0,1,2,3},REAL:] is non empty set
(0,1) --> (z,z2) is Relation-like NAT -defined Function-like set
(2,3) --> (m1,m2) is Relation-like NAT -defined Function-like set
((0,1) --> (z,z2)) +* ((2,3) --> (m1,m2)) is Relation-like NAT -defined Function-like set
[*m3,m4*] is complex Element of COMPLEX
(REAL,0,1,2,3,m3,m4,n1,n2) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]
(0,1) --> (m3,m4) is Relation-like NAT -defined Function-like set
(2,3) --> (n1,n2) is Relation-like NAT -defined Function-like set
((0,1) --> (m3,m4)) +* ((2,3) --> (n1,n2)) is Relation-like NAT -defined Function-like set
z is () set
m1 is complex real ext-real Element of REAL
m2 is complex real ext-real Element of REAL
m3 is complex real ext-real Element of REAL
m4 is complex real ext-real Element of REAL
(m1,m2,m3,m4) is () Element of ()
z2 is () set
n1 is complex real ext-real Element of REAL
n2 is complex real ext-real Element of REAL
n3 is complex real ext-real Element of REAL
n4 is complex real ext-real Element of REAL
(n1,n2,n3,n4) is () Element of ()
m1 + n1 is complex real ext-real Element of REAL
m2 + n2 is complex real ext-real Element of REAL
m3 + n3 is complex real ext-real Element of REAL
m4 + n4 is complex real ext-real Element of REAL
((m1 + n1),(m2 + n2),(m3 + n3),(m4 + n4)) is () Element of ()
b1 is set
b2 is set
b3 is complex real ext-real Element of REAL
b4 is complex real ext-real Element of REAL
a3 is complex real ext-real Element of REAL
a4 is complex real ext-real Element of REAL
(b3,b4,a3,a4) is () Element of ()
a5 is complex real ext-real Element of REAL
a6 is complex real ext-real Element of REAL
a7 is complex real ext-real Element of REAL
a8 is complex real ext-real Element of REAL
(a5,a6,a7,a8) is () Element of ()
b3 + a5 is complex real ext-real Element of REAL
b4 + a6 is complex real ext-real Element of REAL
a3 + a7 is complex real ext-real Element of REAL
a4 + a8 is complex real ext-real Element of REAL
((b3 + a5),(b4 + a6),(a3 + a7),(a4 + a8)) is () Element of ()
a9 is complex real ext-real Element of REAL
a10 is complex real ext-real Element of REAL
a11 is complex real ext-real Element of REAL
a12 is complex real ext-real Element of REAL
(a9,a10,a11,a12) is () Element of ()
b1 is complex real ext-real Element of REAL
b2 is complex real ext-real Element of REAL
b3 is complex real ext-real Element of REAL
b4 is complex real ext-real Element of REAL
(b1,b2,b3,b4) is () Element of ()
a9 + b1 is complex real ext-real Element of REAL
a10 + b2 is complex real ext-real Element of REAL
a11 + b3 is complex real ext-real Element of REAL
a12 + b4 is complex real ext-real Element of REAL
((a9 + b1),(a10 + b2),(a11 + b3),(a12 + b4)) is () Element of ()
b2 is () set
b4 is complex real ext-real Element of REAL
a3 is complex real ext-real Element of REAL
a4 is complex real ext-real Element of REAL
a5 is complex real ext-real Element of REAL
(b4,a3,a4,a5) is () Element of ()
b3 is () set
a6 is complex real ext-real Element of REAL
a7 is complex real ext-real Element of REAL
a8 is complex real ext-real Element of REAL
a9 is complex real ext-real Element of REAL
(a6,a7,a8,a9) is () Element of ()
b1 is set
b4 + a6 is complex real ext-real Element of REAL
a3 + a7 is complex real ext-real Element of REAL
a4 + a8 is complex real ext-real Element of REAL
a5 + a9 is complex real ext-real Element of REAL
((b4 + a6),(a3 + a7),(a4 + a8),(a5 + a9)) is () Element of ()
(0,0,0,0) is () Element of ()
z is complex real ext-real Element of REAL
z2 is complex real ext-real Element of REAL
[*z,z2*] is complex Element of COMPLEX
z is () set
z2 is complex real ext-real Element of REAL
m1 is complex real ext-real Element of REAL
m2 is complex real ext-real Element of REAL
m3 is complex real ext-real Element of REAL
(z2,m1,m2,m3) is () Element of ()
- z2 is complex real ext-real Element of REAL
- m1 is complex real ext-real Element of REAL
- m2 is complex real ext-real Element of REAL
- m3 is complex real ext-real Element of REAL
((- z2),(- m1),(- m2),(- m3)) is () Element of ()
m4 is () set
(z,m4) is set
z2 + (- z2) is complex real ext-real Element of REAL
m1 + (- m1) is complex real ext-real Element of REAL
m2 + (- m2) is complex real ext-real Element of REAL
m3 + (- m3) is complex real ext-real Element of REAL
m4 is () set
(z,m4) is set
n1 is () set
(z,n1) is set
n2 is complex real ext-real Element of REAL
n3 is complex real ext-real Element of REAL
n4 is complex real ext-real Element of REAL
b1 is complex real ext-real Element of REAL
(n2,n3,n4,b1) is () Element of ()
b2 is complex real ext-real Element of REAL
b3 is complex real ext-real Element of REAL
b4 is complex real ext-real Element of REAL
a3 is complex real ext-real Element of REAL
(b2,b3,b4,a3) is () Element of ()
n2 + b2 is complex real ext-real Element of REAL
n3 + b3 is complex real ext-real Element of REAL
n4 + b4 is complex real ext-real Element of REAL
b1 + a3 is complex real ext-real Element of REAL
((n2 + b2),(n3 + b3),(n4 + b4),(b1 + a3)) is () Element of ()
a4 is complex real ext-real Element of REAL
a5 is complex real ext-real Element of REAL
a6 is complex real ext-real Element of REAL
a7 is complex real ext-real Element of REAL
(a4,a5,a6,a7) is () Element of ()
a8 is complex real ext-real Element of REAL
a9 is complex real ext-real Element of REAL
a10 is complex real ext-real Element of REAL
a11 is complex real ext-real Element of REAL
(a8,a9,a10,a11) is () Element of ()
a4 + a8 is complex real ext-real Element of REAL
a5 + a9 is complex real ext-real Element of REAL
a6 + a10 is complex real ext-real Element of REAL
a7 + a11 is complex real ext-real Element of REAL
((a4 + a8),(a5 + a9),(a6 + a10),(a7 + a11)) is () Element of ()
n2 + a8 is complex real ext-real Element of REAL
n3 + a9 is complex real ext-real Element of REAL
n4 + a10 is complex real ext-real Element of REAL
b1 + a11 is complex real ext-real Element of REAL
n1 is () set
m4 is () set
(n1,m4) is set
(m4,n1) is set
z is () set
z2 is () set
(z2) is () set
(z,(z2)) is set
z is () set
m1 is complex real ext-real Element of REAL
m2 is complex real ext-real Element of REAL
m3 is complex real ext-real Element of REAL
m4 is complex real ext-real Element of REAL
(m1,m2,m3,m4) is () Element of ()
z2 is () set
n1 is complex real ext-real Element of REAL
n2 is complex real ext-real Element of REAL
n3 is complex real ext-real Element of REAL
n4 is complex real ext-real Element of REAL
(n1,n2,n3,n4) is () Element of ()
m1 * n1 is complex real ext-real Element of REAL
m2 * n2 is complex real ext-real Element of REAL
(m1 * n1) - (m2 * n2) is complex real ext-real Element of REAL
- (m2 * n2) is complex real ext-real set
(m1 * n1) + (- (m2 * n2)) is complex real ext-real set
m3 * n3 is complex real ext-real Element of REAL
((m1 * n1) - (m2 * n2)) - (m3 * n3) is complex real ext-real Element of REAL
- (m3 * n3) is complex real ext-real set
((m1 * n1) - (m2 * n2)) + (- (m3 * n3)) is complex real ext-real set
m4 * n4 is complex real ext-real Element of REAL
(((m1 * n1) - (m2 * n2)) - (m3 * n3)) - (m4 * n4) is complex real ext-real Element of REAL
- (m4 * n4) is complex real ext-real set
(((m1 * n1) - (m2 * n2)) - (m3 * n3)) + (- (m4 * n4)) is complex real ext-real set
m1 * n2 is complex real ext-real Element of REAL
m2 * n1 is complex real ext-real Element of REAL
(m1 * n2) + (m2 * n1) is complex real ext-real Element of REAL
m3 * n4 is complex real ext-real Element of REAL
((m1 * n2) + (m2 * n1)) + (m3 * n4) is complex real ext-real Element of REAL
m4 * n3 is complex real ext-real Element of REAL
(((m1 * n2) + (m2 * n1)) + (m3 * n4)) - (m4 * n3) is complex real ext-real Element of REAL
- (m4 * n3) is complex real ext-real set
(((m1 * n2) + (m2 * n1)) + (m3 * n4)) + (- (m4 * n3)) is complex real ext-real set
m1 * n3 is complex real ext-real Element of REAL
n1 * m3 is complex real ext-real Element of REAL
(m1 * n3) + (n1 * m3) is complex real ext-real Element of REAL
n2 * m4 is complex real ext-real Element of REAL
((m1 * n3) + (n1 * m3)) + (n2 * m4) is complex real ext-real Element of REAL
n4 * m2 is complex real ext-real Element of REAL
(((m1 * n3) + (n1 * m3)) + (n2 * m4)) - (n4 * m2) is complex real ext-real Element of REAL
- (n4 * m2) is complex real ext-real set
(((m1 * n3) + (n1 * m3)) + (n2 * m4)) + (- (n4 * m2)) is complex real ext-real set
m1 * n4 is complex real ext-real Element of REAL
m4 * n1 is complex real ext-real Element of REAL
(m1 * n4) + (m4 * n1) is complex real ext-real Element of REAL
m2 * n3 is complex real ext-real Element of REAL
((m1 * n4) + (m4 * n1)) + (m2 * n3) is complex real ext-real Element of REAL
m3 * n2 is complex real ext-real Element of REAL
(((m1 * n4) + (m4 * n1)) + (m2 * n3)) - (m3 * n2) is complex real ext-real Element of REAL
- (m3 * n2) is complex real ext-real set
(((m1 * n4) + (m4 * n1)) + (m2 * n3)) + (- (m3 * n2)) is complex real ext-real set
(((((m1 * n1) - (m2 * n2)) - (m3 * n3)) - (m4 * n4)),((((m1 * n2) + (m2 * n1)) + (m3 * n4)) - (m4 * n3)),((((m1 * n3) + (n1 * m3)) + (n2 * m4)) - (n4 * m2)),((((m1 * n4) + (m4 * n1)) + (m2 * n3)) - (m3 * n2))) is () Element of ()
b1 is set
b2 is set
b3 is complex real ext-real Element of REAL
b4 is complex real ext-real Element of REAL
a3 is complex real ext-real Element of REAL
a4 is complex real ext-real Element of REAL
(b3,b4,a3,a4) is () Element of ()
a5 is complex real ext-real Element of REAL
a6 is complex real ext-real Element of REAL
a7 is complex real ext-real Element of REAL
a8 is complex real ext-real Element of REAL
(a5,a6,a7,a8) is () Element of ()
b3 * a5 is complex real ext-real Element of REAL
b4 * a6 is complex real ext-real Element of REAL
(b3 * a5) - (b4 * a6) is complex real ext-real Element of REAL
- (b4 * a6) is complex real ext-real set
(b3 * a5) + (- (b4 * a6)) is complex real ext-real set
a3 * a7 is complex real ext-real Element of REAL
((b3 * a5) - (b4 * a6)) - (a3 * a7) is complex real ext-real Element of REAL
- (a3 * a7) is complex real ext-real set
((b3 * a5) - (b4 * a6)) + (- (a3 * a7)) is complex real ext-real set
a4 * a8 is complex real ext-real Element of REAL
(((b3 * a5) - (b4 * a6)) - (a3 * a7)) - (a4 * a8) is complex real ext-real Element of REAL
- (a4 * a8) is complex real ext-real set
(((b3 * a5) - (b4 * a6)) - (a3 * a7)) + (- (a4 * a8)) is complex real ext-real set
b3 * a6 is complex real ext-real Element of REAL
b4 * a5 is complex real ext-real Element of REAL
(b3 * a6) + (b4 * a5) is complex real ext-real Element of REAL
a3 * a8 is complex real ext-real Element of REAL
((b3 * a6) + (b4 * a5)) + (a3 * a8) is complex real ext-real Element of REAL
a4 * a7 is complex real ext-real Element of REAL
(((b3 * a6) + (b4 * a5)) + (a3 * a8)) - (a4 * a7) is complex real ext-real Element of REAL
- (a4 * a7) is complex real ext-real set
(((b3 * a6) + (b4 * a5)) + (a3 * a8)) + (- (a4 * a7)) is complex real ext-real set
b3 * a7 is complex real ext-real Element of REAL
a5 * a3 is complex real ext-real Element of REAL
(b3 * a7) + (a5 * a3) is complex real ext-real Element of REAL
a6 * a4 is complex real ext-real Element of REAL
((b3 * a7) + (a5 * a3)) + (a6 * a4) is complex real ext-real Element of REAL
a8 * b4 is complex real ext-real Element of REAL
(((b3 * a7) + (a5 * a3)) + (a6 * a4)) - (a8 * b4) is complex real ext-real Element of REAL
- (a8 * b4) is complex real ext-real set
(((b3 * a7) + (a5 * a3)) + (a6 * a4)) + (- (a8 * b4)) is complex real ext-real set
b3 * a8 is complex real ext-real Element of REAL
a4 * a5 is complex real ext-real Element of REAL
(b3 * a8) + (a4 * a5) is complex real ext-real Element of REAL
b4 * a7 is complex real ext-real Element of REAL
((b3 * a8) + (a4 * a5)) + (b4 * a7) is complex real ext-real Element of REAL
a3 * a6 is complex real ext-real Element of REAL
(((b3 * a8) + (a4 * a5)) + (b4 * a7)) - (a3 * a6) is complex real ext-real Element of REAL
- (a3 * a6) is complex real ext-real set
(((b3 * a8) + (a4 * a5)) + (b4 * a7)) + (- (a3 * a6)) is complex real ext-real set
(((((b3 * a5) - (b4 * a6)) - (a3 * a7)) - (a4 * a8)),((((b3 * a6) + (b4 * a5)) + (a3 * a8)) - (a4 * a7)),((((b3 * a7) + (a5 * a3)) + (a6 * a4)) - (a8 * b4)),((((b3 * a8) + (a4 * a5)) + (b4 * a7)) - (a3 * a6))) is () Element of ()
a9 is complex real ext-real Element of REAL
a10 is complex real ext-real Element of REAL
a11 is complex real ext-real Element of REAL
a12 is complex real ext-real Element of REAL
(a9,a10,a11,a12) is () Element of ()
b1 is complex real ext-real Element of REAL
b2 is complex real ext-real Element of REAL
b3 is complex real ext-real Element of REAL
b4 is complex real ext-real Element of REAL
(b1,b2,b3,b4) is () Element of ()
a9 * b1 is complex real ext-real Element of REAL
a10 * b2 is complex real ext-real Element of REAL
(a9 * b1) - (a10 * b2) is complex real ext-real Element of REAL
- (a10 * b2) is complex real ext-real set
(a9 * b1) + (- (a10 * b2)) is complex real ext-real set
a11 * b3 is complex real ext-real Element of REAL
((a9 * b1) - (a10 * b2)) - (a11 * b3) is complex real ext-real Element of REAL
- (a11 * b3) is complex real ext-real set
((a9 * b1) - (a10 * b2)) + (- (a11 * b3)) is complex real ext-real set
a12 * b4 is complex real ext-real Element of REAL
(((a9 * b1) - (a10 * b2)) - (a11 * b3)) - (a12 * b4) is complex real ext-real Element of REAL
- (a12 * b4) is complex real ext-real set
(((a9 * b1) - (a10 * b2)) - (a11 * b3)) + (- (a12 * b4)) is complex real ext-real set
a9 * b2 is complex real ext-real Element of REAL
a10 * b1 is complex real ext-real Element of REAL
(a9 * b2) + (a10 * b1) is complex real ext-real Element of REAL
a11 * b4 is complex real ext-real Element of REAL
((a9 * b2) + (a10 * b1)) + (a11 * b4) is complex real ext-real Element of REAL
a12 * b3 is complex real ext-real Element of REAL
(((a9 * b2) + (a10 * b1)) + (a11 * b4)) - (a12 * b3) is complex real ext-real Element of REAL
- (a12 * b3) is complex real ext-real set
(((a9 * b2) + (a10 * b1)) + (a11 * b4)) + (- (a12 * b3)) is complex real ext-real set
a9 * b3 is complex real ext-real Element of REAL
b1 * a11 is complex real ext-real Element of REAL
(a9 * b3) + (b1 * a11) is complex real ext-real Element of REAL
b2 * a12 is complex real ext-real Element of REAL
((a9 * b3) + (b1 * a11)) + (b2 * a12) is complex real ext-real Element of REAL
b4 * a10 is complex real ext-real Element of REAL
(((a9 * b3) + (b1 * a11)) + (b2 * a12)) - (b4 * a10) is complex real ext-real Element of REAL
- (b4 * a10) is complex real ext-real set
(((a9 * b3) + (b1 * a11)) + (b2 * a12)) + (- (b4 * a10)) is complex real ext-real set
a9 * b4 is complex real ext-real Element of REAL
a12 * b1 is complex real ext-real Element of REAL
(a9 * b4) + (a12 * b1) is complex real ext-real Element of REAL
a10 * b3 is complex real ext-real Element of REAL
((a9 * b4) + (a12 * b1)) + (a10 * b3) is complex real ext-real Element of REAL
a11 * b2 is complex real ext-real Element of REAL
(((a9 * b4) + (a12 * b1)) + (a10 * b3)) - (a11 * b2) is complex real ext-real Element of REAL
- (a11 * b2) is complex real ext-real set
(((a9 * b4) + (a12 * b1)) + (a10 * b3)) + (- (a11 * b2)) is complex real ext-real set
(((((a9 * b1) - (a10 * b2)) - (a11 * b3)) - (a12 * b4)),((((a9 * b2) + (a10 * b1)) + (a11 * b4)) - (a12 * b3)),((((a9 * b3) + (b1 * a11)) + (b2 * a12)) - (b4 * a10)),((((a9 * b4) + (a12 * b1)) + (a10 * b3)) - (a11 * b2))) is () Element of ()
z is () set
z2 is () set
(z,z2) is set
m1 is complex real ext-real Element of REAL
m2 is complex real ext-real Element of REAL
m3 is complex real ext-real Element of REAL
m4 is complex real ext-real Element of REAL
(m1,m2,m3,m4) is () Element of ()
n1 is complex real ext-real Element of REAL
n2 is complex real ext-real Element of REAL
n3 is complex real ext-real Element of REAL
n4 is complex real ext-real Element of REAL
(n1,n2,n3,n4) is () Element of ()
m1 + n1 is complex real ext-real Element of REAL
m2 + n2 is complex real ext-real Element of REAL
m3 + n3 is complex real ext-real Element of REAL
m4 + n4 is complex real ext-real Element of REAL
((m1 + n1),(m2 + n2),(m3 + n3),(m4 + n4)) is () Element of ()
(z,z2) is set
m1 is complex real ext-real Element of REAL
m2 is complex real ext-real Element of REAL
m3 is complex real ext-real Element of REAL
m4 is complex real ext-real Element of REAL
(m1,m2,m3,m4) is () Element of ()
n1 is complex real ext-real Element of REAL
n2 is complex real ext-real Element of REAL
n3 is complex real ext-real Element of REAL
n4 is complex real ext-real Element of REAL
(n1,n2,n3,n4) is () Element of ()
m1 * n1 is complex real ext-real Element of REAL
m2 * n2 is complex real ext-real Element of REAL
(m1 * n1) - (m2 * n2) is complex real ext-real Element of REAL
- (m2 * n2) is complex real ext-real set
(m1 * n1) + (- (m2 * n2)) is complex real ext-real set
m3 * n3 is complex real ext-real Element of REAL
((m1 * n1) - (m2 * n2)) - (m3 * n3) is complex real ext-real Element of REAL
- (m3 * n3) is complex real ext-real set
((m1 * n1) - (m2 * n2)) + (- (m3 * n3)) is complex real ext-real set
m4 * n4 is complex real ext-real Element of REAL
(((m1 * n1) - (m2 * n2)) - (m3 * n3)) - (m4 * n4) is complex real ext-real Element of REAL
- (m4 * n4) is complex real ext-real set
(((m1 * n1) - (m2 * n2)) - (m3 * n3)) + (- (m4 * n4)) is complex real ext-real set
m1 * n2 is complex real ext-real Element of REAL
m2 * n1 is complex real ext-real Element of REAL
(m1 * n2) + (m2 * n1) is complex real ext-real Element of REAL
m3 * n4 is complex real ext-real Element of REAL
((m1 * n2) + (m2 * n1)) + (m3 * n4) is complex real ext-real Element of REAL
m4 * n3 is complex real ext-real Element of REAL
(((m1 * n2) + (m2 * n1)) + (m3 * n4)) - (m4 * n3) is complex real ext-real Element of REAL
- (m4 * n3) is complex real ext-real set
(((m1 * n2) + (m2 * n1)) + (m3 * n4)) + (- (m4 * n3)) is complex real ext-real set
m1 * n3 is complex real ext-real Element of REAL
n1 * m3 is complex real ext-real Element of REAL
(m1 * n3) + (n1 * m3) is complex real ext-real Element of REAL
n2 * m4 is complex real ext-real Element of REAL
((m1 * n3) + (n1 * m3)) + (n2 * m4) is complex real ext-real Element of REAL
n4 * m2 is complex real ext-real Element of REAL
(((m1 * n3) + (n1 * m3)) + (n2 * m4)) - (n4 * m2) is complex real ext-real Element of REAL
- (n4 * m2) is complex real ext-real set
(((m1 * n3) + (n1 * m3)) + (n2 * m4)) + (- (n4 * m2)) is complex real ext-real set
m1 * n4 is complex real ext-real Element of REAL
m4 * n1 is complex real ext-real Element of REAL
(m1 * n4) + (m4 * n1) is complex real ext-real Element of REAL
m2 * n3 is complex real ext-real Element of REAL
((m1 * n4) + (m4 * n1)) + (m2 * n3) is complex real ext-real Element of REAL
m3 * n2 is complex real ext-real Element of REAL
(((m1 * n4) + (m4 * n1)) + (m2 * n3)) - (m3 * n2) is complex real ext-real Element of REAL
- (m3 * n2) is complex real ext-real set
(((m1 * n4) + (m4 * n1)) + (m2 * n3)) + (- (m3 * n2)) is complex real ext-real set
(((((m1 * n1) - (m2 * n2)) - (m3 * n3)) - (m4 * n4)),((((m1 * n2) + (m2 * n1)) + (m3 * n4)) - (m4 * n3)),((((m1 * n3) + (n1 * m3)) + (n2 * m4)) - (n4 * m2)),((((m1 * n4) + (m4 * n1)) + (m2 * n3)) - (m3 * n2))) is () Element of ()
(0,0,1,0) is () Element of ()
z is () Element of ()
z2 is () Element of ()
(0,0,0,1) is () Element of ()
z is () Element of ()
z2 is () Element of ()
() is () Element of ()
() is () Element of ()
(<i>,<i>) is () set
- 1 is complex real ext-real non positive Element of REAL
(0,1,0,0) is () Element of ()
0 * 0 is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL
1 * 1 is complex real ext-real non negative Element of REAL
(0 * 0) - (1 * 1) is complex real ext-real non positive Element of REAL
- (1 * 1) is complex real ext-real non positive set
(0 * 0) + (- (1 * 1)) is complex real ext-real non positive set
((0 * 0) - (1 * 1)) - (0 * 0) is complex real ext-real non positive Element of REAL
- (0 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set
((0 * 0) - (1 * 1)) + (- (0 * 0)) is complex real ext-real non positive set
(((0 * 0) - (1 * 1)) - (0 * 0)) - (0 * 0) is complex real ext-real non positive Element of REAL
(((0 * 0) - (1 * 1)) - (0 * 0)) + (- (0 * 0)) is complex real ext-real non positive set
0 * 1 is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL
1 * 0 is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL
(0 * 1) + (1 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL
((0 * 1) + (1 * 0)) + (0 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL
(((0 * 1) + (1 * 0)) + (0 * 0)) - (0 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL
(((0 * 1) + (1 * 0)) + (0 * 0)) + (- (0 * 0)) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set
(0 * 0) + (0 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL
((0 * 0) + (0 * 0)) + (1 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL
(((0 * 0) + (0 * 0)) + (1 * 0)) - (0 * 1) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL
- (0 * 1) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set
(((0 * 0) + (0 * 0)) + (1 * 0)) + (- (0 * 1)) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set
(((((0 * 0) - (1 * 1)) - (0 * 0)) - (0 * 0)),((((0 * 1) + (1 * 0)) + (0 * 0)) - (0 * 0)),((((0 * 0) + (0 * 0)) + (1 * 0)) - (0 * 1)),((((0 * 0) + (0 * 0)) + (1 * 0)) - (0 * 1))) is () Element of ()
((- 1),0,0,0) is () Element of ()
[*(- 1),0*] is complex Element of COMPLEX
((),()) is () set
0 * 0 is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL
(0 * 0) - (0 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL
- (0 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set
(0 * 0) + (- (0 * 0)) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set
1 * 1 is complex real ext-real non negative Element of REAL
((0 * 0) - (0 * 0)) - (1 * 1) is complex real ext-real non positive Element of REAL
- (1 * 1) is complex real ext-real non positive set
((0 * 0) - (0 * 0)) + (- (1 * 1)) is complex real ext-real non positive set
(((0 * 0) - (0 * 0)) - (1 * 1)) - (0 * 0) is complex real ext-real non positive Element of REAL
(((0 * 0) - (0 * 0)) - (1 * 1)) + (- (0 * 0)) is complex real ext-real non positive set
(0 * 0) + (0 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL
((0 * 0) + (0 * 0)) + (0 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL
0 * 1 is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL
(((0 * 0) + (0 * 0)) + (0 * 0)) - (0 * 1) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL
- (0 * 1) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set
(((0 * 0) + (0 * 0)) + (0 * 0)) + (- (0 * 1)) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set
(0 * 1) + (0 * 1) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non