Theorem List for Intuitionistic Logic Explorer - 9001-9100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | elxrge0 9001 |
Elementhood in the set of nonnegative extended reals. (Contributed by
Mario Carneiro, 28-Jun-2014.)
|
⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴)) |
|
Theorem | 0e0icopnf 9002 |
0 is a member of (0[,)+∞) (common case).
(Contributed by David
A. Wheeler, 8-Dec-2018.)
|
⊢ 0 ∈ (0[,)+∞) |
|
Theorem | 0e0iccpnf 9003 |
0 is a member of (0[,]+∞) (common case).
(Contributed by David
A. Wheeler, 8-Dec-2018.)
|
⊢ 0 ∈ (0[,]+∞) |
|
Theorem | ge0addcl 9004 |
The nonnegative reals are closed under addition. (Contributed by Mario
Carneiro, 19-Jun-2014.)
|
⊢ ((𝐴 ∈ (0[,)+∞) ∧ 𝐵 ∈ (0[,)+∞)) →
(𝐴 + 𝐵) ∈ (0[,)+∞)) |
|
Theorem | ge0mulcl 9005 |
The nonnegative reals are closed under multiplication. (Contributed by
Mario Carneiro, 19-Jun-2014.)
|
⊢ ((𝐴 ∈ (0[,)+∞) ∧ 𝐵 ∈ (0[,)+∞)) →
(𝐴 · 𝐵) ∈
(0[,)+∞)) |
|
Theorem | lbicc2 9006 |
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.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
|
Theorem | ubicc2 9007 |
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.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
|
Theorem | 0elunit 9008 |
Zero is an element of the closed unit. (Contributed by Scott Fenton,
11-Jun-2013.)
|
⊢ 0 ∈ (0[,]1) |
|
Theorem | 1elunit 9009 |
One is an element of the closed unit. (Contributed by Scott Fenton,
11-Jun-2013.)
|
⊢ 1 ∈ (0[,]1) |
|
Theorem | iooneg 9010 |
Membership in a negated open real interval. (Contributed by Paul Chapman,
26-Nov-2007.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (𝐴(,)𝐵) ↔ -𝐶 ∈ (-𝐵(,)-𝐴))) |
|
Theorem | iccneg 9011 |
Membership in a negated closed real interval. (Contributed by Paul
Chapman, 26-Nov-2007.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ -𝐶 ∈ (-𝐵[,]-𝐴))) |
|
Theorem | icoshft 9012 |
A shifted real is a member of a shifted, closed-below, open-above real
interval. (Contributed by Paul Chapman, 25-Mar-2008.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑋 ∈ (𝐴[,)𝐵) → (𝑋 + 𝐶) ∈ ((𝐴 + 𝐶)[,)(𝐵 + 𝐶)))) |
|
Theorem | icoshftf1o 9013* |
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.)
|
⊢ 𝐹 = (𝑥 ∈ (𝐴[,)𝐵) ↦ (𝑥 + 𝐶)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐹:(𝐴[,)𝐵)–1-1-onto→((𝐴 + 𝐶)[,)(𝐵 + 𝐶))) |
|
Theorem | icodisj 9014 |
End-to-end closed-below, open-above real intervals are disjoint.
(Contributed by Mario Carneiro, 16-Jun-2014.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴[,)𝐵) ∩ (𝐵[,)𝐶)) = ∅) |
|
Theorem | ioodisj 9015 |
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.)
|
⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (𝐶 ∈
ℝ* ∧ 𝐷 ∈ ℝ*)) ∧ 𝐵 ≤ 𝐶) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) = ∅) |
|
Theorem | iccshftr 9016 |
Membership in a shifted interval. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ (𝐴 + 𝑅) = 𝐶
& ⊢ (𝐵 + 𝑅) = 𝐷 ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 + 𝑅) ∈ (𝐶[,]𝐷))) |
|
Theorem | iccshftri 9017 |
Membership in a shifted interval. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝑅 ∈ ℝ & ⊢ (𝐴 + 𝑅) = 𝐶
& ⊢ (𝐵 + 𝑅) = 𝐷 ⇒ ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 + 𝑅) ∈ (𝐶[,]𝐷)) |
|
Theorem | iccshftl 9018 |
Membership in a shifted interval. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ (𝐴 − 𝑅) = 𝐶
& ⊢ (𝐵 − 𝑅) = 𝐷 ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 − 𝑅) ∈ (𝐶[,]𝐷))) |
|
Theorem | iccshftli 9019 |
Membership in a shifted interval. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝑅 ∈ ℝ & ⊢ (𝐴 − 𝑅) = 𝐶
& ⊢ (𝐵 − 𝑅) = 𝐷 ⇒ ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 − 𝑅) ∈ (𝐶[,]𝐷)) |
|
Theorem | iccdil 9020 |
Membership in a dilated interval. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ (𝐴 · 𝑅) = 𝐶
& ⊢ (𝐵 · 𝑅) = 𝐷 ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 · 𝑅) ∈ (𝐶[,]𝐷))) |
|
Theorem | iccdili 9021 |
Membership in a dilated interval. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝑅 ∈
ℝ+
& ⊢ (𝐴 · 𝑅) = 𝐶
& ⊢ (𝐵 · 𝑅) = 𝐷 ⇒ ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 · 𝑅) ∈ (𝐶[,]𝐷)) |
|
Theorem | icccntr 9022 |
Membership in a contracted interval. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ (𝐴 / 𝑅) = 𝐶
& ⊢ (𝐵 / 𝑅) = 𝐷 ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 / 𝑅) ∈ (𝐶[,]𝐷))) |
|
Theorem | icccntri 9023 |
Membership in a contracted interval. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝑅 ∈
ℝ+
& ⊢ (𝐴 / 𝑅) = 𝐶
& ⊢ (𝐵 / 𝑅) = 𝐷 ⇒ ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 / 𝑅) ∈ (𝐶[,]𝐷)) |
|
Theorem | divelunit 9024 |
A condition for a ratio to be a member of the closed unit. (Contributed
by Scott Fenton, 11-Jun-2013.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((𝐴 / 𝐵) ∈ (0[,]1) ↔ 𝐴 ≤ 𝐵)) |
|
Theorem | lincmb01cmp 9025 |
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.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐵)) ∈ (𝐴[,]𝐵)) |
|
Theorem | iccf1o 9026* |
Describe a bijection from [0, 1] to an arbitrary
nontrivial
closed interval [𝐴, 𝐵]. (Contributed by Mario Carneiro,
8-Sep-2015.)
|
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴))) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐹:(0[,]1)–1-1-onto→(𝐴[,]𝐵) ∧ ◡𝐹 = (𝑦 ∈ (𝐴[,]𝐵) ↦ ((𝑦 − 𝐴) / (𝐵 − 𝐴))))) |
|
Theorem | unitssre 9027 |
(0[,]1) is a subset of the reals. (Contributed by
David Moews,
28-Feb-2017.)
|
⊢ (0[,]1) ⊆ ℝ |
|
Theorem | zltaddlt1le 9028 |
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.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ (0(,)1)) → ((𝑀 + 𝐴) < 𝑁 ↔ (𝑀 + 𝐴) ≤ 𝑁)) |
|
3.5.4 Finite intervals of integers
|
|
Syntax | cfz 9029 |
Extend class notation to include the notation for a contiguous finite set
of integers. Read "𝑀...𝑁 " as "the set of integers
from 𝑀 to
𝑁 inclusive."
|
class ... |
|
Definition | df-fz 9030* |
Define an operation that produces a finite set of sequential integers.
Read "𝑀...𝑁 " as "the set of integers
from 𝑀 to 𝑁
inclusive." See fzval 9031 for its value and additional comments.
(Contributed by NM, 6-Sep-2005.)
|
⊢ ... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)}) |
|
Theorem | fzval 9031* |
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.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = {𝑘 ∈ ℤ ∣ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)}) |
|
Theorem | fzval2 9032 |
An alternate way of expressing a finite set of sequential integers.
(Contributed by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ)) |
|
Theorem | fzf 9033 |
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.)
|
⊢ ...:(ℤ ×
ℤ)⟶𝒫 ℤ |
|
Theorem | elfz1 9034 |
Membership in a finite set of sequential integers. (Contributed by NM,
21-Jul-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
|
Theorem | elfz 9035 |
Membership in a finite set of sequential integers. (Contributed by NM,
29-Sep-2005.)
|
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
|
Theorem | elfz2 9036 |
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.)
|
⊢ (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
|
Theorem | elfz5 9037 |
Membership in a finite set of sequential integers. (Contributed by NM,
26-Dec-2005.)
|
⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ 𝐾 ≤ 𝑁)) |
|
Theorem | elfz4 9038 |
Membership in a finite set of sequential integers. (Contributed by NM,
21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) → 𝐾 ∈ (𝑀...𝑁)) |
|
Theorem | elfzuzb 9039 |
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.)
|
⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾))) |
|
Theorem | eluzfz 9040 |
Membership in a finite set of sequential integers. (Contributed by NM,
4-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|
⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝐾 ∈ (𝑀...𝑁)) |
|
Theorem | elfzuz 9041 |
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.)
|
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀)) |
|
Theorem | elfzuz3 9042 |
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.)
|
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) |
|
Theorem | elfzel2 9043 |
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.)
|
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ) |
|
Theorem | elfzel1 9044 |
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.)
|
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ) |
|
Theorem | elfzelz 9045 |
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.)
|
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ) |
|
Theorem | elfzle1 9046 |
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.)
|
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐾) |
|
Theorem | elfzle2 9047 |
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.)
|
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ≤ 𝑁) |
|
Theorem | elfzuz2 9048 |
Implication of membership in a finite set of sequential integers.
(Contributed by NM, 20-Sep-2005.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝑀)) |
|
Theorem | elfzle3 9049 |
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.)
|
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝑁) |
|
Theorem | eluzfz1 9050 |
Membership in a finite set of sequential integers - special case.
(Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
|
Theorem | eluzfz2 9051 |
Membership in a finite set of sequential integers - special case.
(Contributed by NM, 13-Sep-2005.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
|
Theorem | eluzfz2b 9052 |
Membership in a finite set of sequential integers - special case.
(Contributed by NM, 14-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑁 ∈ (𝑀...𝑁)) |
|
Theorem | elfz3 9053 |
Membership in a finite set of sequential integers containing one integer.
(Contributed by NM, 21-Jul-2005.)
|
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (𝑁...𝑁)) |
|
Theorem | elfz1eq 9054 |
Membership in a finite set of sequential integers containing one integer.
(Contributed by NM, 19-Sep-2005.)
|
⊢ (𝐾 ∈ (𝑁...𝑁) → 𝐾 = 𝑁) |
|
Theorem | elfzubelfz 9055 |
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.)
|
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (𝑀...𝑁)) |
|
Theorem | peano2fzr 9056 |
A Peano-postulate-like theorem for downward closure of a finite set of
sequential integers. (Contributed by Mario Carneiro, 27-May-2014.)
|
⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ (𝐾 + 1) ∈ (𝑀...𝑁)) → 𝐾 ∈ (𝑀...𝑁)) |
|
Theorem | fzm 9057* |
Properties of a finite interval of integers which is inhabited.
(Contributed by Jim Kingdon, 15-Apr-2020.)
|
⊢ (∃𝑥 𝑥 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (ℤ≥‘𝑀)) |
|
Theorem | fztri3or 9058 |
Trichotomy in terms of a finite interval of integers. (Contributed by Jim
Kingdon, 1-Jun-2020.)
|
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑀 ∨ 𝐾 ∈ (𝑀...𝑁) ∨ 𝑁 < 𝐾)) |
|
Theorem | fzdcel 9059 |
Decidability of membership in a finite interval of integers. (Contributed
by Jim Kingdon, 1-Jun-2020.)
|
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
DECID 𝐾
∈ (𝑀...𝑁)) |
|
Theorem | fznlem 9060 |
A finite set of sequential integers is empty if the bounds are reversed.
(Contributed by Jim Kingdon, 16-Apr-2020.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < 𝑀 → (𝑀...𝑁) = ∅)) |
|
Theorem | fzn 9061 |
A finite set of sequential integers is empty if the bounds are reversed.
(Contributed by NM, 22-Aug-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < 𝑀 ↔ (𝑀...𝑁) = ∅)) |
|
Theorem | fzen 9062 |
A shifted finite set of sequential integers is equinumerous to the
original set. (Contributed by Paul Chapman, 11-Apr-2009.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀...𝑁) ≈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) |
|
Theorem | fz1n 9063 |
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)) |
|
Theorem | 0fz1 9064 |
Two ways to say a finite 1-based sequence is empty. (Contributed by Paul
Chapman, 26-Oct-2012.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 Fn (1...𝑁)) → (𝐹 = ∅ ↔ 𝑁 = 0)) |
|
Theorem | fz10 9065 |
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) = ∅ |
|
Theorem | uzsubsubfz 9066 |
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.)
|
⊢ ((𝐿 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐿)) → (𝑁 − (𝐿 − 𝑀)) ∈ (𝑀...𝑁)) |
|
Theorem | uzsubsubfz1 9067 |
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...𝑁)) |
|
Theorem | ige3m2fz 9068 |
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...𝑁)) |
|
Theorem | fzsplit2 9069 |
Split a finite interval of integers into two parts. (Contributed by
Mario Carneiro, 13-Apr-2016.)
|
⊢ (((𝐾 + 1) ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝑀...𝑁) = ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁))) |
|
Theorem | fzsplit 9070 |
Split a finite interval of integers into two parts. (Contributed by
Jeff Madsen, 17-Jun-2010.) (Revised by Mario Carneiro, 13-Apr-2016.)
|
⊢ (𝐾 ∈ (𝑀...𝑁) → (𝑀...𝑁) = ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁))) |
|
Theorem | fzdisj 9071 |
Condition for two finite intervals of integers to be disjoint.
(Contributed by Jeff Madsen, 17-Jun-2010.)
|
⊢ (𝐾 < 𝑀 → ((𝐽...𝐾) ∩ (𝑀...𝑁)) = ∅) |
|
Theorem | fz01en 9072 |
0-based and 1-based finite sets of sequential integers are equinumerous.
(Contributed by Paul Chapman, 11-Apr-2009.)
|
⊢ (𝑁 ∈ ℤ → (0...(𝑁 − 1)) ≈ (1...𝑁)) |
|
Theorem | elfznn 9073 |
A member of a finite set of sequential integers starting at 1 is a
positive integer. (Contributed by NM, 24-Aug-2005.)
|
⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ) |
|
Theorem | elfz1end 9074 |
A nonempty finite range of integers contains its end point. (Contributed
by Stefan O'Rear, 10-Oct-2014.)
|
⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ (1...𝐴)) |
|
Theorem | fznn0sub 9075 |
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) |
|
Theorem | fzmmmeqm 9076 |
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.)
|
⊢ (𝑀 ∈ (𝐿...𝑁) → ((𝑁 − 𝐿) − (𝑀 − 𝐿)) = (𝑁 − 𝑀)) |
|
Theorem | fzaddel 9077 |
Membership of a sum in a finite set of sequential integers. (Contributed
by NM, 30-Jul-2005.)
|
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))) |
|
Theorem | fzsubel 9078 |
Membership of a difference in a finite set of sequential integers.
(Contributed by NM, 30-Jul-2005.)
|
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 − 𝐾) ∈ ((𝑀 − 𝐾)...(𝑁 − 𝐾)))) |
|
Theorem | fzopth 9079 |
A finite set of sequential integers can represent an ordered pair.
(Contributed by NM, 31-Oct-2005.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑀...𝑁) = (𝐽...𝐾) ↔ (𝑀 = 𝐽 ∧ 𝑁 = 𝐾))) |
|
Theorem | fzass4 9080 |
Two ways to express a nondecreasing sequence of four integers.
(Contributed by Stefan O'Rear, 15-Aug-2015.)
|
⊢ ((𝐵 ∈ (𝐴...𝐷) ∧ 𝐶 ∈ (𝐵...𝐷)) ↔ (𝐵 ∈ (𝐴...𝐶) ∧ 𝐶 ∈ (𝐴...𝐷))) |
|
Theorem | fzss1 9081 |
Subset relationship for finite sets of sequential integers.
(Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro,
28-Apr-2015.)
|
⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁)) |
|
Theorem | fzss2 9082 |
Subset relationship for finite sets of sequential integers.
(Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro,
30-Apr-2015.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁)) |
|
Theorem | fzssuz 9083 |
A finite set of sequential integers is a subset of an upper set of
integers. (Contributed by NM, 28-Oct-2005.)
|
⊢ (𝑀...𝑁) ⊆
(ℤ≥‘𝑀) |
|
Theorem | fzsn 9084 |
A finite interval of integers with one element. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) |
|
Theorem | fzssp1 9085 |
Subset relationship for finite sets of sequential integers.
(Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1)) |
|
Theorem | fzsuc 9086 |
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)})) |
|
Theorem | fzpred 9087 |
Join a predecessor to the beginning of a finite set of sequential
integers. (Contributed by AV, 24-Aug-2019.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁))) |
|
Theorem | fzpreddisj 9088 |
A finite set of sequential integers is disjoint with its predecessor.
(Contributed by AV, 24-Aug-2019.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ({𝑀} ∩ ((𝑀 + 1)...𝑁)) = ∅) |
|
Theorem | elfzp1 9089 |
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)))) |
|
Theorem | fzp1ss 9090 |
Subset relationship for finite sets of sequential integers. (Contributed
by NM, 26-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|
⊢ (𝑀 ∈ ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
|
Theorem | fzelp1 9091 |
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))) |
|
Theorem | fzp1elp1 9092 |
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))) |
|
Theorem | fznatpl1 9093 |
Shift membership in a finite sequence of naturals. (Contributed by Scott
Fenton, 17-Jul-2013.)
|
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → (𝐼 + 1) ∈ (1...𝑁)) |
|
Theorem | fzpr 9094 |
A finite interval of integers with two elements. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)}) |
|
Theorem | fztp 9095 |
A finite interval of integers with three elements. (Contributed by NM,
13-Sep-2011.) (Revised by Mario Carneiro, 7-Mar-2014.)
|
⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 2)) = {𝑀, (𝑀 + 1), (𝑀 + 2)}) |
|
Theorem | fzsuc2 9096 |
Join a successor to the end of a finite set of sequential integers.
(Contributed by Mario Carneiro, 7-Mar-2014.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 − 1))) → (𝑀...(𝑁 + 1)) = ((𝑀...𝑁) ∪ {(𝑁 + 1)})) |
|
Theorem | fzp1disj 9097 |
(𝑀...(𝑁 + 1)) is the disjoint union of (𝑀...𝑁) with
{(𝑁 +
1)}. (Contributed by Mario Carneiro, 7-Mar-2014.)
|
⊢ ((𝑀...𝑁) ∩ {(𝑁 + 1)}) = ∅ |
|
Theorem | fzdifsuc 9098 |
Remove a successor from the end of a finite set of sequential integers.
(Contributed by AV, 4-Sep-2019.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) |
|
Theorem | fzprval 9099* |
Two ways of defining the first two values of a sequence on ℕ.
(Contributed by NM, 5-Sep-2011.)
|
⊢ (∀𝑥 ∈ (1...2)(𝐹‘𝑥) = if(𝑥 = 1, 𝐴, 𝐵) ↔ ((𝐹‘1) = 𝐴 ∧ (𝐹‘2) = 𝐵)) |
|
Theorem | fztpval 9100* |
Two ways of defining the first three values of a sequence on ℕ.
(Contributed by NM, 13-Sep-2011.)
|
⊢ (∀𝑥 ∈ (1...3)(𝐹‘𝑥) = if(𝑥 = 1, 𝐴, if(𝑥 = 2, 𝐵, 𝐶)) ↔ ((𝐹‘1) = 𝐴 ∧ (𝐹‘2) = 𝐵 ∧ (𝐹‘3) = 𝐶)) |