Theorem List for Intuitionistic Logic Explorer - 10301-10400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | flqltnz 10301 |
If A is not an integer, then the floor of A is less than A. (Contributed
by Jim Kingdon, 9-Oct-2021.)
|
  
      |
|
Theorem | flqwordi 10302 |
Ordering relationship for the greatest integer function. (Contributed by
Jim Kingdon, 9-Oct-2021.)
|
 
           |
|
Theorem | flqword2 10303 |
Ordering relationship for the greatest integer function. (Contributed by
Jim Kingdon, 9-Oct-2021.)
|
 
    
          |
|
Theorem | flqbi 10304 |
A condition equivalent to floor. (Contributed by Jim Kingdon,
9-Oct-2021.)
|
        
      |
|
Theorem | flqbi2 10305 |
A condition equivalent to floor. (Contributed by Jim Kingdon,
9-Oct-2021.)
|
         

    |
|
Theorem | adddivflid 10306 |
The floor of a sum of an integer and a fraction is equal to the integer
iff the denominator of the fraction is less than the numerator.
(Contributed by AV, 14-Jul-2021.)
|
               |
|
Theorem | flqge0nn0 10307 |
The floor of a number greater than or equal to 0 is a nonnegative integer.
(Contributed by Jim Kingdon, 10-Oct-2021.)
|
      
  |
|
Theorem | flqge1nn 10308 |
The floor of a number greater than or equal to 1 is a positive integer.
(Contributed by Jim Kingdon, 10-Oct-2021.)
|
      
  |
|
Theorem | fldivnn0 10309 |
The floor function of a division of a nonnegative integer by a positive
integer is a nonnegative integer. (Contributed by Alexander van der
Vekens, 14-Apr-2018.)
|
           |
|
Theorem | divfl0 10310 |
The floor of a fraction is 0 iff the denominator is less than the
numerator. (Contributed by AV, 8-Jul-2021.)
|
             |
|
Theorem | flqaddz 10311 |
An integer can be moved in and out of the floor of a sum. (Contributed by
Jim Kingdon, 10-Oct-2021.)
|
      
          |
|
Theorem | flqzadd 10312 |
An integer can be moved in and out of the floor of a sum. (Contributed by
Jim Kingdon, 10-Oct-2021.)
|
      
          |
|
Theorem | flqmulnn0 10313 |
Move a nonnegative integer in and out of a floor. (Contributed by Jim
Kingdon, 10-Oct-2021.)
|
                 |
|
Theorem | btwnzge0 10314 |
A real bounded between an integer and its successor is nonnegative iff the
integer is nonnegative. Second half of Lemma 13-4.1 of [Gleason] p. 217.
(Contributed by NM, 12-Mar-2005.)
|
             |
|
Theorem | 2tnp1ge0ge0 10315 |
Two times an integer plus one is not negative iff the integer is not
negative. (Contributed by AV, 19-Jun-2021.)
|
    
    |
|
Theorem | flhalf 10316 |
Ordering relation for the floor of half of an integer. (Contributed by
NM, 1-Jan-2006.) (Proof shortened by Mario Carneiro, 7-Jun-2016.)
|

            |
|
Theorem | fldivnn0le 10317 |
The floor function of a division of a nonnegative integer by a positive
integer is less than or equal to the division. (Contributed by Alexander
van der Vekens, 14-Apr-2018.)
|
             |
|
Theorem | flltdivnn0lt 10318 |
The floor function of a division of a nonnegative integer by a positive
integer is less than the division of a greater dividend by the same
positive integer. (Contributed by Alexander van der Vekens,
14-Apr-2018.)
|
               |
|
Theorem | fldiv4p1lem1div2 10319 |
The floor of an integer equal to 3 or greater than 4, increased by 1, is
less than or equal to the half of the integer minus 1. (Contributed by
AV, 8-Jul-2021.)
|
                 
   |
|
Theorem | ceilqval 10320 |
The value of the ceiling function. (Contributed by Jim Kingdon,
10-Oct-2021.)
|
 ⌈          |
|
Theorem | ceiqcl 10321 |
The ceiling function returns an integer (closure law). (Contributed by
Jim Kingdon, 11-Oct-2021.)
|
      
  |
|
Theorem | ceilqcl 10322 |
Closure of the ceiling function. (Contributed by Jim Kingdon,
11-Oct-2021.)
|
 ⌈    |
|
Theorem | ceiqge 10323 |
The ceiling of a real number is greater than or equal to that number.
(Contributed by Jim Kingdon, 11-Oct-2021.)
|

        |
|
Theorem | ceilqge 10324 |
The ceiling of a real number is greater than or equal to that number.
(Contributed by Jim Kingdon, 11-Oct-2021.)
|

