Home Intuitionistic Logic ExplorerTheorem List (p. 87 of 95) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 8601-8700   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremioossico 8601 An open interval is a subset of its closure-below. (Contributed by Thierry Arnoux, 3-Mar-2017.)
(A(,)B) ⊆ (A[,)B)

Theoremiocssioo 8602 Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.)
(((A * B *) (A𝐶 𝐷 < B)) → (𝐶(,]𝐷) ⊆ (A(,)B))

Theoremicossioo 8603 Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.)
(((A * B *) (A < 𝐶 𝐷B)) → (𝐶[,)𝐷) ⊆ (A(,)B))

Theoremioossioo 8604 Condition for an open interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 26-Sep-2017.)
(((A * B *) (A𝐶 𝐷B)) → (𝐶(,)𝐷) ⊆ (A(,)B))

Theoremiccsupr 8605* A nonempty subset of a closed real interval satisfies the conditions for the existence of its supremum. To be useful without excluded middle, we'll probably need to change not equal to apart, and perhaps make other changes, but the theorem does hold as stated here. (Contributed by Paul Chapman, 21-Jan-2008.)
(((A B ℝ) 𝑆 ⊆ (A[,]B) 𝐶 𝑆) → (𝑆 ⊆ ℝ 𝑆 ≠ ∅ x y 𝑆 yx))

Theoremelioopnf 8606 Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.)
(A * → (B (A(,)+∞) ↔ (B A < B)))

Theoremelioomnf 8607 Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.)
(A * → (B (-∞(,)A) ↔ (B B < A)))

Theoremelicopnf 8608 Membership in a closed unbounded interval of reals. (Contributed by Mario Carneiro, 16-Sep-2014.)
(A ℝ → (B (A[,)+∞) ↔ (B AB)))

Theoremrepos 8609 Two ways of saying that a real number is positive. (Contributed by NM, 7-May-2007.)
(A (0(,)+∞) ↔ (A 0 < A))

Theoremioof 8610 The set of open intervals of extended reals maps to subsets of reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
(,):(ℝ* × ℝ*)⟶𝒫 ℝ

Theoremiccf 8611 The set of closed intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
[,]:(ℝ* × ℝ*)⟶𝒫 ℝ*

Theoremunirnioo 8612 The union of the range of the open interval function. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)
ℝ = ran (,)

Theoremdfioo2 8613* Alternate definition of the set of open intervals of extended reals. (Contributed by NM, 1-Mar-2007.) (Revised by Mario Carneiro, 1-Sep-2015.)
(,) = (x *, y * ↦ {w ℝ ∣ (x < w w < y)})

Theoremioorebasg 8614 Open intervals are elements of the set of all open intervals. (Contributed by Jim Kingdon, 4-Apr-2020.)
((A * B *) → (A(,)B) ran (,))

Theoremelrege0 8615 The predicate "is a nonnegative real". (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 18-Jun-2014.)
(A (0[,)+∞) ↔ (A 0 ≤ A))

Theoremrge0ssre 8616 Nonnegative real numbers are real numbers. (Contributed by Thierry Arnoux, 9-Sep-2018.) (Proof shortened by AV, 8-Sep-2019.)
(0[,)+∞) ⊆ ℝ

Theoremelxrge0 8617 Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.)
(A (0[,]+∞) ↔ (A * 0 ≤ A))

Theorem0e0icopnf 8618 0 is a member of (0[,)+∞) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
0 (0[,)+∞)

Theorem0e0iccpnf 8619 0 is a member of (0[,]+∞) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
0 (0[,]+∞)

Theoremge0addcl 8620 The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 19-Jun-2014.)
((A (0[,)+∞) B (0[,)+∞)) → (A + B) (0[,)+∞))

Theoremge0mulcl 8621 The nonnegative reals are closed under multiplication. (Contributed by Mario Carneiro, 19-Jun-2014.)
((A (0[,)+∞) B (0[,)+∞)) → (A · B) (0[,)+∞))

Theoremlbicc2 8622 The lower bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by FL, 29-May-2014.) (Revised by Mario Carneiro, 9-Sep-2015.)
((A * B * AB) → A (A[,]B))

Theoremubicc2 8623 The upper bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by FL, 29-May-2014.)
((A * B * AB) → B (A[,]B))

Theorem0elunit 8624 Zero is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.)
0 (0[,]1)

Theorem1elunit 8625 One is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.)
1 (0[,]1)

Theoremiooneg 8626 Membership in a negated open real interval. (Contributed by Paul Chapman, 26-Nov-2007.)
((A B 𝐶 ℝ) → (𝐶 (A(,)B) ↔ -𝐶 (-B(,)-A)))

Theoremiccneg 8627 Membership in a negated closed real interval. (Contributed by Paul Chapman, 26-Nov-2007.)
((A B 𝐶 ℝ) → (𝐶 (A[,]B) ↔ -𝐶 (-B[,]-A)))

Theoremicoshft 8628 A shifted real is a member of a shifted, closed-below, open-above real interval. (Contributed by Paul Chapman, 25-Mar-2008.)
((A B 𝐶 ℝ) → (𝑋 (A[,)B) → (𝑋 + 𝐶) ((A + 𝐶)[,)(B + 𝐶))))

Theoremicoshftf1o 8629* Shifting a closed-below, open-above interval is one-to-one onto. (Contributed by Paul Chapman, 25-Mar-2008.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
𝐹 = (x (A[,)B) ↦ (x + 𝐶))       ((A B 𝐶 ℝ) → 𝐹:(A[,)B)–1-1-onto→((A + 𝐶)[,)(B + 𝐶)))

Theoremicodisj 8630 End-to-end closed-below, open-above real intervals are disjoint. (Contributed by Mario Carneiro, 16-Jun-2014.)
((A * B * 𝐶 *) → ((A[,)B) ∩ (B[,)𝐶)) = ∅)

Theoremioodisj 8631 If the upper bound of one open interval is less than or equal to the lower bound of the other, the intervals are disjoint. (Contributed by Jeff Hankins, 13-Jul-2009.)
((((A * B *) (𝐶 * 𝐷 *)) B𝐶) → ((A(,)B) ∩ (𝐶(,)𝐷)) = ∅)

Theoremiccshftr 8632 Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
(A + 𝑅) = 𝐶    &   (B + 𝑅) = 𝐷       (((A B ℝ) (𝑋 𝑅 ℝ)) → (𝑋 (A[,]B) ↔ (𝑋 + 𝑅) (𝐶[,]𝐷)))

Theoremiccshftri 8633 Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
A     &   B     &   𝑅     &   (A + 𝑅) = 𝐶    &   (B + 𝑅) = 𝐷       (𝑋 (A[,]B) → (𝑋 + 𝑅) (𝐶[,]𝐷))

Theoremiccshftl 8634 Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
(A𝑅) = 𝐶    &   (B𝑅) = 𝐷       (((A B ℝ) (𝑋 𝑅 ℝ)) → (𝑋 (A[,]B) ↔ (𝑋𝑅) (𝐶[,]𝐷)))

Theoremiccshftli 8635 Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
A     &   B     &   𝑅     &   (A𝑅) = 𝐶    &   (B𝑅) = 𝐷       (𝑋 (A[,]B) → (𝑋𝑅) (𝐶[,]𝐷))

Theoremiccdil 8636 Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
(A · 𝑅) = 𝐶    &   (B · 𝑅) = 𝐷       (((A B ℝ) (𝑋 𝑅 +)) → (𝑋 (A[,]B) ↔ (𝑋 · 𝑅) (𝐶[,]𝐷)))

Theoremiccdili 8637 Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
A     &   B     &   𝑅 +    &   (A · 𝑅) = 𝐶    &   (B · 𝑅) = 𝐷       (𝑋 (A[,]B) → (𝑋 · 𝑅) (𝐶[,]𝐷))

Theoremicccntr 8638 Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
(A / 𝑅) = 𝐶    &   (B / 𝑅) = 𝐷       (((A B ℝ) (𝑋 𝑅 +)) → (𝑋 (A[,]B) ↔ (𝑋 / 𝑅) (𝐶[,]𝐷)))

Theoremicccntri 8639 Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
A     &   B     &   𝑅 +    &   (A / 𝑅) = 𝐶    &   (B / 𝑅) = 𝐷       (𝑋 (A[,]B) → (𝑋 / 𝑅) (𝐶[,]𝐷))

Theoremdivelunit 8640 A condition for a ratio to be a member of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.)
(((A 0 ≤ A) (B 0 < B)) → ((A / B) (0[,]1) ↔ AB))

Theoremlincmb01cmp 8641 A linear combination of two reals which lies in the interval between them. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 8-Sep-2015.)
(((A B A < B) 𝑇 (0[,]1)) → (((1 − 𝑇) · A) + (𝑇 · B)) (A[,]B))

Theoremiccf1o 8642* Describe a bijection from [0, 1] to an arbitrary nontrivial closed interval [A, B]. (Contributed by Mario Carneiro, 8-Sep-2015.)
𝐹 = (x (0[,]1) ↦ ((x · B) + ((1 − x) · A)))       ((A B A < B) → (𝐹:(0[,]1)–1-1-onto→(A[,]B) 𝐹 = (y (A[,]B) ↦ ((yA) / (BA)))))

Theoremunitssre 8643 (0[,]1) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.)
(0[,]1) ⊆ ℝ

3.5.4  Finite intervals of integers

Syntaxcfz 8644 Extend class notation to include the notation for a contiguous finite set of integers. Read "𝑀...𝑁 " as "the set of integers from 𝑀 to 𝑁 inclusive."
class ...

Definitiondf-fz 8645* Define an operation that produces a finite set of sequential integers. Read "𝑀...𝑁 " as "the set of integers from 𝑀 to 𝑁 inclusive." See fzval 8646 for its value and additional comments. (Contributed by NM, 6-Sep-2005.)
... = (𝑚 ℤ, 𝑛 ℤ ↦ {𝑘 ℤ ∣ (𝑚𝑘 𝑘𝑛)})

Theoremfzval 8646* 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 _k means our 1...𝑘; he calls these sets segments of the integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
((𝑀 𝑁 ℤ) → (𝑀...𝑁) = {𝑘 ℤ ∣ (𝑀𝑘 𝑘𝑁)})

Theoremfzval2 8647 An alternative way of expressing a finite set of sequential integers. (Contributed by Mario Carneiro, 3-Nov-2013.)
((𝑀 𝑁 ℤ) → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ))

Theoremfzf 8648 Establish the domain and codomain of the finite integer sequence function. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 16-Nov-2013.)
...:(ℤ × ℤ)⟶𝒫 ℤ

Theoremelfz1 8649 Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.)
((𝑀 𝑁 ℤ) → (𝐾 (𝑀...𝑁) ↔ (𝐾 𝑀𝐾 𝐾𝑁)))

Theoremelfz 8650 Membership in a finite set of sequential integers. (Contributed by NM, 29-Sep-2005.)
((𝐾 𝑀 𝑁 ℤ) → (𝐾 (𝑀...𝑁) ↔ (𝑀𝐾 𝐾𝑁)))

Theoremelfz2 8651 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 𝑀 and 𝑁 . (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐾 (𝑀...𝑁) ↔ ((𝑀 𝑁 𝐾 ℤ) (𝑀𝐾 𝐾𝑁)))

Theoremelfz5 8652 Membership in a finite set of sequential integers. (Contributed by NM, 26-Dec-2005.)
((𝐾 (ℤ𝑀) 𝑁 ℤ) → (𝐾 (𝑀...𝑁) ↔ 𝐾𝑁))

Theoremelfz4 8653 Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(((𝑀 𝑁 𝐾 ℤ) (𝑀𝐾 𝐾𝑁)) → 𝐾 (𝑀...𝑁))

Theoremelfzuzb 8654 Membership in a finite set of sequential integers in terms of sets of upper integers. (Contributed by NM, 18-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐾 (𝑀...𝑁) ↔ (𝐾 (ℤ𝑀) 𝑁 (ℤ𝐾)))

Theoremeluzfz 8655 Membership in a finite set of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
((𝐾 (ℤ𝑀) 𝑁 (ℤ𝐾)) → 𝐾 (𝑀...𝑁))

Theoremelfzuz 8656 A member of a finite set of sequential integers belongs to an upper set of integers. (Contributed by NM, 17-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐾 (𝑀...𝑁) → 𝐾 (ℤ𝑀))

Theoremelfzuz3 8657 Membership in a finite set of sequential integers implies membership in an upper set of integers. (Contributed by NM, 28-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐾 (𝑀...𝑁) → 𝑁 (ℤ𝐾))

Theoremelfzel2 8658 Membership in a finite set of sequential integer implies the upper bound is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐾 (𝑀...𝑁) → 𝑁 ℤ)

Theoremelfzel1 8659 Membership in a finite set of sequential integer implies the lower bound is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐾 (𝑀...𝑁) → 𝑀 ℤ)

Theoremelfzelz 8660 A member of a finite set of sequential integer is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐾 (𝑀...𝑁) → 𝐾 ℤ)

Theoremelfzle1 8661 A member of a finite set of sequential integer is greater than or equal to the lower bound. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐾 (𝑀...𝑁) → 𝑀𝐾)

Theoremelfzle2 8662 A member of a finite set of sequential integer is less than or equal to the upper bound. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐾 (𝑀...𝑁) → 𝐾𝑁)

Theoremelfzuz2 8663 Implication of membership in a finite set of sequential integers. (Contributed by NM, 20-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐾 (𝑀...𝑁) → 𝑁 (ℤ𝑀))

Theoremelfzle3 8664 Membership in a finite set of sequential integer implies the bounds are comparable. (Contributed by NM, 18-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐾 (𝑀...𝑁) → 𝑀𝑁)

Theoremeluzfz1 8665 Membership in a finite set of sequential integers - special case. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝑁 (ℤ𝑀) → 𝑀 (𝑀...𝑁))

Theoremeluzfz2 8666 Membership in a finite set of sequential integers - special case. (Contributed by NM, 13-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝑁 (ℤ𝑀) → 𝑁 (𝑀...𝑁))

Theoremeluzfz2b 8667 Membership in a finite set of sequential integers - special case. (Contributed by NM, 14-Sep-2005.)
(𝑁 (ℤ𝑀) ↔ 𝑁 (𝑀...𝑁))

Theoremelfz3 8668 Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 21-Jul-2005.)
(𝑁 ℤ → 𝑁 (𝑁...𝑁))

Theoremelfz1eq 8669 Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 19-Sep-2005.)
(𝐾 (𝑁...𝑁) → 𝐾 = 𝑁)

Theoremelfzubelfz 8670 If there is a member in a finite set of sequential integers, the upper bound is also a member of this finite set of sequential integers. (Contributed by Alexander van der Vekens, 31-May-2018.)
(𝐾 (𝑀...𝑁) → 𝑁 (𝑀...𝑁))

Theorempeano2fzr 8671 A Peano-postulate-like theorem for downward closure of a finite set of sequential integers. (Contributed by Mario Carneiro, 27-May-2014.)
((𝐾 (ℤ𝑀) (𝐾 + 1) (𝑀...𝑁)) → 𝐾 (𝑀...𝑁))

Theoremfzm 8672* Properties of a finite interval of integers which is inhabited. (Contributed by Jim Kingdon, 15-Apr-2020.)
(x x (𝑀...𝑁) ↔ 𝑁 (ℤ𝑀))

Theoremfztri3or 8673 Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.)
((𝐾 𝑀 𝑁 ℤ) → (𝐾 < 𝑀 𝐾 (𝑀...𝑁) 𝑁 < 𝐾))

Theoremfzdcel 8674 Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.)
((𝐾 𝑀 𝑁 ℤ) → DECID 𝐾 (𝑀...𝑁))

Theoremfznlem 8675 A finite set of sequential integers is empty if the bounds are reversed. (Contributed by Jim Kingdon, 16-Apr-2020.)
((𝑀 𝑁 ℤ) → (𝑁 < 𝑀 → (𝑀...𝑁) = ∅))

Theoremfzn 8676 A finite set of sequential integers is empty if the bounds are reversed. (Contributed by NM, 22-Aug-2005.)
((𝑀 𝑁 ℤ) → (𝑁 < 𝑀 ↔ (𝑀...𝑁) = ∅))

Theoremfzen 8677 A shifted finite set of sequential integers is equinumerous to the original set. (Contributed by Paul Chapman, 11-Apr-2009.)
((𝑀 𝑁 𝐾 ℤ) → (𝑀...𝑁) ≈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))

Theoremfz1n 8678 A 1-based finite set of sequential integers is empty iff it ends at index 0. (Contributed by Paul Chapman, 22-Jun-2011.)
(𝑁 0 → ((1...𝑁) = ∅ ↔ 𝑁 = 0))

Theorem0fz1 8679 Two ways to say a finite 1-based sequence is empty. (Contributed by Paul Chapman, 26-Oct-2012.)
((𝑁 0 𝐹 Fn (1...𝑁)) → (𝐹 = ∅ ↔ 𝑁 = 0))

