Theorem List for Intuitionistic Logic Explorer - 8601-8700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | rpreap0 8601 |
A positive real is a real number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
# |
|
Theorem | rpcnne0 8602 |
A positive real is a nonzero complex number. (Contributed by NM,
11-Nov-2008.)
|
|
|
Theorem | rpcnap0 8603 |
A positive real is a complex number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
# |
|
Theorem | ralrp 8604 |
Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
|
|
|
Theorem | rexrp 8605 |
Quantification over positive reals. (Contributed by Mario Carneiro,
21-May-2014.)
|
|
|
Theorem | rpaddcl 8606 |
Closure law for addition of positive reals. Part of Axiom 7 of [Apostol]
p. 20. (Contributed by NM, 27-Oct-2007.)
|
|
|
Theorem | rpmulcl 8607 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by NM,
27-Oct-2007.)
|
|
|
Theorem | rpdivcl 8608 |
Closure law for division of positive reals. (Contributed by FL,
27-Dec-2007.)
|
|
|
Theorem | rpreccl 8609 |
Closure law for reciprocation of positive reals. (Contributed by Jeff
Hankins, 23-Nov-2008.)
|
|
|
Theorem | rphalfcl 8610 |
Closure law for half of a positive real. (Contributed by Mario Carneiro,
31-Jan-2014.)
|
|
|
Theorem | rpgecl 8611 |
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rphalflt 8612 |
Half of a positive real is less than the original number. (Contributed by
Mario Carneiro, 21-May-2014.)
|
|
|
Theorem | rerpdivcl 8613 |
Closure law for division of a real by a positive real. (Contributed by
NM, 10-Nov-2008.)
|
|
|
Theorem | ge0p1rp 8614 |
A nonnegative number plus one is a positive number. (Contributed by Mario
Carneiro, 5-Oct-2015.)
|
|
|
Theorem | rpnegap 8615 |
Either a real apart from zero or its negation is a positive real, but not
both. (Contributed by Jim Kingdon, 23-Mar-2020.)
|
#
|
|
Theorem | 0nrp 8616 |
Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by
NM, 27-Oct-2007.)
|
|
|
Theorem | ltsubrp 8617 |
Subtracting a positive real from another number decreases it.
(Contributed by FL, 27-Dec-2007.)
|
|
|
Theorem | ltaddrp 8618 |
Adding a positive number to another number increases it. (Contributed by
FL, 27-Dec-2007.)
|
|
|
Theorem | difrp 8619 |
Two ways to say one number is less than another. (Contributed by Mario
Carneiro, 21-May-2014.)
|
|
|
Theorem | elrpd 8620 |
Membership in the set of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | nnrpd 8621 |
A positive integer is a positive real. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpred 8622 |
A positive real is a real. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpxrd 8623 |
A positive real is an extended real. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpcnd 8624 |
A positive real is a complex number. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpgt0d 8625 |
A positive real is greater than zero. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpge0d 8626 |
A positive real is greater than or equal to zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpne0d 8627 |
A positive real is nonzero. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpap0d 8628 |
A positive real is apart from zero. (Contributed by Jim Kingdon,
28-Jul-2021.)
|
# |
|
Theorem | rpregt0d 8629 |
A positive real is real and greater than zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rprege0d 8630 |
A positive real is real and greater or equal to zero. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rprene0d 8631 |
A positive real is a nonzero real number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpcnne0d 8632 |
A positive real is a nonzero complex number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpreccld 8633 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rprecred 8634 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rphalfcld 8635 |
Closure law for half of a positive real. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | reclt1d 8636 |
The reciprocal of a positive number less than 1 is greater than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | recgt1d 8637 |
The reciprocal of a positive number greater than 1 is less than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rpaddcld 8638 |
Closure law for addition of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpmulcld 8639 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpdivcld 8640 |
Closure law for division of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | ltrecd 8641 |
The reciprocal of both sides of 'less than'. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | lerecd 8642 |
The reciprocal of both sides of 'less than or equal to'. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltrec1d 8643 |
Reciprocal swap in a 'less than' relation. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | lerec2d 8644 |
Reciprocal swap in a 'less than or equal to' relation. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lediv2ad 8645 |
Division of both sides of 'less than or equal to' into a nonnegative
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltdiv2d 8646 |
Division of a positive number by both sides of 'less than'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lediv2d 8647 |
Division of a positive number by both sides of 'less than or equal to'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ledivdivd 8648 |
Invert ratios of positive numbers and swap their ordering.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | divge1 8649 |
The ratio of a number over a smaller positive number is larger than 1.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
|
Theorem | divlt1lt 8650 |
A real number divided by a positive real number is less than 1 iff the
real number is less than the positive real number. (Contributed by AV,
25-May-2020.)
|
|
|
Theorem | divle1le 8651 |
A real number divided by a positive real number is less than or equal to 1
iff the real number is less than or equal to the positive real number.
(Contributed by AV, 29-Jun-2021.)
|
|
|
Theorem | ledivge1le 8652 |
If a number is less than or equal to another number, the number divided by
a positive number greater than or equal to one is less than or equal to
the other number. (Contributed by AV, 29-Jun-2021.)
|
|
|
Theorem | ge0p1rpd 8653 |
A nonnegative number plus one is a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rerpdivcld 8654 |
Closure law for division of a real by a positive real. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltsubrpd 8655 |
Subtracting a positive real from another number decreases it.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltaddrpd 8656 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltaddrp2d 8657 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmulgt11d 8658 |
Multiplication by a number greater than 1. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmulgt12d 8659 |
Multiplication by a number greater than 1. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | gt0divd 8660 |
Division of a positive number by a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ge0divd 8661 |
Division of a nonnegative number by a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rpgecld 8662 |
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | divge0d 8663 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmul1d 8664 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmul2d 8665 |
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | lemul1d 8666 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lemul2d 8667 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltdiv1d 8668 |
Division of both sides of 'less than' by a positive number.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lediv1d 8669 |
Division of both sides of a less than or equal to relation by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmuldivd 8670 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmuldiv2d 8671 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lemuldivd 8672 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | lemuldiv2d 8673 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | ltdivmuld 8674 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltdivmul2d 8675 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ledivmuld 8676 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ledivmul2d 8677 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmul1dd 8678 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | ltmul2dd 8679 |
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by Mario Carneiro,
30-May-2016.)
|
|
|
Theorem | ltdiv1dd 8680 |
Division of both sides of 'less than' by a positive number.
(Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | lediv1dd 8681 |
Division of both sides of a less than or equal to relation by a
positive number. (Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | lediv12ad 8682 |
Comparison of ratio of two nonnegative numbers. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | ltdiv23d 8683 |
Swap denominator with other side of 'less than'. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lediv23d 8684 |
Swap denominator with other side of 'less than or equal to'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lt2mul2divd 8685 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
3.5.2 Infinity and the extended real number
system (cont.)
|
|
Syntax | cxne 8686 |
Extend class notation to include the negative of an extended real.
|
|
|
Syntax | cxad 8687 |
Extend class notation to include addition of extended reals.
|
|
|
Syntax | cxmu 8688 |
Extend class notation to include multiplication of extended reals.
|
|
|
Definition | df-xneg 8689 |
Define the negative of an extended real number. (Contributed by FL,
26-Dec-2011.)
|
|
|
Definition | df-xadd 8690* |
Define addition over extended real numbers. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Definition | df-xmul 8691* |
Define multiplication over extended real numbers. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | pnfxr 8692 |
Plus infinity belongs to the set of extended reals. (Contributed by NM,
13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)
|
|
|
Theorem | pnfex 8693 |
Plus infinity exists (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
|
|
Theorem | mnfxr 8694 |
Minus infinity belongs to the set of extended reals. (Contributed by NM,
13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof
shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | ltxr 8695 |
The 'less than' binary relation on the set of extended reals.
Definition 12-3.1 of [Gleason] p. 173.
(Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | elxr 8696 |
Membership in the set of extended reals. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | pnfnemnf 8697 |
Plus and minus infinity are different elements of . (Contributed
by NM, 14-Oct-2005.)
|
|
|
Theorem | mnfnepnf 8698 |
Minus and plus infinity are different (common case). (Contributed by
David A. Wheeler, 8-Dec-2018.)
|
|
|
Theorem | xrnemnf 8699 |
An extended real other than minus infinity is real or positive infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xrnepnf 8700 |
An extended real other than plus infinity is real or negative infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|