Copyright (c) 2000 Association of Mizar Users
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;