Theorem List for Intuitionistic Logic Explorer - 9001-9100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | decmul1 9001 |
The product of a numeral with a number (no carry). (Contributed by
AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.)
|
⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐴 ∈
ℕ0
& ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 = ;𝐴𝐵
& ⊢ 𝐷 ∈ ℕ0 & ⊢ (𝐴 · 𝑃) = 𝐶
& ⊢ (𝐵 · 𝑃) = 𝐷 ⇒ ⊢ (𝑁 · 𝑃) = ;𝐶𝐷 |
|
Theorem | decmul1c 9002 |
The product of a numeral with a number (with carry). (Contributed by
Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐴 ∈
ℕ0
& ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 = ;𝐴𝐵
& ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈
ℕ0
& ⊢ ((𝐴 · 𝑃) + 𝐸) = 𝐶
& ⊢ (𝐵 · 𝑃) = ;𝐸𝐷 ⇒ ⊢ (𝑁 · 𝑃) = ;𝐶𝐷 |
|
Theorem | decmul2c 9003 |
The product of a numeral with a number (with carry). (Contributed by
Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐴 ∈
ℕ0
& ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 = ;𝐴𝐵
& ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈
ℕ0
& ⊢ ((𝑃 · 𝐴) + 𝐸) = 𝐶
& ⊢ (𝑃 · 𝐵) = ;𝐸𝐷 ⇒ ⊢ (𝑃 · 𝑁) = ;𝐶𝐷 |
|
Theorem | decmulnc 9004 |
The product of a numeral with a number (no carry). (Contributed by AV,
15-Jun-2021.)
|
⊢ 𝑁 ∈ ℕ0 & ⊢ 𝐴 ∈
ℕ0
& ⊢ 𝐵 ∈
ℕ0 ⇒ ⊢ (𝑁 · ;𝐴𝐵) = ;(𝑁 · 𝐴)(𝑁 · 𝐵) |
|
Theorem | 11multnc 9005 |
The product of 11 (as numeral) with a number (no carry). (Contributed
by AV, 15-Jun-2021.)
|
⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ (𝑁 · ;11) = ;𝑁𝑁 |
|
Theorem | decmul10add 9006 |
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 9007 |
Lemma for 6p5e11 9010 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐷 ∈
ℕ0
& ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐵 = (𝐷 + 1) & ⊢ 𝐶 = (𝐸 + 1) & ⊢ (𝐴 + 𝐷) = ;1𝐸 ⇒ ⊢ (𝐴 + 𝐵) = ;1𝐶 |
|
Theorem | 5p5e10 9008 |
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 9009 |
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 9010 |
6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (6 + 5) = ;11 |
|
Theorem | 6p6e12 9011 |
6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 + 6) = ;12 |
|
Theorem | 7p3e10 9012 |
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 9013 |
7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (7 + 4) = ;11 |
|
Theorem | 7p5e12 9014 |
7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 + 5) = ;12 |
|
Theorem | 7p6e13 9015 |
7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 + 6) = ;13 |
|
Theorem | 7p7e14 9016 |
7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 + 7) = ;14 |
|
Theorem | 8p2e10 9017 |
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 9018 |
8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (8 + 3) = ;11 |
|
Theorem | 8p4e12 9019 |
8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 4) = ;12 |
|
Theorem | 8p5e13 9020 |
8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 5) = ;13 |
|
Theorem | 8p6e14 9021 |
8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 6) = ;14 |
|
Theorem | 8p7e15 9022 |
8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 7) = ;15 |
|
Theorem | 8p8e16 9023 |
8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 8) = ;16 |
|
Theorem | 9p2e11 9024 |
9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (9 + 2) = ;11 |
|
Theorem | 9p3e12 9025 |
9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 3) = ;12 |
|
Theorem | 9p4e13 9026 |
9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 4) = ;13 |
|
Theorem | 9p5e14 9027 |
9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 5) = ;14 |
|
Theorem | 9p6e15 9028 |
9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 6) = ;15 |
|
Theorem | 9p7e16 9029 |
9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 7) = ;16 |
|
Theorem | 9p8e17 9030 |
9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 8) = ;17 |
|
Theorem | 9p9e18 9031 |
9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 9) = ;18 |
|
Theorem | 10p10e20 9032 |
10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (;10 + ;10) = ;20 |
|
Theorem | 10m1e9 9033 |
10 - 1 = 9. (Contributed by AV, 6-Sep-2021.)
|
⊢ (;10 − 1) = 9 |
|
Theorem | 4t3lem 9034 |
Lemma for 4t3e12 9035 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝐶 = (𝐵 + 1) & ⊢ (𝐴 · 𝐵) = 𝐷
& ⊢ (𝐷 + 𝐴) = 𝐸 ⇒ ⊢ (𝐴 · 𝐶) = 𝐸 |
|
Theorem | 4t3e12 9035 |
4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (4 · 3) = ;12 |
|
Theorem | 4t4e16 9036 |
4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (4 · 4) = ;16 |
|
Theorem | 5t2e10 9037 |
5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV,
4-Sep-2021.)
|
⊢ (5 · 2) = ;10 |
|
Theorem | 5t3e15 9038 |
5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 3) = ;15 |
|
Theorem | 5t4e20 9039 |
5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 4) = ;20 |
|
Theorem | 5t5e25 9040 |
5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 5) = ;25 |
|
Theorem | 6t2e12 9041 |
6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 2) = ;12 |
|
Theorem | 6t3e18 9042 |
6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 3) = ;18 |
|
Theorem | 6t4e24 9043 |
6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 4) = ;24 |
|
Theorem | 6t5e30 9044 |
6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (6 · 5) = ;30 |
|
Theorem | 6t6e36 9045 |
6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (6 · 6) = ;36 |
|
Theorem | 7t2e14 9046 |
7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 2) = ;14 |
|
Theorem | 7t3e21 9047 |
7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 3) = ;21 |
|
Theorem | 7t4e28 9048 |
7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 4) = ;28 |
|
Theorem | 7t5e35 9049 |
7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 5) = ;35 |
|
Theorem | 7t6e42 9050 |
7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 6) = ;42 |
|
Theorem | 7t7e49 9051 |
7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 7) = ;49 |
|
Theorem | 8t2e16 9052 |
8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 2) = ;16 |
|
Theorem | 8t3e24 9053 |
8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 3) = ;24 |
|
Theorem | 8t4e32 9054 |
8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 4) = ;32 |
|
Theorem | 8t5e40 9055 |
8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (8 · 5) = ;40 |
|
Theorem | 8t6e48 9056 |
8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (8 · 6) = ;48 |
|
Theorem | 8t7e56 9057 |
8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 7) = ;56 |
|
Theorem | 8t8e64 9058 |
8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 8) = ;64 |
|
Theorem | 9t2e18 9059 |
9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 2) = ;18 |
|
Theorem | 9t3e27 9060 |
9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 3) = ;27 |
|
Theorem | 9t4e36 9061 |
9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 4) = ;36 |
|
Theorem | 9t5e45 9062 |
9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 5) = ;45 |
|
Theorem | 9t6e54 9063 |
9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 6) = ;54 |
|
Theorem | 9t7e63 9064 |
9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 7) = ;63 |
|
Theorem | 9t8e72 9065 |
9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 8) = ;72 |
|
Theorem | 9t9e81 9066 |
9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 9) = ;81 |
|
Theorem | 9t11e99 9067 |
9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV,
6-Sep-2021.)
|
⊢ (9 · ;11) = ;99 |
|
Theorem | 9lt10 9068 |
9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
⊢ 9 < ;10 |
|
Theorem | 8lt10 9069 |
8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
⊢ 8 < ;10 |
|
Theorem | 7lt10 9070 |
7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 7 < ;10 |
|
Theorem | 6lt10 9071 |
6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 6 < ;10 |
|
Theorem | 5lt10 9072 |
5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 5 < ;10 |
|
Theorem | 4lt10 9073 |
4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 4 < ;10 |
|
Theorem | 3lt10 9074 |
3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 3 < ;10 |
|
Theorem | 2lt10 9075 |
2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 2 < ;10 |
|
Theorem | 1lt10 9076 |
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 9077 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝐴 ∈
ℕ0 ⇒ ⊢ (4 · 𝐴) = (2 · (2 · 𝐴)) |
|
Theorem | decbin2 9078 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝐴 ∈
ℕ0 ⇒ ⊢ ((4 · 𝐴) + 2) = (2 · ((2 · 𝐴) + 1)) |
|
Theorem | decbin3 9079 |
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 9080 |
Extend class notation with the upper integer function.
Read "ℤ≥‘𝑀 " as "the set of integers
greater than or equal to
𝑀."
|
class ℤ≥ |
|
Definition | df-uz 9081* |
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 9082 for its
value, uzssz 9099 for its relationship to ℤ, nnuz 9115 and nn0uz 9114 for
its relationships to ℕ and ℕ0, and eluz1 9084 and eluz2 9086 for
its membership relations. (Contributed by NM, 5-Sep-2005.)
|
⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘}) |
|
Theorem | uzval 9082* |
The value of the upper integers function. (Contributed by NM,
5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ (𝑁 ∈ ℤ →
(ℤ≥‘𝑁) = {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘}) |
|
Theorem | uzf 9083 |
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 9084 |
Membership in the upper set of integers starting at 𝑀.
(Contributed by NM, 5-Sep-2005.)
|
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) |
|
Theorem | eluzel2 9085 |
Implication of membership in an upper set of integers. (Contributed by
NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
|
Theorem | eluz2 9086 |
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 9087 |
Membership in an upper set of integers. (Contributed by NM,
5-Sep-2005.)
|
⊢ 𝑀 ∈ ℤ
⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
|
Theorem | eluzuzle 9088 |
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 9089 |
A member of an upper set of integers is an integer. (Contributed by NM,
6-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
|
Theorem | eluzelre 9090 |
A member of an upper set of integers is a real. (Contributed by Mario
Carneiro, 31-Aug-2013.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ) |
|
Theorem | eluzelcn 9091 |
A member of an upper set of integers is a complex number. (Contributed by
Glauco Siliprandi, 29-Jun-2017.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ) |
|
Theorem | eluzle 9092 |
Implication of membership in an upper set of integers. (Contributed by
NM, 6-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
|
Theorem | eluz 9093 |
Membership in an upper set of integers. (Contributed by NM,
2-Oct-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) |
|
Theorem | uzid 9094 |
Membership of the least member in an upper set of integers. (Contributed
by NM, 2-Sep-2005.)
|
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀)) |
|
Theorem | uzn0 9095 |
The upper integers are all nonempty. (Contributed by Mario Carneiro,
16-Jan-2014.)
|
⊢ (𝑀 ∈ ran ℤ≥ →
𝑀 ≠
∅) |
|
Theorem | uztrn 9096 |
Transitive law for sets of upper integers. (Contributed by NM,
20-Sep-2005.)
|
⊢ ((𝑀 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝑁)) |
|
Theorem | uztrn2 9097 |
Transitive law for sets of upper integers. (Contributed by Mario
Carneiro, 26-Dec-2013.)
|
⊢ 𝑍 = (ℤ≥‘𝐾)
⇒ ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍) |
|
Theorem | uzneg 9098 |
Contraposition law for upper integers. (Contributed by NM,
28-Nov-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → -𝑀 ∈
(ℤ≥‘-𝑁)) |
|
Theorem | uzssz 9099 |
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 9100 |
Subset relationship for two sets of upper integers. (Contributed by NM,
5-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |