:: COMPLFLD semantic presentation

begin

definition
func F_Complex  ->  strict doubleLoopStr  means :Def1: :: COMPLFLD:def 1
( the carrier of it = COMPLEX & the addF of it = addcomplex & the multF of it = multcomplex & 1. it = 1r & 0. it = 0c );
existence
 ex b1 being strict doubleLoopStr st
( the carrier of b1 = COMPLEX & the addF of b1 = addcomplex & the multF of b1 = multcomplex & 1. b1 = 1r & 0. b1 = 0c )
proof
take  doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) ; ::_thesis: ( the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = COMPLEX & the addF of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = addcomplex & the multF of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = multcomplex & 1. doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = 1r & 0. doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = 0c )
thus  ( the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = COMPLEX & the addF of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = addcomplex & the multF of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = multcomplex & 1. doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = 1r & 0. doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = 0c ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict doubleLoopStr st the carrier of b1 = COMPLEX & the addF of b1 = addcomplex & the multF of b1 = multcomplex & 1. b1 = 1r & 0. b1 = 0c & the carrier of b2 = COMPLEX & the addF of b2 = addcomplex & the multF of b2 = multcomplex & 1. b2 = 1r & 0. b2 = 0c holds
b1 = b2 ;
end;

:: deftheorem Def1 defines F_Complex COMPLFLD:def_1_:_
 for b1 being strict doubleLoopStr holds
( b1 = F_Complex iff ( the carrier of b1 = COMPLEX & the addF of b1 = addcomplex & the multF of b1 = multcomplex & 1. b1 = 1r & 0. b1 = 0c ) );

registration
cluster F_Complex  ->  non empty strict ;
coherence
 not F_Complex is empty by Def1;
end;

registration
cluster  ->  complex for Element of the carrier of F_Complex;
coherence
 for b1 being Element of F_Complex holds b1 is complex
proof
let c be Element of F_Complex; ::_thesis: c is complex
 c in the carrier of F_Complex ;
then  c in COMPLEX by Def1;
hence  c is complex ; ::_thesis: verum
end;
end;

registration
let a, b be complex number ;
let x, y be Element of F_Complex;
identifyx + y with a + b when x = a, y = b;
compatibility
 ( x = a & y = b implies x + y = a + b )
proof
reconsider a9 = a, b9 = b as Element of COMPLEX by XCMPLX_0:def_2;
assume  ( x = a & y = b ) ; ::_thesis: x + y = a + b
hence x + y = addcomplex . (a9,b9) by Def1
.= a + b by BINOP_2:def_3 ;
::_thesis: verum
end;
identifyx * y with a * b when x = a, y = b;
compatibility
 ( x = a & y = b implies x * y = a * b )
proof
reconsider a9 = a, b9 = b as Element of COMPLEX by XCMPLX_0:def_2;
assume  ( x = a & y = b ) ; ::_thesis: x * y = a * b
hence x * y = multcomplex . (a9,b9) by Def1
.= a * b by BINOP_2:def_5 ;
::_thesis: verum
end;
end;

registration
cluster F_Complex  ->  strict well-unital ;
coherence
 F_Complex is well-unital
proof
let x be Element of F_Complex; :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. F_Complex) = x & (1. F_Complex) * x = x )
 1. F_Complex = 1r by Def1;
hence  ( x * (1. F_Complex) = x & (1. F_Complex) * x = x ) ; ::_thesis: verum
end;
end;

Lm1:  1_ F_Complex = 1r
by Def1;

Lm2:  1. F_Complex = 1r
by Def1;

registration
cluster F_Complex  ->  non degenerated right_complementable almost_left_invertible strict associative commutative right_unital distributive left_unital Abelian add-associative right_zeroed ;
coherence
 ( F_Complex is add-associative & F_Complex is right_zeroed & F_Complex is right_complementable & F_Complex is Abelian & F_Complex is commutative & F_Complex is associative & F_Complex is left_unital & F_Complex is right_unital & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )
proof
thus  F_Complex is add-associative ::_thesis: ( F_Complex is right_zeroed & F_Complex is right_complementable & F_Complex is Abelian & F_Complex is commutative & F_Complex is associative & F_Complex is left_unital & F_Complex is right_unital & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )
proof
let x, y, z be Element of F_Complex; :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as Element of COMPLEX by Def1;
thus (x + y) + z = addcomplex . [( the addF of F_Complex . [x1,y1]),z1] by Def1
.= addcomplex . ((addcomplex . (x1,y1)),z1) by Def1
.= addcomplex . ((x1 + y1),z1) by BINOP_2:def_3
.= (x1 + y1) + z1 by BINOP_2:def_3
.= x1 + (y1 + z1)
.= addcomplex . (x1,(y1 + z1)) by BINOP_2:def_3
.= addcomplex . [x1,(addcomplex . (y1,z1))] by BINOP_2:def_3
.= addcomplex . [x1,( the addF of F_Complex . [y1,z1])] by Def1
.= x + (y + z) by Def1 ; ::_thesis: verum
end;
thus  F_Complex is right_zeroed ::_thesis: ( F_Complex is right_complementable & F_Complex is Abelian & F_Complex is commutative & F_Complex is associative & F_Complex is left_unital & F_Complex is right_unital & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )
proof
let x be Element of F_Complex; :: according to RLVECT_1:def_4 ::_thesis: x + (0. F_Complex) = x
reconsider x1 = x as Element of COMPLEX by Def1;
thus x + (0. F_Complex) = the addF of F_Complex . (x1,0c) by Def1
.= addcomplex . (x1,0c) by Def1
.= x1 + 0c by BINOP_2:def_3
.= x ; ::_thesis: verum
end;
thus  F_Complex is right_complementable ::_thesis: ( F_Complex is Abelian & F_Complex is commutative & F_Complex is associative & F_Complex is left_unital & F_Complex is right_unital & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )
proof
let x be Element of F_Complex; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x1 = x as Element of COMPLEX by Def1;
reconsider y = - x1 as Element of F_Complex by Def1;
take  y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. F_Complex
thus  x + y = 0. F_Complex by Def1; ::_thesis: verum
end;
thus  F_Complex is Abelian ::_thesis: ( F_Complex is commutative & F_Complex is associative & F_Complex is left_unital & F_Complex is right_unital & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )
proof
let x, y be Element of F_Complex; :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
thus  x + y = y + x ; ::_thesis: verum
end;
thus  F_Complex is commutative ::_thesis: ( F_Complex is associative & F_Complex is left_unital & F_Complex is right_unital & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )
proof
let x, y be Element of F_Complex; :: according to GROUP_1:def_12 ::_thesis: x * y = y * x
thus  x * y = y * x ; ::_thesis: verum
end;
thus  F_Complex is associative ::_thesis: ( F_Complex is left_unital & F_Complex is right_unital & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )
proof
let x, y, z be Element of F_Complex; :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
reconsider x1 = x, y1 = y, z1 = z as Element of COMPLEX by Def1;
thus (x * y) * z = multcomplex . (( the multF of F_Complex . (x1,y1)),z1) by Def1
.= multcomplex . ((multcomplex . (x1,y1)),z1) by Def1
.= multcomplex . ((x1 * y1),z1) by BINOP_2:def_5
.= (x1 * y1) * z1 by BINOP_2:def_5
.= x1 * (y1 * z1)
.= multcomplex . (x1,(y1 * z1)) by BINOP_2:def_5
.= multcomplex . (x1,(multcomplex . (y1,z1))) by BINOP_2:def_5
.= multcomplex . (x1,( the multF of F_Complex . (y1,z1))) by Def1
.= x * (y * z) by Def1 ; ::_thesis: verum
end;
thus  F_Complex is left_unital ; ::_thesis: ( F_Complex is right_unital & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )
thus  F_Complex is right_unital ; ::_thesis: ( F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )
thus  F_Complex is distributive ::_thesis: ( F_Complex is almost_left_invertible & not F_Complex is degenerated )
proof
let x, y, z be Element of F_Complex; :: according to VECTSP_1:def_7 ::_thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
reconsider x1 = x, y1 = y, z1 = z as Element of COMPLEX by Def1;
thus x * (y + z) = multcomplex . (x1,( the addF of F_Complex . (y1,z1))) by Def1
.= multcomplex . (x1,(addcomplex . (y1,z1))) by Def1
.= multcomplex . (x1,(y1 + z1)) by BINOP_2:def_3
.= x1 * (y1 + z1) by BINOP_2:def_5
.= (x1 * y1) + (x1 * z1)
.= addcomplex . ((x1 * y1),(x1 * z1)) by BINOP_2:def_3
.= addcomplex . ((multcomplex . (x1,y1)),(x1 * z1)) by BINOP_2:def_5
.= addcomplex . ((multcomplex . (x1,y1)),(multcomplex . (x1,z1))) by BINOP_2:def_5
.= the addF of F_Complex . ((multcomplex . (x1,y1)),(multcomplex . (x1,z1))) by Def1
.= the addF of F_Complex . (( the multF of F_Complex . (x1,y1)),(multcomplex . (x1,z1))) by Def1
.= (x * y) + (x * z) by Def1 ; ::_thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = multcomplex . (( the addF of F_Complex . (y1,z1)),x1) by Def1
.= multcomplex . ((addcomplex . (y1,z1)),x1) by Def1
.= multcomplex . ((y1 + z1),x1) by BINOP_2:def_3
.= (y1 + z1) * x1 by BINOP_2:def_5
.= (y1 * x1) + (z1 * x1)
.= addcomplex . ((y1 * x1),(z1 * x1)) by BINOP_2:def_3
.= addcomplex . ((multcomplex . (y1,x1)),(z1 * x1)) by BINOP_2:def_5
.= addcomplex . ((multcomplex . (y1,x1)),(multcomplex . (z1,x1))) by BINOP_2:def_5
.= the addF of F_Complex . ((multcomplex . (y1,x1)),(multcomplex . (z1,x1))) by Def1
.= the addF of F_Complex . (( the multF of F_Complex . (y1,x1)),(multcomplex . (z1,x1))) by Def1
.= (y * x) + (z * x) by Def1 ; ::_thesis: verum
end;
thus  F_Complex is almost_left_invertible ::_thesis: not F_Complex is degenerated
proof
let x be Element of F_Complex; :: according to ALGSTR_0:def_39 ::_thesis: ( x = 0. F_Complex or x is left_invertible )
reconsider x1 = x as Element of COMPLEX by Def1;
assume A1: x <> 0. F_Complex ; ::_thesis: x is left_invertible
reconsider y = x1 " as Element of F_Complex by Def1;
take  y ; :: according to ALGSTR_0:def_27 ::_thesis: y * x = 1. F_Complex
 x1 <> 0c by A1, Def1;
hence  y * x = 1. F_Complex by Lm2, XCMPLX_0:def_7; ::_thesis: verum
end;
 0. F_Complex <> 1. F_Complex by Def1, Lm1;
hence  not F_Complex is degenerated by STRUCT_0:def_8; ::_thesis: verum
end;
end;

theorem :: COMPLFLD:1
for x1, y1 being Element of F_Complex
for x2, y2 being complex number st x1 = x2 & y1 = y2 holds
x1 + y1 = x2 + y2 ;

theorem Th2: :: COMPLFLD:2
for x1 being Element of F_Complex
for x2 being complex number st x1 = x2 holds
- x1 = - x2
proof
let x1 be Element of F_Complex; ::_thesis: for x2 being complex number st x1 = x2 holds
- x1 = - x2
let x2 be complex number ; ::_thesis: ( x1 = x2 implies - x1 = - x2 )
assume A1: x1 = x2 ; ::_thesis: - x1 = - x2
reconsider x2 = x2 as Element of COMPLEX by XCMPLX_0:def_2;
reconsider x9 = - x2 as Element of F_Complex by Def1;
 x1 + x9 = 0. F_Complex by A1, Def1;
hence  - x1 = - x2 by RLVECT_1:def_10; ::_thesis: verum
end;

theorem Th3: :: COMPLFLD:3
for x1, y1 being Element of F_Complex
for x2, y2 being complex number st x1 = x2 & y1 = y2 holds
x1 - y1 = x2 - y2
proof
let x1, y1 be Element of F_Complex; ::_thesis: for x2, y2 being complex number st x1 = x2 & y1 = y2 holds
x1 - y1 = x2 - y2
let x2, y2 be complex number ; ::_thesis: ( x1 = x2 & y1 = y2 implies x1 - y1 = x2 - y2 )
assume that
A1: x1 = x2 and
A2: y1 = y2 ; ::_thesis: x1 - y1 = x2 - y2
 - y1 = - y2 by A2, Th2;
hence  x1 - y1 = x2 - y2 by A1; ::_thesis: verum
end;

theorem :: COMPLFLD:4
for x1, y1 being Element of F_Complex
for x2, y2 being complex number st x1 = x2 & y1 = y2 holds
x1 * y1 = x2 * y2 ;

theorem Th5: :: COMPLFLD:5
for x1 being Element of F_Complex
for x2 being complex number st x1 = x2 & x1 <> 0. F_Complex holds
x1 " = x2 "
proof
let x1 be Element of F_Complex; ::_thesis: for x2 being complex number st x1 = x2 & x1 <> 0. F_Complex holds
x1 " = x2 "
let x2 be complex number ; ::_thesis: ( x1 = x2 & x1 <> 0. F_Complex implies x1 " = x2 " )
reconsider x4 = x2 as Element of COMPLEX by XCMPLX_0:def_2;
reconsider x9 = x4 " as Element of F_Complex by Def1;
assume that
A1: x1 = x2 and
A2: x1 <> 0. F_Complex ; ::_thesis: x1 " = x2 "
 0c = 0. F_Complex by Def1;
then  x1 * x9 = 1. F_Complex by A1, A2, Lm2, XCMPLX_0:def_7;
hence  x1 " = x2 " by A2, VECTSP_1:def_10; ::_thesis: verum
end;

theorem Th6: :: COMPLFLD:6
for x1, y1 being Element of F_Complex
for x2, y2 being complex number st x1 = x2 & y1 = y2 & y1 <> 0. F_Complex holds
x1 / y1 = x2 / y2
proof
let x1, y1 be Element of F_Complex; ::_thesis: for x2, y2 being complex number st x1 = x2 & y1 = y2 & y1 <> 0. F_Complex holds
x1 / y1 = x2 / y2
let x2, y2 be complex number ; ::_thesis: ( x1 = x2 & y1 = y2 & y1 <> 0. F_Complex implies x1 / y1 = x2 / y2 )
assume that
A1: x1 = x2 and
A2: y1 = y2 ; ::_thesis: ( not y1 <> 0. F_Complex or x1 / y1 = x2 / y2 )
assume  y1 <> 0. F_Complex ; ::_thesis: x1 / y1 = x2 / y2
then  y1 " = y2 " by A2, Th5;
hence  x1 / y1 = x2 / y2 by A1, XCMPLX_0:def_9; ::_thesis: verum
end;

theorem Th7: :: COMPLFLD:7
0. F_Complex = 0c by Def1;

theorem :: COMPLFLD:8
1_ F_Complex = 1r by Def1;

theorem :: COMPLFLD:9
(1_ F_Complex) + (1_ F_Complex) <> 0. F_Complex by Def1, Lm1;

definition
let z be Element of F_Complex;
:: original: *'
redefine funcz *'  ->  Element of F_Complex;
coherence
 z *' is Element of F_Complex
proof
 z *' in COMPLEX ;
hence  z *' is Element of F_Complex by Def1; ::_thesis: verum
end;
end;


theorem :: COMPLFLD:10
for z being Element of F_Complex holds - z = (- (1_ F_Complex)) * z
proof
let z be Element of F_Complex; ::_thesis: - z = (- (1_ F_Complex)) * z
reconsider z9 = z as Element of COMPLEX by Def1;
A1: - 1r = - (1_ F_Complex) by Lm1, Th2;
thus  - z = - z9 by Th2
.= (- (1_ F_Complex)) * z by A1 ; ::_thesis: verum
end;

theorem :: COMPLFLD:11
for z1, z2 being Element of F_Complex holds z1 - (- z2) = z1 + z2
proof
let z1, z2 be Element of F_Complex; ::_thesis: z1 - (- z2) = z1 + z2
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
 - z2 = - z29 by Th2;
hence z1 - (- z2) = z19 - (- z29) by Th3
.= z1 + z2 ;
::_thesis: verum
end;

theorem :: COMPLFLD:12
for z1, z being Element of F_Complex holds z1 = (z1 + z) - z
proof
let z1, z be Element of F_Complex; ::_thesis: z1 = (z1 + z) - z
reconsider z19 = z1, z9 = z as Element of COMPLEX by Def1;
thus (z1 + z) - z = (z19 + z9) - z9 by Th3
.= z1 ; ::_thesis: verum
end;

theorem :: COMPLFLD:13
for z1, z being Element of F_Complex holds z1 = (z1 - z) + z
proof
let z1, z be Element of F_Complex; ::_thesis: z1 = (z1 - z) + z
reconsider z19 = z1, z9 = z as Element of COMPLEX by Def1;
 z1 - z = z19 - z9 by Th3;
