Theorem List for Intuitionistic Logic Explorer - 10101-10200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | elfzoel1 10101 |
Reverse closure for half-open integer sets. (Contributed by Stefan
O'Rear, 14-Aug-2015.)
|
⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ) |
|
Theorem | elfzoel2 10102 |
Reverse closure for half-open integer sets. (Contributed by Stefan
O'Rear, 14-Aug-2015.)
|
⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ) |
|
Theorem | elfzoelz 10103 |
Reverse closure for half-open integer sets. (Contributed by Stefan
O'Rear, 14-Aug-2015.)
|
⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ) |
|
Theorem | fzoval 10104 |
Value of the half-open integer set in terms of the closed integer set.
(Contributed by Stefan O'Rear, 14-Aug-2015.)
|
⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
|
Theorem | elfzo 10105 |
Membership in a half-open finite set of integers. (Contributed by Stefan
O'Rear, 15-Aug-2015.)
|
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀..^𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁))) |
|
Theorem | elfzo2 10106 |
Membership in a half-open integer interval. (Contributed by Mario
Carneiro, 29-Sep-2015.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁)) |
|
Theorem | elfzouz 10107 |
Membership in a half-open integer interval. (Contributed by Mario
Carneiro, 29-Sep-2015.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (ℤ≥‘𝑀)) |
|
Theorem | fzodcel 10108 |
Decidability of membership in a half-open integer interval. (Contributed
by Jim Kingdon, 25-Aug-2022.)
|
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
DECID 𝐾
∈ (𝑀..^𝑁)) |
|
Theorem | fzolb 10109 |
The left endpoint of a half-open integer interval is in the set iff the
two arguments are integers with 𝑀 < 𝑁. This provides an alternate
notation for the "strict upper integer" predicate by analogy to
the "weak
upper integer" predicate 𝑀 ∈ (ℤ≥‘𝑁). (Contributed by Mario
Carneiro, 29-Sep-2015.)
|
⊢ (𝑀 ∈ (𝑀..^𝑁) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁)) |
|
Theorem | fzolb2 10110 |
The left endpoint of a half-open integer interval is in the set iff the
two arguments are integers with 𝑀 < 𝑁. This provides an alternate
notation for the "strict upper integer" predicate by analogy to
the "weak
upper integer" predicate 𝑀 ∈ (ℤ≥‘𝑁). (Contributed by Mario
Carneiro, 29-Sep-2015.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (𝑀..^𝑁) ↔ 𝑀 < 𝑁)) |
|
Theorem | elfzole1 10111 |
A member in a half-open integer interval is greater than or equal to the
lower bound. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝐾) |
|
Theorem | elfzolt2 10112 |
A member in a half-open integer interval is less than the upper bound.
(Contributed by Stefan O'Rear, 15-Aug-2015.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 < 𝑁) |
|
Theorem | elfzolt3 10113 |
Membership in a half-open integer interval implies that the bounds are
unequal. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑀 < 𝑁) |
|
Theorem | elfzolt2b 10114 |
A member in a half-open integer interval is less than the upper bound.
(Contributed by Mario Carneiro, 29-Sep-2015.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (𝐾..^𝑁)) |
|
Theorem | elfzolt3b 10115 |
Membership in a half-open integer interval implies that the bounds are
unequal. (Contributed by Mario Carneiro, 29-Sep-2015.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑀 ∈ (𝑀..^𝑁)) |
|
Theorem | fzonel 10116 |
A half-open range does not contain its right endpoint. (Contributed by
Stefan O'Rear, 25-Aug-2015.)
|
⊢ ¬ 𝐵 ∈ (𝐴..^𝐵) |
|
Theorem | elfzouz2 10117 |
The upper bound of a half-open range is greater or equal to an element of
the range. (Contributed by Mario Carneiro, 29-Sep-2015.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) |
|
Theorem | elfzofz 10118 |
A half-open range is contained in the corresponding closed range.
(Contributed by Stefan O'Rear, 23-Aug-2015.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (𝑀...𝑁)) |
|
Theorem | elfzo3 10119 |
Express membership in a half-open integer interval in terms of the "less
than or equal" and "less than" predicates on integers,
resp.
𝐾
∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝐾, 𝐾 ∈ (𝐾..^𝑁) ↔ 𝐾 < 𝑁.
(Contributed by Mario Carneiro, 29-Sep-2015.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ (𝐾..^𝑁))) |
|
Theorem | fzom 10120* |
A half-open integer interval is inhabited iff it contains its left
endpoint. (Contributed by Jim Kingdon, 20-Apr-2020.)
|
⊢ (∃𝑥 𝑥 ∈ (𝑀..^𝑁) ↔ 𝑀 ∈ (𝑀..^𝑁)) |
|
Theorem | fzossfz 10121 |
A half-open range is contained in the corresponding closed range.
(Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario
Carneiro, 29-Sep-2015.)
|
⊢ (𝐴..^𝐵) ⊆ (𝐴...𝐵) |
|
Theorem | fzon 10122 |
A half-open set of sequential integers is empty if the bounds are equal or
reversed. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅)) |
|
Theorem | fzonlt0 10123 |
A half-open integer range is empty if the bounds are equal or reversed.
(Contributed by AV, 20-Oct-2018.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ 𝑀 < 𝑁 ↔ (𝑀..^𝑁) = ∅)) |
|
Theorem | fzo0 10124 |
Half-open sets with equal endpoints are empty. (Contributed by Stefan
O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.)
|
⊢ (𝐴..^𝐴) = ∅ |
|
Theorem | fzonnsub 10125 |
If 𝐾 <
𝑁 then 𝑁 − 𝐾 is a positive integer.
(Contributed by Mario
Carneiro, 29-Sep-2015.) (Revised by Mario Carneiro, 1-Jan-2017.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝑁 − 𝐾) ∈ ℕ) |
|
Theorem | fzonnsub2 10126 |
If 𝑀 <
𝑁 then 𝑁 − 𝑀 is a positive integer.
(Contributed by Mario
Carneiro, 1-Jan-2017.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝑁 − 𝑀) ∈ ℕ) |
|
Theorem | fzoss1 10127 |
Subset relationship for half-open sequences of integers. (Contributed
by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro,
29-Sep-2015.)
|
⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝐾..^𝑁) ⊆ (𝑀..^𝑁)) |
|
Theorem | fzoss2 10128 |
Subset relationship for half-open sequences of integers. (Contributed by
Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀..^𝐾) ⊆ (𝑀..^𝑁)) |
|
Theorem | fzossrbm1 10129 |
Subset of a half open range. (Contributed by Alexander van der Vekens,
1-Nov-2017.)
|
⊢ (𝑁 ∈ ℤ → (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) |
|
Theorem | fzo0ss1 10130 |
Subset relationship for half-open integer ranges with lower bounds 0 and
1. (Contributed by Alexander van der Vekens, 18-Mar-2018.)
|
⊢ (1..^𝑁) ⊆ (0..^𝑁) |
|
Theorem | fzossnn0 10131 |
A half-open integer range starting at a nonnegative integer is a subset of
the nonnegative integers. (Contributed by Alexander van der Vekens,
13-May-2018.)
|
⊢ (𝑀 ∈ ℕ0 → (𝑀..^𝑁) ⊆
ℕ0) |
|
Theorem | fzospliti 10132 |
One direction of splitting a half-open integer range in half.
(Contributed by Stefan O'Rear, 14-Aug-2015.)
|
⊢ ((𝐴 ∈ (𝐵..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 ∈ (𝐵..^𝐷) ∨ 𝐴 ∈ (𝐷..^𝐶))) |
|
Theorem | fzosplit 10133 |
Split a half-open integer range in half. (Contributed by Stefan O'Rear,
14-Aug-2015.)
|
⊢ (𝐷 ∈ (𝐵...𝐶) → (𝐵..^𝐶) = ((𝐵..^𝐷) ∪ (𝐷..^𝐶))) |
|
Theorem | fzodisj 10134 |
Abutting half-open integer ranges are disjoint. (Contributed by Stefan
O'Rear, 14-Aug-2015.)
|
⊢ ((𝐴..^𝐵) ∩ (𝐵..^𝐶)) = ∅ |
|
Theorem | fzouzsplit 10135 |
Split an upper integer set into a half-open integer range and another
upper integer set. (Contributed by Mario Carneiro, 21-Sep-2016.)
|
⊢ (𝐵 ∈ (ℤ≥‘𝐴) →
(ℤ≥‘𝐴) = ((𝐴..^𝐵) ∪ (ℤ≥‘𝐵))) |
|
Theorem | fzouzdisj 10136 |
A half-open integer range does not overlap the upper integer range
starting at the endpoint of the first range. (Contributed by Mario
Carneiro, 21-Sep-2016.)
|
⊢ ((𝐴..^𝐵) ∩ (ℤ≥‘𝐵)) = ∅ |
|
Theorem | lbfzo0 10137 |
An integer is strictly greater than zero iff it is a member of ℕ.
(Contributed by Mario Carneiro, 29-Sep-2015.)
|
⊢ (0 ∈ (0..^𝐴) ↔ 𝐴 ∈ ℕ) |
|
Theorem | elfzo0 10138 |
Membership in a half-open integer range based at 0. (Contributed by
Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.)
|
⊢ (𝐴 ∈ (0..^𝐵) ↔ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵)) |
|
Theorem | fzo1fzo0n0 10139 |
An integer between 1 and an upper bound of a half-open integer range is
not 0 and between 0 and the upper bound of the half-open integer range.
(Contributed by Alexander van der Vekens, 21-Mar-2018.)
|
⊢ (𝐾 ∈ (1..^𝑁) ↔ (𝐾 ∈ (0..^𝑁) ∧ 𝐾 ≠ 0)) |
|
Theorem | elfzo0z 10140 |
Membership in a half-open range of nonnegative integers, generalization of
elfzo0 10138 requiring the upper bound to be an integer
only. (Contributed by
Alexander van der Vekens, 23-Sep-2018.)
|
⊢ (𝐴 ∈ (0..^𝐵) ↔ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵)) |
|
Theorem | elfzo0le 10141 |
A member in a half-open range of nonnegative integers is less than or
equal to the upper bound of the range. (Contributed by Alexander van der
Vekens, 23-Sep-2018.)
|
⊢ (𝐴 ∈ (0..^𝐵) → 𝐴 ≤ 𝐵) |
|
Theorem | elfzonn0 10142 |
A member of a half-open range of nonnegative integers is a nonnegative
integer. (Contributed by Alexander van der Vekens, 21-May-2018.)
|
⊢ (𝐾 ∈ (0..^𝑁) → 𝐾 ∈
ℕ0) |
|
Theorem | fzonmapblen 10143 |
The result of subtracting a nonnegative integer from a positive integer
and adding another nonnegative integer which is less than the first one is
less then the positive integer. (Contributed by Alexander van der Vekens,
19-May-2018.)
|
⊢ ((𝐴 ∈ (0..^𝑁) ∧ 𝐵 ∈ (0..^𝑁) ∧ 𝐵 < 𝐴) → (𝐵 + (𝑁 − 𝐴)) < 𝑁) |
|
Theorem | fzofzim 10144 |
If a nonnegative integer in a finite interval of integers is not the upper
bound of the interval, it is contained in the corresponding half-open
integer range. (Contributed by Alexander van der Vekens, 15-Jun-2018.)
|
⊢ ((𝐾 ≠ 𝑀 ∧ 𝐾 ∈ (0...𝑀)) → 𝐾 ∈ (0..^𝑀)) |
|
Theorem | fzossnn 10145 |
Half-open integer ranges starting with 1 are subsets of ℕ.
(Contributed by Thierry Arnoux, 28-Dec-2016.)
|
⊢ (1..^𝑁) ⊆ ℕ |
|
Theorem | elfzo1 10146 |
Membership in a half-open integer range based at 1. (Contributed by
Thierry Arnoux, 14-Feb-2017.)
|
⊢ (𝑁 ∈ (1..^𝑀) ↔ (𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 < 𝑀)) |
|
Theorem | fzo0m 10147* |
A half-open integer range based at 0 is inhabited precisely if the upper
bound is a positive integer. (Contributed by Jim Kingdon,
20-Apr-2020.)
|
⊢ (∃𝑥 𝑥 ∈ (0..^𝐴) ↔ 𝐴 ∈ ℕ) |
|
Theorem | fzoaddel 10148 |
Translate membership in a half-open integer range. (Contributed by Stefan
O'Rear, 15-Aug-2015.)
|
⊢ ((𝐴 ∈ (𝐵..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 + 𝐷) ∈ ((𝐵 + 𝐷)..^(𝐶 + 𝐷))) |
|
Theorem | fzoaddel2 10149 |
Translate membership in a shifted-down half-open integer range.
(Contributed by Stefan O'Rear, 15-Aug-2015.)
|
⊢ ((𝐴 ∈ (0..^(𝐵 − 𝐶)) ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 + 𝐶) ∈ (𝐶..^𝐵)) |
|
Theorem | fzosubel 10150 |
Translate membership in a half-open integer range. (Contributed by Stefan
O'Rear, 15-Aug-2015.)
|
⊢ ((𝐴 ∈ (𝐵..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 − 𝐷) ∈ ((𝐵 − 𝐷)..^(𝐶 − 𝐷))) |
|
Theorem | fzosubel2 10151 |
Membership in a translated half-open integer range implies translated
membership in the original range. (Contributed by Stefan O'Rear,
15-Aug-2015.)
|
⊢ ((𝐴 ∈ ((𝐵 + 𝐶)..^(𝐵 + 𝐷)) ∧ (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → (𝐴 − 𝐵) ∈ (𝐶..^𝐷)) |
|
Theorem | fzosubel3 10152 |
Membership in a translated half-open integer range when the original range
is zero-based. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|
⊢ ((𝐴 ∈ (𝐵..^(𝐵 + 𝐷)) ∧ 𝐷 ∈ ℤ) → (𝐴 − 𝐵) ∈ (0..^𝐷)) |
|
Theorem | eluzgtdifelfzo 10153 |
Membership of the difference of integers in a half-open range of
nonnegative integers. (Contributed by Alexander van der Vekens,
17-Sep-2018.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑁 ∈ (ℤ≥‘𝐴) ∧ 𝐵 < 𝐴) → (𝑁 − 𝐴) ∈ (0..^(𝑁 − 𝐵)))) |
|
Theorem | ige2m2fzo 10154 |
Membership of an integer greater than 1 decreased by 2 in a half-open
range of nonnegative integers. (Contributed by Alexander van der Vekens,
3-Oct-2018.)
|
⊢ (𝑁 ∈ (ℤ≥‘2)
→ (𝑁 − 2)
∈ (0..^(𝑁 −
1))) |
|
Theorem | fzocatel 10155 |
Translate membership in a half-open integer range. (Contributed by
Thierry Arnoux, 28-Sep-2018.)
|
⊢ (((𝐴 ∈ (0..^(𝐵 + 𝐶)) ∧ ¬ 𝐴 ∈ (0..^𝐵)) ∧ (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ)) → (𝐴 − 𝐵) ∈ (0..^𝐶)) |
|
Theorem | ubmelfzo 10156 |
If an integer in a 1 based finite set of sequential integers is subtracted
from the upper bound of this finite set of sequential integers, the result
is contained in a half-open range of nonnegative integers with the same
upper bound. (Contributed by AV, 18-Mar-2018.) (Revised by AV,
30-Oct-2018.)
|
⊢ (𝐾 ∈ (1...𝑁) → (𝑁 − 𝐾) ∈ (0..^𝑁)) |
|
Theorem | elfzodifsumelfzo 10157 |
If an integer is in a half-open range of nonnegative integers with a
difference as upper bound, the sum of the integer with the subtrahend of
the difference is in the a half-open range of nonnegative integers
containing the minuend of the difference. (Contributed by AV,
13-Nov-2018.)
|
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...𝑃)) → (𝐼 ∈ (0..^(𝑁 − 𝑀)) → (𝐼 + 𝑀) ∈ (0..^𝑃))) |
|
Theorem | elfzom1elp1fzo 10158 |
Membership of an integer incremented by one in a half-open range of
nonnegative integers. (Contributed by Alexander van der Vekens,
24-Jun-2018.) (Proof shortened by AV, 5-Jan-2020.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(𝑁 − 1))) → (𝐼 + 1) ∈ (0..^𝑁)) |
|
Theorem | elfzom1elfzo 10159 |
Membership in a half-open range of nonnegative integers. (Contributed by
Alexander van der Vekens, 18-Jun-2018.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(𝑁 − 1))) → 𝐼 ∈ (0..^𝑁)) |
|
Theorem | fzval3 10160 |
Expressing a closed integer range as a half-open integer range.
(Contributed by Stefan O'Rear, 15-Aug-2015.)
|
⊢ (𝑁 ∈ ℤ → (𝑀...𝑁) = (𝑀..^(𝑁 + 1))) |
|
Theorem | fzosn 10161 |
Expressing a singleton as a half-open range. (Contributed by Stefan
O'Rear, 23-Aug-2015.)
|
⊢ (𝐴 ∈ ℤ → (𝐴..^(𝐴 + 1)) = {𝐴}) |
|
Theorem | elfzomin 10162 |
Membership of an integer in the smallest open range of integers.
(Contributed by Alexander van der Vekens, 22-Sep-2018.)
|
⊢ (𝑍 ∈ ℤ → 𝑍 ∈ (𝑍..^(𝑍 + 1))) |
|
Theorem | zpnn0elfzo 10163 |
Membership of an integer increased by a nonnegative integer in a half-
open integer range. (Contributed by Alexander van der Vekens,
22-Sep-2018.)
|
⊢ ((𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝑍 + 𝑁) ∈ (𝑍..^((𝑍 + 𝑁) + 1))) |
|
Theorem | zpnn0elfzo1 10164 |
Membership of an integer increased by a nonnegative integer in a half-
open integer range. (Contributed by Alexander van der Vekens,
22-Sep-2018.)
|
⊢ ((𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝑍 + 𝑁) ∈ (𝑍..^(𝑍 + (𝑁 + 1)))) |
|
Theorem | fzosplitsnm1 10165 |
Removing a singleton from a half-open integer range at the end.
(Contributed by Alexander van der Vekens, 23-Mar-2018.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈
(ℤ≥‘(𝐴 + 1))) → (𝐴..^𝐵) = ((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1)})) |
|
Theorem | elfzonlteqm1 10166 |
If an element of a half-open integer range is not less than the upper
bound of the range decreased by 1, it must be equal to the upper bound of
the range decreased by 1. (Contributed by AV, 3-Nov-2018.)
|
⊢ ((𝐴 ∈ (0..^𝐵) ∧ ¬ 𝐴 < (𝐵 − 1)) → 𝐴 = (𝐵 − 1)) |
|
Theorem | fzonn0p1 10167 |
A nonnegative integer is element of the half-open range of nonnegative
integers with the element increased by one as an upper bound.
(Contributed by Alexander van der Vekens, 5-Aug-2018.)
|
⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ (0..^(𝑁 + 1))) |
|
Theorem | fzossfzop1 10168 |
A half-open range of nonnegative integers is a subset of a half-open range
of nonnegative integers with the upper bound increased by one.
(Contributed by Alexander van der Vekens, 5-Aug-2018.)
|
⊢ (𝑁 ∈ ℕ0 →
(0..^𝑁) ⊆
(0..^(𝑁 +
1))) |
|
Theorem | fzonn0p1p1 10169 |
If a nonnegative integer is element of a half-open range of nonnegative
integers, increasing this integer by one results in an element of a half-
open range of nonnegative integers with the upper bound increased by one.
(Contributed by Alexander van der Vekens, 5-Aug-2018.)
|
⊢ (𝐼 ∈ (0..^𝑁) → (𝐼 + 1) ∈ (0..^(𝑁 + 1))) |
|
Theorem | elfzom1p1elfzo 10170 |
Increasing an element of a half-open range of nonnegative integers by 1
results in an element of the half-open range of nonnegative integers with
an upper bound increased by 1. (Contributed by Alexander van der Vekens,
1-Aug-2018.)
|
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ (0..^(𝑁 − 1))) → (𝑋 + 1) ∈ (0..^𝑁)) |
|
Theorem | fzo0ssnn0 10171 |
Half-open integer ranges starting with 0 are subsets of NN0.
(Contributed by Thierry Arnoux, 8-Oct-2018.)
|
⊢ (0..^𝑁) ⊆
ℕ0 |
|
Theorem | fzo01 10172 |
Expressing the singleton of 0 as a half-open integer
range.
(Contributed by Stefan O'Rear, 15-Aug-2015.)
|
⊢ (0..^1) = {0} |
|
Theorem | fzo12sn 10173 |
A 1-based half-open integer interval up to, but not including, 2 is a
singleton. (Contributed by Alexander van der Vekens, 31-Jan-2018.)
|
⊢ (1..^2) = {1} |
|
Theorem | fzo0to2pr 10174 |
A half-open integer range from 0 to 2 is an unordered pair. (Contributed
by Alexander van der Vekens, 4-Dec-2017.)
|
⊢ (0..^2) = {0, 1} |
|
Theorem | fzo0to3tp 10175 |
A half-open integer range from 0 to 3 is an unordered triple.
(Contributed by Alexander van der Vekens, 9-Nov-2017.)
|
⊢ (0..^3) = {0, 1, 2} |
|
Theorem | fzo0to42pr 10176 |
A half-open integer range from 0 to 4 is a union of two unordered pairs.
(Contributed by Alexander van der Vekens, 17-Nov-2017.)
|
⊢ (0..^4) = ({0, 1} ∪ {2,
3}) |
|
Theorem | fzo0sn0fzo1 10177 |
A half-open range of nonnegative integers is the union of the singleton
set containing 0 and a half-open range of positive integers. (Contributed
by Alexander van der Vekens, 18-May-2018.)
|
⊢ (𝑁 ∈ ℕ → (0..^𝑁) = ({0} ∪ (1..^𝑁))) |
|
Theorem | fzoend 10178 |
The endpoint of a half-open integer range. (Contributed by Mario
Carneiro, 29-Sep-2015.)
|
⊢ (𝐴 ∈ (𝐴..^𝐵) → (𝐵 − 1) ∈ (𝐴..^𝐵)) |
|
Theorem | fzo0end 10179 |
The endpoint of a zero-based half-open range. (Contributed by Stefan
O'Rear, 27-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.)
|
⊢ (𝐵 ∈ ℕ → (𝐵 − 1) ∈ (0..^𝐵)) |
|
Theorem | ssfzo12 10180 |
Subset relationship for half-open integer ranges. (Contributed by
Alexander van der Vekens, 16-Mar-2018.)
|
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) |
|
Theorem | ssfzo12bi 10181 |
Subset relationship for half-open integer ranges. (Contributed by
Alexander van der Vekens, 5-Nov-2018.)
|
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) |
|
Theorem | ubmelm1fzo 10182 |
The result of subtracting 1 and an integer of a half-open range of
nonnegative integers from the upper bound of this range is contained in
this range. (Contributed by AV, 23-Mar-2018.) (Revised by AV,
30-Oct-2018.)
|
⊢ (𝐾 ∈ (0..^𝑁) → ((𝑁 − 𝐾) − 1) ∈ (0..^𝑁)) |
|
Theorem | fzofzp1 10183 |
If a point is in a half-open range, the next point is in the closed range.
(Contributed by Stefan O'Rear, 23-Aug-2015.)
|
⊢ (𝐶 ∈ (𝐴..^𝐵) → (𝐶 + 1) ∈ (𝐴...𝐵)) |
|
Theorem | fzofzp1b 10184 |
If a point is in a half-open range, the next point is in the closed range.
(Contributed by Mario Carneiro, 27-Sep-2015.)
|
⊢ (𝐶 ∈ (ℤ≥‘𝐴) → (𝐶 ∈ (𝐴..^𝐵) ↔ (𝐶 + 1) ∈ (𝐴...𝐵))) |
|
Theorem | elfzom1b 10185 |
An integer is a member of a 1-based finite set of sequential integers iff
its predecessor is a member of the corresponding 0-based set.
(Contributed by Mario Carneiro, 27-Sep-2015.)
|
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (1..^𝑁) ↔ (𝐾 − 1) ∈ (0..^(𝑁 − 1)))) |
|
Theorem | elfzonelfzo 10186 |
If an element of a half-open integer range is not contained in the lower
subrange, it must be in the upper subrange. (Contributed by Alexander van
der Vekens, 30-Mar-2018.)
|
⊢ (𝑁 ∈ ℤ → ((𝐾 ∈ (𝑀..^𝑅) ∧ ¬ 𝐾 ∈ (𝑀..^𝑁)) → 𝐾 ∈ (𝑁..^𝑅))) |
|
Theorem | elfzomelpfzo 10187 |
An integer increased by another integer is an element of a half-open
integer range if and only if the integer is contained in the half-open
integer range with bounds decreased by the other integer. (Contributed by
Alexander van der Vekens, 30-Mar-2018.)
|
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝐾 ∈ ((𝑀 − 𝐿)..^(𝑁 − 𝐿)) ↔ (𝐾 + 𝐿) ∈ (𝑀..^𝑁))) |
|
Theorem | peano2fzor 10188 |
A Peano-postulate-like theorem for downward closure of a half-open integer
range. (Contributed by Mario Carneiro, 1-Oct-2015.)
|
⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ (𝐾 + 1) ∈ (𝑀..^𝑁)) → 𝐾 ∈ (𝑀..^𝑁)) |
|
Theorem | fzosplitsn 10189 |
Extending a half-open range by a singleton on the end. (Contributed by
Stefan O'Rear, 23-Aug-2015.)
|
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (𝐴..^(𝐵 + 1)) = ((𝐴..^𝐵) ∪ {𝐵})) |
|
Theorem | fzosplitprm1 10190 |
Extending a half-open integer range by an unordered pair at the end.
(Contributed by Alexander van der Vekens, 22-Sep-2018.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → (𝐴..^(𝐵 + 1)) = ((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1), 𝐵})) |
|
Theorem | fzosplitsni 10191 |
Membership in a half-open range extended by a singleton. (Contributed by
Stefan O'Rear, 23-Aug-2015.)
|
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (𝐶 ∈ (𝐴..^(𝐵 + 1)) ↔ (𝐶 ∈ (𝐴..^𝐵) ∨ 𝐶 = 𝐵))) |
|
Theorem | fzisfzounsn 10192 |
A finite interval of integers as union of a half-open integer range and a
singleton. (Contributed by Alexander van der Vekens, 15-Jun-2018.)
|
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (𝐴...𝐵) = ((𝐴..^𝐵) ∪ {𝐵})) |
|
Theorem | fzostep1 10193 |
Two possibilities for a number one greater than a number in a half-open
range. (Contributed by Stefan O'Rear, 23-Aug-2015.)
|
⊢ (𝐴 ∈ (𝐵..^𝐶) → ((𝐴 + 1) ∈ (𝐵..^𝐶) ∨ (𝐴 + 1) = 𝐶)) |
|
Theorem | fzoshftral 10194* |
Shift the scanning order inside of a quantification over a half-open
integer range, analogous to fzshftral 10064. (Contributed by Alexander van
der Vekens, 23-Sep-2018.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ (𝑀..^𝑁)𝜑 ↔ ∀𝑘 ∈ ((𝑀 + 𝐾)..^(𝑁 + 𝐾))[(𝑘 − 𝐾) / 𝑗]𝜑)) |
|
Theorem | fzind2 10195* |
Induction on the integers from 𝑀 to 𝑁 inclusive. The first
four
hypotheses give us the substitution instances we need; the last two are
the basis and the induction step. Version of fzind 9327 using integer
range definitions. (Contributed by Mario Carneiro, 6-Feb-2016.)
|
⊢ (𝑥 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐾 → (𝜑 ↔ 𝜏)) & ⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝜓)
& ⊢ (𝑦 ∈ (𝑀..^𝑁) → (𝜒 → 𝜃)) ⇒ ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝜏) |
|
Theorem | exfzdc 10196* |
Decidability of the existence of an integer defined by a decidable
proposition. (Contributed by Jim Kingdon, 28-Jan-2022.)
|
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → DECID 𝜓) ⇒ ⊢ (𝜑 → DECID ∃𝑛 ∈ (𝑀...𝑁)𝜓) |
|
Theorem | fvinim0ffz 10197 |
The function values for the borders of a finite interval of integers,
which is the domain of the function, are not in the image of the
interior of the interval iff the intersection of the images of the
interior and the borders is empty. (Contributed by Alexander van der
Vekens, 31-Oct-2017.) (Revised by AV, 5-Feb-2021.)
|
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) →
(((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ ↔ ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹‘𝐾) ∉ (𝐹 “ (1..^𝐾))))) |
|
Theorem | subfzo0 10198 |
The difference between two elements in a half-open range of nonnegative
integers is greater than the negation of the upper bound and less than the
upper bound of the range. (Contributed by AV, 20-Mar-2021.)
|
⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁)) |
|
4.5.7 Rational numbers (cont.)
|
|
Theorem | qtri3or 10199 |
Rational trichotomy. (Contributed by Jim Kingdon, 6-Oct-2021.)
|
⊢ ((𝑀 ∈ ℚ ∧ 𝑁 ∈ ℚ) → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀)) |
|
Theorem | qletric 10200 |
Rational trichotomy. (Contributed by Jim Kingdon, 6-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴)) |