Theorem List for Intuitionistic Logic Explorer - 10301-10400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | fnfzo0hash 10301 |
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 10302* |
The number of bijections between two sets is a cardinal invariant.
(Contributed by Mario Carneiro, 21-Jan-2015.)
|
                 |
|
Theorem | leisorel 10303 |
Version of isorel 5601 for strictly increasing functions on the
reals.
(Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro,
9-Sep-2015.)
|
    

   
    
       |
|
Theorem | zfz1isolemsplit 10304 |
Lemma for zfz1iso 10307. Removing one element from an integer
range.
(Contributed by Jim Kingdon, 8-Sep-2022.)
|
        ♯  
    ♯        ♯      |
|
Theorem | zfz1isolemiso 10305* |
Lemma for zfz1iso 10307. Adding one element to the order
isomorphism.
(Contributed by Jim Kingdon, 8-Sep-2022.)
|
              ♯                  ♯        ♯          ♯  
          ♯  
         |
|
Theorem | zfz1isolem1 10306* |
Lemma for zfz1iso 10307. Existence of an order isomorphism given
the
existence of shorter isomorphisms. (Contributed by Jim Kingdon,
7-Sep-2022.)
|
       
  
    ♯       
   
       
    ♯       |
|
Theorem | zfz1iso 10307* |
A finite set of integers has an order isomorphism to a one-based finite
sequence. (Contributed by Jim Kingdon, 3-Sep-2022.)
|
        ♯       |
|
Theorem | iseqcoll 10308* |
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.)
|
          
  
   
         ♯          ♯                
           
              ♯            
   ♯       
                      
       |
|
3.7 Elementary real and complex
functions
|
|
3.7.1 The "shift" operation
|
|
Syntax | cshi 10309 |
Extend class notation with function shifter.
|
 |
|
Definition | df-shft 10310* |
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 10320 for its value. (Contributed by NM,
20-Jul-2005.)
|
      
        |
|
Theorem | shftlem 10311* |
Two ways to write a shifted set   . (Contributed by Mario
Carneiro, 3-Nov-2013.)
|
       
      |
|
Theorem | shftuz 10312* |
A shift of the upper integers. (Contributed by Mario Carneiro,
5-Nov-2013.)
|
          
   
    |
|
Theorem | shftfvalg 10313* |
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 10314 |
Existence of the result of applying shift. (Contributed by Jim Kingdon,
15-Aug-2021.)
|
       |
|
Theorem | shftfibg 10315 |
Value of a fiber of the relation . (Contributed by Jim Kingdon,
15-Aug-2021.)
|
          
          |
|
Theorem | shftfval 10316* |
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 10317* |
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 10318 |
Value of a fiber of the relation . (Contributed by Mario
Carneiro, 4-Nov-2013.)
|
                     |
