diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index 33be5ca7f1..5340946090 100644 --- a/src/elementary-number-theory.lagda.md +++ b/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 diff --git a/src/elementary-number-theory/absolute-value-integers.lagda.md b/src/elementary-number-theory/absolute-value-integers.lagda.md index 030d2f663e..112d558d78 100644 --- a/src/elementary-number-theory/absolute-value-integers.lagda.md +++ b/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 +``` diff --git a/src/elementary-number-theory/multiplication-natural-numbers.lagda.md b/src/elementary-number-theory/multiplication-natural-numbers.lagda.md index 335c42ad42..5a6a8732ca 100644 --- a/src/elementary-number-theory/multiplication-natural-numbers.lagda.md +++ b/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) diff --git a/src/elementary-number-theory/parity-natural-numbers.lagda.md b/src/elementary-number-theory/parity-natural-numbers.lagda.md index 5a7c82123c..06eadf1860 100644 --- a/src/elementary-number-theory/parity-natural-numbers.lagda.md +++ b/src/elementary-number-theory/parity-natural-numbers.lagda.md @@ -7,14 +7,17 @@ module elementary-number-theory.parity-natural-numbers where
Imports ```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²) +``` diff --git a/src/elementary-number-theory/positive-integers.lagda.md b/src/elementary-number-theory/positive-integers.lagda.md index 4d20d11351..03dc324291 100644 --- a/src/elementary-number-theory/positive-integers.lagda.md +++ b/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 diff --git a/src/elementary-number-theory/rational-numbers.lagda.md b/src/elementary-number-theory/rational-numbers.lagda.md index ed81dcc1dc..1c7bb3cb8e 100644 --- a/src/elementary-number-theory/rational-numbers.lagda.md +++ b/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 diff --git a/src/elementary-number-theory/relatively-prime-integers.lagda.md b/src/elementary-number-theory/relatively-prime-integers.lagda.md index 6090b9bf26..bfceab694d 100644 --- a/src/elementary-number-theory/relatively-prime-integers.lagda.md +++ b/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 diff --git a/src/elementary-number-theory/squares-integers.lagda.md b/src/elementary-number-theory/squares-integers.lagda.md index 2a7edb2a63..23617fe125 100644 --- a/src/elementary-number-theory/squares-integers.lagda.md +++ b/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 diff --git a/src/elementary-number-theory/squares-natural-numbers.lagda.md b/src/elementary-number-theory/squares-natural-numbers.lagda.md index 75f66ed2fd..735e4d421a 100644 --- a/src/elementary-number-theory/squares-natural-numbers.lagda.md +++ b/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 diff --git a/src/elementary-number-theory/strict-inequality-integers.lagda.md b/src/elementary-number-theory/strict-inequality-integers.lagda.md index c1dedd545f..76f7714639 100644 --- a/src/elementary-number-theory/strict-inequality-integers.lagda.md +++ b/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 _ xImports + +```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 elementary-number-theory.strict-inequality-integers + +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.negation +``` + +
+ +## 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-ℚ + + is-not-square-two-ℚ : ¬ (is-square-ℚ (rational-ℕ 2)) + is-not-square-two-ℚ ((p/q@(p , q⁺@(q , is-pos-q)) , coprime-p-q) , 2=p²/q²) = + 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)) + ( ( inv 2=p²/q²) ∙ + ( 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 + ( neq-le-ℤ' (int-ℕ 2) one-ℤ _) + ( neq-le-ℤ' (int-ℕ 2) neg-one-ℤ _) + ( 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 irrational](real-numbers.irrationality-square-root-of-two.md) diff --git a/src/literature/100-theorems.lagda.md b/src/literature/100-theorems.lagda.md index 81353f5e14..204e54f0cd 100644 --- a/src/literature/100-theorems.lagda.md +++ b/src/literature/100-theorems.lagda.md @@ -11,6 +11,17 @@ module literature.100-theorems where ## The list +### 1. The irrationality of the square root of 2 {#1} + +**Author:** [Louis Wasserman](https://github.com/lowasser) + +```agda +open import elementary-number-theory.unsolvability-of-squaring-to-two-in-rational-numbers using + ( is-not-square-two-ℚ) +open import real-numbers.irrationality-square-root-of-two using + ( irrational-sqrt-two-ℝ) +``` + ### 3. The denumerability of the rational numbers {#3} **Author:** [Fredrik Bakke](https://www.ntnu.edu/employees/fredrik.bakke) diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index f7b0c6a18d..035444db6c 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -38,6 +38,8 @@ open import real-numbers.infima-and-suprema-families-real-numbers public open import real-numbers.infima-families-real-numbers public open import real-numbers.inhabited-finitely-enumerable-subsets-real-numbers public open import real-numbers.inhabited-totally-bounded-subsets-real-numbers public +open import real-numbers.irrational-real-numbers public +open import real-numbers.irrationality-square-root-of-two public open import real-numbers.isometry-addition-real-numbers public open import real-numbers.isometry-difference-real-numbers public open import real-numbers.isometry-negation-real-numbers public diff --git a/src/real-numbers/irrational-real-numbers.lagda.md b/src/real-numbers/irrational-real-numbers.lagda.md new file mode 100644 index 0000000000..2721ab950b --- /dev/null +++ b/src/real-numbers/irrational-real-numbers.lagda.md @@ -0,0 +1,40 @@ +# Irrational real numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.irrational-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.rational-numbers + +open import foundation.dependent-pair-types +open import foundation.negation +open import foundation.propositions +open import foundation.universe-levels + +open import real-numbers.dedekind-real-numbers +open import real-numbers.rational-real-numbers +``` + +
+ +## Idea + +An +{{#concept "irrational real number" WDID=Q607728 WD="irrational number" Agda=is-irrational-ℝ}} +is a [real number](real-numbers.dedekind-real-numbers.md) that is not +[rational](real-numbers.rational-real-numbers.md). + +## Definition + +```agda +is-irrational-prop-ℝ : {l : Level} → ℝ l → Prop l +is-irrational-prop-ℝ x = ¬' (subtype-rational-real x) + +is-irrational-ℝ : {l : Level} → ℝ l → UU l +is-irrational-ℝ x = type-Prop (is-irrational-prop-ℝ x) +``` diff --git a/src/real-numbers/irrationality-square-root-of-two.lagda.md b/src/real-numbers/irrationality-square-root-of-two.lagda.md new file mode 100644 index 0000000000..c3fde382ca --- /dev/null +++ b/src/real-numbers/irrationality-square-root-of-two.lagda.md @@ -0,0 +1,63 @@ +# The irrationality of the square root of two + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.irrationality-square-root-of-two where +``` + +
Imports + +```agda +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](real-numbers.square-roots-nonnegative-real-numbers.md) of two +is not a [rational real number](real-numbers.rational-real-numbers.md). + +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}}. + +## Proof + +```agda +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 + +- [Two is not the square of any rational number](elementary-number-theory.unsolvability-of-squaring-to-two-in-rational-numbers.md) diff --git a/src/real-numbers/nonnegative-real-numbers.lagda.md b/src/real-numbers/nonnegative-real-numbers.lagda.md index d536334e57..fe4444a2b0 100644 --- a/src/real-numbers/nonnegative-real-numbers.lagda.md +++ b/src/real-numbers/nonnegative-real-numbers.lagda.md @@ -10,6 +10,7 @@ module real-numbers.nonnegative-real-numbers where ```agda open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.natural-numbers open import elementary-number-theory.negative-rational-numbers open import elementary-number-theory.nonnegative-rational-numbers open import elementary-number-theory.positive-and-negative-rational-numbers @@ -141,6 +142,13 @@ nonnegative-real-ℚ⁺ : ℚ⁺ → ℝ⁰⁺ lzero nonnegative-real-ℚ⁺ q = nonnegative-real-ℚ⁰⁺ (nonnegative-ℚ⁺ q) ``` +### The canonical embedding of natural numbers in the nonnegative real numbers + +```agda +nonnegative-real-ℕ : ℕ → ℝ⁰⁺ lzero +nonnegative-real-ℕ n = nonnegative-real-ℚ⁰⁺ (nonnegative-rational-ℕ n) +``` + ### Important nonnegative real numbers ```agda diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md index 4e48764ed5..381ab6c0c6 100644 --- a/src/real-numbers/rational-real-numbers.lagda.md +++ b/src/real-numbers/rational-real-numbers.lagda.md @@ -24,6 +24,7 @@ open import foundation.empty-types open import foundation.equivalences open import foundation.function-types open import foundation.identity-types +open import foundation.injective-maps open import foundation.negation open import foundation.propositions open import foundation.retractions @@ -282,3 +283,27 @@ pr2 equiv-rational-real = retraction-rational-rational-ℝ = (rational-real-ℚ , is-retraction-rational-real-ℚ) ``` + +### The canonical embedding of the rational numbers in the real numbers is injective + +```agda +abstract opaque + unfolding real-ℚ + + is-injective-real-ℚ : is-injective real-ℚ + is-injective-real-ℚ {p} {q} pℝ=qℝ = + trichotomy-le-ℚ + ( p) + ( q) + ( λ p