:: XCMPLX_1 semantic presentation
begin
theorem
:: XCMPLX_1:1
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
+
(
b
: ( (
complex
) (
complex
)
number
)
+
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:2
for
a
,
c
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:3
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
=
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) holds
b
: ( (
complex
) (
complex
)
number
)
=
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: XCMPLX_1:4
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
*
(
b
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:5
for
c
,
a
,
b
being ( (
complex
) (
complex
)
number
) st
c
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
a
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:6
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
( not
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) or
a
: ( (
complex
) (
complex
)
number
)
=
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) or
b
: ( (
complex
) (
complex
)
number
)
=
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) ) ;
theorem
:: XCMPLX_1:7
for
b
,
a
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: XCMPLX_1:8
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
*
(
b
: ( (
complex
) (
complex
)
number
)
+
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
(
a
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:9
for
a
,
b
,
c
,
d
being ( (
complex
) (
complex
)
number
) holds
(
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
a
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
(
b
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
(
c
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:10
for
a
,
b
,
c
,
d
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
c
: ( (
complex
) (
complex
)
number
)
+
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
(
(
a
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
(
a
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
(
b
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
(
b
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:11
for
a
being ( (
complex
) (
complex
)
number
) holds 2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
+
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:12
for
a
being ( (
complex
) (
complex
)
number
) holds 3 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
+
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:13
for
a
being ( (
complex
) (
complex
)
number
) holds 4 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
a
: ( (
complex
) (
complex
)
number
)
+
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:14
for
a
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
-
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: XCMPLX_1:15
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:16
for
b
,
a
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
-
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
=
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: XCMPLX_1:17
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
=
a
: ( (
complex
) (
complex
)
number
)
-
(
b
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:18
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
-
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:19
for
a
,
c
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:20
for
c
,
a
,
b
being ( (
complex
) (
complex
)
number
) st
c
: ( (
complex
) (
complex
)
number
)
-
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
c
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:21
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:22
for
a
,
c
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
(
c
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:23
for
c
,
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
c
: ( (
complex
) (
complex
)
number
)
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
(
c
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
-
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:24
for
a
,
b
,
c
,
d
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
c
: ( (
complex
) (
complex
)
number
)
-
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
-
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:25
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
=
a
: ( (
complex
) (
complex
)
number
)
+
(
b
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:26
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
=
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:27
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
=
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:28
for
a
,
c
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
(
c
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:29
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:30
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
c
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:31
for
a
,
c
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
(
b
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:32
for
a
,
c
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
(
c
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:33
for
a
,
b
,
c
,
d
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
c
: ( (
complex
) (
complex
)
number
)
+
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
d
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:34
for
a
,
c
,
d
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
d
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
c
: ( (
complex
) (
complex
)
number
)
+
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:35
for
a
,
b
,
c
,
d
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
c
: ( (
complex
) (
complex
)
number
)
-
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
+
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
c
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:36
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
-
(
b
: ( (
complex
) (
complex
)
number
)
+
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:37
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
-
(
b
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:38
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
-
(
b
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
+
(
c
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:39
for
a
,
c
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
(
b
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:40
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
*
(
b
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
(
a
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:41
for
a
,
b
,
c
,
d
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
c
: ( (
complex
) (
complex
)
number
)
-
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
b
: ( (
complex
) (
complex
)
number
)
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
d
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:42
for
a
,
b
,
c
,
d
being ( (
complex
) (
complex
)
number
) holds
(
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
a
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
(
b
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
-
(
c
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:43
for
a
,
b
,
c
,
d
being ( (
complex
) (
complex
)
number
) holds
(
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
a
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
(
b
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
-
(
c
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:44
for
a
,
b
,
c
,
d
being ( (
complex
) (
complex
)
number
) holds
(
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
a
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
(
b
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
(
c
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:45
for
a
,
b
,
c
,
d
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
c
: ( (
complex
) (
complex
)
number
)
-
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
(
(
a
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
(
a
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
(
b
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
-
(
b
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:46
for
a
,
b
,
c
,
d
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
c
: ( (
complex
) (
complex
)
number
)
+
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
(
(
a
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
(
a
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
-
(
b
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
-
(
b
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:47
for
a
,
b
,
e
,
d
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
e
: ( (
complex
) (
complex
)
number
)
-
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
(
(
a
: ( (
complex
) (
complex
)
number
)
*
e
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
(
a
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
-
(
b
: ( (
complex
) (
complex
)
number
)
*
e
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
(
b
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:48
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:49
for
a
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
/
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) : ( ( ) (
complex
)
set
)
=
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: XCMPLX_1:50
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: XCMPLX_1:51
for
b
,
a
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
=
a
: ( (
complex
) (
complex
)
number
)
/
(
b
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:52
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
/
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:53
for
c
,
a
,
b
being ( (
complex
) (
complex
)
number
) st
c
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
a
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:54
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
b
: ( (
complex
) (
complex
)
number
)
=
a
: ( (
complex
) (
complex
)
number
)
/
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:55
for
c
,
a
,
b
being ( (
complex
) (
complex
)
number
) st
c
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
(
b
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:56
for
a
being ( (
complex
) (
complex
)
number
) holds 1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:57
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds 1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
/
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:58
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:59
for
a
,
b
being ( (
complex
) (
complex
)
number
) st 1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:60
for
a
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
/
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: XCMPLX_1:61
for
b
,
a
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
b
: ( (
complex
) (
complex
)
number
)
/
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: XCMPLX_1:62
for
a
,
c
,
b
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
(
b
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:63
for
a
,
b
,
e
,
d
being ( (
complex
) (
complex
)
number
) holds
(
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
e
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
a
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
(
b
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
(
e
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:64
for
a
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
+
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:65
for
a
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
complex
)
set
)
+
(
a
: ( (
complex
) (
complex
)
number
)
/
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:66
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
=
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:67
for
a
being ( (
complex
) (
complex
)
number
) holds
(
(
a
: ( (
complex
) (
complex
)
number
)
+
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
3 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:68
for
a
being ( (
complex
) (
complex
)
number
) holds
(
(
a
: ( (
complex
) (
complex
)
number
)
/
3 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
complex
)
set
)
+
(
a
: ( (
complex
) (
complex
)
number
)
/
3 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
(
a
: ( (
complex
) (
complex
)
number
)
/
3 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:69
for
a
being ( (
complex
) (
complex
)
number
) holds
(
(
(
a
: ( (
complex
) (
complex
)
number
)
+
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
4 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:70
for
a
being ( (
complex
) (
complex
)
number
) holds
(
(
(
a
: ( (
complex
) (
complex
)
number
)
/
4 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
complex
)
set
)
+
(
a
: ( (
complex
) (
complex
)
number
)
/
4 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
(
a
: ( (
complex
) (
complex
)
number
)
/
4 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
(
a
: ( (
complex
) (
complex
)
number
)
/
4 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:71
for
a
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
4 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
complex
)
set
)
+
(
a
: ( (
complex
) (
complex
)
number
)
/
4 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
/
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:72
for
a
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
+
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
4 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
/
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:73
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:74
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
*
(
b
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:75
for
a
,
b
,
e
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
e
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
e
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:76
for
a
,
b
,
c
,
d
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
c
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
(
b
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:77
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
/
(
b
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:78
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
/
(
b
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:79
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
/
(
b
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
*
(
c
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:80
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
/
(
b
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
c
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:81
for
a
,
b
,
e
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
/
(
b
: ( (
complex
) (
complex
)
number
)
/
e
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
e
: ( (
complex
) (
complex
)
number
)
*
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:82
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
/
(
b
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:83
for
a
,
b
,
c
,
d
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
(
c
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
(
a
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:84
for
a
,
b
,
c
,
d
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
(
c
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
(
b
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:85
for
a
,
c
,
b
,
d
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
b
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
b
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:86
for
a
,
b
,
c
,
d
,
e
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
/
(
(
b
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
d
: ( (
complex
) (
complex
)
number
)
/
e
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
e
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
a
: ( (
complex
) (
complex
)
number
)
/
(
b
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:87
for
b
,
a
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:88
for
b
,
a
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
=
a
: ( (
complex
) (
complex
)
number
)
*
(
b
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:89
for
b
,
a
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
=
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:90
for
b
,
a
,
c
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
c
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:91
for
c
,
a
,
b
being ( (
complex
) (
complex
)
number
) st
c
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
(
b
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:92
for
c
,
a
,
b
being ( (
complex
) (
complex
)
number
) st
c
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
/
(
b
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
*
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:93
for
b
,
a
,
c
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
(
b
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:94
for
c
,
d
,
a
,
b
being ( (
complex
) (
complex
)
number
) st
c
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
d
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
a
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:95
for
c
,
d
,
a
,
b
being ( (
complex
) (
complex
)
number
) st
c
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
d
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
a
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:96
for
c
,
d
,
a
,
b
being ( (
complex
) (
complex
)
number
) st
c
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
d
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
a
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:97
for
c
,
a
,
b
being ( (
complex
) (
complex
)
number
) st
c
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
c
: ( (
complex
) (
complex
)
number
)
*
(
(
a
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:98
for
c
,
a
,
b
being ( (
complex
) (
complex
)
number
) st
c
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
c
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:99
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
*
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:100
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
/
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:101
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:102
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:103
for
c
,
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
/
(
b
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:104
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
a
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:105
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:106
for
a
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
*
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: XCMPLX_1:107
for
b
,
a
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
=
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:108
for
b
,
a
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
=
a
: ( (
complex
) (
complex
)
number
)
*
(
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:109
for
b
,
a
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
=
(
a
: ( (
complex
) (
complex
)
number
)
*
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
*
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:110
for
b
,
a
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
=
a
: ( (
complex
) (
complex
)
number
)
/
(
b
: ( (
complex
) (
complex
)
number
)
*
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:111
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: XCMPLX_1:112
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
b
: ( (
complex
) (
complex
)
number
)
/
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: XCMPLX_1:113
for
b
,
a
,
c
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
+
(
b
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:114
for
c
,
a
,
b
being ( (
complex
) (
complex
)
number
) st
c
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
c
: ( (
complex
) (
complex
)
number
)
*
(
(
a
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
(
b
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:115
for
c
,
a
,
b
being ( (
complex
) (
complex
)
number
) st
c
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
a
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
(
b
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
/
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:116
for
b
,
d
,
a
,
c
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
d
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
(
c
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
(
a
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
(
c
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
/
(
b
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:117
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
*
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
+
(
b
: ( (
complex
) (
complex
)
number
)
/
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:118
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
(
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
(
a
: ( (
complex
) (
complex
)
number
)
/
(
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:119
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
(
a
: ( (
complex
) (
complex
)
number
)
/
(
3 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
(
a
: ( (
complex
) (
complex
)
number
)
/
(
3 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
(
a
: ( (
complex
) (
complex
)
number
)
/
(
3 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:120
for
a
,
c
,
b
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
(
b
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:121
for
a
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
-
(
a
: ( (
complex
) (
complex
)
number
)
/
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
/
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:122
for
a
,
b
,
c
,
d
being ( (
complex
) (
complex
)
number
) holds
(
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
a
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
(
b
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
-
(
c
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:123
for
b
,
d
,
a
,
e
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
d
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
b
: ( (
complex
) (
complex
)
number
)
<>
d
: ( (
complex
) (
complex
)
number
) &
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
e
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
-
e
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
(
b
: ( (
complex
) (
complex
)
number
)
-
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:124
for
a
,
b
,
e
,
d
being ( (
complex
) (
complex
)
number
) holds
(
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
e
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
a
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
(
b
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
-
(
e
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:125
for
a
,
b
,
e
,
d
being ( (
complex
) (
complex
)
number
) holds
(
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
e
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
a
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
(
b
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
(
e
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:126
for
b
,
a
,
e
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
e
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
-
(
e
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:127
for
b
,
c
,
a
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
c
: ( (
complex
) (
complex
)
number
)
-
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
(
c
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:128
for
c
,
a
,
b
being ( (
complex
) (
complex
)
number
) st
c
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
c
: ( (
complex
) (
complex
)
number
)
*
(
(
a
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
(
b
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:129
for
c
,
a
,
b
being ( (
complex
) (
complex
)
number
) st
c
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
a
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
(
b
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
/
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:130
for
b
,
d
,
a
,
c
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
d
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
(
c
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
(
a
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
(
c
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
/
(
b
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:131
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
*
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
-
(
b
: ( (
complex
) (
complex
)
number
)
/
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:132
for
a
,
c
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
c
: ( (
complex
) (
complex
)
number
)
=
(
(
(
a
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:133
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
-
a
: ( (
complex
) (
complex
)
number
) : ( (
complex
) (
complex
)
set
)
=
-
b
: ( (
complex
) (
complex
)
number
) : ( (
complex
) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:134
for
a
being ( (
complex
) (
complex
)
number
) st
-
a
: ( (
complex
) (
complex
)
number
) : ( (
complex
) (
complex
)
set
)
=
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
=
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: XCMPLX_1:135
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
+
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:136
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
=
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:137
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
=
a
: ( (
complex
) (
complex
)
number
)
+
(
b
: ( (
complex
) (
complex
)
number
)
+
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:138
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
=
(
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:139
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
-
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:140
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
-
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
+
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:141
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
-
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
) ;
theorem
:: XCMPLX_1:142
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
-
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
-
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:143
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:144
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
=
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:145
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:146
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:147
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:148
for
c
,
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
c
: ( (
complex
) (
complex
)
number
)
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
(
c
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
-
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
) ;
theorem
:: XCMPLX_1:149
for
a
being ( (
complex
) (
complex
)
number
) holds
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
-
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
-
a
: ( (
complex
) (
complex
)
number
) : ( (
complex
) (
complex
)
set
) ;
theorem
:: XCMPLX_1:150
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
-
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:151
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
=
a
: ( (
complex
) (
complex
)
number
)
-
(
b
: ( (
complex
) (
complex
)
number
)
+
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:152
for
a
,
c
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
+
(
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:153
for
c
,
a
,
b
being ( (
complex
) (
complex
)
number
) st
c
: ( (
complex
) (
complex
)
number
)
-
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
c
: ( (
complex
) (
complex
)
number
)
+
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:154
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:155
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:156
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
-
(
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:157
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:158
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:159
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:160
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
-
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:161
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
-
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:162
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
-
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:163
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
-
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
) ;
theorem
:: XCMPLX_1:164
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:165
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:166
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
-
(
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:167
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
-
(
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:168
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
-
(
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:169
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
-
(
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:170
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
-
(
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:171
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
-
(
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:172
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
-
(
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:173
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
-
(
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:174
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
*
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
-
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
) ;
theorem
:: XCMPLX_1:175
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
*
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
*
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:176
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
*
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:177
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
-
(
a
: ( (
complex
) (
complex
)
number
)
*
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:178
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
-
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:179
for
a
being ( (
complex
) (
complex
)
number
) holds
(
-
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( (
complex
) ( non
zero
complex
V12
()
V15
() )
set
)
*
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
-
a
: ( (
complex
) (
complex
)
number
) : ( (
complex
) (
complex
)
set
) ;
theorem
:: XCMPLX_1:180
for
a
being ( (
complex
) (
complex
)
number
) holds
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
*
(
-
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( (
complex
) ( non
zero
complex
V12
()
V15
() )
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:181
for
b
,
a
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
-
b
: ( (
complex
) (
complex
)
number
) : ( (
complex
) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
=
-
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) : ( (
complex
) ( non
zero
complex
V12
()
V15
() )
set
) ;
theorem
:: XCMPLX_1:182
for
a
being ( (
complex
) (
complex
)
number
) holds
( not
a
: ( (
complex
) (
complex
)
number
)
*
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) or
a
: ( (
complex
) (
complex
)
number
)
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) or
a
: ( (
complex
) (
complex
)
number
)
=
-
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) : ( (
complex
) ( non
zero
complex
V12
()
V15
() )
set
) ) ;
theorem
:: XCMPLX_1:183
for
a
being ( (
complex
) (
complex
)
number
) holds
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
(
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:184
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
b
: ( (
complex
) (
complex
)
number
)
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:185
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
-
(
(
b
: ( (
complex
) (
complex
)
number
)
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
) ;
theorem
:: XCMPLX_1:186
for
a
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
-
(
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
-
a
: ( (
complex
) (
complex
)
number
) : ( (
complex
) (
complex
)
set
) ;
theorem
:: XCMPLX_1:187
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
-
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:188
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
/
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
-
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
) ;
theorem
:: XCMPLX_1:189
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
-
(
a
: ( (
complex
) (
complex
)
number
)
/
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:190
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
-
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:191
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
/
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:192
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
/
(
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:193
for
a
being ( (
complex
) (
complex
)
number
) holds
-
a
: ( (
complex
) (
complex
)
number
) : ( (
complex
) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
/
(
-
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( (
complex
) ( non
zero
complex
V12
()
V15
() )
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:194
for
a
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
=
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
/
(
-
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( (
complex
) ( non
zero
complex
V12
()
V15
() )
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:195
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
-
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) : ( (
complex
) ( non
zero
complex
V12
()
V15
() )
set
) holds
(
a
: ( (
complex
) (
complex
)
number
)
=
-
b
: ( (
complex
) (
complex
)
number
) : ( (
complex
) (
complex
)
set
) &
b
: ( (
complex
) (
complex
)
number
)
=
-
a
: ( (
complex
) (
complex
)
number
) : ( (
complex
) (
complex
)
set
) ) ;
theorem
:: XCMPLX_1:196
for
b
,
a
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
b
: ( (
complex
) (
complex
)
number
)
/
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
-
b
: ( (
complex
) (
complex
)
number
) : ( (
complex
) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
=
-
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) : ( (
complex
) ( non
zero
complex
V12
()
V15
() )
set
) ;
theorem
:: XCMPLX_1:197
for
a
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
/
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
-
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) : ( (
complex
) ( non
zero
complex
V12
()
V15
() )
set
) ;
theorem
:: XCMPLX_1:198
for
a
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
/
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
-
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) : ( (
complex
) ( non
zero
complex
V12
()
V15
() )
set
) ;
theorem
:: XCMPLX_1:199
for
a
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
a
: ( (
complex
) (
complex
)
number
)
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) & not
a
: ( (
complex
) (
complex
)
number
)
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
=
-
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) : ( (
complex
) ( non
zero
complex
V12
()
V15
() )
set
) ;
theorem
:: XCMPLX_1:200
for
b
,
d
,
a
,
e
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
d
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
b
: ( (
complex
) (
complex
)
number
)
<>
-
d
: ( (
complex
) (
complex
)
number
) : ( (
complex
) (
complex
)
set
) &
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
e
: ( (
complex
) (
complex
)
number
)
/
d
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
+
e
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
(
b
: ( (
complex
) (
complex
)
number
)
+
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:201
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
"
: ( (
complex
) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
"
: ( (
complex
) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:202
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
"
: ( (
complex
) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
set
)
=
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: XCMPLX_1:203
for
b
,
a
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
=
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
b
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:204
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
)
*
(
b
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
"
: ( (
complex
) (
complex
)
set
) ;
theorem
:: XCMPLX_1:205
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
*
(
b
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
"
: ( (
complex
) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
)
*
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:206
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
(
a
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
)
*
(
b
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
"
: ( (
complex
) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:207
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
*
(
b
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: XCMPLX_1:208
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
a
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
)
*
(
b
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: XCMPLX_1:209
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
*
(
b
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:210
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
)
"
: ( (
complex
) (
complex
)
set
) ;
theorem
:: XCMPLX_1:211
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
a
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
)
+
(
b
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
"
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:212
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
a
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
)
-
(
b
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
b
: ( (
complex
) (
complex
)
number
)
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
"
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:213
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
"
: ( (
complex
) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
/
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:214
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
)
/
(
b
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
/
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:215
for
a
being ( (
complex
) (
complex
)
number
) holds 1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
"
: ( (
complex
) (
complex
)
set
) ;
theorem
:: XCMPLX_1:216
for
a
being ( (
complex
) (
complex
)
number
) holds 1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
(
a
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:217
for
a
being ( (
complex
) (
complex
)
number
) holds
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
"
: ( (
complex
) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:218
for
a
,
b
being ( (
complex
) (
complex
)
number
) st 1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
b
: ( (
complex
) (
complex
)
number
)
"
: ( (
complex
) (
complex
)
set
) holds
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
) ;
theorem
:: XCMPLX_1:219
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
/
(
b
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:220
for
a
,
c
,
b
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
)
*
(
c
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
c
: ( (
complex
) (
complex
)
number
)
/
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:221
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
)
/
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
"
: ( (
complex
) (
complex
)
set
) ;
theorem
:: XCMPLX_1:222
for
a
being ( (
complex
) (
complex
)
number
) holds
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
"
: ( (
complex
) (
complex
)
set
)
=
-
(
a
: ( (
complex
) (
complex
)
number
)
"
)
: ( (
complex
) (
complex
)
set
) : ( (
complex
) (
complex
)
set
) ;
theorem
:: XCMPLX_1:223
for
a
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
a
: ( (
complex
) (
complex
)
number
)
=
a
: ( (
complex
) (
complex
)
number
)
"
: ( (
complex
) (
complex
)
set
) & not
a
: ( (
complex
) (
complex
)
number
)
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
a
: ( (
complex
) (
complex
)
number
)
=
-
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) : ( (
complex
) ( non
zero
complex
V12
()
V15
() )
set
) ;
begin
theorem
:: XCMPLX_1:224
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:225
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:226
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
(
a
: ( (
complex
) (
complex
)
number
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:227
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) holds
(
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:228
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
-
b
: ( (
complex
) (
complex
)
number
) : ( (
complex
) (
complex
)
set
) ;
theorem
:: XCMPLX_1:229
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
+
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
-
b
: ( (
complex
) (
complex
)
number
) : ( (
complex
) (
complex
)
set
) ;
theorem
:: XCMPLX_1:230
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
a
: ( (
complex
) (
complex
)
number
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
-
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
-
b
: ( (
complex
) (
complex
)
number
) : ( (
complex
) (
complex
)
set
) ;
theorem
:: XCMPLX_1:231
for
a
,
b
being ( (
complex
) (
complex
)
number
) holds
(
(
-
a
: ( (
complex
) (
complex
)
number
)
)
: ( (
complex
) (
complex
)
set
)
-
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
a
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
-
b
: ( (
complex
) (
complex
)
number
) : ( (
complex
) (
complex
)
set
) ;
begin
theorem
:: XCMPLX_1:232
for
a
,
b
being ( (
complex
) (
complex
)
number
) st
b
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
ex
e
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
=
b
: ( (
complex
) (
complex
)
number
)
/
e
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:233
for
a
,
b
,
c
,
d
,
e
being ( (
complex
) (
complex
)
number
) holds
a
: ( (
complex
) (
complex
)
number
)
/
(
(
b
: ( (
complex
) (
complex
)
number
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
d
: ( (
complex
) (
complex
)
number
)
/
e
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
(
e
: ( (
complex
) (
complex
)
number
)
/
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
(
a
: ( (
complex
) (
complex
)
number
)
/
(
b
: ( (
complex
) (
complex
)
number
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:234
for
d
,
c
,
b
,
a
being ( (
complex
) (
complex
)
number
) holds
(
(
(
d
: ( (
complex
) (
complex
)
number
)
-
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
(
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V12
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
-
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
*
c
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
(
(
a
: ( (
complex
) (
complex
)
number
)
/
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
d
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: XCMPLX_1:235
for
a
,
b
,
c
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V12
()
V13
()
V14
()
V15
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
a
: ( (
complex
) (
complex
)
number
)
*
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
a
: ( (
complex
) (
complex
)
number
)
*
(
b
: ( (
complex
) (
complex
)
number
)
+
(
c
: ( (
complex
) (
complex
)
number
)
/
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;