Type | Label | Description |
Statement |
|
Theorem | fseq1hash 10801 |
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 10802 |
Mapping ordinal addition to integer addition. (Contributed by Jim
Kingdon, 24-Feb-2022.)
|
frec             
              |
|
Theorem | fihashdom 10803 |
Dominance relation for the size function. (Contributed by Jim Kingdon,
24-Feb-2022.)
|
    ♯  ♯     |
|
Theorem | hashunlem 10804 |
Lemma for hashun 10805. Ordinal size of the union. (Contributed
by Jim
Kingdon, 25-Feb-2022.)
|
                   
   |
|
Theorem | hashun 10805 |
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 10806 |
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 10807 |
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 10808 |
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 10809 |
There is (at least) one set with two different elements: the unordered
pair containing and
. In contrast to pr0hash2ex 10815, numbers
are used instead of sets because their representation is shorter (and more
comprehensive). (Contributed by AV, 29-Jan-2020.)
|
♯      |
|
Theorem | hashp1i 10810 |
Size of a natural number ordinal. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
♯ 
 
♯   |
|
Theorem | hash1 10811 |
Size of a natural number ordinal. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
♯   |
|
Theorem | hash2 10812 |
Size of a natural number ordinal. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
♯   |
|
Theorem | hash3 10813 |
Size of a natural number ordinal. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
♯   |
|
Theorem | hash4 10814 |
Size of a natural number ordinal. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
♯   |
|
Theorem | pr0hash2ex 10815 |
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 10816 |
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 10817 |
The size of a superset of a proper unordered pair is greater than 1.
(Contributed by AV, 6-Feb-2021.)
|
    
  

