Type  Label  Description 
Statement 

Theorem  div12apd 7801 
A commutative/associative law for division. (Contributed by Jim
Kingdon, 2Mar2020.)

# 

Theorem  div23apd 7802 
A commutative/associative law for division. (Contributed by Jim
Kingdon, 2Mar2020.)

#


Theorem  divdirapd 7803 
Distribution of division over addition. (Contributed by Jim Kingdon,
2Mar2020.)

#


Theorem  divsubdirapd 7804 
Distribution of division over subtraction. (Contributed by Jim
Kingdon, 2Mar2020.)

#


Theorem  div11apd 7805 
Onetoone relationship for division. (Contributed by Jim Kingdon,
2Mar2020.)

# 

Theorem  divmuldivapd 7806 
Multiplication of two ratios. (Contributed by Jim Kingdon,
30Jul2021.)

# #


Theorem  rerecclapd 7807 
Closure law for reciprocal. (Contributed by Jim Kingdon,
29Feb2020.)

#


Theorem  redivclapd 7808 
Closure law for division of reals. (Contributed by Jim Kingdon,
29Feb2020.)

#


Theorem  mvllmulapd 7809 
Move LHS left multiplication to RHS. (Contributed by Jim Kingdon,
10Jun2020.)

#


3.3.9 Ordering on reals (cont.)


Theorem  ltp1 7810 
A number is less than itself plus 1. (Contributed by NM, 20Aug2001.)



Theorem  lep1 7811 
A number is less than or equal to itself plus 1. (Contributed by NM,
5Jan2006.)



Theorem  ltm1 7812 
A number minus 1 is less than itself. (Contributed by NM, 9Apr2006.)



Theorem  lem1 7813 
A number minus 1 is less than or equal to itself. (Contributed by Mario
Carneiro, 2Oct2015.)



Theorem  letrp1 7814 
A transitive property of 'less than or equal' and plus 1. (Contributed by
NM, 5Aug2005.)



Theorem  p1le 7815 
A transitive property of plus 1 and 'less than or equal'. (Contributed by
NM, 16Aug2005.)



Theorem  recgt0 7816 
The reciprocal of a positive number is positive. Exercise 4 of [Apostol]
p. 21. (Contributed by NM, 25Aug1999.) (Revised by Mario Carneiro,
27May2016.)



Theorem  prodgt0gt0 7817 
Infer that a multiplicand is positive from a positive multiplier and
positive product. See prodgt0 7818 for the same theorem with
replaced by the weaker condition
. (Contributed by Jim
Kingdon, 29Feb2020.)



Theorem  prodgt0 7818 
Infer that a multiplicand is positive from a nonnegative multiplier and
positive product. (Contributed by NM, 24Apr2005.) (Revised by Mario
Carneiro, 27May2016.)



Theorem  prodgt02 7819 
Infer that a multiplier is positive from a nonnegative multiplicand and
positive product. (Contributed by NM, 24Apr2005.)



Theorem  prodge0 7820 
Infer that a multiplicand is nonnegative from a positive multiplier and
nonnegative product. (Contributed by NM, 2Jul2005.) (Revised by Mario
Carneiro, 27May2016.)



Theorem  prodge02 7821 
Infer that a multiplier is nonnegative from a positive multiplicand and
nonnegative product. (Contributed by NM, 2Jul2005.)



Theorem  ltmul2 7822 
Multiplication of both sides of 'less than' by a positive number. Theorem
I.19 of [Apostol] p. 20. (Contributed by
NM, 13Feb2005.)



Theorem  lemul2 7823 
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by NM, 16Mar2005.)



Theorem  lemul1a 7824 
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, 21Feb2005.)



Theorem  lemul2a 7825 
Multiplication of both sides of 'less than or equal to' by a nonnegative
number. (Contributed by Paul Chapman, 7Sep2007.)



Theorem  ltmul12a 7826 
Comparison of product of two positive numbers. (Contributed by NM,
30Dec2005.)



Theorem  lemul12b 7827 
Comparison of product of two nonnegative numbers. (Contributed by NM,
22Feb2008.)



Theorem  lemul12a 7828 
Comparison of product of two nonnegative numbers. (Contributed by NM,
22Feb2008.)



Theorem  mulgt1 7829 
The product of two numbers greater than 1 is greater than 1. (Contributed
by NM, 13Feb2005.)



Theorem  ltmulgt11 7830 
Multiplication by a number greater than 1. (Contributed by NM,
24Dec2005.)



Theorem  ltmulgt12 7831 
Multiplication by a number greater than 1. (Contributed by NM,
24Dec2005.)



Theorem  lemulge11 7832 
Multiplication by a number greater than or equal to 1. (Contributed by
NM, 17Dec2005.)



Theorem  lemulge12 7833 
Multiplication by a number greater than or equal to 1. (Contributed by
Paul Chapman, 21Mar2011.)



Theorem  ltdiv1 7834 
Division of both sides of 'less than' by a positive number. (Contributed
by NM, 10Oct2004.) (Revised by Mario Carneiro, 27May2016.)



Theorem  lediv1 7835 
Division of both sides of a less than or equal to relation by a positive
number. (Contributed by NM, 18Nov2004.)



Theorem  gt0div 7836 
Division of a positive number by a positive number. (Contributed by NM,
28Sep2005.)



Theorem  ge0div 7837 
Division of a nonnegative number by a positive number. (Contributed by
NM, 28Sep2005.)



Theorem  divgt0 7838 
The ratio of two positive numbers is positive. (Contributed by NM,
12Oct1999.)



Theorem  divge0 7839 
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by NM, 27Sep1999.)



Theorem  ltmuldiv 7840 
'Less than' relationship between division and multiplication.
(Contributed by NM, 12Oct1999.) (Proof shortened by Mario Carneiro,
27May2016.)



Theorem  ltmuldiv2 7841 
'Less than' relationship between division and multiplication.
(Contributed by NM, 18Nov2004.)



Theorem  ltdivmul 7842 
'Less than' relationship between division and multiplication.
(Contributed by NM, 18Nov2004.)



Theorem  ledivmul 7843 
'Less than or equal to' relationship between division and multiplication.
(Contributed by NM, 9Dec2005.)



Theorem  ltdivmul2 7844 
'Less than' relationship between division and multiplication.
(Contributed by NM, 24Feb2005.)



Theorem  lt2mul2div 7845 
'Less than' relationship between division and multiplication.
(Contributed by NM, 8Jan2006.)



Theorem  ledivmul2 7846 
'Less than or equal to' relationship between division and multiplication.
(Contributed by NM, 9Dec2005.)



Theorem  lemuldiv 7847 
'Less than or equal' relationship between division and multiplication.
(Contributed by NM, 10Mar2006.)



Theorem  lemuldiv2 7848 
'Less than or equal' relationship between division and multiplication.
(Contributed by NM, 10Mar2006.)



Theorem  ltrec 7849 
The reciprocal of both sides of 'less than'. (Contributed by NM,
26Sep1999.) (Revised by Mario Carneiro, 27May2016.)



Theorem  lerec 7850 
The reciprocal of both sides of 'less than or equal to'. (Contributed by
NM, 3Oct1999.) (Proof shortened by Mario Carneiro, 27May2016.)



Theorem  lt2msq1 7851 
Lemma for lt2msq 7852. (Contributed by Mario Carneiro,
27May2016.)



Theorem  lt2msq 7852 
Two nonnegative numbers compare the same as their squares. (Contributed
by Roy F. Longton, 8Aug2005.) (Revised by Mario Carneiro,
27May2016.)



Theorem  ltdiv2 7853 
Division of a positive number by both sides of 'less than'. (Contributed
by NM, 27Apr2005.)



Theorem  ltrec1 7854 
Reciprocal swap in a 'less than' relation. (Contributed by NM,
24Feb2005.)



Theorem  lerec2 7855 
Reciprocal swap in a 'less than or equal to' relation. (Contributed by
NM, 24Feb2005.)



Theorem  ledivdiv 7856 
Invert ratios of positive numbers and swap their ordering. (Contributed
by NM, 9Jan2006.)



Theorem  lediv2 7857 
Division of a positive number by both sides of 'less than or equal to'.
(Contributed by NM, 10Jan2006.)



Theorem  ltdiv23 7858 
Swap denominator with other side of 'less than'. (Contributed by NM,
3Oct1999.)



Theorem  lediv23 7859 
Swap denominator with other side of 'less than or equal to'. (Contributed
by NM, 30May2005.)



Theorem  lediv12a 7860 
Comparison of ratio of two nonnegative numbers. (Contributed by NM,
31Dec2005.)



Theorem  lediv2a 7861 
Division of both sides of 'less than or equal to' into a nonnegative
number. (Contributed by Paul Chapman, 7Sep2007.)



Theorem  reclt1 7862 
The reciprocal of a positive number less than 1 is greater than 1.
(Contributed by NM, 23Feb2005.)



Theorem  recgt1 7863 
The reciprocal of a positive number greater than 1 is less than 1.
(Contributed by NM, 28Dec2005.)



Theorem  recgt1i 7864 
The reciprocal of a number greater than 1 is positive and less than 1.
(Contributed by NM, 23Feb2005.)



