mmtheorems73 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19026

Statement List for Metamath Proof Explorer - 7201-7300 - Page 73 of 191

Type	Label	Description
Statement
Theorem	mulge0 7201	The product of two nonnegative numbers is nonnegative.
|- (((A e. RR /\ 0 <_ A) /\ (B e. RR /\ 0 <_ B)) -> 0 <_ (A x. B))
Theorem	mulge0OLD 7202	The product of two nonnegative numbers is nonnegative.
|- (((A e. RR /\ B e. RR) /\ (0 <_ A /\ 0 <_ B)) -> 0 <_ (A x. B))
Theorem	mullt0 7203	The product of two negative numbers is positive. (Contributed by Jeffrey Hankins, 8-Jun-2009.)
|- (((A e. RR /\ A < 0) /\ (B e. RR /\ B < 0)) -> 0 < (A x. B))
Theorem	lt01 7204	0 is less than 1. Theorem I.21 of [Apostol] p. 20.
|- 0 < 1
Reciprocals
Theorem	ixi 7205	_i times itself is minus 1. (The proof was shortened by Andrew Salmon, 19-Nov-2011.)
|- (_i x. _i) = -u1
Theorem	recextlem1 7206	Lemma for recex 7208. [Auxiliary lemma - not displayed.]
Theorem	recextlem2 7207	Lemma for recex 7208. [Auxiliary lemma - not displayed.]
Theorem	recex 7208	Existence of reciprocal of nonzero complex number. (Contributed by Eric Schmidt, 22-May-2007.)
|- ((A e. CC /\ A =/= 0) -> E.x e. CC (A x. x) = 1)
Theorem	recexi 7209	Existence of reciprocals.
|- A e. CC   &   |- A =/= 0   =>   |- E.x e. CC (A x. x) = 1
Theorem	mulcani 7210	Cancellation law for multiplication. Theorem I.7 of [Apostol] p. 18.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C =/= 0   =>   |- ((C x. A) = (C x. B) <-> A = B)
Theorem	mulcant2i 7211	Cancellation law for multiplication. Theorem I.7 of [Apostol] p. 18. Illustrates use of keephyp 3221.
|- C =/= 0   =>   |- ((A e. CC /\ B e. CC /\ C e. CC) -> ((C x. A) = (C x. B) <-> A = B))
Theorem	mulcan 7212	Cancellation law for multiplication (full theorem form). Theorem I.7 of [Apostol] p. 18. Illustrates use of dedth 3208 and elimne0 6820.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((C x. A) = (C x. B) <-> A = B))
Theorem	mulcan2 7213	Cancellation law for multiplication.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A x. C) = (B x. C) <-> A = B))
Theorem	mul0ori 7214	If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18.
|- A e. CC   &   |- B e. CC   =>   |- ((A x. B) = 0 <-> (A = 0 \/ B = 0))
Theorem	msq0i 7215	A number is zero iff its square is zero (where square is represented using multiplication).
|- A e. CC   =>   |- ((A x. A) = 0 <-> A = 0)
Theorem	mul0or 7216	If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18.
|- ((A e. CC /\ B e. CC) -> ((A x. B) = 0 <-> (A = 0 \/ B = 0)))
Theorem	mulne0b 7217	The product of two nonzero numbers is nonzero. (The proof was shortened by Andrew Salmon, 19-Nov-2011.)
|- ((A e. CC /\ B e. CC) -> ((A =/= 0 /\ B =/= 0) <-> (A x. B) =/= 0))
Theorem	mulne0 7218	The product of two nonzero numbers is nonzero.
|- (((A e. CC /\ A =/= 0) /\ (B e. CC /\ B =/= 0)) -> (A x. B) =/= 0)
Theorem	mulne0i 7219	The product of two nonzero numbers is nonzero.
|- A e. CC   &   |- B e. CC   &   |- A =/= 0   &   |- B =/= 0   =>   |- (A x. B) =/= 0
Theorem	muleqadd 7220	Property of numbers whose product equals their sum. Equation 5 of [Kreyszig] p. 12.
|- ((A e. CC /\ B e. CC) -> ((A x. B) = (A + B) <-> ((A - 1) x. (B - 1)) = 1))
Theorem	receui 7221	Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18.
|- A e. CC   &   |- B e. CC   &   |- A =/= 0   =>   |- E!x e. CC (A x. x) = B
Theorem	mulnzcnopr 7222	Multiplication maps nonzero complex numbers to nonzero complex numbers. (Contributed by Steve Rodriguez, 23-Feb-2007.)
|- ( x. |` ((CC \ {0}) X. (CC \ {0}))):((CC \ {0}) X. (CC \ {0}))-->(CC \ {0})
Division
Definition	df-div 7223	Define division. Theorem divmuli 7225 relates it to multiplication, and divcli 7230 and redivcli 7307 prove its closure laws.
|- / = {<.<.x, y>., z>. | ((x e. CC /\ y e. (CC \ {0})) /\ z = (iota_w e. CC(y x. w) = x))}
Theorem	divvali 7224	Value of division: the (unique) element x such that (B x. x) = A. This is meaningful only when B is nonzero.
|- A e. CC   &   |- B e. CC   &   |- B =/= 0   =>   |- (A / B) = (iota_x e. CC(B x. x) = A)
Theorem	divmuli 7225	Relationship between division and multiplication.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- B =/= 0   =>   |- ((A / B) = C <-> (B x. C) = A)
Theorem	divmulzi 7226	Relationship between division and multiplication.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- (B =/= 0 -> ((A / B) = C <-> (B x. C) = A))
Theorem	divmul 7227	Relationship between division and multiplication.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A / C) = B <-> (C x. B) = A))
Theorem	divmul2 7228	Relationship between division and multiplication.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A / C) = B <-> A = (C x. B)))
Theorem	divmul3 7229	Relationship between division and multiplication.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A / C) = B <-> A = (B x. C)))
Theorem	divcli 7230	Closure law for division.
|- A e. CC   &   |- B e. CC   &   |- B =/= 0   =>   |- (A / B) e. CC
Theorem	divclzi 7231	Closure law for division.
|- A e. CC   &   |- B e. CC   =>   |- (B =/= 0 -> (A / B) e. CC)
Theorem	divcl 7232	Closure law for division.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> (A / B) e. CC)
Theorem	reccli 7233	Closure law for reciprocal.
|- A e. CC   &   |- A =/= 0   =>   |- (1 / A) e. CC
Theorem	recclzi 7234	Closure law for reciprocal.
|- A e. CC   =>   |- (A =/= 0 -> (1 / A) e. CC)
Theorem	reccl 7235	Closure law for reciprocal.
|- ((A e. CC /\ A =/= 0) -> (1 / A) e. CC)
Theorem	divcan2i 7236	A cancellation law for division.
|- A e. CC   &   |- B e. CC   &   |- B =/= 0   =>   |- (B x. (A / B)) = A
Theorem	divcan1i 7237	A cancellation law for division.
|- A e. CC   &   |- B e. CC   &   |- B =/= 0   =>   |- ((A / B) x. B) = A
Theorem	divcan1zi 7238	A cancellation law for division.
|- A e. CC   &   |- B e. CC   =>   |- (B =/= 0 -> ((A / B) x. B) = A)
Theorem	divcan2zi 7239	A cancellation law for division. We eliminate the third hypothesis of divcan2i 7236 using the weak deduction theorem dedth 3208 and keep the other two. Because the first hypothesis shares the class variable B with the hypothesis we're eliminating, we need to use keepel 3224 in order to keep the first hypothesis.
|- A e. CC   &   |- B e. CC   =>   |- (B =/= 0 -> (B x. (A / B)) = A)
Theorem	divcan1 7240	A cancellation law for division.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> ((A / B) x. B) = A)
Theorem	divcan2 7241	A cancellation law for division.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> (B x. (A / B)) = A)
Theorem	divne0b 7242	The ratio of nonzero numbers is nonzero.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> (A =/= 0 <-> (A / B) =/= 0))
Theorem	divne0 7243	The ratio of nonzero numbers is nonzero.
|- (((A e. CC /\ A =/= 0) /\ (B e. CC /\ B =/= 0)) -> (A / B) =/= 0)
Theorem	divne0i 7244	The ratio of nonzero numbers is nonzero.
|- A e. CC   &   |- B e. CC   &   |- A =/= 0   &   |- B =/= 0   =>   |- (A / B) =/= 0
Theorem	recne0zi 7245	The reciprocal of a nonzero number is nonzero.
|- A e. CC   =>   |- (A =/= 0 -> (1 / A) =/= 0)
Theorem	recne0 7246	The reciprocal of a nonzero number is nonzero.
|- ((A e. CC /\ A =/= 0) -> (1 / A) =/= 0)
Theorem	recidi 7247	Multiplication of a number and its reciprocal.
|- A e. CC   &   |- A =/= 0   =>   |- (A x. (1 / A)) = 1
Theorem	recidzi 7248	Multiplication of a number and its reciprocal.
|- A e. CC   =>   |- (A =/= 0 -> (A x. (1 / A)) = 1)
Theorem	recid 7249	Multiplication of a number and its reciprocal.
|- ((A e. CC /\ A =/= 0) -> (A x. (1 / A)) = 1)
Theorem	recid2 7250	Multiplication of a number and its reciprocal.
|- ((A e. CC /\ A =/= 0) -> ((1 / A) x. A) = 1)
Theorem	divreci 7251	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18.
|- A e. CC   &   |- B e. CC   &   |- B =/= 0   =>   |- (A / B) = (A x. (1 / B))
Theorem	divreczi 7252	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18.
|- A e. CC   &   |- B e. CC   =>   |- (B =/= 0 -> (A / B) = (A x. (1 / B)))
Theorem	divrec 7253	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> (A / B) = (A x. (1 / B)))
Theorem	divrec2 7254	Relationship between division and reciprocal.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> (A / B) = ((1 / B) x. A))
Theorem	divass 7255	An associative law for division.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A x. B) / C) = (A x. (B / C)))
Theorem	div23 7256	A commutative/associative law for division.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A x. B) / C) = ((A / C) x. B))
Theorem	div13 7257	A commutative/associative law for division.
|- ((A e. CC /\ (B e. CC /\ B =/= 0) /\ C e. CC) -> ((A / B) x. C) = ((C / B) x. A))
Theorem	div12 7258	A commutative/associative law for division.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> (A x. (B / C)) = (B x. (A / C)))
Theorem	divasszi 7259	An associative law for division.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- (C =/= 0 -> ((A x. B) / C) = (A x. (B / C)))
Theorem	divassi 7260	An associative law for division.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C =/= 0   =>   |- ((A x. B) / C) = (A x. (B / C))
Theorem	divdiri 7261	Distribution of division over addition.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C =/= 0   =>   |- ((A + B) / C) = ((A / C) + (B / C))
Theorem	div23i 7262	A commutative/associative law for division.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C =/= 0   =>   |- ((A x. B) / C) = ((A / C) x. B)
Theorem	divdirzi 7263	Distribution of division over addition.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- (C =/= 0 -> ((A + B) / C) = ((A / C) + (B / C)))
Theorem	divdir 7264	Distribution of division over addition.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A + B) / C) = ((A / C) + (B / C)))
Theorem	divcan3i 7265	A cancellation law for division.
|- A e. CC   &   |- B e. CC   &   |- B =/= 0   =>   |- ((B x. A) / B) = A
Theorem	divcan4i 7266	A cancellation law for division.
|- A e. CC   &   |- B e. CC   &   |- B =/= 0   =>   |- ((A x. B) / B) = A
Theorem	divcan3zi 7267	A cancellation law for division. (Eliminates a hypothesis of divcan3i 7265 with the weak deduction theorem.)
|- A e. CC   &   |- B e. CC   =>   |- (B =/= 0 -> ((B x. A) / B) = A)
Theorem	divcan4zi 7268	A cancellation law for division.
|- A e. CC   &   |- B e. CC   =>   |- (B =/= 0 -> ((A x. B) / B) = A)
Theorem	divcan3 7269	A cancellation law for division.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> ((B x. A) / B) = A)
Theorem	divcan4 7270	A cancellation law for division.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> ((A x. B) / B) = A)
Theorem	div11i 7271	One-to-one relationship for division.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C =/= 0   =>   |- ((A / C) = (B / C) <-> A = B)
Theorem	div11 7272	One-to-one relationship for division.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A / C) = (B / C) <-> A = B))
Theorem	divid 7273	A number divided by itself is one.
|- ((A e. CC /\ A =/= 0) -> (A / A) = 1)
Theorem	div0 7274	Division into zero is zero.
|- ((A e. CC /\ A =/= 0) -> (0 / A) = 0)
Theorem	diveq0 7275	A ratio is zero iff the numerator is zero.
|- ((A e. CC /\ C e. CC /\ C =/= 0) -> ((A / C) = 0 <-> A = 0))
Theorem	recreci 7276	A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18.
|- A e. CC   &   |- A =/= 0   =>   |- (1 / (1 / A)) = A
Theorem	dividi 7277	A number divided by itself is one.
|- A e. CC   &   |- A =/= 0   =>   |- (A / A) = 1
Theorem	div0i 7278	Division into zero is zero.
|- A e. CC   &   |- A =/= 0   =>   |- (0 / A) = 0
Theorem	div1i 7279	A number divided by 1 is itself.
|- A e. CC   =>   |- (A / 1) = A
Theorem	div1 7280	A number divided by 1 is itself.
|- (A e. CC -> (A / 1) = A)
Theorem	divneg 7281	Move negative sign inside of a division.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> -u(A / B) = (-uA / B))
Theorem	divsubdir 7282	Distribution of division over subtraction.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A - B) / C) = ((A / C) - (B / C)))
Theorem	recrec 7283	A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18.
|- ((A e. CC /\ A =/= 0) -> (1 / (1 / A)) = A)
Theorem	rec11ii 7284	Reciprocal is one-to-one.
|- A e. CC   &   |- B e. CC   &   |- A =/= 0   &   |- B =/= 0   =>   |- ((1 / A) = (1 / B) <-> A = B)
Theorem	rec11i 7285	Reciprocal is one-to-one.
|- A e. CC   &   |- B e. CC   =>   |- ((A =/= 0 /\ B =/= 0) -> ((1 / A) = (1 / B) <-> A = B))
Theorem	rec11r 7286	Mutual reciprocals. (Contributed by Paul Chapman, 18-Oct-2007.)
|- (((A e. CC /\ A =/= 0) /\ (B e. CC /\ B =/= 0)) -> ((1 / A) = B <-> (1 / B) = A))
Theorem	divmuldiv 7287	Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18.
|- (((A e. CC /\ B e. CC) /\ ((C e. CC /\ C =/= 0) /\ (D e. CC /\ D =/= 0))) -> ((A / C) x. (B / D)) = ((A x. B) / (C x. D)))
Theorem	divcan5 7288	Cancellation of common factor in a ratio.
|- ((A e. CC /\ (B e. CC /\ B =/= 0) /\ (C e. CC /\ C =/= 0)) -> ((C x. A) / (C x. B)) = (A / B))
Theorem	divmul13 7289	Swap the denominators in the product of two ratios.
|- (((A e. CC /\ B e. CC) /\ ((C e. CC /\ C =/= 0) /\ (D e. CC /\ D =/= 0))) -> ((A / C) x. (B / D)) = ((B / C) x. (A / D)))
Theorem	divmul24 7290	Swap the numerators in the product of two ratios.
|- (((A e. CC /\ B e. CC) /\ ((C e. CC /\ C =/= 0) /\ (D e. CC /\ D =/= 0))) -> ((A / C) x. (B / D)) = ((A / D) x. (B / C)))
Theorem	divadddiv 7291	Addition of two ratios. Theorem I.13 of [Apostol] p. 18.
|- (((A e. CC /\ B e. CC) /\ ((C e. CC /\ C =/= 0) /\ (D e. CC /\ D =/= 0))) -> ((A / C) + (B / D)) = (((A x. D) + (C x. B)) / (C x. D)))
Theorem	divdivdiv 7292	Division of two ratios. Theorem I.15 of [Apostol] p. 18.
|- (((A e. CC /\ (B e. CC /\ B =/= 0)) /\ ((C e. CC /\ C =/= 0) /\ (D e. CC /\ D =/= 0))) -> ((A / B) / (C / D)) = ((A x. D) / (B x. C)))
Theorem	divdivdivOLD 7293	Division of two ratios. Theorem I.15 of [Apostol] p. 18.
|- (((A e. CC /\ (B e. CC /\ B =/= 0)) /\ ((C e. CC /\ C =/= 0) /\ (D e. CC /\ D =/= 0))) -> ((A / B) / (C / D)) = ((A x. D) / (B x. C)))
Theorem	divmuldivi 7294	Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- D e. CC   &   |- B =/= 0   &   |- D =/= 0   =>   |- ((A / B) x. (C / D)) = ((A x. C) / (B x. D))
Theorem	divmul13i 7295	Swap denominators of two ratios.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- D e. CC   &   |- B =/= 0   &   |- D =/= 0   =>   |- ((A / B) x. (C / D)) = ((C / B) x. (A / D))
Theorem	divadddivi 7296	Addition of two ratios. Theorem I.13 of [Apostol] p. 18.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- D e. CC   &   |- B =/= 0   &   |- D =/= 0   =>   |- ((A / B) + (C / D)) = (((A x. D) + (B x. C)) / (B x. D))
Theorem	divdivdivi 7297	Division of two ratios. Theorem I.15 of [Apostol] p. 18.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- D e. CC   &   |- B =/= 0   &   |- D =/= 0   &   |- C =/= 0   =>   |- ((A / B) / (C / D)) = ((A x. D) / (B x. C))
Theorem	recdiv 7298	The reciprocal of a ratio.
|- (((A e. CC /\ A =/= 0) /\ (B e. CC /\ B =/= 0)) -> (1 / (A / B)) = (B / A))
Theorem	divcan6 7299	Cancellation of inverted fractions.
|- (((A e. CC /\ A =/= 0) /\ (B e. CC /\ B =/= 0)) -> ((A / B) x. (B / A)) = 1)
Theorem	divdiv23 7300	Swap denominators in a division.
|- ((A e. CC /\ (B e. CC /\ B =/= 0) /\ (C e. CC /\ C =/= 0)) -> ((A / B) / C) = ((A / C) / B))