Type  Label  Description 
Statement 

Theorem  divcanap5rd 8601 
Cancellation of common factor in a ratio. (Contributed by Jim
Kingdon, 8Mar2020.)

# # 

Theorem  divcanap7d 8602 
Cancel equal divisors in a division. (Contributed by Jim Kingdon,
8Mar2020.)

# # 

Theorem  dmdcanapd 8603 
Cancellation law for division and multiplication. (Contributed by Jim
Kingdon, 8Mar2020.)

# # 

Theorem  dmdcanap2d 8604 
Cancellation law for division and multiplication. (Contributed by Jim
Kingdon, 8Mar2020.)

# # 

Theorem  divdivap1d 8605 
Division into a fraction. (Contributed by Jim Kingdon,
8Mar2020.)

# # 

Theorem  divdivap2d 8606 
Division by a fraction. (Contributed by Jim Kingdon, 8Mar2020.)

# #


Theorem  divmulap2d 8607 
Relationship between division and multiplication. (Contributed by Jim
Kingdon, 2Mar2020.)

#


Theorem  divmulap3d 8608 
Relationship between division and multiplication. (Contributed by Jim
Kingdon, 2Mar2020.)

#


Theorem  divassapd 8609 
An associative law for division. (Contributed by Jim Kingdon,
2Mar2020.)

# 

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

# 

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

#


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

#


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

#


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

# 

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

# #


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

#


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

#


Theorem  diveqap1bd 8618 
If two complex numbers are equal, their quotient is one. Oneway
deduction form of diveqap1 8488. Converse of diveqap1d 8581. (Contributed
by David Moews, 28Feb2017.) (Revised by Jim Kingdon, 2Aug2023.)

# 

Theorem  div2subap 8619 
Swap the order of subtraction in a division. (Contributed by Scott
Fenton, 24Jun2013.)

#


Theorem  div2subapd 8620 
Swap subtrahend and minuend inside the numerator and denominator of a
fraction. Deduction form of div2subap 8619. (Contributed by David Moews,
28Feb2017.)

#


Theorem  subrecap 8621 
Subtraction of reciprocals. (Contributed by Scott Fenton, 9Jul2015.)

#
#


Theorem  subrecapi 8622 
Subtraction of reciprocals. (Contributed by Scott Fenton,
9Jan2017.)

# #


Theorem  subrecapd 8623 
Subtraction of reciprocals. (Contributed by Scott Fenton,
9Jan2017.)

#
#


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

#


4.3.9 Ordering on reals (cont.)


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



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



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



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



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



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



Theorem  recgt0 8631 
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 8632 
Infer that a multiplicand is positive from a positive multiplier and
positive product. See prodgt0 8633 for the same theorem with
replaced by the weaker condition
. (Contributed by Jim
Kingdon, 29Feb2020.)



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



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



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



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



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



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



Theorem  lemul1a 8639 
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 8640 
Multiplication of both sides of 'less than or equal to' by a nonnegative
number. (Contributed by Paul Chapman, 7Sep2007.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  lt2msq1 8666 
Lemma for lt2msq 8667. (Contributed by Mario Carneiro,
27May2016.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

