Theorem List for Intuitionistic Logic Explorer - 9301-9400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 10m1e9 9301 |
10 - 1 = 9. (Contributed by AV, 6-Sep-2021.)
|
⊢ (;10 − 1) = 9 |
|
Theorem | 4t3lem 9302 |
Lemma for 4t3e12 9303 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝐶 = (𝐵 + 1) & ⊢ (𝐴 · 𝐵) = 𝐷
& ⊢ (𝐷 + 𝐴) = 𝐸 ⇒ ⊢ (𝐴 · 𝐶) = 𝐸 |
|
Theorem | 4t3e12 9303 |
4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (4 · 3) = ;12 |
|
Theorem | 4t4e16 9304 |
4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (4 · 4) = ;16 |
|
Theorem | 5t2e10 9305 |
5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV,
4-Sep-2021.)
|
⊢ (5 · 2) = ;10 |
|
Theorem | 5t3e15 9306 |
5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 3) = ;15 |
|
Theorem | 5t4e20 9307 |
5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 4) = ;20 |
|
Theorem | 5t5e25 9308 |
5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 5) = ;25 |
|
Theorem | 6t2e12 9309 |
6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 2) = ;12 |
|
Theorem | 6t3e18 9310 |
6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 3) = ;18 |
|
Theorem | 6t4e24 9311 |
6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 4) = ;24 |
|
Theorem | 6t5e30 9312 |
6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (6 · 5) = ;30 |
|
Theorem | 6t6e36 9313 |
6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (6 · 6) = ;36 |
|
Theorem | 7t2e14 9314 |
7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 2) = ;14 |
|
Theorem | 7t3e21 9315 |
7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 3) = ;21 |
|
Theorem | 7t4e28 9316 |
7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 4) = ;28 |
|
Theorem | 7t5e35 9317 |
7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 5) = ;35 |
|
Theorem | 7t6e42 9318 |
7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 6) = ;42 |
|
Theorem | 7t7e49 9319 |
7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 7) = ;49 |
|
Theorem | 8t2e16 9320 |
8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 2) = ;16 |
|
Theorem | 8t3e24 9321 |
8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 3) = ;24 |
|
Theorem | 8t4e32 9322 |
8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 4) = ;32 |
|
Theorem | 8t5e40 9323 |
8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (8 · 5) = ;40 |
|
Theorem | 8t6e48 9324 |
8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (8 · 6) = ;48 |
|
Theorem | 8t7e56 9325 |
8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 7) = ;56 |
|
Theorem | 8t8e64 9326 |
8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 8) = ;64 |
|
Theorem | 9t2e18 9327 |
9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 2) = ;18 |
|
Theorem | 9t3e27 9328 |
9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 3) = ;27 |
|
Theorem | 9t4e36 9329 |
9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 4) = ;36 |
|
Theorem | 9t5e45 9330 |
9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 5) = ;45 |
|
Theorem | 9t6e54 9331 |
9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 6) = ;54 |
|
Theorem | 9t7e63 9332 |
9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 7) = ;63 |
|
Theorem | 9t8e72 9333 |
9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 8) = ;72 |
|
Theorem | 9t9e81 9334 |
9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 9) = ;81 |
|
Theorem | 9t11e99 9335 |
9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV,
6-Sep-2021.)
|
⊢ (9 · ;11) = ;99 |
|
Theorem | 9lt10 9336 |
9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
⊢ 9 < ;10 |
|
Theorem | 8lt10 9337 |
8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
⊢ 8 < ;10 |
|
Theorem | 7lt10 9338 |
7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 7 < ;10 |
|
Theorem | 6lt10 9339 |
6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 6 < ;10 |
|
Theorem | 5lt10 9340 |
5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 5 < ;10 |
|
Theorem | 4lt10 9341 |
4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 4 < ;10 |
|
Theorem | 3lt10 9342 |
3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 3 < ;10 |
|
Theorem | 2lt10 9343 |
2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 2 < ;10 |
|
Theorem | 1lt10 9344 |
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 9345 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝐴 ∈
ℕ0 ⇒ ⊢ (4 · 𝐴) = (2 · (2 · 𝐴)) |
|
Theorem | decbin2 9346 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝐴 ∈
ℕ0 ⇒ ⊢ ((4 · 𝐴) + 2) = (2 · ((2 · 𝐴) + 1)) |
|
Theorem | decbin3 9347 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝐴 ∈
ℕ0 ⇒ ⊢ ((4 · 𝐴) + 3) = ((2 · ((2 · 𝐴) + 1)) + 1) |
|
Theorem | halfthird 9348 |
Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015.)
|
⊢ ((1 / 2) − (1 / 3)) = (1 /
6) |
|
Theorem | 5recm6rec 9349 |
One fifth minus one sixth. (Contributed by Scott Fenton, 9-Jan-2017.)
|
⊢ ((1 / 5) − (1 / 6)) = (1 / ;30) |
|
4.4.11 Upper sets of integers
|
|
Syntax | cuz 9350 |
Extend class notation with the upper integer function.
Read "ℤ≥‘𝑀 " as "the set of integers
greater than or equal to
𝑀."
|
class ℤ≥ |
|
Definition | df-uz 9351* |
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 9352 for its
value, uzssz 9369 for its relationship to ℤ, nnuz 9385 and nn0uz 9384 for
its relationships to ℕ and ℕ0, and eluz1 9354 and eluz2 9356 for
its membership relations. (Contributed by NM, 5-Sep-2005.)
|
⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘}) |
|
Theorem | uzval 9352* |
The value of the upper integers function. (Contributed by NM,
5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ (𝑁 ∈ ℤ →
(ℤ≥‘𝑁) = {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘}) |
|
Theorem | uzf 9353 |
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 9354 |
Membership in the upper set of integers starting at 𝑀.
(Contributed by NM, 5-Sep-2005.)
|
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) |
|
Theorem | eluzel2 9355 |
Implication of membership in an upper set of integers. (Contributed by
NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
|
Theorem | eluz2 9356 |
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 9357 |
Membership in an upper set of integers. (Contributed by NM,
5-Sep-2005.)
|
⊢ 𝑀 ∈ ℤ
⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
|
Theorem | eluzuzle 9358 |
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 9359 |
A member of an upper set of integers is an integer. (Contributed by NM,
6-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
|
Theorem | eluzelre 9360 |
A member of an upper set of integers is a real. (Contributed by Mario
Carneiro, 31-Aug-2013.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ) |
|
Theorem | eluzelcn 9361 |
A member of an upper set of integers is a complex number. (Contributed by
Glauco Siliprandi, 29-Jun-2017.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ) |
|
Theorem | eluzle 9362 |
Implication of membership in an upper set of integers. (Contributed by
NM, 6-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
|
Theorem | eluz 9363 |
Membership in an upper set of integers. (Contributed by NM,
2-Oct-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) |
|
Theorem | uzid 9364 |
Membership of the least member in an upper set of integers. (Contributed
by NM, 2-Sep-2005.)
|
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀)) |
|
Theorem | uzn0 9365 |
The upper integers are all nonempty. (Contributed by Mario Carneiro,
16-Jan-2014.)
|
⊢ (𝑀 ∈ ran ℤ≥ →
𝑀 ≠
∅) |
|
Theorem | uztrn 9366 |
Transitive law for sets of upper integers. (Contributed by NM,
20-Sep-2005.)
|
⊢ ((𝑀 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝑁)) |
|
Theorem | uztrn2 9367 |
Transitive law for sets of upper integers. (Contributed by Mario
Carneiro, 26-Dec-2013.)
|
⊢ 𝑍 = (ℤ≥‘𝐾)
⇒ ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍) |
|
Theorem | uzneg 9368 |
Contraposition law for upper integers. (Contributed by NM,
28-Nov-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → -𝑀 ∈
(ℤ≥‘-𝑁)) |
|
Theorem | uzssz 9369 |
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 9370 |
Subset relationship for two sets of upper integers. (Contributed by NM,
5-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
|
Theorem | uztric 9371 |
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 9372 |
The upper integers function is one-to-one. (Contributed by NM,
12-Dec-2005.)
|
⊢ (𝑀 ∈ ℤ →
((ℤ≥‘𝑀) = (ℤ≥‘𝑁) ↔ 𝑀 = 𝑁)) |
|
Theorem | eluzp1m1 9373 |
Membership in the next upper set of integers. (Contributed by NM,
12-Sep-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
|
Theorem | eluzp1l 9374 |
Strict ordering implied by membership in the next upper set of integers.
(Contributed by NM, 12-Sep-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁) |
|
Theorem | eluzp1p1 9375 |
Membership in the next upper set of integers. (Contributed by NM,
5-Oct-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
|
Theorem | eluzaddi 9376 |
Membership in a later upper set of integers. (Contributed by Paul
Chapman, 22-Nov-2007.)
|
⊢ 𝑀 ∈ ℤ & ⊢ 𝐾 ∈
ℤ ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 𝐾) ∈
(ℤ≥‘(𝑀 + 𝐾))) |
|
Theorem | eluzsubi 9377 |
Membership in an earlier upper set of integers. (Contributed by Paul
Chapman, 22-Nov-2007.)
|
⊢ 𝑀 ∈ ℤ & ⊢ 𝐾 ∈
ℤ ⇒ ⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 𝐾)) → (𝑁 − 𝐾) ∈
(ℤ≥‘𝑀)) |
|
Theorem | eluzadd 9378 |
Membership in a later upper set of integers. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈
(ℤ≥‘(𝑀 + 𝐾))) |
|
Theorem | eluzsub 9379 |
Membership in an earlier upper set of integers. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 𝐾))) → (𝑁 − 𝐾) ∈
(ℤ≥‘𝑀)) |
|
Theorem | uzm1 9380 |
Choices for an element of an upper interval of integers. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈
(ℤ≥‘𝑀))) |
|
Theorem | uznn0sub 9381 |
The nonnegative difference of integers is a nonnegative integer.
(Contributed by NM, 4-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 − 𝑀) ∈
ℕ0) |
|
Theorem | uzin 9382 |
Intersection of two upper intervals of integers. (Contributed by Mario
Carneiro, 24-Dec-2013.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) =
(ℤ≥‘if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
|
Theorem | uzp1 9383 |
Choices for an element of an upper interval of integers. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈
(ℤ≥‘(𝑀 + 1)))) |
|
Theorem | nn0uz 9384 |
Nonnegative integers expressed as an upper set of integers. (Contributed
by NM, 2-Sep-2005.)
|
⊢ ℕ0 =
(ℤ≥‘0) |
|
Theorem | nnuz 9385 |
Positive integers expressed as an upper set of integers. (Contributed by
NM, 2-Sep-2005.)
|
⊢ ℕ =
(ℤ≥‘1) |
|
Theorem | elnnuz 9386 |
A positive integer expressed as a member of an upper set of integers.
(Contributed by NM, 6-Jun-2006.)
|
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈
(ℤ≥‘1)) |
|
Theorem | elnn0uz 9387 |
A nonnegative integer expressed as a member an upper set of integers.
(Contributed by NM, 6-Jun-2006.)
|
⊢ (𝑁 ∈ ℕ0 ↔ 𝑁 ∈
(ℤ≥‘0)) |
|
Theorem | eluz2nn 9388 |
An integer is greater than or equal to 2 is a positive integer.
(Contributed by AV, 3-Nov-2018.)
|
⊢ (𝐴 ∈ (ℤ≥‘2)
→ 𝐴 ∈
ℕ) |
|
Theorem | eluz4eluz2 9389 |
An integer greater than or equal to 4 is an integer greater than or equal
to 2. (Contributed by AV, 30-May-2023.)
|
⊢ (𝑋 ∈ (ℤ≥‘4)
→ 𝑋 ∈
(ℤ≥‘2)) |
|
Theorem | eluz4nn 9390 |
An integer greater than or equal to 4 is a positive integer. (Contributed
by AV, 30-May-2023.)
|
⊢ (𝑋 ∈ (ℤ≥‘4)
→ 𝑋 ∈
ℕ) |
|
Theorem | eluzge2nn0 9391 |
If an integer is greater than or equal to 2, then it is a nonnegative
integer. (Contributed by AV, 27-Aug-2018.) (Proof shortened by AV,
3-Nov-2018.)
|
⊢ (𝑁 ∈ (ℤ≥‘2)
→ 𝑁 ∈
ℕ0) |
|
Theorem | eluz2n0 9392 |
An integer greater than or equal to 2 is not 0. (Contributed by AV,
25-May-2020.)
|
⊢ (𝑁 ∈ (ℤ≥‘2)
→ 𝑁 ≠
0) |
|
Theorem | uzuzle23 9393 |
An integer in the upper set of integers starting at 3 is element of the
upper set of integers starting at 2. (Contributed by Alexander van der
Vekens, 17-Sep-2018.)
|
⊢ (𝐴 ∈ (ℤ≥‘3)
→ 𝐴 ∈
(ℤ≥‘2)) |
|
Theorem | eluzge3nn 9394 |
If an integer is greater than 3, then it is a positive integer.
(Contributed by Alexander van der Vekens, 17-Sep-2018.)
|
⊢ (𝑁 ∈ (ℤ≥‘3)
→ 𝑁 ∈
ℕ) |
|
Theorem | uz3m2nn 9395 |
An integer greater than or equal to 3 decreased by 2 is a positive
integer. (Contributed by Alexander van der Vekens, 17-Sep-2018.)
|
⊢ (𝑁 ∈ (ℤ≥‘3)
→ (𝑁 − 2)
∈ ℕ) |
|
Theorem | 1eluzge0 9396 |
1 is an integer greater than or equal to 0. (Contributed by Alexander van
der Vekens, 8-Jun-2018.)
|
⊢ 1 ∈
(ℤ≥‘0) |
|
Theorem | 2eluzge0 9397 |
2 is an integer greater than or equal to 0. (Contributed by Alexander van
der Vekens, 8-Jun-2018.) (Proof shortened by OpenAI, 25-Mar-2020.)
|
⊢ 2 ∈
(ℤ≥‘0) |
|
Theorem | 2eluzge1 9398 |
2 is an integer greater than or equal to 1. (Contributed by Alexander van
der Vekens, 8-Jun-2018.)
|
⊢ 2 ∈
(ℤ≥‘1) |
|
Theorem | uznnssnn 9399 |
The upper integers starting from a natural are a subset of the naturals.
(Contributed by Scott Fenton, 29-Jun-2013.)
|
⊢ (𝑁 ∈ ℕ →
(ℤ≥‘𝑁) ⊆ ℕ) |
|
Theorem | raluz 9400* |
Restricted universal quantification in an upper set of integers.
(Contributed by NM, 9-Sep-2005.)
|
⊢ (𝑀 ∈ ℤ → (∀𝑛 ∈
(ℤ≥‘𝑀)𝜑 ↔ ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑))) |