Theorem List for Intuitionistic Logic Explorer - 10701-10800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | fihashen1 10701 |
A finite set has size 1 if and only if it is equinumerous to the ordinal
1. (Contributed by AV, 14-Apr-2019.) (Intuitionized by Jim Kingdon,
23-Feb-2022.)
|
♯
|
|
Theorem | fihashfn 10702 |
A function on a finite set is equinumerous to its domain. (Contributed by
Mario Carneiro, 12-Mar-2015.) (Intuitionized by Jim Kingdon,
24-Feb-2022.)
|
♯ ♯ |
|
Theorem | fseq1hash 10703 |
The value of the size function on a finite 1-based sequence. (Contributed
by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro,
12-Mar-2015.)
|
♯ |
|
Theorem | omgadd 10704 |
Mapping ordinal addition to integer addition. (Contributed by Jim
Kingdon, 24-Feb-2022.)
|
frec
|
|
Theorem | fihashdom 10705 |
Dominance relation for the size function. (Contributed by Jim Kingdon,
24-Feb-2022.)
|
♯ ♯ |
|
Theorem | hashunlem 10706 |
Lemma for hashun 10707. Ordinal size of the union. (Contributed
by Jim
Kingdon, 25-Feb-2022.)
|
|
|
Theorem | hashun 10707 |
The size of the union of disjoint finite sets is the sum of their sizes.
(Contributed by Paul Chapman, 30-Nov-2012.) (Revised by Mario Carneiro,
15-Sep-2013.)
|
♯
♯ ♯ |
|
Theorem | 1elfz0hash 10708 |
1 is an element of the finite set of sequential nonnegative integers
bounded by the size of a nonempty finite set. (Contributed by AV,
9-May-2020.)
|
♯ |
|
Theorem | hashunsng 10709 |
The size of the union of a finite set with a disjoint singleton is one
more than the size of the set. (Contributed by Paul Chapman,
30-Nov-2012.)
|
♯ ♯ |
|
Theorem | hashprg 10710 |
The size of an unordered pair. (Contributed by Mario Carneiro,
27-Sep-2013.) (Revised by Mario Carneiro, 5-May-2016.) (Revised by AV,
18-Sep-2021.)
|
♯ |
|
Theorem | prhash2ex 10711 |
There is (at least) one set with two different elements: the unordered
pair containing and
. In contrast to pr0hash2ex 10717, numbers
are used instead of sets because their representation is shorter (and more
comprehensive). (Contributed by AV, 29-Jan-2020.)
|
♯ |
|
Theorem | hashp1i 10712 |
Size of a natural number ordinal. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
♯
♯ |
|
Theorem | hash1 10713 |
Size of a natural number ordinal. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
♯ |
|
Theorem | hash2 10714 |
Size of a natural number ordinal. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
♯ |
|
Theorem | hash3 10715 |
Size of a natural number ordinal. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
♯ |
|
Theorem | hash4 10716 |
Size of a natural number ordinal. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
♯ |
|
Theorem | pr0hash2ex 10717 |
There is (at least) one set with two different elements: the unordered
pair containing the empty set and the singleton containing the empty set.
(Contributed by AV, 29-Jan-2020.)
|
♯ |
|
Theorem | fihashss 10718 |
The size of a subset is less than or equal to the size of its superset.
(Contributed by Alexander van der Vekens, 14-Jul-2018.)
|
♯ ♯ |
|
Theorem | fiprsshashgt1 10719 |
The size of a superset of a proper unordered pair is greater than 1.
(Contributed by AV, 6-Feb-2021.)
|
♯ |
|
Theorem | fihashssdif 10720 |
The size of the difference of a finite set and a finite subset is the
set's size minus the subset's. (Contributed by Jim Kingdon,
31-May-2022.)
|
♯ ♯ ♯ |
|
Theorem | hashdifsn 10721 |
The size of the difference of a finite set and a singleton subset is the
set's size minus 1. (Contributed by Alexander van der Vekens,
6-Jan-2018.)
|
♯ ♯ |
|
Theorem | hashdifpr 10722 |
The size of the difference of a finite set and a proper ordered pair
subset is the set's size minus 2. (Contributed by AV, 16-Dec-2020.)
|
♯ ♯ |
|
Theorem | hashfz 10723 |
Value of the numeric cardinality of a nonempty integer range.
(Contributed by Stefan O'Rear, 12-Sep-2014.) (Proof shortened by Mario
Carneiro, 15-Apr-2015.)
|
♯
|
|
Theorem | hashfzo 10724 |
Cardinality of a half-open set of integers. (Contributed by Stefan
O'Rear, 15-Aug-2015.)
|
♯..^
|
|
Theorem | hashfzo0 10725 |
Cardinality of a half-open set of integers based at zero. (Contributed by
Stefan O'Rear, 15-Aug-2015.)
|
♯..^
|
|
Theorem | hashfzp1 10726 |
Value of the numeric cardinality of a (possibly empty) integer range.
(Contributed by AV, 19-Jun-2021.)
|
♯ |
|
Theorem | hashfz0 10727 |
Value of the numeric cardinality of a nonempty range of nonnegative
integers. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
|
♯ |
|
Theorem | hashxp 10728 |
The size of the Cartesian product of two finite sets is the product of
their sizes. (Contributed by Paul Chapman, 30-Nov-2012.)
|
♯ ♯ ♯ |
|
Theorem | fimaxq 10729* |
A finite set of rational numbers has a maximum. (Contributed by Jim
Kingdon, 6-Sep-2022.)
|
|
|
Theorem | resunimafz0 10730 |
The union of a restriction by an image over an open range of nonnegative
integers and a singleton of an ordered pair is a restriction by an image
over an interval of nonnegative integers. (Contributed by Mario
Carneiro, 8-Apr-2015.) (Revised by AV, 20-Feb-2021.)
|
..^♯ ..^♯
..^ |
|
Theorem | fnfz0hash 10731 |
The size of a function on a finite set of sequential nonnegative integers.
(Contributed by Alexander van der Vekens, 25-Jun-2018.)
|
♯ |
|
Theorem | ffz0hash 10732 |
The size of a function on a finite set of sequential nonnegative integers
equals the upper bound of the sequence increased by 1. (Contributed by
Alexander van der Vekens, 15-Mar-2018.) (Proof shortened by AV,
11-Apr-2021.)
|
♯ |
|
Theorem | ffzo0hash 10733 |
The size of a function on a half-open range of nonnegative integers.
(Contributed by Alexander van der Vekens, 25-Mar-2018.)
|
..^ ♯ |
|
Theorem | fnfzo0hash 10734 |
The size of a function on a half-open range of nonnegative integers equals
the upper bound of this range. (Contributed by Alexander van der Vekens,
26-Jan-2018.) (Proof shortened by AV, 11-Apr-2021.)
|
..^ ♯ |
|
Theorem | hashfacen 10735* |
The number of bijections between two sets is a cardinal invariant.
(Contributed by Mario Carneiro, 21-Jan-2015.)
|
|
|
Theorem | leisorel 10736 |
Version of isorel 5770 for strictly increasing functions on the
reals.
(Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro,
9-Sep-2015.)
|
|
|
Theorem | zfz1isolemsplit 10737 |
Lemma for zfz1iso 10740. Removing one element from an integer
range.
(Contributed by Jim Kingdon, 8-Sep-2022.)
|
♯
♯ ♯ |
|
Theorem | zfz1isolemiso 10738* |
Lemma for zfz1iso 10740. Adding one element to the order
isomorphism.
(Contributed by Jim Kingdon, 8-Sep-2022.)
|
♯ ♯ ♯ ♯
♯
|
|
Theorem | zfz1isolem1 10739* |
Lemma for zfz1iso 10740. Existence of an order isomorphism given
the
existence of shorter isomorphisms. (Contributed by Jim Kingdon,
7-Sep-2022.)
|
♯
♯ |
|
Theorem | zfz1iso 10740* |
A finite set of integers has an order isomorphism to a one-based finite
sequence. (Contributed by Jim Kingdon, 3-Sep-2022.)
|
♯ |
|
Theorem | seq3coll 10741* |
The function contains
a sparse set of nonzero values to be summed.
The function
is an order isomorphism from the set of nonzero
values of to a
1-based finite sequence, and collects these
nonzero values together. Under these conditions, the sum over the
values in
yields the same result as the sum over the original set
. (Contributed
by Mario Carneiro, 2-Apr-2014.) (Revised by Jim
Kingdon, 9-Apr-2023.)
|
♯ ♯
♯
♯
|
|
4.7 Elementary real and complex
functions
|
|
4.7.1 The "shift" operation
|
|
Syntax | cshi 10742 |
Extend class notation with function shifter.
|
|
|
Definition | df-shft 10743* |
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 10753 for its value. (Contributed by NM,
20-Jul-2005.)
|
|
|
Theorem | shftlem 10744* |
Two ways to write a shifted set . (Contributed by Mario
Carneiro, 3-Nov-2013.)
|
|
|
Theorem | shftuz 10745* |
A shift of the upper integers. (Contributed by Mario Carneiro,
5-Nov-2013.)
|
|
|
Theorem | shftfvalg 10746* |
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 10747 |
Existence of the result of applying shift. (Contributed by Jim Kingdon,
15-Aug-2021.)
|
|
|
Theorem | shftfibg 10748 |
Value of a fiber of the relation . (Contributed by Jim Kingdon,
15-Aug-2021.)
|
|
|
Theorem | shftfval 10749* |
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 10750* |
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 10751 |
Value of a fiber of the relation . (Contributed by Mario
Carneiro, 4-Nov-2013.)
|
|
|
Theorem | shftfn 10752* |
Functionality and domain of a sequence shifted by . (Contributed
by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | shftval 10753 |
Value of a sequence shifted by . (Contributed by NM,
20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.)
|
|
|
Theorem | shftval2 10754 |
Value of a sequence shifted by . (Contributed by NM,
20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | shftval3 10755 |
Value of a sequence shifted by . (Contributed by NM,
20-Jul-2005.)
|
|
|
Theorem | shftval4 10756 |
Value of a sequence shifted by .
(Contributed by NM,
18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | shftval5 10757 |
Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | shftf 10758* |
Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | 2shfti 10759 |
Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised
by Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | shftidt2 10760 |
Identity law for the shift operation. (Contributed by Mario Carneiro,
5-Nov-2013.)
|
|
|
Theorem | shftidt 10761 |
Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | shftcan1 10762 |
Cancellation law for the shift operation. (Contributed by NM,
4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | shftcan2 10763 |
Cancellation law for the shift operation. (Contributed by NM,
4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | shftvalg 10764 |
Value of a sequence shifted by . (Contributed by Scott Fenton,
16-Dec-2017.)
|
|
|
Theorem | shftval4g 10765 |
Value of a sequence shifted by .
(Contributed by Jim Kingdon,
19-Aug-2021.)
|
|
|
Theorem | seq3shft 10766* |
Shifting the index set of a sequence. (Contributed by NM, 17-Mar-2005.)
(Revised by Jim Kingdon, 17-Oct-2022.)
|
|
|
4.7.2 Real and imaginary parts;
conjugate
|
|
Syntax | ccj 10767 |
Extend class notation to include complex conjugate function.
|
|
|
Syntax | cre 10768 |
Extend class notation to include real part of a complex number.
|
|
|
Syntax | cim 10769 |
Extend class notation to include imaginary part of a complex number.
|
|
|
Definition | df-cj 10770* |
Define the complex conjugate function. See cjcli 10841 for its closure and
cjval 10773 for its value. (Contributed by NM,
9-May-1999.) (Revised by
Mario Carneiro, 6-Nov-2013.)
|
|
|
Definition | df-re 10771 |
Define a function whose value is the real part of a complex number. See
reval 10777 for its value, recli 10839 for its closure, and replim 10787 for its use
in decomposing a complex number. (Contributed by NM, 9-May-1999.)
|
|
|
Definition | df-im 10772 |
Define a function whose value is the imaginary part of a complex number.
See imval 10778 for its value, imcli 10840 for its closure, and replim 10787 for its
use in decomposing a complex number. (Contributed by NM,
9-May-1999.)
|
|
|
Theorem | cjval 10773* |
The value of the conjugate of a complex number. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
|
|
Theorem | cjth 10774 |
The defining property of the complex conjugate. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
|
|
Theorem | cjf 10775 |
Domain and codomain of the conjugate function. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
|
|
Theorem | cjcl 10776 |
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 10777 |
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 10778 |
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 10779 |
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 10780 |
The real part of a complex number in terms of the imaginary part
function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|
|
|
Theorem | recl 10781 |
The real part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
|
|
Theorem | imcl 10782 |
The imaginary part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
|
|
Theorem | ref 10783 |
Domain and codomain of the real part function. (Contributed by Paul
Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
|
|
Theorem | imf 10784 |
Domain and codomain of the imaginary part function. (Contributed by
Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
|
|
Theorem | crre 10785 |
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 10786 |
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 10787 |
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 10788 |
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 10789 |
The imaginary part of a real number is 0. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
|
|
|
Theorem | reim0b 10790 |
A number is real iff its imaginary part is 0. (Contributed by NM,
26-Sep-2005.)
|
|
|
Theorem | rereb 10791 |
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 10792 |
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 10793 |
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 10794 |
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 10795 |
Real part of a complex conjugate. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
|
|
Theorem | reneg 10796 |
Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by
Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | readd 10797 |
Real part distributes over addition. (Contributed by NM, 17-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | resub 10798 |
Real part distributes over subtraction. (Contributed by NM,
17-Mar-2005.)
|
|
|
Theorem | remullem 10799 |
Lemma for remul 10800, immul 10807, and cjmul 10813. (Contributed by NM,
28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | remul 10800 |
Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by
Mario Carneiro, 14-Jul-2014.)
|
|