Theorem List for Intuitionistic Logic Explorer - 9101-9200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 11multnc 9101 |
The product of 11 (as numeral) with a number (no carry). (Contributed
by AV, 15-Jun-2021.)
|
⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ (𝑁 · ;11) = ;𝑁𝑁 |
|
Theorem | decmul10add 9102 |
A multiplication of a number and a numeral expressed as addition with
first summand as multiple of 10. (Contributed by AV, 22-Jul-2021.)
(Revised by AV, 6-Sep-2021.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝑀 ∈ ℕ0 & ⊢ 𝐸 = (𝑀 · 𝐴)
& ⊢ 𝐹 = (𝑀 · 𝐵) ⇒ ⊢ (𝑀 · ;𝐴𝐵) = (;𝐸0 + 𝐹) |
|
Theorem | 6p5lem 9103 |
Lemma for 6p5e11 9106 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐷 ∈
ℕ0
& ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐵 = (𝐷 + 1) & ⊢ 𝐶 = (𝐸 + 1) & ⊢ (𝐴 + 𝐷) = ;1𝐸 ⇒ ⊢ (𝐴 + 𝐵) = ;1𝐶 |
|
Theorem | 5p5e10 9104 |
5 + 5 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
⊢ (5 + 5) = ;10 |
|
Theorem | 6p4e10 9105 |
6 + 4 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
⊢ (6 + 4) = ;10 |
|
Theorem | 6p5e11 9106 |
6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (6 + 5) = ;11 |
|
Theorem | 6p6e12 9107 |
6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 + 6) = ;12 |
|
Theorem | 7p3e10 9108 |
7 + 3 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
⊢ (7 + 3) = ;10 |
|
Theorem | 7p4e11 9109 |
7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (7 + 4) = ;11 |
|
Theorem | 7p5e12 9110 |
7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 + 5) = ;12 |
|
Theorem | 7p6e13 9111 |
7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 + 6) = ;13 |
|
Theorem | 7p7e14 9112 |
7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 + 7) = ;14 |
|
Theorem | 8p2e10 9113 |
8 + 2 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
⊢ (8 + 2) = ;10 |
|
Theorem | 8p3e11 9114 |
8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (8 + 3) = ;11 |
|
Theorem | 8p4e12 9115 |
8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 4) = ;12 |
|
Theorem | 8p5e13 9116 |
8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 5) = ;13 |
|
Theorem | 8p6e14 9117 |
8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 6) = ;14 |
|
Theorem | 8p7e15 9118 |
8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 7) = ;15 |
|
Theorem | 8p8e16 9119 |
8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 8) = ;16 |
|
Theorem | 9p2e11 9120 |
9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (9 + 2) = ;11 |
|
Theorem | 9p3e12 9121 |
9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 3) = ;12 |
|
Theorem | 9p4e13 9122 |
9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 4) = ;13 |
|
Theorem | 9p5e14 9123 |
9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 5) = ;14 |
|
Theorem | 9p6e15 9124 |
9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 6) = ;15 |
|
Theorem | 9p7e16 9125 |
9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 7) = ;16 |
|
Theorem | 9p8e17 9126 |
9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 8) = ;17 |
|
Theorem | 9p9e18 9127 |
9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 9) = ;18 |
|
Theorem | 10p10e20 9128 |
10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (;10 + ;10) = ;20 |
|
Theorem | 10m1e9 9129 |
10 - 1 = 9. (Contributed by AV, 6-Sep-2021.)
|
⊢ (;10 − 1) = 9 |
|
Theorem | 4t3lem 9130 |
Lemma for 4t3e12 9131 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝐶 = (𝐵 + 1) & ⊢ (𝐴 · 𝐵) = 𝐷
& ⊢ (𝐷 + 𝐴) = 𝐸 ⇒ ⊢ (𝐴 · 𝐶) = 𝐸 |
|
Theorem | 4t3e12 9131 |
4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (4 · 3) = ;12 |
|
Theorem | 4t4e16 9132 |
4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (4 · 4) = ;16 |
|
Theorem | 5t2e10 9133 |
5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV,
4-Sep-2021.)
|
⊢ (5 · 2) = ;10 |
|
Theorem | 5t3e15 9134 |
5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 3) = ;15 |
|
Theorem | 5t4e20 9135 |
5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 4) = ;20 |
|
Theorem | 5t5e25 9136 |
5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 5) = ;25 |
|
Theorem | 6t2e12 9137 |
6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 2) = ;12 |
|
Theorem | 6t3e18 9138 |
6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 3) = ;18 |
|
Theorem | 6t4e24 9139 |
6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 4) = ;24 |
|
Theorem | 6t5e30 9140 |
6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (6 · 5) = ;30 |
|
Theorem | 6t6e36 9141 |
6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (6 · 6) = ;36 |
|
Theorem | 7t2e14 9142 |
7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 2) = ;14 |
|
Theorem | 7t3e21 9143 |
7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 3) = ;21 |
|
Theorem | 7t4e28 9144 |
7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 4) = ;28 |
|
Theorem | 7t5e35 9145 |
7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 5) = ;35 |
|
Theorem | 7t6e42 9146 |
7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 6) = ;42 |
|
Theorem | 7t7e49 9147 |
7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 7) = ;49 |
|
Theorem | 8t2e16 9148 |
8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 2) = ;16 |
|
Theorem | 8t3e24 9149 |
8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 3) = ;24 |
|
Theorem | 8t4e32 9150 |
8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 4) = ;32 |
|
Theorem | 8t5e40 9151 |
8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (8 · 5) = ;40 |
|
Theorem | 8t6e48 9152 |
8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (8 · 6) = ;48 |
|
Theorem | 8t7e56 9153 |
8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 7) = ;56 |
|
Theorem | 8t8e64 9154 |
8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 8) = ;64 |
|
Theorem | 9t2e18 9155 |
9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 2) = ;18 |
|
Theorem | 9t3e27 9156 |
9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 3) = ;27 |
|
Theorem | 9t4e36 9157 |
9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 4) = ;36 |
|
Theorem | 9t5e45 9158 |
9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 5) = ;45 |
|
Theorem | 9t6e54 9159 |
9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 6) = ;54 |
|
Theorem | 9t7e63 9160 |
9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 7) = ;63 |
|
Theorem | 9t8e72 9161 |
9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 8) = ;72 |
|
Theorem | 9t9e81 9162 |
9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 9) = ;81 |
|
Theorem | 9t11e99 9163 |
9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV,
6-Sep-2021.)
|
⊢ (9 · ;11) = ;99 |
|
Theorem | 9lt10 9164 |
9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
⊢ 9 < ;10 |
|
Theorem | 8lt10 9165 |
8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
⊢ 8 < ;10 |
|
Theorem | 7lt10 9166 |
7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 7 < ;10 |
|
Theorem | 6lt10 9167 |
6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 6 < ;10 |
|
Theorem | 5lt10 9168 |
5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 5 < ;10 |
|
Theorem | 4lt10 9169 |
4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 4 < ;10 |
|
Theorem | 3lt10 9170 |
3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 3 < ;10 |
|
Theorem | 2lt10 9171 |
2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 2 < ;10 |
|
Theorem | 1lt10 9172 |
1 is less than 10. (Contributed by NM, 7-Nov-2012.) (Revised by Mario
Carneiro, 9-Mar-2015.) (Revised by AV, 8-Sep-2021.)
|
⊢ 1 < ;10 |
|
Theorem | decbin0 9173 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝐴 ∈
ℕ0 ⇒ ⊢ (4 · 𝐴) = (2 · (2 · 𝐴)) |
|
Theorem | decbin2 9174 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝐴 ∈
ℕ0 ⇒ ⊢ ((4 · 𝐴) + 2) = (2 · ((2 · 𝐴) + 1)) |
|
Theorem | decbin3 9175 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝐴 ∈
ℕ0 ⇒ ⊢ ((4 · 𝐴) + 3) = ((2 · ((2 · 𝐴) + 1)) + 1) |
|
3.4.11 Upper sets of integers
|
|
Syntax | cuz 9176 |
Extend class notation with the upper integer function.
Read "ℤ≥‘𝑀 " as "the set of integers
greater than or equal to
𝑀."
|
class ℤ≥ |
|
Definition | df-uz 9177* |
Define a function whose value at 𝑗 is the semi-infinite set of
contiguous integers starting at 𝑗, which we will also call the
upper integers starting at 𝑗. Read "ℤ≥‘𝑀 " as "the set
of integers greater than or equal to 𝑀." See uzval 9178 for its
value, uzssz 9195 for its relationship to ℤ, nnuz 9211 and nn0uz 9210 for
its relationships to ℕ and ℕ0, and eluz1 9180 and eluz2 9182 for
its membership relations. (Contributed by NM, 5-Sep-2005.)
|
⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘}) |
|
Theorem | uzval 9178* |
The value of the upper integers function. (Contributed by NM,
5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ (𝑁 ∈ ℤ →
(ℤ≥‘𝑁) = {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘}) |
|
Theorem | uzf 9179 |
The domain and range of the upper integers function. (Contributed by
Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢
ℤ≥:ℤ⟶𝒫
ℤ |
|
Theorem | eluz1 9180 |
Membership in the upper set of integers starting at 𝑀.
(Contributed by NM, 5-Sep-2005.)
|
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) |
|
Theorem | eluzel2 9181 |
Implication of membership in an upper set of integers. (Contributed by
NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
|
Theorem | eluz2 9182 |
Membership in an upper set of integers. We use the fact that a
function's value (under our function value definition) is empty outside
of its domain to show 𝑀 ∈ ℤ. (Contributed by NM,
5-Sep-2005.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
|
Theorem | eluz1i 9183 |
Membership in an upper set of integers. (Contributed by NM,
5-Sep-2005.)
|
⊢ 𝑀 ∈ ℤ
⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
|
Theorem | eluzuzle 9184 |
An integer in an upper set of integers is an element of an upper set of
integers with a smaller bound. (Contributed by Alexander van der Vekens,
17-Jun-2018.)
|
⊢ ((𝐵 ∈ ℤ ∧ 𝐵 ≤ 𝐴) → (𝐶 ∈ (ℤ≥‘𝐴) → 𝐶 ∈ (ℤ≥‘𝐵))) |
|
Theorem | eluzelz 9185 |
A member of an upper set of integers is an integer. (Contributed by NM,
6-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
|
Theorem | eluzelre 9186 |
A member of an upper set of integers is a real. (Contributed by Mario
Carneiro, 31-Aug-2013.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ) |
|
Theorem | eluzelcn 9187 |
A member of an upper set of integers is a complex number. (Contributed by
Glauco Siliprandi, 29-Jun-2017.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ) |
|
Theorem | eluzle 9188 |
Implication of membership in an upper set of integers. (Contributed by
NM, 6-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
|
Theorem | eluz 9189 |
Membership in an upper set of integers. (Contributed by NM,
2-Oct-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) |
|
Theorem | uzid 9190 |
Membership of the least member in an upper set of integers. (Contributed
by NM, 2-Sep-2005.)
|
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀)) |
|
Theorem | uzn0 9191 |
The upper integers are all nonempty. (Contributed by Mario Carneiro,
16-Jan-2014.)
|
⊢ (𝑀 ∈ ran ℤ≥ →
𝑀 ≠
∅) |
|
Theorem | uztrn 9192 |
Transitive law for sets of upper integers. (Contributed by NM,
20-Sep-2005.)
|
⊢ ((𝑀 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝑁)) |
|
Theorem | uztrn2 9193 |
Transitive law for sets of upper integers. (Contributed by Mario
Carneiro, 26-Dec-2013.)
|
⊢ 𝑍 = (ℤ≥‘𝐾)
⇒ ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍) |
|
Theorem | uzneg 9194 |
Contraposition law for upper integers. (Contributed by NM,
28-Nov-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → -𝑀 ∈
(ℤ≥‘-𝑁)) |
|
Theorem | uzssz 9195 |
An upper set of integers is a subset of all integers. (Contributed by
NM, 2-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ (ℤ≥‘𝑀) ⊆
ℤ |
|
Theorem | uzss 9196 |
Subset relationship for two sets of upper integers. (Contributed by NM,
5-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
|
Theorem | uztric 9197 |
Trichotomy of the ordering relation on integers, stated in terms of upper
integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro,
25-Jun-2013.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ∨ 𝑀 ∈ (ℤ≥‘𝑁))) |
|
Theorem | uz11 9198 |
The upper integers function is one-to-one. (Contributed by NM,
12-Dec-2005.)
|
⊢ (𝑀 ∈ ℤ →
((ℤ≥‘𝑀) = (ℤ≥‘𝑁) ↔ 𝑀 = 𝑁)) |
|
Theorem | eluzp1m1 9199 |
Membership in the next upper set of integers. (Contributed by NM,
12-Sep-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
|
Theorem | eluzp1l 9200 |
Strict ordering implied by membership in the next upper set of integers.
(Contributed by NM, 12-Sep-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁) |