The square root of two is irrational (#1718)

We prove both the elementary version (two is not the square of any
rational number) and the real version (the square root of two is not a
rational real number).

Author: lowasser

src/elementary-number-theory.lagda.md

@@ -235,6 +235,7 @@ open import elementary-number-theory.unit-similarity-standard-finite-types publi
 open import elementary-number-theory.universal-property-conatural-numbers public
 open import elementary-number-theory.universal-property-integers public
 open import elementary-number-theory.universal-property-natural-numbers public
+open import elementary-number-theory.unsolvability-of-squaring-to-two-in-rational-numbers public
 open import elementary-number-theory.upper-bounds-natural-numbers public
 open import elementary-number-theory.well-ordering-principle-natural-numbers public
 open import elementary-number-theory.well-ordering-principle-standard-finite-types public

src/elementary-number-theory/absolute-value-integers.lagda.md

@@ -250,3 +250,14 @@ abstract
   double-negative-law-mul-abs-ℤ x y =
     ap abs-ℤ (inv (double-negative-law-mul-ℤ x y))
 ```
+
+### `x = |x|` or `x = -|x|`
+
+```agda
+abstract
+  is-pos-or-neg-abs-ℤ :
+    (x : ℤ) → (x ＝ int-ℕ (abs-ℤ x)) + (x ＝ neg-ℤ (int-ℕ (abs-ℤ x)))
+  is-pos-or-neg-abs-ℤ (inr (inl unit)) = inl refl
+  is-pos-or-neg-abs-ℤ (inr (inr n)) = inl refl
+  is-pos-or-neg-abs-ℤ (inl n) = inr refl
+```

src/elementary-number-theory/multiplication-natural-numbers.lagda.md

@@ -345,6 +345,19 @@ abstract
     is-zero-mul-ℕ-is-zero-right-summand x y H
 ```
 
+### Swapping laws
+
+```agda
+abstract
+  right-swap-mul-ℕ : (x y z : ℕ) → (x *ℕ y) *ℕ z ＝ (x *ℕ z) *ℕ y
+  right-swap-mul-ℕ x y z =
+    equational-reasoning
+      x *ℕ y *ℕ z
+      ＝ x *ℕ (y *ℕ z) by associative-mul-ℕ x y z
+      ＝ x *ℕ (z *ℕ y) by ap (x *ℕ_) (commutative-mul-ℕ y z)
+      ＝ x *ℕ z *ℕ y by inv (associative-mul-ℕ x z y)
+```
+
 ## See also
 
 - [Squares of natural numbers](elementary-number-theory.squares-natural-numbers.md)

src/elementary-number-theory/parity-natural-numbers.lagda.md

@@ -7,14 +7,17 @@ module elementary-number-theory.parity-natural-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.divisibility-natural-numbers
 open import elementary-number-theory.equality-natural-numbers
 open import elementary-number-theory.modular-arithmetic-standard-finite-types
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.nonzero-natural-numbers
+open import elementary-number-theory.squares-natural-numbers
 
 open import foundation.action-on-identifications-functions
+open import foundation.coproduct-types
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
@@ -188,3 +191,66 @@ abstract
     (x y : ℕ) → is-odd-ℕ x → is-even-ℕ y → x ≠ y
   noneq-odd-even x y odd-x even-y x=y = odd-x (inv-tr is-even-ℕ x=y even-y)
 ```
+
+### If `x` and `y` are odd, `xy` is odd
+
+```agda
+abstract
+  is-odd-mul-is-odd-ℕ :
+    (x y : ℕ) → is-odd-ℕ x → is-odd-ℕ y → is-odd-ℕ (x *ℕ y)
+  is-odd-mul-is-odd-ℕ _ _ odd-x odd-y
+    with has-odd-expansion-is-odd _ odd-x | has-odd-expansion-is-odd _ odd-y
+  ... | (m , refl) | (n , refl) =
+    is-odd-has-odd-expansion _
+      ( m *ℕ (2 *ℕ n) +ℕ m +ℕ n ,
+        ( equational-reasoning
+          succ-ℕ ((m *ℕ (2 *ℕ n) +ℕ m +ℕ n) *ℕ 2)
+          ＝ succ-ℕ ((m *ℕ (2 *ℕ n) +ℕ m) *ℕ 2 +ℕ n *ℕ 2)
+            by ap succ-ℕ (right-distributive-mul-add-ℕ (m *ℕ (2 *ℕ n) +ℕ m) n 2)
+          ＝ (m *ℕ (2 *ℕ n) +ℕ (m *ℕ 1)) *ℕ 2 +ℕ succ-ℕ (n *ℕ 2)
+            by
+              ap
+                ( λ k → succ-ℕ ((m *ℕ (2 *ℕ n) +ℕ k) *ℕ 2 +ℕ n *ℕ 2))
+                ( inv (right-unit-law-mul-ℕ m))
+          ＝ m *ℕ (2 *ℕ n +ℕ 1) *ℕ 2 +ℕ succ-ℕ (n *ℕ 2)
+            by
+              ap
+                ( λ k → k *ℕ 2 +ℕ succ-ℕ (n *ℕ 2))
+                ( inv (left-distributive-mul-add-ℕ m (2 *ℕ n) 1))
+          ＝ m *ℕ 2 *ℕ succ-ℕ (2 *ℕ n) +ℕ succ-ℕ (n *ℕ 2)
+            by ap (_+ℕ succ-ℕ (n *ℕ 2)) (right-swap-mul-ℕ m (succ-ℕ (2 *ℕ n)) 2)
+          ＝ m *ℕ 2 *ℕ succ-ℕ (n *ℕ 2) +ℕ 1 *ℕ succ-ℕ (n *ℕ 2)
+            by
+              ap-add-ℕ
+                ( ap (λ k → m *ℕ 2 *ℕ succ-ℕ k) (commutative-mul-ℕ 2 n))
+                ( inv (left-unit-law-mul-ℕ (succ-ℕ (n *ℕ 2))))
+          ＝ succ-ℕ (m *ℕ 2) *ℕ succ-ℕ (n *ℕ 2)
+            by inv (right-distributive-mul-add-ℕ (m *ℕ 2) 1 (succ-ℕ (n *ℕ 2)))))
+```
+
+### If `xy` is even, `x` or `y` is even
+
+```agda
+abstract
+  is-even-either-factor-is-even-mul-ℕ :
+    (x y : ℕ) → is-even-ℕ (x *ℕ y) → (is-even-ℕ x) + (is-even-ℕ y)
+  is-even-either-factor-is-even-mul-ℕ x y is-even-xy =
+    rec-coproduct
+      ( inl)
+      ( λ is-odd-x →
+        rec-coproduct
+          ( inr)
+          ( λ is-odd-y →
+            ex-falso (is-odd-mul-is-odd-ℕ x y is-odd-x is-odd-y is-even-xy))
+          ( is-decidable-is-even-ℕ y))
+      ( is-decidable-is-even-ℕ x)
+```
+
+### If `x²` is even, `x` is even
+
+```agda
+abstract
+  is-even-is-even-square-ℕ : (x : ℕ) → is-even-ℕ (square-ℕ x) → is-even-ℕ x
+  is-even-is-even-square-ℕ x is-even-x² =
+    rec-coproduct id id (is-even-either-factor-is-even-mul-ℕ x x is-even-x²)
+```

src/elementary-number-theory/positive-integers.lagda.md

@@ -23,6 +23,7 @@ open import foundation.equivalences
 open import foundation.existential-quantification
 open import foundation.function-types
 open import foundation.identity-types
+open import foundation.negation
 open import foundation.propositions
 open import foundation.retractions
 open import foundation.sections
@@ -91,6 +92,9 @@ module _
   int-positive-ℤ : ℤ
   int-positive-ℤ = pr1 p
 
+  int-ℤ⁺ : ℤ
+  int-ℤ⁺ = int-positive-ℤ
+
   is-positive-int-positive-ℤ : is-positive-ℤ int-positive-ℤ
   is-positive-int-positive-ℤ = pr2 p
 ```
@@ -192,6 +196,11 @@ abstract
 positive-int-ℕ : ℕ → positive-ℤ
 positive-int-ℕ = rec-ℕ one-positive-ℤ (λ _ → succ-positive-ℤ)
 
+abstract
+  int-positive-int-ℕ : (n : ℕ) → int-positive-ℤ (positive-int-ℕ n) ＝ in-pos-ℤ n
+  int-positive-int-ℕ 0 = refl
+  int-positive-int-ℕ (succ-ℕ n) = ap succ-ℤ (int-positive-int-ℕ n)
+
 nat-positive-ℤ : positive-ℤ → ℕ
 nat-positive-ℤ (inr (inr x) , H) = x
 
@@ -239,6 +248,13 @@ is-countable-positive-ℤ =
       ( is-surjective-is-equiv is-equiv-positive-int-ℕ))
 ```
 
+### Zero is not positive
+
+```agda
+not-is-positive-zero-ℤ : ¬ (is-positive-ℤ zero-ℤ)
+not-is-positive-zero-ℤ ()
+```
+
 ## See also
 
 - The relations between positive and nonnegative, negative and nonnpositive

src/elementary-number-theory/rational-numbers.lagda.md

@@ -23,6 +23,7 @@ open import foundation.dependent-pair-types
 open import foundation.equality-cartesian-product-types
 open import foundation.equality-dependent-pair-types
 open import foundation.identity-types
+open import foundation.logical-equivalences
 open import foundation.negation
 open import foundation.propositions
 open import foundation.reflecting-maps-equivalence-relations
@@ -31,6 +32,7 @@ open import foundation.sections
 open import foundation.sets
 open import foundation.subtypes
 open import foundation.surjective-maps
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import set-theory.countable-sets
@@ -173,20 +175,50 @@ opaque
 
 ## Properties
 
-### The rational images of two similar integer fractions are equal
+### Two integer fractions are similar if and only if they are equal as rational numbers
 
 ```agda
