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)))) |