mmtheorems65 - 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-10658

Statement List for Metamath Proof Explorer - 6401-6500 - Page 65 of 107

Type	Label	Description
Statement
Theorem	nnwos 6401	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 6402	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	uzinfm 6403	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 6404	The infimum of the set of natural numbers is one.
|- sup(NN, RR, `' < ) = 1
Theorem	nn0infm 6405	The infimum of the set of nonnegative integers is zero. Note that "`' <" turns sup into inf.
|- sup(NN0, RR, `' < ) = 0
Theorem	infmssuzle 6406	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 6407	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 6408	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 6409	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 fzvalt 6410 for its value and additional comments.
|- ... = {<.<.m, n>., z>. | ((m e. ZZ /\ n e. ZZ) /\ z = {k e. ZZ | (m <_ k /\ k <_ n)})}
Theorem	fzvalt 6410	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	elfz1t 6411	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	elfzt 6412	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	elfz2t 6413	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))))
Theorem	elfzlem 6414	Lemma for elfzel1 6422 and others.
Theorem	elfz5t 6415	Membership in a finite set of sequential integers.
|- ((K e. (ZZ>` M) /\ N e. ZZ) -> (K e. (M...N) <-> K <_ N))
Theorem	elfz4t 6416	Membership in a finite set of sequential integers.
|- (((M e. ZZ /\ N e. ZZ /\ K e. ZZ) /\ (M <_ K /\ K <_ N)) -> K e. (M...N))
Theorem	elfzuzb 6417	Membership in a finite set of sequential integers in terms of sets of upper integers.
|- (N e. A -> (K e. (M...N) <-> (K e. (ZZ>` M) /\ N e. (ZZ>` K))))
Theorem	eluzfzt 6418	Membership in a finite set of sequential integers.
|- ((K e. (ZZ>` M) /\ N e. (ZZ>` K)) -> K e. (M...N))
Theorem	elfzuz3t 6419	Membership in a finite set of sequential integers implies membership in a set of upper integers.
|- ((N e. A /\ K e. (M...N)) -> N e. (ZZ>` K))
Theorem	elfzel2 6420	Membership in a finite set of sequential integer implies the upper bound is an integer.
|- N e. V   =>   |- (K e. (M...N) -> N e. ZZ)
Theorem	elfzel2g 6421	Membership in a finite set of sequential integers implies the upper bound is an integer.
|- ((N e. A /\ K e. (M...N)) -> N e. ZZ)
Theorem	elfzel1 6422	Membership in a finite set of sequential integer implies the lower bound is an integer.
|- (K e. (M...N) -> M e. ZZ)
Theorem	elfzelz 6423	A member of a finite set of sequential integer is an integer.
|- (K e. (M...N) -> K e. ZZ)
Theorem	elfzle1 6424	A member of a finite set of sequential integer is greater than or equal to the lower bound.
|- (K e. (M...N) -> M <_ K)
Theorem	elfzle2 6425	A member of a finite set of sequential integer is less than or equal to the upper bound.
|- (K e. (M...N) -> K <_ N)
Theorem	elfzle3 6426	Membership in a finite set of sequential integer implies the bounds are comparable.
|- ((N e. A /\ K e. (M...N)) -> M <_ N)
Theorem	elfzuz2t 6427	Implication of membership in a finite set of sequential integers.
|- ((N e. A /\ K e. (M...N)) -> N e. (ZZ>` M))
Theorem	eluzfz1t 6428	Membership in a finite set of sequential integers - special case.
|- (N e. (ZZ>` M) -> M e. (M...N))
Theorem	elfzuzt 6429	A member of a finite set of sequential integers belongs to a set of upper integers.
|- (K e. (M...N) -> K e. (ZZ>` M))
Theorem	eluzfz2t 6430	Membership in a finite set of sequential integers - special case.
|- (N e. (ZZ>` M) -> N e. (M...N))
Theorem	eluzfz2b 6431	Membership in a finite set of sequential integers - special case.
|- (N e. (ZZ>` M) <-> N e. (M...N))
Theorem	elfz3t 6432	Membership in a finite set of sequential integers containing one integer.
|- (N e. ZZ -> N e. (N...N))
Theorem	elfz1eqt 6433	Membership in a finite set of sequential integers containing one integer.
|- (K e. (N...N) -> K = N)
Theorem	fznt 6434	A finite set of sequential integers is empty if the bounds are reversed.
|- ((M e. ZZ /\ N e. ZZ) -> (N < M <-> (M...N) = (/)))
Theorem	elfznnt 6435	A member of a finite set of sequential integers starting at 1 is a natural number.
|- (K e. (1...N) -> K e. NN)
Theorem	elfz2nn0t 6436	Membership in a finite set of sequential integers starting at 0.
|- (N e. A -> (K e. (0...N) <-> (K e. NN0 /\ N e. NN0 /\ K <_ N)))
Theorem	elfznn0t 6437	A member of a finite set of sequential integers starting at 0 is a nonnegative integer.
|- (K e. (0...N) -> K e. NN0)
Theorem	elfz3nn0t 6438	The upper bound of a nonempty finite set of sequential integers starting at 0 is a nonnegative integer.
|- ((N e. A /\ K e. (0...N)) -> N e. NN0)
Theorem	fznn0subt 6439	Subtraction closure for a member of a finite set of sequential integers.
|- ((N e. A /\ K e. (M...N)) -> (N - K) e. NN0)
Theorem	fznn0sub2t 6440	Subtraction closure for a member of a finite set of sequential integers.
|- ((N e. A /\ K e. (0...N)) -> (N - K) e. (0...N))
Theorem	fzaddelt 6441	Membership of a sum in a finite set of sequential integers.
|- (((M e. ZZ /\ N e. ZZ) /\ (J e. ZZ /\ K e. ZZ)) -> (J e. (M...N) <-> (J + K) e. ((M + K)...(N + K))))
Theorem	fzsubelt 6442	Membership of a difference in a finite set of sequential integers.
|- (((M e. ZZ /\ N e. ZZ) /\ (J e. ZZ /\ K e. ZZ)) -> (J e. (M...N) <-> (J - K) e. ((M - K)...(N - K))))
Theorem	fzoptht 6443	A finite set of sequential integers can represent an ordered pair.
|- ((N e. (ZZ>` M) /\ K e. A) -> ((M...N) = (J...K) <-> (M = J /\ N = K)))
Theorem	fzss1t 6444	Subset relationship for finite sets of sequential integers.
|- ((K e. (ZZ>` M) /\ N e. ZZ) -> (K...N) (_ (M...N))
Theorem	fzss2t 6445	Subset relationship for finite sets of sequential integers.
|- ((N e. (ZZ>` K) /\ M e. ZZ) -> (M...K) (_ (M...N))
Theorem	fzssuzt 6446	A finite set of sequential integers is a subset of a set of upper integers.
|- (M...N) (_ (ZZ>` M)
Theorem	fzssp1t 6447	Subset relationship for finite sets of sequential integers.
|- ((M e. ZZ /\ N e. ZZ) -> (M...N) (_ (M...(N + 1)))
Theorem	fzp1sst 6448	Subset relationship for finite sets of sequential integers.
|- ((M e. ZZ /\ N e. ZZ) -> ((M + 1)...N) (_ (M...N))
Theorem	fzelp1t 6449	Membership in a set of sequential integers with an appended element.
|- ((N e. A /\ K e. (M...N)) -> K e. (M...(N + 1)))
Theorem	fzelp1 6450	Membership in a set of sequential integers with an appended element.
|- N e. V   =>   |- (K e. (M...N) -> K e. (M...(N + 1)))
Theorem	elfzp1 6451	Append an element to a finite set of sequential integers.
|- (N e. (ZZ>` M) -> (K e. (M...(N + 1)) <-> (K e. (M...N) \/ K = (N + 1))))
Theorem	fzrevt 6452	Reversal of start and end of a finite set of sequential integers.
|- (((M e. ZZ /\ N e. ZZ) /\ (J e. ZZ /\ K e. ZZ)) -> (K e. ((J - N)...(J - M)) <-> (J - K) e. (M...N)))
Theorem	fzrev2t 6453	Reversal of start and end of a finite set of sequential integers.
|- (((M e. ZZ /\ N e. ZZ) /\ (J e. ZZ /\ K e. ZZ)) -> (K e. (M...N) <-> (J - K) e. ((J - N)...(J - M))))
Theorem	fzrev2it 6454	Reversal of start and end of a finite set of sequential integers.
|- ((N e. A /\ J e. ZZ /\ K e. (M...N)) -> (J - K) e. ((J - N)...(J - M)))
Theorem	fzrev3t 6455	The "complement" of a member of a finite set of sequential integers.
|- ((N e. A /\ K e. ZZ) -> (K e. (M...N) <-> ((M + N) - K) e. (M...N)))
Theorem	fzrev3it 6456	The "complement" of a member of a finite set of sequential integers.
|- ((N e. A /\ K e. (M...N)) -> ((M + N) - K) e. (M...N))
Theorem	fznn0t 6457	Finite set of sequential integers starting at 0.
|- (N e. NN0 -> (K e. (0...N) <-> (K e. NN0 /\