mmtheorems66 - 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 - 6501-6600 - Page 66 of 123

Type	Label	Description
Statement
Theorem	iocval 6501	Value of the open-below, closed-above interval function.
|- ((A e. RR* /\ B e. RR*) -> (A(,]B) = {x e. RR* | (A < x /\ x <_ B)})
Theorem	icoval 6502	Value of the closed-below, open-above interval function.
|- ((A e. RR* /\ B e. RR*) -> (A[,)B) = {x e. RR* | (A <_ x /\ x < B)})
Theorem	iccval 6503	Value of the closed interval function.
|- ((A e. RR* /\ B e. RR*) -> (A[,]B) = {x e. RR* | (A <_ x /\ x <_ B)})
Theorem	elioo1 6504	Membership in an open interval of extended reals.
|- ((A e. RR* /\ B e. RR*) -> (C e. (A(,)B) <-> (C e. RR* /\ A < C /\ C < B)))
Theorem	elioo2 6505	Membership in an open interval of extended reals.
|- ((A e. RR* /\ B e. RR*) -> (C e. (A(,)B) <-> (C e. RR /\ A < C /\ C < B)))
Theorem	elioo3g 6506	Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show A e. RR* and B e. RR*.
|- (B e. D -> (C e. (A(,)B) <-> ((A e. RR* /\ B e. RR* /\ C e. RR*) /\ (A < C /\ C < B))))
Theorem	elioc1 6507	Membership in an open-below, closed-above interval of extended reals.
|- ((A e. RR* /\ B e. RR*) -> (C e. (A(,]B) <-> (C e. RR* /\ A < C /\ C <_ B)))
Theorem	elico1 6508	Membership in a closed-below, open-above interval of extended reals.
|- ((A e. RR* /\ B e. RR*) -> (C e. (A[,)B) <-> (C e. RR* /\ A <_ C /\ C < B)))
Theorem	elicc1 6509	Membership in a closed interval of extended reals.
|- ((A e. RR* /\ B e. RR*) -> (C e. (A[,]B) <-> (C e. RR* /\ A <_ C /\ C <_ B)))
Theorem	elioo5 6510	Membership in an open interval of extended reals.
|- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> (C e. (A(,)B) <-> (A < C /\ C < B)))
Theorem	elioo4g 6511	Membership in an open interval of extended reals.
|- (B e. D -> (C e. (A(,)B) <-> ((A e. RR* /\ B e. RR* /\ C e. RR) /\ (A < C /\ C < B))))
Theorem	elioore 6512	A member of an open interval of reals is a real.
|- (A e. (B(,)C) -> A e. RR)
Theorem	eliooxr 6513	A non-empty open interval spans an interval of extended reals.
|- (A e. (B(,)C) -> (B e. RR* /\ C e. RR*))
Theorem	eliooord 6514	Ordering implied by a member of an open interval of reals.
|- (A e. (B(,)C) -> (B <_ A /\ A <_ C))
Theorem	ioossre 6515	An open interval is a set of reals.
|- (A(,)B) (_ RR
Theorem	elioc2 6516	Membership in an open-below, closed-above real interval. (Contributed by Paul Chapman, 30-Dec-2007.)
|- ((A e. RR /\ B e. RR) -> (C e. (A(,]B) <-> (C e. RR /\ A < C /\ C <_ B)))
Theorem	elico2 6517	Membership in a closed-below, open-above real interval. (Contributed by Paul Chapman, 21-Jan-2008.)
|- ((A e. RR /\ B e. RR) -> (C e. (A[,)B) <-> (C e. RR /\ A <_ C /\ C < B)))
Theorem	elicc2 6518	Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007.)
|- ((A e. RR /\ B e. RR) -> (C e. (A[,]B) <-> (C e. RR /\ A <_ C /\ C <_ B)))
Theorem	ioomax 6519	The open interval from minus to plus infinity.
|- ( -oo(,) +oo) = RR
Theorem	ioopos 6520	The set of positive reals expressed as an open interval.
|- (0(,) +oo) = {x e. RR | 0 < x}
Theorem	ioorp 6521	The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- (0(,) +oo) = RR+
Theorem	iooshf 6522	Shift the arguments of the open interval function.
|- (((A e. RR /\ B e. RR) /\ (C e. RR /\ D e. RR)) -> ((A - B) e. (C(,)D) <-> A e. ((C + B)(,)(D + B))))
Theorem	iccssre 6523	A closed real interval is a set of reals. (Contributed by FL, 6-Jun-2007. Proof shortened by Paul Chapman, 21-Jan-2008.)
|- ((A e. RR /\ B e. RR) -> (A[,]B) (_ RR)
Theorem	ioossicc 6524	An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.)
|- (A(,)B) (_ (A[,]B)
Theorem	iccsupr 6525	A nonempty subset of a closed real interval satisfies the conditions for the existence of its supremum (see suprcl 6223). (Contributed by Paul Chapman, 21-Jan-2008.)
|- (((A e. RR /\ B e. RR) /\ S (_ (A[,]B) /\ C e. S) -> (S (_ RR /\ S =/= (/) /\ E.x e. RR A.y e. S y <_ x))
Theorem	repos 6526	Two ways of saying that a real number is positive.
|- (A e. (0(,) +oo) <-> (A e. RR /\ 0 < A))
Theorem	ioof 6527	The set of open intervals of extended reals maps to subsets of reals.
|- (,):(RR* X. RR*)-->P~RR
Theorem	iccf 6528	The set of closed intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007.)
|- [,]:(RR* X. RR*)-->P~RR*
Theorem	unirnioo 6529	The union of the range of the open interval function.
|- U.ran (,) = RR
Theorem	dfioo2 6530	Alternate definition of the set of open intervals of extended reals.
|- (,) = {<.<.x, y>., z>. | ((x e. RR* /\ y e. RR*) /\ z = {w e. RR | (x < w /\ w < y)})}
Theorem	lbicc2 6531	The lower bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.)
|- ((A e. RR /\ B e. RR /\ A <_ B) -> A e. (A[,]B))
Theorem	ubicc2 6532	The upper bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.)
|- ((A e. RR /\ B e. RR /\ A <_ B) -> B e. (A[,]B))
Theorem	iooneg 6533	Membership in a negated open real interval. (Contributed by Paul Chapman, 26-Nov-2007.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (C e. (A(,)B) <-> -uC e. (-uB(,)-uA)))
Theorem	iccneg 6534	Membership in a negated closed real interval. (Contributed by Paul Chapman, 26-Nov-2007.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (C e. (A[,]B) <-> -uC e. (-uB[,]-uA)))
Theorem	icoshft 6535	A shifted real is a member of a shifted, closed-below, open-above real interval. (Contributed by Paul Chapman, 25-Mar-2008.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (X e. (A[,)B) -> (X + C) e. ((A + C)[,)(B + C))))
Theorem	icoshftf1oii 6536	Shifting a closed-below, open-above interval is one-to-one onto. (Contributed by Paul Chapman, 25-Mar-2008.)
|- F = {<.x, y>. | (x e. (A[,)B) /\ y = (x + C))}   &   |- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- F:(A[,)B)-1-1-onto->((A + C)[,)(B + C))
Theorem	icoshftf1olem 6537	Lemma for icoshftf1o 6538.
Theorem	icoshftf1o 6538	Shifting a closed-below, open-above interval is one-to-one onto. (Contributed by Paul Chapman, 25-Mar-2008.)
|- F = {<.x, y>. | (x e. (A[,)B) /\ y = (x + C))}   =>   |- ((A e. RR /\ B e. RR /\ C e. RR) -> F:(A[,)B)-1-1-onto->((A + C)[,)(B + C)))
Theorem	icounlem 6539	Lemma for icoun 6540.
Theorem	icoun 6540	The union of end-to-end closed-below, open-above real intervals. (Contributed by Paul Chapman, 15-Mar-2008.)
|- (((A e. RR /\ B e. RR /\ C e. RR) /\ (A <_ B /\ B <_ C)) -> ((A[,)B) u. (B[,)C)) = (A[,)C))
Theorem	snunioolem 6541	Lemma for snunioo 6542.
Theorem	snunioo 6542	The closure of one end of an open real interval. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ((A e. RR /\ B e. RR /\ A < B) -> ({A} u. (A(,)B)) = (A[,)B))
Theorem	ioojoin 6543	Join two open intervals to create a third.
|- (((A e. RR /\ B e. RR /\ C e. RR) /\ (A < B /\ B < C)) -> (((A(,)B) u. {B}) u. (B(,)C)) = (A(,)C))
Upper partititions of integers
Syntax	cuz 6544	Extend class notation with the upper integer function. Read "ZZ>=` M" as "the set of integers greater than or equal to M."
class ZZ>=
Definition	df-uz 6545	Define a function whose value at j is the semi-infinite set of contiguous integers starting at j, which we will also call the upper integers starting at j. Read "ZZ>=` M" as "the set of integers greater than or equal to M." See uzval 6546 for its value, uzssz 6557 for its relationship to ZZ, nnuz 6566 and nn0uz 6565 for its relationships to NN and NN0, and eluz1 6547 and eluz2 6548 for its membership relations.
|- ZZ>= = {<.j, y>. | (j e. ZZ /\ y = {k e. ZZ | j <_ k})}
Theorem	uzval 6546	The value of the upper integers function.
|- (N e. ZZ -> (ZZ>=` N) = {k e. ZZ | N <_ k})
Theorem	eluz1 6547	Membership in the set of upper integers starting at M.
|- (M e. ZZ -> (N e. (ZZ>=` M) <-> (N e. ZZ /\ M <_ N)))
Theorem	eluz2 6548	Membership in a set of upper integers. We use the fact that a function's value (under our function value definition) is empty outside of its domain to show M e. ZZ.
|- (N e. (ZZ>=` M) <-> (M e. ZZ /\ N e. ZZ /\ M <_ N))
Theorem	eluz1i 6549	Membership in a set of upper integers.
|- M e. ZZ   =>   |- (N e. (ZZ>=` M) <-> (N e. ZZ /\ M <_ N))
Theorem	eluzelz 6550	Implication of membership in a set of upper integers.
|- (N e. (ZZ>=` M) -> N e. ZZ)
Theorem	eluzel2 6551	Implication of membership in a set of upper integers.
|- (N e. (ZZ>=` M) -> M e. ZZ)
Theorem	eluzle 6552	Implication of membership in a set of upper integers.
|- (N e. (ZZ>=` M) -> M <_ N)
Theorem	eluz 6553	Membership in a set of upper integers.
|- ((M e. ZZ /\ N e. ZZ) -> (N e. (ZZ>=` M) <-> M <_ N))
Theorem	uzid 6554	Membership of the least member in a set of upper integers.
|- (M e. ZZ -> M e. (ZZ>=` M))
Theorem	uztrn 6555	Transitive law for sets of upper integers.
|- ((M e. (ZZ>=` K) /\ K e. (ZZ>=` N)) -> M e. (ZZ>=` N))
Theorem	uzneg 6556	Contraposition law for upper integers.
|- (N e. (ZZ>=` M) -> -uM e. (ZZ>=` -uN))
Theorem	uzssz 6557	A set of upper integers is a subset of all integers.
|- (ZZ>=` M) (_ ZZ
Theorem	uzss 6558	Subset relationship for two sets of upper integers.
|- (N e. (ZZ>=` M) -> (ZZ>=` N) (_ (ZZ>=` M))
Theorem	uz11 6559	The upper integers function is one-to-one.
|- (M e. ZZ -> ((ZZ>=` M) = (ZZ>=` N) <-> M = N))
Theorem	eluzp1m1 6560	Membership in the next set of upper integers.
|- ((M e. ZZ /\ N e. (ZZ>=` (M + 1))) -> (N - 1) e. (ZZ>=` M))
Theorem	eluzp1l 6561	Strict ordering implied by membership in the next set of upper integers.
|- ((M e. ZZ /\ N e. (ZZ>=` (M + 1))) -> M < N)
Theorem	eluzp1p1 6562	Membership in the next set of upper integers.
|- (N e. (ZZ>=` M) -> (N + 1) e. (ZZ>=` (M + 1)))
Theorem	eluzaddi 6563	Membership in a later set of upper integers. (Contributed by Paul Chapman, 22-Nov-2007.)
|- M e. ZZ   &   |- K e. ZZ   =>   |- (N e. (ZZ>=` M) -> (N + K) e. (ZZ>=` (M + K)))
Theorem	eluzsubi 6564	Membership in an earlier set of upper integers. (Contributed by Paul Chapman, 22-Nov-2007.)
|- M e. ZZ   &   |- K e. ZZ   =>   |- (N e. (ZZ>=` (M + K)) -> (N - K) e. (ZZ>=` M))
Theorem	nn0uz 6565	Nonnegative integers expressed as a set of upper integers.
|- NN0 = (ZZ>=` 0)
Theorem	nnuz 6566	Natural numbers expressed as a set of upper integers.
|- NN = (ZZ>=` 1)
Theorem	elnnuz 6567	A natural number expressed as a member of a set of upper integers.
|- (N e. NN <-> N e. (ZZ>=` 1))
Theorem	elnn0uz 6568	A nonnegative integer expressed as a member a set of upper integers.
|- (N e. NN0 <-> N e. (ZZ>=` 0))
Theorem	raluz 6569	Restricted universal quantification in a set of upper integers.
|- (M e. ZZ -> (A.n e. (ZZ>=` M)ph <-> A.n e. ZZ (M <_ n -> ph)))
Theorem	raluz2 6570	Restricted universal quantification in a set of upper integers.
|- (A.n e. (ZZ>=` M)ph <-> (M e. ZZ -> A.n e. ZZ (M <_ n -> ph)))
Theorem	rexuz 6571	Restricted existential quantification in a set of upper integers.
|- (M e. ZZ -> (E.n e. (ZZ>=` M)ph <-> E.n e. ZZ (M <_ n /\ ph)))
Theorem	rexuz2 6572	Restricted existential quantification in a set of upper integers.
|- (E.n e. (ZZ>=` M)ph <-> (M e. ZZ /\ E.n e. ZZ (M <_ n /\ ph)))
Theorem	2rexuz 6573	Double existential quantification in a set of upper integers.
|- (E.mE.n e. (ZZ>=` m)ph <-> E.m e. ZZ E.n e. ZZ (m <_ n /\ ph))
Theorem	peano2uz 6574	Second Peano postulate for a set of upper integers.
|- (N e. (ZZ>=` M) -> (N + 1) e. (ZZ>=` M))
Theorem	peano2uzr 6575	Reversed second Peano axiom for upper integers.
|- ((M e. ZZ /\ N e. (ZZ>=` (M + 1))) -> N e. (ZZ>=` M))
Theorem	uzaddcl 6576	Addition closure law for a set of upper integers.
|- ((N e. (ZZ>=` M) /\ K e. NN0) -> (N + K) e. (ZZ>=` M))
Theorem	uzind4 6577	Induction on the set of upper integers that starts at an integer M. The first four hypotheses give us the substitution instances we need, and the last two are the basis and the induction hypothesis.
|- (j = M -> (ph <-> ps))   &   |- (j = k -> (ph <-> ch))   &   |- (j = (k + 1) -> (ph <-> th))   &   |- (j = N -> (ph <-> ta))   &   |- (M e. ZZ -> ps)   &   |- (k e. (ZZ>=` M) -> (ch -> th))   =>   |- (N e. (ZZ>=` M) -> ta)
Theorem	uzind4ALT 6578	Alternate version of uzind4 6577 with different hypothesis order for easier use with the Metamath Proof Assistant, since "assign last" will assign the substitutions first. (This may or may not be kept permanenently, or it may replace uzind4 6577 - I haven't decided yet. -nm)
|- (M e. ZZ -> ps)   &   |- (k e. (ZZ>=` M) -> (ch -> th))   &   |- (j = M -> (ph <-> ps))   &   |- (j = k -> (ph <-> ch))   &   |- (j = (k + 1) -> (ph <-> th))   &   |- (j = N -> (ph <-> ta))   =>   |- (N e. (ZZ>=` M) -> ta)
Theorem	uzind4s 6579	Induction on the set of upper integers that starts at an integer M, using explicit substitution. The hypotheses are the basis and the induction hypothesis.
|- (M e. ZZ -> [M / k]ph)   &   |- (k e. (ZZ>=` M) -> (ph -> [(k + 1) / k]ph))   =>   |- (N e. (ZZ>=` M) -> [N / k]ph)
Theorem	uzind4s2 6580	Induction on the set of upper integers that starts at an integer M, using explicit substitution. The hypotheses are the basis and the induction hypothesis. Use this instead of uzind4s 6579 when j and k must be distinct in [(k + 1) / j]ph.
|- (M e. ZZ -> [M / j]ph)   &   |- (k e. (ZZ>=` M) -> ([k / j]ph -> [(k + 1) / j]ph))   =>   |- (N e. (ZZ>=` M) -> [N / j]ph)
Theorem	uzind4i 6581	Induction on the upper integers that start at M. The first hypothesis specifies the lower bound, the next four give us the substitution instances we need, and the last two are the basis and the induction hypothesis.
|- M e. ZZ   &   |- (j = M -> (ph <-> ps))   &   |- (j = k -> (ph <-> ch))   &   |- (j = (k + 1) -> (ph <-> th))   &   |- (j = N -> (ph <-> ta))   &   |- ps   &   |- (k e. (ZZ>=` M) -> (ch -> th))   =>   |- (N e. (ZZ>=` M) -> ta)
Theorem	uzwo 6582	Well-ordering principle: any non-empty subset of a set of upper integers has a least element.
|- ((S (_ (ZZ>=` M) /\ S =/= (/)) -> E.j e. S A.k e. S j <_ k)
Theorem	uzwoOLD 6583	Well-ordering principle: any non-empty subset of the upper integers has a least element.
|- ((S (_ (ZZ>=` M) /\ -. S = (/)) -> E.j e. S A.k e. S j <_ k)
Theorem	uzwo2 6584	Well-ordering principle: any non-empty subset of upper integers has a unique least element.
|- ((S (_ (ZZ>=` M) /\ S =/= (/)) -> E!j e. S A.k e. S j <_ k)
Theorem	nnwo 6585	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 6586	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 6587	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 6588	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	uzinfmi 6589	Extract the lower bound of a set of upper integers as its infimum. Note that the "`' <" argument turns supremum into infimum (for which we do not currently have a separate notation).
|- M e. ZZ   =>   |- sup((ZZ>=` M), RR, `' < ) = M
Theorem	nninfm 6590	The infimum of the set of natural numbers is one.
|- sup(NN, RR, `' < ) = 1
Theorem	nn0infm 6591	The infimum of the set of nonnegative integers is zero. Note that "`' <" turns sup into inf.
|- sup(NN0, RR, `' < ) = 0
Theorem	infmssuzle 6592	The infimum of a subset of a set of upper integers is less than or equal to all members of the subset. Note that the "`' < " argument turns supremum into infimum (for which we do not currently have a separate notation).
|- ((S (_ (ZZ>=` M) /\ S =/= (/) /\ A e. S) -> sup(S, RR, `' < ) <_ A)
Theorem	infmssuzleOLD 6593	The infimum of a subset of a set of upper integers is less than or equal to all members of the subset. Note that the "`' < " argument turns supremum into infimum (for which we do not currently have a separate notation).
|- ((S (_ (ZZ>=` M) /\ -. S = (/) /\ A e. S) -> sup(S, RR, `' < ) <_ A)
Theorem	infmssuzcl 6594	The infimum of a subset of a set of upper integers belongs to the subset.
|- ((S (_ (ZZ>=` M) /\ S =/= (/)) -> sup(S, RR, `' < ) e. S)
Finite intervals of integers
Syntax	cfz 6595	Extend class notation to include the notation for a contiguous finite set of integers. Read "M...N" as "the set of integers from M to N inclusive."
class ...
Definition	df-fz 6596	Define an operation that produces a finite set of sequential integers. Read "M...N" as "the set of integers from M to N inclusive." See fzval 6597 for its value and additional comments.
|- ... = {<.<.m, n>., z>. | ((m e. ZZ /\ n e. ZZ) /\ z = {k e. ZZ | (m <_ k /\ k <_ n)})}
Theorem	fzval 6597	The value of a finite set of sequential integers. E.g., 2...5 means the set {2, 3, 4, 5}. A special case of this definition (starting at 1) appears as Definition 11-2.1 of [Gleason] p. 141, where NNk means our 1...k; he calls these sets segments of the integers.
|- ((M e. ZZ /\ N e. ZZ) -> (M...N) = {k e. ZZ | (M <_ k /\ k <_ N)})
Theorem	elfz1 6598	Membership in a finite set of sequential integers.
|- ((M e. ZZ /\ N e. ZZ) -> (K e. (M...N) <-> (K e. ZZ /\ M <_ K /\ K <_ N)))
Theorem	elfz 6599	Membership in a finite set of sequential integers.
|- ((K e. ZZ /\ M e. ZZ /\ N e. ZZ) -> (K e. (M...N) <-> (M <_ K /\ K <_ N)))
Theorem	elfz2 6600	Membership in a finite set of sequential integers. We use the fact that an operation's value is empty outside of its domain to show M e. ZZ and N e. ZZ.
|- (N e. A -> (K e. (M...N) <-> ((M e. ZZ /\ N e. ZZ /\ K e. ZZ) /\ (M <_ K /\ K <_ N))))