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	ltleadd 8201	Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷)))
Theorem	leltadd 8202	Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷)))
Theorem	addgt0 8203	The sum of 2 positive numbers is positive. (Contributed by NM, 1-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐴 ∧ 0 < 𝐵)) → 0 < (𝐴 + 𝐵))
Theorem	addgegt0 8204	The sum of nonnegative and positive numbers is positive. (Contributed by NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 < 𝐵)) → 0 < (𝐴 + 𝐵))
Theorem	addgtge0 8205	The sum of nonnegative and positive numbers is positive. (Contributed by NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐴 ∧ 0 ≤ 𝐵)) → 0 < (𝐴 + 𝐵))
Theorem	addge0 8206	The sum of 2 nonnegative numbers is nonnegative. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 + 𝐵))
Theorem	ltaddpos 8207	Adding a positive number to another number increases it. (Contributed by NM, 17-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴)))
Theorem	ltaddpos2 8208	Adding a positive number to another number increases it. (Contributed by NM, 8-Apr-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐴 + 𝐵)))
Theorem	ltsubpos 8209	Subtracting a positive number from another number decreases it. (Contributed by NM, 17-Nov-2004.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ (𝐵 − 𝐴) < 𝐵))
Theorem	posdif 8210	Comparison of two numbers whose difference is positive. (Contributed by NM, 17-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
Theorem	lesub1 8211	Subtraction from both sides of 'less than or equal to'. (Contributed by NM, 13-May-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 − 𝐶) ≤ (𝐵 − 𝐶)))
Theorem	lesub2 8212	Subtraction of both sides of 'less than or equal to'. (Contributed by NM, 29-Sep-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐶 − 𝐵) ≤ (𝐶 − 𝐴)))
Theorem	ltsub1 8213	Subtraction from both sides of 'less than'. (Contributed by FL, 3-Jan-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 − 𝐶) < (𝐵 − 𝐶)))
Theorem	ltsub2 8214	Subtraction of both sides of 'less than'. (Contributed by NM, 29-Sep-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 − 𝐵) < (𝐶 − 𝐴)))
Theorem	lt2sub 8215	Subtracting both sides of two 'less than' relations. (Contributed by Mario Carneiro, 14-Apr-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐷 < 𝐵) → (𝐴 − 𝐵) < (𝐶 − 𝐷)))
Theorem	le2sub 8216	Subtracting both sides of two 'less than or equal to' relations. (Contributed by Mario Carneiro, 14-Apr-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵) → (𝐴 − 𝐵) ≤ (𝐶 − 𝐷)))
Theorem	ltneg 8217	Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20. (Contributed by NM, 27-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ -𝐵 < -𝐴))
Theorem	ltnegcon1 8218	Contraposition of negative in 'less than'. (Contributed by NM, 8-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 < 𝐵 ↔ -𝐵 < 𝐴))
Theorem	ltnegcon2 8219	Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < -𝐵 ↔ 𝐵 < -𝐴))
Theorem	leneg 8220	Negative of both sides of 'less than or equal to'. (Contributed by NM, 12-Sep-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ -𝐵 ≤ -𝐴))
Theorem	lenegcon1 8221	Contraposition of negative in 'less than or equal to'. (Contributed by NM, 10-May-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴))
Theorem	lenegcon2 8222	Contraposition of negative in 'less than or equal to'. (Contributed by NM, 8-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ -𝐵 ↔ 𝐵 ≤ -𝐴))
Theorem	lt0neg1 8223	Comparison of a number and its negative to zero. Theorem I.23 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.)
⊢ (𝐴 ∈ ℝ → (𝐴 < 0 ↔ 0 < -𝐴))
Theorem	lt0neg2 8224	Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.)
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ -𝐴 < 0))
Theorem	le0neg1 8225	Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.)
⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴))
Theorem	le0neg2 8226	Comparison of a number and its negative to zero. (Contributed by NM, 24-Aug-1999.)
⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐴 ↔ -𝐴 ≤ 0))
Theorem	addge01 8227	A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 21-Feb-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐴 + 𝐵)))
Theorem	addge02 8228	A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 27-Jul-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 + 𝐴)))
Theorem	add20 8229	Two nonnegative numbers are zero iff their sum is zero. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 + 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
Theorem	subge0 8230	Nonnegative subtraction. (Contributed by NM, 14-Mar-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴))
Theorem	suble0 8231	Nonpositive subtraction. (Contributed by NM, 20-Mar-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 0 ↔ 𝐴 ≤ 𝐵))
Theorem	leaddle0 8232	The sum of a real number and a second real number is less then the real number iff the second real number is negative. (Contributed by Alexander van der Vekens, 30-May-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐴 ↔ 𝐵 ≤ 0))
Theorem	subge02 8233	Nonnegative subtraction. (Contributed by NM, 27-Jul-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ (𝐴 − 𝐵) ≤ 𝐴))
Theorem	lesub0 8234	Lemma to show a nonnegative number is zero. (Contributed by NM, 8-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 ≤ 𝐴 ∧ 𝐵 ≤ (𝐵 − 𝐴)) ↔ 𝐴 = 0))
Theorem	mullt0 8235	The product of two negative numbers is positive. (Contributed by Jeff Hankins, 8-Jun-2009.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐴 < 0) ∧ (𝐵 ∈ ℝ ∧ 𝐵 < 0)) → 0 < (𝐴 · 𝐵))
Theorem	0le1 8236	0 is less than or equal to 1. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ 0 ≤ 1
Theorem	ltordlem 8237*	Lemma for eqord1 8238. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)    &   ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)    &   ⊢ 𝑆 ⊆ ℝ    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐴 < 𝐵))    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 < 𝐷 → 𝑀 < 𝑁))
Theorem	eqord1 8238*	A strictly increasing real function on a subset of ℝ is one-to-one. (Contributed by Mario Carneiro, 14-Jun-2014.) (Revised by Jim Kingdon, 20-Dec-2022.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)    &   ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)    &   ⊢ 𝑆 ⊆ ℝ    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐴 < 𝐵))    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 = 𝐷 ↔ 𝑀 = 𝑁))
Theorem	eqord2 8239*	A strictly decreasing real function on a subset of ℝ is one-to-one. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)    &   ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)    &   ⊢ 𝑆 ⊆ ℝ    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐵 < 𝐴))    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 = 𝐷 ↔ 𝑀 = 𝑁))
Theorem	leidi 8240	'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 𝐴 ≤ 𝐴
Theorem	gt0ne0i 8241	Positive means nonzero (useful for ordering theorems involving division). (Contributed by NM, 16-Sep-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (0 < 𝐴 → 𝐴 ≠ 0)
Theorem	gt0ne0ii 8242	Positive implies nonzero. (Contributed by NM, 15-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 0 < 𝐴    ⇒   ⊢ 𝐴 ≠ 0
Theorem	addgt0i 8243	Addition of 2 positive numbers is positive. (Contributed by NM, 16-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 + 𝐵))
Theorem	addge0i 8244	Addition of 2 nonnegative numbers is nonnegative. (Contributed by NM, 28-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → 0 ≤ (𝐴 + 𝐵))
Theorem	addgegt0i 8245	Addition of nonnegative and positive numbers is positive. (Contributed by NM, 25-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 + 𝐵))
Theorem	addgt0ii 8246	Addition of 2 positive numbers is positive. (Contributed by NM, 18-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 0 < 𝐴    &   ⊢ 0 < 𝐵    ⇒   ⊢ 0 < (𝐴 + 𝐵)
Theorem	add20i 8247	Two nonnegative numbers are zero iff their sum is zero. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((𝐴 + 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
Theorem	ltnegi 8248	Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20. (Contributed by NM, 21-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 < 𝐵 ↔ -𝐵 < -𝐴)
Theorem	lenegi 8249	Negative of both sides of 'less than or equal to'. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 ≤ 𝐵 ↔ -𝐵 ≤ -𝐴)
Theorem	ltnegcon2i 8250	Contraposition of negative in 'less than'. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 < -𝐵 ↔ 𝐵 < -𝐴)
Theorem	lesub0i 8251	Lemma to show a nonnegative number is zero. (Contributed by NM, 8-Oct-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 𝐵 ≤ (𝐵 − 𝐴)) ↔ 𝐴 = 0)
Theorem	ltaddposi 8252	Adding a positive number to another number increases it. (Contributed by NM, 25-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴))
Theorem	posdifi 8253	Comparison of two numbers whose difference is positive. (Contributed by NM, 19-Aug-2001.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))
Theorem	ltnegcon1i 8254	Contraposition of negative in 'less than'. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (-𝐴 < 𝐵 ↔ -𝐵 < 𝐴)
Theorem	lenegcon1i 8255	Contraposition of negative in 'less than or equal to'. (Contributed by NM, 6-Apr-2005.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (-𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴)
Theorem	subge0i 8256	Nonnegative subtraction. (Contributed by NM, 13-Aug-2000.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴)
Theorem	ltadd1i 8257	Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20. (Contributed by NM, 21-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (𝐴 < 𝐵 ↔ (𝐴 + 𝐶) < (𝐵 + 𝐶))
Theorem	leadd1i 8258	Addition to both sides of 'less than or equal to'. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (𝐴 ≤ 𝐵 ↔ (𝐴 + 𝐶) ≤ (𝐵 + 𝐶))
Theorem	leadd2i 8259	Addition to both sides of 'less than or equal to'. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (𝐴 ≤ 𝐵 ↔ (𝐶 + 𝐴) ≤ (𝐶 + 𝐵))
Theorem	ltsubaddi 8260	'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵))
Theorem	lesubaddi 8261	'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 30-Sep-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 + 𝐵))
Theorem	ltsubadd2i 8262	'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶))
Theorem	lesubadd2i 8263	'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 3-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐵 + 𝐶))
Theorem	ltaddsubi 8264	'Less than' relationship between subtraction and addition. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵))
Theorem	lt2addi 8265	Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 𝐷 ∈ ℝ    ⇒   ⊢ ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))
Theorem	le2addi 8266	Adding both side of two inequalities. (Contributed by NM, 16-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 𝐷 ∈ ℝ    ⇒   ⊢ ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷))
Theorem	gt0ne0d 8267	Positive implies nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0)
Theorem	lt0ne0d 8268	Something less than zero is not zero. Deduction form. See also lt0ap0d 8404 which is similar but for apartness. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 < 0)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0)
Theorem	leidd 8269	'Less than or equal to' is reflexive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐴)
Theorem	lt0neg1d 8270	Comparison of a number and its negative to zero. Theorem I.23 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 < 0 ↔ 0 < -𝐴))
Theorem	lt0neg2d 8271	Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (0 < 𝐴 ↔ -𝐴 < 0))
Theorem	le0neg1d 8272	Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴))
Theorem	le0neg2d 8273	Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (0 ≤ 𝐴 ↔ -𝐴 ≤ 0))
Theorem	addgegt0d 8274	Addition of nonnegative and positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → 0 < (𝐴 + 𝐵))
Theorem	addgtge0d 8275	Addition of positive and nonnegative numbers is positive. (Contributed by Asger C. Ipsen, 12-May-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 0 < (𝐴 + 𝐵))
Theorem	addgt0d 8276	Addition of 2 positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → 0 < (𝐴 + 𝐵))
Theorem	addge0d 8277	Addition of 2 nonnegative numbers is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴 + 𝐵))
Theorem	ltnegd 8278	Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ -𝐵 < -𝐴))
Theorem	lenegd 8279	Negative of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ -𝐵 ≤ -𝐴))
Theorem	ltnegcon1d 8280	Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → -𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → -𝐵 < 𝐴)
Theorem	ltnegcon2d 8281	Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < -𝐵)    ⇒   ⊢ (𝜑 → 𝐵 < -𝐴)
Theorem	lenegcon1d 8282	Contraposition of negative in 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → -𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → -𝐵 ≤ 𝐴)
Theorem	lenegcon2d 8283	Contraposition of negative in 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ -𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≤ -𝐴)
Theorem	ltaddposd 8284	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴)))
Theorem	ltaddpos2d 8285	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (0 < 𝐴 ↔ 𝐵 < (𝐴 + 𝐵)))
Theorem	ltsubposd 8286	Subtracting a positive number from another number decreases it. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (0 < 𝐴 ↔ (𝐵 − 𝐴) < 𝐵))
Theorem	posdifd 8287	Comparison of two numbers whose difference is positive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
Theorem	addge01d 8288	A number is less than or equal to itself plus a nonnegative number. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐴 + 𝐵)))
Theorem	addge02d 8289	A number is less than or equal to itself plus a nonnegative number. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 + 𝐴)))
Theorem	subge0d 8290	Nonnegative subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴))
Theorem	suble0d 8291	Nonpositive subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) ≤ 0 ↔ 𝐴 ≤ 𝐵))
Theorem	subge02d 8292	Nonnegative subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (0 ≤ 𝐵 ↔ (𝐴 − 𝐵) ≤ 𝐴))
Theorem	ltadd1d 8293	Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 + 𝐶) < (𝐵 + 𝐶)))
Theorem	leadd1d 8294	Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 + 𝐶) ≤ (𝐵 + 𝐶)))
Theorem	leadd2d 8295	Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐶 + 𝐴) ≤ (𝐶 + 𝐵)))
Theorem	ltsubaddd 8296	'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵)))
Theorem	lesubaddd 8297	'Less than or equal to' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 + 𝐵)))
Theorem	ltsubadd2d 8298	'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶)))
Theorem	lesubadd2d 8299	'Less than or equal to' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐵 + 𝐶)))
Theorem	ltaddsubd 8300	'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵)))