P. 77 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7601-7700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ltmuldiv 7601	'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((A · 𝐶) < B ↔ A < (B / 𝐶)))
Theorem	ltmuldiv2 7602	'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 · A) < B ↔ A < (B / 𝐶)))
Theorem	ltdivmul 7603	'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((A / 𝐶) < B ↔ A < (𝐶 · B)))
Theorem	ledivmul 7604	'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((A / 𝐶) ≤ B ↔ A ≤ (𝐶 · B)))
Theorem	ltdivmul2 7605	'Less than' relationship between division and multiplication. (Contributed by NM, 24-Feb-2005.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((A / 𝐶) < B ↔ A < (B · 𝐶)))
Theorem	lt2mul2div 7606	'Less than' relationship between division and multiplication. (Contributed by NM, 8-Jan-2006.)
⊢ (((A ∈ ℝ ∧ (B ∈ ℝ ∧ 0 < B)) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷))) → ((A · B) < (𝐶 · 𝐷) ↔ (A / 𝐷) < (𝐶 / B)))
Theorem	ledivmul2 7607	'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((A / 𝐶) ≤ B ↔ A ≤ (B · 𝐶)))
Theorem	lemuldiv 7608	'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((A · 𝐶) ≤ B ↔ A ≤ (B / 𝐶)))
Theorem	lemuldiv2 7609	'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 · A) ≤ B ↔ A ≤ (B / 𝐶)))
Theorem	ltrec 7610	The reciprocal of both sides of 'less than'. (Contributed by NM, 26-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (((A ∈ ℝ ∧ 0 < A) ∧ (B ∈ ℝ ∧ 0 < B)) → (A < B ↔ (1 / B) < (1 / A)))
Theorem	lerec 7611	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.)
⊢ (((A ∈ ℝ ∧ 0 < A) ∧ (B ∈ ℝ ∧ 0 < B)) → (A ≤ B ↔ (1 / B) ≤ (1 / A)))
Theorem	lt2msq1 7612	Lemma for lt2msq 7613. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (((A ∈ ℝ ∧ 0 ≤ A) ∧ B ∈ ℝ ∧ A < B) → (A · A) < (B · B))
Theorem	lt2msq 7613	Two nonnegative numbers compare the same as their squares. (Contributed by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (((A ∈ ℝ ∧ 0 ≤ A) ∧ (B ∈ ℝ ∧ 0 ≤ B)) → (A < B ↔ (A · A) < (B · B)))
Theorem	ltdiv2 7614	Division of a positive number by both sides of 'less than'. (Contributed by NM, 27-Apr-2005.)
⊢ (((A ∈ ℝ ∧ 0 < A) ∧ (B ∈ ℝ ∧ 0 < B) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (A < B ↔ (𝐶 / B) < (𝐶 / A)))
Theorem	ltrec1 7615	Reciprocal swap in a 'less than' relation. (Contributed by NM, 24-Feb-2005.)
⊢ (((A ∈ ℝ ∧ 0 < A) ∧ (B ∈ ℝ ∧ 0 < B)) → ((1 / A) < B ↔ (1 / B) < A))
Theorem	lerec2 7616	Reciprocal swap in a 'less than or equal to' relation. (Contributed by NM, 24-Feb-2005.)
⊢ (((A ∈ ℝ ∧ 0 < A) ∧ (B ∈ ℝ ∧ 0 < B)) → (A ≤ (1 / B) ↔ B ≤ (1 / A)))
Theorem	ledivdiv 7617	Invert ratios of positive numbers and swap their ordering. (Contributed by NM, 9-Jan-2006.)
⊢ ((((A ∈ ℝ ∧ 0 < A) ∧ (B ∈ ℝ ∧ 0 < B)) ∧ ((𝐶 ∈ ℝ ∧ 0 < 𝐶) ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷))) → ((A / B) ≤ (𝐶 / 𝐷) ↔ (𝐷 / 𝐶) ≤ (B / A)))
Theorem	lediv2 7618	Division of a positive number by both sides of 'less than or equal to'. (Contributed by NM, 10-Jan-2006.)
⊢ (((A ∈ ℝ ∧ 0 < A) ∧ (B ∈ ℝ ∧ 0 < B) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (A ≤ B ↔ (𝐶 / B) ≤ (𝐶 / A)))
Theorem	ltdiv23 7619	Swap denominator with other side of 'less than'. (Contributed by NM, 3-Oct-1999.)
⊢ ((A ∈ ℝ ∧ (B ∈ ℝ ∧ 0 < B) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((A / B) < 𝐶 ↔ (A / 𝐶) < B))
Theorem	lediv23 7620	Swap denominator with other side of 'less than or equal to'. (Contributed by NM, 30-May-2005.)
⊢ ((A ∈ ℝ ∧ (B ∈ ℝ ∧ 0 < B) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((A / B) ≤ 𝐶 ↔ (A / 𝐶) ≤ B))
Theorem	lediv12a 7621	Comparison of ratio of two nonnegative numbers. (Contributed by NM, 31-Dec-2005.)
⊢ ((((A ∈ ℝ ∧ B ∈ ℝ) ∧ (0 ≤ A ∧ A ≤ B)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → (A / 𝐷) ≤ (B / 𝐶))
Theorem	lediv2a 7622	Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ ((((A ∈ ℝ ∧ 0 < A) ∧ (B ∈ ℝ ∧ 0 < B) ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ A ≤ B) → (𝐶 / B) ≤ (𝐶 / A))
Theorem	reclt1 7623	The reciprocal of a positive number less than 1 is greater than 1. (Contributed by NM, 23-Feb-2005.)
⊢ ((A ∈ ℝ ∧ 0 < A) → (A < 1 ↔ 1 < (1 / A)))
Theorem	recgt1 7624	The reciprocal of a positive number greater than 1 is less than 1. (Contributed by NM, 28-Dec-2005.)
⊢ ((A ∈ ℝ ∧ 0 < A) → (1 < A ↔ (1 / A) < 1))
Theorem	recgt1i 7625	The reciprocal of a number greater than 1 is positive and less than 1. (Contributed by NM, 23-Feb-2005.)
⊢ ((A ∈ ℝ ∧ 1 < A) → (0 < (1 / A) ∧ (1 / A) < 1))
Theorem	recp1lt1 7626	Construct a number less than 1 from any nonnegative number. (Contributed by NM, 30-Dec-2005.)
⊢ ((A ∈ ℝ ∧ 0 ≤ A) → (A / (1 + A)) < 1)
Theorem	recreclt 7627	Given a positive number A, construct a new positive number less than both A and 1. (Contributed by NM, 28-Dec-2005.)
⊢ ((A ∈ ℝ ∧ 0 < A) → ((1 / (1 + (1 / A))) < 1 ∧ (1 / (1 + (1 / A))) < A))
Theorem	le2msq 7628	The square function on nonnegative reals is monotonic. (Contributed by NM, 3-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (((A ∈ ℝ ∧ 0 ≤ A) ∧ (B ∈ ℝ ∧ 0 ≤ B)) → (A ≤ B ↔ (A · A) ≤ (B · B)))
Theorem	msq11 7629	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.)
⊢ (((A ∈ ℝ ∧ 0 ≤ A) ∧ (B ∈ ℝ ∧ 0 ≤ B)) → ((A · A) = (B · B) ↔ A = B))
Theorem	ledivp1 7630	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.)
⊢ (((A ∈ ℝ ∧ 0 ≤ A) ∧ (B ∈ ℝ ∧ 0 ≤ B)) → ((A / (B + 1)) · B) ≤ A)
Theorem	squeeze0 7631*	If a nonnegative number is less than any positive number, it is zero. (Contributed by NM, 11-Feb-2006.)
⊢ ((A ∈ ℝ ∧ 0 ≤ A ∧ ∀x ∈ ℝ (0 < x → A < x)) → A = 0)
Theorem	ltp1i 7632	A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
⊢ A ∈ ℝ    ⇒   ⊢ A < (A + 1)
Theorem	recgt0i 7633	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.)
⊢ A ∈ ℝ    ⇒   ⊢ (0 < A → 0 < (1 / A))
Theorem	recgt0ii 7634	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.)
⊢ A ∈ ℝ    &   ⊢ 0 < A    ⇒   ⊢ 0 < (1 / A)
Theorem	prodgt0i 7635	Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 15-May-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ 0 < (A · B)) → 0 < B)
Theorem	prodge0i 7636	Infer that a multiplicand is nonnegative from a positive multiplier and nonnegative product. (Contributed by NM, 2-Jul-2005.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 < A ∧ 0 ≤ (A · B)) → 0 ≤ B)
Theorem	divgt0i 7637	The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 < A ∧ 0 < B) → 0 < (A / B))
Theorem	divge0i 7638	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 12-Aug-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ 0 < B) → 0 ≤ (A / B))
Theorem	ltreci 7639	The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 < A ∧ 0 < B) → (A < B ↔ (1 / B) < (1 / A)))
Theorem	lereci 7640	The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 16-Sep-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 < A ∧ 0 < B) → (A ≤ B ↔ (1 / B) ≤ (1 / A)))
Theorem	lt2msqi 7641	The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 3-Aug-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ 0 ≤ B) → (A < B ↔ (A · A) < (B · B)))
Theorem	le2msqi 7642	The square function on nonnegative reals is monotonic. (Contributed by NM, 2-Aug-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ 0 ≤ B) → (A ≤ B ↔ (A · A) ≤ (B · B)))
Theorem	msq11i 7643	The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ 0 ≤ B) → ((A · A) = (B · B) ↔ A = B))
Theorem	divgt0i2i 7644	The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 0 < B    ⇒   ⊢ (0 < A → 0 < (A / B))
Theorem	ltrecii 7645	The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 0 < A    &   ⊢ 0 < B    ⇒   ⊢ (A < B ↔ (1 / B) < (1 / A))
Theorem	divgt0ii 7646	The ratio of two positive numbers is positive. (Contributed by NM, 18-May-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 0 < A    &   ⊢ 0 < B    ⇒   ⊢ 0 < (A / B)
Theorem	ltmul1i 7647	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (A < B ↔ (A · 𝐶) < (B · 𝐶)))
Theorem	ltdiv1i 7648	Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (A < B ↔ (A / 𝐶) < (B / 𝐶)))
Theorem	ltmuldivi 7649	'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → ((A · 𝐶) < B ↔ A < (B / 𝐶)))
Theorem	ltmul2i 7650	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (A < B ↔ (𝐶 · A) < (𝐶 · B)))
Theorem	lemul1i 7651	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 2-Aug-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (A ≤ B ↔ (A · 𝐶) ≤ (B · 𝐶)))
Theorem	lemul2i 7652	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 1-Aug-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (0 < 𝐶 → (A ≤ B ↔ (𝐶 · A) ≤ (𝐶 · B)))
Theorem	ltdiv23i 7653	Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((0 < B ∧ 0 < 𝐶) → ((A / B) < 𝐶 ↔ (A / 𝐶) < B))
Theorem	ltdiv23ii 7654	Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 0 < B    &   ⊢ 0 < 𝐶    ⇒   ⊢ ((A / B) < 𝐶 ↔ (A / 𝐶) < B)
Theorem	ltmul1ii 7655	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.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 0 < 𝐶    ⇒   ⊢ (A < B ↔ (A · 𝐶) < (B · 𝐶))
Theorem	ltdiv1ii 7656	Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 0 < 𝐶    ⇒   ⊢ (A < B ↔ (A / 𝐶) < (B / 𝐶))
Theorem	ltp1d 7657	A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → A < (A + 1))
Theorem	lep1d 7658	A number is less than or equal to itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → A ≤ (A + 1))
Theorem	ltm1d 7659	A number minus 1 is less than itself. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → (A − 1) < A)
Theorem	lem1d 7660	A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → (A − 1) ≤ A)
Theorem	recgt0d 7661	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 0 < A)    ⇒   ⊢ (φ → 0 < (1 / A))
Theorem	divgt0d 7662	The ratio of two positive numbers is positive. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 0 < A)    &   ⊢ (φ → 0 < B)    ⇒   ⊢ (φ → 0 < (A / B))
Theorem	mulgt1d 7663	The product of two numbers greater than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 1 < A)    &   ⊢ (φ → 1 < B)    ⇒   ⊢ (φ → 1 < (A · B))
Theorem	lemulge11d 7664	Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 0 ≤ A)    &   ⊢ (φ → 1 ≤ B)    ⇒   ⊢ (φ → A ≤ (A · B))
Theorem	lemulge12d 7665	Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 0 ≤ A)    &   ⊢ (φ → 1 ≤ B)    ⇒   ⊢ (φ → A ≤ (B · A))
Theorem	lemul1ad 7666	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ)    &   ⊢ (φ → 0 ≤ 𝐶)    &   ⊢ (φ → A ≤ B)    ⇒   ⊢ (φ → (A · 𝐶) ≤ (B · 𝐶))
Theorem	lemul2ad 7667	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ)    &   ⊢ (φ → 0 ≤ 𝐶)    &   ⊢ (φ → A ≤ B)    ⇒   ⊢ (φ → (𝐶 · A) ≤ (𝐶 · B))
Theorem	ltmul12ad 7668	Comparison of product of two positive numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ)    &   ⊢ (φ → 𝐷 ∈ ℝ)    &   ⊢ (φ → 0 ≤ A)    &   ⊢ (φ → A < B)    &   ⊢ (φ → 0 ≤ 𝐶)    &   ⊢ (φ → 𝐶 < 𝐷)    ⇒   ⊢ (φ → (A · 𝐶) < (B · 𝐷))
Theorem	lemul12ad 7669	Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ)    &   ⊢ (φ → 𝐷 ∈ ℝ)    &   ⊢ (φ → 0 ≤ A)    &   ⊢ (φ → 0 ≤ 𝐶)    &   ⊢ (φ → A ≤ B)    &   ⊢ (φ → 𝐶 ≤ 𝐷)    ⇒   ⊢ (φ → (A · 𝐶) ≤ (B · 𝐷))
Theorem	lemul12bd 7670	Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ)    &   ⊢ (φ → 𝐷 ∈ ℝ)    &   ⊢ (φ → 0 ≤ A)    &   ⊢ (φ → 0 ≤ 𝐷)    &   ⊢ (φ → A ≤ B)    &   ⊢ (φ → 𝐶 ≤ 𝐷)    ⇒   ⊢ (φ → (A · 𝐶) ≤ (B · 𝐷))
3.3.10  Imaginary and complex number properties
Theorem	crap0 7671	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.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((A # 0 ∨ B # 0) ↔ (A + (i · B)) # 0))
Theorem	creur 7672*	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.)
⊢ (A ∈ ℂ → ∃!x ∈ ℝ ∃y ∈ ℝ A = (x + (i · y)))
Theorem	creui 7673*	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.)
⊢ (A ∈ ℂ → ∃!y ∈ ℝ ∃x ∈ ℝ A = (x + (i · y)))
Theorem	cju 7674*	The complex conjugate of a complex number is unique. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ (A ∈ ℂ → ∃!x ∈ ℂ ((A + x) ∈ ℝ ∧ (i · (A − x)) ∈ ℝ))
3.4  Integer sets
3.4.1  Positive integers (as a subset of complex numbers)
Syntax	cn 7675	Extend class notation to include the class of positive integers.
class ℕ
Definition	df-inn 7676*	Definition of the set of positive integers. For naming consistency with the Metamath Proof Explorer usages should refer to dfnn2 7677 instead. (Contributed by Jeff Hankins, 12-Sep-2013.) (Revised by Mario Carneiro, 3-May-2014.) (New usage is discouraged.)
⊢ ℕ = ∩ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}
Theorem	dfnn2 7677*	Definition of the set of positive integers. Another name for df-inn 7676. (Contributed by Jeff Hankins, 12-Sep-2013.) (Revised by Mario Carneiro, 3-May-2014.)
⊢ ℕ = ∩ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}
Theorem	peano5nni 7678*	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 ∈ A ∧ ∀x ∈ A (x + 1) ∈ A) → ℕ ⊆ A)
Theorem	nnssre 7679	The positive integers are a subset of the reals. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.)
⊢ ℕ ⊆ ℝ
Theorem	nnsscn 7680	The positive integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
⊢ ℕ ⊆ ℂ
Theorem	nnex 7681	The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ℕ ∈ V
Theorem	nnre 7682	A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
⊢ (A ∈ ℕ → A ∈ ℝ)
Theorem	nncn 7683	A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)
⊢ (A ∈ ℕ → A ∈ ℂ)
Theorem	nnrei 7684	A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
⊢ A ∈ ℕ    ⇒   ⊢ A ∈ ℝ
Theorem	nncni 7685	A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)
⊢ A ∈ ℕ    ⇒   ⊢ A ∈ ℂ
Theorem	1nn 7686	Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.)
⊢ 1 ∈ ℕ
Theorem	peano2nn 7687	Peano postulate: a successor of a positive integer is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (A ∈ ℕ → (A + 1) ∈ ℕ)
Theorem	nnred 7688	A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℕ)    ⇒   ⊢ (φ → A ∈ ℝ)
Theorem	nncnd 7689	A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℕ)    ⇒   ⊢ (φ → A ∈ ℂ)
Theorem	peano2nnd 7690	Peano postulate: a successor of a positive integer is a positive integer. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℕ)    ⇒   ⊢ (φ → (A + 1) ∈ ℕ)
3.4.2  Principle of mathematical induction
Theorem	nnind 7691*	Principle of Mathematical Induction (inference schema). The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. See nnaddcl 7695 for an example of its use. This is an alternative for Metamath 100 proof #74. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.)
⊢ (x = 1 → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = (y + 1) → (φ ↔ θ))    &   ⊢ (x = A → (φ ↔ τ))    &   ⊢ ψ    &   ⊢ (y ∈ ℕ → (χ → θ))    ⇒   ⊢ (A ∈ ℕ → τ)
Theorem	nnindALT 7692*	Principle of Mathematical Induction (inference schema). The last four hypotheses give us the substitution instances we need; the first two are the induction step and the basis. This ALT version of nnind 7691 has a different hypothesis order. It may be easier to use with the metamath program's Proof Assistant, because "MM-PA> assign last" will be applied to the substitution instances first. We may eventually use this one as the official version. You may use either version. After the proof is complete, the ALT version can be changed to the non-ALT version with "MM-PA> minimize nnind /allow". (Contributed by NM, 7-Dec-2005.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (y ∈ ℕ → (χ → θ))    &   ⊢ ψ    &   ⊢ (x = 1 → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = (y + 1) → (φ ↔ θ))    &   ⊢ (x = A → (φ ↔ τ))    ⇒   ⊢ (A ∈ ℕ → τ)
Theorem	nn1m1nn 7693	Every positive integer is one or a successor. (Contributed by Mario Carneiro, 16-May-2014.)
⊢ (A ∈ ℕ → (A = 1 ∨ (A − 1) ∈ ℕ))
Theorem	nn1suc 7694*	If a statement holds for 1 and also holds for a successor, it holds for all positive integers. The first three hypotheses give us the substitution instances we need; the last two show that it holds for 1 and for a successor. (Contributed by NM, 11-Oct-2004.) (Revised by Mario Carneiro, 16-May-2014.)
⊢ (x = 1 → (φ ↔ ψ))    &   ⊢ (x = (y + 1) → (φ ↔ χ))    &   ⊢ (x = A → (φ ↔ θ))    &   ⊢ ψ    &   ⊢ (y ∈ ℕ → χ)    ⇒   ⊢ (A ∈ ℕ → θ)
Theorem	nnaddcl 7695	Closure of addition of positive integers, proved by induction on the second addend. (Contributed by NM, 12-Jan-1997.)
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (A + B) ∈ ℕ)
Theorem	nnmulcl 7696	Closure of multiplication of positive integers. (Contributed by NM, 12-Jan-1997.)
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (A · B) ∈ ℕ)
Theorem	nnmulcli 7697	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ    &   ⊢ B ∈ ℕ    ⇒   ⊢ (A · B) ∈ ℕ
Theorem	nnge1 7698	A positive integer is one or greater. (Contributed by NM, 25-Aug-1999.)
⊢ (A ∈ ℕ → 1 ≤ A)
Theorem	nnle1eq1 7699	A positive integer is less than or equal to one iff it is equal to one. (Contributed by NM, 3-Apr-2005.)
⊢ (A ∈ ℕ → (A ≤ 1 ↔ A = 1))
Theorem	nngt0 7700	A positive integer is positive. (Contributed by NM, 26-Sep-1999.)
⊢ (A ∈ ℕ → 0 < A)