Theorem List for Intuitionistic Logic Explorer - 9501-9600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 8p5e13 9501 |
8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 5) = ;13 |
|
Theorem | 8p6e14 9502 |
8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 6) = ;14 |
|
Theorem | 8p7e15 9503 |
8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 7) = ;15 |
|
Theorem | 8p8e16 9504 |
8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 8) = ;16 |
|
Theorem | 9p2e11 9505 |
9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (9 + 2) = ;11 |
|
Theorem | 9p3e12 9506 |
9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 3) = ;12 |
|
Theorem | 9p4e13 9507 |
9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 4) = ;13 |
|
Theorem | 9p5e14 9508 |
9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 5) = ;14 |
|
Theorem | 9p6e15 9509 |
9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 6) = ;15 |
|
Theorem | 9p7e16 9510 |
9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 7) = ;16 |
|
Theorem | 9p8e17 9511 |
9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 8) = ;17 |
|
Theorem | 9p9e18 9512 |
9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 9) = ;18 |
|
Theorem | 10p10e20 9513 |
10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (;10 + ;10) = ;20 |
|
Theorem | 10m1e9 9514 |
10 - 1 = 9. (Contributed by AV, 6-Sep-2021.)
|
⊢ (;10 − 1) = 9 |
|
Theorem | 4t3lem 9515 |
Lemma for 4t3e12 9516 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝐶 = (𝐵 + 1) & ⊢ (𝐴 · 𝐵) = 𝐷
& ⊢ (𝐷 + 𝐴) = 𝐸 ⇒ ⊢ (𝐴 · 𝐶) = 𝐸 |
|
Theorem | 4t3e12 9516 |
4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (4 · 3) = ;12 |
|
Theorem | 4t4e16 9517 |
4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (4 · 4) = ;16 |
|
Theorem | 5t2e10 9518 |
5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV,
4-Sep-2021.)
|
⊢ (5 · 2) = ;10 |
|
Theorem | 5t3e15 9519 |
5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 3) = ;15 |
|
Theorem | 5t4e20 9520 |
5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 4) = ;20 |
|
Theorem | 5t5e25 9521 |
5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 5) = ;25 |
|
Theorem | 6t2e12 9522 |
6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 2) = ;12 |
|
Theorem | 6t3e18 9523 |
6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 3) = ;18 |
|
Theorem | 6t4e24 9524 |
6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 4) = ;24 |
|
Theorem | 6t5e30 9525 |
6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (6 · 5) = ;30 |
|
Theorem | 6t6e36 9526 |
6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (6 · 6) = ;36 |
|
Theorem | 7t2e14 9527 |
7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 2) = ;14 |
|
Theorem | 7t3e21 9528 |
7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 3) = ;21 |
|
Theorem | 7t4e28 9529 |
7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 4) = ;28 |
|
Theorem | 7t5e35 9530 |
7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 5) = ;35 |
|
Theorem | 7t6e42 9531 |
7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 6) = ;42 |
|
Theorem | 7t7e49 9532 |
7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 7) = ;49 |
|
Theorem | 8t2e16 9533 |
8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 2) = ;16 |
|
Theorem | 8t3e24 9534 |
8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 3) = ;24 |
|
Theorem | 8t4e32 9535 |
8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 4) = ;32 |
|
Theorem | 8t5e40 9536 |
8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (8 · 5) = ;40 |
|
Theorem | 8t6e48 9537 |
8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (8 · 6) = ;48 |
|
Theorem | 8t7e56 9538 |
8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 7) = ;56 |
|
Theorem | 8t8e64 9539 |
8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 8) = ;64 |
|
Theorem | 9t2e18 9540 |
9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 2) = ;18 |
|
Theorem | 9t3e27 9541 |
9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 3) = ;27 |
|
Theorem | 9t4e36 9542 |
9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 4) = ;36 |
|
Theorem | 9t5e45 9543 |
9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 5) = ;45 |
|
Theorem | 9t6e54 9544 |
9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 6) = ;54 |
|
Theorem | 9t7e63 9545 |
9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 7) = ;63 |
|
Theorem | 9t8e72 9546 |
9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 8) = ;72 |
|
Theorem | 9t9e81 9547 |
9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 9) = ;81 |
|
Theorem | 9t11e99 9548 |
9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV,
6-Sep-2021.)
|
⊢ (9 · ;11) = ;99 |
|
Theorem | 9lt10 9549 |
9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
⊢ 9 < ;10 |
|
Theorem | 8lt10 9550 |
8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
⊢ 8 < ;10 |
|
Theorem | 7lt10 9551 |
7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 7 < ;10 |
|
Theorem | 6lt10 9552 |
6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 6 < ;10 |
|
Theorem | 5lt10 9553 |
5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 5 < ;10 |
|
Theorem | 4lt10 9554 |
4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 4 < ;10 |
|
Theorem | 3lt10 9555 |
3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 3 < ;10 |
|
Theorem | 2lt10 9556 |
2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 2 < ;10 |
|
Theorem | 1lt10 9557 |
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 9558 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝐴 ∈
ℕ0 ⇒ ⊢ (4 · 𝐴) = (2 · (2 · 𝐴)) |
|
Theorem | decbin2 9559 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝐴 ∈
ℕ0 ⇒ ⊢ ((4 · 𝐴) + 2) = (2 · ((2 · 𝐴) + 1)) |
|
Theorem | decbin3 9560 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝐴 ∈
ℕ0 ⇒ ⊢ ((4 · 𝐴) + 3) = ((2 · ((2 · 𝐴) + 1)) + 1) |
|
Theorem | halfthird 9561 |
Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015.)
|
⊢ ((1 / 2) − (1 / 3)) = (1 /
6) |
|
Theorem | 5recm6rec 9562 |
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 9563 |
Extend class notation with the upper integer function.
Read "ℤ≥‘𝑀 " as "the set of integers
greater than or equal to
𝑀".
|
class ℤ≥ |
|
Definition | df-uz 9564* |
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 9565 for its
value, uzssz 9583 for its relationship to ℤ, nnuz 9599 and nn0uz 9598 for
its relationships to ℕ and ℕ0, and eluz1 9567 and eluz2 9569 for
its membership relations. (Contributed by NM, 5-Sep-2005.)
|
⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘}) |
|
Theorem | uzval 9565* |
The value of the upper integers function. (Contributed by NM,
5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ (𝑁 ∈ ℤ →
(ℤ≥‘𝑁) = {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘}) |
|
Theorem | uzf 9566 |
The domain and codomain of the upper integers function. (Contributed by
Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢
ℤ≥:ℤ⟶𝒫
ℤ |
|
Theorem | eluz1 9567 |
Membership in the upper set of integers starting at 𝑀.
(Contributed by NM, 5-Sep-2005.)
|
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) |
|
Theorem | eluzel2 9568 |
Implication of membership in an upper set of integers. (Contributed by
NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
|
Theorem | eluz2 9569 |
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 9570 |
Membership in an upper set of integers. (Contributed by NM,
5-Sep-2005.)
|
⊢ 𝑀 ∈ ℤ
⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
|
Theorem | eluzuzle 9571 |
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 9572 |
A member of an upper set of integers is an integer. (Contributed by NM,
6-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
|
Theorem | eluzelre 9573 |
A member of an upper set of integers is a real. (Contributed by Mario
Carneiro, 31-Aug-2013.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ) |
|
Theorem | eluzelcn 9574 |
A member of an upper set of integers is a complex number. (Contributed by
Glauco Siliprandi, 29-Jun-2017.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ) |
|
Theorem | eluzle 9575 |
Implication of membership in an upper set of integers. (Contributed by
NM, 6-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
|
Theorem | eluz 9576 |
Membership in an upper set of integers. (Contributed by NM,
2-Oct-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) |
|
Theorem | uzid 9577 |
Membership of the least member in an upper set of integers. (Contributed
by NM, 2-Sep-2005.)
|
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀)) |
|
Theorem | uzidd 9578 |
Membership of the least member in an upper set of integers.
(Contributed by Glauco Siliprandi, 23-Oct-2021.)
|
⊢ (𝜑 → 𝑀 ∈ ℤ)
⇒ ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
|
Theorem | uzn0 9579 |
The upper integers are all nonempty. (Contributed by Mario Carneiro,
16-Jan-2014.)
|
⊢ (𝑀 ∈ ran ℤ≥ →
𝑀 ≠
∅) |
|
Theorem | uztrn 9580 |
Transitive law for sets of upper integers. (Contributed by NM,
20-Sep-2005.)
|
⊢ ((𝑀 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝑁)) |
|
Theorem | uztrn2 9581 |
Transitive law for sets of upper integers. (Contributed by Mario
Carneiro, 26-Dec-2013.)
|
⊢ 𝑍 = (ℤ≥‘𝐾)
⇒ ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍) |
|
Theorem | uzneg 9582 |
Contraposition law for upper integers. (Contributed by NM,
28-Nov-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → -𝑀 ∈
(ℤ≥‘-𝑁)) |
|
Theorem | uzssz 9583 |
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 9584 |
Subset relationship for two sets of upper integers. (Contributed by NM,
5-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
|
Theorem | uztric 9585 |
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 9586 |
The upper integers function is one-to-one. (Contributed by NM,
12-Dec-2005.)
|
⊢ (𝑀 ∈ ℤ →
((ℤ≥‘𝑀) = (ℤ≥‘𝑁) ↔ 𝑀 = 𝑁)) |
|
Theorem | eluzp1m1 9587 |
Membership in the next upper set of integers. (Contributed by NM,
12-Sep-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
|
Theorem | eluzp1l 9588 |
Strict ordering implied by membership in the next upper set of integers.
(Contributed by NM, 12-Sep-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁) |
|
Theorem | eluzp1p1 9589 |
Membership in the next upper set of integers. (Contributed by NM,
5-Oct-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
|
Theorem | eluzaddi 9590 |
Membership in a later upper set of integers. (Contributed by Paul
Chapman, 22-Nov-2007.)
|
⊢ 𝑀 ∈ ℤ & ⊢ 𝐾 ∈
ℤ ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 𝐾) ∈
(ℤ≥‘(𝑀 + 𝐾))) |
|
Theorem | eluzsubi 9591 |
Membership in an earlier upper set of integers. (Contributed by Paul
Chapman, 22-Nov-2007.)
|
⊢ 𝑀 ∈ ℤ & ⊢ 𝐾 ∈
ℤ ⇒ ⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 𝐾)) → (𝑁 − 𝐾) ∈
(ℤ≥‘𝑀)) |
|
Theorem | eluzadd 9592 |
Membership in a later upper set of integers. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈
(ℤ≥‘(𝑀 + 𝐾))) |
|
Theorem | eluzsub 9593 |
Membership in an earlier upper set of integers. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 𝐾))) → (𝑁 − 𝐾) ∈
(ℤ≥‘𝑀)) |
|
Theorem | uzm1 9594 |
Choices for an element of an upper interval of integers. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈
(ℤ≥‘𝑀))) |
|
Theorem | uznn0sub 9595 |
The nonnegative difference of integers is a nonnegative integer.
(Contributed by NM, 4-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 − 𝑀) ∈
ℕ0) |
|
Theorem | uzin 9596 |
Intersection of two upper intervals of integers. (Contributed by Mario
Carneiro, 24-Dec-2013.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) =
(ℤ≥‘if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
|
Theorem | uzp1 9597 |
Choices for an element of an upper interval of integers. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈
(ℤ≥‘(𝑀 + 1)))) |
|
Theorem | nn0uz 9598 |
Nonnegative integers expressed as an upper set of integers. (Contributed
by NM, 2-Sep-2005.)
|
⊢ ℕ0 =
(ℤ≥‘0) |
|
Theorem | nnuz 9599 |
Positive integers expressed as an upper set of integers. (Contributed by
NM, 2-Sep-2005.)
|
⊢ ℕ =
(ℤ≥‘1) |
|
Theorem | elnnuz 9600 |
A positive integer expressed as a member of an upper set of integers.
(Contributed by NM, 6-Jun-2006.)
|
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈
(ℤ≥‘1)) |