Journal of Formalized Mathematics
EMM, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

### Complex Numbers --- Basic Theorems

by
Library Committee

MML identifier: XCMPLX_1
[ Mizar article, MML identifier index ]

```environ

vocabulary ARYTM, ARYTM_1, RELAT_1, ARYTM_3, XCMPLX_0, COMPLEX1, OPPCAT_1;
notation SUBSET_1, ORDINAL1, NUMBERS, ARYTM_0, XCMPLX_0;
constructors ARYTM_0, XREAL_0, XCMPLX_0, ARYTM_3, XBOOLE_0;
clusters NUMBERS, XREAL_0, XCMPLX_0, ARYTM_3, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE, NUMERALS, ARITHM;

begin

reserve a, b, c, d, e for complex number;

:: '+' operation only

theorem :: XCMPLX_1:1  :: AXIOMS'13
a + (b + c) = (a + b) + c;

theorem :: XCMPLX_1:2  :: REAL_1'10
a + c = b + c implies a = b;

theorem :: XCMPLX_1:3  :: INT_1'24
a = a + b implies b = 0;

theorem :: XCMPLX_1:4  :: AXIOMS'16
a * (b * c) = (a * b) * c;

theorem :: XCMPLX_1:5  :: REAL_1'9
c <> 0 & a * c = b * c implies a = b;

theorem :: XCMPLX_1:6  :: REAL_1'23  :: right to left - requirements REAL
a*b=0 implies a=0 or b=0;

theorem :: XCMPLX_1:7  :: REAL_2'37
b <> 0 & a * b = b implies a = 1;

:: operations '+' and '*' only

theorem :: XCMPLX_1:8  :: AXIOMS'18
a * (b + c) = a * b + a * c;

theorem :: XCMPLX_1:9  :: REAL_2'99_1
(a + b + c) * d = a * d + b * d + c * d;

theorem :: XCMPLX_1:10  :: REAL_2'101_1
(a + b) * (c + d) = a * c + a * d + b * c + b * d;

theorem :: XCMPLX_1:11  :: SQUARE_1'5
2 * a = a + a;

theorem :: XCMPLX_1:12  :: REAL_2'88_1
3 * a = a + a + a;

theorem :: XCMPLX_1:13  :: REAL_2'88_2
4 * a = a + a + a + a;

:: using operation '-'

theorem :: XCMPLX_1:14  :: REAL_1'36
a - a = 0;

theorem :: XCMPLX_1:15  :: SQUARE_1'8
a - b = 0 implies a = b;

theorem :: XCMPLX_1:16  :: REAL_2'1
b - a = b implies a = 0;

:: 2 times '-'

theorem :: XCMPLX_1:17  :: REAL_2'17_2
a = a - (b - b);

theorem :: XCMPLX_1:18  :: SEQ_4'3
a - (a - b) = b;

theorem :: XCMPLX_1:19  :: REAL_2'2_3
a - c = b - c implies a = b;

theorem :: XCMPLX_1:20  :: REAL_2'2_5
c - a = c - b implies a = b;

theorem :: XCMPLX_1:21  :: REAL_2'24_1
a - b - c = a - c - b;

theorem :: XCMPLX_1:22   :: REAL_2'29_1
a - c = (a - b) - (c - b);

theorem :: XCMPLX_1:23  :: JGRAPH_6'1_1
(c - a) - (c - b) = b - a;

theorem :: XCMPLX_1:24  :: REAL_2'15
a - b = c - d implies a - c = b - d;

:: using operations '-' and '+'

theorem :: XCMPLX_1:25   :: REAL_2'17_1
a = a + (b - b);

theorem :: XCMPLX_1:26  :: REAL_1'30
a = a + b - b;

theorem :: XCMPLX_1:27  :: SQUARE_1'6
a = a - b + b;

theorem :: XCMPLX_1:28  :: REAL_2'28_1
a + c = a + b + (c - b);

:: 2 times '-'

theorem :: XCMPLX_1:29  :: REAL_2'22_1, INT_1'1, REAL_1'17
a + b - c = a - c + b;

theorem :: XCMPLX_1:30  :: REAL_2'23_1
a - b + c = c - b + a;

theorem :: XCMPLX_1:31  :: REAL_2'28_2
a + c = a + b - (b - c);

theorem :: XCMPLX_1:32  :: REAL_2'29_3
a - c = a + b - (c + b);

theorem :: XCMPLX_1:33  :: REAL_2'13
a + b = c + d implies a - c = d - b;

theorem :: XCMPLX_1:34  :: REAL_2'14
a - c = d - b implies a + b = c + d;

theorem :: XCMPLX_1:35  :: REAL_2'16
a + b = c - d implies a + d = c - b;

:: 3 times '-'

theorem :: XCMPLX_1:36  :: REAL_1'27
a - (b + c) = a - b - c;

theorem :: XCMPLX_1:37  :: REAL_1'28
a - (b - c) = a - b + c;

theorem :: XCMPLX_1:38  :: REAL_2'18
a - (b - c) = a + (c - b);

theorem :: XCMPLX_1:39  :: REAL_2'29_2
a - c = (a - b) + (b - c);

theorem :: XCMPLX_1:40  :: REAL_1'29
a * (b - c) = a * b - a * c;

theorem :: XCMPLX_1:41  :: REAL_2'98
(a - b) * (c - d) = (b - a) * (d - c);

theorem :: XCMPLX_1:42  :: REAL_2'99_4
(a - b - c) * d = a * d - b * d - c * d;

:: using operations '-' and '*', '+'

theorem :: XCMPLX_1:43  :: REAL_2'99_2
(a + b - c) * d = a * d + b * d - c * d;

theorem :: XCMPLX_1:44  :: REAL_2'99_3
(a - b + c) * d = a * d - b * d + c * d;

theorem :: XCMPLX_1:45  :: REAL_2'101_2
(a + b) * (c - d) = a * c - a * d + b * c - b * d;

theorem :: XCMPLX_1:46  :: REAL_2'101_3
(a - b) * (c + d) = a * c + a * d - b * c - b * d;

theorem :: XCMPLX_1:47  :: REAL_2'101_4
(a - b) * (e - d) = a * e - a * d - b * e + b * d;

:: using operation '/'

theorem :: XCMPLX_1:48  :: REAL_2'67_1
a / b / c = a / c / b;

:: 0

theorem :: XCMPLX_1:49  :: REAL_2'19
a / 0 = 0;

theorem :: XCMPLX_1:50  :: REAL_2'42_2
a <> 0 & b <> 0 implies a / b <> 0;

:: 2 times '/'

theorem :: XCMPLX_1:51  :: REAL_2'62_4
b <> 0 implies a = a / (b / b);

theorem :: XCMPLX_1:52  :: TOPREAL6'5
a <> 0 implies a / (a / b) = b;

theorem :: XCMPLX_1:53  :: REAL_2'31
c <> 0 & a / c = b / c implies a = b;

theorem :: XCMPLX_1:54  :: REAL_2'74
a / b <> 0 implies b = a / (a / b);

theorem :: XCMPLX_1:55  :: REAL_2'55_1
c <> 0 implies a / b = (a / c) / (b / c);

:: 1

theorem :: XCMPLX_1:56  :: SQUARE_1'16
1 / (1 / a) = a;

theorem :: XCMPLX_1:57  :: REAL_2'48_1
1 / (a / b) = b / a;

theorem :: XCMPLX_1:58  :: REAL_2'30_1
a / b = 1 implies a = b;

theorem :: XCMPLX_1:59  :: REAL_2'33_2
1 / a = 1 / b implies a = b;

:: 0 and 1

theorem :: XCMPLX_1:60  :: REAL_1'37
a <> 0 implies a / a = 1;

theorem :: XCMPLX_1:61  :: REAL_2'39
b <> 0 & b / a = b implies a = 1;

theorem :: XCMPLX_1:62  :: REAL_2'41
a <> 0 implies 1 / a <> 0;

:: using operations '/' and '+'

theorem :: XCMPLX_1:63  :: REAL_1'40_1
a / c + b / c = (a + b) / c;

theorem :: XCMPLX_1:64  :: REAL_2'100_1
(a + b + e) / d = a / d + b / d + e / d;

:: 2

theorem :: XCMPLX_1:65  :: SQUARE_1'15
(a + a) / 2 = a;

theorem :: XCMPLX_1:66  :: SEQ_2'2_1
a/2 + a/2 = a;

theorem :: XCMPLX_1:67  :: TOPREAL3'4
a = (a + b) / 2 implies a = b;

:: 3

theorem :: XCMPLX_1:68  :: REAL_2'89_1
(a + a + a)/3 = a;

theorem :: XCMPLX_1:69  :: SEQ_4'5
a/3 + a/3 + a/3 = a;

:: 4

theorem :: XCMPLX_1:70  :: REAL_2'89_2
(a + a + a + a) / 4 = a;

theorem :: XCMPLX_1:71  :: REAL_2'90
a/4 + a/4 + a/4 + a/4 = a;

theorem :: XCMPLX_1:72  :: SEQ_2'2_2
a / 4 + a / 4 = a / 2;

theorem :: XCMPLX_1:73  :: REAL_2'89_3
(a + a) / 4 = a / 2;

:: using operations '/' and '*'

theorem :: XCMPLX_1:74  :: REAL_2'35_1
a * b = 1 implies a = 1 / b;

theorem :: XCMPLX_1:75  :: SQUARE_1'18
a * (b / c) = (a * b) / c;

theorem :: XCMPLX_1:76  :: REAL_2'80_1
a / b * e = e / b * a;

:: 3 times '/'

theorem :: XCMPLX_1:77  :: REAL_1'35
(a / b) * (c / d) = (a * c) / (b * d);

theorem :: XCMPLX_1:78  :: REAL_1'42
a / (b / c) = (a * c) / b;

theorem :: XCMPLX_1:79  :: SQUARE_1'17
a / (b * c) = a / b / c;

theorem :: XCMPLX_1:80  :: REAL_2'61_1
a / (b / c) = a * (c / b);

theorem :: XCMPLX_1:81  :: REAL_2'61_2
a / (b / c) = c / b * a;

theorem :: XCMPLX_1:82  :: REAL_2'61_3
a / (b / e) = e * (a / b);

theorem :: XCMPLX_1:83  :: REAL_2'61_4
a / (b / c) = a / b * c;

theorem :: XCMPLX_1:84  :: REAL_2'70
(a * b) / (c * d) = (a / c * b) / d;

:: 4 times '/'

theorem :: XCMPLX_1:85  :: REAL_1'82
(a / b) / (c / d) = (a * d) / (b * c);

theorem :: XCMPLX_1:86  :: REAL_2'53
(a / c) * (b / d) = (a / d) * (b / c);

theorem :: XCMPLX_1:87  :: IRRAT_1'5
a / (b * c * (d / e)) = (e / c) * (a / (b * d));

:: 0

theorem :: XCMPLX_1:88  :: REAL_1'43
b <> 0 implies a / b * b = a;

theorem :: XCMPLX_1:89  :: REAL_2'62_1
b <> 0 implies a = a * (b / b);

theorem :: XCMPLX_1:90  :: REAL_2'62_2
b <> 0 implies a = a * b / b;

theorem :: XCMPLX_1:91  :: REAL_2'78
b <> 0 implies a * c = a * b * (c / b);

:: 2 times '/'

theorem :: XCMPLX_1:92  :: REAL_1'38
c <> 0 implies a / b = (a * c) / (b * c);

theorem :: XCMPLX_1:93  :: REAL_2'55_2
c <> 0 implies a / b = a / (b * c) * c;

theorem :: XCMPLX_1:94  :: REAL_2'79
b <> 0 implies a * c = a * b / (b / c);

theorem :: XCMPLX_1:95  :: REAL_2'75
c <> 0 & d <> 0 & a * c = b * d implies a / d = b / c;

theorem :: XCMPLX_1:96  :: REAL_2'76
c <> 0 & d<>0 & a/d=b/c implies a*c = b*d;

theorem :: XCMPLX_1:97  :: REAL_2'77
c <> 0 & d <> 0 & a * c = b / d implies a * d = b / c;

:: 3 times '/'

theorem :: XCMPLX_1:98  :: REAL_2'55_3
c <> 0 implies a / b = c * (a / c / b);

theorem :: XCMPLX_1:99  :: REAL_2'55
c <> 0 implies a / b = a / c * (c / b);

:: 1

theorem :: XCMPLX_1:100  :: REAL_2'56:
a * (1 / b) = a / b;

theorem :: XCMPLX_1:101  :: REAL_2'57
a / (1 / b) = a * b;

theorem :: XCMPLX_1:102  :: REAL_2'80_3
a / b * c = 1 / b * c * a;

:: 3 times '/'

theorem :: XCMPLX_1:103  :: REAL_2'51
(1 / a) * (1 / b) = 1 / (a * b);

theorem :: XCMPLX_1:104  :: REAL_2'67_4
1 / c * (a / b) = a / (b * c);

:: 4 times '/'

theorem :: XCMPLX_1:105  :: REAL_2'67_2
a / b / c = 1 / b * (a / c);

theorem :: XCMPLX_1:106  :: REAL_2'67_3
a / b / c = 1 / c * (a / b);

:: 1 and 0

theorem :: XCMPLX_1:107  :: REAL_1'34
a <> 0 implies a * (1 / a) = 1;

theorem :: XCMPLX_1:108  :: REAL_2'62_3
b <> 0 implies a = a * b * (1 / b);

theorem :: XCMPLX_1:109  :: REAL_2'62_6
b <> 0 implies a = a * (1 / b * b);

theorem :: XCMPLX_1:110  :: REAL_2'62_7
b <> 0 implies a = a * (1 / b) * b;

theorem :: XCMPLX_1:111  :: REAL_2'62_5
b <> 0 implies a = a / (b * (1 / b));

theorem :: XCMPLX_1:112  :: REAL_2'42_4
a <> 0 & b <> 0 implies 1 / (a * b) <> 0;

theorem :: XCMPLX_1:113  :: JGRAPH_2'1
a <> 0 & b <> 0 implies (a / b) * (b / a) = 1;

:: using operations '*', '+' and '/'

theorem :: XCMPLX_1:114  :: REAL_2'65
b <> 0 implies a / b + c = (a + b * c) / b;

theorem :: XCMPLX_1:115  :: REAL_2'92
c <> 0 implies a + b = c * (a / c + b / c);

theorem :: XCMPLX_1:116  :: REAL_2'94
c <> 0 implies a + b = (a * c + b * c) / c;

theorem :: XCMPLX_1:117  :: REAL_1'41_1
b <> 0 & d <> 0 implies a / b + c / d =(a * d + c * b) / (b * d);

theorem :: XCMPLX_1:118  :: REAL_2'96
a <> 0 implies a + b = a * (1 + b / a);

:: 2

theorem :: XCMPLX_1:119  :: REAL_2'91_1
a / (2 * b) + a / (2 * b) = a / b;

:: 3

theorem :: XCMPLX_1:120  :: REAL_2'91_2
a / (3 * b) + a / (3 * b) + a / (3 * b) = a / b;

theorem :: XCMPLX_1:121  :: REAL_1'40_2
a / c - b / c = (a - b) / c;

theorem :: XCMPLX_1:122  :: TOPREAL6'4
a - a / 2 = a / 2;

theorem :: XCMPLX_1:123  :: REAL_2'100_4
(a - b - c) / d = a / d - b / d - c / d;

theorem :: XCMPLX_1:124  :: REAL_2'82
b <> 0 & d <> 0 & b <> d & a / b = e / d implies a / b = (a - e) / (b - d);

:: using operations '-', '/' and '+'

theorem :: XCMPLX_1:125  :: REAL_2'100_2
(a + b - e) / d = a / d + b / d - e / d;

theorem :: XCMPLX_1:126  :: REAL_2'100_3
(a - b + e) / d = a / d - b / d + e / d;

:: using operations '-', '/' and '*'

theorem :: XCMPLX_1:127  :: REAL_2'66_1
b <> 0 implies a / b - e = (a - e * b) / b;

theorem :: XCMPLX_1:128  :: REAL_2'66_2
b <> 0 implies c - a / b = (c * b - a) / b;

theorem :: XCMPLX_1:129  :: REAL_2'93
c <> 0 implies a - b = c * (a / c - b / c);

theorem :: XCMPLX_1:130  :: REAL_2'95
c <> 0 implies a - b = (a * c - b * c) / c;

theorem :: XCMPLX_1:131  :: REAL_1'41_2
b <> 0 & d <> 0 implies a / b - c / d = (a * d - c * b) / (b * d);

theorem :: XCMPLX_1:132  :: REAL_2'97
a <> 0 implies a - b = a * (1 - b / a);

:: using operation '-', '/', '*' and '+'

theorem :: XCMPLX_1:133  :: POLYEQ_1'24
a <> 0 implies c = (a * c + b - b) / a;

:: using unary operation '-'

theorem :: XCMPLX_1:134  :: REAL_2'2_2
-a = -b implies a = b;

theorem :: XCMPLX_1:135  :: REAL_1'22:  :: right to left - requirements REAL
-a = 0 implies a = 0;

theorem :: XCMPLX_1:136  :: REAL_2'2_1
a + -b = 0 implies a = b;

theorem :: XCMPLX_1:137  :: REAL_2'11
a = a + b + -b;

theorem :: XCMPLX_1:138   :: REAL_2'17_1
a = a + (b + -b);

theorem :: XCMPLX_1:139    :: INT_1'3
a = (- b + a) + b;

theorem :: XCMPLX_1:140  :: REAL_2'6_1
- (a + b) = -a + -b;

theorem :: XCMPLX_1:141  :: REAL_2'9_2
- (-a + b) = a + -b;

theorem :: XCMPLX_1:142 :: REAL_2'10_2
a+b=-(-a+-b);

:: using unary and binary operation '-'

theorem :: XCMPLX_1:143  :: REAL_1'83
-(a - b) = b - a;

theorem :: XCMPLX_1:144  :: REAL_2'5
- a - b = - b - a;

theorem :: XCMPLX_1:145  :: REAL_2'17_4
a = - b - (- a - b);

:: binary '-' 4 times

theorem :: XCMPLX_1:146  :: REAL_2'26_1
- a - b - c = - a - c - b;

theorem :: XCMPLX_1:147  :: REAL_2'26_2
- a - b - c = - b - c - a;

theorem :: XCMPLX_1:148  :: REAL_2'26_4
- a - b - c = - c - b - a;

theorem :: XCMPLX_1:149  :: JGRAPH_6'1_2
(c - a) - (c - b) = - (a - b);

:: 0

theorem :: XCMPLX_1:150  :: REAL_1'19
0 - a = - a;

:: using unary and binary operations '-' and '+'

theorem :: XCMPLX_1:151  :: REAL_2'10_3
a + b = a - - b;

theorem :: XCMPLX_1:152  :: REAL_2'17_3
a = a - (b + -b);

theorem :: XCMPLX_1:153  :: REAL_2'2_4
a - c = b + - c implies a = b;

theorem :: XCMPLX_1:154  :: REAL_2'2_6
c - a = c + - b implies a = b;

:: '+' 3 times

theorem :: XCMPLX_1:155  :: REAL_2'22_2
a + b - c = - c + a + b;

theorem :: XCMPLX_1:156  :: REAL_2'23_2
a - b + c = - b + c + a;

theorem :: XCMPLX_1:157  :: REAL_2'20_2
a - (- b - c) = a + b + c;

:: binary '-' 3 times

theorem :: XCMPLX_1:158  :: REAL_2'20_1
a - b - c = - b - c + a;

theorem :: XCMPLX_1:159  :: REAL_2'24_3
a - b - c = - c + a - b;

theorem :: XCMPLX_1:160  :: REAL_2'24_4
a - b - c = - c - b + a;

:: using unary and binary operations '-' and '+'

theorem :: XCMPLX_1:161  :: REAL_2'6_2
- (a + b) = - b - a;

theorem :: XCMPLX_1:162  :: REAL_2'8
- (a - b) = - a + b;

theorem :: XCMPLX_1:163  :: REAL_2'9_1
-(-a+b)=a-b;

theorem :: XCMPLX_1:164  :: REAL_2'10_1
a + b = -(- a - b);

theorem :: XCMPLX_1:165  :: REAL_2'25_1
- a + b - c = - c + b - a;

:: using unary and binary operations '-' and '+' (both '-' 2 times)

theorem :: XCMPLX_1:166  :: REAL_2'25_2
- a + b - c = - c - a + b;

theorem :: XCMPLX_1:167  :: REAL_2'27_1
- (a + b + c) = - a - b - c;

theorem :: XCMPLX_1:168  :: REAL_2'27_2
- (a + b - c) = - a - b + c;

theorem :: XCMPLX_1:169  :: REAL_2'27_3
- (a - b + c) = - a + b - c;

theorem :: XCMPLX_1:170  :: REAL_2'27_5
- (a - b - c) = - a + b + c;

theorem :: XCMPLX_1:171  :: REAL_2'27_4
- (- a + b + c) = a - b - c;

theorem :: XCMPLX_1:172  :: REAL_2'27_6
- (- a + b - c) = a - b + c;

theorem :: XCMPLX_1:173  :: REAL_2'27_7
- (- a - b + c) = a + b - c;

theorem :: XCMPLX_1:174  :: REAL_2'27_8
- (- a - b - c) = a + b + c;

:: using unary operations '-' and '*'

theorem :: XCMPLX_1:175  :: REAL_1'21_1
(- a) * b = -(a * b);

theorem :: XCMPLX_1:176  :: REAL_1'21_2
(- a) * b = a * (- b);

theorem :: XCMPLX_1:177  :: REAL_2'49_1
(- a) * (- b) = a * b;

theorem :: XCMPLX_1:178  :: REAL_2'49_2
- a * (- b) = a * b;

theorem :: XCMPLX_1:179  :: REAL_2'49_3
-(-a) * b = a * b;

theorem :: XCMPLX_1:180  :: REAL_2'71_1
(-1) * a = -a;

theorem :: XCMPLX_1:181  :: REAL_2'71_2
(- a) * (- 1) = a;

theorem :: XCMPLX_1:182  :: REAL_2'38
b<>0 & a*b=-b implies a=-1;

theorem :: XCMPLX_1:183  :: Thx
a * a = 1 implies a = 1 or a = -1;

theorem :: XCMPLX_1:184  :: TOPREAL6'3
-a + 2 * a = a;

theorem :: XCMPLX_1:185  :: REAL_2'85_1
(a - b) * c = (b - a) * (- c);

theorem :: XCMPLX_1:186  :: REAL_2'85_2
(a - b) * c = - (b - a) * c;

theorem :: XCMPLX_1:187  :: TOPREAL6'2
a - 2 * a = -a;

:: using unary operations '-' and '/'

theorem :: XCMPLX_1:188  :: REAL_1'39_1
-a / b = (-a) / b;

theorem :: XCMPLX_1:189  :: REAL_1'39_2
a / (- b) = -a / b;

theorem :: XCMPLX_1:190  :: REAL_2'58_1
- a / (- b) = a / b;

theorem :: XCMPLX_1:191  :: REAL_2'58_2
-(- a) / b = a / b;

theorem :: XCMPLX_1:192  :: REAL_2'58_3
(- a) / (- b) = a / b;

theorem :: XCMPLX_1:193  :: REAL_2'58
(-a) / b = a / (-b);

theorem :: XCMPLX_1:194  :: REAL_2'71_3
-a = a / (-1);

theorem :: XCMPLX_1:195  :: REAL_2'71
a = (- a) / (-1);

theorem :: XCMPLX_1:196  :: REAL_2'34
a / b = - 1 implies a = - b & b = - a;

theorem :: XCMPLX_1:197  :: REAL_2'40
b <> 0 & b / a = - b implies a = -1;

theorem :: XCMPLX_1:198  :: REAL_2'45_2
a <> 0 implies (-a) / a = -1;

theorem :: XCMPLX_1:199  :: REAL_2'45_3
a <> 0 implies a / (- a) = -1;

theorem :: XCMPLX_1:200  :: REAL_2'46_2
a <> 0 & a = 1 / a implies a = 1 or a = -1;

theorem :: XCMPLX_1:201  :: REAL_2'83:
b <> 0 & d <> 0 & b <> -d & a / b = e / d implies a / b = (a + e) / (b + d)
;

:: using operation '"'

theorem :: XCMPLX_1:202  :: REAL_2'33_1
a" = b" implies a = b;

theorem :: XCMPLX_1:203  :: REAL_1'31
a" = 0 implies a = 0;

:: using '"' and '*'

theorem :: XCMPLX_1:204
b <> 0 implies a = a*b*b";

theorem :: XCMPLX_1:205  :: REAL_1'24
a" * b" = (a * b)";

theorem :: XCMPLX_1:206  :: REAL_2'47_1
(a * b")" = a" * b;

theorem :: XCMPLX_1:207  :: REAL_2'47_2
(a" * b")" = a * b;

theorem :: XCMPLX_1:208  :: REAL_2'42_1:
a <> 0 & b <> 0 implies a * b" <> 0;

theorem :: XCMPLX_1:209  :: REAL_2'42_3
a <> 0 & b <> 0 implies a" * b" <> 0;

theorem :: XCMPLX_1:210  :: REAL_2'30_2
a * b" = 1 implies a = b;

theorem :: XCMPLX_1:211  :: REAL_2'35_2
a * b = 1 implies a = b";

:: using '"', '*', and '+'

canceled;

theorem :: XCMPLX_1:213
a <> 0 & b <> 0 implies a" + b" = (a + b)*(a*b)";

:: using '"', '*', and '-'

theorem :: XCMPLX_1:214
a <> 0 & b <> 0 implies a" - b" = (b - a)*(a*b)";

:: using '"' and '/'

theorem :: XCMPLX_1:215  :: REAL_1'81
(a / b)" = b / a;

theorem :: XCMPLX_1:216
(a"/b") = b/a;

theorem :: XCMPLX_1:217  :: REAL_1'33_1
1 / a = a";

theorem :: XCMPLX_1:218  :: REAL_1'33_2
1 / a" = a;

theorem :: XCMPLX_1:219  :: REAL_2'36_21
(1 / a)" = a;

theorem :: XCMPLX_1:220  :: REAL_2'33_3
1 / a = b" implies a = b;

:: using '"', '*', and '/'

theorem :: XCMPLX_1:221
a/b" = a*b;

theorem :: XCMPLX_1:222
a"*(c/b) = c/(a*b);

theorem :: XCMPLX_1:223
a"/b = (a*b)";

:: both unary operations

theorem :: XCMPLX_1:224  :: REAL_2'45_1
(- a)" = -a";

theorem :: XCMPLX_1:225  :: REAL_2'46_1
a <> 0 & a = a" implies a = 1 or a = -1;

:: from JORDAN4

theorem :: XCMPLX_1:226
a+b+c-b=a+c;

theorem :: XCMPLX_1:227
a-b+c+b=a+c;

theorem :: XCMPLX_1:228
a+b-c-b=a-c;

theorem :: XCMPLX_1:229
a-b-c+b=a-c;

theorem :: XCMPLX_1:230
a-a-b=-b;

theorem :: XCMPLX_1:231
-a+a-b=-b;

theorem :: XCMPLX_1:232
a-b-a=-b;

theorem :: XCMPLX_1:233
-a-b+a=-b;

```