Theorem List for Intuitionistic Logic Explorer - 9801-9900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | iooneg 9801 |
Membership in a negated open real interval. (Contributed by Paul Chapman,
26-Nov-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![(,) (,)](_ioo.gif) ![B B](_cb.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![(,) (,)](_ioo.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | iccneg 9802 |
Membership in a negated closed real interval. (Contributed by Paul
Chapman, 26-Nov-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![[,] [,]](_icc.gif) ![B B](_cb.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![[,] [,]](_icc.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | icoshft 9803 |
A shifted real is a member of a shifted, closed-below, open-above real
interval. (Contributed by Paul Chapman, 25-Mar-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![[,) [,)](_ico.gif) ![B B](_cb.gif) ![( (](lp.gif)
![C C](_cc.gif)
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![[,) [,)](_ico.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | icoshftf1o 9804* |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![[,) [,)](_ico.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif)
![F F](_cf.gif) ![: :](colon.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![[,) [,)](_ico.gif) ![B B](_cb.gif) ![) )](rp.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![[,) [,)](_ico.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | icodisj 9805 |
End-to-end closed-below, open-above real intervals are disjoint.
(Contributed by Mario Carneiro, 16-Jun-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR* RR*](_bbrast.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![[,) [,)](_ico.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![[,) [,)](_ico.gif) ![C C](_cc.gif) ![) )](rp.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | ioodisj 9806 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR* RR*](_bbrast.gif) ![( (](lp.gif)
![RR* RR*](_bbrast.gif) ![) )](rp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![(,) (,)](_ioo.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![(,) (,)](_ioo.gif) ![D D](_cd.gif) ![) )](rp.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | iccshftr 9807 |
Membership in a shifted interval. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![[,] [,]](_icc.gif) ![B B](_cb.gif) ![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif) ![C C](_cc.gif) ![[,] [,]](_icc.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | iccshftri 9808 |
Membership in a shifted interval. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![[,] [,]](_icc.gif) ![B B](_cb.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![C C](_cc.gif) ![[,] [,]](_icc.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | iccshftl 9809 |
Membership in a shifted interval. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![[,] [,]](_icc.gif) ![B B](_cb.gif) ![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif) ![C C](_cc.gif) ![[,] [,]](_icc.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | iccshftli 9810 |
Membership in a shifted interval. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![[,] [,]](_icc.gif) ![B B](_cb.gif) ![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![C C](_cc.gif) ![[,] [,]](_icc.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | iccdil 9811 |
Membership in a dilated interval. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![[,] [,]](_icc.gif) ![B B](_cb.gif) ![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif) ![C C](_cc.gif) ![[,] [,]](_icc.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | iccdili 9812 |
Membership in a dilated interval. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![[,] [,]](_icc.gif) ![B B](_cb.gif) ![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![C C](_cc.gif) ![[,] [,]](_icc.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | icccntr 9813 |
Membership in a contracted interval. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![[,] [,]](_icc.gif) ![B B](_cb.gif) ![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif) ![C C](_cc.gif) ![[,] [,]](_icc.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | icccntri 9814 |
Membership in a contracted interval. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![[,] [,]](_icc.gif) ![B B](_cb.gif) ![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![C C](_cc.gif) ![[,] [,]](_icc.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | divelunit 9815 |
A condition for a ratio to be a member of the closed unit. (Contributed
by Scott Fenton, 11-Jun-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![0
0](0.gif) ![[,] [,]](_icc.gif) ![1 1](1.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | lincmb01cmp 9816 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![0 0](0.gif) ![[,] [,]](_icc.gif) ![1 1](1.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![T T](_ct.gif)
![A A](_ca.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![[,] [,]](_icc.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | iccf1o 9817* |
Describe a bijection from ![[ [](lbrack.gif) ![0 0](0.gif) ![1 1](1.gif) to an arbitrary nontrivial
closed interval ![[ [](lbrack.gif) ![A A](_ca.gif) ![B B](_cb.gif) . (Contributed by Mario Carneiro,
8-Sep-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![[,] [,]](_icc.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![( (](lp.gif) ![0 0](0.gif) ![[,] [,]](_icc.gif) ![1 1](1.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![( (](lp.gif) ![A A](_ca.gif) ![[,] [,]](_icc.gif) ![B B](_cb.gif) ![`' `'](_cnv.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![[,] [,]](_icc.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | unitssre 9818 |
![( (](lp.gif) ![0 0](0.gif) ![[,] [,]](_icc.gif) ![1 1](1.gif) is a subset of the reals.
(Contributed by David Moews,
28-Feb-2017.)
|
![( (](lp.gif) ![0 0](0.gif) ![[,] [,]](_icc.gif) ![1 1](1.gif)
![RR RR](bbr.gif) |
|
Theorem | iccen 9819 |
Any nontrivial closed interval is equinumerous to the unit interval.
(Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario
Carneiro, 8-Sep-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![0 0](0.gif) ![[,] [,]](_icc.gif) ![1 1](1.gif)
![( (](lp.gif) ![A A](_ca.gif) ![[,] [,]](_icc.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | zltaddlt1le 9820 |
The sum of an integer and a real number between 0 and 1 is less than or
equal to a second integer iff the sum is less than the second integer.
(Contributed by AV, 1-Jul-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif) ![A A](_ca.gif)
![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
4.5.4 Finite intervals of integers
|
|
Syntax | cfz 9821 |
Extend class notation to include the notation for a contiguous finite set
of integers. Read "![M M](_cm.gif) ![... ...](ldots.gif) " as "the set of
integers from to
inclusive."
|
![... ...](ldots.gif) |
|
Definition | df-fz 9822* |
Define an operation that produces a finite set of sequential integers.
Read "![M M](_cm.gif) ![... ...](ldots.gif) " as "the set of integers from
to
inclusive." See fzval 9823 for its value and additional comments.
(Contributed by NM, 6-Sep-2005.)
|
![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![{ {](lbrace.gif) ![( (](lp.gif)
![n n](_n.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | fzval 9823* |
The value of a finite set of sequential integers. E.g., ![2 2](2.gif) ![... ...](ldots.gif)
means the set ![{ {](lbrace.gif) ![2 2](2.gif) ![3 3](3.gif) ![4 4](4.gif) ![5 5](5.gif) . A special case of this definition
(starting at 1) appears as Definition 11-2.1 of [Gleason] p. 141, where
k means our ![1 1](1.gif) ![... ...](ldots.gif) ; he calls these sets
segments of the
integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro,
3-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![{ {](lbrace.gif) ![( (](lp.gif)
![N N](_cn.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | fzval2 9824 |
An alternate way of expressing a finite set of sequential integers.
(Contributed by Mario Carneiro, 3-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![[,] [,]](_icc.gif) ![N N](_cn.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzf 9825 |
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.)
|
![...
...](ldots.gif) ![: :](colon.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![~P ~P](scrp.gif) ![ZZ ZZ](bbz.gif) |
|
Theorem | elfz1 9826 |
Membership in a finite set of sequential integers. (Contributed by NM,
21-Jul-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![(
(](lp.gif)
![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elfz 9827 |
Membership in a finite set of sequential integers. (Contributed by NM,
29-Sep-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elfz2 9828 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif)
![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elfz5 9829 |
Membership in a finite set of sequential integers. (Contributed by NM,
26-Dec-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif)
![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elfz4 9830 |
Membership in a finite set of sequential integers. (Contributed by NM,
21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif)
![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elfzuzb 9831 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eluzfz 9832 |
Membership in a finite set of sequential integers. (Contributed by NM,
4-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![K K](_ck.gif) ![) )](rp.gif)
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elfzuz 9833 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elfzuz3 9834 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elfzel2 9835 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
|
Theorem | elfzel1 9836 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
|
Theorem | elfzelz 9837 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
|
Theorem | elfzle1 9838 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![K K](_ck.gif) ![) )](rp.gif) |
|
Theorem | elfzle2 9839 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![N N](_cn.gif) ![) )](rp.gif) |
|
Theorem | elfzuz2 9840 |
Implication of membership in a finite set of sequential integers.
(Contributed by NM, 20-Sep-2005.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elfzle3 9841 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![N N](_cn.gif) ![) )](rp.gif) |
|
Theorem | eluzfz1 9842 |
Membership in a finite set of sequential integers - special case.
(Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif)
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eluzfz2 9843 |
Membership in a finite set of sequential integers - special case.
(Contributed by NM, 13-Sep-2005.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif)
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eluzfz2b 9844 |
Membership in a finite set of sequential integers - special case.
(Contributed by NM, 14-Sep-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif)
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elfz3 9845 |
Membership in a finite set of sequential integers containing one integer.
(Contributed by NM, 21-Jul-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![...
...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elfz1eq 9846 |
Membership in a finite set of sequential integers containing one integer.
(Contributed by NM, 19-Sep-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![... ...](ldots.gif) ![N N](_cn.gif)
![N N](_cn.gif) ![) )](rp.gif) |
|
Theorem | elfzubelfz 9847 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif)
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | peano2fzr 9848 |
A Peano-postulate-like theorem for downward closure of a finite set of
sequential integers. (Contributed by Mario Carneiro, 27-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![M M](_cm.gif) ![...
...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![...
...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzm 9849* |
Properties of a finite interval of integers which is inhabited.
(Contributed by Jim Kingdon, 15-Apr-2020.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fztri3or 9850 |
Trichotomy in terms of a finite interval of integers. (Contributed by Jim
Kingdon, 1-Jun-2020.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![...
...](ldots.gif) ![N N](_cn.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzdcel 9851 |
Decidability of membership in a finite interval of integers. (Contributed
by Jim Kingdon, 1-Jun-2020.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) DECID ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fznlem 9852 |
A finite set of sequential integers is empty if the bounds are reversed.
(Contributed by Jim Kingdon, 16-Apr-2020.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzn 9853 |
A finite set of sequential integers is empty if the bounds are reversed.
(Contributed by NM, 22-Aug-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzen 9854 |
A shifted finite set of sequential integers is equinumerous to the
original set. (Contributed by Paul Chapman, 11-Apr-2009.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fz1n 9855 |
A 1-based finite set of sequential integers is empty iff it ends at index
. (Contributed by
Paul Chapman, 22-Jun-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N
N](_cn.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | 0fz1 9856 |
Two ways to say a finite 1-based sequence is empty. (Contributed by Paul
Chapman, 26-Oct-2012.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![...
...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fz10 9857 |
There are no integers between 1 and 0. (Contributed by Jeff Madsen,
16-Jun-2010.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
|
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![0 0](0.gif) ![(/) (/)](varnothing.gif) |
|
Theorem | uzsubsubfz 9858 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![L L](_cl.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | uzsubsubfz1 9859 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![L L](_cl.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N
N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ige3m2fz 9860 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![3 3](3.gif) ![( (](lp.gif)
![2 2](2.gif) ![( (](lp.gif) ![1 1](1.gif) ![...
...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzsplit2 9861 |
Split a finite interval of integers into two parts. (Contributed by
Mario Carneiro, 13-Apr-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![...
...](ldots.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzsplit 9862 |
Split a finite interval of integers into two parts. (Contributed by
Jeff Madsen, 17-Jun-2010.) (Revised by Mario Carneiro, 13-Apr-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![...
...](ldots.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzdisj 9863 |
Condition for two finite intervals of integers to be disjoint.
(Contributed by Jeff Madsen, 17-Jun-2010.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![J J](_cj.gif) ![... ...](ldots.gif) ![K K](_ck.gif) ![( (](lp.gif) ![M M](_cm.gif) ![...
...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | fz01en 9864 |
0-based and 1-based finite sets of sequential integers are equinumerous.
(Contributed by Paul Chapman, 11-Apr-2009.)
|
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N
N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elfznn 9865 |
A member of a finite set of sequential integers starting at 1 is a
positive integer. (Contributed by NM, 24-Aug-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif)
![NN NN](bbn.gif) ![) )](rp.gif) |
|
Theorem | elfz1end 9866 |
A nonempty finite range of integers contains its end point. (Contributed
by Stefan O'Rear, 10-Oct-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fz1ssnn 9867 |
A finite set of positive integers is a set of positive integers.
(Contributed by Stefan O'Rear, 16-Oct-2014.)
|
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![A A](_ca.gif) ![NN NN](bbn.gif) |
|
Theorem | fznn0sub 9868 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif)
![K K](_ck.gif)
![NN0 NN0](_bbn0.gif) ![) )](rp.gif) |
|
Theorem | fzmmmeqm 9869 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![L L](_cl.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![L L](_cl.gif)
![( (](lp.gif) ![L L](_cl.gif) ![) )](rp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzaddel 9870 |
Membership of a sum in a finite set of sequential integers. (Contributed
by NM, 30-Jul-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![K K](_ck.gif)
![( (](lp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzsubel 9871 |
Membership of a difference in a finite set of sequential integers.
(Contributed by NM, 30-Jul-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![K K](_ck.gif)
![( (](lp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzopth 9872 |
A finite set of sequential integers can represent an ordered pair.
(Contributed by NM, 31-Oct-2005.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![J J](_cj.gif) ![...
...](ldots.gif) ![K K](_ck.gif) ![( (](lp.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzass4 9873 |
Two ways to express a nondecreasing sequence of four integers.
(Contributed by Stefan O'Rear, 15-Aug-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![... ...](ldots.gif) ![D D](_cd.gif) ![( (](lp.gif) ![B B](_cb.gif) ![... ...](ldots.gif) ![D D](_cd.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![... ...](ldots.gif) ![C C](_cc.gif)
![( (](lp.gif) ![A A](_ca.gif) ![... ...](ldots.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzss1 9874 |
Subset relationship for finite sets of sequential integers.
(Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro,
28-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![K K](_ck.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzss2 9875 |
Subset relationship for finite sets of sequential integers.
(Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro,
30-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![K K](_ck.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![K K](_ck.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzssuz 9876 |
A finite set of sequential integers is a subset of an upper set of
integers. (Contributed by NM, 28-Oct-2005.)
|
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) |
|
Theorem | fzsn 9877 |
A finite interval of integers with one element. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![M M](_cm.gif)
![{ {](lbrace.gif) ![M M](_cm.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | fzssp1 9878 |
Subset relationship for finite sets of sequential integers.
(Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | fzssnn 9879 |
Finite sets of sequential integers starting from a natural are a subset of
the positive integers. (Contributed by Thierry Arnoux, 4-Aug-2017.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![NN NN](bbn.gif) ![) )](rp.gif) |
|
Theorem | fzsuc 9880 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![...
...](ldots.gif) ![N N](_cn.gif) ![{
{](lbrace.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | fzpred 9881 |
Join a predecessor to the beginning of a finite set of sequential
integers. (Contributed by AV, 24-Aug-2019.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzpreddisj 9882 |
A finite set of sequential integers is disjoint with its predecessor.
(Contributed by AV, 24-Aug-2019.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | elfzp1 9883 |
Append an element to a finite set of sequential integers. (Contributed by
NM, 19-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif)
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzp1ss 9884 |
Subset relationship for finite sets of sequential integers. (Contributed
by NM, 26-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzelp1 9885 |
Membership in a set of sequential integers with an appended element.
(Contributed by NM, 7-Dec-2005.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif)
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzp1elp1 9886 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif)
![1 1](1.gif) ![( (](lp.gif) ![M M](_cm.gif) ![...
...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fznatpl1 9887 |
Shift membership in a finite sequence of naturals. (Contributed by Scott
Fenton, 17-Jul-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![1 1](1.gif) ![...
...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzpr 9888 |
A finite interval of integers with two elements. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![M M](_cm.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | fztp 9889 |
A finite interval of integers with three elements. (Contributed by NM,
13-Sep-2011.) (Revised by Mario Carneiro, 7-Mar-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![M M](_cm.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
|
Theorem | fzsuc2 9890 |
Join a successor to the end of a finite set of sequential integers.
(Contributed by Mario Carneiro, 7-Mar-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | fzp1disj 9891 |
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) is the
disjoint union of ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) with
![{ {](lbrace.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) . (Contributed by Mario Carneiro, 7-Mar-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![{ {](lbrace.gif) ![( (](lp.gif)
![1 1](1.gif) ![) )](rp.gif) ![} }](rbrace.gif)
![(/) (/)](varnothing.gif) |
|
Theorem | fzdifsuc 9892 |
Remove a successor from the end of a finite set of sequential integers.
(Contributed by AV, 4-Sep-2019.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![...
...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | fzprval 9893* |
Two ways of defining the first two values of a sequence on .
(Contributed by NM, 5-Sep-2011.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif)
![if if](_if.gif) ![( (](lp.gif)
![1 1](1.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![1 1](1.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![2 2](2.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fztpval 9894* |
Two ways of defining the first three values of a sequence on .
(Contributed by NM, 13-Sep-2011.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![3 3](3.gif) ![)
)](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif)
![if if](_if.gif) ![( (](lp.gif)
![1 1](1.gif) ![A A](_ca.gif) ![if if](_if.gif) ![( (](lp.gif)
![2 2](2.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![1 1](1.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![2 2](2.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![3 3](3.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzrev 9895 |
Reversal of start and end of a finite set of sequential integers.
(Contributed by NM, 25-Nov-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![K K](_ck.gif)
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzrev2 9896 |
Reversal of start and end of a finite set of sequential integers.
(Contributed by NM, 25-Nov-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![K K](_ck.gif)
![( (](lp.gif) ![(
(](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzrev2i 9897 |
Reversal of start and end of a finite set of sequential integers.
(Contributed by NM, 25-Nov-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![K K](_ck.gif)
![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![( (](lp.gif)
![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzrev3 9898 |
The "complement" of a member of a finite set of sequential integers.
(Contributed by NM, 20-Nov-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![K K](_ck.gif)
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fzrev3i 9899 |
The "complement" of a member of a finite set of sequential integers.
(Contributed by NM, 20-Nov-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif)
![K K](_ck.gif)
![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fznn 9900 |
Finite set of sequential integers starting at 1. (Contributed by NM,
31-Aug-2011.) (Revised by Mario Carneiro, 18-Jun-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |