Theorem List for Intuitionistic Logic Explorer - 8701-8800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | div23apd 8701 |
A commutative/associative law for division. (Contributed by Jim
Kingdon, 2-Mar-2020.)
|
#
|
|
Theorem | divdirapd 8702 |
Distribution of division over addition. (Contributed by Jim Kingdon,
2-Mar-2020.)
|
#
|
|
Theorem | divsubdirapd 8703 |
Distribution of division over subtraction. (Contributed by Jim
Kingdon, 2-Mar-2020.)
|
#
|
|
Theorem | div11apd 8704 |
One-to-one relationship for division. (Contributed by Jim Kingdon,
2-Mar-2020.)
|
# |
|
Theorem | divmuldivapd 8705 |
Multiplication of two ratios. (Contributed by Jim Kingdon,
30-Jul-2021.)
|
# #
|
|
Theorem | rerecclapd 8706 |
Closure law for reciprocal. (Contributed by Jim Kingdon,
29-Feb-2020.)
|
#
|
|
Theorem | redivclapd 8707 |
Closure law for division of reals. (Contributed by Jim Kingdon,
29-Feb-2020.)
|
#
|
|
Theorem | diveqap1bd 8708 |
If two complex numbers are equal, their quotient is one. One-way
deduction form of diveqap1 8578. Converse of diveqap1d 8671. (Contributed
by David Moews, 28-Feb-2017.) (Revised by Jim Kingdon, 2-Aug-2023.)
|
# |
|
Theorem | div2subap 8709 |
Swap the order of subtraction in a division. (Contributed by Scott
Fenton, 24-Jun-2013.)
|
#
|
|
Theorem | div2subapd 8710 |
Swap subtrahend and minuend inside the numerator and denominator of a
fraction. Deduction form of div2subap 8709. (Contributed by David Moews,
28-Feb-2017.)
|
#
|
|
Theorem | subrecap 8711 |
Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jul-2015.)
|
#
#
|
|
Theorem | subrecapi 8712 |
Subtraction of reciprocals. (Contributed by Scott Fenton,
9-Jan-2017.)
|
# #
|
|
Theorem | subrecapd 8713 |
Subtraction of reciprocals. (Contributed by Scott Fenton,
9-Jan-2017.)
|
#
#
|
|
Theorem | mvllmulapd 8714 |
Move LHS left multiplication to RHS. (Contributed by Jim Kingdon,
10-Jun-2020.)
|
#
|
|
4.3.9 Ordering on reals (cont.)
|
|
Theorem | ltp1 8715 |
A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
|
|
|
Theorem | lep1 8716 |
A number is less than or equal to itself plus 1. (Contributed by NM,
5-Jan-2006.)
|
|
|
Theorem | ltm1 8717 |
A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006.)
|
|
|
Theorem | lem1 8718 |
A number minus 1 is less than or equal to itself. (Contributed by Mario
Carneiro, 2-Oct-2015.)
|
|
|
Theorem | letrp1 8719 |
A transitive property of 'less than or equal' and plus 1. (Contributed by
NM, 5-Aug-2005.)
|
|
|
Theorem | p1le 8720 |
A transitive property of plus 1 and 'less than or equal'. (Contributed by
NM, 16-Aug-2005.)
|
|
|
Theorem | recgt0 8721 |
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.)
|
|
|
Theorem | prodgt0gt0 8722 |
Infer that a multiplicand is positive from a positive multiplier and
positive product. See prodgt0 8723 for the same theorem with
replaced by the weaker condition
. (Contributed by Jim
Kingdon, 29-Feb-2020.)
|
|
|
Theorem | prodgt0 8723 |
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.)
|
|
|
Theorem | prodgt02 8724 |
Infer that a multiplier is positive from a nonnegative multiplicand and
positive product. (Contributed by NM, 24-Apr-2005.)
|
|
|
Theorem | prodge0 8725 |
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.)
|
|
|
Theorem | prodge02 8726 |
Infer that a multiplier is nonnegative from a positive multiplicand and
nonnegative product. (Contributed by NM, 2-Jul-2005.)
|
|
|
Theorem | ltmul2 8727 |
Multiplication of both sides of 'less than' by a positive number. Theorem
I.19 of [Apostol] p. 20. (Contributed by
NM, 13-Feb-2005.)
|
|
|
Theorem | lemul2 8728 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by NM, 16-Mar-2005.)
|
|
|
Theorem | lemul1a 8729 |
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.)
|
|
|
Theorem | lemul2a 8730 |
Multiplication of both sides of 'less than or equal to' by a nonnegative
number. (Contributed by Paul Chapman, 7-Sep-2007.)
|
|
|
Theorem | ltmul12a 8731 |
Comparison of product of two positive numbers. (Contributed by NM,
30-Dec-2005.)
|
|
|
Theorem | lemul12b 8732 |
Comparison of product of two nonnegative numbers. (Contributed by NM,
22-Feb-2008.)
|
|
|
Theorem | lemul12a 8733 |
Comparison of product of two nonnegative numbers. (Contributed by NM,
22-Feb-2008.)
|
|
|
Theorem | mulgt1 8734 |
The product of two numbers greater than 1 is greater than 1. (Contributed
by NM, 13-Feb-2005.)
|
|
|
Theorem | ltmulgt11 8735 |
Multiplication by a number greater than 1. (Contributed by NM,
24-Dec-2005.)
|
|
|
Theorem | ltmulgt12 8736 |
Multiplication by a number greater than 1. (Contributed by NM,
24-Dec-2005.)
|
|
|
Theorem | lemulge11 8737 |
Multiplication by a number greater than or equal to 1. (Contributed by
NM, 17-Dec-2005.)
|
|
|
Theorem | lemulge12 8738 |
Multiplication by a number greater than or equal to 1. (Contributed by
Paul Chapman, 21-Mar-2011.)
|
|
|
Theorem | ltdiv1 8739 |
Division of both sides of 'less than' by a positive number. (Contributed
by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | lediv1 8740 |
Division of both sides of a less than or equal to relation by a positive
number. (Contributed by NM, 18-Nov-2004.)
|
|
|
Theorem | gt0div 8741 |
Division of a positive number by a positive number. (Contributed by NM,
28-Sep-2005.)
|
|
|
Theorem | ge0div 8742 |
Division of a nonnegative number by a positive number. (Contributed by
NM, 28-Sep-2005.)
|
|
|
Theorem | divgt0 8743 |
The ratio of two positive numbers is positive. (Contributed by NM,
12-Oct-1999.)
|
|
|
Theorem | divge0 8744 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by NM, 27-Sep-1999.)
|
|
|
Theorem | ltmuldiv 8745 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 12-Oct-1999.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | ltmuldiv2 8746 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 18-Nov-2004.)
|
|
|
Theorem | ltdivmul 8747 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 18-Nov-2004.)
|
|
|
Theorem | ledivmul 8748 |
'Less than or equal to' relationship between division and multiplication.
(Contributed by NM, 9-Dec-2005.)
|
|
|
Theorem | ltdivmul2 8749 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 24-Feb-2005.)
|
|
|
Theorem | lt2mul2div 8750 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 8-Jan-2006.)
|
|
|
Theorem | ledivmul2 8751 |
'Less than or equal to' relationship between division and multiplication.
(Contributed by NM, 9-Dec-2005.)
|
|
|
Theorem | lemuldiv 8752 |
'Less than or equal' relationship between division and multiplication.
(Contributed by NM, 10-Mar-2006.)
|
|
|
Theorem | lemuldiv2 8753 |
'Less than or equal' relationship between division and multiplication.
(Contributed by NM, 10-Mar-2006.)
|
|
|
Theorem | ltrec 8754 |
The reciprocal of both sides of 'less than'. (Contributed by NM,
26-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | lerec 8755 |
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 8756 |
Lemma for lt2msq 8757. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | lt2msq 8757 |
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 8758 |
Division of a positive number by both sides of 'less than'. (Contributed
by NM, 27-Apr-2005.)
|
|
|
Theorem | ltrec1 8759 |
Reciprocal swap in a 'less than' relation. (Contributed by NM,
24-Feb-2005.)
|
|
|
Theorem | lerec2 8760 |
Reciprocal swap in a 'less than or equal to' relation. (Contributed by
NM, 24-Feb-2005.)
|
|
|
Theorem | ledivdiv 8761 |
Invert ratios of positive numbers and swap their ordering. (Contributed
by NM, 9-Jan-2006.)
|
|
|
Theorem | lediv2 8762 |
Division of a positive number by both sides of 'less than or equal to'.
(Contributed by NM, 10-Jan-2006.)
|
|
|
Theorem | ltdiv23 8763 |
Swap denominator with other side of 'less than'. (Contributed by NM,
3-Oct-1999.)
|
|
|
Theorem | lediv23 8764 |
Swap denominator with other side of 'less than or equal to'. (Contributed
by NM, 30-May-2005.)
|
|
|
Theorem | lediv12a 8765 |
Comparison of ratio of two nonnegative numbers. (Contributed by NM,
31-Dec-2005.)
|
|
|
Theorem | lediv2a 8766 |
Division of both sides of 'less than or equal to' into a nonnegative
number. (Contributed by Paul Chapman, 7-Sep-2007.)
|
|
|
Theorem | reclt1 8767 |
The reciprocal of a positive number less than 1 is greater than 1.
(Contributed by NM, 23-Feb-2005.)
|
|
|
Theorem | recgt1 8768 |
The reciprocal of a positive number greater than 1 is less than 1.
(Contributed by NM, 28-Dec-2005.)
|
|
|
Theorem | recgt1i 8769 |
The reciprocal of a number greater than 1 is positive and less than 1.
(Contributed by NM, 23-Feb-2005.)
|
|
|
Theorem | recp1lt1 8770 |
Construct a number less than 1 from any nonnegative number. (Contributed
by NM, 30-Dec-2005.)
|
|
|
Theorem | recreclt 8771 |
Given a positive number , construct a new positive number less than
both and 1.
(Contributed by NM, 28-Dec-2005.)
|
|
|
Theorem | le2msq 8772 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 3-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | msq11 8773 |
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 8774 |
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 8775* |
If a nonnegative number is less than any positive number, it is zero.
(Contributed by NM, 11-Feb-2006.)
|
|
|
Theorem | ltp1i 8776 |
A number is less than itself plus 1. (Contributed by NM,
20-Aug-2001.)
|
|
|
Theorem | recgt0i 8777 |
The reciprocal of a positive number is positive. Exercise 4 of
[Apostol] p. 21. (Contributed by NM,
15-May-1999.)
|
|
|
Theorem | recgt0ii 8778 |
The reciprocal of a positive number is positive. Exercise 4 of
[Apostol] p. 21. (Contributed by NM,
15-May-1999.)
|
|
|
Theorem | prodgt0i 8779 |
Infer that a multiplicand is positive from a nonnegative multiplier and
positive product. (Contributed by NM, 15-May-1999.)
|
|
|
Theorem | prodge0i 8780 |
Infer that a multiplicand is nonnegative from a positive multiplier and
nonnegative product. (Contributed by NM, 2-Jul-2005.)
|
|
|
Theorem | divgt0i 8781 |
The ratio of two positive numbers is positive. (Contributed by NM,
16-May-1999.)
|
|
|
Theorem | divge0i 8782 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by NM, 12-Aug-1999.)
|
|
|
Theorem | ltreci 8783 |
The reciprocal of both sides of 'less than'. (Contributed by NM,
15-Sep-1999.)
|
|
|
Theorem | lereci 8784 |
The reciprocal of both sides of 'less than or equal to'. (Contributed
by NM, 16-Sep-1999.)
|
|
|
Theorem | lt2msqi 8785 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 3-Aug-1999.)
|
|
|
Theorem | le2msqi 8786 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 2-Aug-1999.)
|
|
|
Theorem | msq11i 8787 |
The square of a nonnegative number is a one-to-one function.
(Contributed by NM, 29-Jul-1999.)
|
|
|
Theorem | divgt0i2i 8788 |
The ratio of two positive numbers is positive. (Contributed by NM,
16-May-1999.)
|
|
|
Theorem | ltrecii 8789 |
The reciprocal of both sides of 'less than'. (Contributed by NM,
15-Sep-1999.)
|
|
|
Theorem | divgt0ii 8790 |
The ratio of two positive numbers is positive. (Contributed by NM,
18-May-1999.)
|
|
|
Theorem | ltmul1i 8791 |
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 8792 |
Division of both sides of 'less than' by a positive number.
(Contributed by NM, 16-May-1999.)
|
|
|
Theorem | ltmuldivi 8793 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 12-Oct-1999.)
|
|
|
Theorem | ltmul2i 8794 |
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 8795 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | lemul2i 8796 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by NM, 1-Aug-1999.)
|
|
|
Theorem | ltdiv23i 8797 |
Swap denominator with other side of 'less than'. (Contributed by NM,
26-Sep-1999.)
|
|
|
Theorem | ltdiv23ii 8798 |
Swap denominator with other side of 'less than'. (Contributed by NM,
26-Sep-1999.)
|
|
|
Theorem | ltmul1ii 8799 |
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 8800 |
Division of both sides of 'less than' by a positive number.
(Contributed by NM, 16-May-1999.)
|
|