Proof of proveit.numbers.divisibility.divides_is_bool theorem

import proveit
from proveit import defaults
# from proveit.core_expr_types import
from proveit import a, b, x, y
from proveit.numbers import frac
from proveit.numbers.divisibility  import divides_def
from proveit.numbers.number_sets.integers import int_membership_is_bool
theory = proveit.Theory() # the theorem's theory

%proving divides_is_bool

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

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

defaults.assumptions = divides_is_bool.conditions

defaults.assumptions:

divides_def

 ⊢  

divides_def_inst = divides_def.instantiate(
    {x:x, y:y})

divides_def_inst:  ⊢  

int_membership_is_bool

 ⊢  

int_membership_is_bool_inst = int_membership_is_bool.instantiate({x:frac(y, x)})

int_membership_is_bool_inst:  ⊢  

divides_def_inst.sub_left_side_into(int_membership_is_bool_inst)

 ⊢  

%qed

proveit.numbers.divisibility.divides_is_bool has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3, 4	⊢
	: , : , :
2	theorem		⊢
	proveit.logic.equality.sub_left_side_into
3	instantiation	5	⊢
	:
4	instantiation	6	⊢
	: , :
5	conjecture		⊢
	proveit.numbers.number_sets.integers.int_membership_is_bool
6	axiom		⊢
	proveit.numbers.divisibility.divides_def