| Metamath
Proof Explorer Theorem List (p. 152 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | dfrtrcl2 15101 | 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 15102* | 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 15103* | 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 15104* | 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 15105 | Extend class notation with function shifter. |
| class shift | ||
| Definition | df-shft 15106* | 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 15113 for its value. (Contributed by NM, 20-Jul-2005.) |
| ⊢ shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)}) | ||
| Theorem | shftlem 15107* | Two ways to write a shifted set (𝐵 + 𝐴). (Contributed by Mario Carneiro, 3-Nov-2013.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ⊆ ℂ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵} = {𝑥 ∣ ∃𝑦 ∈ 𝐵 𝑥 = (𝑦 + 𝐴)}) | ||
| Theorem | shftuz 15108* | A shift of the upper integers. (Contributed by Mario Carneiro, 5-Nov-2013.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ (ℤ≥‘𝐵)} = (ℤ≥‘(𝐵 + 𝐴))) | ||
| Theorem | shftfval 15109* | 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 15110* | 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 15111 | Value of a fiber of the relation 𝐹. (Contributed by Mario Carneiro, 4-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) “ {𝐵}) = (𝐹 “ {(𝐵 − 𝐴)})) | ||
| Theorem | shftfn 15112* | 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 15113 | Value of a sequence shifted by 𝐴. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴))) | ||
| Theorem | shftval2 15114 | Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘(𝐴 + 𝐶)) = (𝐹‘(𝐵 + 𝐶))) | ||
| Theorem | shftval3 15115 | Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM, 20-Jul-2005.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘𝐴) = (𝐹‘𝐵)) | ||
| Theorem | shftval4 15116 | Value of a sequence shifted by -𝐴. (Contributed by NM, 18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift -𝐴)‘𝐵) = (𝐹‘(𝐴 + 𝐵))) | ||
| Theorem | shftval5 15117 | Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘(𝐵 + 𝐴)) = (𝐹‘𝐵)) | ||
| Theorem | shftf 15118* | Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐴 ∈ ℂ) → (𝐹 shift 𝐴):{𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵}⟶𝐶) | ||
| Theorem | 2shfti 15119 | Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) shift 𝐵) = (𝐹 shift (𝐴 + 𝐵))) | ||
| Theorem | shftidt2 15120 | Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 shift 0) = (𝐹 ↾ ℂ) | ||
| Theorem | shftidt 15121 | Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ (𝐴 ∈ ℂ → ((𝐹 shift 0)‘𝐴) = (𝐹‘𝐴)) | ||
| Theorem | shftcan1 15122 | Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐹 shift 𝐴) shift -𝐴)‘𝐵) = (𝐹‘𝐵)) | ||
| Theorem | shftcan2 15123 | Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐹 shift -𝐴) shift 𝐴)‘𝐵) = (𝐹‘𝐵)) | ||
| Theorem | seqshft 15124 | 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 15125 | Extend class notation to include the Signum function. |
| class sgn | ||
| Definition | df-sgn 15126 | Signum function. We do not call it "sign", which is homophonic with "sine" (df-sin 16105). 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 16105. We define this over ℝ* (df-xr 11299) instead of ℝ so that it can accept +∞ and -∞. Note that df-psgn 19509 defines the sign of a permutation, which is different. Value shown in sgnval 15127. (Contributed by David A. Wheeler, 15-May-2015.) |
| ⊢ sgn = (𝑥 ∈ ℝ* ↦ if(𝑥 = 0, 0, if(𝑥 < 0, -1, 1))) | ||
| Theorem | sgnval 15127 | Value of the signum function. (Contributed by David A. Wheeler, 15-May-2015.) |
| ⊢ (𝐴 ∈ ℝ* → (sgn‘𝐴) = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1))) | ||
| Theorem | sgn0 15128 | The signum of 0 is 0. (Contributed by David A. Wheeler, 15-May-2015.) |
| ⊢ (sgn‘0) = 0 | ||
| Theorem | sgnp 15129 | The signum of a positive extended real is 1. (Contributed by David A. Wheeler, 15-May-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (sgn‘𝐴) = 1) | ||
| Theorem | sgnrrp 15130 | The signum of a positive real is 1. (Contributed by David A. Wheeler, 18-May-2015.) |
| ⊢ (𝐴 ∈ ℝ+ → (sgn‘𝐴) = 1) | ||
| Theorem | sgn1 15131 | The signum of 1 is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
| ⊢ (sgn‘1) = 1 | ||
| Theorem | sgnpnf 15132 | The signum of +∞ is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
| ⊢ (sgn‘+∞) = 1 | ||
| Theorem | sgnn 15133 | The signum of a negative extended real is -1. (Contributed by David A. Wheeler, 15-May-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 < 0) → (sgn‘𝐴) = -1) | ||
| Theorem | sgnmnf 15134 | The signum of -∞ is -1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
| ⊢ (sgn‘-∞) = -1 | ||
| Syntax | ccj 15135 | Extend class notation to include complex conjugate function. |
| class ∗ | ||
| Syntax | cre 15136 | Extend class notation to include real part of a complex number. |
| class ℜ | ||
| Syntax | cim 15137 | Extend class notation to include imaginary part of a complex number. |
| class ℑ | ||
| Definition | df-cj 15138* | Define the complex conjugate function. See cjcli 15208 for its closure and cjval 15141 for its value. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
| ⊢ ∗ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ))) | ||
| Definition | df-re 15139 | Define a function whose value is the real part of a complex number. See reval 15145 for its value, recli 15206 for its closure, and replim 15155 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.) |
| ⊢ ℜ = (𝑥 ∈ ℂ ↦ ((𝑥 + (∗‘𝑥)) / 2)) | ||
| Definition | df-im 15140 | Define a function whose value is the imaginary part of a complex number. See imval 15146 for its value, imcli 15207 for its closure, and replim 15155 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.) |
| ⊢ ℑ = (𝑥 ∈ ℂ ↦ (ℜ‘(𝑥 / i))) | ||
| Theorem | cjval 15141* | The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013.) |
| ⊢ (𝐴 ∈ ℂ → (∗‘𝐴) = (℩𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ))) | ||
| Theorem | cjth 15142 | The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.) |
| ⊢ (𝐴 ∈ ℂ → ((𝐴 + (∗‘𝐴)) ∈ ℝ ∧ (i · (𝐴 − (∗‘𝐴))) ∈ ℝ)) | ||
| Theorem | cjf 15143 | Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.) |
| ⊢ ∗:ℂ⟶ℂ | ||
| Theorem | cjcl 15144 | 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 15145 | 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 15146 | 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 15147 | 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 15148 | The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
| ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = (ℑ‘(i · 𝐴))) | ||
| Theorem | recl 15149 | The real part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
| ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ) | ||
| Theorem | imcl 15150 | The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
| ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ) | ||
| Theorem | ref 15151 | Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.) |
| ⊢ ℜ:ℂ⟶ℝ | ||
| Theorem | imf 15152 | Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.) |
| ⊢ ℑ:ℂ⟶ℝ | ||
| Theorem | crre 15153 | 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 15154 | 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 15155 | 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 15156 | 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 15157 | 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 15158 | A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0)) | ||
| Theorem | rereb 15159 | 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 15160 | A product with a nonzero real multiplier is real iff the multiplicand is real. (Contributed by NM, 21-Aug-2008.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 ∈ ℝ ↔ (𝐵 · 𝐴) ∈ ℝ)) | ||
| Theorem | rere 15161 | 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 15162 | 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 15163 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.) |
| ⊢ (𝐴 ∈ ℂ → (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴)) | ||
| Theorem | reneg 15164 | Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
| ⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) = -(ℜ‘𝐴)) | ||
| Theorem | readd 15165 | Real part distributes over addition. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))) | ||
| Theorem | resub 15166 | Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 − 𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵))) | ||
| Theorem | remullem 15167 | Lemma for remul 15168, immul 15175, and cjmul 15181. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))) ∧ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))) ∧ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵)))) | ||
| Theorem | remul 15168 | Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵)))) | ||
| Theorem | remul2 15169 | Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵))) | ||
| Theorem | rediv 15170 | Real part of a division. Related to remul2 15169. (Contributed by David A. Wheeler, 10-Jun-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (ℜ‘(𝐴 / 𝐵)) = ((ℜ‘𝐴) / 𝐵)) | ||
| Theorem | imcj 15171 | Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
| ⊢ (𝐴 ∈ ℂ → (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴)) | ||
| Theorem | imneg 15172 | The imaginary part of a negative number. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
| ⊢ (𝐴 ∈ ℂ → (ℑ‘-𝐴) = -(ℑ‘𝐴)) | ||
| Theorem | imadd 15173 | Imaginary part distributes over addition. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))) | ||
| Theorem | imsub 15174 | Imaginary part distributes over subtraction. (Contributed by NM, 18-Mar-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 − 𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵))) | ||
| Theorem | immul 15175 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵)))) | ||
| Theorem | immul2 15176 | Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 · 𝐵)) = (𝐴 · (ℑ‘𝐵))) | ||
| Theorem | imdiv 15177 | Imaginary part of a division. Related to immul2 15176. (Contributed by Mario Carneiro, 20-Jun-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (ℑ‘(𝐴 / 𝐵)) = ((ℑ‘𝐴) / 𝐵)) | ||
| Theorem | cjre 15178 | A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 8-Oct-1999.) |
| ⊢ (𝐴 ∈ ℝ → (∗‘𝐴) = 𝐴) | ||
| Theorem | cjcj 15179 | 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 15180 | 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 15181 | 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 15182 | Standard inner product on complex numbers. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵)))) | ||
| Theorem | cjmulrcl 15183 | A complex number times its conjugate is real. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) ∈ ℝ) | ||
| Theorem | cjmulval 15184 | A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 14-Jul-2014.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) | ||
| Theorem | cjmulge0 15185 | A complex number times its conjugate is nonnegative. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
| ⊢ (𝐴 ∈ ℂ → 0 ≤ (𝐴 · (∗‘𝐴))) | ||
| Theorem | cjneg 15186 | Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
| ⊢ (𝐴 ∈ ℂ → (∗‘-𝐴) = -(∗‘𝐴)) | ||
| Theorem | addcj 15187 | 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 15188 | Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∗‘(𝐴 − 𝐵)) = ((∗‘𝐴) − (∗‘𝐵))) | ||
| Theorem | cjexp 15189 | Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁)) | ||
| Theorem | imval2 15190 | The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.) |
| ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) = ((𝐴 − (∗‘𝐴)) / (2 · i))) | ||
| Theorem | re0 15191 | The real part of zero. (Contributed by NM, 27-Jul-1999.) |
| ⊢ (ℜ‘0) = 0 | ||
| Theorem | im0 15192 | The imaginary part of zero. (Contributed by NM, 27-Jul-1999.) |
| ⊢ (ℑ‘0) = 0 | ||
| Theorem | re1 15193 | The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.) |
| ⊢ (ℜ‘1) = 1 | ||
| Theorem | im1 15194 | The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.) |
| ⊢ (ℑ‘1) = 0 | ||
| Theorem | rei 15195 | The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
| ⊢ (ℜ‘i) = 0 | ||
| Theorem | imi 15196 | The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
| ⊢ (ℑ‘i) = 1 | ||
| Theorem | cj0 15197 | The conjugate of zero. (Contributed by NM, 27-Jul-1999.) |
| ⊢ (∗‘0) = 0 | ||
| Theorem | cji 15198 | The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
| ⊢ (∗‘i) = -i | ||
| Theorem | cjreim 15199 | The conjugate of a representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (∗‘(𝐴 + (i · 𝐵))) = (𝐴 − (i · 𝐵))) | ||
| Theorem | cjreim2 15200 | The conjugate of the representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (∗‘(𝐴 − (i · 𝐵))) = (𝐴 + (i · 𝐵))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |