:: Inner Products and Angles of Complex Numbers
:: by Wenpai Chang, Yatsuka Nakamura and Piotr Rudnicki
::
:: Received May 29, 2003
:: Copyright (c) 2003 Association of Mizar Users
theorem :: COMPLEX2:1
canceled;
theorem Th2: :: COMPLEX2:2
theorem Th3: :: COMPLEX2:3
theorem Th4: :: COMPLEX2:4
theorem :: COMPLEX2:5
theorem Th6: :: COMPLEX2:6
theorem Th7: :: COMPLEX2:7
theorem Th8: :: COMPLEX2:8
theorem Th9: :: COMPLEX2:9
theorem Th10: :: COMPLEX2:10
theorem Th11: :: COMPLEX2:11
theorem Th12: :: COMPLEX2:12
theorem :: COMPLEX2:13
canceled;
theorem :: COMPLEX2:14
canceled;
theorem :: COMPLEX2:15
canceled;
theorem :: COMPLEX2:16
canceled;
theorem :: COMPLEX2:17
canceled;
theorem :: COMPLEX2:18
canceled;
theorem Th19: :: COMPLEX2:19
Lm2:
Arg 0 = 0
by COMPTRIG:53;
theorem :: COMPLEX2:20
canceled;
theorem :: COMPLEX2:21
canceled;
theorem Th22: :: COMPLEX2:22
theorem Th23: :: COMPLEX2:23
theorem Th24: :: COMPLEX2:24
theorem Th25: :: COMPLEX2:25
theorem Th26: :: COMPLEX2:26
theorem Th27: :: COMPLEX2:27
theorem :: COMPLEX2:28
theorem :: COMPLEX2:29
theorem :: COMPLEX2:30
canceled;
theorem :: COMPLEX2:31
canceled;
theorem :: COMPLEX2:32
canceled;
theorem :: COMPLEX2:33
canceled;
theorem Th34: :: COMPLEX2:34
theorem Th35: :: COMPLEX2:35
theorem Th36: :: COMPLEX2:36
theorem Th37: :: COMPLEX2:37
theorem Th38: :: COMPLEX2:38
theorem Th39: :: COMPLEX2:39
theorem Th40: :: COMPLEX2:40
theorem Th41: :: COMPLEX2:41
:: deftheorem COMPLEX2:def 1 :
canceled;
:: deftheorem COMPLEX2:def 2 :
canceled;
:: deftheorem defines .|. COMPLEX2:def 3 :
theorem Th42: :: COMPLEX2:42
theorem Th43: :: COMPLEX2:43
theorem Th44: :: COMPLEX2:44
theorem Th45: :: COMPLEX2:45
theorem :: COMPLEX2:46
theorem Th47: :: COMPLEX2:47
theorem :: COMPLEX2:48
theorem Th49: :: COMPLEX2:49
theorem :: COMPLEX2:50
theorem Th51: :: COMPLEX2:51
theorem :: COMPLEX2:52
theorem :: COMPLEX2:53
theorem :: COMPLEX2:54
theorem Th55: :: COMPLEX2:55
theorem :: COMPLEX2:56
theorem Th57: :: COMPLEX2:57
theorem :: COMPLEX2:58
theorem :: COMPLEX2:59
theorem Th60: :: COMPLEX2:60
theorem :: COMPLEX2:61
canceled;
theorem :: COMPLEX2:62
theorem Th63: :: COMPLEX2:63
Lm3:
for z being Element of COMPLEX holds |.z.| ^2 = ((Re z) ^2 ) + ((Im z) ^2 )
theorem Th64: :: COMPLEX2:64
:: deftheorem defines Rotate COMPLEX2:def 4 :
theorem :: COMPLEX2:65
theorem Th66: :: COMPLEX2:66
theorem Th67: :: COMPLEX2:67
theorem Th68: :: COMPLEX2:68
theorem :: COMPLEX2:69
theorem Th70: :: COMPLEX2:70
theorem Th71: :: COMPLEX2:71
theorem Th72: :: COMPLEX2:72
theorem Th73: :: COMPLEX2:73
theorem Th74: :: COMPLEX2:74
:: deftheorem Def5 defines angle COMPLEX2:def 5 :
theorem Th75: :: COMPLEX2:75
theorem Th76: :: COMPLEX2:76
theorem Th77: :: COMPLEX2:77
theorem Th78: :: COMPLEX2:78
theorem Th79: :: COMPLEX2:79
theorem :: COMPLEX2:80
theorem :: COMPLEX2:81
theorem :: COMPLEX2:82
theorem Th83: :: COMPLEX2:83
:: deftheorem Def6 defines angle COMPLEX2:def 6 :
theorem Th84: :: COMPLEX2:84
theorem Th85: :: COMPLEX2:85
theorem Th86: :: COMPLEX2:86
theorem Th87: :: COMPLEX2:87
theorem Th88: :: COMPLEX2:88
theorem Th89: :: COMPLEX2:89
theorem :: COMPLEX2:90
Lm4:
for a, b, c being Element of COMPLEX st a <> b & c <> b holds
( Re ((a - b) .|. (c - b)) = 0 iff ( angle a,b,c = PI / 2 or angle a,b,c = (3 / 2) * PI ) )
theorem :: COMPLEX2:91
theorem Th92: :: COMPLEX2:92
theorem Th93: :: COMPLEX2:93
Lm5:
for x, y, z being Element of COMPLEX st angle x,y,z <> 0 holds
angle z,y,x = (2 * PI ) - (angle x,y,z)
theorem Th94: :: COMPLEX2:94
theorem :: COMPLEX2:95
theorem :: COMPLEX2:96
theorem Th97: :: COMPLEX2:97
Lm6:
for a, b being Element of COMPLEX st Im a = 0 & Re a > 0 & 0 < Arg b & Arg b < PI holds
( ((angle a,0c ,b) + (angle 0c ,b,a)) + (angle b,a,0c ) = PI & 0 < angle 0c ,b,a & 0 < angle b,a,0c )
theorem Th98: :: COMPLEX2:98
for
a,
b,
c being
Element of
COMPLEX st
a <> b &
b <> c &
0 < angle a,
b,
c &
angle a,
b,
c < PI holds
(
((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI &
0 < angle b,
c,
a &
0 < angle c,
a,
b )
theorem Th99: :: COMPLEX2:99
for
a,
b,
c being
Element of
COMPLEX st
a <> b &
b <> c &
angle a,
b,
c > PI holds
(
((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5
* PI &
angle b,
c,
a > PI &
angle c,
a,
b > PI )
Lm7:
for a, b being Element of COMPLEX st Im a = 0 & Re a > 0 & Arg b = PI holds
( ((angle a,0 ,b) + (angle 0 ,b,a)) + (angle b,a,0 ) = PI & 0 = angle 0 ,b,a & 0 = angle b,a,0 )
theorem Th100: :: COMPLEX2:100
theorem Th101: :: COMPLEX2:101
for
a,
b,
c being
Element of
COMPLEX st
a <> b &
a <> c &
b <> c &
angle a,
b,
c = 0 & not (
angle b,
c,
a = 0 &
angle c,
a,
b = PI ) holds
(
angle b,
c,
a = PI &
angle c,
a,
b = 0 )
theorem :: COMPLEX2:102
for
a,
b,
c being
Element of
COMPLEX holds
( (
((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI or
((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5
* PI ) iff (
a <> b &
a <> c &
b <> c ) )