:: ARITHM semantic presentation
begin
theorem
:: ARITHM:1
for
x
being ( (
complex
) (
complex
)
number
) holds
x
: ( (
complex
) (
complex
)
number
)
+
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
)
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
K19
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
complex
)
set
)
=
x
: ( (
complex
) (
complex
)
number
) ;
theorem
:: ARITHM:2
for
x
being ( (
complex
) (
complex
)
number
) holds
x
: ( (
complex
) (
complex
)
number
)
*
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
)
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
K19
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
complex
)
set
)
=
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
)
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
K19
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: ARITHM:3
for
x
being ( (
complex
) (
complex
)
number
) holds 1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
)
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
K19
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
x
: ( (
complex
) (
complex
)
number
) ;
theorem
:: ARITHM:4
for
x
being ( (
complex
) (
complex
)
number
) holds
x
: ( (
complex
) (
complex
)
number
)
-
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
)
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
K19
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
complex
)
set
)
=
x
: ( (
complex
) (
complex
)
number
) ;
theorem
:: ARITHM:5
for
x
being ( (
complex
) (
complex
)
number
) holds
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
)
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
K19
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) )
/
x
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
)
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
K19
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: ARITHM:6
for
x
being ( (
complex
) (
complex
)
number
) holds
x
: ( (
complex
) (
complex
)
number
)
/
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
)
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
K19
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
complex
)
set
)
=
x
: ( (
complex
) (
complex
)
number
) ;