P. 109 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10801-10900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	shftval4g 10801	Value of a sequence shifted by -𝐴. (Contributed by Jim Kingdon, 19-Aug-2021.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift -𝐴)‘𝐵) = (𝐹‘(𝐴 + 𝐵)))
Theorem	seq3shft 10802*	Shifting the index set of a sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 17-Oct-2022.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 − 𝑁))) → (𝐹‘𝑥) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → seq𝑀( + , (𝐹 shift 𝑁)) = (seq(𝑀 − 𝑁)( + , 𝐹) shift 𝑁))
4.7.2  Real and imaginary parts; conjugate
Syntax	ccj 10803	Extend class notation to include complex conjugate function.
class ∗
Syntax	cre 10804	Extend class notation to include real part of a complex number.
class ℜ
Syntax	cim 10805	Extend class notation to include imaginary part of a complex number.
class ℑ
Definition	df-cj 10806*	Define the complex conjugate function. See cjcli 10877 for its closure and cjval 10809 for its value. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ ∗ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ)))
Definition	df-re 10807	Define a function whose value is the real part of a complex number. See reval 10813 for its value, recli 10875 for its closure, and replim 10823 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
⊢ ℜ = (𝑥 ∈ ℂ ↦ ((𝑥 + (∗‘𝑥)) / 2))
Definition	df-im 10808	Define a function whose value is the imaginary part of a complex number. See imval 10814 for its value, imcli 10876 for its closure, and replim 10823 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
⊢ ℑ = (𝑥 ∈ ℂ ↦ (ℜ‘(𝑥 / i)))
Theorem	cjval 10809*	The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (∗‘𝐴) = (℩𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ)))
Theorem	cjth 10810	The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → ((𝐴 + (∗‘𝐴)) ∈ ℝ ∧ (i · (𝐴 − (∗‘𝐴))) ∈ ℝ))
Theorem	cjf 10811	Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ ∗:ℂ⟶ℂ
Theorem	cjcl 10812	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 10813	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 10814	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 10815	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 10816	The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = (ℑ‘(i · 𝐴)))
Theorem	recl 10817	The real part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ)
Theorem	imcl 10818	The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ)
Theorem	ref 10819	Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ ℜ:ℂ⟶ℝ
Theorem	imf 10820	Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ ℑ:ℂ⟶ℝ
Theorem	crre 10821	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 10822	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 10823	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 10824	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 10825	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 10826	A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.)
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0))
Theorem	rereb 10827	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	mulreap 10828	A product with a real multiplier apart from zero is real iff the multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 # 0) → (𝐴 ∈ ℝ ↔ (𝐵 · 𝐴) ∈ ℝ))
Theorem	rere 10829	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 10830	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 10831	Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴))
Theorem	reneg 10832	Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) = -(ℜ‘𝐴))
Theorem	readd 10833	Real part distributes over addition. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵)))
Theorem	resub 10834	Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 − 𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵)))
Theorem	remullem 10835	Lemma for remul 10836, immul 10843, and cjmul 10849. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))) ∧ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))) ∧ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵))))
Theorem	remul 10836	Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))))
Theorem	remul2 10837	Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵)))
Theorem	redivap 10838	Real part of a division. Related to remul2 10837. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 # 0) → (ℜ‘(𝐴 / 𝐵)) = ((ℜ‘𝐴) / 𝐵))
Theorem	imcj 10839	Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴))
Theorem	imneg 10840	The imaginary part of a negative number. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (ℑ‘-𝐴) = -(ℑ‘𝐴))
Theorem	imadd 10841	Imaginary part distributes over addition. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵)))
Theorem	imsub 10842	Imaginary part distributes over subtraction. (Contributed by NM, 18-Mar-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 − 𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵)))
Theorem	immul 10843	Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))))
Theorem	immul2 10844	Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 · 𝐵)) = (𝐴 · (ℑ‘𝐵)))
Theorem	imdivap 10845	Imaginary part of a division. Related to immul2 10844. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 # 0) → (ℑ‘(𝐴 / 𝐵)) = ((ℑ‘𝐴) / 𝐵))
Theorem	cjre 10846	A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 8-Oct-1999.)
⊢ (𝐴 ∈ ℝ → (∗‘𝐴) = 𝐴)
Theorem	cjcj 10847	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 10848	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 10849	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 10850	Standard inner product on complex numbers. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵))))
Theorem	cjmulrcl 10851	A complex number times its conjugate is real. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) ∈ ℝ)
Theorem	cjmulval 10852	A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
Theorem	cjmulge0 10853	A complex number times its conjugate is nonnegative. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → 0 ≤ (𝐴 · (∗‘𝐴)))
Theorem	cjneg 10854	Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (∗‘-𝐴) = -(∗‘𝐴))
Theorem	addcj 10855	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 10856	Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∗‘(𝐴 − 𝐵)) = ((∗‘𝐴) − (∗‘𝐵)))
Theorem	cjexp 10857	Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁))
Theorem	imval2 10858	The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) = ((𝐴 − (∗‘𝐴)) / (2 · i)))
Theorem	re0 10859	The real part of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (ℜ‘0) = 0
Theorem	im0 10860	The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (ℑ‘0) = 0
Theorem	re1 10861	The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℜ‘1) = 1
Theorem	im1 10862	The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℑ‘1) = 0
Theorem	rei 10863	The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℜ‘i) = 0
Theorem	imi 10864	The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℑ‘i) = 1
Theorem	cj0 10865	The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (∗‘0) = 0
Theorem	cji 10866	The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
⊢ (∗‘i) = -i
Theorem	cjreim 10867	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 10868	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 10869	Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((∗‘𝐴) = (∗‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	cjap 10870	Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((∗‘𝐴) # (∗‘𝐵) ↔ 𝐴 # 𝐵))
Theorem	cjap0 10871	A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ (𝐴 ∈ ℂ → (𝐴 # 0 ↔ (∗‘𝐴) # 0))
Theorem	cjne0 10872	A number is nonzero iff its complex conjugate is nonzero. Also see cjap0 10871 which is similar but for apartness. (Contributed by NM, 29-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 ↔ (∗‘𝐴) ≠ 0))
Theorem	cjdivap 10873	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵)))
Theorem	cnrecnv 10874*	The inverse to the canonical bijection from (ℝ × ℝ) to ℂ from cnref1o 9609. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    ⇒   ⊢ ◡𝐹 = (𝑧 ∈ ℂ ↦ ⟨(ℜ‘𝑧), (ℑ‘𝑧)⟩)
Theorem	recli 10875	The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℜ‘𝐴) ∈ ℝ
Theorem	imcli 10876	The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℑ‘𝐴) ∈ ℝ
Theorem	cjcli 10877	Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (∗‘𝐴) ∈ ℂ
Theorem	replimi 10878	Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴)))
Theorem	cjcji 10879	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 10880	A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0)
Theorem	rerebi 10881	A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ∈ ℝ ↔ (ℜ‘𝐴) = 𝐴)
Theorem	cjrebi 10882	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 10883	Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴)
Theorem	imcji 10884	Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴)
Theorem	cjmulrcli 10885	A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · (∗‘𝐴)) ∈ ℝ
Theorem	cjmulvali 10886	A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))
Theorem	cjmulge0i 10887	A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ 0 ≤ (𝐴 · (∗‘𝐴))
Theorem	renegi 10888	Real part of negative. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℜ‘-𝐴) = -(ℜ‘𝐴)
Theorem	imnegi 10889	Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℑ‘-𝐴) = -(ℑ‘𝐴)
Theorem	cjnegi 10890	Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (∗‘-𝐴) = -(∗‘𝐴)
Theorem	addcji 10891	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 10892	Real part distributes over addition. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))
Theorem	imaddi 10893	Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))
Theorem	remuli 10894	Real part of a product. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵)))
Theorem	immuli 10895	Imaginary part of a product. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵)))
Theorem	cjaddi 10896	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵))
Theorem	cjmuli 10897	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵))
Theorem	ipcni 10898	Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵)))
Theorem	cjdivapi 10899	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵)))
Theorem	crrei 10900	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