:: The Complex Numbers
:: by Czes{\l}aw Byli\'nski
::
:: Received March 1, 1990
:: Copyright (c) 1990-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 NUMBERS, SUBSET_1, XREAL_0, SQUARE_1, ARYTM_3, CARD_1, XXREAL_0,
XCMPLX_0, FUNCT_1, FUNCT_2, XBOOLE_0, RELAT_1, REAL_1, FUNCOP_1, ARYTM_0,
ARYTM_1, COMPLEX1, ORDINAL1;
notations TARSKI, SUBSET_1, ORDINAL1, ARYTM_0, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, SQUARE_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, XXREAL_0;
constructors FUNCT_4, ARYTM_0, REAL_1, SQUARE_1, MEMBERED, RELSET_1, XXREAL_0;
registrations XBOOLE_0, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
SQUARE_1, ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities SQUARE_1;
theorems SQUARE_1, XREAL_0, FUNCT_2, XBOOLE_0, TARSKI, NUMBERS, FUNCT_4,
XCMPLX_0, XCMPLX_1, ARYTM_0, XREAL_1, XXREAL_0, CARD_1;
begin
reserve a,b,c,d for Real;
:: Auxiliary theorems
theorem Th1:
a^2 + b^2 = 0 implies a = 0
proof
0 <= a^2 & 0 <= b^2 by XREAL_1:63;
hence thesis;
end;
Lm1: 0 <= a^2 + b^2
proof
0<=a^2 & 0<=b^2 by XREAL_1:63;
hence thesis;
end;
:: Complex Numbers
definition
let z be Complex;
func Re z -> number means
:Def1:
it = z if z is real
otherwise ex f being Function of 2,REAL st z = f & it = f.0;
existence
proof
thus z is real implies ex IT being set st IT = z
proof
assume z is real; then
z in REAL by XREAL_0:def 1;
hence thesis;
end;
A1: z in COMPLEX by XCMPLX_0:def 2;
assume not z is real; then
not z in REAL; then
z in Funcs(2,REAL) \ { x where x is Element of Funcs(2,REAL): x.1 = 0
} by A1,CARD_1:50,NUMBERS:def 2,XBOOLE_0:def 3;
then reconsider f = z as Function of 2, REAL by FUNCT_2:66;
take f.0, f;
thus thesis;
end;
uniqueness;
consistency;
func Im z -> number means
:Def2:
it = 0 if z is real otherwise ex f being Function of
2,REAL st z = f & it = f.1;
existence
proof
thus z is real implies ex IT being set st IT = 0;
A2: z in COMPLEX by XCMPLX_0:def 2;
assume not z is real; then
not z in REAL; then
z in Funcs(2,REAL) \ { x where x is Element of Funcs(2,REAL): x.1 = 0
} by A2,CARD_1:50,NUMBERS:def 2,XBOOLE_0:def 3;
then reconsider f = z as Function of 2, REAL by FUNCT_2:66;
take f.1, f;
thus thesis;
end;
uniqueness;
consistency;
end;
registration
let z be Complex;
cluster Re z -> real;
coherence
proof
per cases;
suppose
z is real;
hence thesis by Def1;
end;
suppose
not z is real;
then consider f being Function of 2,REAL such that
z = f and
A1: Re z = f.0 by Def1;
0 in 2 by CARD_1:50,TARSKI:def 2;
then f.0 in REAL by FUNCT_2:5;
hence thesis by A1;
end;
end;
cluster Im z -> real;
coherence
proof
per cases;
suppose
z is real;
hence thesis by Def2;
end;
suppose
not z is real;
then consider f being Function of 2,REAL such that
z = f and
A2: Im z = f.1 by Def2;
1 in 2 by CARD_1:50,TARSKI:def 2;
then f.1 in REAL by FUNCT_2:5;
hence thesis by A2;
end;
end;
end;
definition
let z be Complex;
redefine func Re z -> Element of REAL;
coherence by XREAL_0:def 1;
redefine func Im z -> Element of REAL;
coherence by XREAL_0:def 1;
end;
registration
let r be Real;
cluster Im r -> zero;
coherence
proof
thus thesis by Def2;
end;
end;
theorem Th2:
for f being Function of 2,REAL
ex a,b being Element of REAL st f = (0,1)-->(a,b)
proof
let f be Function of 2,REAL;
0 in 2 & 1 in 2 by CARD_1:50,TARSKI:def 2;
then reconsider a = f.0, b = f.1 as Element of REAL by FUNCT_2:5;
take a,b;
dom f = {0,1} by CARD_1:50,FUNCT_2:def 1;
hence thesis by FUNCT_4:66;
end;
Lm2:
for a, b being Element of REAL holds Re [*a,b*] = a & Im [*a,b*] = b
proof
let a, b be Element of REAL;
reconsider a9 =a, b9 = b as Element of REAL;
thus Re [*a,b*] = a
proof
per cases;
suppose
b = 0;
then [*a,b*] = a by ARYTM_0:def 5;
hence thesis by Def1;
end;
suppose
b <> 0; then
A1: [*a,b*] = (0,1)-->(a9,b9) by ARYTM_0:def 5;
then reconsider f = [*a,b*] as Function of 2, REAL by CARD_1:50;
A2: not [*a,b*] in REAL & f.0 = a by A1,ARYTM_0:8,FUNCT_4:63; then
not [*a,b*] is real by XREAL_0:def 1;
hence thesis by Def1,A2;
end;
end;
per cases;
suppose
A2: b = 0;
then [*a,b*] = a by ARYTM_0:def 5;
hence thesis by A2;
end;
suppose
b <> 0;
then
A3: [*a,b*] = (0,1)-->(a9,b9) by ARYTM_0:def 5;
then reconsider f = [*a,b*] as Function of 2, REAL by CARD_1:50;
A4: not [*a,b*] in REAL & f.1 = b by A3,ARYTM_0:8,FUNCT_4:63; then
not [*a,b*] is real by XREAL_0:def 1;
hence thesis by Def2,A4;
end;
end;
reserve z,z1,z2 for Complex;
Lm3: [*Re z, Im z*] = z
proof
A1: z in COMPLEX by XCMPLX_0:def 2;
per cases;
suppose
A2: z is real;
then Im z = 0;
hence [*Re z, Im z*] = Re z by ARYTM_0:def 5
.= z by A2,Def1;
end;
suppose
A3: not z is real; then
a3: not z in REAL;
A4: ex f being Function of 2,REAL st z = f & Im z = f.1 by Def2,A3;
then consider a,b being Element of REAL such that
A5: z = (0,1)-->(a,b) by Th2;
reconsider f = z as Element of Funcs(2,REAL) by A5,CARD_1:50,FUNCT_2:8;
z in Funcs(2,REAL) \ { x where x is Element of Funcs(2,REAL): x.1 = 0
} by A1,a3,CARD_1:50,NUMBERS:def 2,XBOOLE_0:def 3;
then not z in { x where x is Element of Funcs(2,REAL): x.1 = 0} by
XBOOLE_0:def 5;
then f.1 <> 0;
then
A6: b <> 0 by A5,FUNCT_4:63;
ex f being Function of 2,REAL st z = f & Re z = f.0 by A3,Def1;
then
A7: Re z = a by A5,FUNCT_4:63;
Im z = b by A4,A5,FUNCT_4:63;
hence thesis by A5,A7,A6,ARYTM_0:def 5;
end;
end;
theorem Th3:
Re z1 = Re z2 & Im z1 = Im z2 implies z1 = z2
proof
assume Re z1 = Re z2 & Im z1 = Im z2;
hence z1 = [*Re z2,Im z2*] by Lm3
.= z2 by Lm3;
end;
definition
let z1,z2 be Complex;
redefine pred z1 = z2 means
Re z1 = Re z2 & Im z1 = Im z2;
compatibility by Th3;
end;
notation
synonym 0c for 0;
end;
definition
redefine func 0c -> Element of COMPLEX;
correctness by XCMPLX_0:def 2;
end;
definition
func 1r -> Element of COMPLEX equals
1;
correctness by XCMPLX_0:def 2;
redefine func * -> Element of COMPLEX;
coherence by XCMPLX_0:def 2;
end;
theorem Th4:
Re 0 = 0 & Im 0 = 0
proof
reconsider zz=0 as Element of REAL by XREAL_0:def 1;
0 = [*zz,zz*] by ARYTM_0:def 5;
hence thesis by Lm2;
end;
theorem Th5:
z = 0 iff (Re z)^2 + (Im z)^2 = 0
by Th4,Th1;
theorem Th6:
Re(1r) = 1 & Im(1r) = 0
proof
reconsider zz=0,j=1 as Element of REAL by XREAL_0:def 1;
1r = [*j,zz*] by ARYTM_0:def 5;
hence thesis by Lm2;
end;
theorem Th7:
Re(**) = 0 & Im(**) = 1
proof
reconsider zz=0,j=1 as Element of REAL by XREAL_0:def 1;
** = [*zz,j*] by ARYTM_0:def 5,XCMPLX_0:def 1;
hence thesis by Lm2;
end;
Lm7: for x being Real, x1,x2 being Element of REAL st x = [*x1,x2*]
holds x2 = 0 & x = x1
proof
let x be Real, 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,1) --> (x1,x2) by A1,ARYTM_0:def 5;
hence contradiction by A2,ARYTM_0:8;
end;
hence thesis by A1,ARYTM_0:def 5;
end;
Lm8: for x9,y9 being Element of REAL, x,y being Real st x9 = x & y9 = y
holds +(x9,y9) = x + y
proof
let x9,y9 be Element of REAL, x,y be Real such that
A1: x9 = x & y9 = y;
consider x1,x2,y1,y2 being Element of REAL such that
A2: x = [* x1,x2 *] & y = [*y1,y2*] and
A3: x+y = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
x2 = 0 & y2 = 0 by A2,Lm7;
then
A4: +(x2,y2) = 0 by ARYTM_0:11;
x = x1 & y = y1 by A2,Lm7;
hence thesis by A1,A3,A4,ARYTM_0:def 5;
end;
Lm9: 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 3;
then x + opp x = 0 by Lm8;
hence thesis;
end;
Lm10: for x9,y9 being Element of REAL, x,y being Real st x9 = x & y9 =
y holds *(x9,y9) = x * y
proof
let x9,y9 be Element of REAL, x,y be Real such that
A1: x9 = x & y9 = 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
;
x2 = 0 by A2,Lm7;
then
A5: *(x2,y1) = 0 by ARYTM_0:12;
A6: y2 = 0 by A3,Lm7;
then *(x1,y2) = 0 by ARYTM_0:12;
then
A7: +(*(x1,y2),*(x2,y1)) = 0 by A5,ARYTM_0:11;
x = x1 & y = y1 by A2,A3,Lm7;
hence *(x9,y9) = +(*(x1,y1),*(opp x2,y2)) by A1,A6,ARYTM_0:11,12
.= +(*(x1,y1),opp*(x2,y2)) by ARYTM_0:15
.= x * y by A4,A7,ARYTM_0:def 5;
end;
Lm11: for x,y,z being Complex st z = x + y holds Re z = Re x + Re y
proof
let x,y,z be Complex such that
A1: z = x + y;
consider x1,x2,y1,y2 being Element of REAL such that
A2: x = [*x1,x2*] & y = [*y1,y2*] and
A3: x + y = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
A4: Re x = x1 & Re y = y1 by A2,Lm2;
thus Re z = +(x1,y1) by A1,A3,Lm2
.= Re x + Re y by A4,Lm8;
end;
Lm12: for x,y,z being Complex st z = x+y holds Im z = Im x + Im y
proof
let x,y,z be Complex such that
A1: z = x+y;
consider x1,x2,y1,y2 being Element of REAL such that
A2: x = [*x1,x2*] & y = [*y1,y2*] and
A3: x + y = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
A4: Im x = x2 & Im y = y2 by A2,Lm2;
thus Im z = +(x2,y2) by A1,A3,Lm2
.= Im x + Im y by A4,Lm8;
end;
Lm13: for x,y,z being Complex st z = x * y holds Re z = Re x * Re y -
Im x * Im y
proof
let x,y,z be Complex such that
A1: z = x * y;
consider x1,x2,y1,y2 being Element of REAL such that
A2: x = [*x1,x2*] & y = [*y1,y2*] and
A3: x * y = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *] by
XCMPLX_0:def 5;
A4: Re x = x1 & Re y = y1 by A2,Lm2;
A5: Im x = x2 & Im y = y2 by A2,Lm2;
thus Re z = +(*(x1,y1),opp*(x2,y2)) by A1,A3,Lm2
.= *(x1,y1) + opp*(x2,y2) by Lm8
.= x1*y1 + opp*(x2,y2) by Lm10
.= x1*y1 + -*(x2,y2) by Lm9
.= x1*y1 - *(x2,y2)
.= Re x * Re y - Im x * Im y by A4,A5,Lm10;
end;
Lm14: for x,y,z being Complex st z = x*y holds Im z = Re x * Im y + Im
x * Re y
proof
let x,y,z be Complex such that
A1: z = x*y;
consider x1,x2,y1,y2 being Element of REAL such that
A2: x = [*x1,x2*] & y = [*y1,y2*] and
A3: x * y = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *] by
XCMPLX_0:def 5;
A4: Im x = x2 & Im y = y2 by A2,Lm2;
A5: Re x = x1 & Re y = y1 by A2,Lm2;
thus Im z = +(*(x1,y2),*(x2,y1)) by A1,A3,Lm2
.= *(x1,y2) + *(x2,y1) by Lm8
.= x1*y2 + *(x2,y1) by Lm10
.= Re x * Im y + Im x * Re y by A4,A5,Lm10;
end;
Lm15: z1+z2 = [* Re z1 + Re z2, Im z1 + Im z2 *]
proof
set z = [* Re z1 + Re z2, Im z1 + Im z2 *];
reconsider z9 = z1 + z2 as Element of COMPLEX by XCMPLX_0:def 2;
A1: Im z = Im z1 + Im z2 by Lm2
.= Im z9 by Lm12;
Re z = Re z1 + Re z2 by Lm2
.= Re z9 by Lm11;
hence thesis by A1;
end;
Lm16: z1 * z2 = [* Re z1 * Re z2 - Im z1 * Im z2, Re z1 * Im z2 + Re z2 * Im
z1 *]
proof
set z = [* Re z1 * Re z2 - Im z1 * Im z2, Re z1 * Im z2 + Re z2 * Im z1 *];
reconsider z9 = z1 * z2 as Element of COMPLEX by XCMPLX_0:def 2;
A1: Im z = Re z1 * Im z2 + Re z2 * Im z1 by Lm2
.= Im z9 by Lm14;
Re z = Re z1 * Re z2 - Im z1 * Im z2 by Lm2
.= Re z9 by Lm13;
hence thesis by A1;
end;
Lm17: Re(z1 * z2) = Re z1 * Re z2 - Im
z1 * Im z2 & Im(z1 * z2) = Re z1 * Im z2 + Re z2 * Im z1
proof
z1 * z2 = [*Re z1 * Re z2 - Im z1 * Im z2, Re z1 * Im z2 + Re z2 * Im z1
*] by Lm16;
hence thesis by Lm2;
end;
Lm18: 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 Lm15;
hence thesis by Lm2;
end;
Lm19: for x being Element of REAL holds Re (x***) = 0
proof
let x be Element of REAL;
thus Re (x***) = Re x * Re (**) - Im x * Im (**) by Lm17
.= Re x * 0 - 0 * Im (**) by Th7
.= 0;
end;
Lm20: for x being Element of REAL holds Im (x***) = x
proof
let x be Element of REAL;
thus Im (x***) = Re x * Im (**) + Im x * Re (**) by Lm17
.= x by Def1,Th7;
end;
Lm21: for x, y being Element of REAL holds [*x,y*] = x + y * **
proof
let x, y be Element of REAL;
A1: Im (x + y***) = Im x + Im (y***) by Lm18
.= 0 + Im (y***)
.= y by Lm20;
Re (x + y***) = Re x + Re (y***) by Lm18
.= Re x + 0 by Lm19
.= x by Def1;
hence thesis by A1,Lm3;
end;
definition
::$CD
end;
theorem Th8:
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 Lm15;
hence thesis by Lm2;
end;
definition
::$CD
end;
theorem Th9:
Re(z1 * z2) = Re z1 * Re z2 - Im z1 * Im z2 &
Im(z1 * z2) = Re z1 * Im z2 + Re z2 * Im z1
proof
z1 * z2 = [*Re z1 * Re z2 - Im z1 * Im z2, Re z1 * Im z2 + Re z2 * Im z1
*] by Lm16;
hence thesis by Lm2;
end;
theorem
Re (a***) = 0
proof
thus Re (a***) = Re a * Re (**) - Im a * Im (**) by Th9
.= Re a * 0 - 0 * Im (**) by Th7
.= 0;
end;
theorem
Im (a***) = a
proof
thus Im (a***) = Re a * Im (**) + Im a * Re (**) by Th9
.= a by Def1,Th7;
end;
theorem Th12:
Re(a+b***) = a & Im(a+b***) = b
proof
reconsider a,b as Element of REAL by XREAL_0:def 1;
(a+b***) = [*a,b*] by Lm21;
hence thesis by Lm2;
end;
theorem Th13:
Re z+(Im z)*** = z
proof
[*Re z, Im z*] = z by Lm3;
hence thesis by Lm21;
end;
theorem Th14:
Im z1 = 0 & Im z2 = 0 implies Re(z1*z2) = Re z1 * Re z2 & Im(z1*z2) = 0
proof
assume that
A1: Im z1 = 0 and
A2: Im z2 = 0;
thus Re(z1*z2) = Re z1 * Re z2 - Im z1 * Im z2 by Th9
.= Re z1 * Re z2 by A1;
thus Im(z1*z2) = Re z1 * Im z2 + Re z2 * Im z1 by Th9
.= 0 by A1,A2;
end;
theorem Th15:
Re z1 = 0 & Re z2 = 0 implies Re(z1*z2) = - Im z1 * Im z2 & Im(z1*z2) = 0
proof
assume that
A1: Re z1 = 0 and
A2: Re z2 = 0;
thus Re(z1*z2) = Re z1 * Re z2 - Im z1 * Im z2 by Th9
.= - Im z1 * Im z2 by A1;
thus Im(z1*z2) = Re z1 * Im z2 + Re z2 * Im z1 by Th9
.= 0 by A1,A2;
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)^2 - (Im z)^2 by Th9;
thus Im(z*z) = Re z *Im z + Re z *Im z by Th9
.= 2*(Re z *Im z);
end;
definition
::$CD
end;
Lm22: for z being Complex holds -z = -Re z+(-Im z)***
proof let z be Complex;
reconsider zz=0 as Element of REAL by XREAL_0:def 1;
set z9 = [* -Re z, -Im z *];
z9 + z = [* Re z9 + Re z, Im z9 + Im z *] by Lm15
.= [* -Re z + Re z, Im z9 + Im z *] by Lm2
.= [* zz, -Im z + Im z *] by Lm2
.= 0 by ARYTM_0:def 5;
hence thesis by Lm21;
end;
theorem Th17:
Re(-z) = -(Re z) & Im(-z) = -(Im z)
proof
-z = -Re z+(-Im z)*** by Lm22;
hence thesis by Th12;
end;
theorem
***** = -1r;
definition
::$CD
end;
Lm23: for z1,z2 being Complex holds
z1 - z2 = Re z1 - Re z2 + (Im z1 - Im z2)***
proof let z1,z2 be Complex;
A1: z1 = Re z1 + (Im z1)*** by Th13;
z1 - z2 = z1 + -z2 .= z1 + (-Re z2+(-Im z2)***) by Lm22
.= Re z1 - Re z2 + (Im z1 - Im z2)*** by A1;
hence thesis;
end;
theorem Th19:
Re(z1 - z2) = Re z1 - Re z2 & Im(z1 - z2) = Im z1 - Im z2
proof
thus Re(z1 - z2) = Re(Re z1 - Re z2 + (Im z1 - Im z2)***) by Lm23
.= Re z1 - Re z2 by Th12;
thus Im(z1 - z2) = Im(Re z1 - Re z2 + (Im z1 - Im z2)***) by Lm23
.= Im z1 - Im z2 by Th12;
end;
definition
::$CD
end;
Lm24: for z being Complex
holds z" = Re z / ((Re z)^2+(Im z)^2)+((- Im z) / ((Re z)^2+(Im z)^2))***
proof let z be Complex;
reconsider z9 =Re z / ((Re z)^2+(Im z)^2)+((- Im z) / ((Re z)^2+(Im z)^2))
*** as Element of COMPLEX by XCMPLX_0:def 2;
per cases;
suppose
z = 0;
hence thesis by Th4;
end;
suppose
A1: z <> 0;
then
A2: (Re z)^2+(Im z)^2 <> 0 by Th5;
A3: Im z9 = (-Im z) / ((Re z)^2+(Im z)^2) by Th12;
then
A4: Re z * Im z9 + Re z9 * Im z = (Re z)/1 * ((-Im z) / ((Re z)^2+(Im z)
^2)) + Re z / ((Re z)^2+(Im z)^2) * Im z by Th12
.= 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:76
.= 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:76
.= (- Re z * Im z + Re z * Im z) / ((Re z)^2+(Im z)^2) by XCMPLX_1:62
.= 0;
A5: Re z * Re z9 - Im z * Im z9 = (Re z)/1 * (Re z / ((Re z)^2+(Im z)^2)
) - Im z *((-Im z)/((Re z)^2+(Im z)^2)) by A3,Th12
.= 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:76
.= (Re z)^2 / ((Re z)^2+(Im z)^2) - Im z *(-Im z)/(1*((Re z)^2+(Im z
)^2)) by XCMPLX_1:76
.= (Re z)^2 / ((Re z)^2+(Im z)^2) - (-((Im z)^2))/(1*((Re z)^2+(Im z
)^2))
.= (Re z)^2 / ((Re z)^2+(Im z)^2) - -((Im z)^2)/((Re z)^2+(Im z)^2)
by XCMPLX_1:187
.= (Re z)^2 / ((Re z)^2+(Im z)^2) + (Im z)^2/(1*((Re z)^2+(Im z)^2))
.= ((Re z)^2 + (Im z)^2)/((Re z)^2+(Im z)^2) by XCMPLX_1:62
.= 1 by A2,XCMPLX_1:60;
z * z9= [*Re z * Re z9 - Im z * Im z9,Re z * Im z9 + Re z9 * Im z*]
by Lm16
.= 1 by A5,A4,ARYTM_0:def 5;
hence thesis by A1,XCMPLX_0:def 7;
end;
end;
theorem Th20:
Re(z") = Re z / ((Re z)^2+(Im z)^2) &
Im(z") = (- Im z) / ((Re z)^2+(Im z)^2)
proof
z" = Re z / ((Re z)^2+(Im z)^2)+((- Im z) / ((Re z)^2+(Im z)^2))***
by Lm24;
hence thesis by Th12;
end;
theorem
**" = -**;
theorem Th22:
Re z <> 0 & Im z = 0 implies Re(z") = (Re z)" & Im(z") = 0
proof
assume that
A1: Re z <> 0 and
A2: Im z = 0;
Re(z") = Re z / ((Re z)^2+(Im z)^2) by Th20;
hence Re(z") = (1*Re z) / (Re z * Re z) by A2
.= 1/Re z by A1,XCMPLX_1:91
.= (Re z)" by XCMPLX_1:215;
Im(z") = (- Im z) / ((Re z)^2+(Im z)^2) by Th20;
hence thesis by A2;
end;
theorem Th23:
Re z = 0 & Im z <> 0 implies Re(z") = 0 & Im(z") = -(Im z)"
proof
assume that
A1: Re z = 0 and
A2: Im z <> 0;
Re(z") = Re z / ((Re z)^2+(Im z)^2) by Th20;
hence Re(z") = 0 by A1;
Im(z") = (- Im z) / ((Re z)^2+(Im z)^2) by Th20;
hence Im(z") = -(1*Im z / (Im z * Im z)) by A1,XCMPLX_1:187
.= -(1 / Im z) by A2,XCMPLX_1:91
.= - (Im z)" by XCMPLX_1:215;
end;
definition
::$CD
end;
Lm25: for z1,z2 being Complex
holds 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))***
proof let z1,z2 be Complex;
reconsider z1,z2 as Element of COMPLEX by XCMPLX_0:def 2;
reconsider k = (Re z2)^2 + (Im z2)^2 as Element of REAL by XREAL_0:def 1;
reconsider r = Re z2/k, i = (-Im z2)/k as Element of REAL;
A1: Re[*r,i*] = Re(Re z2/k+(-Im z2)/k***) by Lm21
.= Re z2/k by Th12;
A2: Im[*r,i*] = Im(Re z2/k+(-Im z2)/k***) by Lm21
.= (-Im z2)/k by Th12;
reconsider r1 = (Re z1)/1 * (Re z2/k) - Im z1 * ((-Im z2)/k),
i1 =Re z1 * ((-Im z2)/k) + (Re z2/k) * Im z1
as Element of REAL by XREAL_0:def 1;
z1 / z2 = z1 * z2" by XCMPLX_0:def 9
.= z1*(r+i***) by Lm24
.= z1*[*r,i*] by Lm21
.= [* r1, i1 *] by A1,A2,Lm16
.= (Re z1)/1 * (Re z2/k) - Im z1 * ((-Im z2)/k)+ (Re z1 * ((-Im z2)/k)
+ (Re z2/k) * Im z1)*** by Lm21
.= 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:76
.= 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:76
.= 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:76
.= Re z1 * Re z2/k - Im z1 * (-Im z2)/k+ (Re z1 * (-Im z2)/k + Im z1 *
Re z2/(1*k))*** by XCMPLX_1:76
.= (Re z1 * Re z2 - Im z1 * (-Im z2))/k+ (Re z1 * (-Im z2)/k + Im z1 *
Re z2/(1*k))*** by XCMPLX_1:120
.= (Re z1 * Re z2 + Im z1 * Im z2)/k+ ((-Re z1 * Im z2 + Im z1 * Re z2
)/k)*** by XCMPLX_1:62
.= (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))***;
hence thesis;
end;
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
thus Re(z1 / z2) = Re((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 Lm25
.= (Re z1 * Re z2 + Im z1 * Im z2) / ((Re z2)^2 + (Im z2)^2) by Th12;
thus Im(z1 / z2) = Im((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 Lm25
.= (Re z2 * Im z1 - Re z1 * Im z2) / ((Re z2)^2 + (Im z2)^2) by Th12;
end;
theorem
Im z1 = 0 & Im z2 = 0 & Re z2 <> 0 implies Re(z1/z2) = (Re z1)/(Re z2)
& Im(z1/z2) = 0
proof
assume that
A1: Im z1 = 0 and
A2: Im z2 = 0 & Re z2 <> 0;
A3: z1/z2 = z1*z2" & Im(z2") = 0 by A2,Th22,XCMPLX_0:def 9;
hence Re(z1/z2) = (Re z1)*Re(z2") by A1,Th14
.= (Re z1)*(Re z2)" by A2,Th22
.= (Re z1)/(Re z2) by XCMPLX_0:def 9;
thus thesis by A1,A3,Th14;
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 that
A1: Re z1 = 0 and
A2: Re z2 = 0 & Im z2 <> 0;
A3: z1/z2 = z1*z2" & Re(z2") = 0 by A2,Th23,XCMPLX_0:def 9;
hence Re(z1/z2) = -(Im z1)*Im(z2") by A1,Th15
.= -(Im z1)*-(Im z2)" by A2,Th23
.= --(Im z1)*(Im z2)"
.= (Im z1)/(Im z2) by XCMPLX_0:def 9;
thus thesis by A1,A3,Th15;
end;
definition
let z be Complex;
func z*' -> Complex equals
Re z-(Im z)***;
correctness;
involutiveness
proof
let z,z9 be Complex;
assume z = Re z9-(Im z9)***;
then z = Re z9+(-Im z9)***;
then Re z = Re z9 & -Im z = --Im z9 by Th12;
hence z9= Re z+(-Im z)*** by Th13
.= Re z-(Im z)***;
end;
end;
theorem Th27:
Re (z*') = Re z & Im (z*') = -Im z
proof
z*' = Re z+(-Im z)***;
hence thesis by Th12;
end;
theorem
0*' = 0 by Th4;
theorem
z*' = 0 implies z = 0
proof
assume z*' = 0;
then 0 = Re z+(-Im z)***;
hence Re z = Re 0 & Im z = Im 0 by Th12;
end;
theorem
1r*' = 1r by Th6;
theorem
***' = -** by Th7;
theorem Th32:
(z1 + z2)*' = z1*' + z2*'
proof
thus Re ((z1 + z2)*') = Re(z1 + z2) by Th27
.= Re z1 + Re z2 by Th8
.= Re (z1*') + Re z2 by Th27
.= Re (z1*') + Re (z2*') by Th27
.= Re (z1*'+ z2*') by Th8;
thus Im ((z1 + z2)*') = -Im(z1 + z2) by Th27
.= -(Im z1 + --Im z2) by Th8
.= -Im z1 + -Im z2
.= Im (z1*') + -Im z2 by Th27
.= Im (z1*') + Im (z2*') by Th27
.= Im (z1*' + z2*') by Th8;
end;
theorem Th33:
(-z)*' = -(z*')
proof
thus Re ((-z)*') = Re -z by Th27
.= - Re z by Th17
.= - Re (z*') by Th27
.= Re -(z*') by Th17;
thus Im ((-z)*') = -Im -z by Th27
.= - -Im z by Th17
.= - Im (z*') by Th27
.= Im -(z*') by Th17;
end;
theorem
(z1 - z2)*' = z1*' - z2*'
proof
thus (z1 - z2)*' = (z1 + -z2)*' .= z1*' + (-z2)*' by Th32
.= z1*' + -(z2*') by Th33
.= z1*' - z2*';
end;
theorem Th35:
(z1*z2)*' = z1*'*z2*'
proof
A1: Re(z1*') = Re z1 & Re(z2*') = Re z2 by Th27;
A2: Im(z1*') = -Im z1 & Im(z2*') = -Im z2 by Th27;
thus Re((z1*z2)*') = Re(z1*z2) by Th27
.= (Re (z1*') * Re (z2*')) - (-Im (z1*')) * -Im (z2*') by A1,A2,Th9
.= (Re (z1*') * Re (z2*')) - --(Im (z1*') * Im (z2*'))
.= Re(z1*'*z2*') by Th9;
thus Im((z1*z2)*') = -Im(z1*z2) by Th27
.= -((Re (z1*') * -Im (z2*')) + (Re (z2*') * -Im (z1*'))) by A1,A2,Th9
.= (Re (z2*') * Im (z1*'))+--(Re (z1*') * Im (z2*'))
.= Im(z1*'*z2*') by Th9;
end;
theorem Th36:
z"*' = z*'"
proof
A1: Re z = Re (z*') & -Im z = Im (z*') by Th27;
thus Re(z"*') = Re(z") by Th27
.= Re z / ((Re z)^2+(Im z)^2) by Th20
.= (Re (z*')) / ((Re (z*'))^2+(Im (z*'))^2) by A1
.= Re(z*'") by Th20;
thus Im(z"*') = -Im(z") by Th27
.= -((- Im z) / ((Re z)^2+(Im z)^2)) by Th20
.= (-Im (z*'))/((Re (z*'))^2+(Im (z*'))^2) by A1,XCMPLX_1:187
.= Im(z*'") by Th20;
end;
theorem
(z1/z2)*' = (z1*')/(z2*')
proof
thus (z1/z2)*' = (z1*z2")*' by XCMPLX_0:def 9
.= (z1*'*z2"*') by Th35
.= (z1*'*z2*'") by Th36
.= (z1*')/(z2*') by XCMPLX_0:def 9;
end;
theorem Th38:
Im z = 0 implies z*' = z
by Th27;
registration
let r be Real;
reduce r*' to r;
reducibility by Th38;
end;
theorem
Re z = 0 implies z*' = -z
proof
assume
A1: Re z = 0;
hence z*' = -0+(-Im z)*** .= -z by A1,Lm22;
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 Th9
.= Re z * Re z - Im z * Im (z*') by Th27
.= Re z * Re z - Im z * -Im z by Th27
.= (Re z)^2 + (Im z)^2;
thus Im(z*(z*')) = Re z * Im (z*') + Re (z*') * Im z by Th9
.= Re z * -Im z + Re (z*') * Im z by Th27
.= -Re z * Im z + Re z * Im z by Th27
.= 0;
end;
theorem
Re(z + z*') = 2*Re z & Im(z + z*') = 0
proof
thus Re(z + z*') = Re z + Re (z*') by Th8
.= Re z + Re z by Th27
.= 2*Re z;
thus Im(z + (z*')) = Im z + Im (z*') by Th8
.= Im z + -Im z by Th27
.= 0;
end;
theorem
Re(z - z*') = 0 & Im(z - z*') = 2*Im z
proof
thus Re(z - z*') = Re z - Re (z*') by Th19
.= Re z - Re z by Th27
.= 0;
thus Im(z - z*') = Im z - Im (z*') by Th19
.= Im z - -Im z by Th27
.= 2*Im z;
end;
definition
let z be Complex;
func |.z.| -> Real equals
sqrt ((Re z)^2 + (Im z)^2);
coherence;
projectivity
proof
let r be Real;
reconsider rr = r as Element of REAL by XREAL_0:def 1;
let z be Complex;
assume
A1: r = sqrt ((Re z)^2 + (Im z)^2);
(Re z)^2 >= 0 & (Im z)^2 >= 0 by XREAL_1:63;
then r >= 0 by A1,SQUARE_1:def 2;
then
A2: Re rr >= 0 by Def1;
thus r = Re rr by Def1
.= sqrt ((Re r)^2 + (Im r)^2) by A2,SQUARE_1:22;
end;
end;
theorem Th43:
a >= 0 implies |.a.| = a
proof
assume a >= 0;
then Re a >= 0 by Def1;
hence |.a.| = Re a by SQUARE_1:22
.= a by Def1;
end;
registration let z be zero Complex;
cluster |.z.| -> zero;
coherence by Th4,SQUARE_1:17;
end;
theorem
|.0.| = 0;
registration
let z be non zero Complex;
cluster |.z.| -> non zero;
coherence
proof
assume |.z.| is zero;
then (Re z)^2 + (Im z)^2 = 0 by Lm1,SQUARE_1:24;
hence thesis by Th5;
end;
end;
theorem
|.z.| = 0 implies z = 0;
registration
let z;
cluster |.z.| -> non negative;
coherence
proof
0 <= (Re z)^2 + (Im z)^2 by Lm1;
hence thesis by SQUARE_1:def 2;
end;
end;
theorem
0 <= |.z.|;
theorem
z <> 0 iff 0 < |.z.|;
theorem Th48:
|.1r.| = 1 by Th6,SQUARE_1:18;
theorem
|.**.| = 1 by Th7,SQUARE_1:18;
Lm26: |.-z.| = |.z.|
proof
thus |.-z.| = sqrt ((-Re z)^2 + (Im -z)^2) by Th17
.= sqrt ((-Re z)^2 + (-Im z)^2) by Th17
.= |.z.|;
end;
Lm27: a <= 0 implies |.a.| = -a
proof
assume a <= 0;
then |.-a.| = -a by Th43;
hence thesis by Lm26;
end;
Lm28: sqrt a^2 = |.a.|
proof
per cases;
suppose
A1: 0 <= a;
then sqrt a^2 = a by SQUARE_1:22;
hence thesis by A1,Th43;
end;
suppose
A2: not 0 <= a;
then |.a.| = -a by Lm27;
hence thesis by A2,SQUARE_1:23;
end;
end;
theorem
Im z = 0 implies |.z.| = |.Re z.| by Lm28;
theorem
Re z = 0 implies |.z.| = |.Im z.| by Lm28;
theorem
|.-z.| = |.z.| by Lm26;
theorem Th53:
|.z*'.| = |.z.|
proof
thus |.z*'.| = sqrt ((Re z)^2 + (Im (z*'))^2) by Th27
.= sqrt ((Re z)^2 + (-Im z)^2) by Th27
.= |.z.|;
end;
Lm29: -|.a.| <= a & a <= |.a.|
proof
a < 0 implies -|.a.| <= a & a <= |.a.|
proof
assume a < 0;
then |.a.| = -a by Lm27;
hence thesis;
end;
hence thesis by Th43;
end;
theorem
Re z <= |.z.|
proof
0<=(Im z)^2 by XREAL_1:63;
then
A1: (Re z)^2+0 <= ((Re z)^2 + (Im z)^2) by XREAL_1:7;
0<=(Re z)^2 by XREAL_1:63;
then sqrt (Re z)^2 <= |.z.| by A1,SQUARE_1:26;
then
A2: |.Re z.| <= |.z.| by Lm28;
Re z <= |.Re z.| by Lm29;
hence thesis by A2,XXREAL_0:2;
end;
theorem
Im z <= |.z.|
proof
0<=(Re z)^2 by XREAL_1:63;
then
A1: (Im z)^2+0 <= ((Re z)^2 + (Im z)^2) by XREAL_1:7;
0<=(Im z)^2 by XREAL_1:63;
then sqrt (Im z)^2 <= |.z.| by A1,SQUARE_1:26;
then
A2: |.Im z.| <= |.z.| by Lm28;
Im z <= |.Im z.| by Lm29;
hence thesis by A2,XXREAL_0:2;
end;
theorem Th56:
|.z1 + z2.| <= |.z1.| + |.z2.|
proof
set r1 = Re z1, r2 = Re z2, i1 = Im z1, i2 = Im z2;
A1: (Im(z1 + z2))^2 = (i1 + i2)^2 by Th8
.= i1^2 + 2*i1*i2 + i2^2;
A2: 0 <= r1^2+i1^2 by Lm1;
(r1^2+i1^2)*(r2^2+i2^2)-(r1*r2+i1*i2)^2 = (r1*i2-i1*r2)^2;
then 0 <= (r1^2+i1^2)*(r2^2+i2^2)-(r1*r2+i1*i2)^2 by XREAL_1:63;
then
A3: (r1*r2+i1*i2)^2+0 <= (r1^2+i1^2)*(r2^2+i2^2) by XREAL_1:19;
r1*r2+i1*i2 <= |.r1*r2+i1*i2.| by Lm29;
then
A4: r1*r2+i1*i2 <= sqrt (r1*r2+i1*i2)^2 by Lm28;
A5: 0 <= r2^2+i2^2 by Lm1;
then
A6: (sqrt (r2^2+i2^2))^2 = r2^2+i2^2 by SQUARE_1:def 2;
0<=(r1*r2+i1*i2)^2 by XREAL_1:63;
then sqrt (r1*r2+i1*i2)^2 <= sqrt ((r1^2+i1^2)*(r2^2+i2^2)) by A3,SQUARE_1:26
;
then sqrt (r1*r2+i1*i2)^2 <= sqrt (r1^2+i1^2)*sqrt (r2^2+i2^2) by A2,A5,
SQUARE_1:29;
then
A7: r1*r2 + i1*i2 <= sqrt (r1^2+i1^2)*sqrt (r2^2+i2^2) by A4,XXREAL_0:2;
(2*r1*r2 + 2*i1*i2) = 2*(r1*r2 + i1*i2);
then (2*r1*r2 + 2*i1*i2) <= 2*(sqrt (r1^2+i1^2)*sqrt (r2^2+i2^2)) by A7,
XREAL_1:64;
then
A8: (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) by XREAL_1:7;
(Re(z1 + z2))^2 = (r1+ r2)^2 by Th8
.= r1^2 + 2*r1*r2 + r2^2;
then
(Re(z1+z2))^2+(Im(z1+z2))^2 = r1^2 + i1^2 + (2*r1*r2 + 2*i1*i2) + (r2^2
+ i2^2) by A1;
then
A9: (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 A8,XREAL_1:7;
A10: 0 <= (Re(z1 + z2))^2 + (Im(z1 + z2))^2 by Lm1;
(sqrt (r1^2+i1^2))^2 = r1^2+i1^2 by A2,SQUARE_1:def 2;
then sqrt ((Re(z1 + z2))^2 + (Im(z1 + z2))^2) <= sqrt ((sqrt (r1^2+i1^2) +
sqrt (r2^2+i2^2))^2) by A6,A9,A10,SQUARE_1:26;
hence thesis by SQUARE_1:22;
end;
theorem Th57:
|.z1 - z2.| <= |.z1.| + |.z2.|
proof
|.z1 - z2.| = |.z1 + - z2.|;
then |.z1 - z2.| <= |.z1.| + |.-z2.| by Th56;
hence thesis by Lm26;
end;
theorem
|.z1.| - |.z2.| <= |.z1 + z2.|
proof
z1 = z1 + z2 - z2;
then |.z1.| <= |.z1 + z2.| + |.z2.| by Th57;
hence thesis by XREAL_1:20;
end;
theorem Th59:
|.z1.| - |.z2.| <= |.z1 - z2.|
proof
z1 = z1 - z2 + z2;
then |.z1.| <= |.z1 - z2.| + |.z2.| by Th56;
hence thesis by XREAL_1:20;
end;
theorem Th60:
|.z1 - z2.| = |.z2 - z1.|
proof
thus |.z1 - z2.| = |.-(z2 - z1).| .= |.z2 - z1.| by Lm26;
end;
theorem Th61:
|.z1 - z2.| = 0 iff z1 = z2
proof
thus |.z1 - z2.| = 0 implies z1 = z2
proof
assume |.z1 - z2.| = 0;
then z1 - z2 = 0;
hence thesis;
end;
thus thesis;
end;
theorem
z1 <> z2 iff 0 < |.z1 - z2.|
proof
thus z1 <> z2 implies 0 < |.z1 - z2.|
proof
assume z1 <> z2;
then |.z1 - z2.| <> 0 by Th61;
hence thesis;
end;
thus thesis;
end;
theorem
|.z1 - z2.| <= |.z1 - z.| + |.z - z2.|
proof
|.z1 - z2.| = |.(z1 - z) + (z - z2).|;
hence thesis by Th56;
end;
Lm30: -b <= a & a <= b iff |.a.| <= b
proof
A1: |.a.| <= b implies -b <= a & a <= b
proof
assume
A2: |.a.| <= b;
a < -0 implies -b <= a & a <= b
proof
assume
A3: a < -0;
then -a <= b by A2,Lm27;
then -b <= -(-a) by XREAL_1:24;
hence thesis by A3;
end;
hence thesis by A2,Th43;
end;
-b <= a & a <= b implies |.a.| <= b
proof
assume that
A4: -b <= a and
A5: a <= b;
-a <= -(-b) by A4,XREAL_1:24;
then a < 0 implies |.a.| <= b by Lm27;
hence thesis by A5,Th43;
end;
hence thesis by A1;
end;
theorem
|.|.z1.| - |.z2.|.| <= |.z1 - z2.|
proof
|.z2.| - |.z1.| <= |.z2 - z1.| by Th59;
then -(|.z1.| - |.z2.|) <= |.z1 - z2.| by Th60;
then
A1: -|.z1 - z2.| <= --(|.z1.| - |.z2.|) by XREAL_1:24;
|.z1.| - |.z2.| <= |.z1 - z2.| by Th59;
hence thesis by A1,Lm30;
end;
theorem Th65:
|.z1*z2.| = |.z1.|*|.z2.|
proof
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 Lm1;
A2: (Im(z1*z2))^2 = (r1*i2 + r2*i1)^2 by Th9
.= 2*(r1*r2)*(i1*i2) + ((r1*i2)^2 + (r2*i1)^2);
(Re(z1*z2))^2 = (r1*r2 - i1*i2)^2 by Th9
.= (r1*r2)^2 + (i1*i2)^2 + - 2*(r1*r2)*(i1*i2);
then (Re(z1*z2))^2+(Im(z1*z2))^2 = (r1^2 + i1^2)*(r2^2 + i2^2) by A2;
hence thesis by A1,SQUARE_1:29;
end;
theorem Th66:
|.z".| = |.z.|"
proof
per cases;
suppose
A1: z <> 0;
set r2i2 = (Re z)^2+(Im z)^2;
A2: r2i2 <> 0 by A1,Th5;
A3: 0 <= r2i2 by Lm1;
thus |.z".| = sqrt ((Re z / r2i2)^2 + (Im(z"))^2) by Th20
.= sqrt ((Re z / r2i2)^2 + ((-Im z) / r2i2)^2) by Th20
.= sqrt ((Re z)^2 / r2i2^2 + ((-Im z) / r2i2)^2) by XCMPLX_1:76
.= sqrt ((Re z)^2 / r2i2^2 + (-Im z)^2 / r2i2^2) by XCMPLX_1:76
.= sqrt ((1*r2i2) / (r2i2*r2i2)) by XCMPLX_1:62
.= sqrt (1 / r2i2) by A2,XCMPLX_1:91
.= 1 / |.z.| by A3,SQUARE_1:18,30
.= |.z.|" by XCMPLX_1:215;
end;
suppose
A4: z = 0;
hence |.z".| = 0" .= |.z.|" by A4;
end;
end;
theorem Th67:
|.z1.| / |.z2.| = |.z1/z2.|
proof
thus |.z1.|/|.z2.| = |.z1.|*|.z2.|" by XCMPLX_0:def 9
.= |.z1.|*|.z2".| by Th66
.= |.z1*z2".| by Th65
.= |.z1/z2.| by XCMPLX_0:def 9;
end;
theorem
|.z*z.| = (Re z)^2 + (Im z)^2
proof
0<=(Re z)^2 + (Im z)^2 & |.z*z.| = |.z.|*|.z.| by Lm1,Th65;
then |.z*z.| = sqrt (((Re z)^2 + (Im z)^2)^2) by SQUARE_1:29;
hence thesis by Lm1,SQUARE_1:22;
end;
theorem
|.z*z.| = |.z*z*'.|
proof
thus |.z*z.| = |.z.|*|.z.| by Th65
.= |.z.|*|.z*'.| by Th53
.= |.z*z*'.| by Th65;
end;
:: Originally from SQUARE_1
theorem
a <= 0 implies |.a.| = -a by Lm27;
theorem Th71:
|.a.| = a or |.a.| = -a
proof
a >= 0 or a < 0;
hence thesis by Lm27,Th43;
end;
theorem :: SQUARE_1'91
sqrt a^2 = |.a.| by Lm28;
theorem :: SQUARE_1'34
min(a,b) = (a + b - |.a - b.|) / 2
proof
per cases;
suppose
A1: a <= b;
|.a - b.| = |.-(b - a).| .= |.b - a.| by Lm26
.= b - a by A1,Th43,XREAL_1:48;
hence thesis by A1,XXREAL_0:def 9;
end;
suppose
A2: b <= a;
hence min(a,b) = ((a+b)- (a - b))/2 by XXREAL_0:def 9
.= ((a+b)-|.a-b.|)/2 by A2,Th43,XREAL_1:48;
end;
end;
theorem :: SQUARE_1'45
max(a,b) = (a + b + |.a - b.|) / 2
proof
per cases;
suppose
A1: b <= a;
hence max(a,b) = ((a+b)+ (a - b))/2 by XXREAL_0:def 10
.= ((a+b)+|.a-b.|)/2 by A1,Th43,XREAL_1:48;
end;
suppose
A2: a <= b;
then
A3: 0 <= b - a by XREAL_1:48;
thus max(a,b) = ((a+b)+ -(a - b))/2 by A2,XXREAL_0:def 10
.= ((a+b)+|.-(a-b).|)/2 by A3,Th43
.= ((a+b)+|.a-b.|)/2 by Lm26;
end;
end;
theorem Th75: :: SQUARE_1'62
|.a.|^2 = a^2
proof
|.a.| = a or |.a.| = -a by Th71;
hence thesis;
end;
theorem
-|.a.| <= a & a <= |.a.| by Lm29;
theorem
a+b*** = c+d*** implies a = c & b = d
proof
assume
A1: a+b*** = c+d***;
then a-c+(b-d)*** = 0;
then a-c = 0 by Th4,Th12;
hence thesis by A1;
end;
:: from JGRAPH_1, 29.12.2006, AK
theorem
sqrt(a^2+b^2) <= |.a.|+|.b.|
proof
A1: (sqrt(a^2+b^2))^2>=0 by XREAL_1:63;
a^2>=0 & b^2>=0 by XREAL_1:63;
then
A2: (sqrt(a^2+b^2))^2=a^2+b^2 by SQUARE_1:def 2;
(|.a.|+|.b.|)^2=(|.a.|)^2+2*(|.a.|)*(|.b.|)+(|.b.|)^2 & |.a.|^2=a^2
by Th75;
then
(|.a.|+|.b.|)^2 - (sqrt(a^2+b^2))^2= a^2+2*(|.a.|)*(|.b.|)+b
^2-(a^2+b^2) by A2,Th75
.=2*(|.a.|)*(|.b.|);
then (|.a.|+|.b.|)^2>= (sqrt(a^2+b^2))^2 by XREAL_1:49;
then sqrt((|.a.|+|.b.|)^2)>=sqrt((sqrt(a^2+b^2))^2) by A1,SQUARE_1:26;
hence thesis by A2,SQUARE_1:22;
end;
theorem
|.a.| <= sqrt(a^2+b^2)
proof
a^2>=0 & a^2+0<= a^2+b^2 by XREAL_1:6,63;
then sqrt(a^2)<= sqrt(a^2+b^2) by SQUARE_1:26;
hence thesis by Lm28;
end;
theorem
|. 1/z1 .| = 1 / |.z1.| by Th48,Th67;
theorem
for z1,z2 being Complex
holds z1 + z2 = Re z1 + Re z2 + (Im z1 + Im z2)***
proof let z1,z2 be Complex;
z1 + z2 = [* Re z1 + Re z2, Im z1 + Im z2 *] by Lm15;
hence thesis by Lm21;
end;
theorem
for z1,z2 being Complex holds
z1 * z2 = Re z1 * Re z2 - Im z1 * Im z2+(Re z1 * Im z2 + Re z2 * Im z1)***
proof let z1,z2 be Complex;
z1 * z2 = [* Re z1 * Re z2 - Im z1 * Im z2, Re z1 * Im z2 + Re z2 * Im
z1 *] by Lm16;
hence thesis by Lm21;
end;
theorem
for z being Complex holds -z = -Re z+(-Im z)*** by Lm22;
theorem
for z1,z2 being Complex holds
z1 - z2 = Re z1 - Re z2 + (Im z1 - Im z2)*** by Lm23;
theorem
for z being Complex
holds z" = Re z / ((Re z)^2+(Im z)^2)+((- Im z) / ((Re z)^2+(Im z)^2))***
by Lm24;
theorem
for z1,z2 being Complex
holds 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 Lm25;
*