⌈    |
|
Theorem | ceiqm1l 10325 |
One less than the ceiling of a real number is strictly less than that
number. (Contributed by Jim Kingdon, 11-Oct-2021.)
|
           |
|
Theorem | ceilqm1lt 10326 |
One less than the ceiling of a real number is strictly less than that
number. (Contributed by Jim Kingdon, 11-Oct-2021.)
|
  ⌈     |
|
Theorem | ceiqle 10327 |
The ceiling of a real number is the smallest integer greater than or equal
to it. (Contributed by Jim Kingdon, 11-Oct-2021.)
|
 
         |
|
Theorem | ceilqle 10328 |
The ceiling of a real number is the smallest integer greater than or equal
to it. (Contributed by Jim Kingdon, 11-Oct-2021.)
|
 
 ⌈    |
|
Theorem | ceilid 10329 |
An integer is its own ceiling. (Contributed by AV, 30-Nov-2018.)
|
 ⌈    |
|
Theorem | ceilqidz 10330 |
A rational number equals its ceiling iff it is an integer. (Contributed
by Jim Kingdon, 11-Oct-2021.)
|
  ⌈     |
|
Theorem | flqleceil 10331 |
The floor of a rational number is less than or equal to its ceiling.
(Contributed by Jim Kingdon, 11-Oct-2021.)
|
     ⌈    |
|
Theorem | flqeqceilz 10332 |
A rational number is an integer iff its floor equals its ceiling.
(Contributed by Jim Kingdon, 11-Oct-2021.)
|
      ⌈     |
|
Theorem | intqfrac2 10333 |
Decompose a real into integer and fractional parts. (Contributed by Jim
Kingdon, 18-Oct-2021.)
|
      

     |
|
Theorem | intfracq 10334 |
Decompose a rational number, expressed as a ratio, into integer and
fractional parts. The fractional part has a tighter bound than that of
intqfrac2 10333. (Contributed by NM, 16-Aug-2008.)
|
             
   
       |
|
Theorem | flqdiv 10335 |
Cancellation of the embedded floor of a real divided by an integer.
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
                     |
|
4.6.2 The modulo (remainder)
operation
|
|
Syntax | cmo 10336 |
Extend class notation with the modulo operation.
|
 |
|
Definition | df-mod 10337* |
Define the modulo (remainder) operation. See modqval 10338 for its value.
For example,   and    . As with
df-fl 10284 we define this for first and second
arguments which are real and
positive real, respectively, even though many theorems will need to be
more restricted (for example, specify rational arguments). (Contributed
by NM, 10-Nov-2008.)
|
   
          |
|
Theorem | modqval 10338 |
The value of the modulo operation. The modulo congruence notation of
number theory,
(modulo ), can be expressed in our
notation as     . Definition 1 in Knuth,
The
Art of Computer Programming, Vol. I (1972), p. 38. Knuth uses
"mod"
for the operation and "modulo" for the congruence. Unlike
Knuth, we
restrict the second argument to positive numbers to simplify certain
theorems. (This also gives us future flexibility to extend it to any
one of several different conventions for a zero or negative second
argument, should there be an advantage in doing so.) As with flqcl 10287 we
only prove this for rationals although other particular kinds of real
numbers may be possible. (Contributed by Jim Kingdon, 16-Oct-2021.)
|
    
            |
|
Theorem | modqvalr 10339 |
The value of the modulo operation (multiplication in reversed order).
(Contributed by Jim Kingdon, 16-Oct-2021.)
|
    
            |
|
Theorem | modqcl 10340 |
Closure law for the modulo operation. (Contributed by Jim Kingdon,
16-Oct-2021.)
|
    
  |
|
Theorem | flqpmodeq 10341 |
Partition of a division into its integer part and the remainder.
(Contributed by Jim Kingdon, 16-Oct-2021.)
|
          

     |
|
Theorem | modqcld 10342 |
Closure law for the modulo operation. (Contributed by Jim Kingdon,
16-Oct-2021.)
|
           |
|
Theorem | modq0 10343 |
is zero iff is evenly divisible by . (Contributed
by Jim Kingdon, 17-Oct-2021.)
|
       
   |
|
Theorem | mulqmod0 10344 |
The product of an integer and a positive rational number is 0 modulo the
positive real number. (Contributed by Jim Kingdon, 18-Oct-2021.)
|
     
   |
|
Theorem | negqmod0 10345 |
is divisible by iff its negative is.
(Contributed by Jim
Kingdon, 18-Oct-2021.)
|
            |
|
Theorem | modqge0 10346 |
The modulo operation is nonnegative. (Contributed by Jim Kingdon,
18-Oct-2021.)
|
  
    |
|
Theorem | modqlt 10347 |
The modulo operation is less than its second argument. (Contributed by
Jim Kingdon, 18-Oct-2021.)
|
       |
|
Theorem | modqelico 10348 |
Modular reduction produces a half-open interval. (Contributed by Jim
Kingdon, 18-Oct-2021.)
|
    
      |
|
Theorem | modqdiffl 10349 |
The modulo operation differs from by an integer multiple of .
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
     
           |
|
Theorem | modqdifz 10350 |
The modulo operation differs from by an integer multiple of .
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
     
     |
|
Theorem | modqfrac 10351 |
The fractional part of a number is the number modulo 1. (Contributed by
Jim Kingdon, 18-Oct-2021.)
|
           |
|
Theorem | flqmod 10352 |
The floor function expressed in terms of the modulo operation.
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
    
      |
|
Theorem | intqfrac 10353 |
Break a number into its integer part and its fractional part.
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
           |
|
Theorem | zmod10 10354 |
An integer modulo 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.)
|
     |
|
Theorem | zmod1congr 10355 |
Two arbitrary integers are congruent modulo 1, see example 4 in
[ApostolNT] p. 107. (Contributed by AV,
21-Jul-2021.)
|
    
    |
|
Theorem | modqmulnn 10356 |
Move a positive integer in and out of a floor in the first argument of a
modulo operation. (Contributed by Jim Kingdon, 18-Oct-2021.)
|
                         |
|
Theorem | modqvalp1 10357 |
The value of the modulo operation (expressed with sum of denominator and
nominator). (Contributed by Jim Kingdon, 20-Oct-2021.)
|
     
               |
|
Theorem | zmodcl 10358 |
Closure law for the modulo operation restricted to integers. (Contributed
by NM, 27-Nov-2008.)
|
       |
|
Theorem | zmodcld 10359 |
Closure law for the modulo operation restricted to integers.
(Contributed by Mario Carneiro, 28-May-2016.)
|
         |
|
Theorem | zmodfz 10360 |
An integer mod lies
in the first
nonnegative integers.
(Contributed by Jeff Madsen, 17-Jun-2010.)
|
             |
|
Theorem | zmodfzo 10361 |
An integer mod lies
in the first
nonnegative integers.
(Contributed by Stefan O'Rear, 6-Sep-2015.)
|
      ..^   |
|
Theorem | zmodfzp1 10362 |
An integer mod lies
in the first nonnegative integers.
(Contributed by AV, 27-Oct-2018.)
|
           |
|
Theorem | modqid 10363 |
Identity law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.)
|
    
   
  |
|
Theorem | modqid0 10364 |
A positive real number modulo itself is 0. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
       |
|
Theorem | modqid2 10365 |
Identity law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.)
|
           |
|
Theorem | zmodid2 10366 |
Identity law for modulo restricted to integers. (Contributed by Paul
Chapman, 22-Jun-2011.)
|
               |
|
Theorem | zmodidfzo 10367 |
Identity law for modulo restricted to integers. (Contributed by AV,
27-Oct-2018.)
|
       ..^    |
|
Theorem | zmodidfzoimp 10368 |
Identity law for modulo restricted to integers. (Contributed by AV,
27-Oct-2018.)
|
  ..^ 
   |
|
Theorem | q0mod 10369 |
Special case: 0 modulo a positive real number is 0. (Contributed by Jim
Kingdon, 21-Oct-2021.)
|
       |
|
Theorem | q1mod 10370 |
Special case: 1 modulo a real number greater than 1 is 1. (Contributed by
Jim Kingdon, 21-Oct-2021.)
|
       |
|
Theorem | modqabs 10371 |
Absorption law for modulo. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
                   |
|
Theorem | modqabs2 10372 |
Absorption law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.)
|
           |
|
Theorem | modqcyc 10373 |
The modulo operation is periodic. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
    
    
 
     |
|
Theorem | modqcyc2 10374 |
The modulo operation is periodic. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
    
    
 
     |
|
Theorem | modqadd1 10375 |
Addition property of the modulo operation. (Contributed by Jim Kingdon,
22-Oct-2021.)
|
                       
   |
|
Theorem | modqaddabs 10376 |
Absorption law for modulo. (Contributed by Jim Kingdon, 22-Oct-2021.)
|
    
                |
|
Theorem | modqaddmod 10377 |
The sum of a number modulo a modulus and another number equals the sum of
the two numbers modulo the same modulus. (Contributed by Jim Kingdon,
23-Oct-2021.)
|
    
          
   |
|
Theorem | mulqaddmodid 10378 |
The sum of a positive rational number less than an upper bound and the
product of an integer and the upper bound is the positive rational number
modulo the upper bound. (Contributed by Jim Kingdon, 23-Oct-2021.)
|
    
          
   |
|
Theorem | mulp1mod1 10379 |
The product of an integer and an integer greater than 1 increased by 1 is
1 modulo the integer greater than 1. (Contributed by AV, 15-Jul-2021.)
|
           
   |
|
Theorem | modqmuladd 10380* |
Decomposition of an integer into a multiple of a modulus and a
remainder. (Contributed by Jim Kingdon, 23-Oct-2021.)
|
          
      

       |
|
Theorem | modqmuladdim 10381* |
Implication of a decomposition of an integer into a multiple of a
modulus and a remainder. (Contributed by Jim Kingdon, 23-Oct-2021.)
|
              |
|
Theorem | modqmuladdnn0 10382* |
Implication of a decomposition of a nonnegative integer into a multiple
of a modulus and a remainder. (Contributed by Jim Kingdon,
23-Oct-2021.)
|
              |
|
Theorem | qnegmod 10383 |
The negation of a number modulo a positive number is equal to the
difference of the modulus and the number modulo the modulus. (Contributed
by Jim Kingdon, 24-Oct-2021.)
|
     
      |
|
Theorem | m1modnnsub1 10384 |
Minus one modulo a positive integer is equal to the integer minus one.
(Contributed by AV, 14-Jul-2021.)
|
   
    |
|
Theorem | m1modge3gt1 10385 |
Minus one modulo an integer greater than two is greater than one.
(Contributed by AV, 14-Jul-2021.)
|
    
     |
|
Theorem | addmodid 10386 |
The sum of a positive integer and a nonnegative integer less than the
positive integer is equal to the nonnegative integer modulo the positive
integer. (Contributed by Alexander van der Vekens, 30-Oct-2018.) (Proof
shortened by AV, 5-Jul-2020.)
|
     
   |
|
Theorem | addmodidr 10387 |
The sum of a positive integer and a nonnegative integer less than the
positive integer is equal to the nonnegative integer modulo the positive
integer. (Contributed by AV, 19-Mar-2021.)
|
     
   |
|
Theorem | modqadd2mod 10388 |
The sum of a number modulo a modulus and another number equals the sum of
the two numbers modulo the modulus. (Contributed by Jim Kingdon,
24-Oct-2021.)
|
    
    
         |
|
Theorem | modqm1p1mod0 10389 |
If a number modulo a modulus equals the modulus decreased by 1, the first
number increased by 1 modulo the modulus equals 0. (Contributed by Jim
Kingdon, 24-Oct-2021.)
|
          
    |
|
Theorem | modqltm1p1mod 10390 |
If a number modulo a modulus is less than the modulus decreased by 1, the
first number increased by 1 modulo the modulus equals the first number
modulo the modulus, increased by 1. (Contributed by Jim Kingdon,
24-Oct-2021.)
|
        
    
       |
|
Theorem | modqmul1 10391 |
Multiplication property of the modulo operation. Note that the
multiplier
must be an integer. (Contributed by Jim Kingdon,
24-Oct-2021.)
|
                       
   |
|
Theorem | modqmul12d 10392 |
Multiplication property of the modulo operation, see theorem 5.2(b) in
[ApostolNT] p. 107. (Contributed by
Jim Kingdon, 24-Oct-2021.)
|
                               
   |
|
Theorem | modqnegd 10393 |
Negation property of the modulo operation. (Contributed by Jim Kingdon,
24-Oct-2021.)
|
                       |
|
Theorem | modqadd12d 10394 |
Additive property of the modulo operation. (Contributed by Jim Kingdon,
25-Oct-2021.)
|
                               
   |
|
Theorem | modqsub12d 10395 |
Subtraction property of the modulo operation. (Contributed by Jim
Kingdon, 25-Oct-2021.)
|
                               
   |
|
Theorem | modqsubmod 10396 |
The difference of a number modulo a modulus and another number equals the
difference of the two numbers modulo the modulus. (Contributed by Jim
Kingdon, 25-Oct-2021.)
|
    
          
   |
|
Theorem | modqsubmodmod 10397 |
The difference of a number modulo a modulus and another number modulo the
same modulus equals the difference of the two numbers modulo the modulus.
(Contributed by Jim Kingdon, 25-Oct-2021.)
|
    
                |
|
Theorem | q2txmodxeq0 10398 |
Two times a positive number modulo the number is zero. (Contributed by
Jim Kingdon, 25-Oct-2021.)
|
         |
|
Theorem | q2submod 10399 |
If a number is between a modulus and twice the modulus, the first number
modulo the modulus equals the first number minus the modulus.
(Contributed by Jim Kingdon, 25-Oct-2021.)
|
   
           |
|
Theorem | modifeq2int 10400 |
If a nonnegative integer is less than twice a positive integer, the
nonnegative integer modulo the positive integer equals the nonnegative
integer or the nonnegative integer minus the positive integer.
(Contributed by Alexander van der Vekens, 21-May-2018.)
|
     
          |