mmtheorems60 - 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-10687

Statement List for Metamath Proof Explorer - 5901-6000 - Page 60 of 107

Type	Label	Description
Statement
Theorem	1nn 5901	Peano postulate: 1 is a natural number.
|- 1 e. NN
Theorem	peano2nn 5902	Peano postulate: a successor of a natural number is a natural number.
|- (A e. NN -> (A + 1) e. NN)
Theorem	dfnn2 5903	Alternate definition of the set of natural numbers. Definition of positive integers in [Apostol] p. 22.
|- NN = |^|{x | (x (_ RR /\ 1 e. x /\ A.y e. x (y + 1) e. x)}
Principle of mathematical induction
Theorem	nnind 5904	Principle of Mathematical Induction (inference schema). The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction hypothesis. See nnaddclt 5907 for an example of its use. See nn0ind 6179 for induction on nonnegative integers and uzind 6172, uzind4 6401 for induction on an arbitrary set of upper integers. See indstr 6412 for strong induction.
|- (x = 1 -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = (y + 1) -> (ph <-> th))   &   |- (x = A -> (ph <-> ta))   &   |- ps   &   |- (y e. NN -> (ch -> th))   =>   |- (A e. NN -> ta)
Theorem	nnindALT 5905	Principle of Mathematical Induction (inference schema). The last four hypotheses give us the substitution instances we need; the first two are the induction hypothesis and the basis. (This ALT version of nnind 5904 is easier to use with the Proof Assistant since 'assign last' will be applied to the substitution instances first. We may switch to it as the official version.)
|- (y e. NN -> (ch -> th))   &   |- ps   &   |- (x = 1 -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = (y + 1) -> (ph <-> th))   &   |- (x = A -> (ph <-> ta))   =>   |- (A e. NN -> ta)
Natural numbers (cont.)
Theorem	nn1suc 5906	If a statement holds for 1 and also holds for a successor, it holds for all natural numbers. The first three hypotheses give us the substitution instances we need; the last two show that it holds for 1 and for a successor.
|- (x = 1 -> (ph <-> ps))   &   |- (x = (y + 1) -> (ph <-> ch))   &   |- (x = A -> (ph <-> th))   &   |- ps   &   |- (y e. NN -> ch)   =>   |- (A e. NN -> th)
Theorem	nnaddclt 5907	Closure of addition of natural numbers, proved by induction on the second addend.
|- ((A e. NN /\ B e. NN) -> (A + B) e. NN)
Theorem	nnmulclt 5908	Closure of multiplication of natural numbers.
|- ((A e. NN /\ B e. NN) -> (A x. B) e. NN)
Theorem	nn2get 5909	There exists a natural number greater than or equal to any two others.
|- ((A e. NN /\ B e. NN) -> E.x e. NN (A <_ x /\ B <_ x))
Theorem	nnge1t 5910	A natural number is one or greater.
|- (A e. NN -> 1 <_ A)
Theorem	nngt1ne1t 5911	A natural number is greater than one iff it is not equal to one.
|- (A e. NN -> (1 < A <-> A =/= 1))
Theorem	nnle1eq1t 5912	A natural number is less than or equal to one iff it is equal to one.
|- (A e. NN -> (A <_ 1 <-> A = 1))
Theorem	nngt0t 5913	A natural number is positive.
|- (A e. NN -> 0 < A)
Theorem	lt1nnn 5914	A number less than one is not a natural number.
|- ((A e. RR /\ A < 1) -> -. A e. NN)
Theorem	0nnn 5915	Zero is not a natural number.
|- -. 0 e. NN
Theorem	nnne0t 5916	A natural number is non-zero.
|- (A e. NN -> A =/= 0)
Theorem	nngt0 5917	A natural number is positive (inference version).
|- A e. NN   =>   |- 0 < A
Theorem	nnne0 5918	A natural number is non-zero (inference version).
|- A e. NN   =>   |- A =/= 0
Theorem	nnrecgt0t 5919	The reciprocal of a natural number is positive.
|- (A e. NN -> 0 < (1 / A))
Theorem	nnleltp1t 5920	Natural number ordering relation.
|- ((A e. NN /\ B e. NN) -> (A <_ B <-> A < (B + 1)))
Theorem	nnltp1let 5921	Natural number ordering relation.
|- ((A e. NN /\ B e. NN) -> (A < B <-> (A + 1) <_ B))
Theorem	nnsub 5922	Subtraction of natural numbers.
|- A e. NN   &   |- B e. NN   =>   |- (A < B <-> (B - A) e. NN)
Theorem	nnsubt 5923	Subtraction of natural numbers.
|- ((A e. NN /\ B e. NN) -> (A < B <-> (B - A) e. NN))
Theorem	nnaddm1clt 5924	Closure of addition of natural numbers minus one.
|- ((A e. NN /\ B e. NN) -> ((A + B) - 1) e. NN)
Theorem	nndivt 5925	Two ways to express "A divides B" for natural numbers.
|- ((A e. NN /\ B e. NN) -> (E.x e. NN (A x. x) = B <-> (B / A) e. NN))
Theorem	nndivtrt 5926	Transitive property of divisibility: if A divides B and B divides C, then A divides C.
|- (((A e. NN /\ B e. NN /\ C e. CC) /\ ((B / A) e. NN /\ (C / B) e. NN)) -> (C / A) e. NN)
Decimal representation of numbers
Syntax	c2 5927	Extend class notation to include the number 2.
class 2
Syntax	c3 5928	Extend class notation to include the number 3.
class 3
Syntax	c4 5929	Extend class notation to include the number 4.
class 4
Syntax	c5 5930	Extend class notation to include the number 5.
class 5
Syntax	c6 5931	Extend class notation to include the number 6.
class 6
Syntax	c7 5932	Extend class notation to include the number 7.
class 7
Syntax	c8 5933	Extend class notation to include the number 8.
class 8
Syntax	c9 5934	Extend class notation to include the number 9.
class 9
Syntax	c10 5935	Extend class notation to include the number 10.
class 10
Definition	df-2 5936	Define the number 2. Note that the numbers 0 and 1 are constants defined as primitives of the complex number axiom system (see df-0 5232 and df-1 5233). Note: Only the digits 0 through 9 (df-0 5232 through df-9 5943) and the number 10 (df-10 5944) are explicitly defined. Integers can be exhibited as sums of powers of 10 or as some other expression built from operations on the numbers 0 through 10. For example, the prime number 823541 can be expressed as (7^7) - 2. Decimals can be expressed as ratios of integers, as in cos2bnd 7436. (Fortunately, most abstract math rarely requires numbers larger than 4. Even in Wiles' proof of Fermat's Last Theorem, the largest number used appears to be 12.) A decimal representation of numbers may be added at some point in the future if it is deemed useful. Ideas for a clean, eliminable definition are welcome. (An awkward earlier definition was deleted from the database on 18-Sep-1999.)
|- 2 = (1 + 1)
Definition	df-3 5937	Define the number 3.
|- 3 = (2 + 1)
Definition	df-4 5938	Define the number 4.
|- 4 = (3 + 1)
Definition	df-5 5939	Define the number 5.
|- 5 = (4 + 1)
Definition	df-6 5940	Define the number 6.
|- 6 = (5 + 1)
Definition	df-7 5941	Define the number 7.
|- 7 = (6 + 1)
Definition	df-8 5942	Define the number 8.
|- 8 = (7 + 1)
Definition	df-9 5943	Define the number 9.
|- 9 = (8 + 1)
Definition	df-10 5944	Define the number 10. See remarks under df-2 5936.
|- 10 = (9 + 1)
Theorem	2re 5945	The number 2 is real.
|- 2 e. RR
Theorem	2cn 5946	The number 2 is a complex number.
|- 2 e. CC
Theorem	3re 5947	The number 3 is real.
|- 3 e. RR
Theorem	4re 5948	The number 4 is real.
|- 4 e. RR
Theorem	5re 5949	The number 5 is real.
|- 5 e. RR
Theorem	6re 5950	The number 6 is real.
|- 6 e. RR
Theorem	7re 5951	The number 7 is real.
|- 7 e. RR
Theorem	8re 5952	The number 8 is real.
|- 8 e. RR
Theorem	9re 5953	The number 9 is real.
|- 9 e. RR
Theorem	10re 5954	The number 10 is real.
|- 10 e. RR
Theorem	2pos 5955	The number 2 is positive.
|- 0 < 2
Theorem	2ne0 5956	The number 2 is nonzero.
|- 2 =/= 0
Theorem	3pos 5957	The number 3 is positive.
|- 0 < 3
Theorem	4pos 5958	The number 4 is positive.
|- 0 < 4
Theorem	5pos 5959	The number 5 is positive.
|- 0 < 5
Theorem	6pos 5960	The number 6 is positive.
|- 0 < 6
Theorem	7pos 5961	The number 7 is positive.
|- 0 < 7
Theorem	8pos 5962	The number 8 is positive.
|- 0 < 8
Theorem	9pos 5963	The number 9 is positive.
|- 0 < 9
Theorem	10pos 5964	The number 10 is positive.
|- 0 < 10
Theorem	2nn 5965	2 is a natural number.
|- 2 e. NN
Theorem	3nn 5966	3 is a natural number.
|- 3 e. NN
Some properties of specific numbers
Theorem	2p2e4 5967	Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page: http://us.metamath.org/mpegif/mmset.html#trivia.
|- (2 + 2) = 4
Theorem	4nn 5968	4 is a natural number.
|- 4 e. NN
Theorem	2times 5969	Two times a number.
|- A e. CC   =>   |- (2 x. A) = (A + A)
Theorem	2timest 5970	Two times a number.
|- (A e. CC -> (2 x. A) = (A + A))
Theorem	times2t 5971	A number times 2.
|- (A e. CC -> (A x. 2) = (A + A))
Theorem	times2 5972	A number times 2.
|- A e. CC   =>   |- (A x. 2) = (A + A)
Theorem	3p2e5 5973	3 + 2 = 5.
|- (3 + 2) = 5
Theorem	3p3e6 5974	3 + 3 = 6.
|- (3 + 3) = 6
Theorem	4p2e6 5975	4 + 2 = 6.
|- (4 + 2) = 6
Theorem	4p3e7 5976	4 + 3 = 7.
|- (4 + 3) = 7
Theorem	4p4e8 5977	4 + 4 = 8.
|- (4 + 4) = 8
Theorem	5p2e7 5978	5 + 2 = 7.
|- (5 + 2) = 7
Theorem	5p3e8 5979	5 + 3 = 8.
|- (5 + 3) = 8
Theorem	5p4e9 5980	5 + 4 = 9.
|- (5 + 4) = 9
Theorem	5p5e10 5981	5 + 5 = 10.
|- (5 + 5) = 10
Theorem	6p2e8 5982	6 + 2 = 8.
|- (6 + 2) = 8
Theorem	6p3e9 5983	6 + 3 = 9.
|- (6 + 3) = 9
Theorem	6p4e10 5984	6 + 4 = 10.
|- (6 + 4) = 10
Theorem	7p2e9 5985	7 + 2 = 9.
|- (7 + 2) = 9
Theorem	7p3e10 5986	7 + 3 = 10.
|- (7 + 3) = 10
Theorem	8p2e10 5987	8 + 2 = 10.
|- (8 + 2) = 10
Theorem	2t2e4 5988	2 times 2 equals 4.
|- (2 x. 2) = 4
Theorem	3t2e6 5989	3 times 2 equals 6.
|- (3 x. 2) = 6
Theorem	3t3e9 5990	3 times 3 equals 9.
|- (3 x. 3) = 9
Theorem	4t2e8 5991	4 times 2 equals 8.
|- (4 x. 2) = 8
Theorem	5t2e10 5992	5 times 2 equals 10.
|- (5 x. 2) = 10
Theorem	4d2e2 5993	One half of four is two.
|- (4 / 2) = 2
Theorem	1lt2 5994	1 is less than 2.
|- 1 < 2
Theorem	halfgt0 5995	One-half is greater than zero.
|- 0 < (1 / 2)
Theorem	halflt1 5996	One-half is less than one.
|- (1 / 2) < 1
Theorem	8th4div3 5997	An eighth of four thirds is a sixth. (Contributed by Paul Chapman, 24-Nov-2007.)
|- ((1 / 8) x. (4 / 3)) = (1 / 6)
Theorem	halfpm6th 5998	One half plus or minus one sixth. (Contributed by Paul Chapman, 17-Jan-2008.)
|- (((1 / 2) - (1 / 6)) = (1 / 3) /\ ((1 / 2) + (1 / 6)) = (2 / 3))
Theorem	halfclt 5999	Closure of half of a number (frequently used special case).
|- (A e. CC -> (A / 2) e. CC)
Theorem	rehalfclt 6000	Real closure of half.
|- (A e. RR -> (A / 2) e. RR)