Theorem List for Intuitionistic Logic Explorer - 9701-9800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 4bc2eq6 9701 |
The value of four choose two. (Contributed by Scott Fenton,
9-Jan-2017.)
|
|
|
3.7 Elementary real and complex
functions
|
|
3.7.1 The "shift" operation
|
|
Syntax | cshi 9702 |
Extend class notation with function shifter.
|
|
|
Definition | df-shft 9703* |
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 9713 for its value. (Contributed by NM,
20-Jul-2005.)
|
|
|
Theorem | shftlem 9704* |
Two ways to write a shifted set . (Contributed by Mario
Carneiro, 3-Nov-2013.)
|
|
|
Theorem | shftuz 9705* |
A shift of the upper integers. (Contributed by Mario Carneiro,
5-Nov-2013.)
|
|
|
Theorem | shftfvalg 9706* |
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.)
|
|
|
Theorem | ovshftex 9707 |
Existence of the result of applying shift. (Contributed by Jim Kingdon,
15-Aug-2021.)
|
|
|
Theorem | shftfibg 9708 |
Value of a fiber of the relation . (Contributed by Jim Kingdon,
15-Aug-2021.)
|
|
|
Theorem | shftfval 9709* |
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.)
|
|
|
Theorem | shftdm 9710* |
Domain of a relation shifted by . The set on the right is more
commonly notated as
(meaning add to every
element of ).
(Contributed by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | shftfib 9711 |
Value of a fiber of the relation . (Contributed by Mario
Carneiro, 4-Nov-2013.)
|
|
|
Theorem | shftfn 9712* |
Functionality and domain of a sequence shifted by . (Contributed
by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | shftval 9713 |
Value of a sequence shifted by . (Contributed by NM,
20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.)
|
|
|
Theorem | shftval2 9714 |
Value of a sequence shifted by . (Contributed by NM,
20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | shftval3 9715 |
Value of a sequence shifted by . (Contributed by NM,
20-Jul-2005.)
|
|
|
Theorem | shftval4 9716 |
Value of a sequence shifted by .
(Contributed by NM,
18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | shftval5 9717 |
Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | shftf 9718* |
Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | 2shfti 9719 |
Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised
by Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | shftidt2 9720 |
Identity law for the shift operation. (Contributed by Mario Carneiro,
5-Nov-2013.)
|
|
|
Theorem | shftidt 9721 |
Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | shftcan1 9722 |
Cancellation law for the shift operation. (Contributed by NM,
4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | shftcan2 9723 |
Cancellation law for the shift operation. (Contributed by NM,
4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | shftvalg 9724 |
Value of a sequence shifted by . (Contributed by Scott Fenton,
16-Dec-2017.)
|
|
|
Theorem | shftval4g 9725 |
Value of a sequence shifted by .
(Contributed by Jim Kingdon,
19-Aug-2021.)
|
|
|
3.7.2 Real and imaginary parts;
conjugate
|
|
Syntax | ccj 9726 |
Extend class notation to include complex conjugate function.
|
|
|
Syntax | cre 9727 |
Extend class notation to include real part of a complex number.
|
|
|
Syntax | cim 9728 |
Extend class notation to include imaginary part of a complex number.
|
|
|
Definition | df-cj 9729* |
Define the complex conjugate function. See cjcli 9800 for its closure and
cjval 9732 for its value. (Contributed by NM,
9-May-1999.) (Revised by
Mario Carneiro, 6-Nov-2013.)
|
|
|
Definition | df-re 9730 |
Define a function whose value is the real part of a complex number. See
reval 9736 for its value, recli 9798 for its closure, and replim 9746 for its use
in decomposing a complex number. (Contributed by NM, 9-May-1999.)
|
|
|
Definition | df-im 9731 |
Define a function whose value is the imaginary part of a complex number.
See imval 9737 for its value, imcli 9799 for its closure, and replim 9746 for its
use in decomposing a complex number. (Contributed by NM,
9-May-1999.)
|
|
|
Theorem | cjval 9732* |
The value of the conjugate of a complex number. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
|
|
Theorem | cjth 9733 |
The defining property of the complex conjugate. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
|
|
Theorem | cjf 9734 |
Domain and codomain of the conjugate function. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
|
|
Theorem | cjcl 9735 |
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 9736 |
The value of the real part of a complex number. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
|
|
Theorem | imval 9737 |
The value of the imaginary part of a complex number. (Contributed by
NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
|
|
Theorem | imre 9738 |
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.)
|
|
|
Theorem | reim 9739 |
The real part of a complex number in terms of the imaginary part
function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|
|
|
Theorem | recl 9740 |
The real part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
|
|
Theorem | imcl 9741 |
The imaginary part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
|
|
Theorem | ref 9742 |
Domain and codomain of the real part function. (Contributed by Paul
Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
|
|
Theorem | imf 9743 |
Domain and codomain of the imaginary part function. (Contributed by
Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
|
|
Theorem | crre 9744 |
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.)
|
|
|
Theorem | crim 9745 |
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.)
|
|
|
Theorem | replim 9746 |
Reconstruct a complex number from its real and imaginary parts.
(Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro,
7-Nov-2013.)
|
|
|
Theorem | remim 9747 |
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 NM, 10-May-1999.) (Revised by Mario Carneiro,
7-Nov-2013.)
|
|
|
Theorem | reim0 9748 |
The imaginary part of a real number is 0. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
|
|
|
Theorem | reim0b 9749 |
A number is real iff its imaginary part is 0. (Contributed by NM,
26-Sep-2005.)
|
|
|
Theorem | rereb 9750 |
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 9751 |
A product with a real multiplier apart from zero is real iff the
multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.)
|
#
|
|
Theorem | rere 9752 |
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 9753 |
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 9754 |
Real part of a complex conjugate. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
|
|
Theorem | reneg 9755 |
Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by
Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | readd 9756 |
Real part distributes over addition. (Contributed by NM, 17-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | resub 9757 |
Real part distributes over subtraction. (Contributed by NM,
17-Mar-2005.)
|
|
|
Theorem | remullem 9758 |
Lemma for remul 9759, immul 9766, and cjmul 9772. (Contributed by NM,
28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | remul 9759 |
Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by
Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | remul2 9760 |
Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
|
|
|
Theorem | redivap 9761 |
Real part of a division. Related to remul2 9760. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
# |
|
Theorem | imcj 9762 |
Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | imneg 9763 |
The imaginary part of a negative number. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | imadd 9764 |
Imaginary part distributes over addition. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | imsub 9765 |
Imaginary part distributes over subtraction. (Contributed by NM,
18-Mar-2005.)
|
|
|
Theorem | immul 9766 |
Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised
by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | immul2 9767 |
Imaginary part of a product. (Contributed by Mario Carneiro,
2-Aug-2014.)
|
|
|
Theorem | imdivap 9768 |
Imaginary part of a division. Related to immul2 9767. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
# |
|
Theorem | cjre 9769 |
A real number equals its complex conjugate. Proposition 10-3.4(f) of
[Gleason] p. 133. (Contributed by NM,
8-Oct-1999.)
|
|
|
Theorem | cjcj 9770 |
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 9771 |
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 9772 |
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 9773 |
Standard inner product on complex numbers. (Contributed by NM,
29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | cjmulrcl 9774 |
A complex number times its conjugate is real. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | cjmulval 9775 |
A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | cjmulge0 9776 |
A complex number times its conjugate is nonnegative. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | cjneg 9777 |
Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | addcj 9778 |
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 9779 |
Complex conjugate distributes over subtraction. (Contributed by NM,
28-Apr-2005.)
|
|
|
Theorem | cjexp 9780 |
Complex conjugate of positive integer exponentiation. (Contributed by
NM, 7-Jun-2006.)
|
|
|
Theorem | imval2 9781 |
The imaginary part of a number in terms of complex conjugate.
(Contributed by NM, 30-Apr-2005.)
|
|
|
Theorem | re0 9782 |
The real part of zero. (Contributed by NM, 27-Jul-1999.)
|
|
|
Theorem | im0 9783 |
The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
|
|
|
Theorem | re1 9784 |
The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|
|
|
Theorem | im1 9785 |
The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|
|
|
Theorem | rei 9786 |
The real part of .
(Contributed by Scott Fenton, 9-Jun-2006.)
|
|
|
Theorem | imi 9787 |
The imaginary part of . (Contributed by Scott Fenton,
9-Jun-2006.)
|
|
|
Theorem | cj0 9788 |
The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
|
|
|
Theorem | cji 9789 |
The complex conjugate of the imaginary unit. (Contributed by NM,
26-Mar-2005.)
|
|
|
Theorem | cjreim 9790 |
The conjugate of a representation of a complex number in terms of real and
imaginary parts. (Contributed by NM, 1-Jul-2005.)
|
|
|
Theorem | cjreim2 9791 |
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 9792 |
Complex conjugate is a one-to-one function. (Contributed by NM,
29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.)
|
|
|
Theorem | cjap 9793 |
Complex conjugate and apartness. (Contributed by Jim Kingdon,
14-Jun-2020.)
|
# # |
|
Theorem | cjap0 9794 |
A number is apart from zero iff its complex conjugate is apart from zero.
(Contributed by Jim Kingdon, 14-Jun-2020.)
|
# #
|
|
Theorem | cjne0 9795 |
A number is nonzero iff its complex conjugate is nonzero. Also see
cjap0 9794 which is similar but for apartness.
(Contributed by NM,
29-Apr-2005.)
|
|
|
Theorem | cjdivap 9796 |
Complex conjugate distributes over division. (Contributed by Jim Kingdon,
14-Jun-2020.)
|
# |
|
Theorem | cnrecnv 9797* |
The inverse to the canonical bijection from
to
from cnref1o 8733. (Contributed by Mario Carneiro,
25-Aug-2014.)
|
|
|
Theorem | recli 9798 |
The real part of a complex number is real (closure law). (Contributed
by NM, 11-May-1999.)
|
|
|
Theorem | imcli 9799 |
The imaginary part of a complex number is real (closure law).
(Contributed by NM, 11-May-1999.)
|
|
|
Theorem | cjcli 9800 |
Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
|
|