Type  Label  Description 
Statement 

Theorem  msqge0i 7401 
A square is nonnegative. (Contributed by NM, 14May1999.) (Proof
shortened by Andrew Salmon, 19Nov2011.)



Theorem  msqge0d 7402 
A square is nonnegative. (Contributed by Mario Carneiro,
27May2016.)



Theorem  mulge0 7403 
The product of two nonnegative numbers is nonnegative. (Contributed by
NM, 8Oct1999.) (Revised by Mario Carneiro, 27May2016.)



Theorem  mulge0i 7404 
The product of two nonnegative numbers is nonnegative. (Contributed by
NM, 30Jul1999.)



Theorem  mulge0d 7405 
The product of two nonnegative numbers is nonnegative. (Contributed by
Mario Carneiro, 27May2016.)



Theorem  apti 7406 
Complex apartness is tight. (Contributed by Jim Kingdon,
21Feb2020.)

# 

Theorem  apne 7407 
Apartness implies negated equality. We cannot in general prove the
converse, which is the whole point of having separate notations for
apartness and negated equality. (Contributed by Jim Kingdon,
21Feb2020.)

# 

Theorem  gt0ap0 7408 
Positive implies apart from zero. (Contributed by Jim Kingdon,
27Feb2020.)

# 

Theorem  gt0ap0i 7409 
Positive means apart from zero (useful for ordering theorems involving
division). (Contributed by Jim Kingdon, 27Feb2020.)

# 

Theorem  gt0ap0ii 7410 
Positive implies apart from zero. (Contributed by Jim Kingdon,
27Feb2020.)

# 

Theorem  gt0ap0d 7411 
Positive implies apart from zero. Because of the way we define #,
must be an
element of , not
just .
(Contributed by
Jim Kingdon, 27Feb2020.)

# 

Theorem  negap0 7412 
A number is apart from zero iff its negative is apart from zero.
(Contributed by Jim Kingdon, 27Feb2020.)

# # 

Theorem  ltleap 7413 
Less than in terms of nonstrict order and apartness. (Contributed by Jim
Kingdon, 28Feb2020.)

# 

3.3.7 Reciprocals


Theorem  recextlem1 7414 
Lemma for recexap 7416. (Contributed by Eric Schmidt, 23May2007.)



Theorem  recexaplem2 7415 
Lemma for recexap 7416. (Contributed by Jim Kingdon, 20Feb2020.)

#
# 

Theorem  recexap 7416* 
Existence of reciprocal of nonzero complex number. (Contributed by Jim
Kingdon, 20Feb2020.)

#


Theorem  mulap0 7417 
The product of two numbers apart from zero is apart from zero. Lemma
2.15 of [Geuvers], p. 6. (Contributed
by Jim Kingdon, 22Feb2020.)

#
# # 

Theorem  mulap0b 7418 
The product of two numbers apart from zero is apart from zero.
(Contributed by Jim Kingdon, 24Feb2020.)

# # # 

Theorem  mulap0i 7419 
The product of two numbers apart from zero is apart from zero.
(Contributed by Jim Kingdon, 23Feb2020.)

# # # 

Theorem  mulap0bd 7420 
The product of two numbers apart from zero is apart from zero.
(Contributed by Jim Kingdon, 24Feb2020.)

# # # 

Theorem  mulap0d 7421 
The product of two numbers apart from zero is apart from zero.
(Contributed by Jim Kingdon, 23Feb2020.)

# # # 

Theorem  mulap0bad 7422 
A factor of a complex number apart from zero is apart from zero.
Partial converse of mulap0d 7421 and consequence of mulap0bd 7420.
(Contributed by Jim Kingdon, 24Feb2020.)

# # 

Theorem  mulap0bbd 7423 
A factor of a complex number apart from zero is apart from zero.
Partial converse of mulap0d 7421 and consequence of mulap0bd 7420.
(Contributed by Jim Kingdon, 24Feb2020.)

# # 

Theorem  mulcanapd 7424 
Cancellation law for multiplication. (Contributed by Jim Kingdon,
21Feb2020.)

#


Theorem  mulcanap2d 7425 
Cancellation law for multiplication. (Contributed by Jim Kingdon,
21Feb2020.)

#


Theorem  mulcanapad 7426 
Cancellation of a nonzero factor on the left in an equation. Oneway
deduction form of mulcanapd 7424. (Contributed by Jim Kingdon,
21Feb2020.)

# 

Theorem  mulcanap2ad 7427 
Cancellation of a nonzero factor on the right in an equation. Oneway
deduction form of mulcanap2d 7425. (Contributed by Jim Kingdon,
21Feb2020.)

# 

Theorem  mulcanap 7428 
Cancellation law for multiplication (full theorem form). (Contributed by
Jim Kingdon, 21Feb2020.)

#


Theorem  mulcanap2 7429 
Cancellation law for multiplication. (Contributed by Jim Kingdon,
21Feb2020.)

#


Theorem  mulcanapi 7430 
Cancellation law for multiplication. (Contributed by Jim Kingdon,
21Feb2020.)

#


Theorem  muleqadd 7431 
Property of numbers whose product equals their sum. Equation 5 of
[Kreyszig] p. 12. (Contributed by NM,
13Nov2006.)



Theorem  receuap 7432* 
Existential uniqueness of reciprocals. (Contributed by Jim Kingdon,
21Feb2020.)

# 

3.3.8 Division


Syntax  cdiv 7433 
Extend class notation to include division.



Definition  dfdiv 7434* 
Define division. Theorem divmulap 7436 relates it to multiplication, and
divclap 7439 and redivclap 7489 prove its closure laws. (Contributed by NM,
2Feb1995.) (Revised by Mario Carneiro, 1Apr2014.)
(New usage is discouraged.)



Theorem  divvalap 7435* 
Value of division: the (unique) element such that
. This is meaningful only when is apart from
zero. (Contributed by Jim Kingdon, 21Feb2020.)

#


Theorem  divmulap 7436 
Relationship between division and multiplication. (Contributed by Jim
Kingdon, 22Feb2020.)

#


Theorem  divmulap2 7437 
Relationship between division and multiplication. (Contributed by Jim
Kingdon, 22Feb2020.)

#


Theorem  divmulap3 7438 
Relationship between division and multiplication. (Contributed by Jim
Kingdon, 22Feb2020.)

#


Theorem  divclap 7439 
Closure law for division. (Contributed by Jim Kingdon, 22Feb2020.)

# 

Theorem  recclap 7440 
Closure law for reciprocal. (Contributed by Jim Kingdon, 22Feb2020.)

# 

Theorem  divcanap2 7441 
A cancellation law for division. (Contributed by Jim Kingdon,
22Feb2020.)

# 

Theorem  divcanap1 7442 
A cancellation law for division. (Contributed by Jim Kingdon,
22Feb2020.)

#


Theorem  diveqap0 7443 
A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon,
22Feb2020.)

#


Theorem  divap0b 7444 
The ratio of numbers apart from zero is apart from zero. (Contributed by
Jim Kingdon, 22Feb2020.)

# #
# 

Theorem  divap0 7445 
The ratio of numbers apart from zero is apart from zero. (Contributed by
Jim Kingdon, 22Feb2020.)

#
# # 

Theorem  recap0 7446 
The reciprocal of a number apart from zero is apart from zero.
(Contributed by Jim Kingdon, 24Feb2020.)

# # 

Theorem  recidap 7447 
Multiplication of a number and its reciprocal. (Contributed by Jim
Kingdon, 24Feb2020.)

#


Theorem  recidap2 7448 
Multiplication of a number and its reciprocal. (Contributed by Jim
Kingdon, 24Feb2020.)

#


Theorem  divrecap 7449 
Relationship between division and reciprocal. (Contributed by Jim
Kingdon, 24Feb2020.)

#


Theorem  divrecap2 7450 
Relationship between division and reciprocal. (Contributed by Jim
Kingdon, 25Feb2020.)

#


Theorem  divassap 7451 
An associative law for division. (Contributed by Jim Kingdon,
25Feb2020.)

#


Theorem  div23ap 7452 
A commutative/associative law for division. (Contributed by Jim Kingdon,
25Feb2020.)

#


Theorem  div32ap 7453 
A commutative/associative law for division. (Contributed by Jim Kingdon,
25Feb2020.)

#


Theorem  div13ap 7454 
A commutative/associative law for division. (Contributed by Jim Kingdon,
25Feb2020.)

#


Theorem  div12ap 7455 
A commutative/associative law for division. (Contributed by Jim Kingdon,
25Feb2020.)

#


Theorem  divdirap 7456 
Distribution of division over addition. (Contributed by Jim Kingdon,
25Feb2020.)

#


Theorem  divcanap3 7457 
A cancellation law for division. (Contributed by Jim Kingdon,
25Feb2020.)

#


Theorem  divcanap4 7458 
A cancellation law for division. (Contributed by Jim Kingdon,
25Feb2020.)

#


Theorem  div11ap 7459 
Onetoone relationship for division. (Contributed by Jim Kingdon,
25Feb2020.)

#


Theorem  dividap 7460 
A number divided by itself is one. (Contributed by Jim Kingdon,
25Feb2020.)

#


Theorem  div0ap 7461 
Division into zero is zero. (Contributed by Jim Kingdon, 25Feb2020.)

#


Theorem  div1 7462 
A number divided by 1 is itself. (Contributed by NM, 9Jan2002.) (Proof
shortened by Mario Carneiro, 27May2016.)



Theorem  1div1e1 7463 
1 divided by 1 is 1 (common case). (Contributed by David A. Wheeler,
7Dec2018.)



Theorem  diveqap1 7464 
Equality in terms of unit ratio. (Contributed by Jim Kingdon,
25Feb2020.)

#


Theorem  divnegap 7465 
Move negative sign inside of a division. (Contributed by Jim Kingdon,
25Feb2020.)

# 

Theorem  divsubdirap 7466 
Distribution of division over subtraction. (Contributed by NM,
4Mar2005.)

#


Theorem  recrecap 7467 
A number is equal to the reciprocal of its reciprocal. (Contributed by
Jim Kingdon, 25Feb2020.)

#


Theorem  rec11ap 7468 
Reciprocal is onetoone. (Contributed by Jim Kingdon, 25Feb2020.)

#
#


Theorem  rec11rap 7469 
Mutual reciprocals. (Contributed by Jim Kingdon, 25Feb2020.)

#
#


Theorem  divmuldivap 7470 
Multiplication of two ratios. (Contributed by Jim Kingdon,
25Feb2020.)

#
# 

Theorem  divdivdivap 7471 
Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by
Jim Kingdon, 25Feb2020.)

#
#
#


Theorem  divcanap5 7472 
Cancellation of common factor in a ratio. (Contributed by Jim Kingdon,
25Feb2020.)

# #


Theorem  divmul13ap 7473 
Swap the denominators in the product of two ratios. (Contributed by Jim
Kingdon, 26Feb2020.)

#
# 

Theorem  divmul24ap 7474 
Swap the numerators in the product of two ratios. (Contributed by Jim
Kingdon, 26Feb2020.)

#
# 

Theorem  divmuleqap 7475 
Crossmultiply in an equality of ratios. (Contributed by Jim Kingdon,
26Feb2020.)

#
#


Theorem  recdivap 7476 
The reciprocal of a ratio. (Contributed by Jim Kingdon, 26Feb2020.)

#
#


Theorem  divcanap6 7477 
Cancellation of inverted fractions. (Contributed by Jim Kingdon,
26Feb2020.)

#
#


Theorem  divdiv32ap 7478 
Swap denominators in a division. (Contributed by Jim Kingdon,
26Feb2020.)

# #


Theorem  divcanap7 7479 
Cancel equal divisors in a division. (Contributed by Jim Kingdon,
26Feb2020.)

# #


Theorem  dmdcanap 7480 
Cancellation law for division and multiplication. (Contributed by Jim
Kingdon, 26Feb2020.)

#
#


Theorem  divdivap1 7481 
Division into a fraction. (Contributed by Jim Kingdon, 26Feb2020.)

# #


Theorem  divdivap2 7482 
Division by a fraction. (Contributed by Jim Kingdon, 26Feb2020.)

# # 

Theorem  recdivap2 7483 
Division into a reciprocal. (Contributed by Jim Kingdon, 26Feb2020.)

#
#


Theorem  ddcanap 7484 
Cancellation in a double division. (Contributed by Jim Kingdon,
26Feb2020.)

#
# 

Theorem  divadddivap 7485 
Addition of two ratios. (Contributed by Jim Kingdon, 26Feb2020.)

#
#


Theorem  divsubdivap 7486 
Subtraction of two ratios. (Contributed by Jim Kingdon, 26Feb2020.)

#
#


Theorem  conjmulap 7487 
Two numbers whose reciprocals sum to 1 are called "conjugates" and
satisfy
this relationship. (Contributed by Jim Kingdon, 26Feb2020.)

#
#


Theorem  rerecclap 7488 
Closure law for reciprocal. (Contributed by Jim Kingdon,
26Feb2020.)

# 

Theorem  redivclap 7489 
Closure law for division of reals. (Contributed by Jim Kingdon,
26Feb2020.)

# 

Theorem  eqneg 7490 
A number equal to its negative is zero. (Contributed by NM,
12Jul2005.) (Revised by Mario Carneiro, 27May2016.)



Theorem  eqnegd 7491 
A complex number equals its negative iff it is zero. Deduction form of
eqneg 7490. (Contributed by David Moews, 28Feb2017.)



Theorem  eqnegad 7492 
If a complex number equals its own negative, it is zero. Oneway
deduction form of eqneg 7490. (Contributed by David Moews,
28Feb2017.)



Theorem  div2negap 7493 
Quotient of two negatives. (Contributed by Jim Kingdon, 27Feb2020.)

#


Theorem  divneg2ap 7494 
Move negative sign inside of a division. (Contributed by Jim Kingdon,
27Feb2020.)

# 

Theorem  recclapzi 7495 
Closure law for reciprocal. (Contributed by Jim Kingdon,
27Feb2020.)

#


Theorem  recap0apzi 7496 
The reciprocal of a number apart from zero is apart from zero.
(Contributed by Jim Kingdon, 27Feb2020.)

#
# 

Theorem  recidapzi 7497 
Multiplication of a number and its reciprocal. (Contributed by Jim
Kingdon, 27Feb2020.)

#


Theorem  div1i 7498 
A number divided by 1 is itself. (Contributed by NM, 9Jan2002.)



Theorem  eqnegi 7499 
A number equal to its negative is zero. (Contributed by NM,
29May1999.)



Theorem  recclapi 7500 
Closure law for reciprocal. (Contributed by NM, 30Apr2005.)

# 