Theorem List for Intuitionistic Logic Explorer - 7901-8000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | div13apd 7901 |
A commutative/associative law for division. (Contributed by Jim
Kingdon, 8-Mar-2020.)
|
#
|
|
Theorem | divdiv32apd 7902 |
Swap denominators in a division. (Contributed by Jim Kingdon,
8-Mar-2020.)
|
# #
|
|
Theorem | divcanap5d 7903 |
Cancellation of common factor in a ratio. (Contributed by Jim
Kingdon, 8-Mar-2020.)
|
# # |
|
Theorem | divcanap5rd 7904 |
Cancellation of common factor in a ratio. (Contributed by Jim
Kingdon, 8-Mar-2020.)
|
# # |
|
Theorem | divcanap7d 7905 |
Cancel equal divisors in a division. (Contributed by Jim Kingdon,
8-Mar-2020.)
|
# # |
|
Theorem | dmdcanapd 7906 |
Cancellation law for division and multiplication. (Contributed by Jim
Kingdon, 8-Mar-2020.)
|
# # |
|
Theorem | dmdcanap2d 7907 |
Cancellation law for division and multiplication. (Contributed by Jim
Kingdon, 8-Mar-2020.)
|
# # |
|
Theorem | divdivap1d 7908 |
Division into a fraction. (Contributed by Jim Kingdon,
8-Mar-2020.)
|
# # |
|
Theorem | divdivap2d 7909 |
Division by a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.)
|
# #
|
|
Theorem | divmulap2d 7910 |
Relationship between division and multiplication. (Contributed by Jim
Kingdon, 2-Mar-2020.)
|
#
|
|
Theorem | divmulap3d 7911 |
Relationship between division and multiplication. (Contributed by Jim
Kingdon, 2-Mar-2020.)
|
#
|
|
Theorem | divassapd 7912 |
An associative law for division. (Contributed by Jim Kingdon,
2-Mar-2020.)
|
# |
|
Theorem | div12apd 7913 |
A commutative/associative law for division. (Contributed by Jim
Kingdon, 2-Mar-2020.)
|
# |
|
Theorem | div23apd 7914 |
A commutative/associative law for division. (Contributed by Jim
Kingdon, 2-Mar-2020.)
|
#
|
|
Theorem | divdirapd 7915 |
Distribution of division over addition. (Contributed by Jim Kingdon,
2-Mar-2020.)
|
#
|
|
Theorem | divsubdirapd 7916 |
Distribution of division over subtraction. (Contributed by Jim
Kingdon, 2-Mar-2020.)
|
#
|
|
Theorem | div11apd 7917 |
One-to-one relationship for division. (Contributed by Jim Kingdon,
2-Mar-2020.)
|
# |
|
Theorem | divmuldivapd 7918 |
Multiplication of two ratios. (Contributed by Jim Kingdon,
30-Jul-2021.)
|
# #
|
|
Theorem | rerecclapd 7919 |
Closure law for reciprocal. (Contributed by Jim Kingdon,
29-Feb-2020.)
|
#
|
|
Theorem | redivclapd 7920 |
Closure law for division of reals. (Contributed by Jim Kingdon,
29-Feb-2020.)
|
#
|
|
Theorem | mvllmulapd 7921 |
Move LHS left multiplication to RHS. (Contributed by Jim Kingdon,
10-Jun-2020.)
|
#
|
|
3.3.9 Ordering on reals (cont.)
|
|
Theorem | ltp1 7922 |
A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
|
|
|
Theorem | lep1 7923 |
A number is less than or equal to itself plus 1. (Contributed by NM,
5-Jan-2006.)
|
|
|
Theorem | ltm1 7924 |
A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006.)
|
|
|
Theorem | lem1 7925 |
A number minus 1 is less than or equal to itself. (Contributed by Mario
Carneiro, 2-Oct-2015.)
|
|
|
Theorem | letrp1 7926 |
A transitive property of 'less than or equal' and plus 1. (Contributed by
NM, 5-Aug-2005.)
|
|
|
Theorem | p1le 7927 |
A transitive property of plus 1 and 'less than or equal'. (Contributed by
NM, 16-Aug-2005.)
|
|
|
Theorem | recgt0 7928 |
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 7929 |
Infer that a multiplicand is positive from a positive multiplier and
positive product. See prodgt0 7930 for the same theorem with
replaced by the weaker condition
. (Contributed by Jim
Kingdon, 29-Feb-2020.)
|
|
|
Theorem | prodgt0 7930 |
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 7931 |
Infer that a multiplier is positive from a nonnegative multiplicand and
positive product. (Contributed by NM, 24-Apr-2005.)
|
|
|
Theorem | prodge0 7932 |
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 7933 |
Infer that a multiplier is nonnegative from a positive multiplicand and
nonnegative product. (Contributed by NM, 2-Jul-2005.)
|
|
|
Theorem | ltmul2 7934 |
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 7935 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by NM, 16-Mar-2005.)
|
|
|
Theorem | lemul1a 7936 |
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 7937 |
Multiplication of both sides of 'less than or equal to' by a nonnegative
number. (Contributed by Paul Chapman, 7-Sep-2007.)
|
|
|
Theorem | ltmul12a 7938 |
Comparison of product of two positive numbers. (Contributed by NM,
30-Dec-2005.)
|
|
|
Theorem | lemul12b 7939 |
Comparison of product of two nonnegative numbers. (Contributed by NM,
22-Feb-2008.)
|
|
|
Theorem | lemul12a 7940 |
Comparison of product of two nonnegative numbers. (Contributed by NM,
22-Feb-2008.)
|
|
|
Theorem | mulgt1 7941 |
The product of two numbers greater than 1 is greater than 1. (Contributed
by NM, 13-Feb-2005.)
|
|
|
Theorem | ltmulgt11 7942 |
Multiplication by a number greater than 1. (Contributed by NM,
24-Dec-2005.)
|
|
|
Theorem | ltmulgt12 7943 |
Multiplication by a number greater than 1. (Contributed by NM,
24-Dec-2005.)
|
|
|
Theorem | lemulge11 7944 |
Multiplication by a number greater than or equal to 1. (Contributed by
NM, 17-Dec-2005.)
|
|
|
Theorem | lemulge12 7945 |
Multiplication by a number greater than or equal to 1. (Contributed by
Paul Chapman, 21-Mar-2011.)
|
|
|
Theorem | ltdiv1 7946 |
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 7947 |
Division of both sides of a less than or equal to relation by a positive
number. (Contributed by NM, 18-Nov-2004.)
|
|
|
Theorem | gt0div 7948 |
Division of a positive number by a positive number. (Contributed by NM,
28-Sep-2005.)
|
|
|
Theorem | ge0div 7949 |
Division of a nonnegative number by a positive number. (Contributed by
NM, 28-Sep-2005.)
|
|
|
Theorem | divgt0 7950 |
The ratio of two positive numbers is positive. (Contributed by NM,
12-Oct-1999.)
|
|
|
Theorem | divge0 7951 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by NM, 27-Sep-1999.)
|
|
|
Theorem | ltmuldiv 7952 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 12-Oct-1999.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | ltmuldiv2 7953 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 18-Nov-2004.)
|
|
|
Theorem | ltdivmul 7954 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 18-Nov-2004.)
|
|
|
Theorem | ledivmul 7955 |
'Less than or equal to' relationship between division and multiplication.
(Contributed by NM, 9-Dec-2005.)
|
|
|
Theorem | ltdivmul2 7956 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 24-Feb-2005.)
|
|
|
Theorem | lt2mul2div 7957 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 8-Jan-2006.)
|
|
|
Theorem | ledivmul2 7958 |
'Less than or equal to' relationship between division and multiplication.
(Contributed by NM, 9-Dec-2005.)
|
|
|
Theorem | lemuldiv 7959 |
'Less than or equal' relationship between division and multiplication.
(Contributed by NM, 10-Mar-2006.)
|
|
|
Theorem | lemuldiv2 7960 |
'Less than or equal' relationship between division and multiplication.
(Contributed by NM, 10-Mar-2006.)
|
|
|
Theorem | ltrec 7961 |
The reciprocal of both sides of 'less than'. (Contributed by NM,
26-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | lerec 7962 |
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 7963 |
Lemma for lt2msq 7964. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | lt2msq 7964 |
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 7965 |
Division of a positive number by both sides of 'less than'. (Contributed
by NM, 27-Apr-2005.)
|
|
|
Theorem | ltrec1 7966 |
Reciprocal swap in a 'less than' relation. (Contributed by NM,
24-Feb-2005.)
|
|
|
Theorem | lerec2 7967 |
Reciprocal swap in a 'less than or equal to' relation. (Contributed by
NM, 24-Feb-2005.)
|
|
|
Theorem | ledivdiv 7968 |
Invert ratios of positive numbers and swap their ordering. (Contributed
by NM, 9-Jan-2006.)
|
|
|
Theorem | lediv2 7969 |
Division of a positive number by both sides of 'less than or equal to'.
(Contributed by NM, 10-Jan-2006.)
|
|
|
Theorem | ltdiv23 7970 |
Swap denominator with other side of 'less than'. (Contributed by NM,
3-Oct-1999.)
|
|
|
Theorem | lediv23 7971 |
Swap denominator with other side of 'less than or equal to'. (Contributed
by NM, 30-May-2005.)
|
|
|
Theorem | lediv12a 7972 |
Comparison of ratio of two nonnegative numbers. (Contributed by NM,
31-Dec-2005.)
|
|
|
Theorem | lediv2a 7973 |
Division of both sides of 'less than or equal to' into a nonnegative
number. (Contributed by Paul Chapman, 7-Sep-2007.)
|
|
|
Theorem | reclt1 7974 |
The reciprocal of a positive number less than 1 is greater than 1.
(Contributed by NM, 23-Feb-2005.)
|
|
|
Theorem | recgt1 7975 |
The reciprocal of a positive number greater than 1 is less than 1.
(Contributed by NM, 28-Dec-2005.)
|
|
|
Theorem | recgt1i 7976 |
The reciprocal of a number greater than 1 is positive and less than 1.
(Contributed by NM, 23-Feb-2005.)
|
|
|
Theorem | recp1lt1 7977 |
Construct a number less than 1 from any nonnegative number. (Contributed
by NM, 30-Dec-2005.)
|
|
|
Theorem | recreclt 7978 |
Given a positive number , construct a new positive number less than
both and 1.
(Contributed by NM, 28-Dec-2005.)
|
|
|
Theorem | le2msq 7979 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 3-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | msq11 7980 |
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 7981 |
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 7982* |
If a nonnegative number is less than any positive number, it is zero.
(Contributed by NM, 11-Feb-2006.)
|
|
|
Theorem | ltp1i 7983 |
A number is less than itself plus 1. (Contributed by NM,
20-Aug-2001.)
|
|
|
Theorem | recgt0i 7984 |
The reciprocal of a positive number is positive. Exercise 4 of
[Apostol] p. 21. (Contributed by NM,
15-May-1999.)
|
|
|
Theorem | recgt0ii 7985 |
The reciprocal of a positive number is positive. Exercise 4 of
[Apostol] p. 21. (Contributed by NM,
15-May-1999.)
|
|
|
Theorem | prodgt0i 7986 |
Infer that a multiplicand is positive from a nonnegative multiplier and
positive product. (Contributed by NM, 15-May-1999.)
|
|
|
Theorem | prodge0i 7987 |
Infer that a multiplicand is nonnegative from a positive multiplier and
nonnegative product. (Contributed by NM, 2-Jul-2005.)
|
|
|
Theorem | divgt0i 7988 |
The ratio of two positive numbers is positive. (Contributed by NM,
16-May-1999.)
|
|
|
Theorem | divge0i 7989 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by NM, 12-Aug-1999.)
|
|
|
Theorem | ltreci 7990 |
The reciprocal of both sides of 'less than'. (Contributed by NM,
15-Sep-1999.)
|
|
|
Theorem | lereci 7991 |
The reciprocal of both sides of 'less than or equal to'. (Contributed
by NM, 16-Sep-1999.)
|
|
|
Theorem | lt2msqi 7992 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 3-Aug-1999.)
|
|
|
Theorem | le2msqi 7993 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 2-Aug-1999.)
|
|
|
Theorem | msq11i 7994 |
The square of a nonnegative number is a one-to-one function.
(Contributed by NM, 29-Jul-1999.)
|
|
|
Theorem | divgt0i2i 7995 |
The ratio of two positive numbers is positive. (Contributed by NM,
16-May-1999.)
|
|
|
Theorem | ltrecii 7996 |
The reciprocal of both sides of 'less than'. (Contributed by NM,
15-Sep-1999.)
|
|
|
Theorem | divgt0ii 7997 |
The ratio of two positive numbers is positive. (Contributed by NM,
18-May-1999.)
|
|
|
Theorem | ltmul1i 7998 |
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 7999 |
Division of both sides of 'less than' by a positive number.
(Contributed by NM, 16-May-1999.)
|
|
|
Theorem | ltmuldivi 8000 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 12-Oct-1999.)
|
|