Theorem List for Intuitionistic Logic Explorer - 7401-7500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | msqge0i 7401 |
A square is nonnegative. (Contributed by NM, 14-May-1999.) (Proof
shortened by Andrew Salmon, 19-Nov-2011.)
|
   |
|
Theorem | msqge0d 7402 |
A square is nonnegative. (Contributed by Mario Carneiro,
27-May-2016.)
|
       |
|
Theorem | mulge0 7403 |
The product of two nonnegative numbers is nonnegative. (Contributed by
NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
      
    |
|
Theorem | mulge0i 7404 |
The product of two nonnegative numbers is nonnegative. (Contributed by
NM, 30-Jul-1999.)
|
       |
|
Theorem | mulge0d 7405 |
The product of two nonnegative numbers is nonnegative. (Contributed by
Mario Carneiro, 27-May-2016.)
|
             |
|
Theorem | apti 7406 |
Complex apartness is tight. (Contributed by Jim Kingdon,
21-Feb-2020.)
|
    #    |
|
Theorem | apne 7407 |
Apartness implies negated equality. We cannot in general prove the
converse, which is the whole point of having separate notations for
apartness and negated equality. (Contributed by Jim Kingdon,
21-Feb-2020.)
|
    #    |
|
Theorem | gt0ap0 7408 |
Positive implies apart from zero. (Contributed by Jim Kingdon,
27-Feb-2020.)
|
   #   |
|
Theorem | gt0ap0i 7409 |
Positive means apart from zero (useful for ordering theorems involving
division). (Contributed by Jim Kingdon, 27-Feb-2020.)
|
 #   |
|
Theorem | gt0ap0ii 7410 |
Positive implies apart from zero. (Contributed by Jim Kingdon,
27-Feb-2020.)
|
#  |
|
Theorem | gt0ap0d 7411 |
Positive implies apart from zero. Because of the way we define #,
must be an
element of , not
just .
(Contributed by
Jim Kingdon, 27-Feb-2020.)
|
     #   |
|
Theorem | negap0 7412 |
A number is apart from zero iff its negative is apart from zero.
(Contributed by Jim Kingdon, 27-Feb-2020.)
|
  #  #    |
|
Theorem | ltleap 7413 |
Less than in terms of non-strict order and apartness. (Contributed by Jim
Kingdon, 28-Feb-2020.)
|
    
#     |
|
3.3.7 Reciprocals
|
|
Theorem | recextlem1 7414 |
Lemma for recexap 7416. (Contributed by Eric Schmidt, 23-May-2007.)
|
               
     |
|
Theorem | recexaplem2 7415 |
Lemma for recexap 7416. (Contributed by Jim Kingdon, 20-Feb-2020.)
|
      #   
    #   |
|
Theorem | recexap 7416* |
Existence of reciprocal of nonzero complex number. (Contributed by Jim
Kingdon, 20-Feb-2020.)
|
  #   

  |
|
Theorem | mulap0 7417 |
The product of two numbers apart from zero is apart from zero. Lemma
2.15 of [Geuvers], p. 6. (Contributed
by Jim Kingdon, 22-Feb-2020.)
|
   # 
 #     #   |
|
Theorem | mulap0b 7418 |
The product of two numbers apart from zero is apart from zero.
(Contributed by Jim Kingdon, 24-Feb-2020.)
|
     # #    #    |
|
Theorem | mulap0i 7419 |
The product of two numbers apart from zero is apart from zero.
(Contributed by Jim Kingdon, 23-Feb-2020.)
|
# #   #  |
|
Theorem | mulap0bd 7420 |
The product of two numbers apart from zero is apart from zero.
(Contributed by Jim Kingdon, 24-Feb-2020.)
|
      
# #    #    |
|
Theorem | mulap0d 7421 |
The product of two numbers apart from zero is apart from zero.
(Contributed by Jim Kingdon, 23-Feb-2020.)
|
     #   #     #   |
|
Theorem | mulap0bad 7422 |
A factor of a complex number apart from zero is apart from zero.
Partial converse of mulap0d 7421 and consequence of mulap0bd 7420.
(Contributed by Jim Kingdon, 24-Feb-2020.)
|
       #   #   |
|
Theorem | mulap0bbd 7423 |
A factor of a complex number apart from zero is apart from zero.
Partial converse of mulap0d 7421 and consequence of mulap0bd 7420.
(Contributed by Jim Kingdon, 24-Feb-2020.)
|
       #   #   |
|
Theorem | mulcanapd 7424 |
Cancellation law for multiplication. (Contributed by Jim Kingdon,
21-Feb-2020.)
|
       #    

     |
|
Theorem | mulcanap2d 7425 |
Cancellation law for multiplication. (Contributed by Jim Kingdon,
21-Feb-2020.)
|
       #    

     |
|
Theorem | mulcanapad 7426 |
Cancellation of a nonzero factor on the left in an equation. One-way
deduction form of mulcanapd 7424. (Contributed by Jim Kingdon,
21-Feb-2020.)
|
       #           |
|
Theorem | mulcanap2ad 7427 |
Cancellation of a nonzero factor on the right in an equation. One-way
deduction form of mulcanap2d 7425. (Contributed by Jim Kingdon,
21-Feb-2020.)
|
       #           |
|
Theorem | mulcanap 7428 |
Cancellation law for multiplication (full theorem form). (Contributed by
Jim Kingdon, 21-Feb-2020.)
|
   #     
     |
|
Theorem | mulcanap2 7429 |
Cancellation law for multiplication. (Contributed by Jim Kingdon,
21-Feb-2020.)
|
   #     
     |
|
Theorem | mulcanapi 7430 |
Cancellation law for multiplication. (Contributed by Jim Kingdon,
21-Feb-2020.)
|
#   
    |
|
Theorem | muleqadd 7431 |
Property of numbers whose product equals their sum. Equation 5 of
[Kreyszig] p. 12. (Contributed by NM,
13-Nov-2006.)
|
          
      |
|
Theorem | receuap 7432* |
Existential uniqueness of reciprocals. (Contributed by Jim Kingdon,
21-Feb-2020.)
|
  #       |
|
3.3.8 Division
|
|
Syntax | cdiv 7433 |
Extend class notation to include division.
|
 |
|
Definition | df-div 7434* |
Define division. Theorem divmulap 7436 relates it to multiplication, and
divclap 7439 and redivclap 7489 prove its closure laws. (Contributed by NM,
2-Feb-1995.) (Revised by Mario Carneiro, 1-Apr-2014.)
(New usage is discouraged.)
|
       


   |
|
Theorem | divvalap 7435* |
Value of division: the (unique) element such that
 
. This is meaningful only when is apart from
zero. (Contributed by Jim Kingdon, 21-Feb-2020.)
|
  #      

   |
|
Theorem | divmulap 7436 |
Relationship between division and multiplication. (Contributed by Jim
Kingdon, 22-Feb-2020.)
|
   #     


   |
|
Theorem | divmulap2 7437 |
Relationship between division and multiplication. (Contributed by Jim
Kingdon, 22-Feb-2020.)
|
   #     
     |
|
Theorem | divmulap3 7438 |
Relationship between division and multiplication. (Contributed by Jim
Kingdon, 22-Feb-2020.)
|
   #     
     |
|
Theorem | divclap 7439 |
Closure law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
|
  #      |
|
Theorem | recclap 7440 |
Closure law for reciprocal. (Contributed by Jim Kingdon, 22-Feb-2020.)
|
  #      |
|
Theorem | divcanap2 7441 |
A cancellation law for division. (Contributed by Jim Kingdon,
22-Feb-2020.)
|
  #        |
|
Theorem | divcanap1 7442 |
A cancellation law for division. (Contributed by Jim Kingdon,
22-Feb-2020.)
|
  #   
    |
|
Theorem | diveqap0 7443 |
A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon,
22-Feb-2020.)
|
  #   
    |
|
Theorem | divap0b 7444 |
The ratio of numbers apart from zero is apart from zero. (Contributed by
Jim Kingdon, 22-Feb-2020.)
|
  #   #
  #    |
|
Theorem | divap0 7445 |
The ratio of numbers apart from zero is apart from zero. (Contributed by
Jim Kingdon, 22-Feb-2020.)
|
   # 
 #     #   |
|
Theorem | recap0 7446 |
The reciprocal of a number apart from zero is apart from zero.
(Contributed by Jim Kingdon, 24-Feb-2020.)
|
  #    #   |
|
Theorem | recidap 7447 |
Multiplication of a number and its reciprocal. (Contributed by Jim
Kingdon, 24-Feb-2020.)
|
  #   
 
  |
|
Theorem | recidap2 7448 |
Multiplication of a number and its reciprocal. (Contributed by Jim
Kingdon, 24-Feb-2020.)
|
  #    

  |
|
Theorem | divrecap 7449 |
Relationship between division and reciprocal. (Contributed by Jim
Kingdon, 24-Feb-2020.)
|
  #     
    |
|
Theorem | divrecap2 7450 |
Relationship between division and reciprocal. (Contributed by Jim
Kingdon, 25-Feb-2020.)
|
  #      
   |
|
Theorem | divassap 7451 |
An associative law for division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
   #     
  
    |
