Type  Label  Description 
Statement 

Theorem  recidapd 7501 
Multiplication of a number and its reciprocal. (Contributed by Jim
Kingdon, 3Mar2020.)

# 

Theorem  recidap2d 7502 
Multiplication of a number and its reciprocal. (Contributed by Jim
Kingdon, 3Mar2020.)

#


Theorem  recrecapd 7503 
A number is equal to the reciprocal of its reciprocal. (Contributed
by Jim Kingdon, 3Mar2020.)

#


Theorem  dividapd 7504 
A number divided by itself is one. (Contributed by Jim Kingdon,
3Mar2020.)

# 

Theorem  div0apd 7505 
Division into zero is zero. (Contributed by Jim Kingdon,
3Mar2020.)

#


Theorem  apmul1 7506 
Multiplication of both sides of complex apartness by a complex number
apart from zero. (Contributed by Jim Kingdon, 20Mar2020.)

# # # 

Theorem  divclapd 7507 
Closure law for division. (Contributed by Jim Kingdon,
29Feb2020.)

# 

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

#


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

# 

Theorem  divrecapd 7510 
Relationship between division and reciprocal. Theorem I.9 of
[Apostol] p. 18. (Contributed by Jim
Kingdon, 29Feb2020.)

#


Theorem  divrecap2d 7511 
Relationship between division and reciprocal. (Contributed by Jim
Kingdon, 29Feb2020.)

#


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

#


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

#


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

# 

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

# 

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

#


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

#


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

# # # 

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

# #
# 

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

# 

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

# 

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

#


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

# # # 

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

# #


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

# #


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

# #


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

# # 

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

# #


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

#


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

#


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

#


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

# #


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

# #


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

# #


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

# #


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

# #


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

# #


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

# #


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

# # 

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

#


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

#


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

#


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

# 

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

#


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

#


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

#


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

# 

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

#


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

# 

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

# 

3.3.9 Ordering on reals (cont.)


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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  lt2msq1 7592 
Lemma for lt2msq 7593. (Contributed by Mario Carneiro,
27May2016.)



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



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



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



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



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



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



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



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

