Proof of proveit.numbers.exponentiation.sqrt2_is_not_rational theorem¶
In [1]:
import proveit
from proveit import defaults, Variable
from proveit import p, a_star, b_star
from proveit.logic import InSet, Equals
from proveit.numbers import (zero, two, NaturalPos,
Rational, RationalNonZero, RationalPos,
Abs, greater, Mult, frac, Divides, GCD, Exp, sqrt)
In [2]:
%proving sqrt2_is_not_rational
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
sqrt2_is_not_rational:
(see dependencies)
sqrt2_is_not_rational:
(see dependencies)
Setting up a contradiction proof by first assuming $\sqrt{2} \in \mathbb{Q}$¶
In [3]:
sqrt_2_is_rational = InSet(sqrt(two), Rational)
sqrt_2_is_rational: 
In [4]:
defaults.assumptions = [sqrt_2_is_rational]
defaults.assumptions: 
If $\sqrt{2}$ is in $\mathbb{Q}$, then $\left|\sqrt{2}\right|$ is in $\mathbb{Q^+}$¶
($\sqrt{2} \in \mathbb{Q^+}$ as well by convention, but this proof is really about showing that no squared rational number is equal to $2$.)
We know that a non-zero rational raised to a rational power is non-zero.¶
In [5]:
sqrt(two).deduce_not_zero()
The absolute value of a non-zero rational is a positive rational.¶
In [6]:
abs_sqrt_2_is_rational_pos = InSet(Abs(sqrt(two)), RationalPos).prove()
abs_sqrt_2_is_rational_pos: ⊢ 
⊢ 
In [7]:
abs_sqrt_2_is_rational_pos.choose_reduced_rational_fraction(a_star, b_star)
From $\sqrt{2} = a^* / b^*$, derive $2 \cdot (b^*)^2 = (a^*)^2$¶
In [8]:
sqrt_2_equation = Equals(Abs(sqrt(two)), frac(a_star, b_star)).prove()
sqrt_2_equation: 
⊢ 
⊢ 
In [9]:
sqrt_2_equation = sqrt_2_equation.right_mult_both_sides(b_star)
sqrt_2_equation: 
, , 
, ⊢ 
, , 
, ⊢ 
In [10]:
sqrt_2_equation = sqrt_2_equation.square_both_sides()
sqrt_2_equation: , , , ⊢ 
, , , ⊢ 
In [11]:
two_bStar_sqrd__eq__a_star_sqrd = sqrt_2_equation.inner_expr().lhs.distribute()
two_bStar_sqrd__eq__a_star_sqrd: , , , ⊢ 
, , , ⊢ 
Now prove that $2~|~a^*$ via $2 \cdot (b^*)^2 = (a^*)^2$¶
In [12]:
InSet(Exp(b_star, two), NaturalPos).prove()
Proving $2~|~(2 \cdot (b^*)^2)$ is trivial knowing $(b^*)^2 \in \mathbb{N^+}$¶
In [13]:
two_divides_two_bStar_sqrd = Divides(two, Mult(two, Exp(b_star, two))).prove()
two_divides_two_bStar_sqrd: ⊢ 
⊢ 
In [14]:
two_bStar_sqrd__eq__a_star_sqrd.sub_right_side_into(two_divides_two_bStar_sqrd)
, , , ⊢ 
$2~|~(a^*)$ was proven as a side-effect of $2~|~(a^*)^2$ since any integer is even if its square is even¶
In [15]:
two_divides_a_star = Divides(two, a_star).prove()
two_divides_a_star: , , , ⊢ 
, , , ⊢ 
In [16]:
two_sqrd__divides__a_star_sqrd = \
two_divides_a_star.introduce_common_exponent(two, auto_simplify=False)
two_sqrd__divides__a_star_sqrd: , , , ⊢ 
, , , ⊢ 
Derive $2^{2}~|~2 \cdot (b^{*})^2$ from $2^{2}~|~(a^{*})^2$¶
In [17]:
two_sqrd__divides__two_bStar_sqrd = \
two_bStar_sqrd__eq__a_star_sqrd.sub_left_side_into(
two_sqrd__divides__a_star_sqrd)
two_sqrd__divides__two_bStar_sqrd: , , , ⊢ 
, , , ⊢ 
Derive $2~|~(b^*)^2$ from $2^{2}~|~2 \cdot (b^{*})^2$¶
In [18]:
two_sqrd__eq__two_times_two = Exp(two, two).expansion(auto_simplify=False)
two_sqrd__eq__two_times_two: ⊢ 
In [19]:
two_sqrd__eq__two_times_two.sub_right_side_into(
two_sqrd__divides__two_bStar_sqrd)
, , , ⊢ 
In [20]:
Divides(two, Exp(b_star, two)).prove()
, , , ⊢ 
Finally, derive $2~|~(b^*)$ from $2~|~(b^*)^2$¶
In [21]:
two_divides_bStar = Divides(two, b_star).prove()
two_divides_bStar: , , , ⊢ 
, , , ⊢ 
Prove a contradiction given that $2~|~(a^*)$, $2~|~(b^*)$, and $a^*$ and $b^*$ were chosen to be relatively prime¶
In [22]:
a_star_bStar_relatively_prime = GCD(a_star, b_star).deduce_relatively_prime()
a_star_bStar_relatively_prime: , , ⊢ 
, , ⊢ 
In [23]:
two_does_not_divide_both = a_star_bStar_relatively_prime.instantiate({p:two})
two_does_not_divide_both: , , ⊢ 
, , ⊢ 
In [24]:
contradiction_with_choices = two_does_not_divide_both.derive_contradiction()
contradiction_with_choices: , , , ⊢ 
, , , ⊢ 
Use the existence of $a^*$ and $b^*$, assuming $\sqrt{2} \in \mathbb{Q}$, to eliminate extra assumptions (effective Skolemization)¶
In [25]:
contradiction = contradiction_with_choices.eliminate(a_star, b_star)
contradiction: ⊢
⊢ Prove $\sqrt{2} \notin \mathbb{Q}$ via contradiction¶
In [26]:
sqrt2_impl_F = contradiction.as_implication(hypothesis=sqrt_2_is_rational)
sqrt2_impl_F: ⊢ 
In [27]:
sqrt2_impl_F.deny_antecedent(assumptions=[])
In [28]:
%qed
Out[28]:
