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.)
|
⊢ 𝑀 ∈ ℤ & ⊢ 𝐾 ∈
ℤ ⇒ ⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 𝐾)) → (𝑁 − 𝐾) ∈
(ℤ≥‘𝑀)) |