hence  z1 = (z1 - z) + z ; ::_thesis: verum
end;

theorem :: COMPLFLD:14
for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex & z1 " = z2 " holds
z1 = z2
proof
let z1, z2 be Element of F_Complex; ::_thesis: ( z1 <> 0. F_Complex & z2 <> 0. F_Complex & z1 " = z2 " implies z1 = z2 )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
assume A1: z1 <> 0. F_Complex ; ::_thesis: ( not z2 <> 0. F_Complex or not z1 " = z2 " or z1 = z2 )
assume A2: z2 <> 0. F_Complex ; ::_thesis: ( not z1 " = z2 " or z1 = z2 )
assume  z1 " = z2 " ; ::_thesis: z1 = z2
then z19 " = z2 " by A1, Th5
.= z29 " by A2, Th5 ;
hence  z1 = z2 by XCMPLX_1:201; ::_thesis: verum
end;

theorem :: COMPLFLD:15
for z2, z1 being Element of F_Complex st z2 <> 0. F_Complex & ( z1 * z2 = 1. F_Complex or z2 * z1 = 1. F_Complex ) holds
z1 = z2 "
proof
let z2, z1 be Element of F_Complex; ::_thesis: ( z2 <> 0. F_Complex & ( z1 * z2 = 1. F_Complex or z2 * z1 = 1. F_Complex ) implies z1 = z2 " )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
assume A1: z2 <> 0. F_Complex ; ::_thesis: ( ( not z1 * z2 = 1. F_Complex & not z2 * z1 = 1. F_Complex ) or z1 = z2 " )
assume A2: ( z1 * z2 = 1. F_Complex or z2 * z1 = 1. F_Complex ) ; ::_thesis: z1 = z2 "
percases ( z1 * z2 = 1. F_Complex or z2 * z1 = 1. F_Complex ) by A2;
supposeA3: z1 * z2 = 1. F_Complex ; ::_thesis: z1 = z2 "
A4: z2 " = z29 " by A1, Th5;
 z19 * z29 = 1r by A3, Def1;
hence  z1 = z2 " by A1, A4, Th7, XCMPLX_0:def_7; ::_thesis: verum
end;
supposeA5: z2 * z1 = 1. F_Complex ; ::_thesis: z1 = z2 "
A6: z2 " = z29 " by A1, Th5;
 z29 * z19 = 1r by A5, Def1;
hence  z1 = z2 " by A1, A6, Th7, XCMPLX_0:def_7; ::_thesis: verum
end;
end;
end;

theorem :: COMPLFLD:16
for z2, z1, z3 being Element of F_Complex st z2 <> 0. F_Complex & ( z1 * z2 = z3 or z2 * z1 = z3 ) holds
( z1 = z3 * (z2 ") & z1 = (z2 ") * z3 )
proof
let z2, z1, z3 be Element of F_Complex; ::_thesis: ( z2 <> 0. F_Complex & ( z1 * z2 = z3 or z2 * z1 = z3 ) implies ( z1 = z3 * (z2 ") & z1 = (z2 ") * z3 ) )
reconsider z29 = z2 as Element of COMPLEX by Def1;
assume A1: z2 <> 0. F_Complex ; ::_thesis: ( ( not z1 * z2 = z3 & not z2 * z1 = z3 ) or ( z1 = z3 * (z2 ") & z1 = (z2 ") * z3 ) )
then A2: z2 " = z29 " by Th5;
assume A3: ( z1 * z2 = z3 or z2 * z1 = z3 ) ; ::_thesis: ( z1 = z3 * (z2 ") & z1 = (z2 ") * z3 )
percases ( z1 * z2 = z3 or z2 * z1 = z3 ) by A3;
suppose z1 * z2 = z3 ; ::_thesis: ( z1 = z3 * (z2 ") & z1 = (z2 ") * z3 )
hence  ( z1 = z3 * (z2 ") & z1 = (z2 ") * z3 ) by A1, A2, Th7, XCMPLX_1:203; ::_thesis: verum
end;
suppose z2 * z1 = z3 ; ::_thesis: ( z1 = z3 * (z2 ") & z1 = (z2 ") * z3 )
hence  ( z1 = z3 * (z2 ") & z1 = (z2 ") * z3 ) by A1, A2, Th7, XCMPLX_1:203; ::_thesis: verum
end;
end;
end;

theorem :: COMPLFLD:17
(1. F_Complex) " = 1. F_Complex
proof
 1. F_Complex = 1r " by Def1;
hence  (1. F_Complex) " = 1. F_Complex by Th5; ::_thesis: verum
end;

theorem :: COMPLFLD:18
for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 * z2) " = (z1 ") * (z2 ")
proof
let z1, z2 be Element of F_Complex; ::_thesis: ( z1 <> 0. F_Complex & z2 <> 0. F_Complex implies (z1 * z2) " = (z1 ") * (z2 ") )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
assume A1: z1 <> 0. F_Complex ; ::_thesis: ( not z2 <> 0. F_Complex or (z1 * z2) " = (z1 ") * (z2 ") )
then A2: z1 " = z19 " by Th5;
assume A3: z2 <> 0. F_Complex ; ::_thesis: (z1 * z2) " = (z1 ") * (z2 ")
then A4: z2 " = z29 " by Th5;
 z1 * z2 <> 0. F_Complex by A1, A3, VECTSP_1:12;
hence (z1 * z2) " = (z19 * z29) " by Th5
.= (z1 ") * (z2 ") by A2, A4, XCMPLX_1:204 ;
::_thesis: verum
end;

theorem :: COMPLFLD:19
for z being Element of F_Complex st z <> 0. F_Complex holds
(- z) " = - (z ")
proof
let z be Element of F_Complex; ::_thesis: ( z <> 0. F_Complex implies (- z) " = - (z ") )
reconsider z1 = z as Element of COMPLEX by Def1;
A1: - z = - z1 by Th2;
assume A2: z <> 0. F_Complex ; ::_thesis: (- z) " = - (z ")
then A3: z1 " = z " by Th5;
 - z <> 0. F_Complex by A2, VECTSP_1:28;
