P. 90 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8901-9000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnaddcld 8901	Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ)
Theorem	nnmulcld 8902	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ)
Theorem	nndivred 8903	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
4.4.3  Decimal representation of numbers The decimal representation of numbers/integers is based on the decimal digits 0 through 9 (df-0 7756 through df-9 8919), 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 7756 and df-1 7757). Integers can also be exhibited as sums of powers of 10 (e.g., the number 103 can be expressed as ((;10↑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 8904	Extend class notation to include the number 2.
class 2
Syntax	c3 8905	Extend class notation to include the number 3.
class 3
Syntax	c4 8906	Extend class notation to include the number 4.
class 4
Syntax	c5 8907	Extend class notation to include the number 5.
class 5
Syntax	c6 8908	Extend class notation to include the number 6.
class 6
Syntax	c7 8909	Extend class notation to include the number 7.
class 7
Syntax	c8 8910	Extend class notation to include the number 8.
class 8
Syntax	c9 8911	Extend class notation to include the number 9.
class 9
Definition	df-2 8912	Define the number 2. (Contributed by NM, 27-May-1999.)
⊢ 2 = (1 + 1)
Definition	df-3 8913	Define the number 3. (Contributed by NM, 27-May-1999.)
⊢ 3 = (2 + 1)
Definition	df-4 8914	Define the number 4. (Contributed by NM, 27-May-1999.)
⊢ 4 = (3 + 1)
Definition	df-5 8915	Define the number 5. (Contributed by NM, 27-May-1999.)
⊢ 5 = (4 + 1)
Definition	df-6 8916	Define the number 6. (Contributed by NM, 27-May-1999.)
⊢ 6 = (5 + 1)
Definition	df-7 8917	Define the number 7. (Contributed by NM, 27-May-1999.)
⊢ 7 = (6 + 1)
Definition	df-8 8918	Define the number 8. (Contributed by NM, 27-May-1999.)
⊢ 8 = (7 + 1)
Definition	df-9 8919	Define the number 9. (Contributed by NM, 27-May-1999.)
⊢ 9 = (8 + 1)
Theorem	0ne1 8920	0 ≠ 1 (common case). See aso 1ap0 8484. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ≠ 1
Theorem	1ne0 8921	1 ≠ 0. See aso 1ap0 8484. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 1 ≠ 0
Theorem	1m1e0 8922	(1 − 1) = 0 (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (1 − 1) = 0
Theorem	2re 8923	The number 2 is real. (Contributed by NM, 27-May-1999.)
⊢ 2 ∈ ℝ
Theorem	2cn 8924	The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)
⊢ 2 ∈ ℂ
Theorem	2ex 8925	2 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 2 ∈ V
Theorem	2cnd 8926	2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (𝜑 → 2 ∈ ℂ)
Theorem	3re 8927	The number 3 is real. (Contributed by NM, 27-May-1999.)
⊢ 3 ∈ ℝ
Theorem	3cn 8928	The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)
⊢ 3 ∈ ℂ
Theorem	3ex 8929	3 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 3 ∈ V
Theorem	4re 8930	The number 4 is real. (Contributed by NM, 27-May-1999.)
⊢ 4 ∈ ℝ
Theorem	4cn 8931	The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 4 ∈ ℂ
Theorem	5re 8932	The number 5 is real. (Contributed by NM, 27-May-1999.)
⊢ 5 ∈ ℝ
Theorem	5cn 8933	The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 5 ∈ ℂ
Theorem	6re 8934	The number 6 is real. (Contributed by NM, 27-May-1999.)
⊢ 6 ∈ ℝ
Theorem	6cn 8935	The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 6 ∈ ℂ
Theorem	7re 8936	The number 7 is real. (Contributed by NM, 27-May-1999.)
⊢ 7 ∈ ℝ
Theorem	7cn 8937	The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 7 ∈ ℂ
Theorem	8re 8938	The number 8 is real. (Contributed by NM, 27-May-1999.)
⊢ 8 ∈ ℝ
Theorem	8cn 8939	The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 8 ∈ ℂ
Theorem	9re 8940	The number 9 is real. (Contributed by NM, 27-May-1999.)
⊢ 9 ∈ ℝ
Theorem	9cn 8941	The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 9 ∈ ℂ
Theorem	0le0 8942	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 0 ≤ 0
Theorem	0le2 8943	0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.)
⊢ 0 ≤ 2
Theorem	2pos 8944	The number 2 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 2
Theorem	2ne0 8945	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
⊢ 2 ≠ 0
Theorem	2ap0 8946	The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 2 # 0
Theorem	3pos 8947	The number 3 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 3
Theorem	3ne0 8948	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 3 ≠ 0
Theorem	3ap0 8949	The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
⊢ 3 # 0
Theorem	4pos 8950	The number 4 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 4
Theorem	4ne0 8951	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ 4 ≠ 0
Theorem	4ap0 8952	The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
⊢ 4 # 0
Theorem	5pos 8953	The number 5 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 5
Theorem	6pos 8954	The number 6 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 6
Theorem	7pos 8955	The number 7 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 7
Theorem	8pos 8956	The number 8 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 8
Theorem	9pos 8957	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 8958	-1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ -1 ∈ ℂ
Theorem	neg1rr 8959	-1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ -1 ∈ ℝ
Theorem	neg1ne0 8960	-1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 ≠ 0
Theorem	neg1lt0 8961	-1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 < 0
Theorem	neg1ap0 8962	-1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
⊢ -1 # 0
Theorem	negneg1e1 8963	--1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ --1 = 1
Theorem	1pneg1e0 8964	1 + -1 is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + -1) = 0
Theorem	0m0e0 8965	0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (0 − 0) = 0
Theorem	1m0e1 8966	1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 − 0) = 1
Theorem	0p1e1 8967	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (0 + 1) = 1
Theorem	fv0p1e1 8968	Function value at 𝑁 + 1 with 𝑁 replaced by 0. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.)
⊢ (𝑁 = 0 → (𝐹‘(𝑁 + 1)) = (𝐹‘1))
Theorem	1p0e1 8969	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 0) = 1
Theorem	1p1e2 8970	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
⊢ (1 + 1) = 2
Theorem	2m1e1 8971	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 8998. (Contributed by David A. Wheeler, 4-Jan-2017.)
⊢ (2 − 1) = 1
Theorem	1e2m1 8972	1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 1 = (2 − 1)
Theorem	3m1e2 8973	3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.)
⊢ (3 − 1) = 2
Theorem	4m1e3 8974	4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.)
⊢ (4 − 1) = 3
Theorem	5m1e4 8975	5 - 1 = 4. (Contributed by AV, 6-Sep-2021.)
⊢ (5 − 1) = 4
Theorem	6m1e5 8976	6 - 1 = 5. (Contributed by AV, 6-Sep-2021.)
⊢ (6 − 1) = 5
Theorem	7m1e6 8977	7 - 1 = 6. (Contributed by AV, 6-Sep-2021.)
⊢ (7 − 1) = 6
Theorem	8m1e7 8978	8 - 1 = 7. (Contributed by AV, 6-Sep-2021.)
⊢ (8 − 1) = 7
Theorem	9m1e8 8979	9 - 1 = 8. (Contributed by AV, 6-Sep-2021.)
⊢ (9 − 1) = 8
Theorem	2p2e4 8980	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 8981	Two times a number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) (Proof shortened by AV, 26-Feb-2020.)
⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
Theorem	times2 8982	A number times 2. (Contributed by NM, 16-Oct-2007.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 2) = (𝐴 + 𝐴))
Theorem	2timesi 8983	Two times a number. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (2 · 𝐴) = (𝐴 + 𝐴)
Theorem	times2i 8984	A number times 2. (Contributed by NM, 11-May-2004.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · 2) = (𝐴 + 𝐴)
Theorem	2div2e1 8985	2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (2 / 2) = 1
Theorem	2p1e3 8986	2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (2 + 1) = 3
Theorem	1p2e3 8987	1 + 2 = 3 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 2) = 3
Theorem	3p1e4 8988	3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (3 + 1) = 4
Theorem	4p1e5 8989	4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (4 + 1) = 5
Theorem	5p1e6 8990	5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (5 + 1) = 6
Theorem	6p1e7 8991	6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (6 + 1) = 7
Theorem	7p1e8 8992	7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (7 + 1) = 8
Theorem	8p1e9 8993	8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (8 + 1) = 9
Theorem	3p2e5 8994	3 + 2 = 5. (Contributed by NM, 11-May-2004.)
⊢ (3 + 2) = 5
Theorem	3p3e6 8995	3 + 3 = 6. (Contributed by NM, 11-May-2004.)
⊢ (3 + 3) = 6
Theorem	4p2e6 8996	4 + 2 = 6. (Contributed by NM, 11-May-2004.)
⊢ (4 + 2) = 6
Theorem	4p3e7 8997	4 + 3 = 7. (Contributed by NM, 11-May-2004.)
⊢ (4 + 3) = 7
Theorem	4p4e8 8998	4 + 4 = 8. (Contributed by NM, 11-May-2004.)
⊢ (4 + 4) = 8
Theorem	5p2e7 8999	5 + 2 = 7. (Contributed by NM, 11-May-2004.)
⊢ (5 + 2) = 7
Theorem	5p3e8 9000	5 + 3 = 8. (Contributed by NM, 11-May-2004.)
⊢ (5 + 3) = 8