Theorem List for Intuitionistic Logic Explorer - 9401-9500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 1e0p1 9401 |
The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
|
   |
|
Theorem | dec10p 9402 |
Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; 
;  |
|
Theorem | numma 9403 |
Perform a multiply-add of two decimal integers and against
a fixed multiplicand (no carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
      
   

   
  
   
  |
|
Theorem | nummac 9404 |
Perform a multiply-add of two decimal integers and against
a fixed multiplicand (with carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
      
   

    
   
   

     |
|
Theorem | numma2c 9405 |
Perform a multiply-add of two decimal integers and against
a fixed multiplicand (with carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
      
   

    
   
   

     |
|
Theorem | numadd 9406 |
Add two decimal integers and (no
carry). (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
      
  
 

   
  |
|
Theorem | numaddc 9407 |
Add two decimal integers and (with
carry). (Contributed
by Mario Carneiro, 18-Feb-2014.)
|
      
   
 
   
  
     |
|
Theorem | nummul1c 9408 |
The product of a decimal integer with a number. (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
      

 
  
     
  |
|
Theorem | nummul2c 9409 |
The product of a decimal integer with a number (with carry).
(Contributed by Mario Carneiro, 18-Feb-2014.)
|
      

 
  
     
  |
|
Theorem | decma 9410 |
Perform a multiply-add of two numerals and against a fixed
multiplicand
(no carry). (Contributed by Mario Carneiro,
18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
; ;   
    
  
 ;  |
|
Theorem | decmac 9411 |
Perform a multiply-add of two numerals and against a fixed
multiplicand
(with carry). (Contributed by Mario Carneiro,
18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
; ;   

    
 ;   

;  |
|
Theorem | decma2c 9412 |
Perform a multiply-add of two numerals and against a fixed
multiplier
(with carry). (Contributed by Mario Carneiro,
18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
; ;   

    
 ;   

;  |
|
Theorem | decadd 9413 |
Add two numerals and
(no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
; ;  

  
;  |
|
Theorem | decaddc 9414 |
Add two numerals and
(with carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
; ;    
 
;  
;  |
|
Theorem | decaddc2 9415 |
Add two numerals and
(with carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
; ;    

 ;  
;  |
|
Theorem | decrmanc 9416 |
Perform a multiply-add of two numerals and against a fixed
multiplicand
(no carry). (Contributed by AV, 16-Sep-2021.)
|
;      
  
 ;  |
|
Theorem | decrmac 9417 |
Perform a multiply-add of two numerals and against a fixed
multiplicand
(with carry). (Contributed by AV, 16-Sep-2021.)
|
;   

   
;   

;  |
|
Theorem | decaddm10 9418 |
The sum of two multiples of 10 is a multiple of 10. (Contributed by AV,
30-Jul-2021.)
|
; ;  ;
   |
|
Theorem | decaddi 9419 |
Add two numerals and
(no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.)
|
;  

 ;  |
|
Theorem | decaddci 9420 |
Add two numerals and
(no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.)
|
;  
 
;  
;  |
|
Theorem | decaddci2 9421 |
Add two numerals and
(no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
;  

 ;  
;  |
|
Theorem | decsubi 9422 |
Difference between a numeral and a nonnegative integer (no
underflow). (Contributed by AV, 22-Jul-2021.) (Revised by AV,
6-Sep-2021.)
|
;  
   
;  |
|
Theorem | decmul1 9423 |
The product of a numeral with a number (no carry). (Contributed by
AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.)
|
;    
  ;  |
|
Theorem | decmul1c 9424 |
The product of a numeral with a number (with carry). (Contributed by
Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
;   

 
;  
;  |
|
Theorem | decmul2c 9425 |
The product of a numeral with a number (with carry). (Contributed by
Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
;   

 
;  
;  |
|
Theorem | decmulnc 9426 |
The product of a numeral with a number (no carry). (Contributed by AV,
15-Jun-2021.)
|
 ;  ;      |
|
Theorem | 11multnc 9427 |
The product of 11 (as numeral) with a number (no carry). (Contributed
by AV, 15-Jun-2021.)
|
 ;  ;  |
|
Theorem | decmul10add 9428 |
A multiplication of a number and a numeral expressed as addition with
first summand as multiple of 10. (Contributed by AV, 22-Jul-2021.)
(Revised by AV, 6-Sep-2021.)
|
     ;  ;   |
|
Theorem | 6p5lem 9429 |
Lemma for 6p5e11 9432 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
     
;  
;  |
|
Theorem | 5p5e10 9430 |
5 + 5 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 6p4e10 9431 |
6 + 4 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 6p5e11 9432 |
6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 6p6e12 9433 |
6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 7p3e10 9434 |
7 + 3 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 7p4e11 9435 |
7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 7p5e12 9436 |
7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 7p6e13 9437 |
7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 7p7e14 9438 |
7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 8p2e10 9439 |
8 + 2 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 8p3e11 9440 |
8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 8p4e12 9441 |
8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 8p5e13 9442 |
8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 8p6e14 9443 |
8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 8p7e15 9444 |
8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 8p8e16 9445 |
8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 9p2e11 9446 |
9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 9p3e12 9447 |
9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 9p4e13 9448 |
9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 9p5e14 9449 |
9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 9p6e15 9450 |
9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 9p7e16 9451 |
9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 9p8e17 9452 |
9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 9p9e18 9453 |
9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 10p10e20 9454 |
10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
; ;  ;  |
|
Theorem | 10m1e9 9455 |
10 - 1 = 9. (Contributed by AV, 6-Sep-2021.)
|
;   |
|
Theorem | 4t3lem 9456 |
Lemma for 4t3e12 9457 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
     
   |
|
Theorem | 4t3e12 9457 |
4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 4t4e16 9458 |
4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 5t2e10 9459 |
5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV,
4-Sep-2021.)
|
  ;  |
|
Theorem | 5t3e15 9460 |
5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 5t4e20 9461 |
5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 5t5e25 9462 |
5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 6t2e12 9463 |
6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 6t3e18 9464 |
6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 6t4e24 9465 |
6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 6t5e30 9466 |
6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 6t6e36 9467 |
6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 7t2e14 9468 |
7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 7t3e21 9469 |
7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 7t4e28 9470 |
7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 7t5e35 9471 |
7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 7t6e42 9472 |
7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 7t7e49 9473 |
7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 8t2e16 9474 |
8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 8t3e24 9475 |
8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 8t4e32 9476 |
8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 8t5e40 9477 |
8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 8t6e48 9478 |
8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 8t7e56 9479 |
8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 8t8e64 9480 |
8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 9t2e18 9481 |
9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 9t3e27 9482 |
9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 9t4e36 9483 |
9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 9t5e45 9484 |
9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 9t6e54 9485 |
9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 9t7e63 9486 |
9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 9t8e72 9487 |
9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 9t9e81 9488 |
9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 9t11e99 9489 |
9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV,
6-Sep-2021.)
|
 ;  ;  |
|
Theorem | 9lt10 9490 |
9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
;  |
|
Theorem | 8lt10 9491 |
8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
;  |
|
Theorem | 7lt10 9492 |
7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
;  |
|
Theorem | 6lt10 9493 |
6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
;  |
|
Theorem | 5lt10 9494 |
5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
;  |
|
Theorem | 4lt10 9495 |
4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
;  |
|
Theorem | 3lt10 9496 |
3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
;  |
|
Theorem | 2lt10 9497 |
2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
;  |
|
Theorem | 1lt10 9498 |
1 is less than 10. (Contributed by NM, 7-Nov-2012.) (Revised by Mario
Carneiro, 9-Mar-2015.) (Revised by AV, 8-Sep-2021.)
|
;  |
|
Theorem | decbin0 9499 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
 
     |
|
Theorem | decbin2 9500 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
           |