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	neg1sqe1 9001	-1 squared is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (-1↑2) = 1
Theorem	sq2 9002	The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
⊢ (2↑2) = 4
Theorem	sq3 9003	The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
⊢ (3↑2) = 9
Theorem	cu2 9004	The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
⊢ (2↑3) = 8
Theorem	irec 9005	The reciprocal of i. (Contributed by NM, 11-Oct-1999.)
⊢ (1 / i) = -i
Theorem	i2 9006	i squared. (Contributed by NM, 6-May-1999.)
⊢ (i↑2) = -1
Theorem	i3 9007	i cubed. (Contributed by NM, 31-Jan-2007.)
⊢ (i↑3) = -i
Theorem	i4 9008	i to the fourth power. (Contributed by NM, 31-Jan-2007.)
⊢ (i↑4) = 1
Theorem	nnlesq 9009	A positive integer is less than or equal to its square. (Contributed by NM, 15-Sep-1999.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁↑2))
Theorem	expnass 9010	A counterexample showing that exponentiation is not associative. (Contributed by Stefan Allan and Gérard Lang, 21-Sep-2010.)
⊢ ((3↑3)↑3) < (3↑(3↑3))
Theorem	subsq 9011	Factor the difference of two squares. (Contributed by NM, 21-Feb-2008.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A↑2) − (B↑2)) = ((A + B) · (A − B)))
Theorem	subsq2 9012	Express the difference of the squares of two numbers as a polynomial in the difference of the numbers. (Contributed by NM, 21-Feb-2008.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A↑2) − (B↑2)) = (((A − B)↑2) + ((2 · B) · (A − B))))
Theorem	binom2i 9013	The square of a binomial. (Contributed by NM, 11-Aug-1999.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ ((A + B)↑2) = (((A↑2) + (2 · (A · B))) + (B↑2))
Theorem	subsqi 9014	Factor the difference of two squares. (Contributed by NM, 7-Feb-2005.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ ((A↑2) − (B↑2)) = ((A + B) · (A − B))
Theorem	binom2 9015	The square of a binomial. (Contributed by FL, 10-Dec-2006.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A + B)↑2) = (((A↑2) + (2 · (A · B))) + (B↑2)))
Theorem	binom21 9016	Special case of binom2 9015 where B = 1. (Contributed by Scott Fenton, 11-May-2014.)
⊢ (A ∈ ℂ → ((A + 1)↑2) = (((A↑2) + (2 · A)) + 1))
Theorem	binom2sub 9017	Expand the square of a subtraction. (Contributed by Scott Fenton, 10-Jun-2013.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A − B)↑2) = (((A↑2) − (2 · (A · B))) + (B↑2)))
Theorem	binom2subi 9018	Expand the square of a subtraction. (Contributed by Scott Fenton, 13-Jun-2013.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ ((A − B)↑2) = (((A↑2) − (2 · (A · B))) + (B↑2))
Theorem	binom3 9019	The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A + B)↑3) = (((A↑3) + (3 · ((A↑2) · B))) + ((3 · (A · (B↑2))) + (B↑3))))
Theorem	zesq 9020	An integer is even iff its square is even. (Contributed by Mario Carneiro, 12-Sep-2015.)
⊢ (𝑁 ∈ ℤ → ((𝑁 / 2) ∈ ℤ ↔ ((𝑁↑2) / 2) ∈ ℤ))
Theorem	nnesq 9021	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 9022	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 9023	Variation of Bernoulli's inequality bernneq 9022. (Contributed by NM, 18-Oct-2007.)
⊢ ((A ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ A) → (((A − 1) · 𝑁) + 1) ≤ (A↑𝑁))
Theorem	bernneq3 9024	A corollary of bernneq 9022. (Contributed by Mario Carneiro, 11-Mar-2014.)
⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → 𝑁 < (𝑃↑𝑁))
Theorem	expnbnd 9025*	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 9026*	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 9027*	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 9028	Value of a complex number raised to the 0th power. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A↑0) = 1)
Theorem	exp1d 9029	Value of a complex number raised to the first power. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A↑1) = A)
Theorem	expeq0d 9030	Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → 𝑁 ∈ ℕ)    &   ⊢ (φ → (A↑𝑁) = 0)    ⇒   ⊢ (φ → A = 0)
Theorem	sqvald 9031	Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A↑2) = (A · A))
Theorem	sqcld 9032	Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A↑2) ∈ ℂ)
Theorem	sqeq0d 9033	A number is zero iff its square is zero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → (A↑2) = 0)    ⇒   ⊢ (φ → A = 0)
Theorem	expcld 9034	Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℂ)
Theorem	expp1d 9035	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 9036	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 9037	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 9038	Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    ⇒   ⊢ (φ → ((1 / A)↑2) = (1 / (A↑2)))
Theorem	expclzapd 9039	Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℂ)
Theorem	expap0d 9040	Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → (A↑𝑁) # 0)
Theorem	expnegapd 9041	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 9042	Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → ((1 / A)↑𝑁) = (1 / (A↑𝑁)))
Theorem	expp1zapd 9043	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 9044	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 9045	Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    &   ⊢ (φ → 𝑀 ∈ ℤ)    ⇒   ⊢ (φ → (A↑(𝑀 − 𝑁)) = ((A↑𝑀) / (A↑𝑁)))
Theorem	sqmuld 9046	Distribution of square over multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → ((A · B)↑2) = ((A↑2) · (B↑2)))
Theorem	sqdivapd 9047	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 9048	Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    &   ⊢ (φ → B # 0)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → ((A / B)↑𝑁) = ((A↑𝑁) / (B↑𝑁)))
Theorem	mulexpd 9049	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 9050	Value of zero raised to a positive integer power. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → 𝑁 ∈ ℕ)    ⇒   ⊢ (φ → (0↑𝑁) = 0)
Theorem	reexpcld 9051	Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℝ)
Theorem	expge0d 9052	Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    &   ⊢ (φ → 0 ≤ A)    ⇒   ⊢ (φ → 0 ≤ (A↑𝑁))
Theorem	expge1d 9053	Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    &   ⊢ (φ → 1 ≤ A)    ⇒   ⊢ (φ → 1 ≤ (A↑𝑁))
Theorem	nnsqcld 9054	The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℕ)    ⇒   ⊢ (φ → (A↑2) ∈ ℕ)
Theorem	nnexpcld 9055	Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℕ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℕ)
Theorem	nn0expcld 9056	Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℕ0)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℕ0)
Theorem	rpexpcld 9057	Closure law for exponentiation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℝ+)
Theorem	reexpclzapd 9058	Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℝ)
Theorem	resqcld 9059	Closure of square in reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → (A↑2) ∈ ℝ)
Theorem	sqge0d 9060	A square of a real is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → 0 ≤ (A↑2))
Theorem	sqgt0apd 9061	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 9062	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 1 ≤ A)    &   ⊢ (φ → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (φ → (A↑𝑀) ≤ (A↑𝑁))
Theorem	leexp2rd 9063	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 𝑀 ∈ ℕ0)    &   ⊢ (φ → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (φ → 0 ≤ A)    &   ⊢ (φ → A ≤ 1)    ⇒   ⊢ (φ → (A↑𝑁) ≤ (A↑𝑀))
Theorem	lt2sqd 9064	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 9065	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 9066	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 9067	Extend class notation to include complex conjugate function.
class ∗
Syntax	cre 9068	Extend class notation to include real part of a complex number.
class ℜ
Syntax	cim 9069	Extend class notation to include imaginary part of a complex number.
class ℑ
Definition	df-cj 9070*	Define the complex conjugate function. See cjcli 9141 for its closure and cjval 9073 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 9071	Define a function whose value is the real part of a complex number. See reval 9077 for its value, recli 9139 for its closure, and replim 9087 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
⊢ ℜ = (x ∈ ℂ ↦ ((x + (∗‘x)) / 2))
Definition	df-im 9072	Define a function whose value is the imaginary part of a complex number. See imval 9078 for its value, imcli 9140 for its closure, and replim 9087 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
⊢ ℑ = (x ∈ ℂ ↦ (ℜ‘(x / i)))
Theorem	cjval 9073*	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 9074	The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ (A ∈ ℂ → ((A + (∗‘A)) ∈ ℝ ∧ (i · (A − (∗‘A))) ∈ ℝ))
Theorem	cjf 9075	Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ ∗:ℂ⟶ℂ
Theorem	cjcl 9076	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 9077	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 9078	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 9079	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 9080	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 9081	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 9082	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 9083	Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ ℜ:ℂ⟶ℝ
Theorem	imf 9084	Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
⊢ ℑ:ℂ⟶ℝ
Theorem	crre 9085	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 9086	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 9087	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 9088	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 9089	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 9090	A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.)
⊢ (A ∈ ℂ → (A ∈ ℝ ↔ (ℑ‘A) = 0))
Theorem	rereb 9091	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 9092	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 9093	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 9094	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 9095	Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (A ∈ ℂ → (ℜ‘(∗‘A)) = (ℜ‘A))
Theorem	reneg 9096	Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (A ∈ ℂ → (ℜ‘-A) = -(ℜ‘A))
Theorem	readd 9097	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 9098	Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (ℜ‘(A − B)) = ((ℜ‘A) − (ℜ‘B)))
Theorem	remullem 9099	Lemma for remul 9100, immul 9107, and cjmul 9113. (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 9100	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))))