Theorem List for Intuitionistic Logic Explorer - 9401-9500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | nnsqcld 9401 |
The naturals are closed under squaring. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℕ)
⇒ ⊢ (𝜑 → (𝐴↑2) ∈ ℕ) |
|
Theorem | nnexpcld 9402 |
Closure of exponentiation of nonnegative integers. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈
ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℕ) |
|
Theorem | nn0expcld 9403 |
Closure of exponentiation of nonnegative integers. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈
ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈
ℕ0) |
|
Theorem | rpexpcld 9404 |
Closure law for exponentiation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℤ)
⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈
ℝ+) |
|
Theorem | reexpclzapd 9405 |
Closure of exponentiation of reals. (Contributed by Jim Kingdon,
13-Jun-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 # 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ)
⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ) |
|
Theorem | resqcld 9406 |
Closure of square in reals. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴↑2) ∈ ℝ) |
|
Theorem | sqge0d 9407 |
A square of a real is nonnegative. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → 0 ≤ (𝐴↑2)) |
|
Theorem | sqgt0apd 9408 |
The square of a real apart from zero is positive. (Contributed by Jim
Kingdon, 13-Jun-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 # 0) ⇒ ⊢ (𝜑 → 0 < (𝐴↑2)) |
|
Theorem | leexp2ad 9409 |
Ordering relationship for exponentiation. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 ≤ 𝐴)
& ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
⇒ ⊢ (𝜑 → (𝐴↑𝑀) ≤ (𝐴↑𝑁)) |
|
Theorem | leexp2rd 9410 |
Ordering relationship for exponentiation. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 𝐴 ≤ 1) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ≤ (𝐴↑𝑀)) |
|
Theorem | lt2sqd 9411 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2))) |
|
Theorem | le2sqd 9412 |
The square function on nonnegative reals is monotonic. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2))) |
|
Theorem | sq11d 9413 |
The square function is one-to-one for nonnegative reals. (Contributed
by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 0 ≤ 𝐵)
& ⊢ (𝜑 → (𝐴↑2) = (𝐵↑2)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
|
Theorem | sq11ap 9414 |
Analogue to sq11 9326 but for apartness. (Contributed by Jim
Kingdon,
12-Aug-2021.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) # (𝐵↑2) ↔ 𝐴 # 𝐵)) |
|
3.7 Elementary real and complex
functions
|
|
3.7.1 The "shift" operation
|
|
Syntax | cshi 9415 |
Extend class notation with function shifter.
|
class shift |
|
Definition | df-shft 9416* |
Define a function shifter. This operation offsets the value argument of
a function (ordinarily on a subset of ℂ)
and produces a new
function on ℂ. See shftval 9426 for its value. (Contributed by NM,
20-Jul-2005.)
|
⊢ shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)}) |
|
Theorem | shftlem 9417* |
Two ways to write a shifted set (𝐵 + 𝐴). (Contributed by Mario
Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ⊆ ℂ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵} = {𝑥 ∣ ∃𝑦 ∈ 𝐵 𝑥 = (𝑦 + 𝐴)}) |
|
Theorem | shftuz 9418* |
A shift of the upper integers. (Contributed by Mario Carneiro,
5-Nov-2013.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈
(ℤ≥‘𝐵)} = (ℤ≥‘(𝐵 + 𝐴))) |
|
Theorem | shftfvalg 9419* |
The value of the sequence shifter operation is a function on ℂ.
𝐴 is ordinarily an integer.
(Contributed by NM, 20-Jul-2005.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐹 ∈ 𝑉) → (𝐹 shift 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |
|
Theorem | ovshftex 9420 |
Existence of the result of applying shift. (Contributed by Jim Kingdon,
15-Aug-2021.)
|
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ) → (𝐹 shift 𝐴) ∈ V) |
|
Theorem | shftfibg 9421 |
Value of a fiber of the relation 𝐹. (Contributed by Jim Kingdon,
15-Aug-2021.)
|
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) “ {𝐵}) = (𝐹 “ {(𝐵 − 𝐴)})) |
|
Theorem | shftfval 9422* |
The value of the sequence shifter operation is a function on ℂ.
𝐴 is ordinarily an integer.
(Contributed by NM, 20-Jul-2005.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐴 ∈ ℂ → (𝐹 shift 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) |
|
Theorem | shftdm 9423* |
Domain of a relation shifted by 𝐴. The set on the right is more
commonly notated as (dom 𝐹 + 𝐴) (meaning add 𝐴 to every
element of dom 𝐹). (Contributed by Mario Carneiro,
3-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐴 ∈ ℂ → dom (𝐹 shift 𝐴) = {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ dom 𝐹}) |
|
Theorem | shftfib 9424 |
Value of a fiber of the relation 𝐹. (Contributed by Mario
Carneiro, 4-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) “ {𝐵}) = (𝐹 “ {(𝐵 − 𝐴)})) |
|
Theorem | shftfn 9425* |
Functionality and domain of a sequence shifted by 𝐴. (Contributed
by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐹 Fn 𝐵 ∧ 𝐴 ∈ ℂ) → (𝐹 shift 𝐴) Fn {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵}) |
|
Theorem | shftval 9426 |
Value of a sequence shifted by 𝐴. (Contributed by NM,
20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴))) |
|
Theorem | shftval2 9427 |
Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM,
20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘(𝐴 + 𝐶)) = (𝐹‘(𝐵 + 𝐶))) |
|
Theorem | shftval3 9428 |
Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM,
20-Jul-2005.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘𝐴) = (𝐹‘𝐵)) |
|
Theorem | shftval4 9429 |
Value of a sequence shifted by -𝐴. (Contributed by NM,
18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift -𝐴)‘𝐵) = (𝐹‘(𝐴 + 𝐵))) |
|
Theorem | shftval5 9430 |
Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘(𝐵 + 𝐴)) = (𝐹‘𝐵)) |
|
Theorem | shftf 9431* |
Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐴 ∈ ℂ) → (𝐹 shift 𝐴):{𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵}⟶𝐶) |
|
Theorem | 2shfti 9432 |
Composite shift operations. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) shift 𝐵) = (𝐹 shift (𝐴 + 𝐵))) |
|
Theorem | shftidt2 9433 |
Identity law for the shift operation. (Contributed by Mario Carneiro,
5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 shift 0) = (𝐹 ↾ ℂ) |
|
Theorem | shftidt 9434 |
Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐴 ∈ ℂ → ((𝐹 shift 0)‘𝐴) = (𝐹‘𝐴)) |
|
Theorem | shftcan1 9435 |
Cancellation law for the shift operation. (Contributed by NM,
4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐹 shift 𝐴) shift -𝐴)‘𝐵) = (𝐹‘𝐵)) |
|
Theorem | shftcan2 9436 |
Cancellation law for the shift operation. (Contributed by NM,
4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐹 shift -𝐴) shift 𝐴)‘𝐵) = (𝐹‘𝐵)) |
|
Theorem | shftvalg 9437 |
Value of a sequence shifted by 𝐴. (Contributed by Scott Fenton,
16-Dec-2017.)
|
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴))) |
|
Theorem | shftval4g 9438 |
Value of a sequence shifted by -𝐴. (Contributed by Jim Kingdon,
19-Aug-2021.)
|
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift -𝐴)‘𝐵) = (𝐹‘(𝐴 + 𝐵))) |
|
3.7.2 Real and imaginary parts;
conjugate
|
|
Syntax | ccj 9439 |
Extend class notation to include complex conjugate function.
|
class ∗ |
|
Syntax | cre 9440 |
Extend class notation to include real part of a complex number.
|
class ℜ |
|
Syntax | cim 9441 |
Extend class notation to include imaginary part of a complex number.
|
class ℑ |
|
Definition | df-cj 9442* |
Define the complex conjugate function. See cjcli 9513 for its closure and
cjval 9445 for its value. (Contributed by NM,
9-May-1999.) (Revised by
Mario Carneiro, 6-Nov-2013.)
|
⊢ ∗ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ))) |
|
Definition | df-re 9443 |
Define a function whose value is the real part of a complex number. See
reval 9449 for its value, recli 9511 for its closure, and replim 9459 for its use
in decomposing a complex number. (Contributed by NM, 9-May-1999.)
|
⊢ ℜ = (𝑥 ∈ ℂ ↦ ((𝑥 + (∗‘𝑥)) / 2)) |
|
Definition | df-im 9444 |
Define a function whose value is the imaginary part of a complex number.
See imval 9450 for its value, imcli 9512 for its closure, and replim 9459 for its
use in decomposing a complex number. (Contributed by NM,
9-May-1999.)
|
⊢ ℑ = (𝑥 ∈ ℂ ↦ (ℜ‘(𝑥 / i))) |
|
Theorem | cjval 9445* |
The value of the conjugate of a complex number. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
⊢ (𝐴 ∈ ℂ →
(∗‘𝐴) =
(℩𝑥 ∈
ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i
· (𝐴 − 𝑥)) ∈
ℝ))) |
|
Theorem | cjth 9446 |
The defining property of the complex conjugate. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴 + (∗‘𝐴)) ∈ ℝ ∧ (i · (𝐴 − (∗‘𝐴))) ∈
ℝ)) |
|
Theorem | cjf 9447 |
Domain and codomain of the conjugate function. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
⊢
∗:ℂ⟶ℂ |
|
Theorem | cjcl 9448 |
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.)
|
⊢ (𝐴 ∈ ℂ →
(∗‘𝐴) ∈
ℂ) |
|
Theorem | reval 9449 |
The value of the real part of a complex number. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = ((𝐴 + (∗‘𝐴)) / 2)) |
|
Theorem | imval 9450 |
The value of the imaginary part of a complex number. (Contributed by
NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) = (ℜ‘(𝐴 / i))) |
|
Theorem | imre 9451 |
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.)
|
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) = (ℜ‘(-i ·
𝐴))) |
|
Theorem | reim 9452 |
The real part of a complex number in terms of the imaginary part
function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = (ℑ‘(i ·
𝐴))) |
|
Theorem | recl 9453 |
The real part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈
ℝ) |
|
Theorem | imcl 9454 |
The imaginary part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈
ℝ) |
|
Theorem | ref 9455 |
Domain and codomain of the real part function. (Contributed by Paul
Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
⊢
ℜ:ℂ⟶ℝ |
|
Theorem | imf 9456 |
Domain and codomain of the imaginary part function. (Contributed by
Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
⊢
ℑ:ℂ⟶ℝ |
|
Theorem | crre 9457 |
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.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(ℜ‘(𝐴 + (i
· 𝐵))) = 𝐴) |
|
Theorem | crim 9458 |
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.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(ℑ‘(𝐴 + (i
· 𝐵))) = 𝐵) |
|
Theorem | replim 9459 |
Reconstruct a complex number from its real and imaginary parts.
(Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro,
7-Nov-2013.)
|
⊢ (𝐴 ∈ ℂ → 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴)))) |
|
Theorem | remim 9460 |
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.)
|
⊢ (𝐴 ∈ ℂ →
(∗‘𝐴) =
((ℜ‘𝐴) −
(i · (ℑ‘𝐴)))) |
|
Theorem | reim0 9461 |
The imaginary part of a real number is 0. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
|
⊢ (𝐴 ∈ ℝ → (ℑ‘𝐴) = 0) |
|
Theorem | reim0b 9462 |
A number is real iff its imaginary part is 0. (Contributed by NM,
26-Sep-2005.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0)) |
|
Theorem | rereb 9463 |
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.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (ℜ‘𝐴) = 𝐴)) |
|
Theorem | mulreap 9464 |
A product with a real multiplier apart from zero is real iff the
multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 # 0) → (𝐴 ∈ ℝ ↔ (𝐵 · 𝐴) ∈ ℝ)) |
|
Theorem | rere 9465 |
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.)
|
⊢ (𝐴 ∈ ℝ → (ℜ‘𝐴) = 𝐴) |
|
Theorem | cjreb 9466 |
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.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(∗‘𝐴) = 𝐴)) |
|
Theorem | recj 9467 |
Real part of a complex conjugate. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ →
(ℜ‘(∗‘𝐴)) = (ℜ‘𝐴)) |
|
Theorem | reneg 9468 |
Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by
Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) = -(ℜ‘𝐴)) |
|
Theorem | readd 9469 |
Real part distributes over addition. (Contributed by NM, 17-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))) |
|
Theorem | resub 9470 |
Real part distributes over subtraction. (Contributed by NM,
17-Mar-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘(𝐴 −
𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵))) |
|
Theorem | remullem 9471 |
Lemma for remul 9472, immul 9479, and cjmul 9485. (Contributed by NM,
28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℜ‘(𝐴 ·
𝐵)) =
(((ℜ‘𝐴)
· (ℜ‘𝐵))
− ((ℑ‘𝐴)
· (ℑ‘𝐵))) ∧ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))) ∧ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵)))) |
|
Theorem | remul 9472 |
Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by
Mario Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘(𝐴 ·
𝐵)) =
(((ℜ‘𝐴)
· (ℜ‘𝐵))
− ((ℑ‘𝐴)
· (ℑ‘𝐵)))) |
|
Theorem | remul2 9473 |
Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) →
(ℜ‘(𝐴 ·
𝐵)) = (𝐴 · (ℜ‘𝐵))) |
|
Theorem | redivap 9474 |
Real part of a division. Related to remul2 9473. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 # 0) → (ℜ‘(𝐴 / 𝐵)) = ((ℜ‘𝐴) / 𝐵)) |
|
Theorem | imcj 9475 |
Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ →
(ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴)) |
|
Theorem | imneg 9476 |
The imaginary part of a negative number. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ →
(ℑ‘-𝐴) =
-(ℑ‘𝐴)) |
|
Theorem | imadd 9477 |
Imaginary part distributes over addition. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))) |
|
Theorem | imsub 9478 |
Imaginary part distributes over subtraction. (Contributed by NM,
18-Mar-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘(𝐴 −
𝐵)) =
((ℑ‘𝐴) −
(ℑ‘𝐵))) |
|
Theorem | immul 9479 |
Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised
by Mario Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘(𝐴 ·
𝐵)) =
(((ℜ‘𝐴)
· (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵)))) |
|
Theorem | immul2 9480 |
Imaginary part of a product. (Contributed by Mario Carneiro,
2-Aug-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) →
(ℑ‘(𝐴 ·
𝐵)) = (𝐴 · (ℑ‘𝐵))) |
|
Theorem | imdivap 9481 |
Imaginary part of a division. Related to immul2 9480. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 # 0) → (ℑ‘(𝐴 / 𝐵)) = ((ℑ‘𝐴) / 𝐵)) |
|
Theorem | cjre 9482 |
A real number equals its complex conjugate. Proposition 10-3.4(f) of
[Gleason] p. 133. (Contributed by NM,
8-Oct-1999.)
|
⊢ (𝐴 ∈ ℝ →
(∗‘𝐴) = 𝐴) |
|
Theorem | cjcj 9483 |
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.)
|
⊢ (𝐴 ∈ ℂ →
(∗‘(∗‘𝐴)) = 𝐴) |
|
Theorem | cjadd 9484 |
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.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵))) |
|
Theorem | cjmul 9485 |
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.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(∗‘(𝐴
· 𝐵)) =
((∗‘𝐴)
· (∗‘𝐵))) |
|
Theorem | ipcnval 9486 |
Standard inner product on complex numbers. (Contributed by NM,
29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘(𝐴 ·
(∗‘𝐵))) =
(((ℜ‘𝐴)
· (ℜ‘𝐵))
+ ((ℑ‘𝐴)
· (ℑ‘𝐵)))) |
|
Theorem | cjmulrcl 9487 |
A complex number times its conjugate is real. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) ∈ ℝ) |
|
Theorem | cjmulval 9488 |
A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) |
|
Theorem | cjmulge0 9489 |
A complex number times its conjugate is nonnegative. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ → 0 ≤ (𝐴 · (∗‘𝐴))) |
|
Theorem | cjneg 9490 |
Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ →
(∗‘-𝐴) =
-(∗‘𝐴)) |
|
Theorem | addcj 9491 |
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.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 + (∗‘𝐴)) = (2 · (ℜ‘𝐴))) |
|
Theorem | cjsub 9492 |
Complex conjugate distributes over subtraction. (Contributed by NM,
28-Apr-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(∗‘(𝐴 −
𝐵)) =
((∗‘𝐴)
− (∗‘𝐵))) |
|
Theorem | cjexp 9493 |
Complex conjugate of positive integer exponentiation. (Contributed by
NM, 7-Jun-2006.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) →
(∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁)) |
|
Theorem | imval2 9494 |
The imaginary part of a number in terms of complex conjugate.
(Contributed by NM, 30-Apr-2005.)
|
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) = ((𝐴 − (∗‘𝐴)) / (2 · i))) |
|
Theorem | re0 9495 |
The real part of zero. (Contributed by NM, 27-Jul-1999.)
|
⊢ (ℜ‘0) = 0 |
|
Theorem | im0 9496 |
The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
|
⊢ (ℑ‘0) = 0 |
|
Theorem | re1 9497 |
The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|
⊢ (ℜ‘1) = 1 |
|
Theorem | im1 9498 |
The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|
⊢ (ℑ‘1) = 0 |
|
Theorem | rei 9499 |
The real part of i. (Contributed by Scott Fenton,
9-Jun-2006.)
|
⊢ (ℜ‘i) = 0 |
|
Theorem | imi 9500 |
The imaginary part of i. (Contributed by Scott Fenton,
9-Jun-2006.)
|
⊢ (ℑ‘i) = 1 |