Theorem List for Intuitionistic Logic Explorer - 9401-9500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | nn0ind-raph 9401* |
Principle of Mathematical Induction (inference schema) on nonnegative
integers. The first four hypotheses give us the substitution instances
we need; the last two are the basis and the induction step. Raph Levien
remarks: "This seems a bit painful. I wonder if an explicit
substitution version would be easier." (Contributed by Raph
Levien,
10-Apr-2004.)
|
    
   
     
    
     |
|
Theorem | zindd 9402* |
Principle of Mathematical Induction on all integers, deduction version.
The first five hypotheses give the substitutions; the last three are the
basis, the induction, and the extension to negative numbers.
(Contributed by Paul Chapman, 17-Apr-2009.) (Proof shortened by Mario
Carneiro, 4-Jan-2017.)
|
    
   
     
    
       
     
    
   |
|
Theorem | btwnz 9403* |
Any real number can be sandwiched between two integers. Exercise 2 of
[Apostol] p. 28. (Contributed by NM,
10-Nov-2004.)
|
       |
|
Theorem | nn0zd 9404 |
A positive integer is an integer. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | nnzd 9405 |
A nonnegative integer is an integer. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | zred 9406 |
An integer is a real number. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | zcnd 9407 |
An integer is a complex number. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | znegcld 9408 |
Closure law for negative integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
      |
|
Theorem | peano2zd 9409 |
Deduction from second Peano postulate generalized to integers.
(Contributed by Mario Carneiro, 28-May-2016.)
|
   
   |
|
Theorem | zaddcld 9410 |
Closure of addition of integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
         |
|
Theorem | zsubcld 9411 |
Closure of subtraction of integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
         |
|
Theorem | zmulcld 9412 |
Closure of multiplication of integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
         |
|
Theorem | zadd2cl 9413 |
Increasing an integer by 2 results in an integer. (Contributed by
Alexander van der Vekens, 16-Sep-2018.)
|
     |
|
Theorem | btwnapz 9414 |
A number between an integer and its successor is apart from any integer.
(Contributed by Jim Kingdon, 6-Jan-2023.)
|
             #   |
|
4.4.10 Decimal arithmetic
|
|
Syntax | cdc 9415 |
Constant used for decimal constructor.
|
;  |
|
Definition | df-dec 9416 |
Define the "decimal constructor", which is used to build up
"decimal
integers" or "numeric terms" in base  . For example,
;;;   ;;;    ;;;   1kp2ke3k 14954.
(Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV,
1-Aug-2021.)
|
;        |
|
Theorem | 9p1e10 9417 |
9 + 1 = 10. (Contributed by Mario Carneiro, 18-Apr-2015.) (Revised by
Stanislas Polu, 7-Apr-2020.) (Revised by AV, 1-Aug-2021.)
|
  ;  |
|
Theorem | dfdec10 9418 |
Version of the definition of the "decimal constructor" using ;
instead of the symbol 10. Of course, this statement cannot be used as
definition, because it uses the "decimal constructor".
(Contributed by
AV, 1-Aug-2021.)
|
;  ; 
  |
|
Theorem | deceq1 9419 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
 ;
;   |
|
Theorem | deceq2 9420 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
 ;
;   |
|
Theorem | deceq1i 9421 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.)
|
; ;  |
|
Theorem | deceq2i 9422 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.)
|
; ;  |
|
Theorem | deceq12i 9423 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.)
|
; ;  |
|
Theorem | numnncl 9424 |
Closure for a numeral (with units place). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
   
 |
|
Theorem | num0u 9425 |
Add a zero in the units place. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
 
     |
|
Theorem | num0h 9426 |
Add a zero in the higher places. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
     |
|
Theorem | numcl 9427 |
Closure for a decimal integer (with units place). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
  

 |
|
Theorem | numsuc 9428 |
The successor of a decimal integer (no carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
    
        |
|
Theorem | deccl 9429 |
Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
;  |
|
Theorem | 10nn 9430 |
10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by
AV, 6-Sep-2021.)
|
;  |
|
Theorem | 10pos 9431 |
The number 10 is positive. (Contributed by NM, 5-Feb-2007.) (Revised by
AV, 8-Sep-2021.)
|
;  |
|
Theorem | 10nn0 9432 |
10 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
;  |
|
Theorem | 10re 9433 |
The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV,
8-Sep-2021.)
|
;  |
|
Theorem | decnncl 9434 |
Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
;  |
|
Theorem | dec0u 9435 |
Add a zero in the units place. (Contributed by Mario Carneiro,
17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
; 
;  |
|
Theorem | dec0h 9436 |
Add a zero in the higher places. (Contributed by Mario Carneiro,
17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
;  |
|
Theorem | numnncl2 9437 |
Closure for a decimal integer (zero units place). (Contributed by Mario
Carneiro, 9-Mar-2015.)
|
  
  |
|
Theorem | decnncl2 9438 |
Closure for a decimal integer (zero units place). (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
;  |
|
Theorem | numlt 9439 |
Comparing two decimal integers (equal higher places). (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
  
      |
|
Theorem | numltc 9440 |
Comparing two decimal integers (unequal higher places). (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
  
      |
|
Theorem | le9lt10 9441 |
A "decimal digit" (i.e. a nonnegative integer less than or equal to
9)
is less then 10. (Contributed by AV, 8-Sep-2021.)
|
;  |
|
Theorem | declt 9442 |
Comparing two decimal integers (equal higher places). (Contributed by
Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
; ;  |
|
Theorem | decltc 9443 |
Comparing two decimal integers (unequal higher places). (Contributed
by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
; ; ;  |
|
Theorem | declth 9444 |
Comparing two decimal integers (unequal higher places). (Contributed
by AV, 8-Sep-2021.)
|
; ;  |
|
Theorem | decsuc 9445 |
The successor of a decimal integer (no carry). (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
  ;   ;  |
|
Theorem | 3declth 9446 |
Comparing two decimal integers with three "digits" (unequal higher
places). (Contributed by AV, 8-Sep-2021.)
|
;; 
;;   |
|
Theorem | 3decltc 9447 |
Comparing two decimal integers with three "digits" (unequal higher
places). (Contributed by AV, 15-Jun-2021.) (Revised by AV,
6-Sep-2021.)
|
;
; ;;  ;;   |
|
Theorem | decle 9448 |
Comparing two decimal integers (equal higher places). (Contributed by
AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.)
|
; ;  |
|
Theorem | decleh 9449 |
Comparing two decimal integers (unequal higher places). (Contributed by
AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.)
|
; ;  |
|
Theorem | declei 9450 |
Comparing a digit to a decimal integer. (Contributed by AV,
17-Aug-2021.)
|
;  |
|
Theorem | numlti 9451 |
Comparing a digit to a decimal integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
  
  |
|
Theorem | declti 9452 |
Comparing a digit to a decimal integer. (Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
;
;  |
|
Theorem | decltdi 9453 |
Comparing a digit to a decimal integer. (Contributed by AV,
8-Sep-2021.)
|
;  |
|
Theorem | numsucc 9454 |
The successor of a decimal integer (with carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
      
        |
|
Theorem | decsucc 9455 |
The successor of a decimal integer (with carry). (Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
  ;   ;  |
|
Theorem | 1e0p1 9456 |
The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
|
   |
|
Theorem | dec10p 9457 |
Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; 
;  |
|
Theorem | numma 9458 |
Perform a multiply-add of two decimal integers and against
a fixed multiplicand (no carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
      
   

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

    
   
   

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

    
   
   

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

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

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

 
  
     
  |
|
Theorem | decma 9465 |
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 9466 |
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 9467 |
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 9468 |
Add two numerals and
(no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
; ;  

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

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

   
;   

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

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

 ;  
;  |
|
Theorem | decsubi 9477 |
Difference between a numeral and a nonnegative integer (no
underflow). (Contributed by AV, 22-Jul-2021.) (Revised by AV,
6-Sep-2021.)
|
;  
   
;  |
|
Theorem | decmul1 9478 |
The product of a numeral with a number (no carry). (Contributed by
AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.)
|
;    
  ;  |
|
Theorem | decmul1c 9479 |
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 9480 |
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 9481 |
The product of a numeral with a number (no carry). (Contributed by AV,
15-Jun-2021.)
|
 ;  ;      |
|
Theorem | 11multnc 9482 |
The product of 11 (as numeral) with a number (no carry). (Contributed
by AV, 15-Jun-2021.)
|
 ;  ;  |
|
Theorem | decmul10add 9483 |
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 9484 |
Lemma for 6p5e11 9487 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
     
;  
;  |
|
Theorem | 5p5e10 9485 |
5 + 5 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 6p4e10 9486 |
6 + 4 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 6p5e11 9487 |
6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 6p6e12 9488 |
6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 7p3e10 9489 |
7 + 3 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 7p4e11 9490 |
7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 7p5e12 9491 |
7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 7p6e13 9492 |
7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 7p7e14 9493 |
7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 8p2e10 9494 |
8 + 2 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 8p3e11 9495 |
8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
  ;  |
|
Theorem | 8p4e12 9496 |
8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 8p5e13 9497 |
8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 8p6e14 9498 |
8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 8p7e15 9499 |
8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |
|
Theorem | 8p8e16 9500 |
8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
  ;  |