-opaque
-  unfolding rational-fraction-ℤ
+module _
+  (x y : fraction-ℤ)
+  where
 
-  eq-ℚ-sim-fraction-ℤ :
-    (x y : fraction-ℤ) → (H : sim-fraction-ℤ x y) →
-    rational-fraction-ℤ x ＝ rational-fraction-ℤ y
-  eq-ℚ-sim-fraction-ℤ x y H =
-    eq-pair-Σ'
-      ( pair
-        ( unique-reduce-fraction-ℤ x y H)
-        ( eq-is-prop (is-prop-is-reduced-fraction-ℤ (reduce-fraction-ℤ y))))
+  abstract opaque
+    unfolding rational-fraction-ℤ
+
+    eq-ℚ-sim-fraction-ℤ :
+      sim-fraction-ℤ x y → rational-fraction-ℤ x ＝ rational-fraction-ℤ y
+    eq-ℚ-sim-fraction-ℤ H =
+      eq-pair-Σ'
+        ( pair
+          ( unique-reduce-fraction-ℤ x y H)
+          ( eq-is-prop (is-prop-is-reduced-fraction-ℤ (reduce-fraction-ℤ y))))
+
+    sim-fraction-ℤ-eq-ℚ :
+      rational-fraction-ℤ x ＝ rational-fraction-ℤ y → sim-fraction-ℤ x y
+    sim-fraction-ℤ-eq-ℚ H =
+      transitive-sim-fraction-ℤ
+        ( x)
+        ( reduce-fraction-ℤ y)
+        ( y)
+        ( symmetric-sim-fraction-ℤ
+          ( y)
+          ( reduce-fraction-ℤ y)
+          ( sim-reduced-fraction-ℤ y))
+        ( transitive-sim-fraction-ℤ
+          ( x)
+          ( reduce-fraction-ℤ x)
+          ( reduce-fraction-ℤ y)
+          ( tr
+            ( sim-fraction-ℤ (reduce-fraction-ℤ x))
+            ( ap fraction-ℚ H)
+            ( refl-sim-fraction-ℤ (reduce-fraction-ℤ x)))
+          ( sim-reduced-fraction-ℤ x))
+
+    eq-ℚ-iff-sim-fraction-ℤ :
+      (sim-fraction-ℤ x y) ↔ (rational-fraction-ℤ x ＝ rational-fraction-ℤ y)
+    eq-ℚ-iff-sim-fraction-ℤ =
+      ( eq-ℚ-sim-fraction-ℤ ,
+        sim-fraction-ℤ-eq-ℚ)
 ```
 
 ### The type of rationals is a set

src/elementary-number-theory/relatively-prime-integers.lagda.md

@@ -8,12 +8,16 @@ module elementary-number-theory.relatively-prime-integers where
 
 ```agda
 open import elementary-number-theory.absolute-value-integers
+open import elementary-number-theory.divisibility-integers
 open import elementary-number-theory.greatest-common-divisor-integers
 open import elementary-number-theory.integers
 open import elementary-number-theory.relatively-prime-natural-numbers
 
 open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.logical-equivalences
 open import foundation.propositions
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 ```
 
@@ -60,6 +64,20 @@ abstract
   is-relatively-prime-is-relatively-prime-abs-ℤ {a} {b} H = ap int-ℕ H
 ```
 
+### For two relatively prime integers `x` and `y` and any integer `d`, if `d` divides `x` and `y`, `d` is a unit
+
+```agda
+abstract
+  is-unit-div-relatively-prime-ℤ :
+    (x y : ℤ) (d : ℤ) → is-relatively-prime-ℤ x y →
+    is-common-divisor-ℤ x y d → is-unit-ℤ d
+  is-unit-div-relatively-prime-ℤ x y d gcd=1 d|x∧d|y =
+    tr
+      ( λ k → div-ℤ d k)
+      ( gcd=1)
+      ( forward-implication (pr2 (is-gcd-gcd-ℤ x y) d) d|x∧d|y)
+```
+
 ### For any two integers `a` and `b` that are not both `0`, the integers `a/gcd(a,b)` and `b/gcd(a,b)` are relatively prime
 
 ```agda

src/elementary-number-theory/squares-integers.lagda.md

@@ -63,6 +63,14 @@ is-nonnegative-square-ℤ a =
     ( decide-is-negative-is-nonnegative-ℤ {a})
 ```
 
+### The square of an embedding of a natural number is the embedding of the square of the natural number
+
+```agda
+abstract
+  square-int-ℕ : (n : ℕ) → square-ℤ (int-ℕ n) ＝ int-ℕ (square-ℕ n)
+  square-int-ℕ n = mul-int-ℕ n n
+```
+
 ### The square of the negation of `x` is the square of `x`
 
 ```agda
@@ -109,6 +117,32 @@ pr2
       ( pr2 (is-square-int-is-square-nat (root , pf-square)))))
 ```
 
+### `|x|² = x²`
+
+```agda
+abstract
+  square-abs-ℤ : (x : ℤ) → int-ℕ (square-ℕ (abs-ℤ x)) ＝ square-ℤ x
+  square-abs-ℤ x =
+    rec-coproduct
+      ( λ x=|x| →
+        equational-reasoning
+          int-ℕ (square-ℕ (abs-ℤ x))
+          ＝ square-ℤ (int-ℕ (abs-ℤ x))
+            by inv (mul-int-ℕ (abs-ℤ x) (abs-ℤ x))
+          ＝ square-ℤ x
+            by inv (ap square-ℤ x=|x|))
+      ( λ x=-|x| →
+        equational-reasoning
+          int-ℕ (square-ℕ (abs-ℤ x))
+          ＝ square-ℤ (int-abs-ℤ x)
+            by inv (mul-int-ℕ (abs-ℤ x) (abs-ℤ x))
+          ＝ square-ℤ (neg-ℤ (int-abs-ℤ x))
+            by inv (square-neg-ℤ (int-abs-ℤ x))
+          ＝ square-ℤ x
+            by inv (ap square-ℤ x=-|x|))
+      ( is-pos-or-neg-abs-ℤ x)
+```
+
 ### Squareness in ℤ is decidable
 
 ```agda

src/elementary-number-theory/squares-natural-numbers.lagda.md

@@ -96,6 +96,15 @@ abstract
           ( left-distributive-mul-add-ℕ 2 n 2))
 ```
 
+### Squaring distributes over multiplication
+
+```agda
+abstract
+  distributive-square-mul-ℕ :
+    (m n : ℕ) → square-ℕ (m *ℕ n) ＝ square-ℕ m *ℕ square-ℕ n
+  distributive-square-mul-ℕ m n = interchange-law-mul-mul-ℕ m n m n
+```
+
 ### `n > √n` for `n > 1`
 
 The idea is to assume `n = m + 2 ≤ sqrt(m + 2)` for some `m : ℕ` and derive a

src/elementary-number-theory/strict-inequality-integers.lagda.md

@@ -129,6 +129,29 @@ connected-le-ℤ x y H =
     ( decide-sign-nonzero-ℤ (H ∘ eq-diff-ℤ))
 ```
 
+### Strict inequality on the integers is irreflexive
+
+```agda
+abstract
+  irreflexive-le-ℤ : (x : ℤ) → ¬ (le-ℤ x x)
+  irreflexive-le-ℤ x =
+    inv-tr
+      ( λ z → ¬ (is-positive-ℤ z))
+      ( right-inverse-law-add-ℤ x)
+      ( not-is-positive-zero-ℤ)
+```
+
+### If `x < y`, `x ≠ y`
+
+```agda
+abstract
+  neq-le-ℤ : (x y : ℤ) → le-ℤ x y → x ≠ y
+  neq-le-ℤ x _ x<x refl = irreflexive-le-ℤ x x<x
+
+  neq-le-ℤ' : (x y : ℤ) → le-ℤ y x → x ≠ y
+  neq-le-ℤ' _ y y<y refl = irreflexive-le-ℤ y y<y
+```
+
 ### Any integer is strictly greater than its predecessor
 
 ```agda