Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  lt2msq1 7926 
Lemma for lt2msq 7927. (Contributed by Mario Carneiro,
27May2016.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  ltmul1ii 7969 
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 7970 
Division of both sides of 'less than' by a positive number.
(Contributed by NM, 16May1999.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  mulle0r 7985 
Multiplying a nonnegative number by a nonpositive number yields a
nonpositive number. (Contributed by Jim Kingdon, 28Oct2021.)



3.3.10 Imaginary and complex number
properties


Theorem  crap0 7986 
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 7987* 
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 7988* 
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 7989* 
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 7990 
Extend class notation to include the class of positive integers.



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



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



Theorem  peano5nni 7993* 
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 7994 
The positive integers are a subset of the reals. (Contributed by NM,
10Jan1997.) (Revised by Mario Carneiro, 16Jun2013.)



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



Theorem  nnex 7996 
The set of positive integers exists. (Contributed by NM, 3Oct1999.)
(Revised by Mario Carneiro, 17Nov2014.)



Theorem  nnre 7997 
A positive integer is a real number. (Contributed by NM, 18Aug1999.)



Theorem  nncn 7998 
A positive integer is a complex number. (Contributed by NM,
18Aug1999.)



Theorem  nnrei 7999 
A positive integer is a real number. (Contributed by NM,
18Aug1999.)



Theorem  nncni 8000 
A positive integer is a complex number. (Contributed by NM,
18Aug1999.)

