Theorem List for Intuitionistic Logic Explorer - 9201-9300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | decmac 9201 |
Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed
multiplicand 𝑃 (with carry). (Contributed by Mario
Carneiro,
18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈
ℕ0
& ⊢ 𝑀 = ;𝐴𝐵
& ⊢ 𝑁 = ;𝐶𝐷
& ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐹 ∈
ℕ0
& ⊢ 𝐺 ∈ ℕ0 & ⊢ ((𝐴 · 𝑃) + (𝐶 + 𝐺)) = 𝐸
& ⊢ ((𝐵 · 𝑃) + 𝐷) = ;𝐺𝐹 ⇒ ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹 |
|
Theorem | decma2c 9202 |
Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed
multiplier 𝑃 (with carry). (Contributed by Mario
Carneiro,
18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈
ℕ0
& ⊢ 𝑀 = ;𝐴𝐵
& ⊢ 𝑁 = ;𝐶𝐷
& ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐹 ∈
ℕ0
& ⊢ 𝐺 ∈ ℕ0 & ⊢ ((𝑃 · 𝐴) + (𝐶 + 𝐺)) = 𝐸
& ⊢ ((𝑃 · 𝐵) + 𝐷) = ;𝐺𝐹 ⇒ ⊢ ((𝑃 · 𝑀) + 𝑁) = ;𝐸𝐹 |
|
Theorem | decadd 9203 |
Add two numerals 𝑀 and 𝑁 (no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈
ℕ0
& ⊢ 𝑀 = ;𝐴𝐵
& ⊢ 𝑁 = ;𝐶𝐷
& ⊢ (𝐴 + 𝐶) = 𝐸
& ⊢ (𝐵 + 𝐷) = 𝐹 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐸𝐹 |
|
Theorem | decaddc 9204 |
Add two numerals 𝑀 and 𝑁 (with carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈
ℕ0
& ⊢ 𝑀 = ;𝐴𝐵
& ⊢ 𝑁 = ;𝐶𝐷
& ⊢ ((𝐴 + 𝐶) + 1) = 𝐸
& ⊢ 𝐹 ∈ ℕ0 & ⊢ (𝐵 + 𝐷) = ;1𝐹 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐸𝐹 |
|
Theorem | decaddc2 9205 |
Add two numerals 𝑀 and 𝑁 (with carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈
ℕ0
& ⊢ 𝑀 = ;𝐴𝐵
& ⊢ 𝑁 = ;𝐶𝐷
& ⊢ ((𝐴 + 𝐶) + 1) = 𝐸
& ⊢ (𝐵 + 𝐷) = ;10 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐸0 |
|
Theorem | decrmanc 9206 |
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 9207 |
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 9208 |
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 9209 |
Add two numerals 𝑀 and 𝑁 (no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵
& ⊢ (𝐵 + 𝑁) = 𝐶 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐴𝐶 |
|
Theorem | decaddci 9210 |
Add two numerals 𝑀 and 𝑁 (no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵
& ⊢ (𝐴 + 1) = 𝐷
& ⊢ 𝐶 ∈ ℕ0 & ⊢ (𝐵 + 𝑁) = ;1𝐶 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐷𝐶 |
|
Theorem | decaddci2 9211 |
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 9212 |
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 9213 |
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 9214 |
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 9215 |
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 9216 |
The product of a numeral with a number (no carry). (Contributed by AV,
15-Jun-2021.)
|
⊢ 𝑁 ∈ ℕ0 & ⊢ 𝐴 ∈
ℕ0
& ⊢ 𝐵 ∈
ℕ0 ⇒ ⊢ (𝑁 · ;𝐴𝐵) = ;(𝑁 · 𝐴)(𝑁 · 𝐵) |
|
Theorem | 11multnc 9217 |
The product of 11 (as numeral) with a number (no carry). (Contributed
by AV, 15-Jun-2021.)
|
⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ (𝑁 · ;11) = ;𝑁𝑁 |
|
Theorem | decmul10add 9218 |
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 9219 |
Lemma for 6p5e11 9222 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐷 ∈
ℕ0
& ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐵 = (𝐷 + 1) & ⊢ 𝐶 = (𝐸 + 1) & ⊢ (𝐴 + 𝐷) = ;1𝐸 ⇒ ⊢ (𝐴 + 𝐵) = ;1𝐶 |
|
Theorem | 5p5e10 9220 |
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 9221 |
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 9222 |
6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (6 + 5) = ;11 |
|
Theorem | 6p6e12 9223 |
6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 + 6) = ;12 |
|
Theorem | 7p3e10 9224 |
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 9225 |
7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (7 + 4) = ;11 |
|
Theorem | 7p5e12 9226 |
7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 + 5) = ;12 |
|
Theorem | 7p6e13 9227 |
7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 + 6) = ;13 |
|
Theorem | 7p7e14 9228 |
7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 + 7) = ;14 |
|
Theorem | 8p2e10 9229 |
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 9230 |
8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (8 + 3) = ;11 |
|
Theorem | 8p4e12 9231 |
8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 4) = ;12 |
|
Theorem | 8p5e13 9232 |
8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 5) = ;13 |
|
Theorem | 8p6e14 9233 |
8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 6) = ;14 |
|
Theorem | 8p7e15 9234 |
8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 7) = ;15 |
|
Theorem | 8p8e16 9235 |
8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 8) = ;16 |
|
Theorem | 9p2e11 9236 |
9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (9 + 2) = ;11 |
|
Theorem | 9p3e12 9237 |
9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 3) = ;12 |
|
Theorem | 9p4e13 9238 |
9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 4) = ;13 |
|
Theorem | 9p5e14 9239 |
9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 5) = ;14 |
|
Theorem | 9p6e15 9240 |
9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 6) = ;15 |
|
Theorem | 9p7e16 9241 |
9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 7) = ;16 |
|
Theorem | 9p8e17 9242 |
9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 8) = ;17 |
|
Theorem | 9p9e18 9243 |
9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 9) = ;18 |
|
Theorem | 10p10e20 9244 |
10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (;10 + ;10) = ;20 |
|
Theorem | 10m1e9 9245 |
10 - 1 = 9. (Contributed by AV, 6-Sep-2021.)
|
⊢ (;10 − 1) = 9 |
|
Theorem | 4t3lem 9246 |
Lemma for 4t3e12 9247 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝐶 = (𝐵 + 1) & ⊢ (𝐴 · 𝐵) = 𝐷
& ⊢ (𝐷 + 𝐴) = 𝐸 ⇒ ⊢ (𝐴 · 𝐶) = 𝐸 |
|
Theorem | 4t3e12 9247 |
4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (4 · 3) = ;12 |
|
Theorem | 4t4e16 9248 |
4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (4 · 4) = ;16 |
|
Theorem | 5t2e10 9249 |
5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV,
4-Sep-2021.)
|
⊢ (5 · 2) = ;10 |
|
Theorem | 5t3e15 9250 |
5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 3) = ;15 |
|
Theorem | 5t4e20 9251 |
5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 4) = ;20 |
|
Theorem | 5t5e25 9252 |
5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 5) = ;25 |
|
Theorem | 6t2e12 9253 |
6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 2) = ;12 |
|
Theorem | 6t3e18 9254 |
6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 3) = ;18 |
|
Theorem | 6t4e24 9255 |
6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 4) = ;24 |
|
Theorem | 6t5e30 9256 |
6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (6 · 5) = ;30 |
|
Theorem | 6t6e36 9257 |
6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (6 · 6) = ;36 |
|
Theorem | 7t2e14 9258 |
7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 2) = ;14 |
|
Theorem | 7t3e21 9259 |
7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 3) = ;21 |
|
Theorem | 7t4e28 9260 |
7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 4) = ;28 |
|
Theorem | 7t5e35 9261 |
7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 5) = ;35 |
|
Theorem | 7t6e42 9262 |
7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 6) = ;42 |
|
Theorem | 7t7e49 9263 |
7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 7) = ;49 |
|
Theorem | 8t2e16 9264 |
8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 2) = ;16 |
|
Theorem | 8t3e24 9265 |
8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 3) = ;24 |
|
Theorem | 8t4e32 9266 |
8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 4) = ;32 |
|
Theorem | 8t5e40 9267 |
8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (8 · 5) = ;40 |
|
Theorem | 8t6e48 9268 |
8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (8 · 6) = ;48 |
|
Theorem | 8t7e56 9269 |
8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 7) = ;56 |
|
Theorem | 8t8e64 9270 |
8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 8) = ;64 |
|
Theorem | 9t2e18 9271 |
9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 2) = ;18 |
|
Theorem | 9t3e27 9272 |
9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 3) = ;27 |
|
Theorem | 9t4e36 9273 |
9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 4) = ;36 |
|
Theorem | 9t5e45 9274 |
9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 5) = ;45 |
|
Theorem | 9t6e54 9275 |
9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 6) = ;54 |
|
Theorem | 9t7e63 9276 |
9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 7) = ;63 |
|
Theorem | 9t8e72 9277 |
9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 8) = ;72 |
|
Theorem | 9t9e81 9278 |
9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 · 9) = ;81 |
|
Theorem | 9t11e99 9279 |
9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV,
6-Sep-2021.)
|
⊢ (9 · ;11) = ;99 |
|
Theorem | 9lt10 9280 |
9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
⊢ 9 < ;10 |
|
Theorem | 8lt10 9281 |
8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
⊢ 8 < ;10 |
|
Theorem | 7lt10 9282 |
7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 7 < ;10 |
|
Theorem | 6lt10 9283 |
6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 6 < ;10 |
|
Theorem | 5lt10 9284 |
5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 5 < ;10 |
|
Theorem | 4lt10 9285 |
4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 4 < ;10 |
|
Theorem | 3lt10 9286 |
3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 3 < ;10 |
|
Theorem | 2lt10 9287 |
2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
⊢ 2 < ;10 |
|
Theorem | 1lt10 9288 |
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 9289 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝐴 ∈
ℕ0 ⇒ ⊢ (4 · 𝐴) = (2 · (2 · 𝐴)) |
|
Theorem | decbin2 9290 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝐴 ∈
ℕ0 ⇒ ⊢ ((4 · 𝐴) + 2) = (2 · ((2 · 𝐴) + 1)) |
|
Theorem | decbin3 9291 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝐴 ∈
ℕ0 ⇒ ⊢ ((4 · 𝐴) + 3) = ((2 · ((2 · 𝐴) + 1)) + 1) |
|
Theorem | halfthird 9292 |
Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015.)
|
⊢ ((1 / 2) − (1 / 3)) = (1 /
6) |
|
Theorem | 5recm6rec 9293 |
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 9294 |
Extend class notation with the upper integer function.
Read "ℤ≥‘𝑀 " as "the set of integers
greater than or equal to
𝑀."
|
class ℤ≥ |
|
Definition | df-uz 9295* |
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 9296 for its
value, uzssz 9313 for its relationship to ℤ, nnuz 9329 and nn0uz 9328 for
its relationships to ℕ and ℕ0, and eluz1 9298 and eluz2 9300 for
its membership relations. (Contributed by NM, 5-Sep-2005.)
|
⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘}) |
|
Theorem | uzval 9296* |
The value of the upper integers function. (Contributed by NM,
5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ (𝑁 ∈ ℤ →
(ℤ≥‘𝑁) = {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘}) |
|
Theorem | uzf 9297 |
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 9298 |
Membership in the upper set of integers starting at 𝑀.
(Contributed by NM, 5-Sep-2005.)
|
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) |
|
Theorem | eluzel2 9299 |
Implication of membership in an upper set of integers. (Contributed by
NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
|
Theorem | eluz2 9300 |
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.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |