Theorem List for Intuitionistic Logic Explorer - 9101-9200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | remul2 9101 |
Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℂ) → (ℜ‘(A ·
B)) = (A · (ℜ‘B))) |
|
Theorem | redivap 9102 |
Real part of a division. Related to remul2 9101. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
⊢ ((A ∈ ℂ ∧
B ∈
ℝ ∧ B # 0) → (ℜ‘(A / B)) =
((ℜ‘A) / B)) |
|
Theorem | imcj 9103 |
Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (A ∈ ℂ →
(ℑ‘(∗‘A)) =
-(ℑ‘A)) |
|
Theorem | imneg 9104 |
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 9105 |
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 9106 |
Imaginary part distributes over subtraction. (Contributed by NM,
18-Mar-2005.)
|
⊢ ((A ∈ ℂ ∧
B ∈
ℂ) → (ℑ‘(A −
B)) = ((ℑ‘A) − (ℑ‘B))) |
|
Theorem | immul 9107 |
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 9108 |
Imaginary part of a product. (Contributed by Mario Carneiro,
2-Aug-2014.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℂ) → (ℑ‘(A ·
B)) = (A · (ℑ‘B))) |
|
Theorem | imdivap 9109 |
Imaginary part of a division. Related to immul2 9108. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
⊢ ((A ∈ ℂ ∧
B ∈
ℝ ∧ B # 0) → (ℑ‘(A / B)) =
((ℑ‘A) / B)) |
|
Theorem | cjre 9110 |
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 9111 |
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 9112 |
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 9113 |
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 9114 |
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 9115 |
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 9116 |
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 9117 |
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 9118 |
Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (A ∈ ℂ → (∗‘-A) = -(∗‘A)) |
|
Theorem | addcj 9119 |
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 9120 |
Complex conjugate distributes over subtraction. (Contributed by NM,
28-Apr-2005.)
|
⊢ ((A ∈ ℂ ∧
B ∈
ℂ) → (∗‘(A −
B)) = ((∗‘A) − (∗‘B))) |
|
Theorem | cjexp 9121 |
Complex conjugate of positive integer exponentiation. (Contributed by
NM, 7-Jun-2006.)
|
⊢ ((A ∈ ℂ ∧ 𝑁 ∈ ℕ0) →
(∗‘(A↑𝑁)) = ((∗‘A)↑𝑁)) |
|
Theorem | imval2 9122 |
The imaginary part of a number in terms of complex conjugate.
(Contributed by NM, 30-Apr-2005.)
|
⊢ (A ∈ ℂ → (ℑ‘A) = ((A
− (∗‘A)) / (2 ·
i))) |
|
Theorem | re0 9123 |
The real part of zero. (Contributed by NM, 27-Jul-1999.)
|
⊢ (ℜ‘0) = 0 |
|
Theorem | im0 9124 |
The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
|
⊢ (ℑ‘0) = 0 |
|
Theorem | re1 9125 |
The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|
⊢ (ℜ‘1) = 1 |
|
Theorem | im1 9126 |
The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|
⊢ (ℑ‘1) = 0 |
|
Theorem | rei 9127 |
The real part of i. (Contributed by Scott Fenton,
9-Jun-2006.)
|
⊢ (ℜ‘i) = 0 |
|
Theorem | imi 9128 |
The imaginary part of i. (Contributed by Scott Fenton,
9-Jun-2006.)
|
⊢ (ℑ‘i) = 1 |
|
Theorem | cj0 9129 |
The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
|
⊢ (∗‘0) = 0 |
|
Theorem | cji 9130 |
The complex conjugate of the imaginary unit. (Contributed by NM,
26-Mar-2005.)
|
⊢ (∗‘i) = -i |
|
Theorem | cjreim 9131 |
The conjugate of a representation of a complex number in terms of real and
imaginary parts. (Contributed by NM, 1-Jul-2005.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ) → (∗‘(A + (i
· B))) = (A − (i · B))) |
|
Theorem | cjreim2 9132 |
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.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ) → (∗‘(A −
(i · B))) = (A + (i · B))) |
|
Theorem | cj11 9133 |
Complex conjugate is a one-to-one function. (Contributed by NM,
29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.)
|
⊢ ((A ∈ ℂ ∧
B ∈
ℂ) → ((∗‘A) =
(∗‘B) ↔ A = B)) |
|
Theorem | cjap 9134 |
Complex conjugate and apartness. (Contributed by Jim Kingdon,
14-Jun-2020.)
|
⊢ ((A ∈ ℂ ∧
B ∈
ℂ) → ((∗‘A) #
(∗‘B) ↔ A # B)) |
|
Theorem | cjap0 9135 |
A number is apart from zero iff its complex conjugate is apart from zero.
(Contributed by Jim Kingdon, 14-Jun-2020.)
|
⊢ (A ∈ ℂ → (A # 0 ↔ (∗‘A) # 0)) |
|
Theorem | cjne0 9136 |
A number is nonzero iff its complex conjugate is nonzero. (Contributed by
NM, 29-Apr-2005.)
|
⊢ (A ∈ ℂ → (A ≠ 0 ↔ (∗‘A) ≠ 0)) |
|
Theorem | cjdivap 9137 |
Complex conjugate distributes over division. (Contributed by Jim Kingdon,
14-Jun-2020.)
|
⊢ ((A ∈ ℂ ∧
B ∈
ℂ ∧ B # 0) → (∗‘(A / B)) =
((∗‘A) /
(∗‘B))) |
|
Theorem | cnrecnv 9138* |
The inverse to the canonical bijection from (ℝ ×
ℝ) to ℂ
from cnref1o 8357. (Contributed by Mario Carneiro,
25-Aug-2014.)
|
⊢ 𝐹 = (x
∈ ℝ, y ∈ ℝ
↦ (x + (i · y))) ⇒ ⊢ ◡𝐹 = (z
∈ ℂ ↦
〈(ℜ‘z),
(ℑ‘z)〉) |
|
Theorem | recli 9139 |
The real part of a complex number is real (closure law). (Contributed
by NM, 11-May-1999.)
|
⊢ A ∈ ℂ ⇒ ⊢ (ℜ‘A) ∈
ℝ |
|
Theorem | imcli 9140 |
The imaginary part of a complex number is real (closure law).
(Contributed by NM, 11-May-1999.)
|
⊢ A ∈ ℂ ⇒ ⊢ (ℑ‘A) ∈
ℝ |
|
Theorem | cjcli 9141 |
Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
|
⊢ A ∈ ℂ ⇒ ⊢ (∗‘A) ∈
ℂ |
|
Theorem | replimi 9142 |
Construct a complex number from its real and imaginary parts.
(Contributed by NM, 1-Oct-1999.)
|
⊢ A ∈ ℂ ⇒ ⊢ A = ((ℜ‘A) + (i · (ℑ‘A))) |
|
Theorem | cjcji 9143 |
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.)
|
⊢ A ∈ ℂ ⇒ ⊢
(∗‘(∗‘A))
= A |
|
Theorem | reim0bi 9144 |
A number is real iff its imaginary part is 0. (Contributed by NM,
29-May-1999.)
|
⊢ A ∈ ℂ ⇒ ⊢ (A ∈ ℝ
↔ (ℑ‘A) =
0) |
|
Theorem | rerebi 9145 |
A real number equals its real part. Proposition 10-3.4(f) of [Gleason]
p. 133. (Contributed by NM, 27-Oct-1999.)
|
⊢ A ∈ ℂ ⇒ ⊢ (A ∈ ℝ
↔ (ℜ‘A) = A) |
|
Theorem | cjrebi 9146 |
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.)
|
⊢ A ∈ ℂ ⇒ ⊢ (A ∈ ℝ
↔ (∗‘A) = A) |
|
Theorem | recji 9147 |
Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
|
⊢ A ∈ ℂ ⇒ ⊢
(ℜ‘(∗‘A)) =
(ℜ‘A) |
|
Theorem | imcji 9148 |
Imaginary part of a complex conjugate. (Contributed by NM,
2-Oct-1999.)
|
⊢ A ∈ ℂ ⇒ ⊢
(ℑ‘(∗‘A))
= -(ℑ‘A) |
|
Theorem | cjmulrcli 9149 |
A complex number times its conjugate is real. (Contributed by NM,
11-May-1999.)
|
⊢ A ∈ ℂ ⇒ ⊢ (A · (∗‘A)) ∈
ℝ |
|
Theorem | cjmulvali 9150 |
A complex number times its conjugate. (Contributed by NM,
2-Oct-1999.)
|
⊢ A ∈ ℂ ⇒ ⊢ (A · (∗‘A)) = (((ℜ‘A)↑2) + ((ℑ‘A)↑2)) |
|
Theorem | cjmulge0i 9151 |
A complex number times its conjugate is nonnegative. (Contributed by
NM, 28-May-1999.)
|
⊢ A ∈ ℂ ⇒ ⊢ 0 ≤ (A · (∗‘A)) |
|
Theorem | renegi 9152 |
Real part of negative. (Contributed by NM, 2-Aug-1999.)
|
⊢ A ∈ ℂ ⇒ ⊢ (ℜ‘-A) = -(ℜ‘A) |
|
Theorem | imnegi 9153 |
Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
|
⊢ A ∈ ℂ ⇒ ⊢ (ℑ‘-A) = -(ℑ‘A) |
|
Theorem | cjnegi 9154 |
Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
|
⊢ A ∈ ℂ ⇒ ⊢ (∗‘-A) = -(∗‘A) |
|
Theorem | addcji 9155 |
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.)
|
⊢ A ∈ ℂ ⇒ ⊢ (A + (∗‘A)) = (2 · (ℜ‘A)) |
|
Theorem | readdi 9156 |
Real part distributes over addition. (Contributed by NM,
28-Jul-1999.)
|
⊢ A ∈ ℂ & ⊢ B ∈
ℂ ⇒ ⊢ (ℜ‘(A + B)) =
((ℜ‘A) + (ℜ‘B)) |
|
Theorem | imaddi 9157 |
Imaginary part distributes over addition. (Contributed by NM,
28-Jul-1999.)
|
⊢ A ∈ ℂ & ⊢ B ∈
ℂ ⇒ ⊢ (ℑ‘(A + B)) =
((ℑ‘A) +
(ℑ‘B)) |
|
Theorem | remuli 9158 |
Real part of a product. (Contributed by NM, 28-Jul-1999.)
|
⊢ A ∈ ℂ & ⊢ B ∈
ℂ ⇒ ⊢ (ℜ‘(A · B))
= (((ℜ‘A) ·
(ℜ‘B)) −
((ℑ‘A) ·
(ℑ‘B))) |
|
Theorem | immuli 9159 |
Imaginary part of a product. (Contributed by NM, 28-Jul-1999.)
|
⊢ A ∈ ℂ & ⊢ B ∈
ℂ ⇒ ⊢ (ℑ‘(A · B))
= (((ℜ‘A) ·
(ℑ‘B)) +
((ℑ‘A) ·
(ℜ‘B))) |
|
Theorem | cjaddi 9160 |
Complex conjugate distributes over addition. Proposition 10-3.4(a) of
[Gleason] p. 133. (Contributed by NM,
28-Jul-1999.)
|
⊢ A ∈ ℂ & ⊢ B ∈
ℂ ⇒ ⊢ (∗‘(A + B)) =
((∗‘A) +
(∗‘B)) |
|
Theorem | cjmuli 9161 |
Complex conjugate distributes over multiplication. Proposition
10-3.4(c) of [Gleason] p. 133.
(Contributed by NM, 28-Jul-1999.)
|
⊢ A ∈ ℂ & ⊢ B ∈
ℂ ⇒ ⊢ (∗‘(A · B))
= ((∗‘A) ·
(∗‘B)) |
|
Theorem | ipcni 9162 |
Standard inner product on complex numbers. (Contributed by NM,
2-Oct-1999.)
|
⊢ A ∈ ℂ & ⊢ B ∈
ℂ ⇒ ⊢ (ℜ‘(A · (∗‘B))) = (((ℜ‘A) · (ℜ‘B)) + ((ℑ‘A) · (ℑ‘B))) |
|
Theorem | cjdivapi 9163 |
Complex conjugate distributes over division. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
⊢ A ∈ ℂ & ⊢ B ∈
ℂ ⇒ ⊢ (B # 0 → (∗‘(A / B)) =
((∗‘A) /
(∗‘B))) |
|
Theorem | crrei 9164 |
The real part of a complex number representation. Definition 10-3.1 of
[Gleason] p. 132. (Contributed by NM,
10-May-1999.)
|
⊢ A ∈ ℝ & ⊢ B ∈
ℝ ⇒ ⊢ (ℜ‘(A + (i · B))) = A |
|
Theorem | crimi 9165 |
The imaginary part of a complex number representation. Definition
10-3.1 of [Gleason] p. 132.
(Contributed by NM, 10-May-1999.)
|
⊢ A ∈ ℝ & ⊢ B ∈
ℝ ⇒ ⊢ (ℑ‘(A + (i · B))) = B |
|
Theorem | recld 9166 |
The real part of a complex number is real (closure law). (Contributed
by Mario Carneiro, 29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ → (ℜ‘A) ∈
ℝ) |
|
Theorem | imcld 9167 |
The imaginary part of a complex number is real (closure law).
(Contributed by Mario Carneiro, 29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ → (ℑ‘A) ∈
ℝ) |
|
Theorem | cjcld 9168 |
Closure law for complex conjugate. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ → (∗‘A) ∈
ℂ) |
|
Theorem | replimd 9169 |
Construct a complex number from its real and imaginary parts.
(Contributed by Mario Carneiro, 29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ → A = ((ℜ‘A) + (i · (ℑ‘A)))) |
|
Theorem | remimd 9170 |
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.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ → (∗‘A) = ((ℜ‘A) − (i · (ℑ‘A)))) |
|
Theorem | cjcjd 9171 |
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.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ →
(∗‘(∗‘A)) =
A) |
|
Theorem | reim0bd 9172 |
A number is real iff its imaginary part is 0. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) & ⊢ (φ → (ℑ‘A) = 0) ⇒ ⊢ (φ → A ∈
ℝ) |
|
Theorem | rerebd 9173 |
A real number equals its real part. Proposition 10-3.4(f) of
[Gleason] p. 133. (Contributed by
Mario Carneiro, 29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) & ⊢ (φ → (ℜ‘A) = A) ⇒ ⊢ (φ → A ∈
ℝ) |
|
Theorem | cjrebd 9174 |
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.)
|
⊢ (φ
→ A ∈ ℂ) & ⊢ (φ → (∗‘A) = A) ⇒ ⊢ (φ → A ∈
ℝ) |
|
Theorem | cjne0d 9175 |
A number is nonzero iff its complex conjugate is nonzero.
(Contributed by Mario Carneiro, 29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) & ⊢ (φ → A ≠ 0) ⇒ ⊢ (φ → (∗‘A) ≠ 0) |
|
Theorem | recjd 9176 |
Real part of a complex conjugate. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ →
(ℜ‘(∗‘A)) =
(ℜ‘A)) |
|
Theorem | imcjd 9177 |
Imaginary part of a complex conjugate. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ →
(ℑ‘(∗‘A)) =
-(ℑ‘A)) |
|
Theorem | cjmulrcld 9178 |
A complex number times its conjugate is real. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ → (A · (∗‘A)) ∈
ℝ) |
|
Theorem | cjmulvald 9179 |
A complex number times its conjugate. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ → (A · (∗‘A)) = (((ℜ‘A)↑2) + ((ℑ‘A)↑2))) |
|
Theorem | cjmulge0d 9180 |
A complex number times its conjugate is nonnegative. (Contributed by
Mario Carneiro, 29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ → 0 ≤ (A · (∗‘A))) |
|
Theorem | renegd 9181 |
Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ → (ℜ‘-A) = -(ℜ‘A)) |
|
Theorem | imnegd 9182 |
Imaginary part of negative. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ → (ℑ‘-A) = -(ℑ‘A)) |
|
Theorem | cjnegd 9183 |
Complex conjugate of negative. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ → (∗‘-A) = -(∗‘A)) |
|
Theorem | addcjd 9184 |
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.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ → (A + (∗‘A)) = (2 · (ℜ‘A))) |
|
Theorem | cjexpd 9185 |
Complex conjugate of positive integer exponentiation. (Contributed by
Mario Carneiro, 29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) & ⊢ (φ → 𝑁 ∈
ℕ0) ⇒ ⊢ (φ → (∗‘(A↑𝑁)) = ((∗‘A)↑𝑁)) |
|
Theorem | readdd 9186 |
Real part distributes over addition. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) & ⊢ (φ → B ∈
ℂ) ⇒ ⊢ (φ → (ℜ‘(A + B)) =
((ℜ‘A) + (ℜ‘B))) |
|
Theorem | imaddd 9187 |
Imaginary part distributes over addition. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) & ⊢ (φ → B ∈
ℂ) ⇒ ⊢ (φ → (ℑ‘(A + B)) =
((ℑ‘A) +
(ℑ‘B))) |
|
Theorem | resubd 9188 |
Real part distributes over subtraction. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) & ⊢ (φ → B ∈
ℂ) ⇒ ⊢ (φ → (ℜ‘(A − B)) =
((ℜ‘A) −
(ℜ‘B))) |
|
Theorem | imsubd 9189 |
Imaginary part distributes over subtraction. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) & ⊢ (φ → B ∈
ℂ) ⇒ ⊢ (φ → (ℑ‘(A − B)) =
((ℑ‘A) −
(ℑ‘B))) |
|
Theorem | remuld 9190 |
Real part of a product. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) & ⊢ (φ → B ∈
ℂ) ⇒ ⊢ (φ → (ℜ‘(A · B))
= (((ℜ‘A) ·
(ℜ‘B)) −
((ℑ‘A) ·
(ℑ‘B)))) |
|
Theorem | immuld 9191 |
Imaginary part of a product. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) & ⊢ (φ → B ∈
ℂ) ⇒ ⊢ (φ → (ℑ‘(A · B))
= (((ℜ‘A) ·
(ℑ‘B)) +
((ℑ‘A) ·
(ℜ‘B)))) |
|
Theorem | cjaddd 9192 |
Complex conjugate distributes over addition. Proposition 10-3.4(a) of
[Gleason] p. 133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) & ⊢ (φ → B ∈
ℂ) ⇒ ⊢ (φ → (∗‘(A + B)) =
((∗‘A) +
(∗‘B))) |
|
Theorem | cjmuld 9193 |
Complex conjugate distributes over multiplication. Proposition
10-3.4(c) of [Gleason] p. 133.
(Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) & ⊢ (φ → B ∈
ℂ) ⇒ ⊢ (φ → (∗‘(A · B))
= ((∗‘A) ·
(∗‘B))) |
|
Theorem | ipcnd 9194 |
Standard inner product on complex numbers. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) & ⊢ (φ → B ∈
ℂ) ⇒ ⊢ (φ → (ℜ‘(A · (∗‘B))) = (((ℜ‘A) · (ℜ‘B)) + ((ℑ‘A) · (ℑ‘B)))) |
|
Theorem | cjdivapd 9195 |
Complex conjugate distributes over division. (Contributed by Jim
Kingdon, 15-Jun-2020.)
|
⊢ (φ
→ A ∈ ℂ) & ⊢ (φ → B ∈
ℂ)
& ⊢ (φ
→ B # 0)
⇒ ⊢ (φ → (∗‘(A / B)) =
((∗‘A) /
(∗‘B))) |
|
Theorem | rered 9196 |
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.)
|
⊢ (φ
→ A ∈ ℝ) ⇒ ⊢ (φ → (ℜ‘A) = A) |
|
Theorem | reim0d 9197 |
The imaginary part of a real number is 0. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) ⇒ ⊢ (φ → (ℑ‘A) = 0) |
|
Theorem | cjred 9198 |
A real number equals its complex conjugate. Proposition 10-3.4(f) of
[Gleason] p. 133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) ⇒ ⊢ (φ → (∗‘A) = A) |
|
Theorem | remul2d 9199 |
Real part of a product. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℂ) ⇒ ⊢ (φ → (ℜ‘(A · B))
= (A · (ℜ‘B))) |
|
Theorem | immul2d 9200 |
Imaginary part of a product. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℂ) ⇒ ⊢ (φ → (ℑ‘(A · B))
= (A · (ℑ‘B))) |