P. 78 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7701-7800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnnlt1 7701	A positive integer is not less than one. (Contributed by NM, 18-Jan-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (A ∈ ℕ → ¬ A < 1)
Theorem	0nnn 7702	Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.)
⊢ ¬ 0 ∈ ℕ
Theorem	nnne0 7703	A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.)
⊢ (A ∈ ℕ → A ≠ 0)
Theorem	nnap0 7704	A positive integer is apart from zero. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (A ∈ ℕ → A # 0)
Theorem	nngt0i 7705	A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.)
⊢ A ∈ ℕ    ⇒   ⊢ 0 < A
Theorem	nnne0i 7706	A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.)
⊢ A ∈ ℕ    ⇒   ⊢ A ≠ 0
Theorem	nn2ge 7707*	There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999.)
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → ∃x ∈ ℕ (A ≤ x ∧ B ≤ x))
Theorem	nn1gt1 7708	A positive integer is either one or greater than one. This is for ℕ; 0elnn 4283 is a similar theorem for 𝜔 (the natural numbers as ordinals). (Contributed by Jim Kingdon, 7-Mar-2020.)
⊢ (A ∈ ℕ → (A = 1 ∨ 1 < A))
Theorem	nngt1ne1 7709	A positive integer is greater than one iff it is not equal to one. (Contributed by NM, 7-Oct-2004.)
⊢ (A ∈ ℕ → (1 < A ↔ A ≠ 1))
Theorem	nndivre 7710	The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.)
⊢ ((A ∈ ℝ ∧ 𝑁 ∈ ℕ) → (A / 𝑁) ∈ ℝ)
Theorem	nnrecre 7711	The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.)
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ)
Theorem	nnrecgt0 7712	The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.)
⊢ (A ∈ ℕ → 0 < (1 / A))
Theorem	nnsub 7713	Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.)
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (A < B ↔ (B − A) ∈ ℕ))
Theorem	nnsubi 7714	Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.)
⊢ A ∈ ℕ    &   ⊢ B ∈ ℕ    ⇒   ⊢ (A < B ↔ (B − A) ∈ ℕ)
Theorem	nndiv 7715*	Two ways to express "A divides B " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (∃x ∈ ℕ (A · x) = B ↔ (B / A) ∈ ℕ))
Theorem	nndivtr 7716	Transitive property of divisibility: if A divides B and B divides 𝐶, then A divides 𝐶. Typically, 𝐶 would be an integer, although the theorem holds for complex 𝐶. (Contributed by NM, 3-May-2005.)
⊢ (((A ∈ ℕ ∧ B ∈ ℕ ∧ 𝐶 ∈ ℂ) ∧ ((B / A) ∈ ℕ ∧ (𝐶 / B) ∈ ℕ)) → (𝐶 / A) ∈ ℕ)
Theorem	nnge1d 7717	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℕ)    ⇒   ⊢ (φ → 1 ≤ A)
Theorem	nngt0d 7718	A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℕ)    ⇒   ⊢ (φ → 0 < A)
Theorem	nnne0d 7719	A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℕ)    ⇒   ⊢ (φ → A ≠ 0)
Theorem	nnrecred 7720	The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℕ)    ⇒   ⊢ (φ → (1 / A) ∈ ℝ)
Theorem	nnaddcld 7721	Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℕ)    &   ⊢ (φ → B ∈ ℕ)    ⇒   ⊢ (φ → (A + B) ∈ ℕ)
Theorem	nnmulcld 7722	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℕ)    &   ⊢ (φ → B ∈ ℕ)    ⇒   ⊢ (φ → (A · B) ∈ ℕ)
Theorem	nndivred 7723	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℕ)    ⇒   ⊢ (φ → (A / B) ∈ ℝ)
3.4.3  Decimal representation of numbers Note that the numbers 0 and 1 are constants defined as primitives of the complex number axiom system (see df-0 6698 and df-1 6699). Only the digits 0 through 9 (df-0 6698 through df-9 7740) and the number 10 (df-10 7741) are explicitly defined. 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 7724	Extend class notation to include the number 2.
class 2
Syntax	c3 7725	Extend class notation to include the number 3.
class 3
Syntax	c4 7726	Extend class notation to include the number 4.
class 4
Syntax	c5 7727	Extend class notation to include the number 5.
class 5
Syntax	c6 7728	Extend class notation to include the number 6.
class 6
Syntax	c7 7729	Extend class notation to include the number 7.
class 7
Syntax	c8 7730	Extend class notation to include the number 8.
class 8
Syntax	c9 7731	Extend class notation to include the number 9.
class 9
Syntax	c10 7732	Extend class notation to include the number 10.
class 10
Definition	df-2 7733	Define the number 2. (Contributed by NM, 27-May-1999.)
⊢ 2 = (1 + 1)
Definition	df-3 7734	Define the number 3. (Contributed by NM, 27-May-1999.)
⊢ 3 = (2 + 1)
Definition	df-4 7735	Define the number 4. (Contributed by NM, 27-May-1999.)
⊢ 4 = (3 + 1)
Definition	df-5 7736	Define the number 5. (Contributed by NM, 27-May-1999.)
⊢ 5 = (4 + 1)
Definition	df-6 7737	Define the number 6. (Contributed by NM, 27-May-1999.)
⊢ 6 = (5 + 1)
Definition	df-7 7738	Define the number 7. (Contributed by NM, 27-May-1999.)
⊢ 7 = (6 + 1)
Definition	df-8 7739	Define the number 8. (Contributed by NM, 27-May-1999.)
⊢ 8 = (7 + 1)
Definition	df-9 7740	Define the number 9. (Contributed by NM, 27-May-1999.)
⊢ 9 = (8 + 1)
Definition	df-10 7741	Define the number 10. See remarks under df-2 7733. (Contributed by NM, 5-Feb-2007.)
⊢ 10 = (9 + 1)
Theorem	0ne1 7742	0 ≠ 1 (common case). See aso 1ap0 7354. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ≠ 1
Theorem	1ne0 7743	1 ≠ 0. See aso 1ap0 7354. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 1 ≠ 0
Theorem	1m1e0 7744	(1 − 1) = 0 (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (1 − 1) = 0
Theorem	2re 7745	The number 2 is real. (Contributed by NM, 27-May-1999.)
⊢ 2 ∈ ℝ
Theorem	2cn 7746	The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)
⊢ 2 ∈ ℂ
Theorem	2ex 7747	2 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 2 ∈ V
Theorem	2cnd 7748	2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (φ → 2 ∈ ℂ)
Theorem	3re 7749	The number 3 is real. (Contributed by NM, 27-May-1999.)
⊢ 3 ∈ ℝ
Theorem	3cn 7750	The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)
⊢ 3 ∈ ℂ
Theorem	3ex 7751	3 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 3 ∈ V
Theorem	4re 7752	The number 4 is real. (Contributed by NM, 27-May-1999.)
⊢ 4 ∈ ℝ
Theorem	4cn 7753	The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 4 ∈ ℂ
Theorem	5re 7754	The number 5 is real. (Contributed by NM, 27-May-1999.)
⊢ 5 ∈ ℝ
Theorem	5cn 7755	The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 5 ∈ ℂ
Theorem	6re 7756	The number 6 is real. (Contributed by NM, 27-May-1999.)
⊢ 6 ∈ ℝ
Theorem	6cn 7757	The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 6 ∈ ℂ
Theorem	7re 7758	The number 7 is real. (Contributed by NM, 27-May-1999.)
⊢ 7 ∈ ℝ
Theorem	7cn 7759	The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 7 ∈ ℂ
Theorem	8re 7760	The number 8 is real. (Contributed by NM, 27-May-1999.)
⊢ 8 ∈ ℝ
Theorem	8cn 7761	The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 8 ∈ ℂ
Theorem	9re 7762	The number 9 is real. (Contributed by NM, 27-May-1999.)
⊢ 9 ∈ ℝ
Theorem	9cn 7763	The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 9 ∈ ℂ
Theorem	10re 7764	The number 10 is real. (Contributed by NM, 5-Feb-2007.)
⊢ 10 ∈ ℝ
Theorem	0le0 7765	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 0 ≤ 0
Theorem	0le2 7766	0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.)
⊢ 0 ≤ 2
Theorem	2pos 7767	The number 2 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 2
Theorem	2ne0 7768	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
⊢ 2 ≠ 0
Theorem	2ap0 7769	The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 2 # 0
Theorem	3pos 7770	The number 3 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 3
Theorem	3ne0 7771	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 3 ≠ 0
Theorem	4pos 7772	The number 4 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 4
Theorem	4ne0 7773	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ 4 ≠ 0
Theorem	5pos 7774	The number 5 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 5
Theorem	6pos 7775	The number 6 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 6
Theorem	7pos 7776	The number 7 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 7
Theorem	8pos 7777	The number 8 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 8
Theorem	9pos 7778	The number 9 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 9
Theorem	10pos 7779	The number 10 is positive. (Contributed by NM, 5-Feb-2007.)
⊢ 0 < 10
3.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 7780	-1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ -1 ∈ ℂ
Theorem	neg1rr 7781	-1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ -1 ∈ ℝ
Theorem	neg1ne0 7782	-1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 ≠ 0
Theorem	neg1lt0 7783	-1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 < 0
Theorem	neg1ap0 7784	-1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
⊢ -1 # 0
Theorem	negneg1e1 7785	--1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ --1 = 1
Theorem	1pneg1e0 7786	1 + -1 is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + -1) = 0
Theorem	0m0e0 7787	0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (0 − 0) = 0
Theorem	1m0e1 7788	1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 − 0) = 1
Theorem	0p1e1 7789	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (0 + 1) = 1
Theorem	1p0e1 7790	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 0) = 1
Theorem	1p1e2 7791	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
⊢ (1 + 1) = 2
Theorem	2m1e1 7792	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 7814. (Contributed by David A. Wheeler, 4-Jan-2017.)
⊢ (2 − 1) = 1
Theorem	1e2m1 7793	1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 1 = (2 − 1)
Theorem	3m1e2 7794	3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.)
⊢ (3 − 1) = 2
Theorem	2p2e4 7795	Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page: http://us.metamath.org/mpeuni/mmset.html#trivia. (Contributed by NM, 27-May-1999.)
⊢ (2 + 2) = 4
Theorem	2times 7796	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 ∈ ℂ → (2 · A) = (A + A))
Theorem	times2 7797	A number times 2. (Contributed by NM, 16-Oct-2007.)
⊢ (A ∈ ℂ → (A · 2) = (A + A))
Theorem	2timesi 7798	Two times a number. (Contributed by NM, 1-Aug-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (2 · A) = (A + A)
Theorem	times2i 7799	A number times 2. (Contributed by NM, 11-May-2004.)
⊢ A ∈ ℂ    ⇒   ⊢ (A · 2) = (A + A)
Theorem	2div2e1 7800	2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (2 / 2) = 1