Proof of proveit.numbers.exponentiation.exp_rational_non_zero__not_zero theorem¶
In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving exp_rational_non_zero__not_zero
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
exp_rational_non_zero__not_zero:
(see dependencies)
exp_rational_non_zero__not_zero:
(see dependencies)
Proof by contradiction. Assume $a^b = 0$. Since $(a^b)^{1/b} = a$ and $0^{1/b} = 0$ then $a = 0$. But that contradicts our restriction on $a$ to be in $\mathbb{Q}^{\neq 0}$.