Type | Label | Description |
Statement |
|
Theorem | hashprg 10801 |
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 10802 |
There is (at least) one set with two different elements: the unordered
pair containing and
. In contrast to pr0hash2ex 10808, numbers
are used instead of sets because their representation is shorter (and more
comprehensive). (Contributed by AV, 29-Jan-2020.)
|
♯      |
|
Theorem | hashp1i 10803 |
Size of a natural number ordinal. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
♯ 
 
♯   |
|
Theorem | hash1 10804 |
Size of a natural number ordinal. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
♯   |
|
Theorem | hash2 10805 |
Size of a natural number ordinal. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
♯   |
|
Theorem | hash3 10806 |
Size of a natural number ordinal. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
♯   |
|
Theorem | hash4 10807 |
Size of a natural number ordinal. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
♯   |
|
Theorem | pr0hash2ex 10808 |
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 10809 |
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 10810 |
The size of a superset of a proper unordered pair is greater than 1.
(Contributed by AV, 6-Feb-2021.)
|
    
  

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

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