mmtheorems62 - 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 - 6101-6200 - Page 62 of 123

Type	Label	Description
Statement
Theorem	nnltp1le 6101	Natural number ordering relation.
|- ((A e. NN /\ B e. NN) -> (A < B <-> (A + 1) <_ B))
Theorem	nnsubi 6102	Subtraction of natural numbers.
|- A e. NN   &   |- B e. NN   =>   |- (A < B <-> (B - A) e. NN)
Theorem	nnsub 6103	Subtraction of natural numbers.
|- ((A e. NN /\ B e. NN) -> (A < B <-> (B - A) e. NN))
Theorem	nnaddm1cl 6104	Closure of addition of natural numbers minus one.
|- ((A e. NN /\ B e. NN) -> ((A + B) - 1) e. NN)
Theorem	nndiv 6105	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	nndivtr 6106	Transitive property of divisibility: if A divides B and B divides C, then A divides C. Typically C would be an integer, although the theorem holds for complex 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 6107	Extend class notation to include the number 2.
class 2
Syntax	c3 6108	Extend class notation to include the number 3.
class 3
Syntax	c4 6109	Extend class notation to include the number 4.
class 4
Syntax	c5 6110	Extend class notation to include the number 5.
class 5
Syntax	c6 6111	Extend class notation to include the number 6.
class 6
Syntax	c7 6112	Extend class notation to include the number 7.
class 7
Syntax	c8 6113	Extend class notation to include the number 8.
class 8
Syntax	c9 6114	Extend class notation to include the number 9.
class 9
Syntax	c10 6115	Extend class notation to include the number 10.
class 10
Definition	df-2 6116	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 5395 and df-1 5396). Note: Only the digits 0 through 9 (df-0 5395 through df-9 6123) and the number 10 (df-10 6124) 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 7684. (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 6117	Define the number 3.
|- 3 = (2 + 1)
Definition	df-4 6118	Define the number 4.
|- 4 = (3 + 1)
Definition	df-5 6119	Define the number 5.
|- 5 = (4 + 1)
Definition	df-6 6120	Define the number 6.
|- 6 = (5 + 1)
Definition	df-7 6121	Define the number 7.
|- 7 = (6 + 1)
Definition	df-8 6122	Define the number 8.
|- 8 = (7 + 1)
Definition	df-9 6123	Define the number 9.
|- 9 = (8 + 1)
Definition	df-10 6124	Define the number 10. See remarks under df-2 6116.
|- 10 = (9 + 1)
Theorem	2re 6125	The number 2 is real.
|- 2 e. RR
Theorem	2cn 6126	The number 2 is a complex number.
|- 2 e. CC
Theorem	3re 6127	The number 3 is real.
|- 3 e. RR
Theorem	4re 6128	The number 4 is real.
|- 4 e. RR
Theorem	5re 6129	The number 5 is real.
|- 5 e. RR
Theorem	6re 6130	The number 6 is real.
|- 6 e. RR
Theorem	7re 6131	The number 7 is real.
|- 7 e. RR
Theorem	8re 6132	The number 8 is real.
|- 8 e. RR
Theorem	9re 6133	The number 9 is real.
|- 9 e. RR
Theorem	10re 6134	The number 10 is real.
|- 10 e. RR
Theorem	2pos 6135	The number 2 is positive.
|- 0 < 2
Theorem	2ne0 6136	The number 2 is nonzero.
|- 2 =/= 0
Theorem	3pos 6137	The number 3 is positive.
|- 0 < 3
Theorem	4pos 6138	The number 4 is positive.
|- 0 < 4
Theorem	5pos 6139	The number 5 is positive.
|- 0 < 5
Theorem	6pos 6140	The number 6 is positive.
|- 0 < 6
Theorem	7pos 6141	The number 7 is positive.
|- 0 < 7
Theorem	8pos 6142	The number 8 is positive.
|- 0 < 8
Theorem	9pos 6143	The number 9 is positive.
|- 0 < 9
Theorem	10pos 6144	The number 10 is positive.
|- 0 < 10
Theorem	2nn 6145	2 is a natural number.
|- 2 e. NN
Theorem	3nn 6146	3 is a natural number.
|- 3 e. NN
Some properties of specific numbers
Theorem	2p2e4 6147	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 6148	4 is a natural number.
|- 4 e. NN
Theorem	2timesi 6149	Two times a number.
|- A e. CC   =>   |- (2 x. A) = (A + A)
Theorem	2times 6150	Two times a number.
|- (A e. CC -> (2 x. A) = (A + A))
Theorem	times2 6151	A number times 2.
|- (A e. CC -> (A x. 2) = (A + A))
Theorem	times2i 6152	A number times 2.
|- A e. CC   =>   |- (A x. 2) = (A + A)
Theorem	3p2e5 6153	3 + 2 = 5.
|- (3 + 2) = 5
Theorem	3p3e6 6154	3 + 3 = 6.
|- (3 + 3) = 6
Theorem	4p2e6 6155	4 + 2 = 6.
|- (4 + 2) = 6
Theorem	4p3e7 6156	4 + 3 = 7.
|- (4 + 3) = 7
Theorem	4p4e8 6157	4 + 4 = 8.
|- (4 + 4) = 8
Theorem	5p2e7 6158	5 + 2 = 7.
|- (5 + 2) = 7
Theorem	5p3e8 6159	5 + 3 = 8.
|- (5 + 3) = 8
Theorem	5p4e9 6160	5 + 4 = 9.
|- (5 + 4) = 9
Theorem	5p5e10 6161	5 + 5 = 10.
|- (5 + 5) = 10
Theorem	6p2e8 6162	6 + 2 = 8.
|- (6 + 2) = 8
Theorem	6p3e9 6163	6 + 3 = 9.
|- (6 + 3) = 9
Theorem	6p4e10 6164	6 + 4 = 10.
|- (6 + 4) = 10
Theorem	7p2e9 6165	7 + 2 = 9.
|- (7 + 2) = 9
Theorem	7p3e10 6166	7 + 3 = 10.
|- (7 + 3) = 10
Theorem	8p2e10 6167	8 + 2 = 10.
|- (8 + 2) = 10
Theorem	2t2e4 6168	2 times 2 equals 4.
|- (2 x. 2) = 4
Theorem	3t2e6 6169	3 times 2 equals 6.
|- (3 x. 2) = 6
Theorem	3t3e9 6170	3 times 3 equals 9.
|- (3 x. 3) = 9
Theorem	4t2e8 6171	4 times 2 equals 8.
|- (4 x. 2) = 8
Theorem	5t2e10 6172	5 times 2 equals 10.
|- (5 x. 2) = 10
Theorem	4d2e2 6173	One half of four is two.
|- (4 / 2) = 2
Theorem	1lt2 6174	1 is less than 2.
|- 1 < 2
Theorem	halfgt0 6175	One-half is greater than zero.
|- 0 < (1 / 2)
Theorem	halflt1 6176	One-half is less than one.
|- (1 / 2) < 1
Theorem	8th4div3 6177	An eighth of four thirds is a sixth. (Contributed by Paul Chapman, 24-Nov-2007.)
|- ((1 / 8) x. (4 / 3)) = (1 / 6)
Theorem	halfpm6th 6178	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	halfcl 6179	Closure of half of a number (frequently used special case).
|- (A e. CC -> (A / 2) e. CC)
Theorem	rehalfcl 6180	Real closure of half.
|- (A e. RR -> (A / 2) e. RR)
Theorem	half0 6181	Half of a number is zero iff the number is zero.
|- (A e. CC -> ((A / 2) = 0 <-> A = 0))
Theorem	halfpos 6182	A positive number is greater than its half.
|- (A e. RR -> (0 < A <-> (A / 2) < A))
Theorem	halfpos2 6183	A number is positive iff its half is positive.
|- (A e. RR -> (0 < A <-> 0 < (A / 2)))
Theorem	halfnneg2 6184	A number is nonnegative iff its half is nonnegative.
|- (A e. RR -> (0 <_ A <-> 0 <_ (A / 2)))
Theorem	2halves 6185	Two halves make a whole.
|- (A e. CC -> ((A / 2) + (A / 2)) = A)
Theorem	halfaddsubcl 6186	Closure of half-sum and half-difference. (Contributed by Paul Chapman, 12-Oct-2007.)
|- ((A e. CC /\ B e. CC) -> (((A + B) / 2) e. CC /\ ((A - B) / 2) e. CC))
Theorem	halfaddsub 6187	Sum and difference of half-sum and half-difference. (Contributed by Paul Chapman, 12-Oct-2007.)
|- ((A e. CC /\ B e. CC) -> ((((A + B) / 2) + ((A - B) / 2)) = A /\ (((A + B) / 2) - ((A - B) / 2)) = B))
Theorem	lt2halves 6188	A sum is less than the whole if each term is less than half.
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A < (C / 2) /\ B < (C / 2)) -> (A + B) < C))
Theorem	nominpos 6189	There is no smallest positive real number.
|- -. E.x e. RR (0 < x /\ -. E.y e. RR (0 < y /\ y < x))
Theorem	avgle 6190	The average of two numbers is less than or equal to at least one of them.
|- ((A e. RR /\ B e. RR) -> (((A + B) / 2) <_ A \/ ((A + B) / 2) <_ B))
Positive reals (as a subset of complex numbers)
Definition	df-rp 6191	Define the set of positive reals. Definition of positive numbers in [Apostol] p. 20.
|- RR+ = {x e. RR | 0 < x}
Theorem	elrp 6192	Membership in the set of positive reals.
|- (A e. RR+ <-> (A e. RR /\ 0 < A))
Theorem	elrpii 6193	Membership in the set of positive reals.
|- A e. RR   &   |- 0 < A   =>   |- A e. RR+
Theorem	1rp 6194	1 is a positive real. (Contributed by Jeffrey Hankins, 23-Nov-2008.)
|- 1 e. RR+
Theorem	rpre 6195	A positive real is a real.
|- (A e. RR+ -> A e. RR)
Theorem	rpcn 6196	A positive real is a complex number.
|- (A e. RR+ -> A e. CC)
Theorem	nnrp 6197	A natural number is a positive real.
|- (A e. NN -> A e. RR+)
Theorem	rpssre 6198	The positive reals are a subset of the reals.
|- RR+ (_ RR
Theorem	rpgt0 6199	A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)
|- (A e. RR+ -> 0 < A)
Theorem	rpge0 6200	A positive real is greater than or equal to zero.
|- (A e. RR+ -> 0 <_ A)