P. 92 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9101-9200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	remul2 9101	Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((A ∈ ℝ ∧ B ∈ ℂ) → (ℜ‘(A · B)) = (A · (ℜ‘B)))
Theorem	redivap 9102	Real part of a division. Related to remul2 9101. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((A ∈ ℂ ∧ B ∈ ℝ ∧ B # 0) → (ℜ‘(A / B)) = ((ℜ‘A) / B))
Theorem	imcj 9103	Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (A ∈ ℂ → (ℑ‘(∗‘A)) = -(ℑ‘A))
Theorem	imneg 9104	The imaginary part of a negative number. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (A ∈ ℂ → (ℑ‘-A) = -(ℑ‘A))
Theorem	imadd 9105	Imaginary part distributes over addition. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (ℑ‘(A + B)) = ((ℑ‘A) + (ℑ‘B)))
Theorem	imsub 9106	Imaginary part distributes over subtraction. (Contributed by NM, 18-Mar-2005.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (ℑ‘(A − B)) = ((ℑ‘A) − (ℑ‘B)))
Theorem	immul 9107	Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (ℑ‘(A · B)) = (((ℜ‘A) · (ℑ‘B)) + ((ℑ‘A) · (ℜ‘B))))
Theorem	immul2 9108	Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((A ∈ ℝ ∧ B ∈ ℂ) → (ℑ‘(A · B)) = (A · (ℑ‘B)))
Theorem	imdivap 9109	Imaginary part of a division. Related to immul2 9108. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((A ∈ ℂ ∧ B ∈ ℝ ∧ B # 0) → (ℑ‘(A / B)) = ((ℑ‘A) / B))
Theorem	cjre 9110	A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 8-Oct-1999.)
⊢ (A ∈ ℝ → (∗‘A) = A)
Theorem	cjcj 9111	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.)
⊢ (A ∈ ℂ → (∗‘(∗‘A)) = A)
Theorem	cjadd 9112	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.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (∗‘(A + B)) = ((∗‘A) + (∗‘B)))
Theorem	cjmul 9113	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.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (∗‘(A · B)) = ((∗‘A) · (∗‘B)))
Theorem	ipcnval 9114	Standard inner product on complex numbers. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (ℜ‘(A · (∗‘B))) = (((ℜ‘A) · (ℜ‘B)) + ((ℑ‘A) · (ℑ‘B))))
Theorem	cjmulrcl 9115	A complex number times its conjugate is real. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (A ∈ ℂ → (A · (∗‘A)) ∈ ℝ)
Theorem	cjmulval 9116	A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (A ∈ ℂ → (A · (∗‘A)) = (((ℜ‘A)↑2) + ((ℑ‘A)↑2)))
Theorem	cjmulge0 9117	A complex number times its conjugate is nonnegative. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (A ∈ ℂ → 0 ≤ (A · (∗‘A)))
Theorem	cjneg 9118	Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (A ∈ ℂ → (∗‘-A) = -(∗‘A))
Theorem	addcj 9119	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.)
⊢ (A ∈ ℂ → (A + (∗‘A)) = (2 · (ℜ‘A)))
Theorem	cjsub 9120	Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (∗‘(A − B)) = ((∗‘A) − (∗‘B)))
Theorem	cjexp 9121	Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.)
⊢ ((A ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (∗‘(A↑𝑁)) = ((∗‘A)↑𝑁))
Theorem	imval2 9122	The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.)
⊢ (A ∈ ℂ → (ℑ‘A) = ((A − (∗‘A)) / (2 · i)))
Theorem	re0 9123	The real part of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (ℜ‘0) = 0
Theorem	im0 9124	The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (ℑ‘0) = 0
Theorem	re1 9125	The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℜ‘1) = 1
Theorem	im1 9126	The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℑ‘1) = 0
Theorem	rei 9127	The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℜ‘i) = 0
Theorem	imi 9128	The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℑ‘i) = 1
Theorem	cj0 9129	The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (∗‘0) = 0
Theorem	cji 9130	The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
⊢ (∗‘i) = -i
Theorem	cjreim 9131	The conjugate of a representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (∗‘(A + (i · B))) = (A − (i · B)))
Theorem	cjreim2 9132	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.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (∗‘(A − (i · B))) = (A + (i · B)))
Theorem	cj11 9133	Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((∗‘A) = (∗‘B) ↔ A = B))
Theorem	cjap 9134	Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((∗‘A) # (∗‘B) ↔ A # B))
Theorem	cjap0 9135	A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ (A ∈ ℂ → (A # 0 ↔ (∗‘A) # 0))
Theorem	cjne0 9136	A number is nonzero iff its complex conjugate is nonzero. (Contributed by NM, 29-Apr-2005.)
⊢ (A ∈ ℂ → (A ≠ 0 ↔ (∗‘A) ≠ 0))
Theorem	cjdivap 9137	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ B # 0) → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))
Theorem	cnrecnv 9138*	The inverse to the canonical bijection from (ℝ × ℝ) to ℂ from cnref1o 8357. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐹 = (x ∈ ℝ, y ∈ ℝ ↦ (x + (i · y)))    ⇒   ⊢ ◡𝐹 = (z ∈ ℂ ↦ ⟨(ℜ‘z), (ℑ‘z)⟩)
Theorem	recli 9139	The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (ℜ‘A) ∈ ℝ
Theorem	imcli 9140	The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (ℑ‘A) ∈ ℝ
Theorem	cjcli 9141	Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (∗‘A) ∈ ℂ
Theorem	replimi 9142	Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ A = ((ℜ‘A) + (i · (ℑ‘A)))
Theorem	cjcji 9143	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.)
⊢ A ∈ ℂ    ⇒   ⊢ (∗‘(∗‘A)) = A
Theorem	reim0bi 9144	A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (A ∈ ℝ ↔ (ℑ‘A) = 0)
Theorem	rerebi 9145	A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (A ∈ ℝ ↔ (ℜ‘A) = A)
Theorem	cjrebi 9146	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.)
⊢ A ∈ ℂ    ⇒   ⊢ (A ∈ ℝ ↔ (∗‘A) = A)
Theorem	recji 9147	Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (ℜ‘(∗‘A)) = (ℜ‘A)
Theorem	imcji 9148	Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (ℑ‘(∗‘A)) = -(ℑ‘A)
Theorem	cjmulrcli 9149	A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (A · (∗‘A)) ∈ ℝ
Theorem	cjmulvali 9150	A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (A · (∗‘A)) = (((ℜ‘A)↑2) + ((ℑ‘A)↑2))
Theorem	cjmulge0i 9151	A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ 0 ≤ (A · (∗‘A))
Theorem	renegi 9152	Real part of negative. (Contributed by NM, 2-Aug-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (ℜ‘-A) = -(ℜ‘A)
Theorem	imnegi 9153	Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (ℑ‘-A) = -(ℑ‘A)
Theorem	cjnegi 9154	Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (∗‘-A) = -(∗‘A)
Theorem	addcji 9155	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.)
⊢ A ∈ ℂ    ⇒   ⊢ (A + (∗‘A)) = (2 · (ℜ‘A))
Theorem	readdi 9156	Real part distributes over addition. (Contributed by NM, 28-Jul-1999.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℜ‘(A + B)) = ((ℜ‘A) + (ℜ‘B))
Theorem	imaddi 9157	Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℑ‘(A + B)) = ((ℑ‘A) + (ℑ‘B))
Theorem	remuli 9158	Real part of a product. (Contributed by NM, 28-Jul-1999.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℜ‘(A · B)) = (((ℜ‘A) · (ℜ‘B)) − ((ℑ‘A) · (ℑ‘B)))
Theorem	immuli 9159	Imaginary part of a product. (Contributed by NM, 28-Jul-1999.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℑ‘(A · B)) = (((ℜ‘A) · (ℑ‘B)) + ((ℑ‘A) · (ℜ‘B)))
Theorem	cjaddi 9160	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (∗‘(A + B)) = ((∗‘A) + (∗‘B))
Theorem	cjmuli 9161	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (∗‘(A · B)) = ((∗‘A) · (∗‘B))
Theorem	ipcni 9162	Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℜ‘(A · (∗‘B))) = (((ℜ‘A) · (ℜ‘B)) + ((ℑ‘A) · (ℑ‘B)))
Theorem	cjdivapi 9163	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (B # 0 → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))
Theorem	crrei 9164	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (ℜ‘(A + (i · B))) = A
Theorem	crimi 9165	The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (ℑ‘(A + (i · B))) = B
Theorem	recld 9166	The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘A) ∈ ℝ)
Theorem	imcld 9167	The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘A) ∈ ℝ)
Theorem	cjcld 9168	Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (∗‘A) ∈ ℂ)
Theorem	replimd 9169	Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → A = ((ℜ‘A) + (i · (ℑ‘A))))
Theorem	remimd 9170	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.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (∗‘A) = ((ℜ‘A) − (i · (ℑ‘A))))
Theorem	cjcjd 9171	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.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (∗‘(∗‘A)) = A)
Theorem	reim0bd 9172	A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → (ℑ‘A) = 0)    ⇒   ⊢ (φ → A ∈ ℝ)
Theorem	rerebd 9173	A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → (ℜ‘A) = A)    ⇒   ⊢ (φ → A ∈ ℝ)
Theorem	cjrebd 9174	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.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → (∗‘A) = A)    ⇒   ⊢ (φ → A ∈ ℝ)
Theorem	cjne0d 9175	A number is nonzero iff its complex conjugate is nonzero. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A ≠ 0)    ⇒   ⊢ (φ → (∗‘A) ≠ 0)
Theorem	recjd 9176	Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(∗‘A)) = (ℜ‘A))
Theorem	imcjd 9177	Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘(∗‘A)) = -(ℑ‘A))
Theorem	cjmulrcld 9178	A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A · (∗‘A)) ∈ ℝ)
Theorem	cjmulvald 9179	A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A · (∗‘A)) = (((ℜ‘A)↑2) + ((ℑ‘A)↑2)))
Theorem	cjmulge0d 9180	A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → 0 ≤ (A · (∗‘A)))
Theorem	renegd 9181	Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘-A) = -(ℜ‘A))
Theorem	imnegd 9182	Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘-A) = -(ℑ‘A))
Theorem	cjnegd 9183	Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (∗‘-A) = -(∗‘A))
Theorem	addcjd 9184	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.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A + (∗‘A)) = (2 · (ℜ‘A)))
Theorem	cjexpd 9185	Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → (∗‘(A↑𝑁)) = ((∗‘A)↑𝑁))
Theorem	readdd 9186	Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(A + B)) = ((ℜ‘A) + (ℜ‘B)))
Theorem	imaddd 9187	Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘(A + B)) = ((ℑ‘A) + (ℑ‘B)))
Theorem	resubd 9188	Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(A − B)) = ((ℜ‘A) − (ℜ‘B)))
Theorem	imsubd 9189	Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘(A − B)) = ((ℑ‘A) − (ℑ‘B)))
Theorem	remuld 9190	Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(A · B)) = (((ℜ‘A) · (ℜ‘B)) − ((ℑ‘A) · (ℑ‘B))))
Theorem	immuld 9191	Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘(A · B)) = (((ℜ‘A) · (ℑ‘B)) + ((ℑ‘A) · (ℜ‘B))))
Theorem	cjaddd 9192	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (∗‘(A + B)) = ((∗‘A) + (∗‘B)))
Theorem	cjmuld 9193	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (∗‘(A · B)) = ((∗‘A) · (∗‘B)))
Theorem	ipcnd 9194	Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(A · (∗‘B))) = (((ℜ‘A) · (ℜ‘B)) + ((ℑ‘A) · (ℑ‘B))))
Theorem	cjdivapd 9195	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    &   ⊢ (φ → B # 0)    ⇒   ⊢ (φ → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))
Theorem	rered 9196	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.)
⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → (ℜ‘A) = A)
Theorem	reim0d 9197	The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → (ℑ‘A) = 0)
Theorem	cjred 9198	A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → (∗‘A) = A)
Theorem	remul2d 9199	Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(A · B)) = (A · (ℜ‘B)))
Theorem	immul2d 9200	Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘(A · B)) = (A · (ℑ‘B)))