P. 152 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15101-15200   *Has distinct variable group(s)

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