Theorem List for Intuitionistic Logic Explorer - 10801-10900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | remul2 10801 |
Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) →
(ℜ‘(𝐴 ·
𝐵)) = (𝐴 · (ℜ‘𝐵))) |
|
Theorem | redivap 10802 |
Real part of a division. Related to remul2 10801. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 # 0) → (ℜ‘(𝐴 / 𝐵)) = ((ℜ‘𝐴) / 𝐵)) |
|
Theorem | imcj 10803 |
Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ →
(ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴)) |
|
Theorem | imneg 10804 |
The imaginary part of a negative number. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ →
(ℑ‘-𝐴) =
-(ℑ‘𝐴)) |
|
Theorem | imadd 10805 |
Imaginary part distributes over addition. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))) |
|
Theorem | imsub 10806 |
Imaginary part distributes over subtraction. (Contributed by NM,
18-Mar-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘(𝐴 −
𝐵)) =
((ℑ‘𝐴) −
(ℑ‘𝐵))) |
|
Theorem | immul 10807 |
Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised
by Mario Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘(𝐴 ·
𝐵)) =
(((ℜ‘𝐴)
· (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵)))) |
|
Theorem | immul2 10808 |
Imaginary part of a product. (Contributed by Mario Carneiro,
2-Aug-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) →
(ℑ‘(𝐴 ·
𝐵)) = (𝐴 · (ℑ‘𝐵))) |
|
Theorem | imdivap 10809 |
Imaginary part of a division. Related to immul2 10808. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 # 0) → (ℑ‘(𝐴 / 𝐵)) = ((ℑ‘𝐴) / 𝐵)) |
|
Theorem | cjre 10810 |
A real number equals its complex conjugate. Proposition 10-3.4(f) of
[Gleason] p. 133. (Contributed by NM,
8-Oct-1999.)
|
⊢ (𝐴 ∈ ℝ →
(∗‘𝐴) = 𝐴) |
|
Theorem | cjcj 10811 |
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 10812 |
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 10813 |
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 10814 |
Standard inner product on complex numbers. (Contributed by NM,
29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘(𝐴 ·
(∗‘𝐵))) =
(((ℜ‘𝐴)
· (ℜ‘𝐵))
+ ((ℑ‘𝐴)
· (ℑ‘𝐵)))) |
|
Theorem | cjmulrcl 10815 |
A complex number times its conjugate is real. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) ∈ ℝ) |
|
Theorem | cjmulval 10816 |
A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) |
|
Theorem | cjmulge0 10817 |
A complex number times its conjugate is nonnegative. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ → 0 ≤ (𝐴 · (∗‘𝐴))) |
|
Theorem | cjneg 10818 |
Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ →
(∗‘-𝐴) =
-(∗‘𝐴)) |
|
Theorem | addcj 10819 |
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 10820 |
Complex conjugate distributes over subtraction. (Contributed by NM,
28-Apr-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(∗‘(𝐴 −
𝐵)) =
((∗‘𝐴)
− (∗‘𝐵))) |
|
Theorem | cjexp 10821 |
Complex conjugate of positive integer exponentiation. (Contributed by
NM, 7-Jun-2006.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) →
(∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁)) |
|
Theorem | imval2 10822 |
The imaginary part of a number in terms of complex conjugate.
(Contributed by NM, 30-Apr-2005.)
|
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) = ((𝐴 − (∗‘𝐴)) / (2 · i))) |
|
Theorem | re0 10823 |
The real part of zero. (Contributed by NM, 27-Jul-1999.)
|
⊢ (ℜ‘0) = 0 |
|
Theorem | im0 10824 |
The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
|
⊢ (ℑ‘0) = 0 |
|
Theorem | re1 10825 |
The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|
⊢ (ℜ‘1) = 1 |
|
Theorem | im1 10826 |
The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|
⊢ (ℑ‘1) = 0 |
|
Theorem | rei 10827 |
The real part of i. (Contributed by Scott Fenton,
9-Jun-2006.)
|
⊢ (ℜ‘i) = 0 |
|
Theorem | imi 10828 |
The imaginary part of i. (Contributed by Scott Fenton,
9-Jun-2006.)
|
⊢ (ℑ‘i) = 1 |
|
Theorem | cj0 10829 |
The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
|
⊢ (∗‘0) = 0 |
|
Theorem | cji 10830 |
The complex conjugate of the imaginary unit. (Contributed by NM,
26-Mar-2005.)
|
⊢ (∗‘i) = -i |
|
Theorem | cjreim 10831 |
The conjugate of a representation of a complex number in terms of real and
imaginary parts. (Contributed by NM, 1-Jul-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(∗‘(𝐴 + (i
· 𝐵))) = (𝐴 − (i · 𝐵))) |
|
Theorem | cjreim2 10832 |
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.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(∗‘(𝐴 −
(i · 𝐵))) = (𝐴 + (i · 𝐵))) |
|
Theorem | cj11 10833 |
Complex conjugate is a one-to-one function. (Contributed by NM,
29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((∗‘𝐴) =
(∗‘𝐵) ↔
𝐴 = 𝐵)) |
|
Theorem | cjap 10834 |
Complex conjugate and apartness. (Contributed by Jim Kingdon,
14-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((∗‘𝐴) #
(∗‘𝐵) ↔
𝐴 # 𝐵)) |
|
Theorem | cjap0 10835 |
A number is apart from zero iff its complex conjugate is apart from zero.
(Contributed by Jim Kingdon, 14-Jun-2020.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 # 0 ↔ (∗‘𝐴) # 0)) |
|
Theorem | cjne0 10836 |
A number is nonzero iff its complex conjugate is nonzero. Also see
cjap0 10835 which is similar but for apartness.
(Contributed by NM,
29-Apr-2005.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 ↔ (∗‘𝐴) ≠ 0)) |
|
Theorem | cjdivap 10837 |
Complex conjugate distributes over division. (Contributed by Jim Kingdon,
14-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵))) |
|
Theorem | cnrecnv 10838* |
The inverse to the canonical bijection from (ℝ ×
ℝ) to ℂ
from cnref1o 9579. (Contributed by Mario Carneiro,
25-Aug-2014.)
|
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) ⇒ ⊢ ◡𝐹 = (𝑧 ∈ ℂ ↦
〈(ℜ‘𝑧),
(ℑ‘𝑧)〉) |
|
Theorem | recli 10839 |
The real part of a complex number is real (closure law). (Contributed
by NM, 11-May-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (ℜ‘𝐴) ∈ ℝ |
|
Theorem | imcli 10840 |
The imaginary part of a complex number is real (closure law).
(Contributed by NM, 11-May-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (ℑ‘𝐴) ∈
ℝ |
|
Theorem | cjcli 10841 |
Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (∗‘𝐴) ∈
ℂ |
|
Theorem | replimi 10842 |
Construct a complex number from its real and imaginary parts.
(Contributed by NM, 1-Oct-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴))) |
|
Theorem | cjcji 10843 |
The conjugate of the conjugate is the original complex number.
Proposition 10-3.4(e) of [Gleason] p.
133. (Contributed by NM,
11-May-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢
(∗‘(∗‘𝐴)) = 𝐴 |
|
Theorem | reim0bi 10844 |
A number is real iff its imaginary part is 0. (Contributed by NM,
29-May-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0) |
|
Theorem | rerebi 10845 |
A real number equals its real part. Proposition 10-3.4(f) of [Gleason]
p. 133. (Contributed by NM, 27-Oct-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 ∈ ℝ ↔ (ℜ‘𝐴) = 𝐴) |
|
Theorem | cjrebi 10846 |
A number is real iff it equals its complex conjugate. Proposition
10-3.4(f) of [Gleason] p. 133.
(Contributed by NM, 11-Oct-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 ∈ ℝ ↔
(∗‘𝐴) = 𝐴) |
|
Theorem | recji 10847 |
Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢
(ℜ‘(∗‘𝐴)) = (ℜ‘𝐴) |
|
Theorem | imcji 10848 |
Imaginary part of a complex conjugate. (Contributed by NM,
2-Oct-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢
(ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴) |
|
Theorem | cjmulrcli 10849 |
A complex number times its conjugate is real. (Contributed by NM,
11-May-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 · (∗‘𝐴)) ∈ ℝ |
|
Theorem | cjmulvali 10850 |
A complex number times its conjugate. (Contributed by NM,
2-Oct-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) |
|
Theorem | cjmulge0i 10851 |
A complex number times its conjugate is nonnegative. (Contributed by
NM, 28-May-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ 0 ≤ (𝐴 · (∗‘𝐴)) |
|
Theorem | renegi 10852 |
Real part of negative. (Contributed by NM, 2-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (ℜ‘-𝐴) = -(ℜ‘𝐴) |
|
Theorem | imnegi 10853 |
Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (ℑ‘-𝐴) = -(ℑ‘𝐴) |
|
Theorem | cjnegi 10854 |
Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (∗‘-𝐴) = -(∗‘𝐴) |
|
Theorem | addcji 10855 |
A number plus its conjugate is twice its real part. Compare Proposition
10-3.4(h) of [Gleason] p. 133.
(Contributed by NM, 2-Oct-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 + (∗‘𝐴)) = (2 · (ℜ‘𝐴)) |
|
Theorem | readdi 10856 |
Real part distributes over addition. (Contributed by NM,
28-Jul-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵)) |
|
Theorem | imaddi 10857 |
Imaginary part distributes over addition. (Contributed by NM,
28-Jul-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵)) |
|
Theorem | remuli 10858 |
Real part of a product. (Contributed by NM, 28-Jul-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))) |
|
Theorem | immuli 10859 |
Imaginary part of a product. (Contributed by NM, 28-Jul-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))) |
|
Theorem | cjaddi 10860 |
Complex conjugate distributes over addition. Proposition 10-3.4(a) of
[Gleason] p. 133. (Contributed by NM,
28-Jul-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵)) |
|
Theorem | cjmuli 10861 |
Complex conjugate distributes over multiplication. Proposition
10-3.4(c) of [Gleason] p. 133.
(Contributed by NM, 28-Jul-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵)) |
|
Theorem | ipcni 10862 |
Standard inner product on complex numbers. (Contributed by NM,
2-Oct-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵))) |
|
Theorem | cjdivapi 10863 |
Complex conjugate distributes over division. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (𝐵 # 0 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵))) |
|
Theorem | crrei 10864 |
The real part of a complex number representation. Definition 10-3.1 of
[Gleason] p. 132. (Contributed by NM,
10-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴 |
|
Theorem | crimi 10865 |
The imaginary part of a complex number representation. Definition
10-3.1 of [Gleason] p. 132.
(Contributed by NM, 10-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵 |
|
Theorem | recld 10866 |
The real part of a complex number is real (closure law). (Contributed
by Mario Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (ℜ‘𝐴) ∈ ℝ) |
|
Theorem | imcld 10867 |
The imaginary part of a complex number is real (closure law).
(Contributed by Mario Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (ℑ‘𝐴) ∈ ℝ) |
|
Theorem | cjcld 10868 |
Closure law for complex conjugate. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ) |
|
Theorem | replimd 10869 |
Construct a complex number from its real and imaginary parts.
(Contributed by Mario Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴)))) |
|
Theorem | remimd 10870 |
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 Mario Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (∗‘𝐴) = ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))) |
|
Theorem | cjcjd 10871 |
The conjugate of the conjugate is the original complex number.
Proposition 10-3.4(e) of [Gleason] p.
133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 →
(∗‘(∗‘𝐴)) = 𝐴) |
|
Theorem | reim0bd 10872 |
A number is real iff its imaginary part is 0. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (ℑ‘𝐴) = 0)
⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) |
|
Theorem | rerebd 10873 |
A real number equals its real part. Proposition 10-3.4(f) of
[Gleason] p. 133. (Contributed by
Mario Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (ℜ‘𝐴) = 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) |
|
Theorem | cjrebd 10874 |
A number is real iff it equals its complex conjugate. Proposition
10-3.4(f) of [Gleason] p. 133.
(Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (∗‘𝐴) = 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) |
|
Theorem | cjne0d 10875 |
A number which is nonzero has a complex conjugate which is nonzero.
Also see cjap0d 10876 which is similar but for apartness.
(Contributed by
Mario Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (∗‘𝐴) ≠ 0) |
|
Theorem | cjap0d 10876 |
A number which is apart from zero has a complex conjugate which is
apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 # 0) ⇒ ⊢ (𝜑 → (∗‘𝐴) # 0) |
|
Theorem | recjd 10877 |
Real part of a complex conjugate. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴)) |
|
Theorem | imcjd 10878 |
Imaginary part of a complex conjugate. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 →
(ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴)) |
|
Theorem | cjmulrcld 10879 |
A complex number times its conjugate is real. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℝ) |
|
Theorem | cjmulvald 10880 |
A complex number times its conjugate. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) |
|
Theorem | cjmulge0d 10881 |
A complex number times its conjugate is nonnegative. (Contributed by
Mario Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → 0 ≤ (𝐴 · (∗‘𝐴))) |
|
Theorem | renegd 10882 |
Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (ℜ‘-𝐴) = -(ℜ‘𝐴)) |
|
Theorem | imnegd 10883 |
Imaginary part of negative. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (ℑ‘-𝐴) = -(ℑ‘𝐴)) |
|
Theorem | cjnegd 10884 |
Complex conjugate of negative. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (∗‘-𝐴) = -(∗‘𝐴)) |
|
Theorem | addcjd 10885 |
A number plus its conjugate is twice its real part. Compare Proposition
10-3.4(h) of [Gleason] p. 133.
(Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 + (∗‘𝐴)) = (2 · (ℜ‘𝐴))) |
|
Theorem | cjexpd 10886 |
Complex conjugate of positive integer exponentiation. (Contributed by
Mario Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈
ℕ0) ⇒ ⊢ (𝜑 → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁)) |
|
Theorem | readdd 10887 |
Real part distributes over addition. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))) |
|
Theorem | imaddd 10888 |
Imaginary part distributes over addition. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))) |
|
Theorem | resubd 10889 |
Real part distributes over subtraction. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (ℜ‘(𝐴 − 𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵))) |
|
Theorem | imsubd 10890 |
Imaginary part distributes over subtraction. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (ℑ‘(𝐴 − 𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵))) |
|
Theorem | remuld 10891 |
Real part of a product. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵)))) |
|
Theorem | immuld 10892 |
Imaginary part of a product. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵)))) |
|
Theorem | cjaddd 10893 |
Complex conjugate distributes over addition. Proposition 10-3.4(a) of
[Gleason] p. 133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵))) |
|
Theorem | cjmuld 10894 |
Complex conjugate distributes over multiplication. Proposition
10-3.4(c) of [Gleason] p. 133.
(Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵))) |
|
Theorem | ipcnd 10895 |
Standard inner product on complex numbers. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵)))) |
|
Theorem | cjdivapd 10896 |
Complex conjugate distributes over division. (Contributed by Jim
Kingdon, 15-Jun-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 # 0) ⇒ ⊢ (𝜑 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵))) |
|
Theorem | rered 10897 |
A real number equals its real part. One direction of Proposition
10-3.4(f) of [Gleason] p. 133.
(Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (ℜ‘𝐴) = 𝐴) |
|
Theorem | reim0d 10898 |
The imaginary part of a real number is 0. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (ℑ‘𝐴) = 0) |
|
Theorem | cjred 10899 |
A real number equals its complex conjugate. Proposition 10-3.4(f) of
[Gleason] p. 133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (∗‘𝐴) = 𝐴) |
|
Theorem | remul2d 10900 |
Real part of a product. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵))) |