Copyright (c) 1990 Association of Mizar Users
environ
vocabulary ARYTM, ARYTM_3, SQUARE_1, ARYTM_1, RELAT_1, ABSVALUE, COMPLEX1,
FUNCT_2, BOOLE, FUNCT_1, FUNCOP_1, ORDINAL2, XCMPLX_0, OPPCAT_1,
ORDINAL1, XREAL_0;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ARYTM_3, ARYTM_0, NUMBERS,
XCMPLX_0, XREAL_0, REAL_1, ABSVALUE, SQUARE_1, RELAT_1, FUNCT_1, FUNCT_2,
FUNCT_4;
constructors REAL_1, ABSVALUE, SQUARE_1, FRAENKEL, ARYTM_2, FUNCT_4, MEMBERED,
XBOOLE_0, ARYTM_0;
clusters XREAL_0, SQUARE_1, FRAENKEL, RELSET_1, FUNCT_2, XCMPLX_0, MEMBERED,
ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
theorems AXIOMS, REAL_1, ABSVALUE, SQUARE_1, XREAL_0, FUNCT_2, XBOOLE_0,
TARSKI, NUMBERS, ENUMSET1, FUNCT_4, XCMPLX_0, ORDINAL2, ORDINAL1,
XCMPLX_1, ARYTM_0;
begin
reserve a,b,c,d for Element of REAL;
:: Auxiliary theorems
Lm1: one = succ 0 by ORDINAL2:def 4 .= 1;
Lm2: 2 = succ 1
.= succ 0 \/ {1} by ORDINAL1:def 1
.= {} \/ {0} \/ {1} by ORDINAL1:def 1
.= {0,one} by Lm1,ENUMSET1:41;
canceled;
theorem Th2:
for a, b being real number holds
a^2 + b^2 = 0 iff a = 0 & b = 0
proof
let a, b be real number;
thus a^2 + b^2 = 0 implies a = 0 & b = 0
proof assume
A1: a^2 + b^2 = 0;
A2: 0 <= a^2 & 0 <= b^2 by SQUARE_1:72;
assume a <> 0 or b <> 0;
then a^2 <> 0 or b^2 <> 0 by SQUARE_1:73;
then 0 + 0 < a^2 + b^2 by A2,REAL_1:67;
hence contradiction by A1;
end;
assume a = 0 & b = 0;
hence thesis by SQUARE_1:60;
end;
Lm3: 0 <= a^2 + b^2
proof 0<=a^2 & 0<=b^2 by SQUARE_1:72; then 0 +0 <=a^2 + b^2 by REAL_1:55;
hence thesis;
end;
:: Complex Numbers
definition
cluster -> complex Element of COMPLEX;
coherence;
end;
definition let z be complex number;
canceled;
func Re z means
:Def2: it = z if z in REAL
otherwise
ex f being Function of 2,REAL st z = f & it = f.0;
existence
proof
thus z in REAL implies ex IT being set st IT = z;
assume A1: not z in REAL;
z in COMPLEX by XCMPLX_0:def 2;
then z in Funcs(2,REAL) \ { x where x is Element of Funcs(2,REAL): x.1 = 0}
by A1,Lm1,Lm2,NUMBERS:def 2,XBOOLE_0:def 2;
then z in Funcs(2,REAL) by XBOOLE_0:def 4;
then reconsider f = z as Function of 2, REAL by FUNCT_2:121;
take f.0, f;
thus thesis;
end;
uniqueness;
consistency;
func Im z means
:Def3: it = 0 if z in REAL
otherwise
ex f being Function of 2,REAL st z = f & it = f.1;
existence
proof
thus z in REAL implies ex IT being set st IT = 0;
assume A2: not z in REAL;
z in COMPLEX by XCMPLX_0:def 2;
then z in Funcs(2,REAL) \ { x where x is Element of Funcs(2,REAL): x.1 = 0}
by A2,Lm1,Lm2,NUMBERS:def 2,XBOOLE_0:def 2;
then z in Funcs(2,REAL) by XBOOLE_0:def 4;
then reconsider f = z as Function of 2, REAL by FUNCT_2:121;
take f.1, f;
thus thesis;
end;
uniqueness;
consistency;
end;
definition let z be complex number;
cluster Re z -> real;
coherence
proof
per cases;
suppose
A1: z in REAL;
then Re z = z by Def2;
hence thesis by A1,XREAL_0:def 1;
suppose not z in REAL;
then consider f being Function of 2,REAL such that z = f and
A2: Re z = f.0 by Def2;
0 in 2 by Lm2,TARSKI:def 2;
then f.0 in REAL by FUNCT_2:7;
hence thesis by A2,XREAL_0:def 1;
end;
cluster Im z -> real;
coherence
proof
per cases;
suppose z in REAL;
hence thesis by Def3;
suppose not z in REAL;
then consider f being Function of 2,REAL such that z = f and
A3: Im z = f.1 by Def3;
1 in 2 by Lm1,Lm2,TARSKI:def 2;
then f.1 in REAL by FUNCT_2:7;
hence thesis by A3,XREAL_0:def 1;
end;
end;
definition let z be complex number;
redefine func Re z -> Real;
coherence by XREAL_0:def 1;
redefine func Im z -> Real;
coherence by XREAL_0:def 1;
end;
canceled 2;
theorem Th5:
for f being Function of 2,REAL
ex a,b st f = (0,1)-->(a,b)
proof let f be Function of 2,REAL;
0 in 2 & 1 in 2 by Lm1,Lm2,TARSKI:def 2;
then reconsider a = f.0, b = f.1 as Element of REAL by FUNCT_2:7;
take a,b;
dom f = {0,1} by Lm1,Lm2,FUNCT_2:def 1;
hence f = (0,1)-->(a,b) by FUNCT_4:69;
end;
canceled;
theorem Th7:
Re [*a,b*] = a & Im [*a,b*] = b
proof
reconsider a' =a, b' = b as Element of REAL;
thus Re [*a,b*] = a
proof per cases;
suppose b = 0;
then [*a,b*] = a by ARYTM_0:def 7;
hence thesis by Def2;
suppose b <> 0;
then A1: [*a,b*] = (0,1)-->(a',b') by Lm1,ARYTM_0:def 7;
then reconsider f = [*a,b*] as Function of 2, REAL by Lm1,Lm2;
A2: not [*a,b*] in REAL by A1,Lm1,ARYTM_0:10;
f.0 = a by A1,FUNCT_4:66;
hence thesis by A2,Def2;
end;
per cases;
suppose
A3: b = 0;
then [*a,b*] = a by ARYTM_0:def 7;
hence thesis by A3,Def3;
suppose b <> 0;
then A4: [*a,b*] = (0,1)-->(a',b') by Lm1,ARYTM_0:def 7;
then reconsider f = [*a,b*] as Function of 2, REAL by Lm1,Lm2;
A5: not [*a,b*] in REAL by A4,Lm1,ARYTM_0:10;
f.1 = b by A4,FUNCT_4:66;
hence thesis by A5,Def3;
end;
theorem Th8:
for z being complex number holds [*Re z, Im z*] = z
proof
let z be complex number;
A1: z in COMPLEX by XCMPLX_0:def 2;
per cases;
suppose
A2: z in REAL;
then Im z = 0 by Def3;
hence [*Re z, Im z*] = Re z by ARYTM_0:def 7
.= z by A2,Def2;
suppose
A3: not z in REAL;
then consider f being Function of 2,REAL such that
A4: z = f and
A5: Im z = f.1 by Def3;
consider f being Function of 2,REAL such that
A6: z = f and
A7: Re z = f.0 by A3,Def2;
consider a,b such that
A8: z = (0,1)-->(a,b) by A4,Th5;
A9: Re z = a by A6,A7,A8,FUNCT_4:66;
A10: Im z = b by A4,A5,A8,FUNCT_4:66;
z in Funcs(2,REAL) \ { x where x is Element of Funcs(2,REAL): x.1 = 0}
by A1,A3,Lm1,Lm2,NUMBERS:def 2,XBOOLE_0:def 2;
then A11: not z in { x where x is Element of Funcs(2,REAL): x.1 = 0}
by XBOOLE_0:def 4;
reconsider f = z as Element of Funcs(2,REAL)
by A8,Lm1,Lm2,FUNCT_2:11;
f.1 <> 0 by A11;
then b <> 0 by A8,FUNCT_4:66;
hence [*Re z, Im z*] = z by A8,A9,A10,Lm1,ARYTM_0:def 7;
end;
theorem Th9:
for z1, z2 being complex number st
Re z1 = Re z2 & Im z1 = Im z2 holds z1 = z2
proof
let z1, z2 be complex number;
assume Re z1 = Re z2 & Im z1 = Im z2;
hence z1 = [*Re z2,Im z2*] by Th8 .= z2 by Th8;
end;
definition let z1,z2 be complex number;
canceled;
redefine pred z1 = z2 means Re z1 = Re z2 & Im z1 = Im z2;
compatibility by Th9;
end;
definition
func 0c -> Element of COMPLEX equals
:Def6: 0;
correctness by XCMPLX_0:def 2;
func 1r -> Element of COMPLEX equals
:Def7: 1;
correctness by XCMPLX_0:def 2;
redefine func <i> -> Element of COMPLEX equals
:Def8: [*0,1*];
coherence by XCMPLX_0:def 2;
compatibility by Lm1,ARYTM_0:def 7,XCMPLX_0:def 1;
end;
L0: 0c = [*0,0*] by ARYTM_0:def 7,Def6;
L1: 1r = [*1,0*] by ARYTM_0:def 7,Def7;
definition
cluster 0c -> zero;
coherence by Def6;
end;
canceled 2;
theorem Th12:
Re(0c) = 0 & Im(0c) = 0 by Th7,L0;
theorem Th13:
for z being complex number holds
z = 0c iff (Re z)^2 + (Im z)^2 = 0
proof
let z be complex number;
set r = Re z , i = Im z;
thus z=0c implies r^2 + i^2 = 0 by Th2,Th12;
assume 0 = r^2+i^2; then r = 0 & i = 0 by Th2;
hence thesis by Th9,Th12;
end;
theorem Th14:
0 = 0c;
theorem Th15:
Re(1r) = 1 & Im(1r) = 0 by Th7,L1;
canceled;
theorem Th17:
Re(<i>) = 0 & Im(<i>) = 1 by Def8,Th7;
Lm4: for x being real number, x1,x2 being Element of REAL st x = [*x1,x2*]
holds x2 = 0 & x = x1
proof let x be real number, x1,x2 being Element of REAL;
assume
A1: x = [*x1,x2*];
A2: x in REAL by XREAL_0:def 1;
hereby assume x2 <> 0;
then x = (0,one) --> (x1,x2) by A1,ARYTM_0:def 7;
hence contradiction by A2,ARYTM_0:10;
end;
hence x = x1 by A1,ARYTM_0:def 7;
end;
Lm5:
for x',y' being Element of REAL, x,y being real number st x' = x & y' = y
holds +(x',y') = x + y
proof let x',y' be Element of REAL, x,y be real number such that
A1: x' = x & y' = y;
consider x1,x2,y1,y2 being Element of REAL such that
A2: x = [* x1,x2 *] and
A3: y = [*y1,y2*] and
A4: x+y = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
A5: x = x1 & y = y1 by A2,A3,Lm4;
x2 = 0 & y2 = 0 by A2,A3,Lm4;
then +(x2,y2) = 0 by ARYTM_0:13;
hence +(x',y') = x + y by A1,A4,A5,ARYTM_0:def 7;
end;
Lm6:
for x being Element of REAL holds opp x = -x
proof let x be Element of REAL;
+(x,opp x) = 0 by ARYTM_0:def 4;
then x + opp x = 0 by Lm5;
hence opp x = -x by XCMPLX_0:def 6;
end;
Lm7:
for x',y' being Element of REAL, x,y being real number st x' = x & y' = y
holds *(x',y') = x * y
proof let x',y' be Element of REAL, x,y be real number such that
A1: x' = x & y' = y;
consider x1,x2,y1,y2 being Element of REAL such that
A2: x = [* x1,x2 *] and
A3: y = [*y1,y2*] and
A4: x*y = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *]
by XCMPLX_0:def 5;
A5: x = x1 & y = y1 by A2,A3,Lm4;
A6: x2 = 0 & y2 = 0 by A2,A3,Lm4;
then *(x1,y2) = 0 & *(x2,y1) = 0 by ARYTM_0:14;
then A7: +(*(x1,y2),*(x2,y1)) = 0 by ARYTM_0:13;
thus *(x',y') = +(*(x1,y1),0) by A1,A5,ARYTM_0:13
.= +(*(x1,y1),*(opp x2,y2)) by A6,ARYTM_0:14
.= +(*(x1,y1),opp*(x2,y2)) by ARYTM_0:17
.= x * y by A4,A7,ARYTM_0:def 7;
end;
Lm8:
for x,y,z being Element of COMPLEX st z = x + y
holds Re z = Re x + Re y
proof let x,y,z be Element of COMPLEX such that
A1: z = x + y;
consider x1,x2,y1,y2 being Element of REAL such that
A2: x = [*x1,x2*] and
A3: y = [*y1,y2*] and
A4: x + y = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
A5: Re x = x1 & Re y = y1 by A2,A3,Th7;
thus Re z = +(x1,y1) by A1,A4,Th7
.= Re x + Re y by A5,Lm5;
end;
Lm9:
for x,y,z being Element of COMPLEX st z = x+y
holds Im z = Im x + Im y
proof let x,y,z be Element of COMPLEX such that
A1: z = x+y;
consider x1,x2,y1,y2 being Element of REAL such that
A2: x = [*x1,x2*] and
A3: y = [*y1,y2*] and
A4: x + y = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
A5: Im x = x2 & Im y = y2 by A2,A3,Th7;
thus Im z = +(x2,y2) by A1,A4,Th7
.= Im x + Im y by A5,Lm5;
end;
Lm10:
for x,y,z being Element of COMPLEX st z = x * y
holds Re z = Re x * Re y - Im x * Im y
proof let x,y,z be Element of COMPLEX such that
A1: z = x * y;
consider x1,x2,y1,y2 being Element of REAL such that
A2: x = [*x1,x2*] and
A3: y = [*y1,y2*] and
A4: x * y = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *]
by XCMPLX_0:def 5;
A5: Re x = x1 & Re y = y1 by A2,A3,Th7;
A6: Im x = x2 & Im y = y2 by A2,A3,Th7;
thus Re z = +(*(x1,y1),opp*(x2,y2)) by A1,A4,Th7
.= *(x1,y1) + opp*(x2,y2) by Lm5
.= x1*y1 + opp*(x2,y2) by Lm7
.= x1*y1 + -*(x2,y2) by Lm6
.= x1*y1 - *(x2,y2) by XCMPLX_0:def 8
.= Re x * Re y - Im x * Im y by A5,A6,Lm7;
end;
Lm11:
for x,y,z being Element of COMPLEX st z = x*y
holds Im z = Re x * Im y + Im x * Re y
proof let x,y,z be Element of COMPLEX such that
A1: z = x*y;
consider x1,x2,y1,y2 being Element of REAL such that
A2: x = [*x1,x2*] and
A3: y = [*y1,y2*] and
A4: x * y = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *]
by XCMPLX_0:def 5;
A5: Im x = x2 & Im y = y2 by A2,A3,Th7;
A6: Re x = x1 & Re y = y1 by A2,A3,Th7;
thus Im z = +(*(x1,y2),*(x2,y1)) by A1,A4,Th7
.= *(x1,y2) + *(x2,y1) by Lm5
.= x1*y2 + *(x2,y1) by Lm7
.= Re x * Im y + Im x * Re y by A5,A6,Lm7;
end;
reserve z,z1,z2 for Element of COMPLEX;
definition let z1,z2;
redefine func z1 + z2 -> Element of COMPLEX equals
:Def9: [* Re z1 + Re z2, Im z1 + Im z2 *];
coherence by XCMPLX_0:def 2;
compatibility
proof set z = [* Re z1 + Re z2 , Im z1 + Im z2 *];
reconsider z' = z1 + z2 as Element of COMPLEX by XCMPLX_0:def 2;
A1: Re z = Re z1 + Re z2 by Th7
.= Re z' by Lm8;
Im z = Im z1 + Im z2 by Th7
.= Im z' by Lm9;
hence thesis by A1,Th9;
end;
end;
canceled;
theorem Th19:
for z1, z2 being complex number holds
Re(z1 + z2) = Re z1 + Re z2 & Im(z1 + z2) = Im z1 + Im z2
proof
let z1, z2 be complex number;
z1 in COMPLEX & z2 in COMPLEX by XCMPLX_0:def 2;
then (z1 + z2) = [* Re z1 + Re z2, Im z1 + Im z2 *] by Def9;
hence thesis by Th7;
end;
canceled 2;
theorem
0c + z = z by Def6;
definition let z1,z2;
redefine func z1 * z2 -> Element of COMPLEX equals
:Def10: [* Re z1 * Re z2 - Im z1 * Im z2, Re z1 * Im z2 + Re z2 * Im z1 *];
coherence by XCMPLX_0:def 2;
compatibility
proof
set z =
[* Re z1 * Re z2 - Im z1 * Im z2, Re z1 * Im z2 + Re z2 * Im z1 *];
reconsider z' = z1 * z2 as Element of COMPLEX by XCMPLX_0:def 2;
A1: Re z = Re z1 * Re z2 - Im z1 * Im z2 by Th7
.= Re z' by Lm10;
Im z = Re z1 * Im z2 + Re z2 * Im z1 by Th7
.= Im z' by Lm11;
hence thesis by A1,Th9;
end;
end;
canceled;
theorem Th24:
for z1, z2 being complex number holds
Re(z1 * z2) = Re z1 * Re z2 - Im z1 * Im z2 &
Im(z1 * z2) = Re z1 * Im z2 + Re z2 * Im z1
proof
let z1, z2 be complex number;
z1 in COMPLEX & z2 in COMPLEX by XCMPLX_0:def 2;
then z1 * z2 = [*Re z1 * Re z2 - Im z1 * Im z2, Re z1 * Im z2 + Re z2 * Im
z1*]
by Def10;
hence thesis by Th7;
end;
Lm12: (a + b) + (c + d) = (a + c) + (b + d)
proof
thus (a + b) + (c + d) = a + b + c + d by XCMPLX_1:1
.= a + c + b + d by XCMPLX_1:1
.= (a + c) + (b + d) by XCMPLX_1:1;
end;
canceled 3;
theorem
0c*z = 0c by Def6;
theorem
1r*z = z by Def7;
theorem Th30:
Im z1 = 0 & Im z2 = 0 implies Re(z1*z2) = Re z1 * Re z2 & Im(z1*z2) = 0
proof assume
A1: Im z1 = 0 & Im z2 = 0;
thus Re(z1*z2) = Re z1 * Re z2 - Im z1 * Im z2 by Th24
.= Re z1 * Re z2 by A1;
thus Im(z1*z2) = Re z1 * Im z2 + Re z2 * Im z1 by Th24
.= 0 by A1;
end;
theorem Th31:
Re z1 = 0 & Re z2 = 0 implies Re(z1*z2) = - Im z1 * Im z2 & Im(z1*z2) = 0
proof assume
A1: Re z1 = 0 & Re z2 = 0;
thus Re(z1*z2) = Re z1 * Re z2 - Im z1 * Im z2 by Th24
.= - Im z1 * Im z2 by A1,XCMPLX_1:150;
thus Im(z1*z2) = Re z1 * Im z2 + Re z2 * Im z1 by Th24
.= 0 by A1;
end;
theorem
Re(z*z) = (Re z)^2 - (Im z)^2 & Im(z*z) = 2*(Re z *Im z)
proof
thus Re(z*z) = Re z * Re z - Im z * Im z by Th24
.= (Re z)^2 - Im z * Im z by SQUARE_1:def 3
.= (Re z)^2 - (Im z)^2 by SQUARE_1:def 3;
thus Im(z*z) = Re z * Im z + Re z * Im z by Th24
.= 2*(Re z * Im z) by XCMPLX_1:11;
end;
definition let z;
redefine func -z -> Element of COMPLEX equals
:Def11: [* -Re z , -Im z *];
coherence by XCMPLX_0:def 2;
compatibility
proof set z' = [* -Re z , -Im z *];
z' + z = [* Re z' + Re z , Im z' + Im z *] by Def9
.= [* -Re z + Re z , Im z' + Im z *] by Th7
.= [* -Re z + Re z , -Im z + Im z *] by Th7
.= [* 0, -Im z + Im z *] by XCMPLX_0:def 6
.= [* 0, 0 *] by XCMPLX_0:def 6
.= 0 by ARYTM_0:def 7;
hence thesis by XCMPLX_0:def 6;
end;
end;
canceled;
theorem Th34:
for z being complex number holds
Re(-z) = -(Re z) & Im(-z) = -(Im z)
proof
let z be complex number; z in COMPLEX by XCMPLX_0:def 2;
then -z = [*-Re z,-Im z*] by Def11;
hence thesis by Th7;
end;
-<i> = [*0,-1*] by Def11,Th17,REAL_1:26;
then Lm13: Re -<i> = 0 & Im -<i> = -1 by Th7;
Lm14:-1r = [*-1,0*] by Def11,Th15,REAL_1:26;
canceled 2;
theorem
<i>*<i> = -1r
proof thus Re(<i>*<i>) = 0 * 0 - 1 * 1 by Th17,Th24 .= Re -1r by Lm14,Th7;
thus Im(<i>*<i>) = 0 * 1 + 0 * 1 by Th17,Th24 .= Im -1r by Lm14,Th7;
end;
canceled 8;
theorem
-z = (-1r)*z by Def7,XCMPLX_1:180;
definition let z1,z2;
redefine func z1 - z2 -> Element of COMPLEX equals
:Def12: [* Re z1 - Re z2 , Im z1 - Im z2 *];
coherence by XCMPLX_0:def 2;
compatibility
proof
A1: -z2 = [*-Re z2, -Im z2 *] by Def11;
z1 - z2 = z1 + -z2 by XCMPLX_0:def 8
.= [* Re z1 + Re-z2, Im z1 + Im-z2*] by Def9
.= [* Re z1 + - Re z2, Im z1 + Im -z2*] by A1,Th7
.= [* Re z1 + - Re z2, Im z1 + - Im z2*] by A1,Th7
.= [* Re z1 - Re z2, Im z1 + - Im z2*] by XCMPLX_0:def 8
.= [* Re z1 - Re z2 , Im z1 - Im z2 *] by XCMPLX_0:def 8;
hence thesis;
end;
end;
canceled;
theorem Th48:
Re(z1 - z2) = Re z1 - Re z2 & Im(z1 - z2) = Im z1 - Im z2
proof z1 - z2 = [* Re z1 - Re z2 , Im z1 - Im z2 *] by Def12;
hence thesis by Th7;
end;
canceled 3;
theorem
z - 0c = z by Th14;
definition let z;
redefine func z" -> Element of COMPLEX equals
:Def13: [* Re z / ((Re z)^2+(Im z)^2) , (- Im z) / ((Re z)^2+(Im z)^2) *];
coherence by XCMPLX_0:def 2;
compatibility
proof
set z' =[* Re z / ((Re z)^2+(Im z)^2) , (- Im z) / ((Re z)^2+(Im z)^2) *];
per cases;
suppose
A1: z = 0;
then [* Re z / ((Re z)^2+(Im z)^2) , (- Im z) / ((Re z)^2+(Im z)^2) *]
= 0 by Th12,ARYTM_0:def 7;
hence thesis by A1,XCMPLX_0:def 7;
suppose
A2: z <> 0;
then A3: (Re z)^2+(Im z)^2 <> 0 by Th13;
A4: Im z' = (-Im z) / ((Re z)^2+(Im z)^2) by Th7;
then A5: Re z * Re z' - Im z * Im z'
= (Re z)/1 * (Re z / ((Re z)^2+(Im z)^2)) -
Im z *((-Im z)/((Re z)^2+(Im z)^2)) by Th7
.= Re z * Re z / (1*((Re z)^2+(Im z)^2)) -
(Im z)/1 *((-Im z)/((Re z)^2+(Im z)^2)) by XCMPLX_1:77
.= (Re z)^2 / (1*((Re z)^2+(Im z)^2)) -
(Im z)/1 *((-Im z)/((Re z)^2+(Im z)^2)) by SQUARE_1:def 3
.= (Re z)^2 / ((Re z)^2+(Im z)^2) -
Im z *(-Im z)/(1*((Re z)^2+(Im z)^2)) by XCMPLX_1:77
.= (Re z)^2 / ((Re z)^2+(Im z)^2) -
(-(Im z * Im z))/(1*((Re z)^2+(Im z)^2)) by XCMPLX_1:175
.= (Re z)^2 / ((Re z)^2+(Im z)^2) -
(-((Im z)^2))/(1*((Re z)^2+(Im z)^2)) by SQUARE_1:def 3
.= (Re z)^2 / ((Re z)^2+(Im z)^2) -
-((Im z)^2)/((Re z)^2+(Im z)^2) by XCMPLX_1:188
.= (Re z)^2 / ((Re z)^2+(Im z)^2) +
(Im z)^2/(1*((Re z)^2+(Im z)^2)) by XCMPLX_1:151
.= ((Re z)^2 + (Im z)^2)/((Re z)^2+(Im z)^2) by XCMPLX_1:63
.= 1 by A3,XCMPLX_1:60;
A6: Re z * Im z' + Re z' * Im z
= (Re z)/1 * ((-Im z) / ((Re z)^2+(Im z)^2)) +
Re z / ((Re z)^2+(Im z)^2) * Im z by A4,Th7
.= Re z * (-Im z) / (1*((Re z)^2+(Im z)^2)) +
Re z / ((Re z)^2+(Im z)^2) * (Im z)/1 by XCMPLX_1:77
.= Re z * (-Im z) / (1*((Re z)^2+(Im z)^2)) +
(Im z)/1 * Re z / ((Re z)^2+(Im z)^2) by XCMPLX_1:77
.= (Re z * (-Im z) + Re z * Im z) / ((Re z)^2+(Im z)^2) by XCMPLX_1:63
.= (- Re z * Im z + Re z * Im z) / ((Re z)^2+(Im z)^2) by XCMPLX_1:175
.= 0 / ((Re z)^2+(Im z)^2) by XCMPLX_0:def 6
.= 0;
z * z' = [* Re z * Re z' - Im z * Im z', Re z * Im z' + Re z' * Im z *]
by Def10
.= 1 by A5,A6,ARYTM_0:def 7;
hence thesis by A2,XCMPLX_0:def 7;
end;
end;
canceled 11;
theorem Th64:
for z being complex number holds
Re(z") = Re z / ((Re z)^2+(Im z)^2) &
Im(z") = (- Im z) / ((Re z)^2+(Im z)^2)
proof
let z be complex number;
z in COMPLEX by XCMPLX_0:def 2;
then z" = [* Re z / ((Re z)^2+(Im z)^2),(- Im z) / ((Re z)^2+(Im z)^2)*]
by Def13;
hence thesis by Th7;
end;
theorem
z <> 0c implies z*z" = 1r by Def7,XCMPLX_0:def 7;
canceled 3;
theorem
z2 <> 0c & z1*z2 = 1r implies z1 = z2" by Def7,XCMPLX_0:def 7;
canceled;
theorem
1r" = 1r by Def7;
0^2+1^2 = 1 & 0/1 = 0 & (-1)/1 = -1 by SQUARE_1:59,60;
then Lm15: Re(<i>") = 0 & Im(<i>") = -1 by Th17,Th64;
theorem
<i>" = -<i> by Lm13,Lm15,Th9;
canceled 6;
theorem Th79:
Re z <> 0 & Im z = 0 implies Re(z") = (Re z)" & Im(z") = 0
proof assume
A1: Re z <> 0 & Im z = 0;
then A2: (Re z)^2 + (Im z)^2 = (Re z)^2 by SQUARE_1:60;
hence Re(z") = Re z / (Re z)^2 by Th64
.= (1*Re z) / (Re z * Re z) by SQUARE_1:def 3
.= 1/Re z by A1,XCMPLX_1:92
.= (Re z)" by XCMPLX_1:217;
thus Im(z") = (- Im z) / (Re z)^2 by A2,Th64
.= 0 by A1;
end;
theorem Th80:
Re z = 0 & Im z <> 0 implies Re(z") = 0 & Im(z") = -(Im z)"
proof assume
A1: Re z = 0 & Im z <> 0;
then A2: (Re z)^2 + (Im z)^2 = (Im z)^2 by SQUARE_1:60;
hence Re(z") = Re z / (Im z)^2 by Th64
.= 0 by A1;
thus Im(z") = (- Im z) / (Im z)^2 by A2,Th64
.= -(Im z / (Im z)^2) by XCMPLX_1:188
.= -(1*Im z / (Im z * Im z)) by SQUARE_1:def 3
.= -(1 / Im z) by A1,XCMPLX_1:92
.= - (Im z)" by XCMPLX_1:217;
end;
definition let z1,z2;
redefine func z1 / z2 -> Element of COMPLEX equals
:Def14: [* (Re z1 * Re z2 + Im z1 * Im z2) / ((Re z2)^2 + (Im z2)^2),
(Re z2 * Im z1 - Re z1 * Im z2) / ((Re z2)^2 + (Im z2)^2) *];
coherence by XCMPLX_0:def 2;
compatibility
proof set k = (Re z2)^2 + (Im z2)^2;
set z = [* (Re z1 * Re z2 + Im z1 * Im z2) / k,
(Re z2 * Im z1 - Re z1 * Im z2) / k *];
per cases;
suppose
A1: z2 = 0;
then z2 = [*0,0*] by ARYTM_0:def 7;
then A2: Re z2 = 0 & Im z2 = 0 by Th7;
z1/z2 = z1 * z2" by XCMPLX_0:def 9
.= z1 * 0 by A1,XCMPLX_0:def 7
.= z by A2,ARYTM_0:def 7;
hence thesis;
suppose z2 <> 0;
A3: Re[* Re z2/k, (-Im z2)/k *]= Re z2/k by Th7;
A4: Im[* Re z2/k, (-Im z2)/k *]= (-Im z2)/k by Th7;
z1 / z2 = z1 * z2" by XCMPLX_0:def 9
.= z1*[* Re z2/k, (-Im z2)/k *] by Def13
.= [* (Re z1)/1 * (Re z2/k) - Im z1 * ((-Im z2)/k),
Re z1 * ((-Im z2)/k) + (Re z2/k) * Im z1 *] by A3,A4,Def10
.= [* Re z1 * Re z2/(1*k) - (Im z1)/1 * ((-Im z2)/k),
Re z1 * ((-Im z2)/k) + (Re z2/k) * Im z1 *] by XCMPLX_1:77
.= [* Re z1 * Re z2/k - Im z1 * (-Im z2)/(1*k),
(Re z1)/1 * ((-Im z2)/k) + (Re z2/k) * Im z1 *] by XCMPLX_1:77
.= [* Re z1 * Re z2/k - Im z1 * (-Im z2)/k,
Re z1 * (-Im z2)/(1*k) + (Re z2/k) * ((Im z1)/1) *] by XCMPLX_1:77
.= [* Re z1 * Re z2/k - Im z1 * (-Im z2)/k,
Re z1 * (-Im z2)/k + Im z1 * Re z2/(1*k) *] by XCMPLX_1:77
.= [* (Re z1 * Re z2 - Im z1 * (-Im z2))/k,
Re z1 * (-Im z2)/k + Im z1 * Re z2/(1*k) *] by XCMPLX_1:121
.= [* (Re z1 * Re z2 - Im z1 * (-Im z2))/k,
(Re z1 * (-Im z2) + Im z1 * Re z2)/k *] by XCMPLX_1:63
.= [* (Re z1 * Re z2 - -(Im z1 * Im z2))/k,
(Re z1 * (-Im z2) + Im z1 * Re z2)/k *] by XCMPLX_1:175
.= [* (Re z1 * Re z2 + Im z1 * Im z2)/k,
(Re z1 * (-Im z2) + Im z1 * Re z2)/k *] by XCMPLX_1:151
.= [* (Re z1 * Re z2 + Im z1 * Im z2)/k,
(-Re z1 * Im z2 + Im z1 * Re z2)/k *] by XCMPLX_1:175
.= z by XCMPLX_0:def 8;
hence thesis;
end;
end;
canceled;
theorem
Re(z1 / z2) = (Re z1 * Re z2 + Im z1 * Im z2) / ((Re z2)^2 + (Im z2)^2) &
Im(z1 / z2) = (Re z2 * Im z1 - Re z1 * Im z2) / ((Re z2)^2 + (Im z2)^2)
proof
z1 / z2 = [* (Re z1 * Re z2 + Im z1 * Im z2) / ((Re z2)^2 + (Im z2)^2),
(Re z2 * Im z1 - Re z1 * Im z2) / ((Re z2)^2 + (Im z2)^2) *]
by Def14;
hence thesis by Th7;
end;
canceled;
theorem
z<>0c implies z" = 1r/z by Def7,XCMPLX_1:217;
theorem
z/1r = z by Def7;
theorem
z<>0c implies z/z = 1r by Def7,XCMPLX_1:60;
theorem
0c/z = 0c by Th14;
canceled 3;
theorem
z2<>0c & z1/z2 = 1r implies z1 = z2 by Def7,XCMPLX_1:58;
canceled 17;
theorem
Im z1 = 0 & Im z2 = 0 & Re z2 <> 0 implies
Re(z1/z2) = (Re z1)/(Re z2) & Im(z1/z2) = 0
proof assume
A1: Im z1 = 0 & Im z2 = 0 & Re z2 <> 0;
then A2: z1/z2 = z1*z2" & Im(z2") = 0 by Th79,XCMPLX_0:def 9;
hence Re(z1/z2) = (Re z1)*Re(z2") by A1,Th30
.= (Re z1)*(Re z2)" by A1,Th79
.= (Re z1)/(Re z2) by XCMPLX_0:def 9;
thus Im(z1/z2) = 0 by A1,A2,Th30;
end;
theorem
Re z1 = 0 & Re z2 = 0 & Im z2 <> 0 implies
Re(z1/z2) = (Im z1)/(Im z2) & Im(z1/z2) = 0
proof assume
A1: Re z1 = 0 & Re z2 = 0 & Im z2 <> 0;
then A2: z1/z2 = z1*z2" & Re(z2") = 0 by Th80,XCMPLX_0:def 9;
hence Re(z1/z2) = -(Im z1)*Im(z2") by A1,Th31
.= -(Im z1)*-(Im z2)" by A1,Th80
.= --(Im z1)*(Im z2)" by XCMPLX_1:175
.= (Im z1)/(Im z2) by XCMPLX_0:def 9;
thus Im(z1/z2) = 0 by A1,A2,Th31;
end;
definition let z be complex number;
func z*' -> complex number equals
:Def15: [*Re z,-Im z*];
correctness;
involutiveness
proof let z,z' be complex number;
assume z = [* Re z' , -Im z' *];
then Re z = Re z' & Im z = - Im z' by Th7;
hence z' = [* Re z , -Im z *] by Th8;
end;
end;
definition let z be complex number;
redefine func z*' -> Element of COMPLEX;
coherence by XCMPLX_0:def 2;
end;
canceled;
theorem Th112:
for z being complex number holds
Re (z*') = Re z & Im (z*') = -Im z
proof
let z be complex number;
z*' = [*Re z,-Im z*] by Def15;
hence thesis by Th7;
end;
then Lm16: Re (0c*') = 0 & Im (0c*') = 0 by Th12,REAL_1:26;
theorem
0c*' = 0c by Lm16,Th9,Th12;
theorem
z*' = 0c implies z = 0c
proof assume
A1: z*' = 0c;
z*' = [*Re z,-Im z*] by Def15;
then Re z = 0 & --Im z = -0 by A1,ARYTM_0:12,L0;
hence Re z = Re 0c & Im z = Im 0c by Th7,L0;
end;
Lm17: Re (1r*') = 1 & Im (1r*') = 0 by Th15,Th112,REAL_1:26;
theorem
1r*' = 1r by Lm17,Th9,Th15;
Lm18: Re (<i>*') = 0 & Im (<i>*') = -1 by Th17,Th112;
theorem
<i>*' = -<i> by Lm13,Lm18,Th9;
canceled;
theorem Th118:
(z1 + z2)*' = z1*' + z2*'
proof
thus Re ((z1 + z2)*') = Re(z1 + z2) by Th112
.= Re z1 + Re z2 by Th19
.= Re (z1*') + Re z2 by Th112
.= Re (z1*') + Re (z2*') by Th112
.= Re (z1*'+ z2*') by Th19;
thus Im ((z1 + z2)*') = -Im(z1 + z2) by Th112
.= -(Im z1 + --Im z2) by Th19
.= -(Im z1 - -Im z2) by XCMPLX_0:def 8
.= -Im z2 - Im z1 by XCMPLX_1:143
.= -Im z1 + -Im z2 by XCMPLX_0:def 8
.= Im (z1*') + -Im z2 by Th112
.= Im (z1*') + Im (z2*') by Th112
.= Im (z1*' + z2*') by Th19;
end;
theorem Th119:
(-z)*' = -(z*')
proof
thus Re ((-z)*') = Re -z by Th112
.= - Re z by Th34
.= - Re (z*') by Th112
.= Re -(z*') by Th34;
thus Im ((-z)*') = -Im -z by Th112
.= - -Im z by Th34
.= - Im (z*') by Th112
.= Im -(z*') by Th34;
end;
theorem
(z1 - z2)*' = z1*' - z2*'
proof
thus (z1 - z2)*' = (z1 + -z2)*' by XCMPLX_0:def 8
.= z1*' + (-z2)*' by Th118
.= z1*' + -(z2*') by Th119
.= z1*' - z2*' by XCMPLX_0:def 8;
end;
theorem Th121:
(z1*z2)*' = z1*'*z2*'
proof
A1: Re(z1*') = Re z1 & Re(z2*') = Re z2 by Th112;
A2: Im(z1*') = -Im z1 & Im(z2*') = -Im z2 by Th112;
thus Re((z1*z2)*')
= Re(z1*z2) by Th112
.= (Re (z1*') * Re (z2*')) - (-Im (z1*')) * -Im (z2*') by A1,A2,Th24
.= (Re (z1*') * Re (z2*')) - -(Im (z1*') * -Im (z2*')) by XCMPLX_1:175
.= (Re (z1*') * Re (z2*')) - --(Im (z1*') * Im (z2*')) by XCMPLX_1:175
.= Re(z1*'*z2*') by Th24;
thus Im((z1*z2)*')
= -Im(z1*z2) by Th112
.= -((Re (z1*') * -Im (z2*')) + (Re (z2*') * -Im (z1*'))) by A1,A2,Th24
.= -(-(Re (z1*') * Im (z2*')) + (Re (z2*') * -Im (z1*'))) by XCMPLX_1:175
.= -(-(Re (z1*') * Im (z2*')) + -(Re (z2*') * Im (z1*'))) by XCMPLX_1:175
.= -(-(Re (z1*') * Im (z2*')) - (Re (z2*') * Im (z1*'))) by XCMPLX_0:def 8
.= (Re (z2*') * Im (z1*'))--(Re (z1*') * Im (z2*')) by XCMPLX_1:143
.= (Re (z2*') * Im (z1*'))+--(Re (z1*') * Im (z2*')) by XCMPLX_0:def 8
.= Im(z1*'*z2*') by Th24;
end;
theorem Th122:
z"*' = z*'"
proof
A1: Re z = Re (z*') & -Im z = Im (z*') by Th112;
then A2: (Re z)^2+(Im z)^2 = (Re (z*'))^2+(Im (z*'))^2 by SQUARE_1:61;
thus Re(z"*') = Re(z") by Th112
.= Re(z*')/ ((Re(z*'))^2+(Im(z*'))^2) by A1,A2,Th64
.= Re(z*'") by Th64;
thus Im(z"*') = -Im(z") by Th112
.= -((Im(z*'))/((Re(z*'))^2+(Im(z*'))^2)) by A1,A2,Th64
.= (-Im (z*'))/((Re (z*'))^2+(Im (z*'))^2) by XCMPLX_1:188
.= Im(z*'") by Th64;
end;
theorem
(z1/z2)*' = (z1*')/(z2*')
proof
thus (z1/z2)*' = (z1*z2")*' by XCMPLX_0:def 9
.= (z1*'*z2"*') by Th121
.= (z1*'*z2*'") by Th122
.= (z1*')/(z2*') by XCMPLX_0:def 9;
end;
theorem
Im z = 0 implies z*' = z
proof Re (z*') = Re z & Im (z*') = -Im z by Th112;
hence thesis by Th9;
end;
theorem
Re z = 0 implies z*' = -z
proof Re (z*') = Re z & Im (z*') = -Im z & Re - z = - Re z & Im -z = -Im z
by Th34,Th112;
hence thesis by Th9;
end;
theorem
Re(z*z*') = (Re z)^2 + (Im z)^2 & Im(z*z*') = 0
proof
thus Re(z*(z*')) = Re z * Re (z*') - Im z * Im (z*') by Th24
.= Re z * Re z - Im z * Im (z*') by Th112
.= Re z * Re z - Im z * -Im z by Th112
.= Re z * Re z - -Im z * Im z by XCMPLX_1:175
.= Re z * Re z +- -Im z * Im z by XCMPLX_0:def 8
.= (Re z)^2 + Im z * Im z by SQUARE_1:def 3
.= (Re z)^2 + (Im z)^2 by SQUARE_1:def 3;
thus Im(z*(z*')) = Re z * Im (z*') + Re (z*') * Im z by Th24
.= Re z * -Im z + Re (z*') * Im z by Th112
.= Re z * -Im z + Re z * Im z by Th112
.= -Re z * Im z + Re z * Im z by XCMPLX_1:175
.= 0 by XCMPLX_0:def 6;
end;
theorem
Re(z + z*') = 2*Re z & Im(z + z*') = 0
proof
thus Re(z + z*') = Re z + Re (z*') by Th19
.= Re z + Re z by Th112
.= 2*Re z by XCMPLX_1:11;
thus Im(z + (z*')) = Im z + Im (z*') by Th19
.= Im z + -Im z by Th112
.= 0 by XCMPLX_0:def 6;
end;
theorem
Re(z - z*') = 0 & Im(z - z*') = 2*Im z
proof
thus Re(z - z*') = Re z - Re (z*') by Th48
.= Re z - Re z by Th112
.= 0 by XCMPLX_1:14;
thus Im(z - z*') = Im z - Im (z*') by Th48
.= Im z - -Im z by Th112
.= Im z +- -Im z by XCMPLX_0:def 8
.= 2*Im z by XCMPLX_1:11;
end;
definition let z be complex number;
func |.z.| equals
:Def16: sqrt ((Re z)^2 + (Im z)^2);
coherence;
end;
definition let z be complex number;
cluster |.z.| -> real;
coherence
proof
|.z.| = sqrt ((Re z)^2 + (Im z)^2) by Def16;
hence thesis;
end;
end;
definition let z be complex number;
redefine func |.z.| -> Real;
coherence by XREAL_0:def 1;
end;
Lm19: sqrt (0^2 + 0^2) = 0 by SQUARE_1:60,82;
canceled;
theorem Th130:
|.0c.| = 0 by Def16,Lm19,Th12;
theorem Th131:
for z being complex number st |.z.| = 0 holds z = 0c
proof let z be complex number; assume |.z.| = 0;
then sqrt ((Re z)^2 + (Im z)^2) = 0 & 0 <= (Re z)^2 + (Im z)^2 by Def16,Lm3;
then (Re z)^2 + (Im z)^2 = 0 by SQUARE_1:92;
hence z = 0c by Th13;
end;
theorem Th132:
for z being complex number holds 0 <= |.z.|
proof let z be complex number; |.z.| = sqrt ((Re z)^2 + (Im z)^2) &
0 <= (Re z)^2 + (Im z)^2 by Def16,Lm3;
hence thesis by SQUARE_1:def 4;
end;
theorem
for z being complex number holds z <> 0c iff 0 < |.z.|
proof
let z be complex number;
thus z <> 0c implies 0 < |.z.|
proof assume z <> 0c;
then 0 <= |.z.| & 0 <> |.z.| by Th131,Th132;
hence thesis;
end;
thus thesis by Def16,Lm19,Th12;
end;
Lm20: sqrt (1^2 + 0^2) = 1 by SQUARE_1:59,60,83;
theorem
|.1r.| = 1 by Def16,Lm20,Th15;
Lm21: sqrt (0^2 + 1^2) = 1 by SQUARE_1:59,60,83;
theorem
|.<i>.| = 1 by Def16,Lm21,Th17;
theorem
for z being complex number st Im z = 0 holds |.z.| = abs(Re z)
proof
let z be complex number;
assume Im z = 0;
then sqrt ((Re z)^2 + (Im z)^2) = sqrt ((Re z)^2) by SQUARE_1:60;
then |.z.| = sqrt ((Re z)^2) by Def16;
hence thesis by SQUARE_1:91;
end;
theorem
for z being complex number st Re z = 0 holds |.z.| = abs(Im z)
proof
let z be complex number;
assume Re z = 0;
then sqrt ((Re z)^2 + (Im z)^2) = sqrt ((Im z)^2) by SQUARE_1:60;
then |.z.| = sqrt ((Im z)^2) by Def16;
hence thesis by SQUARE_1:91;
end;
theorem Th138:
for z being complex number holds |.-z.| = |.z.|
proof
let z be complex number;
thus |.-z.| = sqrt ((Re -z)^2 + (Im -z)^2) by Def16
.= sqrt ((-Re z)^2 + (Im -z)^2) by Th34
.= sqrt ((-Re z)^2 + (-Im z)^2) by Th34
.= sqrt ((Re z)^2 + (-Im z)^2) by SQUARE_1:61
.= sqrt ((Re z)^2 + (Im z)^2) by SQUARE_1:61
.= |.z.| by Def16;
end;
reserve z for complex number;
theorem Th139:
|.z*'.| = |.z.|
proof
thus |.z*'.| = sqrt ((Re (z*'))^2 + (Im (z*'))^2) by Def16
.= sqrt ((Re z)^2 + (Im (z*'))^2) by Th112
.= sqrt ((Re z)^2 + (-Im z)^2) by Th112
.= sqrt ((Re z)^2 + (Im z)^2) by SQUARE_1:61
.= |.z.| by Def16;
end;
theorem
Re z <= |.z.|
proof (Re z)^2 <= (Re z)^2 & 0<=(Im z)^2 by SQUARE_1:72;
then (Re z)^2+0 <= ((Re z)^2 + (Im z)^2) by REAL_1:55;
then 0<=(Re z)^2 & (Re z)^2 <= ((Re z)^2 + (Im z)^2) by SQUARE_1:72;
then sqrt (Re z)^2 <= sqrt ((Re z)^2 + (Im z)^2) by SQUARE_1:94;
then sqrt (Re z)^2 <= |.z.| by Def16;
then Re z <= abs(Re z) & abs(Re z) <= |.z.| by ABSVALUE:11,SQUARE_1:91;
hence thesis by AXIOMS:22;
end;
theorem
Im z <= |.z.|
proof (Im z)^2 <= (Im z)^2 & 0<=(Re z)^2 by SQUARE_1:72;
then (Im z)^2+0 <= ((Re z)^2 + (Im z)^2) by REAL_1:55;
then 0<=(Im z)^2 & (Im z)^2 <= ((Re z)^2 + (Im z)^2) by SQUARE_1:72;
then sqrt (Im z)^2 <= sqrt ((Re z)^2 + (Im z)^2) by SQUARE_1:94;
then sqrt (Im z)^2 <= |.z.| by Def16;
then Im z <= abs(Im z) & abs(Im z) <= |.z.| by ABSVALUE:11,SQUARE_1:91;
hence thesis by AXIOMS:22;
end;
theorem Th142:
for z1, z2 being complex number holds
|.z1 + z2.| <= |.z1.| + |.z2.|
proof
let z1, z2 be complex number;
set r1 = Re z1, r2 = Re z2, i1 = Im z1, i2 = Im z2;
A1: 0 <= r1^2+i1^2 & 0 <= r2^2+i2^2 by Lm3;
then A2: (sqrt (r1^2+i1^2))^2 = r1^2+i1^2 &
(sqrt (r2^2+i2^2))^2 = r2^2+i2^2 by SQUARE_1:def 4;
A3:(Re(z1 + z2))^2 = (r1+ r2)^2 by Th19
.= r1^2 + 2*r1*r2 + r2^2 by SQUARE_1:63;
(Im(z1 + z2))^2 = (i1 + i2)^2 by Th19
.= i1^2 + 2*i1*i2 + i2^2 by SQUARE_1:63;
then A4: (Re(z1+z2))^2+(Im(z1+z2))^2
= (r1^2 + 2*r1*r2 + r2^2) + (i1^2 + (2*i1*i2 + i2^2
)) by A3,XCMPLX_1:1
.= (r1^2 + 2*r1*r2 + r2^2) + i1^2 + (2*i1*i2 + i2^2) by XCMPLX_1:1
.= (r1^2 + 2*r1*r2 + i1^2) + r2^2 + (2*i1*i2 + i2^2) by XCMPLX_1:1
.= (r1^2 + i1^2 + 2*r1*r2) + r2^2 + (2*i1*i2 + i2^2) by XCMPLX_1:1
.= (r1^2 + i1^2 + 2*r1*r2) + (r2^2 + (2*i1*i2 + i2^2)) by XCMPLX_1:1
.= (r1^2 + i1^2 + 2*r1*r2) + (2*i1*i2 + (r2^2 + i2^2)) by XCMPLX_1:1
.= (r1^2 + i1^2 + 2*r1*r2) + 2*i1*i2 + (r2^2 + i2^2) by XCMPLX_1:1
.= r1^2 + i1^2 + (2*r1*r2 + 2*i1*i2) + (r2^2 + i2^2) by XCMPLX_1:1;
r1^2*r2^2=(r1*r2)^2 & r1^2*i2^2=(r1*i2)^2 & i1^2*r2^2=(i1*r2)^2 & i1^2*i2
^2
=(i1*i2)^2 by SQUARE_1:68;
then r1^2*(r2^2+i2^2)=(r1*r2)^2+(r1*i2)^2 & i1^2*(r2^2+i2^2)=(i1*r2)^2+(i1
*i2)^2 by XCMPLX_1:8;
then A5: (r1^2+i1^2)*(r2^2+i2^2)
= (r1*i2)^2+(r1*r2)^2+((i1*r2)^2+(i1*i2)^2) by XCMPLX_1:8
.= (r1*i2)^2+((r1*r2)^2+((i1*r2)^2+(i1*i2)^2)) by XCMPLX_1:1
.= (r1*i2)^2+((i1*r2)^2+((r1*r2)^2+(i1*i2)^2)) by XCMPLX_1:1
.= ((r1*i2)^2+(i1*r2)^2)+((r1*r2)^2+(i1*i2)^2)by XCMPLX_1:1;
(r1*r2 + i1*i2)^2 = (r1*r2)^2+2*(r1*r2)*(i1*i2)+(i1*i2)^2 by SQUARE_1:63
.= ((r1*r2)^2+(i1*i2)^2) + 2*(r1*r2)*(i1*i2) by XCMPLX_1:1
.= ((r1*r2)^2+(i1*i2)^2) + 2*((r1*r2)*(i1*i2)) by XCMPLX_1:4
.= ((r1*r2)^2+(i1*i2)^2) + 2*(r1*(r2*(i2*i1))) by XCMPLX_1:4
.= ((r1*r2)^2+(i1*i2)^2) + 2*(r1*(i2*(r2*i1))) by XCMPLX_1:4
.= ((r1*r2)^2+(i1*i2)^2) + 2*((r1*i2)*(i1*r2)) by XCMPLX_1:4
.= ((r1*r2)^2+(i1*i2)^2) + 2*(r1*i2)*(i1*r2) by XCMPLX_1:4;
then (r1^2+i1^2)*(r2^2+i2^2)-(r1*r2+i1*i2)^2
= (((r1*i2)^2+(i1*r2)^2)+((r1*r2)^2+(i1*i2)^2))
- ((r1*r2)^2+(i1*i2)^2)-2*(r1*i2)*(i1*r2) by A5,XCMPLX_1:36
.= ((r1*i2)^2+(i1*r2)^2)-2*(r1*i2)*(i1*r2) by XCMPLX_1:26
.= (r1*i2)^2+((i1*r2)^2-2*(r1*i2)*(i1*r2)) by XCMPLX_1:29
.= (r1*i2)^2+(-2*(r1*i2)*(i1*r2)+(i1*r2)^2) by XCMPLX_0:def 8
.= (r1*i2)^2+-2*(r1*i2)*(i1*r2)+(i1*r2)^2 by XCMPLX_1:1
.= (r1*i2)^2-2*(r1*i2)*(i1*r2)+(i1*r2)^2 by XCMPLX_0:def 8
.= (r1*i2-i1*r2)^2 by SQUARE_1:64;
then 0 <= (r1^2+i1^2)*(r2^2+i2^2)-(r1*r2+i1*i2)^2 by SQUARE_1:72;
then (r1*r2+i1*i2)^2+0 <= (r1^2+i1^2)*(r2^2+i2^2) by REAL_1:84;
then 0<=(r1*r2+i1*i2)^2 & (r1*r2+i1*i2)^2 <= (r1^2+i1^2)*(r2^2+i2^2)
by SQUARE_1:72;
then r1*r2+i1*i2 <= abs(r1*r2+i1*i2) & sqrt (r1*r2+i1*i2)^2 <=
sqrt ((r1^2+i1^2)*(r2^2+i2^2)) by ABSVALUE:11,SQUARE_1:94;
then r1*r2+i1*i2 <= sqrt (r1*r2+i1*i2)^2 & sqrt (r1*r2+i1*i2)^2 <=
sqrt (r1^2+i1^2)*sqrt (r2^2+i2^2)
by A1,SQUARE_1:91,97;
then A6: r1*r2 + i1*i2 <= sqrt (r1^2+i1^2)*sqrt (r2^2+i2^2) by AXIOMS:22;
2*r1*r2 = 2*(r1*r2) & 2*i1*i2 = 2*(i1*i2) by XCMPLX_1:4;
then (2*r1*r2 + 2*i1*i2) = 2*(r1*r2 + i1*i2) & 0 <= 2 by XCMPLX_1:8;
then (2*r1*r2 + 2*i1*i2) <= 2*(sqrt (r1^2+i1^2)*sqrt (r2^2+i2^2))
by A6,AXIOMS:25;
then r1^2 + i1^2 <= r1^2 + i1^2 &
(2*r1*r2 + 2*i1*i2) <= 2*sqrt (r1^2+i1^2)*sqrt (r2^2+i2^2)
by XCMPLX_1:4;
then (r1^2 + i1^2)+(2*r1*r2+2*i1*i2) <=
(r1^2+i1^2)+2*sqrt (r1^2+i1^2)*sqrt (r2^2+i2^2) &
r2^2 + i2^2 <= r2^2 + i2^2 by REAL_1:55;
then (Re(z1+z2))^2+(Im(z1+z2))^2 <=
(r1^2+i1^2)+2*sqrt (r1^2+i1^2)*sqrt (r2^2+i2^2)+(r2^2+i2^2)
by A4,REAL_1:55;
then 0 <= (Re(z1 + z2))^2 + (Im(z1 + z2))^2 & 0 <= sqrt (r1^2+i1^2) & 0 <=
sqrt (r2^2+i2^2) &
(Re(z1 + z2))^2 + (Im(z1 + z2))^2 <= (sqrt (r1^2+i1^2) + sqrt (r2^2+i2^2
))^2
by A1,A2,Lm3,SQUARE_1:63,def 4;
then 0 + 0 <= sqrt (r1^2+i1^2) + sqrt (r2^2+i2^2) &
sqrt ((Re(z1 + z2))^2 + (Im(z1 + z2))^2) <=
sqrt ((sqrt (r1^2+i1^2) + sqrt (r2^2+i2^2))^2)
by REAL_1:55,SQUARE_1:94;
then sqrt ((Re(z1 + z2))^2 + (Im(z1 + z2))^2) <=
(sqrt (r1^2+i1^2) + sqrt (r2^2+i2^2))
by SQUARE_1:89;
then sqrt ((Re(z1 + z2))^2 + (Im(z1 + z2))^2) <= sqrt (r1^2+i1^2) + |.z2.|
by Def16;
then sqrt ((Re(z1 + z2))^2 + (Im(z1 + z2))^2) <= |.z1.| + |.z2.| by Def16;
hence thesis by Def16;
end;
theorem Th143:
|.z1 - z2.| <= |.z1.| + |.z2.|
proof |.z1 - z2.| = |.z1 + - z2.| by XCMPLX_0:def 8;
then |.z1 - z2.| <= |.z1.| + |.-z2.| by Th142;
hence |.z1 - z2.| <= |.z1.| + |.z2.| by Th138;
end;
theorem
|.z1.| - |.z2.| <= |.z1 + z2.|
proof z1 = z1 + z2 - z2 by XCMPLX_1:26;
then |.z1.| <= |.z1 + z2.| + |.z2.| by Th143;
hence thesis by REAL_1:86;
end;
theorem Th145:
|.z1.| - |.z2.| <= |.z1 - z2.|
proof z1 = z1 - z2 + z2 by XCMPLX_1:27;
then |.z1.| <= |.z1 - z2.| + |.z2.| by Th142;
hence thesis by REAL_1:86;
end;
theorem Th146:
|.z1 - z2.| = |.z2 - z1.|
proof
thus |.z1 - z2.| = |.-(z2 - z1).| by XCMPLX_1:143 .= |.z2 - z1.| by Th138;
end;
theorem Th147:
|.z1 - z2.| = 0 iff z1 = z2
proof
thus |.z1 - z2.| = 0 implies z1 = z2
proof assume |.z1 - z2.| = 0; then z1 - z2 = 0c by Th131;
hence z1 = z2 by XCMPLX_1:15;
end;
thus thesis by Th130,XCMPLX_1:14;
end;
theorem
z1 <> z2 iff 0 < |.z1 - z2.|
proof
thus z1 <> z2 implies 0 < |.z1 - z2.|
proof assume z1 <> z2;
then 0 <= |.z1 - z2.| & |.z1 - z2.| <> 0 by Th132,Th147;
hence thesis;
end;
assume 0 < |.z1 - z2.|;
hence thesis by Th147;
end;
theorem
|.z1 - z2.| <= |.z1 - z.| + |.z - z2.|
proof
|.z1 - z2.| = |.z1 - z + z - z2.| by XCMPLX_1:27
.= |.(z1 - z) + (z - z2).| by XCMPLX_1:29;
hence thesis by Th142;
end;
theorem
abs(|.z1.| - |.z2.|) <= |.z1 - z2.|
proof
|.z2.| - |.z1.| <= |.z2 - z1.| by Th145;
then -(|.z1.| - |.z2.|) <= |.z2 - z1.| by XCMPLX_1:143;
then -(|.z1.| - |.z2.|) <= |.z1 - z2.| by Th146;
then -|.z1 - z2.| <= --(|.z1.| - |.z2.|) by REAL_1:50;
then -|.z1 - z2.| <= (|.z1.| - |.z2.|) & |.z1.| - |.z2.| <= |.z1 - z2.|
by Th145;
hence thesis by ABSVALUE:12;
end;
theorem Th151:
for z1, z2 being complex number holds
|.z1*z2.| = |.z1.|*|.z2.|
proof
let z1, z2 be complex number;
set r1 = Re z1, r2 = Re z2, i1 = Im z1, i2 = Im z2;
A1: 0<=r1^2 + i1^2 & 0<=r2^2 + i2^2 by Lm3;
A2: (Re(z1*z2))^2 = (r1*r2 - i1*i2)^2 by Th24
.= (r1*r2)^2 - 2*(r1*r2)*(i1*i2) + (i1*i2)^2 by SQUARE_1:64
.= (r1*r2)^2 + - 2*(r1*r2)*(i1*i2) + (i1*i2)^2
by XCMPLX_0:def 8
.= (r1*r2)^2 + (i1*i2)^2 + - 2*(r1*r2)*(i1*i2) by XCMPLX_1:1;
A3: 2*(r1*i2)*(r2*i1) = 2*((r1*i2)*(r2*i1)) by XCMPLX_1:4
.= 2*((r1*i2)*r2*i1) by XCMPLX_1:4
.= 2*((r1*r2)*i2*i1) by XCMPLX_1:4
.= 2*((r1*r2)*(i1*i2)) by XCMPLX_1:4
.= 2*(r1*r2)*(i1*i2) by XCMPLX_1:4;
A4: (r1*r2)^2 = r1^2*r2^2 & (r1*i2)^2 = r1^2*i2^2 &
(i1*i2)^2 = i1^2*i2^2 & (i1*r2)^2 = i1^2*r2^2 by SQUARE_1:68;
(Im(z1*z2))^2 = (r1*i2 + r2*i1)^2 by Th24
.= 2*(r1*i2)*(r2*i1) + (r1*i2)^2 + (r2*i1)^2 by SQUARE_1:63
.= 2*(r1*r2)*(i1*i2) + ((r1*i2)^2 + (r2*i1)^2) by A3,XCMPLX_1:1;
then (Re(z1*z2))^2+(Im(z1*z2))^2
= ((r1*r2)^2 + (i1*i2)^2) + -2*(r1*r2)*(i1*i2)
+ 2*(r1*r2)*(i1*i2) + ((r1*i2)^2 + (r2*i1)^2) by A2,XCMPLX_1:1
.= ((r1*r2)^2 + (i1*i2)^2) +(- 2*(r1*r2)*(i1*i2)
+ 2*(r1*r2)*(i1*i2)) + ((r1*i2)^2 + (r2*i1)^2) by XCMPLX_1:1
.= ((r1*r2)^2 + (i1*i2)^2) + 0 + ((r1*i2)^2 + (r2*i1)^2)
by XCMPLX_0:def 6
.= ((r1*r2)^2 + (r1*i2)^2) + ((i1*i2)^2 + (r2*i1)^2) by Lm12
.= r1^2*(r2^2 + i2^2) + ((i1*i2)^2 + (i1*r2)^2) by A4,XCMPLX_1:8
.= r1^2*(r2^2 + i2^2) + i1^2*(r2^2 + i2^2) by A4,XCMPLX_1:8
.= (r1^2 + i1^2)*(r2^2 + i2^2) by XCMPLX_1:8;
hence |.z1*z2.| = sqrt ((r1^2 + i1^2)*(r2^2 + i2^2)) by Def16
.= sqrt (r1^2 + i1^2)*sqrt (r2^2 + i2^2) by A1,SQUARE_1:97
.= sqrt (r1^2 + i1^2)*|.z2.| by Def16
.= |.z1.|*|.z2.| by Def16;
end;
theorem Th152:
z <> 0c implies |.z".| = |.z.|"
proof assume
A1: z <> 0c;
set r2i2 = (Re z)^2+(Im z)^2;
A2: r2i2 <> 0 by A1,Th13;
A3: 0 <= r2i2 by Lm3;
thus |.z".| = sqrt ((Re(z"))^2 + (Im(z"))^2) by Def16
.= sqrt ((Re z / r2i2)^2 + (Im(z"))^2) by Th64
.= sqrt ((Re z / r2i2)^2 + ((-Im z) / r2i2)^2) by Th64
.= sqrt ((Re z)^2 / r2i2^2 + ((-Im z) / r2i2)^2) by SQUARE_1:69
.= sqrt ((Re z)^2 / r2i2^2 + (-Im z)^2 / r2i2^2) by SQUARE_1:69
.= sqrt (((Re z)^2 + (-Im z)^2) / r2i2^2) by XCMPLX_1:63
.= sqrt (r2i2 / r2i2^2) by SQUARE_1:61
.= sqrt ((1*r2i2) / (r2i2*r2i2)) by SQUARE_1:def 3
.= sqrt (1 / r2i2) by A2,XCMPLX_1:92
.= 1 / sqrt r2i2 by A3,SQUARE_1:83,99
.= 1 / |.z.| by Def16
.= |.z.|" by XCMPLX_1:217;
end;
theorem
z2 <> 0c implies |.z1.|/|.z2.| = |.z1/z2.|
proof assume
A1: z2 <> 0c;
thus |.z1.|/|.z2.| = |.z1.|*|.z2.|" by XCMPLX_0:def 9
.= |.z1.|*|.z2".| by A1,Th152
.= |.z1*z2".| by Th151
.= |.z1/z2.| by XCMPLX_0:def 9;
end;
theorem
|.z*z.| = (Re z)^2 + (Im z)^2
proof
A1: 0<=(Re z)^2 + (Im z)^2 by Lm3;
|.z*z.| = |.z.|*|.z.| & |.z.| = sqrt ((Re z)^2 + (Im z)^2) by Def16,Th151;
then |.z*z.| = sqrt (((Re z)^2 + (Im z)^2)*((Re z)^2 + (Im z)^2))
by A1,SQUARE_1:97;
then |.z*z.| = sqrt (((Re z)^2 + (Im z)^2)^2) by SQUARE_1:def 3;
hence thesis by A1,SQUARE_1:89;
end;
theorem
|.z*z.| = |.z*z*'.|
proof
thus |.z*z.| = |.z.|*|.z.| by Th151
.= |.z.|*|.z*'.| by Th139
.= |.z*z*'.| by Th151;
end;