hence (- z) " = (- z1) " by A1, Th5
.= - (z1 ") by XCMPLX_1:222
.= - (z ") by A3, Th2 ;
::_thesis: verum
end;

theorem :: COMPLFLD:20
for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 ") + (z2 ") = (z1 + z2) * ((z1 * z2) ")
proof
let z1, z2 be Element of F_Complex; ::_thesis: ( z1 <> 0. F_Complex & z2 <> 0. F_Complex implies (z1 ") + (z2 ") = (z1 + z2) * ((z1 * z2) ") )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
assume A1: z1 <> 0. F_Complex ; ::_thesis: ( not z2 <> 0. F_Complex or (z1 ") + (z2 ") = (z1 + z2) * ((z1 * z2) ") )
then A2: z1 " = z19 " by Th5;
assume A3: z2 <> 0. F_Complex ; ::_thesis: (z1 ") + (z2 ") = (z1 + z2) * ((z1 * z2) ")
then  z1 * z2 <> 0. F_Complex by A1, VECTSP_1:12;
then A4: (z1 * z2) " = (z19 * z29) " by Th5;
 z2 " = z29 " by A3, Th5;
hence  (z1 ") + (z2 ") = (z1 + z2) * ((z1 * z2) ") by A1, A2, A3, A4, Th7, XCMPLX_1:211; ::_thesis: verum
end;

theorem :: COMPLFLD:21
for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 ") - (z2 ") = (z2 - z1) * ((z1 * z2) ")
proof
let z1, z2 be Element of F_Complex; ::_thesis: ( z1 <> 0. F_Complex & z2 <> 0. F_Complex implies (z1 ") - (z2 ") = (z2 - z1) * ((z1 * z2) ") )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
A1: z2 - z1 = z29 - z19 by Th3;
assume A2: z1 <> 0. F_Complex ; ::_thesis: ( not z2 <> 0. F_Complex or (z1 ") - (z2 ") = (z2 - z1) * ((z1 * z2) ") )
then A3: z1 " = z19 " by Th5;
assume A4: z2 <> 0. F_Complex ; ::_thesis: (z1 ") - (z2 ") = (z2 - z1) * ((z1 * z2) ")
then  z1 * z2 <> 0. F_Complex by A2, VECTSP_1:12;
then A5: (z1 * z2) " = (z19 * z29) " by Th5;
 z2 " = z29 " by A4, Th5;
hence (z1 ") - (z2 ") = (z19 ") - (z29 ") by A3, Th3
.= (z2 - z1) * ((z1 * z2) ") by A2, A4, A1, A5, Th7, XCMPLX_1:212 ;
::_thesis: verum
end;

theorem :: COMPLFLD:22
for z being Element of F_Complex st z <> 0. F_Complex holds
z " = (1. F_Complex) / z
proof
let z be Element of F_Complex; ::_thesis: ( z <> 0. F_Complex implies z " = (1. F_Complex) / z )
reconsider z1 = z as Element of COMPLEX by Def1;
A1: 1. F_Complex = 1r by Def1;
assume A2: z <> 0. F_Complex ; ::_thesis: z " = (1. F_Complex) / z
hence z " = z1 " by Th5
.= 1r / z1 by XCMPLX_1:215
.= (1. F_Complex) / z by A2, A1, Th6 ;
::_thesis: verum
end;

theorem :: COMPLFLD:23
for z being Element of F_Complex holds z / (1. F_Complex) = z
proof
let z be Element of F_Complex; ::_thesis: z / (1. F_Complex) = z
reconsider z1 = z as Element of COMPLEX by Def1;
 1. F_Complex = 1r by Def1;
hence z / (1. F_Complex) = z1 / 1r by Th6
.= z ;
::_thesis: verum
end;

theorem :: COMPLFLD:24
for z being Element of F_Complex st z <> 0. F_Complex holds
z / z = 1. F_Complex
proof
let z be Element of F_Complex; ::_thesis: ( z <> 0. F_Complex implies z / z = 1. F_Complex )
reconsider z1 = z as Element of COMPLEX by Def1;
assume A1: z <> 0. F_Complex ; ::_thesis: z / z = 1. F_Complex
hence z / z = z1 / z1 by Th6
.= 1r by A1, Th7, XCMPLX_1:60
.= 1. F_Complex by Def1 ;
::_thesis: verum
end;

theorem :: COMPLFLD:25
for z being Element of F_Complex st z <> 0. F_Complex holds
(0. F_Complex) / z = 0. F_Complex by Th7;

theorem Th26: :: COMPLFLD:26
for z2, z1 being Element of F_Complex st z2 <> 0. F_Complex & z1 / z2 = 0. F_Complex holds
z1 = 0. F_Complex
proof
let z2, z1 be Element of F_Complex; ::_thesis: ( z2 <> 0. F_Complex & z1 / z2 = 0. F_Complex implies z1 = 0. F_Complex )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
assume A1: z2 <> 0. F_Complex ; ::_thesis: ( not z1 / z2 = 0. F_Complex or z1 = 0. F_Complex )
assume  z1 / z2 = 0. F_Complex ; ::_thesis: z1 = 0. F_Complex
then  z19 / z29 = 0. F_Complex by A1, Th6;
hence  z1 = 0. F_Complex by A1, Th7; ::_thesis: verum
end;

theorem :: COMPLFLD:27
for z2, z4, z1, z3 being Element of F_Complex st z2 <> 0. F_Complex & z4 <> 0. F_Complex holds
(z1 / z2) * (z3 / z4) = (z1 * z3) / (z2 * z4)
proof
let z2, z4, z1, z3 be Element of F_Complex; ::_thesis: ( z2 <> 0. F_Complex & z4 <> 0. F_Complex implies (z1 / z2) * (z3 / z4) = (z1 * z3) / (z2 * z4) )
reconsider z19 = z1, z29 = z2, z39 = z3, z49 = z4 as Element of COMPLEX by Def1;
assume A1: z2 <> 0. F_Complex ; ::_thesis: ( not z4 <> 0. F_Complex or (z1 / z2) * (z3 / z4) = (z1 * z3) / (z2 * z4) )
assume A2: z4 <> 0. F_Complex ; ::_thesis: (z1 / z2) * (z3 / z4) = (z1 * z3) / (z2 * z4)
then A3: z2 * z4 <> 0. F_Complex by A1, VECTSP_1:12;
A4: z39 / z49 = z3 / z4 by A2, Th6;
 z19 / z29 = z1 / z2 by A1, Th6;
hence (z1 / z2) * (z3 / z4) = (z19 * z39) / (z29 * z49) by A4, XCMPLX_1:76
.= (z1 * z3) / (z2 * z4) by A3, Th6 ;
::_thesis: verum
end;

theorem :: COMPLFLD:28
for z2, z, z1 being Element of F_Complex st z2 <> 0. F_Complex holds
z * (z1 / z2) = (z * z1) / z2 ;

theorem :: COMPLFLD:29
for z2, z1 being Element of F_Complex st z2 <> 0. F_Complex & z1 / z2 = 1. F_Complex holds
z1 = z2
proof
let z2, z1 be Element of F_Complex; ::_thesis: ( z2 <> 0. F_Complex & z1 / z2 = 1. F_Complex implies z1 = z2 )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
assume A1: z2 <> 0. F_Complex ; ::_thesis: ( not z1 / z2 = 1. F_Complex or z1 = z2 )
assume  z1 / z2 = 1. F_Complex ; ::_thesis: z1 = z2
then  z19 / z29 = 1. F_Complex by A1, Th6;
then  z19 / z29 = 1 by Def1;
hence  z1 = z2 by XCMPLX_1:58; ::_thesis: verum
end;

theorem :: COMPLFLD:30
for z, z1 being Element of F_Complex st z <> 0. F_Complex holds
z1 = (z1 * z) / z
proof
let z, z1 be Element of F_Complex; ::_thesis: ( z <> 0. F_Complex implies z1 = (z1 * z) / z )
reconsider z19 = z1, z9 = z as Element of COMPLEX by Def1;
assume A1: z <> 0. F_Complex ; ::_thesis: z1 = (z1 * z) / z
hence z1 = (z19 * z9) / z9 by Th7, XCMPLX_1:89
.= (z1 * z) / z by A1, Th6 ;
::_thesis: verum
end;

theorem :: COMPLFLD:31
for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 / z2) " = z2 / z1
proof
let z1, z2 be Element of F_Complex; ::_thesis: ( z1 <> 0. F_Complex & z2 <> 0. F_Complex implies (z1 / z2) " = z2 / z1 )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
assume A1: z1 <> 0. F_Complex ; ::_thesis: ( not z2 <> 0. F_Complex or (z1 / z2) " = z2 / z1 )
assume A2: z2 <> 0. F_Complex ; ::_thesis: (z1 / z2) " = z2 / z1
then A3: z19 / z29 = z1 / z2 by Th6;
 z1 / z2 <> 0. F_Complex by A1, A2, Th26;
hence (z1 / z2) " = (z19 / z29) " by A3, Th5
.= z29 / z19 by XCMPLX_1:213
.= z2 / z1 by A1, Th6 ;
::_thesis: verum
end;

theorem :: COMPLFLD:32
for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 ") / (z2 ") = z2 / z1
proof
let z1, z2 be Element of F_Complex; ::_thesis: ( z1 <> 0. F_Complex & z2 <> 0. F_Complex implies (z1 ") / (z2 ") = z2 / z1 )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
assume A1: z1 <> 0. F_Complex ; ::_thesis: ( not z2 <> 0. F_Complex or (z1 ") / (z2 ") = z2 / z1 )
assume  z2 <> 0. F_Complex ; ::_thesis: (z1 ") / (z2 ") = z2 / z1
then A2: ( z2 " = z29 " & z2 " <> 0. F_Complex ) by Th5, VECTSP_1:25;
 z1 " = z19 " by A1, Th5;
hence (z1 ") / (z2 ") = (z19 ") / (z29 ") by A2, Th6
.= z29 / z19 by XCMPLX_1:214
.= z2 / z1 by A1, Th6 ;
::_thesis: verum
end;

theorem :: COMPLFLD:33
for z2, z1 being Element of F_Complex st z2 <> 0. F_Complex holds
z1 / (z2 ") = z1 * z2
proof
let z2, z1 be Element of F_Complex; ::_thesis: ( z2 <> 0. F_Complex implies z1 / (z2 ") = z1 * z2 )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
assume  z2 <> 0. F_Complex ; ::_thesis: z1 / (z2 ") = z1 * z2
then  ( z2 " <> 0. F_Complex & z2 " = z29 " ) by Th5, VECTSP_1:25;
hence z1 / (z2 ") = z19 / (z29 ") by Th6
.= z1 * z2 by XCMPLX_1:219 ;
::_thesis: verum
end;

theorem :: COMPLFLD:34
for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 ") / z2 = (z1 * z2) "
proof
let z1, z2 be Element of F_Complex; ::_thesis: ( z1 <> 0. F_Complex & z2 <> 0. F_Complex implies (z1 ") / z2 = (z1 * z2) " )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
assume A1: z1 <> 0. F_Complex ; ::_thesis: ( not z2 <> 0. F_Complex or (z1 ") / z2 = (z1 * z2) " )
assume A2: z2 <> 0. F_Complex ; ::_thesis: (z1 ") / z2 = (z1 * z2) "
then A3: z1 * z2 <> 0. F_Complex by A1, VECTSP_1:12;
 z1 " = z19 " by A1, Th5;
hence (z1 ") / z2 = (z19 ") / z29 by A2, Th6
.= (z19 * z29) " by XCMPLX_1:221
.= (z1 * z2) " by A3, Th5 ;
::_thesis: verum
end;

theorem :: COMPLFLD:35
for z1, z2, z being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 ") * (z / z2) = z / (z1 * z2)
proof
let z1, z2, z be Element of F_Complex; ::_thesis: ( z1 <> 0. F_Complex & z2 <> 0. F_Complex implies (z1 ") * (z / z2) = z / (z1 * z2) )
reconsider z19 = z1, z29 = z2, z9 = z as Element of COMPLEX by Def1;
assume A1: z1 <> 0. F_Complex ; ::_thesis: ( not z2 <> 0. F_Complex or (z1 ") * (z / z2) = z / (z1 * z2) )
assume A2: z2 <> 0. F_Complex ; ::_thesis: (z1 ") * (z / z2) = z / (z1 * z2)
then A3: z1 * z2 <> 0. F_Complex by A1, VECTSP_1:12;
A4: z9 / z29 = z / z2 by A2, Th6;
 z1 " = z19 " by A1, Th5;
hence (z1 ") * (z / z2) = z9 / (z19 * z29) by A4, XCMPLX_1:220
.= z / (z1 * z2) by A3, Th6 ;
::_thesis: verum
end;

theorem :: COMPLFLD:36
for z, z2, z1 being Element of F_Complex st z <> 0. F_Complex & z2 <> 0. F_Complex holds
( z1 / z2 = (z1 * z) / (z2 * z) & z1 / z2 = (z * z1) / (z * z2) )
proof
let z, z2, z1 be Element of F_Complex; ::_thesis: ( z <> 0. F_Complex & z2 <> 0. F_Complex implies ( z1 / z2 = (z1 * z) / (z2 * z) & z1 / z2 = (z * z1) / (z * z2) ) )
reconsider z19 = z1, z29 = z2, z9 = z as Element of COMPLEX by Def1;
assume A1: z <> 0. F_Complex ; ::_thesis: ( not z2 <> 0. F_Complex or ( z1 / z2 = (z1 * z) / (z2 * z) & z1 / z2 = (z * z1) / (z * z2) ) )
assume A2: z2 <> 0. F_Complex ; ::_thesis: ( z1 / z2 = (z1 * z) / (z2 * z) & z1 / z2 = (z * z1) / (z * z2) )
then A3: z2 * z <> 0. F_Complex by A1, VECTSP_1:12;
thus z1 / z2 = z19 / z29 by A2, Th6
.= (z19 * z9) / (z29 * z9) by A1, Th7, XCMPLX_1:91
.= (z1 * z) / (z2 * z) by A3, Th6 ; ::_thesis: z1 / z2 = (z * z1) / (z * z2)
hence  z1 / z2 = (z * z1) / (z * z2) ; ::_thesis: verum
end;

theorem :: COMPLFLD:37
for z2, z3, z1 being Element of F_Complex st z2 <> 0. F_Complex & z3 <> 0. F_Complex holds
z1 / (z2 * z3) = (z1 / z2) / z3
proof
let z2, z3, z1 be Element of F_Complex; ::_thesis: ( z2 <> 0. F_Complex & z3 <> 0. F_Complex implies z1 / (z2 * z3) = (z1 / z2) / z3 )
reconsider z19 = z1, z29 = z2, z39 = z3 as Element of COMPLEX by Def1;
assume A1: z2 <> 0. F_Complex ; ::_thesis: ( not z3 <> 0. F_Complex or z1 / (z2 * z3) = (z1 / z2) / z3 )
then A2: z1 / z2 = z19 / z29 by Th6;
assume A3: z3 <> 0. F_Complex ; ::_thesis: z1 / (z2 * z3) = (z1 / z2) / z3
then  z2 * z3 <> 0. F_Complex by A1, VECTSP_1:12;
hence z1 / (z2 * z3) = z19 / (z29 * z39) by Th6
.= (z19 / z29) / z39 by XCMPLX_1:78
.= (z1 / z2) / z3 by A3, A2, Th6 ;
::_thesis: verum
end;

theorem :: COMPLFLD:38
for z2, z3, z1 being Element of F_Complex st z2 <> 0. F_Complex & z3 <> 0. F_Complex holds
(z1 * z3) / z2 = z1 / (z2 / z3)
proof
let z2, z3, z1 be Element of F_Complex; ::_thesis: ( z2 <> 0. F_Complex & z3 <> 0. F_Complex implies (z1 * z3) / z2 = z1 / (z2 / z3) )
reconsider z19 = z1, z29 = z2, z39 = z3 as Element of COMPLEX by Def1;
assume A1: z2 <> 0. F_Complex ; ::_thesis: ( not z3 <> 0. F_Complex or (z1 * z3) / z2 = z1 / (z2 / z3) )
assume A2: z3 <> 0. F_Complex ; ::_thesis: (z1 * z3) / z2 = z1 / (z2 / z3)
then A3: z2 / z3 <> 0. F_Complex by A1, Th26;
A4: z2 / z3 = z29 / z39 by A2, Th6;
thus (z1 * z3) / z2 = (z19 * z39) / z29 by A1, Th6
.= z19 / (z29 / z39) by XCMPLX_1:77
.= z1 / (z2 / z3) by A4, A3, Th6 ; ::_thesis: verum
end;

theorem :: COMPLFLD:39
for z2, z3, z4, z1 being Element of F_Complex st z2 <> 0. F_Complex & z3 <> 0. F_Complex & z4 <> 0. F_Complex holds
(z1 / z2) / (z3 / z4) = (z1 * z4) / (z2 * z3)
proof
let z2, z3, z4, z1 be Element of F_Complex; ::_thesis: ( z2 <> 0. F_Complex & z3 <> 0. F_Complex & z4 <> 0. F_Complex implies (z1 / z2) / (z3 / z4) = (z1 * z4) / (z2 * z3) )
reconsider z19 = z1, z29 = z2, z39 = z3, z49 = z4 as Element of COMPLEX by Def1;
assume A1: z2 <> 0. F_Complex ; ::_thesis: ( not z3 <> 0. F_Complex or not z4 <> 0. F_Complex or (z1 / z2) / (z3 / z4) = (z1 * z4) / (z2 * z3) )
then A2: z1 / z2 = z19 / z29 by Th6;
assume A3: z3 <> 0. F_Complex ; ::_thesis: ( not z4 <> 0. F_Complex or (z1 / z2) / (z3 / z4) = (z1 * z4) / (z2 * z3) )
then A4: z2 * z3 <> 0. F_Complex by A1, VECTSP_1:12;
assume A5: z4 <> 0. F_Complex ; ::_thesis: (z1 / z2) / (z3 / z4) = (z1 * z4) / (z2 * z3)
then A6: z3 / z4 = z39 / z49 by Th6;
 z3 / z4 <> 0. F_Complex by A3, A5, Th26;
hence (z1 / z2) / (z3 / z4) = (z19 / z29) / (z39 / z49) by A2, A6, Th6
.= (z19 * z49) / (z29 * z39) by XCMPLX_1:84
.= (z1 * z4) / (z2 * z3) by A4, Th6 ;
::_thesis: verum
end;

theorem :: COMPLFLD:40
for z2, z4, z1, z3 being Element of F_Complex st z2 <> 0. F_Complex & z4 <> 0. F_Complex holds
(z1 / z2) + (z3 / z4) = ((z1 * z4) + (z3 * z2)) / (z2 * z4)
proof
let z2, z4, z1, z3 be Element of F_Complex; ::_thesis: ( z2 <> 0. F_Complex & z4 <> 0. F_Complex implies (z1 / z2) + (z3 / z4) = ((z1 * z4) + (z3 * z2)) / (z2 * z4) )
reconsider z19 = z1, z29 = z2, z39 = z3, z49 = z4 as Element of COMPLEX by Def1;
assume A1: z2 <> 0. F_Complex ; ::_thesis: ( not z4 <> 0. F_Complex or (z1 / z2) + (z3 / z4) = ((z1 * z4) + (z3 * z2)) / (z2 * z4) )
then A2: z1 / z2 = z19 / z29 by Th6;
assume A3: z4 <> 0. F_Complex ; ::_thesis: (z1 / z2) + (z3 / z4) = ((z1 * z4) + (z3 * z2)) / (z2 * z4)
then A4: z2 * z4 <> 0. F_Complex by A1, VECTSP_1:12;
 z3 / z4 = z39 / z49 by A3, Th6;
hence (z1 / z2) + (z3 / z4) = ((z19 * z49) + (z39 * z29)) / (z29 * z49) by A1, A3, A2, Th7, XCMPLX_1:116
.= ((z1 * z4) + (z3 * z2)) / (z2 * z4) by A4, Th6 ;
::_thesis: verum
end;

theorem :: COMPLFLD:41
for z, z1, z2 being Element of F_Complex st z <> 0. F_Complex holds
(z1 / z) + (z2 / z) = (z1 + z2) / z ;

theorem :: COMPLFLD:42
for z2, z1 being Element of F_Complex st z2 <> 0. F_Complex holds
( - (z1 / z2) = (- z1) / z2 & - (z1 / z2) = z1 / (- z2) )
proof
let z2, z1 be Element of F_Complex; ::_thesis: ( z2 <> 0. F_Complex implies ( - (z1 / z2) = (- z1) / z2 & - (z1 / z2) = z1 / (- z2) ) )
assume A1: z2 <> 0. F_Complex ; ::_thesis: ( - (z1 / z2) = (- z1) / z2 & - (z1 / z2) = z1 / (- z2) )
then A2: - z2 <> 0. F_Complex by VECTSP_1:28;
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
A3: - z1 = - z19 by Th2;
 z1 / z2 = z19 / z29 by A1, Th6;
hence  - (z1 / z2) = - (z19 / z29) by Th2
.= (- z19) / z29 by XCMPLX_1:187
.= (- z1) / z2 by A3, A1, Th6 ;
::_thesis: - (z1 / z2) = z1 / (- z2)
A4: - z2 = - z29 by Th2;
 z1 / z2 = z19 / z29 by A1, Th6;
hence  - (z1 / z2) = - (z19 / z29) by Th2
.= z19 / (- z29) by XCMPLX_1:188
.= z1 / (- z2) by A4, A2, Th6 ;
::_thesis: verum
end;

theorem :: COMPLFLD:43
for z2, z1 being Element of F_Complex st z2 <> 0. F_Complex holds
z1 / z2 = (- z1) / (- z2)
proof
let z2, z1 be Element of F_Complex; ::_thesis: ( z2 <> 0. F_Complex implies z1 / z2 = (- z1) / (- z2) )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
assume A1: z2 <> 0. F_Complex ; ::_thesis: z1 / z2 = (- z1) / (- z2)
then A2: - z2 <> 0. F_Complex by VECTSP_1:28;
A3: ( - z19 = - z1 & - z29 = - z2 ) by Th2;
thus z1 / z2 = z19 / z29 by A1, Th6
.= (- z19) / (- z29) by XCMPLX_1:191
.= (- z1) / (- z2) by A2, A3, Th6 ; ::_thesis: verum
end;

theorem :: COMPLFLD:44
for z2, z4, z1, z3 being Element of F_Complex st z2 <> 0. F_Complex & z4 <> 0. F_Complex holds
(z1 / z2) - (z3 / z4) = ((z1 * z4) - (z3 * z2)) / (z2 * z4)
proof
let z2, z4, z1, z3 be Element of F_Complex; ::_thesis: ( z2 <> 0. F_Complex & z4 <> 0. F_Complex implies (z1 / z2) - (z3 / z4) = ((z1 * z4) - (z3 * z2)) / (z2 * z4) )
reconsider z19 = z1, z29 = z2, z39 = z3, z49 = z4 as Element of COMPLEX by Def1;
A1: (z1 * z4) - (z3 * z2) = (z19 * z49) - (z39 * z29) by Th3;
assume A2: z2 <> 0. F_Complex ; ::_thesis: ( not z4 <> 0. F_Complex or (z1 / z2) - (z3 / z4) = ((z1 * z4) - (z3 * z2)) / (z2 * z4) )
then A3: z19 / z29 = z1 / z2 by Th6;
assume A4: z4 <> 0. F_Complex ; ::_thesis: (z1 / z2) - (z3 / z4) = ((z1 * z4) - (z3 * z2)) / (z2 * z4)
then A5: z2 * z4 <> 0. F_Complex by A2, VECTSP_1:12;
 z39 / z49 = z3 / z4 by A4, Th6;
hence (z1 / z2) - (z3 / z4) = (z19 / z29) - (z39 / z49) by A3, Th3
.= ((z19 * z49) - (z39 * z29)) / (z29 * z49) by A2, A4, Th7, XCMPLX_1:130
.= ((z1 * z4) - (z3 * z2)) / (z2 * z4) by A5, A1, Th6 ;
::_thesis: verum
end;

theorem :: COMPLFLD:45
for z, z1, z2 being Element of F_Complex st z <> 0. F_Complex holds
(z1 / z) - (z2 / z) = (z1 - z2) / z
proof
let z, z1, z2 be Element of F_Complex; ::_thesis: ( z <> 0. F_Complex implies (z1 / z) - (z2 / z) = (z1 - z2) / z )
reconsider z9 = z, z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
A1: z19 - z29 = z1 - z2 by Th3;
assume A2: z <> 0. F_Complex ; ::_thesis: (z1 / z) - (z2 / z) = (z1 - z2) / z
then  ( z19 / z9 = z1 / z & z29 / z9 = z2 / z ) by Th6;
hence (z1 / z) - (z2 / z) = (z19 / z9) - (z29 / z9) by Th3
.= (z19 - z29) / z9 by XCMPLX_1:120
.= (z1 - z2) / z by A2, A1, Th6 ;
::_thesis: verum
end;

theorem :: COMPLFLD:46
for z2, z1, z3 being Element of F_Complex st z2 <> 0. F_Complex & ( z1 * z2 = z3 or z2 * z1 = z3 ) holds
z1 = z3 / z2
proof
let z2, z1, z3 be Element of F_Complex; ::_thesis: ( z2 <> 0. F_Complex & ( z1 * z2 = z3 or z2 * z1 = z3 ) implies z1 = z3 / z2 )
reconsider z39 = z3, z29 = z2 as Element of COMPLEX by Def1;
assume A1: z2 <> 0. F_Complex ; ::_thesis: ( ( not z1 * z2 = z3 & not z2 * z1 = z3 ) or z1 = z3 / z2 )
assume A2: ( z1 * z2 = z3 or z2 * z1 = z3 ) ; ::_thesis: z1 = z3 / z2
percases ( z1 * z2 = z3 or z2 * z1 = z3 ) by A2;
suppose z1 * z2 = z3 ; ::_thesis: z1 = z3 / z2
hence z1 = z39 / z29 by A1, Th7, XCMPLX_1:89
.= z3 / z2 by A1, Th6 ;
::_thesis: verum
end;
suppose z2 * z1 = z3 ; ::_thesis: z1 = z3 / z2
hence z1 = z39 / z29 by A1, Th7, XCMPLX_1:89
.= z3 / z2 by A1, Th6 ;
::_thesis: verum
end;
end;
end;

theorem :: COMPLFLD:47
(0. F_Complex) *' = 0. F_Complex
proof
 0. F_Complex = 0c by Def1;
hence  (0. F_Complex) *' = 0. F_Complex by COMPLEX1:28; ::_thesis: verum
end;

theorem Th48: :: COMPLFLD:48
for z being Element of F_Complex st z *' = 0. F_Complex holds
z = 0. F_Complex
proof
let z be Element of F_Complex; ::_thesis: ( z *' = 0. F_Complex implies z = 0. F_Complex )
assume  z *' = 0. F_Complex ; ::_thesis: z = 0. F_Complex
then  z *' = 0c by Def1;
then  z = 0c by COMPLEX1:29;
hence  z = 0. F_Complex by Def1; ::_thesis: verum
end;

theorem :: COMPLFLD:49
(1. F_Complex) *' = 1. F_Complex
proof
 1. F_Complex = 1r by Def1;
hence  (1. F_Complex) *' = 1. F_Complex by COMPLEX1:30; ::_thesis: verum
end;

theorem :: COMPLFLD:50
for z being Element of F_Complex holds (z *') *' = z ;

theorem :: COMPLFLD:51
for z1, z2 being Element of F_Complex holds (z1 + z2) *' = (z1 *') + (z2 *') by COMPLEX1:32;

theorem :: COMPLFLD:52
for z being Element of F_Complex holds (- z) *' = - (z *')
proof
let z be Element of F_Complex; ::_thesis: (- z) *' = - (z *')
reconsider z9 = z as Element of COMPLEX by Def1;
 - z = - z9 by Th2;
hence (- z) *' = - (z9 *') by COMPLEX1:33
.= - (z *') by Th2 ;
::_thesis: verum
end;

theorem :: COMPLFLD:53
for z1, z2 being Element of F_Complex holds (z1 - z2) *' = (z1 *') - (z2 *')
proof
let z1, z2 be Element of F_Complex; ::_thesis: (z1 - z2) *' = (z1 *') - (z2 *')
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
 z19 - z29 = z1 - z2 by Th3;
hence (z1 - z2) *' = (z19 *') - (z29 *') by COMPLEX1:34
.= (z1 *') - (z2 *') by Th3 ;
::_thesis: verum
end;

theorem :: COMPLFLD:54
for z1, z2 being Element of F_Complex holds (z1 * z2) *' = (z1 *') * (z2 *') by COMPLEX1:35;

theorem :: COMPLFLD:55
for z being Element of F_Complex st z <> 0. F_Complex holds
(z ") *' = (z *') "
proof
let z be Element of F_Complex; ::_thesis: ( z <> 0. F_Complex implies (z ") *' = (z *') " )
reconsider z1 = z as Element of COMPLEX by Def1;
assume A1: z <> 0. F_Complex ; ::_thesis: (z ") *' = (z *') "
then A2: z *' <> 0. F_Complex by Th48;
 z " = z1 " by A1, Th5;
hence (z ") *' = (z1 *') " by COMPLEX1:36
.= (z *') " by A2, Th5 ;
::_thesis: verum
end;

theorem :: COMPLFLD:56
for z2, z1 being Element of F_Complex st z2 <> 0. F_Complex holds
(z1 / z2) *' = (z1 *') / (z2 *')
proof
let z2, z1 be Element of F_Complex; ::_thesis: ( z2 <> 0. F_Complex implies (z1 / z2) *' = (z1 *') / (z2 *') )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
assume A1: z2 <> 0. F_Complex ; ::_thesis: (z1 / z2) *' = (z1 *') / (z2 *')
then A2: z2 *' <> 0. F_Complex by Th48;
 z19 / z29 = z1 / z2 by A1, Th6;
hence (z1 / z2) *' = (z19 *') / (z29 *') by COMPLEX1:37
.= (z1 *') / (z2 *') by A2, Th6 ;
::_thesis: verum
end;

theorem :: COMPLFLD:57
|.(0. F_Complex).| = 0 by Def1, COMPLEX1:44;

theorem :: COMPLFLD:58
for z being Element of F_Complex st |.z.| = 0 holds
z = 0. F_Complex by Th7;

theorem :: COMPLFLD:59
for z being Element of F_Complex holds
( z <> 0. F_Complex iff 0 < |.z.| ) by Th7, COMPLEX1:47;

theorem :: COMPLFLD:60
|.(1. F_Complex).| = 1 by Def1, COMPLEX1:48;

theorem :: COMPLFLD:61
for z being Element of F_Complex holds |.(- z).| = |.z.|
proof
let z be Element of F_Complex; ::_thesis: |.(- z).| = |.z.|
reconsider z1 = z as Element of COMPLEX by Def1;
 - z1 = - z by Th2;
hence  |.(- z).| = |.z.| by COMPLEX1:52; ::_thesis: verum
end;

theorem :: COMPLFLD:62
for z1, z2 being Element of F_Complex holds |.(z1 + z2).| <= |.z1.| + |.z2.| by COMPLEX1:56;

theorem :: COMPLFLD:63
for z1, z2 being Element of F_Complex holds |.(z1 - z2).| <= |.z1.| + |.z2.|
proof
let z1, z2 be Element of F_Complex; ::_thesis: |.(z1 - z2).| <= |.z1.| + |.z2.|
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
 z19 - z29 = z1 - z2 by Th3;
hence  |.(z1 - z2).| <= |.z1.| + |.z2.| by COMPLEX1:57; ::_thesis: verum
end;

theorem :: COMPLFLD:64
for z1, z2 being Element of F_Complex holds |.z1.| - |.z2.| <= |.(z1 + z2).| by COMPLEX1:58;

theorem :: COMPLFLD:65
for z1, z2 being Element of F_Complex holds |.z1.| - |.z2.| <= |.(z1 - z2).|
proof
let z1, z2 be Element of F_Complex; ::_thesis: |.z1.| - |.z2.| <= |.(z1 - z2).|
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
 z19 - z29 = z1 - z2 by Th3;
hence  |.z1.| - |.z2.| <= |.(z1 - z2).| by COMPLEX1:59; ::_thesis: verum
end;

theorem :: COMPLFLD:66
for z1, z2 being Element of F_Complex holds |.(z1 - z2).| = |.(z2 - z1).|
proof
let z1, z2 be Element of F_Complex; ::_thesis: |.(z1 - z2).| = |.(z2 - z1).|
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
 ( z29 - z19 = z2 - z1 & z19 - z29 = z1 - z2 ) by Th3;
hence  |.(z1 - z2).| = |.(z2 - z1).| by COMPLEX1:60; ::_thesis: verum
end;

theorem :: COMPLFLD:67
for z1, z2 being Element of F_Complex holds
( |.(z1 - z2).| = 0 iff z1 = z2 )
proof
let z1, z2 be Element of F_Complex; ::_thesis: ( |.(z1 - z2).| = 0 iff z1 = z2 )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
thus  ( |.(z1 - z2).| = 0 implies z1 = z2 ) ::_thesis: ( z1 = z2 implies |.(z1 - z2).| = 0 )
proof
assume A1: |.(z1 - z2).| = 0 ; ::_thesis: z1 = z2
 z1 - z2 = z19 - z29 by Th3;
hence  z1 = z2 by A1, COMPLEX1:61; ::_thesis: verum
end;
assume A2: z1 = z2 ; ::_thesis: |.(z1 - z2).| = 0
 z19 - z29 = z1 - z2 by Th3;
hence  |.(z1 - z2).| = 0 by A2; ::_thesis: verum
end;

theorem :: COMPLFLD:68
for z1, z2 being Element of F_Complex holds
( z1 <> z2 iff 0 < |.(z1 - z2).| )
proof
let z1, z2 be Element of F_Complex; ::_thesis: ( z1 <> z2 iff 0 < |.(z1 - z2).| )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
thus  ( z1 <> z2 implies 0 < |.(z1 - z2).| ) ::_thesis: ( 0 < |.(z1 - z2).| implies z1 <> z2 )
proof
assume A1: z1 <> z2 ; ::_thesis: 0 < |.(z1 - z2).|
 z1 - z2 = z19 - z29 by Th3;
hence  0 < |.(z1 - z2).| by A1, COMPLEX1:62; ::_thesis: verum
end;
assume A2: 0 < |.(z1 - z2).| ; ::_thesis: z1 <> z2
 z1 - z2 = z19 - z29 by Th3;
hence  z1 <> z2 by A2; ::_thesis: verum
end;

theorem :: COMPLFLD:69
for z1, z2, z being Element of F_Complex holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|
proof
let z1, z2, z be Element of F_Complex; ::_thesis: |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|
reconsider z9 = z, z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
A1: z9 - z29 = z - z2 by Th3;
 ( |.(z19 - z29).| = |.(z1 - z2).| & |.(z19 - z9).| = |.(z1 - z).| ) by Th3;
hence  |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| by A1, COMPLEX1:63; ::_thesis: verum
end;

theorem :: COMPLFLD:70
for z1, z2 being Element of F_Complex holds abs (|.z1.| - |.z2.|) <= |.(z1 - z2).|
proof
let z1, z2 be Element of F_Complex; ::_thesis: abs (|.z1.| - |.z2.|) <= |.(z1 - z2).|
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
 z19 - z29 = z1 - z2 by Th3;
hence  abs (|.z1.| - |.z2.|) <= |.(z1 - z2).| by COMPLEX1:64; ::_thesis: verum
end;

theorem :: COMPLFLD:71
for z1, z2 being Element of F_Complex holds |.(z1 * z2).| = |.z1.| * |.z2.| by COMPLEX1:65;

theorem :: COMPLFLD:72
for z being Element of F_Complex st z <> 0. F_Complex holds
|.(z ").| = |.z.| "
proof
let z be Element of F_Complex; ::_thesis: ( z <> 0. F_Complex implies |.(z ").| = |.z.| " )
reconsider z1 = z as Element of COMPLEX by Def1;
assume  z <> 0. F_Complex ; ::_thesis: |.(z ").| = |.z.| "
then  z " = z1 " by Th5;
hence  |.(z ").| = |.z.| " by COMPLEX1:66; ::_thesis: verum
end;

theorem :: COMPLFLD:73
for z2, z1 being Element of F_Complex st z2 <> 0. F_Complex holds
|.z1.| / |.z2.| = |.(z1 / z2).|
proof
let z2, z1 be Element of F_Complex; ::_thesis: ( z2 <> 0. F_Complex implies |.z1.| / |.z2.| = |.(z1 / z2).| )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
assume  z2 <> 0. F_Complex ; ::_thesis: |.z1.| / |.z2.| = |.(z1 / z2).|
then  z19 / z29 = z1 / z2 by Th6;
hence  |.z1.| / |.z2.| = |.(z1 / z2).| by COMPLEX1:67; ::_thesis: verum
end;

begin

scheme :: COMPLFLD:sch 1
Regrwithout0{ P1[ Nat] } :
 P1[1]
provided
A1: ex k being non empty Element of NAT st P1[k] and
A2: for k being non empty Element of NAT st k <> 1 & P1[k] holds
ex n being non empty Element of NAT st
( n < k & P1[n] )
proof
consider t being non empty Element of NAT  such that
A3: P1[t] by A1;
defpred S1[ Nat] means P1[$1 + 1];
A4: now__::_thesis:_for_k_being_Nat_st_k_<>_0_&_S1[k]_holds_
ex_l_being_Nat_st_
(_l_<_k_&_S1[l]_)
let k be Nat; ::_thesis: ( k <> 0 & S1[k] implies ex l being Nat st
( l < k & S1[l] ) )
assume that
A5: k <> 0 and
A6: S1[k] ; ::_thesis: ex l being Nat st
( l < k & S1[l] )
reconsider k1 = k + 1 as non empty Element of NAT ;
 k > 0 by A5, NAT_1:3;
then  k + 1 > 0 + 1 by XREAL_1:6;
then consider n being non empty Element of NAT  such that
A7: n < k1 and
A8: P1[n] by A2, A6;
consider l being Nat such that
A9: n = l + 1 by NAT_1:6;
take l = l; ::_thesis: ( l < k & S1[l] )
thus  l < k by A7, A9, XREAL_1:6; ::_thesis: S1[l]
thus  S1[l] by A8, A9; ::_thesis: verum
end;
 ex s being Nat st t = s + 1 by NAT_1:6;
then A10: ex k being Nat st S1[k] by A3;
 S1[ 0 ] from NAT_1:sch_7(A10, A4);
hence  P1[1] ; ::_thesis: verum
end;

theorem Th74: :: COMPLFLD:74
for e being Element of F_Complex
for n being non empty Nat holds (power F_Complex) . (e,n) = e |^ n
proof
let e be Element of F_Complex; ::_thesis: for n being non empty Nat holds (power F_Complex) . (e,n) = e |^ n
defpred S1[ Nat] means (power F_Complex) . (e,$1) = e |^ $1;
A1: now__::_thesis:_for_n_being_non_empty_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be non empty Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
reconsider p = (power F_Complex) . (e,n9) as Element of F_Complex ;
assume A2: S1[n] ; ::_thesis: S1[n + 1]
(power F_Complex) . (e,(n + 1)) = p * e by GROUP_1:def_7
.= e |^ (n + 1) by A2, NEWTON:6 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
 (power F_Complex) . (e,1) = e by GROUP_1:50;
then A3: S1[1] by NEWTON:5;
thus  for n being non empty Nat holds S1[n] from NAT_1:sch_10(A3, A1); ::_thesis: verum
end;

definition
let x be Element of F_Complex;
let n be non empty Element of NAT ;
:: original: CRoot
redefine mode CRoot of n,x ->  Element of F_Complex means :Def2: :: COMPLFLD:def 2
(power F_Complex) . (it,n) = x;
coherence
 for b1 being CRoot of n,x holds b1 is Element of F_Complex
proof
let e be CRoot of n,x; ::_thesis: e is Element of F_Complex
 e is Element of COMPLEX by XCMPLX_0:def_2;
hence  e is Element of F_Complex by Def1; ::_thesis: verum
end;
compatibility
 for b1 being Element of F_Complex holds
( b1 is CRoot of n,x iff (power F_Complex) . (b1,n) = x )
proof
let e be Element of F_Complex; ::_thesis: ( e is CRoot of n,x iff (power F_Complex) . (e,n) = x )
thus  ( e is CRoot of n,x implies (power F_Complex) . (e,n) = x ) ::_thesis: ( (power F_Complex) . (e,n) = x implies e is CRoot of n,x )
proof
assume  e is CRoot of n,x ; ::_thesis: (power F_Complex) . (e,n) = x
then  e |^ n = x by COMPTRIG:def_2;
hence  (power F_Complex) . (e,n) = x by Th74; ::_thesis: verum
end;
assume  (power F_Complex) . (e,n) = x ; ::_thesis: e is CRoot of n,x
hence  e |^ n = x by Th74; :: according to COMPTRIG:def_2 ::_thesis: verum
end;
end;

:: deftheorem Def2 defines CRoot COMPLFLD:def_2_:_
 for x being Element of F_Complex
for n being non empty Element of NAT
for b3 being Element of F_Complex holds
( b3 is CRoot of n,x iff (power F_Complex) . (b3,n) = x );

theorem :: COMPLFLD:75
for x being Element of F_Complex
for v being CRoot of 1,x holds v = x
proof
let x be Element of F_Complex; ::_thesis: for v being CRoot of 1,x holds v = x
let v be CRoot of 1,x; ::_thesis: v = x
 (power F_Complex) . (v,1) = x by Def2;
hence  v = x by GROUP_1:50; ::_thesis: verum
end;

theorem :: COMPLFLD:76
for n being non empty Element of NAT
for v being CRoot of n, 0. F_Complex holds v = 0. F_Complex
proof
let n be non empty Element of NAT ; ::_thesis: for v being CRoot of n, 0. F_Complex holds v = 0. F_Complex
let v be CRoot of n, 0. F_Complex; ::_thesis: v = 0. F_Complex
defpred S1[ Element of NAT ] means (power F_Complex) . (v,$1) = 0. F_Complex;
A1: now__::_thesis:_for_k_being_non_empty_Element_of_NAT_st_k_<>_1_&_S1[k]_holds_
ex_t_being_non_empty_Element_of_NAT_st_
(_t_<_k_&_S1[t]_)
let k be non empty Element of NAT ; ::_thesis: ( k <> 1 & S1[k] implies ex t being non empty Element of NAT st
( t < k & S1[t] ) )
assume that
A2: k <> 1 and
A3: S1[k] ; ::_thesis: ex t being non empty Element of NAT st
( t < k & S1[t] )
consider t being Nat such that
A4: k = t + 1 by NAT_1:6;
reconsider t = t as Element of NAT by ORDINAL1:def_12;
reconsider t = t as non empty Element of NAT by A2, A4;
take t = t; ::_thesis: ( t < k & S1[t] )
thus  t < k by A4, NAT_1:13; ::_thesis: S1[t]
 (power F_Complex) . (v,k) = ((power F_Complex) . (v,t)) * v by A4, GROUP_1:def_7;
then  ( (power F_Complex) . (v,t) = 0. F_Complex or v = 0. F_Complex ) by A3, VECTSP_1:12;
hence  S1[t] by NAT_1:3, VECTSP_1:36; ::_thesis: verum
end;
A5: ex n being non empty Element of NAT st S1[n]
proof
take  n ; ::_thesis: S1[n]
thus  S1[n] by Def2; ::_thesis: verum
end;
 S1[1] from COMPLFLD:sch_1(A5, A1);
hence  v = 0. F_Complex by GROUP_1:50; ::_thesis: verum
end;

theorem :: COMPLFLD:77
for n being non empty Element of NAT
for x being Element of F_Complex
for v being CRoot of n,x st v = 0. F_Complex holds
x = 0. F_Complex
proof
let n be non empty Element of NAT ; ::_thesis: for x being Element of F_Complex
for v being CRoot of n,x st v = 0. F_Complex holds
x = 0. F_Complex
let x be Element of F_Complex; ::_thesis: for v being CRoot of n,x st v = 0. F_Complex holds
x = 0. F_Complex
let v be CRoot of n,x; ::_thesis: ( v = 0. F_Complex implies x = 0. F_Complex )
assume  v = 0. F_Complex ; ::_thesis: x = 0. F_Complex
then  (power F_Complex) . ((0. F_Complex),n) = x by Def2;
hence  x = 0. F_Complex by NAT_1:3, VECTSP_1:36; ::_thesis: verum
end;