![]() |
Metamath
Proof Explorer Theorem List (p. 143 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43661) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | relexpaddd 14201 | Relation composition becomes addition under exponentiation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) |
⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))) | ||
Syntax | crtrcl 14202 | Extend class notation with recursively defined reflexive, transitive closure. |
class t*rec | ||
Definition | df-rtrclrec 14203* | 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 | dfrtrclrec2 14204* | 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.) |
⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (𝐴(t*rec‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵)) | ||
Theorem | rtrclreclem1 14205 | The reflexive, transitive closure is indeed reflexive. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) |
⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ( I ↾ ∪ ∪ 𝑅) ⊆ (t*rec‘𝑅)) | ||
Theorem | rtrclreclem2 14206 | The reflexive, transitive closure is indeed a closure. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ (t*rec‘𝑅)) | ||
Theorem | rtrclreclem3 14207 | The reflexive, transitive closure is indeed transitive. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) |
⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ((t*rec‘𝑅) ∘ (t*rec‘𝑅)) ⊆ (t*rec‘𝑅)) | ||
Theorem | rtrclreclem4 14208* | 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.) |
⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ∀𝑠((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (t*rec‘𝑅) ⊆ 𝑠)) | ||
Theorem | dfrtrcl2 14209 | 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.) |
⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (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 14210* | 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.) |
⊢ (𝜂 → Rel 𝑅) & ⊢ (𝜂 → 𝑅 ∈ V) & ⊢ (𝜂 → 𝑆 ∈ V) & ⊢ (𝑖 = 𝑆 → (𝜑 ↔ 𝜒)) & ⊢ (𝑖 = 𝑥 → (𝜑 ↔ 𝜓)) & ⊢ (𝑖 = 𝑗 → (𝜑 ↔ 𝜃)) & ⊢ (𝜂 → 𝜒) & ⊢ (𝜂 → (𝑗𝑅𝑥 → (𝜃 → 𝜓))) ⇒ ⊢ (𝜂 → (𝑛 ∈ ℕ0 → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))) | ||
Theorem | relexpind 14211* | Principle of transitive induction, finite 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.) |
⊢ (𝜂 → Rel 𝑅) & ⊢ (𝜂 → 𝑅 ∈ V) & ⊢ (𝜂 → 𝑆 ∈ V) & ⊢ (𝜂 → 𝑋 ∈ V) & ⊢ (𝑖 = 𝑆 → (𝜑 ↔ 𝜒)) & ⊢ (𝑖 = 𝑥 → (𝜑 ↔ 𝜓)) & ⊢ (𝑖 = 𝑗 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜏)) & ⊢ (𝜂 → 𝜒) & ⊢ (𝜂 → (𝑗𝑅𝑥 → (𝜃 → 𝜓))) ⇒ ⊢ (𝜂 → (𝑛 ∈ ℕ0 → (𝑆(𝑅↑𝑟𝑛)𝑋 → 𝜏))) | ||
Theorem | rtrclind 14212* | Principle of transitive induction. The first four 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.) |
⊢ (𝜂 → Rel 𝑅) & ⊢ (𝜂 → 𝑅 ∈ V) & ⊢ (𝜂 → 𝑆 ∈ V) & ⊢ (𝜂 → 𝑋 ∈ V) & ⊢ (𝑖 = 𝑆 → (𝜑 ↔ 𝜒)) & ⊢ (𝑖 = 𝑥 → (𝜑 ↔ 𝜓)) & ⊢ (𝑖 = 𝑗 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜏)) & ⊢ (𝜂 → 𝜒) & ⊢ (𝜂 → (𝑗𝑅𝑥 → (𝜃 → 𝜓))) ⇒ ⊢ (𝜂 → (𝑆(t*‘𝑅)𝑋 → 𝜏)) | ||
Syntax | cshi 14213 | Extend class notation with function shifter. |
class shift | ||
Definition | df-shft 14214* | 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 14221 for its value. (Contributed by NM, 20-Jul-2005.) |
⊢ shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)}) | ||
Theorem | shftlem 14215* | Two ways to write a shifted set (𝐵 + 𝐴). (Contributed by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ⊆ ℂ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵} = {𝑥 ∣ ∃𝑦 ∈ 𝐵 𝑥 = (𝑦 + 𝐴)}) | ||
Theorem | shftuz 14216* | A shift of the upper integers. (Contributed by Mario Carneiro, 5-Nov-2013.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ (ℤ≥‘𝐵)} = (ℤ≥‘(𝐵 + 𝐴))) | ||
Theorem | shftfval 14217* | 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 14218* | 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 14219 | Value of a fiber of the relation 𝐹. (Contributed by Mario Carneiro, 4-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) “ {𝐵}) = (𝐹 “ {(𝐵 − 𝐴)})) | ||
Theorem | shftfn 14220* | 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 14221 | Value of a sequence shifted by 𝐴. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴))) | ||
Theorem | shftval2 14222 | Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘(𝐴 + 𝐶)) = (𝐹‘(𝐵 + 𝐶))) | ||
Theorem | shftval3 14223 | Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM, 20-Jul-2005.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘𝐴) = (𝐹‘𝐵)) | ||
Theorem | shftval4 14224 | Value of a sequence shifted by -𝐴. (Contributed by NM, 18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift -𝐴)‘𝐵) = (𝐹‘(𝐴 + 𝐵))) | ||
Theorem | shftval5 14225 | Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘(𝐵 + 𝐴)) = (𝐹‘𝐵)) | ||
Theorem | shftf 14226* | Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐴 ∈ ℂ) → (𝐹 shift 𝐴):{𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵}⟶𝐶) | ||
Theorem | 2shfti 14227 | Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) shift 𝐵) = (𝐹 shift (𝐴 + 𝐵))) | ||
Theorem | shftidt2 14228 | Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 shift 0) = (𝐹 ↾ ℂ) | ||
Theorem | shftidt 14229 | Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐴 ∈ ℂ → ((𝐹 shift 0)‘𝐴) = (𝐹‘𝐴)) | ||
Theorem | shftcan1 14230 | Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐹 shift 𝐴) shift -𝐴)‘𝐵) = (𝐹‘𝐵)) | ||
Theorem | shftcan2 14231 | Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐹 shift -𝐴) shift 𝐴)‘𝐵) = (𝐹‘𝐵)) | ||
Theorem | seqshft 14232 | 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 14233 | Extend class notation to include the Signum function. |
class sgn | ||
Definition | df-sgn 14234 | Signum function. We do not call it "sign", which is homophonic with "sine" (df-sin 15202). 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. We define this over ℝ* (df-xr 10415) instead of ℝ so that it can accept +∞ and -∞. Note that df-psgn 18294 defines the sign of a permutation, which is different. Value shown in sgnval 14235. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ sgn = (𝑥 ∈ ℝ* ↦ if(𝑥 = 0, 0, if(𝑥 < 0, -1, 1))) | ||
Theorem | sgnval 14235 | Value of the signum function. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ (𝐴 ∈ ℝ* → (sgn‘𝐴) = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1))) | ||
Theorem | sgn0 14236 | The signum of 0 is 0. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ (sgn‘0) = 0 | ||
Theorem | sgnp 14237 | The signum of a positive extended real is 1. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (sgn‘𝐴) = 1) | ||
Theorem | sgnrrp 14238 | The signum of a positive real is 1. (Contributed by David A. Wheeler, 18-May-2015.) |
⊢ (𝐴 ∈ ℝ+ → (sgn‘𝐴) = 1) | ||
Theorem | sgn1 14239 | The signum of 1 is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
⊢ (sgn‘1) = 1 | ||
Theorem | sgnpnf 14240 | The signum of +∞ is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
⊢ (sgn‘+∞) = 1 | ||
Theorem | sgnn 14241 | The signum of a negative extended real is -1. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 < 0) → (sgn‘𝐴) = -1) | ||
Theorem | sgnmnf 14242 | The signum of -∞ is -1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
⊢ (sgn‘-∞) = -1 | ||
Syntax | ccj 14243 | Extend class notation to include complex conjugate function. |
class ∗ | ||
Syntax | cre 14244 | Extend class notation to include real part of a complex number. |
class ℜ | ||
Syntax | cim 14245 | Extend class notation to include imaginary part of a complex number. |
class ℑ | ||
Definition | df-cj 14246* | Define the complex conjugate function. See cjcli 14316 for its closure and cjval 14249 for its value. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
⊢ ∗ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ))) | ||
Definition | df-re 14247 | Define a function whose value is the real part of a complex number. See reval 14253 for its value, recli 14314 for its closure, and replim 14263 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.) |
⊢ ℜ = (𝑥 ∈ ℂ ↦ ((𝑥 + (∗‘𝑥)) / 2)) | ||
Definition | df-im 14248 | Define a function whose value is the imaginary part of a complex number. See imval 14254 for its value, imcli 14315 for its closure, and replim 14263 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.) |
⊢ ℑ = (𝑥 ∈ ℂ ↦ (ℜ‘(𝑥 / i))) | ||
Theorem | cjval 14249* | The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013.) |
⊢ (𝐴 ∈ ℂ → (∗‘𝐴) = (℩𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ))) | ||
Theorem | cjth 14250 | The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.) |
⊢ (𝐴 ∈ ℂ → ((𝐴 + (∗‘𝐴)) ∈ ℝ ∧ (i · (𝐴 − (∗‘𝐴))) ∈ ℝ)) | ||
Theorem | cjf 14251 | Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.) |
⊢ ∗:ℂ⟶ℂ | ||
Theorem | cjcl 14252 | 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 14253 | 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 14254 | 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 14255 | 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 14256 | The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = (ℑ‘(i · 𝐴))) | ||
Theorem | recl 14257 | The real part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ) | ||
Theorem | imcl 14258 | The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ) | ||
Theorem | ref 14259 | Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.) |
⊢ ℜ:ℂ⟶ℝ | ||
Theorem | imf 14260 | Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.) |
⊢ ℑ:ℂ⟶ℝ | ||
Theorem | crre 14261 | 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 14262 | 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 14263 | 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 14264 | 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 14265 | 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 14266 | A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.) |
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0)) | ||
Theorem | rereb 14267 | 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 14268 | A product with a nonzero real multiplier is real iff the multiplicand is real. (Contributed by NM, 21-Aug-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 ∈ ℝ ↔ (𝐵 · 𝐴) ∈ ℝ)) | ||
Theorem | rere 14269 | 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 14270 | 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 14271 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴)) | ||
Theorem | reneg 14272 | Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) = -(ℜ‘𝐴)) | ||
Theorem | readd 14273 | Real part distributes over addition. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))) | ||
Theorem | resub 14274 | Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 − 𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵))) | ||
Theorem | remullem 14275 | Lemma for remul 14276, immul 14283, and cjmul 14289. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))) ∧ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))) ∧ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵)))) | ||
Theorem | remul 14276 | Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵)))) | ||
Theorem | remul2 14277 | Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵))) | ||
Theorem | rediv 14278 | Real part of a division. Related to remul2 14277. (Contributed by David A. Wheeler, 10-Jun-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (ℜ‘(𝐴 / 𝐵)) = ((ℜ‘𝐴) / 𝐵)) | ||
Theorem | imcj 14279 | Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴)) | ||
Theorem | imneg 14280 | The imaginary part of a negative number. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (ℑ‘-𝐴) = -(ℑ‘𝐴)) | ||
Theorem | imadd 14281 | Imaginary part distributes over addition. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))) | ||
Theorem | imsub 14282 | Imaginary part distributes over subtraction. (Contributed by NM, 18-Mar-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 − 𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵))) | ||
Theorem | immul 14283 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵)))) | ||
Theorem | immul2 14284 | Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 · 𝐵)) = (𝐴 · (ℑ‘𝐵))) | ||
Theorem | imdiv 14285 | Imaginary part of a division. Related to immul2 14284. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (ℑ‘(𝐴 / 𝐵)) = ((ℑ‘𝐴) / 𝐵)) | ||
Theorem | cjre 14286 | A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 8-Oct-1999.) |
⊢ (𝐴 ∈ ℝ → (∗‘𝐴) = 𝐴) | ||
Theorem | cjcj 14287 | The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (∗‘(∗‘𝐴)) = 𝐴) | ||
Theorem | cjadd 14288 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵))) | ||
Theorem | cjmul 14289 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵))) | ||
Theorem | ipcnval 14290 | Standard inner product on complex numbers. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵)))) | ||
Theorem | cjmulrcl 14291 | A complex number times its conjugate is real. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) ∈ ℝ) | ||
Theorem | cjmulval 14292 | A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) | ||
Theorem | cjmulge0 14293 | A complex number times its conjugate is nonnegative. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → 0 ≤ (𝐴 · (∗‘𝐴))) | ||
Theorem | cjneg 14294 | Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (∗‘-𝐴) = -(∗‘𝐴)) | ||
Theorem | addcj 14295 | A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by NM, 21-Jan-2007.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴 + (∗‘𝐴)) = (2 · (ℜ‘𝐴))) | ||
Theorem | cjsub 14296 | Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∗‘(𝐴 − 𝐵)) = ((∗‘𝐴) − (∗‘𝐵))) | ||
Theorem | cjexp 14297 | Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁)) | ||
Theorem | imval2 14298 | The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) = ((𝐴 − (∗‘𝐴)) / (2 · i))) | ||
Theorem | re0 14299 | The real part of zero. (Contributed by NM, 27-Jul-1999.) |
⊢ (ℜ‘0) = 0 | ||
Theorem | im0 14300 | The imaginary part of zero. (Contributed by NM, 27-Jul-1999.) |
⊢ (ℑ‘0) = 0 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |