Type  Label  Description 
Statement 

Theorem  addext 7601 
Strong extensionality for addition. Given excluded middle, apartness
would be equivalent to negated equality and this would follow readily (for
all operations) from oveq12 5521. For us, it is proved a different way.
(Contributed by Jim Kingdon, 15Feb2020.)

#
# # 

Theorem  apneg 7602 
Negation respects apartness. (Contributed by Jim Kingdon,
14Feb2020.)

# # 

Theorem  mulext1 7603 
Left extensionality for complex multiplication. (Contributed by Jim
Kingdon, 22Feb2020.)

#
# 

Theorem  mulext2 7604 
Right extensionality for complex multiplication. (Contributed by Jim
Kingdon, 22Feb2020.)

#
# 

Theorem  mulext 7605 
Strong extensionality for multiplication. Given excluded middle,
apartness would be equivalent to negated equality and this would follow
readily (for all operations) from oveq12 5521. For us, it is proved a
different way. (Contributed by Jim Kingdon, 23Feb2020.)

#
# # 

Theorem  mulap0r 7606 
A product apart from zero. Lemma 2.13 of [Geuvers], p. 6. (Contributed
by Jim Kingdon, 24Feb2020.)

# #
# 

Theorem  msqge0 7607 
A square is nonnegative. Lemma 2.35 of [Geuvers], p. 9. (Contributed by
NM, 23May2007.) (Revised by Mario Carneiro, 27May2016.)



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



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



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



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



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



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

# 

Theorem  apne 7614 
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  leltap 7615 
'<_' implies 'less than' is 'apart'. (Contributed by Jim Kingdon,
13Aug2021.)

# 

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

#


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

#


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

# 

Theorem  gt0ap0d 7619 
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 7620 
A number is apart from zero iff its negative is apart from zero.
(Contributed by Jim Kingdon, 27Feb2020.)

# # 

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

# 

Theorem  ltap 7622 
'Less than' implies apart. (Contributed by Jim Kingdon, 12Aug2021.)

# 

Theorem  gtapii 7623 
'Greater than' implies apart. (Contributed by Jim Kingdon,
12Aug2021.)

# 

Theorem  ltapii 7624 
'Less than' implies apart. (Contributed by Jim Kingdon,
12Aug2021.)

# 

Theorem  ltapi 7625 
'Less than' implies apart. (Contributed by Jim Kingdon,
12Aug2021.)

# 

Theorem  gtapd 7626 
'Greater than' implies apart. (Contributed by Jim Kingdon,
12Aug2021.)

# 

Theorem  ltapd 7627 
'Less than' implies apart. (Contributed by Jim Kingdon,
12Aug2021.)

# 

Theorem  leltapd 7628 
'<_' implies 'less than' is 'apart'. (Contributed by Jim Kingdon,
13Aug2021.)

#


Theorem  ap0gt0 7629 
A nonnegative number is apart from zero if and only if it is positive.
(Contributed by Jim Kingdon, 11Aug2021.)

# 

Theorem  ap0gt0d 7630 
A nonzero nonnegative number is positive. (Contributed by Jim
Kingdon, 11Aug2021.)

# 

Theorem  subap0d 7631 
Two numbers apart from each other have difference apart from zero.
(Contributed by Jim Kingdon, 12Aug2021.)

#
#


3.3.7 Reciprocals


Theorem  recextlem1 7632 
Lemma for recexap 7634. (Contributed by Eric Schmidt, 23May2007.)



Theorem  recexaplem2 7633 
Lemma for recexap 7634. (Contributed by Jim Kingdon, 20Feb2020.)

#
# 

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

#


Theorem  mulap0 7635 
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 7636 
The product of two numbers apart from zero is apart from zero.
(Contributed by Jim Kingdon, 24Feb2020.)

# # # 

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

# # # 

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

# # #


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

#
#
#


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

#
#


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

#
#


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

#


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

#


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

# 

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

# 

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

#


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

#


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

#


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



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

#


3.3.8 Division


Syntax  cdiv 7651 
Extend class notation to include division.



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



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

#


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

#


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

#


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

#


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

#


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

#


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

#


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

#


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

#


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

# #
#


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

#
#
# 

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

# # 

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

#


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

#


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

#


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

#


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

#


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

#


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

# 

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

# 

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

#


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

#


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

#


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

#


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

#


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

#


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

#


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



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



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

#


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

#


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

#


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

#


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

#
#


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

#
#


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

#
#


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

# # #


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

# #


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

#
#


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

#
#


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

#
#


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

#
# 

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

#
#


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

# #


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

# #


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

#
#


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

# #


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

# #
