mmtheorems56 - 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-10658

Statement List for Metamath Proof Explorer - 5501-5600 - Page 56 of 107

Type	Label	Description
Statement
Theorem	eqleltt 5501	Equality in terms of 'less than or equal to', 'less than'.
|- ((A e. RR /\ B e. RR) -> (A = B <-> (A <_ B /\ -. A < B)))
Theorem	ltlet 5502	'Less than' implies 'less than or equal to'.
|- ((A e. RR /\ B e. RR) -> (A < B -> A <_ B))
Theorem	leltnet 5503	'Less than or equal to' implies 'less than' is not 'equals'.
|- ((A e. RR /\ B e. RR /\ A <_ B) -> (A < B <-> B =/= A))
Theorem	ltlent 5504	'Less than' expressed in terms of 'less than or equal to'.
|- ((A e. RR /\ B e. RR) -> (A < B <-> (A <_ B /\ B =/= A)))
Theorem	lelttrt 5505	Transitive law.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A <_ B /\ B < C) -> A < C))
Theorem	ltletrt 5506	Transitive law.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A < B /\ B <_ C) -> A < C))
Theorem	letrt 5507	Transitive law.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A <_ B /\ B <_ C) -> A <_ C))
Theorem	letrd 5508	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 5509	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 5510	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 5511	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	ltnrt 5512	'Less than' is irreflexive.
|- (A e. RR -> -. A < A)
Theorem	leidt 5513	'Less than or equal to' is reflexive.
|- (A e. RR -> A <_ A)
Theorem	ltnsymt 5514	'Less than' is not symmetric.
|- ((A e. RR /\ B e. RR) -> (A < B -> -. B < A))
Theorem	ltnsym2t 5515	'Less than' is antisymmetric and irreflexive.
|- ((A e. RR /\ B e. RR) -> -. (A < B /\ B < A))
Theorem	pm2.61ltle 5516	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 5517	Membership in the set of extended reals.
|- (A e. RR* <-> (A e. RR \/ A = +oo \/ A = -oo))
Theorem	pnfnemnf 5518	Plus and minus infinity are distinguished elements of RR*.
|- +oo =/= -oo
Theorem	renepnft 5519	No (finite) real equals plus infinity.
|- (A e. RR -> A =/= +oo)
Theorem	renemnft 5520	No real equals minus infinity.
|- (A e. RR -> A =/= -oo)
Theorem	renfdisj 5521	The reals and the infinities are disjoint.
|- (RR i^i { +oo, -oo}) = (/)
Theorem	ssxr 5522	The three (non-exclusive) possibilities implied by a subset of extended reals.
|- (A (_ RR* -> (A (_ RR \/ +oo e. A \/ -oo e. A))
Theorem	xrltnrt 5523	The extended real 'less than' is irreflexive.
|- (A e. RR* -> -. A < A)
Theorem	ltpnft 5524	Any (finite) real is less than plus infinity.
|- (A e. RR -> A < +oo)
Theorem	mnfltt 5525	Minus infinity is less than any (finite) real.
|- (A e. RR -> -oo < A)
Theorem	mnfltpnf 5526	Minus infinity is less than plus infinity.
|- -oo < +oo
Theorem	mnfltxrt 5527	Minus infinity is less than an extended real that is either real or plus infinity.
|- ((A e. RR \/ A = +oo) -> -oo < A)
Theorem	pnfnltt 5528	No extended real is greater than plus infinity.
|- (A e. RR* -> -. +oo < A)
Theorem	nltmnft 5529	No extended real is less than minus infinity.
|- (A e. RR* -> -. A < -oo)
Theorem	pnfget 5530	Plus infinity is an upper bound for extended reals.
|- (A e. RR* -> A <_ +oo)
Theorem	mnflet 5531	Minus infinity is less than or equal to any extended real.
|- (A e. RR* -> -oo <_ A)
Theorem	xrltnsymt 5532	Ordering on the extended reals is not symmetric.
|- ((A e. RR* /\ B e. RR*) -> (A < B -> -. B < A))
Theorem	xrltnsym2t 5533	'Less than' is antisymmetric and irreflexive for extended reals.
|- ((A e. RR* /\ B e. RR*) -> -. (A < B /\ B < A))
Theorem	xrlttrit 5534	Ordering on the extended reals satisfies strict trichotomy.
|- ((A e. RR* /\ B e. RR*) -> (A < B <-> -. (A = B \/ B < A)))
Theorem	xrlttrt 5535	Ordering on the extended reals is transitive.
|- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> ((A < B /\ B < C) -> A < C))
Theorem	xrltso 5536	'Less than' is a strict ordering on the extended reals.
|- < Or RR*
Theorem	xrlttri2t 5537	Trichotomy law for 'less than' for extended reals.
|- ((A e. RR* /\ B e. RR*) -> (A =/= B <-> (A < B \/ B < A)))
Theorem	xrlttri3t 5538	Trichotomy law for 'less than' for extended reals.
|- ((A e. RR* /\ B e. RR*) -> (A = B <-> (-. A < B /\ -. B < A)))
Theorem	xrleloet 5539	'Less than or equal' expressed in terms of 'less than' or 'equals', for extended reals.
|- ((A e. RR* /\ B e. RR*) -> (A <_ B <-> (A < B \/ A = B)))
Theorem	xrleltnet 5540	'Less than or equal to' implies 'less than' is not 'equals', for extended reals.
|- ((A e. RR* /\ B e. RR* /\ A <_ B) -> (A < B <-> B =/= A))
Theorem	xrltlet 5541	'Less than' implies 'less than or equal' for extended reals.
|- ((A e. RR* /\ B e. RR*) -> (A < B -> A <_ B))
Theorem	xrleidt 5542	'Less than or equal to' is reflexive for extended reals.
|- (A e. RR* -> A <_ A)
Theorem	xrletrit 5543	Trichotomy law for extended reals.
|- ((A e. RR* /\ B e. RR*) -> (A <_ B \/ B <_ A))
Theorem	xrlelttrt 5544	Transitive law for ordering on extended reals.
|- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> ((A <_ B /\ B < C) -> A < C))
Theorem	xrltletrt 5545	Transitive law for ordering on extended reals.
|- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> ((A < B /\ B <_ C) -> A < C))
Theorem	xrletrt 5546	Transitive law for ordering on extended reals.
|- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> ((A <_ B /\ B <_ C) -> A <_ C))
Theorem	xrltnet 5547	'Less than' implies not equal for extended reals.
|- ((A e. RR* /\ B e. RR* /\ A < B) -> B =/= A)
Theorem	nltpnftt 5548	An extended real is not less than plus infinity iff they are equal.
|- (A e. RR* -> (A = +oo <-> -. A < +oo))
Theorem	ngtmnftt 5549	An extended real is not greater than minus infinity iff they are equal.
|- (A e. RR* -> (A = -oo <-> -. -oo < A))
Theorem	xrrebndt 5550	An extended real is real iff it is strictly bounded by infinities.
|- (A e. RR* -> (A e. RR <-> ( -oo < A /\ A < +oo)))
Theorem	xrret 5551	A way of proving that an extended real is real.
|- (((A e. RR* /\ B e. RR) /\ ( -oo < A /\ A <_ B)) -> A e. RR)
Theorem	xrre2t 5552	An extended real between two others is real.
|- (((A e. RR* /\ B e. RR* /\ C e. RR*) /\ (A < B /\ B < C)) -> B e. RR)
Ordering on reals (cont.)
Theorem	eqlet 5553	Equality implies 'less than or equal to'.
|- ((A e. RR /\ A = B) -> A <_ B)
Theorem	lttri2 5554	Consequence of trichotomy.
|- A e. RR   &   |- B e. RR   =>   |- (A =/= B <-> (A < B \/ B < A))
Theorem	lttri3 5555	Consequence of trichotomy.
|- A e. RR   &   |- B e. RR   =>   |- (A = B <-> (-. A < B /\ -. B < A))
Theorem	letri3 5556	Consequence of trichotomy.
|- A e. RR   &   |- B e. RR   =>   |- (A = B <-> (A <_ B /\ B <_ A))
Theorem	leloe 5557	'Less than or equal to' in terms of 'less than'.
|- A e. RR   &   |- B e. RR   =>   |- (A <_ B <-> (A < B \/ A = B))
Theorem	ltlen 5558	'Less than' expressed in terms of 'less than or equal to'.
|- A e. RR   &   |- B e. RR   =>   |- (A < B <-> (A <_ B /\ B =/= A))
Theorem	ltnsym 5559	'Less than' is not symmetric.
|- A e. RR   &   |- B e. RR   =>   |- (A < B -> -. B < A)
Theorem	lenlt 5560	'Less than or equal to' in terms of 'less than'.
|- A e. RR   &   |- B e. RR   =>   |- (A <_ B <-> -. B < A)
Theorem	ltnle 5561	'Less than' in terms of 'less than or equal to'.
|- A e. RR   &   |- B e. RR   =>   |- (A < B <-> -. B <_ A)
Theorem	ltle 5562	'Less than' implies 'less than or equal to'.
|- A e. RR   &   |- B e. RR   =>   |- (A < B -> A <_ B)
Theorem	ltlei 5563	'Less than' implies 'less than or equal to' (inference).
|- A e. RR   &   |- B e. RR   &   |- A < B   =>   |- A <_ B
Theorem	eqle 5564	Equality implies 'less than or equal to'.
|- A e. RR   &   |- B e. RR   =>   |- (A = B -> A <_ B)
Theorem	ltne 5565	'Less than' implies not equal.
|- A e. RR   &   |- B e. RR   =>   |- (A < B -> B =/= A)
Theorem	ltneOLD 5566	'Less than' implies not equal.
|- A e. RR   &   |- B e. RR   =>   |- (A