Type  Label  Description 
Statement 

Theorem  divcanap3zi 7801 
A cancellation law for division. (Contributed by Jim Kingdon,
27Feb2020.)

#


Theorem  divcanap4zi 7802 
A cancellation law for division. (Contributed by Jim Kingdon,
27Feb2020.)

#


Theorem  rec11api 7803 
Reciprocal is onetoone. (Contributed by Jim Kingdon, 28Feb2020.)

# #


Theorem  divclapi 7804 
Closure law for division. (Contributed by Jim Kingdon,
28Feb2020.)

#


Theorem  divcanap2i 7805 
A cancellation law for division. (Contributed by Jim Kingdon,
28Feb2020.)

#


Theorem  divcanap1i 7806 
A cancellation law for division. (Contributed by Jim Kingdon,
28Feb2020.)

# 

Theorem  divrecapi 7807 
Relationship between division and reciprocal. (Contributed by Jim
Kingdon, 28Feb2020.)

#


Theorem  divcanap3i 7808 
A cancellation law for division. (Contributed by Jim Kingdon,
28Feb2020.)

#


Theorem  divcanap4i 7809 
A cancellation law for division. (Contributed by Jim Kingdon,
28Feb2020.)

#


Theorem  divap0i 7810 
The ratio of numbers apart from zero is apart from zero. (Contributed
by Jim Kingdon, 28Feb2020.)

# # # 

Theorem  rec11apii 7811 
Reciprocal is onetoone. (Contributed by Jim Kingdon,
28Feb2020.)

# #


Theorem  divassapzi 7812 
An associative law for division. (Contributed by Jim Kingdon,
28Feb2020.)

#


Theorem  divmulapzi 7813 
Relationship between division and multiplication. (Contributed by Jim
Kingdon, 28Feb2020.)

#


Theorem  divdirapzi 7814 
Distribution of division over addition. (Contributed by Jim Kingdon,
28Feb2020.)

#


Theorem  divdiv23apzi 7815 
Swap denominators in a division. (Contributed by Jim Kingdon,
28Feb2020.)

# #


Theorem  divmulapi 7816 
Relationship between division and multiplication. (Contributed by Jim
Kingdon, 29Feb2020.)

#


Theorem  divdiv32api 7817 
Swap denominators in a division. (Contributed by Jim Kingdon,
29Feb2020.)

# #


Theorem  divassapi 7818 
An associative law for division. (Contributed by Jim Kingdon,
9Mar2020.)

#


Theorem  divdirapi 7819 
Distribution of division over addition. (Contributed by Jim Kingdon,
9Mar2020.)

#


Theorem  div23api 7820 
A commutative/associative law for division. (Contributed by Jim
Kingdon, 9Mar2020.)

#


Theorem  div11api 7821 
Onetoone relationship for division. (Contributed by Jim Kingdon,
9Mar2020.)

#


Theorem  divmuldivapi 7822 
Multiplication of two ratios. (Contributed by Jim Kingdon,
9Mar2020.)

# #


Theorem  divmul13api 7823 
Swap denominators of two ratios. (Contributed by Jim Kingdon,
9Mar2020.)

# #


Theorem  divadddivapi 7824 
Addition of two ratios. (Contributed by Jim Kingdon, 9Mar2020.)

# #


Theorem  divdivdivapi 7825 
Division of two ratios. (Contributed by Jim Kingdon, 9Mar2020.)

# # #


Theorem  rerecclapzi 7826 
Closure law for reciprocal. (Contributed by Jim Kingdon,
9Mar2020.)

#


Theorem  rerecclapi 7827 
Closure law for reciprocal. (Contributed by Jim Kingdon,
9Mar2020.)

#


Theorem  redivclapzi 7828 
Closure law for division of reals. (Contributed by Jim Kingdon,
9Mar2020.)

#


Theorem  redivclapi 7829 
Closure law for division of reals. (Contributed by Jim Kingdon,
9Mar2020.)

#


Theorem  div1d 7830 
A number divided by 1 is itself. (Contributed by Mario Carneiro,
27May2016.)



Theorem  recclapd 7831 
Closure law for reciprocal. (Contributed by Jim Kingdon,
3Mar2020.)

#


Theorem  recap0d 7832 
The reciprocal of a number apart from zero is apart from zero.
(Contributed by Jim Kingdon, 3Mar2020.)

#
# 

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

# 

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

# 

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

#


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

# 

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

#


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

# # #


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

#


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

#


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

#


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

#


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

#


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

#


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

#


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

#


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

#


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

#


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

#


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

#
#
#


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

#
# # 

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

#


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

#


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

#


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

#
#
#


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

#
#


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

#
#


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

#
#


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

#
#


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

#
#


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

#


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

# 

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

#


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

# #


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

# # 

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

# # 

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

# # 

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

# # 

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

# # 

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

# # 

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

# #


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

#


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

#


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

# 

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

# 

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

#


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

#


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

#


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

# 

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

# #


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

#


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

#


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

#


3.3.9 Ordering on reals (cont.)


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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

