EMM, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### The abstract of the Mizar article:

### Complex Numbers --- Basic Theorems

**by****Library Committee**- Received April 10, 2003
- 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; begin :: additional :: 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;

Back to top