:: The Complex Numbers
:: by Czes{\l}aw Byli\'nski
::
:: Received March 1, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem :: COMPLEX1:1
canceled;
theorem Th2: :: COMPLEX1:2
Lm2:
for a, b being Element of REAL holds 0 <= (a ^2 ) + (b ^2 )
definition
let z be
complex number ;
canceled;func Re z -> set means :
Def2:
:: COMPLEX1:def 2
it = z if z in REAL otherwise ex
f being
Function of 2,
REAL st
(
z = f &
it = f . 0 );
existence
( ( z in REAL implies ex b1 being set st b1 = z ) & ( not z in REAL implies ex b1 being set ex f being Function of 2, REAL st
( z = f & b1 = f . 0 ) ) )
uniqueness
for b1, b2 being set holds
( ( z in REAL & b1 = z & b2 = z implies b1 = b2 ) & ( not z in REAL & ex f being Function of 2, REAL st
( z = f & b1 = f . 0 ) & ex f being Function of 2, REAL st
( z = f & b2 = f . 0 ) implies b1 = b2 ) )
;
consistency
for b1 being set holds verum
;
func Im z -> set means :
Def3:
:: COMPLEX1:def 3
it = 0 if z in REAL otherwise ex
f being
Function of 2,
REAL st
(
z = f &
it = f . 1 );
existence
( ( z in REAL implies ex b1 being set st b1 = 0 ) & ( not z in REAL implies ex b1 being set ex f being Function of 2, REAL st
( z = f & b1 = f . 1 ) ) )
uniqueness
for b1, b2 being set holds
( ( z in REAL & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not z in REAL & ex f being Function of 2, REAL st
( z = f & b1 = f . 1 ) & ex f being Function of 2, REAL st
( z = f & b2 = f . 1 ) implies b1 = b2 ) )
;
consistency
for b1 being set holds verum
;
end;
:: deftheorem COMPLEX1:def 1 :
canceled;
:: deftheorem Def2 defines Re COMPLEX1:def 2 :
:: deftheorem Def3 defines Im COMPLEX1:def 3 :
theorem :: COMPLEX1:3
canceled;
theorem :: COMPLEX1:4
canceled;
theorem Th5: :: COMPLEX1:5
Lm3:
for a, b being Element of REAL holds
( Re [*a,b*] = a & Im [*a,b*] = b )
Lm4:
for z being complex number holds [*(Re z),(Im z)*] = z
theorem :: COMPLEX1:6
canceled;
theorem :: COMPLEX1:7
canceled;
theorem :: COMPLEX1:8
canceled;
theorem Th9: :: COMPLEX1:9
:: deftheorem COMPLEX1:def 4 :
canceled;
:: deftheorem defines = COMPLEX1:def 5 :
:: deftheorem COMPLEX1:def 6 :
canceled;
:: deftheorem defines 1r COMPLEX1:def 7 :
Lm5:
0 = [*0 ,0 *]
by ARYTM_0:def 7;
Lm6:
1r = [*1,0 *]
by ARYTM_0:def 7;
theorem :: COMPLEX1:10
canceled;
theorem :: COMPLEX1:11
canceled;
theorem Th12: :: COMPLEX1:12
theorem Th13: :: COMPLEX1:13
theorem :: COMPLEX1:14
canceled;
theorem Th15: :: COMPLEX1:15
theorem :: COMPLEX1:16
canceled;
Lmx:
<i> = [*0 ,1*]
by ARYTM_0:def 7, XCMPLX_0:def 1;
theorem Th17: :: COMPLEX1:17
Lm7:
for x being real number
for x1, x2 being Element of REAL st x = [*x1,x2*] holds
( x2 = 0 & x = x1 )
Lm8:
for x', y' being Element of REAL
for x, y being real number st x' = x & y' = y holds
+ x',y' = x + y
Lm9:
for x being Element of REAL holds opp x = - x
Lm10:
for x', y' being Element of REAL
for x, y being real number st x' = x & y' = y holds
* x',y' = x * y
Lm11:
for x, y, z being complex number st z = x + y holds
Re z = (Re x) + (Re y)
Lm12:
for x, y, z being complex number st z = x + y holds
Im z = (Im x) + (Im y)
Lm13:
for x, y, z being complex number st z = x * y holds
Re z = ((Re x) * (Re y)) - ((Im x) * (Im y))
Lm14:
for x, y, z being complex number st z = x * y holds
Im z = ((Re x) * (Im y)) + ((Im x) * (Re y))
Lm15:
for z1, z2 being Element of COMPLEX holds z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*]
Lm16:
for z1, z2 being Element of COMPLEX holds z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*]
Lm17:
for z1, z2 being complex number holds
( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) )
Lm18:
for z1, z2 being complex number holds
( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) )
Lm19:
for x being Real holds Re (x * <i> ) = 0
Lm20:
for x being Real holds Im (x * <i> ) = x
Lm21:
for x, y being Real holds [*x,y*] = x + (y * <i> )
:: deftheorem COMPLEX1:def 8 :
canceled;
:: deftheorem defines + COMPLEX1:def 9 :
theorem :: COMPLEX1:18
canceled;
theorem Th19: :: COMPLEX1:19
:: deftheorem defines * COMPLEX1:def 10 :
theorem :: COMPLEX1:20
canceled;
theorem :: COMPLEX1:21
canceled;
theorem :: COMPLEX1:22
canceled;
theorem :: COMPLEX1:23
canceled;
theorem Th24: :: COMPLEX1:24
theorem Th25: :: COMPLEX1:25
theorem Th26: :: COMPLEX1:26
theorem :: COMPLEX1:27
canceled;
theorem Th28: :: COMPLEX1:28
theorem Th29: :: COMPLEX1:29
theorem Th30: :: COMPLEX1:30
theorem Th31: :: COMPLEX1:31
theorem :: COMPLEX1:32
:: deftheorem Def11 defines - COMPLEX1:def 11 :
theorem :: COMPLEX1:33
canceled;
theorem Th34: :: COMPLEX1:34
theorem :: COMPLEX1:35
canceled;
theorem :: COMPLEX1:36
canceled;
theorem :: COMPLEX1:37
:: deftheorem Def12 defines - COMPLEX1:def 12 :
theorem :: COMPLEX1:38
canceled;
theorem :: COMPLEX1:39
canceled;
theorem :: COMPLEX1:40
canceled;
theorem :: COMPLEX1:41
canceled;
theorem :: COMPLEX1:42
canceled;
theorem :: COMPLEX1:43
canceled;
theorem :: COMPLEX1:44
canceled;
theorem :: COMPLEX1:45
canceled;
theorem :: COMPLEX1:46
canceled;
theorem :: COMPLEX1:47
canceled;
theorem Th48: :: COMPLEX1:48
:: deftheorem Def13 defines " COMPLEX1:def 13 :
theorem :: COMPLEX1:49
canceled;
theorem :: COMPLEX1:50
canceled;
theorem :: COMPLEX1:51
canceled;
theorem :: COMPLEX1:52
canceled;
theorem :: COMPLEX1:53
canceled;
theorem :: COMPLEX1:54
canceled;
theorem :: COMPLEX1:55
canceled;
theorem :: COMPLEX1:56
canceled;
theorem :: COMPLEX1:57
canceled;
theorem :: COMPLEX1:58
canceled;
theorem :: COMPLEX1:59
canceled;
theorem :: COMPLEX1:60
canceled;
theorem :: COMPLEX1:61
canceled;
theorem :: COMPLEX1:62
canceled;
theorem :: COMPLEX1:63
canceled;
theorem Th64: :: COMPLEX1:64
theorem :: COMPLEX1:65
canceled;
theorem :: COMPLEX1:66
canceled;
theorem :: COMPLEX1:67
canceled;
theorem :: COMPLEX1:68
canceled;
theorem :: COMPLEX1:69
canceled;
theorem :: COMPLEX1:70
canceled;
theorem :: COMPLEX1:71
canceled;
theorem :: COMPLEX1:72
theorem :: COMPLEX1:73
canceled;
theorem :: COMPLEX1:74
canceled;
theorem :: COMPLEX1:75
canceled;
theorem :: COMPLEX1:76
canceled;
theorem :: COMPLEX1:77
canceled;
theorem :: COMPLEX1:78
canceled;
theorem Th79: :: COMPLEX1:79
theorem Th80: :: COMPLEX1:80
:: deftheorem Def14 defines / COMPLEX1:def 14 :
theorem :: COMPLEX1:81
canceled;
theorem :: COMPLEX1:82
theorem :: COMPLEX1:83
canceled;
theorem :: COMPLEX1:84
canceled;
theorem :: COMPLEX1:85
canceled;
theorem :: COMPLEX1:86
canceled;
theorem :: COMPLEX1:87
canceled;
theorem :: COMPLEX1:88
canceled;
theorem :: COMPLEX1:89
canceled;
theorem :: COMPLEX1:90
canceled;
theorem :: COMPLEX1:91
canceled;
theorem :: COMPLEX1:92
canceled;
theorem :: COMPLEX1:93
canceled;
theorem :: COMPLEX1:94
canceled;
theorem :: COMPLEX1:95
canceled;
theorem :: COMPLEX1:96
canceled;
theorem :: COMPLEX1:97
canceled;
theorem :: COMPLEX1:98
canceled;
theorem :: COMPLEX1:99
canceled;
theorem :: COMPLEX1:100
canceled;
theorem :: COMPLEX1:101
canceled;
theorem :: COMPLEX1:102
canceled;
theorem :: COMPLEX1:103
canceled;
theorem :: COMPLEX1:104
canceled;
theorem :: COMPLEX1:105
canceled;
theorem :: COMPLEX1:106
canceled;
theorem :: COMPLEX1:107
canceled;
theorem :: COMPLEX1:108
canceled;
theorem :: COMPLEX1:109
theorem :: COMPLEX1:110
:: deftheorem defines *' COMPLEX1:def 15 :
theorem :: COMPLEX1:111
canceled;
theorem Th112: :: COMPLEX1:112
theorem :: COMPLEX1:113
theorem :: COMPLEX1:114
theorem :: COMPLEX1:115
theorem :: COMPLEX1:116
theorem :: COMPLEX1:117
canceled;
theorem Th118: :: COMPLEX1:118
theorem Th119: :: COMPLEX1:119
theorem :: COMPLEX1:120
theorem Th121: :: COMPLEX1:121
theorem Th122: :: COMPLEX1:122
theorem :: COMPLEX1:123
theorem :: COMPLEX1:124
theorem :: COMPLEX1:125
theorem :: COMPLEX1:126
theorem :: COMPLEX1:127
theorem :: COMPLEX1:128
:: deftheorem defines |. COMPLEX1:def 16 :
theorem Th129: :: COMPLEX1:129
theorem :: COMPLEX1:130
theorem Th131: :: COMPLEX1:131
theorem Th132: :: COMPLEX1:132
theorem :: COMPLEX1:133
theorem Th134: :: COMPLEX1:134
theorem :: COMPLEX1:135
Lm22:
for z being complex number holds |.(- z).| = |.z.|
Lm23:
for a being real number st a <= 0 holds
|.a.| = - a
Lm24:
for a being real number holds sqrt (a ^2 ) = |.a.|
theorem :: COMPLEX1:136
theorem :: COMPLEX1:137
theorem :: COMPLEX1:138
theorem Th139: :: COMPLEX1:139
Lm25:
for x being real number holds
( - |.x.| <= x & x <= |.x.| )
theorem :: COMPLEX1:140
theorem :: COMPLEX1:141
theorem Th142: :: COMPLEX1:142
theorem Th143: :: COMPLEX1:143
theorem :: COMPLEX1:144
theorem Th145: :: COMPLEX1:145
theorem Th146: :: COMPLEX1:146
theorem Th147: :: COMPLEX1:147
theorem :: COMPLEX1:148
theorem :: COMPLEX1:149
Lm26:
for x, y being real number holds
( ( - y <= x & x <= y ) iff |.x.| <= y )
theorem :: COMPLEX1:150
theorem Th151: :: COMPLEX1:151
theorem Th152: :: COMPLEX1:152
theorem Th153: :: COMPLEX1:153
theorem :: COMPLEX1:154
theorem :: COMPLEX1:155
theorem :: COMPLEX1:156
theorem Th157: :: COMPLEX1:157
theorem :: COMPLEX1:158
theorem :: COMPLEX1:159
theorem :: COMPLEX1:160
theorem Th161: :: COMPLEX1:161
theorem :: COMPLEX1:162
theorem :: COMPLEX1:163
theorem :: COMPLEX1:164
theorem :: COMPLEX1:165
theorem :: COMPLEX1:166