P. 151 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15001-15100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	relexpfldd 15001	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 15002	Relation composition becomes addition under exponentiation. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))
Theorem	relexpuzrel 15003	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 15004	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 15005	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)    ⇒   ⊢ (𝜑 → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))
5.8.5  Reflexive-transitive closure as an indexed union
Syntax	crtrcl 15006	Extend class notation with recursively defined reflexive, transitive closure.
class t*rec
Definition	df-rtrclrec 15007*	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 15008	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 15009*	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 15010	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 15011	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 15012*	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 15013	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‘𝑅))
5.8.6  Principle of transitive induction. 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 15014*	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 15015*	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 15016*	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*‘𝑅)𝑋 → 𝜏))
5.9  Elementary real and complex functions
5.9.1  The "shift" operation
Syntax	cshi 15017	Extend class notation with function shifter.
class shift
Definition	df-shft 15018*	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 15025 for its value. (Contributed by NM, 20-Jul-2005.)
⊢ shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)})
Theorem	shftlem 15019*	Two ways to write a shifted set (𝐵 + 𝐴). (Contributed by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ⊆ ℂ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵} = {𝑥 ∣ ∃𝑦 ∈ 𝐵 𝑥 = (𝑦 + 𝐴)})
Theorem	shftuz 15020*	A shift of the upper integers. (Contributed by Mario Carneiro, 5-Nov-2013.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ (ℤ≥‘𝐵)} = (ℤ≥‘(𝐵 + 𝐴)))
Theorem	shftfval 15021*	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 15022*	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 15023	Value of a fiber of the relation 𝐹. (Contributed by Mario Carneiro, 4-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) “ {𝐵}) = (𝐹 “ {(𝐵 − 𝐴)}))
Theorem	shftfn 15024*	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 15025	Value of a sequence shifted by 𝐴. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴)))
Theorem	shftval2 15026	Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘(𝐴 + 𝐶)) = (𝐹‘(𝐵 + 𝐶)))
Theorem	shftval3 15027	Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM, 20-Jul-2005.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘𝐴) = (𝐹‘𝐵))
Theorem	shftval4 15028	Value of a sequence shifted by -𝐴. (Contributed by NM, 18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift -𝐴)‘𝐵) = (𝐹‘(𝐴 + 𝐵)))
Theorem	shftval5 15029	Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘(𝐵 + 𝐴)) = (𝐹‘𝐵))
Theorem	shftf 15030*	Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐴 ∈ ℂ) → (𝐹 shift 𝐴):{𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵}⟶𝐶)
Theorem	2shfti 15031	Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) shift 𝐵) = (𝐹 shift (𝐴 + 𝐵)))
Theorem	shftidt2 15032	Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 shift 0) = (𝐹 ↾ ℂ)
Theorem	shftidt 15033	Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐴 ∈ ℂ → ((𝐹 shift 0)‘𝐴) = (𝐹‘𝐴))
Theorem	shftcan1 15034	Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐹 shift 𝐴) shift -𝐴)‘𝐵) = (𝐹‘𝐵))
Theorem	shftcan2 15035	Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐹 shift -𝐴) shift 𝐴)‘𝐵) = (𝐹‘𝐵))
Theorem	seqshft 15036	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 𝑁))
5.9.2  Signum (sgn or sign) function
Syntax	csgn 15037	Extend class notation to include the Signum function.
class sgn
Definition	df-sgn 15038	Signum function. We do not call it "sign", which is homophonic with "sine" (df-sin 16017). 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 16017. We define this over ℝ* (df-xr 11256) instead of ℝ so that it can accept +∞ and -∞. Note that df-psgn 19400 defines the sign of a permutation, which is different. Value shown in sgnval 15039. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ sgn = (𝑥 ∈ ℝ* ↦ if(𝑥 = 0, 0, if(𝑥 < 0, -1, 1)))
Theorem	sgnval 15039	Value of the signum function. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ (𝐴 ∈ ℝ* → (sgn‘𝐴) = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1)))
Theorem	sgn0 15040	The signum of 0 is 0. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ (sgn‘0) = 0
Theorem	sgnp 15041	The signum of a positive extended real is 1. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (sgn‘𝐴) = 1)
Theorem	sgnrrp 15042	The signum of a positive real is 1. (Contributed by David A. Wheeler, 18-May-2015.)
⊢ (𝐴 ∈ ℝ+ → (sgn‘𝐴) = 1)
Theorem	sgn1 15043	The signum of 1 is 1. (Contributed by David A. Wheeler, 26-Jun-2016.)
⊢ (sgn‘1) = 1
Theorem	sgnpnf 15044	The signum of +∞ is 1. (Contributed by David A. Wheeler, 26-Jun-2016.)
⊢ (sgn‘+∞) = 1
Theorem	sgnn 15045	The signum of a negative extended real is -1. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 < 0) → (sgn‘𝐴) = -1)
Theorem	sgnmnf 15046	The signum of -∞ is -1. (Contributed by David A. Wheeler, 26-Jun-2016.)
⊢ (sgn‘-∞) = -1
5.9.3  Real and imaginary parts; conjugate
Syntax	ccj 15047	Extend class notation to include complex conjugate function.
class ∗
Syntax	cre 15048	Extend class notation to include real part of a complex number.
class ℜ
Syntax	cim 15049	Extend class notation to include imaginary part of a complex number.
class ℑ
Definition	df-cj 15050*	Define the complex conjugate function. See cjcli 15120 for its closure and cjval 15053 for its value. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ ∗ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ)))
Definition	df-re 15051	Define a function whose value is the real part of a complex number. See reval 15057 for its value, recli 15118 for its closure, and replim 15067 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
⊢ ℜ = (𝑥 ∈ ℂ ↦ ((𝑥 + (∗‘𝑥)) / 2))
Definition	df-im 15052	Define a function whose value is the imaginary part of a complex number. See imval 15058 for its value, imcli 15119 for its closure, and replim 15067 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
⊢ ℑ = (𝑥 ∈ ℂ ↦ (ℜ‘(𝑥 / i)))
Theorem	cjval 15053*	The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (∗‘𝐴) = (℩𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ)))
Theorem	cjth 15054	The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → ((𝐴 + (∗‘𝐴)) ∈ ℝ ∧ (i · (𝐴 − (∗‘𝐴))) ∈ ℝ))
Theorem	cjf 15055	Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ ∗:ℂ⟶ℂ
Theorem	cjcl 15056	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 15057	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 15058	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 15059	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 15060	The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = (ℑ‘(i · 𝐴)))
Theorem	recl 15061	The real part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ)
Theorem	imcl 15062	The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ)
Theorem	ref 15063	Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ ℜ:ℂ⟶ℝ
Theorem	imf 15064	Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ ℑ:ℂ⟶ℝ
Theorem	crre 15065	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 15066	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 15067	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 15068	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 15069	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 15070	A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.)
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0))
Theorem	rereb 15071	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 15072	A product with a nonzero real multiplier is real iff the multiplicand is real. (Contributed by NM, 21-Aug-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 ∈ ℝ ↔ (𝐵 · 𝐴) ∈ ℝ))
Theorem	rere 15073	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 15074	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 15075	Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴))
Theorem	reneg 15076	Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) = -(ℜ‘𝐴))
Theorem	readd 15077	Real part distributes over addition. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵)))
Theorem	resub 15078	Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 − 𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵)))
Theorem	remullem 15079	Lemma for remul 15080, immul 15087, and cjmul 15093. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))) ∧ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))) ∧ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵))))
Theorem	remul 15080	Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))))
Theorem	remul2 15081	Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵)))
Theorem	rediv 15082	Real part of a division. Related to remul2 15081. (Contributed by David A. Wheeler, 10-Jun-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (ℜ‘(𝐴 / 𝐵)) = ((ℜ‘𝐴) / 𝐵))
Theorem	imcj 15083	Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴))
Theorem	imneg 15084	The imaginary part of a negative number. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (ℑ‘-𝐴) = -(ℑ‘𝐴))
Theorem	imadd 15085	Imaginary part distributes over addition. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵)))
Theorem	imsub 15086	Imaginary part distributes over subtraction. (Contributed by NM, 18-Mar-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 − 𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵)))
Theorem	immul 15087	Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))))
Theorem	immul2 15088	Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 · 𝐵)) = (𝐴 · (ℑ‘𝐵)))
Theorem	imdiv 15089	Imaginary part of a division. Related to immul2 15088. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (ℑ‘(𝐴 / 𝐵)) = ((ℑ‘𝐴) / 𝐵))
Theorem	cjre 15090	A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 8-Oct-1999.)
⊢ (𝐴 ∈ ℝ → (∗‘𝐴) = 𝐴)
Theorem	cjcj 15091	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 15092	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 15093	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 15094	Standard inner product on complex numbers. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵))))
Theorem	cjmulrcl 15095	A complex number times its conjugate is real. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) ∈ ℝ)
Theorem	cjmulval 15096	A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
Theorem	cjmulge0 15097	A complex number times its conjugate is nonnegative. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → 0 ≤ (𝐴 · (∗‘𝐴)))
Theorem	cjneg 15098	Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (∗‘-𝐴) = -(∗‘𝐴))
Theorem	addcj 15099	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 15100	Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∗‘(𝐴 − 𝐵)) = ((∗‘𝐴) − (∗‘𝐵)))