P. 81 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8001-8100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elnnnn0 8001	The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-May-2004.)
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℂ ∧ (𝑁 − 1) ∈ ℕ0))
Theorem	elnnnn0b 8002	The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 1-Sep-2005.)
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0 ∧ 0 < 𝑁))
Theorem	elnnnn0c 8003	The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-Jan-2006.)
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁))
Theorem	nn0addge1 8004	A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
⊢ ((A ∈ ℝ ∧ 𝑁 ∈ ℕ0) → A ≤ (A + 𝑁))
Theorem	nn0addge2 8005	A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
⊢ ((A ∈ ℝ ∧ 𝑁 ∈ ℕ0) → A ≤ (𝑁 + A))
Theorem	nn0addge1i 8006	A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
⊢ A ∈ ℝ    &   ⊢ 𝑁 ∈ ℕ0    ⇒   ⊢ A ≤ (A + 𝑁)
Theorem	nn0addge2i 8007	A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
⊢ A ∈ ℝ    &   ⊢ 𝑁 ∈ ℕ0    ⇒   ⊢ A ≤ (𝑁 + A)
Theorem	nn0le2xi 8008	A nonnegative integer is less than or equal to twice itself. (Contributed by Raph Levien, 10-Dec-2002.)
⊢ 𝑁 ∈ ℕ0    ⇒   ⊢ 𝑁 ≤ (2 · 𝑁)
Theorem	nn0lele2xi 8009	'Less than or equal to' implies 'less than or equal to twice' for nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.)
⊢ 𝑀 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    ⇒   ⊢ (𝑁 ≤ 𝑀 → 𝑁 ≤ (2 · 𝑀))
Theorem	nn0supp 8010	Two ways to write the support of a function on ℕ0. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ (𝐹:𝐼⟶ℕ0 → (◡𝐹 “ (V ∖ {0})) = (◡𝐹 “ ℕ))
Theorem	nnnn0d 8011	A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℕ)    ⇒   ⊢ (φ → A ∈ ℕ0)
Theorem	nn0red 8012	A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℕ0)    ⇒   ⊢ (φ → A ∈ ℝ)
Theorem	nn0cnd 8013	A nonnegative integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℕ0)    ⇒   ⊢ (φ → A ∈ ℂ)
Theorem	nn0ge0d 8014	A nonnegative integer is greater than or equal to zero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℕ0)    ⇒   ⊢ (φ → 0 ≤ A)
Theorem	nn0addcld 8015	Closure of addition of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℕ0)    &   ⊢ (φ → B ∈ ℕ0)    ⇒   ⊢ (φ → (A + B) ∈ ℕ0)
Theorem	nn0mulcld 8016	Closure of multiplication of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℕ0)    &   ⊢ (φ → B ∈ ℕ0)    ⇒   ⊢ (φ → (A · B) ∈ ℕ0)
Theorem	nn0readdcl 8017	Closure law for addition of reals, restricted to nonnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
⊢ ((A ∈ ℕ0 ∧ B ∈ ℕ0) → (A + B) ∈ ℝ)
Theorem	nn0ge2m1nn 8018	If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 4-Jan-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁) → (𝑁 − 1) ∈ ℕ)
Theorem	nn0ge2m1nn0 8019	If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is also a nonnegative integer. (Contributed by Alexander van der Vekens, 1-Aug-2018.)
⊢ ((𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁) → (𝑁 − 1) ∈ ℕ0)
Theorem	nn0nndivcl 8020	Closure law for dividing of a nonnegative integer by a positive integer. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
⊢ ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ) → (𝐾 / 𝐿) ∈ ℝ)
3.4.8  Integers (as a subset of complex numbers)
Syntax	cz 8021	Extend class notation to include the class of integers.
class ℤ
Definition	df-z 8022	Define the set of integers, which are the positive and negative integers together with zero. Definition of integers in [Apostol] p. 22. The letter Z abbreviates the German word Zahlen meaning "numbers." (Contributed by NM, 8-Jan-2002.)
⊢ ℤ = {𝑛 ∈ ℝ ∣ (𝑛 = 0 ∨ 𝑛 ∈ ℕ ∨ -𝑛 ∈ ℕ)}
Theorem	elz 8023	Membership in the set of integers. (Contributed by NM, 8-Jan-2002.)
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
Theorem	nnnegz 8024	The negative of a positive integer is an integer. (Contributed by NM, 12-Jan-2002.)
⊢ (𝑁 ∈ ℕ → -𝑁 ∈ ℤ)
Theorem	zre 8025	An integer is a real. (Contributed by NM, 8-Jan-2002.)
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
Theorem	zcn 8026	An integer is a complex number. (Contributed by NM, 9-May-2004.)
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
Theorem	zrei 8027	An integer is a real number. (Contributed by NM, 14-Jul-2005.)
⊢ A ∈ ℤ    ⇒   ⊢ A ∈ ℝ
Theorem	zssre 8028	The integers are a subset of the reals. (Contributed by NM, 2-Aug-2004.)
⊢ ℤ ⊆ ℝ
Theorem	zsscn 8029	The integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
⊢ ℤ ⊆ ℂ
Theorem	zex 8030	The set of integers exists. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ℤ ∈ V
Theorem	elnnz 8031	Positive integer property expressed in terms of integers. (Contributed by NM, 8-Jan-2002.)
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
Theorem	0z 8032	Zero is an integer. (Contributed by NM, 12-Jan-2002.)
⊢ 0 ∈ ℤ
Theorem	0zd 8033	Zero is an integer, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (φ → 0 ∈ ℤ)
Theorem	elnn0z 8034	Nonnegative integer property expressed in terms of integers. (Contributed by NM, 9-May-2004.)
⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))
Theorem	elznn0nn 8035	Integer property expressed in terms nonnegative integers and positive integers. (Contributed by NM, 10-May-2004.)
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)))
Theorem	elznn0 8036	Integer property expressed in terms of nonnegative integers. (Contributed by NM, 9-May-2004.)
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)))
Theorem	elznn 8037	Integer property expressed in terms of positive integers and nonnegative integers. (Contributed by NM, 12-Jul-2005.)
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ0)))
Theorem	nnssz 8038	Positive integers are a subset of integers. (Contributed by NM, 9-Jan-2002.)
⊢ ℕ ⊆ ℤ
Theorem	nn0ssz 8039	Nonnegative integers are a subset of the integers. (Contributed by NM, 9-May-2004.)
⊢ ℕ0 ⊆ ℤ
Theorem	nnz 8040	A positive integer is an integer. (Contributed by NM, 9-May-2004.)
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
Theorem	nn0z 8041	A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
Theorem	nnzi 8042	A positive integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑁 ∈ ℕ    ⇒   ⊢ 𝑁 ∈ ℤ
Theorem	nn0zi 8043	A nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑁 ∈ ℕ0    ⇒   ⊢ 𝑁 ∈ ℤ
Theorem	elnnz1 8044	Positive integer property expressed in terms of integers. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 1 ≤ 𝑁))
Theorem	nnzrab 8045	Positive integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.)
⊢ ℕ = {x ∈ ℤ ∣ 1 ≤ x}
Theorem	nn0zrab 8046	Nonnegative integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.)
⊢ ℕ0 = {x ∈ ℤ ∣ 0 ≤ x}
Theorem	1z 8047	One is an integer. (Contributed by NM, 10-May-2004.)
⊢ 1 ∈ ℤ
Theorem	1zzd 8048	1 is an integer, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (φ → 1 ∈ ℤ)
Theorem	2z 8049	Two is an integer. (Contributed by NM, 10-May-2004.)
⊢ 2 ∈ ℤ
Theorem	3z 8050	3 is an integer. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 3 ∈ ℤ
Theorem	4z 8051	4 is an integer. (Contributed by BJ, 26-Mar-2020.)
⊢ 4 ∈ ℤ
Theorem	znegcl 8052	Closure law for negative integers. (Contributed by NM, 9-May-2004.)
⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ)
Theorem	neg1z 8053	-1 is an integer (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ -1 ∈ ℤ
Theorem	znegclb 8054	A number is an integer iff its negative is. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (A ∈ ℂ → (A ∈ ℤ ↔ -A ∈ ℤ))
Theorem	nn0negz 8055	The negative of a nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
⊢ (𝑁 ∈ ℕ0 → -𝑁 ∈ ℤ)
Theorem	nn0negzi 8056	The negative of a nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑁 ∈ ℕ0    ⇒   ⊢ -𝑁 ∈ ℤ
Theorem	peano2z 8057	Second Peano postulate generalized to integers. (Contributed by NM, 13-Feb-2005.)
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ)
Theorem	zaddcllempos 8058	Lemma for zaddcl 8061. Special case in which 𝑁 is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℤ)
Theorem	peano2zm 8059	"Reverse" second Peano postulate for integers. (Contributed by NM, 12-Sep-2005.)
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
Theorem	zaddcllemneg 8060	Lemma for zaddcl 8061. Special case in which -𝑁 is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℤ)
Theorem	zaddcl 8061	Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ)
Theorem	zsubcl 8062	Closure of subtraction of integers. (Contributed by NM, 11-May-2004.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ)
Theorem	ztri3or0 8063	Integer trichotomy (with zero). (Contributed by Jim Kingdon, 14-Mar-2020.)
⊢ (𝑁 ∈ ℤ → (𝑁 < 0 ∨ 𝑁 = 0 ∨ 0 < 𝑁))
Theorem	ztri3or 8064	Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀))
Theorem	zletric 8065	Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.)
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → (A ≤ B ∨ B ≤ A))
Theorem	zlelttric 8066	Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.)
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → (A ≤ B ∨ B < A))
Theorem	zltnle 8067	'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 14-Mar-2020.)
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → (A < B ↔ ¬ B ≤ A))
Theorem	zleloe 8068	Integer 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.)
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → (A ≤ B ↔ (A < B ∨ A = B)))
Theorem	znnnlt1 8069	An integer is not a positive integer iff it is less than one. (Contributed by NM, 13-Jul-2005.)
⊢ (𝑁 ∈ ℤ → (¬ 𝑁 ∈ ℕ ↔ 𝑁 < 1))
Theorem	zletr 8070	Transitive law of ordering for integers. (Contributed by Alexander van der Vekens, 3-Apr-2018.)
⊢ ((𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐽 ≤ 𝐾 ∧ 𝐾 ≤ 𝐿) → 𝐽 ≤ 𝐿))
Theorem	zrevaddcl 8071	Reverse closure law for addition of integers. (Contributed by NM, 11-May-2004.)
⊢ (𝑁 ∈ ℤ → ((𝑀 ∈ ℂ ∧ (𝑀 + 𝑁) ∈ ℤ) ↔ 𝑀 ∈ ℤ))
Theorem	znnsub 8072	The positive difference of unequal integers is a positive integer. (Generalization of nnsub 7733.) (Contributed by NM, 11-May-2004.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ))
Theorem	zmulcl 8073	Closure of multiplication of integers. (Contributed by NM, 30-Jul-2004.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 · 𝑁) ∈ ℤ)
Theorem	zltp1le 8074	Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))
Theorem	zleltp1 8075	Integer ordering relation. (Contributed by NM, 10-May-2004.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ 𝑀 < (𝑁 + 1)))
Theorem	zlem1lt 8076	Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁))
Theorem	zltlem1 8077	Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1)))
Theorem	zgt0ge1 8078	An integer greater than 0 is greater than or equal to 1. (Contributed by AV, 14-Oct-2018.)
⊢ (𝑍 ∈ ℤ → (0 < 𝑍 ↔ 1 ≤ 𝑍))
Theorem	nnleltp1 8079	Positive integer ordering relation. (Contributed by NM, 13-Aug-2001.) (Proof shortened by Mario Carneiro, 16-May-2014.)
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (A ≤ B ↔ A < (B + 1)))
Theorem	nnltp1le 8080	Positive integer ordering relation. (Contributed by NM, 19-Aug-2001.)
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (A < B ↔ (A + 1) ≤ B))
Theorem	nnaddm1cl 8081	Closure of addition of positive integers minus one. (Contributed by NM, 6-Aug-2003.) (Proof shortened by Mario Carneiro, 16-May-2014.)
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → ((A + B) − 1) ∈ ℕ)
Theorem	nn0ltp1le 8082	Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Dec-2002.) (Proof shortened by Mario Carneiro, 16-May-2014.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))
Theorem	nn0leltp1 8083	Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Apr-2004.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ≤ 𝑁 ↔ 𝑀 < (𝑁 + 1)))
Theorem	nn0ltlem1 8084	Nonnegative integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1)))
Theorem	znn0sub 8085	The nonnegative difference of integers is a nonnegative integer. (Generalization of nn0sub 8086.) (Contributed by NM, 14-Jul-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ0))
Theorem	nn0sub 8086	Subtraction of nonnegative integers. (Contributed by NM, 9-May-2004.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ≤ 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ0))
Theorem	nn0n0n1ge2 8087	A nonnegative integer which is neither 0 nor 1 is greater than or equal to 2. (Contributed by Alexander van der Vekens, 6-Dec-2017.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ∧ 𝑁 ≠ 1) → 2 ≤ 𝑁)
Theorem	elz2 8088*	Membership in the set of integers. Commonly used in constructions of the integers as equivalence classes under subtraction of the positive integers. (Contributed by Mario Carneiro, 16-May-2014.)
⊢ (𝑁 ∈ ℤ ↔ ∃x ∈ ℕ ∃y ∈ ℕ 𝑁 = (x − y))
Theorem	dfz2 8089	Alternative definition of the integers, based on elz2 8088. (Contributed by Mario Carneiro, 16-May-2014.)
⊢ ℤ = ( − “ (ℕ × ℕ))
Theorem	nn0sub2 8090	Subtraction of nonnegative integers. (Contributed by NM, 4-Sep-2005.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁) → (𝑁 − 𝑀) ∈ ℕ0)
Theorem	zapne 8091	Apartness is equivalent to not equal for integers. (Contributed by Jim Kingdon, 14-Mar-2020.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 # 𝑁 ↔ 𝑀 ≠ 𝑁))
Theorem	zdceq 8092	Equality of integers is decidable. (Contributed by Jim Kingdon, 14-Mar-2020.)
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → DECID A = B)
Theorem	zdcle 8093	Integer ≤ is decidable. (Contributed by Jim Kingdon, 7-Apr-2020.)
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → DECID A ≤ B)
Theorem	zdclt 8094	Integer < is decidable. (Contributed by Jim Kingdon, 1-Jun-2020.)
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → DECID A < B)
Theorem	zltlen 8095	Integer 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 7413 which is a similar result for complex numbers. (Contributed by Jim Kingdon, 14-Mar-2020.)
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → (A < B ↔ (A ≤ B ∧ B ≠ A)))
Theorem	nn0n0n1ge2b 8096	A nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by Alexander van der Vekens, 17-Jan-2018.)
⊢ (𝑁 ∈ ℕ0 → ((𝑁 ≠ 0 ∧ 𝑁 ≠ 1) ↔ 2 ≤ 𝑁))
Theorem	nn0lt10b 8097	A nonnegative integer less than 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝑁 ∈ ℕ0 → (𝑁 < 1 ↔ 𝑁 = 0))
Theorem	nn0lt2 8098	A nonnegative integer less than 2 must be 0 or 1. (Contributed by Alexander van der Vekens, 16-Sep-2018.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 < 2) → (𝑁 = 0 ∨ 𝑁 = 1))
Theorem	nn0lem1lt 8099	Nonnegative integer ordering relation. (Contributed by NM, 21-Jun-2005.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁))
Theorem	nnlem1lt 8100	Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁))