P. 96 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9501-9600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	decadd 9501	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 9502	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 9503	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 9504	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 9505	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 9506	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 9507	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ (𝐵 + 𝑁) = 𝐶    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐴𝐶
Theorem	decaddci 9508	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ (𝐴 + 1) = 𝐷    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ (𝐵 + 𝑁) = ;1𝐶    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐷𝐶
Theorem	decaddci2 9509	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 9510	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 9511	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 9512	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 9513	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 9514	The product of a numeral with a number (no carry). (Contributed by AV, 15-Jun-2021.)
⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    ⇒   ⊢ (𝑁 · ;𝐴𝐵) = ;(𝑁 · 𝐴)(𝑁 · 𝐵)
Theorem	11multnc 9515	The product of 11 (as numeral) with a number (no carry). (Contributed by AV, 15-Jun-2021.)
⊢ 𝑁 ∈ ℕ0    ⇒   ⊢ (𝑁 · ;11) = ;𝑁𝑁
Theorem	decmul10add 9516	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 9517	Lemma for 6p5e11 9520 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐵 = (𝐷 + 1)    &   ⊢ 𝐶 = (𝐸 + 1)    &   ⊢ (𝐴 + 𝐷) = ;1𝐸    ⇒   ⊢ (𝐴 + 𝐵) = ;1𝐶
Theorem	5p5e10 9518	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 9519	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 9520	6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (6 + 5) = ;11
Theorem	6p6e12 9521	6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 + 6) = ;12
Theorem	7p3e10 9522	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 9523	7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (7 + 4) = ;11
Theorem	7p5e12 9524	7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 5) = ;12
Theorem	7p6e13 9525	7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 6) = ;13
Theorem	7p7e14 9526	7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 7) = ;14
Theorem	8p2e10 9527	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 9528	8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (8 + 3) = ;11
Theorem	8p4e12 9529	8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 4) = ;12
Theorem	8p5e13 9530	8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 5) = ;13
Theorem	8p6e14 9531	8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 6) = ;14
Theorem	8p7e15 9532	8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 7) = ;15
Theorem	8p8e16 9533	8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 8) = ;16
Theorem	9p2e11 9534	9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (9 + 2) = ;11
Theorem	9p3e12 9535	9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 3) = ;12
Theorem	9p4e13 9536	9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 4) = ;13
Theorem	9p5e14 9537	9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 5) = ;14
Theorem	9p6e15 9538	9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 6) = ;15
Theorem	9p7e16 9539	9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 7) = ;16
Theorem	9p8e17 9540	9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 8) = ;17
Theorem	9p9e18 9541	9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 9) = ;18
Theorem	10p10e20 9542	10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (;10 + ;10) = ;20
Theorem	10m1e9 9543	10 - 1 = 9. (Contributed by AV, 6-Sep-2021.)
⊢ (;10 − 1) = 9
Theorem	4t3lem 9544	Lemma for 4t3e12 9545 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 = (𝐵 + 1)    &   ⊢ (𝐴 · 𝐵) = 𝐷    &   ⊢ (𝐷 + 𝐴) = 𝐸    ⇒   ⊢ (𝐴 · 𝐶) = 𝐸
Theorem	4t3e12 9545	4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (4 · 3) = ;12
Theorem	4t4e16 9546	4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (4 · 4) = ;16
Theorem	5t2e10 9547	5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 4-Sep-2021.)
⊢ (5 · 2) = ;10
Theorem	5t3e15 9548	5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (5 · 3) = ;15
Theorem	5t4e20 9549	5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (5 · 4) = ;20
Theorem	5t5e25 9550	5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (5 · 5) = ;25
Theorem	6t2e12 9551	6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 2) = ;12
Theorem	6t3e18 9552	6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 3) = ;18
Theorem	6t4e24 9553	6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 4) = ;24
Theorem	6t5e30 9554	6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (6 · 5) = ;30
Theorem	6t6e36 9555	6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (6 · 6) = ;36
Theorem	7t2e14 9556	7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 2) = ;14
Theorem	7t3e21 9557	7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 3) = ;21
Theorem	7t4e28 9558	7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 4) = ;28
Theorem	7t5e35 9559	7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 5) = ;35
Theorem	7t6e42 9560	7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 6) = ;42
Theorem	7t7e49 9561	7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 7) = ;49
Theorem	8t2e16 9562	8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 2) = ;16
Theorem	8t3e24 9563	8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 3) = ;24
Theorem	8t4e32 9564	8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 4) = ;32
Theorem	8t5e40 9565	8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (8 · 5) = ;40
Theorem	8t6e48 9566	8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (8 · 6) = ;48
Theorem	8t7e56 9567	8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 7) = ;56
Theorem	8t8e64 9568	8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 8) = ;64
Theorem	9t2e18 9569	9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 2) = ;18
Theorem	9t3e27 9570	9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 3) = ;27
Theorem	9t4e36 9571	9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 4) = ;36
Theorem	9t5e45 9572	9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 5) = ;45
Theorem	9t6e54 9573	9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 6) = ;54
Theorem	9t7e63 9574	9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 7) = ;63
Theorem	9t8e72 9575	9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 8) = ;72
Theorem	9t9e81 9576	9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 9) = ;81
Theorem	9t11e99 9577	9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.)
⊢ (9 · ;11) = ;99
Theorem	9lt10 9578	9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 9 < ;10
Theorem	8lt10 9579	8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 8 < ;10
Theorem	7lt10 9580	7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 7 < ;10
Theorem	6lt10 9581	6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 6 < ;10
Theorem	5lt10 9582	5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 5 < ;10
Theorem	4lt10 9583	4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 4 < ;10
Theorem	3lt10 9584	3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 3 < ;10
Theorem	2lt10 9585	2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 2 < ;10
Theorem	1lt10 9586	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 9587	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (4 · 𝐴) = (2 · (2 · 𝐴))
Theorem	decbin2 9588	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((4 · 𝐴) + 2) = (2 · ((2 · 𝐴) + 1))
Theorem	decbin3 9589	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((4 · 𝐴) + 3) = ((2 · ((2 · 𝐴) + 1)) + 1)
Theorem	halfthird 9590	Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015.)
⊢ ((1 / 2) − (1 / 3)) = (1 / 6)
Theorem	5recm6rec 9591	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 9592	Extend class notation with the upper integer function. Read "ℤ≥‘𝑀 " as "the set of integers greater than or equal to 𝑀".
class ℤ≥
Definition	df-uz 9593*	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 9594 for its value, uzssz 9612 for its relationship to ℤ, nnuz 9628 and nn0uz 9627 for its relationships to ℕ and ℕ0, and eluz1 9596 and eluz2 9598 for its membership relations. (Contributed by NM, 5-Sep-2005.)
⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘})
Theorem	uzval 9594*	The value of the upper integers function. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝑁 ∈ ℤ → (ℤ≥‘𝑁) = {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘})
Theorem	uzf 9595	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 9596	Membership in the upper set of integers starting at 𝑀. (Contributed by NM, 5-Sep-2005.)
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
Theorem	eluzel2 9597	Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
Theorem	eluz2 9598	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 9599	Membership in an upper set of integers. (Contributed by NM, 5-Sep-2005.)
⊢ 𝑀 ∈ ℤ    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
Theorem	eluzuzle 9600	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.)
⊢ ((𝐵 ∈ ℤ ∧ 𝐵 ≤ 𝐴) → (𝐶 ∈ (ℤ≥‘𝐴) → 𝐶 ∈ (ℤ≥‘𝐵)))