P. 90 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8901-9000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ltmuldiv 8901	'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 · 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶)))
Theorem	ltmuldiv2 8902	'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 · 𝐴) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶)))
Theorem	ltdivmul 8903	'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐶 · 𝐵)))
Theorem	ledivmul 8904	'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐶 · 𝐵)))
Theorem	ltdivmul2 8905	'Less than' relationship between division and multiplication. (Contributed by NM, 24-Feb-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 · 𝐶)))
Theorem	lt2mul2div 8906	'Less than' relationship between division and multiplication. (Contributed by NM, 8-Jan-2006.)
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷))) → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ (𝐴 / 𝐷) < (𝐶 / 𝐵)))
Theorem	ledivmul2 8907	'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 · 𝐶)))
Theorem	lemuldiv 8908	'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 · 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶)))
Theorem	lemuldiv2 8909	'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 · 𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶)))
Theorem	ltrec 8910	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 8911	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 8912	Lemma for lt2msq 8913. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐴 · 𝐴) < (𝐵 · 𝐵))
Theorem	lt2msq 8913	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 8914	Division of a positive number by both sides of 'less than'. (Contributed by NM, 27-Apr-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 < 𝐵 ↔ (𝐶 / 𝐵) < (𝐶 / 𝐴)))
Theorem	ltrec1 8915	Reciprocal swap in a 'less than' relation. (Contributed by NM, 24-Feb-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((1 / 𝐴) < 𝐵 ↔ (1 / 𝐵) < 𝐴))
Theorem	lerec2 8916	Reciprocal swap in a 'less than or equal to' relation. (Contributed by NM, 24-Feb-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 ≤ (1 / 𝐵) ↔ 𝐵 ≤ (1 / 𝐴)))
Theorem	ledivdiv 8917	Invert ratios of positive numbers and swap their ordering. (Contributed by NM, 9-Jan-2006.)
⊢ ((((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 0 < 𝐶) ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷))) → ((𝐴 / 𝐵) ≤ (𝐶 / 𝐷) ↔ (𝐷 / 𝐶) ≤ (𝐵 / 𝐴)))
Theorem	lediv2 8918	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 8919	Swap denominator with other side of 'less than'. (Contributed by NM, 3-Oct-1999.)
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵))
Theorem	lediv23 8920	Swap denominator with other side of 'less than or equal to'. (Contributed by NM, 30-May-2005.)
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐵) ≤ 𝐶 ↔ (𝐴 / 𝐶) ≤ 𝐵))
Theorem	lediv12a 8921	Comparison of ratio of two nonnegative numbers. (Contributed by NM, 31-Dec-2005.)
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → (𝐴 / 𝐷) ≤ (𝐵 / 𝐶))
Theorem	lediv2a 8922	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 8923	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 8924	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 8925	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 8926	Construct a number less than 1 from any nonnegative number. (Contributed by NM, 30-Dec-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 / (1 + 𝐴)) < 1)
Theorem	recreclt 8927	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 8928	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 8929	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 8930	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 8931*	If a nonnegative number is less than any positive number, it is zero. (Contributed by NM, 11-Feb-2006.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀𝑥 ∈ ℝ (0 < 𝑥 → 𝐴 < 𝑥)) → 𝐴 = 0)
Theorem	ltp1i 8932	A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 𝐴 < (𝐴 + 1)
Theorem	recgt0i 8933	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 8934	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 8935	Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 15-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 < (𝐴 · 𝐵)) → 0 < 𝐵)
Theorem	prodge0i 8936	Infer that a multiplicand is nonnegative from a positive multiplier and nonnegative product. (Contributed by NM, 2-Jul-2005.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 < 𝐴 ∧ 0 ≤ (𝐴 · 𝐵)) → 0 ≤ 𝐵)
Theorem	divgt0i 8937	The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 / 𝐵))
Theorem	divge0i 8938	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 12-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 < 𝐵) → 0 ≤ (𝐴 / 𝐵))
Theorem	ltreci 8939	The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴)))
Theorem	lereci 8940	The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 16-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → (𝐴 ≤ 𝐵 ↔ (1 / 𝐵) ≤ (1 / 𝐴)))
Theorem	lt2msqi 8941	The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 3-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 < 𝐵 ↔ (𝐴 · 𝐴) < (𝐵 · 𝐵)))
Theorem	le2msqi 8942	The square function on nonnegative reals is monotonic. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐴) ≤ (𝐵 · 𝐵)))
Theorem	msq11i 8943	The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((𝐴 · 𝐴) = (𝐵 · 𝐵) ↔ 𝐴 = 𝐵))
Theorem	divgt0i2i 8944	The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 0 < 𝐵    ⇒   ⊢ (0 < 𝐴 → 0 < (𝐴 / 𝐵))
Theorem	ltrecii 8945	The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 0 < 𝐴    &   ⊢ 0 < 𝐵    ⇒   ⊢ (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴))
Theorem	divgt0ii 8946	The ratio of two positive numbers is positive. (Contributed by NM, 18-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 0 < 𝐴    &   ⊢ 0 < 𝐵    ⇒   ⊢ 0 < (𝐴 / 𝐵)
Theorem	ltmul1i 8947	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 8948	Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶)))
Theorem	ltmuldivi 8949	'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → ((𝐴 · 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶)))
Theorem	ltmul2i 8950	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 8951	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶)))
Theorem	lemul2i 8952	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (𝐴 ≤ 𝐵 ↔ (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)))
Theorem	ltdiv23i 8953	Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((0 < 𝐵 ∧ 0 < 𝐶) → ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵))
Theorem	ltdiv23ii 8954	Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 0 < 𝐵    &   ⊢ 0 < 𝐶    ⇒   ⊢ ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵)
Theorem	ltmul1ii 8955	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 8956	Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 0 < 𝐶    ⇒   ⊢ (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶))
Theorem	ltp1d 8957	A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 < (𝐴 + 1))
Theorem	lep1d 8958	A number is less than or equal to itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≤ (𝐴 + 1))
Theorem	ltm1d 8959	A number minus 1 is less than itself. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 − 1) < 𝐴)
Theorem	lem1d 8960	A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 − 1) ≤ 𝐴)
Theorem	recgt0d 8961	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 8962	The ratio of two positive numbers is positive. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → 0 < (𝐴 / 𝐵))
Theorem	mulgt1d 8963	The product of two numbers greater than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → 1 < 𝐵)    ⇒   ⊢ (𝜑 → 1 < (𝐴 · 𝐵))
Theorem	lemulge11d 8964	Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 1 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≤ (𝐴 · 𝐵))
Theorem	lemulge12d 8965	Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 1 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≤ (𝐵 · 𝐴))
Theorem	lemul1ad 8966	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))
Theorem	lemul2ad 8967	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))
Theorem	ltmul12ad 8968	Comparison of product of two positive numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐶 < 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐶) < (𝐵 · 𝐷))
Theorem	lemul12ad 8969	Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷))
Theorem	lemul12bd 8970	Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐷)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷))
Theorem	mulle0r 8971	Multiplying a nonnegative number by a nonpositive number yields a nonpositive number. (Contributed by Jim Kingdon, 28-Oct-2021.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ 0 ∧ 0 ≤ 𝐵)) → (𝐴 · 𝐵) ≤ 0)
4.3.10  Suprema
Theorem	lbreu 8972*	If a set of reals contains a lower bound, it contains a unique lower bound. (Contributed by NM, 9-Oct-2005.)
⊢ ((𝑆 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → ∃!𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦)
Theorem	lbcl 8973*	If a set of reals contains a lower bound, it contains a unique lower bound that belongs to the set. (Contributed by NM, 9-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ ((𝑆 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∈ 𝑆)
Theorem	lble 8974*	If a set of reals contains a lower bound, the lower bound is less than or equal to all members of the set. (Contributed by NM, 9-Oct-2005.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
⊢ ((𝑆 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝑆) → (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ≤ 𝐴)
Theorem	lbinf 8975*	If a set of reals contains a lower bound, the lower bound is its infimum. (Contributed by NM, 9-Oct-2005.) (Revised by AV, 4-Sep-2020.)
⊢ ((𝑆 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → inf(𝑆, ℝ, < ) = (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦))
Theorem	lbinfcl 8976*	If a set of reals contains a lower bound, it contains its infimum. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 4-Sep-2020.)
⊢ ((𝑆 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → inf(𝑆, ℝ, < ) ∈ 𝑆)
Theorem	lbinfle 8977*	If a set of reals contains a lower bound, its infimum is less than or equal to all members of the set. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 4-Sep-2020.)
⊢ ((𝑆 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝑆) → inf(𝑆, ℝ, < ) ≤ 𝐴)
Theorem	suprubex 8978*	A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by Jim Kingdon, 18-Jan-2022.)
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < ))
Theorem	suprlubex 8979*	The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by Jim Kingdon, 19-Jan-2022.)
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 < sup(𝐴, ℝ, < ) ↔ ∃𝑧 ∈ 𝐴 𝐵 < 𝑧))
Theorem	suprnubex 8980*	An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by Jim Kingdon, 19-Jan-2022.)
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (¬ 𝐵 < sup(𝐴, ℝ, < ) ↔ ∀𝑧 ∈ 𝐴 ¬ 𝐵 < 𝑧))
Theorem	suprleubex 8981*	The supremum of a nonempty bounded set of reals is less than or equal to an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 6-Sep-2014.)
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (sup(𝐴, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝐵))
Theorem	negiso 8982	Negation is an order anti-isomorphism of the real numbers, which is its own inverse. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ -𝑥)    ⇒   ⊢ (𝐹 Isom < , ◡ < (ℝ, ℝ) ∧ ◡𝐹 = 𝐹)
Theorem	dfinfre 8983*	The infimum of a set of reals 𝐴. (Contributed by NM, 9-Oct-2005.) (Revised by AV, 4-Sep-2020.)
⊢ (𝐴 ⊆ ℝ → inf(𝐴, ℝ, < ) = ∪ {𝑥 ∈ ℝ ∣ (∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))})
Theorem	sup3exmid 8984*	If any inhabited set of real numbers bounded from above has a supremum, excluded middle follows. (Contributed by Jim Kingdon, 2-Apr-2023.)
⊢ ((𝑢 ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ 𝑢 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧)))    ⇒   ⊢ DECID 𝜑
4.3.11  Imaginary and complex number properties
Theorem	crap0 8985	The real representation of complex numbers is apart from zero iff one of its terms is apart from zero. (Contributed by Jim Kingdon, 5-Mar-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 # 0 ∨ 𝐵 # 0) ↔ (𝐴 + (i · 𝐵)) # 0))
Theorem	creur 8986*	The real part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → ∃!𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	creui 8987*	The imaginary part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → ∃!𝑦 ∈ ℝ ∃𝑥 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	cju 8988*	The complex conjugate of a complex number is unique. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → ∃!𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ))
4.3.12  Function operation analogue theorems
Theorem	ofnegsub 8989	Function analogue of negsub 8274. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ) → (𝐹 ∘𝑓 + ((𝐴 × {-1}) ∘𝑓 · 𝐺)) = (𝐹 ∘𝑓 − 𝐺))
4.4  Integer sets
4.4.1  Positive integers (as a subset of complex numbers)
Syntax	cn 8990	Extend class notation to include the class of positive integers.
class ℕ
Definition	df-inn 8991*	Definition of the set of positive integers. For naming consistency with the Metamath Proof Explorer usages should refer to dfnn2 8992 instead. (Contributed by Jeff Hankins, 12-Sep-2013.) (Revised by Mario Carneiro, 3-May-2014.) (New usage is discouraged.)
⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
Theorem	dfnn2 8992*	Definition of the set of positive integers. Another name for df-inn 8991. (Contributed by Jeff Hankins, 12-Sep-2013.) (Revised by Mario Carneiro, 3-May-2014.)
⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
Theorem	peano5nni 8993*	Peano's inductive postulate. Theorem I.36 (principle of mathematical induction) of [Apostol] p. 34. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ((1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → ℕ ⊆ 𝐴)
Theorem	nnssre 8994	The positive integers are a subset of the reals. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.)
⊢ ℕ ⊆ ℝ
Theorem	nnsscn 8995	The positive integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
⊢ ℕ ⊆ ℂ
Theorem	nnex 8996	The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ℕ ∈ V
Theorem	nnre 8997	A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
Theorem	nncn 8998	A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
Theorem	nnrei 8999	A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 𝐴 ∈ ℝ
Theorem	nncni 9000	A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 𝐴 ∈ ℂ