:: Trigonometric Form of Complex Numbers
:: by Robert Milewski
::
:: Received July 21, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem :: COMPTRIG:1
canceled;
theorem :: COMPTRIG:2
canceled;
theorem Th3: :: COMPTRIG:3
theorem :: COMPTRIG:4
theorem :: COMPTRIG:5
canceled;
theorem :: COMPTRIG:6
canceled;
theorem Th7: :: COMPTRIG:7
theorem :: COMPTRIG:8
canceled;
theorem :: COMPTRIG:9
canceled;
theorem :: COMPTRIG:10
canceled;
theorem :: COMPTRIG:11
canceled;
theorem :: COMPTRIG:12
canceled;
theorem :: COMPTRIG:13
canceled;
theorem :: COMPTRIG:14
canceled;
theorem :: COMPTRIG:15
canceled;
theorem :: COMPTRIG:16
canceled;
theorem Th17: :: COMPTRIG:17
theorem :: COMPTRIG:18
canceled;
theorem :: COMPTRIG:19
canceled;
theorem :: COMPTRIG:20
canceled;
PI in ].0 ,4.[
by SIN_COS:def 32;
then Lm0:
( 0 < PI & PI < 4 )
by XXREAL_1:4;
Lx2:
0 + (PI / 2) < (PI / 2) + (PI / 2)
by Lm0, XREAL_1:8;
Lx3:
0 + PI < PI + PI
by Lm0, XREAL_1:8;
Lx4:
0 + (PI / 2) < PI + (PI / 2)
by Lm0, XREAL_1:8;
Lm6:
(PI / 2) + (PI / 2) < PI + (PI / 2)
by Lx2, XREAL_1:8;
((3 / 2) * PI ) + (PI / 2) = 2 * PI
;
then Lm7:
(3 / 2) * PI < 2 * PI
by Lm6, XREAL_1:8;
Lm8:
0 < (3 / 2) * PI
by Lm0;
theorem :: COMPTRIG:21
theorem Th22: :: COMPTRIG:22
theorem Th23: :: COMPTRIG:23
theorem Th24: :: COMPTRIG:24
theorem Th25: :: COMPTRIG:25
theorem Th26: :: COMPTRIG:26
theorem Th27: :: COMPTRIG:27
theorem Th28: :: COMPTRIG:28
theorem Th29: :: COMPTRIG:29
theorem Th30: :: COMPTRIG:30
theorem Th31: :: COMPTRIG:31
theorem Th32: :: COMPTRIG:32
theorem Th33: :: COMPTRIG:33
theorem Th34: :: COMPTRIG:34
theorem Th35: :: COMPTRIG:35
theorem Th36: :: COMPTRIG:36
theorem Th37: :: COMPTRIG:37
theorem Th38: :: COMPTRIG:38
theorem :: COMPTRIG:39
theorem :: COMPTRIG:40
theorem Th41: :: COMPTRIG:41
theorem Th42: :: COMPTRIG:42
theorem :: COMPTRIG:43
canceled;
theorem :: COMPTRIG:44
canceled;
theorem Th45: :: COMPTRIG:45
theorem :: COMPTRIG:46
theorem :: COMPTRIG:47
theorem :: COMPTRIG:48
theorem :: COMPTRIG:49
theorem Th50: :: COMPTRIG:50
theorem Th51: :: COMPTRIG:51
:: deftheorem Def1 defines Arg COMPTRIG:def 1 :
theorem Th52: :: COMPTRIG:52
theorem Th53: :: COMPTRIG:53
theorem Th54: :: COMPTRIG:54
theorem Th55: :: COMPTRIG:55
theorem Th56: :: COMPTRIG:56
theorem :: COMPTRIG:57
theorem :: COMPTRIG:58
theorem Th59: :: COMPTRIG:59
theorem Th60: :: COMPTRIG:60
theorem Th61: :: COMPTRIG:61
theorem Th62: :: COMPTRIG:62
theorem Th63: :: COMPTRIG:63
theorem Th64: :: COMPTRIG:64
theorem :: COMPTRIG:65
theorem :: COMPTRIG:66
theorem Th67: :: COMPTRIG:67
theorem Th68: :: COMPTRIG:68
theorem :: COMPTRIG:69
theorem :: COMPTRIG:70
theorem Th71: :: COMPTRIG:71
theorem :: COMPTRIG:72
theorem Th73: :: COMPTRIG:73
theorem Th74: :: COMPTRIG:74
:: deftheorem Def2 defines CRoot COMPTRIG:def 2 :
theorem :: COMPTRIG:75
theorem :: COMPTRIG:76
theorem :: COMPTRIG:77
theorem :: COMPTRIG:78
theorem :: COMPTRIG:79
theorem :: COMPTRIG:80