mmtheorems69 - 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-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 6801-6900 - Page 69 of 175

Type	Label	Description
Statement
Theorem	ne0gt0 6801	A nonzero nonnegative number is positive.
|- ((A e. RR /\ 0 <_ A) -> (A =/= 0 <-> 0 < A))
Theorem	letric 6802	Trichotomy law. (The proof was shortened by Andrew Salmon, 19-Nov-2011.)
|- ((A e. RR /\ B e. RR) -> (A <_ B \/ B <_ A))
Theorem	letricOLD 6803	Trichotomy law.
|- ((A e. RR /\ B e. RR) -> (A <_ B \/ B <_ A))
Theorem	lecasei 6804	Ordering elimination by cases.
|- (ph -> A e. RR)   &   |- (ph -> B e. RR)   &   |- ((ph /\ A <_ B) -> ps)   &   |- ((ph /\ B <_ A) -> ps)   =>   |- (ph -> ps)
Theorem	lelttric 6805	Trichotomy law.
|- ((A e. RR /\ B e. RR) -> (A <_ B \/ B < A))
Theorem	ltadd1 6806	Addition to both sides of 'less than'.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A < B <-> (A + C) < (B + C)))
Theorem	ltadd2 6807	Addition to both sides of 'less than'.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A < B <-> (C + A) < (C + B)))
Theorem	leadd1 6808	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 6809	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 6810	'Less than' relationship between subtraction and addition.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A - B) < C <-> A < (C + B)))
Theorem	ltsubadd2 6811	'Less than' relationship between subtraction and addition.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A - B) < C <-> A < (B + C)))
Theorem	lesubadd 6812	'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 6813	'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 6814	'Less than' relationship between addition and subtraction.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A + B) < C <-> A < (C - B)))
Theorem	ltaddsub2 6815	'Less than' relationship between addition and subtraction.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A + B) < C <-> B < (C - A)))
Theorem	leaddsub 6816	'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 6817	'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 6818	Swap subtrahends in an inequality.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A - B) <_ C <-> (A - C) <_ B))
Theorem	lesub 6819	Swap subtrahends in an inequality. (The proof was shortened by Andrew Salmon, 19-Nov-2011.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A <_ (B - C) <-> C <_ (B - A)))
Theorem	lesubOLD 6820	Swap subtrahends in an inequality.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A <_ (B - C) <-> C <_ (B - A)))
Theorem	ltsubadd2i 6821	'Less than' relationship between subtraction and addition.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- ((A - B) < C <-> A < (B + C))
Theorem	lesubadd2i 6822	'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 6823	'Less than' relationship between subtraction and addition.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- ((A + B) < C <-> A < (C - B))
Theorem	ltmullem 6824	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 6825	'Less than' relationship between subtraction and addition.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A - B) < C <-> (A - C) < B))
Theorem	ltsub13 6826	'Less than' relationship between subtraction and addition.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A < (B - C) <-> C < (B - A)))
Theorem	lt2add 6827	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 6828	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 6829	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 6830	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	addgt0 6831	The sum of 2 positive numbers is positive. (The proof was shortened by Andrew Salmon, 19-Nov-2011.)
|- (((A e. RR /\ B e. RR) /\ (0 < A /\ 0 < B)) -> 0 < (A + B))
Theorem	addgt0OLD 6832	The sum of 2 positive numbers is positive.
|- (((A e. RR /\ B e. RR) /\ (0 < A /\ 0 < B)) -> 0 < (A + B))
Theorem	addgegt0 6833	The sum of nonnegative and positive numbers is positive. (The proof was shortened by Andrew Salmon, 19-Nov-2011.)
|- (((A e. RR /\ B e. RR) /\ (0 <_ A /\ 0 < B)) -> 0 < (A + B))
Theorem	addgegt0OLD 6834	The sum of nonnegative and positive numbers is positive.
|- (((A e. RR /\ B e. RR) /\ (0 <_ A /\ 0 < B)) -> 0 < (A + B))
Theorem	addgtge0 6835	The sum of nonnegative and positive numbers is positive. (The proof was shortened by Andrew Salmon, 19-Nov-2011.)
|- (((A e. RR /\ B e. RR) /\ (0 < A /\ 0 <_ B)) -> 0 < (A + B))
Theorem	addgtge0OLD 6836	The sum of nonnegative and positive numbers is positive.
|- (((A e. RR /\ B e. RR) /\ (0 < A /\ 0 <_ B)) -> 0 < (A + B))
Theorem	addge0 6837	The sum of 2 nonnegative numbers is nonnegative. (The proof was shortened by Andrew Salmon, 19-Nov-2011.)
|- (((A e. RR /\ B e. RR) /\ (0 <_ A /\ 0 <_ B)) -> 0 <_ (A + B))
Theorem	addge0OLD 6838	The sum of 2 nonnegative numbers is nonnegative.
|- (((A e. RR /\ B e. RR) /\ (0 <_ A /\ 0 <_ B)) -> 0 <_ (A + B))
Theorem	ltaddpos 6839	Adding a positive number to another number increases it.
|- ((A e. RR /\ B e. RR) -> (0 < A <-> B < (B + A)))
Theorem	ltaddpos2 6840	Adding a positive number to another number increases it.
|- ((A e. RR /\ B e. RR) -> (0 < A <-> B < (A + B)))
Theorem	ltsubpos 6841	Subtracting a positive number from another number decreases it. (The proof was shortened by Andrew Salmon, 19-Nov-2011.)
|- ((A e. RR /\ B e. RR) -> (0 < A <-> (B - A) < B))
Theorem	ltsubposOLD 6842	Subtracting a positive number from another number decreases it.
|- ((A e. RR /\ B e. RR) -> (0 < A <-> (B - A) < B))
Theorem	posdif 6843	Comparison of two numbers whose difference is positive.
|- ((A e. RR /\ B e. RR) -> (A < B <-> 0 < (B - A)))
Theorem	ltneg 6844	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	ltnegcon1 6845	Contraposition of negative in 'less than'.
|- ((A e. RR /\ B e. RR) -> (-uA < B <-> -uB < A))
Theorem	leneg 6846	Negative of both sides of 'less than or equal to'.
|- ((A e. RR /\ B e. RR) -> (A <_ B <-> -uB <_ -uA))
Theorem	lenegcon1 6847	Contraposition of negative in 'less than or equal to'.
|- ((A e. RR /\ B e. RR) -> (-uA <_ B <-> -uB <_ A))
Theorem	lenegcon2 6848	Contraposition of negative in 'less than or equal to'.
|- ((A e. RR /\ B e. RR) -> (A <_ -uB <-> B <_ -uA))
Theorem	lesub1 6849	Subtraction from both sides of 'less than or equal to'.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A <_ B <-> (A - C) <_ (B - C)))
Theorem	lesub2 6850	Subtraction of both sides of 'less than or equal to'.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A <_ B <-> (C - B) <_ (C - A)))
Theorem	ltsub1 6851	Subtraction from both sides of 'less than'. (Contributed by FL, 3-Jan-2008.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A < B <-> (A - C) < (B - C)))
Theorem	ltsub2 6852	Subtraction of both sides of 'less than'.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A < B <-> (C - B) < (C - A)))
Theorem	ltaddposi 6853	Adding a positive number to another number increases it.
|- A e. RR   &   |- B e. RR   =>   |- (0 < A <-> B < (B + A))
Theorem	posdifi 6854	Comparison of two numbers whose difference is positive.
|- A e. RR   &   |- B e. RR   =>   |- (A < B <-> 0 < (B - A))
Theorem	ltnegcon1i 6855	Contraposition of negative in 'less than'.
|- A e. RR   &   |- B e. RR   =>   |- (-uA < B <-> -uB < A)
Theorem	lenegcon1i 6856	Contraposition of negative in 'less than or equal to'.
|- A e. RR   &   |- B e. RR   =>   |- (-uA <_ B <-> -uB <_ A)
Theorem	lt0neg1 6857	Comparison of a number and its negative to zero. Theorem I.23 of [Apostol] p. 20.
|- (A e. RR -> (A < 0 <-> 0 < -uA))
Theorem	lt0neg2 6858	Comparison of a number and its negative to zero.
|- (A e. RR -> (0 < A <-> -uA < 0))
Theorem	le0neg1 6859	Comparison of a number and its negative to zero.
|- (A e. RR -> (A <_ 0 <-> 0 <_ -uA))
Theorem	le0neg2 6860	Comparison of a number and its negative to zero.
|- (A e. RR -> (0 <_ A <-> -uA <_ 0))
Theorem	addge01 6861	A number is less than or equal to itself plus a nonnegative number.
|- ((A e. RR /\ B e. RR) -> (0 <_ B <-> A <_ (A + B)))
Theorem	addge02 6862	A number is less than or equal to itself plus a nonnegative number.
|- ((A e. RR /\ B e. RR) -> (0 <_ B <-> A <_ (B + A)))
Theorem	subge0 6863	Nonnegative subtraction.
|- ((A e. RR /\ B e. RR) -> (0 <_ (A - B) <-> B <_ A))
Theorem	suble0 6864	Nonpositive subtraction.
|- ((A e. RR /\ B e. RR) -> ((A - B) <_ 0 <-> A <_ B))
Theorem	subge0i 6865	Nonnegative subtraction.
|- A e. RR   &   |- B e. RR   =>   |- (0 <_ (A - B) <-> B <_ A)
Theorem	subge02 6866	Nonnegative subtraction.
|- ((A e. RR /\ B e. RR) -> (0 <_ B <-> (A - B) <_ A))
Theorem	lesub0 6867	Lemma to show a nonnegative number is zero.
|- ((A e. RR /\ B e. RR) -> ((0 <_ A /\ B <_ (B - A)) <-> A = 0))
Theorem	mulge0 6868	The product of two nonnegative numbers is nonnegative.
|- (((A e. RR /\ 0 <_ A) /\ (B e. RR /\ 0 <_ B)) -> 0 <_ (A x. B))
Theorem	mulge0OLD 6869	The product of two nonnegative numbers is nonnegative.
|- (((A e. RR /\ B e. RR) /\ (0 <_ A /\ 0 <_ B)) -> 0 <_ (A x. B))
Theorem	mullt0 6870	The product of two negative numbers is positive. (Contributed by Jeffrey Hankins, 8-Jun-2009.)
|- (((A e. RR /\ A < 0) /\ (B e. RR /\ B < 0)) -> 0 < (A x. B))
Theorem	lt01 6871	0 is less than 1. Theorem I.21 of [Apostol] p. 20.
|- 0 < 1
Reciprocals
Theorem	ixi 6872	_i times itself is minus 1. (The proof was shortened by Andrew Salmon, 19-Nov-2011.)
|- (_i x. _i) = -u1
Theorem	ixiOLD 6873	_i times itself is minus 1.
|- (_i x. _i) = -u1
Theorem	recextlem1 6874	Lemma for recex 6876.
Theorem	recextlem2 6875	Lemma for recex 6876.
Theorem	recex 6876	Existence of reciprocal of nonzero complex number. (Contributed by Eric Schmidt, 22-May-2007.)
|- ((A e. CC /\ A =/= 0) -> E.x e. CC (A x. x) = 1)
Theorem	recexi 6877	Existence of reciprocals.
|- A e. CC   &   |- A =/= 0   =>   |- E.x e. CC (A x. x) = 1
Theorem	mulcani 6878	Cancellation law for multiplication. Theorem I.7 of [Apostol] p. 18.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C =/= 0   =>   |- ((C x. A) = (C x. B) <-> A = B)
Theorem	mulcant2i 6879	Cancellation law for multiplication. Theorem I.7 of [Apostol] p. 18. Illustrates use of keephyp 3027.
|- C =/= 0   =>   |- ((A e. CC /\ B e. CC /\ C e. CC) -> ((C x. A) = (C x. B) <-> A = B))
Theorem	mulcan 6880	Cancellation law for multiplication (full theorem form). Theorem I.7 of [Apostol] p. 18. Illustrates use of dedth 3011 and elimne0 6469.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((C x. A) = (C x. B) <-> A = B))
Theorem	mulcan2 6881	Cancellation law for multiplication.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A x. C) = (B x. C) <-> A = B))
Theorem	mul0ori 6882	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	msq0i 6883	A number is zero iff its square is zero (where square is represented using multiplication).
|- A e. CC   =>   |- ((A x. A) = 0 <-> A = 0)
Theorem	mul0or 6884	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	mulne0b 6885	The product of two nonzero numbers is nonzero. (The proof was shortened by Andrew Salmon, 19-Nov-2011.)
|- ((A e. CC /\ B e. CC) -> ((A =/= 0 /\ B =/= 0) <-> (A x. B) =/= 0))
Theorem	mulne0bOLD 6886	The product of two nonzero numbers is nonzero.
|- ((A e. CC /\ B e. CC) -> ((A =/= 0 /\ B =/= 0) <-> (A x. B) =/= 0))
Theorem	mulne0 6887	The product of two nonzero numbers is nonzero.
|- (((A e. CC /\ A =/= 0) /\ (B e. CC /\ B =/= 0)) -> (A x. B) =/= 0)
Theorem	mulne0i 6888	The product of two nonzero numbers is nonzero.
|- A e. CC   &   |- B e. CC   &   |- A =/= 0   &   |- B =/= 0   =>   |- (A x. B) =/= 0
Theorem	muleqadd 6889	Property of numbers whose product equals their sum. Equation 5 of [Kreyszig] p. 12.
|- ((A e. CC /\ B e. CC) -> ((A x. B) = (A + B) <-> ((A - 1) x. (B - 1)) = 1))
Theorem	receui 6890	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
Theorem	mulnzcnopr 6891	Multiplication maps nonzero complex numbers to nonzero complex numbers. (Contributed by Steve Rodriguez, 23-Feb-2007.)
|- ( x. |` ((CC \ {0}) X. (CC \ {0}))):((CC \ {0}) X. (CC \ {0}))-->(CC \ {0})
Division
Definition	df-div 6892	Define division. Theorem divmuli 6894 relates it to multiplication, and divcli 6899 and redivcli 6976 prove its closure laws.
|- / = {<.<.x, y>., z>. | ((x e. CC /\ y e. (CC \ {0})) /\ z = (iota_w e. CC(y x. w) = x))}
Theorem	divvali 6893	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) = (iota_x e. CC(B x. x) = A)
Theorem	divmuli 6894	Relationship between division and multiplication.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- B =/= 0   =>   |- ((A / B) = C <-> (B x. C) = A)
Theorem	divmulzi 6895	Relationship between division and multiplication.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- (B =/= 0 -> ((A / B) = C <-> (B x. C) = A))
Theorem	divmul 6896	Relationship between division and multiplication.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A / C) = B <-> (C x. B) = A))
Theorem	divmul2 6897	Relationship between division and multiplication.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A / C) = B <-> A = (C x. B)))
Theorem	divmul3 6898	Relationship between division and multiplication.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A / C) = B <-> A = (B x. C)))
Theorem	divcli 6899	Closure law for division.
|- A e. CC   &   |- B e. CC   &   |- B =/= 0   =>   |- (A / B) e. CC
Theorem	divclzi 6900	Closure law for division.
|- A e. CC   &   |- B e. CC   =>   |- (B =/= 0 -> (A / B) e. CC)