Different Proofs

3. Irrationality of √2🔗

Definition3.1
Group: Irrationality of square root of 2. (5)
Hover another entry in this group to preview it.
L∃∀N
Used by 2
Hover a use site to preview it.
Preview
Theorem 3.3
Loading preview
Hover a use site to preview it.

The real number \sqrt{2} is irrational: it is not the image of any rational number under the canonical embedding \mathbb{Q} \hookrightarrow \mathbb{R}.

Lean code for Definition3.11 definition
  • def IrrationalSqrtTwoIrrationalSqrtTwo : Prop : PropThe universe of propositions. `Prop ≡ Sort 0`.
    
    Every proposition is propositionally equal to either `True` or `False`. 
    def IrrationalSqrtTwoIrrationalSqrtTwo : Prop : PropThe universe of propositions. `Prop ≡ Sort 0`.
    
    Every proposition is propositionally equal to either `True` or `False`. 
Definition3.2
Group: Irrationality of square root of 2. (5)
Hover another entry in this group to preview it.
L∃∀Nused by 1

The natural-number form says that the equation p^2 = 2q^2 has no solution in natural numbers with q \neq 0.

Lean code for Definition3.21 definition
  • def IrrationalSqrtTwoNatIrrationalSqrtTwoNat : Prop : PropThe universe of propositions. `Prop ≡ Sort 0`.
    
    Every proposition is propositionally equal to either `True` or `False`. 
    def IrrationalSqrtTwoNatIrrationalSqrtTwoNat : Prop : PropThe universe of propositions. `Prop ≡ Sort 0`.
    
    Every proposition is propositionally equal to either `True` or `False`. 
Theorem3.3
Group: Irrationality of square root of 2. (5)
Hover another entry in this group to preview it.
L∃∀N
Used by 2
Hover a use site to preview it.
Preview
Theorem 3.4
Loading preview
Hover a use site to preview it.

The natural-number statement Definition 3.2 implies the real statement Definition 3.1.

Lean code for Theorem3.31 theorem
  • theorem IrrationalSqrtTwoNat_impl_IrrationalSqrtTwoIrrationalSqrtTwoNat_impl_IrrationalSqrtTwo : IrrationalSqrtTwoNat → IrrationalSqrtTwo :
      IrrationalSqrtTwoNatIrrationalSqrtTwoNat : Prop  IrrationalSqrtTwoIrrationalSqrtTwo : Prop
    theorem IrrationalSqrtTwoNat_impl_IrrationalSqrtTwoIrrationalSqrtTwoNat_impl_IrrationalSqrtTwo : IrrationalSqrtTwoNat → IrrationalSqrtTwo :
      IrrationalSqrtTwoNatIrrationalSqrtTwoNat : Prop  IrrationalSqrtTwoIrrationalSqrtTwo : Prop
Proof for Theorem 3.3

If \sqrt{2} were the image of a rational r, squaring gives r^2 = 2 in \mathbb{Q}. Writing r as the quotient of its numerator and denominator and clearing denominators yields \mathrm{num}(r)^2 = 2\,\mathrm{den}(r)^2, so taking absolute values gives a natural-number solution of p^2 = 2q^2 with q = \mathrm{den}(r) \neq 0.

First proof is by infinite descent.

Theorem3.4
Group: Irrationality of square root of 2. (5)
Hover another entry in this group to preview it.
L∃∀Nused by 0

\sqrt{2} is irrational.

Lean code for Theorem3.41 theorem
  • theorem IrrationalSqrtTwo_DescentIrrationalSqrtTwo_Descent : IrrationalSqrtTwo : IrrationalSqrtTwoIrrationalSqrtTwo : Prop
    theorem IrrationalSqrtTwo_DescentIrrationalSqrtTwo_Descent : IrrationalSqrtTwo :
      IrrationalSqrtTwoIrrationalSqrtTwo : Prop
Proof for Theorem 3.4

Use Theorem 3.3 to reduce to the natural-number form. Suppose p^2 = 2q^2 with q > 0. Then 2 \mid p^2, so 2 \mid p since 2 is prime; write p = 2r. Substituting gives q^2 = 2r^2, a new solution whose first component q is strictly smaller than p. By strong induction no solution with q \neq 0 exists.

Second proof is by 2-adic valuation.

Theorem3.5
Group: Irrationality of square root of 2. (5)
Hover another entry in this group to preview it.
L∃∀Nused by 0

\sqrt{2} is irrational.

Lean code for Theorem3.51 theorem
  • theorem IrrationalSqrtTwo_ValuationIrrationalSqrtTwo_Valuation : IrrationalSqrtTwo : IrrationalSqrtTwoIrrationalSqrtTwo : Prop
    theorem IrrationalSqrtTwo_ValuationIrrationalSqrtTwo_Valuation : IrrationalSqrtTwo :
      IrrationalSqrtTwoIrrationalSqrtTwo : Prop
Proof for Theorem 3.5

Use Theorem 3.3 to reduce to the natural-number form. Apply the exponent of 2 in the prime factorization to both sides of p^2 = 2q^2. The left side has even 2-adic valuation 2v_2(p), while the right side has odd valuation 1 + 2v_2(q), a contradiction.

Third proof is by Fermat's Last Theorem for exponent 3.

Theorem3.6
Group: Irrationality of square root of 2. (5)
Hover another entry in this group to preview it.
L∃∀Nused by 0

\sqrt{2} is irrational.

Lean code for Theorem3.61 theorem
  • theorem IrrationalSqrtTwo_FermatLastTheoremIrrationalSqrtTwo_FermatLastTheorem : IrrationalSqrtTwo : IrrationalSqrtTwoIrrationalSqrtTwo : Prop
    theorem IrrationalSqrtTwo_FermatLastTheoremIrrationalSqrtTwo_FermatLastTheorem : IrrationalSqrtTwo :
      IrrationalSqrtTwoIrrationalSqrtTwo : Prop
Proof for Theorem 3.6

This proof establishes the irrationality of \sqrt{2} Definition 3.1 directly, without the natural-number reduction. One has the identity (18+17\sqrt{2})^3 + (18-17\sqrt{2})^3 = 42^3, due to Jarvis and Meekin. If \sqrt{2} were a rational r, then 18+17r, 18-17r, and 42 would be nonzero rationals (nonzero because (\pm 18/17)^2 \neq 2) solving x^3 + y^3 = z^3, contradicting Fermat's Last Theorem for exponent 3. See this Math StackExchange answer.