Home | Intuitionistic Logic Explorer Theorem List (p. 92 of 94) | < 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 | cjcli 9101 | Closure law for complex conjugate. (Contributed by NM, 11-May-1999.) | ||||||||||||
Theorem | replimi 9102 | Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.) | ||||||||||||
Theorem | cjcji 9103 | The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by NM, 11-May-1999.) | ||||||||||||
Theorem | reim0bi 9104 | A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.) | ||||||||||||
Theorem | rerebi 9105 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.) | ||||||||||||
Theorem | cjrebi 9106 | A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 11-Oct-1999.) | ||||||||||||
Theorem | recji 9107 | Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) | ||||||||||||
Theorem | imcji 9108 | Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) | ||||||||||||
Theorem | cjmulrcli 9109 | A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.) | ||||||||||||
Theorem | cjmulvali 9110 | A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.) | ||||||||||||
Theorem | cjmulge0i 9111 | A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.) | ||||||||||||
Theorem | renegi 9112 | Real part of negative. (Contributed by NM, 2-Aug-1999.) | ||||||||||||
Theorem | imnegi 9113 | Imaginary part of negative. (Contributed by NM, 2-Aug-1999.) | ||||||||||||
Theorem | cjnegi 9114 | Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.) | ||||||||||||
Theorem | addcji 9115 | A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.) | ||||||||||||
Theorem | readdi 9116 | Real part distributes over addition. (Contributed by NM, 28-Jul-1999.) | ||||||||||||
Theorem | imaddi 9117 | Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.) | ||||||||||||
Theorem | remuli 9118 | Real part of a product. (Contributed by NM, 28-Jul-1999.) | ||||||||||||
Theorem | immuli 9119 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) | ||||||||||||
Theorem | cjaddi 9120 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) | ||||||||||||
Theorem | cjmuli 9121 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) | ||||||||||||
Theorem | ipcni 9122 | Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.) | ||||||||||||
Theorem | cjdivapi 9123 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) | ||||||||||||
# | ||||||||||||||
Theorem | crrei 9124 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) | ||||||||||||
Theorem | crimi 9125 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) | ||||||||||||
Theorem | recld 9126 | The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | imcld 9127 | The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | cjcld 9128 | Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | replimd 9129 | Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | remimd 9130 | Value of the conjugate of a complex number. The value is the real part minus times the imaginary part. Definition 10-3.2 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | cjcjd 9131 | The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | reim0bd 9132 | A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | rerebd 9133 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | cjrebd 9134 | A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | cjne0d 9135 | A number is nonzero iff its complex conjugate is nonzero. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | recjd 9136 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | imcjd 9137 | Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | cjmulrcld 9138 | A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | cjmulvald 9139 | A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | cjmulge0d 9140 | A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | renegd 9141 | Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | imnegd 9142 | Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | cjnegd 9143 | Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | addcjd 9144 | A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | cjexpd 9145 | Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | readdd 9146 | Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | imaddd 9147 | Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | resubd 9148 | Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | imsubd 9149 | Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | remuld 9150 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | immuld 9151 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | cjaddd 9152 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | cjmuld 9153 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | ipcnd 9154 | Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | cjdivapd 9155 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.) | ||||||||||||
# | ||||||||||||||
Theorem | rered 9156 | A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | reim0d 9157 | The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | cjred 9158 | A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | remul2d 9159 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | immul2d 9160 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | redivapd 9161 | Real part of a division. Related to remul2 9061. (Contributed by Jim Kingdon, 15-Jun-2020.) | ||||||||||||
# | ||||||||||||||
Theorem | imdivapd 9162 | Imaginary part of a division. Related to remul2 9061. (Contributed by Jim Kingdon, 15-Jun-2020.) | ||||||||||||
# | ||||||||||||||
Theorem | crred 9163 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
Theorem | crimd 9164 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) | ||||||||||||
This section describes the conventions we use. However, these conventions often refer to existing mathematical practices, which are discussed in more detail in other references. The following sources lay out how mathematics is developed without the law of the excluded middle. Of course, there are a greater number of sources which assume excluded middle and most of what is in them applies here too (especially in a treatment such as ours which is built on first order logic and set theory, rather than, say, type theory). Studying how a topic is treated in the Metamath Proof Explorer and the references therein is often a good place to start (and is easy to compare with the Intuitionistic Logic Explorer). The textbooks provide a motivation for what we are doing, whereas Metamath lets you see in detail all hidden and implicit steps. Most standard theorems are accompanied by citations. Some closely followed texts include the following:
| ||||||||||||||
Theorem | conventions 9165 |
Unless there is a reason to diverge, we follow the conventions of
the Metamath Proof Explorer (aka "set.mm"). This list of
conventions is intended to be read in conjunction with the
corresponding conventions in the Metamath Proof Explorer, and
only the differences are described below.
Label naming conventions Here are a few of the label naming conventions:
The following table shows some commonly-used abbreviations in labels which are not found in the Metamath Proof Explorer, in alphabetical order. For each abbreviation we provide a mnenomic to help you remember it, the source theorem/assumption defining it, an expression showing what it looks like, whether or not it is a "syntax fragment" (an abbreviation that indicates a particular kind of syntax), and hyperlinks to label examples that use the abbreviation. The abbreviation is bolded if there is a df-NAME definition but the label fragment is not NAME.
(Contributed by Jim Kingdon, 24-Feb-2020.) | ||||||||||||
Theorem | mathbox 9166 |
(This theorem is a dummy placeholder for these guidelines. The name of
this theorem, "mathbox", is hard-coded into the Metamath program
to
identify the start of the mathbox section for web page generation.)
A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of set.mm. For contributors: By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of set.mm. Mathboxes are provided to help keep your work synchronized with changes in set.mm, but they shouldn't be depended on as a permanent archive. If you want to preserve your original contribution, it is your responsibility to keep your own copy of it along with the version of set.mm that works with it. Guidelines: 1. If at all possible, please use only 0-ary class constants for new definitions. 2. Try to follow the style of the rest of set.mm. Each $p and $a statement must be immediately preceded with the comment that will be shown on its web page description. The metamath program command "write source set.mm /rewrap" will take care of wrapping comment lines and indentation conventions. All mathbox content will be on public display and should hopefully reflect the overall quality of the website. 3. Before submitting a revised mathbox, please make sure it verifies against the current set.mm. 4. Mathboxes should be independent i.e. the proofs should verify with all other mathboxes removed. If you need a theorem from another mathbox, that is fine (and encouraged), but let me know, so I can move the theorem to the main section. One way avoid undesired accidental use of other mathbox theorems is to develop your mathbox using a modified set.mm that has mathboxes removed. Notes: 1. We may decide to move some theorems to the main part of set.mm for general use. 2. We may make changes to mathboxes to maintain the overall quality of set.mm. Normally we will let you know if a change might impact what you are working on. 3. If you use theorems from another user's mathbox, we don't provide assurance that they are based on correct or consistent $a statements. (If you find such a problem, please let us know so it can be corrected.) (Contributed by NM, 20-Feb-2007.) (New usage is discouraged.) | ||||||||||||
Theorem | ax1hfs 9167 | Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11-Aug-2018.) | ||||||||||||
Theorem | nnexmid 9168 | Double negation of excluded middle. Intuitionistic logic refutes the negation of excluded middle (but, of course, does not prove excluded middle) for any formula. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||
Theorem | nndc 9169 | Double negation of decidability of a formula. Intuitionistic logic refutes undecidability (but, of course, does not prove decidability) of any formula. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||
DECID | ||||||||||||||
Theorem | dcdc 9170 | Decidability of a proposition is decidable if and only if that proposition is decidable. DECID is idempotent. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||
DECID DECID DECID | ||||||||||||||
Theorem | bj-ex 9171* | Existential generalization. (Contributed by BJ, 8-Dec-2019.) Proof modification is discouraged because there are shorter proofs, but using less basic results (like exlimiv 1486 and 19.9ht 1529 or 19.23ht 1383). (Proof modification is discouraged.) | ||||||||||||
Theorem | bj-hbalt 9172 | Closed form of hbal 1363 (copied from set.mm). (Contributed by BJ, 2-May-2019.) | ||||||||||||
Theorem | bj-nfalt 9173 | Closed form of nfal 1465 (copied from set.mm). (Contributed by BJ, 2-May-2019.) | ||||||||||||
Theorem | spimd 9174 | Deduction form of spim 1623. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||
Theorem | 2spim 9175* | Double substitution, as in spim 1623. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||
Theorem | ch2var 9176* | Implicit substitution of for and for into a theorem. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||
Theorem | ch2varv 9177* | Version of ch2var 9176 with non-freeness hypotheses replaced by DV conditions. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||
Theorem | bj-exlimmp 9178 | Lemma for bj-vtoclgf 9184. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
Theorem | bj-exlimmpi 9179 | Lemma for bj-vtoclgf 9184. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
Theorem | bj-sbimedh 9180 | A strengthening of sbiedh 1667 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||
Theorem | bj-sbimeh 9181 | A strengthening of sbieh 1670 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||
Theorem | bj-sbime 9182 | A strengthening of sbie 1671 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||
Various utility theorems using FOL and extensionality. | ||||||||||||||
Theorem | bj-vtoclgft 9183 | Weakening two hypotheses of vtoclgf 2606. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||
Theorem | bj-vtoclgf 9184 | Weakening two hypotheses of vtoclgf 2606. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||
Theorem | elabgf0 9185 | Lemma for elabgf 2679. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||
Theorem | elabgft1 9186 | One implication of elabgf 2679, in closed form. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||
Theorem | elabgf1 9187 | One implication of elabgf 2679. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||
Theorem | elabgf2 9188 | One implication of elabgf 2679. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||
Theorem | elabf1 9189* | One implication of elabf 2680. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||
Theorem | elabf2 9190* | One implication of elabf 2680. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||
Theorem | elab1 9191* | One implication of elab 2681. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||
Theorem | elab2a 9192* | One implication of elab 2681. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||
Theorem | elabg2 9193* | One implication of elabg 2682. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||
Theorem | bj-rspgt 9194 | Restricted specialization, generalized. Weakens a hypothesis of rspccv 2647 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||
Theorem | bj-rspg 9195 | Restricted specialization, generalized. Weakens a hypothesis of rspccv 2647 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||
Theorem | cbvrald 9196* | Rule used to change bound variables, using implicit substitution. (Contributed by BJ, 22-Nov-2019.) | ||||||||||||
Theorem | bj-intabssel 9197 | Version of intss1 3621 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.) | ||||||||||||
Theorem | bj-intabssel1 9198 | Version of intss1 3621 using a class abstraction and implicit substitution. Closed form of intmin3 3633. (Contributed by BJ, 29-Nov-2019.) | ||||||||||||
Theorem | bj-elssuniab 9199 | Version of elssuni 3599 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.) | ||||||||||||
Theorem | bj-sseq 9200 | If two converse inclusions are characterized each by a formula, then equality is characterized by the conjunction of these formulas. (Contributed by BJ, 30-Nov-2019.) | ||||||||||||
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |