P. 89 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8801-8900   *Has distinct variable group(s)

Type	Label	Description
Statement
4.3.9  Ordering on reals (cont.)
Theorem	ltp1 8801	A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))
Theorem	lep1 8802	A number is less than or equal to itself plus 1. (Contributed by NM, 5-Jan-2006.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (𝐴 + 1))
Theorem	ltm1 8803	A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006.)
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) < 𝐴)
Theorem	lem1 8804	A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) ≤ 𝐴)
Theorem	letrp1 8805	A transitive property of 'less than or equal' and plus 1. (Contributed by NM, 5-Aug-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ (𝐵 + 1))
Theorem	p1le 8806	A transitive property of plus 1 and 'less than or equal'. (Contributed by NM, 16-Aug-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 + 1) ≤ 𝐵) → 𝐴 ≤ 𝐵)
Theorem	recgt0 8807	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 25-Aug-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 0 < (1 / 𝐴))
Theorem	prodgt0gt0 8808	Infer that a multiplicand is positive from a positive multiplier and positive product. See prodgt0 8809 for the same theorem with 0 < 𝐴 replaced by the weaker condition 0 ≤ 𝐴. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐴 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐵)
Theorem	prodgt0 8809	Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 24-Apr-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐵)
Theorem	prodgt02 8810	Infer that a multiplier is positive from a nonnegative multiplicand and positive product. (Contributed by NM, 24-Apr-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐵 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐴)
Theorem	prodge0 8811	Infer that a multiplicand is nonnegative from a positive multiplier and nonnegative product. (Contributed by NM, 2-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐴 ∧ 0 ≤ (𝐴 · 𝐵))) → 0 ≤ 𝐵)
Theorem	prodge02 8812	Infer that a multiplier is nonnegative from a positive multiplicand and nonnegative product. (Contributed by NM, 2-Jul-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐵 ∧ 0 ≤ (𝐴 · 𝐵))) → 0 ≤ 𝐴)
Theorem	ltmul2 8813	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 13-Feb-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 < 𝐵 ↔ (𝐶 · 𝐴) < (𝐶 · 𝐵)))
Theorem	lemul2 8814	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 16-Mar-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)))
Theorem	lemul1a 8815	Multiplication of both sides of 'less than or equal to' by a nonnegative number. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 21-Feb-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))
Theorem	lemul2a 8816	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))
Theorem	ltmul12a 8817	Comparison of product of two positive numbers. (Contributed by NM, 30-Dec-2005.)
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 ≤ 𝐶 ∧ 𝐶 < 𝐷))) → (𝐴 · 𝐶) < (𝐵 · 𝐷))
Theorem	lemul12b 8818	Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.)
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))) → ((𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷)))
Theorem	lemul12a 8819	Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.)
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ) ∧ ((𝐶 ∈ ℝ ∧ 0 ≤ 𝐶) ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷)))
Theorem	mulgt1 8820	The product of two numbers greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) → 1 < (𝐴 · 𝐵))
Theorem	ltmulgt11 8821	Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴) → (1 < 𝐵 ↔ 𝐴 < (𝐴 · 𝐵)))
Theorem	ltmulgt12 8822	Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴) → (1 < 𝐵 ↔ 𝐴 < (𝐵 · 𝐴)))
Theorem	lemulge11 8823	Multiplication by a number greater than or equal to 1. (Contributed by NM, 17-Dec-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 1 ≤ 𝐵)) → 𝐴 ≤ (𝐴 · 𝐵))
Theorem	lemulge12 8824	Multiplication by a number greater than or equal to 1. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 1 ≤ 𝐵)) → 𝐴 ≤ (𝐵 · 𝐴))
Theorem	ltdiv1 8825	Division of both sides of 'less than' by a positive number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶)))
Theorem	lediv1 8826	Division of both sides of a less than or equal to relation by a positive number. (Contributed by NM, 18-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐴 / 𝐶) ≤ (𝐵 / 𝐶)))
Theorem	gt0div 8827	Division of a positive number by a positive number. (Contributed by NM, 28-Sep-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 < 𝐴 ↔ 0 < (𝐴 / 𝐵)))
Theorem	ge0div 8828	Division of a nonnegative number by a positive number. (Contributed by NM, 28-Sep-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 𝐵)))
Theorem	divgt0 8829	The ratio of two positive numbers is positive. (Contributed by NM, 12-Oct-1999.)
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 < (𝐴 / 𝐵))
Theorem	divge0 8830	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 27-Sep-1999.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ (𝐴 / 𝐵))
Theorem	ltmuldiv 8831	'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 · 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶)))
Theorem	ltmuldiv2 8832	'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 · 𝐴) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶)))
Theorem	ltdivmul 8833	'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐶 · 𝐵)))
Theorem	ledivmul 8834	'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐶 · 𝐵)))
Theorem	ltdivmul2 8835	'Less than' relationship between division and multiplication. (Contributed by NM, 24-Feb-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 · 𝐶)))
Theorem	lt2mul2div 8836	'Less than' relationship between division and multiplication. (Contributed by NM, 8-Jan-2006.)
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷))) → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ (𝐴 / 𝐷) < (𝐶 / 𝐵)))
Theorem	ledivmul2 8837	'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 · 𝐶)))
Theorem	lemuldiv 8838	'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 · 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶)))
Theorem	lemuldiv2 8839	'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 · 𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶)))
Theorem	ltrec 8840	The reciprocal of both sides of 'less than'. (Contributed by NM, 26-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴)))
Theorem	lerec 8841	The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 3-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 ≤ 𝐵 ↔ (1 / 𝐵) ≤ (1 / 𝐴)))
Theorem	lt2msq1 8842	Lemma for lt2msq 8843. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐴 · 𝐴) < (𝐵 · 𝐵))
Theorem	lt2msq 8843	Two nonnegative numbers compare the same as their squares. (Contributed by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 < 𝐵 ↔ (𝐴 · 𝐴) < (𝐵 · 𝐵)))
Theorem	ltdiv2 8844	Division of a positive number by both sides of 'less than'. (Contributed by NM, 27-Apr-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 < 𝐵 ↔ (𝐶 / 𝐵) < (𝐶 / 𝐴)))
Theorem	ltrec1 8845	Reciprocal swap in a 'less than' relation. (Contributed by NM, 24-Feb-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((1 / 𝐴) < 𝐵 ↔ (1 / 𝐵) < 𝐴))
Theorem	lerec2 8846	Reciprocal swap in a 'less than or equal to' relation. (Contributed by NM, 24-Feb-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 ≤ (1 / 𝐵) ↔ 𝐵 ≤ (1 / 𝐴)))
Theorem	ledivdiv 8847	Invert ratios of positive numbers and swap their ordering. (Contributed by NM, 9-Jan-2006.)
⊢ ((((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 0 < 𝐶) ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷))) → ((𝐴 / 𝐵) ≤ (𝐶 / 𝐷) ↔ (𝐷 / 𝐶) ≤ (𝐵 / 𝐴)))
Theorem	lediv2 8848	Division of a positive number by both sides of 'less than or equal to'. (Contributed by NM, 10-Jan-2006.)
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐶 / 𝐵) ≤ (𝐶 / 𝐴)))
Theorem	ltdiv23 8849	Swap denominator with other side of 'less than'. (Contributed by NM, 3-Oct-1999.)
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵))
Theorem	lediv23 8850	Swap denominator with other side of 'less than or equal to'. (Contributed by NM, 30-May-2005.)
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐵) ≤ 𝐶 ↔ (𝐴 / 𝐶) ≤ 𝐵))
Theorem	lediv12a 8851	Comparison of ratio of two nonnegative numbers. (Contributed by NM, 31-Dec-2005.)
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → (𝐴 / 𝐷) ≤ (𝐵 / 𝐶))
Theorem	lediv2a 8852	Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ ((((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐶 / 𝐵) ≤ (𝐶 / 𝐴))
Theorem	reclt1 8853	The reciprocal of a positive number less than 1 is greater than 1. (Contributed by NM, 23-Feb-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → (𝐴 < 1 ↔ 1 < (1 / 𝐴)))
Theorem	recgt1 8854	The reciprocal of a positive number greater than 1 is less than 1. (Contributed by NM, 28-Dec-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → (1 < 𝐴 ↔ (1 / 𝐴) < 1))
Theorem	recgt1i 8855	The reciprocal of a number greater than 1 is positive and less than 1. (Contributed by NM, 23-Feb-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → (0 < (1 / 𝐴) ∧ (1 / 𝐴) < 1))
Theorem	recp1lt1 8856	Construct a number less than 1 from any nonnegative number. (Contributed by NM, 30-Dec-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 / (1 + 𝐴)) < 1)
Theorem	recreclt 8857	Given a positive number 𝐴, construct a new positive number less than both 𝐴 and 1. (Contributed by NM, 28-Dec-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → ((1 / (1 + (1 / 𝐴))) < 1 ∧ (1 / (1 + (1 / 𝐴))) < 𝐴))
Theorem	le2msq 8858	The square function on nonnegative reals is monotonic. (Contributed by NM, 3-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐴) ≤ (𝐵 · 𝐵)))
Theorem	msq11 8859	The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 · 𝐴) = (𝐵 · 𝐵) ↔ 𝐴 = 𝐵))
Theorem	ledivp1 8860	Less-than-or-equal-to and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 28-Sep-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 / (𝐵 + 1)) · 𝐵) ≤ 𝐴)
Theorem	squeeze0 8861*	If a nonnegative number is less than any positive number, it is zero. (Contributed by NM, 11-Feb-2006.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀𝑥 ∈ ℝ (0 < 𝑥 → 𝐴 < 𝑥)) → 𝐴 = 0)
Theorem	ltp1i 8862	A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 𝐴 < (𝐴 + 1)
Theorem	recgt0i 8863	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (0 < 𝐴 → 0 < (1 / 𝐴))
Theorem	recgt0ii 8864	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 0 < 𝐴    ⇒   ⊢ 0 < (1 / 𝐴)
Theorem	prodgt0i 8865	Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 15-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 < (𝐴 · 𝐵)) → 0 < 𝐵)
Theorem	prodge0i 8866	Infer that a multiplicand is nonnegative from a positive multiplier and nonnegative product. (Contributed by NM, 2-Jul-2005.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 < 𝐴 ∧ 0 ≤ (𝐴 · 𝐵)) → 0 ≤ 𝐵)
Theorem	divgt0i 8867	The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 / 𝐵))
Theorem	divge0i 8868	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 12-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 < 𝐵) → 0 ≤ (𝐴 / 𝐵))
Theorem	ltreci 8869	The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴)))
Theorem	lereci 8870	The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 16-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → (𝐴 ≤ 𝐵 ↔ (1 / 𝐵) ≤ (1 / 𝐴)))
Theorem	lt2msqi 8871	The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 3-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 < 𝐵 ↔ (𝐴 · 𝐴) < (𝐵 · 𝐵)))
Theorem	le2msqi 8872	The square function on nonnegative reals is monotonic. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐴) ≤ (𝐵 · 𝐵)))
Theorem	msq11i 8873	The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((𝐴 · 𝐴) = (𝐵 · 𝐵) ↔ 𝐴 = 𝐵))
Theorem	divgt0i2i 8874	The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 0 < 𝐵    ⇒   ⊢ (0 < 𝐴 → 0 < (𝐴 / 𝐵))
Theorem	ltrecii 8875	The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 0 < 𝐴    &   ⊢ 0 < 𝐵    ⇒   ⊢ (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴))
Theorem	divgt0ii 8876	The ratio of two positive numbers is positive. (Contributed by NM, 18-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 0 < 𝐴    &   ⊢ 0 < 𝐵    ⇒   ⊢ 0 < (𝐴 / 𝐵)
Theorem	ltmul1i 8877	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (𝐴 < 𝐵 ↔ (𝐴 · 𝐶) < (𝐵 · 𝐶)))
Theorem	ltdiv1i 8878	Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶)))
Theorem	ltmuldivi 8879	'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → ((𝐴 · 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶)))
Theorem	ltmul2i 8880	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (𝐴 < 𝐵 ↔ (𝐶 · 𝐴) < (𝐶 · 𝐵)))
Theorem	lemul1i 8881	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶)))
Theorem	lemul2i 8882	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (𝐴 ≤ 𝐵 ↔ (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)))
Theorem	ltdiv23i 8883	Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((0 < 𝐵 ∧ 0 < 𝐶) → ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵))
Theorem	ltdiv23ii 8884	Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 0 < 𝐵    &   ⊢ 0 < 𝐶    ⇒   ⊢ ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵)
Theorem	ltmul1ii 8885	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.) (Proof shortened by Paul Chapman, 25-Jan-2008.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 0 < 𝐶    ⇒   ⊢ (𝐴 < 𝐵 ↔ (𝐴 · 𝐶) < (𝐵 · 𝐶))
Theorem	ltdiv1ii 8886	Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 0 < 𝐶    ⇒   ⊢ (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶))
Theorem	ltp1d 8887	A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 < (𝐴 + 1))
Theorem	lep1d 8888	A number is less than or equal to itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≤ (𝐴 + 1))
Theorem	ltm1d 8889	A number minus 1 is less than itself. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 − 1) < 𝐴)
Theorem	lem1d 8890	A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 − 1) ≤ 𝐴)
Theorem	recgt0d 8891	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → 0 < (1 / 𝐴))
Theorem	divgt0d 8892	The ratio of two positive numbers is positive. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → 0 < (𝐴 / 𝐵))
Theorem	mulgt1d 8893	The product of two numbers greater than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → 1 < 𝐵)    ⇒   ⊢ (𝜑 → 1 < (𝐴 · 𝐵))
Theorem	lemulge11d 8894	Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 1 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≤ (𝐴 · 𝐵))
Theorem	lemulge12d 8895	Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 1 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≤ (𝐵 · 𝐴))
Theorem	lemul1ad 8896	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))
Theorem	lemul2ad 8897	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))
Theorem	ltmul12ad 8898	Comparison of product of two positive numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐶 < 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐶) < (𝐵 · 𝐷))
Theorem	lemul12ad 8899	Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷))
Theorem	lemul12bd 8900	Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐷)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷))