P. 128 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 12701-12800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	decrmanc 12701	Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (no carry). (Contributed by AV, 16-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ (𝐴 · 𝑃) = 𝐸    &   ⊢ ((𝐵 · 𝑃) + 𝑁) = 𝐹    ⇒   ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹
Theorem	decrmac 12702	Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (with carry). (Contributed by AV, 16-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ ((𝐴 · 𝑃) + 𝐺) = 𝐸    &   ⊢ ((𝐵 · 𝑃) + 𝑁) = ;𝐺𝐹    ⇒   ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹
Theorem	decaddm10 12703	The sum of two multiples of 10 is a multiple of 10. (Contributed by AV, 30-Jul-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    ⇒   ⊢ (;𝐴0 + ;𝐵0) = ;(𝐴 + 𝐵)0
Theorem	decaddi 12704	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ (𝐵 + 𝑁) = 𝐶    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐴𝐶
Theorem	decaddci 12705	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ (𝐴 + 1) = 𝐷    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ (𝐵 + 𝑁) = ;1𝐶    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐷𝐶
Theorem	decaddci2 12706	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ (𝐴 + 1) = 𝐷    &   ⊢ (𝐵 + 𝑁) = ;10    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐷0
Theorem	decsubi 12707	Difference between a numeral 𝑀 and a nonnegative integer 𝑁 (no underflow). (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ (𝐴 + 1) = 𝐷    &   ⊢ (𝐵 − 𝑁) = 𝐶    ⇒   ⊢ (𝑀 − 𝑁) = ;𝐴𝐶
Theorem	decmul1 12708	The product of a numeral with a number (no carry). (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.) Remove hypothesis 𝐷 ∈ ℕ0. (Revised by Steven Nguyen, 7-Dec-2022.)
⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 = ;𝐴𝐵    &   ⊢ (𝐴 · 𝑃) = 𝐶    &   ⊢ (𝐵 · 𝑃) = 𝐷    ⇒   ⊢ (𝑁 · 𝑃) = ;𝐶𝐷
Theorem	decmul1c 12709	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 12710	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 12711	The product of a numeral with a number (no carry). (Contributed by AV, 15-Jun-2021.)
⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    ⇒   ⊢ (𝑁 · ;𝐴𝐵) = ;(𝑁 · 𝐴)(𝑁 · 𝐵)
Theorem	11multnc 12712	The product of 11 (as numeral) with a number (no carry). (Contributed by AV, 15-Jun-2021.)
⊢ 𝑁 ∈ ℕ0    ⇒   ⊢ (𝑁 · ;11) = ;𝑁𝑁
Theorem	decmul10add 12713	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 12714	Lemma for 6p5e11 12717 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐵 = (𝐷 + 1)    &   ⊢ 𝐶 = (𝐸 + 1)    &   ⊢ (𝐴 + 𝐷) = ;1𝐸    ⇒   ⊢ (𝐴 + 𝐵) = ;1𝐶
Theorem	5p5e10 12715	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 12716	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 12717	6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (6 + 5) = ;11
Theorem	6p6e12 12718	6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 + 6) = ;12
Theorem	7p3e10 12719	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 12720	7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (7 + 4) = ;11
Theorem	7p5e12 12721	7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 5) = ;12
Theorem	7p6e13 12722	7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 6) = ;13
Theorem	7p7e14 12723	7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 7) = ;14
Theorem	8p2e10 12724	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 12725	8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (8 + 3) = ;11
Theorem	8p4e12 12726	8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 4) = ;12
Theorem	8p5e13 12727	8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 5) = ;13
Theorem	8p6e14 12728	8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 6) = ;14
Theorem	8p7e15 12729	8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 7) = ;15
Theorem	8p8e16 12730	8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 8) = ;16
Theorem	9p2e11 12731	9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (9 + 2) = ;11
Theorem	9p3e12 12732	9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 3) = ;12
Theorem	9p4e13 12733	9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 4) = ;13
Theorem	9p5e14 12734	9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 5) = ;14
Theorem	9p6e15 12735	9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 6) = ;15
Theorem	9p7e16 12736	9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 7) = ;16
Theorem	9p8e17 12737	9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 8) = ;17
Theorem	9p9e18 12738	9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 9) = ;18
Theorem	10p10e20 12739	10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (;10 + ;10) = ;20
Theorem	10m1e9 12740	10 - 1 = 9. (Contributed by AV, 6-Sep-2021.)
⊢ (;10 − 1) = 9
Theorem	4t3lem 12741	Lemma for 4t3e12 12742 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 = (𝐵 + 1)    &   ⊢ (𝐴 · 𝐵) = 𝐷    &   ⊢ (𝐷 + 𝐴) = 𝐸    ⇒   ⊢ (𝐴 · 𝐶) = 𝐸
Theorem	4t3e12 12742	4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (4 · 3) = ;12
Theorem	4t4e16 12743	4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (4 · 4) = ;16
Theorem	5t2e10 12744	5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 4-Sep-2021.)
⊢ (5 · 2) = ;10
Theorem	5t3e15 12745	5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (5 · 3) = ;15
Theorem	5t4e20 12746	5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (5 · 4) = ;20
Theorem	5t5e25 12747	5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (5 · 5) = ;25
Theorem	6t2e12 12748	6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 2) = ;12
Theorem	6t3e18 12749	6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 3) = ;18
Theorem	6t4e24 12750	6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 4) = ;24
Theorem	6t5e30 12751	6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (6 · 5) = ;30
Theorem	6t6e36 12752	6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (6 · 6) = ;36
Theorem	7t2e14 12753	7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 2) = ;14
Theorem	7t3e21 12754	7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 3) = ;21
Theorem	7t4e28 12755	7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 4) = ;28
Theorem	7t5e35 12756	7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 5) = ;35
Theorem	7t6e42 12757	7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 6) = ;42
Theorem	7t7e49 12758	7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 7) = ;49
Theorem	8t2e16 12759	8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 2) = ;16
Theorem	8t3e24 12760	8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 3) = ;24
Theorem	8t4e32 12761	8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 4) = ;32
Theorem	8t5e40 12762	8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (8 · 5) = ;40
Theorem	8t6e48 12763	8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (8 · 6) = ;48
Theorem	8t7e56 12764	8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 7) = ;56
Theorem	8t8e64 12765	8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 8) = ;64
Theorem	9t2e18 12766	9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 2) = ;18
Theorem	9t3e27 12767	9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 3) = ;27
Theorem	9t4e36 12768	9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 4) = ;36
Theorem	9t5e45 12769	9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 5) = ;45
Theorem	9t6e54 12770	9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 6) = ;54
Theorem	9t7e63 12771	9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 7) = ;63
Theorem	9t8e72 12772	9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 8) = ;72
Theorem	9t9e81 12773	9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 9) = ;81
Theorem	9t11e99 12774	9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.)
⊢ (9 · ;11) = ;99
Theorem	9lt10 12775	9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 9 < ;10
Theorem	8lt10 12776	8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 8 < ;10
Theorem	7lt10 12777	7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 7 < ;10
Theorem	6lt10 12778	6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 6 < ;10
Theorem	5lt10 12779	5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 5 < ;10
Theorem	4lt10 12780	4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 4 < ;10
Theorem	3lt10 12781	3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 3 < ;10
Theorem	2lt10 12782	2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 2 < ;10
Theorem	1lt10 12783	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 12784	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (4 · 𝐴) = (2 · (2 · 𝐴))
Theorem	decbin2 12785	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((4 · 𝐴) + 2) = (2 · ((2 · 𝐴) + 1))
Theorem	decbin3 12786	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((4 · 𝐴) + 3) = ((2 · ((2 · 𝐴) + 1)) + 1)
Theorem	5recm6rec 12787	One fifth minus one sixth. (Contributed by Scott Fenton, 9-Jan-2017.)
⊢ ((1 / 5) − (1 / 6)) = (1 / ;30)
5.4.11  Upper sets of integers
Syntax	cuz 12788	Extend class notation with the upper integer function. Read "ℤ≥‘𝑀 " as "the set of integers greater than or equal to 𝑀".
class ℤ≥
Definition	df-uz 12789*	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 12790 for its value, uzssz 12809 for its relationship to ℤ, nnuz 12827 and nn0uz 12826 for its relationships to ℕ and ℕ0, and eluz1 12792 and eluz2 12794 for its membership relations. (Contributed by NM, 5-Sep-2005.)
⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘})
Theorem	uzval 12790*	The value of the upper integers function. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝑁 ∈ ℤ → (ℤ≥‘𝑁) = {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘})
Theorem	uzf 12791	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 12792	Membership in the upper set of integers starting at 𝑀. (Contributed by NM, 5-Sep-2005.)
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
Theorem	eluzel2 12793	Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
Theorem	eluz2 12794	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	eluzmn 12795	Membership in an earlier upper set of integers. (Contributed by Thierry Arnoux, 8-Oct-2018.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ (ℤ≥‘(𝑀 − 𝑁)))
Theorem	eluz1i 12796	Membership in an upper set of integers. (Contributed by NM, 5-Sep-2005.)
⊢ 𝑀 ∈ ℤ    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
Theorem	eluzuzle 12797	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 12798	A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
Theorem	eluzelre 12799	A member of an upper set of integers is a real. (Contributed by Mario Carneiro, 31-Aug-2013.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ)
Theorem	eluzelcn 12800	A member of an upper set of integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ)