mmtheorems57 - 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-12229

Statement List for Metamath Proof Explorer - 5601-5700 - Page 57 of 123

Type	Label	Description
Statement
Theorem	mul2negi 5601	Product of two negatives. Theorem I.12 of [Apostol] p. 18.
|- A e. CC   &   |- B e. CC   =>   |- (-uA x. -uB) = (A x. B)
Theorem	negdii 5602	Distribution of negative over addition.
|- A e. CC   &   |- B e. CC   =>   |- -u(A + B) = (-uA + -uB)
Theorem	negsubdii 5603	Distribution of negative over subtraction.
|- A e. CC   &   |- B e. CC   =>   |- -u(A - B) = (-uA + B)
Theorem	negsubdi2i 5604	Distribution of negative over subtraction.
|- A e. CC   &   |- B e. CC   =>   |- -u(A - B) = (B - A)
Theorem	mulneg1 5605	Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18.
|- ((A e. CC /\ B e. CC) -> (-uA x. B) = -u(A x. B))
Theorem	mulneg2 5606	The product with a negative is the negative of the product.
|- ((A e. CC /\ B e. CC) -> (A x. -uB) = -u(A x. B))
Theorem	mulneg12 5607	Swap the negative sign in a product.
|- ((A e. CC /\ B e. CC) -> (-uA x. B) = (A x. -uB))
Theorem	mul2neg 5608	Product of two negatives. Theorem I.12 of [Apostol] p. 18.
|- ((A e. CC /\ B e. CC) -> (-uA x. -uB) = (A x. B))
Theorem	negdi 5609	Distribution of negative over addition.
|- ((A e. CC /\ B e. CC) -> -u(A + B) = (-uA + -uB))
Theorem	negdi2 5610	Distribution of negative over addition.
|- ((A e. CC /\ B e. CC) -> -u(A + B) = (-uA - B))
Theorem	negsubdi 5611	Distribution of negative over subtraction.
|- ((A e. CC /\ B e. CC) -> -u(A - B) = (-uA + B))
Theorem	negsubdi2 5612	Distribution of negative over subtraction.
|- ((A e. CC /\ B e. CC) -> -u(A - B) = (B - A))
Theorem	neg2sub 5613	Relationship between subtraction and negative. (Contributed by Paul Chapman, 8-Oct-2007.)
|- ((A e. CC /\ B e. CC) -> (-uA - -uB) = (B - A))
Theorem	submul2 5614	Convert a subtraction to addition using multiplication by a negative.
|- ((A e. CC /\ B e. CC /\ C e. CC) -> (A - (B x. C)) = (A + (B x. -uC)))
Theorem	subsub2 5615	Law for double subtraction.
|- ((A e. CC /\ B e. CC /\ C e. CC) -> (A - (B - C)) = (A + (C - B)))
Theorem	subsub 5616	Law for double subtraction.
|- ((A e. CC /\ B e. CC /\ C e. CC) -> (A - (B - C)) = ((A - B) + C))
Theorem	subsub3 5617	Law for double subtraction.
|- ((A e. CC /\ B e. CC /\ C e. CC) -> (A - (B - C)) = ((A + C) - B))
Theorem	subsub4 5618	Law for double subtraction.
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A - B) - C) = (A - (B + C)))
Theorem	sub23 5619	Swap the second and third terms in a double subtraction.
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A - B) - C) = ((A - C) - B))
Theorem	nnncan 5620	Cancellation law for subtraction.
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A - (B - C)) - C) = (A - B))
Theorem	nnncan1 5621	Cancellation law for subtraction.
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A - B) - (A - C)) = (C - B))
Theorem	nnncan2 5622	Cancellation law for subtraction.
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A - C) - (B - C)) = (A - B))
Theorem	nncan 5623	Cancellation law for subtraction.
|- ((A e. CC /\ B e. CC) -> (A - (A - B)) = B)
Theorem	nppcan2 5624	Cancellation law for subtraction.
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A - (B + C)) + C) = (A - B))
Theorem	mulm1 5625	Product with minus one is negative.
|- (A e. CC -> (-u1 x. A) = -uA)
Theorem	mulm1i 5626	Product with minus one is negative.
|- A e. CC   =>   |- (-u1 x. A) = -uA
Theorem	addsub4 5627	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	addsub4i 5628	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	subadd4 5629	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 + D) - (B + C)))
Theorem	sub4 5630	Rearrangement of 4 terms in a subtraction.
|- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> ((A - B) - (C - D)) = ((A - C) - (B - D)))
Theorem	mulsub 5631	Product of two differences.
|- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> ((A - B) x. (C - D)) = (((A x. C) + (D x. B)) - ((A x. D) + (C x. B))))
Theorem	pnpcan 5632	Cancellation law for mixed addition and subtraction.
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A + B) - (A + C)) = (B - C))
Theorem	pnpcan2 5633	Cancellation law for mixed addition and subtraction. (Contributed by Scott Fenton, 9-Jun-2006.)
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A + C) - (B + C)) = (A - B))
Theorem	pnncan 5634	Cancellation law for mixed addition and subtraction.
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A + B) - (A - C)) = (B + C))
Theorem	ppncan 5635	Cancellation law for mixed addition and subtraction.
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A + B) + (C - B)) = (A + C))
Theorem	pnncani 5636	Cancellation law for mixed addition and subtraction.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- ((A + B) - (A - C)) = (B + C)
Infinity and the extended real number system
Syntax	cpnf 5637	Plus infinity.
class +oo
Syntax	cmnf 5638	Minus infinity.
class -oo
Syntax	cxr 5639	The set of extended reals (includes plus and minus infinity).
class RR*
Syntax	clt 5640	'Less than' predicate (extended to include the extended reals).
class <
Definition	df-pnf 5641	Define plus infinity. Note that the definition is arbitrary, requiring only that +oo be a set not in RR and different from -oo (df-mnf 5642). We use P~U.CC to make it independent of the construction of CC, and Cantor's Theorem will show that it is different from any member of CC and therefore RR. See pnfnre 5650, mnfnre 5651, and pnfnemnf 5690. A simpler possibility is to define +oo as CC and -oo as {CC}, but that approach requires the Axiom of Regularity to show that +oo and -oo are different from each other and from all members of RR.
|- +oo = P~U.CC
Definition	df-mnf 5642	Define minus infinity as the power set of plus infinity. Note that the definition is arbitrary, requiring only that -oo be a set not in RR and different from +oo (see mnfnre 5651 and pnfnemnf 5690).
|- -oo = P~ +oo
Definition	df-xr 5643	Define the set of extended reals that includes plus and minus infinity. Definition 12-3.1 of [Gleason] p. 173.
|- RR* = (RR u. { +oo, -oo})
Definition	df-ltxr 5644	Define 'less than' on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. The clipping of <R makes our definition independent of the complex number construction, since the postulates don't presuppose that <R is a relation on RR.
|- < = ((( <R i^i (RR X. RR)) u. {<. -oo, +oo>.}) u. ((RR X. { +oo}) u. ({ -oo} X. RR)))
Definition	df-le 5645	Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 5672 relates it to 'less than' for reals.
|- <_ = ((RR* X. RR*) \ `' < )
Theorem	xrex 5646	The set of extended reals exists.
|- RR* e. V
Theorem	pnfxr 5647	Plus infinity belongs to the set of extended reals.
|- +oo e. RR*
Theorem	mnfxr 5648	Minus infinity belongs to the set of extended reals.
|- -oo e. RR*
Theorem	ltxr 5649	The 'less than' binary relation on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173.
|- ((A e. RR* /\ B e. RR*) -> (A < B <-> ((((A e. RR /\ B e. RR) /\ A <R B) \/ (A = -oo /\ B = +oo)) \/ ((A e. RR /\ B = +oo) \/ (A = -oo /\ B e. RR)))))
Theorem	pnfnre 5650	Plus infinity is not a real number.
|- +oo e/ RR
Theorem	mnfnre 5651	Minus infinity is not a real number.
|- -oo e/ RR
Theorem	ressxr 5652	The standard reals are a subset of the extended reals.
|- RR (_ RR*
Theorem	rexr 5653	A standard real is an extended real.
|- (A e. RR -> A e. RR*)
Theorem	ltxrlt 5654	The standard less-than <R and the extended real less-than < are identical when restricted to the non-extended reals RR.
|- ((A e. RR /\ B e. RR) -> (A < B <-> A <R B))
Theorem	xrlenlt 5655	'Less than or equal to' expressed in terms of 'less than', for extended reals.
|- ((A e. RR* /\ B e. RR*) -> (A <_ B <-> -. B < A))
Theorem	xrltnle 5656	'Less than' expressed in terms of 'less than or equal to', for extended reals.
|- ((A e. RR* /\ B e. RR*) -> (A < B <-> -. B <_ A))
Restate the ordering postulates with extended real "less than"
Theorem	axlttri 5657	Ordering on reals satisfies strict trichotomy. Axiom 22 of 27 for real and complex numbers, derived from ZF set theory. (This restates pre-axlttri 5441 with ordering on the extended reals.)
|- ((A e. RR /\ B e. RR) -> (A < B <-> -. (A = B \/ B < A)))
Theorem	axlttrn 5658	Ordering on reals is transitive. Axiom 23 of 27 for real and complex numbers, derived from ZF set theory. (This restates pre-axlttrn 5442 with ordering on the extended reals.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A < B /\ B < C) -> A < C))
Theorem	axltadd 5659	Ordering property of addition on reals. Axiom 24 of 27 for real and complex numbers, derived from ZF set theory. (This restates pre-axltadd 5443 with ordering on the extended reals.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A < B -> (C + A) < (C + B)))
Theorem	axmulgt0 5660	The product of two positive reals is positive. Axiom 25 of 27 for real and complex numbers, derived from ZF set theory. (This restates pre-axmulgt0 5444 with ordering on the extended reals.)
|- ((A e. RR /\ B e. RR) -> ((0 < A /\ 0 < B) -> 0 < (A x. B)))
Theorem	axsup 5661	A non-empty, bounded-above set of reals has a supremum. Axiom 27 of 27 for real and complex numbers, derived from ZF set theory. (This restates pre-axsup 5445 with ordering on the extended reals.)
|- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A y < x) -> E.x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)))
Ordering on reals
Theorem	lttr 5662	Alias for axlttrn 5658, for naming consistency with lttri 5739.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A < B /\ B < C) -> A < C))
Theorem	mulgt0 5663	The product of two positive numbers is positive.
|- (((A e. RR /\ 0 < A) /\ (B e. RR /\ 0 < B)) -> 0 < (A x. B))
Theorem	lenlt 5664	'Less than or equal to' expressed in terms of 'less than'.
|- ((A e. RR /\ B e. RR) -> (A <_ B <-> -. B < A))
Theorem	ltnle 5665	'Less than' expressed in terms of 'less than or equal to'.
|- ((A e. RR /\ B e. RR) -> (A < B <-> -. B <_ A))
Theorem	ltso 5666	'Less than' is a strict ordering. Note: do not shorten this with ltsor 5415, and do not use ltsor 5415 in complex number proofs, in order to maintain a portable derivation of all complex number proofs directly from postulates.
|- < Or RR
Theorem	lttri2 5667	Consequence of trichotomy.
|- ((A e. RR /\ B e. RR) -> (A =/= B <-> (A < B \/ B < A)))
Theorem	lttri3 5668	Trichotomy law for 'less than'.
|- ((A e. RR /\ B e. RR) -> (A = B <-> (-. A < B /\ -. B < A)))
Theorem	lttri4 5669	Trichotomy law for 'less than'.
|- ((A e. RR /\ B e. RR) -> (A < B \/ A = B \/ B < A))
Theorem	ltne 5670	'Less than' implies not equal.
|- ((A e. RR /\ B e. RR /\ A < B) -> B =/= A)
Theorem	letri3 5671	Trichotomy law.
|- ((A e. RR /\ B e. RR) -> (A = B <-> (A <_ B /\ B <_ A)))
Theorem	leloe 5672	'Less than or equal to' expressed in terms of 'less than' or 'equals'.
|- ((A e. RR /\ B e. RR) -> (A <_ B <-> (A < B \/ A = B)))
Theorem	eqlelt 5673	Equality in terms of 'less than or equal to', 'less than'.
|- ((A e. RR /\ B e. RR) -> (A = B <-> (A <_ B /\ -. A < B)))
Theorem	ltle 5674	'Less than' implies 'less than or equal to'.
|- ((A e. RR /\ B e. RR) -> (A < B -> A <_ B))
Theorem	leltne 5675	'Less than or equal to' implies 'less than' is not 'equals'.
|- ((A e. RR /\ B e. RR /\ A <_ B) -> (A < B <-> B =/= A))
Theorem	ltlen 5676	'Less than' expressed in terms of 'less than or equal to'.
|- ((A e. RR /\ B e. RR) -> (A < B <-> (A <_ B /\ B =/= A)))
Theorem	lelttr 5677	Transitive law.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A <_ B /\ B < C) -> A < C))
Theorem	ltletr 5678	Transitive law.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A < B /\ B <_ C) -> A < C))
Theorem	letr 5679	Transitive law.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A <_ B /\ B <_ C) -> A <_ C))
Theorem	letrd 5680	Transitive law deduction for 'less than or equal to'.
|- (ph -> A e. RR)   &   |- (ph -> B e. RR)   &   |- (ph -> C e. RR)   &   |- (ph -> A <_ B)   &   |- (ph -> B <_ C)   =>   |- (ph -> A <_ C)
Theorem	lelttrd 5681	Transitive law deduction for 'less than or equal to', 'less than'.
|- (ph -> A e. RR)   &   |- (ph -> B e. RR)   &   |- (ph -> C e. RR)   &   |- (ph -> A <_ B)   &   |- (ph -> B < C)   =>   |- (ph -> A < C)
Theorem	ltletrd 5682	Transitive law deduction for 'less than', 'less than or equal to'.
|- (ph -> A e. RR)   &   |- (ph -> B e. RR)   &   |- (ph -> C e. RR)   &   |- (ph -> A < B)   &   |- (ph -> B <_ C)   =>   |- (ph -> A < C)
Theorem	lttrd 5683	Transitive law deduction for 'less than'.
|- (ph -> A e. RR)   &   |- (ph -> B e. RR)   &   |- (ph -> C e. RR)   &   |- (ph -> A < B)   &   |- (ph -> B < C)   =>   |- (ph -> A < C)
Theorem	ltnr 5684	'Less than' is irreflexive.
|- (A e. RR -> -. A < A)
Theorem	leid 5685	'Less than or equal to' is reflexive.
|- (A e. RR -> A <_ A)
Theorem	ltnsym 5686	'Less than' is not symmetric.
|- ((A e. RR /\ B e. RR) -> (A < B -> -. B < A))
Theorem	ltnsym2 5687	'Less than' is antisymmetric and irreflexive.
|- ((A e. RR /\ B e. RR) -> -. (A < B /\ B < A))
Theorem	pm2.61ltlei 5688	Ordering elimination by cases.
|- ((ph /\ A < B) -> ps)   &   |- ((ph /\ B <_ A) -> ps)   &   |- (ph -> A e. RR)   &   |- (ph -> B e. RR)   =>   |- (ph -> ps)
Ordering on the extended reals
Theorem	elxr 5689	Membership in the set of extended reals.
|- (A e. RR* <-> (A e. RR \/ A = +oo \/ A = -oo))
Theorem	pnfnemnf 5690	Plus and minus infinity are distinguished elements of RR*.
|- +oo =/= -oo
Theorem	renepnf 5691	No (finite) real equals plus infinity.
|- (A e. RR -> A =/= +oo)
Theorem	renemnf 5692	No real equals minus infinity.
|- (A e. RR -> A =/= -oo)
Theorem	renfdisj 5693	The reals and the infinities are disjoint.
|- (RR i^i { +oo, -oo}) = (/)
Theorem	ssxr 5694	The three (non-exclusive) possibilities implied by a subset of extended reals.
|- (A (_ RR* -> (A (_ RR \/ +oo e. A \/ -oo e. A))
Theorem	xrltnr 5695	The extended real 'less than' is irreflexive.
|- (A e. RR* -> -. A < A)
Theorem	ltpnf 5696	Any (finite) real is less than plus infinity.
|- (A e. RR -> A < +oo)
Theorem	mnflt 5697	Minus infinity is less than any (finite) real.
|- (A e. RR -> -oo < A)
Theorem	mnfltpnf 5698	Minus infinity is less than plus infinity.
|- -oo < +oo
Theorem	mnfltxr 5699	Minus infinity is less than an extended real that is either real or plus infinity.
|- ((A e. RR \/ A = +oo) -> -oo < A)
Theorem	pnfnlt 5700	No extended real is greater than plus infinity.
|- (A e. RR* -> -. +oo < A)