P. 83 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8201-8300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nngt0 8201	A positive integer is positive. (Contributed by NM, 26-Sep-1999.)
⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
Theorem	nnnlt1 8202	A positive integer is not less than one. (Contributed by NM, 18-Jan-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℕ → ¬ 𝐴 < 1)
Theorem	0nnn 8203	Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.)
⊢ ¬ 0 ∈ ℕ
Theorem	nnne0 8204	A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Theorem	nnap0 8205	A positive integer is apart from zero. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝐴 ∈ ℕ → 𝐴 # 0)
Theorem	nngt0i 8206	A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 0 < 𝐴
Theorem	nnne0i 8207	A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 𝐴 ≠ 0
Theorem	nn2ge 8208*	There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ (𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥))
Theorem	nn1gt1 8209	A positive integer is either one or greater than one. This is for ℕ; 0elnn 4386 is a similar theorem for ω (the natural numbers as ordinals). (Contributed by Jim Kingdon, 7-Mar-2020.)
⊢ (𝐴 ∈ ℕ → (𝐴 = 1 ∨ 1 < 𝐴))
Theorem	nngt1ne1 8210	A positive integer is greater than one iff it is not equal to one. (Contributed by NM, 7-Oct-2004.)
⊢ (𝐴 ∈ ℕ → (1 < 𝐴 ↔ 𝐴 ≠ 1))
Theorem	nndivre 8211	The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) ∈ ℝ)
Theorem	nnrecre 8212	The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.)
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ)
Theorem	nnrecgt0 8213	The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 0 < (1 / 𝐴))
Theorem	nnsub 8214	Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ))
Theorem	nnsubi 8215	Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ)
Theorem	nndiv 8216*	Two ways to express "𝐴 divides 𝐵 " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑥 ∈ ℕ (𝐴 · 𝑥) = 𝐵 ↔ (𝐵 / 𝐴) ∈ ℕ))
Theorem	nndivtr 8217	Transitive property of divisibility: if 𝐴 divides 𝐵 and 𝐵 divides 𝐶, then 𝐴 divides 𝐶. Typically, 𝐶 would be an integer, although the theorem holds for complex 𝐶. (Contributed by NM, 3-May-2005.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℂ) ∧ ((𝐵 / 𝐴) ∈ ℕ ∧ (𝐶 / 𝐵) ∈ ℕ)) → (𝐶 / 𝐴) ∈ ℕ)
Theorem	nnge1d 8218	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 1 ≤ 𝐴)
Theorem	nngt0d 8219	A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 0 < 𝐴)
Theorem	nnne0d 8220	A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0)
Theorem	nnap0d 8221	A positive integer is apart from zero. (Contributed by Jim Kingdon, 25-Aug-2021.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 # 0)
Theorem	nnrecred 8222	The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ)
Theorem	nnaddcld 8223	Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ)
Theorem	nnmulcld 8224	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ)
Theorem	nndivred 8225	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
3.4.3  Decimal representation of numbers The decimal representation of numbers/integers is based on the decimal digits 0 through 9 (df-0 7120 through df-9 8242), 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 7120 and df-1 7121). 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 8226	Extend class notation to include the number 2.
class 2
Syntax	c3 8227	Extend class notation to include the number 3.
class 3
Syntax	c4 8228	Extend class notation to include the number 4.
class 4
Syntax	c5 8229	Extend class notation to include the number 5.
class 5
Syntax	c6 8230	Extend class notation to include the number 6.
class 6
Syntax	c7 8231	Extend class notation to include the number 7.
class 7
Syntax	c8 8232	Extend class notation to include the number 8.
class 8
Syntax	c9 8233	Extend class notation to include the number 9.
class 9
Syntax	c10 8234	Extend class notation to include the number 10.
class 10
Definition	df-2 8235	Define the number 2. (Contributed by NM, 27-May-1999.)
⊢ 2 = (1 + 1)
Definition	df-3 8236	Define the number 3. (Contributed by NM, 27-May-1999.)
⊢ 3 = (2 + 1)
Definition	df-4 8237	Define the number 4. (Contributed by NM, 27-May-1999.)
⊢ 4 = (3 + 1)
Definition	df-5 8238	Define the number 5. (Contributed by NM, 27-May-1999.)
⊢ 5 = (4 + 1)
Definition	df-6 8239	Define the number 6. (Contributed by NM, 27-May-1999.)
⊢ 6 = (5 + 1)
Definition	df-7 8240	Define the number 7. (Contributed by NM, 27-May-1999.)
⊢ 7 = (6 + 1)
Definition	df-8 8241	Define the number 8. (Contributed by NM, 27-May-1999.)
⊢ 8 = (7 + 1)
Definition	df-9 8242	Define the number 9. (Contributed by NM, 27-May-1999.)
⊢ 9 = (8 + 1)
Theorem	0ne1 8243	0 ≠ 1 (common case). See aso 1ap0 7827. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ≠ 1
Theorem	1ne0 8244	1 ≠ 0. See aso 1ap0 7827. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 1 ≠ 0
Theorem	1m1e0 8245	(1 − 1) = 0 (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (1 − 1) = 0
Theorem	2re 8246	The number 2 is real. (Contributed by NM, 27-May-1999.)
⊢ 2 ∈ ℝ
Theorem	2cn 8247	The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)
⊢ 2 ∈ ℂ
Theorem	2ex 8248	2 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 2 ∈ V
Theorem	2cnd 8249	2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (𝜑 → 2 ∈ ℂ)
Theorem	3re 8250	The number 3 is real. (Contributed by NM, 27-May-1999.)
⊢ 3 ∈ ℝ
Theorem	3cn 8251	The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)
⊢ 3 ∈ ℂ
Theorem	3ex 8252	3 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 3 ∈ V
Theorem	4re 8253	The number 4 is real. (Contributed by NM, 27-May-1999.)
⊢ 4 ∈ ℝ
Theorem	4cn 8254	The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 4 ∈ ℂ
Theorem	5re 8255	The number 5 is real. (Contributed by NM, 27-May-1999.)
⊢ 5 ∈ ℝ
Theorem	5cn 8256	The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 5 ∈ ℂ
Theorem	6re 8257	The number 6 is real. (Contributed by NM, 27-May-1999.)
⊢ 6 ∈ ℝ
Theorem	6cn 8258	The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 6 ∈ ℂ
Theorem	7re 8259	The number 7 is real. (Contributed by NM, 27-May-1999.)
⊢ 7 ∈ ℝ
Theorem	7cn 8260	The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 7 ∈ ℂ
Theorem	8re 8261	The number 8 is real. (Contributed by NM, 27-May-1999.)
⊢ 8 ∈ ℝ
Theorem	8cn 8262	The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 8 ∈ ℂ
Theorem	9re 8263	The number 9 is real. (Contributed by NM, 27-May-1999.)
⊢ 9 ∈ ℝ
Theorem	9cn 8264	The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 9 ∈ ℂ
Theorem	0le0 8265	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 0 ≤ 0
Theorem	0le2 8266	0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.)
⊢ 0 ≤ 2
Theorem	2pos 8267	The number 2 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 2
Theorem	2ne0 8268	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
⊢ 2 ≠ 0
Theorem	2ap0 8269	The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 2 # 0
Theorem	3pos 8270	The number 3 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 3
Theorem	3ne0 8271	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 3 ≠ 0
Theorem	3ap0 8272	The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
⊢ 3 # 0
Theorem	4pos 8273	The number 4 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 4
Theorem	4ne0 8274	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ 4 ≠ 0
Theorem	4ap0 8275	The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
⊢ 4 # 0
Theorem	5pos 8276	The number 5 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 5
Theorem	6pos 8277	The number 6 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 6
Theorem	7pos 8278	The number 7 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 7
Theorem	8pos 8279	The number 8 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 8
Theorem	9pos 8280	The number 9 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 9
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 8281	-1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ -1 ∈ ℂ
Theorem	neg1rr 8282	-1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ -1 ∈ ℝ
Theorem	neg1ne0 8283	-1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 ≠ 0
Theorem	neg1lt0 8284	-1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 < 0
Theorem	neg1ap0 8285	-1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
⊢ -1 # 0
Theorem	negneg1e1 8286	--1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ --1 = 1
Theorem	1pneg1e0 8287	1 + -1 is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + -1) = 0
Theorem	0m0e0 8288	0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (0 − 0) = 0
Theorem	1m0e1 8289	1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 − 0) = 1
Theorem	0p1e1 8290	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (0 + 1) = 1
Theorem	1p0e1 8291	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 0) = 1
Theorem	1p1e2 8292	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
⊢ (1 + 1) = 2
Theorem	2m1e1 8293	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 8314. (Contributed by David A. Wheeler, 4-Jan-2017.)
⊢ (2 − 1) = 1
Theorem	1e2m1 8294	1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 1 = (2 − 1)
Theorem	3m1e2 8295	3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.)
⊢ (3 − 1) = 2
Theorem	2p2e4 8296	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 8297	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 8298	A number times 2. (Contributed by NM, 16-Oct-2007.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 2) = (𝐴 + 𝐴))
Theorem	2timesi 8299	Two times a number. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (2 · 𝐴) = (𝐴 + 𝐴)
Theorem	times2i 8300	A number times 2. (Contributed by NM, 11-May-2004.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · 2) = (𝐴 + 𝐴)