Proof of proveit.numbers.rounding.ceil_of_real_is_real theorem

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import defaults, x
from proveit.numbers.rounding import ceil_is_an_int

%proving ceil_of_real_is_real

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
ceil_of_real_is_real:
(see dependencies)

ceil_of_real_is_real may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

defaults.assumptions = ceil_of_real_is_real.conditions

defaults.assumptions:

ceil_is_an_int

 ⊢  

ceil_is_an_int.instantiate({x:x})

 ⊢  

%qed

proveit.numbers.rounding.ceil_of_real_is_real has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	4, 2, 3	⊢
	: , : , :
2	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
3	instantiation	4, 5, 6	⊢
	: , : , :
4	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
5	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
6	instantiation	7, 8	⊢
	:
7	axiom		⊢
	proveit.numbers.rounding.ceil_is_an_int
8	assumption		⊢