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-10700 108 10701-10722

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

Type	Label	Description
Statement
Ordering on reals
Theorem	lttrt 5501	Alias for axlttrn 5497, for naming consistency with lttr 5578.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A < B /\ B < C) -> A < C))
Theorem	mulgt0t 5502	Alias for axmulgt0 5499, for naming consistency with mulgt0 5599.
|- ((A e. RR /\ B e. RR) -> ((0 < A /\ 0 < B) -> 0 < (A x. B)))
Theorem	lenltt 5503	'Less than or equal to' expressed in terms of 'less than'.
|- ((A e. RR /\ B e. RR) -> (A <_ B <-> -. B < A))
Theorem	ltnlet 5504	'Less than' expressed in terms of 'less than or equal to'.
|- ((A e. RR /\ B e. RR) -> (A < B <-> -. B <_ A))
Theorem	ltso 5505	'Less than' is a strict ordering. Note: do not shorten this with ltsor 5254, and do not use ltsor 5254 in complex number proofs, in order to maintain a portable derivation of all complex number proofs directly from postulates.
|- < Or RR
Theorem	lttri2t 5506	Consequence of trichotomy.
|- ((A e. RR /\ B e. RR) -> (A =/= B <-> (A < B \/ B < A)))
Theorem	lttri3t 5507	Trichotomy law for 'less than'.
|- ((A e. RR /\ B e. RR) -> (A = B <-> (-. A < B /\ -. B < A)))
Theorem	lttri4t 5508	Trichotomy law for 'less than'.
|- ((A e. RR /\ B e. RR) -> (A < B \/ A = B \/ B < A))
Theorem	ltnet 5509	'Less than' implies not equal.
|- ((A e. RR /\ B e. RR /\ A < B) -> B =/= A)
Theorem	letri3t 5510	Trichotomy law.
|- ((A e. RR /\ B e. RR) -> (A = B <-> (A <_ B /\ B <_ A)))
Theorem	leloet 5511	'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	eqleltt 5512	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 5513	'Less than' implies 'less than or equal to'.
|- ((A e. RR /\ B e. RR) -> (A < B -> A <_ B))
Theorem	leltnet 5514	'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 5515	'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 5516	Transitive law.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A <_ B /\ B < C) -> A < C))
Theorem	ltletrt 5517	Transitive law.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A < B /\ B <_ C) -> A < C))
Theorem	letrt 5518	Transitive law.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A <_ B /\ B <_ C) -> A <_ C))
Theorem	letrd 5519	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 5520	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 5521	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 5522	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 5523	'Less than' is irreflexive.
|- (A e. RR -> -. A < A)
Theorem	leidt 5524	'Less than or equal to' is reflexive.
|- (A e. RR -> A <_ A)
Theorem	ltnsymt 5525	'Less than' is not symmetric.
|- ((A e. RR /\ B e. RR) -> (A < B -> -. B < A))
Theorem	ltnsym2t 5526	'Less than' is antisymmetric and irreflexive.
|- ((A e. RR /\ B e. RR) -> -. (A < B /\ B < A))
Theorem	pm2.61ltle 5527	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 5528	Membership in the set of extended reals.
|- (A e. RR* <-> (A e. RR \/ A = +oo \/ A = -oo))
Theorem	pnfnemnf 5529	Plus and minus infinity are distinguished elements of RR*.
|- +oo =/= -oo
Theorem	renepnft 5530	No (finite) real equals plus infinity.
|- (A e. RR -> A =/= +oo)
Theorem	renemnft 5531	No real equals minus infinity.
|- (A e. RR -> A =/= -oo)
Theorem	renfdisj 5532	The reals and the infinities are disjoint.
|- (RR i^i { +oo, -oo}) = (/)
Theorem	ssxr 5533	The three (non-exclusive) possibilities implied by a subset of extended reals.
|- (A (_ RR* -> (A (_ RR \/ +oo e. A \/ -oo e. A))
Theorem	xrltnrt 5534	The extended real 'less than' is irreflexive.
|- (A e. RR* -> -. A < A)
Theorem	ltpnft 5535	Any (finite) real is less than plus infinity.
|- (A e. RR -> A < +oo)
Theorem	mnfltt 5536	Minus infinity is less than any (finite) real.
|- (A e. RR -> -oo < A)
Theorem	mnfltpnf 5537	Minus infinity is less than plus infinity.
|- -oo < +oo
Theorem	mnfltxrt 5538	Minus infinity is less than an extended real that is either real or plus infinity.
|- ((A e. RR \/ A = +oo) -> -oo < A)
Theorem	pnfnltt 5539	No extended real is greater than plus infinity.
|- (A e. RR* -> -. +oo < A)
Theorem	nltmnft 5540	No extended real is less than minus infinity.
|- (A e. RR* -> -. A < -oo)
Theorem	pnfget 5541	Plus infinity is an upper bound for extended reals.
|- (A e. RR* -> A <_ +oo)
Theorem	mnflet 5542	Minus infinity is less than or equal to any extended real.
|- (A e. RR* -> -oo <_ A)
Theorem	xrltnsymt 5543	Ordering on the extended reals is not symmetric.
|- ((A e. RR* /\ B e. RR*) -> (A < B -> -. B < A))
Theorem	xrltnsym2t 5544	'Less than' is antisymmetric and irreflexive for extended reals.
|- ((A e. RR* /\ B e. RR*) -> -. (A < B /\ B < A))
Theorem	xrlttrit 5545	Ordering on the extended reals satisfies strict trichotomy.
|- ((A e. RR* /\ B e. RR*) -> (A < B <-> -. (A = B \/ B < A)))
Theorem	xrlttrt 5546	Ordering on the extended reals is transitive.
|- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> ((A < B /\ B < C) -> A < C))
Theorem	xrltso 5547	'Less than' is a strict ordering on the extended reals.
|- < Or RR*
Theorem	xrlttri2t 5548	Trichotomy law for 'less than' for extended reals.
|- ((A e. RR* /\ B e. RR*) -> (A =/= B <-> (A < B \/ B < A)))
Theorem	xrlttri3t 5549	Trichotomy law for 'less than' for extended reals.
|- ((A e. RR* /\ B e. RR*) -> (A = B <-> (-. A < B /\ -. B < A)))
Theorem	xrleloet 5550	'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 5551	'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 5552	'Less than' implies 'less than or equal' for extended reals.
|- ((A e. RR* /\ B e. RR*) -> (A < B -> A <_ B))
Theorem	xrleidt 5553	'Less than or equal to' is reflexive for extended reals.
|- (A e. RR* -> A <_ A)
Theorem	xrletrit 5554	Trichotomy law for extended reals.
|- ((A e. RR* /\ B e. RR*) -> (A <_ B \/ B <_ A))
Theorem	xrlelttrt 5555	Transitive law for ordering on extended reals.
|- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> ((A <_ B /\ B < C) -> A < C))
Theorem	xrltletrt 5556	Transitive law for ordering on extended reals.
|- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> ((A < B /\ B <_ C) -> A < C))
Theorem	xrletrt 5557	Transitive law for ordering on extended reals.
|- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> ((A <_ B /\ B <_ C) -> A <_ C))
Theorem	xrltnet 5558	'Less than' implies not equal for extended reals.
|- ((A e. RR* /\ B e. RR* /\ A < B) -> B =/= A)
Theorem	nltpnftt 5559	An extended real is not less than plus infinity iff they are equal.
|- (A e. RR* -> (A = +oo <-> -. A < +oo))
Theorem	ngtmnftt 5560	An extended real is not greater than minus infinity iff they are equal.
|- (A e. RR* -> (A = -oo <-> -. -oo < A))
Theorem	xrrebndt 5561	An extended real is real iff it is strictly bounded by infinities.
|- (A e. RR* -> (A e. RR <-> ( -oo < A /\ A < +oo)))
Theorem	xrret 5562	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 5563	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 5564	Equality implies 'less than or equal to'.
|- ((A e. RR /\ A = B) -> A <_ B)
Theorem	lttri2 5565	Consequence of trichotomy.
|- A e. RR   &   |- B e. RR   =>   |- (A =/= B <-> (A < B