Home | Metamath
Proof Explorer Theorem List (p. 145 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | relexpuzrel 14401 | 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 14402 | 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 14403 | Relation composition becomes addition under exponentiation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) |
⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))) | ||
Syntax | crtrcl 14404 | Extend class notation with recursively defined reflexive, transitive closure. |
class t*rec | ||
Definition | df-rtrclrec 14405* | 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 14406* | 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 14407 | 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 14408 | 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 14409 | 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 14410* | 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 14411 | 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 14412* | 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 14413* | 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 14414* | 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 14415 | Extend class notation with function shifter. |
class shift | ||
Definition | df-shft 14416* | 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 14423 for its value. (Contributed by NM, 20-Jul-2005.) |
⊢ shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)}) | ||
Theorem | shftlem 14417* | Two ways to write a shifted set (𝐵 + 𝐴). (Contributed by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ⊆ ℂ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵} = {𝑥 ∣ ∃𝑦 ∈ 𝐵 𝑥 = (𝑦 + 𝐴)}) | ||
Theorem | shftuz 14418* | A shift of the upper integers. (Contributed by Mario Carneiro, 5-Nov-2013.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ (ℤ≥‘𝐵)} = (ℤ≥‘(𝐵 + 𝐴))) | ||
Theorem | shftfval 14419* | 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 14420* | 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 14421 | Value of a fiber of the relation 𝐹. (Contributed by Mario Carneiro, 4-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) “ {𝐵}) = (𝐹 “ {(𝐵 − 𝐴)})) | ||
Theorem | shftfn 14422* | 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 14423 | Value of a sequence shifted by 𝐴. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴))) | ||
Theorem | shftval2 14424 | Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘(𝐴 + 𝐶)) = (𝐹‘(𝐵 + 𝐶))) | ||
Theorem | shftval3 14425 | Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM, 20-Jul-2005.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘𝐴) = (𝐹‘𝐵)) | ||
Theorem | shftval4 14426 | Value of a sequence shifted by -𝐴. (Contributed by NM, 18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift -𝐴)‘𝐵) = (𝐹‘(𝐴 + 𝐵))) | ||
Theorem | shftval5 14427 | Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘(𝐵 + 𝐴)) = (𝐹‘𝐵)) | ||
Theorem | shftf 14428* | Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐴 ∈ ℂ) → (𝐹 shift 𝐴):{𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵}⟶𝐶) | ||
Theorem | 2shfti 14429 | Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) shift 𝐵) = (𝐹 shift (𝐴 + 𝐵))) | ||
Theorem | shftidt2 14430 | Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 shift 0) = (𝐹 ↾ ℂ) | ||
Theorem | shftidt 14431 | Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐴 ∈ ℂ → ((𝐹 shift 0)‘𝐴) = (𝐹‘𝐴)) | ||
Theorem | shftcan1 14432 | Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐹 shift 𝐴) shift -𝐴)‘𝐵) = (𝐹‘𝐵)) | ||
Theorem | shftcan2 14433 | Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐹 shift -𝐴) shift 𝐴)‘𝐵) = (𝐹‘𝐵)) | ||
Theorem | seqshft 14434 | 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 14435 | Extend class notation to include the Signum function. |
class sgn | ||
Definition | df-sgn 14436 | Signum function. We do not call it "sign", which is homophonic with "sine" (df-sin 15413). 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 15413. We define this over ℝ* (df-xr 10668) instead of ℝ so that it can accept +∞ and -∞. Note that df-psgn 18550 defines the sign of a permutation, which is different. Value shown in sgnval 14437. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ sgn = (𝑥 ∈ ℝ* ↦ if(𝑥 = 0, 0, if(𝑥 < 0, -1, 1))) | ||
Theorem | sgnval 14437 | Value of the signum function. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ (𝐴 ∈ ℝ* → (sgn‘𝐴) = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1))) | ||
Theorem | sgn0 14438 | The signum of 0 is 0. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ (sgn‘0) = 0 | ||
Theorem | sgnp 14439 | The signum of a positive extended real is 1. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (sgn‘𝐴) = 1) | ||
Theorem | sgnrrp 14440 | The signum of a positive real is 1. (Contributed by David A. Wheeler, 18-May-2015.) |
⊢ (𝐴 ∈ ℝ+ → (sgn‘𝐴) = 1) | ||
Theorem | sgn1 14441 | The signum of 1 is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
⊢ (sgn‘1) = 1 | ||
Theorem | sgnpnf 14442 | The signum of +∞ is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
⊢ (sgn‘+∞) = 1 | ||
Theorem | sgnn 14443 | The signum of a negative extended real is -1. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 < 0) → (sgn‘𝐴) = -1) | ||
Theorem | sgnmnf 14444 | The signum of -∞ is -1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
⊢ (sgn‘-∞) = -1 | ||
Syntax | ccj 14445 | Extend class notation to include complex conjugate function. |
class ∗ | ||
Syntax | cre 14446 | Extend class notation to include real part of a complex number. |
class ℜ | ||
Syntax | cim 14447 | Extend class notation to include imaginary part of a complex number. |
class ℑ | ||
Definition | df-cj 14448* | Define the complex conjugate function. See cjcli 14518 for its closure and cjval 14451 for its value. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
⊢ ∗ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ))) | ||
Definition | df-re 14449 | Define a function whose value is the real part of a complex number. See reval 14455 for its value, recli 14516 for its closure, and replim 14465 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.) |
⊢ ℜ = (𝑥 ∈ ℂ ↦ ((𝑥 + (∗‘𝑥)) / 2)) | ||
Definition | df-im 14450 | Define a function whose value is the imaginary part of a complex number. See imval 14456 for its value, imcli 14517 for its closure, and replim 14465 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.) |
⊢ ℑ = (𝑥 ∈ ℂ ↦ (ℜ‘(𝑥 / i))) | ||
Theorem | cjval 14451* | The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013.) |
⊢ (𝐴 ∈ ℂ → (∗‘𝐴) = (℩𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ))) | ||
Theorem | cjth 14452 | The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.) |
⊢ (𝐴 ∈ ℂ → ((𝐴 + (∗‘𝐴)) ∈ ℝ ∧ (i · (𝐴 − (∗‘𝐴))) ∈ ℝ)) | ||
Theorem | cjf 14453 | Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.) |
⊢ ∗:ℂ⟶ℂ | ||
Theorem | cjcl 14454 | 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 14455 | 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 14456 | 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 14457 | 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 14458 | The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = (ℑ‘(i · 𝐴))) | ||
Theorem | recl 14459 | The real part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ) | ||
Theorem | imcl 14460 | The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ) | ||
Theorem | ref 14461 | Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.) |
⊢ ℜ:ℂ⟶ℝ | ||
Theorem | imf 14462 | Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.) |
⊢ ℑ:ℂ⟶ℝ | ||
Theorem | crre 14463 | 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 14464 | 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 14465 | 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 14466 | 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 14467 | 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 14468 | A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.) |
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0)) | ||
Theorem | rereb 14469 | 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 14470 | A product with a nonzero real multiplier is real iff the multiplicand is real. (Contributed by NM, 21-Aug-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 ∈ ℝ ↔ (𝐵 · 𝐴) ∈ ℝ)) | ||
Theorem | rere 14471 | 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 14472 | 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 14473 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴)) | ||
Theorem | reneg 14474 | Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) = -(ℜ‘𝐴)) | ||
Theorem | readd 14475 | Real part distributes over addition. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))) | ||
Theorem | resub 14476 | Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 − 𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵))) | ||
Theorem | remullem 14477 | Lemma for remul 14478, immul 14485, and cjmul 14491. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))) ∧ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))) ∧ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵)))) | ||
Theorem | remul 14478 | Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵)))) | ||
Theorem | remul2 14479 | Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵))) | ||
Theorem | rediv 14480 | Real part of a division. Related to remul2 14479. (Contributed by David A. Wheeler, 10-Jun-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (ℜ‘(𝐴 / 𝐵)) = ((ℜ‘𝐴) / 𝐵)) | ||
Theorem | imcj 14481 | Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴)) | ||
Theorem | imneg 14482 | The imaginary part of a negative number. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (ℑ‘-𝐴) = -(ℑ‘𝐴)) | ||
Theorem | imadd 14483 | Imaginary part distributes over addition. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))) | ||
Theorem | imsub 14484 | Imaginary part distributes over subtraction. (Contributed by NM, 18-Mar-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 − 𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵))) | ||
Theorem | immul 14485 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵)))) | ||
Theorem | immul2 14486 | Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 · 𝐵)) = (𝐴 · (ℑ‘𝐵))) | ||
Theorem | imdiv 14487 | Imaginary part of a division. Related to immul2 14486. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (ℑ‘(𝐴 / 𝐵)) = ((ℑ‘𝐴) / 𝐵)) | ||
Theorem | cjre 14488 | A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 8-Oct-1999.) |
⊢ (𝐴 ∈ ℝ → (∗‘𝐴) = 𝐴) | ||
Theorem | cjcj 14489 | 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 14490 | 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 14491 | 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 14492 | Standard inner product on complex numbers. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵)))) | ||
Theorem | cjmulrcl 14493 | A complex number times its conjugate is real. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) ∈ ℝ) | ||
Theorem | cjmulval 14494 | A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) | ||
Theorem | cjmulge0 14495 | A complex number times its conjugate is nonnegative. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → 0 ≤ (𝐴 · (∗‘𝐴))) | ||
Theorem | cjneg 14496 | Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (∗‘-𝐴) = -(∗‘𝐴)) | ||
Theorem | addcj 14497 | 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 14498 | Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∗‘(𝐴 − 𝐵)) = ((∗‘𝐴) − (∗‘𝐵))) | ||
Theorem | cjexp 14499 | Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁)) | ||
Theorem | imval2 14500 | The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) = ((𝐴 − (∗‘𝐴)) / (2 · i))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |