Type  Label  Description 
Statement 

Theorem  divcanap4d 8201 
A cancellation law for division. (Contributed by Jim Kingdon,
29Feb2020.)

#


Theorem  diveqap0d 8202 
If a ratio is zero, the numerator is zero. (Contributed by Jim
Kingdon, 19Mar2020.)

#


Theorem  diveqap1d 8203 
Equality in terms of unit ratio. (Contributed by Jim Kingdon,
19Mar2020.)

#


Theorem  diveqap1ad 8204 
The quotient of two complex numbers is one iff they are equal.
Deduction form of diveqap1 8111. Generalization of diveqap1d 8203.
(Contributed by Jim Kingdon, 19Mar2020.)

#


Theorem  diveqap0ad 8205 
A fraction of complex numbers is zero iff its numerator is. Deduction
form of diveqap0 8088. (Contributed by Jim Kingdon, 19Mar2020.)

#


Theorem  divap1d 8206 
If two complex numbers are apart, their quotient is apart from one.
(Contributed by Jim Kingdon, 20Mar2020.)

#
#
#


Theorem  divap0bd 8207 
A ratio is zero iff the numerator is zero. (Contributed by Jim
Kingdon, 19Mar2020.)

#
# # 

Theorem  divnegapd 8208 
Move negative sign inside of a division. (Contributed by Jim Kingdon,
19Mar2020.)

#


Theorem  divneg2apd 8209 
Move negative sign inside of a division. (Contributed by Jim Kingdon,
19Mar2020.)

#


Theorem  div2negapd 8210 
Quotient of two negatives. (Contributed by Jim Kingdon,
19Mar2020.)

#


Theorem  divap0d 8211 
The ratio of numbers apart from zero is apart from zero. (Contributed
by Jim Kingdon, 3Mar2020.)

#
#
#


Theorem  recdivapd 8212 
The reciprocal of a ratio. (Contributed by Jim Kingdon,
3Mar2020.)

#
#


Theorem  recdivap2d 8213 
Division into a reciprocal. (Contributed by Jim Kingdon,
3Mar2020.)

#
#


Theorem  divcanap6d 8214 
Cancellation of inverted fractions. (Contributed by Jim Kingdon,
3Mar2020.)

#
#


Theorem  ddcanapd 8215 
Cancellation in a double division. (Contributed by Jim Kingdon,
3Mar2020.)

#
#


Theorem  rec11apd 8216 
Reciprocal is onetoone. (Contributed by Jim Kingdon,
3Mar2020.)

#
#


Theorem  divmulapd 8217 
Relationship between division and multiplication. (Contributed by Jim
Kingdon, 8Mar2020.)

#


Theorem  div32apd 8218 
A commutative/associative law for division. (Contributed by Jim
Kingdon, 8Mar2020.)

# 

Theorem  div13apd 8219 
A commutative/associative law for division. (Contributed by Jim
Kingdon, 8Mar2020.)

#


Theorem  divdiv32apd 8220 
Swap denominators in a division. (Contributed by Jim Kingdon,
8Mar2020.)

# #


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

# # 

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

# # 

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

# # 

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

# # 

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

# # 

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

# # 

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

# #


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

#


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

#


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

# 

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

# 

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

#


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

#


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

#


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

# 

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

# #


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

#


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

#


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

#


3.3.9 Ordering on reals (cont.)


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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  lt2msq1 8281 
Lemma for lt2msq 8282. (Contributed by Mario Carneiro,
27May2016.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

