 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

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

Theoremlbicc2 8602 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 8603 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 8604 Zero is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.)
0 (0[,]1)

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

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

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

Theoremicoshft 8608 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 8609* 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 8610 End-to-end closed-below, open-above real intervals are disjoint. (Contributed by Mario Carneiro, 16-Jun-2014.)
((A * B * 𝐶 *) → ((A[,)B) ∩ (B[,)𝐶)) = ∅)

Theoremioodisj 8611 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 8612 Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
(A + 𝑅) = 𝐶    &   (B + 𝑅) = 𝐷       (((A B ℝ) (𝑋 𝑅 ℝ)) → (𝑋 (A[,]B) ↔ (𝑋 + 𝑅) (𝐶[,]𝐷)))

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

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

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

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

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

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

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

Theoremdivelunit 8620 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 8621 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 8622* 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 8623 (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 8624 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 8625* Define an operation that produces a finite set of sequential integers. Read "𝑀...𝑁 " as "the set of integers from 𝑀 to 𝑁 inclusive." See fzval 8626 for its value and additional comments. (Contributed by NM, 6-Sep-2005.)
... = (𝑚 ℤ, 𝑛 ℤ ↦ {𝑘 ℤ ∣ (𝑚𝑘 𝑘𝑛)})

Theoremfzval 8626* 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 8627 An alternative way of expressing a finite set of sequential integers. (Contributed by Mario Carneiro, 3-Nov-2013.)
((𝑀 𝑁 ℤ) → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ))

Theoremfzf 8628 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 8629 Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.)
((𝑀 𝑁 ℤ) → (𝐾 (𝑀...𝑁) ↔ (𝐾 𝑀𝐾 𝐾𝑁)))

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

Theoremelfz2 8631 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 8632 Membership in a finite set of sequential integers. (Contributed by NM, 26-Dec-2005.)
((𝐾 (ℤ𝑀) 𝑁 ℤ) → (𝐾 (𝑀...𝑁) ↔ 𝐾𝑁))

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

Theoremelfzuzb 8634 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 8635 Membership in a finite set of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
((𝐾 (ℤ𝑀) 𝑁 (ℤ𝐾)) → 𝐾 (𝑀...𝑁))

Theoremelfzuz 8636 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 8637 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 8638 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 8639 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 8640 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 8641 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 8642 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 8643 Implication of membership in a finite set of sequential integers. (Contributed by NM, 20-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐾 (𝑀...𝑁) → 𝑁 (ℤ𝑀))

Theoremelfzle3 8644 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 8645 Membership in a finite set of sequential integers - special case. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝑁 (ℤ𝑀) → 𝑀 (𝑀...𝑁))

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

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

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

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

Theoremelfzubelfz 8650 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 8651 A Peano-postulate-like theorem for downward closure of a finite set of sequential integers. (Contributed by Mario Carneiro, 27-May-2014.)
((𝐾 (ℤ𝑀) (𝐾 + 1) (𝑀...𝑁)) → 𝐾 (𝑀...𝑁))

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

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

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

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

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

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

Theoremfz1n 8658 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 8659 Two ways to say a finite 1-based sequence is empty. (Contributed by Paul Chapman, 26-Oct-2012.)
((𝑁 0 𝐹 Fn (1...𝑁)) → (𝐹 = ∅ ↔ 𝑁 = 0))

Theoremfz10 8660 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 8661 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 8662 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 8663 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 8664 Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016.)
(((𝐾 + 1) (ℤ𝑀) 𝑁 (ℤ𝐾)) → (𝑀...𝑁) = ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁)))

Theoremfzsplit 8665 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 8666 Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010.)
(𝐾 < 𝑀 → ((𝐽...𝐾) ∩ (𝑀...𝑁)) = ∅)

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

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

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

Theoremfznn0sub 8670 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 8671 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 8672 Membership of a sum in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.)
(((𝑀 𝑁 ℤ) (𝐽 𝐾 ℤ)) → (𝐽 (𝑀...𝑁) ↔ (𝐽 + 𝐾) ((𝑀 + 𝐾)...(𝑁 + 𝐾))))

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

Theoremfzopth 8674 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 8675 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 8676 Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
(𝐾 (ℤ𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁))

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

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

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

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

Theoremfzsuc 8681 Join a successor to the end of a finite set of sequential integers. (Contributed by NM, 19-Jul-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝑁 (ℤ𝑀) → (𝑀...(𝑁 + 1)) = ((𝑀...𝑁) ∪ {(𝑁 + 1)}))

Theoremfzpred 8682 Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.)
(𝑁 (ℤ𝑀) → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁)))

Theoremfzpreddisj 8683 A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019.)
(𝑁 (ℤ𝑀) → ({𝑀} ∩ ((𝑀 + 1)...𝑁)) = ∅)

Theoremelfzp1 8684 Append an element to a finite set of sequential integers. (Contributed by NM, 19-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
(𝑁 (ℤ𝑀) → (𝐾 (𝑀...(𝑁 + 1)) ↔ (𝐾 (𝑀...𝑁) 𝐾 = (𝑁 + 1))))

Theoremfzp1ss 8685 Subset relationship for finite sets of sequential integers. (Contributed by NM, 26-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝑀 ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁))

Theoremfzelp1 8686 Membership in a set of sequential integers with an appended element. (Contributed by NM, 7-Dec-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐾 (𝑀...𝑁) → 𝐾 (𝑀...(𝑁 + 1)))

Theoremfzp1elp1 8687 Add one to an element of a finite set of integers. (Contributed by Jeff Madsen, 6-Jun-2010.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐾 (𝑀...𝑁) → (𝐾 + 1) (𝑀...(𝑁 + 1)))

Theoremfznatpl1 8688 Shift membership in a finite sequence of naturals. (Contributed by Scott Fenton, 17-Jul-2013.)
((𝑁 𝐼 (1...(𝑁 − 1))) → (𝐼 + 1) (1...𝑁))

Theoremfzpr 8689 A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009.)
(𝑀 ℤ → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)})

Theoremfztp 8690 A finite interval of integers with three elements. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 7-Mar-2014.)
(𝑀 ℤ → (𝑀...(𝑀 + 2)) = {𝑀, (𝑀 + 1), (𝑀 + 2)})

Theoremfzsuc2 8691 Join a successor to the end of a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Mar-2014.)
((𝑀 𝑁 (ℤ‘(𝑀 − 1))) → (𝑀...(𝑁 + 1)) = ((𝑀...𝑁) ∪ {(𝑁 + 1)}))

Theoremfzp1disj 8692 (𝑀...(𝑁 + 1)) is the disjoint union of (𝑀...𝑁) with {(𝑁 + 1)}. (Contributed by Mario Carneiro, 7-Mar-2014.)
((𝑀...𝑁) ∩ {(𝑁 + 1)}) = ∅

Theoremfzdifsuc 8693 Remove a successor from the end of a finite set of sequential integers. (Contributed by AV, 4-Sep-2019.)
(𝑁 (ℤ𝑀) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)}))

Theoremfzprval 8694* Two ways of defining the first two values of a sequence on . (Contributed by NM, 5-Sep-2011.)
(x (1...2)(𝐹x) = if(x = 1, A, B) ↔ ((𝐹‘1) = A (𝐹‘2) = B))

Theoremfztpval 8695* Two ways of defining the first three values of a sequence on . (Contributed by NM, 13-Sep-2011.)
(x (1...3)(𝐹x) = if(x = 1, A, if(x = 2, B, 𝐶)) ↔ ((𝐹‘1) = A (𝐹‘2) = B (𝐹‘3) = 𝐶))

Theoremfzrev 8696 Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.)
(((𝑀 𝑁 ℤ) (𝐽 𝐾 ℤ)) → (𝐾 ((𝐽𝑁)...(𝐽𝑀)) ↔ (𝐽𝐾) (𝑀...𝑁)))

Theoremfzrev2 8697 Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.)
(((𝑀 𝑁 ℤ) (𝐽 𝐾 ℤ)) → (𝐾 (𝑀...𝑁) ↔ (𝐽𝐾) ((𝐽𝑁)...(𝐽𝑀))))

Theoremfzrev2i 8698 Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.)
((𝐽 𝐾 (𝑀...𝑁)) → (𝐽𝐾) ((𝐽𝑁)...(𝐽𝑀)))

Theoremfzrev3 8699 The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.)
(𝐾 ℤ → (𝐾 (𝑀...𝑁) ↔ ((𝑀 + 𝑁) − 𝐾) (𝑀...𝑁)))

Theoremfzrev3i 8700 The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.)
(𝐾 (𝑀...𝑁) → ((𝑀 + 𝑁) − 𝐾) (𝑀...𝑁))

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-9427
 Copyright terms: Public domain < Previous  Next >