:: The Field of Complex Numbers
:: by Anna Justyna Milewska
::
:: Received January 18, 2000
:: Copyright (c) 2000-2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, ALGSTR_0, NUMBERS, BINOP_2, MESFUNC1, COMPLEX1,
SUPINF_2, XBOOLE_0, XCMPLX_0, SUBSET_1, ORDINAL1, ARYTM_3, FUNCT_1,
RELAT_1, VECTSP_1, GROUP_1, RLVECT_1, BINOP_1, LATTICES, ARYTM_1, CARD_1,
XXREAL_0, NAT_1, NEWTON, COMPTRIG, COMPLFLD, MEMBERED;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1,
REAL_1, NAT_1, MEMBERED, FUNCT_1, XXREAL_0, COMPTRIG, BINOP_1, BINOP_2,
STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, NEWTON, VECTSP_1;
constructors BINOP_1, XXREAL_0, REAL_1, NAT_1, BINOP_2, NEWTON, COMPTRIG,
VECTSP_1, RLVECT_1, GROUP_1, MEMBERED;
registrations ORDINAL1, RELSET_1, NUMBERS, XCMPLX_0, NAT_1, COMPLEX1,
STRUCT_0, VECTSP_1, XREAL_0, CARD_1, MEMBERED;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions RLVECT_1, GROUP_1, VECTSP_1, COMPTRIG, ALGSTR_0;
equalities VECTSP_1, BINOP_1, STRUCT_0, COMPLEX1, ALGSTR_0;
expansions RLVECT_1, GROUP_1, VECTSP_1, STRUCT_0;
theorems COMPLEX1, RLVECT_1, VECTSP_1, XCMPLX_0, XCMPLX_1, BINOP_2, GROUP_1,
COMPTRIG, NEWTON, ORDINAL1, NAT_1, XREAL_1;
schemes NAT_1;
begin
definition
func F_Complex -> strict doubleLoopStr means
:Def1:
the carrier of it = COMPLEX & the addF of it = addcomplex &
the multF of it = multcomplex & 1.it = 1r & 0.it = 0c;
existence
proof
take doubleLoopStr (# COMPLEX,addcomplex,multcomplex,1r,0c #);
thus thesis;
end;
uniqueness;
end;
registration
cluster F_Complex -> non empty;
coherence by Def1;
end;
registration
cluster the carrier of F_Complex -> complex-membered;
coherence by Def1;
end;
registration
let a,b be Complex;
let x,y be Element of F_Complex;
identify x+y with a+b when x=a, y=b;
compatibility
proof
reconsider a9=a, b9=b as Element of COMPLEX by XCMPLX_0:def 2;
assume x=a & y=b;
hence x+y = addcomplex.(a9,b9) by Def1
.= a+b by BINOP_2:def 3;
end;
identify x*y with a*b when x=a, y=b;
compatibility
proof
reconsider a9=a, b9=b as Element of COMPLEX by XCMPLX_0:def 2;
assume x=a & y=b;
hence x*y = multcomplex.(a9,b9) by Def1
.= a*b by BINOP_2:def 5;
end;
end;
registration
cluster F_Complex -> well-unital;
coherence
proof
let x be Element of F_Complex;
1.F_Complex = 1r by Def1;
hence thesis;
end;
end;
Lm1: 1_F_Complex = 1r by Def1;
Lm2: 1.F_Complex = 1r by Def1;
registration
cluster F_Complex -> add-associative right_zeroed right_complementable
Abelian commutative associative left_unital right_unital distributive
almost_left_invertible non degenerated;
coherence
proof
thus F_Complex is add-associative;
thus F_Complex is right_zeroed
proof
let x be Element of F_Complex;
reconsider x1=x as Element of COMPLEX by Def1;
thus x + 0.F_Complex = (the addF of F_Complex).(x1,0c) by Def1
.= addcomplex.(x1,0c) by Def1
.= x1 + 0c by BINOP_2:def 3
.= x;
end;
thus F_Complex is right_complementable
proof
let x be Element of F_Complex;
reconsider x1=x as Element of COMPLEX by Def1;
-x1 in COMPLEX by XCMPLX_0:def 2;
then reconsider y=-x1 as Element of F_Complex by Def1;
take y;
thus thesis by Def1;
end;
thus F_Complex is Abelian;
thus F_Complex is commutative;
thus F_Complex is associative;
thus F_Complex is left_unital;
thus F_Complex is right_unital;
thus F_Complex is distributive;
thus F_Complex is almost_left_invertible
proof
let x be Element of F_Complex;
reconsider x1=x as Element of COMPLEX by Def1;
assume
A1: x <> 0.F_Complex;
x1" in COMPLEX by XCMPLX_0:def 2;
then reconsider y=x1" as Element of F_Complex by Def1;
take y;
x1<>0c by A1,Def1;
hence thesis by Lm2,XCMPLX_0:def 7;
end;
0.F_Complex <> 1.F_Complex by Def1,Lm1;
hence F_Complex is non degenerated;
end;
end;
theorem
for x1,y1 be Element of F_Complex for x2,y2 be Complex st x1 =
x2 & y1 = y2 holds x1 + y1 = x2 + y2;
theorem Th2:
for x1 be Element of F_Complex for x2 be Complex st x1 =
x2 holds - x1 = - x2
proof
let x1 be Element of F_Complex;
let x2 be Complex;
assume
A1: x1 = x2;
reconsider x2 as Element of COMPLEX by XCMPLX_0:def 2;
-x2 in COMPLEX by XCMPLX_0:def 2;
then reconsider x9=-x2 as Element of F_Complex by Def1;
x1 + x9 = 0.F_Complex by A1,Def1;
hence thesis by RLVECT_1:def 10;
end;
theorem Th3:
for x1,y1 be Element of F_Complex for x2,y2 be Complex st
x1 = x2 & y1 = y2 holds x1 - y1 = x2 - y2
proof
let x1,y1 be Element of F_Complex;
let x2,y2 be Complex;
assume that
A1: x1 = x2 and
A2: y1 = y2;
- y1 = -y2 by A2,Th2;
hence thesis by A1;
end;
theorem
for x1,y1 be Element of F_Complex for x2,y2 be Complex st x1 =
x2 & y1 = y2 holds x1 * y1 = x2 * y2;
theorem Th5:
for x1 be Element of F_Complex for x2 be Complex st x1 =
x2 & x1 <> 0.F_Complex holds x1" = x2"
proof
let x1 be Element of F_Complex;
let x2 be Complex;
reconsider x4 = x2 as Element of COMPLEX by XCMPLX_0:def 2;
x4" in COMPLEX by XCMPLX_0:def 2;
then reconsider x9= x4" as Element of F_Complex by Def1;
assume that
A1: x1 = x2 and
A2: x1 <> 0.F_Complex;
0c = 0.F_Complex by Def1;
then x1 * x9 = 1.F_Complex by A1,A2,Lm2,XCMPLX_0:def 7;
hence thesis by A2,VECTSP_1:def 10;
end;
theorem Th6:
for x1,y1 be Element of F_Complex for x2,y2 be Complex st
x1 = x2 & y1 = y2 & y1 <> 0.F_Complex holds x1/y1 = x2/y2
proof
let x1,y1 be Element of F_Complex;
let x2,y2 be Complex;
assume that
A1: x1 = x2 and
A2: y1 = y2;
assume y1 <> 0.F_Complex;
then y1" = y2" by A2,Th5;
hence thesis by A1,XCMPLX_0:def 9;
end;
theorem Th7:
0.F_Complex = 0c by Def1;
theorem
1_F_Complex = 1r by Def1;
theorem
1_F_Complex + 1_F_Complex <> 0.F_Complex by Def1,Lm1;
definition
let z be Element of F_Complex;
redefine func z *' -> Element of F_Complex;
coherence
proof
z *' in COMPLEX by XCMPLX_0:def 2;
hence thesis by Def1;
end;
end;
reserve z,z1,z2,z3,z4 for Element of F_Complex;
theorem
-z = (-1_F_Complex) * z
proof
reconsider z9=z as Element of COMPLEX by Def1;
A1: -1r = -1_F_Complex by Lm1,Th2;
thus -z = -z9 by Th2
.= (-1_F_Complex) * z by A1;
end;
theorem
z1 - -z2 = z1 + z2
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
-z2 = -z29 by Th2;
hence z1 - -z2 = z19- -z29 by Th3
.= z1 + z2;
end;
theorem
z1 = z1 + z - z
proof
reconsider z19=z1,z9=z as Element of COMPLEX by Def1;
thus z1 + z - z = z19 + z9 - z9 by Th3
.= z1;
end;
theorem
z1 = z1 - z + z
proof
reconsider z19=z1,z9=z as Element of COMPLEX by Def1;
z1 - z = z19 - z9 by Th3;
hence thesis;
end;
theorem
z1 <> 0.F_Complex & z2 <> 0.F_Complex & z1" = z2" implies z1 = z2
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
assume
A1: z1 <> 0.F_Complex;
assume
A2: z2 <> 0.F_Complex;
assume z1" = z2";
then z19" = z2" by A1,Th5
.= z29" by A2,Th5;
hence thesis by XCMPLX_1:201;
end;
theorem
z2 <> 0.F_Complex & (z1 * z2 = 1.F_Complex or z2 * z1 = 1.F_Complex)
implies z1 = z2"
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
assume
A1: z2 <> 0.F_Complex;
assume
A2: z1 * z2 = 1.F_Complex or z2 * z1 = 1.F_Complex;
per cases by A2;
suppose
A3: z1 * z2 = 1.F_Complex;
A4: z2" = z29" by A1,Th5;
z19 * z29 = 1r by A3,Def1;
hence thesis by A1,A4,Th7,XCMPLX_0:def 7;
end;
suppose
A5: z2 * z1 = 1.F_Complex;
A6: z2" = z29" by A1,Th5;
z29 * z19 = 1r by A5,Def1;
hence thesis by A1,A6,Th7,XCMPLX_0:def 7;
end;
end;
theorem
z2 <> 0.F_Complex & (z1 * z2 = z3 or z2 * z1 = z3) implies z1 = z3 *
z2" & z1 = z2" * z3
proof
reconsider z29=z2 as Element of COMPLEX by Def1;
assume
A1: z2 <> 0.F_Complex;
then
A2: z2" = z29" by Th5;
assume
A3: z1 * z2 = z3 or z2 * z1 = z3;
per cases by A3;
suppose
z1 * z2 = z3;
hence thesis by A1,A2,Th7,XCMPLX_1:203;
end;
suppose
z2 * z1 = z3;
hence thesis by A1,A2,Th7,XCMPLX_1:203;
end;
end;
theorem
(1.F_Complex)" = 1.F_Complex
proof
1.F_Complex = 1r" by Def1;
hence thesis by Th5;
end;
theorem
z1 <> 0.F_Complex & z2 <> 0.F_Complex implies (z1 * z2)" = z1" * z2"
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
assume
A1: z1 <> 0.F_Complex;
then
A2: z1" = z19" by Th5;
assume
A3: z2 <> 0.F_Complex;
then
A4: z2" = z29" by Th5;
z1 * z2 <> 0.F_Complex by A1,A3,VECTSP_1:12;
hence (z1 * z2)" = (z19 * z29)" by Th5
.= z1" * z2" by A2,A4,XCMPLX_1:204;
end;
theorem
z <> 0.F_Complex implies (-z)" = -(z")
proof
reconsider z1=z as Element of COMPLEX by Def1;
A1: -z = -z1 by Th2;
assume
A2: z <> 0.F_Complex;
then
A3: z1" = z" by Th5;
-z <> 0.F_Complex by A2,VECTSP_1:28;
hence (-z)" = (-z1)" by A1,Th5
.= -(z1") by XCMPLX_1:222
.= -(z") by A3,Th2;
end;
theorem
z1 <> 0.F_Complex & z2 <> 0.F_Complex implies z1" + z2" = (z1 + z2) *
(z1 * z2)"
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
assume
A1: z1 <> 0.F_Complex;
then
A2: z1" = z19" by Th5;
assume
A3: z2 <> 0.F_Complex;
then z1 * z2 <> 0.F_Complex by A1,VECTSP_1:12;
then
A4: (z1 * z2)" = (z19 * z29)" by Th5;
z2" = z29" by A3,Th5;
hence thesis by A1,A2,A3,A4,Th7,XCMPLX_1:211;
end;
theorem
z1 <> 0.F_Complex & z2 <> 0.F_Complex implies z1" - z2" = (z2 - z1) *
(z1 * z2)"
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
A1: z2 - z1 = z29 - z19 by Th3;
assume
A2: z1 <> 0.F_Complex;
then
A3: z1" = z19" by Th5;
assume
A4: z2 <> 0.F_Complex;
then z1 * z2 <> 0.F_Complex by A2,VECTSP_1:12;
then
A5: (z1 * z2)" = (z19 * z29)" by Th5;
z2" = z29" by A4,Th5;
hence z1" - z2" = z19" - z29" by A3,Th3
.= (z2 - z1) * (z1 * z2)" by A2,A4,A1,A5,Th7,XCMPLX_1:212;
end;
theorem
z <> 0.F_Complex implies z" = (1.F_Complex) / z
proof
reconsider z1=z as Element of COMPLEX by Def1;
A1: 1.F_Complex = 1r by Def1;
assume
A2: z <> 0.F_Complex;
hence z" = z1" by Th5
.= 1r / z1 by XCMPLX_1:215
.= (1.F_Complex) / z by A2,A1,Th6;
end;
theorem
z / (1.F_Complex) = z
proof
reconsider z1=z as Element of COMPLEX by Def1;
1.F_Complex = 1r by Def1;
hence z / (1.F_Complex) = z1 / 1r by Th6
.= z;
end;
theorem
z <> 0.F_Complex implies z / z = 1.F_Complex
proof
reconsider z1=z as Element of COMPLEX by Def1;
assume
A1: z <> 0.F_Complex;
hence z / z = z1 / z1 by Th6
.= 1r by A1,Th7,XCMPLX_1:60
.= 1.F_Complex by Def1;
end;
theorem
z <> 0.F_Complex implies (0.F_Complex) / z = 0.F_Complex;
theorem Th26:
z2 <> 0.F_Complex & z1 / z2 = 0.F_Complex implies z1 = 0. F_Complex
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
assume
A1: z2 <> 0.F_Complex;
assume z1 / z2 = 0.F_Complex;
then z19 / z29 = 0.F_Complex by A1,Th6;
hence thesis by A1,Th7;
end;
theorem
z2 <> 0.F_Complex & z4 <> 0.F_Complex implies (z1 / z2) * (z3 / z4) =
(z1 * z3) / (z2 * z4)
proof
reconsider z19=z1,z29=z2,z39=z3,z49=z4 as Element of COMPLEX by Def1;
assume
A1: z2 <> 0.F_Complex;
assume
A2: z4 <> 0.F_Complex;
then
A3: z2 * z4 <> 0.F_Complex by A1,VECTSP_1:12;
A4: z39 / z49 = z3 / z4 by A2,Th6;
z19 / z29 = z1 / z2 by A1,Th6;
hence (z1 / z2) * (z3 / z4) = (z19 * z39) / (z29 * z49) by A4,XCMPLX_1:76
.= (z1 * z3) / (z2 * z4) by A3,Th6;
end;
theorem
z2 <> 0.F_Complex implies z * (z1 / z2) = (z * z1) / z2;
theorem
z2 <> 0.F_Complex & z1 / z2 = 1.F_Complex implies z1 = z2
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
assume
A1: z2 <> 0.F_Complex;
assume z1 / z2 = 1.F_Complex;
then z19 / z29 = 1.F_Complex by A1,Th6;
then z19 / z29 = 1 by Def1;
hence thesis by XCMPLX_1:58;
end;
theorem
z <> 0.F_Complex implies z1 = (z1 * z) / z
proof
reconsider z19=z1,z9=z as Element of COMPLEX by Def1;
assume
A1: z <> 0.F_Complex;
hence z1 = (z19 * z9) / z9 by Th7,XCMPLX_1:89
.= (z1 * z) / z by A1,Th6;
end;
theorem
z1 <> 0.F_Complex & z2 <> 0.F_Complex implies (z1 / z2)" = z2 / z1
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
assume
A1: z1 <> 0.F_Complex;
assume
A2: z2 <> 0.F_Complex;
then
A3: z19 / z29 = z1 / z2 by Th6;
z1 / z2 <> 0.F_Complex by A1,A2,Th26;
hence (z1 / z2)" = (z19 / z29)" by A3,Th5
.= z29 / z19 by XCMPLX_1:213
.= z2 / z1 by A1,Th6;
end;
theorem
z1 <> 0.F_Complex & z2 <> 0.F_Complex implies (z1" / z2") = z2 / z1
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
assume
A1: z1 <> 0.F_Complex;
assume z2 <> 0.F_Complex;
then
A2: z2" = z29" & z2" <> 0.F_Complex by Th5,VECTSP_1:25;
z1" = z19" by A1,Th5;
hence (z1" / z2") = (z19" / z29") by A2,Th6
.= z29 / z19 by XCMPLX_1:214
.= z2 / z1 by A1,Th6;
end;
theorem
z2 <> 0.F_Complex implies z1 / z2" = z1 * z2
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
assume z2 <> 0.F_Complex;
then z2" <> 0.F_Complex & z2" = z29" by Th5,VECTSP_1:25;
hence z1 / z2" = z19 / z29" by Th6
.= z1 * z2 by XCMPLX_1:219;
end;
theorem
z1 <> 0.F_Complex & z2 <> 0.F_Complex implies z1" / z2 = (z1 * z2)"
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
assume
A1: z1 <> 0.F_Complex;
assume
A2: z2 <> 0.F_Complex;
then
A3: z1 * z2 <> 0.F_Complex by A1,VECTSP_1:12;
z1" = z19" by A1,Th5;
hence z1" / z2 = z19" / z29 by A2,Th6
.= (z19 * z29)" by XCMPLX_1:221
.= (z1 * z2)" by A3,Th5;
end;
theorem
z1 <> 0.F_Complex & z2 <> 0.F_Complex implies z1"* (z / z2) = z / (z1 * z2)
proof
reconsider z19=z1,z29=z2,z9=z as Element of COMPLEX by Def1;
assume
A1: z1 <> 0.F_Complex;
assume
A2: z2 <> 0.F_Complex;
then
A3: z1 * z2 <> 0.F_Complex by A1,VECTSP_1:12;
A4: z9 / z29 = z / z2 by A2,Th6;
z1" = z19" by A1,Th5;
hence z1"* (z / z2) = z9 / (z19 * z29) by A4,XCMPLX_1:220
.= z / (z1 * z2) by A3,Th6;
end;
theorem
z <> 0.F_Complex & z2 <> 0.F_Complex implies (z1 / z2) = (z1 * z) / (
z2 * z) & (z1 / z2) = (z * z1) / (z * z2)
proof
reconsider z19=z1,z29=z2,z9=z as Element of COMPLEX by Def1;
assume
A1: z <> 0.F_Complex;
assume
A2: z2 <> 0.F_Complex;
then
A3: z2 * z <> 0.F_Complex by A1,VECTSP_1:12;
thus (z1 / z2) = (z19 / z29) by A2,Th6
.= (z19 * z9) / (z29 * z9) by A1,Th7,XCMPLX_1:91
.= (z1 * z) / (z2 * z) by A3,Th6;
hence thesis;
end;
theorem
z2 <> 0.F_Complex & z3 <> 0.F_Complex implies z1 / (z2 * z3) = z1 / z2 / z3
proof
reconsider z19=z1,z29=z2,z39=z3 as Element of COMPLEX by Def1;
assume
A1: z2 <> 0.F_Complex;
then
A2: z1 / z2 = z19 / z29 by Th6;
assume
A3: z3 <> 0.F_Complex;
then z2 * z3 <> 0.F_Complex by A1,VECTSP_1:12;
hence z1 / (z2 * z3) = z19 / (z29 * z39) by Th6
.= z19 / z29 / z39 by XCMPLX_1:78
.= z1 / z2 / z3 by A3,A2,Th6;
end;
theorem
z2 <> 0.F_Complex & z3 <> 0.F_Complex implies (z1 * z3) / z2 = z1 / (
z2 / z3)
proof
reconsider z19=z1,z29=z2,z39=z3 as Element of COMPLEX by Def1;
assume
A1: z2 <> 0.F_Complex;
assume
A2: z3 <> 0.F_Complex;
then
A3: z2 / z3 <> 0.F_Complex by A1,Th26;
A4: z2 / z3 = z29 / z39 by A2,Th6;
thus (z1 * z3) / z2 = (z19 * z39) / z29 by A1,Th6
.= z19 / (z29 / z39) by XCMPLX_1:77
.= z1 / (z2 / z3) by A4,A3,Th6;
end;
theorem
z2 <> 0.F_Complex & z3 <> 0.F_Complex & z4 <> 0.F_Complex implies (z1
/ z2) / (z3 / z4) = (z1 * z4) / (z2 * z3)
proof
reconsider z19=z1,z29=z2,z39=z3,z49=z4 as Element of COMPLEX by Def1;
assume
A1: z2 <> 0.F_Complex;
then
A2: z1 / z2 = z19 / z29 by Th6;
assume
A3: z3 <> 0.F_Complex;
then
A4: z2 * z3 <> 0.F_Complex by A1,VECTSP_1:12;
assume
A5: z4 <> 0.F_Complex;
then
A6: z3 / z4 = z39 / z49 by Th6;
z3 / z4 <> 0.F_Complex by A3,A5,Th26;
hence (z1 / z2) / (z3 / z4) = (z19 / z29) / (z39 / z49) by A2,A6,Th6
.= (z19 * z49) / (z29 * z39) by XCMPLX_1:84
.= (z1 * z4) / (z2 * z3) by A4,Th6;
end;
theorem
z2 <> 0.F_Complex & z4 <> 0.F_Complex implies z1 / z2 + z3 / z4 = (z1
* z4 + z3 * z2) / (z2 * z4)
proof
reconsider z19=z1,z29=z2,z39=z3,z49=z4 as Element of COMPLEX by Def1;
assume
A1: z2 <> 0.F_Complex;
then
A2: z1 / z2 = z19 / z29 by Th6;
assume
A3: z4 <> 0.F_Complex;
then
A4: z2 * z4 <> 0.F_Complex by A1,VECTSP_1:12;
z3 / z4 = z39 / z49 by A3,Th6;
hence
z1 / z2 + z3 / z4 = (z19 * z49 + z39 * z29) / (z29 * z49) by A1,A3,A2,Th7,
XCMPLX_1:116
.= (z1 * z4 + z3 * z2) / (z2 * z4) by A4,Th6;
end;
theorem
z <> 0.F_Complex implies z1 / z + z2 / z = (z1 + z2) / z;
theorem
z2 <> 0.F_Complex implies -(z1 / z2) = (-z1) / z2 & -(z1 / z2) = z1 / (-z2)
proof
assume
A1: z2 <> 0.F_Complex;
then
A2: -z2 <> 0.F_Complex by VECTSP_1:28;
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
A3: -z1 = -z19 by Th2;
z1 / z2 = z19 / z29 by A1,Th6;
hence -(z1 / z2) = -(z19 / z29) by Th2
.= (-z19) / z29 by XCMPLX_1:187
.= (-z1) / z2 by A3,A1,Th6;
A4: -z2 = -z29 by Th2;
z1 / z2 = z19 / z29 by A1,Th6;
hence -(z1 / z2) = -(z19 / z29) by Th2
.= z19 / -(z29) by XCMPLX_1:188
.= z1 / -z2 by A4,A2,Th6;
end;
theorem
z2 <> 0.F_Complex implies z1 / z2 = (-z1) / (-z2)
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
assume
A1: z2 <> 0.F_Complex;
then
A2: -z2 <> 0.F_Complex by VECTSP_1:28;
A3: -z19 = -z1 & -z29 = -z2 by Th2;
thus z1 / z2 = z19 / z29 by A1,Th6
.= (-z19) / (-z29) by XCMPLX_1:191
.= (-z1) / (-z2) by A2,A3,Th6;
end;
theorem
z2 <> 0.F_Complex & z4 <> 0.F_Complex implies z1 / z2 - z3 / z4 = (z1
* z4 - z3 * z2) / (z2 * z4)
proof
reconsider z19=z1,z29=z2,z39=z3,z49=z4 as Element of COMPLEX by Def1;
A1: z1 * z4 - z3 * z2 = z19 * z49 - z39 * z29 by Th3;
assume
A2: z2 <> 0.F_Complex;
then
A3: z19 / z29 = z1 / z2 by Th6;
assume
A4: z4 <> 0.F_Complex;
then
A5: z2 * z4 <> 0.F_Complex by A2,VECTSP_1:12;
z39 / z49 = z3 / z4 by A4,Th6;
hence z1 / z2 - z3 / z4 = z19 / z29 - z39 / z49 by A3,Th3
.= (z19 * z49 - z39 * z29) / (z29 * z49) by A2,A4,Th7,XCMPLX_1:130
.= (z1 * z4 - z3 * z2) / (z2 * z4) by A5,A1,Th6;
end;
theorem
z <> 0.F_Complex implies z1 / z - z2 / z = (z1 - z2) / z
proof
reconsider z9=z,z19=z1,z29=z2 as Element of COMPLEX by Def1;
A1: z19 - z29 = z1 - z2 by Th3;
assume
A2: z <> 0.F_Complex;
then z19 / z9 = z1 / z & z29 / z9 = z2 / z by Th6;
hence z1 / z - z2 / z = z19 / z9 - z29 / z9 by Th3
.= (z19 - z29) / z9 by XCMPLX_1:120
.= (z1 - z2) / z by A2,A1,Th6;
end;
theorem
z2 <> 0.F_Complex & (z1 * z2 = z3 or z2 * z1 = z3) implies z1 = z3 / z2
proof
reconsider z39=z3,z29=z2 as Element of COMPLEX by Def1;
assume
A1: z2 <> 0.F_Complex;
assume
A2: z1 * z2 = z3 or z2 * z1 = z3;
per cases by A2;
suppose
z1 * z2 = z3;
hence z1 = z39 / z29 by A1,Th7,XCMPLX_1:89
.= z3 / z2 by A1,Th6;
end;
suppose
z2 * z1 = z3;
hence z1 = z39 / z29 by A1,Th7,XCMPLX_1:89
.= z3 / z2 by A1,Th6;
end;
end;
theorem
(0.F_Complex)*' = 0.F_Complex
proof
0.F_Complex = 0c by Def1;
hence thesis;
end;
theorem Th48:
z*' = 0.F_Complex implies z = 0.F_Complex
proof
assume z*' = 0.F_Complex;
then z*' = 0c by Def1;
then z = 0c by COMPLEX1:29;
hence thesis by Def1;
end;
theorem
(1.F_Complex)*' = 1.F_Complex
proof
1.F_Complex = 1r by Def1;
hence thesis;
end;
theorem
z*'*' = z;
theorem
(z1 + z2)*' = z1*' + z2*' by COMPLEX1:32;
theorem
(-z)*' = -(z*')
proof
reconsider z9=z as Element of COMPLEX by Def1;
-z = -z9 by Th2;
hence (-z)*' = -(z9*') by COMPLEX1:33
.= -(z*') by Th2;
end;
theorem
(z1 - z2)*' = z1*' - z2*'
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
z19 - z29 = z1 - z2 by Th3;
hence (z1 - z2)*' = z19*' - z29*' by COMPLEX1:34
.= z1*' - z2*' by Th3;
end;
theorem
(z1 * z2)*' = z1*' * z2*' by COMPLEX1:35;
theorem
z <> 0.F_Complex implies z"*' = z*'"
proof
reconsider z1=z as Element of COMPLEX by Def1;
assume
A1: z <> 0.F_Complex;
then
A2: z*' <> 0.F_Complex by Th48;
z" = z1" by A1,Th5;
hence z"*' = z1*'" by COMPLEX1:36
.= z*'" by A2,Th5;
end;
theorem
z2 <> 0.F_Complex implies (z1 / z2)*' = (z1*') / (z2*')
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
assume
A1: z2 <> 0.F_Complex;
then
A2: z2*' <> 0.F_Complex by Th48;
z19 / z29 = z1 / z2 by A1,Th6;
hence (z1 / z2)*' = (z19*') / (z29*') by COMPLEX1:37
.= (z1*') / (z2*') by A2,Th6;
end;
theorem
|.0.F_Complex.| = 0 by Def1,COMPLEX1:44;
theorem
|.z.| = 0 implies z = 0.F_Complex by Th7;
theorem
z <> 0.F_Complex iff 0 < |.z.| by Th7,COMPLEX1:47;
theorem
|.1.F_Complex.| = 1 by Def1,COMPLEX1:48;
theorem
|.-z.| = |.z.|
proof
reconsider z1=z as Element of COMPLEX by Def1;
-z1 = -z by Th2;
hence thesis by COMPLEX1:52;
end;
theorem
|.z1 + z2.| <= |.z1.| + |.z2.| by COMPLEX1:56;
theorem
|.z1 - z2.| <= |.z1.| + |.z2.|
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
z19 - z29 = z1 - z2 by Th3;
hence thesis by COMPLEX1:57;
end;
theorem
|.z1.| - |.z2.| <= |.z1 + z2.| by COMPLEX1:58;
theorem
|.z1.| - |.z2.| <= |.z1 - z2.|
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
z19 - z29 = z1 - z2 by Th3;
hence thesis by COMPLEX1:59;
end;
theorem
|.z1 - z2.| = |.z2 - z1.|
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
z29 - z19 = z2 - z1 & z19 - z29 = z1 - z2 by Th3;
hence thesis by COMPLEX1:60;
end;
theorem
|.z1 - z2.| = 0 iff z1 = z2
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
thus |.z1 - z2.| = 0 implies z1 = z2
proof
assume
A1: |.z1 - z2.| = 0;
z1 - z2 = z19 - z29 by Th3;
hence thesis by A1,COMPLEX1:61;
end;
assume
A2: z1 = z2;
z19 - z29 = z1 - z2 by Th3;
hence thesis by A2;
end;
theorem
z1 <> z2 iff 0 < |.z1 - z2.|
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
thus z1 <> z2 implies 0 < |.z1 - z2.|
proof
assume
A1: z1 <> z2;
z1 - z2 = z19 - z29 by Th3;
hence thesis by A1,COMPLEX1:62;
end;
assume
A2: 0 < |.z1 - z2.|;
z1 - z2 = z19 - z29 by Th3;
hence thesis by A2;
end;
theorem
|.z1 - z2.| <= |.z1 - z.| + |.z - z2.|
proof
reconsider z9=z,z19=z1,z29=z2 as Element of COMPLEX by Def1;
A1: z9 - z29 = z - z2 by Th3;
|.z19 - z29.| = |.z1 - z2.| & |.z19 - z9.| = |.z1 - z.| by Th3;
hence thesis by A1,COMPLEX1:63;
end;
theorem
|.|.z1.| - |.z2.|.| <= |.z1 - z2.|
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
z19 - z29 = z1 - z2 by Th3;
hence thesis by COMPLEX1:64;
end;
theorem
|.z1*z2.| = |.z1.|*|.z2.| by COMPLEX1:65;
theorem
z <> 0.F_Complex implies |.z".| = |.z.|"
proof
reconsider z1=z as Element of COMPLEX by Def1;
assume z <> 0.F_Complex;
then z" = z1" by Th5;
hence thesis by COMPLEX1:66;
end;
theorem
z2 <> 0.F_Complex implies |.z1.| / |.z2.| = |.z1 / z2.|
proof
reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
assume z2 <> 0.F_Complex;
then z19 / z29 = z1 / z2 by Th6;
hence thesis by COMPLEX1:67;
end;
begin :: Addenda
:: from COMPTRIG, 2006.08.12, A.T.
scheme
Regrwithout0 { P[Nat] } : P[1]
provided
A1: ex k be non zero Element of NAT st P[k] and
A2: for k be non zero Element of NAT st k <> 1 & P[k]
ex n be non zero Element of NAT st n < k & P[n]
proof
consider t be non zero Element of NAT such that
A3: P[t] by A1;
defpred R[Nat] means P[$1+1];
A4: now
let k be Nat;
assume that
A5: k <> 0 and
A6: R[k];
reconsider k1=k+1 as non zero Element of NAT;
k > 0 by A5,NAT_1:3;
then k+1 > 0+1 by XREAL_1:6;
then consider n be non zero Element of NAT such that
A7: n < k1 and
A8: P[n] by A2,A6;
consider l be Nat such that
A9: n = l+1 by NAT_1:6;
take l;
thus l < k by A7,A9,XREAL_1:6;
thus R[l] by A8,A9;
end;
ex s be Nat st t = s+1 by NAT_1:6;
then
A10: ex k be Nat st R[k] by A3;
R[0] from NAT_1:sch 7(A10,A4);
hence thesis;
end;
theorem Th74:
for e being Element of F_Complex, n be Nat holds
(power F_Complex).(e,n) = e|^n
proof
let e be Element of F_Complex;
defpred P[Nat] means (power F_Complex).(e,$1) = e|^$1;
A1: now
let n be Nat;
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
reconsider p = (power F_Complex).(e,n9) as Element of F_Complex;
assume
A2: P[n];
(power F_Complex).(e,n+1) = p*e by GROUP_1:def 7
.= e|^(n+1) by A2,NEWTON:6;
hence P[n+1];
end;
(power F_Complex).(e,0) = 1_F_Complex by GROUP_1:def 7
.= 1 by Def1;
then
A3: P[0] by NEWTON:4;
thus for n being Nat holds P[n] from NAT_1:sch 2(A3,A1);
end;
definition
let x be Element of F_Complex;
let n be non zero Element of NAT;
redefine mode CRoot of n,x -> Element of F_Complex means
:Def2:
(power F_Complex).(it,n) = x;
coherence
proof
let e be CRoot of n,x;
e is Element of COMPLEX by XCMPLX_0:def 2;
hence thesis by Def1;
end;
compatibility
proof
let e be Element of F_Complex;
thus e is CRoot of n,x implies (power F_Complex).(e,n) = x
proof
assume e is CRoot of n,x;
then e|^n = x by COMPTRIG:def 2;
hence thesis by Th74;
end;
assume (power F_Complex).(e,n) = x;
hence e|^n = x by Th74;
end;
end;
theorem
for x be Element of F_Complex for v be CRoot of 1,x holds v = x
proof
let x be Element of F_Complex;
let v be CRoot of 1,x;
(power F_Complex).(v,1) = x by Def2;
hence thesis by GROUP_1:50;
end;
theorem
for n be non zero Element of NAT for v be CRoot of n,0.F_Complex
holds v = 0.F_Complex
proof
let n be non zero Element of NAT;
let v be CRoot of n,0.F_Complex;
defpred P[Element of omega] means (power F_Complex).(v,$1) = 0.F_Complex;
A1: now
let k be non zero Element of NAT;
assume that
A2: k <> 1 and
A3: P[k];
consider t be Nat such that
A4: k = t+1 by NAT_1:6;
reconsider t as Element of NAT by ORDINAL1:def 12;
reconsider t as non zero Element of NAT by A2,A4;
take t;
thus t < k by A4,NAT_1:13;
(power F_Complex).(v,k) = (power F_Complex).(v,t)*v by A4,GROUP_1:def 7;
then (power F_Complex).(v,t) = 0.F_Complex or v = 0.F_Complex by A3,
VECTSP_1:12;
hence P[t] by NAT_1:3,VECTSP_1:36;
end;
A5: ex n be non zero Element of NAT st P[n]
proof
take n;
thus thesis by Def2;
end;
P[1] from Regrwithout0(A5,A1);
hence thesis by GROUP_1:50;
end;
theorem
for n be non zero Element of NAT for x be Element of F_Complex for v
be CRoot of n,x st v = 0.F_Complex holds x = 0.F_Complex
proof
let n be non zero Element of NAT;
let x be Element of F_Complex;
let v be CRoot of n,x;
assume v = 0.F_Complex;
then (power F_Complex).(0.F_Complex,n) = x by Def2;
hence thesis by NAT_1:3,VECTSP_1:36;
end;