Home | Intuitionistic Logic Explorer Theorem List (p. 77 of 108) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lenegcon1i 7601 | Contraposition of negative in 'less than or equal to'. (Contributed by NM, 6-Apr-2005.) |
Theorem | subge0i 7602 | Nonnegative subtraction. (Contributed by NM, 13-Aug-2000.) |
Theorem | ltadd1i 7603 | Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20. (Contributed by NM, 21-Jan-1997.) |
Theorem | leadd1i 7604 | Addition to both sides of 'less than or equal to'. (Contributed by NM, 11-Aug-1999.) |
Theorem | leadd2i 7605 | Addition to both sides of 'less than or equal to'. (Contributed by NM, 11-Aug-1999.) |
Theorem | ltsubaddi 7606 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | lesubaddi 7607 | 'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 30-Sep-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | ltsubadd2i 7608 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) |
Theorem | lesubadd2i 7609 | 'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 3-Aug-1999.) |
Theorem | ltaddsubi 7610 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 14-May-1999.) |
Theorem | lt2addi 7611 | Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.) |
Theorem | le2addi 7612 | Adding both side of two inequalities. (Contributed by NM, 16-Sep-1999.) |
Theorem | gt0ne0d 7613 | Positive implies nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lt0ne0d 7614 | Something less than zero is not zero. Deduction form. (Contributed by David Moews, 28-Feb-2017.) |
Theorem | leidd 7615 | 'Less than or equal to' is reflexive. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lt0neg1d 7616 | Comparison of a number and its negative to zero. Theorem I.23 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lt0neg2d 7617 | Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | le0neg1d 7618 | Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | le0neg2d 7619 | Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addgegt0d 7620 | Addition of nonnegative and positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addgt0d 7621 | Addition of 2 positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addge0d 7622 | Addition of 2 nonnegative numbers is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltnegd 7623 | Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lenegd 7624 | Negative of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltnegcon1d 7625 | Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltnegcon2d 7626 | Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lenegcon1d 7627 | Contraposition of negative in 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lenegcon2d 7628 | Contraposition of negative in 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltaddposd 7629 | Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltaddpos2d 7630 | Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltsubposd 7631 | Subtracting a positive number from another number decreases it. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | posdifd 7632 | Comparison of two numbers whose difference is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addge01d 7633 | A number is less than or equal to itself plus a nonnegative number. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addge02d 7634 | A number is less than or equal to itself plus a nonnegative number. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | subge0d 7635 | Nonnegative subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | suble0d 7636 | Nonpositive subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | subge02d 7637 | Nonnegative subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltadd1d 7638 | Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | leadd1d 7639 | Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | leadd2d 7640 | Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltsubaddd 7641 | 'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lesubaddd 7642 | 'Less than or equal to' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltsubadd2d 7643 | 'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lesubadd2d 7644 | 'Less than or equal to' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltaddsubd 7645 | 'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltaddsub2d 7646 | 'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 29-Dec-2016.) |
Theorem | leaddsub2d 7647 | 'Less than or equal to' relationship between and addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | subled 7648 | Swap subtrahends in an inequality. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lesubd 7649 | Swap subtrahends in an inequality. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltsub23d 7650 | 'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltsub13d 7651 | 'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lesub1d 7652 | Subtraction from both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lesub2d 7653 | Subtraction of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltsub1d 7654 | Subtraction from both sides of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltsub2d 7655 | Subtraction of both sides of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltadd1dd 7656 | Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20. (Contributed by Mario Carneiro, 30-May-2016.) |
Theorem | ltsub1dd 7657 | Subtraction from both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016.) |
Theorem | ltsub2dd 7658 | Subtraction of both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016.) |
Theorem | leadd1dd 7659 | Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 30-May-2016.) |
Theorem | leadd2dd 7660 | Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 30-May-2016.) |
Theorem | lesub1dd 7661 | Subtraction from both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 30-May-2016.) |
Theorem | lesub2dd 7662 | Subtraction of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 30-May-2016.) |
Theorem | le2addd 7663 | Adding both side of two inequalities. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | le2subd 7664 | Subtracting both sides of two 'less than or equal to' relations. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltleaddd 7665 | Adding both sides of two orderings. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | leltaddd 7666 | Adding both sides of two orderings. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lt2addd 7667 | Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lt2subd 7668 | Subtracting both sides of two 'less than' relations. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | possumd 7669 | Condition for a positive sum. (Contributed by Scott Fenton, 16-Dec-2017.) |
Theorem | sublt0d 7670 | When a subtraction gives a negative result. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | ltaddsublt 7671 | Addition and subtraction on one side of 'less than'. (Contributed by AV, 24-Nov-2018.) |
Theorem | 1le1 7672 | . Common special case. (Contributed by David A. Wheeler, 16-Jul-2016.) |
Theorem | gt0add 7673 | A positive sum must have a positive addend. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by Jim Kingdon, 26-Jan-2020.) |
Syntax | creap 7674 | Class of real apartness relation. |
#ℝ | ||
Definition | df-reap 7675* | Define real apartness. Definition in Section 11.2.1 of [HoTT], p. (varies). Although #ℝ is an apartness relation on the reals (see df-ap 7682 for more discussion of apartness relations), for our purposes it is just a stepping stone to defining # which is an apartness relation on complex numbers. On the reals, #ℝ and # agree (apreap 7687). (Contributed by Jim Kingdon, 26-Jan-2020.) |
#ℝ | ||
Theorem | reapval 7676 | Real apartness in terms of classes. Beyond the development of # itself, proofs should use reaplt 7688 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 29-Jan-2020.) |
#ℝ | ||
Theorem | reapirr 7677 | Real apartness is irreflexive. Part of Definition 11.2.7(v) of [HoTT], p. (varies). Beyond the development of # itself, proofs should use apirr 7705 instead. (Contributed by Jim Kingdon, 26-Jan-2020.) |
#ℝ | ||
Theorem | recexre 7678* | Existence of reciprocal of real number. (Contributed by Jim Kingdon, 29-Jan-2020.) |
#ℝ | ||
Theorem | reapti 7679 | Real apartness is tight. Beyond the development of apartness itself, proofs should use apti 7722. (Contributed by Jim Kingdon, 30-Jan-2020.) (New usage is discouraged.) |
#ℝ | ||
Theorem | recexgt0 7680* | Existence of reciprocal of positive real number. (Contributed by Jim Kingdon, 6-Feb-2020.) |
Syntax | cap 7681 | Class of complex apartness relation. |
# | ||
Definition | df-ap 7682* |
Define complex apartness. Definition 6.1 of [Geuvers], p. 17.
Two numbers are considered apart if it is possible to separate them. One common usage is that we can divide by a number if it is apart from zero (see for example recclap 7767 which says that a number apart from zero has a reciprocal). The defining characteristics of an apartness are irreflexivity (apirr 7705), symmetry (apsym 7706), and cotransitivity (apcotr 7707). Apartness implies negated equality, as seen at apne 7723, and the converse would also follow if we assumed excluded middle. In addition, apartness of complex numbers is tight, which means that two numbers which are not apart are equal (apti 7722). (Contributed by Jim Kingdon, 26-Jan-2020.) |
# #ℝ #ℝ | ||
Theorem | ixi 7683 | times itself is minus 1. (Contributed by NM, 6-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | inelr 7684 | The imaginary unit is not a real number. (Contributed by NM, 6-May-1999.) |
Theorem | rimul 7685 | A real number times the imaginary unit is real only if the number is 0. (Contributed by NM, 28-May-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
Theorem | rereim 7686 | Decomposition of a real number into real part (itself) and imaginary part (zero). (Contributed by Jim Kingdon, 30-Jan-2020.) |
Theorem | apreap 7687 | Complex apartness and real apartness agree on the real numbers. (Contributed by Jim Kingdon, 31-Jan-2020.) |
# #ℝ | ||
Theorem | reaplt 7688 | Real apartness in terms of less than. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by Jim Kingdon, 1-Feb-2020.) |
# | ||
Theorem | reapltxor 7689 | Real apartness in terms of less than (exclusive-or version). (Contributed by Jim Kingdon, 23-Mar-2020.) |
# | ||
Theorem | 1ap0 7690 | One is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.) |
# | ||
Theorem | ltmul1a 7691 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 15-May-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
Theorem | ltmul1 7692 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 13-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
Theorem | lemul1 7693 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 21-Feb-2005.) |
Theorem | reapmul1lem 7694 | Lemma for reapmul1 7695. (Contributed by Jim Kingdon, 8-Feb-2020.) |
# # | ||
Theorem | reapmul1 7695 | Multiplication of both sides of real apartness by a real number apart from zero. Special case of apmul1 7876. (Contributed by Jim Kingdon, 8-Feb-2020.) |
# # # | ||
Theorem | reapadd1 7696 | Real addition respects apartness. (Contributed by Jim Kingdon, 13-Feb-2020.) |
# # | ||
Theorem | reapneg 7697 | Real negation respects apartness. (Contributed by Jim Kingdon, 13-Feb-2020.) |
# # | ||
Theorem | reapcotr 7698 | Real apartness is cotransitive. Part of Definition 11.2.7(v) of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Feb-2020.) |
# # # | ||
Theorem | remulext1 7699 | Left extensionality for multiplication. (Contributed by Jim Kingdon, 19-Feb-2020.) |
# # | ||
Theorem | remulext2 7700 | Right extensionality for real multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.) |
# # |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |