:: Property of Complex Functions
:: by Takashi Mitsuishi , Katsumi Wasaki and Yasunari Shidama
::
:: Copyright (c) 1999-2012 Association of Mizar Users

begin

::
::DEFINITIONS OF COMPLEX FUNCTIONS
::
definition end;

definition
let C be non empty set ;
let f1, f2 be PartFunc of C,COMPLEX;
deffunc H1( set ) -> Element of COMPLEX = (f1 /. $1) * ((f2 /.$1) ");
func f1 / f2 -> PartFunc of C,COMPLEX means :Def1: :: CFUNCT_1:def 1
( dom it = (dom f1) /\ ((dom f2) \ (f2 " )) & ( for c being Element of C st c in dom it holds
it /. c = (f1 /. c) * ((f2 /. c) ") ) );
existence
ex b1 being PartFunc of C,COMPLEX st
( dom b1 = (dom f1) /\ ((dom f2) \ (f2 " )) & ( for c being Element of C st c in dom b1 holds
b1 /. c = (f1 /. c) * ((f2 /. c) ") ) )
proof end;
uniqueness
for b1, b2 being PartFunc of C,COMPLEX st dom b1 = (dom f1) /\ ((dom f2) \ (f2 " )) & ( for c being Element of C st c in dom b1 holds
b1 /. c = (f1 /. c) * ((f2 /. c) ") ) & dom b2 = (dom f1) /\ ((dom f2) \ (f2 " )) & ( for c being Element of C st c in dom b2 holds
b2 /. c = (f1 /. c) * ((f2 /. c) ") ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines / CFUNCT_1:def 1 :
for C being non empty set
for f1, f2, b4 being PartFunc of C,COMPLEX holds
( b4 = f1 / f2 iff ( dom b4 = (dom f1) /\ ((dom f2) \ (f2 " )) & ( for c being Element of C st c in dom b4 holds
b4 /. c = (f1 /. c) * ((f2 /. c) ") ) ) );

definition
let C be non empty set ;
let f be PartFunc of C,COMPLEX;
deffunc H1( set ) -> Element of COMPLEX = (f /. \$1) " ;
func f ^ -> PartFunc of C,COMPLEX means :Def2: :: CFUNCT_1:def 2
( dom it = (dom f) \ (f " ) & ( for c being Element of C st c in dom it holds
it /. c = (f /. c) " ) );
existence
ex b1 being PartFunc of C,COMPLEX st
( dom b1 = (dom f) \ (f " ) & ( for c being Element of C st c in dom b1 holds
b1 /. c = (f /. c) " ) )
proof end;
uniqueness
for b1, b2 being PartFunc of C,COMPLEX st dom b1 = (dom f) \ (f " ) & ( for c being Element of C st c in dom b1 holds
b1 /. c = (f /. c) " ) & dom b2 = (dom f) \ (f " ) & ( for c being Element of C st c in dom b2 holds
b2 /. c = (f /. c) " ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines ^ CFUNCT_1:def 2 :
for C being non empty set
for f, b3 being PartFunc of C,COMPLEX holds
( b3 = f ^ iff ( dom b3 = (dom f) \ (f " ) & ( for c being Element of C st c in dom b3 holds
b3 /. c = (f /. c) " ) ) );

theorem Th1: :: CFUNCT_1:1
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( dom (f1 + f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 + f2) holds
(f1 + f2) /. c = (f1 /. c) + (f2 /. c) ) )
proof end;

theorem Th2: :: CFUNCT_1:2
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( dom (f1 - f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 - f2) holds
(f1 - f2) /. c = (f1 /. c) - (f2 /. c) ) )
proof end;

theorem Th3: :: CFUNCT_1:3
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 (#) f2) holds
(f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) ) )
proof end;

theorem Th4: :: CFUNCT_1:4
for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds
( dom (r (#) f) = dom f & ( for c being Element of C st c in dom (r (#) f) holds
(r (#) f) /. c = r * (f /. c) ) )
proof end;

theorem Th5: :: CFUNCT_1:5
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( dom (- f) = dom f & ( for c being Element of C st c in dom (- f) holds
(- f) /. c = - (f /. c) ) )
proof end;

Lm1: for x, Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( x in f " Y iff ( x in dom f & f /. x in Y ) )

by PARTFUN2:26;

theorem Th6: :: CFUNCT_1:6
for C being non empty set
for g being PartFunc of C,COMPLEX holds
( dom (g ^) c= dom g & (dom g) /\ ((dom g) \ (g " )) = (dom g) \ (g " ) )
proof end;

theorem Th7: :: CFUNCT_1:7
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " ) = ((dom f1) \ (f1 " )) /\ ((dom f2) \ (f2 " ))
proof end;

theorem Th8: :: CFUNCT_1:8
for C being non empty set
for c being Element of C
for f being PartFunc of C,COMPLEX st c in dom (f ^) holds
f /. c <> 0
proof end;

theorem Th9: :: CFUNCT_1:9
for C being non empty set
for f being PartFunc of C,COMPLEX holds (f ^) " = {}
proof end;

theorem Th10: :: CFUNCT_1:10
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( |.f.| " = f " & (- f) " = f " )
proof end;

theorem Th11: :: CFUNCT_1:11
for C being non empty set
for f being PartFunc of C,COMPLEX holds dom ((f ^) ^) = dom (f | (dom (f ^)))
proof end;

theorem Th12: :: CFUNCT_1:12
for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX st r <> 0 holds
(r (#) f) " = f "
proof end;

begin

::
:: BASIC PROPERTIES OF OPERATIONS
::
theorem :: CFUNCT_1:13
for C being non empty set
for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 + f2) + f3 = f1 + (f2 + f3)
proof end;

theorem Th14: :: CFUNCT_1:14
for C being non empty set
for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
proof end;

theorem Th15: :: CFUNCT_1:15
for C being non empty set
for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
proof end;

theorem :: CFUNCT_1:16
for C being non empty set
for f3, f1, f2 being PartFunc of C,COMPLEX holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2) by Th15;

theorem Th17: :: CFUNCT_1:17
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2
proof end;

theorem Th18: :: CFUNCT_1:18
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
proof end;

theorem Th19: :: CFUNCT_1:19
for C being non empty set
for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
proof end;

theorem :: CFUNCT_1:20
for C being non empty set
for f3, f1, f2 being PartFunc of C,COMPLEX holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2) by Th19;

theorem :: CFUNCT_1:21
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)
proof end;

theorem :: CFUNCT_1:22
for C being non empty set
for f being PartFunc of C,COMPLEX
for r, q being Element of COMPLEX holds (r * q) (#) f = r (#) (q (#) f)
proof end;

theorem :: CFUNCT_1:23
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)
proof end;

theorem :: CFUNCT_1:24
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds f1 - f2 = () (#) (f2 - f1)
proof end;

theorem :: CFUNCT_1:25
for C being non empty set
for f1, f2, f3 being PartFunc of C,COMPLEX holds f1 - (f2 + f3) = (f1 - f2) - f3
proof end;

theorem :: CFUNCT_1:26
for C being non empty set
for f being PartFunc of C,COMPLEX holds 1r (#) f = f
proof end;

theorem :: CFUNCT_1:27
for C being non empty set
for f1, f2, f3 being PartFunc of C,COMPLEX holds f1 - (f2 - f3) = (f1 - f2) + f3
proof end;

theorem :: CFUNCT_1:28
for C being non empty set
for f1, f2, f3 being PartFunc of C,COMPLEX holds f1 + (f2 - f3) = (f1 + f2) - f3
proof end;

theorem Th29: :: CFUNCT_1:29
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds |.(f1 (#) f2).| = |.f1.| (#) |.f2.|
proof end;

theorem Th30: :: CFUNCT_1:30
for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds |.(r (#) f).| = |.r.| (#) |.f.|
proof end;

theorem :: CFUNCT_1:31
for C being non empty set
for f being PartFunc of C,COMPLEX holds - f = () (#) f by COMPLEX1:def 4;

theorem :: CFUNCT_1:32
canceled;

theorem :: CFUNCT_1:33
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds f1 - (- f2) = f1 + f2 ;

theorem Th34: :: CFUNCT_1:34
for C being non empty set
for f being PartFunc of C,COMPLEX holds (f ^) ^ = f | (dom (f ^))
proof end;

theorem Th35: :: CFUNCT_1:35
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^)
proof end;

theorem Th36: :: CFUNCT_1:36
for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX st r <> 0 holds
(r (#) f) ^ = (r ") (#) (f ^)
proof end;

Lm2: () " = - 1r
by COMPLEX1:def 4;

theorem :: CFUNCT_1:37
for C being non empty set
for f being PartFunc of C,COMPLEX holds (- f) ^ = () (#) (f ^) by ;

theorem Th38: :: CFUNCT_1:38
for C being non empty set
for f being PartFunc of C,COMPLEX holds |.f.| ^ = |.(f ^).|
proof end;

theorem Th39: :: CFUNCT_1:39
for C being non empty set
for f, g being PartFunc of C,COMPLEX holds f / g = f (#) (g ^)
proof end;

theorem Th40: :: CFUNCT_1:40
for C being non empty set
for g, f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds r (#) (g / f) = (r (#) g) / f
proof end;

theorem :: CFUNCT_1:41
for C being non empty set
for f, g being PartFunc of C,COMPLEX holds (f / g) (#) g = f | (dom (g ^))
proof end;

theorem Th42: :: CFUNCT_1:42
for C being non empty set
for f, g, f1, g1 being PartFunc of C,COMPLEX holds (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1)
proof end;

theorem Th43: :: CFUNCT_1:43
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds (f1 / f2) ^ = (f2 | (dom (f2 ^))) / f1
proof end;

theorem Th44: :: CFUNCT_1:44
for C being non empty set
for g, f1, f2 being PartFunc of C,COMPLEX holds g (#) (f1 / f2) = (g (#) f1) / f2
proof end;

theorem :: CFUNCT_1:45
for C being non empty set
for g, f1, f2 being PartFunc of C,COMPLEX holds g / (f1 / f2) = (g (#) (f2 | (dom (f2 ^)))) / f1
proof end;

theorem :: CFUNCT_1:46
for C being non empty set
for f, g being PartFunc of C,COMPLEX holds
( - (f / g) = (- f) / g & f / (- g) = - (f / g) )
proof end;

theorem :: CFUNCT_1:47
for C being non empty set
for f1, f, f2 being PartFunc of C,COMPLEX holds
( (f1 / f) + (f2 / f) = (f1 + f2) / f & (f1 / f) - (f2 / f) = (f1 - f2) / f )
proof end;

theorem Th48: :: CFUNCT_1:48
for C being non empty set
for f1, f, g1, g being PartFunc of C,COMPLEX holds (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)
proof end;

theorem :: CFUNCT_1:49
for C being non empty set
for f, g, f1, g1 being PartFunc of C,COMPLEX holds (f / g) / (f1 / g1) = (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1)
proof end;

theorem :: CFUNCT_1:50
for C being non empty set
for f1, f, g1, g being PartFunc of C,COMPLEX holds (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g)
proof end;

theorem :: CFUNCT_1:51
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds |.(f1 / f2).| = |.f1.| / |.f2.|
proof end;

theorem Th52: :: CFUNCT_1:52
for X being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
proof end;

theorem Th53: :: CFUNCT_1:53
for X being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
proof end;

theorem Th54: :: CFUNCT_1:54
for X being set
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( (- f) | X = - (f | X) & (f ^) | X = (f | X) ^ & |.f.| | X = |.(f | X).| )
proof end;

theorem :: CFUNCT_1:55
for X being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
proof end;

theorem :: CFUNCT_1:56
for X being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( (f1 / f2) | X = (f1 | X) / (f2 | X) & (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) )
proof end;

theorem :: CFUNCT_1:57
for X being set
for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds (r (#) f) | X = r (#) (f | X)
proof end;

begin

::
:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN, TO COMPLEX
::
theorem Th58: :: CFUNCT_1:58
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 (#) f2 is total ) & ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) )
proof end;

theorem Th59: :: CFUNCT_1:59
for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds
( f is total iff r (#) f is total )
proof end;

theorem Th60: :: CFUNCT_1:60
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( f is total iff - f is total )
proof end;

theorem Th61: :: CFUNCT_1:61
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( f is total iff |.f.| is total )
proof end;

theorem Th62: :: CFUNCT_1:62
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( f ^ is total iff ( f " = {} & f is total ) )
proof end;

theorem Th63: :: CFUNCT_1:63
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( ( f1 is total & f2 " = {} & f2 is total ) iff f1 / f2 is total )
proof end;

theorem :: CFUNCT_1:64
for C being non empty set
for c being Element of C
for f1, f2 being PartFunc of C,COMPLEX st f1 is total & f2 is total holds
( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) & (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) )
proof end;

theorem :: CFUNCT_1:65
for C being non empty set
for c being Element of C
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX st f is total holds
(r (#) f) /. c = r * (f /. c)
proof end;

theorem :: CFUNCT_1:66
for C being non empty set
for c being Element of C
for f being PartFunc of C,COMPLEX st f is total holds
( (- f) /. c = - (f /. c) & |.f.| . c = |.(f /. c).| )
proof end;

theorem :: CFUNCT_1:67
for C being non empty set
for c being Element of C
for f being PartFunc of C,COMPLEX st f ^ is total holds
(f ^) /. c = (f /. c) "
proof end;

theorem :: CFUNCT_1:68
for C being non empty set
for c being Element of C
for f1, f2 being PartFunc of C,COMPLEX st f1 is total & f2 ^ is total holds
(f1 / f2) /. c = (f1 /. c) * ((f2 /. c) ")
proof end;

begin

Lm3: for C being non empty set
for f being PartFunc of C,COMPLEX holds
( |.f.| is bounded iff f is bounded )

proof end;

theorem Th69: :: CFUNCT_1:69
for Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( f | Y is bounded iff ex p being real number st
for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p )
proof end;

theorem :: CFUNCT_1:70
for Y, X being set
for C being non empty set
for f being PartFunc of C,COMPLEX st Y c= X & f | X is bounded holds
f | Y is bounded
proof end;

theorem :: CFUNCT_1:71
for X being set
for C being non empty set
for f being PartFunc of C,COMPLEX st X misses dom f holds
f | X is bounded
proof end;

theorem Th72: :: CFUNCT_1:72
for Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX st f | Y is bounded holds
(r (#) f) | Y is bounded
proof end;

theorem :: CFUNCT_1:73
for X being set
for C being non empty set
for f being PartFunc of C,COMPLEX holds |.f.| | X is bounded_below
proof end;

theorem Th74: :: CFUNCT_1:74
for Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX st f | Y is bounded holds
( |.f.| | Y is bounded & (- f) | Y is bounded )
proof end;

theorem Th75: :: CFUNCT_1:75
for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is bounded holds
(f1 + f2) | (X /\ Y) is bounded
proof end;

theorem Th76: :: CFUNCT_1:76
for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is bounded holds
( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
proof end;

theorem :: CFUNCT_1:77
for X, Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX st f | X is bounded & f | Y is bounded holds
f | (X \/ Y) is bounded
proof end;

theorem :: CFUNCT_1:78
for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX st f1 | X is constant & f2 | Y is constant holds
( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )
proof end;

theorem Th79: :: CFUNCT_1:79
for Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX
for q being Element of COMPLEX st f | Y is constant holds
(q (#) f) | Y is constant
proof end;

theorem Th80: :: CFUNCT_1:80
for Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX st f | Y is constant holds
( |.f.| | Y is constant & (- f) | Y is constant )
proof end;

theorem Th81: :: CFUNCT_1:81
for Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX st f | Y is constant holds
f | Y is bounded
proof end;

theorem :: CFUNCT_1:82
for Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX st f | Y is constant holds
( ( for r being Element of COMPLEX holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & |.f.| | Y is bounded )
proof end;

theorem Th83: :: CFUNCT_1:83
for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is constant holds
(f1 + f2) | (X /\ Y) is bounded
proof end;

theorem :: CFUNCT_1:84
for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is constant holds
( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded )
proof end;

theorem :: CFUNCT_1:85
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( |.f.| is bounded iff f is bounded ) by Lm3;