Theorem List for Intuitionistic Logic Explorer - 7601-7700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | prodge0 7601 |
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.)
|
⊢ (((A ∈ ℝ ∧
B ∈
ℝ) ∧ (0 < A ∧ 0 ≤
(A · B))) → 0 ≤ B) |
|
Theorem | prodge02 7602 |
Infer that a multiplier is nonnegative from a positive multiplicand and
nonnegative product. (Contributed by NM, 2-Jul-2005.)
|
⊢ (((A ∈ ℝ ∧
B ∈
ℝ) ∧ (0 < B ∧ 0 ≤
(A · B))) → 0 ≤ A) |
|
Theorem | ltmul2 7603 |
Multiplication of both sides of 'less than' by a positive number. Theorem
I.19 of [Apostol] p. 20. (Contributed by
NM, 13-Feb-2005.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈
ℝ ∧ 0 < 𝐶)) → (A < B ↔
(𝐶 · A) < (𝐶 · B))) |
|
Theorem | lemul2 7604 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by NM, 16-Mar-2005.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈
ℝ ∧ 0 < 𝐶)) → (A ≤ B ↔
(𝐶 · A) ≤ (𝐶 · B))) |
|
Theorem | lemul1a 7605 |
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.)
|
⊢ (((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈
ℝ ∧ 0 ≤ 𝐶)) ∧
A ≤ B) → (A
· 𝐶) ≤ (B · 𝐶)) |
|
Theorem | lemul2a 7606 |
Multiplication of both sides of 'less than or equal to' by a nonnegative
number. (Contributed by Paul Chapman, 7-Sep-2007.)
|
⊢ (((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈
ℝ ∧ 0 ≤ 𝐶)) ∧
A ≤ B) → (𝐶 · A) ≤ (𝐶 · B)) |
|
Theorem | ltmul12a 7607 |
Comparison of product of two positive numbers. (Contributed by NM,
30-Dec-2005.)
|
⊢ ((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (0 ≤ A ∧ A < B))
∧ ((𝐶 ∈
ℝ ∧ 𝐷 ∈
ℝ) ∧ (0 ≤ 𝐶 ∧ 𝐶 < 𝐷))) → (A · 𝐶) < (B · 𝐷)) |
|
Theorem | lemul12b 7608 |
Comparison of product of two nonnegative numbers. (Contributed by NM,
22-Feb-2008.)
|
⊢ ((((A ∈ ℝ ∧ 0
≤ A) ∧
B ∈
ℝ) ∧ (𝐶 ∈
ℝ ∧ (𝐷 ∈
ℝ ∧ 0 ≤ 𝐷))) → ((A ≤ B ∧ 𝐶 ≤ 𝐷) → (A · 𝐶) ≤ (B · 𝐷))) |
|
Theorem | lemul12a 7609 |
Comparison of product of two nonnegative numbers. (Contributed by NM,
22-Feb-2008.)
|
⊢ ((((A ∈ ℝ ∧ 0
≤ A) ∧
B ∈
ℝ) ∧ ((𝐶 ∈
ℝ ∧ 0 ≤ 𝐶) ∧ 𝐷 ∈ ℝ)) → ((A ≤ B ∧ 𝐶 ≤ 𝐷) → (A · 𝐶) ≤ (B · 𝐷))) |
|
Theorem | mulgt1 7610 |
The product of two numbers greater than 1 is greater than 1. (Contributed
by NM, 13-Feb-2005.)
|
⊢ (((A ∈ ℝ ∧
B ∈
ℝ) ∧ (1 < A ∧ 1 <
B)) → 1 < (A · B)) |
|
Theorem | ltmulgt11 7611 |
Multiplication by a number greater than 1. (Contributed by NM,
24-Dec-2005.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ ∧ 0 < A) → (1 < B ↔ A <
(A · B))) |
|
Theorem | ltmulgt12 7612 |
Multiplication by a number greater than 1. (Contributed by NM,
24-Dec-2005.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ ∧ 0 < A) → (1 < B ↔ A <
(B · A))) |
|
Theorem | lemulge11 7613 |
Multiplication by a number greater than or equal to 1. (Contributed by
NM, 17-Dec-2005.)
|
⊢ (((A ∈ ℝ ∧
B ∈
ℝ) ∧ (0 ≤ A ∧ 1 ≤
B)) → A ≤ (A
· B)) |
|
Theorem | lemulge12 7614 |
Multiplication by a number greater than or equal to 1. (Contributed by
Paul Chapman, 21-Mar-2011.)
|
⊢ (((A ∈ ℝ ∧
B ∈
ℝ) ∧ (0 ≤ A ∧ 1 ≤
B)) → A ≤ (B
· A)) |
|
Theorem | ltdiv1 7615 |
Division of both sides of 'less than' by a positive number. (Contributed
by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈
ℝ ∧ 0 < 𝐶)) → (A < B ↔
(A / 𝐶) < (B / 𝐶))) |
|
Theorem | lediv1 7616 |
Division of both sides of a less than or equal to relation by a positive
number. (Contributed by NM, 18-Nov-2004.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈
ℝ ∧ 0 < 𝐶)) → (A ≤ B ↔
(A / 𝐶) ≤ (B / 𝐶))) |
|
Theorem | gt0div 7617 |
Division of a positive number by a positive number. (Contributed by NM,
28-Sep-2005.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ ∧ 0 < B) → (0 < A ↔ 0 < (A / B))) |
|
Theorem | ge0div 7618 |
Division of a nonnegative number by a positive number. (Contributed by
NM, 28-Sep-2005.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ ∧ 0 < B) → (0 ≤ A ↔ 0 ≤ (A / B))) |
|
Theorem | divgt0 7619 |
The ratio of two positive numbers is positive. (Contributed by NM,
12-Oct-1999.)
|
⊢ (((A ∈ ℝ ∧ 0
< A) ∧
(B ∈
ℝ ∧ 0 < B)) → 0 < (A / B)) |
|
Theorem | divge0 7620 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by NM, 27-Sep-1999.)
|
⊢ (((A ∈ ℝ ∧ 0
≤ A) ∧
(B ∈
ℝ ∧ 0 < B)) → 0 ≤ (A / B)) |
|
Theorem | ltmuldiv 7621 |
'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 7622 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 18-Nov-2004.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈
ℝ ∧ 0 < 𝐶)) → ((𝐶 · A) < B
↔ A < (B / 𝐶))) |
|
Theorem | ltdivmul 7623 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 18-Nov-2004.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈
ℝ ∧ 0 < 𝐶)) → ((A / 𝐶) < B ↔ A <
(𝐶 · B))) |
|
Theorem | ledivmul 7624 |
'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 7625 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 24-Feb-2005.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈
ℝ ∧ 0 < 𝐶)) → ((A / 𝐶) < B ↔ A <
(B · 𝐶))) |
|
Theorem | lt2mul2div 7626 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 8-Jan-2006.)
|
⊢ (((A ∈ ℝ ∧
(B ∈
ℝ ∧ 0 < B)) ∧ (𝐶 ∈ ℝ ∧
(𝐷 ∈ ℝ ∧ 0
< 𝐷))) →
((A · B) < (𝐶 · 𝐷) ↔ (A / 𝐷) < (𝐶 / B))) |
|
Theorem | ledivmul2 7627 |
'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 7628 |
'Less than or equal' relationship between division and multiplication.
(Contributed by NM, 10-Mar-2006.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈
ℝ ∧ 0 < 𝐶)) → ((A · 𝐶) ≤ B ↔ A ≤
(B / 𝐶))) |
|
Theorem | lemuldiv2 7629 |
'Less than or equal' relationship between division and multiplication.
(Contributed by NM, 10-Mar-2006.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈
ℝ ∧ 0 < 𝐶)) → ((𝐶 · A) ≤ B
↔ A ≤ (B / 𝐶))) |
|
Theorem | ltrec 7630 |
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 7631 |
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 7632 |
Lemma for lt2msq 7633. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (((A ∈ ℝ ∧ 0
≤ A) ∧
B ∈
ℝ ∧ A < B)
→ (A · A) < (B
· B)) |
|
Theorem | lt2msq 7633 |
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 7634 |
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 7635 |
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 7636 |
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 7637 |
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 7638 |
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 7639 |
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 7640 |
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 7641 |
Comparison of ratio of two nonnegative numbers. (Contributed by NM,
31-Dec-2005.)
|
⊢ ((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (0 ≤ A ∧ A ≤ B))
∧ ((𝐶 ∈
ℝ ∧ 𝐷 ∈
ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → (A / 𝐷) ≤ (B / 𝐶)) |
|
Theorem | lediv2a 7642 |
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 7643 |
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 7644 |
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 7645 |
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 7646 |
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 7647 |
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 7648 |
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 7649 |
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 7650 |
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 7651* |
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 7652 |
A number is less than itself plus 1. (Contributed by NM,
20-Aug-2001.)
|
⊢ A ∈ ℝ ⇒ ⊢ A < (A +
1) |
|
Theorem | recgt0i 7653 |
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 7654 |
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 7655 |
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 7656 |
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 7657 |
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 7658 |
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 7659 |
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 7660 |
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 7661 |
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 7662 |
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 7663 |
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 7664 |
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 7665 |
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 7666 |
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 7667 |
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 7668 |
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 7669 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 12-Oct-1999.)
|
⊢ A ∈ ℝ & ⊢ B ∈
ℝ
& ⊢ 𝐶 ∈
ℝ ⇒ ⊢ (0 < 𝐶 → ((A · 𝐶) < B ↔ A <
(B / 𝐶))) |
|
Theorem | ltmul2i 7670 |
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 7671 |
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 7672 |
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 7673 |
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 7674 |
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 7675 |
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 7676 |
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 7677 |
A number is less than itself plus 1. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) ⇒ ⊢ (φ → A < (A +
1)) |
|
Theorem | lep1d 7678 |
A number is less than or equal to itself plus 1. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) ⇒ ⊢ (φ → A ≤ (A +
1)) |
|
Theorem | ltm1d 7679 |
A number minus 1 is less than itself. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) ⇒ ⊢ (φ → (A − 1) < A) |
|
Theorem | lem1d 7680 |
A number minus 1 is less than or equal to itself. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) ⇒ ⊢ (φ → (A − 1) ≤ A) |
|
Theorem | recgt0d 7681 |
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 7682 |
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 7683 |
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 7684 |
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 7685 |
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 7686 |
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 7687 |
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 7688 |
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 7689 |
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 7690 |
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 7691 |
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 7692* |
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 7693* |
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 7694* |
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 7695 |
Extend class notation to include the class of positive integers.
|
class ℕ |
|
Definition | df-inn 7696* |
Definition of the set of positive integers. For naming consistency with
the Metamath Proof Explorer usages should refer to dfnn2 7697 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 7697* |
Definition of the set of positive integers. Another name for
df-inn 7696. (Contributed by Jeff Hankins, 12-Sep-2013.)
(Revised by
Mario Carneiro, 3-May-2014.)
|
⊢ ℕ = ∩
{x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} |
|
Theorem | peano5nni 7698* |
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 7699 |
The positive integers are a subset of the reals. (Contributed by NM,
10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.)
|
⊢ ℕ ⊆ ℝ |
|
Theorem | nnsscn 7700 |
The positive integers are a subset of the complex numbers. (Contributed
by NM, 2-Aug-2004.)
|
⊢ ℕ ⊆ ℂ |