P. 117 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 11601-11700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	subaddmulsub 11601	The difference with a product of a sum and a difference. (Contributed by AV, 5-Mar-2023.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ) ∧ 𝐸 ∈ ℂ) → (𝐸 − ((𝐴 + 𝐵) · (𝐶 − 𝐷))) = (((𝐸 − (𝐴 · 𝐶)) − (𝐵 · 𝐶)) + ((𝐴 · 𝐷) + (𝐵 · 𝐷))))
Theorem	mulsubaddmulsub 11602	A special difference of a product with a product of a sum and a difference. (Contributed by AV, 5-Mar-2023.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐵 · 𝐶) − ((𝐴 + 𝐵) · (𝐶 − 𝐷))) = (((𝐴 · 𝐷) + (𝐵 · 𝐷)) − (𝐴 · 𝐶)))
5.3.4  Ordering on reals (cont.)
Theorem	gt0ne0 11603	Positive implies nonzero. (Contributed by NM, 3-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 ≠ 0)
Theorem	lt0ne0 11604	A number which is less than zero is not zero. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 0) → 𝐴 ≠ 0)
Theorem	ltadd1 11605	Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 + 𝐶) < (𝐵 + 𝐶)))
Theorem	leadd1 11606	Addition to both sides of 'less than or equal to'. (Contributed by NM, 18-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 + 𝐶) ≤ (𝐵 + 𝐶)))
Theorem	leadd2 11607	Addition to both sides of 'less than or equal to'. (Contributed by NM, 26-Oct-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐶 + 𝐴) ≤ (𝐶 + 𝐵)))
Theorem	ltsubadd 11608	'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵)))
Theorem	ltsubadd2 11609	'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶)))
Theorem	lesubadd 11610	'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 17-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 + 𝐵)))
Theorem	lesubadd2 11611	'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 10-Aug-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐵 + 𝐶)))
Theorem	ltaddsub 11612	'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵)))
Theorem	ltaddsub2 11613	'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐵 < (𝐶 − 𝐴)))
Theorem	leaddsub 11614	'Less than or equal to' relationship between addition and subtraction. (Contributed by NM, 6-Apr-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 − 𝐵)))
Theorem	leaddsub2 11615	'Less than or equal to' relationship between and addition and subtraction. (Contributed by NM, 6-Apr-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐵 ≤ (𝐶 − 𝐴)))
Theorem	suble 11616	Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ (𝐴 − 𝐶) ≤ 𝐵))
Theorem	lesub 11617	Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ (𝐵 − 𝐶) ↔ 𝐶 ≤ (𝐵 − 𝐴)))
Theorem	ltsub23 11618	'Less than' relationship between subtraction and addition. (Contributed by NM, 4-Oct-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ (𝐴 − 𝐶) < 𝐵))
Theorem	ltsub13 11619	'Less than' relationship between subtraction and addition. (Contributed by NM, 17-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < (𝐵 − 𝐶) ↔ 𝐶 < (𝐵 − 𝐴)))
Theorem	le2add 11620	Adding both sides of two 'less than or equal to' relations. (Contributed by NM, 17-Apr-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷)))
Theorem	ltleadd 11621	Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷)))
Theorem	leltadd 11622	Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷)))
Theorem	lt2add 11623	Adding both sides of two 'less than' relations. Theorem I.25 of [Apostol] p. 20. (Contributed by NM, 15-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷)))
Theorem	addgt0 11624	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 11625	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 11626	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 11627	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 11628	Adding a positive number to another number increases it. (Contributed by NM, 17-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴)))
Theorem	ltaddpos2 11629	Adding a positive number to another number increases it. (Contributed by NM, 8-Apr-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐴 + 𝐵)))
Theorem	ltsubpos 11630	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 11631	Comparison of two numbers whose difference is positive. (Contributed by NM, 17-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
Theorem	lesub1 11632	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 11633	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 11634	Subtraction from both sides of 'less than'. (Contributed by FL, 3-Jan-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 − 𝐶) < (𝐵 − 𝐶)))
Theorem	ltsub2 11635	Subtraction of both sides of 'less than'. (Contributed by NM, 29-Sep-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 − 𝐵) < (𝐶 − 𝐴)))
Theorem	lt2sub 11636	Subtracting both sides of two 'less than' relations. (Contributed by Mario Carneiro, 14-Apr-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐷 < 𝐵) → (𝐴 − 𝐵) < (𝐶 − 𝐷)))
Theorem	le2sub 11637	Subtracting both sides of two 'less than or equal to' relations. (Contributed by Mario Carneiro, 14-Apr-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵) → (𝐴 − 𝐵) ≤ (𝐶 − 𝐷)))
Theorem	ltneg 11638	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 11639	Contraposition of negative in 'less than'. (Contributed by NM, 8-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 < 𝐵 ↔ -𝐵 < 𝐴))
Theorem	ltnegcon2 11640	Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < -𝐵 ↔ 𝐵 < -𝐴))
Theorem	leneg 11641	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 11642	Contraposition of negative in 'less than or equal to'. (Contributed by NM, 10-May-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴))
Theorem	lenegcon2 11643	Contraposition of negative in 'less than or equal to'. (Contributed by NM, 8-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ -𝐵 ↔ 𝐵 ≤ -𝐴))
Theorem	lt0neg1 11644	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 11645	Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.)
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ -𝐴 < 0))
Theorem	le0neg1 11646	Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.)
⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴))
Theorem	le0neg2 11647	Comparison of a number and its negative to zero. (Contributed by NM, 24-Aug-1999.)
⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐴 ↔ -𝐴 ≤ 0))
Theorem	addge01 11648	A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 21-Feb-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐴 + 𝐵)))
Theorem	addge02 11649	A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 27-Jul-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 + 𝐴)))
Theorem	add20 11650	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 11651	Nonnegative subtraction. (Contributed by NM, 14-Mar-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴))
Theorem	suble0 11652	Nonpositive subtraction. (Contributed by NM, 20-Mar-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 0 ↔ 𝐴 ≤ 𝐵))
Theorem	leaddle0 11653	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 11654	Nonnegative subtraction. (Contributed by NM, 27-Jul-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ (𝐴 − 𝐵) ≤ 𝐴))
Theorem	lesub0 11655	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 11656	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 11657	The product of two negative numbers is positive. (Contributed by Jeff Hankins, 8-Jun-2009.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐴 < 0) ∧ (𝐵 ∈ ℝ ∧ 𝐵 < 0)) → 0 < (𝐴 · 𝐵))
Theorem	msqgt0 11658	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 11659	A square is nonnegative. (Contributed by NM, 23-May-2007.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℝ → 0 ≤ (𝐴 · 𝐴))
Theorem	0lt1 11660	0 is less than 1. Theorem I.21 of [Apostol] p. 20. (Contributed by NM, 17-Jan-1997.)
⊢ 0 < 1
Theorem	0le1 11661	0 is less than or equal to 1. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ 0 ≤ 1
Theorem	relin01 11662	An interval law for less than or equal. (Contributed by Scott Fenton, 27-Jun-2013.)
⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 0 ∨ (0 ≤ 𝐴 ∧ 𝐴 ≤ 1) ∨ 1 ≤ 𝐴))
Theorem	ltordlem 11663*	Lemma for ltord1 11664. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)    &   ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)    &   ⊢ 𝑆 ⊆ ℝ    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐴 < 𝐵))    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 < 𝐷 → 𝑀 < 𝑁))
Theorem	ltord1 11664*	Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)    &   ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)    &   ⊢ 𝑆 ⊆ ℝ    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐴 < 𝐵))    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 < 𝐷 ↔ 𝑀 < 𝑁))
Theorem	leord1 11665*	Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)    &   ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)    &   ⊢ 𝑆 ⊆ ℝ    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐴 < 𝐵))    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 ≤ 𝐷 ↔ 𝑀 ≤ 𝑁))
Theorem	eqord1 11666*	A strictly increasing real function on a subset of ℝ is one-to-one. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)    &   ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)    &   ⊢ 𝑆 ⊆ ℝ    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐴 < 𝐵))    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 = 𝐷 ↔ 𝑀 = 𝑁))
Theorem	ltord2 11667*	Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)    &   ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)    &   ⊢ 𝑆 ⊆ ℝ    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐵 < 𝐴))    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 < 𝐷 ↔ 𝑁 < 𝑀))
Theorem	leord2 11668*	Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)    &   ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)    &   ⊢ 𝑆 ⊆ ℝ    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐵 < 𝐴))    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 ≤ 𝐷 ↔ 𝑁 ≤ 𝑀))
Theorem	eqord2 11669*	A strictly decreasing real function on a subset of ℝ is one-to-one. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)    &   ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)    &   ⊢ 𝑆 ⊆ ℝ    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐵 < 𝐴))    ⇒   ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 = 𝐷 ↔ 𝑀 = 𝑁))
Theorem	wloglei 11670*	Form of wlogle 11671 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 11671*	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 11672	'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 𝐴 ≤ 𝐴
Theorem	gt0ne0i 11673	Positive means nonzero (useful for ordering theorems involving division). (Contributed by NM, 16-Sep-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (0 < 𝐴 → 𝐴 ≠ 0)
Theorem	gt0ne0ii 11674	Positive implies nonzero. (Contributed by NM, 15-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 0 < 𝐴    ⇒   ⊢ 𝐴 ≠ 0
Theorem	msqgt0i 11675	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 11676	A square is nonnegative. (Contributed by NM, 14-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 0 ≤ (𝐴 · 𝐴)
Theorem	addgt0i 11677	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 11678	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 11679	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 11680	Addition of 2 positive numbers is positive. (Contributed by NM, 18-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 0 < 𝐴    &   ⊢ 0 < 𝐵    ⇒   ⊢ 0 < (𝐴 + 𝐵)
Theorem	add20i 11681	Two nonnegative numbers are zero iff their sum is zero. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((𝐴 + 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
Theorem	ltnegi 11682	Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20. (Contributed by NM, 21-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 < 𝐵 ↔ -𝐵 < -𝐴)
Theorem	lenegi 11683	Negative of both sides of 'less than or equal to'. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 ≤ 𝐵 ↔ -𝐵 ≤ -𝐴)
Theorem	ltnegcon2i 11684	Contraposition of negative in 'less than'. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 < -𝐵 ↔ 𝐵 < -𝐴)
Theorem	mulge0i 11685	The product of two nonnegative numbers is nonnegative. (Contributed by NM, 30-Jul-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → 0 ≤ (𝐴 · 𝐵))
Theorem	lesub0i 11686	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 11687	Adding a positive number to another number increases it. (Contributed by NM, 25-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴))
Theorem	posdifi 11688	Comparison of two numbers whose difference is positive. (Contributed by NM, 19-Aug-2001.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))
Theorem	ltnegcon1i 11689	Contraposition of negative in 'less than'. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (-𝐴 < 𝐵 ↔ -𝐵 < 𝐴)
Theorem	lenegcon1i 11690	Contraposition of negative in 'less than or equal to'. (Contributed by NM, 6-Apr-2005.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (-𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴)
Theorem	subge0i 11691	Nonnegative subtraction. (Contributed by NM, 13-Aug-2000.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴)
Theorem	ltadd1i 11692	Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20. (Contributed by NM, 21-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (𝐴 < 𝐵 ↔ (𝐴 + 𝐶) < (𝐵 + 𝐶))
Theorem	leadd1i 11693	Addition to both sides of 'less than or equal to'. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (𝐴 ≤ 𝐵 ↔ (𝐴 + 𝐶) ≤ (𝐵 + 𝐶))
Theorem	leadd2i 11694	Addition to both sides of 'less than or equal to'. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (𝐴 ≤ 𝐵 ↔ (𝐶 + 𝐴) ≤ (𝐶 + 𝐵))
Theorem	ltsubaddi 11695	'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵))
Theorem	lesubaddi 11696	'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 11697	'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶))
Theorem	lesubadd2i 11698	'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 3-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐵 + 𝐶))
Theorem	ltaddsubi 11699	'Less than' relationship between subtraction and addition. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵))
Theorem	lt2addi 11700	Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 𝐷 ∈ ℝ    ⇒   ⊢ ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))