Theoremfz10 8680 There are no integers between 1 and 0. (Contributed by Jeff Madsen, 16-Jun-2010.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
(1...0) = ∅

Theoremuzsubsubfz 8681 Membership of an integer greater than L decreased by ( L - M ) in an M based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018.)
((𝐿 (ℤ𝑀) 𝑁 (ℤ𝐿)) → (𝑁 − (𝐿𝑀)) (𝑀...𝑁))

Theoremuzsubsubfz1 8682 Membership of an integer greater than L decreased by ( L - 1 ) in a 1 based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018.)
((𝐿 𝑁 (ℤ𝐿)) → (𝑁 − (𝐿 − 1)) (1...𝑁))

Theoremige3m2fz 8683 Membership of an integer greater than 2 decreased by 2 in a 1 based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018.)
(𝑁 (ℤ‘3) → (𝑁 − 2) (1...𝑁))

Theoremfzsplit2 8684 Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016.)
(((𝐾 + 1) (ℤ𝑀) 𝑁 (ℤ𝐾)) → (𝑀...𝑁) = ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁)))

Theoremfzsplit 8685 Split a finite interval of integers into two parts. (Contributed by Jeff Madsen, 17-Jun-2010.) (Revised by Mario Carneiro, 13-Apr-2016.)
(𝐾 (𝑀...𝑁) → (𝑀...𝑁) = ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁)))

Theoremfzdisj 8686 Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010.)
(𝐾 < 𝑀 → ((𝐽...𝐾) ∩ (𝑀...𝑁)) = ∅)

Theoremfz01en 8687 0-based and 1-based finite sets of sequential integers are equinumerous. (Contributed by Paul Chapman, 11-Apr-2009.)
(𝑁 ℤ → (0...(𝑁 − 1)) ≈ (1...𝑁))

Theoremelfznn 8688 A member of a finite set of sequential integers starting at 1 is a positive integer. (Contributed by NM, 24-Aug-2005.)
(𝐾 (1...𝑁) → 𝐾 ℕ)

Theoremelfz1end 8689 A nonempty finite range of integers contains its end point. (Contributed by Stefan O'Rear, 10-Oct-2014.)
(A ℕ ↔ A (1...A))

Theoremfznn0sub 8690 Subtraction closure for a member of a finite set of sequential integers. (Contributed by NM, 16-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐾 (𝑀...𝑁) → (𝑁𝐾) 0)

Theoremfzmmmeqm 8691 Subtracting the difference of a member of a finite range of integers and the lower bound of the range from the difference of the upper bound and the lower bound of the range results in the difference of the upper bound of the range and the member. (Contributed by Alexander van der Vekens, 27-May-2018.)
(𝑀 (𝐿...𝑁) → ((𝑁𝐿) − (𝑀𝐿)) = (𝑁𝑀))

Theoremfzaddel 8692 Membership of a sum in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.)
(((𝑀 𝑁 ℤ) (𝐽 𝐾 ℤ)) → (𝐽 (𝑀...𝑁) ↔ (𝐽 + 𝐾) ((𝑀 + 𝐾)...(𝑁 + 𝐾))))

Theoremfzsubel 8693 Membership of a difference in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.)
(((𝑀 𝑁 ℤ) (𝐽 𝐾 ℤ)) → (𝐽 (𝑀...𝑁) ↔ (𝐽𝐾) ((𝑀𝐾)...(𝑁𝐾))))

Theoremfzopth 8694 A finite set of sequential integers can represent an ordered pair. (Contributed by NM, 31-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝑁 (ℤ𝑀) → ((𝑀...𝑁) = (𝐽...𝐾) ↔ (𝑀 = 𝐽 𝑁 = 𝐾)))

Theoremfzass4 8695 Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015.)
((B (A...𝐷) 𝐶 (B...𝐷)) ↔ (B (A...𝐶) 𝐶 (A...𝐷)))

Theoremfzss1 8696 Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
(𝐾 (ℤ𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁))

Theoremfzss2 8697 Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 30-Apr-2015.)
(𝑁 (ℤ𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁))

Theoremfzssuz 8698 A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005.)
(𝑀...𝑁) ⊆ (ℤ𝑀)

Theoremfzsn 8699 A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.)
(𝑀 ℤ → (𝑀...𝑀) = {𝑀})

Theoremfzssp1 8700 Subset relationship for finite sets of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))

Page List
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-9457
 Copyright terms: Public domain < Previous  Next >