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	nnesq 9001	A positive integer is even iff its square is even. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ↔ ((𝑁↑2) / 2) ∈ ℕ))
Theorem	bernneq 9002	Bernoulli's inequality, due to Johan Bernoulli (1667-1748). (Contributed by NM, 21-Feb-2005.)
⊢ ((A ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ -1 ≤ A) → (1 + (A · 𝑁)) ≤ ((1 + A)↑𝑁))
Theorem	bernneq2 9003	Variation of Bernoulli's inequality bernneq 9002. (Contributed by NM, 18-Oct-2007.)
⊢ ((A ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ A) → (((A − 1) · 𝑁) + 1) ≤ (A↑𝑁))
Theorem	bernneq3 9004	A corollary of bernneq 9002. (Contributed by Mario Carneiro, 11-Mar-2014.)
⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → 𝑁 < (𝑃↑𝑁))
Theorem	expnbnd 9005*	Exponentiation with a mantissa greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < B) → ∃𝑘 ∈ ℕ A < (B↑𝑘))
Theorem	expnlbnd 9006*	The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound. (Contributed by NM, 18-Jul-2008.)
⊢ ((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 < B) → ∃𝑘 ∈ ℕ (1 / (B↑𝑘)) < A)
Theorem	expnlbnd2 9007*	The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound. (Contributed by NM, 18-Jul-2008.) (Proof shortened by Mario Carneiro, 5-Jun-2014.)
⊢ ((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 < B) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(1 / (B↑𝑘)) < A)
Theorem	exp0d 9008	Value of a complex number raised to the 0th power. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A↑0) = 1)
Theorem	exp1d 9009	Value of a complex number raised to the first power. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A↑1) = A)
Theorem	expeq0d 9010	Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → 𝑁 ∈ ℕ)    &   ⊢ (φ → (A↑𝑁) = 0)    ⇒   ⊢ (φ → A = 0)
Theorem	sqvald 9011	Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A↑2) = (A · A))
Theorem	sqcld 9012	Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A↑2) ∈ ℂ)
Theorem	sqeq0d 9013	A number is zero iff its square is zero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → (A↑2) = 0)    ⇒   ⊢ (φ → A = 0)
Theorem	expcld 9014	Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℂ)
Theorem	expp1d 9015	Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑(𝑁 + 1)) = ((A↑𝑁) · A))
Theorem	expaddd 9016	Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    &   ⊢ (φ → 𝑀 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑(𝑀 + 𝑁)) = ((A↑𝑀) · (A↑𝑁)))
Theorem	expmuld 9017	Product of exponents law for positive integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    &   ⊢ (φ → 𝑀 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑(𝑀 · 𝑁)) = ((A↑𝑀)↑𝑁))
Theorem	sqrecapd 9018	Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    ⇒   ⊢ (φ → ((1 / A)↑2) = (1 / (A↑2)))
Theorem	expclzapd 9019	Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℂ)
Theorem	expap0d 9020	Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → (A↑𝑁) # 0)
Theorem	expnegapd 9021	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 9022	Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → ((1 / A)↑𝑁) = (1 / (A↑𝑁)))
Theorem	expp1zapd 9023	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 9024	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 9025	Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    &   ⊢ (φ → 𝑀 ∈ ℤ)    ⇒   ⊢ (φ → (A↑(𝑀 − 𝑁)) = ((A↑𝑀) / (A↑𝑁)))
Theorem	sqmuld 9026	Distribution of square over multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → ((A · B)↑2) = ((A↑2) · (B↑2)))
Theorem	sqdivapd 9027	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 9028	Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    &   ⊢ (φ → B # 0)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → ((A / B)↑𝑁) = ((A↑𝑁) / (B↑𝑁)))
Theorem	mulexpd 9029	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 9030	Value of zero raised to a positive integer power. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → 𝑁 ∈ ℕ)    ⇒   ⊢ (φ → (0↑𝑁) = 0)
Theorem	reexpcld 9031	Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℝ)
Theorem	expge0d 9032	Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    &   ⊢ (φ → 0 ≤ A)    ⇒   ⊢ (φ → 0 ≤ (A↑𝑁))
Theorem	expge1d 9033	Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    &   ⊢ (φ → 1 ≤ A)    ⇒   ⊢ (φ → 1 ≤ (A↑𝑁))
Theorem	nnsqcld 9034	The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℕ)    ⇒   ⊢ (φ → (A↑2) ∈ ℕ)
Theorem	nnexpcld 9035	Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℕ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℕ)
Theorem	nn0expcld 9036	Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℕ0)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℕ0)
Theorem	rpexpcld 9037	Closure law for exponentiation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℝ+)
Theorem	reexpclzapd 9038	Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℝ)
Theorem	resqcld 9039	Closure of square in reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → (A↑2) ∈ ℝ)
Theorem	sqge0d 9040	A square of a real is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → 0 ≤ (A↑2))
Theorem	sqgt0apd 9041	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 9042	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 1 ≤ A)    &   ⊢ (φ → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (φ → (A↑𝑀) ≤ (A↑𝑁))
Theorem	leexp2rd 9043	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 𝑀 ∈ ℕ0)    &   ⊢ (φ → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (φ → 0 ≤ A)    &   ⊢ (φ → A ≤ 1)    ⇒   ⊢ (φ → (A↑𝑁) ≤ (A↑𝑀))
Theorem	lt2sqd 9044	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 9045	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 9046	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 9047	Extend class notation to include complex conjugate function.
class ∗
Syntax	cre 9048	Extend class notation to include real part of a complex number.
class ℜ
Syntax	cim 9049	Extend class notation to include imaginary part of a complex number.
class ℑ
Definition	df-cj 9050*	Define the complex conjugate function. See cjcli 9121 for its closure and cjval 9053 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 9051	Define a function whose value is the real part of a complex number. See reval 9057 for its value, recli 9119 for its closure, and replim 9067 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
⊢ ℜ = (x ∈ ℂ ↦ ((x + (∗‘x)) / 2))
Definition	df-im 9052	Define a function whose value is the imaginary part of a complex number. See imval 9058 for its value, imcli 9120 for its closure, and replim 9067 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
⊢ ℑ = (x ∈ ℂ ↦ (ℜ‘(x / i)))
Theorem	cjval 9053*	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 9054	The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ (A ∈ ℂ → ((A + (∗‘A)) ∈ ℝ ∧ (i · (A − (∗‘A))) ∈ ℝ))
Theorem	cjf 9055	Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ ∗:ℂ⟶ℂ
Theorem	cjcl 9056	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 9057	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 9058	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 9059	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 9060	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 9061	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 9062	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 9063	Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ ℜ:ℂ⟶ℝ
Theorem	imf 9064	Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ ℑ:ℂ⟶ℝ
Theorem	crre 9065	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 9066	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 9067	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 9068	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 9069	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 9070	A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.)
⊢ (A ∈ ℂ → (A ∈ ℝ ↔ (ℑ‘A) = 0))
Theorem	rereb 9071	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 9072	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 9073	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 9074	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 9075	Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (A ∈ ℂ → (ℜ‘(∗‘A)) = (ℜ‘A))
Theorem	reneg 9076	Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (A ∈ ℂ → (ℜ‘-A) = -(ℜ‘A))
Theorem	readd 9077	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 9078	Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (ℜ‘(A − B)) = ((ℜ‘A) − (ℜ‘B)))
Theorem	remullem 9079	Lemma for remul 9080, immul 9087, and cjmul 9093. (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 9080	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 9081	Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((A ∈ ℝ ∧ B ∈ ℂ) → (ℜ‘(A · B)) = (A · (ℜ‘B)))
Theorem	redivap 9082	Real part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((A ∈ ℂ ∧ B ∈ ℝ ∧ B # 0) → (ℜ‘(A / B)) = ((ℜ‘A) / B))
Theorem	imcj 9083	Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (A ∈ ℂ → (ℑ‘(∗‘A)) = -(ℑ‘A))
Theorem	imneg 9084	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 9085	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 9086	Imaginary part distributes over subtraction. (Contributed by NM, 18-Mar-2005.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (ℑ‘(A − B)) = ((ℑ‘A) − (ℑ‘B)))
Theorem	immul 9087	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 9088	Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((A ∈ ℝ ∧ B ∈ ℂ) → (ℑ‘(A · B)) = (A · (ℑ‘B)))
Theorem	imdivap 9089	Imaginary part of a division. Related to immul2 9088. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((A ∈ ℂ ∧ B ∈ ℝ ∧ B # 0) → (ℑ‘(A / B)) = ((ℑ‘A) / B))
Theorem	cjre 9090	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 9091	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 9092	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 9093	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 9094	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 9095	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 9096	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 9097	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 9098	Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (A ∈ ℂ → (∗‘-A) = -(∗‘A))
Theorem	addcj 9099	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 9100	Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (∗‘(A − B)) = ((∗‘A) − (∗‘B)))