Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users

### The Field of Complex Numbers

by
Anna Justyna Milewska

MML identifier: COMPLFLD
[ Mizar article, MML identifier index ]

```environ

vocabulary COMPLEX1, ARYTM, VECTSP_1, RLVECT_1, COMPLSP1, BINOP_1, LATTICES,
FUNCT_1, ARYTM_1, RELAT_1, ARYTM_3, ABSVALUE, COMPLFLD, XCMPLX_0;
notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, ORDINAL1, NUMBERS, ARYTM_0,
XCMPLX_0, XREAL_0, REAL_1, BINOP_1, ABSVALUE, RLVECT_1, VECTSP_1,
COMPLSP1, COMPLEX1, FUNCT_1;
constructors REAL_1, ABSVALUE, VECTSP_1, COMPLSP1, DOMAIN_1, BINOP_1,
COMPLEX1, MEMBERED, ARYTM_0, ARYTM_3, FUNCT_4;
clusters VECTSP_1, RELSET_1, XREAL_0, COMPLEX1, MEMBERED;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;

begin

canceled;

theorem :: COMPLFLD:2
for x1,y1,x2,y2 be Element of REAL holds
[*x1,y1*] + [*x2,y2*] = [*x1 + x2,y1 + y2*];

definition
func F_Complex -> strict doubleLoopStr means
:: COMPLFLD:def 1
the carrier of it = COMPLEX &
the mult of it = multcomplex &
the unity of it = 1r &
the Zero of it = 0c;
end;

definition
cluster F_Complex -> non empty;
end;

definition
cluster -> complex Element of F_Complex;
end;

definition
cluster F_Complex -> add-associative right_zeroed right_complementable
Abelian commutative associative left_unital
right_unital distributive Field-like non degenerated;
end;

theorem :: COMPLFLD:3
for x1,y1 be Element of F_Complex
for x2,y2 be Element of COMPLEX st x1 = x2 & y1 = y2 holds
x1 + y1 = x2 + y2;

theorem :: COMPLFLD:4
for x1 be Element of F_Complex
for x2 be Element of COMPLEX st x1 = x2 holds
- x1 = - x2;

theorem :: COMPLFLD:5
for x1,y1 be Element of F_Complex
for x2,y2 be Element of COMPLEX st x1 = x2 & y1 = y2 holds
x1 - y1 = x2 - y2;

theorem :: COMPLFLD:6
for x1,y1 be Element of F_Complex
for x2,y2 be Element of COMPLEX st x1 = x2 & y1 = y2 holds
x1 * y1 = x2 * y2;

theorem :: COMPLFLD:7
for x1 be Element of F_Complex
for x2 be Element of COMPLEX st x1 = x2 & x1 <> 0.F_Complex holds
x1" = x2";

theorem :: COMPLFLD:8
for x1,y1 be Element of F_Complex
for x2,y2 be Element of COMPLEX st
x1 = x2 & y1 = y2 & y1 <> 0.F_Complex holds x1/y1 = x2/y2;

theorem :: COMPLFLD:9
0.F_Complex = 0c;

theorem :: COMPLFLD:10
1_ F_Complex = 1r;

theorem :: COMPLFLD:11
1_ F_Complex + 1_ F_Complex <> 0.F_Complex;

definition
let z be Element of F_Complex;
func z*' -> Element of F_Complex means
:: COMPLFLD:def 2
ex z' be Element of COMPLEX
st z = z' & it = z'*';
end;

definition
let z be Element of F_Complex;
func |.z.| -> real number means
:: COMPLFLD:def 3
ex z' be Element of COMPLEX st z = z' & it = |.z'.|;
end;

definition
let z be Element of F_Complex;
redefine func |.z.| -> Element of REAL;
end;

theorem :: COMPLFLD:12
for x1 be Element of F_Complex
for x2 be Element of COMPLEX st
x1 = x2 holds x1*' = x2*';

reserve z,z1,z2,z3,z4 for Element of F_Complex;

canceled 16;

theorem :: COMPLFLD:29
-z = (-1_ F_Complex) * z;

canceled 5;

theorem :: COMPLFLD:35
z1 - -z2 = z1 + z2;

canceled 5;

theorem :: COMPLFLD:41
z1 = z1 + z - z;

theorem :: COMPLFLD:42
z1 = z1 - z + z;

canceled 4;

theorem :: COMPLFLD:47
z1 <> 0.F_Complex & z2 <> 0.F_Complex &
z1" = z2" implies z1 = z2;

theorem :: COMPLFLD:48
z2 <> 0.F_Complex &
(z1 * z2 = the unity of F_Complex or z2 * z1 = the unity of F_Complex)
implies z1 = z2";

theorem :: COMPLFLD:49
z2 <> 0.F_Complex & (z1 * z2 = z3 or z2 * z1 = z3) implies
z1 = z3 * z2" & z1 = z2" * z3;

theorem :: COMPLFLD:50
(the unity of F_Complex)" = the unity of F_Complex;

theorem :: COMPLFLD:51
z1 <> 0.F_Complex & z2 <> 0.F_Complex implies
(z1 * z2)" = z1" * z2";

canceled;

theorem :: COMPLFLD:53
z <> 0.F_Complex implies (-z)" = -(z");

canceled;

theorem :: COMPLFLD:55
z1 <> 0.F_Complex & z2 <> 0.F_Complex implies
z1" + z2" = (z1 + z2) * (z1 * z2)";

theorem :: COMPLFLD:56
z1 <> 0.F_Complex & z2 <> 0.F_Complex implies
z1" - z2" = (z2 - z1) * (z1 * z2)";

canceled;

theorem :: COMPLFLD:58
z <> 0.F_Complex implies z" = (the unity of F_Complex) / z;

theorem :: COMPLFLD:59
z / (the unity of F_Complex) = z;

theorem :: COMPLFLD:60
z <> 0.F_Complex implies z / z = the unity of F_Complex;

theorem :: COMPLFLD:61
z <> 0.F_Complex implies (0.F_Complex) / z = 0.F_Complex;

theorem :: COMPLFLD:62
z2 <> 0.F_Complex & z1 / z2 = 0.F_Complex implies
z1 = 0.F_Complex;

theorem :: COMPLFLD:63
z2 <> 0.F_Complex & z4 <> 0.F_Complex implies
(z1 / z2) * (z3 / z4) = (z1 * z3) / (z2 * z4);

theorem :: COMPLFLD:64
z2 <> 0.F_Complex implies z * (z1 / z2) = (z * z1) / z2;

theorem :: COMPLFLD:65
z2 <> 0.F_Complex & z1 / z2 = the unity of F_Complex implies
z1 = z2;

theorem :: COMPLFLD:66
z <> 0.F_Complex implies z1 = (z1 * z) / z;

theorem :: COMPLFLD:67
z1 <> 0.F_Complex & z2 <> 0.F_Complex implies
(z1 / z2)" = z2 / z1;

theorem :: COMPLFLD:68
z1 <> 0.F_Complex & z2 <> 0.F_Complex implies
(z1" / z2") = z2 / z1;

theorem :: COMPLFLD:69
z2 <> 0.F_Complex implies z1 / z2" = z1 * z2;

theorem :: COMPLFLD:70
z1 <> 0.F_Complex & z2 <> 0.F_Complex implies
z1" / z2 = (z1 * z2)";

theorem :: COMPLFLD:71
z1 <> 0.F_Complex & z2 <> 0.F_Complex implies
z1"* (z / z2) = z / (z1 * z2);

theorem :: COMPLFLD:72
z <> 0.F_Complex & z2 <> 0.F_Complex implies
(z1 / z2) = (z1 * z) / (z2 * z) & (z1 / z2) = (z * z1) / (z * z2);

theorem :: COMPLFLD:73
z2 <> 0.F_Complex & z3 <> 0.F_Complex implies
z1 / (z2 * z3) = z1 / z2 / z3;

theorem :: COMPLFLD:74
z2 <> 0.F_Complex & z3 <> 0.F_Complex implies
(z1 * z3) / z2 = z1 / (z2 / z3);

theorem :: COMPLFLD:75
z2 <> 0.F_Complex & z3 <> 0.F_Complex &
z4 <> 0.F_Complex implies
(z1 / z2) / (z3 / z4) = (z1 * z4) / (z2 * z3);

theorem :: COMPLFLD:76
z2 <> 0.F_Complex & z4 <> 0.F_Complex implies
z1 / z2 + z3 / z4 = (z1 * z4 + z3 * z2) / (z2 * z4);

theorem :: COMPLFLD:77
z <> 0.F_Complex implies z1 / z + z2 / z = (z1 + z2) / z;

theorem :: COMPLFLD:78
z2 <> 0.F_Complex implies -(z1 / z2) = (-z1) / z2 &
-(z1 / z2) = z1 / (-z2);

theorem :: COMPLFLD:79
z2 <> 0.F_Complex implies z1 / z2 = (-z1) / (-z2);

theorem :: COMPLFLD:80
z2 <> 0.F_Complex & z4 <> 0.F_Complex implies
z1 / z2 - z3 / z4 = (z1 * z4 - z3 * z2) / (z2 * z4);

theorem :: COMPLFLD:81
z <> 0.F_Complex implies z1 / z - z2 / z = (z1 - z2) / z;

theorem :: COMPLFLD:82
z2 <> 0.F_Complex & (z1 * z2 = z3 or z2 * z1 = z3) implies
z1 = z3 / z2;

theorem :: COMPLFLD:83
(the Zero of F_Complex)*' = the Zero of F_Complex;

theorem :: COMPLFLD:84
z*' = the Zero of F_Complex implies z = the Zero of F_Complex;

theorem :: COMPLFLD:85
(the unity of F_Complex)*' = the unity of F_Complex;

theorem :: COMPLFLD:86
z*'*' = z;

theorem :: COMPLFLD:87
(z1 + z2)*' = z1*' + z2*';

theorem :: COMPLFLD:88
(-z)*' = -(z*');

theorem :: COMPLFLD:89
(z1 - z2)*' = z1*' - z2*';

theorem :: COMPLFLD:90
(z1 * z2)*' = z1*' * z2*';

theorem :: COMPLFLD:91
z <> the Zero of F_Complex implies z"*' = z*'";

theorem :: COMPLFLD:92
z2 <> the Zero of F_Complex implies (z1 / z2)*' = (z1*') / (z2*');

theorem :: COMPLFLD:93
|.the Zero of F_Complex.| = 0;

theorem :: COMPLFLD:94
|.z.| = 0 implies z = 0.F_Complex;

theorem :: COMPLFLD:95
0 <= |.z.|;

theorem :: COMPLFLD:96
z <> 0.F_Complex iff 0 < |.z.|;

theorem :: COMPLFLD:97
|.the unity of F_Complex.| = 1;

theorem :: COMPLFLD:98
|.-z.| = |.z.|;

theorem :: COMPLFLD:99
|.z*'.| = |.z.|;

theorem :: COMPLFLD:100
|.z1 + z2.| <= |.z1.| + |.z2.|;

theorem :: COMPLFLD:101
|.z1 - z2.| <= |.z1.| + |.z2.|;

theorem :: COMPLFLD:102
|.z1.| - |.z2.| <= |.z1 + z2.|;

theorem :: COMPLFLD:103
|.z1.| - |.z2.| <= |.z1 - z2.|;

theorem :: COMPLFLD:104
|.z1 - z2.| = |.z2 - z1.|;

theorem :: COMPLFLD:105
|.z1 - z2.| = 0 iff z1 = z2;

theorem :: COMPLFLD:106
z1 <> z2 iff 0 < |.z1 - z2.|;

theorem :: COMPLFLD:107
|.z1 - z2.| <= |.z1 - z.| + |.z - z2.|;

theorem :: COMPLFLD:108
abs(|.z1.| - |.z2.|) <= |.z1 - z2.|;

theorem :: COMPLFLD:109
|.z1*z2.| = |.z1.|*|.z2.|;

theorem :: COMPLFLD:110
z <> the Zero of F_Complex implies |.z".| = |.z.|";

theorem :: COMPLFLD:111
z2 <> the Zero of F_Complex implies |.z1.| / |.z2.| = |.z1 / z2.|;

theorem :: COMPLFLD:112
|.z * z.| = |.z * z*'.|;
```