:: COMPLFLD semantic presentation

theorem :: COMPLFLD:1

canceled;

theorem :: COMPLFLD:2

for x1, y1, x2, y2 being real number holds (x1 + (y1 * <i> )) + (x2 + (y2 * <i> )) = (x1 + x2) + ((y1 + y2) * <i> ) ;

definition

func F_Complex -> strict doubleLoopStr means :Def1: :: COMPLFLD:def 1
( 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 end;

uniqueness ;

end;

:: deftheorem Def1 defines F_Complex COMPLFLD:def 1 :

registration

cluster F_Complex -> non empty strict ;
coherence

proof end;

end;

registration

cluster -> complex Element of the carrier of F_Complex ;
coherence

proof end;

end;

Lm1: now

let x, e be Element of F_Complex ; :: thesis:
assume A1: e = 1r ; :: thesis:
reconsider a = x as Element of COMPLEX by Def1;
thus x * e = the mult of F_Complex . x,e
.= multcomplex . x,e by Def1
.= a * 1r by A1, BINOP_2:def 5
.= x by COMPLEX1:def 7 ; :: thesis:
thus e * x = the mult of F_Complex . e,x
.= multcomplex . e,x by Def1
.= a * 1r by A1, BINOP_2:def 5
.= x by COMPLEX1:def 7 ; :: thesis:

end;

registration

cluster F_Complex -> non empty unital strict ;
coherence

proof end;

end;

Lm2: 1. F_Complex = 1r

proof end;

registration

cluster F_Complex -> non empty Abelian add-associative right_zeroed right_complementable unital associative commutative strict right_unital distributive left_unital Field-like non degenerated ;
coherence

proof end;

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

theorem Th4: :: COMPLFLD:4

for x1 being Element of F_Complex
for x2 being complex number st x1 = x2 holds
- x1 = - x2

proof end;

theorem Th5: :: COMPLFLD:5

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

theorem Th6: :: COMPLFLD:6

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

theorem Th7: :: COMPLFLD:7

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

proof end;

theorem Th8: :: COMPLFLD:8

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

theorem Th9: :: COMPLFLD:9

0. F_Complex = 0c by Def1;

theorem Th10: :: COMPLFLD:10

1. F_Complex = 1r by Lm2;

theorem :: COMPLFLD:11

(1. F_Complex ) + (1. F_Complex ) <> 0. F_Complex

proof end;

definition

let z be Element of F_Complex ;
:: original: *'
redefine func z *' -> Element of F_Complex ;
coherence

proof end;

:: original: |.
redefine func |.z.| -> Element of REAL ;
coherence by XREAL_0:def 1;

end;

theorem :: COMPLFLD:12

canceled;

theorem :: COMPLFLD:13

canceled;

theorem :: COMPLFLD:14

canceled;

theorem :: COMPLFLD:15

canceled;

theorem :: COMPLFLD:16

canceled;

theorem :: COMPLFLD:17

canceled;

theorem :: COMPLFLD:18

canceled;

theorem :: COMPLFLD:19

canceled;

theorem :: COMPLFLD:20

canceled;

theorem :: COMPLFLD:21

canceled;

theorem :: COMPLFLD:22

canceled;

theorem :: COMPLFLD:23

canceled;

theorem :: COMPLFLD:24

canceled;

theorem :: COMPLFLD:25

canceled;

theorem :: COMPLFLD:26

canceled;

theorem :: COMPLFLD:27

canceled;

theorem :: COMPLFLD:28

canceled;

theorem :: COMPLFLD:29

for z being Element of F_Complex holds - z = (- (1. F_Complex )) * z

proof end;

theorem :: COMPLFLD:30

canceled;

theorem :: COMPLFLD:31

canceled;

theorem :: COMPLFLD:32

canceled;

theorem :: COMPLFLD:33

canceled;

theorem :: COMPLFLD:34

canceled;

theorem :: COMPLFLD:35

for z1, z2 being Element of F_Complex holds z1 - (- z2) = z1 + z2

proof end;

theorem :: COMPLFLD:36

canceled;

theorem :: COMPLFLD:37

canceled;

theorem :: COMPLFLD:38

canceled;

theorem :: COMPLFLD:39

canceled;

theorem :: COMPLFLD:40

canceled;

theorem :: COMPLFLD:41

for z1, z being Element of F_Complex holds z1 = (z1 + z) - z

proof end;

theorem :: COMPLFLD:42

for z1, z being Element of F_Complex holds z1 = (z1 - z) + z

proof end;

theorem :: COMPLFLD:43

canceled;

theorem :: COMPLFLD:44

canceled;

theorem :: COMPLFLD:45

canceled;

theorem :: COMPLFLD:46

canceled;

theorem :: COMPLFLD:47

for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex & z1 " = z2 " holds
z1 = z2

proof end;

theorem :: COMPLFLD:48

for z2, z1 being Element of F_Complex st z2 <> 0. F_Complex & ( z1 * z2 = the unity of F_Complex or z2 * z1 = the unity of F_Complex ) holds
z1 = z2 "

proof end;

theorem :: COMPLFLD:49

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

theorem :: COMPLFLD:50

the unity of F_Complex " = the unity of F_Complex

proof end;

theorem :: COMPLFLD:51

for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 * z2) " = (z1 " ) * (z2 " )

proof end;

theorem :: COMPLFLD:52

canceled;

theorem :: COMPLFLD:53

for z being Element of F_Complex st z <> 0. F_Complex holds
(- z) " = - (z " )

proof end;

theorem :: COMPLFLD:54

canceled;

theorem :: COMPLFLD:55

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

theorem :: COMPLFLD:56

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

theorem :: COMPLFLD:57

canceled;

theorem :: COMPLFLD:58

for z being Element of F_Complex st z <> 0. F_Complex holds
z " = the unity of F_Complex / z

proof end;

theorem :: COMPLFLD:59

for z being Element of F_Complex holds z / the unity of F_Complex = z

proof end;

theorem :: COMPLFLD:60

for z being Element of F_Complex st z <> 0. F_Complex holds
z / z = the unity of F_Complex

proof end;

theorem :: COMPLFLD:61

for z being Element of F_Complex st z <> 0. F_Complex holds
(0. F_Complex ) / z = 0. F_Complex

proof end;

theorem Th62: :: COMPLFLD:62

for z2, z1 being Element of F_Complex st z2 <> 0. F_Complex & z1 / z2 = 0. F_Complex holds
z1 = 0. F_Complex

proof end;

theorem :: COMPLFLD:63

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

theorem :: COMPLFLD:64

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

proof end;

theorem :: COMPLFLD:65

for z2, z1 being Element of F_Complex st z2 <> 0. F_Complex & z1 / z2 = the unity of F_Complex holds
z1 = z2

proof end;

theorem :: COMPLFLD:66

for z, z1 being Element of F_Complex st z <> 0. F_Complex holds
z1 = (z1 * z) / z

proof end;

theorem :: COMPLFLD:67

for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 / z2) " = z2 / z1

proof end;

theorem :: COMPLFLD:68

for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 " ) / (z2 " ) = z2 / z1

proof end;

theorem :: COMPLFLD:69

for z2, z1 being Element of F_Complex st z2 <> 0. F_Complex holds
z1 / (z2 " ) = z1 * z2

proof end;

theorem :: COMPLFLD:70

for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 " ) / z2 = (z1 * z2) "

proof end;

theorem :: COMPLFLD:71

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

theorem :: COMPLFLD:72

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

theorem :: COMPLFLD:73

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

theorem :: COMPLFLD:74

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

theorem :: COMPLFLD:75

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

theorem :: COMPLFLD:76

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

theorem :: COMPLFLD:77

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

proof end;

theorem :: COMPLFLD:78

for z2, z1 being Element of F_Complex st z2 <> 0. F_Complex holds
( - (z1 / z2) = (- z1) / z2 & - (z1 / z2) = z1 / (- z2) )

proof end;

theorem :: COMPLFLD:79

for z2, z1 being Element of F_Complex st z2 <> 0. F_Complex holds
z1 / z2 = (- z1) / (- z2)

proof end;

theorem :: COMPLFLD:80

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

theorem :: COMPLFLD:81