:: COMPLFLD semantic presentation

theorem Th1: :: COMPLFLD:1

canceled;

theorem Th2: :: COMPLFLD:2

for b₁, b₂, b₃, b₄ being real number holds (b₁ + (b₂ * <i> )) + (b₃ + (b₄ * <i> )) = (b₁ + b₃) + ((b₂ + b₄) * <i> ) ;

definition

func F_Complex -> strict doubleLoopStr means :Def1: :: COMPLFLD:def 1
( the carrier of a₁ = COMPLEX & the add of a₁ = addcomplex & the mult of a₁ = multcomplex & the unity of a₁ = 1r & the Zero of a₁ = 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;

E2: now

let c₁, c₂ be Element of F_Complex ;
assume E3: c₂ = 1r ;
reconsider c₃ = c₁ as Element of COMPLEX by Def1;
thus c₁ * c₂ = the mult of F_Complex . c₁,c₂
.= multcomplex . c₁,c₂ by Def1
.= c₃ * 1r by E3, BINOP_2:def 5
.= c₁ by COMPLEX1:def 7 ;
thus c₂ * c₁ = the mult of F_Complex . c₂,c₁
.= multcomplex . c₂,c₁ by Def1
.= c₃ * 1r by E3, BINOP_2:def 5
.= c₁ by COMPLEX1:def 7 ;

end;

registration

cluster F_Complex -> non empty unital strict ;
coherence

proof end;

end;

Lemma3: 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 b₁, b₂ being Element of F_Complex
for b₃, b₄ being complex number st b₁ = b₃ & b₂ = b₄ holds
b₁ + b₂ = b₃ + b₄

proof end;

theorem Th4: :: COMPLFLD:4

for b₁ being Element of F_Complex
for b₂ being complex number st b₁ = b₂ holds
- b₁ = - b₂

proof end;

theorem Th5: :: COMPLFLD:5

for b₁, b₂ being Element of F_Complex
for b₃, b₄ being complex number st b₁ = b₃ & b₂ = b₄ holds
b₁ - b₂ = b₃ - b₄

proof end;

theorem Th6: :: COMPLFLD:6

for b₁, b₂ being Element of F_Complex
for b₃, b₄ being complex number st b₁ = b₃ & b₂ = b₄ holds
b₁ * b₂ = b₃ * b₄

proof end;

theorem Th7: :: COMPLFLD:7

for b₁ being Element of F_Complex
for b₂ being complex number st b₁ = b₂ & b₁ <> 0. F_Complex holds
b₁ " = b₂ "

proof end;

theorem Th8: :: COMPLFLD:8

for b₁, b₂ being Element of F_Complex
for b₃, b₄ being complex number st b₁ = b₃ & b₂ = b₄ & b₂ <> 0. F_Complex holds
b₁ / b₂ = b₃ / b₄

proof end;

theorem Th9: :: COMPLFLD:9

0. F_Complex = 0c by Def1;

theorem Th10: :: COMPLFLD:10

1. F_Complex = 1r by Lemma3;

theorem Th11: :: COMPLFLD:11

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

proof end;

definition

let c₁ be Element of F_Complex ;
redefine func *' as c₁ *' -> Element of F_Complex ;
coherence

proof end;

redefine func |. as |.c₁.| -> Element of REAL ;
coherence by XREAL_0:def 1;

end;

theorem Th12: :: COMPLFLD:12

canceled;

theorem Th13: :: COMPLFLD:13

canceled;

theorem Th14: :: COMPLFLD:14

canceled;

theorem Th15: :: COMPLFLD:15

canceled;

theorem Th16: :: COMPLFLD:16

canceled;

theorem Th17: :: COMPLFLD:17

canceled;

theorem Th18: :: COMPLFLD:18

canceled;

theorem Th19: :: COMPLFLD:19

canceled;

theorem Th20: :: COMPLFLD:20

canceled;

theorem Th21: :: COMPLFLD:21

canceled;

theorem Th22: :: COMPLFLD:22

canceled;

theorem Th23: :: COMPLFLD:23

canceled;

theorem Th24: :: COMPLFLD:24

canceled;

theorem Th25: :: COMPLFLD:25

canceled;

theorem Th26: :: COMPLFLD:26

canceled;

theorem Th27: :: COMPLFLD:27

canceled;

theorem Th28: :: COMPLFLD:28

canceled;

theorem Th29: :: COMPLFLD:29

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

proof end;

theorem Th30: :: COMPLFLD:30

canceled;

theorem Th31: :: COMPLFLD:31

canceled;

theorem Th32: :: COMPLFLD:32

canceled;

theorem Th33: :: COMPLFLD:33

canceled;

theorem Th34: :: COMPLFLD:34

canceled;

theorem Th35: :: COMPLFLD:35

for b₁, b₂ being Element of F_Complex holds b₁ - (- b₂) = b₁ + b₂

proof end;

theorem Th36: :: COMPLFLD:36

canceled;

theorem Th37: :: COMPLFLD:37

canceled;

theorem Th38: :: COMPLFLD:38

canceled;

theorem Th39: :: COMPLFLD:39

canceled;

theorem Th40: :: COMPLFLD:40

canceled;

theorem Th41: :: COMPLFLD:41

for b₁, b₂ being Element of F_Complex holds b₁ = (b₁ + b₂) - b₂

proof end;

theorem Th42: :: COMPLFLD:42

for b₁, b₂ being Element of F_Complex holds b₁ = (b₁ - b₂) + b₂

proof end;

theorem Th43: :: COMPLFLD:43

canceled;

theorem Th44: :: COMPLFLD:44

canceled;

theorem Th45: :: COMPLFLD:45

canceled;

theorem Th46: :: COMPLFLD:46

canceled;

theorem Th47: :: COMPLFLD:47

for b₁, b₂ being Element of F_Complex st b₁ <> 0. F_Complex & b₂ <> 0. F_Complex & b₁ " = b₂ " holds
b₁ = b₂

proof end;

theorem Th48: :: COMPLFLD:48

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

proof end;

theorem Th49: :: COMPLFLD:49

for b₁, b₂, b₃ being Element of F_Complex st b₁ <> 0. F_Complex & ( b₂ * b₁ = b₃ or b₁ * b₂ = b₃ ) holds
( b₂ = b₃ * (b₁ " ) & b₂ = (b₁ " ) * b₃ )

proof end;

theorem Th50: :: COMPLFLD:50

the unity of F_Complex " = the unity of F_Complex

proof end;

theorem Th51: :: COMPLFLD:51

for b₁, b₂ being Element of F_Complex st b₁ <> 0. F_Complex & b₂ <> 0. F_Complex holds
(b₁ * b₂) " = (b₁ " ) * (b₂ " )

proof end;

theorem Th52: :: COMPLFLD:52

canceled;

theorem Th53: :: COMPLFLD:53

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

proof end;

theorem Th54: :: COMPLFLD:54

canceled;

theorem Th55: :: COMPLFLD:55

for b₁, b₂ being Element of F_Complex st b₁ <> 0. F_Complex & b₂ <> 0. F_Complex holds
(b₁ " ) + (b₂ " ) = (b₁ + b₂) * ((b₁ * b₂) " )

proof end;

theorem Th56: :: COMPLFLD:56

for b₁, b₂ being Element of F_Complex st b₁ <> 0. F_Complex & b₂ <> 0. F_Complex holds
(b₁ " ) - (b₂ " ) = (b₂ - b₁) * ((b₁ * b₂) " )

proof end;

theorem Th57: :: COMPLFLD:57

canceled;

theorem Th58: :: COMPLFLD:58

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

proof end;

theorem Th59: :: COMPLFLD:59

for b₁ being Element of F_Complex holds b₁ / the unity of F_Complex = b₁

proof end;

theorem Th60: :: COMPLFLD:60

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

proof end;

theorem Th61: :: COMPLFLD:61

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

proof end;

theorem Th62: :: COMPLFLD:62

for b₁, b₂ being Element of F_Complex st b₁ <> 0. F_Complex & b₂ / b₁ = 0. F_Complex holds
b₂ = 0. F_Complex

proof end;

theorem Th63: :: COMPLFLD:63

for b₁, b₂, b₃, b₄ being Element of F_Complex st b₁ <> 0. F_Complex & b₂ <> 0. F_Complex holds
(b₃ / b₁) * (b₄ / b₂) = (b₃ * b₄) / (b₁ * b₂)

proof end;

theorem Th64: :: COMPLFLD:64

for b₁, b₂, b₃ being Element of F_Complex st b₁ <> 0. F_Complex holds
b₂ * (b₃ / b₁) = (b₂ * b₃) / b₁

proof end;

theorem Th65: :: COMPLFLD:65

for b₁, b₂ being Element of F_Complex st b₁ <> 0. F_Complex & b₂ / b₁ = the unity of F_Complex holds
b₂ = b₁

proof end;

theorem Th66: :: COMPLFLD:66

for b₁, b₂ being Element of F_Complex st b₁ <> 0. F_Complex holds
b₂ = (b₂ * b₁) / b₁

proof end;

theorem Th67: :: COMPLFLD:67

for b₁, b₂ being Element of F_Complex st b₁ <> 0. F_Complex & b₂ <> 0. F_Complex holds
(b₁ / b₂) " = b₂ / b₁

proof end;

theorem Th68: :: COMPLFLD:68

for b₁, b₂ being Element of F_Complex st b₁ <> 0. F_Complex & b₂ <> 0. F_Complex holds
(b₁ " ) / (b₂ " ) = b₂ / b₁

proof end;

theorem Th69: :: COMPLFLD:69

for b₁, b₂ being Element of F_Complex st b₁ <> 0. F_Complex holds
b₂ / (b₁ " ) = b₂ * b₁

proof end;

theorem Th70: :: COMPLFLD:70

for b₁, b₂ being Element of F_Complex st b₁ <> 0. F_Complex & b₂ <> 0. F_Complex holds
(b₁ " ) / b₂ = (b₁ * b₂) "

proof end;

theorem Th71: :: COMPLFLD:71

for b₁, b₂, b₃ being Element of F_Complex st b₁ <> 0. F_Complex & b₂ <> 0. F_Complex holds
(b₁ " ) * (b₃ / b₂) = b₃ / (b₁ * b₂)

proof end;

theorem Th72: :: COMPLFLD:72

for b₁, b₂, b₃ being Element of F_Complex st b₁ <> 0. F_Complex & b₂ <> 0. F_Complex holds
( b₃ / b₂ = (b₃ * b₁) / (b₂ * b₁) & b₃ / b₂ = (b₁ * b₃) / (b₁ * b₂) )

proof end;

theorem Th73: :: COMPLFLD:73

for b₁, b₂, b₃ being Element of F_Complex st b₁ <> 0. F_Complex & b₂ <> 0. F_Complex holds
b₃ / (b₁ * b₂) = (b₃ / b₁) / b₂

proof end;

theorem Th74: :: COMPLFLD:74

for b₁, b₂, b₃ being Element of F_Complex st b₁ <> 0. F_Complex & b₂ <> 0. F_Complex holds
(b₃ * b₂) / b₁ = b₃ / (b₁ / b₂)

proof end;

theorem Th75: :: COMPLFLD:75

for b₁, b₂, b₃, b₄ being Element of F_Complex st b₁ <> 0. F_Complex & b₂ <> 0. F_Complex & b₃ <> 0. F_Complex holds
(b₄ / b₁) / (b₂ / b₃) = (b₄ * b₃) / (b₁ * b₂)

proof end;

theorem Th76: :: COMPLFLD:76

for b₁, b₂, b₃, b₄ being Element of F_Complex st b₁ <> 0. F_Complex & b₂ <> 0. F_Complex holds
(b₃ / b₁) + (b₄ / b₂) = ((b₃ * b₂) + (b₄ * b₁)) / (b₁ * b₂)

proof end;

theorem Th77: :: COMPLFLD:77

for b₁, b₂, b₃ being Element of F_Complex st b₁ <> 0. F_Complex holds
(b₂ / b₁) + (b₃ / b₁) = (b₂ + b₃) / b₁

proof end;

theorem Th78: :: COMPLFLD:78

for b₁, b₂ being Element of F_Complex st b₁ <> 0. F_Complex holds
( - (b₂ / b₁) = (- b₂) / b₁ & - (b₂ / b₁) = b₂ / (- b₁) )

proof end;

theorem Th79: :: COMPLFLD:79

for b₁, b₂ being Element of F_Complex st b₁ <> 0. F_Complex holds
b₂ / b₁ = (- b₂) / (- b₁)

proof end;

theorem Th80: :: COMPLFLD:80

for b₁, b₂, b₃, b₄ being Element of F_Complex st b₁ <> 0. F_Complex & b₂ <> 0. F_Complex holds
(b₃ / b₁) - (b₄ / b₂) = ((b₃ * b₂) - (b₄ * b₁)) / (b₁ * b₂)

proof end;

theorem Th81: :: COMPLFLD:81

for b₁, b₂, b₃ being Element of F_Complex st b₁ <> 0. F_Complex holds
(b₂ / b₁) - (b₃ / b₁) = (b₂ - b₃) / b₁

proof end;

theorem Th82: :: COMPLFLD:82

for b₁, b₂, b₃ being Element of F_Complex st b₁ <> 0. F_Complex & ( b₂ * b₁ = b₃ or b₁ * b₂ = b₃ ) holds
b₂ = b₃ / b₁

proof end;

theorem Th83: :: COMPLFLD:83

the Zero of F_Complex *' = the Zero of F_Complex

proof end;

theorem Th84: :: COMPLFLD:84

for b₁ being Element of F_Complex st b₁ *' = the Zero of F_Complex holds
b₁ = the Zero of F_Complex

proof end;

theorem Th85: :: COMPLFLD:85

the unity of F_Complex *' = the unity of F_Complex

proof end;

theorem Th86: :: COMPLFLD:86

for b₁ being Element of F_Complex holds (b₁ *' ) *' = b₁ ;

theorem Th87: :: COMPLFLD:87

for b₁, b₂ being Element of F_Complex holds (b₁ + b₂) *' = (b₁ *' ) + (b₂ *' )

proof end;

theorem Th88: :: COMPLFLD:88

for b₁ being Element of F_Complex holds (- b₁) *' = - (b₁ *' )

proof end;

theorem Th89: :: COMPLFLD:89

for b₁, b₂ being Element of F_Complex holds (b₁ - b₂) *' = (b₁ *' ) - (b₂ *' )

proof end;

theorem Th90: :: COMPLFLD:90

for b₁, b₂ being Element of F_Complex holds (b₁ * b₂) *' = (b₁ *' ) * (b₂ *' )

proof end;

theorem Th91: :: COMPLFLD:91

for b₁ being Element of F_Complex st b₁ <> the Zero of F_Complex holds
(b₁ " ) *' = (b₁ *' ) "

proof end;

theorem Th92: :: COMPLFLD:92

for b₁, b₂ being Element of F_Complex st b₁ <> the Zero of F_Complex holds
(b₂ / b₁) *' = (b₂ *' ) / (b₁ *' )

proof end;

theorem Th93: :: COMPLFLD:93

|.the Zero of F_Complex .| = 0 by Def1, COMPLEX1:130;

theorem Th94: :: COMPLFLD:94

for b₁ being Element of F_Complex st |.b₁.| = 0 holds
b₁ = 0. F_Complex by Th9, COMPLEX1:131;

theorem Th95: :: COMPLFLD:95

canceled;

theorem Th96: :: COMPLFLD:96

for b₁ being Element of F_Complex holds
( b₁ <> 0. F_Complex iff 0 < |.b₁.| ) by Th9, COMPLEX1:133;

theorem Th97: :: COMPLFLD:97

|.the unity of F_Complex .| = 1 by Def1, COMPLEX1:134;

theorem Th98: :: COMPLFLD:98

for b₁ being Element of F_Complex holds |.(- b₁).| = |.b₁.|

proof end;

theorem Th99: :: COMPLFLD:99

canceled;

theorem Th100: :: COMPLFLD:100

for b₁, b₂ being Element of F_Complex holds |.(b₁ + b₂).| <= |.b₁.| + |.b₂.|

proof end;

theorem Th101: :: COMPLFLD:101

for b₁, b₂ being Element of F_Complex holds |.(b₁ - b₂).| <= |.b₁.| + |.b₂.|

proof end;

theorem Th102: :: COMPLFLD:102

for b₁, b₂ being Element of F_Complex holds |.b₁.| - |.b₂.| <= |.(b₁ + b₂).|

proof end;

theorem Th103: :: COMPLFLD:103

for b₁, b₂ being Element of F_Complex holds |.b₁.| - |.b₂.| <= |.(b₁ - b₂).|

proof end;

theorem Th104: :: COMPLFLD:104

for b₁, b₂ being Element of F_Complex holds |.(b₁ - b₂).| = |.(b₂ - b₁).|

proof end;

theorem Th105: :: COMPLFLD:105

for b₁, b₂ being Element of F_Complex holds
( |.(b₁ - b₂).| = 0 iff b₁ = b₂ )

proof end;

theorem Th106: :: COMPLFLD:106

for b₁, b₂ being Element of F_Complex holds
( b₁ <> b₂ iff 0 < |.(b₁ - b₂).| )

proof end;

theorem Th107: :: COMPLFLD:107

for b₁, b₂, b₃ being Element of F_Complex holds |.(b₁ - b₂).| <= |.(b₁ - b₃).| + |.(b₃ - b₂).|

proof end;

theorem Th108: :: COMPLFLD:108

for b₁, b₂ being Element of F_Complex holds abs (|.b₁.| - |.b₂.|) <= |.(b₁ - b₂).|

proof end;

theorem Th109: :: COMPLFLD:109

for b₁, b₂ being Element of F_Complex holds |.(b₁ * b₂).| = |.b₁.| * |.b₂.|

proof end;

theorem Th110: :: COMPLFLD:110

for b₁ being Element of F_Complex st b₁ <> the Zero of F_Complex holds
|.(b₁ " ).| = |.b₁.| "

proof end;

theorem Th111: :: COMPLFLD:111

for b₁, b₂ being Element of F_Complex st b₁ <> the Zero of F_Complex holds
|.b₂.| / |.b₁.| = |.(b₂ / b₁).|

proof end;