P. 91 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9001-9100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	expnegapd 9001	Value of a complex number raised to a negative power. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → (A↑-𝑁) = (1 / (A↑𝑁)))
Theorem	exprecapd 9002	Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → ((1 / A)↑𝑁) = (1 / (A↑𝑁)))
Theorem	expp1zapd 9003	Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → (A↑(𝑁 + 1)) = ((A↑𝑁) · A))
Theorem	expm1apd 9004	Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → (A↑(𝑁 − 1)) = ((A↑𝑁) / A))
Theorem	expsubapd 9005	Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    &   ⊢ (φ → 𝑀 ∈ ℤ)    ⇒   ⊢ (φ → (A↑(𝑀 − 𝑁)) = ((A↑𝑀) / (A↑𝑁)))
Theorem	sqmuld 9006	Distribution of square over multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → ((A · B)↑2) = ((A↑2) · (B↑2)))
Theorem	sqdivapd 9007	Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    &   ⊢ (φ → B # 0)    ⇒   ⊢ (φ → ((A / B)↑2) = ((A↑2) / (B↑2)))
Theorem	expdivapd 9008	Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    &   ⊢ (φ → B # 0)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → ((A / B)↑𝑁) = ((A↑𝑁) / (B↑𝑁)))
Theorem	mulexpd 9009	Positive integer exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → ((A · B)↑𝑁) = ((A↑𝑁) · (B↑𝑁)))
Theorem	0expd 9010	Value of zero raised to a positive integer power. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → 𝑁 ∈ ℕ)    ⇒   ⊢ (φ → (0↑𝑁) = 0)
Theorem	reexpcld 9011	Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℝ)
Theorem	expge0d 9012	Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    &   ⊢ (φ → 0 ≤ A)    ⇒   ⊢ (φ → 0 ≤ (A↑𝑁))
Theorem	expge1d 9013	Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    &   ⊢ (φ → 1 ≤ A)    ⇒   ⊢ (φ → 1 ≤ (A↑𝑁))
Theorem	nnsqcld 9014	The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℕ)    ⇒   ⊢ (φ → (A↑2) ∈ ℕ)
Theorem	nnexpcld 9015	Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℕ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℕ)
Theorem	nn0expcld 9016	Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℕ0)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℕ0)
Theorem	rpexpcld 9017	Closure law for exponentiation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℝ+)
Theorem	reexpclzapd 9018	Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℝ)
Theorem	resqcld 9019	Closure of square in reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → (A↑2) ∈ ℝ)
Theorem	sqge0d 9020	A square of a real is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → 0 ≤ (A↑2))
Theorem	sqgt0apd 9021	The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → A # 0)    ⇒   ⊢ (φ → 0 < (A↑2))
Theorem	leexp2ad 9022	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 1 ≤ A)    &   ⊢ (φ → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (φ → (A↑𝑀) ≤ (A↑𝑁))
Theorem	leexp2rd 9023	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 𝑀 ∈ ℕ0)    &   ⊢ (φ → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (φ → 0 ≤ A)    &   ⊢ (φ → A ≤ 1)    ⇒   ⊢ (φ → (A↑𝑁) ≤ (A↑𝑀))
Theorem	lt2sqd 9024	The square function on nonnegative reals is strictly monotonic. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 0 ≤ A)    &   ⊢ (φ → 0 ≤ B)    ⇒   ⊢ (φ → (A < B ↔ (A↑2) < (B↑2)))
Theorem	le2sqd 9025	The square function on nonnegative reals is monotonic. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 0 ≤ A)    &   ⊢ (φ → 0 ≤ B)    ⇒   ⊢ (φ → (A ≤ B ↔ (A↑2) ≤ (B↑2)))
Theorem	sq11d 9026	The square function is one-to-one for nonnegative reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 0 ≤ A)    &   ⊢ (φ → 0 ≤ B)    &   ⊢ (φ → (A↑2) = (B↑2))    ⇒   ⊢ (φ → A = B)
3.6  Elementary real and complex functions
3.6.1  Real and imaginary parts; conjugate
Syntax	ccj 9027	Extend class notation to include complex conjugate function.
class ∗
Syntax	cre 9028	Extend class notation to include real part of a complex number.
class ℜ
Syntax	cim 9029	Extend class notation to include imaginary part of a complex number.
class ℑ
Definition	df-cj 9030*	Define the complex conjugate function. See cjcli 9101 for its closure and cjval 9033 for its value. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ ∗ = (x ∈ ℂ ↦ (℩y ∈ ℂ ((x + y) ∈ ℝ ∧ (i · (x − y)) ∈ ℝ)))
Definition	df-re 9031	Define a function whose value is the real part of a complex number. See reval 9037 for its value, recli 9099 for its closure, and replim 9047 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
⊢ ℜ = (x ∈ ℂ ↦ ((x + (∗‘x)) / 2))
Definition	df-im 9032	Define a function whose value is the imaginary part of a complex number. See imval 9038 for its value, imcli 9100 for its closure, and replim 9047 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
⊢ ℑ = (x ∈ ℂ ↦ (ℜ‘(x / i)))
Theorem	cjval 9033*	The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ (A ∈ ℂ → (∗‘A) = (℩x ∈ ℂ ((A + x) ∈ ℝ ∧ (i · (A − x)) ∈ ℝ)))
Theorem	cjth 9034	The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ (A ∈ ℂ → ((A + (∗‘A)) ∈ ℝ ∧ (i · (A − (∗‘A))) ∈ ℝ))
Theorem	cjf 9035	Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ ∗:ℂ⟶ℂ
Theorem	cjcl 9036	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.)
⊢ (A ∈ ℂ → (∗‘A) ∈ ℂ)
Theorem	reval 9037	The value of the real part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ (A ∈ ℂ → (ℜ‘A) = ((A + (∗‘A)) / 2))
Theorem	imval 9038	The value of the imaginary part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ (A ∈ ℂ → (ℑ‘A) = (ℜ‘(A / i)))
Theorem	imre 9039	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.)
⊢ (A ∈ ℂ → (ℑ‘A) = (ℜ‘(-i · A)))
Theorem	reim 9040	The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (A ∈ ℂ → (ℜ‘A) = (ℑ‘(i · A)))
Theorem	recl 9041	The real part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ (A ∈ ℂ → (ℜ‘A) ∈ ℝ)
Theorem	imcl 9042	The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ (A ∈ ℂ → (ℑ‘A) ∈ ℝ)
Theorem	ref 9043	Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ ℜ:ℂ⟶ℝ
Theorem	imf 9044	Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ ℑ:ℂ⟶ℝ
Theorem	crre 9045	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.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (ℜ‘(A + (i · B))) = A)
Theorem	crim 9046	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.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (ℑ‘(A + (i · B))) = B)
Theorem	replim 9047	Reconstruct a complex number from its real and imaginary parts. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)
⊢ (A ∈ ℂ → A = ((ℜ‘A) + (i · (ℑ‘A))))
Theorem	remim 9048	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.)
⊢ (A ∈ ℂ → (∗‘A) = ((ℜ‘A) − (i · (ℑ‘A))))
Theorem	reim0 9049	The imaginary part of a real number is 0. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
⊢ (A ∈ ℝ → (ℑ‘A) = 0)
Theorem	reim0b 9050	A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.)
⊢ (A ∈ ℂ → (A ∈ ℝ ↔ (ℑ‘A) = 0))
Theorem	rereb 9051	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.)
⊢ (A ∈ ℂ → (A ∈ ℝ ↔ (ℜ‘A) = A))
Theorem	mulreap 9052	A product with a real multiplier apart from zero is real iff the multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((A ∈ ℂ ∧ B ∈ ℝ ∧ B # 0) → (A ∈ ℝ ↔ (B · A) ∈ ℝ))
Theorem	rere 9053	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.)
⊢ (A ∈ ℝ → (ℜ‘A) = A)
Theorem	cjreb 9054	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.)
⊢ (A ∈ ℂ → (A ∈ ℝ ↔ (∗‘A) = A))
Theorem	recj 9055	Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (A ∈ ℂ → (ℜ‘(∗‘A)) = (ℜ‘A))
Theorem	reneg 9056	Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (A ∈ ℂ → (ℜ‘-A) = -(ℜ‘A))
Theorem	readd 9057	Real part distributes over addition. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (ℜ‘(A + B)) = ((ℜ‘A) + (ℜ‘B)))
Theorem	resub 9058	Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (ℜ‘(A − B)) = ((ℜ‘A) − (ℜ‘B)))
Theorem	remullem 9059	Lemma for remul 9060, immul 9067, and cjmul 9073. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((ℜ‘(A · B)) = (((ℜ‘A) · (ℜ‘B)) − ((ℑ‘A) · (ℑ‘B))) ∧ (ℑ‘(A · B)) = (((ℜ‘A) · (ℑ‘B)) + ((ℑ‘A) · (ℜ‘B))) ∧ (∗‘(A · B)) = ((∗‘A) · (∗‘B))))
Theorem	remul 9060	Real 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	remul2 9061	Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((A ∈ ℝ ∧ B ∈ ℂ) → (ℜ‘(A · B)) = (A · (ℜ‘B)))
Theorem	redivap 9062	Real part of a division. Related to remul2 9061. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((A ∈ ℂ ∧ B ∈ ℝ ∧ B # 0) → (ℜ‘(A / B)) = ((ℜ‘A) / B))
Theorem	imcj 9063	Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (A ∈ ℂ → (ℑ‘(∗‘A)) = -(ℑ‘A))
Theorem	imneg 9064	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 9065	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 9066	Imaginary part distributes over subtraction. (Contributed by NM, 18-Mar-2005.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (ℑ‘(A − B)) = ((ℑ‘A) − (ℑ‘B)))
Theorem	immul 9067	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 9068	Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((A ∈ ℝ ∧ B ∈ ℂ) → (ℑ‘(A · B)) = (A · (ℑ‘B)))
Theorem	imdivap 9069	Imaginary part of a division. Related to immul2 9068. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((A ∈ ℂ ∧ B ∈ ℝ ∧ B # 0) → (ℑ‘(A / B)) = ((ℑ‘A) / B))
Theorem	cjre 9070	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 9071	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 9072	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 9073	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 9074	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 9075	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 9076	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 9077	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 9078	Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (A ∈ ℂ → (∗‘-A) = -(∗‘A))
Theorem	addcj 9079	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 9080	Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (∗‘(A − B)) = ((∗‘A) − (∗‘B)))
Theorem	cjexp 9081	Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.)
⊢ ((A ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (∗‘(A↑𝑁)) = ((∗‘A)↑𝑁))
Theorem	imval2 9082	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 9083	The real part of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (ℜ‘0) = 0
Theorem	im0 9084	The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (ℑ‘0) = 0
Theorem	re1 9085	The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℜ‘1) = 1
Theorem	im1 9086	The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℑ‘1) = 0
Theorem	rei 9087	The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℜ‘i) = 0
Theorem	imi 9088	The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℑ‘i) = 1
Theorem	cj0 9089	The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (∗‘0) = 0
Theorem	cji 9090	The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
⊢ (∗‘i) = -i
Theorem	cjreim 9091	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 9092	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 9093	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 9094	Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((∗‘A) # (∗‘B) ↔ A # B))
Theorem	cjap0 9095	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 9096	A number is nonzero iff its complex conjugate is nonzero. (Contributed by NM, 29-Apr-2005.)
⊢ (A ∈ ℂ → (A ≠ 0 ↔ (∗‘A) ≠ 0))
Theorem	cjdivap 9097	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ B # 0) → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))
Theorem	cnrecnv 9098*	The inverse to the canonical bijection from (ℝ × ℝ) to ℂ from cnref1o 8317. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐹 = (x ∈ ℝ, y ∈ ℝ ↦ (x + (i · y)))    ⇒   ⊢ ◡𝐹 = (z ∈ ℂ ↦ ⟨(ℜ‘z), (ℑ‘z)⟩)
Theorem	recli 9099	The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (ℜ‘A) ∈ ℝ
Theorem	imcli 9100	The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (ℑ‘A) ∈ ℝ