P. 85 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8401-8500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	numadd 8401	Add two decimal integers 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵)    &   ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷)    &   ⊢ (𝐴 + 𝐶) = 𝐸    &   ⊢ (𝐵 + 𝐷) = 𝐹    ⇒   ⊢ (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
Theorem	numaddc 8402	Add two decimal integers 𝑀 and 𝑁 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵)    &   ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷)    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ ((𝐴 + 𝐶) + 1) = 𝐸    &   ⊢ (𝐵 + 𝐷) = ((𝑇 · 1) + 𝐹)    ⇒   ⊢ (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
Theorem	nummul1c 8403	The product of a decimal integer with a number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝐵)    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ ((𝐴 · 𝑃) + 𝐸) = 𝐶    &   ⊢ (𝐵 · 𝑃) = ((𝑇 · 𝐸) + 𝐷)    ⇒   ⊢ (𝑁 · 𝑃) = ((𝑇 · 𝐶) + 𝐷)
Theorem	nummul2c 8404	The product of a decimal integer with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝐵)    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ ((𝑃 · 𝐴) + 𝐸) = 𝐶    &   ⊢ (𝑃 · 𝐵) = ((𝑇 · 𝐸) + 𝐷)    ⇒   ⊢ (𝑃 · 𝑁) = ((𝑇 · 𝐶) + 𝐷)
Theorem	decma 8405	Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ ((𝐴 · 𝑃) + 𝐶) = 𝐸    &   ⊢ ((𝐵 · 𝑃) + 𝐷) = 𝐹    ⇒   ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹
Theorem	decmac 8406	Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ ((𝐴 · 𝑃) + (𝐶 + 𝐺)) = 𝐸    &   ⊢ ((𝐵 · 𝑃) + 𝐷) = ;𝐺𝐹    ⇒   ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹
Theorem	decma2c 8407	Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ ((𝑃 · 𝐴) + (𝐶 + 𝐺)) = 𝐸    &   ⊢ ((𝑃 · 𝐵) + 𝐷) = ;𝐺𝐹    ⇒   ⊢ ((𝑃 · 𝑀) + 𝑁) = ;𝐸𝐹
Theorem	decadd 8408	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ (𝐴 + 𝐶) = 𝐸    &   ⊢ (𝐵 + 𝐷) = 𝐹    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐸𝐹
Theorem	decaddc 8409	Add two numerals 𝑀 and 𝑁 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ ((𝐴 + 𝐶) + 1) = 𝐸    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ (𝐵 + 𝐷) = ;1𝐹    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐸𝐹
Theorem	decaddc2 8410	Add two numerals 𝑀 and 𝑁 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ ((𝐴 + 𝐶) + 1) = 𝐸    &   ⊢ (𝐵 + 𝐷) = 10    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐸0
Theorem	decaddi 8411	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ (𝐵 + 𝑁) = 𝐶    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐴𝐶
Theorem	decaddci 8412	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ (𝐴 + 1) = 𝐷    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ (𝐵 + 𝑁) = ;1𝐶    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐷𝐶
Theorem	decaddci2 8413	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ (𝐴 + 1) = 𝐷    &   ⊢ (𝐵 + 𝑁) = 10    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐷0
Theorem	decmul1c 8414	The product of a numeral with a number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 = ;𝐴𝐵    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ ((𝐴 · 𝑃) + 𝐸) = 𝐶    &   ⊢ (𝐵 · 𝑃) = ;𝐸𝐷    ⇒   ⊢ (𝑁 · 𝑃) = ;𝐶𝐷
Theorem	decmul2c 8415	The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 = ;𝐴𝐵    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ ((𝑃 · 𝐴) + 𝐸) = 𝐶    &   ⊢ (𝑃 · 𝐵) = ;𝐸𝐷    ⇒   ⊢ (𝑃 · 𝑁) = ;𝐶𝐷
Theorem	6p5lem 8416	Lemma for 6p5e11 8417 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐵 = (𝐷 + 1)    &   ⊢ 𝐶 = (𝐸 + 1)    &   ⊢ (𝐴 + 𝐷) = ;1𝐸    ⇒   ⊢ (𝐴 + 𝐵) = ;1𝐶
Theorem	6p5e11 8417	6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 + 5) = ;11
Theorem	6p6e12 8418	6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 + 6) = ;12
Theorem	7p4e11 8419	7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 4) = ;11
Theorem	7p5e12 8420	7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 5) = ;12
Theorem	7p6e13 8421	7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 6) = ;13
Theorem	7p7e14 8422	7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 7) = ;14
Theorem	8p3e11 8423	8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 3) = ;11
Theorem	8p4e12 8424	8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 4) = ;12
Theorem	8p5e13 8425	8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 5) = ;13
Theorem	8p6e14 8426	8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 6) = ;14
Theorem	8p7e15 8427	8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 7) = ;15
Theorem	8p8e16 8428	8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 8) = ;16
Theorem	9p2e11 8429	9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 2) = ;11
Theorem	9p3e12 8430	9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 3) = ;12
Theorem	9p4e13 8431	9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 4) = ;13
Theorem	9p5e14 8432	9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 5) = ;14
Theorem	9p6e15 8433	9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 6) = ;15
Theorem	9p7e16 8434	9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 7) = ;16
Theorem	9p8e17 8435	9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 8) = ;17
Theorem	9p9e18 8436	9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 9) = ;18
Theorem	10p10e20 8437	10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (10 + 10) = ;20
Theorem	4t3lem 8438	Lemma for 4t3e12 8439 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 = (𝐵 + 1)    &   ⊢ (𝐴 · 𝐵) = 𝐷    &   ⊢ (𝐷 + 𝐴) = 𝐸    ⇒   ⊢ (𝐴 · 𝐶) = 𝐸
Theorem	4t3e12 8439	4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (4 · 3) = ;12
Theorem	4t4e16 8440	4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (4 · 4) = ;16
Theorem	5t3e15 8441	5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (5 · 3) = ;15
Theorem	5t4e20 8442	5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (5 · 4) = ;20
Theorem	5t5e25 8443	5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (5 · 5) = ;25
Theorem	6t2e12 8444	6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 2) = ;12
Theorem	6t3e18 8445	6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 3) = ;18
Theorem	6t4e24 8446	6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 4) = ;24
Theorem	6t5e30 8447	6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 5) = ;30
Theorem	6t6e36 8448	6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 6) = ;36
Theorem	7t2e14 8449	7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 2) = ;14
Theorem	7t3e21 8450	7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 3) = ;21
Theorem	7t4e28 8451	7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 4) = ;28
Theorem	7t5e35 8452	7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 5) = ;35
Theorem	7t6e42 8453	7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 6) = ;42
Theorem	7t7e49 8454	7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 7) = ;49
Theorem	8t2e16 8455	8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 2) = ;16
Theorem	8t3e24 8456	8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 3) = ;24
Theorem	8t4e32 8457	8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 4) = ;32
Theorem	8t5e40 8458	8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 5) = ;40
Theorem	8t6e48 8459	8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 6) = ;48
Theorem	8t7e56 8460	8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 7) = ;56
Theorem	8t8e64 8461	8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 8) = ;64
Theorem	9t2e18 8462	9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 2) = ;18
Theorem	9t3e27 8463	9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 3) = ;27
Theorem	9t4e36 8464	9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 4) = ;36
Theorem	9t5e45 8465	9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 5) = ;45
Theorem	9t6e54 8466	9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 6) = ;54
Theorem	9t7e63 8467	9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 7) = ;63
Theorem	9t8e72 8468	9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 8) = ;72
Theorem	9t9e81 8469	9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 9) = ;81
Theorem	decbin0 8470	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (4 · 𝐴) = (2 · (2 · 𝐴))
Theorem	decbin2 8471	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((4 · 𝐴) + 2) = (2 · ((2 · 𝐴) + 1))
Theorem	decbin3 8472	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((4 · 𝐴) + 3) = ((2 · ((2 · 𝐴) + 1)) + 1)
3.4.10  Upper sets of integers
Syntax	cuz 8473	Extend class notation with the upper integer function. Read "ℤ≥‘𝑀 " as "the set of integers greater than or equal to 𝑀."
class ℤ≥
Definition	df-uz 8474*	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 8475 for its value, uzssz 8492 for its relationship to ℤ, nnuz 8508 and nn0uz 8507 for its relationships to ℕ and ℕ0, and eluz1 8477 and eluz2 8479 for its membership relations. (Contributed by NM, 5-Sep-2005.)
⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘})
Theorem	uzval 8475*	The value of the upper integers function. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝑁 ∈ ℤ → (ℤ≥‘𝑁) = {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘})
Theorem	uzf 8476	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 8477	Membership in the upper set of integers starting at 𝑀. (Contributed by NM, 5-Sep-2005.)
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
Theorem	eluzel2 8478	Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
Theorem	eluz2 8479	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 8480	Membership in an upper set of integers. (Contributed by NM, 5-Sep-2005.)
⊢ 𝑀 ∈ ℤ    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
Theorem	eluzuzle 8481	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 8482	A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
Theorem	eluzelre 8483	A member of an upper set of integers is a real. (Contributed by Mario Carneiro, 31-Aug-2013.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ)
Theorem	eluzelcn 8484	A member of an upper set of integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ)
Theorem	eluzle 8485	Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁)
Theorem	eluz 8486	Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁))
Theorem	uzid 8487	Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.)
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
Theorem	uzn0 8488	The upper integers are all nonempty. (Contributed by Mario Carneiro, 16-Jan-2014.)
⊢ (𝑀 ∈ ran ℤ≥ → 𝑀 ≠ ∅)
Theorem	uztrn 8489	Transitive law for sets of upper integers. (Contributed by NM, 20-Sep-2005.)
⊢ ((𝑀 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝑁))
Theorem	uztrn2 8490	Transitive law for sets of upper integers. (Contributed by Mario Carneiro, 26-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝐾)    ⇒   ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍)
Theorem	uzneg 8491	Contraposition law for upper integers. (Contributed by NM, 28-Nov-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → -𝑀 ∈ (ℤ≥‘-𝑁))
Theorem	uzssz 8492	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 8493	Subset relationship for two sets of upper integers. (Contributed by NM, 5-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆ (ℤ≥‘𝑀))
Theorem	uztric 8494	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 8495	The upper integers function is one-to-one. (Contributed by NM, 12-Dec-2005.)
⊢ (𝑀 ∈ ℤ → ((ℤ≥‘𝑀) = (ℤ≥‘𝑁) ↔ 𝑀 = 𝑁))
Theorem	eluzp1m1 8496	Membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈ (ℤ≥‘𝑀))
Theorem	eluzp1l 8497	Strict ordering implied by membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁)
Theorem	eluzp1p1 8498	Membership in the next upper set of integers. (Contributed by NM, 5-Oct-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘(𝑀 + 1)))
Theorem	eluzaddi 8499	Membership in a later upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.)
⊢ 𝑀 ∈ ℤ    &   ⊢ 𝐾 ∈ ℤ    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾)))
Theorem	eluzsubi 8500	Membership in an earlier upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.)
⊢ 𝑀 ∈ ℤ    &   ⊢ 𝐾 ∈ ℤ    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾)) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀))