:: The Complex Numbers :: by Czes{\l}aw Byli\'nski :: :: Received March 1, 1990 :: Copyright (c) 1990-2017 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; 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 -> set 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 -> set 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; reconsider zz=0, j=1 as Element of REAL by XREAL_0:def 1; Lm4: 0 = [*zz,zz*] by ARYTM_0:def 5; Lm5: 1r = [*j,zz*] by ARYTM_0:def 5; theorem Th4: Re 0 = 0 & Im 0 = 0 by Lm2,Lm4; theorem Th5: z = 0 iff (Re z)^2 + (Im z)^2 = 0 by Th4,Th1; theorem Th6: Re(1r) = 1 & Im(1r) = 0 by Lm2,Lm5; Lm6: = [*zz,j*] by ARYTM_0:def 5,XCMPLX_0:def 1; theorem Th7: Re() = 0 & Im() = 1 by Lm2,Lm6; 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; 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;