:: by Anna Justyna Milewska

::

:: Received January 18, 2000

:: Copyright (c) 2000-2012 Association of Mizar Users

begin

definition

ex b_{1} being strict doubleLoopStr st

( the carrier of b_{1} = COMPLEX & the addF of b_{1} = addcomplex & the multF of b_{1} = multcomplex & 1. b_{1} = 1r & 0. b_{1} = 0c )

for b_{1}, b_{2} being strict doubleLoopStr st the carrier of b_{1} = COMPLEX & the addF of b_{1} = addcomplex & the multF of b_{1} = multcomplex & 1. b_{1} = 1r & 0. b_{1} = 0c & the carrier of b_{2} = COMPLEX & the addF of b_{2} = addcomplex & the multF of b_{2} = multcomplex & 1. b_{2} = 1r & 0. b_{2} = 0c holds

b_{1} = b_{2}
;

end;

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 ( the carrier of it = COMPLEX & the addF of it = addcomplex & the multF of it = multcomplex & 1. it = 1r & 0. it = 0c );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def1 defines F_Complex COMPLFLD:def 1 :

for b_{1} being strict doubleLoopStr holds

( b_{1} = F_Complex iff ( the carrier of b_{1} = COMPLEX & the addF of b_{1} = addcomplex & the multF of b_{1} = multcomplex & 1. b_{1} = 1r & 0. b_{1} = 0c ) );

for b

( b

registration

let a, b be complex number ;

let x, y be Element of F_Complex;

compatibility

( x = a & y = b implies x + y = a + b )

( x = a & y = b implies x * y = a * b )

end;
let x, y be Element of F_Complex;

compatibility

( x = a & y = b implies x + y = a + b )

proof end;

compatibility ( x = a & y = b implies x * y = a * b )

proof end;

registration
end;

Lm1: 1_ F_Complex = 1r

by Def1;

Lm2: 1. F_Complex = 1r

by Def1;

registration

( 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 )
end;

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 end;

theorem :: COMPLFLD:1

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

for x2, y2 being complex number st x1 = x2 & y1 = y2 holds

x1 - y1 = x2 - y2

proof end;

theorem :: COMPLFLD:4

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 "

for x2 being complex number st x1 = x2 & x1 <> 0. F_Complex holds

x1 " = x2 "

proof 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

for x2, y2 being complex number st x1 = x2 & y1 = y2 & y1 <> 0. F_Complex holds

x1 / y1 = x2 / y2

proof end;

definition

let z be Element of F_Complex;

:: original: *'

redefine func z *' -> Element of F_Complex;

coherence

z *' is Element of F_Complex

end;
:: original: *'

redefine func z *' -> Element of F_Complex;

coherence

z *' is Element of F_Complex

proof 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

z1 = z2

proof 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 "

z1 = z2 "

proof 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 )

( z1 = z3 * (z2 ") & z1 = (z2 ") * z3 )

proof 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 ")

(z1 * z2) " = (z1 ") * (z2 ")

proof 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) ")

(z1 ") + (z2 ") = (z1 + z2) * ((z1 * z2) ")

proof 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) ")

(z1 ") - (z2 ") = (z2 - z1) * ((z1 * z2) ")

proof end;

theorem :: COMPLFLD:25

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

z1 = 0. F_Complex

proof 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)

(z1 / z2) * (z3 / z4) = (z1 * z3) / (z2 * z4)

proof end;

theorem :: COMPLFLD:28

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

(z1 / z2) " = z2 / z1

proof 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

(z1 ") / (z2 ") = z2 / z1

proof 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) "

(z1 ") / z2 = (z1 * z2) "

proof 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)

(z1 ") * (z / z2) = z / (z1 * z2)

proof 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) )

( z1 / z2 = (z1 * z) / (z2 * z) & z1 / z2 = (z * z1) / (z * z2) )

proof 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

z1 / (z2 * z3) = (z1 / z2) / z3

proof 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)

(z1 * z3) / z2 = z1 / (z2 / z3)

proof 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)

(z1 / z2) / (z3 / z4) = (z1 * z4) / (z2 * z3)

proof 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)

(z1 / z2) + (z3 / z4) = ((z1 * z4) + (z3 * z2)) / (z2 * z4)

proof end;

theorem :: COMPLFLD:41

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) )

( - (z1 / z2) = (- z1) / z2 & - (z1 / z2) = z1 / (- z2) )

proof 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)

(z1 / z2) - (z3 / z4) = ((z1 * z4) - (z3 * z2)) / (z2 * z4)

proof 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

(z1 / z) - (z2 / z) = (z1 - z2) / z

proof 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

z1 = z3 / z2

proof end;

theorem :: COMPLFLD:51

theorem :: COMPLFLD:54

theorem :: COMPLFLD:59

theorem :: COMPLFLD:62

theorem :: COMPLFLD:64

theorem :: COMPLFLD:71

begin

:: from COMPTRIG, 2006.08.12, A.T.

definition

let x be Element of F_Complex;

let n be non empty Element of NAT ;

for b_{1} being CRoot of n,x holds b_{1} is Element of F_Complex

for b_{1} being Element of F_Complex holds

( b_{1} is CRoot of n,x iff (power F_Complex) . (b_{1},n) = x )

end;
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 redefine mode CRoot of n,x -> Element of F_Complex means :Def2: :: COMPLFLD:def 2

(power F_Complex) . (it,n) = x;

for b

proof end;

compatibility for b

( b

proof end;

:: deftheorem Def2 defines CRoot COMPLFLD:def 2 :

for x being Element of F_Complex

for n being non empty Element of NAT

for b_{3} being Element of F_Complex holds

( b_{3} is CRoot of n,x iff (power F_Complex) . (b_{3},n) = x );

for x being Element of F_Complex

for n being non empty Element of NAT

for b

( b

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

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 end;