Type | Label | Description |
Statement |
|
Theorem | imsub 10901 |
Imaginary part distributes over subtraction. (Contributed by NM,
18-Mar-2005.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด โ
๐ต)) =
((โโ๐ด) โ
(โโ๐ต))) |
|
Theorem | immul 10902 |
Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised
by Mario Carneiro, 14-Jul-2014.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
๐ต)) =
(((โโ๐ด)
ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))) |
|
Theorem | immul2 10903 |
Imaginary part of a product. (Contributed by Mario Carneiro,
2-Aug-2014.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
๐ต)) = (๐ด ยท (โโ๐ต))) |
|
Theorem | imdivap 10904 |
Imaginary part of a division. Related to immul2 10903. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต # 0) โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / ๐ต)) |
|
Theorem | cjre 10905 |
A real number equals its complex conjugate. Proposition 10-3.4(f) of
[Gleason] p. 133. (Contributed by NM,
8-Oct-1999.)
|
โข (๐ด โ โ โ
(โโ๐ด) = ๐ด) |
|
Theorem | cjcj 10906 |
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 10907 |
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 10908 |
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 10909 |
Standard inner product on complex numbers. (Contributed by NM,
29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
(โโ๐ต))) =
(((โโ๐ด)
ยท (โโ๐ต))
+ ((โโ๐ด)
ยท (โโ๐ต)))) |
|
Theorem | cjmulrcl 10910 |
A complex number times its conjugate is real. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
โข (๐ด โ โ โ (๐ด ยท (โโ๐ด)) โ โ) |
|
Theorem | cjmulval 10911 |
A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
โข (๐ด โ โ โ (๐ด ยท (โโ๐ด)) = (((โโ๐ด)โ2) + ((โโ๐ด)โ2))) |
|
Theorem | cjmulge0 10912 |
A complex number times its conjugate is nonnegative. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
โข (๐ด โ โ โ 0 โค (๐ด ยท (โโ๐ด))) |
|
Theorem | cjneg 10913 |
Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
โข (๐ด โ โ โ
(โโ-๐ด) =
-(โโ๐ด)) |
|
Theorem | addcj 10914 |
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 10915 |
Complex conjugate distributes over subtraction. (Contributed by NM,
28-Apr-2005.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด โ
๐ต)) =
((โโ๐ด)
โ (โโ๐ต))) |
|
Theorem | cjexp 10916 |
Complex conjugate of positive integer exponentiation. (Contributed by
NM, 7-Jun-2006.)
|
โข ((๐ด โ โ โง ๐ โ โ0) โ
(โโ(๐ดโ๐)) = ((โโ๐ด)โ๐)) |
|
Theorem | imval2 10917 |
The imaginary part of a number in terms of complex conjugate.
(Contributed by NM, 30-Apr-2005.)
|
โข (๐ด โ โ โ (โโ๐ด) = ((๐ด โ (โโ๐ด)) / (2 ยท i))) |
|
Theorem | re0 10918 |
The real part of zero. (Contributed by NM, 27-Jul-1999.)
|
โข (โโ0) = 0 |
|
Theorem | im0 10919 |
The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
|
โข (โโ0) = 0 |
|
Theorem | re1 10920 |
The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|
โข (โโ1) = 1 |
|
Theorem | im1 10921 |
The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|
โข (โโ1) = 0 |
|
Theorem | rei 10922 |
The real part of i. (Contributed by Scott Fenton,
9-Jun-2006.)
|
โข (โโi) = 0 |
|
Theorem | imi 10923 |
The imaginary part of i. (Contributed by Scott Fenton,
9-Jun-2006.)
|
โข (โโi) = 1 |
|
Theorem | cj0 10924 |
The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
|
โข (โโ0) = 0 |
|
Theorem | cji 10925 |
The complex conjugate of the imaginary unit. (Contributed by NM,
26-Mar-2005.)
|
โข (โโi) = -i |
|
Theorem | cjreim 10926 |
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 10927 |
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 10928 |
Complex conjugate is a one-to-one function. (Contributed by NM,
29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) =
(โโ๐ต) โ
๐ด = ๐ต)) |
|
Theorem | cjap 10929 |
Complex conjugate and apartness. (Contributed by Jim Kingdon,
14-Jun-2020.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) #
(โโ๐ต) โ
๐ด # ๐ต)) |
|
Theorem | cjap0 10930 |
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 10931 |
A number is nonzero iff its complex conjugate is nonzero. Also see
cjap0 10930 which is similar but for apartness.
(Contributed by NM,
29-Apr-2005.)
|
โข (๐ด โ โ โ (๐ด โ 0 โ (โโ๐ด) โ 0)) |
|
Theorem | cjdivap 10932 |
Complex conjugate distributes over division. (Contributed by Jim Kingdon,
14-Jun-2020.)
|
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต # 0) โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) |
|
Theorem | cnrecnv 10933* |
The inverse to the canonical bijection from (โ ร
โ) to โ
from cnref1o 9664. (Contributed by Mario Carneiro,
25-Aug-2014.)
|
โข ๐น = (๐ฅ โ โ, ๐ฆ โ โ โฆ (๐ฅ + (i ยท ๐ฆ))) โ โข โก๐น = (๐ง โ โ โฆ
โจ(โโ๐ง),
(โโ๐ง)โฉ) |
|
Theorem | recli 10934 |
The real part of a complex number is real (closure law). (Contributed
by NM, 11-May-1999.)
|
โข ๐ด โ โ
โ โข (โโ๐ด) โ โ |
|
Theorem | imcli 10935 |
The imaginary part of a complex number is real (closure law).
(Contributed by NM, 11-May-1999.)
|
โข ๐ด โ โ
โ โข (โโ๐ด) โ
โ |
|
Theorem | cjcli 10936 |
Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
|
โข ๐ด โ โ
โ โข (โโ๐ด) โ
โ |
|
Theorem | replimi 10937 |
Construct a complex number from its real and imaginary parts.
(Contributed by NM, 1-Oct-1999.)
|
โข ๐ด โ โ
โ โข ๐ด = ((โโ๐ด) + (i ยท (โโ๐ด))) |
|
Theorem | cjcji 10938 |
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 10939 |
A number is real iff its imaginary part is 0. (Contributed by NM,
29-May-1999.)
|
โข ๐ด โ โ
โ โข (๐ด โ โ โ (โโ๐ด) = 0) |
|
Theorem | rerebi 10940 |
A real number equals its real part. Proposition 10-3.4(f) of [Gleason]
p. 133. (Contributed by NM, 27-Oct-1999.)
|
โข ๐ด โ โ
โ โข (๐ด โ โ โ (โโ๐ด) = ๐ด) |
|
Theorem | cjrebi 10941 |
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 10942 |
Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
|
โข ๐ด โ โ
โ โข
(โโ(โโ๐ด)) = (โโ๐ด) |
|
Theorem | imcji 10943 |
Imaginary part of a complex conjugate. (Contributed by NM,
2-Oct-1999.)
|
โข ๐ด โ โ
โ โข
(โโ(โโ๐ด)) = -(โโ๐ด) |
|
Theorem | cjmulrcli 10944 |
A complex number times its conjugate is real. (Contributed by NM,
11-May-1999.)
|
โข ๐ด โ โ
โ โข (๐ด ยท (โโ๐ด)) โ โ |
|
Theorem | cjmulvali 10945 |
A complex number times its conjugate. (Contributed by NM,
2-Oct-1999.)
|
โข ๐ด โ โ
โ โข (๐ด ยท (โโ๐ด)) = (((โโ๐ด)โ2) + ((โโ๐ด)โ2)) |
|
Theorem | cjmulge0i 10946 |
A complex number times its conjugate is nonnegative. (Contributed by
NM, 28-May-1999.)
|
โข ๐ด โ โ
โ โข 0 โค (๐ด ยท (โโ๐ด)) |
|
Theorem | renegi 10947 |
Real part of negative. (Contributed by NM, 2-Aug-1999.)
|
โข ๐ด โ โ
โ โข (โโ-๐ด) = -(โโ๐ด) |
|
Theorem | imnegi 10948 |
Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
|
โข ๐ด โ โ
โ โข (โโ-๐ด) = -(โโ๐ด) |
|
Theorem | cjnegi 10949 |
Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
|
โข ๐ด โ โ
โ โข (โโ-๐ด) = -(โโ๐ด) |
|
Theorem | addcji 10950 |
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 10951 |
Real part distributes over addition. (Contributed by NM,
28-Jul-1999.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต)) |
|
Theorem | imaddi 10952 |
Imaginary part distributes over addition. (Contributed by NM,
28-Jul-1999.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต)) |
|
Theorem | remuli 10953 |
Real part of a product. (Contributed by NM, 28-Jul-1999.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต))) |
|
Theorem | immuli 10954 |
Imaginary part of a product. (Contributed by NM, 28-Jul-1999.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต))) |
|
Theorem | cjaddi 10955 |
Complex conjugate distributes over addition. Proposition 10-3.4(a) of
[Gleason] p. 133. (Contributed by NM,
28-Jul-1999.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต)) |
|
Theorem | cjmuli 10956 |
Complex conjugate distributes over multiplication. Proposition
10-3.4(c) of [Gleason] p. 133.
(Contributed by NM, 28-Jul-1999.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข (โโ(๐ด ยท ๐ต)) = ((โโ๐ด) ยท (โโ๐ต)) |
|
Theorem | ipcni 10957 |
Standard inner product on complex numbers. (Contributed by NM,
2-Oct-1999.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข (โโ(๐ด ยท (โโ๐ต))) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต))) |
|
Theorem | cjdivapi 10958 |
Complex conjugate distributes over division. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข (๐ต # 0 โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) |
|
Theorem | crrei 10959 |
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 10960 |
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 10961 |
The real part of a complex number is real (closure law). (Contributed
by Mario Carneiro, 29-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ (โโ๐ด) โ โ) |
|
Theorem | imcld 10962 |
The imaginary part of a complex number is real (closure law).
(Contributed by Mario Carneiro, 29-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ (โโ๐ด) โ โ) |
|
Theorem | cjcld 10963 |
Closure law for complex conjugate. (Contributed by Mario Carneiro,
29-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ (โโ๐ด) โ โ) |
|
Theorem | replimd 10964 |
Construct a complex number from its real and imaginary parts.
(Contributed by Mario Carneiro, 29-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ ๐ด = ((โโ๐ด) + (i ยท (โโ๐ด)))) |
|
Theorem | remimd 10965 |
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 10966 |
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 10967 |
A number is real iff its imaginary part is 0. (Contributed by Mario
Carneiro, 29-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ (โโ๐ด) = 0)
โ โข (๐ โ ๐ด โ โ) |
|
Theorem | rerebd 10968 |
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 10969 |
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 10970 |
A number which is nonzero has a complex conjugate which is nonzero.
Also see cjap0d 10971 which is similar but for apartness.
(Contributed by
Mario Carneiro, 29-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (โโ๐ด) โ 0) |
|
Theorem | cjap0d 10971 |
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 10972 |
Real part of a complex conjugate. (Contributed by Mario Carneiro,
29-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ (โโ(โโ๐ด)) = (โโ๐ด)) |
|
Theorem | imcjd 10973 |
Imaginary part of a complex conjugate. (Contributed by Mario Carneiro,
29-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ
(โโ(โโ๐ด)) = -(โโ๐ด)) |
|
Theorem | cjmulrcld 10974 |
A complex number times its conjugate is real. (Contributed by Mario
Carneiro, 29-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ (๐ด ยท (โโ๐ด)) โ โ) |
|
Theorem | cjmulvald 10975 |
A complex number times its conjugate. (Contributed by Mario Carneiro,
29-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ (๐ด ยท (โโ๐ด)) = (((โโ๐ด)โ2) + ((โโ๐ด)โ2))) |
|
Theorem | cjmulge0d 10976 |
A complex number times its conjugate is nonnegative. (Contributed by
Mario Carneiro, 29-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ 0 โค (๐ด ยท (โโ๐ด))) |
|
Theorem | renegd 10977 |
Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ (โโ-๐ด) = -(โโ๐ด)) |
|
Theorem | imnegd 10978 |
Imaginary part of negative. (Contributed by Mario Carneiro,
29-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ (โโ-๐ด) = -(โโ๐ด)) |
|
Theorem | cjnegd 10979 |
Complex conjugate of negative. (Contributed by Mario Carneiro,
29-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ (โโ-๐ด) = -(โโ๐ด)) |
|
Theorem | addcjd 10980 |
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 10981 |
Complex conjugate of positive integer exponentiation. (Contributed by
Mario Carneiro, 29-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ
โ0) โ โข (๐ โ (โโ(๐ดโ๐)) = ((โโ๐ด)โ๐)) |
|
Theorem | readdd 10982 |
Real part distributes over addition. (Contributed by Mario Carneiro,
29-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต))) |
|
Theorem | imaddd 10983 |
Imaginary part distributes over addition. (Contributed by Mario
Carneiro, 29-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต))) |
|
Theorem | resubd 10984 |
Real part distributes over subtraction. (Contributed by Mario Carneiro,
29-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (โโ(๐ด โ ๐ต)) = ((โโ๐ด) โ (โโ๐ต))) |
|
Theorem | imsubd 10985 |
Imaginary part distributes over subtraction. (Contributed by Mario
Carneiro, 29-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (โโ(๐ด โ ๐ต)) = ((โโ๐ด) โ (โโ๐ต))) |
|
Theorem | remuld 10986 |
Real part of a product. (Contributed by Mario Carneiro,
29-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต)))) |
|
Theorem | immuld 10987 |
Imaginary part of a product. (Contributed by Mario Carneiro,
29-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))) |
|
Theorem | cjaddd 10988 |
Complex conjugate distributes over addition. Proposition 10-3.4(a) of
[Gleason] p. 133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต))) |
|
Theorem | cjmuld 10989 |
Complex conjugate distributes over multiplication. Proposition
10-3.4(c) of [Gleason] p. 133.
(Contributed by Mario Carneiro,
29-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = ((โโ๐ด) ยท (โโ๐ต))) |
|
Theorem | ipcnd 10990 |
Standard inner product on complex numbers. (Contributed by Mario
Carneiro, 29-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (โโ(๐ด ยท (โโ๐ต))) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))) |
|
Theorem | cjdivapd 10991 |
Complex conjugate distributes over division. (Contributed by Jim
Kingdon, 15-Jun-2020.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต # 0) โ โข (๐ โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) |
|
Theorem | rered 10992 |
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 10993 |
The imaginary part of a real number is 0. (Contributed by Mario
Carneiro, 29-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ (โโ๐ด) = 0) |
|
Theorem | cjred 10994 |
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 10995 |
Real part of a product. (Contributed by Mario Carneiro,
29-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (๐ด ยท (โโ๐ต))) |
|
Theorem | immul2d 10996 |
Imaginary part of a product. (Contributed by Mario Carneiro,
29-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (๐ด ยท (โโ๐ต))) |
|
Theorem | redivapd 10997 |
Real part of a division. Related to remul2 10896. (Contributed by Jim
Kingdon, 15-Jun-2020.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด # 0) โ โข (๐ โ (โโ(๐ต / ๐ด)) = ((โโ๐ต) / ๐ด)) |
|
Theorem | imdivapd 10998 |
Imaginary part of a division. Related to remul2 10896. (Contributed by
Jim Kingdon, 15-Jun-2020.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด # 0) โ โข (๐ โ (โโ(๐ต / ๐ด)) = ((โโ๐ต) / ๐ด)) |
|
Theorem | crred 10999 |
The real part of a complex number representation. Definition 10-3.1 of
[Gleason] p. 132. (Contributed by Mario
Carneiro, 29-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (โโ(๐ด + (i ยท ๐ต))) = ๐ด) |
|
Theorem | crimd 11000 |
The imaginary part of a complex number representation. Definition
10-3.1 of [Gleason] p. 132.
(Contributed by Mario Carneiro,
29-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (โโ(๐ด + (i ยท ๐ต))) = ๐ต) |