|
Theorem | div23ap 7452 |
A commutative/associative law for division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
   #     
       |
|
Theorem | div32ap 7453 |
A commutative/associative law for division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
   #     

      |
|
Theorem | div13ap 7454 |
A commutative/associative law for division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
   #     

      |
|
Theorem | div12ap 7455 |
A commutative/associative law for division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
   #        
    |
|
Theorem | divdirap 7456 |
Distribution of division over addition. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
   #     
         |
|
Theorem | divcanap3 7457 |
A cancellation law for division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
  #   
    |
|
Theorem | divcanap4 7458 |
A cancellation law for division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
  #   
    |
|
Theorem | div11ap 7459 |
One-to-one relationship for division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
   #     
     |
|
Theorem | dividap 7460 |
A number divided by itself is one. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
  #   
  |
|
Theorem | div0ap 7461 |
Division into zero is zero. (Contributed by Jim Kingdon, 25-Feb-2020.)
|
  #   
  |
|
Theorem | div1 7462 |
A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
  
  |
|
Theorem | 1div1e1 7463 |
1 divided by 1 is 1 (common case). (Contributed by David A. Wheeler,
7-Dec-2018.)
|
 
 |
|
Theorem | diveqap1 7464 |
Equality in terms of unit ratio. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
  #   
    |
|
Theorem | divnegap 7465 |
Move negative sign inside of a division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
  #          |
|
Theorem | divsubdirap 7466 |
Distribution of division over subtraction. (Contributed by NM,
4-Mar-2005.)
|
   #     
         |
|
Theorem | recrecap 7467 |
A number is equal to the reciprocal of its reciprocal. (Contributed by
Jim Kingdon, 25-Feb-2020.)
|
  #   
 
  |
|
Theorem | rec11ap 7468 |
Reciprocal is one-to-one. (Contributed by Jim Kingdon, 25-Feb-2020.)
|
   # 
 #    
  
   |
|
Theorem | rec11rap 7469 |
Mutual reciprocals. (Contributed by Jim Kingdon, 25-Feb-2020.)
|
   # 
 #    
      |
|
Theorem | divmuldivap 7470 |
Multiplication of two ratios. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
     
#  
#                  |
|
Theorem | divdivdivap 7471 |
Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by
Jim Kingdon, 25-Feb-2020.)
|
    #    
#  
#         
 
      |
|
Theorem | divcanap5 7472 |
Cancellation of common factor in a ratio. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
   #   #     
       |
|
Theorem | divmul13ap 7473 |
Swap the denominators in the product of two ratios. (Contributed by Jim
Kingdon, 26-Feb-2020.)
|
     
#  
#                  |
|
Theorem | divmul24ap 7474 |
Swap the numerators in the product of two ratios. (Contributed by Jim
Kingdon, 26-Feb-2020.)
|
     