Theorem  recp1lt1 7865 
Construct a number less than 1 from any nonnegative number. (Contributed
by NM, 30Dec2005.)



Theorem  recreclt 7866 
Given a positive number , construct a new positive number less than
both and 1.
(Contributed by NM, 28Dec2005.)



Theorem  le2msq 7867 
The square function on nonnegative reals is monotonic. (Contributed by
NM, 3Aug1999.) (Proof shortened by Mario Carneiro, 27May2016.)



Theorem  msq11 7868 
The square of a nonnegative number is a onetoone function. (Contributed
by NM, 29Jul1999.) (Revised by Mario Carneiro, 27May2016.)



Theorem  ledivp1 7869 
Lessthanorequalto and division relation. (Lemma for computing upper
bounds of products. The "+ 1" prevents division by zero.)
(Contributed
by NM, 28Sep2005.)



Theorem  squeeze0 7870* 
If a nonnegative number is less than any positive number, it is zero.
(Contributed by NM, 11Feb2006.)



Theorem  ltp1i 7871 
A number is less than itself plus 1. (Contributed by NM,
20Aug2001.)



Theorem  recgt0i 7872 
The reciprocal of a positive number is positive. Exercise 4 of
[Apostol] p. 21. (Contributed by NM,
15May1999.)



Theorem  recgt0ii 7873 
The reciprocal of a positive number is positive. Exercise 4 of
[Apostol] p. 21. (Contributed by NM,
15May1999.)



Theorem  prodgt0i 7874 
Infer that a multiplicand is positive from a nonnegative multiplier and
positive product. (Contributed by NM, 15May1999.)



Theorem  prodge0i 7875 
Infer that a multiplicand is nonnegative from a positive multiplier and
nonnegative product. (Contributed by NM, 2Jul2005.)



Theorem  divgt0i 7876 
The ratio of two positive numbers is positive. (Contributed by NM,
16May1999.)



Theorem  divge0i 7877 
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by NM, 12Aug1999.)



Theorem  ltreci 7878 
The reciprocal of both sides of 'less than'. (Contributed by NM,
15Sep1999.)



Theorem  lereci 7879 
The reciprocal of both sides of 'less than or equal to'. (Contributed
by NM, 16Sep1999.)



Theorem  lt2msqi 7880 
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 3Aug1999.)



Theorem  le2msqi 7881 
The square function on nonnegative reals is monotonic. (Contributed by
NM, 2Aug1999.)



Theorem  msq11i 7882 
The square of a nonnegative number is a onetoone function.
(Contributed by NM, 29Jul1999.)



Theorem  divgt0i2i 7883 
The ratio of two positive numbers is positive. (Contributed by NM,
16May1999.)



Theorem  ltrecii 7884 
The reciprocal of both sides of 'less than'. (Contributed by NM,
15Sep1999.)



Theorem  divgt0ii 7885 
The ratio of two positive numbers is positive. (Contributed by NM,
18May1999.)



Theorem  ltmul1i 7886 
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by NM, 16May1999.)



Theorem  ltdiv1i 7887 
Division of both sides of 'less than' by a positive number.
(Contributed by NM, 16May1999.)



Theorem  ltmuldivi 7888 
'Less than' relationship between division and multiplication.
(Contributed by NM, 12Oct1999.)



Theorem  ltmul2i 7889 
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by NM, 16May1999.)



Theorem  lemul1i 7890 
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by NM, 2Aug1999.)



Theorem  lemul2i 7891 
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by NM, 1Aug1999.)



Theorem  ltdiv23i 7892 
Swap denominator with other side of 'less than'. (Contributed by NM,
26Sep1999.)



Theorem  ltdiv23ii 7893 
Swap denominator with other side of 'less than'. (Contributed by NM,
26Sep1999.)



Theorem  ltmul1ii 7894 
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by NM, 16May1999.)
(Proof shortened by Paul Chapman, 25Jan2008.)



Theorem  ltdiv1ii 7895 
Division of both sides of 'less than' by a positive number.
(Contributed by NM, 16May1999.)



Theorem  ltp1d 7896 
A number is less than itself plus 1. (Contributed by Mario Carneiro,
28May2016.)



Theorem  lep1d 7897 
A number is less than or equal to itself plus 1. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  ltm1d 7898 
A number minus 1 is less than itself. (Contributed by Mario Carneiro,
28May2016.)



Theorem  lem1d 7899 
A number minus 1 is less than or equal to itself. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  recgt0d 7900 
The reciprocal of a positive number is positive. Exercise 4 of
[Apostol] p. 21. (Contributed by
Mario Carneiro, 28May2016.)

