Metamath Proof Explorer - mmtheorems47

Jump to page: 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-5787

Statement List for Metamath Proof Explorer - 4601-4700 - Page 47 of 58

Type	Label	Description
Statement
Theorem	zneo 4601	No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of [Apostol] p. 28.
|- ((A e. ZZ /\ B e. ZZ) -> -. (2 x. A) = ((2 x. B) + 1))
Theorem	peano2uz 4602	Second Peano postulate for upper integer partition.
|- ((A e. ZZ /\ B e. {x e. ZZ | A <_ x}) -> (B + 1) e. {x e. ZZ | A <_ x})
Theorem	uzind 4603	Induction on the upper partition of ZZ that starts at an integer B. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction hypothesis. Warning: The HTML proof page is 3/4 megabyte in size. An attempt to shorten it is on my to-do list.
|- (x = B -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = (y + 1) -> (ph <-> th))   &   |- (x = A -> (ph <-> ta ))   &   |- ps   &   |- (((y e. ZZ /\ B e. ZZ) /\ B <_ y) -> (ch -> th))   =>   |- (((A e. ZZ /\ B e. ZZ) /\ B <_ A) -> ta )
Theorem	uzind2 4604	Induction on an upper partition of ZZ that starts at an integer B. The first four hypotheses give us the substitution instances we need, and the last two are the basis and the induction hypothesis.
|- (x = B -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = (y + 1) -> (ph <-> th))   &   |- (x = A -> (ph <-> ta ))   &   |- ps   &   |- ((B e. ZZ /\ y e. {z e. ZZ | B <_ z}) -> (ch -> th))   =>   |- ((B e. ZZ /\ A e. {z e. ZZ | B <_ z}) -> ta )
Theorem	uzwo 4605	Well-ordering principle: any non-empty subset of an upper partition of ZZ has a least element.
|- ((B e. ZZ /\ (A (_ {z e. ZZ | B <_ z} /\ A =/= (/))) -> E.x e. A A.y e. A x <_ y)
Theorem	uzwo2 4606	Well-ordering principle: any non-empty subset of an upper partition of ZZ has a unique least element.
|- ((B e. ZZ /\ (A (_ {z e. ZZ | B <_ z} /\ A =/= (/))) -> E!x e. A A.y e. A x <_ y)
Theorem	nnwo 4607	Well-ordering principle: any non-empty set of natural numbers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34.
|- ((A (_ NN /\ A =/= (/)) -> E.x e. A A.y e. A x <_ y)
Theorem	nnwoOLD 4608	Well-ordering principle: any non-empty set of natural numbers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34.
|- ((A (_ NN /\ A =/= (/)) -> E.x e. A A.y e. A x <_ y)
Theorem	nnwof 4609	Well-ordering principle: any non-empty set of natural numbers has a least element. This version allows x and y to be present in A as long as they are effectively not free.
|- (z e. A -> A.x z e. A)   &   |- (z e. A -> A.y z e. A)   =>   |- ((A (_ NN /\ A =/= (/)) -> E.x e. A A.y e. A x <_ y)
Theorem	nnwos 4610	Well-ordering principle: any non-empty set of natural numbers has a least element (schema form).
|- (x = y -> (ph <-> ps))   =>   |- (E.x e. NN ph -> E.x e. NN (ph /\ A.y e. NN (ps -> x <_ y)))
Theorem	indstr 4611	Strong Mathematical Induction for positive integers (inference schema).
|- (x = y -> (ph <-> ps))   &   |- (x e. NN -> (A.y e. NN (y < x -> ps) -> ph))   =>   |- (x e. NN -> ph)
Theorem	nn0ind 4612	Principle of Mathematical Induction (inference schema) on nonnegative integers. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction hypothesis. (Contributed by Raph Levien, 10-Apr-04. Raph says: "This seems a bit painful. I wonder if an explicit substitution version would be easier.")
|- (x = 0 -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = (y + 1) -> (ph <-> th))   &   |- (x = A -> (ph <-> ta ))   &   |- ps   &   |- (y e. NN0 -> (ch -> th))   =>   |- (A e. NN0 -> ta )
Theorem	btwnz 4613	Any real number can be sandwiched between two integers. Exercise 2 of [Apostol] p. 28.
|- (A e. RR -> (E.x e. ZZ x < A /\ E.y e. ZZ A < y))
Theorem	uzwo3lem1 4614	Lemma for uzwo3 4616 and zmin 4617.
|- R = {z e. ZZ | B <_ z}   =>   |- (B e. RR -> E!x e. R A.y e. R x <_ y)
Theorem	uzwo3lem2 4615	Lemma for uzwo3 4616.
|- R = {z e. ZZ | B <_ z}   &   |- S = U.{w e. R | A.v e. R w <_ v}   =>   |- ((B e. RR /\ (A (_ R /\ A =/= (/))) -> E!x e. A A.y e. A x <_ y)
Theorem	uzwo3 4616	Well-ordering principle: any non-empty subset of an upper partition of ZZ has a unique least element. This generalization of uzwo2 4606 allows the partition boundary B to be any real number.
|- ((B e. RR /\ (A (_ {z e. ZZ | B <_ z} /\ A =/= (/))) -> E!x e. A A.y e. A x <_ y)
Theorem	zmin 4617	There is a unique smallest integer greater than or equal to a given real number.
|- (A e. RR -> E!x e. ZZ (A <_ x /\ A.y e. ZZ (A <_ y -> x <_ y)))
Theorem	zmax 4618	There is a unique largest integer less than or equal to a given real number.
|- (A e. RR -> E!x e. ZZ (x <_ A /\ A.y e. ZZ (y <_ A -> y <_ x)))
Theorem	zbtwnre 4619	There is a unique integer between a real number and the number plus one. Exercise 5 of [Apostol] p. 28.
|- (A e. RR -> E!x e. ZZ (A <_ x /\ x < (A + 1)))
Theorem	rebtwnz 4620	There is a unique greatest integer less than or equal to a real number. Exercise 4 of [Apostol] p. 28.
|- (A e. RR -> E!x e. ZZ (x <_ A /\ A < (x + 1)))
Syntax	cfl 4621	Extend class notation with floor (greatest integer) function.
class floor
Definition	df-fl 4622	Define the floor (greatest integer) function. See flleltt 4625 for its basic property and flclt 4624 for its closure.
|- floor = {<.x, y>. | (x e. RR /\ y = U.{z e. ZZ | (z <_ x /\ x < (z + 1))})}
Theorem	flvalt 4623	Value of the floor (greatest integer) function. The floor of A is the (unique) integer less than or equal to A whose successor is strictly greater than A.
|- (A e. RR -> (floor` A) = U.{x e. ZZ | (x <_ A /\ A < (x + 1))})
Theorem	flclt 4624	The floor (greatest integer) function is an integer (closure law).
|- (A e. RR -> (floor` A) e. ZZ)
Theorem	flleltt 4625	A basic property of the floor (greatest integer) function.
|- (A e. RR -> ((floor` A) <_ A /\ A < ((floor` A) + 1)))
Theorem	flgzt 4626	The floor function value is the greatest integer less than or equal to its argument.
|- ((A e. RR /\ B e. ZZ) -> (B <_ A <-> B <_ (floor` A)))
Theorem	flidt 4627	An integer is its own floor.
|- (A e. ZZ -> (floor` A) = A)
Definition	df-q 4628	Define the set of rationals. Definition of rational numbers in [Apostol] p. 22.
|- QQ = {x | E.y e. ZZ E.z e. NN x = (y / z)}
Theorem	elq 4629	Membership in the set of rationals.
|- (A e. QQ <-> E.x e. ZZ E.y e. NN A = (x / y))
Theorem	znq 4630	The ratio of an integer and a natural number is a rational number.
|- ((A e. ZZ /\ B e. NN) -> (A / B) e. QQ)
Theorem	qret 4631	A rational number is a real number.
|- (A e. QQ -> A e. RR)
Theorem	zqt 4632	An integer is a rational number.
|- (A e. ZZ -> A e. QQ)
Theorem	zssq 4633	The integers are a subset of the rationals.
|- ZZ (_ QQ
Theorem	nn0ssq 4634	The nonnegative integers are a subset of the rationals.
|- NN0 (_ QQ
Theorem	nnssq 4635	The natural numbers are a subset of the rationals.
|- NN (_ QQ
Theorem	qssre 4636	The rationals are a subset of the reals.
|- QQ (_ RR
Theorem	qsscn 4637	The rationals are a subset of the complex numbers.
|- QQ (_ CC
Theorem	nnqt 4638	A natural number is rational.
|- (A e. NN -> A e. QQ)
Theorem	qcnt 4639	A rational number is a complex number.
|- (A e. QQ -> A e. CC)
Theorem	reex 4640	The set of real numbers exists.
|- RR e. V
Theorem	qex 4641	The set of rational numbers exists.
|- QQ e. V
Theorem	qaddclt 4642	Closure of addition of rationals.
|- ((A e. QQ /\ B e. QQ) -> (A + B) e. QQ)
Theorem	qnegclt 4643	Closure law for the negative of a rational.
|- (A e. QQ -> -uA e. QQ)
Theorem	qmulclt 4644	Closure of multiplication of rationals.
|- ((A e. QQ /\ B e. QQ) -> (A x. B) e. QQ)
Theorem	qsubclt 4645	Closure of subtraction of rationals.
|- ((A e. QQ /\ B e. QQ) -> (A - B) e. QQ)
Theorem	qrecclt 4646	Closure of reciprocal of rationals.
|- ((A e. QQ /\ A =/= 0) -> (1 / A) e. QQ)
Theorem	qdivclt 4647	Closure of division of rationals.
|- (((A e. QQ /\ B e. QQ) /\ B =/= 0) -> (A / B) e. QQ)
Theorem	qrevaddclt 4648	Reverse closure law for addition of rationals.
|- (B e. QQ -> ((A e. CC /\ (A + B) e. QQ) <-> A e. QQ))
Theorem	nnrecqt 4649	The reciprocal of a natural number is rational.
|- (A e. NN -> (1 / A) e. QQ)
Theorem	qbtwnre 4650	The rational numbers are dense in RR: any two real numbers have a rational between them. Exercise 6 of [Apostol] p. 28.
|- (((A e. RR /\ B e. RR) /\ A < B) -> E.x e. QQ (A < x /\ x < B))
Theorem	om2uz0 4651	The mapping G is a one-to-one mapping from om onto an upper partition of ZZ that will be used to construct a recursive definition generator. Ordinal natural number 0 maps to complex number C (normally 0 for the upper partition NN0 or 1 for the upper partition NN), 1 maps to C + 1, etc. This theorem shows the value of G at ordinal natural number zero. (Another version of this series of theorems was contributed by Raph Levien, 10-Apr-04.)
|- C e. ZZ   &   |- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)   =>   |- (G` (/)) = C
Theorem	om2uzsuc 4652	The value of G (see om2uz0 4651) at a successor.
|- C e. ZZ   &   |- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)   =>   |- (A e. om -> (G` suc A) = ((G` A) + 1))
Theorem	om2uzuz 4653	The value G (see om2uz0 4651) at an ordinal natural number is in the upper partition of ZZ.
|- C e. ZZ   &   |- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)   =>   |- (A e. om -> (G` A) e. {z e. ZZ | C <_ z})
Theorem	om2uzlt 4654	Less-than relation for G (see om2uz0 4651).
|- C e. ZZ   &   |- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)   =>   |- ((A e. om /\ B e. om) -> (A e. B -> (G` A) < (G` B)))
Theorem	om2uzran 4655	Range of G (see om2uz0 4651).
|- C e. ZZ   &   |- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)   =>   |- ran G = {z e. ZZ | C <_ z}
Theorem	om2uzf1o 4656	G (see om2uz0 4651) is a one-to-one onto mapping.
|- C e. ZZ   &   |- G = (rec({