The irrationality of the square root of two

Content created by Louis Wasserman.

Created on 2025-11-19.
Last modified on 2025-11-19.

{-# OPTIONS --lossy-unification #-}

module real-numbers.irrationality-square-root-of-two where
Imports 
open import elementary-number-theory.rational-numbers
open import elementary-number-theory.squares-rational-numbers
open import elementary-number-theory.unsolvability-of-squaring-to-two-in-rational-numbers

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.negation
open import foundation.universe-levels

open import real-numbers.irrational-real-numbers
open import real-numbers.nonnegative-real-numbers
open import real-numbers.rational-real-numbers
open import real-numbers.similarity-real-numbers
open import real-numbers.square-roots-nonnegative-real-numbers
open import real-numbers.squares-real-numbers

Idea

The square root of two is not a rational real number.

The irrationality of the square root of two is the 1st theorem on Freek Wiedijk’s list of 100 theorems [Wie].

Proof

abstract
  irrational-sqrt-two-ℝ :
    is-irrational-ℝ (real-sqrt-ℝ⁰⁺ (nonnegative-real-ℕ 2))
  irrational-sqrt-two-ℝ (q , √2=q) =
    is-not-square-two-ℚ
      ( q ,
        is-injective-real-ℚ
          ( ( inv (eq-real-square-sqrt-ℝ⁰⁺ (nonnegative-real-ℕ 2))) ∙
            ( ap
              ( square-ℝ)
              ( eq-sim-ℝ
                ( sim-rational-ℝ
                  ( real-sqrt-ℝ⁰⁺ (nonnegative-real-ℕ 2) , q , √2=q)))) ∙
            ( square-real-ℚ q)))

See also

References

[Wie]
Freek Wiedijk. Formalizing 100 theorems. URL: https://www.cs.ru.nl/~freek/100/.

Recent changes