Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  lt2msq1 7632 
Lemma for lt2msq 7633. (Contributed by Mario Carneiro,
27May2016.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  recgt0i 7653 
The reciprocal of a positive number is positive. Exercise 4 of
[Apostol] p. 21. (Contributed by NM,
15May1999.)



Theorem  recgt0ii 7654 
The reciprocal of a positive number is positive. Exercise 4 of
[Apostol] p. 21. (Contributed by NM,
15May1999.)



Theorem  prodgt0i 7655 
Infer that a multiplicand is positive from a nonnegative multiplier and
positive product. (Contributed by NM, 15May1999.)



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



Theorem  divgt0i 7657 
The ratio of two positive numbers is positive. (Contributed by NM,
16May1999.)



Theorem  divge0i 7658 
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by NM, 12Aug1999.)



Theorem  ltreci 7659 
The reciprocal of both sides of 'less than'. (Contributed by NM,
15Sep1999.)



Theorem  lereci 7660 
The reciprocal of both sides of 'less than or equal to'. (Contributed
by NM, 16Sep1999.)



Theorem  lt2msqi 7661 
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 3Aug1999.)



Theorem  le2msqi 7662 
The square function on nonnegative reals is monotonic. (Contributed by
NM, 2Aug1999.)



Theorem  msq11i 7663 
The square of a nonnegative number is a onetoone function.
(Contributed by NM, 29Jul1999.)



Theorem  divgt0i2i 7664 
The ratio of two positive numbers is positive. (Contributed by NM,
16May1999.)



Theorem  ltrecii 7665 
The reciprocal of both sides of 'less than'. (Contributed by NM,
15Sep1999.)



Theorem  divgt0ii 7666 
The ratio of two positive numbers is positive. (Contributed by NM,
18May1999.)



Theorem  ltmul1i 7667 
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by NM, 16May1999.)



Theorem  ltdiv1i 7668 
Division of both sides of 'less than' by a positive number.
(Contributed by NM, 16May1999.)



Theorem  ltmuldivi 7669 
'Less than' relationship between division and multiplication.
(Contributed by NM, 12Oct1999.)



Theorem  ltmul2i 7670 
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by NM, 16May1999.)



Theorem  lemul1i 7671 
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by NM, 2Aug1999.)



Theorem  lemul2i 7672 
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by NM, 1Aug1999.)



Theorem  ltdiv23i 7673 
Swap denominator with other side of 'less than'. (Contributed by NM,
26Sep1999.)



Theorem  ltdiv23ii 7674 
Swap denominator with other side of 'less than'. (Contributed by NM,
26Sep1999.)



Theorem  ltmul1ii 7675 
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by NM, 16May1999.)
(Proof shortened by Paul Chapman, 25Jan2008.)



Theorem  ltdiv1ii 7676 
Division of both sides of 'less than' by a positive number.
(Contributed by NM, 16May1999.)



Theorem  ltp1d 7677 
A number is less than itself plus 1. (Contributed by Mario Carneiro,
28May2016.)



Theorem  lep1d 7678 
A number is less than or equal to itself plus 1. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  ltm1d 7679 
A number minus 1 is less than itself. (Contributed by Mario Carneiro,
28May2016.)



Theorem  lem1d 7680 
A number minus 1 is less than or equal to itself. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  recgt0d 7681 
The reciprocal of a positive number is positive. Exercise 4 of
[Apostol] p. 21. (Contributed by
Mario Carneiro, 28May2016.)



Theorem  divgt0d 7682 
The ratio of two positive numbers is positive. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  mulgt1d 7683 
The product of two numbers greater than 1 is greater than 1.
(Contributed by Mario Carneiro, 28May2016.)



Theorem  lemulge11d 7684 
Multiplication by a number greater than or equal to 1. (Contributed
by Mario Carneiro, 28May2016.)



Theorem  lemulge12d 7685 
Multiplication by a number greater than or equal to 1. (Contributed
by Mario Carneiro, 28May2016.)



Theorem  lemul1ad 7686 
Multiplication of both sides of 'less than or equal to' by a
nonnegative number. (Contributed by Mario Carneiro, 28May2016.)



Theorem  lemul2ad 7687 
Multiplication of both sides of 'less than or equal to' by a
nonnegative number. (Contributed by Mario Carneiro, 28May2016.)



Theorem  ltmul12ad 7688 
Comparison of product of two positive numbers. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  lemul12ad 7689 
Comparison of product of two nonnegative numbers. (Contributed by
Mario Carneiro, 28May2016.)



Theorem  lemul12bd 7690 
Comparison of product of two nonnegative numbers. (Contributed by
Mario Carneiro, 28May2016.)



3.3.10 Imaginary and complex number
properties


Theorem  crap0 7691 
The real representation of complex numbers is apart from zero iff one of
its terms is apart from zero. (Contributed by Jim Kingdon,
5Mar2020.)

# # # 

Theorem  creur 7692* 
The real part of a complex number is unique. Proposition 101.3 of
[Gleason] p. 130. (Contributed by NM,
9May1999.) (Proof shortened by
Mario Carneiro, 27May2016.)



Theorem  creui 7693* 
The imaginary part of a complex number is unique. Proposition 101.3 of
[Gleason] p. 130. (Contributed by NM,
9May1999.) (Proof shortened by
Mario Carneiro, 27May2016.)



Theorem  cju 7694* 
The complex conjugate of a complex number is unique. (Contributed by
Mario Carneiro, 6Nov2013.)



3.4 Integer sets


3.4.1 Positive integers (as a subset of complex
numbers)


Syntax  cn 7695 
Extend class notation to include the class of positive integers.



Definition  dfinn 7696* 
Definition of the set of positive integers. For naming consistency with
the Metamath Proof Explorer usages should refer to dfnn2 7697 instead.
(Contributed by Jeff Hankins, 12Sep2013.) (Revised by Mario Carneiro,
3May2014.) (New usage is discouraged.)



Theorem  dfnn2 7697* 
Definition of the set of positive integers. Another name for
dfinn 7696. (Contributed by Jeff Hankins, 12Sep2013.)
(Revised by
Mario Carneiro, 3May2014.)



Theorem  peano5nni 7698* 
Peano's inductive postulate. Theorem I.36 (principle of mathematical
induction) of [Apostol] p. 34.
(Contributed by NM, 10Jan1997.)
(Revised by Mario Carneiro, 17Nov2014.)



Theorem  nnssre 7699 
The positive integers are a subset of the reals. (Contributed by NM,
10Jan1997.) (Revised by Mario Carneiro, 16Jun2013.)



Theorem  nnsscn 7700 
The positive integers are a subset of the complex numbers. (Contributed
by NM, 2Aug2004.)

