Proof of proveit.numbers.rounding.real_minus_floor_interval theorem¶
In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import defaults, x
from proveit.logic import InSet
from proveit.numbers import Real
from proveit.numbers import zero_in_nats
from proveit.numbers.number_sets.real_numbers import int_within_real
from proveit.numbers.rounding import Floor
from proveit.numbers.rounding import floor_is_an_int, real_minus_floor_lower_bound, real_minus_floor_upper_bound
In [2]:
%proving real_minus_floor_interval
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
real_minus_floor_interval:
(see dependencies)
real_minus_floor_interval:
(see dependencies)
In [3]:
defaults.assumptions = real_minus_floor_interval.conditions
defaults.assumptions: 
In [4]:
interval = real_minus_floor_interval.instance_expr.operands[1]
interval: 
In [5]:
x_minus_floor = real_minus_floor_interval.instance_expr.operands[0]
x_minus_floor: 
In [6]:
floor_is_an_int.instantiate({x:x})
In [7]:
real_minus_floor_lower_bound
In [8]:
real_minus_floor_lower_bound.instantiate({x:x})
In [9]:
real_minus_floor_upper_bound
In [10]:
real_minus_floor_upper_bound.instantiate({x:x})
In [11]:
%qed
Out[11]:
