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
Theorem	cjexp 15101	Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁))
Theorem	imval2 15102	The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) = ((𝐴 − (∗‘𝐴)) / (2 · i)))
Theorem	re0 15103	The real part of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (ℜ‘0) = 0
Theorem	im0 15104	The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (ℑ‘0) = 0
Theorem	re1 15105	The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℜ‘1) = 1
Theorem	im1 15106	The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℑ‘1) = 0
Theorem	rei 15107	The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℜ‘i) = 0
Theorem	imi 15108	The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℑ‘i) = 1
Theorem	cj0 15109	The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (∗‘0) = 0
Theorem	cji 15110	The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
⊢ (∗‘i) = -i
Theorem	cjreim 15111	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 15112	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 15113	Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((∗‘𝐴) = (∗‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	cjne0 15114	A number is nonzero iff its complex conjugate is nonzero. (Contributed by NM, 29-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 ↔ (∗‘𝐴) ≠ 0))
Theorem	cjdiv 15115	Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵)))
Theorem	cnrecnv 15116*	The inverse to the canonical bijection from (ℝ × ℝ) to ℂ from cnref1o 12924. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    ⇒   ⊢ ◡𝐹 = (𝑧 ∈ ℂ ↦ ⟨(ℜ‘𝑧), (ℑ‘𝑧)⟩)
Theorem	sqeqd 15117	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 15118	The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℜ‘𝐴) ∈ ℝ
Theorem	imcli 15119	The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℑ‘𝐴) ∈ ℝ
Theorem	cjcli 15120	Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (∗‘𝐴) ∈ ℂ
Theorem	replimi 15121	Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴)))
Theorem	cjcji 15122	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 15123	A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0)
Theorem	rerebi 15124	A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ∈ ℝ ↔ (ℜ‘𝐴) = 𝐴)
Theorem	cjrebi 15125	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 15126	Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴)
Theorem	imcji 15127	Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴)
Theorem	cjmulrcli 15128	A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · (∗‘𝐴)) ∈ ℝ
Theorem	cjmulvali 15129	A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))
Theorem	cjmulge0i 15130	A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ 0 ≤ (𝐴 · (∗‘𝐴))
Theorem	renegi 15131	Real part of negative. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℜ‘-𝐴) = -(ℜ‘𝐴)
Theorem	imnegi 15132	Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℑ‘-𝐴) = -(ℑ‘𝐴)
Theorem	cjnegi 15133	Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (∗‘-𝐴) = -(∗‘𝐴)
Theorem	addcji 15134	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 15135	Real part distributes over addition. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))
Theorem	imaddi 15136	Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))
Theorem	remuli 15137	Real part of a product. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵)))
Theorem	immuli 15138	Imaginary part of a product. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵)))
Theorem	cjaddi 15139	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵))
Theorem	cjmuli 15140	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵))
Theorem	ipcni 15141	Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵)))
Theorem	cjdivi 15142	Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 ≠ 0 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵)))
Theorem	crrei 15143	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 15144	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 15145	The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘𝐴) ∈ ℝ)
Theorem	imcld 15146	The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘𝐴) ∈ ℝ)
Theorem	cjcld 15147	Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ)
Theorem	replimd 15148	Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴))))
Theorem	remimd 15149	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 15150	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 15151	A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (ℑ‘𝐴) = 0)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	rerebd 15152	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 15153	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 15154	A number is nonzero iff its complex conjugate is nonzero. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (∗‘𝐴) ≠ 0)
Theorem	recjd 15155	Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴))
Theorem	imcjd 15156	Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴))
Theorem	cjmulrcld 15157	A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℝ)
Theorem	cjmulvald 15158	A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
Theorem	cjmulge0d 15159	A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴 · (∗‘𝐴)))
Theorem	renegd 15160	Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘-𝐴) = -(ℜ‘𝐴))
Theorem	imnegd 15161	Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘-𝐴) = -(ℑ‘𝐴))
Theorem	cjnegd 15162	Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘-𝐴) = -(∗‘𝐴))
Theorem	addcjd 15163	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 15164	Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁))
Theorem	readdd 15165	Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵)))
Theorem	imaddd 15166	Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵)))
Theorem	resubd 15167	Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 − 𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵)))
Theorem	imsubd 15168	Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 − 𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵)))
Theorem	remuld 15169	Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))))
Theorem	immuld 15170	Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))))
Theorem	cjaddd 15171	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵)))
Theorem	cjmuld 15172	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵)))
Theorem	ipcnd 15173	Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵))))
Theorem	cjdivd 15174	Complex conjugate distributes over division. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵)))
Theorem	rered 15175	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 15176	The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℑ‘𝐴) = 0)
Theorem	cjred 15177	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 15178	Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵)))
Theorem	immul2d 15179	Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (𝐴 · (ℑ‘𝐵)))
Theorem	redivd 15180	Real part of a division. Related to remul2 15081. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐵 / 𝐴)) = ((ℜ‘𝐵) / 𝐴))
Theorem	imdivd 15181	Imaginary part of a division. Related to remul2 15081. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐵 / 𝐴)) = ((ℑ‘𝐵) / 𝐴))
Theorem	crred 15182	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 15183	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 15184	Extend class notation to include square root of a complex number.
class √
Syntax	cabs 15185	Extend class notation to include a function for the absolute value (modulus) of a complex number.
class abs
Definition	df-sqrt 15186*	Define a function whose value is the square root of a complex number. For example, (√‘25) = 5 (ex-sqrt 30544). 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 30544. The square root symbol was introduced in 1525 by Christoff Rudolff. See sqrtcl 15313 for its closure, sqrtval 15188 for its value, sqrtth 15316 and sqsqrti 15327 for its relationship to squares, and sqrt11i 15336 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.)
⊢ √ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)))
Definition	df-abs 15187	Define the function for the absolute value (modulus) of a complex number. See abscli 15347 for its closure and absval 15189 or absval2i 15349 for its value. For example, (abs‘-2) = 2 (ex-abs 30545). (Contributed by NM, 27-Jul-1999.)
⊢ abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥))))
Theorem	sqrtval 15188*	Value of square root function. (Contributed by Mario Carneiro, 8-Jul-2013.)
⊢ (𝐴 ∈ ℂ → (√‘𝐴) = (℩𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)))
Theorem	absval 15189	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 15190	A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.)
⊢ (𝐴 ∈ ℝ → (i · 𝐴) ∉ ℝ+)
Theorem	cnpart 15191	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 15192	The square root of zero is zero. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ (√‘0) = 0
Theorem	01sqrexlem1 15193*	Lemma for 01sqrex 15200. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ∀𝑦 ∈ 𝑆 𝑦 ≤ 1)
Theorem	01sqrexlem2 15194*	Lemma for 01sqrex 15200. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → 𝐴 ∈ 𝑆)
Theorem	01sqrexlem3 15195*	Lemma for 01sqrex 15200. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧))
Theorem	01sqrexlem4 15196*	Lemma for 01sqrex 15200. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵 ∈ ℝ+ ∧ 𝐵 ≤ 1))
Theorem	01sqrexlem5 15197*	Lemma for 01sqrex 15200. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    &   ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)}    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑣 ∈ ℝ ∀𝑢 ∈ 𝑇 𝑢 ≤ 𝑣) ∧ (𝐵↑2) = sup(𝑇, ℝ, < )))
Theorem	01sqrexlem6 15198*	Lemma for 01sqrex 15200. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    &   ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)}    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵↑2) ≤ 𝐴)
Theorem	01sqrexlem7 15199*	Lemma for 01sqrex 15200. (Contributed by Mario Carneiro, 10-Jul-2013.) (Proof shortened by AV, 9-Jul-2022.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    &   ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)}    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵↑2) = 𝐴)
Theorem	01sqrex 15200*	Existence of a square root for reals in the interval (0, 1]. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ∃𝑥 ∈ ℝ+ (𝑥 ≤ 1 ∧ (𝑥↑2) = 𝐴))