mmtheorems59 - 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 - 5801-5900 - Page 59 of 123

Type	Label	Description
Statement
Theorem	addgt0 5801	The sum of 2 positive numbers is positive.
|- (((A e. RR /\ B e. RR) /\ (0 < A /\ 0 < B)) -> 0 < (A + B))
Theorem	addgegt0 5802	The sum of nonnegative and positive numbers is positive.
|- (((A e. RR /\ B e. RR) /\ (0 <_ A /\ 0 < B)) -> 0 < (A + B))
Theorem	addgtge0 5803	The sum of nonnegative and positive numbers is positive.
|- (((A e. RR /\ B e. RR) /\ (0 < A /\ 0 <_ B)) -> 0 < (A + B))
Theorem	addge0 5804	The sum of 2 nonnegative numbers is nonnegative.
|- (((A e. RR /\ B e. RR) /\ (0 <_ A /\ 0 <_ B)) -> 0 <_ (A + B))
Theorem	ltaddpos 5805	Adding a positive number to another number increases it.
|- ((A e. RR /\ B e. RR) -> (0 < A <-> B < (B + A)))
Theorem	ltaddpos2 5806	Adding a positive number to another number increases it.
|- ((A e. RR /\ B e. RR) -> (0 < A <-> B < (A + B)))
Theorem	ltsubpos 5807	Subtracting a positive number from another number decreases it.
|- ((A e. RR /\ B e. RR) -> (0 < A <-> (B - A) < B))
Theorem	posdif 5808	Comparison of two numbers whose difference is positive.
|- ((A e. RR /\ B e. RR) -> (A < B <-> 0 < (B - A)))
Theorem	ltneg 5809	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 5810	Contraposition of negative in 'less than'.
|- ((A e. RR /\ B e. RR) -> (-uA < B <-> -uB < A))
Theorem	leneg 5811	Negative of both sides of 'less than or equal to'.
|- ((A e. RR /\ B e. RR) -> (A <_ B <-> -uB <_ -uA))
Theorem	lenegcon1 5812	Contraposition of negative in 'less than or equal to'.
|- ((A e. RR /\ B e. RR) -> (-uA <_ B <-> -uB <_ A))
Theorem	lenegcon2 5813	Contraposition of negative in 'less than or equal to'.
|- ((A e. RR /\ B e. RR) -> (A <_ -uB <-> B <_ -uA))
Theorem	lesub1 5814	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 5815	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 5816	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 5817	Subtraction of both sides of 'less than'.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A < B <-> (C - B) < (C - A)))
Theorem	ltaddposi 5818	Adding a positive number to another number increases it.
|- A e. RR   &   |- B e. RR   =>   |- (0 < A <-> B < (B + A))
Theorem	posdifi 5819	Comparison of two numbers whose difference is positive.
|- A e. RR   &   |- B e. RR   =>   |- (A < B <-> 0 < (B - A))
Theorem	ltnegcon1i 5820	Contraposition of negative in 'less than'.
|- A e. RR   &   |- B e. RR   =>   |- (-uA < B <-> -uB < A)
Theorem	lenegcon1i 5821	Contraposition of negative in 'less than or equal to'.
|- A e. RR   &   |- B e. RR   =>   |- (-uA <_ B <-> -uB <_ A)
Theorem	lt0neg1 5822	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 5823	Comparison of a number and its negative to zero.
|- (A e. RR -> (0 < A <-> -uA < 0))
Theorem	le0neg1 5824	Comparison of a number and its negative to zero.
|- (A e. RR -> (A <_ 0 <-> 0 <_ -uA))
Theorem	le0neg2 5825	Comparison of a number and its negative to zero.
|- (A e. RR -> (0 <_ A <-> -uA <_ 0))
Theorem	addge01 5826	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 5827	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 5828	Nonnegative subtraction.
|- ((A e. RR /\ B e. RR) -> (0 <_ (A - B) <-> B <_ A))
Theorem	suble0 5829	Nonpositive subtraction.
|- ((A e. RR /\ B e. RR) -> ((A - B) <_ 0 <-> A <_ B))
Theorem	subge0i 5830	Nonnegative subtraction.
|- A e. RR   &   |- B e. RR   =>   |- (0 <_ (A - B) <-> B <_ A)
Theorem	subge02 5831	Nonnegative subtraction.
|- ((A e. RR /\ B e. RR) -> (0 <_ B <-> (A - B) <_ A))
Theorem	lesub0 5832	Lemma to show a nonnegative number is zero.
|- ((A e. RR /\ B e. RR) -> ((0 <_ A /\ B <_ (B - A)) <-> A = 0))
Theorem	mulge0 5833	The product of two nonnegative numbers is nonnegative.
|- (((A e. RR /\ 0 <_ A) /\ (B e. RR /\ 0 <_ B)) -> 0 <_ (A x. B))
Theorem	mulge0OLD 5834	The product of two nonnegative numbers is nonnegative.
|- (((A e. RR /\ B e. RR) /\ (0 <_ A /\ 0 <_ B)) -> 0 <_ (A x. B))
Theorem	mullt0 5835	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 5836	0 is less than 1. Theorem I.21 of [Apostol] p. 20.
|- 0 < 1
Reciprocals
Theorem	ixi 5837	i times itself is minus 1.
|- (i x. i) = -u1
Theorem	recextlem1 5838	Lemma for recex 5840.
Theorem	recextlem2 5839	Lemma for recex 5840.
Theorem	recex 5840	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 5841	Existence of reciprocals.
|- A e. CC   &   |- A =/= 0   =>   |- E.x e. CC (A x. x) = 1
Theorem	mulcani 5842	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 5843	Cancellation law for multiplication. Theorem I.7 of [Apostol] p. 18. Illustrates use of keephyp 2453.
|- C =/= 0   =>   |- ((A e. CC /\ B e. CC /\ C e. CC) -> ((C x. A) = (C x. B) <-> A = B))
Theorem	mulcan 5844	Cancellation law for multiplication (full theorem form). Theorem I.7 of [Apostol] p. 18. Illustrates use of dedth 2437 and elimne0 5470.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((C x. A) = (C x. B) <-> A = B))
Theorem	mulcan2 5845	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 5846	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 5847	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 5848	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	muln0b 5849	The product of two non-zero numbers is non-zero.
|- ((A e. CC /\ B e. CC) -> ((A =/= 0 /\ B =/= 0) <-> (A x. B) =/= 0))
Theorem	mulne0 5850	The product of two non-zero numbers is non-zero.
|- (((A e. CC /\ A =/= 0) /\ (B e. CC /\ B =/= 0)) -> (A x. B) =/= 0)
Theorem	muln0i 5851	The product of two non-zero numbers is non-zero.
|- A e. CC   &   |- B e. CC   &   |- A =/= 0   &   |- B =/= 0   =>   |- (A x. B) =/= 0
Theorem	muleqadd 5852	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 5853	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 5854	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 5855	Define division. Theorem divmuli 5857 relates it to multiplication, and divcli 5862 and redivcli 5938 prove its closure laws.
|- / = {<.<.x, y>., z>. | ((x e. CC /\ y e. (CC \ {0})) /\ z = U.{w e. CC | (y x. w) = x})}
Theorem	divvali 5856	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) = U.{x e. CC | (B x. x) = A}
Theorem	divmuli 5857	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 5858	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 5859	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 5860	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 5861	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 5862	Closure law for division.
|- A e. CC   &   |- B e. CC   &   |- B =/= 0   =>   |- (A / B) e. CC
Theorem	divclzi 5863	Closure law for division.
|- A e. CC   &   |- B e. CC   =>   |- (B =/= 0 -> (A / B) e. CC)
Theorem	divcl 5864	Closure law for division.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> (A / B) e. CC)
Theorem	reccli 5865	Closure law for reciprocal.
|- A e. CC   &   |- A =/= 0   =>   |- (1 / A) e. CC
Theorem	recclzi 5866	Closure law for reciprocal.
|- A e. CC   =>   |- (A =/= 0 -> (1 / A) e. CC)
Theorem	reccl 5867	Closure law for reciprocal.
|- ((A e. CC /\ A =/= 0) -> (1 / A) e. CC)
Theorem	divcan2i 5868	A cancellation law for division.
|- A e. CC   &   |- B e. CC   &   |- B =/= 0   =>   |- (B x. (A / B)) = A
Theorem	divcan1i 5869	A cancellation law for division.
|- A e. CC   &   |- B e. CC   &   |- B =/= 0   =>   |- ((A / B) x. B) = A
Theorem	divcan1zi 5870	A cancellation law for division.
|- A e. CC   &   |- B e. CC   =>   |- (B =/= 0 -> ((A / B) x. B) = A)
Theorem	divcan2zi 5871	A cancellation law for division. We eliminate the third hypothesis of divcan2i 5868 using the weak deduction theorem dedth 2437 and keep the other two. Because the first hypothesis shares the class variable B with the hypothesis we're eliminating, we need to use keepel 2456 in order to keep the first hypothesis.
|- A e. CC   &   |- B e. CC   =>   |- (B =/= 0 -> (B x. (A / B)) = A)
Theorem	divcan1 5872	A cancellation law for division.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> ((A / B) x. B) = A)
Theorem	divcan2 5873	A cancellation law for division.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> (B x. (A / B)) = A)
Theorem	divne0b 5874	The ratio of non-zero numbers is non-zero.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> (A =/= 0 <-> (A / B) =/= 0))
Theorem	divne0 5875	The ratio of non-zero numbers is non-zero.
|- (((A e. CC /\ A =/= 0) /\ (B e. CC /\ B =/= 0)) -> (A / B) =/= 0)
Theorem	divne0i 5876	The ratio of non-zero numbers is non-zero.
|- A e. CC   &   |- B e. CC   &   |- A =/= 0   &   |- B =/= 0   =>   |- (A / B) =/= 0
Theorem	recne0zi 5877	The reciprocal of a non-zero number is non-zero.
|- A e. CC   =>   |- (A =/= 0 -> (1 / A) =/= 0)
Theorem	recne0 5878	The reciprocal of a non-zero number is non-zero.
|- ((A e. CC /\ A =/= 0) -> (1 / A) =/= 0)
Theorem	recidi 5879	Multiplication of a number and its reciprocal.
|- A e. CC   &   |- A =/= 0   =>   |- (A x. (1 / A)) = 1
Theorem	recidzi 5880	Multiplication of a number and its reciprocal.
|- A e. CC   =>   |- (A =/= 0 -> (A x. (1 / A)) = 1)
Theorem	recid 5881	Multiplication of a number and its reciprocal.
|- ((A e. CC /\ A =/= 0) -> (A x. (1 / A)) = 1)
Theorem	recid2 5882	Multiplication of a number and its reciprocal.
|- ((A e. CC /\ A =/= 0) -> ((1 / A) x. A) = 1)
Theorem	divreci 5883	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18.
|- A e. CC   &   |- B e. CC   &   |- B =/= 0   =>   |- (A / B) = (A x. (1 / B))
Theorem	divreczi 5884	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18.
|- A e. CC   &   |- B e. CC   =>   |- (B =/= 0 -> (A / B) = (A x. (1 / B)))
Theorem	divrec 5885	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> (A / B) = (A x. (1 / B)))
Theorem	divrec2 5886	Relationship between division and reciprocal.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> (A / B) = ((1 / B) x. A))
Theorem	divass 5887	An associative law for division.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A x. B) / C) = (A x. (B / C)))
Theorem	div23 5888	A commutative/associative law for division.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A x. B) / C) = ((A / C) x. B))
Theorem	div13 5889	A commutative/associative law for division.
|- ((A e. CC /\ (B e. CC /\ B =/= 0) /\ C e. CC) -> ((A / B) x. C) = ((C / B) x. A))
Theorem	div12 5890	A commutative/associative law for division.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> (A x. (B / C)) = (B x. (A / C)))
Theorem	divasszi 5891	An associative law for division.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- (C =/= 0 -> ((A x. B) / C) = (A x. (B / C)))
Theorem	divassi 5892	An associative law for division.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C =/= 0   =>   |- ((A x. B) / C) = (A x. (B / C))
Theorem	divdiri 5893	Distribution of division over addition.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C =/= 0   =>   |- ((A + B) / C) = ((A / C) + (B / C))
Theorem	div23i 5894	A commutative/associative law for division.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C =/= 0   =>   |- ((A x. B) / C) = ((A / C) x. B)
Theorem	divdirzi 5895	Distribution of division over addition.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- (C =/= 0 -> ((A + B) / C) = ((A / C) + (B / C)))
Theorem	divdir 5896	Distribution of division over addition.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A + B) / C) = ((A / C) + (B / C)))
Theorem	divcan3i 5897	A cancellation law for division.
|- A e. CC   &   |- B e. CC   &   |- B =/= 0   =>   |- ((B x. A) / B) = A
Theorem	divcan4i 5898	A cancellation law for division.
|- A e. CC   &   |- B e. CC   &   |- B =/= 0   =>   |- ((A x. B) / B) = A
Theorem	divcan3zi 5899	A cancellation law for division. (Eliminates a hypothesis of divcan3i 5897 with the weak deduction theorem.)
|- A e. CC   &   |- B e. CC   =>   |- (B =/= 0 -> ((B x. A) / B) = A)
Theorem	divcan4zi 5900	A cancellation law for division.
|- A e. CC   &   |- B e. CC   =>   |- (B =/= 0 -> ((A x. B) / B) = A)