:: The Complex Numbers :: by Czes{\l}aw Byli\'nski :: :: Received March 1, 1990 :: Copyright (c) 1990-2021 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, ARITHM; begin reserve a,b,c,d for Real; :: Auxiliary theorems theorem :: COMPLEX1:1 a^2 + b^2 = 0 implies a = 0; :: Complex Numbers definition let z be Complex; func Re z -> number means :: COMPLEX1:def 1 it = z if z is real otherwise ex f being Function of 2,REAL st z = f & it = f.0; func Im z -> number means :: COMPLEX1:def 2 it = 0 if z is real otherwise ex f being Function of 2,REAL st z = f & it = f.1; end; registration let z be Complex; cluster Re z -> real; cluster Im z -> real; end; definition let z be Complex; redefine func Re z -> Element of REAL; redefine func Im z -> Element of REAL; end; registration let r be Real; cluster Im r -> zero; end; theorem :: COMPLEX1:2 for f being Function of 2,REAL ex a,b being Element of REAL st f = (0,1)-->(a,b); reserve z,z1,z2 for Complex; theorem :: COMPLEX1:3 Re z1 = Re z2 & Im z1 = Im z2 implies z1 = z2; definition let z1,z2 be Complex; redefine pred z1 = z2 means :: COMPLEX1:def 3 Re z1 = Re z2 & Im z1 = Im z2; end; notation synonym 0c for 0; end; definition redefine func 0c -> Element of COMPLEX; end; definition func 1r -> Element of COMPLEX equals :: COMPLEX1:def 4 1; redefine func -> Element of COMPLEX; end; theorem :: COMPLEX1:4 Re 0 = 0 & Im 0 = 0; theorem :: COMPLEX1:5 z = 0 iff (Re z)^2 + (Im z)^2 = 0; theorem :: COMPLEX1:6 Re(1r) = 1 & Im(1r) = 0; theorem :: COMPLEX1:7 Re() = 0 & Im() = 1; definition ::$CD end; theorem :: COMPLEX1:8 Re(z1 + z2) = Re z1 + Re z2 & Im(z1 + z2) = Im z1 + Im z2; definition ::$CD end; theorem :: COMPLEX1:9 Re(z1 * z2) = Re z1 * Re z2 - Im z1 * Im z2 & Im(z1 * z2) = Re z1 * Im z2 + Re z2 * Im z1; theorem :: COMPLEX1:10 Re (a*) = 0; theorem :: COMPLEX1:11 Im (a*) = a; theorem :: COMPLEX1:12 Re(a+b*) = a & Im(a+b*) = b; theorem :: COMPLEX1:13 Re z+(Im z)* = z; theorem :: COMPLEX1:14 Im z1 = 0 & Im z2 = 0 implies Re(z1*z2) = Re z1 * Re z2 & Im(z1*z2) = 0; theorem :: COMPLEX1:15 Re z1 = 0 & Re z2 = 0 implies Re(z1*z2) = - Im z1 * Im z2 & Im(z1*z2) = 0; theorem :: COMPLEX1:16 Re(z*z) = (Re z)^2 - (Im z)^2 & Im(z*z) = 2*(Re z *Im z); definition ::$CD end; theorem :: COMPLEX1:17 Re(-z) = -(Re z) & Im(-z) = -(Im z); theorem :: COMPLEX1:18 * = -1r; definition ::$CD end; theorem :: COMPLEX1:19 Re(z1 - z2) = Re z1 - Re z2 & Im(z1 - z2) = Im z1 - Im z2; definition ::$CD end; theorem :: COMPLEX1:20 Re(z") = Re z / ((Re z)^2+(Im z)^2) & Im(z") = (- Im z) / ((Re z)^2+(Im z)^2); theorem :: COMPLEX1:21 " = -; theorem :: COMPLEX1:22 Re z <> 0 & Im z = 0 implies Re(z") = (Re z)" & Im(z") = 0; theorem :: COMPLEX1:23 Re z = 0 & Im z <> 0 implies Re(z") = 0 & Im(z") = -(Im z)"; definition ::$CD end; theorem :: COMPLEX1:24 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); theorem :: COMPLEX1:25 Im z1 = 0 & Im z2 = 0 & Re z2 <> 0 implies Re(z1/z2) = (Re z1)/(Re z2) & Im(z1/z2) = 0; theorem :: COMPLEX1:26 Re z1 = 0 & Re z2 = 0 & Im z2 <> 0 implies Re(z1/z2) = (Im z1)/(Im z2) & Im(z1/z2) = 0; definition let z be Complex; func z*' -> Complex equals :: COMPLEX1:def 11 Re z-(Im z)*; involutiveness; end; theorem :: COMPLEX1:27 Re (z*') = Re z & Im (z*') = -Im z; theorem :: COMPLEX1:28 0*' = 0; theorem :: COMPLEX1:29 z*' = 0 implies z = 0; theorem :: COMPLEX1:30 1r*' = 1r; theorem :: COMPLEX1:31 *' = -; theorem :: COMPLEX1:32 (z1 + z2)*' = z1*' + z2*'; theorem :: COMPLEX1:33 (-z)*' = -(z*'); theorem :: COMPLEX1:34 (z1 - z2)*' = z1*' - z2*'; theorem :: COMPLEX1:35 (z1*z2)*' = z1*'*z2*'; theorem :: COMPLEX1:36 z"*' = z*'"; theorem :: COMPLEX1:37 (z1/z2)*' = (z1*')/(z2*'); theorem :: COMPLEX1:38 Im z = 0 implies z*' = z; registration let r be Real; reduce r*' to r; end; theorem :: COMPLEX1:39 Re z = 0 implies z*' = -z; theorem :: COMPLEX1:40 Re(z*z*') = (Re z)^2 + (Im z)^2 & Im(z*z*') = 0; theorem :: COMPLEX1:41 Re(z + z*') = 2*Re z & Im(z + z*') = 0; theorem :: COMPLEX1:42 Re(z - z*') = 0 & Im(z - z*') = 2*Im z; definition let z be Complex; func |.z.| -> Real equals :: COMPLEX1:def 12 sqrt ((Re z)^2 + (Im z)^2); projectivity; end; theorem :: COMPLEX1:43 a >= 0 implies |.a.| = a; registration let z be zero Complex; cluster |.z.| -> zero; end; theorem :: COMPLEX1:44 |.0.| = 0; registration let z be non zero Complex; cluster |.z.| -> non zero; end; theorem :: COMPLEX1:45 |.z.| = 0 implies z = 0; registration let z; cluster |.z.| -> non negative; end; theorem :: COMPLEX1:46 0 <= |.z.|; theorem :: COMPLEX1:47 z <> 0 iff 0 < |.z.|; theorem :: COMPLEX1:48 |.1r.| = 1; theorem :: COMPLEX1:49 |..| = 1; theorem :: COMPLEX1:50 Im z = 0 implies |.z.| = |.Re z.|; theorem :: COMPLEX1:51 Re z = 0 implies |.z.| = |.Im z.|; theorem :: COMPLEX1:52 |.-z.| = |.z.|; theorem :: COMPLEX1:53 |.z*'.| = |.z.|; theorem :: COMPLEX1:54 Re z <= |.z.|; theorem :: COMPLEX1:55 Im z <= |.z.|; theorem :: COMPLEX1:56 |.z1 + z2.| <= |.z1.| + |.z2.|; theorem :: COMPLEX1:57 |.z1 - z2.| <= |.z1.| + |.z2.|; theorem :: COMPLEX1:58 |.z1.| - |.z2.| <= |.z1 + z2.|; theorem :: COMPLEX1:59 |.z1.| - |.z2.| <= |.z1 - z2.|; theorem :: COMPLEX1:60 |.z1 - z2.| = |.z2 - z1.|; theorem :: COMPLEX1:61 |.z1 - z2.| = 0 iff z1 = z2; theorem :: COMPLEX1:62 z1 <> z2 iff 0 < |.z1 - z2.|; theorem :: COMPLEX1:63 |.z1 - z2.| <= |.z1 - z.| + |.z - z2.|; theorem :: COMPLEX1:64 |.|.z1.| - |.z2.|.| <= |.z1 - z2.|; theorem :: COMPLEX1:65 |.z1*z2.| = |.z1.|*|.z2.|; theorem :: COMPLEX1:66 |.z".| = |.z.|"; theorem :: COMPLEX1:67 |.z1.| / |.z2.| = |.z1/z2.|; theorem :: COMPLEX1:68 |.z*z.| = (Re z)^2 + (Im z)^2; theorem :: COMPLEX1:69 |.z*z.| = |.z*z*'.|; :: Originally from SQUARE_1 theorem :: COMPLEX1:70 a <= 0 implies |.a.| = -a; theorem :: COMPLEX1:71 |.a.| = a or |.a.| = -a; theorem :: COMPLEX1:72 :: SQUARE_1'91 sqrt a^2 = |.a.|; theorem :: COMPLEX1:73 :: SQUARE_1'34 min(a,b) = (a + b - |.a - b.|) / 2; theorem :: COMPLEX1:74 :: SQUARE_1'45 max(a,b) = (a + b + |.a - b.|) / 2; theorem :: COMPLEX1:75 :: SQUARE_1'62 |.a.|^2 = a^2; theorem :: COMPLEX1:76 -|.a.| <= a & a <= |.a.|; theorem :: COMPLEX1:77 a+b* = c+d* implies a = c & b = d; :: from JGRAPH_1, 29.12.2006, AK theorem :: COMPLEX1:78 sqrt(a^2+b^2) <= |.a.|+|.b.|; theorem :: COMPLEX1:79 |.a.| <= sqrt(a^2+b^2); theorem :: COMPLEX1:80 |. 1/z1 .| = 1 / |.z1.|; theorem :: COMPLEX1:81 for z1,z2 being Complex holds z1 + z2 = Re z1 + Re z2 + (Im z1 + Im z2)*; theorem :: COMPLEX1:82 for z1,z2 being Complex holds z1 * z2 = Re z1 * Re z2 - Im z1 * Im z2+(Re z1 * Im z2 + Re z2 * Im z1)*; theorem :: COMPLEX1:83 for z being Complex holds -z = -Re z+(-Im z)*; theorem :: COMPLEX1:84 for z1,z2 being Complex holds z1 - z2 = Re z1 - Re z2 + (Im z1 - Im z2)*; theorem :: COMPLEX1:85 for z being Complex holds z" = Re z / ((Re z)^2+(Im z)^2)+((- Im z) / ((Re z)^2+(Im z)^2))*; theorem :: COMPLEX1:86 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))*;