P. 153 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15201-15300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ipcnval 15201	Standard inner product on complex numbers. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵))))
Theorem	cjmulrcl 15202	A complex number times its conjugate is real. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) ∈ ℝ)
Theorem	cjmulval 15203	A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
Theorem	cjmulge0 15204	A complex number times its conjugate is nonnegative. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → 0 ≤ (𝐴 · (∗‘𝐴)))
Theorem	cjneg 15205	Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (∗‘-𝐴) = -(∗‘𝐴))
Theorem	addcj 15206	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 15207	Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∗‘(𝐴 − 𝐵)) = ((∗‘𝐴) − (∗‘𝐵)))
Theorem	cjexp 15208	Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁))
Theorem	imval2 15209	The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) = ((𝐴 − (∗‘𝐴)) / (2 · i)))
Theorem	re0 15210	The real part of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (ℜ‘0) = 0
Theorem	im0 15211	The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (ℑ‘0) = 0
Theorem	re1 15212	The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℜ‘1) = 1
Theorem	im1 15213	The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℑ‘1) = 0
Theorem	rei 15214	The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℜ‘i) = 0
Theorem	imi 15215	The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℑ‘i) = 1
Theorem	cj0 15216	The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (∗‘0) = 0
Theorem	cji 15217	The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
⊢ (∗‘i) = -i
Theorem	cjreim 15218	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 15219	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 15220	Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((∗‘𝐴) = (∗‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	cjne0 15221	A number is nonzero iff its complex conjugate is nonzero. (Contributed by NM, 29-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 ↔ (∗‘𝐴) ≠ 0))
Theorem	cjdiv 15222	Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵)))
Theorem	cnrecnv 15223*	The inverse to the canonical bijection from (ℝ × ℝ) to ℂ from cnref1o 13015. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    ⇒   ⊢ ◡𝐹 = (𝑧 ∈ ℂ ↦ ⟨(ℜ‘𝑧), (ℑ‘𝑧)⟩)
Theorem	sqeqd 15224	A deduction for showing two numbers whose squares are equal are themselves equal. (Contributed by Mario Carneiro, 3-Apr-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴↑2) = (𝐵↑2))    &   ⊢ (𝜑 → 0 ≤ (ℜ‘𝐴))    &   ⊢ (𝜑 → 0 ≤ (ℜ‘𝐵))    &   ⊢ ((𝜑 ∧ (ℜ‘𝐴) = 0 ∧ (ℜ‘𝐵) = 0) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	recli 15225	The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℜ‘𝐴) ∈ ℝ
Theorem	imcli 15226	The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℑ‘𝐴) ∈ ℝ
Theorem	cjcli 15227	Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (∗‘𝐴) ∈ ℂ
Theorem	replimi 15228	Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴)))
Theorem	cjcji 15229	The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (∗‘(∗‘𝐴)) = 𝐴
Theorem	reim0bi 15230	A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0)
Theorem	rerebi 15231	A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ∈ ℝ ↔ (ℜ‘𝐴) = 𝐴)
Theorem	cjrebi 15232	A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 11-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ∈ ℝ ↔ (∗‘𝐴) = 𝐴)
Theorem	recji 15233	Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴)
Theorem	imcji 15234	Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴)
Theorem	cjmulrcli 15235	A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · (∗‘𝐴)) ∈ ℝ
Theorem	cjmulvali 15236	A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))
Theorem	cjmulge0i 15237	A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ 0 ≤ (𝐴 · (∗‘𝐴))
Theorem	renegi 15238	Real part of negative. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℜ‘-𝐴) = -(ℜ‘𝐴)
Theorem	imnegi 15239	Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℑ‘-𝐴) = -(ℑ‘𝐴)
Theorem	cjnegi 15240	Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (∗‘-𝐴) = -(∗‘𝐴)
Theorem	addcji 15241	A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 + (∗‘𝐴)) = (2 · (ℜ‘𝐴))
Theorem	readdi 15242	Real part distributes over addition. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))
Theorem	imaddi 15243	Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))
Theorem	remuli 15244	Real part of a product. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵)))
Theorem	immuli 15245	Imaginary part of a product. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵)))
Theorem	cjaddi 15246	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵))
Theorem	cjmuli 15247	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵))
Theorem	ipcni 15248	Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵)))
Theorem	cjdivi 15249	Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 ≠ 0 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵)))
Theorem	crrei 15250	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴
Theorem	crimi 15251	The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵
Theorem	recld 15252	The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘𝐴) ∈ ℝ)
Theorem	imcld 15253	The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘𝐴) ∈ ℝ)
Theorem	cjcld 15254	Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ)
Theorem	replimd 15255	Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴))))
Theorem	remimd 15256	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 Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘𝐴) = ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))
Theorem	cjcjd 15257	The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘(∗‘𝐴)) = 𝐴)
Theorem	reim0bd 15258	A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (ℑ‘𝐴) = 0)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	rerebd 15259	A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (ℜ‘𝐴) = 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	cjrebd 15260	A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (∗‘𝐴) = 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	cjne0d 15261	A number is nonzero iff its complex conjugate is nonzero. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (∗‘𝐴) ≠ 0)
Theorem	recjd 15262	Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴))
Theorem	imcjd 15263	Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴))
Theorem	cjmulrcld 15264	A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℝ)
Theorem	cjmulvald 15265	A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
Theorem	cjmulge0d 15266	A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴 · (∗‘𝐴)))
Theorem	renegd 15267	Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘-𝐴) = -(ℜ‘𝐴))
Theorem	imnegd 15268	Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘-𝐴) = -(ℑ‘𝐴))
Theorem	cjnegd 15269	Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘-𝐴) = -(∗‘𝐴))
Theorem	addcjd 15270	A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 + (∗‘𝐴)) = (2 · (ℜ‘𝐴)))
Theorem	cjexpd 15271	Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁))
Theorem	readdd 15272	Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵)))
Theorem	imaddd 15273	Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵)))
Theorem	resubd 15274	Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 − 𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵)))
Theorem	imsubd 15275	Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 − 𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵)))
Theorem	remuld 15276	Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))))
Theorem	immuld 15277	Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))))
Theorem	cjaddd 15278	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵)))
Theorem	cjmuld 15279	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵)))
Theorem	ipcnd 15280	Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵))))
Theorem	cjdivd 15281	Complex conjugate distributes over division. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵)))
Theorem	rered 15282	A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℜ‘𝐴) = 𝐴)
Theorem	reim0d 15283	The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℑ‘𝐴) = 0)
Theorem	cjred 15284	A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (∗‘𝐴) = 𝐴)
Theorem	remul2d 15285	Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵)))
Theorem	immul2d 15286	Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (𝐴 · (ℑ‘𝐵)))
Theorem	redivd 15287	Real part of a division. Related to remul2 15188. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐵 / 𝐴)) = ((ℜ‘𝐵) / 𝐴))
Theorem	imdivd 15288	Imaginary part of a division. Related to remul2 15188. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐵 / 𝐴)) = ((ℑ‘𝐵) / 𝐴))
Theorem	crred 15289	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)
Theorem	crimd 15290	The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)
5.9.4  Square root; absolute value
Syntax	csqrt 15291	Extend class notation to include square root of a complex number.
class √
Syntax	cabs 15292	Extend class notation to include a function for the absolute value (modulus) of a complex number.
class abs
Definition	df-sqrt 15293*	Define a function whose value is the square root of a complex number. For example, (√‘25) = 5 (ex-sqrt 30816). Since (𝑦↑2) = 𝑥 iff (-𝑦↑2) = 𝑥, we ensure uniqueness by restricting the range to numbers with positive real part, or numbers with 0 real part and nonnegative imaginary part. A description can be found under "Principal square root of a complex number" at http://en.wikipedia.org/wiki/Square_root 30816. The square root symbol was introduced in 1525 by Christoff Rudolff. See sqrtcl 15420 for its closure, sqrtval 15295 for its value, sqrtth 15423 and sqsqrti 15434 for its relationship to squares, and sqrt11i 15443 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.)
⊢ √ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)))
Definition	df-abs 15294	Define the function for the absolute value (modulus) of a complex number. See abscli 15454 for its closure and absval 15296 or absval2i 15456 for its value. For example, (abs‘-2) = 2 (ex-abs 30817). (Contributed by NM, 27-Jul-1999.)
⊢ abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥))))
Theorem	sqrtval 15295*	Value of square root function. (Contributed by Mario Carneiro, 8-Jul-2013.)
⊢ (𝐴 ∈ ℂ → (√‘𝐴) = (℩𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)))
Theorem	absval 15296	The absolute value (modulus) of a complex number. Proposition 10-3.7(a) of [Gleason] p. 133. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) = (√‘(𝐴 · (∗‘𝐴))))
Theorem	rennim 15297	A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.)
⊢ (𝐴 ∈ ℝ → (i · 𝐴) ∉ ℝ+)
Theorem	cnpart 15298	The specification of restriction to the right half-plane partitions the complex plane without 0 into two disjoint pieces, which are related by a reflection about the origin (under the map 𝑥 ↦ -𝑥). (Contributed by Mario Carneiro, 8-Jul-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((0 ≤ (ℜ‘𝐴) ∧ (i · 𝐴) ∉ ℝ+) ↔ ¬ (0 ≤ (ℜ‘-𝐴) ∧ (i · -𝐴) ∉ ℝ+)))
Theorem	sqrt0 15299	The square root of zero is zero. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ (√‘0) = 0
Theorem	01sqrexlem1 15300*	Lemma for 01sqrex 15307. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ∀𝑦 ∈ 𝑆 𝑦 ≤ 1)