Theorem List for Intuitionistic Logic Explorer - 9201-9300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | decaddci2 9201 |
Add two numerals and
(no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
;
;
; |
|
Theorem | decsubi 9202 |
Difference between a numeral and a nonnegative integer (no
underflow). (Contributed by AV, 22-Jul-2021.) (Revised by AV,
6-Sep-2021.)
|
;
; |
|
Theorem | decmul1 9203 |
The product of a numeral with a number (no carry). (Contributed by
AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.)
|
;
; |
|
Theorem | decmul1c 9204 |
The product of a numeral with a number (with carry). (Contributed by
Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
;
;
; |
|
Theorem | decmul2c 9205 |
The product of a numeral with a number (with carry). (Contributed by
Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
;
;
; |
|
Theorem | decmulnc 9206 |
The product of a numeral with a number (no carry). (Contributed by AV,
15-Jun-2021.)
|
; ; |
|
Theorem | 11multnc 9207 |
The product of 11 (as numeral) with a number (no carry). (Contributed
by AV, 15-Jun-2021.)
|
; ; |
|
Theorem | decmul10add 9208 |
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.)
|
; ; |
|
Theorem | 6p5lem 9209 |
Lemma for 6p5e11 9212 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
;
; |
|
Theorem | 5p5e10 9210 |
5 + 5 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 6p4e10 9211 |
6 + 4 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 6p5e11 9212 |
6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
; |
|
Theorem | 6p6e12 9213 |
6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7p3e10 9214 |
7 + 3 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 7p4e11 9215 |
7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
; |
|
Theorem | 7p5e12 9216 |
7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7p6e13 9217 |
7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7p7e14 9218 |
7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8p2e10 9219 |
8 + 2 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 8p3e11 9220 |
8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
; |
|
Theorem | 8p4e12 9221 |
8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8p5e13 9222 |
8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8p6e14 9223 |
8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8p7e15 9224 |
8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8p8e16 9225 |
8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p2e11 9226 |
9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
; |
|
Theorem | 9p3e12 9227 |
9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p4e13 9228 |
9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p5e14 9229 |
9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p6e15 9230 |
9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p7e16 9231 |
9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p8e17 9232 |
9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p9e18 9233 |
9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 10p10e20 9234 |
10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
; ; ; |
|
Theorem | 10m1e9 9235 |
10 - 1 = 9. (Contributed by AV, 6-Sep-2021.)
|
; |
|
Theorem | 4t3lem 9236 |
Lemma for 4t3e12 9237 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
|
|
Theorem | 4t3e12 9237 |
4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 4t4e16 9238 |
4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 5t2e10 9239 |
5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV,
4-Sep-2021.)
|
; |
|
Theorem | 5t3e15 9240 |
5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 5t4e20 9241 |
5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 5t5e25 9242 |
5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 6t2e12 9243 |
6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 6t3e18 9244 |
6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 6t4e24 9245 |
6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 6t5e30 9246 |
6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 6t6e36 9247 |
6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 7t2e14 9248 |
7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7t3e21 9249 |
7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7t4e28 9250 |
7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7t5e35 9251 |
7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7t6e42 9252 |
7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7t7e49 9253 |
7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8t2e16 9254 |
8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8t3e24 9255 |
8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8t4e32 9256 |
8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8t5e40 9257 |
8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 8t6e48 9258 |
8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 8t7e56 9259 |
8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8t8e64 9260 |
8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t2e18 9261 |
9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t3e27 9262 |
9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t4e36 9263 |
9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t5e45 9264 |
9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t6e54 9265 |
9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t7e63 9266 |
9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t8e72 9267 |
9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t9e81 9268 |
9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t11e99 9269 |
9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV,
6-Sep-2021.)
|
; ; |
|
Theorem | 9lt10 9270 |
9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
; |
|
Theorem | 8lt10 9271 |
8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
; |
|
Theorem | 7lt10 9272 |
7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 6lt10 9273 |
6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 5lt10 9274 |
5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 4lt10 9275 |
4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 3lt10 9276 |
3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 2lt10 9277 |
2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 1lt10 9278 |
1 is less than 10. (Contributed by NM, 7-Nov-2012.) (Revised by Mario
Carneiro, 9-Mar-2015.) (Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | decbin0 9279 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | decbin2 9280 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | decbin3 9281 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
4.4.11 Upper sets of integers
|
|
Syntax | cuz 9282 |
Extend class notation with the upper integer function.
Read " " as "the
set of integers greater than or equal to
."
|
|
|
Definition | df-uz 9283* |
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 9284 for its
value, uzssz 9301 for its relationship to , nnuz 9317
and nn0uz 9316 for
its relationships to and , and eluz1 9286 and eluz2 9288 for
its membership relations. (Contributed by NM, 5-Sep-2005.)
|
|
|
Theorem | uzval 9284* |
The value of the upper integers function. (Contributed by NM,
5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | uzf 9285 |
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 9286 |
Membership in the upper set of integers starting at .
(Contributed by NM, 5-Sep-2005.)
|
|
|
Theorem | eluzel2 9287 |
Implication of membership in an upper set of integers. (Contributed by
NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | eluz2 9288 |
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 9289 |
Membership in an upper set of integers. (Contributed by NM,
5-Sep-2005.)
|
|
|
Theorem | eluzuzle 9290 |
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 9291 |
A member of an upper set of integers is an integer. (Contributed by NM,
6-Sep-2005.)
|
|
|
Theorem | eluzelre 9292 |
A member of an upper set of integers is a real. (Contributed by Mario
Carneiro, 31-Aug-2013.)
|
|
|
Theorem | eluzelcn 9293 |
A member of an upper set of integers is a complex number. (Contributed by
Glauco Siliprandi, 29-Jun-2017.)
|
|
|
Theorem | eluzle 9294 |
Implication of membership in an upper set of integers. (Contributed by
NM, 6-Sep-2005.)
|
|
|
Theorem | eluz 9295 |
Membership in an upper set of integers. (Contributed by NM,
2-Oct-2005.)
|
|
|
Theorem | uzid 9296 |
Membership of the least member in an upper set of integers. (Contributed
by NM, 2-Sep-2005.)
|
|
|
Theorem | uzn0 9297 |
The upper integers are all nonempty. (Contributed by Mario Carneiro,
16-Jan-2014.)
|
|
|
Theorem | uztrn 9298 |
Transitive law for sets of upper integers. (Contributed by NM,
20-Sep-2005.)
|
|
|
Theorem | uztrn2 9299 |
Transitive law for sets of upper integers. (Contributed by Mario
Carneiro, 26-Dec-2013.)
|
|
|
Theorem | uzneg 9300 |
Contraposition law for upper integers. (Contributed by NM,
28-Nov-2005.)
|
|