Metamath Proof Explorer - mmtheorems43

Jump to page: 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-5787

Statement List for Metamath Proof Explorer - 4201-4300 - Page 43 of 58

Type	Label	Description
Statement
Theorem	negdi2t 4201	Distribution of negative over subtraction.
|- ((A e. CC /\ B e. CC) -> -u(A - B) = (-uA + B))
Theorem	negdi3t 4202	Distribution of negative over subtraction.
|- ((A e. CC /\ B e. CC) -> -u(A - B) = (B - A))
Theorem	subsubt 4203	Law for double subtraction.
|- ((A e. CC /\ B e. CC /\ C e. CC) -> (A - (B - C)) = ((A - B) + C))
Theorem	mulm1t 4204	Product with minus one is negative.
|- (A e. CC -> (-u1 x. A) = -uA)
Theorem	mulm1 4205	Product with minus one is negative.
|- A e. CC   =>   |- (-u1 x. A) = -uA
Theorem	sub4 4206	Rearrangement of 4 terms in a mixed addition and subtraction.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- D e. CC   =>   |- ((A + B) - (C + D)) = ((A - C) + (B - D))
Theorem	mulcan 4207	Cancellation law for multiplication. Theorem I.7 of [Apostol] p. 18.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- A =/= 0   =>   |- ((A x. B) = (A x. C) <-> B = C)
Theorem	mulcant 4208	Cancellation law for multiplication (theorem form). Theorem I.7 of [Apostol] p. 18. Illustrates use of keephyp 1794.
|- A =/= 0   =>   |- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A x. B) = (A x. C) <-> B = C))
Theorem	mulcant2 4209	Cancellation law for multiplication (full theorem form). Theorem I.7 of [Apostol] p. 18. Illustrates use of dedth 1784 and elimne0 4102.
|- (((A e. CC /\ B e. CC /\ C e. CC) /\ A =/= 0) -> ((A x. B) = (A x. C) <-> B = C))
Theorem	mul0or 4210	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	sq0 4211	A number is zero iff its square is zero.
|- A e. CC   =>   |- ((A x. A) = 0 <-> A = 0)
Theorem	mul0ort 4212	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	muln0bt 4213	The product of two non-zero numbers is non-zero.
|- ((A e. CC /\ B e. CC) -> ((A =/= 0 /\ B =/= 0) <-> (A x. B) =/= 0))
Theorem	muln0 4214	The product of two non-zero numbers is non-zero.
|- A e. CC   &   |- B e. CC   &   |- A =/= 0   &   |- B =/= 0   =>   |- (A x. B) =/= 0
Theorem	receu 4215	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
Definition	df-div 4216	Define division. Theorem divmul 4218 relates it to multiplication, and divcl 4221 and redivcl 4274 prove its closure laws.
|- / = {<.<.x, y>., z>. | ((x e. CC /\ y e. (CC \ {0})) /\ z = U.{w e. CC | (y x. w) = x})}
Theorem	divval 4217	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) = U.{x e. CC | (B x. x) = A}
Theorem	divmul 4218	Relationship between division and multiplication.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- B =/= 0   =>   |- ((A / B) = C <-> (B x. C) = A)
Theorem	divmulz 4219	Relationship between division and multiplication.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- (B =/= 0 -> ((A / B) = C <-> (B x. C) = A))
Theorem	divmult 4220	Relationship between division and multiplication.
|- (((A e. CC /\ B e. CC /\ C e. CC) /\ B =/= 0) -> ((A / B) = C <-> (B x. C) = A))
Theorem	divcl 4221	Closure law for division.
|- A e. CC   &   |- B e. CC   &   |- B =/= 0   =>   |- (A / B) e. CC
Theorem	divclz 4222	Closure law for division.
|- A e. CC   &   |- B e. CC   =>   |- (B =/= 0 -> (A / B) e. CC)
Theorem	divclt 4223	Closure law for division.
|- (((A e. CC /\ B e. CC) /\ B =/= 0) -> (A / B) e. CC)
Theorem	divcan2 4224	A cancellation law for division.
|- A e. CC   &   |- B e. CC   &   |- A =/= 0   =>   |- (A x. (B / A)) = B
Theorem	divcan1 4225	A cancellation law for division.
|- A e. CC   &   |- B e. CC   &   |- A =/= 0   =>   |- ((B / A) x. A) = B
Theorem	divcan1z 4226	A cancellation law for division.
|- A e. CC   &   |- B e. CC   =>   |- (A =/= 0 -> ((B / A) x. A) = B)
Theorem	divcan2z 4227	A cancellation law for division.
|- A e. CC   &   |- B e. CC   =>   |- (A =/= 0 -> (A x. (B / A)) = B)
Theorem	divcan1t 4228	A cancellation law for division.
|- (((A e. CC /\ B e. CC) /\ A =/= 0) -> ((B / A) x. A) = B)
Theorem	divcan2t 4229	A cancellation law for division.
|- (((A e. CC /\ B e. CC) /\ A =/= 0) -> (A x. (B / A)) = B)
Theorem	divneq0bt 4230	The ratio of non-zero numbers is non-zero.
|- (((A e. CC /\ B e. CC) /\ B =/= 0) -> (A =/= 0 <-> (A / B) =/= 0))
Theorem	divneq0 4231	The ratio of non-zero numbers is non-zero.
|- A e. CC   &   |- B e. CC   &   |- A =/= 0   &   |- B =/= 0   =>   |- (A / B) =/= 0
Theorem	recneq0z 4232	The reciprocal of a non-zero number is non-zero.
|- A e. CC   =>   |- (A =/= 0 -> (1 / A) =/= 0)
Theorem	recid 4233	Multiplication of a number and its reciprocal.
|- A e. CC   &   |- A =/= 0   =>   |- (A x. (1 / A)) = 1
Theorem	recidz 4234	Multiplication of a number and its reciprocal.
|- A e. CC   =>   |- (A =/= 0 -> (A x. (1 / A)) = 1)
Theorem	recidt 4235	Multiplication of a number and its reciprocal.
|- ((A e. CC /\ A =/= 0) -> (A x. (1 / A)) = 1)
Theorem	divrec 4236	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 4237	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 4238	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	divasst 4239	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 4240	An associative/distributive law for division.
|- (((A e. CC /\ B e. CC /\ C e. CC) /\ C =/= 0) -> ((A x. B) / C) = ((A / C) x. B))
Theorem	divassz 4241	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 4242	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	divdistr 4243	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 4244	An associative/distributive law for division.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C =/= 0   =>   |- ((A x. B) / C) = ((A / C) x. B)
Theorem	divdistrz 4245	Distribution of division over addition.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- (C =/= 0 -> ((A + B) / C) = ((A / C) + (B / C)))
Theorem	divdistrt 4246	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 4247	A cancellation law for division.
|- A e. CC   &   |- B e. CC   &   |- A =/= 0   =>   |- ((A x. B) / A) = B
Theorem	divcan4 4248	A cancellation law for division.
|- A e. CC   &   |- B e. CC   &   |- A =/= 0   =>   |- ((B x. A) / A) = B
Theorem	divcan3z 4249	A cancellation law for division. (Eliminates a hypothesis of divcan3 4247 with the weak deduction theorem.)
|- A e. CC   &   |- B e. CC   =>   |- (A =/= 0 -> ((A x. B) / A) = B)
Theorem	divcan4z 4250	A cancellation law for division.
|- A e. CC   &   |- B e. CC   =>   |- (A =/= 0 -> ((B x. A) / A) = B)
Theorem	divcan3t 4251	A cancellation law for division.
|- (((A e. CC /\ B e. CC) /\ A =/= 0) -> ((A x. B) / A) = B)
Theorem	div11 4252	One-to-one relationship for division.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C =/= 0   =>   |- ((A / C) = (B / C) <-> A = B)
Theorem	recrec 4253	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