Proof of proveit.numbers.divisibility.non_zero_divides_zero theorem

import proveit
from proveit import defaults
from proveit import x, y
from proveit.numbers import zero
from proveit.numbers.divisibility  import divides_def
from proveit.numbers.division import frac_zero_numer
from proveit.numbers.number_sets.integers import zero_is_int
theory = proveit.Theory() # the theorem's theory

%proving non_zero_divides_zero

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

defaults.assumptions = non_zero_divides_zero.conditions

defaults.assumptions:

divides_def

 ⊢  

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

divides_def_inst: ,  ⊢  

frac_zero_numer

 ⊢  

frac_zero_numer_inst = frac_zero_numer.instantiate({x:x})

frac_zero_numer_inst: ,  ⊢  

zero_is_int

 ⊢  

zero_over_x_in_z = frac_zero_numer_inst.sub_left_side_into(zero_is_int)

zero_over_x_in_z: ,  ⊢  

divides_def_inst.sub_left_side_into(zero_over_x_in_z)

,  ⊢  

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

%qed

proveit.numbers.divisibility.non_zero_divides_zero 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	conjecture		⊢
	proveit.numbers.number_sets.integers.zero_is_int
4	instantiation	5, 6*	,  ⊢
	: , :
5	axiom		⊢
	proveit.numbers.divisibility.divides_def
6	instantiation	7, 8, 9	,  ⊢
	:
7	conjecture		⊢
	proveit.numbers.division.frac_zero_numer
8	assumption		⊢
9	assumption		⊢
*equality replacement requirements