|
Theorem | shftfn 10319* |
Functionality and domain of a sequence shifted by . (Contributed
by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
       
   |
|
Theorem | shftval 10320 |
Value of a sequence shifted by . (Contributed by NM,
20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.)
|
                 |
|
Theorem | shftval2 10321 |
Value of a sequence shifted by . (Contributed by NM,
20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
  
       
 
        |
|
Theorem | shftval3 10322 |
Value of a sequence shifted by . (Contributed by NM,
20-Jul-2005.)
|
                 |
|
Theorem | shftval4 10323 |
Value of a sequence shifted by  .
(Contributed by NM,
18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
             
    |
|
Theorem | shftval5 10324 |
Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
                 |
|
Theorem | shftf 10325* |
Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
     
             |
|
Theorem | 2shfti 10326 |
Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised
by Mario Carneiro, 5-Nov-2013.)
|
             |
|
Theorem | shftidt2 10327 |
Identity law for the shift operation. (Contributed by Mario Carneiro,
5-Nov-2013.)
|
     |
|
Theorem | shftidt 10328 |
Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
      
      |
|
Theorem | shftcan1 10329 |
Cancellation law for the shift operation. (Contributed by NM,
4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
           
      |
|
Theorem | shftcan2 10330 |
Cancellation law for the shift operation. (Contributed by NM,
4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
       
          |
|
Theorem | shftvalg 10331 |
Value of a sequence shifted by . (Contributed by Scott Fenton,
16-Dec-2017.)
|
            
    |
|
Theorem | shftval4g 10332 |
Value of a sequence shifted by  .
(Contributed by Jim Kingdon,
19-Aug-2021.)
|
         
        |
|
Theorem | seq3shft 10333* |
Shifting the index set of a sequence. (Contributed by NM, 17-Mar-2005.)
(Revised by Jim Kingdon, 17-Oct-2022.)
|
                  
  
   
     
   
 
    |
|
3.7.2 Real and imaginary parts;
conjugate
|
|
Syntax | ccj 10334 |
Extend class notation to include complex conjugate function.
|
 |
|
Syntax | cre 10335 |
Extend class notation to include real part of a complex number.
|
 |
|
Syntax | cim 10336 |
Extend class notation to include imaginary part of a complex number.
|
 |
|
Definition | df-cj 10337* |
Define the complex conjugate function. See cjcli 10408 for its closure and
cjval 10340 for its value. (Contributed by NM,
9-May-1999.) (Revised by
Mario Carneiro, 6-Nov-2013.)
|
              |
|
Definition | df-re 10338 |
Define a function whose value is the real part of a complex number. See
reval 10344 for its value, recli 10406 for its closure, and replim 10354 for its use
in decomposing a complex number. (Contributed by NM, 9-May-1999.)
|
           |
|
Definition | df-im 10339 |
Define a function whose value is the imaginary part of a complex number.
See imval 10345 for its value, imcli 10407 for its closure, and replim 10354 for its
use in decomposing a complex number. (Contributed by NM,
9-May-1999.)
|
         |
|
Theorem | cjval 10340* |
The value of the conjugate of a complex number. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
    
    
   
    |
|
Theorem | cjth 10341 |
The defining property of the complex conjugate. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
        
          |
|
Theorem | cjf 10342 |
Domain and codomain of the conjugate function. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
     |
|
Theorem | cjcl 10343 |
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 10344 |
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 10345 |
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 10346 |
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 10347 |
The real part of a complex number in terms of the imaginary part
function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|
    
        |
|
Theorem | recl 10348 |
The real part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
    
  |
|
Theorem | imcl 10349 |
The imaginary part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
    
  |
|
Theorem | ref 10350 |
Domain and codomain of the real part function. (Contributed by Paul
Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
     |
|
Theorem | imf 10351 |
Domain and codomain of the imaginary part function. (Contributed by
Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
     |
|
Theorem | crre 10352 |
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 10353 |
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 10354 |
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 10355 |
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 10356 |
The imaginary part of a real number is 0. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
|
    
  |
|
Theorem | reim0b 10357 |
A number is real iff its imaginary part is 0. (Contributed by NM,
26-Sep-2005.)
|
         |
|
Theorem | rereb 10358 |
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 10359 |
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 10360 |
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 10361 |
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 10362 |
Real part of a complex conjugate. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
               |
|
Theorem | reneg 10363 |
Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by
Mario Carneiro, 14-Jul-2014.)
|
     
       |
|
Theorem | readd 10364 |
Real part distributes over addition. (Contributed by NM, 17-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
      
 
    
       |
|
Theorem | resub 10365 |
Real part distributes over subtraction. (Contributed by NM,
17-Mar-2005.)
|
      
 
            |
|
Theorem | remullem 10366 |
Lemma for remul 10367, immul 10374, and cjmul 10380. (Contributed by NM,
28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
                    
              
 
     
                                   |
|
Theorem | remul 10367 |
Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by
Mario Carneiro, 14-Jul-2014.)
|
      
 
     
                  |
|
Theorem | remul2 10368 |
Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
|
      
 
        |
|
Theorem | redivap 10369 |
Real part of a division. Related to remul2 10368. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
  #                |
|
Theorem | imcj 10370 |
Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
                |
|
Theorem | imneg 10371 |
The imaginary part of a negative number. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
     
       |
|
Theorem | imadd 10372 |
Imaginary part distributes over addition. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
      
 
    
       |
|
Theorem | imsub 10373 |
Imaginary part distributes over subtraction. (Contributed by NM,
18-Mar-2005.)
|
      
 
            |
|
Theorem | immul 10374 |
Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised
by Mario Carneiro, 14-Jul-2014.)
|
      
 
     
                  |
|
Theorem | immul2 10375 |
Imaginary part of a product. (Contributed by Mario Carneiro,
2-Aug-2014.)
|
      
 
        |
|
Theorem | imdivap 10376 |
Imaginary part of a division. Related to immul2 10375. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
  #                |
|
Theorem | cjre 10377 |
A real number equals its complex conjugate. Proposition 10-3.4(f) of
[Gleason] p. 133. (Contributed by NM,
8-Oct-1999.)
|
    
  |
|
Theorem | cjcj 10378 |
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 10379 |
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 10380 |
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 10381 |
Standard inner product on complex numbers. (Contributed by NM,
29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
      
                     
        |
|
Theorem | cjmulrcl 10382 |
A complex number times its conjugate is real. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
         |
|
Theorem | cjmulval 10383 |
A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
                           |
|
Theorem | cjmulge0 10384 |
A complex number times its conjugate is nonnegative. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|

        |
|
Theorem | cjneg 10385 |
Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
     
       |
|
Theorem | addcj 10386 |
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 10387 |
Complex conjugate distributes over subtraction. (Contributed by NM,
28-Apr-2005.)
|
      
 
            |
|
Theorem | cjexp 10388 |
Complex conjugate of positive integer exponentiation. (Contributed by
NM, 7-Jun-2006.)
|
                     |
|
Theorem | imval2 10389 |
The imaginary part of a number in terms of complex conjugate.
(Contributed by NM, 30-Apr-2005.)
|
    
            |
|
Theorem | re0 10390 |
The real part of zero. (Contributed by NM, 27-Jul-1999.)
|
     |
|
Theorem | im0 10391 |
The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
|
     |
|
Theorem | re1 10392 |
The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|
     |
|
Theorem | im1 10393 |
The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|
     |
|
Theorem | rei 10394 |
The real part of .
(Contributed by Scott Fenton, 9-Jun-2006.)
|
   
 |
|
Theorem | imi 10395 |
The imaginary part of . (Contributed by Scott Fenton,
9-Jun-2006.)
|
   
 |
|
Theorem | cj0 10396 |
The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
|
     |
|
Theorem | cji 10397 |
The complex conjugate of the imaginary unit. (Contributed by NM,
26-Mar-2005.)
|
   
  |
|
Theorem | cjreim 10398 |
The conjugate of a representation of a complex number in terms of real and
imaginary parts. (Contributed by NM, 1-Jul-2005.)
|
      
          |
|
Theorem | cjreim2 10399 |
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 10400 |
Complex conjugate is a one-to-one function. (Contributed by NM,
29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.)
|
               |