P. 99 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9801-9900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	9p8e17 9801	9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 + 8 ) = ; 1 7
Theorem	9p9e18 9802	9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 + 9 ) = ; 1 8
Theorem	10p10e20 9803	10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- (; 1 0 + ; 1 0 ) = ; 2 0
Theorem	10m1e9 9804	10 - 1 = 9. (Contributed by AV, 6-Sep-2021.)
|- (; 1 0 - 1 ) = 9
Theorem	4t3lem 9805	Lemma for 4t3e12 9806 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN0   &    |- B e. NN0   &    |- C = ( B + 1 )   &    |- ( A x. B ) = D   &    |- ( D + A ) = E   =>    |- ( A x. C ) = E
Theorem	4t3e12 9806	4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 4 x. 3 ) = ; 1 2
Theorem	4t4e16 9807	4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 4 x. 4 ) = ; 1 6
Theorem	5t2e10 9808	5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 4-Sep-2021.)
|- ( 5 x. 2 ) = ; 1 0
Theorem	5t3e15 9809	5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 5 x. 3 ) = ; 1 5
Theorem	5t4e20 9810	5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 5 x. 4 ) = ; 2 0
Theorem	5t5e25 9811	5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 5 x. 5 ) = ; 2 5
Theorem	6t2e12 9812	6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 6 x. 2 ) = ; 1 2
Theorem	6t3e18 9813	6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 6 x. 3 ) = ; 1 8
Theorem	6t4e24 9814	6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 6 x. 4 ) = ; 2 4
Theorem	6t5e30 9815	6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 6 x. 5 ) = ; 3 0
Theorem	6t6e36 9816	6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 6 x. 6 ) = ; 3 6
Theorem	7t2e14 9817	7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 x. 2 ) = ; 1 4
Theorem	7t3e21 9818	7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 x. 3 ) = ; 2 1
Theorem	7t4e28 9819	7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 x. 4 ) = ; 2 8
Theorem	7t5e35 9820	7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 x. 5 ) = ; 3 5
Theorem	7t6e42 9821	7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 x. 6 ) = ; 4 2
Theorem	7t7e49 9822	7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 x. 7 ) = ; 4 9
Theorem	8t2e16 9823	8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 x. 2 ) = ; 1 6
Theorem	8t3e24 9824	8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 x. 3 ) = ; 2 4
Theorem	8t4e32 9825	8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 x. 4 ) = ; 3 2
Theorem	8t5e40 9826	8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 8 x. 5 ) = ; 4 0
Theorem	8t6e48 9827	8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 8 x. 6 ) = ; 4 8
Theorem	8t7e56 9828	8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 x. 7 ) = ; 5 6
Theorem	8t8e64 9829	8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 x. 8 ) = ; 6 4
Theorem	9t2e18 9830	9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 x. 2 ) = ; 1 8
Theorem	9t3e27 9831	9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 x. 3 ) = ; 2 7
Theorem	9t4e36 9832	9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 x. 4 ) = ; 3 6
Theorem	9t5e45 9833	9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 x. 5 ) = ; 4 5
Theorem	9t6e54 9834	9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 x. 6 ) = ; 5 4
Theorem	9t7e63 9835	9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 x. 7 ) = ; 6 3
Theorem	9t8e72 9836	9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 x. 8 ) = ; 7 2
Theorem	9t9e81 9837	9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 x. 9 ) = ; 8 1
Theorem	9t11e99 9838	9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.)
|- ( 9 x. ; 1 1 ) = ; 9 9
Theorem	9lt10 9839	9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.)
|- 9 < ; 1 0
Theorem	8lt10 9840	8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.)
|- 8 < ; 1 0
Theorem	7lt10 9841	7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
|- 7 < ; 1 0
Theorem	6lt10 9842	6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
|- 6 < ; 1 0
Theorem	5lt10 9843	5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
|- 5 < ; 1 0
Theorem	4lt10 9844	4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
|- 4 < ; 1 0
Theorem	3lt10 9845	3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
|- 3 < ; 1 0
Theorem	2lt10 9846	2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
|- 2 < ; 1 0
Theorem	1lt10 9847	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 < ; 1 0
Theorem	decbin0 9848	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- A e. NN0   =>    |- ( 4 x. A ) = ( 2 x. ( 2 x. A ) )
Theorem	decbin2 9849	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- A e. NN0   =>    |- ( ( 4 x. A ) + 2 ) = ( 2 x. ( ( 2 x. A ) + 1 ) )
Theorem	decbin3 9850	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- A e. NN0   =>    |- ( ( 4 x. A ) + 3 ) = ( ( 2 x. ( ( 2 x. A ) + 1 ) ) + 1 )
Theorem	halfthird 9851	Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015.)
|- ( ( 1 / 2 ) - ( 1 / 3 ) ) = ( 1 / 6 )
Theorem	5recm6rec 9852	One fifth minus one sixth. (Contributed by Scott Fenton, 9-Jan-2017.)
|- ( ( 1 / 5 ) - ( 1 / 6 ) ) = ( 1 / ; 3 0 )
4.4.11  Upper sets of integers
Syntax	cuz 9853	Extend class notation with the upper integer function. Read " ZZ>= ` M " as "the set of integers greater than or equal to M".
class ZZ>=
Definition	df-uz 9854*	Define a function whose value at j is the semi-infinite set of contiguous integers starting at j, which we will also call the upper integers starting at j. Read " ZZ>= ` M " as "the set of integers greater than or equal to M". See uzval 9855 for its value, uzssz 9874 for its relationship to ZZ, nnuz 9890 and nn0uz 9889 for its relationships to NN and NN0, and eluz1 9857 and eluz2 9859 for its membership relations. (Contributed by NM, 5-Sep-2005.)
|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
Theorem	uzval 9855*	The value of the upper integers function. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( N e. ZZ -> ( ZZ>= ` N ) = { k e. ZZ | N <_ k } )
Theorem	uzf 9856	The domain and codomain of the upper integers function. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ZZ>= : ZZ --> ~P ZZ
Theorem	eluz1 9857	Membership in the upper set of integers starting at M. (Contributed by NM, 5-Sep-2005.)
|- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( N e. ZZ /\ M <_ N ) ) )
Theorem	eluzel2 9858	Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
Theorem	eluz2 9859	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 M e. ZZ. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
Theorem	eluzmn 9860	Membership in an earlier upper set of integers. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- ( ( M e. ZZ /\ N e. NN0 ) -> M e. ( ZZ>= ` ( M - N ) ) )
Theorem	eluz1i 9861	Membership in an upper set of integers. (Contributed by NM, 5-Sep-2005.)
|- M e. ZZ   =>    |- ( N e. ( ZZ>= ` M ) <-> ( N e. ZZ /\ M <_ N ) )
Theorem	eluzuzle 9862	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.)
|- ( ( B e. ZZ /\ B <_ A ) -> ( C e. ( ZZ>= ` A ) -> C e. ( ZZ>= ` B ) ) )
Theorem	eluzelz 9863	A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.)
|- ( N e. ( ZZ>= ` M ) -> N e. ZZ )
Theorem	eluzelre 9864	A member of an upper set of integers is a real. (Contributed by Mario Carneiro, 31-Aug-2013.)
|- ( N e. ( ZZ>= ` M ) -> N e. RR )
Theorem	eluzelcn 9865	A member of an upper set of integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- ( N e. ( ZZ>= ` M ) -> N e. CC )
Theorem	eluzle 9866	Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.)
|- ( N e. ( ZZ>= ` M ) -> M <_ N )
Theorem	eluz 9867	Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` M ) <-> M <_ N ) )
Theorem	uzid 9868	Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.)
|- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
Theorem	uzidd 9869	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   =>    |- ( ph -> M e. ( ZZ>= ` M ) )
Theorem	uzn0 9870	The upper integers are all nonempty. (Contributed by Mario Carneiro, 16-Jan-2014.)
|- ( M e. ran ZZ>= -> M =/= (/) )
Theorem	uztrn 9871	Transitive law for sets of upper integers. (Contributed by NM, 20-Sep-2005.)
|- ( ( M e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` N ) ) -> M e. ( ZZ>= ` N ) )
Theorem	uztrn2 9872	Transitive law for sets of upper integers. (Contributed by Mario Carneiro, 26-Dec-2013.)
|- Z = ( ZZ>= ` K )   =>    |- ( ( N e. Z /\ M e. ( ZZ>= ` N ) ) -> M e. Z )
Theorem	uzneg 9873	Contraposition law for upper integers. (Contributed by NM, 28-Nov-2005.)
|- ( N e. ( ZZ>= ` M ) -> -u M e. ( ZZ>= ` -u N ) )
Theorem	uzssz 9874	An upper set of integers is a subset of all integers. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ZZ>= ` M ) C_ ZZ
Theorem	uzss 9875	Subset relationship for two sets of upper integers. (Contributed by NM, 5-Sep-2005.)
|- ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
Theorem	uztric 9876	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.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` M ) \/ M e. ( ZZ>= ` N ) ) )
Theorem	uz11 9877	The upper integers function is one-to-one. (Contributed by NM, 12-Dec-2005.)
|- ( M e. ZZ -> ( ( ZZ>= ` M ) = ( ZZ>= ` N ) <-> M = N ) )
Theorem	eluzp1m1 9878	Membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.)
|- ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )
Theorem	eluzp1l 9879	Strict ordering implied by membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.)
|- ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> M < N )
Theorem	eluzp1p1 9880	Membership in the next upper set of integers. (Contributed by NM, 5-Oct-2005.)
|- ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
Theorem	eluzaddi 9881	Membership in a later upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.)
|- M e. ZZ   &    |- K e. ZZ   =>    |- ( N e. ( ZZ>= ` M ) -> ( N + K ) e. ( ZZ>= ` ( M + K ) ) )
Theorem	eluzsubi 9882	Membership in an earlier upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.)
|- M e. ZZ   &    |- K e. ZZ   =>    |- ( N e. ( ZZ>= ` ( M + K ) ) -> ( N - K ) e. ( ZZ>= ` M ) )
Theorem	eluzadd 9883	Membership in a later upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) -> ( N + K ) e. ( ZZ>= ` ( M + K ) ) )
Theorem	eluzsub 9884	Membership in an earlier upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( M e. ZZ /\ K e. ZZ /\ N e. ( ZZ>= ` ( M + K ) ) ) -> ( N - K ) e. ( ZZ>= ` M ) )
Theorem	uzm1 9885	Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( N e. ( ZZ>= ` M ) -> ( N = M \/ ( N - 1 ) e. ( ZZ>= ` M ) ) )
Theorem	uznn0sub 9886	The nonnegative difference of integers is a nonnegative integer. (Contributed by NM, 4-Sep-2005.)
|- ( N e. ( ZZ>= ` M ) -> ( N - M ) e. NN0 )
Theorem	uzin 9887	Intersection of two upper intervals of integers. (Contributed by Mario Carneiro, 24-Dec-2013.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ZZ>= ` M ) i^i ( ZZ>= ` N ) ) = ( ZZ>= ` if ( M <_ N , N , M ) ) )
Theorem	uzp1 9888	Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( N e. ( ZZ>= ` M ) -> ( N = M \/ N e. ( ZZ>= ` ( M + 1 ) ) ) )
Theorem	nn0uz 9889	Nonnegative integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)
|- NN0 = ( ZZ>= ` 0 )
Theorem	nnuz 9890	Positive integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)
|- NN = ( ZZ>= ` 1 )
Theorem	elnnuz 9891	A positive integer expressed as a member of an upper set of integers. (Contributed by NM, 6-Jun-2006.)
|- ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
Theorem	elnn0uz 9892	A nonnegative integer expressed as a member an upper set of integers. (Contributed by NM, 6-Jun-2006.)
|- ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
Theorem	5eluz3 9893	5 is an integer greater than or equal to 3. (Contributed by AV, 7-Sep-2025.)
|- 5 e. ( ZZ>= ` 3 )
Theorem	uzuzle23 9894	An integer in the upper set of integers starting at 3 is element of the upper set of integers starting at 2. (Contributed by Alexander van der Vekens, 17-Sep-2018.)
|- ( A e. ( ZZ>= ` 3 ) -> A e. ( ZZ>= ` 2 ) )
Theorem	uzuzle24 9895	An integer greater than or equal to 4 is an integer greater than or equal to 2. (Contributed by AV, 30-May-2023.)
|- ( X e. ( ZZ>= ` 4 ) -> X e. ( ZZ>= ` 2 ) )
Theorem	uzuzle34 9896	An integer greater than or equal to 4 is an integer greater than or equal to 3. (Contributed by AV, 5-Sep-2025.)
|- ( X e. ( ZZ>= ` 4 ) -> X e. ( ZZ>= ` 3 ) )
Theorem	uzuzle35 9897	An integer greater than or equal to 5 is an integer greater than or equal to 3. (Contributed by AV, 15-Nov-2025.)
|- ( A e. ( ZZ>= ` 5 ) -> A e. ( ZZ>= ` 3 ) )
Theorem	eluz2nn 9898	An integer is greater than or equal to 2 is a positive integer. (Contributed by AV, 3-Nov-2018.)
|- ( A e. ( ZZ>= ` 2 ) -> A e. NN )
Theorem	eluz3nn 9899	An integer greater than or equal to 3 is a positive integer. (Contributed by Alexander van der Vekens, 17-Sep-2018.) (Proof shortened by AV, 30-Nov-2025.)
|- ( N e. ( ZZ>= ` 3 ) -> N e. NN )
Theorem	eluz4eluz2 9900	An integer greater than or equal to 4 is an integer greater than or equal to 2. (Contributed by AV, 30-May-2023.)
|- ( X e. ( ZZ>= ` 4 ) -> X e. ( ZZ>= ` 2 ) )