import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import l, defaults
from proveit.logic import Equals, InSet, Not, NotInSet
from proveit.numbers import Integer
from proveit.physics.quantum.QPE import _scaled_delta_b_is_zero_or_non_int
%proving _scaled_delta_b_not_eq_nonzeroInt
defaults.assumptions = _scaled_delta_b_not_eq_nonzeroInt.conditions
# for convenience, name the individual assumptions
ell_in_integers = defaults.assumptions[1]
# for convenience, name the individual assumptions
ell_not_zero = defaults.assumptions[2]
# for convenience, name the scaled delta expression
_scaled_delta = _scaled_delta_b_not_eq_nonzeroInt.instance_expr.lhs
_scaled_delta_b_is_zero_or_non_int
_scaled_delta_b_is_zero_or_non_int_inst = (
_scaled_delta_b_is_zero_or_non_int.instantiate())
# Assume to the contrary that _scaled_delta_b = ell
contradictory_assumption = Equals(_scaled_delta, l)
# Need to explicitly include this, otherwise one of the final steps
# fails, with a generic, unhelpful error message.
contradictory_assumption.deduce_in_bool()
l_notin_ints_implies_not_l_in_ints = (
NotInSet(l, Integer).unfold(assumptions=[NotInSet(l, Integer)]).
as_implication(hypothesis=NotInSet(l, Integer)))
# Must include this and previous cell; helps deal with a double negation later
l_notin_ints_implies_not_l_in_ints.contrapose()
contradictory_assumption_disjunction = (
contradictory_assumption.sub_right_side_into(
_scaled_delta_b_is_zero_or_non_int_inst,
assumptions=[*defaults.assumptions, contradictory_assumption]))
contradictory_assumption_gives_false = contradictory_assumption_disjunction.derive_contradiction()
contradictory_assumption_gives_false.as_implication(hypothesis=contradictory_assumption)
%qed