mmtheorems58 - 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-10691

Statement List for Metamath Proof Explorer - 5701-5800 - Page 58 of 107

Type	Label	Description
Statement
Theorem	divne0bt 5701	The ratio of non-zero numbers is non-zero.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> (A =/= 0 <-> (A / B) =/= 0))
Theorem	divne0t 5702	The ratio of non-zero numbers is non-zero.
|- (((A e. CC /\ A =/= 0) /\ (B e. CC /\ B =/= 0)) -> (A / B) =/= 0)
Theorem	divne0 5703	The ratio of non-zero numbers is non-zero.
|- A e. CC   &   |- B e. CC   &   |- A =/= 0   &   |- B =/= 0   =>   |- (A / B) =/= 0
Theorem	recne0z 5704	The reciprocal of a non-zero number is non-zero.
|- A e. CC   =>   |- (A =/= 0 -> (1 / A) =/= 0)
Theorem	recne0t 5705	The reciprocal of a non-zero number is non-zero.
|- ((A e. CC /\ A =/= 0) -> (1 / A) =/= 0)
Theorem	recid 5706	Multiplication of a number and its reciprocal.
|- A e. CC   &   |- A =/= 0   =>   |- (A x. (1 / A)) = 1
Theorem	recidz 5707	Multiplication of a number and its reciprocal.
|- A e. CC   =>   |- (A =/= 0 -> (A x. (1 / A)) = 1)
Theorem	recidt 5708	Multiplication of a number and its reciprocal.
|- ((A e. CC /\ A =/= 0) -> (A x. (1 / A)) = 1)
Theorem	recid2t 5709	Multiplication of a number and its reciprocal.
|- ((A e. CC /\ A =/= 0) -> ((1 / A) x. A) = 1)
Theorem	divrec 5710	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	divrecz 5711	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	divrect 5712	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	divrec2t 5713	Relationship between division and reciprocal.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> (A / B) = ((1 / B) x. A))
Theorem	divasst 5714	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	div23t 5715	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	div13t 5716	A commutative/associative law for division.
|- (((A e. CC /\ B e. CC /\ C e. CC) /\ B =/= 0) -> ((A / B) x. C) = ((C / B) x. A))
Theorem	div12t 5717	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	divassz 5718	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	divass 5719	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	divdir 5720	Distribution of division over addition.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C =/= 0   =>   |- ((A + B) / C) = ((A / C) + (B / C))
Theorem	div23 5721	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	divdirz 5722	Distribution of division over addition.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- (C =/= 0 -> ((A + B) / C) = ((A / C) + (B / C)))
Theorem	divdirt 5723	Distribution of division over addition.
|- (((A e. CC /\ B e. CC /\ C e. CC) /\ C =/= 0) -> ((A + B) / C) = ((A / C) + (B / C)))
Theorem	divcan3 5724	A cancellation law for division.
|- A e. CC   &   |- B e. CC   &   |- A =/= 0   =>   |- ((A x. B) / A) = B
Theorem	divcan4 5725	A cancellation law for division.
|- A e. CC   &   |- B e. CC   &   |- A =/= 0   =>   |- ((B x. A) / A) = B
Theorem	divcan3z 5726	A cancellation law for division. (Eliminates a hypothesis of divcan3 5724 with the weak deduction theorem.)
|- A e. CC   &   |- B e. CC   =>   |- (A =/= 0 -> ((A x. B) / A) = B)
Theorem	divcan4z 5727	A cancellation law for division.
|- A e. CC   &   |- B e. CC   =>   |- (A =/= 0 -> ((B x. A) / A) = B)
Theorem	divcan3t 5728	A cancellation law for division.
|- ((A e. CC /\ B e. CC /\ A =/= 0) -> ((A x. B) / A) = B)
Theorem	divcan4t 5729	A cancellation law for division.
|- ((A e. CC /\ B e. CC /\ A =/= 0) -> ((B x. A) / A) = B)
Theorem	div11 5730	One-to-one relationship for division.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C =/= 0   =>   |- ((A / C) = (B / C) <-> A = B)
Theorem	div11t 5731	One-to-one relationship for division.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A / C) = (B / C) <-> A = B))
Theorem	dividt 5732	A number divided by itself is one.
|- ((A e. CC /\ A =/= 0) -> (A / A) = 1)
Theorem	div0t 5733	Division into zero is zero.
|- ((A e. CC /\ A =/= 0) -> (0 / A) = 0)
Theorem	diveq0t 5734	A ratio is zero iff the numerator is zero.
|- ((A e. CC /\ C e. CC /\ C =/= 0) -> ((A / C) = 0 <-> A = 0))
Theorem	recrec 5735	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	divid 5736	A number divided by itself is one.
|- A e. CC   &   |- A =/= 0   =>   |- (A / A) = 1
Theorem	div0 5737	Division into zero is zero.
|- A e. CC   &   |- A =/= 0   =>   |- (0 / A) = 0
Theorem	div1 5738	A number divided by 1 is itself.
|- A e. CC   =>   |- (A / 1) = A
Theorem	div1t 5739	A number divided by 1 is itself.
|- (A e. CC -> (A / 1) = A)
Theorem	divnegt 5740	Move negative sign inside of a division.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> -u(A / B) = (-uA / B))
Theorem	divsubdirt 5741	Distribution of division over subtraction.
|- (((A e. CC /\ B e. CC /\ C e. CC) /\ C =/= 0) -> ((A - B) / C) = ((A / C) - (B / C)))
Theorem	recrect 5742	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	rec11i 5743	Reciprocal is one-to-one.
|- A e. CC   &   |- B e. CC   &   |- A =/= 0   &   |- B =/= 0   =>   |- ((1 / A) = (1 / B) <-> A = B)
Theorem	rec11 5744	Reciprocal is one-to-one.
|- A e. CC   &   |- B e. CC   =>   |- ((A =/= 0 /\ B =/= 0) -> ((1 / A) = (1 / B) <-> A = B))
Theorem	rec11rt 5745	Mutual reciprocals. (Contributed by Paul Chapman, 18-Oct-2007.)
|- (((A e. CC /\ B e. CC) /\ (A =/= 0 /\ B =/= 0)) -> ((1 / A) = B <-> (1 / B) = A))
Theorem	divmuldivt 5746	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	divcan5t 5747	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	divmul13t 5748	Swap the denominators in the product 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	divmul24t 5749	Swap the numerators in the product of two ratios.
|- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> ((A / B) x. (C / D)) = ((A / D) x. (C / B)))
Theorem	divadddivt 5750	Addition of two ratios. Theorem I.13 of [Apostol] p. 18.
|- (<