:: The Field of Complex Numbers
:: by Anna Justyna Milewska
::
:: Received January 18, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users
begin
definition
func
F_Complex
->
strict
doubleLoopStr
means
:
Def1
:
:: COMPLFLD:def 1
( the
carrier
of
it
=
COMPLEX
& the
addF
of
it
=
addcomplex
& the
multF
of
it
=
multcomplex
&
1.
it
=
1r
&
0.
it
=
0c
);
existence
ex
b
1
being
strict
doubleLoopStr
st
( the
carrier
of
b
1
=
COMPLEX
& the
addF
of
b
1
=
addcomplex
& the
multF
of
b
1
=
multcomplex
&
1.
b
1
=
1r
&
0.
b
1
=
0c
)
proof
end;
uniqueness
for
b
1
,
b
2
being
strict
doubleLoopStr
st the
carrier
of
b
1
=
COMPLEX
& the
addF
of
b
1
=
addcomplex
& the
multF
of
b
1
=
multcomplex
&
1.
b
1
=
1r
&
0.
b
1
=
0c
& the
carrier
of
b
2
=
COMPLEX
& the
addF
of
b
2
=
addcomplex
& the
multF
of
b
2
=
multcomplex
&
1.
b
2
=
1r
&
0.
b
2
=
0c
holds
b
1
=
b
2
;
end;
::
deftheorem
Def1
defines
F_Complex
COMPLFLD:def 1 :
for
b
1
being
strict
doubleLoopStr
holds
(
b
1
=
F_Complex
iff ( the
carrier
of
b
1
=
COMPLEX
& the
addF
of
b
1
=
addcomplex
& the
multF
of
b
1
=
multcomplex
&
1.
b
1
=
1r
&
0.
b
1
=
0c
) );
registration
cluster
F_Complex
->
non
empty
strict
;
coherence
not
F_Complex
is
empty
by
Def1
;
end;
registration
cluster
->
complex
for
Element
of the
carrier
of
F_Complex
;
coherence
for
b
1
being
Element
of
F_Complex
holds
b
1
is
complex
proof
end;
end;
registration
let
a
,
b
be
complex
number
;
let
x
,
y
be
Element
of
F_Complex
;
identify
x
+
y
with
a
+
b
when
x
=
a
,
y
=
b
;
compatibility
(
x
=
a
&
y
=
b
implies
x
+
y
=
a
+
b
)
proof
end;
identify
x
*
y
with
a
*
b
when
x
=
a
,
y
=
b
;
compatibility
(
x
=
a
&
y
=
b
implies
x
*
y
=
a
*
b
)
proof
end;
end;
registration
cluster
F_Complex
->
strict
well-unital
;
coherence
F_Complex
is
well-unital
proof
end;
end;
Lm1
:
1_
F_Complex
=
1r
by
Def1
;
Lm2
:
1.
F_Complex
=
1r
by
Def1
;
registration
cluster
F_Complex
->
non
degenerated
right_complementable
almost_left_invertible
strict
associative
commutative
right_unital
distributive
left_unital
Abelian
add-associative
right_zeroed
;
coherence
(
F_Complex
is
add-associative
&
F_Complex
is
right_zeroed
&
F_Complex
is
right_complementable
&
F_Complex
is
Abelian
&
F_Complex
is
commutative
&
F_Complex
is
associative
&
F_Complex
is
left_unital
&
F_Complex
is
right_unital
&
F_Complex
is
distributive
&
F_Complex
is
almost_left_invertible
& not
F_Complex
is
degenerated
)
proof
end;
end;
theorem
:: COMPLFLD:1
for
x1
,
y1
being
Element
of
F_Complex
for
x2
,
y2
being
complex
number
st
x1
=
x2
&
y1
=
y2
holds
x1
+
y1
=
x2
+
y2
;
theorem
Th2
:
:: COMPLFLD:2
for
x1
being
Element
of
F_Complex
for
x2
being
complex
number
st
x1
=
x2
holds
-
x1
=
-
x2
proof
end;
theorem
Th3
:
:: COMPLFLD:3
for
x1
,
y1
being
Element
of
F_Complex
for
x2
,
y2
being
complex
number
st
x1
=
x2
&
y1
=
y2
holds
x1
-
y1
=
x2
-
y2
proof
end;
theorem
:: COMPLFLD:4
for
x1
,
y1
being
Element
of
F_Complex
for
x2
,
y2
being
complex
number
st
x1
=
x2
&
y1
=
y2
holds
x1
*
y1
=
x2
*
y2
;
theorem
Th5
:
:: COMPLFLD:5
for
x1
being
Element
of
F_Complex
for
x2
being
complex
number
st
x1
=
x2
&
x1
<>
0.
F_Complex
holds
x1
"
=
x2
"
proof
end;
theorem
Th6
:
:: COMPLFLD:6
for
x1
,
y1
being
Element
of
F_Complex
for
x2
,
y2
being
complex
number
st
x1
=
x2
&
y1
=
y2
&
y1
<>
0.
F_Complex
holds
x1
/
y1
=
x2
/
y2
proof
end;
theorem
Th7
:
:: COMPLFLD:7
0.
F_Complex
=
0c
by
Def1
;
theorem
:: COMPLFLD:8
1_
F_Complex
=
1r
by
Def1
;
theorem
:: COMPLFLD:9
(
1_
F_Complex
)
+
(
1_
F_Complex
)
<>
0.
F_Complex
by
Def1
,
Lm1
;
definition
let
z
be
Element
of
F_Complex
;
:: original:
*'
redefine
func
z
*'
->
Element
of
F_Complex
;
coherence
z
*'
is
Element
of
F_Complex
proof
end;
end;
theorem
:: COMPLFLD:10
for
z
being
Element
of
F_Complex
holds
-
z
=
(
-
(
1_
F_Complex
)
)
*
z
proof
end;
theorem
:: COMPLFLD:11
for
z1
,
z2
being
Element
of
F_Complex
holds
z1
-
(
-
z2
)
=
z1
+
z2
proof
end;
theorem
:: COMPLFLD:12
for
z1
,
z
being
Element
of
F_Complex
holds
z1
=
(
z1
+
z
)
-
z
proof
end;
theorem
:: COMPLFLD:13
for
z1
,
z
being
Element
of
F_Complex
holds
z1
=
(
z1
-
z
)
+
z
proof
end;
theorem
:: COMPLFLD:14
for
z1
,
z2
being
Element
of
F_Complex
st
z1
<>
0.
F_Complex
&
z2
<>
0.
F_Complex
&
z1
"
=
z2
"
holds
z1
=
z2
proof
end;
theorem
:: COMPLFLD:15
for
z2
,
z1
being
Element
of
F_Complex
st
z2
<>
0.
F_Complex
& (
z1
*
z2
=
1.
F_Complex
or
z2
*
z1
=
1.
F_Complex
) holds
z1
=
z2
"
proof
end;
theorem
:: COMPLFLD:16
for
z2
,
z1
,
z3
being
Element
of
F_Complex
st
z2
<>
0.
F_Complex
& (
z1
*
z2
=
z3
or
z2
*
z1
=
z3
) holds
(
z1
=
z3
*
(
z2
"
)
&
z1
=
(
z2
"
)
*
z3
)
proof
end;
theorem
:: COMPLFLD:17
(
1.
F_Complex
)
"
=
1.
F_Complex
proof
end;
theorem
:: COMPLFLD:18
for
z1
,
z2
being
Element
of
F_Complex
st
z1
<>
0.
F_Complex
&
z2
<>
0.
F_Complex
holds
(
z1
*
z2
)
"
=
(
z1
"
)
*
(
z2
"
)
proof
end;
theorem
:: COMPLFLD:19
for
z
being
Element
of
F_Complex
st
z
<>
0.
F_Complex
holds
(
-
z
)
"
=
-
(
z
"
)
proof
end;
theorem
:: COMPLFLD:20
for
z1
,
z2
being
Element
of
F_Complex
st
z1
<>
0.
F_Complex
&
z2
<>
0.
F_Complex
holds
(
z1
"
)
+
(
z2
"
)
=
(
z1
+
z2
)
*
(
(
z1
*
z2
)
"
)
proof
end;
theorem
:: COMPLFLD:21
for
z1
,
z2
being
Element
of
F_Complex
st
z1
<>
0.
F_Complex
&
z2
<>
0.
F_Complex
holds
(
z1
"
)
-
(
z2
"
)
=
(
z2
-
z1
)
*
(
(
z1
*
z2
)
"
)
proof
end;
theorem
:: COMPLFLD:22
for
z
being
Element
of
F_Complex
st
z
<>
0.
F_Complex
holds
z
"
=
(
1.
F_Complex
)
/
z
proof
end;
theorem
:: COMPLFLD:23
for
z
being
Element
of
F_Complex
holds
z
/
(
1.
F_Complex
)
=
z
proof
end;
theorem
:: COMPLFLD:24
for
z
being
Element
of
F_Complex
st
z
<>
0.
F_Complex
holds
z
/
z
=
1.
F_Complex
proof
end;
theorem
:: COMPLFLD:25
for
z
being
Element
of
F_Complex
st
z
<>
0.
F_Complex
holds
(
0.
F_Complex
)
/
z
=
0.
F_Complex
by
Th7
;
theorem
Th26
:
:: COMPLFLD:26
for
z2
,
z1
being
Element
of
F_Complex
st
z2
<>
0.
F_Complex
&
z1
/
z2
=
0.
F_Complex
holds
z1
=
0.
F_Complex
proof
end;
theorem
:: COMPLFLD:27
for
z2
,
z4
,
z1
,
z3
being
Element
of
F_Complex
st
z2
<>
0.
F_Complex
&
z4
<>
0.
F_Complex
holds
(
z1
/
z2
)
*
(
z3
/
z4
)
=
(
z1
*
z3
)
/
(
z2
*
z4
)
proof
end;
theorem
:: COMPLFLD:28
for
z2
,
z
,
z1
being
Element
of
F_Complex
st
z2
<>
0.
F_Complex
holds
z
*
(
z1
/
z2
)
=
(
z
*
z1
)
/
z2
;
theorem
:: COMPLFLD:29
for
z2
,
z1
being
Element
of
F_Complex
st
z2
<>
0.
F_Complex
&
z1
/
z2
=
1.
F_Complex
holds
z1
=
z2
proof
end;
theorem
:: COMPLFLD:30
for
z
,
z1
being
Element
of
F_Complex
st
z
<>
0.
F_Complex
holds
z1
=
(
z1
*
z
)
/
z
proof
end;
theorem
:: COMPLFLD:31
for
z1
,
z2
being
Element
of
F_Complex
st
z1
<>
0.
F_Complex
&
z2
<>
0.
F_Complex
holds
(
z1
/
z2
)
"
=
z2
/
z1
proof
end;
theorem
:: COMPLFLD:32
for
z1
,
z2
being
Element
of
F_Complex
st
z1
<>
0.
F_Complex
&
z2
<>
0.
F_Complex
holds
(
z1
"
)
/
(
z2
"
)
=
z2
/
z1
proof
end;
theorem
:: COMPLFLD:33
for
z2
,
z1
being
Element
of
F_Complex
st
z2
<>
0.
F_Complex
holds
z1
/
(
z2
"
)
=
z1
*
z2
proof
end;
theorem
:: COMPLFLD:34
for
z1
,
z2
being
Element
of
F_Complex
st
z1
<>
0.
F_Complex
&
z2
<>
0.
F_Complex
holds
(
z1
"
)
/
z2
=
(
z1
*
z2
)
"
proof
end;
theorem
:: COMPLFLD:35
for
z1
,
z2
,
z
being
Element
of
F_Complex
st
z1
<>
0.
F_Complex
&
z2
<>
0.
F_Complex
holds
(
z1
"
)
*
(
z
/
z2
)
=
z
/
(
z1
*
z2
)
proof
end;
theorem
:: COMPLFLD:36
for
z
,
z2
,
z1
being
Element
of
F_Complex
st
z
<>
0.
F_Complex
&
z2
<>
0.
F_Complex
holds
(
z1
/
z2
=
(
z1
*
z
)
/
(
z2
*
z
)
&
z1
/
z2
=
(
z
*
z1
)
/
(
z
*
z2
)
)
proof
end;
theorem
:: COMPLFLD:37
for
z2
,
z3
,
z1
being
Element
of
F_Complex
st
z2
<>
0.
F_Complex
&
z3
<>
0.
F_Complex
holds
z1
/
(
z2
*
z3
)
=
(
z1
/
z2
)
/
z3
proof
end;
theorem
:: COMPLFLD:38
for
z2
,
z3
,
z1
being
Element
of
F_Complex
st
z2
<>
0.
F_Complex
&
z3
<>
0.
F_Complex
holds
(
z1
*
z3
)
/
z2
=
z1
/
(
z2
/
z3
)
proof
end;
theorem
:: COMPLFLD:39
for
z2
,
z3
,
z4
,
z1
being
Element
of
F_Complex
st
z2
<>
0.
F_Complex
&
z3
<>
0.
F_Complex
&
z4
<>
0.
F_Complex
holds
(
z1
/
z2
)
/
(
z3
/
z4
)
=
(
z1
*
z4
)
/
(
z2
*
z3
)
proof
end;
theorem
:: COMPLFLD:40
for
z2
,
z4
,
z1
,
z3
being
Element
of
F_Complex
st
z2
<>
0.
F_Complex
&
z4
<>
0.
F_Complex
holds
(
z1
/
z2
)
+
(
z3
/
z4
)
=
(
(
z1
*
z4
)
+
(
z3
*
z2
)
)
/
(
z2
*
z4
)
proof
end;
theorem
:: COMPLFLD:41
for
z
,
z1
,
z2
being
Element
of
F_Complex
st
z
<>
0.
F_Complex
holds
(
z1
/
z
)
+
(
z2
/
z
)
=
(
z1
+
z2
)
/
z
;
theorem
:: COMPLFLD:42
for
z2
,
z1
being
Element
of
F_Complex
st
z2
<>
0.
F_Complex
holds
(
-
(
z1
/
z2
)
=
(
-
z1
)
/
z2
&
-
(
z1
/
z2
)
=
z1
/
(
-
z2
)
)
proof
end;
theorem
:: COMPLFLD:43
for
z2
,
z1
being
Element
of
F_Complex
st
z2
<>
0.
F_Complex
holds
z1
/
z2
=
(
-
z1
)
/
(
-
z2
)
proof
end;
theorem
:: COMPLFLD:44
for
z2
,
z4
,
z1
,
z3
being
Element
of
F_Complex
st
z2
<>
0.
F_Complex
&
z4
<>
0.
F_Complex
holds
(
z1
/
z2
)
-
(
z3
/
z4
)
=
(
(
z1
*
z4
)
-
(
z3
*
z2
)
)
/
(
z2
*
z4
)
proof
end;
theorem
:: COMPLFLD:45
for
z
,
z1
,
z2
being
Element
of
F_Complex
st
z
<>
0.
F_Complex
holds
(
z1
/
z
)
-
(
z2
/
z
)
=
(
z1
-
z2
)
/
z
proof
end;
theorem
:: COMPLFLD:46
for
z2
,
z1
,
z3
being
Element
of
F_Complex
st
z2
<>
0.
F_Complex
& (
z1
*
z2
=
z3
or
z2
*
z1
=
z3
) holds
z1
=
z3
/
z2
proof
end;
theorem
:: COMPLFLD:47
(
0.
F_Complex
)
*'
=
0.
F_Complex
proof
end;
theorem
Th48
:
:: COMPLFLD:48
for
z
being
Element
of
F_Complex
st
z
*'
=
0.
F_Complex
holds
z
=
0.
F_Complex
proof
end;
theorem
:: COMPLFLD:49
(
1.
F_Complex
)
*'
=
1.
F_Complex
proof
end;
theorem
:: COMPLFLD:50
for
z
being
Element
of
F_Complex
holds
(
z
*'
)
*'
=
z
;
theorem
:: COMPLFLD:51
for
z1
,
z2
being
Element
of
F_Complex
holds
(
z1
+
z2
)
*'
=
(
z1
*'
)
+
(
z2
*'
)
by
COMPLEX1:32
;
theorem
:: COMPLFLD:52
for
z
being
Element
of
F_Complex
holds
(
-
z
)
*'
=
-
(
z
*'
)
proof
end;
theorem
:: COMPLFLD:53
for
z1
,
z2
being
Element
of
F_Complex
holds
(
z1
-
z2
)
*'
=
(
z1
*'
)
-
(
z2
*'
)
proof
end;
theorem
:: COMPLFLD:54
for
z1
,
z2
being
Element
of
F_Complex
holds
(
z1
*
z2
)
*'
=
(
z1
*'
)
*
(
z2
*'
)
by
COMPLEX1:35
;
theorem
:: COMPLFLD:55
for
z
being
Element
of
F_Complex
st
z
<>
0.
F_Complex
holds
(
z
"
)
*'
=
(
z
*'
)
"
proof
end;
theorem
:: COMPLFLD:56
for
z2
,
z1
being
Element
of
F_Complex
st
z2
<>
0.
F_Complex
holds
(
z1
/
z2
)
*'
=
(
z1
*'
)
/
(
z2
*'
)
proof
end;
theorem
:: COMPLFLD:57
|.
(
0.
F_Complex
)
.|
=
0
by
Def1
,
COMPLEX1:44
;
theorem
:: COMPLFLD:58
for
z
being
Element
of
F_Complex
st
|.
z
.|
=
0
holds
z
=
0.
F_Complex
by
Th7
;
theorem
:: COMPLFLD:59
for
z
being
Element
of
F_Complex
holds
(
z
<>
0.
F_Complex
iff
0
<
|.
z
.|
)
by
Th7
,
COMPLEX1:47
;
theorem
:: COMPLFLD:60
|.
(
1.
F_Complex
)
.|
=
1
by
Def1
,
COMPLEX1:48
;
theorem
:: COMPLFLD:61
for
z
being
Element
of
F_Complex
holds
|.
(
-
z
)
.|
=
|.
z
.|
proof
end;
theorem
:: COMPLFLD:62
for
z1
,
z2
being
Element
of
F_Complex
holds
|.
(
z1
+
z2
)
.|
<=
|.
z1
.|
+
|.
z2
.|
by
COMPLEX1:56
;
theorem
:: COMPLFLD:63
for
z1
,
z2
being
Element
of
F_Complex
holds
|.
(
z1
-
z2
)
.|
<=
|.
z1
.|
+
|.
z2
.|
proof
end;
theorem
:: COMPLFLD:64
for
z1
,
z2
being
Element
of
F_Complex
holds
|.
z1
.|
-
|.
z2
.|
<=
|.
(
z1
+
z2
)
.|
by
COMPLEX1:58
;
theorem
:: COMPLFLD:65
for
z1
,
z2
being
Element
of
F_Complex
holds
|.
z1
.|
-
|.
z2
.|
<=
|.
(
z1
-
z2
)
.|
proof
end;
theorem
:: COMPLFLD:66
for
z1
,
z2
being
Element
of
F_Complex
holds
|.
(
z1
-
z2
)
.|
=
|.
(
z2
-
z1
)
.|
proof
end;
theorem
:: COMPLFLD:67
for
z1
,
z2
being
Element
of
F_Complex
holds
(
|.
(
z1
-
z2
)
.|
=
0
iff
z1
=
z2
)
proof
end;
theorem
:: COMPLFLD:68
for
z1
,
z2
being
Element
of
F_Complex
holds
(
z1
<>
z2
iff
0
<
|.
(
z1
-
z2
)
.|
)
proof
end;
theorem
:: COMPLFLD:69
for
z1
,
z2
,
z
being
Element
of
F_Complex
holds
|.
(
z1
-
z2
)
.|
<=
|.
(
z1
-
z
)
.|
+
|.
(
z
-
z2
)
.|
proof
end;
theorem
:: COMPLFLD:70
for
z1
,
z2
being
Element
of
F_Complex
holds
abs
(
|.
z1
.|
-
|.
z2
.|
)
<=
|.
(
z1
-
z2
)
.|
proof
end;
theorem
:: COMPLFLD:71
for
z1
,
z2
being
Element
of
F_Complex
holds
|.
(
z1
*
z2
)
.|
=
|.
z1
.|
*
|.
z2
.|
by
COMPLEX1:65
;
theorem
:: COMPLFLD:72
for
z
being
Element
of
F_Complex
st
z
<>
0.
F_Complex
holds
|.
(
z
"
)
.|
=
|.
z
.|
"
proof
end;
theorem
:: COMPLFLD:73
for
z2
,
z1
being
Element
of
F_Complex
st
z2
<>
0.
F_Complex
holds
|.
z1
.|
/
|.
z2
.|
=
|.
(
z1
/
z2
)
.|
proof
end;
begin
:: from COMPTRIG, 2006.08.12, A.T.
scheme
:: COMPLFLD:sch 1
Regrwithout0
{
P
1
[
Nat
] } :
P
1
[1]
provided
A1
: ex
k
being non
empty
Element
of
NAT
st
P
1
[
k
]
and
A2
: for
k
being non
empty
Element
of
NAT
st
k
<>
1 &
P
1
[
k
] holds
ex
n
being non
empty
Element
of
NAT
st
(
n
<
k
&
P
1
[
n
] )
proof
end;
theorem
Th74
:
:: COMPLFLD:74
for
e
being
Element
of
F_Complex
for
n
being non
empty
Nat
holds
(
power
F_Complex
)
.
(
e
,
n
)
=
e
|^
n
proof
end;
definition
let
x
be
Element
of
F_Complex
;
let
n
be non
empty
Element
of
NAT
;
:: original:
CRoot
redefine
mode
CRoot
of
n
,
x
->
Element
of
F_Complex
means
:
Def2
:
:: COMPLFLD:def 2
(
power
F_Complex
)
.
(
it
,
n
)
=
x
;
coherence
for
b
1
being
CRoot
of
n
,
x
holds
b
1
is
Element
of
F_Complex
proof
end;
compatibility
for
b
1
being
Element
of
F_Complex
holds
(
b
1
is
CRoot
of
n
,
x
iff
(
power
F_Complex
)
.
(
b
1
,
n
)
=
x
)
proof
end;
end;
::
deftheorem
Def2
defines
CRoot
COMPLFLD:def 2 :
for
x
being
Element
of
F_Complex
for
n
being non
empty
Element
of
NAT
for
b
3
being
Element
of
F_Complex
holds
(
b
3
is
CRoot
of
n
,
x
iff
(
power
F_Complex
)
.
(
b
3
,
n
)
=
x
);
theorem
:: COMPLFLD:75
for
x
being
Element
of
F_Complex
for
v
being
CRoot
of 1,
x
holds
v
=
x
proof
end;
theorem
:: COMPLFLD:76
for
n
being non
empty
Element
of
NAT
for
v
being
CRoot
of
n
,
0.
F_Complex
holds
v
=
0.
F_Complex
proof
end;
theorem
:: COMPLFLD:77
for
n
being non
empty
Element
of
NAT
for
x
being
Element
of
F_Complex
for
v
being
CRoot
of
n
,
x
st
v
=
0.
F_Complex
holds
x
=
0.
F_Complex
proof
end;