![]() |
Metamath
Proof Explorer Theorem List (p. 151 of 484) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dfid5 15001 | Identity relation is equal to relational exponentiation to the first power. (Contributed by RP, 9-Jun-2020.) |
β’ I = (π₯ β V β¦ (π₯βπ1)) | ||
Theorem | dfid6 15002* | Identity relation expressed as indexed union of relational powers. (Contributed by RP, 9-Jun-2020.) |
β’ I = (π₯ β V β¦ βͺ π β {1} (π₯βππ)) | ||
Theorem | relexp1d 15003 | A relation composed once is itself. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β π β π) β β’ (π β (π βπ1) = π ) | ||
Theorem | relexpsucnnl 15004 | A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.) |
β’ ((π β π β§ π β β) β (π βπ(π + 1)) = (π β (π βππ))) | ||
Theorem | relexpsucl 15005 | A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.) |
β’ ((π β π β§ Rel π β§ π β β0) β (π βπ(π + 1)) = (π β (π βππ))) | ||
Theorem | relexpsucr 15006 | A reduction for relation exponentiation to the right. (Contributed by RP, 23-May-2020.) |
β’ ((π β π β§ Rel π β§ π β β0) β (π βπ(π + 1)) = ((π βππ) β π )) | ||
Theorem | relexpsucrd 15007 | A reduction for relation exponentiation to the right. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β Rel π ) & β’ (π β π β β0) β β’ (π β (π βπ(π + 1)) = ((π βππ) β π )) | ||
Theorem | relexpsucld 15008 | A reduction for relation exponentiation to the left. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β Rel π ) & β’ (π β π β β0) β β’ (π β (π βπ(π + 1)) = (π β (π βππ))) | ||
Theorem | relexpcnv 15009 | Commutation of converse and relation exponentiation. (Contributed by RP, 23-May-2020.) |
β’ ((π β β0 β§ π β π) β β‘(π βππ) = (β‘π βππ)) | ||
Theorem | relexpcnvd 15010 | Commutation of converse and relation exponentiation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β π β π) & β’ (π β π β β0) β β’ (π β β‘(π βππ) = (β‘π βππ)) | ||
Theorem | relexp0rel 15011 | The exponentiation of a class to zero is a relation. (Contributed by RP, 23-May-2020.) |
β’ (π β π β Rel (π βπ0)) | ||
Theorem | relexprelg 15012 | The exponentiation of a class is a relation except when the exponent is one and the class is not a relation. (Contributed by RP, 23-May-2020.) |
β’ ((π β β0 β§ π β π β§ (π = 1 β Rel π )) β Rel (π βππ)) | ||
Theorem | relexprel 15013 | The exponentiation of a relation is a relation. (Contributed by RP, 23-May-2020.) |
β’ ((π β β0 β§ π β π β§ Rel π ) β Rel (π βππ)) | ||
Theorem | relexpreld 15014 | The exponentiation of a relation is a relation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β Rel π ) & β’ (π β π β β0) β β’ (π β Rel (π βππ)) | ||
Theorem | relexpnndm 15015 | The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.) |
β’ ((π β β β§ π β π) β dom (π βππ) β dom π ) | ||
Theorem | relexpdmg 15016 | The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.) |
β’ ((π β β0 β§ π β π) β dom (π βππ) β (dom π βͺ ran π )) | ||
Theorem | relexpdm 15017 | The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.) |
β’ ((π β β0 β§ π β π) β dom (π βππ) β βͺ βͺ π ) | ||
Theorem | relexpdmd 15018 | The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β π β β0) β β’ (π β dom (π βππ) β βͺ βͺ π ) | ||
Theorem | relexpnnrn 15019 | The range of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.) |
β’ ((π β β β§ π β π) β ran (π βππ) β ran π ) | ||
Theorem | relexprng 15020 | The range of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.) |
β’ ((π β β0 β§ π β π) β ran (π βππ) β (dom π βͺ ran π )) | ||
Theorem | relexprn 15021 | The range of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.) |
β’ ((π β β0 β§ π β π) β ran (π βππ) β βͺ βͺ π ) | ||
Theorem | relexprnd 15022 | The range of an exponentiation of a relation a subset of the relation's field. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β π β β0) β β’ (π β ran (π βππ) β βͺ βͺ π ) | ||
Theorem | relexpfld 15023 | The field of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.) |
β’ ((π β β0 β§ π β π) β βͺ βͺ (π βππ) β βͺ βͺ π ) | ||
Theorem | relexpfldd 15024 | The field of an exponentiation of a relation a subset of the relation's field. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β π β β0) β β’ (π β βͺ βͺ (π βππ) β βͺ βͺ π ) | ||
Theorem | relexpaddnn 15025 | Relation composition becomes addition under exponentiation. (Contributed by RP, 23-May-2020.) |
β’ ((π β β β§ π β β β§ π β π) β ((π βππ) β (π βππ)) = (π βπ(π + π))) | ||
Theorem | relexpuzrel 15026 | The exponentiation of a class to an integer not smaller than 2 is a relation. (Contributed by RP, 23-May-2020.) |
β’ ((π β (β€β₯β2) β§ π β π) β Rel (π βππ)) | ||
Theorem | relexpaddg 15027 | Relation composition becomes addition under exponentiation except when the exponents total to one and the class isn't a relation. (Contributed by RP, 30-May-2020.) |
β’ ((π β β0 β§ (π β β0 β§ π β π β§ ((π + π) = 1 β Rel π ))) β ((π βππ) β (π βππ)) = (π βπ(π + π))) | ||
Theorem | relexpaddd 15028 | Relation composition becomes addition under exponentiation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β Rel π ) & β’ (π β π β β0) & β’ (π β π β β0) β β’ (π β ((π βππ) β (π βππ)) = (π βπ(π + π))) | ||
Syntax | crtrcl 15029 | Extend class notation with recursively defined reflexive, transitive closure. |
class t*rec | ||
Definition | df-rtrclrec 15030* | The reflexive, transitive closure of a relation constructed as the union of all finite exponentiations. (Contributed by Drahflow, 12-Nov-2015.) |
β’ t*rec = (π β V β¦ βͺ π β β0 (πβππ)) | ||
Theorem | rtrclreclem1 15031 | The reflexive, transitive closure is indeed a closure. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.) |
β’ (π β π β π) β β’ (π β π β (t*recβπ )) | ||
Theorem | dfrtrclrec2 15032* | If two elements are connected by a reflexive, transitive closure, then they are connected via π instances the relation, for some π. (Contributed by Drahflow, 12-Nov-2015.) (Revised by AV, 13-Jul-2024.) |
β’ (π β Rel π ) β β’ (π β (π΄(t*recβπ )π΅ β βπ β β0 π΄(π βππ)π΅)) | ||
Theorem | rtrclreclem2 15033 | The reflexive, transitive closure is indeed reflexive. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 13-Jul-2024.) |
β’ (π β Rel π ) & β’ (π β π β π) β β’ (π β ( I βΎ βͺ βͺ π ) β (t*recβπ )) | ||
Theorem | rtrclreclem3 15034 | The reflexive, transitive closure is indeed transitive. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 13-Jul-2024.) |
β’ (π β Rel π ) β β’ (π β ((t*recβπ ) β (t*recβπ )) β (t*recβπ )) | ||
Theorem | rtrclreclem4 15035* | The reflexive, transitive closure of π is the smallest reflexive, transitive relation which contains π and the identity. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 13-Jul-2024.) |
β’ (π β Rel π ) β β’ (π β βπ ((( I βΎ (dom π βͺ ran π )) β π β§ π β π β§ (π β π ) β π ) β (t*recβπ ) β π )) | ||
Theorem | dfrtrcl2 15036 | The two definitions t* and t*rec of the reflexive, transitive closure coincide if π is indeed a relation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 13-Jul-2024.) |
β’ (π β Rel π ) β β’ (π β (t*βπ ) = (t*recβπ )) | ||
If we have a statement that holds for some element, and a relation between elements that implies if it holds for the first element then it must hold for the second element, the principle of transitive induction shows the statement holds for any element related to the first by the (reflexive-)transitive closure of the relation. | ||
Theorem | relexpindlem 15037* | Principle of transitive induction, finite and non-class version. The first three hypotheses give various existences, the next three give necessary substitutions and the last two are the basis and the induction hypothesis. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) (Revised by AV, 13-Jul-2024.) |
β’ (π β Rel π ) & β’ (π β π β π) & β’ (π = π β (π β π)) & β’ (π = π₯ β (π β π)) & β’ (π = π β (π β π)) & β’ (π β π) & β’ (π β (ππ π₯ β (π β π))) β β’ (π β (π β β0 β (π(π βππ)π₯ β π))) | ||
Theorem | relexpind 15038* | Principle of transitive induction, finite version. The first three hypotheses give various existences, the next four give necessary substitutions and the last two are the basis and the induction hypothesis. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 13-Jul-2024.) |
β’ (π β Rel π ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π = π β (π β π)) & β’ (π = π₯ β (π β π)) & β’ (π = π β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π β π) & β’ (π β (ππ π₯ β (π β π))) β β’ (π β (π β β0 β (π(π βππ)π β π))) | ||
Theorem | rtrclind 15039* | Principle of transitive induction. The first three hypotheses give various existences, the next four give necessary substitutions and the last two are the basis and the induction step. (Contributed by Drahflow, 12-Nov-2015.) (Revised by AV, 13-Jul-2024.) |
β’ (π β Rel π ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π = π β (π β π)) & β’ (π = π₯ β (π β π)) & β’ (π = π β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π β π) & β’ (π β (ππ π₯ β (π β π))) β β’ (π β (π(t*βπ )π β π)) | ||
Syntax | cshi 15040 | Extend class notation with function shifter. |
class shift | ||
Definition | df-shft 15041* | Define a function shifter. This operation offsets the value argument of a function (ordinarily on a subset of β) and produces a new function on β. See shftval 15048 for its value. (Contributed by NM, 20-Jul-2005.) |
β’ shift = (π β V, π₯ β β β¦ {β¨π¦, π§β© β£ (π¦ β β β§ (π¦ β π₯)ππ§)}) | ||
Theorem | shftlem 15042* | Two ways to write a shifted set (π΅ + π΄). (Contributed by Mario Carneiro, 3-Nov-2013.) |
β’ ((π΄ β β β§ π΅ β β) β {π₯ β β β£ (π₯ β π΄) β π΅} = {π₯ β£ βπ¦ β π΅ π₯ = (π¦ + π΄)}) | ||
Theorem | shftuz 15043* | A shift of the upper integers. (Contributed by Mario Carneiro, 5-Nov-2013.) |
β’ ((π΄ β β€ β§ π΅ β β€) β {π₯ β β β£ (π₯ β π΄) β (β€β₯βπ΅)} = (β€β₯β(π΅ + π΄))) | ||
Theorem | shftfval 15044* | The value of the sequence shifter operation is a function on β. π΄ is ordinarily an integer. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ πΉ β V β β’ (π΄ β β β (πΉ shift π΄) = {β¨π₯, π¦β© β£ (π₯ β β β§ (π₯ β π΄)πΉπ¦)}) | ||
Theorem | shftdm 15045* | Domain of a relation shifted by π΄. The set on the right is more commonly notated as (dom πΉ + π΄) (meaning add π΄ to every element of dom πΉ). (Contributed by Mario Carneiro, 3-Nov-2013.) |
β’ πΉ β V β β’ (π΄ β β β dom (πΉ shift π΄) = {π₯ β β β£ (π₯ β π΄) β dom πΉ}) | ||
Theorem | shftfib 15046 | Value of a fiber of the relation πΉ. (Contributed by Mario Carneiro, 4-Nov-2013.) |
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β ((πΉ shift π΄) β {π΅}) = (πΉ β {(π΅ β π΄)})) | ||
Theorem | shftfn 15047* | Functionality and domain of a sequence shifted by π΄. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ πΉ β V β β’ ((πΉ Fn π΅ β§ π΄ β β) β (πΉ shift π΄) Fn {π₯ β β β£ (π₯ β π΄) β π΅}) | ||
Theorem | shftval 15048 | Value of a sequence shifted by π΄. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.) |
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β ((πΉ shift π΄)βπ΅) = (πΉβ(π΅ β π΄))) | ||
Theorem | shftval2 15049 | Value of a sequence shifted by π΄ β π΅. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((πΉ shift (π΄ β π΅))β(π΄ + πΆ)) = (πΉβ(π΅ + πΆ))) | ||
Theorem | shftval3 15050 | Value of a sequence shifted by π΄ β π΅. (Contributed by NM, 20-Jul-2005.) |
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β ((πΉ shift (π΄ β π΅))βπ΄) = (πΉβπ΅)) | ||
Theorem | shftval4 15051 | Value of a sequence shifted by -π΄. (Contributed by NM, 18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β ((πΉ shift -π΄)βπ΅) = (πΉβ(π΄ + π΅))) | ||
Theorem | shftval5 15052 | Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β ((πΉ shift π΄)β(π΅ + π΄)) = (πΉβπ΅)) | ||
Theorem | shftf 15053* | Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ ((πΉ:π΅βΆπΆ β§ π΄ β β) β (πΉ shift π΄):{π₯ β β β£ (π₯ β π΄) β π΅}βΆπΆ) | ||
Theorem | 2shfti 15054 | Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β ((πΉ shift π΄) shift π΅) = (πΉ shift (π΄ + π΅))) | ||
Theorem | shftidt2 15055 | Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ (πΉ shift 0) = (πΉ βΎ β) | ||
Theorem | shftidt 15056 | Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ (π΄ β β β ((πΉ shift 0)βπ΄) = (πΉβπ΄)) | ||
Theorem | shftcan1 15057 | Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β (((πΉ shift π΄) shift -π΄)βπ΅) = (πΉβπ΅)) | ||
Theorem | shftcan2 15058 | Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β (((πΉ shift -π΄) shift π΄)βπ΅) = (πΉβπ΅)) | ||
Theorem | seqshft 15059 | Shifting the index set of a sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-Feb-2014.) |
β’ πΉ β V β β’ ((π β β€ β§ π β β€) β seqπ( + , (πΉ shift π)) = (seq(π β π)( + , πΉ) shift π)) | ||
Syntax | csgn 15060 | Extend class notation to include the Signum function. |
class sgn | ||
Definition | df-sgn 15061 | Signum function. We do not call it "sign", which is homophonic with "sine" (df-sin 16040). Defined as "sgn" in ISO 80000-2:2009(E) operation 2-9.13. It is named "sign" (with the same definition) in the "NIST Digital Library of Mathematical Functions" , front introduction, "Common Notations and Definitions" section at http://dlmf.nist.gov/front/introduction#Sx4 16040. We define this over β* (df-xr 11277) instead of β so that it can accept +β and -β. Note that df-psgn 19445 defines the sign of a permutation, which is different. Value shown in sgnval 15062. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ sgn = (π₯ β β* β¦ if(π₯ = 0, 0, if(π₯ < 0, -1, 1))) | ||
Theorem | sgnval 15062 | Value of the signum function. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ (π΄ β β* β (sgnβπ΄) = if(π΄ = 0, 0, if(π΄ < 0, -1, 1))) | ||
Theorem | sgn0 15063 | The signum of 0 is 0. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ (sgnβ0) = 0 | ||
Theorem | sgnp 15064 | The signum of a positive extended real is 1. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ ((π΄ β β* β§ 0 < π΄) β (sgnβπ΄) = 1) | ||
Theorem | sgnrrp 15065 | The signum of a positive real is 1. (Contributed by David A. Wheeler, 18-May-2015.) |
β’ (π΄ β β+ β (sgnβπ΄) = 1) | ||
Theorem | sgn1 15066 | The signum of 1 is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
β’ (sgnβ1) = 1 | ||
Theorem | sgnpnf 15067 | The signum of +β is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
β’ (sgnβ+β) = 1 | ||
Theorem | sgnn 15068 | The signum of a negative extended real is -1. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ ((π΄ β β* β§ π΄ < 0) β (sgnβπ΄) = -1) | ||
Theorem | sgnmnf 15069 | The signum of -β is -1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
β’ (sgnβ-β) = -1 | ||
Syntax | ccj 15070 | Extend class notation to include complex conjugate function. |
class β | ||
Syntax | cre 15071 | Extend class notation to include real part of a complex number. |
class β | ||
Syntax | cim 15072 | Extend class notation to include imaginary part of a complex number. |
class β | ||
Definition | df-cj 15073* | Define the complex conjugate function. See cjcli 15143 for its closure and cjval 15076 for its value. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ β = (π₯ β β β¦ (β©π¦ β β ((π₯ + π¦) β β β§ (i Β· (π₯ β π¦)) β β))) | ||
Definition | df-re 15074 | Define a function whose value is the real part of a complex number. See reval 15080 for its value, recli 15141 for its closure, and replim 15090 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.) |
β’ β = (π₯ β β β¦ ((π₯ + (ββπ₯)) / 2)) | ||
Definition | df-im 15075 | Define a function whose value is the imaginary part of a complex number. See imval 15081 for its value, imcli 15142 for its closure, and replim 15090 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.) |
β’ β = (π₯ β β β¦ (ββ(π₯ / i))) | ||
Theorem | cjval 15076* | The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) = (β©π₯ β β ((π΄ + π₯) β β β§ (i Β· (π΄ β π₯)) β β))) | ||
Theorem | cjth 15077 | The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β ((π΄ + (ββπ΄)) β β β§ (i Β· (π΄ β (ββπ΄))) β β)) | ||
Theorem | cjf 15078 | Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.) |
β’ β:ββΆβ | ||
Theorem | cjcl 15079 | The conjugate of a complex number is a complex number (closure law). (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) β β) | ||
Theorem | reval 15080 | The value of the real part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) = ((π΄ + (ββπ΄)) / 2)) | ||
Theorem | imval 15081 | The value of the imaginary part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) = (ββ(π΄ / i))) | ||
Theorem | imre 15082 | The imaginary part of a complex number in terms of the real part function. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) = (ββ(-i Β· π΄))) | ||
Theorem | reim 15083 | The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
β’ (π΄ β β β (ββπ΄) = (ββ(i Β· π΄))) | ||
Theorem | recl 15084 | The real part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) β β) | ||
Theorem | imcl 15085 | The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) β β) | ||
Theorem | ref 15086 | Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ β:ββΆβ | ||
Theorem | imf 15087 | Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ β:ββΆβ | ||
Theorem | crre 15088 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ + (i Β· π΅))) = π΄) | ||
Theorem | crim 15089 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ + (i Β· π΅))) = π΅) | ||
Theorem | replim 15090 | Reconstruct a complex number from its real and imaginary parts. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.) |
β’ (π΄ β β β π΄ = ((ββπ΄) + (i Β· (ββπ΄)))) | ||
Theorem | remim 15091 | Value of the conjugate of a complex number. The value is the real part minus i times the imaginary part. Definition 10-3.2 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) = ((ββπ΄) β (i Β· (ββπ΄)))) | ||
Theorem | reim0 15092 | The imaginary part of a real number is 0. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) = 0) | ||
Theorem | reim0b 15093 | A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.) |
β’ (π΄ β β β (π΄ β β β (ββπ΄) = 0)) | ||
Theorem | rereb 15094 | A number is real iff it equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 20-Aug-2008.) |
β’ (π΄ β β β (π΄ β β β (ββπ΄) = π΄)) | ||
Theorem | mulre 15095 | A product with a nonzero real multiplier is real iff the multiplicand is real. (Contributed by NM, 21-Aug-2008.) |
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (π΄ β β β (π΅ Β· π΄) β β)) | ||
Theorem | rere 15096 | A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Paul Chapman, 7-Sep-2007.) |
β’ (π΄ β β β (ββπ΄) = π΄) | ||
Theorem | cjreb 15097 | A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 2-Jul-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (π΄ β β β (ββπ΄) = π΄)) | ||
Theorem | recj 15098 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (ββ(ββπ΄)) = (ββπ΄)) | ||
Theorem | reneg 15099 | Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (ββ-π΄) = -(ββπ΄)) | ||
Theorem | readd 15100 | Real part distributes over addition. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ + π΅)) = ((ββπ΄) + (ββπ΅))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |