### The Mizar article:

### The Field of Complex Numbers

**by****Anna Justyna Milewska**

- Received January 18, 2000
Copyright (c) 2000 Association of Mizar Users

- MML identifier: COMPLFLD
- [ MML identifier index ]

environ vocabulary COMPLEX1, ARYTM, VECTSP_1, RLVECT_1, COMPLSP1, BINOP_1, LATTICES, FUNCT_1, ARYTM_1, RELAT_1, ARYTM_3, ABSVALUE, COMPLFLD, XCMPLX_0; notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, ORDINAL1, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, REAL_1, BINOP_1, ABSVALUE, RLVECT_1, VECTSP_1, COMPLSP1, COMPLEX1, FUNCT_1; constructors REAL_1, ABSVALUE, VECTSP_1, COMPLSP1, DOMAIN_1, BINOP_1, COMPLEX1, MEMBERED, ARYTM_0, ARYTM_3, FUNCT_4; clusters VECTSP_1, RELSET_1, XREAL_0, COMPLEX1, MEMBERED; requirements NUMERALS, SUBSET, BOOLE, ARITHM; definitions RLVECT_1, VECTSP_1; theorems STRUCT_0, COMPLEX1, RLVECT_1, BINOP_1, COMPLSP1, VECTSP_1, XREAL_0, XCMPLX_0, XCMPLX_1, ARYTM_0; begin canceled; theorem Th2: for x1,y1,x2,y2 be Element of REAL holds [*x1,y1*] + [*x2,y2*] = [*x1 + x2,y1 + y2*] proof let x1,y1,x2,y2 be Element of REAL; thus [*x1,y1*] + [*x2,y2*] = [*Re[*x1,y1*] + Re[*x2,y2*],Im[*x1,y1*] + Im[*x2,y2*]*] by COMPLEX1:def 9 .=[*x1 + Re[*x2,y2*],Im[*x1,y1*] + Im[*x2,y2*]*] by COMPLEX1:7 .=[*x1 + x2,Im[*x1,y1*] + Im[*x2,y2*]*] by COMPLEX1:7 .=[*x1 + x2,y1 + Im[*x2,y2*]*] by COMPLEX1:7 .=[*x1 + x2,y1 + y2*] by COMPLEX1:7; end; definition func F_Complex -> strict doubleLoopStr means :Def1: the carrier of it = COMPLEX & the add of it = addcomplex & the mult of it = multcomplex & the unity of it = 1r & the Zero of it = 0c; existence proof take doubleLoopStr (# COMPLEX,addcomplex,multcomplex,1r,0c #); thus thesis; end; uniqueness; end; definition cluster F_Complex -> non empty; coherence proof the carrier of F_Complex is non empty by Def1; hence F_Complex is non empty by STRUCT_0:def 1; end; end; definition cluster -> complex Element of F_Complex; coherence proof let c be Element of F_Complex; the carrier of F_Complex is non empty by Def1; then c in the carrier of F_Complex; then c in COMPLEX by Def1; hence thesis by XCMPLX_0:def 2; end; end; definition cluster F_Complex -> add-associative right_zeroed right_complementable Abelian commutative associative left_unital right_unital distributive Field-like non degenerated; coherence proof thus F_Complex is add-associative proof let x,y,z be Element of F_Complex; reconsider x1=x, y1=y, z1=z as Element of COMPLEX by Def1; thus (x + y) + z = (the add of F_Complex).[x + y,z1] by RLVECT_1:def 3 .= (the add of F_Complex).[(the add of F_Complex).[x1,y1],z1] by RLVECT_1:def 3 .= addcomplex.[(the add of F_Complex).[x1,y1],z1] by Def1 .= addcomplex.[addcomplex.[x1,y1],z1] by Def1 .= addcomplex.(addcomplex.[x1,y1],z1) by BINOP_1:def 1 .= addcomplex.(addcomplex.(x1,y1),z1) by BINOP_1:def 1 .= addcomplex.(x1 + y1,z1) by COMPLSP1:def 1 .=(x1 + y1) + z1 by COMPLSP1:def 1 .= x1 + (y1 + z1) by XCMPLX_1:1 .= addcomplex.(x1,y1 + z1) by COMPLSP1:def 1 .= addcomplex.(x1,addcomplex.(y1,z1)) by COMPLSP1:def 1 .= addcomplex.[x1,addcomplex.(y1,z1)] by BINOP_1:def 1 .= addcomplex.[x1,addcomplex.[y1,z1]] by BINOP_1:def 1 .= addcomplex.[x1,(the add of F_Complex).[y1,z1]] by Def1 .= (the add of F_Complex).[x1,(the add of F_Complex).[y1,z1]] by Def1 .= (the add of F_Complex).[x1,y + z] by RLVECT_1:def 3 .= x + (y + z) by RLVECT_1:def 3; end; thus F_Complex is right_zeroed proof let x be Element of F_Complex; reconsider x1=x as Element of COMPLEX by Def1; thus x + 0.F_Complex =(the add of F_Complex).[x1,0.F_Complex] by RLVECT_1:def 3 .= (the add of F_Complex).(x1,0.F_Complex) by BINOP_1:def 1 .= (the add of F_Complex).(x1,the Zero of F_Complex) by RLVECT_1:def 2 .= (the add of F_Complex).(x1,0c) by Def1 .= addcomplex.(x1,0c) by Def1 .= x1 + 0c by COMPLSP1:def 1 .= x by COMPLEX1:22; end; thus F_Complex is right_complementable proof let x be Element of F_Complex; reconsider x1=x as Element of COMPLEX by Def1; reconsider y=-x1 as Element of F_Complex by Def1; take y; thus x + y = (the add of F_Complex).[x,y] by RLVECT_1:def 3 .= (the add of F_Complex).(x,y) by BINOP_1:def 1 .= addcomplex.(x1,y) by Def1 .= x1+ -x1 by COMPLSP1:def 1 .= 0c by XCMPLX_0:def 6 .= the Zero of F_Complex by Def1 .= 0.F_Complex by RLVECT_1:def 2; end; thus F_Complex is Abelian proof let x,y be Element of F_Complex; reconsider x1=x ,y1=y as Element of COMPLEX by Def1; thus x + y = (the add of F_Complex).[x1,y1] by RLVECT_1:def 3 .= (the add of F_Complex).(x1,y1) by BINOP_1:def 1 .= addcomplex.(x1,y1) by Def1 .= y1 + x1 by COMPLSP1:def 1 .= addcomplex.(y1,x1) by COMPLSP1:def 1 .= (the add of F_Complex).(y1,x1) by Def1 .= (the add of F_Complex).[y1,x1] by BINOP_1:def 1 .= y + x by RLVECT_1:def 3; end; thus F_Complex is commutative proof let x,y be Element of F_Complex; reconsider x1=x ,y1=y as Element of COMPLEX by Def1; thus x * y = (the mult of F_Complex).(x1,y1) by VECTSP_1:def 10 .= multcomplex.(x1,y1) by Def1 .= y1 * x1 by COMPLSP1:def 4 .= multcomplex.(y1,x1) by COMPLSP1:def 4 .= (the mult of F_Complex).(y1,x1) by Def1 .= y * x by VECTSP_1:def 10; end; thus F_Complex is associative proof let x,y,z be Element of F_Complex; reconsider x1=x, y1=y, z1=z as Element of COMPLEX by Def1; thus (x * y) * z = (the mult of F_Complex).(x * y,z1) by VECTSP_1:def 10 .= (the mult of F_Complex).((the mult of F_Complex).(x1,y1),z1) by VECTSP_1:def 10 .= multcomplex.((the mult of F_Complex).(x1,y1),z1) by Def1 .= multcomplex.(multcomplex.(x1,y1),z1) by Def1 .= multcomplex.(x1 * y1,z1) by COMPLSP1:def 4 .= (x1 * y1) * z1 by COMPLSP1:def 4 .= x1 * (y1 * z1) by XCMPLX_1:4 .= multcomplex.(x1,y1 * z1) by COMPLSP1:def 4 .= multcomplex.(x1,multcomplex.(y1,z1)) by COMPLSP1:def 4 .= multcomplex.(x1,(the mult of F_Complex).(y1,z1)) by Def1 .= (the mult of F_Complex).(x1,(the mult of F_Complex).(y1,z1)) by Def1 .= (the mult of F_Complex).(x1,y * z) by VECTSP_1:def 10 .= x * (y * z) by VECTSP_1:def 10; end; thus F_Complex is left_unital proof let x be Element of F_Complex; reconsider x1=x as Element of COMPLEX by Def1; thus (1_ F_Complex)*x =(the mult of F_Complex).(1_ F_Complex,x1) by VECTSP_1:def 10 .= multcomplex.(1_ F_Complex,x1) by Def1 .= multcomplex.(the unity of F_Complex,x1) by VECTSP_1:def 9 .= multcomplex.(1r,x1) by Def1 .= 1r * x1 by COMPLSP1:def 4 .= x by COMPLEX1:29; end; thus F_Complex is right_unital proof let x be Element of F_Complex; reconsider x1=x as Element of COMPLEX by Def1; thus x*(1_ F_Complex) =(the mult of F_Complex).(x1,1_ F_Complex) by VECTSP_1:def 10 .= multcomplex.(x1,1_ F_Complex) by Def1 .= multcomplex.(x1,the unity of F_Complex) by VECTSP_1:def 9 .= multcomplex.(x1,1r) by Def1 .= x1 * 1r by COMPLSP1:def 4 .= x by COMPLEX1:29; end; thus F_Complex is distributive proof let x,y,z be Element of F_Complex; reconsider x1=x, y1=y, z1=z as Element of COMPLEX by Def1; thus x*(y+z)=(the mult of F_Complex).(x1,y+z) by VECTSP_1:def 10 .= (the mult of F_Complex).(x1,(the add of F_Complex).[y1,z1]) by RLVECT_1:def 3 .= (the mult of F_Complex).(x1,(the add of F_Complex).(y1,z1)) by BINOP_1:def 1 .= multcomplex.(x1,(the add of F_Complex).(y1,z1)) by Def1 .= multcomplex.(x1,addcomplex.(y1,z1)) by Def1 .= multcomplex.(x1,y1 + z1) by COMPLSP1:def 1 .= x1 * (y1 + z1) by COMPLSP1:def 4 .= x1 * y1 + x1 * z1 by XCMPLX_1:8 .= addcomplex.(x1 * y1,x1 * z1) by COMPLSP1:def 1 .= addcomplex.(multcomplex.(x1,y1),x1 * z1) by COMPLSP1:def 4 .= addcomplex.(multcomplex.(x1,y1),multcomplex.(x1,z1)) by COMPLSP1:def 4 .= (the add of F_Complex).(multcomplex.(x1,y1),multcomplex.(x1,z1)) by Def1 .= (the add of F_Complex).((the mult of F_Complex).(x1,y1), multcomplex.(x1,z1)) by Def1 .= (the add of F_Complex).((the mult of F_Complex).(x1,y1), (the mult of F_Complex).(x1,z1)) by Def1 .= (the add of F_Complex).[(the mult of F_Complex).(x1,y1), (the mult of F_Complex).(x1,z1)] by BINOP_1:def 1 .= (the add of F_Complex).[x * y,(the mult of F_Complex).(x1,z1)] by VECTSP_1:def 10 .= (the add of F_Complex).[x * y , x * z ] by VECTSP_1:def 10 .= x*y+x*z by RLVECT_1:def 3; thus (y+z)*x = (the mult of F_Complex).(y+z,x1) by VECTSP_1:def 10 .= (the mult of F_Complex).((the add of F_Complex).[y1,z1],x1) by RLVECT_1:def 3 .= (the mult of F_Complex).((the add of F_Complex).(y1,z1),x1) by BINOP_1:def 1 .= multcomplex.((the add of F_Complex).(y1,z1),x1) by Def1 .= multcomplex.(addcomplex.(y1,z1),x1) by Def1 .= multcomplex.(y1 + z1,x1) by COMPLSP1:def 1 .= (y1 + z1) * x1 by COMPLSP1:def 4 .= y1 * x1 + z1 * x1 by XCMPLX_1:8 .= addcomplex.(y1 * x1,z1 * x1) by COMPLSP1:def 1 .= addcomplex.(multcomplex.(y1,x1),z1 * x1) by COMPLSP1:def 4 .= addcomplex.(multcomplex.(y1,x1),multcomplex.(z1,x1)) by COMPLSP1:def 4 .= (the add of F_Complex).(multcomplex.(y1,x1),multcomplex.(z1,x1)) by Def1 .= (the add of F_Complex).((the mult of F_Complex).(y1,x1), multcomplex.(z1,x1)) by Def1 .= (the add of F_Complex).((the mult of F_Complex).(y1,x1), (the mult of F_Complex).(z1,x1)) by Def1 .= (the add of F_Complex).[(the mult of F_Complex).(y1,x1), (the mult of F_Complex).(z1,x1)] by BINOP_1:def 1 .= (the add of F_Complex).[y * x,(the mult of F_Complex).(z1,x1)] by VECTSP_1:def 10 .= (the add of F_Complex).[y * x , z * x ] by VECTSP_1:def 10 .= y * x + z * x by RLVECT_1:def 3; end; thus F_Complex is Field-like proof let x be Element of F_Complex; assume A1: x <> 0.F_Complex; reconsider x1=x as Element of COMPLEX by Def1; reconsider y=x1" as Element of F_Complex by Def1; take y; x1<>the Zero of F_Complex by A1,RLVECT_1:def 2; then A2: x1<>0c by Def1; thus x * y = (the mult of F_Complex).(x1,x1") by VECTSP_1:def 10 .=multcomplex.(x1,x1") by Def1 .=x1 * x1" by COMPLSP1:def 4 .=1r by A2,COMPLEX1:65 .=the unity of F_Complex by Def1 .=1_ F_Complex by VECTSP_1:def 9; end; thus F_Complex is non degenerated proof A3: 0.F_Complex = the Zero of F_Complex by RLVECT_1:def 2 .= 0c by Def1; 1_ F_Complex = the unity of F_Complex by VECTSP_1:def 9 .= 1r by Def1; hence 0.F_Complex <> 1_ F_Complex by A3,COMPLEX1:12,15; end; end; end; theorem Th3: for x1,y1 be Element of F_Complex for x2,y2 be Element of COMPLEX st x1 = x2 & y1 = y2 holds x1 + y1 = x2 + y2 proof let x1,y1 be Element of F_Complex; let x2,y2 be Element of COMPLEX; assume x1 = x2 & y1 = y2; hence x1 + y1 = (the add of F_Complex).[x2,y2] by RLVECT_1:def 3 .= (the add of F_Complex).(x2,y2) by BINOP_1:def 1 .= addcomplex.(x2,y2) by Def1 .= x2 + y2 by COMPLSP1:def 1; end; theorem Th4: for x1 be Element of F_Complex for x2 be Element of COMPLEX st x1 = x2 holds - x1 = - x2 proof let x1 be Element of F_Complex; let x2 be Element of COMPLEX; assume A1: x1 = x2; reconsider x3 = x1 as Element of COMPLEX by Def1; -x2 is Element of F_Complex by Def1; then reconsider x'=-x2 as Element of F_Complex; x1 + x' = x3 + -x2 by Th3 .= 0c by A1,XCMPLX_0:def 6 .= the Zero of F_Complex by Def1 .= 0.F_Complex by RLVECT_1:def 2; hence thesis by RLVECT_1:def 10; end; theorem Th5: for x1,y1 be Element of F_Complex for x2,y2 be Element of COMPLEX st x1 = x2 & y1 = y2 holds x1 - y1 = x2 - y2 proof let x1,y1 be Element of F_Complex; let x2,y2 be Element of COMPLEX; assume A1: x1 = x2 & y1 = y2; then A2: - y1 = -y2 by Th4; thus x1 - y1 = x1 + (-y1) by RLVECT_1:def 11 .= x2 + (-y2) by A1,A2,Th3 .= x2 - y2 by XCMPLX_0:def 8; end; theorem Th6: for x1,y1 be Element of F_Complex for x2,y2 be Element of COMPLEX st x1 = x2 & y1 = y2 holds x1 * y1 = x2 * y2 proof let x1,y1 be Element of F_Complex; let x2,y2 be Element of COMPLEX; assume x1 = x2 & y1 = y2; hence x1 * y1 = (the mult of F_Complex).(x2,y2) by VECTSP_1:def 10 .= multcomplex.(x2,y2) by Def1 .= x2 * y2 by COMPLSP1:def 4; end; theorem Th7: for x1 be Element of F_Complex for x2 be Element of COMPLEX st x1 = x2 & x1 <> 0.F_Complex holds x1" = x2" proof let x1 be Element of F_Complex; let x2 be Element of COMPLEX; assume A1: x1 = x2 & x1 <> 0.F_Complex; A2: 0c = the Zero of F_Complex by Def1 .= 0.F_Complex by RLVECT_1:def 2; reconsider x3 = x1 as Element of COMPLEX by Def1; x2" is Element of F_Complex by Def1; then reconsider x'= x2" as Element of F_Complex; x1 * x' = x3 * x2" by Th6 .= 1r by A1,A2,COMPLEX1:65 .= the unity of F_Complex by Def1 .= 1_ F_Complex by VECTSP_1:def 9; hence x1" = x2" by A1,VECTSP_1:def 22; end; theorem Th8: for x1,y1 be Element of F_Complex for x2,y2 be Element of COMPLEX st x1 = x2 & y1 = y2 & y1 <> 0.F_Complex holds x1/y1 = x2/y2 proof let x1,y1 be Element of F_Complex; let x2,y2 be Element of COMPLEX; assume A1: x1 = x2 & y1 = y2; assume y1 <> 0.F_Complex; then A2: y1" = y2" by A1,Th7; thus x1/y1 = x1 * y1" by VECTSP_1:def 23 .= x2 * y2" by A1,A2,Th6 .= x2/y2 by XCMPLX_0:def 9; end; theorem Th9: 0.F_Complex = 0c proof thus 0c = the Zero of F_Complex by Def1 .= 0.F_Complex by RLVECT_1:def 2; end; theorem Th10: 1_ F_Complex = 1r proof thus 1r = the unity of F_Complex by Def1 .= 1_ F_Complex by VECTSP_1:def 9; end; theorem 1_ F_Complex + 1_ F_Complex <> 0.F_Complex proof L1: 1r = [*1,0*] by ARYTM_0:def 7,COMPLEX1:def 7; 1_ F_Complex = the unity of F_Complex by VECTSP_1:def 9 .= [*1,0*] by Def1,L1; then A1: 1_ F_Complex + 1_ F_Complex = (the add of F_Complex).[[*1,0*],[*1,0*]] by RLVECT_1:def 3 .= (the add of F_Complex).([*1,0*],[*1,0*]) by BINOP_1:def 1 .= addcomplex.([*1,0*],[*1,0*]) by Def1 .= [*1,0*] + [*1,0*] by COMPLSP1:def 1 .= [*1+1,0+0*] by Th2; L0: 0c = [*0,0*] by ARYTM_0:def 7; 0.F_Complex = the Zero of F_Complex by RLVECT_1:def 2 .= [*0,0*] by Def1,L0; hence thesis by A1,ARYTM_0:12; end; definition let z be Element of F_Complex; func z*' -> Element of F_Complex means :Def2: ex z' be Element of COMPLEX st z = z' & it = z'*'; existence proof reconsider z'=z as Element of COMPLEX by Def1; z'*' is Element of F_Complex by Def1; then reconsider z1=z'*' as Element of F_Complex; take z1; take z'; thus z = z' & z1 = z'*'; end; uniqueness; end; definition let z be Element of F_Complex; func |.z.| -> real number means :Def3: ex z' be Element of COMPLEX st z = z' & it = |.z'.|; existence proof reconsider z'=z as Element of COMPLEX by Def1; take z1=|.z'.|; take z'; thus z = z' & z1 = |.z'.|; end; uniqueness; end; definition let z be Element of F_Complex; redefine func |.z.| -> Element of REAL; coherence by XREAL_0:def 1; end; theorem Th12: for x1 be Element of F_Complex for x2 be Element of COMPLEX st x1 = x2 holds x1*' = x2*' proof let x1 be Element of F_Complex; let x2 be Element of COMPLEX; assume A1: x1 = x2; consider x3 be Element of COMPLEX such that A2: x1 = x3 & x1*' = x3*' by Def2; thus x1*' = x2*' by A1,A2; end; reserve z,z1,z2,z3,z4 for Element of F_Complex; canceled 16; theorem -z = (-1_ F_Complex) * z proof reconsider z'=z as Element of COMPLEX by Def1; A1: -1r = -1_ F_Complex by Th4,Th10; thus -z = -z' by Th4 .= (-1r) * z' by COMPLEX1:46 .= (-1_ F_Complex) * z by A1,Th6; end; canceled 5; theorem z1 - -z2 = z1 + z2 proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; -z2 = -z2' by Th4; hence z1 - -z2 = z1'- -z2' by Th5 .= z1' + z2' by XCMPLX_1:151 .= z1 + z2 by Th3; end; canceled 5; theorem z1 = z1 + z - z proof reconsider z1'=z1,z'=z as Element of COMPLEX by Def1; z1 + z = z1' + z' by Th3; hence z1 + z - z = z1' + z' - z' by Th5 .= z1 by XCMPLX_1:26; end; theorem z1 = z1 - z + z proof reconsider z1'=z1,z'=z as Element of COMPLEX by Def1; z1 - z = z1' - z' by Th5; hence z1 - z + z = z1' - z' + z' by Th3 .= z1 by XCMPLX_1:27; end; canceled 4; theorem z1 <> 0.F_Complex & z2 <> 0.F_Complex & z1" = z2" implies z1 = z2 proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; assume A1: z1 <> 0.F_Complex; assume A2: z2 <> 0.F_Complex; assume z1" = z2"; then z1'" = z2" by A1,Th7 .= z2'" by A2,Th7; hence z1 = z2 by XCMPLX_1:202; end; theorem z2 <> 0.F_Complex & (z1 * z2 = the unity of F_Complex or z2 * z1 = the unity of F_Complex) implies z1 = z2" proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; assume A1: z2 <> 0.F_Complex; assume A2: z1 * z2 = the unity of F_Complex or z2 * z1 = the unity of F_Complex; per cases by A2; suppose z1 * z2 = the unity of F_Complex; then z1' * z2' = the unity of F_Complex by Th6; then A3: z1' * z2' = 1r by Def1; z2" = z2'" by A1,Th7; hence z1 = z2" by A1,A3,Th9,COMPLEX1:69; suppose z2 * z1 = the unity of F_Complex; then z2' * z1' = the unity of F_Complex by Th6; then A4: z2' * z1' = 1r by Def1; z2" = z2'" by A1,Th7; hence z1 = z2" by A1,A4,Th9,COMPLEX1:69; end; theorem z2 <> 0.F_Complex & (z1 * z2 = z3 or z2 * z1 = z3) implies z1 = z3 * z2" & z1 = z2" * z3 proof reconsider z1'=z1,z2'=z2,z3'=z3 as Element of COMPLEX by Def1; assume A1: z2 <> 0.F_Complex; assume A2: (z1 * z2 = z3 or z2 * z1 = z3); A3: z2" = z2'" by A1,Th7; per cases by A2; suppose z1 * z2 = z3; then z1' * z2' = z3' by Th6; then z1' = z3' * z2'" by A1,Th9,XCMPLX_1:204; hence z1 = z3 * z2" & z1 = z2" * z3 by A3,Th6; suppose z2 * z1 = z3; then z2' * z1' = z3' by Th6; then z1' = z3' * z2'" by A1,Th9,XCMPLX_1:204; hence z1 = z3 * z2" & z1 = z2" * z3 by A3,Th6; end; theorem (the unity of F_Complex)" = the unity of F_Complex proof the unity of F_Complex <> 0c by Def1,COMPLEX1:12,15; then the unity of F_Complex <> the Zero of F_Complex by Def1; then A1: the unity of F_Complex <> 0.F_Complex by RLVECT_1:def 2; the unity of F_Complex = 1r by Def1; hence thesis by A1,Th7,COMPLEX1:71; end; theorem z1 <> 0.F_Complex & z2 <> 0.F_Complex implies (z1 * z2)" = z1" * z2" proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; assume A1: z1 <> 0.F_Complex; assume A2: z2 <> 0.F_Complex; A3: z1" = z1'" by A1,Th7; A4: z2" = z2'" by A2,Th7; A5: z1 * z2 <> 0.F_Complex by A1,A2,VECTSP_1:44; z1 * z2 = z1' * z2' by Th6; hence (z1 * z2)" = (z1' * z2')" by A5,Th7 .= z1'" * z2'" by XCMPLX_1:205 .= z1" * z2" by A3,A4,Th6; end; canceled; theorem z <> 0.F_Complex implies (-z)" = -(z") proof reconsider z1=z as Element of COMPLEX by Def1; assume A1: z <> 0.F_Complex; then A2: z1" = z" by Th7; A3: -z <> 0.F_Complex by A1,VECTSP_1:86; -z = -z1 by Th4; hence (-z)" = (-z1)" by A3,Th7 .= -(z1") by XCMPLX_1:224 .= -(z") by A2,Th4; end; canceled; theorem z1 <> 0.F_Complex & z2 <> 0.F_Complex implies z1" + z2" = (z1 + z2) * (z1 * z2)" proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; assume A1: z1 <> 0.F_Complex; then A2: z1" = z1'" by Th7; assume A3: z2 <> 0.F_Complex; then A4: z2" = z2'" by Th7; A5: z1 + z2 = z1' + z2' by Th3; A6: z1 * z2 <> 0.F_Complex by A1,A3,VECTSP_1:44; z1 * z2 = z1' * z2' by Th6; then A7: (z1 * z2)" = (z1' * z2')" by A6,Th7; thus z1" + z2" = z1'" + z2'" by A2,A4,Th3 .= (z1' + z2') * (z1' * z2')" by A1,A3,Th9,XCMPLX_1:213 .= (z1 + z2) * (z1 * z2)" by A5,A7,Th6; end; theorem z1 <> 0.F_Complex & z2 <> 0.F_Complex implies z1" - z2" = (z2 - z1) * (z1 * z2)" proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; assume A1: z1 <> 0.F_Complex; then A2: z1" = z1'" by Th7; assume A3: z2 <> 0.F_Complex; then A4: z2" = z2'" by Th7; A5: z2 - z1 = z2' - z1' by Th5; A6: z1 * z2 <> 0.F_Complex by A1,A3,VECTSP_1:44; z1 * z2 = z1' * z2' by Th6; then A7: (z1 * z2)" = (z1' * z2')" by A6,Th7; thus z1" - z2" = z1'" - z2'" by A2,A4,Th5 .= (z2' - z1') * (z1' * z2')" by A1,A3,Th9,XCMPLX_1:214 .= (z2 - z1) * (z1 * z2)" by A5,A7,Th6; end; canceled; theorem z <> 0.F_Complex implies z" = (the unity of F_Complex) / z proof reconsider z1=z as Element of COMPLEX by Def1; assume A1: z <> 0.F_Complex; A2: the unity of F_Complex = 1r by Def1; thus z" = z1" by A1,Th7 .= 1r / z1 by A1,Th9,COMPLEX1:84 .= (the unity of F_Complex) / z by A1,A2,Th8; end; theorem z / (the unity of F_Complex) = z proof reconsider z1=z as Element of COMPLEX by Def1; the unity of F_Complex = 1r by Def1; hence z / (the unity of F_Complex) = z1 / 1r by Th8,Th9,COMPLEX1:12,15 .= z by COMPLEX1:85; end; theorem z <> 0.F_Complex implies z / z = the unity of F_Complex proof reconsider z1=z as Element of COMPLEX by Def1; assume A1: z <> 0.F_Complex; hence z / z = z1 / z1 by Th8 .= 1r by A1,Th9,COMPLEX1:86 .= the unity of F_Complex by Def1; end; theorem z <> 0.F_Complex implies (0.F_Complex) / z = 0.F_Complex proof reconsider z1=z as Element of COMPLEX by Def1; assume z <> 0.F_Complex; hence (0.F_Complex) / z = 0c / z1 by Th8,Th9 .= 0.F_Complex by Th9,COMPLEX1:87; end; theorem Th62: z2 <> 0.F_Complex & z1 / z2 = 0.F_Complex implies z1 = 0.F_Complex proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; assume A1: z2 <> 0.F_Complex; assume z1 / z2 = 0.F_Complex; then z1' / z2' = 0.F_Complex by A1,Th8; hence z1 = 0.F_Complex by A1,Th9,XCMPLX_1:50; end; theorem z2 <> 0.F_Complex & z4 <> 0.F_Complex implies (z1 / z2) * (z3 / z4) = (z1 * z3) / (z2 * z4) proof reconsider z1'=z1,z2'=z2,z3'=z3,z4'=z4 as Element of COMPLEX by Def1; assume A1: z2 <> 0.F_Complex; assume A2: z4 <> 0.F_Complex; A3: z1' * z3' = z1 * z3 by Th6; A4: z2' * z4' = z2 * z4 by Th6; A5: z2 * z4 <> 0.F_Complex by A1,A2,VECTSP_1:44; A6: z1' / z2' = z1 / z2 by A1,Th8; z3' / z4' = z3 / z4 by A2,Th8; hence (z1 / z2) * (z3 / z4) = (z1' / z2') * (z3' / z4') by A6,Th6 .= (z1' * z3') / (z2' * z4') by XCMPLX_1:77 .= (z1 * z3) / (z2 * z4) by A3,A4,A5,Th8; end; theorem z2 <> 0.F_Complex implies z * (z1 / z2) = (z * z1) / z2 proof reconsider z1'=z1,z2'=z2,z'=z as Element of COMPLEX by Def1; assume A1: z2 <> 0.F_Complex; A2: z' * z1' = z * z1 by Th6; z1' / z2' = z1 / z2 by A1,Th8; hence z * (z1 / z2) = z' * (z1' / z2') by Th6 .= (z' * z1') / z2' by XCMPLX_1:75 .= (z * z1) / z2 by A1,A2,Th8; end; theorem z2 <> 0.F_Complex & z1 / z2 = the unity of F_Complex implies z1 = z2 proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; assume A1: z2 <> 0.F_Complex; assume z1 / z2 = the unity of F_Complex; then z1' / z2' = the unity of F_Complex by A1,Th8; then z1' / z2' = 1r by Def1; hence z1 = z2 by A1,Th9,COMPLEX1:91; end; theorem z <> 0.F_Complex implies z1 = (z1 * z) / z proof reconsider z1'=z1,z'=z as Element of COMPLEX by Def1; assume A1: z <> 0.F_Complex; A2: z1' * z' = z1 * z by Th6; thus z1 = (z1' * z') / z' by A1,Th9,XCMPLX_1:90 .= (z1 * z) / z by A1,A2,Th8; end; theorem z1 <> 0.F_Complex & z2 <> 0.F_Complex implies (z1 / z2)" = z2 / z1 proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; assume A1: z1 <> 0.F_Complex; assume A2: z2 <> 0.F_Complex; then A3: z1 / z2 <> 0.F_Complex by A1,Th62; z1' / z2' = z1 / z2 by A2,Th8; hence (z1 / z2)" = (z1' / z2')" by A3,Th7 .= z2' / z1' by XCMPLX_1:215 .= z2 / z1 by A1,Th8; end; theorem z1 <> 0.F_Complex & z2 <> 0.F_Complex implies (z1" / z2") = z2 / z1 proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; assume A1: z1 <> 0.F_Complex; assume A2: z2 <> 0.F_Complex; A3: z1" = z1'" by A1,Th7; A4: z2" = z2'" by A2,Th7; z2" <> 0.F_Complex by A2,VECTSP_1:74; hence (z1" / z2") = (z1'" / z2'") by A3,A4,Th8 .= z2' / z1' by XCMPLX_1:216 .= z2 / z1 by A1,Th8; end; theorem z2 <> 0.F_Complex implies z1 / z2" = z1 * z2 proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; assume A1: z2 <> 0.F_Complex; then A2: z2" <> 0.F_Complex by VECTSP_1:74; z2" = z2'" by A1,Th7; hence z1 / z2" = z1' / z2'" by A2,Th8 .= z1' * z2' by XCMPLX_1:221 .= z1 * z2 by Th6; end; theorem z1 <> 0.F_Complex & z2 <> 0.F_Complex implies z1" / z2 = (z1 * z2)" proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; assume A1: z1 <> 0.F_Complex; assume A2: z2 <> 0.F_Complex; then A3: z1 * z2 <> 0.F_Complex by A1,VECTSP_1:44; A4: z1 * z2 = z1' * z2' by Th6; z1" = z1'" by A1,Th7; hence z1" / z2 = z1'" / z2' by A2,Th8 .= (z1' * z2')" by XCMPLX_1:223 .= (z1 * z2)" by A3,A4,Th7; end; theorem z1 <> 0.F_Complex & z2 <> 0.F_Complex implies z1"* (z / z2) = z / (z1 * z2) proof reconsider z1'=z1,z2'=z2,z'=z as Element of COMPLEX by Def1; assume A1: z1 <> 0.F_Complex; assume A2: z2 <> 0.F_Complex; then A3: z1 * z2 <> 0.F_Complex by A1,VECTSP_1:44; A4: z1" = z1'" by A1,Th7; A5: z1 * z2 = z1' * z2' by Th6; z' / z2' = z / z2 by A2,Th8; hence z1"* (z / z2) = z1'"* (z' / z2') by A4,Th6 .= z' / (z1' * z2') by XCMPLX_1:222 .= z / (z1 * z2) by A3,A5,Th8; end; theorem z <> 0.F_Complex & z2 <> 0.F_Complex implies (z1 / z2) = (z1 * z) / (z2 * z) & (z1 / z2) = (z * z1) / (z * z2) proof reconsider z1'=z1,z2'=z2,z'=z as Element of COMPLEX by Def1; assume A1: z <> 0.F_Complex; assume A2: z2 <> 0.F_Complex; A3: z1 * z = z1' * z' by Th6; A4: z2 * z = z2' * z' by Th6; A5: z2 * z <> 0.F_Complex by A1,A2,VECTSP_1:44; thus (z1 / z2) = (z1' / z2') by A2,Th8 .= (z1' * z') / (z2' * z') by A1,Th9,XCMPLX_1:92 .= (z1 * z) / (z2 * z) by A3,A4,A5,Th8; hence thesis; end; theorem z2 <> 0.F_Complex & z3 <> 0.F_Complex implies z1 / (z2 * z3) = z1 / z2 / z3 proof reconsider z1'=z1,z2'=z2,z3'=z3 as Element of COMPLEX by Def1; assume A1: z2 <> 0.F_Complex; assume A2: z3 <> 0.F_Complex; A3: z2 * z3 = z2' * z3' by Th6; A4: z2 * z3 <> 0.F_Complex by A1,A2,VECTSP_1:44; A5: z1 / z2 = z1' / z2' by A1,Th8; thus z1 / (z2 * z3) = z1' / (z2' * z3') by A3,A4,Th8 .= z1' / z2' / z3' by XCMPLX_1:79 .= z1 / z2 / z3 by A2,A5,Th8; end; theorem z2 <> 0.F_Complex & z3 <> 0.F_Complex implies (z1 * z3) / z2 = z1 / (z2 / z3) proof reconsider z1'=z1,z2'=z2,z3'=z3 as Element of COMPLEX by Def1; assume A1: z2 <> 0.F_Complex; assume A2: z3 <> 0.F_Complex; then A3: z2 / z3 = z2' / z3' by Th8; A4: z2 / z3 <> 0.F_Complex by A1,A2,Th62; z1 * z3 = z1' * z3' by Th6; hence (z1 * z3) / z2 = (z1' * z3') / z2' by A1,Th8 .= z1' / (z2' / z3') by XCMPLX_1:78 .= z1 / (z2 / z3) by A3,A4,Th8; end; theorem z2 <> 0.F_Complex & z3 <> 0.F_Complex & z4 <> 0.F_Complex implies (z1 / z2) / (z3 / z4) = (z1 * z4) / (z2 * z3) proof reconsider z1'=z1,z2'=z2,z3'=z3,z4'=z4 as Element of COMPLEX by Def1; assume A1: z2 <> 0.F_Complex; assume A2: z3 <> 0.F_Complex; assume A3: z4 <> 0.F_Complex; A4: z1 * z4 = z1' * z4' by Th6; A5: z2 * z3 = z2' * z3' by Th6; A6: z2 * z3 <> 0.F_Complex by A1,A2,VECTSP_1:44; A7: z1 / z2 = z1' / z2' by A1,Th8; A8: z3 / z4 = z3' / z4' by A3,Th8; z3 / z4 <> 0.F_Complex by A2,A3,Th62; hence (z1 / z2) / (z3 / z4) = (z1' / z2') / (z3' / z4') by A7,A8,Th8 .= (z1' * z4') / (z2' * z3') by XCMPLX_1:85 .= (z1 * z4) / (z2 * z3) by A4,A5,A6,Th8; end; theorem z2 <> 0.F_Complex & z4 <> 0.F_Complex implies z1 / z2 + z3 / z4 = (z1 * z4 + z3 * z2) / (z2 * z4) proof reconsider z1'=z1,z2'=z2,z3'=z3,z4'=z4 as Element of COMPLEX by Def1; assume A1: z2 <> 0.F_Complex; assume A2: z4 <> 0.F_Complex; A3: z2 * z4 = z2' * z4' by Th6; A4: z1 * z4 = z1' * z4' by Th6; z3 * z2 = z3' * z2' by Th6; then A5: z1 * z4 + z3 * z2 = z1' * z4' + z3' * z2' by A4,Th3; A6: z2 * z4 <> 0.F_Complex by A1,A2,VECTSP_1:44; A7: z1 / z2 = z1' / z2' by A1,Th8; z3 / z4 = z3' / z4' by A2,Th8; hence z1 / z2 + z3 / z4 = z1' / z2' + z3' / z4' by A7,Th3 .= (z1' * z4' + z3' * z2') / (z2' * z4') by A1,A2,Th9,XCMPLX_1: 117 .= (z1 * z4 + z3 * z2) / (z2 * z4) by A3,A5,A6,Th8; end; theorem z <> 0.F_Complex implies z1 / z + z2 / z = (z1 + z2) / z proof reconsider z1'=z1,z2'=z2,z'=z as Element of COMPLEX by Def1; assume A1: z <> 0.F_Complex; A2: z1 + z2 = z1' + z2' by Th3; A3: z1 / z = z1' / z' by A1,Th8; z2 / z = z2' / z' by A1,Th8; hence z1 / z + z2 / z = z1' / z' + z2' / z' by A3,Th3 .= (z1' + z2') / z' by XCMPLX_1:63 .= (z1 + z2) / z by A1,A2,Th8; end; theorem z2 <> 0.F_Complex implies -(z1 / z2) = (-z1) / z2 & -(z1 / z2) = z1 / (-z2) proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; A1: -z1 = -z1' by Th4; A2: -z2 = -z2' by Th4; assume A3: z2 <> 0.F_Complex; then A4: -z2 <> 0.F_Complex by VECTSP_1:86; z1 / z2 = z1' / z2' by A3,Th8; hence -(z1 / z2) = -(z1' / z2') by Th4 .= (-z1') / z2' by XCMPLX_1:188 .= (-z1) / z2 by A1,A3,Th8; z1 / z2 = z1' / z2' by A3,Th8; hence -(z1 / z2) = -(z1' / z2') by Th4 .= z1' / -(z2') by XCMPLX_1:189 .= z1 / -z2 by A2,A4,Th8; end; theorem z2 <> 0.F_Complex implies z1 / z2 = (-z1) / (-z2) proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; assume A1: z2 <> 0.F_Complex; then A2: -z2 <> 0.F_Complex by VECTSP_1:86; A3: -z1' = -z1 & -z2' = -z2 by Th4; thus z1 / z2 = z1' / z2' by A1,Th8 .= (-z1') / (-z2') by XCMPLX_1:192 .= (-z1) / (-z2) by A2,A3,Th8; end; theorem z2 <> 0.F_Complex & z4 <> 0.F_Complex implies z1 / z2 - z3 / z4 = (z1 * z4 - z3 * z2) / (z2 * z4) proof reconsider z1'=z1,z2'=z2,z3'=z3,z4'=z4 as Element of COMPLEX by Def1; assume A1: z2 <> 0.F_Complex; assume A2: z4 <> 0.F_Complex; then A3: z1' / z2' = z1 / z2 & z3' / z4' = z3 / z4 by A1,Th8; A4: z2' * z4' = z2 * z4 by Th6; A5: z2 * z4 <> 0.F_Complex by A1,A2,VECTSP_1:44; z1' * z4' = z1 * z4 & z3' * z2' = z3 * z2 by Th6; then A6: z1 * z4 - z3 * z2 = z1' * z4' - z3' * z2' by Th5; thus z1 / z2 - z3 / z4 = z1' / z2' - z3' / z4' by A3,Th5 .= (z1' * z4' - z3' * z2') / (z2' * z4') by A1,A2,Th9,XCMPLX_1:131 .= (z1 * z4 - z3 * z2) / (z2 * z4) by A4,A5,A6,Th8; end; theorem z <> 0.F_Complex implies z1 / z - z2 / z = (z1 - z2) / z proof reconsider z'=z,z1'=z1,z2'=z2 as Element of COMPLEX by Def1; assume A1: z <> 0.F_Complex; A2: z1' - z2' = z1 - z2 by Th5; z1' / z' = z1 / z & z2' / z' = z2 / z by A1,Th8; hence z1 / z - z2 / z = z1' / z' - z2' / z' by Th5 .= (z1' - z2') / z' by XCMPLX_1:121 .= (z1 - z2) / z by A1,A2,Th8; end; theorem z2 <> 0.F_Complex & (z1 * z2 = z3 or z2 * z1 = z3) implies z1 = z3 / z2 proof reconsider z3'=z3,z1'=z1,z2'=z2 as Element of COMPLEX by Def1; assume A1: z2 <> 0.F_Complex; assume A2: z1 * z2 = z3 or z2 * z1 = z3; per cases by A2; suppose z1 * z2 = z3; then z1' * z2' = z3' by Th6; hence z1 = z3' / z2' by A1,Th9,XCMPLX_1:90 .= z3 / z2 by A1,Th8; suppose z2 * z1 = z3; then z2' * z1' = z3' by Th6; hence z1 = z3' / z2' by A1,Th9,XCMPLX_1:90 .= z3 / z2 by A1,Th8; end; theorem (the Zero of F_Complex)*' = the Zero of F_Complex proof consider z be Element of COMPLEX such that A1: the Zero of F_Complex = z & (the Zero of F_Complex)*' = z*' by Def2; the Zero of F_Complex = 0c by Def1; hence thesis by A1,COMPLEX1:113; end; theorem Th84: z*' = the Zero of F_Complex implies z = the Zero of F_Complex proof assume A1: z*' = the Zero of F_Complex; consider z1 be Element of COMPLEX such that A2: z1 = z & z1*' = z*' by Def2; the Zero of F_Complex = 0c by Def1; hence thesis by A1,A2,COMPLEX1:114; end; theorem (the unity of F_Complex)*' = the unity of F_Complex proof consider z be Element of COMPLEX such that A1: the unity of F_Complex = z & (the unity of F_Complex)*' = z*' by Def2; the unity of F_Complex = 1r by Def1; hence thesis by A1,COMPLEX1:115; end; theorem z*'*' = z proof reconsider z'=z as Element of COMPLEX by Def1; z*' = z'*' by Th12; hence z*'*' = z'*'*' by Th12 .= z; end; theorem (z1 + z2)*' = z1*' + z2*' proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; A1: z1'*' = z1*' & z2'*' = z2*' by Th12; z1' + z2' = z1 + z2 by Th3; hence (z1 + z2)*' = (z1' + z2')*' by Th12 .= z1'*' + z2'*' by COMPLEX1:118 .= z1*' + z2*' by A1,Th3; end; theorem (-z)*' = -(z*') proof reconsider z'=z as Element of COMPLEX by Def1; A1: z'*' = z*' by Th12; -z = -z' by Th4; hence (-z)*' = (-z')*' by Th12 .= -(z'*') by COMPLEX1:119 .= -(z*') by A1,Th4; end; theorem (z1 - z2)*' = z1*' - z2*' proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; A1: z1'*' = z1*' & z2'*' = z2*' by Th12; z1' - z2' = z1 - z2 by Th5; hence (z1 - z2)*' = (z1' - z2')*' by Th12 .= z1'*' - z2'*' by COMPLEX1:120 .= z1*' - z2*' by A1,Th5; end; theorem (z1 * z2)*' = z1*' * z2*' proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; A1: z1'*' = z1*' & z2'*' = z2*' by Th12; z1' * z2' = z1 * z2 by Th6; hence (z1 * z2)*' = (z1' * z2')*' by Th12 .= z1'*' * z2'*' by COMPLEX1:121 .= z1*' * z2*' by A1,Th6; end; theorem z <> the Zero of F_Complex implies z"*' = z*'" proof reconsider z1=z as Element of COMPLEX by Def1; assume A1: z <> the Zero of F_Complex; then A2: z <> 0.F_Complex by RLVECT_1:def 2; z*' <> the Zero of F_Complex by A1,Th84; then A3: z*' <> 0.F_Complex by RLVECT_1:def 2; A4: z*' = z1*' by Th12; z" = z1" by A2,Th7; hence z"*' = z1"*' by Th12 .= z1*'" by COMPLEX1:122 .= z*'" by A3,A4,Th7; end; theorem z2 <> the Zero of F_Complex implies (z1 / z2)*' = (z1*') / (z2*') proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; assume A1: z2 <> the Zero of F_Complex; then A2: z2 <> 0.F_Complex by RLVECT_1:def 2; A3: z1*' = z1'*' & z2*' = z2'*' by Th12; z2*' <> the Zero of F_Complex by A1,Th84; then A4: z2*' <> 0.F_Complex by RLVECT_1:def 2; z1' / z2' = z1 / z2 by A2,Th8; hence (z1 / z2)*' = (z1' / z2')*' by Th12 .= (z1'*') / (z2'*') by COMPLEX1:123 .= (z1*') / (z2*') by A3,A4,Th8; end; theorem |.the Zero of F_Complex.| = 0 proof the Zero of F_Complex = 0c by Def1; hence thesis by Def3,COMPLEX1:130; end; theorem |.z.| = 0 implies z = 0.F_Complex proof reconsider z'=z as Element of COMPLEX by Def1; assume A1: |.z.| = 0; |.z'.| = |.z.| by Def3; hence z = 0.F_Complex by A1,Th9,COMPLEX1:131; end; theorem 0 <= |.z.| proof reconsider z1=z as Element of COMPLEX by Def1; |.z1.| = |.z.| by Def3; hence thesis by COMPLEX1:132; end; theorem z <> 0.F_Complex iff 0 < |.z.| proof reconsider z1=z as Element of COMPLEX by Def1; thus z <> 0.F_Complex implies 0 < |.z.| proof assume z <> 0.F_Complex; then 0 < |.z1.| by Th9,COMPLEX1:133; hence thesis by Def3; end; assume 0 < |.z.|; then 0 < |.z1.| by Def3; hence thesis by Th9,COMPLEX1:133; end; theorem |.the unity of F_Complex.| = 1 proof the unity of F_Complex = 1r by Def1; hence |.the unity of F_Complex.| = 1 by Def3,COMPLEX1:134; end; theorem |.-z.| = |.z.| proof reconsider z1=z as Element of COMPLEX by Def1; -z1 = -z by Th4; hence |.-z.| = |.-z1.| by Def3 .= |.z1.| by COMPLEX1:138 .= |.z.| by Def3; end; theorem |.z*'.| = |.z.| proof reconsider z1=z as Element of COMPLEX by Def1; z1*' = z*' by Th12; hence |.z*'.| = |.z1*'.| by Def3 .= |.z1.| by COMPLEX1:139 .= |.z.| by Def3; end; theorem |.z1 + z2.| <= |.z1.| + |.z2.| proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; z1' + z2' = z1 + z2 by Th3; then A1: |.z1' + z2'.| = |.z1 + z2.| by Def3; |.z1'.| = |.z1.| & |.z2'.| = |.z2.| by Def3; hence thesis by A1,COMPLEX1:142; end; theorem |.z1 - z2.| <= |.z1.| + |.z2.| proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; z1' - z2' = z1 - z2 by Th5; then A1: |.z1' - z2'.| = |.z1 - z2.| by Def3; |.z1'.| = |.z1.| & |.z2'.| = |.z2.| by Def3; hence thesis by A1,COMPLEX1:143; end; theorem |.z1.| - |.z2.| <= |.z1 + z2.| proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; z1' + z2' = z1 + z2 by Th3; then A1: |.z1' + z2'.| = |.z1 + z2.| by Def3; |.z1'.| = |.z1.| & |.z2'.| = |.z2.| by Def3; hence thesis by A1,COMPLEX1:144; end; theorem |.z1.| - |.z2.| <= |.z1 - z2.| proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; z1' - z2' = z1 - z2 by Th5; then A1: |.z1' - z2'.| = |.z1 - z2.| by Def3; |.z1'.| = |.z1.| & |.z2'.| = |.z2.| by Def3; hence thesis by A1,COMPLEX1:145; end; theorem |.z1 - z2.| = |.z2 - z1.| proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; A1: z2' - z1' = z2 - z1 by Th5; z1' - z2' = z1 - z2 by Th5; hence |.z1 - z2.| = |.z1' - z2'.| by Def3 .= |.z2' - z1'.| by COMPLEX1:146 .= |.z2 - z1.| by A1,Def3; end; theorem |.z1 - z2.| = 0 iff z1 = z2 proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; thus |.z1 - z2.| = 0 implies z1 = z2 proof assume A1: |.z1 - z2.| = 0; z1 - z2 = z1' - z2' by Th5; then |.z1' - z2'.| = 0 by A1,Def3; hence z1 = z2 by COMPLEX1:147; end; z1' - z2' = z1 - z2 by Th5; then A2: |.z1' - z2'.| = |.z1 - z2.| by Def3; assume z1 = z2; hence thesis by A2,COMPLEX1:147; end; theorem z1 <> z2 iff 0 < |.z1 - z2.| proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; thus z1 <> z2 implies 0 < |.z1 - z2.| proof assume A1: z1 <> z2; z1 - z2 = z1' - z2' by Th5; then |.z1 - z2.| = |.z1' - z2'.| by Def3; hence 0 < |.z1 - z2.| by A1,COMPLEX1:148; end; assume A2: 0 < |.z1 - z2.|; z1 - z2 = z1' - z2' by Th5; then |.z1 - z2.| = |.z1' - z2'.| by Def3; hence z1 <> z2 by A2,COMPLEX1:148; end; theorem |.z1 - z2.| <= |.z1 - z.| + |.z - z2.| proof reconsider z'=z,z1'=z1,z2'=z2 as Element of COMPLEX by Def1; z1' - z2' = z1 - z2 by Th5; then A1: |.z1' - z2'.| = |.z1 - z2.| by Def3; z1' - z' = z1 - z by Th5; then A2: |.z1' - z'.| = |.z1 - z.| by Def3; z' - z2' = z - z2 by Th5; then |.z' - z2'.| = |.z - z2.| by Def3; hence thesis by A1,A2,COMPLEX1:149; end; theorem abs(|.z1.| - |.z2.|) <= |.z1 - z2.| proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; A1: |.z1'.| = |.z1.| & |.z2'.| = |.z2.| by Def3; z1' - z2' = z1 - z2 by Th5; then |.z1' - z2'.| = |.z1 - z2.| by Def3; hence thesis by A1,COMPLEX1:150; end; theorem |.z1*z2.| = |.z1.|*|.z2.| proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; A1: |.z1'.| = |.z1.| & |.z2'.| = |.z2.| by Def3; z1' * z2' = z1 * z2 by Th6; hence |.z1 * z2.| = |.z1' * z2'.| by Def3 .= |.z1.| * |.z2.| by A1,COMPLEX1:151; end; theorem z <> the Zero of F_Complex implies |.z".| = |.z.|" proof reconsider z1=z as Element of COMPLEX by Def1; assume A1: z <> the Zero of F_Complex; then A2: z <> 0c by Def1; z <> 0.F_Complex by A1,Def1,Th9; then z" = z1" by Th7; hence |.z".| = |.z1".| by Def3 .= |.z1.|" by A2,COMPLEX1:152 .= |.z.|" by Def3; end; theorem z2 <> the Zero of F_Complex implies |.z1.| / |.z2.| = |.z1 / z2.| proof reconsider z1'=z1,z2'=z2 as Element of COMPLEX by Def1; assume A1: z2 <> the Zero of F_Complex; then A2: z2 <> 0c by Def1; z2 <> 0.F_Complex by A1,Def1,Th9; then A3: z1' / z2' = z1 / z2 by Th8; |.z1'.| = |.z1.| & |.z2'.| = |.z2.| by Def3; hence |.z1.| / |.z2.| = |.z1' / z2'.| by A2,COMPLEX1:153 .= |.z1 / z2.| by A3,Def3; end; theorem |.z * z.| = |.z * z*'.| proof reconsider z1=z as Element of COMPLEX by Def1; z1*' = z*' by Th12; then A1: z1 * z1*' = z * z*' by Th6; z1 * z1 = z * z by Th6; hence |.z * z.| = |.z1 * z1.| by Def3 .= |.z1 * z1*'.| by COMPLEX1:155 .= |.z * z*'.| by A1,Def3; end;

Back to top