Theorem List for Intuitionistic Logic Explorer - 8601-8700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ltmuldiv2 8601 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 18-Nov-2004.)
|
|
|
Theorem | ltdivmul 8602 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 18-Nov-2004.)
|
|
|
Theorem | ledivmul 8603 |
'Less than or equal to' relationship between division and multiplication.
(Contributed by NM, 9-Dec-2005.)
|
|
|
Theorem | ltdivmul2 8604 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 24-Feb-2005.)
|
|
|
Theorem | lt2mul2div 8605 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 8-Jan-2006.)
|
|
|
Theorem | ledivmul2 8606 |
'Less than or equal to' relationship between division and multiplication.
(Contributed by NM, 9-Dec-2005.)
|
|
|
Theorem | lemuldiv 8607 |
'Less than or equal' relationship between division and multiplication.
(Contributed by NM, 10-Mar-2006.)
|
|
|
Theorem | lemuldiv2 8608 |
'Less than or equal' relationship between division and multiplication.
(Contributed by NM, 10-Mar-2006.)
|
|
|
Theorem | ltrec 8609 |
The reciprocal of both sides of 'less than'. (Contributed by NM,
26-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | lerec 8610 |
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.)
|
|
|
Theorem | lt2msq1 8611 |
Lemma for lt2msq 8612. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | lt2msq 8612 |
Two nonnegative numbers compare the same as their squares. (Contributed
by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | ltdiv2 8613 |
Division of a positive number by both sides of 'less than'. (Contributed
by NM, 27-Apr-2005.)
|
|
|
Theorem | ltrec1 8614 |
Reciprocal swap in a 'less than' relation. (Contributed by NM,
24-Feb-2005.)
|
|
|
Theorem | lerec2 8615 |
Reciprocal swap in a 'less than or equal to' relation. (Contributed by
NM, 24-Feb-2005.)
|
|
|
Theorem | ledivdiv 8616 |
Invert ratios of positive numbers and swap their ordering. (Contributed
by NM, 9-Jan-2006.)
|
|
|
Theorem | lediv2 8617 |
Division of a positive number by both sides of 'less than or equal to'.
(Contributed by NM, 10-Jan-2006.)
|
|
|
Theorem | ltdiv23 8618 |
Swap denominator with other side of 'less than'. (Contributed by NM,
3-Oct-1999.)
|
|
|
Theorem | lediv23 8619 |
Swap denominator with other side of 'less than or equal to'. (Contributed
by NM, 30-May-2005.)
|
|
|
Theorem | lediv12a 8620 |
Comparison of ratio of two nonnegative numbers. (Contributed by NM,
31-Dec-2005.)
|
|
|
Theorem | lediv2a 8621 |
Division of both sides of 'less than or equal to' into a nonnegative
number. (Contributed by Paul Chapman, 7-Sep-2007.)
|
|
|
Theorem | reclt1 8622 |
The reciprocal of a positive number less than 1 is greater than 1.
(Contributed by NM, 23-Feb-2005.)
|
|
|
Theorem | recgt1 8623 |
The reciprocal of a positive number greater than 1 is less than 1.
(Contributed by NM, 28-Dec-2005.)
|
|
|
Theorem | recgt1i 8624 |
The reciprocal of a number greater than 1 is positive and less than 1.
(Contributed by NM, 23-Feb-2005.)
|
|
|
Theorem | recp1lt1 8625 |
Construct a number less than 1 from any nonnegative number. (Contributed
by NM, 30-Dec-2005.)
|
|
|
Theorem | recreclt 8626 |
Given a positive number , construct a new positive number less than
both and 1.
(Contributed by NM, 28-Dec-2005.)
|
|
|
Theorem | le2msq 8627 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 3-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | msq11 8628 |
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.)
|
|
|
Theorem | ledivp1 8629 |
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.)
|
|
|
Theorem | squeeze0 8630* |
If a nonnegative number is less than any positive number, it is zero.
(Contributed by NM, 11-Feb-2006.)
|
|
|
Theorem | ltp1i 8631 |
A number is less than itself plus 1. (Contributed by NM,
20-Aug-2001.)
|
|
|
Theorem | recgt0i 8632 |
The reciprocal of a positive number is positive. Exercise 4 of
[Apostol] p. 21. (Contributed by NM,
15-May-1999.)
|
|
|
Theorem | recgt0ii 8633 |
The reciprocal of a positive number is positive. Exercise 4 of
[Apostol] p. 21. (Contributed by NM,
15-May-1999.)
|
|
|
Theorem | prodgt0i 8634 |
Infer that a multiplicand is positive from a nonnegative multiplier and
positive product. (Contributed by NM, 15-May-1999.)
|
|
|
Theorem | prodge0i 8635 |
Infer that a multiplicand is nonnegative from a positive multiplier and
nonnegative product. (Contributed by NM, 2-Jul-2005.)
|
|
|
Theorem | divgt0i 8636 |
The ratio of two positive numbers is positive. (Contributed by NM,
16-May-1999.)
|
|
|
Theorem | divge0i 8637 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by NM, 12-Aug-1999.)
|
|
|
Theorem | ltreci 8638 |
The reciprocal of both sides of 'less than'. (Contributed by NM,
15-Sep-1999.)
|
|
|
Theorem | lereci 8639 |
The reciprocal of both sides of 'less than or equal to'. (Contributed
by NM, 16-Sep-1999.)
|
|
|
Theorem | lt2msqi 8640 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 3-Aug-1999.)
|
|
|
Theorem | le2msqi 8641 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 2-Aug-1999.)
|
|
|
Theorem | msq11i 8642 |
The square of a nonnegative number is a one-to-one function.
(Contributed by NM, 29-Jul-1999.)
|
|
|
Theorem | divgt0i2i 8643 |
The ratio of two positive numbers is positive. (Contributed by NM,
16-May-1999.)
|
|
|
Theorem | ltrecii 8644 |
The reciprocal of both sides of 'less than'. (Contributed by NM,
15-Sep-1999.)
|
|
|
Theorem | divgt0ii 8645 |
The ratio of two positive numbers is positive. (Contributed by NM,
18-May-1999.)
|
|
|
Theorem | ltmul1i 8646 |
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by NM, 16-May-1999.)
|
|
|
Theorem | ltdiv1i 8647 |
Division of both sides of 'less than' by a positive number.
(Contributed by NM, 16-May-1999.)
|
|
|
Theorem | ltmuldivi 8648 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 12-Oct-1999.)
|
|
|
Theorem | ltmul2i 8649 |
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by NM, 16-May-1999.)
|
|
|
Theorem | lemul1i 8650 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | lemul2i 8651 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by NM, 1-Aug-1999.)
|
|
|
Theorem | ltdiv23i 8652 |
Swap denominator with other side of 'less than'. (Contributed by NM,
26-Sep-1999.)
|
|
|
Theorem | ltdiv23ii 8653 |
Swap denominator with other side of 'less than'. (Contributed by NM,
26-Sep-1999.)
|
|
|
Theorem | ltmul1ii 8654 |
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.)
|
|
|
Theorem | ltdiv1ii 8655 |
Division of both sides of 'less than' by a positive number.
(Contributed by NM, 16-May-1999.)
|
|
|
Theorem | ltp1d 8656 |
A number is less than itself plus 1. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | lep1d 8657 |
A number is less than or equal to itself plus 1. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | ltm1d 8658 |
A number minus 1 is less than itself. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | lem1d 8659 |
A number minus 1 is less than or equal to itself. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | recgt0d 8660 |
The reciprocal of a positive number is positive. Exercise 4 of
[Apostol] p. 21. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | divgt0d 8661 |
The ratio of two positive numbers is positive. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | mulgt1d 8662 |
The product of two numbers greater than 1 is greater than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lemulge11d 8663 |
Multiplication by a number greater than or equal to 1. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lemulge12d 8664 |
Multiplication by a number greater than or equal to 1. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lemul1ad 8665 |
Multiplication of both sides of 'less than or equal to' by a
nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lemul2ad 8666 |
Multiplication of both sides of 'less than or equal to' by a
nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmul12ad 8667 |
Comparison of product of two positive numbers. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | lemul12ad 8668 |
Comparison of product of two nonnegative numbers. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lemul12bd 8669 |
Comparison of product of two nonnegative numbers. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | mulle0r 8670 |
Multiplying a nonnegative number by a nonpositive number yields a
nonpositive number. (Contributed by Jim Kingdon, 28-Oct-2021.)
|
|
|
4.3.10 Suprema
|
|
Theorem | lbreu 8671* |
If a set of reals contains a lower bound, it contains a unique lower
bound. (Contributed by NM, 9-Oct-2005.)
|
|
|
Theorem | lbcl 8672* |
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 8673* |
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 8674* |
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 8675* |
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 8676* |
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 8677* |
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.)
|
|
|
Theorem | suprlubex 8678* |
The supremum of a nonempty bounded set of reals is the least upper
bound. (Contributed by Jim Kingdon, 19-Jan-2022.)
|
|
|
Theorem | suprnubex 8679* |
An upper bound is not less than the supremum of a nonempty bounded set
of reals. (Contributed by Jim Kingdon, 19-Jan-2022.)
|
|
|
Theorem | suprleubex 8680* |
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.)
|
|
|
Theorem | negiso 8681 |
Negation is an order anti-isomorphism of the real numbers, which is its
own inverse. (Contributed by Mario Carneiro, 24-Dec-2016.)
|
|
|
Theorem | dfinfre 8682* |
The infimum of a set of reals . (Contributed by NM, 9-Oct-2005.)
(Revised by AV, 4-Sep-2020.)
|
inf
|
|
Theorem | sup3exmid 8683* |
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 8684 |
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.)
|
# # # |
|
Theorem | creur 8685* |
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.)
|
|
|
Theorem | creui 8686* |
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.)
|
|
|
Theorem | cju 8687* |
The complex conjugate of a complex number is unique. (Contributed by
Mario Carneiro, 6-Nov-2013.)
|
|
|
4.4 Integer sets
|
|
4.4.1 Positive integers (as a subset of complex
numbers)
|
|
Syntax | cn 8688 |
Extend class notation to include the class of positive integers.
|
|
|
Definition | df-inn 8689* |
Definition of the set of positive integers. For naming consistency with
the Metamath Proof Explorer usages should refer to dfnn2 8690 instead.
(Contributed by Jeff Hankins, 12-Sep-2013.) (Revised by Mario Carneiro,
3-May-2014.) (New usage is discouraged.)
|
|
|
Theorem | dfnn2 8690* |
Definition of the set of positive integers. Another name for df-inn 8689.
(Contributed by Jeff Hankins, 12-Sep-2013.) (Revised by Mario Carneiro,
3-May-2014.)
|
|
|
Theorem | peano5nni 8691* |
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.)
|
|
|
Theorem | nnssre 8692 |
The positive integers are a subset of the reals. (Contributed by NM,
10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.)
|
|
|
Theorem | nnsscn 8693 |
The positive integers are a subset of the complex numbers. (Contributed
by NM, 2-Aug-2004.)
|
|
|
Theorem | nnex 8694 |
The set of positive integers exists. (Contributed by NM, 3-Oct-1999.)
(Revised by Mario Carneiro, 17-Nov-2014.)
|
|
|
Theorem | nnre 8695 |
A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
|
|
|
Theorem | nncn 8696 |
A positive integer is a complex number. (Contributed by NM,
18-Aug-1999.)
|
|
|
Theorem | nnrei 8697 |
A positive integer is a real number. (Contributed by NM,
18-Aug-1999.)
|
|
|
Theorem | nncni 8698 |
A positive integer is a complex number. (Contributed by NM,
18-Aug-1999.)
|
|
|
Theorem | 1nn 8699 |
Peano postulate: 1 is a positive integer. (Contributed by NM,
11-Jan-1997.)
|
|
|
Theorem | peano2nn 8700 |
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.)
|
|