Theorem List for Intuitionistic Logic Explorer - 10501-10600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Definition | df-re 10501 |
Define a function whose value is the real part of a complex number. See
reval 10507 for its value, recli 10569 for its closure, and replim 10517 for its use
in decomposing a complex number. (Contributed by NM, 9-May-1999.)
|
           |
|
Definition | df-im 10502 |
Define a function whose value is the imaginary part of a complex number.
See imval 10508 for its value, imcli 10570 for its closure, and replim 10517 for its
use in decomposing a complex number. (Contributed by NM,
9-May-1999.)
|
         |
|
Theorem | cjval 10503* |
The value of the conjugate of a complex number. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
    
    
   
    |
|
Theorem | cjth 10504 |
The defining property of the complex conjugate. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
        
          |
|
Theorem | cjf 10505 |
Domain and codomain of the conjugate function. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
     |
|
Theorem | cjcl 10506 |
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 10507 |
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 10508 |
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 10509 |
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 10510 |
The real part of a complex number in terms of the imaginary part
function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|
    
        |
|
Theorem | recl 10511 |
The real part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
    
  |
|
Theorem | imcl 10512 |
The imaginary part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
    
  |
|
Theorem | ref 10513 |
Domain and codomain of the real part function. (Contributed by Paul
Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
     |
|
Theorem | imf 10514 |
Domain and codomain of the imaginary part function. (Contributed by
Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
     |
|
Theorem | crre 10515 |
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 10516 |
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 10517 |
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 10518 |
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 10519 |
The imaginary part of a real number is 0. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
|
    
  |
|
Theorem | reim0b 10520 |
A number is real iff its imaginary part is 0. (Contributed by NM,
26-Sep-2005.)
|
         |
|
Theorem | rereb 10521 |
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 10522 |
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 10523 |
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 10524 |
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 10525 |
Real part of a complex conjugate. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
               |
|
Theorem | reneg 10526 |
Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by
Mario Carneiro, 14-Jul-2014.)
|
     
       |
|
Theorem | readd 10527 |
Real part distributes over addition. (Contributed by NM, 17-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
      
 
    
       |
|
Theorem | resub 10528 |
Real part distributes over subtraction. (Contributed by NM,
17-Mar-2005.)
|
      
 
            |
|
Theorem | remullem 10529 |
Lemma for remul 10530, immul 10537, and cjmul 10543. (Contributed by NM,
28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
                    
              
 
     
                                   |
|
Theorem | remul 10530 |
Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by
Mario Carneiro, 14-Jul-2014.)
|
      
 
     
                  |
|
Theorem | remul2 10531 |
Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
|
      
 
        |
|
Theorem | redivap 10532 |
Real part of a division. Related to remul2 10531. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
  #                |
|
Theorem | imcj 10533 |
Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
                |
|
Theorem | imneg 10534 |
The imaginary part of a negative number. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
     
       |
|
Theorem | imadd 10535 |
Imaginary part distributes over addition. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
      
 
    
       |
|
Theorem | imsub 10536 |
Imaginary part distributes over subtraction. (Contributed by NM,
18-Mar-2005.)
|
      
 
            |
|
Theorem | immul 10537 |
Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised
by Mario Carneiro, 14-Jul-2014.)
|
      
 
     
                  |
|
Theorem | immul2 10538 |
Imaginary part of a product. (Contributed by Mario Carneiro,
2-Aug-2014.)
|
      
 
        |
|
Theorem | imdivap 10539 |
Imaginary part of a division. Related to immul2 10538. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
  #                |
|
Theorem | cjre 10540 |
A real number equals its complex conjugate. Proposition 10-3.4(f) of
[Gleason] p. 133. (Contributed by NM,
8-Oct-1999.)
|
    
  |
|
Theorem | cjcj 10541 |
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 10542 |
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 10543 |
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 10544 |
Standard inner product on complex numbers. (Contributed by NM,
29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
      
                     
        |
|
Theorem | cjmulrcl 10545 |
A complex number times its conjugate is real. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
         |
|
Theorem | cjmulval 10546 |
A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
                           |
|
Theorem | cjmulge0 10547 |
A complex number times its conjugate is nonnegative. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|

        |
|
Theorem | cjneg 10548 |
Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
     
       |
|
Theorem | addcj 10549 |
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 10550 |
Complex conjugate distributes over subtraction. (Contributed by NM,
28-Apr-2005.)
|
      
 
            |
|
Theorem | cjexp 10551 |
Complex conjugate of positive integer exponentiation. (Contributed by
NM, 7-Jun-2006.)
|
                     |
|
Theorem | imval2 10552 |
The imaginary part of a number in terms of complex conjugate.
(Contributed by NM, 30-Apr-2005.)
|
    
            |
|
Theorem | re0 10553 |
The real part of zero. (Contributed by NM, 27-Jul-1999.)
|
     |
|
Theorem | im0 10554 |
The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
|
     |
|
Theorem | re1 10555 |
The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|
     |
|
Theorem | im1 10556 |
The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|
     |
|
Theorem | rei 10557 |
The real part of .
(Contributed by Scott Fenton, 9-Jun-2006.)
|
   
 |
|
Theorem | imi 10558 |
The imaginary part of . (Contributed by Scott Fenton,
9-Jun-2006.)
|
   
 |
|
Theorem | cj0 10559 |
The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
|
     |
|
Theorem | cji 10560 |
The complex conjugate of the imaginary unit. (Contributed by NM,
26-Mar-2005.)
|
   
  |
|
Theorem | cjreim 10561 |
The conjugate of a representation of a complex number in terms of real and
imaginary parts. (Contributed by NM, 1-Jul-2005.)
|
      
          |
|
Theorem | cjreim2 10562 |
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 10563 |
Complex conjugate is a one-to-one function. (Contributed by NM,
29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.)
|
               |
|
Theorem | cjap 10564 |
Complex conjugate and apartness. (Contributed by Jim Kingdon,
14-Jun-2020.)
|
        #     #    |
|
Theorem | cjap0 10565 |
A number is apart from zero iff its complex conjugate is apart from zero.
(Contributed by Jim Kingdon, 14-Jun-2020.)
|
  #     #
   |
|
Theorem | cjne0 10566 |
A number is nonzero iff its complex conjugate is nonzero. Also see
cjap0 10565 which is similar but for apartness.
(Contributed by NM,
29-Apr-2005.)
|
         |
|
Theorem | cjdivap 10567 |
Complex conjugate distributes over division. (Contributed by Jim Kingdon,
14-Jun-2020.)
|
  #                    |
|
Theorem | cnrecnv 10568* |
The inverse to the canonical bijection from 
 to
from cnref1o 9335. (Contributed by Mario Carneiro,
25-Aug-2014.)
|
   
    
             |
|
Theorem | recli 10569 |
The real part of a complex number is real (closure law). (Contributed
by NM, 11-May-1999.)
|
   
 |
|
Theorem | imcli 10570 |
The imaginary part of a complex number is real (closure law).
(Contributed by NM, 11-May-1999.)
|
   
 |
|
Theorem | cjcli 10571 |
Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
|
   
 |
|
Theorem | replimi 10572 |
Construct a complex number from its real and imaginary parts.
(Contributed by NM, 1-Oct-1999.)
|
    
        |
|
Theorem | cjcji 10573 |
The conjugate of the conjugate is the original complex number.
Proposition 10-3.4(e) of [Gleason] p.
133. (Contributed by NM,
11-May-1999.)
|
         |
|
Theorem | reim0bi 10574 |
A number is real iff its imaginary part is 0. (Contributed by NM,
29-May-1999.)
|
    
  |
|
Theorem | rerebi 10575 |
A real number equals its real part. Proposition 10-3.4(f) of [Gleason]
p. 133. (Contributed by NM, 27-Oct-1999.)
|
    
  |
|
Theorem | cjrebi 10576 |
A number is real iff it equals its complex conjugate. Proposition
10-3.4(f) of [Gleason] p. 133.
(Contributed by NM, 11-Oct-1999.)
|
    
  |
|
Theorem | recji 10577 |
Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
|
             |
|
Theorem | imcji 10578 |
Imaginary part of a complex conjugate. (Contributed by NM,
2-Oct-1999.)
|
              |
|
Theorem | cjmulrcli 10579 |
A complex number times its conjugate is real. (Contributed by NM,
11-May-1999.)
|
       |
|
Theorem | cjmulvali 10580 |
A complex number times its conjugate. (Contributed by NM,
2-Oct-1999.)
|
                         |
|
Theorem | cjmulge0i 10581 |
A complex number times its conjugate is nonnegative. (Contributed by
NM, 28-May-1999.)
|
       |
|
Theorem | renegi 10582 |
Real part of negative. (Contributed by NM, 2-Aug-1999.)
|
           |
|
Theorem | imnegi 10583 |
Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
|
           |
|
Theorem | cjnegi 10584 |
Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
|
           |
|
Theorem | addcji 10585 |
A number plus its conjugate is twice its real part. Compare Proposition
10-3.4(h) of [Gleason] p. 133.
(Contributed by NM, 2-Oct-1999.)
|
             |
|
Theorem | readdi 10586 |
Real part distributes over addition. (Contributed by NM,
28-Jul-1999.)
|
   
             |
|
Theorem | imaddi 10587 |
Imaginary part distributes over addition. (Contributed by NM,
28-Jul-1999.)
|
   
             |
|
Theorem | remuli 10588 |
Real part of a product. (Contributed by NM, 28-Jul-1999.)
|
                     
       |
|
Theorem | immuli 10589 |
Imaginary part of a product. (Contributed by NM, 28-Jul-1999.)
|
                     
       |
|
Theorem | cjaddi 10590 |
Complex conjugate distributes over addition. Proposition 10-3.4(a) of
[Gleason] p. 133. (Contributed by NM,
28-Jul-1999.)
|
   
             |
|
Theorem | cjmuli 10591 |
Complex conjugate distributes over multiplication. Proposition
10-3.4(c) of [Gleason] p. 133.
(Contributed by NM, 28-Jul-1999.)
|
                 |
|
Theorem | ipcni 10592 |
Standard inner product on complex numbers. (Contributed by NM,
2-Oct-1999.)
|
                         
       |
|
Theorem | cjdivapi 10593 |
Complex conjugate distributes over division. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
 #                   |
|
Theorem | crrei 10594 |
The real part of a complex number representation. Definition 10-3.1 of
[Gleason] p. 132. (Contributed by NM,
10-May-1999.)
|
   
     |
|
Theorem | crimi 10595 |
The imaginary part of a complex number representation. Definition
10-3.1 of [Gleason] p. 132.
(Contributed by NM, 10-May-1999.)
|
   
     |
|
Theorem | recld 10596 |
The real part of a complex number is real (closure law). (Contributed
by Mario Carneiro, 29-May-2016.)
|
         |
|
Theorem | imcld 10597 |
The imaginary part of a complex number is real (closure law).
(Contributed by Mario Carneiro, 29-May-2016.)
|
         |
|
Theorem | cjcld 10598 |
Closure law for complex conjugate. (Contributed by Mario Carneiro,
29-May-2016.)
|
         |
|
Theorem | replimd 10599 |
Construct a complex number from its real and imaginary parts.
(Contributed by Mario Carneiro, 29-May-2016.)
|
       
         |
|
Theorem | remimd 10600 |
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 Mario Carneiro, 29-May-2016.)
|
           
         |