♯     |
|
Theorem | fihashssdif 10818 |
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 10819 |
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 10820 |
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 10821 |
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 10822 |
Cardinality of a half-open set of integers. (Contributed by Stefan
O'Rear, 15-Aug-2015.)
|
     ♯  ..^ 
    |
|
Theorem | hashfzo0 10823 |
Cardinality of a half-open set of integers based at zero. (Contributed by
Stefan O'Rear, 15-Aug-2015.)
|
 ♯  ..^ 
  |
|
Theorem | hashfzp1 10824 |
Value of the numeric cardinality of a (possibly empty) integer range.
(Contributed by AV, 19-Jun-2021.)
|
     ♯            |
|
Theorem | hashfz0 10825 |
Value of the numeric cardinality of a nonempty range of nonnegative
integers. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
|
 ♯          |
|
Theorem | hashxp 10826 |
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 10827* |
A finite set of rational numbers has a maximum. (Contributed by Jim
Kingdon, 6-Sep-2022.)
|
   
   |
|
Theorem | fiubm 10828* |
Lemma for fiubz 10829 and fiubnn 10830. A general form of those theorems.
(Contributed by Jim Kingdon, 29-Oct-2024.)
|
             |
|
Theorem | fiubz 10829* |
A finite set of integers has an upper bound which is an integer.
(Contributed by Jim Kingdon, 29-Oct-2024.)
|
       |
|
Theorem | fiubnn 10830* |
A finite set of natural numbers has an upper bound which is a a natural
number. (Contributed by Jim Kingdon, 29-Oct-2024.)
|
       |
|
Theorem | resunimafz0 10831 |
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 10832 |
The size of a function on a finite set of sequential nonnegative integers.
(Contributed by Alexander van der Vekens, 25-Jun-2018.)
|
       ♯      |
|
Theorem | ffz0hash 10833 |
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 10834 |
The size of a function on a half-open range of nonnegative integers.
(Contributed by Alexander van der Vekens, 25-Mar-2018.)
|
   ..^  ♯    |
|
Theorem | fnfzo0hash 10835 |
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 10836* |
The number of bijections between two sets is a cardinal invariant.
(Contributed by Mario Carneiro, 21-Jan-2015.)
|
                 |
|
Theorem | leisorel 10837 |
Version of isorel 5826 for strictly increasing functions on the
reals.
(Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro,
9-Sep-2015.)
|
    

   
    
       |
|
Theorem | zfz1isolemsplit 10838 |
Lemma for zfz1iso 10841. Removing one element from an integer
range.
(Contributed by Jim Kingdon, 8-Sep-2022.)
|
        ♯  
    ♯        ♯      |
|
Theorem | zfz1isolemiso 10839* |
Lemma for zfz1iso 10841. Adding one element to the order
isomorphism.
(Contributed by Jim Kingdon, 8-Sep-2022.)
|
              ♯                  ♯        ♯          ♯  
          ♯  
         |
|
Theorem | zfz1isolem1 10840* |
Lemma for zfz1iso 10841. Existence of an order isomorphism given
the
existence of shorter isomorphisms. (Contributed by Jim Kingdon,
7-Sep-2022.)
|
       
  
    ♯       
   
       
    ♯       |
|
Theorem | zfz1iso 10841* |
A finite set of integers has an order isomorphism to a one-based finite
sequence. (Contributed by Jim Kingdon, 3-Sep-2022.)
|
        ♯       |
|
Theorem | seq3coll 10842* |
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 10843 |
Extend class notation with function shifter.
|
 |
|
Definition | df-shft 10844* |
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 10854 for its value. (Contributed by NM,
20-Jul-2005.)
|
      
        |
|
Theorem | shftlem 10845* |
Two ways to write a shifted set   . (Contributed by Mario
Carneiro, 3-Nov-2013.)
|
       
      |
|
Theorem | shftuz 10846* |
A shift of the upper integers. (Contributed by Mario Carneiro,
5-Nov-2013.)
|
          
   
    |
|
Theorem | shftfvalg 10847* |
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 10848 |
Existence of the result of applying shift. (Contributed by Jim Kingdon,
15-Aug-2021.)
|
       |
|
Theorem | shftfibg 10849 |
Value of a fiber of the relation . (Contributed by Jim Kingdon,
15-Aug-2021.)
|
          
          |
|
Theorem | shftfval 10850* |
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 10851* |
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 10852 |
Value of a fiber of the relation . (Contributed by Mario
Carneiro, 4-Nov-2013.)
|
                     |
|
Theorem | shftfn 10853* |
Functionality and domain of a sequence shifted by . (Contributed
by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
       
   |
|
Theorem | shftval 10854 |
Value of a sequence shifted by . (Contributed by NM,
20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.)
|
                 |
|
Theorem | shftval2 10855 |
Value of a sequence shifted by . (Contributed by NM,
20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
  
       
 
        |
|
Theorem | shftval3 10856 |
Value of a sequence shifted by . (Contributed by NM,
20-Jul-2005.)
|
                 |
|
Theorem | shftval4 10857 |
Value of a sequence shifted by  .
(Contributed by NM,
18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
             
    |
|
Theorem | shftval5 10858 |
Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
                 |
|
Theorem | shftf 10859* |
Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
     
             |
|
Theorem | 2shfti 10860 |
Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised
by Mario Carneiro, 5-Nov-2013.)
|
             |
|
Theorem | shftidt2 10861 |
Identity law for the shift operation. (Contributed by Mario Carneiro,
5-Nov-2013.)
|
     |
|
Theorem | shftidt 10862 |
Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
      
      |
|
Theorem | shftcan1 10863 |
Cancellation law for the shift operation. (Contributed by NM,
4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
           
      |
|
Theorem | shftcan2 10864 |
Cancellation law for the shift operation. (Contributed by NM,
4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
       
          |
|
Theorem | shftvalg 10865 |
Value of a sequence shifted by . (Contributed by Scott Fenton,
16-Dec-2017.)
|
            
    |
|
Theorem | shftval4g 10866 |
Value of a sequence shifted by  .
(Contributed by Jim Kingdon,
19-Aug-2021.)
|
         
        |
|
Theorem | seq3shft 10867* |
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 10868 |
Extend class notation to include complex conjugate function.
|
 |
|
Syntax | cre 10869 |
Extend class notation to include real part of a complex number.
|
 |
|
Syntax | cim 10870 |
Extend class notation to include imaginary part of a complex number.
|
 |
|
Definition | df-cj 10871* |
Define the complex conjugate function. See cjcli 10942 for its closure and
cjval 10874 for its value. (Contributed by NM,
9-May-1999.) (Revised by
Mario Carneiro, 6-Nov-2013.)
|
              |
|
Definition | df-re 10872 |
Define a function whose value is the real part of a complex number. See
reval 10878 for its value, recli 10940 for its closure, and replim 10888 for its use
in decomposing a complex number. (Contributed by NM, 9-May-1999.)
|
           |
|
Definition | df-im 10873 |
Define a function whose value is the imaginary part of a complex number.
See imval 10879 for its value, imcli 10941 for its closure, and replim 10888 for its
use in decomposing a complex number. (Contributed by NM,
9-May-1999.)
|
         |
|
Theorem | cjval 10874* |
The value of the conjugate of a complex number. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
    
    
   
    |
|
Theorem | cjth 10875 |
The defining property of the complex conjugate. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
        
          |
|
Theorem | cjf 10876 |
Domain and codomain of the conjugate function. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
     |
|
Theorem | cjcl 10877 |
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 10878 |
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 10879 |
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 10880 |
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 10881 |
The real part of a complex number in terms of the imaginary part
function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|
    
        |
|
Theorem | recl 10882 |
The real part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
    
  |
|
Theorem | imcl 10883 |
The imaginary part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
    
  |
|
Theorem | ref 10884 |
Domain and codomain of the real part function. (Contributed by Paul
Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
     |
|
Theorem | imf 10885 |
Domain and codomain of the imaginary part function. (Contributed by
Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
     |
|
Theorem | crre 10886 |
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 10887 |
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 10888 |
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 10889 |
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 10890 |
The imaginary part of a real number is 0. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
|
    
  |
|
Theorem | reim0b 10891 |
A number is real iff its imaginary part is 0. (Contributed by NM,
26-Sep-2005.)
|
         |
|
Theorem | rereb 10892 |
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 10893 |
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 10894 |
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 10895 |
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 10896 |
Real part of a complex conjugate. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
               |
|
Theorem | reneg 10897 |
Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by
Mario Carneiro, 14-Jul-2014.)
|
     
       |
|
Theorem | readd 10898 |
Real part distributes over addition. (Contributed by NM, 17-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
      
 
    
       |
|
Theorem | resub 10899 |
Real part distributes over subtraction. (Contributed by NM,
17-Mar-2005.)
|
      
 
            |
|
Theorem | remullem 10900 |
Lemma for remul 10901, immul 10908, and cjmul 10914. (Contributed by NM,
28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
                    
              
 
     
                                   |