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-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 - 5701-5800 - Page 58 of 123

Type	Label	Description
Statement
Theorem	nltmnf 5701	No extended real is less than minus infinity.
|- (A e. RR* -> -. A < -oo)
Theorem	pnfge 5702	Plus infinity is an upper bound for extended reals.
|- (A e. RR* -> A <_ +oo)
Theorem	mnfle 5703	Minus infinity is less than or equal to any extended real.
|- (A e. RR* -> -oo <_ A)
Theorem	xrltnsym 5704	Ordering on the extended reals is not symmetric.
|- ((A e. RR* /\ B e. RR*) -> (A < B -> -. B < A))
Theorem	xrltnsym2 5705	'Less than' is antisymmetric and irreflexive for extended reals.
|- ((A e. RR* /\ B e. RR*) -> -. (A < B /\ B < A))
Theorem	xrlttri 5706	Ordering on the extended reals satisfies strict trichotomy.
|- ((A e. RR* /\ B e. RR*) -> (A < B <-> -. (A = B \/ B < A)))
Theorem	xrlttr 5707	Ordering on the extended reals is transitive.
|- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> ((A < B /\ B < C) -> A < C))
Theorem	xrltso 5708	'Less than' is a strict ordering on the extended reals.
|- < Or RR*
Theorem	xrlttri2 5709	Trichotomy law for 'less than' for extended reals.
|- ((A e. RR* /\ B e. RR*) -> (A =/= B <-> (A < B \/ B < A)))
Theorem	xrlttri3 5710	Trichotomy law for 'less than' for extended reals.
|- ((A e. RR* /\ B e. RR*) -> (A = B <-> (-. A < B /\ -. B < A)))
Theorem	xrleloe 5711	'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	xrleltne 5712	'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	xrltle 5713	'Less than' implies 'less than or equal' for extended reals.
|- ((A e. RR* /\ B e. RR*) -> (A < B -> A <_ B))
Theorem	xrleid 5714	'Less than or equal to' is reflexive for extended reals.
|- (A e. RR* -> A <_ A)
Theorem	xrletri 5715	Trichotomy law for extended reals.
|- ((A e. RR* /\ B e. RR*) -> (A <_ B \/ B <_ A))
Theorem	xrlelttr 5716	Transitive law for ordering on extended reals.
|- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> ((A <_ B /\ B < C) -> A < C))
Theorem	xrltletr 5717	Transitive law for ordering on extended reals.
|- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> ((A < B /\ B <_ C) -> A < C))
Theorem	xrletr 5718	Transitive law for ordering on extended reals.
|- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> ((A <_ B /\ B <_ C) -> A <_ C))
Theorem	xrltne 5719	'Less than' implies not equal for extended reals.
|- ((A e. RR* /\ B e. RR* /\ A < B) -> B =/= A)
Theorem	nltpnft 5720	An extended real is not less than plus infinity iff they are equal.
|- (A e. RR* -> (A = +oo <-> -. A < +oo))
Theorem	ngtmnft 5721	An extended real is not greater than minus infinity iff they are equal.
|- (A e. RR* -> (A = -oo <-> -. -oo < A))
Theorem	xrrebnd 5722	An extended real is real iff it is strictly bounded by infinities.
|- (A e. RR* -> (A e. RR <-> ( -oo < A /\ A < +oo)))
Theorem	xrre 5723	A way of proving that an extended real is real.
|- (((A e. RR* /\ B e. RR) /\ ( -oo < A /\ A <_ B)) -> A e. RR)
Theorem	xrre2 5724	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	eqle 5725	Equality implies 'less than or equal to'.
|- ((A e. RR /\ A = B) -> A <_ B)
Theorem	lttri2i 5726	Consequence of trichotomy.
|- A e. RR   &   |- B e. RR   =>   |- (A =/= B <-> (A < B \/ B < A))
Theorem	lttri3i 5727	Consequence of trichotomy.
|- A e. RR   &   |- B e. RR   =>   |- (A = B <-> (-. A < B /\ -. B < A))
Theorem	letri3i 5728	Consequence of trichotomy.
|- A e. RR   &   |- B e. RR   =>   |- (A = B <-> (A <_ B /\ B <_ A))
Theorem	leloei 5729	'Less than or equal to' in terms of 'less than'.
|- A e. RR   &   |- B e. RR   =>   |- (A <_ B <-> (A < B \/ A = B))
Theorem	ltleni 5730	'Less than' expressed in terms of 'less than or equal to'.
|- A e. RR   &   |- B e. RR   =>   |- (A < B <-> (A <_ B /\ B =/= A))
Theorem	ltnsymi 5731	'Less than' is not symmetric.
|- A e. RR   &   |- B e. RR   =>   |- (A < B -> -. B < A)
Theorem	lenlti 5732	'Less than or equal to' in terms of 'less than'.
|- A e. RR   &   |- B e. RR   =>   |- (A <_ B <-> -. B < A)
Theorem	ltnlei 5733	'Less than' in terms of 'less than or equal to'.
|- A e. RR   &   |- B e. RR   =>   |- (A < B <-> -. B <_ A)
Theorem	ltlei 5734	'Less than' implies 'less than or equal to'.
|- A e. RR   &   |- B e. RR   =>   |- (A < B -> A <_ B)
Theorem	ltleii 5735	'Less than' implies 'less than or equal to' (inference).
|- A e. RR   &   |- B e. RR   &   |- A < B   =>   |- A <_ B
Theorem	eqlei 5736	Equality implies 'less than or equal to'.
|- A e. RR   &   |- B e. RR   =>   |- (A = B -> A <_ B)
Theorem	ltnei 5737	'Less than' implies not equal.
|- A e. RR   &   |- B e. RR   =>   |- (A < B -> B =/= A)
Theorem	letrii 5738	Trichotomy law for 'less than or equal to'.
|- A e. RR   &   |- B e. RR   =>   |- (A <_ B \/ B <_ A)
Theorem	lttri 5739	'Less than' is transitive. Theorem I.17 of [Apostol] p. 20.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- ((A < B /\ B < C) -> A < C)
Theorem	lelttri 5740	'Less than or equal to', 'less than' transitive law.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- ((A <_ B /\ B < C) -> A < C)
Theorem	ltletri 5741	'Less than', 'less than or equal to' transitive law.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- ((A < B /\ B <_ C) -> A < C)
Theorem	letri 5742	'Less than or equal to' is transitive.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- ((A <_ B /\ B <_ C) -> A <_ C)
Theorem	le2tri3i 5743	Extended trichotomy law for 'less than or equal to'.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- ((A <_ B /\ B <_ C /\ C <_ A) <-> (A = B /\ B = C /\ C = A))
Theorem	ltadd2i 5744	Addition to both sides of 'less than'. (Proof shortened by Paul Chapman, 27-Jan-2008.)
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- (A < B <-> (C + A) < (C + B))
Theorem	ltadd1i 5745	Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- (A < B <-> (A + C) < (B + C))
Theorem	leadd1i 5746	Addition to both sides of 'less than or equal to'.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- (A <_ B <-> (A + C) <_ (B + C))
Theorem	leadd2i 5747	Addition to both sides of 'less than or equal to'.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- (A <_ B <-> (C + A) <_ (C + B))
Theorem	ltsubaddi 5748	'Less than' relationship between subtraction and addition.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- ((A - B) < C <-> A < (C + B))
Theorem	lesubaddi 5749	'Less than or equal to' relationship between subtraction and addition.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- ((A - B) <_ C <-> A <_ (C + B))
Theorem	lt2addi 5750	Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   &   |- D e. RR   =>   |- ((A < C /\ B < D) -> (A + B) < (C + D))
Theorem	le2addi 5751	Adding both side of two inequalities.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   &   |- D e. RR   =>   |- ((A <_ C /\ B <_ D) -> (A + B) <_ (C + D))
Theorem	addgt0i 5752	Addition of 2 positive numbers is positive.
|- A e. RR   &   |- B e. RR   =>   |- ((0 < A /\ 0 < B) -> 0 < (A + B))
Theorem	addge0i 5753	Addition of 2 nonnegative numbers is nonnegative.
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ 0 <_ B) -> 0 <_ (A + B))
Theorem	addgegt0i 5754	Addition of nonnegative and positive numbers is positive.
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ 0 < B) -> 0 < (A + B))
Theorem	addgt0ii 5755	Addition of 2 positive numbers is positive.
|- A e. RR   &   |- B e. RR   &   |- 0 < A   &   |- 0 < B   =>   |- 0 < (A + B)
Theorem	add20i 5756	Two nonnegative numbers are zero iff their sum is zero.
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ 0 <_ B) -> ((A + B) = 0 <-> (A = 0 /\ B = 0)))
Theorem	ltnegi 5757	Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
|- A e. RR   &   |- B e. RR   =>   |- (A < B <-> -uB < -uA)
Theorem	lenegi 5758	Negative of both sides of 'less than or equal to'.
|- A e. RR   &   |- B e. RR   =>   |- (A <_ B <-> -uB <_ -uA)
Theorem	ltnegcon2i 5759	Contraposition of negative in 'less than'.
|- A e. RR   &   |- B e. RR   =>   |- (A < -uB <-> B < -uA)
Theorem	mulgt0i 5760	The product of two positive numbers is positive.
|- A e. RR   &   |- B e. RR   =>   |- ((0 < A /\ 0 < B) -> 0 < (A x. B))
Theorem	mulge0i 5761	The product of two nonnegative numbers is nonnegative.
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ 0 <_ B) -> 0 <_ (A x. B))
Theorem	mulgt0ii 5762	The product of two positive numbers is positive.
|- A e. RR   &   |- B e. RR   &   |- 0 < A   &   |- 0 < B   =>   |- 0 < (A x. B)
Theorem	ltnri 5763	'Less than' is irreflexive.
|- A e. RR   =>   |- -. A < A
Theorem	leidi 5764	'Less than or equal to' is reflexive.
|- A e. RR   =>   |- A <_ A
Theorem	gt0ne0i 5765	Positive means non-zero (useful for ordering theorems involving division).
|- A e. RR   =>   |- (0 < A -> A =/= 0)
Theorem	lesub0i 5766	Lemma to show a nonnegative number is zero.
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ B <_ (B - A)) <-> A = 0)
Theorem	msqgt0i 5767	A non-zero square is positive. Theorem I.20 of [Apostol] p. 20.
|- A e. RR   =>   |- (A =/= 0 -> 0 < (A x. A))
Theorem	msqge0i 5768	A square is nonnegative.
|- A e. RR   =>   |- 0 <_ (A x. A)
Theorem	msqgt0 5769	A non-zero square is positive. Theorem I.20 of [Apostol] p. 20.
|- ((A e. RR /\ A =/= 0) -> 0 < (A x. A))
Theorem	msqge0 5770	A square is nonnegative.
|- (A e. RR -> 0 <_ (A x. A))
Theorem	gt0ne0ii 5771	Positive implies nonzero.
|- A e. RR   &   |- 0 < A   =>   |- A =/= 0
Theorem	gt0ne0 5772	Positive implies nonzero.
|- ((A e. RR /\ 0 < A) -> A =/= 0)
Theorem	ne0gt0 5773	A nonzero nonnegative number is positive.
|- ((A e. RR /\ 0 <_ A) -> (A =/= 0 <-> 0 < A))
Theorem	letric 5774	Trichotomy law.
|- ((A e. RR /\ B e. RR) -> (A <_ B \/ B <_ A))
Theorem	lecasei 5775	Ordering elimination by cases.
|- (ph -> A e. RR)   &   |- (ph -> B e. RR)   &   |- ((ph /\ A <_ B) -> ps)   &   |- ((ph /\ B <_ A) -> ps)   =>   |- (ph -> ps)
Theorem	lelttric 5776	Trichotomy law.
|- ((A e. RR /\ B e. RR) -> (A <_ B \/ B < A))
Theorem	ltadd1 5777	Addition to both sides of 'less than'.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A < B <-> (A + C) < (B + C)))
Theorem	ltadd2 5778	Addition to both sides of 'less than'.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A < B <-> (C + A) < (C + B)))
Theorem	leadd1 5779	Addition to both sides of 'less than or equal to'.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A <_ B <-> (A + C) <_ (B + C)))
Theorem	leadd2 5780	Addition to both sides of 'less than or equal to'.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A <_ B <-> (C + A) <_ (C + B)))
Theorem	ltsubadd 5781	'Less than' relationship between subtraction and addition.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A - B) < C <-> A < (C + B)))
Theorem	ltsubadd2 5782	'Less than' relationship between subtraction and addition.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A - B) < C <-> A < (B + C)))
Theorem	lesubadd 5783	'Less than or equal to' relationship between subtraction and addition.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A - B) <_ C <-> A <_ (C + B)))
Theorem	lesubadd2 5784	'Less than or equal to' relationship between subtraction and addition.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A - B) <_ C <-> A <_ (B + C)))
Theorem	ltaddsub 5785	'Less than' relationship between addition and subtraction.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A + B) < C <-> A < (C - B)))
Theorem	ltaddsub2 5786	'Less than' relationship between addition and subtraction.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A + B) < C <-> B < (C - A)))
Theorem	leaddsub 5787	'Less than or equal to' relationship between addition and subtraction.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A + B) <_ C <-> A <_ (C - B)))
Theorem	leaddsub2 5788	'Less than or equal to' relationship between and addition and subtraction.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A + B) <_ C <-> B <_ (C - A)))
Theorem	suble 5789	Swap subtrahends in an inequality.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A - B) <_ C <-> (A - C) <_ B))
Theorem	lesub 5790	Swap subtrahends in an inequality.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A <_ (B - C) <-> C <_ (B - A)))
Theorem	ltsubadd2i 5791	'Less than' relationship between subtraction and addition.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- ((A - B) < C <-> A < (B + C))
Theorem	lesubadd2i 5792	'Less than or equal to' relationship between subtraction and addition.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- ((A - B) <_ C <-> A <_ (B + C))
Theorem	ltaddsubi 5793	'Less than' relationship between subtraction and addition.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- ((A + B) < C <-> A < (C - B))
Theorem	ltmullem 5794	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- (0 < C -> (A < B -> (A x. C) < (B x. C)))
Theorem	ltsub23 5795	'Less than' relationship between subtraction and addition.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A - B) < C <-> (A - C) < B))
Theorem	ltsub13 5796	'Less than' relationship between subtraction and addition.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A < (B - C) <-> C < (B - A)))
Theorem	lt2add 5797	Adding both sides of two 'less than' relations. Theorem I.25 of [Apostol] p. 20.
|- (((A e. RR /\ B e. RR) /\ (C e. RR /\ D e. RR)) -> ((A < C /\ B < D) -> (A + B) < (C + D)))
Theorem	le2add 5798	Adding both sides of two 'less than or equal to' relations.
|- (((A e. RR /\ B e. RR) /\ (C e. RR /\ D e. RR)) -> ((A <_ C /\ B <_ D) -> (A + B) <_ (C + D)))
Theorem	ltleadd 5799	Adding both sides of two orderings.
|- (((A e. RR /\ B e. RR) /\ (C e. RR /\ D e. RR)) -> ((A < C /\ B <_ D) -> (A + B) < (C + D)))
Theorem	leltadd 5800	Adding both sides of two orderings.
|- (((A e. RR /\ B e. RR) /\ (C e. RR /\ D e. RR)) -> ((A <_ C /\ B < D) -> (A + B) < (C + D)))