The square root of two is irrational

src/elementary-number-theory.lagda.md

@@ -113,6 +113,7 @@ open import elementary-number-theory.integer-partitions public
 open import elementary-number-theory.integers public
 open import elementary-number-theory.interior-closed-intervals-rational-numbers public
 open import elementary-number-theory.intersections-closed-intervals-rational-numbers public
+open import elementary-number-theory.irrationality-square-root-of-two public
 open import elementary-number-theory.jacobi-symbol public
 open import elementary-number-theory.kolakoski-sequence public
 open import elementary-number-theory.legendre-symbol 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/irrationality-square-root-of-two.lagda.md

@@ -0,0 +1,132 @@
+# The irrationality of the square root of two
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+module elementary-number-theory.irrationality-square-root-of-two where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.absolute-value-integers
+open import elementary-number-theory.divisibility-integers
+open import elementary-number-theory.integer-fractions
+open import elementary-number-theory.integers
+open import elementary-number-theory.multiplication-integer-fractions
+open import elementary-number-theory.multiplication-integers
+open import elementary-number-theory.multiplication-natural-numbers
+open import elementary-number-theory.multiplication-rational-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.parity-natural-numbers
+open import elementary-number-theory.positive-integers
+open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.relatively-prime-integers
+open import elementary-number-theory.squares-integers
+open import elementary-number-theory.squares-natural-numbers
+open import elementary-number-theory.squares-rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.negated-equality
+```
+
+</details>
+
+## Idea
+
+There is no [rational number](elementary-number-theory.rational-numbers.md)
+whose [square](elementary-number-theory.squares-rational-numbers.md) is two.
+
+The irrationality of the square root of two is the
+[1st](literature.100-theorems.md#1) theorem on
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
+[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
+
+This file proves that two is not the square of any rational number.
+
+## Proof
+
+```agda
+abstract opaque
+  unfolding rational-fraction-ℤ mul-ℚ
+
+  neq-two-square-ℚ : (q : ℚ) → square-ℚ q ≠ rational-ℕ 2
+  neq-two-square-ℚ (p/q@(p , q⁺@(q , is-pos-q)) , coprime-p-q) p²/q²=2 =
+    let
+      qℕ = succ-ℕ (nat-positive-ℤ q⁺)
+      qℕ=q : int-ℕ qℕ ＝ q
+      qℕ=q =
+        inv (int-positive-int-ℕ _) ∙ ap int-ℤ⁺ (is-section-nat-positive-ℤ q⁺)
+      |p|²=qℕ²2 : square-ℕ (abs-ℤ p) ＝ square-ℕ qℕ *ℕ 2
+      |p|²=qℕ²2 =
+        is-injective-int-ℕ
+          ( equational-reasoning
+              int-ℕ (square-ℕ (abs-ℤ p))
+              ＝ square-ℤ p
+                by square-abs-ℤ p
+              ＝ square-ℤ p *ℤ one-ℤ
+                by inv (right-unit-law-mul-ℤ _)
+              ＝ int-ℕ 2 *ℤ square-ℤ q
+                by
+                  sim-fraction-ℤ-eq-ℚ
+                    ( mul-fraction-ℤ p/q p/q)
+                    ( in-fraction-ℤ (int-ℕ 2))
+                    ( ( p²/q²=2) ∙
+                      ( inv (is-retraction-rational-fraction-ℚ (rational-ℕ 2))))
+              ＝ int-ℕ 2 *ℤ square-ℤ (int-ℕ qℕ)
+                by ap-mul-ℤ refl (ap square-ℤ (inv qℕ=q))
+              ＝ int-ℕ 2 *ℤ int-ℕ (square-ℕ qℕ)
+                by ap-mul-ℤ refl (square-int-ℕ qℕ)
+              ＝ int-ℕ (2 *ℕ square-ℕ qℕ)
+                by mul-int-ℕ _ _
+              ＝ int-ℕ (square-ℕ qℕ *ℕ 2)
+                by ap int-ℕ (commutative-mul-ℕ 2 (square-ℕ qℕ)))
+      (k , k2=|p|) =
+        is-even-is-even-square-ℕ (abs-ℤ p) (square-ℕ qℕ , inv |p|²=qℕ²2)
+      k²2=qℕ² : square-ℕ k *ℕ 2 ＝ square-ℕ qℕ
+      k²2=qℕ² =
+        is-injective-right-mul-succ-ℕ
+          ( 1)
+          ( equational-reasoning
+            square-ℕ k *ℕ 2 *ℕ 2
+            ＝ square-ℕ k *ℕ square-ℕ 2
+              by associative-mul-ℕ (square-ℕ k) 2 2
+            ＝ square-ℕ (k *ℕ 2)
+              by inv (distributive-square-mul-ℕ k 2)
+            ＝ square-ℕ (abs-ℤ p)
+              by ap square-ℕ k2=|p|
+            ＝ square-ℕ qℕ *ℕ 2
+              by |p|²=qℕ²2)
+      (l , l2=qℕ) = is-even-is-even-square-ℕ qℕ (square-ℕ k , k²2=qℕ²)
+    in
+      rec-coproduct
+        ( λ ())
+        ( λ ())
+        ( is-one-or-neg-one-is-unit-ℤ
+          ( int-ℕ 2)
+          ( is-unit-div-relatively-prime-ℤ
+            ( p)
+            ( q)
+            ( int-ℕ 2)
+            ( coprime-p-q)
+            ( rec-coproduct
+                ( λ p=|p| →
+                  ( int-ℕ k , mul-int-ℕ k 2 ∙ ap int-ℕ k2=|p| ∙ inv p=|p|))
+                ( λ p=-|p| →
+                  ( neg-ℤ (int-ℕ k) ,
+                    ( left-negative-law-mul-ℤ _ _) ∙
+                    ( ap neg-ℤ (mul-int-ℕ k 2)) ∙
+                    ( ap (neg-ℤ ∘ int-ℕ) k2=|p|) ∙
+                    ( inv p=-|p|)))
+                ( is-pos-or-neg-abs-ℤ p) ,
+              ( int-ℕ l , mul-int-ℕ l 2 ∙ ap int-ℕ l2=qℕ ∙ qℕ=q))))
+```
+
+## See also
+
+- [The square root of 2 as a real number is not a rational real number](real-numbers.irrationality-square-root-of-two.md)

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

@@ -91,6 +91,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 +195,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
 

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