#  
#                  |
|
Theorem | divmuleqap 7475 |
Cross-multiply in an equality of ratios. (Contributed by Jim Kingdon,
26-Feb-2020.)
|
     
#  
#        
       |
|
Theorem | recdivap 7476 |
The reciprocal of a ratio. (Contributed by Jim Kingdon, 26-Feb-2020.)
|
   # 
 #   
       |
|
Theorem | divcanap6 7477 |
Cancellation of inverted fractions. (Contributed by Jim Kingdon,
26-Feb-2020.)
|
   # 
 #    
      |
|
Theorem | divdiv32ap 7478 |
Swap denominators in a division. (Contributed by Jim Kingdon,
26-Feb-2020.)
|
   #   #     
       |
|
Theorem | divcanap7 7479 |
Cancel equal divisors in a division. (Contributed by Jim Kingdon,
26-Feb-2020.)
|
   #   #     
       |
|
Theorem | dmdcanap 7480 |
Cancellation law for division and multiplication. (Contributed by Jim
Kingdon, 26-Feb-2020.)
|
   # 
 # 

          |
|
Theorem | divdivap1 7481 |
Division into a fraction. (Contributed by Jim Kingdon, 26-Feb-2020.)
|
   #   #     
  
    |
|
Theorem | divdivap2 7482 |
Division by a fraction. (Contributed by Jim Kingdon, 26-Feb-2020.)
|
   #   #             |
|
Theorem | recdivap2 7483 |
Division into a reciprocal. (Contributed by Jim Kingdon, 26-Feb-2020.)
|
   # 
 #    
        |
|
Theorem | ddcanap 7484 |
Cancellation in a double division. (Contributed by Jim Kingdon,
26-Feb-2020.)
|
   # 
 #         |
|
Theorem | divadddivap 7485 |
Addition of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
|
     
#  
#             
        |
|
Theorem | divsubdivap 7486 |
Subtraction of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
|
     
#  
#             
        |
|
Theorem | conjmulap 7487 |
Two numbers whose reciprocals sum to 1 are called "conjugates" and
satisfy
this relationship. (Contributed by Jim Kingdon, 26-Feb-2020.)
|
   # 
 #            
      |
|
Theorem | rerecclap 7488 |
Closure law for reciprocal. (Contributed by Jim Kingdon,
26-Feb-2020.)
|
  #      |
|
Theorem | redivclap 7489 |
Closure law for division of reals. (Contributed by Jim Kingdon,
26-Feb-2020.)
|
  #      |
|
Theorem | eqneg 7490 |
A number equal to its negative is zero. (Contributed by NM,
12-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|
      |
|
Theorem | eqnegd 7491 |
A complex number equals its negative iff it is zero. Deduction form of
eqneg 7490. (Contributed by David Moews, 28-Feb-2017.)
|
   
    |
|
Theorem | eqnegad 7492 |
If a complex number equals its own negative, it is zero. One-way
deduction form of eqneg 7490. (Contributed by David Moews,
28-Feb-2017.)
|
        |
|
Theorem | div2negap 7493 |
Quotient of two negatives. (Contributed by Jim Kingdon, 27-Feb-2020.)
|
  #     
    |
|
Theorem | divneg2ap 7494 |
Move negative sign inside of a division. (Contributed by Jim Kingdon,
27-Feb-2020.)
|
  #          |
|
Theorem | recclapzi 7495 |
Closure law for reciprocal. (Contributed by Jim Kingdon,
27-Feb-2020.)
|
 # 
   |
|
Theorem | recap0apzi 7496 |
The reciprocal of a number apart from zero is apart from zero.
(Contributed by Jim Kingdon, 27-Feb-2020.)
|
 # 
 #   |
|
Theorem | recidapzi 7497 |
Multiplication of a number and its reciprocal. (Contributed by Jim
Kingdon, 27-Feb-2020.)
|
 # 

 
  |
|
Theorem | div1i 7498 |
A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.)
|
 
 |
|
Theorem | eqnegi 7499 |
A number equal to its negative is zero. (Contributed by NM,
29-May-1999.)
|
    |
|
Theorem | recclapi 7500 |
Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
|
#    |