Theorem List for Intuitionistic Logic Explorer - 10601-10700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | redivap 10601 |
Real part of a division. Related to remul2 10600. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
# |
|
Theorem | imcj 10602 |
Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | imneg 10603 |
The imaginary part of a negative number. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | imadd 10604 |
Imaginary part distributes over addition. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | imsub 10605 |
Imaginary part distributes over subtraction. (Contributed by NM,
18-Mar-2005.)
|
|
|
Theorem | immul 10606 |
Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised
by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | immul2 10607 |
Imaginary part of a product. (Contributed by Mario Carneiro,
2-Aug-2014.)
|
|
|
Theorem | imdivap 10608 |
Imaginary part of a division. Related to immul2 10607. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
# |
|
Theorem | cjre 10609 |
A real number equals its complex conjugate. Proposition 10-3.4(f) of
[Gleason] p. 133. (Contributed by NM,
8-Oct-1999.)
|
|
|
Theorem | cjcj 10610 |
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 10611 |
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 10612 |
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 10613 |
Standard inner product on complex numbers. (Contributed by NM,
29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | cjmulrcl 10614 |
A complex number times its conjugate is real. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | cjmulval 10615 |
A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | cjmulge0 10616 |
A complex number times its conjugate is nonnegative. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | cjneg 10617 |
Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | addcj 10618 |
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.)
|
|
|
Theorem | cjsub 10619 |
Complex conjugate distributes over subtraction. (Contributed by NM,
28-Apr-2005.)
|
|
|
Theorem | cjexp 10620 |
Complex conjugate of positive integer exponentiation. (Contributed by
NM, 7-Jun-2006.)
|
|
|
Theorem | imval2 10621 |
The imaginary part of a number in terms of complex conjugate.
(Contributed by NM, 30-Apr-2005.)
|
|
|
Theorem | re0 10622 |
The real part of zero. (Contributed by NM, 27-Jul-1999.)
|
|
|
Theorem | im0 10623 |
The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
|
|
|
Theorem | re1 10624 |
The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|
|
|
Theorem | im1 10625 |
The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|
|
|
Theorem | rei 10626 |
The real part of .
(Contributed by Scott Fenton, 9-Jun-2006.)
|
|
|
Theorem | imi 10627 |
The imaginary part of . (Contributed by Scott Fenton,
9-Jun-2006.)
|
|
|
Theorem | cj0 10628 |
The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
|
|
|
Theorem | cji 10629 |
The complex conjugate of the imaginary unit. (Contributed by NM,
26-Mar-2005.)
|
|
|
Theorem | cjreim 10630 |
The conjugate of a representation of a complex number in terms of real and
imaginary parts. (Contributed by NM, 1-Jul-2005.)
|
|
|
Theorem | cjreim2 10631 |
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.)
|
|
|
Theorem | cj11 10632 |
Complex conjugate is a one-to-one function. (Contributed by NM,
29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.)
|
|
|
Theorem | cjap 10633 |
Complex conjugate and apartness. (Contributed by Jim Kingdon,
14-Jun-2020.)
|
# # |
|
Theorem | cjap0 10634 |
A number is apart from zero iff its complex conjugate is apart from zero.
(Contributed by Jim Kingdon, 14-Jun-2020.)
|
# #
|
|
Theorem | cjne0 10635 |
A number is nonzero iff its complex conjugate is nonzero. Also see
cjap0 10634 which is similar but for apartness.
(Contributed by NM,
29-Apr-2005.)
|
|
|
Theorem | cjdivap 10636 |
Complex conjugate distributes over division. (Contributed by Jim Kingdon,
14-Jun-2020.)
|
# |
|
Theorem | cnrecnv 10637* |
The inverse to the canonical bijection from
to
from cnref1o 9396. (Contributed by Mario Carneiro,
25-Aug-2014.)
|
|
|
Theorem | recli 10638 |
The real part of a complex number is real (closure law). (Contributed
by NM, 11-May-1999.)
|
|
|
Theorem | imcli 10639 |
The imaginary part of a complex number is real (closure law).
(Contributed by NM, 11-May-1999.)
|
|
|
Theorem | cjcli 10640 |
Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
|
|
|
Theorem | replimi 10641 |
Construct a complex number from its real and imaginary parts.
(Contributed by NM, 1-Oct-1999.)
|
|
|
Theorem | cjcji 10642 |
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 10643 |
A number is real iff its imaginary part is 0. (Contributed by NM,
29-May-1999.)
|
|
|
Theorem | rerebi 10644 |
A real number equals its real part. Proposition 10-3.4(f) of [Gleason]
p. 133. (Contributed by NM, 27-Oct-1999.)
|
|
|
Theorem | cjrebi 10645 |
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 10646 |
Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
|
|
|
Theorem | imcji 10647 |
Imaginary part of a complex conjugate. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | cjmulrcli 10648 |
A complex number times its conjugate is real. (Contributed by NM,
11-May-1999.)
|
|
|
Theorem | cjmulvali 10649 |
A complex number times its conjugate. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | cjmulge0i 10650 |
A complex number times its conjugate is nonnegative. (Contributed by
NM, 28-May-1999.)
|
|
|
Theorem | renegi 10651 |
Real part of negative. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | imnegi 10652 |
Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | cjnegi 10653 |
Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | addcji 10654 |
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.)
|
|
|
Theorem | readdi 10655 |
Real part distributes over addition. (Contributed by NM,
28-Jul-1999.)
|
|
|
Theorem | imaddi 10656 |
Imaginary part distributes over addition. (Contributed by NM,
28-Jul-1999.)
|
|
|
Theorem | remuli 10657 |
Real part of a product. (Contributed by NM, 28-Jul-1999.)
|
|
|
Theorem | immuli 10658 |
Imaginary part of a product. (Contributed by NM, 28-Jul-1999.)
|
|
|
Theorem | cjaddi 10659 |
Complex conjugate distributes over addition. Proposition 10-3.4(a) of
[Gleason] p. 133. (Contributed by NM,
28-Jul-1999.)
|
|
|
Theorem | cjmuli 10660 |
Complex conjugate distributes over multiplication. Proposition
10-3.4(c) of [Gleason] p. 133.
(Contributed by NM, 28-Jul-1999.)
|
|
|
Theorem | ipcni 10661 |
Standard inner product on complex numbers. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | cjdivapi 10662 |
Complex conjugate distributes over division. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
# |
|
Theorem | crrei 10663 |
The real part of a complex number representation. Definition 10-3.1 of
[Gleason] p. 132. (Contributed by NM,
10-May-1999.)
|
|
|
Theorem | crimi 10664 |
The imaginary part of a complex number representation. Definition
10-3.1 of [Gleason] p. 132.
(Contributed by NM, 10-May-1999.)
|
|
|
Theorem | recld 10665 |
The real part of a complex number is real (closure law). (Contributed
by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | imcld 10666 |
The imaginary part of a complex number is real (closure law).
(Contributed by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | cjcld 10667 |
Closure law for complex conjugate. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | replimd 10668 |
Construct a complex number from its real and imaginary parts.
(Contributed by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | remimd 10669 |
Value of the conjugate of a complex number. The value is the real part
minus times
the imaginary part. Definition 10-3.2 of [Gleason]
p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | cjcjd 10670 |
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 10671 |
A number is real iff its imaginary part is 0. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | rerebd 10672 |
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 10673 |
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 10674 |
A number which is nonzero has a complex conjugate which is nonzero.
Also see cjap0d 10675 which is similar but for apartness.
(Contributed by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | cjap0d 10675 |
A number which is apart from zero has a complex conjugate which is
apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.)
|
# # |
|
Theorem | recjd 10676 |
Real part of a complex conjugate. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | imcjd 10677 |
Imaginary part of a complex conjugate. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | cjmulrcld 10678 |
A complex number times its conjugate is real. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | cjmulvald 10679 |
A complex number times its conjugate. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | cjmulge0d 10680 |
A complex number times its conjugate is nonnegative. (Contributed by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | renegd 10681 |
Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | imnegd 10682 |
Imaginary part of negative. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | cjnegd 10683 |
Complex conjugate of negative. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | addcjd 10684 |
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.)
|
|
|
Theorem | cjexpd 10685 |
Complex conjugate of positive integer exponentiation. (Contributed by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | readdd 10686 |
Real part distributes over addition. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | imaddd 10687 |
Imaginary part distributes over addition. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | resubd 10688 |
Real part distributes over subtraction. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | imsubd 10689 |
Imaginary part distributes over subtraction. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | remuld 10690 |
Real part of a product. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | immuld 10691 |
Imaginary part of a product. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | cjaddd 10692 |
Complex conjugate distributes over addition. Proposition 10-3.4(a) of
[Gleason] p. 133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | cjmuld 10693 |
Complex conjugate distributes over multiplication. Proposition
10-3.4(c) of [Gleason] p. 133.
(Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | ipcnd 10694 |
Standard inner product on complex numbers. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | cjdivapd 10695 |
Complex conjugate distributes over division. (Contributed by Jim
Kingdon, 15-Jun-2020.)
|
#
|
|
Theorem | rered 10696 |
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 10697 |
The imaginary part of a real number is 0. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | cjred 10698 |
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 10699 |
Real part of a product. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | immul2d 10700 |
Imaginary part of a product. (Contributed by Mario Carneiro,
29-May-2016.)
|
|