P. 92 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9101-9200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnne0d 9101	A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A =/= 0 )
Theorem	nnap0d 9102	A positive integer is apart from zero. (Contributed by Jim Kingdon, 25-Aug-2021.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A # 0 )
Theorem	nnrecred 9103	The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> ( 1 / A ) e. RR )
Theorem	nnaddcld 9104	Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   =>    |- ( ph -> ( A + B ) e. NN )
Theorem	nnmulcld 9105	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   =>    |- ( ph -> ( A x. B ) e. NN )
Theorem	nndivred 9106	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. NN )   =>    |- ( ph -> ( A / B ) e. RR )
4.4.3  Decimal representation of numbers The decimal representation of numbers/integers is based on the decimal digits 0 through 9 (df-0 7952 through df-9 9122), which are explicitly defined in the following. Note that the numbers 0 and 1 are constants defined as primitives of the complex number axiom system (see df-0 7952 and df-1 7953). Integers can also be exhibited as sums of powers of 10 (e.g., the number 103 can be expressed as ( (; 1 0 ^ 2 ) + 3 )) or as some other expression built from operations on the numbers 0 through 9. For example, the prime number 823541 can be expressed as ( 7 ^ 7 ) - 2. Most abstract math rarely requires numbers larger than 4. Even in Wiles' proof of Fermat's Last Theorem, the largest number used appears to be 12.
Syntax	c2 9107	Extend class notation to include the number 2.
class 2
Syntax	c3 9108	Extend class notation to include the number 3.
class 3
Syntax	c4 9109	Extend class notation to include the number 4.
class 4
Syntax	c5 9110	Extend class notation to include the number 5.
class 5
Syntax	c6 9111	Extend class notation to include the number 6.
class 6
Syntax	c7 9112	Extend class notation to include the number 7.
class 7
Syntax	c8 9113	Extend class notation to include the number 8.
class 8
Syntax	c9 9114	Extend class notation to include the number 9.
class 9
Definition	df-2 9115	Define the number 2. (Contributed by NM, 27-May-1999.)
|- 2 = ( 1 + 1 )
Definition	df-3 9116	Define the number 3. (Contributed by NM, 27-May-1999.)
|- 3 = ( 2 + 1 )
Definition	df-4 9117	Define the number 4. (Contributed by NM, 27-May-1999.)
|- 4 = ( 3 + 1 )
Definition	df-5 9118	Define the number 5. (Contributed by NM, 27-May-1999.)
|- 5 = ( 4 + 1 )
Definition	df-6 9119	Define the number 6. (Contributed by NM, 27-May-1999.)
|- 6 = ( 5 + 1 )
Definition	df-7 9120	Define the number 7. (Contributed by NM, 27-May-1999.)
|- 7 = ( 6 + 1 )
Definition	df-8 9121	Define the number 8. (Contributed by NM, 27-May-1999.)
|- 8 = ( 7 + 1 )
Definition	df-9 9122	Define the number 9. (Contributed by NM, 27-May-1999.)
|- 9 = ( 8 + 1 )
Theorem	0ne1 9123	0 =/= 1 (common case). See aso 1ap0 8683. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 =/= 1
Theorem	1ne0 9124	1 =/= 0. See aso 1ap0 8683. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 1 =/= 0
Theorem	1m1e0 9125	( 1 - 1 ) = 0 (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- ( 1 - 1 ) = 0
Theorem	2re 9126	The number 2 is real. (Contributed by NM, 27-May-1999.)
|- 2 e. RR
Theorem	2cn 9127	The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)
|- 2 e. CC
Theorem	2ex 9128	2 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 2 e. _V
Theorem	2cnd 9129	2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ph -> 2 e. CC )
Theorem	3re 9130	The number 3 is real. (Contributed by NM, 27-May-1999.)
|- 3 e. RR
Theorem	3cn 9131	The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)
|- 3 e. CC
Theorem	3ex 9132	3 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 3 e. _V
Theorem	4re 9133	The number 4 is real. (Contributed by NM, 27-May-1999.)
|- 4 e. RR
Theorem	4cn 9134	The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 4 e. CC
Theorem	5re 9135	The number 5 is real. (Contributed by NM, 27-May-1999.)
|- 5 e. RR
Theorem	5cn 9136	The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 5 e. CC
Theorem	6re 9137	The number 6 is real. (Contributed by NM, 27-May-1999.)
|- 6 e. RR
Theorem	6cn 9138	The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 6 e. CC
Theorem	7re 9139	The number 7 is real. (Contributed by NM, 27-May-1999.)
|- 7 e. RR
Theorem	7cn 9140	The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 7 e. CC
Theorem	8re 9141	The number 8 is real. (Contributed by NM, 27-May-1999.)
|- 8 e. RR
Theorem	8cn 9142	The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 8 e. CC
Theorem	9re 9143	The number 9 is real. (Contributed by NM, 27-May-1999.)
|- 9 e. RR
Theorem	9cn 9144	The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 9 e. CC
Theorem	0le0 9145	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 0 <_ 0
Theorem	0le2 9146	0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.)
|- 0 <_ 2
Theorem	2pos 9147	The number 2 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 2
Theorem	2ne0 9148	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
|- 2 =/= 0
Theorem	2ap0 9149	The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 2 # 0
Theorem	3pos 9150	The number 3 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 3
Theorem	3ne0 9151	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- 3 =/= 0
Theorem	3ap0 9152	The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- 3 # 0
Theorem	4pos 9153	The number 4 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 4
Theorem	4ne0 9154	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
|- 4 =/= 0
Theorem	4ap0 9155	The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- 4 # 0
Theorem	5pos 9156	The number 5 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 5
Theorem	6pos 9157	The number 6 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 6
Theorem	7pos 9158	The number 7 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 7
Theorem	8pos 9159	The number 8 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 8
Theorem	9pos 9160	The number 9 is positive. (Contributed by NM, 27-May-1999.)
|- 0 < 9
4.4.4  Some properties of specific numbers This includes adding two pairs of values 1..10 (where the right is less than the left) and where the left is less than the right for the values 1..10.
Theorem	neg1cn 9161	-1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- -u 1 e. CC
Theorem	neg1rr 9162	-1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
|- -u 1 e. RR
Theorem	neg1ne0 9163	-1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u 1 =/= 0
Theorem	neg1lt0 9164	-1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u 1 < 0
Theorem	neg1ap0 9165	-1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
|- -u 1 # 0
Theorem	negneg1e1 9166	-u -u 1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u -u 1 = 1
Theorem	1pneg1e0 9167	1 + -u 1 is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 + -u 1 ) = 0
Theorem	0m0e0 9168	0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 0 - 0 ) = 0
Theorem	1m0e1 9169	1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 - 0 ) = 1
Theorem	0p1e1 9170	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- ( 0 + 1 ) = 1
Theorem	fv0p1e1 9171	Function value at N + 1 with N replaced by 0. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.)
|- ( N = 0 -> ( F ` ( N + 1 ) ) = ( F ` 1 ) )
Theorem	1p0e1 9172	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 + 0 ) = 1
Theorem	1p1e2 9173	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
|- ( 1 + 1 ) = 2
Theorem	2m1e1 9174	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 9202. (Contributed by David A. Wheeler, 4-Jan-2017.)
|- ( 2 - 1 ) = 1
Theorem	1e2m1 9175	1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 1 = ( 2 - 1 )
Theorem	3m1e2 9176	3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.)
|- ( 3 - 1 ) = 2
Theorem	4m1e3 9177	4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.)
|- ( 4 - 1 ) = 3
Theorem	5m1e4 9178	5 - 1 = 4. (Contributed by AV, 6-Sep-2021.)
|- ( 5 - 1 ) = 4
Theorem	6m1e5 9179	6 - 1 = 5. (Contributed by AV, 6-Sep-2021.)
|- ( 6 - 1 ) = 5
Theorem	7m1e6 9180	7 - 1 = 6. (Contributed by AV, 6-Sep-2021.)
|- ( 7 - 1 ) = 6
Theorem	8m1e7 9181	8 - 1 = 7. (Contributed by AV, 6-Sep-2021.)
|- ( 8 - 1 ) = 7
Theorem	9m1e8 9182	9 - 1 = 8. (Contributed by AV, 6-Sep-2021.)
|- ( 9 - 1 ) = 8
Theorem	2p2e4 9183	Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page: https://us.metamath.org/mpeuni/mmset.html#trivia. (Contributed by NM, 27-May-1999.)
|- ( 2 + 2 ) = 4
Theorem	2times 9184	Two times a number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) (Proof shortened by AV, 26-Feb-2020.)
|- ( A e. CC -> ( 2 x. A ) = ( A + A ) )
Theorem	times2 9185	A number times 2. (Contributed by NM, 16-Oct-2007.)
|- ( A e. CC -> ( A x. 2 ) = ( A + A ) )
Theorem	2timesi 9186	Two times a number. (Contributed by NM, 1-Aug-1999.)
|- A e. CC   =>    |- ( 2 x. A ) = ( A + A )
Theorem	times2i 9187	A number times 2. (Contributed by NM, 11-May-2004.)
|- A e. CC   =>    |- ( A x. 2 ) = ( A + A )
Theorem	2txmxeqx 9188	Two times a complex number minus the number itself results in the number itself. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
|- ( X e. CC -> ( ( 2 x. X ) - X ) = X )
Theorem	2div2e1 9189	2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 2 / 2 ) = 1
Theorem	2p1e3 9190	2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 2 + 1 ) = 3
Theorem	1p2e3 9191	1 + 2 = 3 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 1 + 2 ) = 3
Theorem	3p1e4 9192	3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 3 + 1 ) = 4
Theorem	4p1e5 9193	4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 4 + 1 ) = 5
Theorem	5p1e6 9194	5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 5 + 1 ) = 6
Theorem	6p1e7 9195	6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 6 + 1 ) = 7
Theorem	7p1e8 9196	7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 7 + 1 ) = 8
Theorem	8p1e9 9197	8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)
|- ( 8 + 1 ) = 9
Theorem	3p2e5 9198	3 + 2 = 5. (Contributed by NM, 11-May-2004.)
|- ( 3 + 2 ) = 5
Theorem	3p3e6 9199	3 + 3 = 6. (Contributed by NM, 11-May-2004.)
|- ( 3 + 3 ) = 6
Theorem	4p2e6 9200	4 + 2 = 6. (Contributed by NM, 11-May-2004.)
|- ( 4 + 2 ) = 6