P. 119 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 11801-11900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ltsubpos 11801	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 11802	Comparison of two numbers whose difference is positive. (Contributed by NM, 17-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
Theorem	lesub1 11803	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 11804	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 11805	Subtraction from both sides of 'less than'. (Contributed by FL, 3-Jan-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 − 𝐶) < (𝐵 − 𝐶)))
Theorem	ltsub2 11806	Subtraction of both sides of 'less than'. (Contributed by NM, 29-Sep-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 − 𝐵) < (𝐶 − 𝐴)))
Theorem	lt2sub 11807	Subtracting both sides of two 'less than' relations. (Contributed by Mario Carneiro, 14-Apr-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐷 < 𝐵) → (𝐴 − 𝐵) < (𝐶 − 𝐷)))
Theorem	le2sub 11808	Subtracting both sides of two 'less than or equal to' relations. (Contributed by Mario Carneiro, 14-Apr-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵) → (𝐴 − 𝐵) ≤ (𝐶 − 𝐷)))
Theorem	ltneg 11809	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 11810	Contraposition of negative in 'less than'. (Contributed by NM, 8-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 < 𝐵 ↔ -𝐵 < 𝐴))
Theorem	ltnegcon2 11811	Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < -𝐵 ↔ 𝐵 < -𝐴))
Theorem	leneg 11812	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 11813	Contraposition of negative in 'less than or equal to'. (Contributed by NM, 10-May-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴))
Theorem	lenegcon2 11814	Contraposition of negative in 'less than or equal to'. (Contributed by NM, 8-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ -𝐵 ↔ 𝐵 ≤ -𝐴))
Theorem	lt0neg1 11815	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 11816	Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.)
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ -𝐴 < 0))
Theorem	le0neg1 11817	Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.)
⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴))
Theorem	le0neg2 11818	Comparison of a number and its negative to zero. (Contributed by NM, 24-Aug-1999.)
⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐴 ↔ -𝐴 ≤ 0))
Theorem	addge01 11819	A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 21-Feb-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐴 + 𝐵)))
Theorem	addge02 11820	A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 27-Jul-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 + 𝐴)))
Theorem	add20 11821	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 11822	Nonnegative subtraction. (Contributed by NM, 14-Mar-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴))
Theorem	suble0 11823	Nonpositive subtraction. (Contributed by NM, 20-Mar-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 0 ↔ 𝐴 ≤ 𝐵))
Theorem	leaddle0 11824	The sum of a real number and a second real number is less than the real number iff the second real number is negative. (Contributed by Alexander van der Vekens, 30-May-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐴 ↔ 𝐵 ≤ 0))
Theorem	subge02 11825	Nonnegative subtraction. (Contributed by NM, 27-Jul-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ (𝐴 − 𝐵) ≤ 𝐴))
Theorem	lesub0 11826	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	mulge0 11827	The product of two nonnegative numbers is nonnegative. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 · 𝐵))
Theorem	mullt0 11828	The product of two negative numbers is positive. (Contributed by Jeff Hankins, 8-Jun-2009.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐴 < 0) ∧ (𝐵 ∈ ℝ ∧ 𝐵 < 0)) → 0 < (𝐴 · 𝐵))
Theorem	msqgt0 11829	A nonzero square is positive. Theorem I.20 of [Apostol] p. 20. (Contributed by NM, 6-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 0 < (𝐴 · 𝐴))
Theorem	msqge0 11830	A square is nonnegative. (Contributed by NM, 23-May-2007.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℝ → 0 ≤ (𝐴 · 𝐴))
Theorem	0lt1 11831	0 is less than 1. Theorem I.21 of [Apostol] p. 20. (Contributed by NM, 17-Jan-1997.)
⊢ 0 < 1
Theorem	0le1 11832	0 is less than or equal to 1. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ 0 ≤ 1
Theorem	relin01 11833	An interval law for less than or equal. (Contributed by Scott Fenton, 27-Jun-2013.)
⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 0 ∨ (0 ≤ 𝐴 ∧ 𝐴 ≤ 1) ∨ 1 ≤ 𝐴))
Theorem	ltordlem 11834*	Lemma for ltord1 11835. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)    &   ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)    &   ⊢ 𝑆 ⊆ ℝ    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐴 < 𝐵))    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 < 𝐷 → 𝑀 < 𝑁))
Theorem	ltord1 11835*	Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)    &   ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)    &   ⊢ 𝑆 ⊆ ℝ    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐴 < 𝐵))    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 < 𝐷 ↔ 𝑀 < 𝑁))
Theorem	leord1 11836*	Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)    &   ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)    &   ⊢ 𝑆 ⊆ ℝ    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐴 < 𝐵))    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 ≤ 𝐷 ↔ 𝑀 ≤ 𝑁))
Theorem	eqord1 11837*	A strictly increasing real function on a subset of ℝ is one-to-one. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)    &   ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)    &   ⊢ 𝑆 ⊆ ℝ    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐴 < 𝐵))    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 = 𝐷 ↔ 𝑀 = 𝑁))
Theorem	ltord2 11838*	Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)    &   ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)    &   ⊢ 𝑆 ⊆ ℝ    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐵 < 𝐴))    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 < 𝐷 ↔ 𝑁 < 𝑀))
Theorem	leord2 11839*	Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)    &   ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)    &   ⊢ 𝑆 ⊆ ℝ    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐵 < 𝐴))    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 ≤ 𝐷 ↔ 𝑁 ≤ 𝑀))
Theorem	eqord2 11840*	A strictly decreasing real function on a subset of ℝ is one-to-one. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)    &   ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)    &   ⊢ 𝑆 ⊆ ℝ    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐵 < 𝐴))    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 = 𝐷 ↔ 𝑀 = 𝑁))
Theorem	wloglei 11841*	Form of wlogle 11842 where both sides of the equivalence are proven rather than showing that they are equivalent to each other. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝑧 = 𝑦 ∧ 𝑤 = 𝑥) → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 → 𝑆 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑥 ≤ 𝑦)) → 𝜃)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑥 ≤ 𝑦)) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝜒)
Theorem	wlogle 11842*	If the predicate 𝜒(𝑥, 𝑦) is symmetric under interchange of 𝑥, 𝑦, then "without loss of generality" we can assume that 𝑥 ≤ 𝑦. (Contributed by Mario Carneiro, 18-Aug-2014.) (Revised by Mario Carneiro, 11-Sep-2014.)
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝑧 = 𝑦 ∧ 𝑤 = 𝑥) → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 → 𝑆 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝜒 ↔ 𝜃))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑥 ≤ 𝑦)) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝜒)
Theorem	leidi 11843	'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 𝐴 ≤ 𝐴
Theorem	gt0ne0i 11844	Positive means nonzero (useful for ordering theorems involving division). (Contributed by NM, 16-Sep-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (0 < 𝐴 → 𝐴 ≠ 0)
Theorem	gt0ne0ii 11845	Positive implies nonzero. (Contributed by NM, 15-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 0 < 𝐴    ⇒   ⊢ 𝐴 ≠ 0
Theorem	msqgt0i 11846	A nonzero square is positive. Theorem I.20 of [Apostol] p. 20. (Contributed by NM, 17-Jan-1997.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (𝐴 ≠ 0 → 0 < (𝐴 · 𝐴))
Theorem	msqge0i 11847	A square is nonnegative. (Contributed by NM, 14-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 0 ≤ (𝐴 · 𝐴)
Theorem	addgt0i 11848	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 11849	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 11850	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 11851	Addition of 2 positive numbers is positive. (Contributed by NM, 18-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 0 < 𝐴    &   ⊢ 0 < 𝐵    ⇒   ⊢ 0 < (𝐴 + 𝐵)
Theorem	add20i 11852	Two nonnegative numbers are zero iff their sum is zero. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((𝐴 + 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
Theorem	ltnegi 11853	Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20. (Contributed by NM, 21-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 < 𝐵 ↔ -𝐵 < -𝐴)
Theorem	lenegi 11854	Negative of both sides of 'less than or equal to'. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 ≤ 𝐵 ↔ -𝐵 ≤ -𝐴)
Theorem	ltnegcon2i 11855	Contraposition of negative in 'less than'. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 < -𝐵 ↔ 𝐵 < -𝐴)
Theorem	mulge0i 11856	The product of two nonnegative numbers is nonnegative. (Contributed by NM, 30-Jul-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → 0 ≤ (𝐴 · 𝐵))
Theorem	lesub0i 11857	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 11858	Adding a positive number to another number increases it. (Contributed by NM, 25-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴))
Theorem	posdifi 11859	Comparison of two numbers whose difference is positive. (Contributed by NM, 19-Aug-2001.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))
Theorem	ltnegcon1i 11860	Contraposition of negative in 'less than'. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (-𝐴 < 𝐵 ↔ -𝐵 < 𝐴)
Theorem	lenegcon1i 11861	Contraposition of negative in 'less than or equal to'. (Contributed by NM, 6-Apr-2005.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (-𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴)
Theorem	subge0i 11862	Nonnegative subtraction. (Contributed by NM, 13-Aug-2000.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴)
Theorem	ltadd1i 11863	Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20. (Contributed by NM, 21-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (𝐴 < 𝐵 ↔ (𝐴 + 𝐶) < (𝐵 + 𝐶))
Theorem	leadd1i 11864	Addition to both sides of 'less than or equal to'. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (𝐴 ≤ 𝐵 ↔ (𝐴 + 𝐶) ≤ (𝐵 + 𝐶))
Theorem	leadd2i 11865	Addition to both sides of 'less than or equal to'. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (𝐴 ≤ 𝐵 ↔ (𝐶 + 𝐴) ≤ (𝐶 + 𝐵))
Theorem	ltsubaddi 11866	'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵))
Theorem	lesubaddi 11867	'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 11868	'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶))
Theorem	lesubadd2i 11869	'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 3-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐵 + 𝐶))
Theorem	ltaddsubi 11870	'Less than' relationship between subtraction and addition. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵))
Theorem	lt2addi 11871	Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 𝐷 ∈ ℝ    ⇒   ⊢ ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))
Theorem	le2addi 11872	Adding both side of two inequalities. (Contributed by NM, 16-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 𝐷 ∈ ℝ    ⇒   ⊢ ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷))
Theorem	gt0ne0d 11873	Positive implies nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0)
Theorem	lt0ne0d 11874	Something less than zero is not zero. Deduction form. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 < 0)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0)
Theorem	leidd 11875	'Less than or equal to' is reflexive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐴)
Theorem	msqgt0d 11876	A nonzero square is positive. Theorem I.20 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → 0 < (𝐴 · 𝐴))
Theorem	msqge0d 11877	A square is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐴))
Theorem	lt0neg1d 11878	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 11879	Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (0 < 𝐴 ↔ -𝐴 < 0))
Theorem	le0neg1d 11880	Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴))
Theorem	le0neg2d 11881	Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (0 ≤ 𝐴 ↔ -𝐴 ≤ 0))
Theorem	addgegt0d 11882	Addition of nonnegative and positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → 0 < (𝐴 + 𝐵))
Theorem	addgtge0d 11883	Addition of positive and nonnegative numbers is positive. (Contributed by Asger C. Ipsen, 12-May-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 0 < (𝐴 + 𝐵))
Theorem	addgt0d 11884	Addition of 2 positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → 0 < (𝐴 + 𝐵))
Theorem	addge0d 11885	Addition of 2 nonnegative numbers is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴 + 𝐵))
Theorem	mulge0d 11886	The product of two nonnegative numbers is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵))
Theorem	ltnegd 11887	Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ -𝐵 < -𝐴))
Theorem	lenegd 11888	Negative of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ -𝐵 ≤ -𝐴))
Theorem	ltnegcon1d 11889	Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → -𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → -𝐵 < 𝐴)
Theorem	ltnegcon2d 11890	Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < -𝐵)    ⇒   ⊢ (𝜑 → 𝐵 < -𝐴)
Theorem	lenegcon1d 11891	Contraposition of negative in 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → -𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → -𝐵 ≤ 𝐴)
Theorem	lenegcon2d 11892	Contraposition of negative in 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ -𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≤ -𝐴)
Theorem	ltaddposd 11893	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴)))
Theorem	ltaddpos2d 11894	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (0 < 𝐴 ↔ 𝐵 < (𝐴 + 𝐵)))
Theorem	ltsubposd 11895	Subtracting a positive number from another number decreases it. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (0 < 𝐴 ↔ (𝐵 − 𝐴) < 𝐵))
Theorem	posdifd 11896	Comparison of two numbers whose difference is positive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
Theorem	addge01d 11897	A number is less than or equal to itself plus a nonnegative number. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐴 + 𝐵)))
Theorem	addge02d 11898	A number is less than or equal to itself plus a nonnegative number. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 + 𝐴)))
Theorem	subge0d 11899	Nonnegative subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴))
Theorem	suble0d 11900	Nonpositive subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) ≤ 0 ↔ 𝐴 ≤ 𝐵))