Reciprocals of nonzero natural numbers (#1345)

Many related properties along with it. Hopefully this will help us do
things like simply take half of a rational number and the like.

src/elementary-number-theory.lagda.md

@@ -20,6 +20,7 @@ open import elementary-number-theory.additive-group-of-rational-numbers public
 open import elementary-number-theory.archimedean-property-integer-fractions public
 open import elementary-number-theory.archimedean-property-integers public
 open import elementary-number-theory.archimedean-property-natural-numbers public
+open import elementary-number-theory.archimedean-property-positive-rational-numbers public
 open import elementary-number-theory.archimedean-property-rational-numbers public
 open import elementary-number-theory.arithmetic-functions public
 open import elementary-number-theory.based-induction-natural-numbers public
@@ -173,6 +174,7 @@ open import elementary-number-theory.triangular-numbers public
 open import elementary-number-theory.twin-prime-conjecture public
 open import elementary-number-theory.type-arithmetic-natural-numbers public
 open import elementary-number-theory.unit-elements-standard-finite-types public
+open import elementary-number-theory.unit-fractions-rational-numbers public
 open import elementary-number-theory.unit-similarity-standard-finite-types public
 open import elementary-number-theory.universal-property-conatural-numbers public
 open import elementary-number-theory.universal-property-integers public

src/elementary-number-theory/archimedean-property-integer-fractions.lagda.md

@@ -23,6 +23,7 @@ open import elementary-number-theory.strict-inequality-integers
 open import foundation.dependent-pair-types
 open import foundation.existential-quantification
 open import foundation.identity-types
+open import foundation.propositional-truncations
 open import foundation.transport-along-identifications
 ```
 
@@ -36,28 +37,31 @@ than `n` as an integer fraction times `x`.
 
 ```agda
 abstract
+  bound-archimedean-property-fraction-ℤ :
+    (x y : fraction-ℤ) →
+    is-positive-fraction-ℤ x →
+    Σ ℕ (λ n → le-fraction-ℤ y (in-fraction-ℤ (int-ℕ n) *fraction-ℤ x))
+  bound-archimedean-property-fraction-ℤ
+    x@(px , qx , pos-qx) y@(py , qy , pos-qy) pos-px =
+      let
+        (n , H) =
+          bound-archimedean-property-ℤ
+            ( px *ℤ qy)
+            ( py *ℤ qx)
+            ( is-positive-mul-ℤ pos-px pos-qy)
+      in
+        n ,
+        tr
+          ( le-ℤ (py *ℤ qx))
+          ( inv (associative-mul-ℤ (int-ℕ n) px qy))
+          ( H)
+
   archimedean-property-fraction-ℤ :
     (x y : fraction-ℤ) →
     is-positive-fraction-ℤ x →
     exists
       ℕ
       (λ n → le-fraction-ℤ-Prop y (in-fraction-ℤ (int-ℕ n) *fraction-ℤ x))
-  archimedean-property-fraction-ℤ
-    x@(px , qx , pos-qx) y@(py , qy , pos-qy) pos-px =
-      elim-exists
-        (∃
-          ( ℕ)
-          ( λ n →
-            le-fraction-ℤ-Prop y (in-fraction-ℤ (int-ℕ n) *fraction-ℤ x)))
-        ( λ n H →
-          intro-exists
-            ( n)
-            ( tr
-              ( le-ℤ (py *ℤ qx))
-              ( inv (associative-mul-ℤ (int-ℕ n) px qy))
-              ( H)))
-        ( archimedean-property-ℤ
-          ( px *ℤ qy)
-          ( py *ℤ qx)
-          ( is-positive-mul-ℤ pos-px pos-qy))
+  archimedean-property-fraction-ℤ x y pos-x =
+    unit-trunc-Prop (bound-archimedean-property-fraction-ℤ x y pos-x)
 ```

src/elementary-number-theory/archimedean-property-integers.lagda.md

@@ -24,8 +24,8 @@ open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.existential-quantification
 open import foundation.identity-types
+open import foundation.propositional-truncations
 open import foundation.transport-along-identifications
-open import foundation.unit-type
 ```
 
 </details>
@@ -40,35 +40,40 @@ integer `y`, there is an `n : ℕ` such that `y < int-ℕ n *ℤ x`.
 
 ```agda
 abstract
+  bound-archimedean-property-ℤ :
+    (x y : ℤ) → is-positive-ℤ x → Σ ℕ (λ n → le-ℤ y (int-ℕ n *ℤ x))
+  bound-archimedean-property-ℤ x y pos-x
+    with decide-is-negative-is-nonnegative-ℤ {y}
+  ... | inl neg-y = zero-ℕ , le-zero-is-negative-ℤ y neg-y
+  ... | inr nonneg-y =
+      let
+        (nx , nonzero-nx , nx=x) = pos-ℤ-to-ℕ x pos-x
+        (n , ny<n*nx) =
+          bound-archimedean-property-ℕ
+            ( nx)
+            ( nat-nonnegative-ℤ (y , nonneg-y))
+            ( nonzero-nx)
+      in
+        n ,
+        binary-tr
+          ( le-ℤ)
+          ( ap pr1 (is-section-nat-nonnegative-ℤ (y , nonneg-y)))
+          ( inv (mul-int-ℕ n nx) ∙ ap (int-ℕ n *ℤ_) nx=x)
+          ( le-natural-le-ℤ
+            ( nat-nonnegative-ℤ (y , nonneg-y))
+            ( n *ℕ nx)
+            ( ny<n*nx))
+    where
+      pos-ℤ-to-ℕ :
+        (z : ℤ) →
+        is-positive-ℤ z →
+        Σ ℕ (λ n → is-nonzero-ℕ n × (int-ℕ n ＝ z))
+      pos-ℤ-to-ℕ (inr (inr n)) H = succ-ℕ n , (λ ()) , refl
+
   archimedean-property-ℤ :
     (x y : ℤ) → is-positive-ℤ x → exists ℕ (λ n → le-ℤ-Prop y (int-ℕ n *ℤ x))
-  archimedean-property-ℤ x y pos-x with decide-is-negative-is-nonnegative-ℤ {y}
-  ... | inl neg-y = intro-exists zero-ℕ (le-zero-is-negative-ℤ y neg-y)
-  ... | inr nonneg-y =
-      ind-Σ
-        ( λ nx (nonzero-nx , nx=x) →
-          elim-exists
-            (∃ ℕ (λ n → le-ℤ-Prop y (int-ℕ n *ℤ x)))
-            ( λ n ny<n*nx →
-              intro-exists
-                ( n)
-                ( binary-tr
-                  ( le-ℤ)
-                  ( ap pr1 (is-section-nat-nonnegative-ℤ (y , nonneg-y)))
-                  ( inv (mul-int-ℕ n nx) ∙ ap (int-ℕ n *ℤ_) nx=x)
-                  ( le-natural-le-ℤ
-                    ( nat-nonnegative-ℤ (y , nonneg-y))
-                    ( n *ℕ nx)
-                    ( ny<n*nx))))
-            ( archimedean-property-ℕ
-              ( nx)
-              ( nat-nonnegative-ℤ (y , nonneg-y)) nonzero-nx))
-        (pos-ℤ-to-ℕ x pos-x)
-    where pos-ℤ-to-ℕ :
-            (z : ℤ) →
-              is-positive-ℤ z →
-              Σ ℕ (λ n → is-nonzero-ℕ n × (int-ℕ n ＝ z))
-          pos-ℤ-to-ℕ (inr (inr n)) H = succ-ℕ n , (λ ()) , refl
+  archimedean-property-ℤ x y pos-x =
+    unit-trunc-Prop (bound-archimedean-property-ℤ x y pos-x)
 ```
 
 ## External links

src/elementary-number-theory/archimedean-property-natural-numbers.lagda.md

@@ -7,7 +7,6 @@ module elementary-number-theory.archimedean-property-natural-numbers where
 <details><summary>Imports</summary>
 
 ```agda
-open import elementary-number-theory.equality-natural-numbers
 open import elementary-number-theory.euclidean-division-natural-numbers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
@@ -16,6 +15,7 @@ open import elementary-number-theory.strict-inequality-natural-numbers
 
 open import foundation.dependent-pair-types
 open import foundation.existential-quantification
+open import foundation.propositional-truncations
 open import foundation.transport-along-identifications
 ```
 
@@ -31,19 +31,23 @@ for any nonzero natural number `x` and any natural number `y`, there is an
 
 ```agda
 abstract
+  bound-archimedean-property-ℕ :
+    (x y : ℕ) → is-nonzero-ℕ x → Σ ℕ (λ n → le-ℕ y (n *ℕ x))
+  bound-archimedean-property-ℕ x y nonzero-x =
+    succ-ℕ (quotient-euclidean-division-ℕ x y) ,
+    tr
+      ( λ z → z <-ℕ succ-ℕ (quotient-euclidean-division-ℕ x y) *ℕ x)
+      ( eq-euclidean-division-ℕ x y)
+      ( preserves-le-left-add-ℕ
+        ( quotient-euclidean-division-ℕ x y *ℕ x)
+        ( remainder-euclidean-division-ℕ x y)
+        ( x)
+        ( strict-upper-bound-remainder-euclidean-division-ℕ x y nonzero-x))
+
   archimedean-property-ℕ :
     (x y : ℕ) → is-nonzero-ℕ x → exists ℕ (λ n → le-ℕ-Prop y (n *ℕ x))
   archimedean-property-ℕ x y nonzero-x =
-    intro-exists
-      (succ-ℕ (quotient-euclidean-division-ℕ x y))
-      ( tr
-        ( λ z → z <-ℕ succ-ℕ (quotient-euclidean-division-ℕ x y) *ℕ x)
-        ( eq-euclidean-division-ℕ x y)
-        ( preserves-le-left-add-ℕ
-          ( quotient-euclidean-division-ℕ x y *ℕ x)
-          ( remainder-euclidean-division-ℕ x y)
-          ( x)
-          ( strict-upper-bound-remainder-euclidean-division-ℕ x y nonzero-x)))
+    unit-trunc-Prop (bound-archimedean-property-ℕ x y nonzero-x)
 ```
 
 ## External links

src/elementary-number-theory/archimedean-property-positive-rational-numbers.lagda.md

@@ -0,0 +1,74 @@
+# The Archimedean property of the positive rational numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module elementary-number-theory.archimedean-property-positive-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.archimedean-property-rational-numbers
+open import elementary-number-theory.integers
+open import elementary-number-theory.multiplication-rational-numbers
+open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.nonzero-natural-numbers
+open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.strict-inequality-rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.identity-types
+open import foundation.propositional-truncations
+open import foundation.transport-along-identifications
+```
+
+</details>
+
+## Definition
+
+The
+{{#concept "Archimedean property" Disambiguation="positive rational numbers" Agda=archimedean-property-ℚ⁺}}
+of `ℚ⁺` is that for any two
+[positive rational numbers](elementary-number-theory.positive-rational-numbers.md)
+`x y : ℚ⁺`, there is a
+[nonzero natural number](elementary-number-theory.nonzero-natural-numbers.md)
+`n` such that `y` is
+[less than](elementary-number-theory.strict-inequality-rational-numbers.md) `n`
+times `x`.
+
+```agda
+abstract
+  bound-archimedean-property-ℚ⁺ :
+    (x y : ℚ⁺) →
+    Σ ℕ⁺ (λ n → le-ℚ⁺ y (positive-rational-ℕ⁺ n *ℚ⁺ x))
+  bound-archimedean-property-ℚ⁺ (x , pos-x) (y , pos-y) =
+    let
+      (n , y<nx) = bound-archimedean-property-ℚ x y pos-x
+      n≠0 : is-nonzero-ℕ n
+      n≠0 n=0 =
+        asymmetric-le-ℚ
+          ( zero-ℚ)
+          ( y)
+          ( le-zero-is-positive-ℚ y pos-y)
+          ( tr
+            ( le-ℚ y)
+            ( equational-reasoning
+              rational-ℤ (int-ℕ n) *ℚ x
+              ＝ rational-ℤ (int-ℕ 0) *ℚ x
+                by ap (λ m → rational-ℤ (int-ℕ m) *ℚ x) n=0
+              ＝ zero-ℚ by left-zero-law-mul-ℚ x)
+            y<nx)
+    in (n , n≠0) , y<nx
+
+  archimedean-property-ℚ⁺ :
+    (x y : ℚ⁺) →
+    exists ℕ⁺ (λ n → le-prop-ℚ⁺ y (positive-rational-ℕ⁺ n *ℚ⁺ x))
+  archimedean-property-ℚ⁺ x y =
+    unit-trunc-Prop (bound-archimedean-property-ℚ⁺ x y)
+```

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

@@ -24,6 +24,7 @@ open import foundation.binary-transport
 open import foundation.dependent-pair-types
 open import foundation.existential-quantification
 open import foundation.identity-types
+open import foundation.propositional-truncations
 ```
 
 </details>
@@ -39,32 +40,38 @@ an `n : ℕ` such that `y` is less than `n` as a rational number times `x`.
 
 ```agda
 abstract
+  bound-archimedean-property-ℚ :
+    (x y : ℚ) →
+    is-positive-ℚ x →
+    Σ ℕ (λ n → le-ℚ y (rational-ℤ (int-ℕ n) *ℚ x))
+  bound-archimedean-property-ℚ x y pos-x =
+    let
+      (n , nx<y) =
+        bound-archimedean-property-fraction-ℤ
+          ( fraction-ℚ x)
+          ( fraction-ℚ y)
+          ( pos-x)
+    in
+      n ,
+      binary-tr
+        ( le-ℚ)
+        ( is-retraction-rational-fraction-ℚ y)
+        ( inv
+          ( mul-rational-fraction-ℤ
+            ( in-fraction-ℤ (int-ℕ n))
+            ( fraction-ℚ x)) ∙
+          ap-binary
+            ( mul-ℚ)
+            ( is-retraction-rational-fraction-ℚ (rational-ℤ (int-ℕ n)))
+            ( is-retraction-rational-fraction-ℚ x))
+        ( preserves-le-rational-fraction-ℤ
+          ( fraction-ℚ y)
+          ( in-fraction-ℤ (int-ℕ n) *fraction-ℤ fraction-ℚ x) nx<y)
+
   archimedean-property-ℚ :
     (x y : ℚ) →
       is-positive-ℚ x →
       exists ℕ (λ n → le-ℚ-Prop y (rational-ℤ (int-ℕ n) *ℚ x))
-  archimedean-property-ℚ x y positive-x =
-    elim-exists
-      ( ∃ ℕ (λ n → le-ℚ-Prop y (rational-ℤ (int-ℕ n) *ℚ x)))
-      ( λ n nx<y →
-        intro-exists
-          ( n)
-          ( binary-tr
-              le-ℚ
-              ( is-retraction-rational-fraction-ℚ y)
-              ( inv
-                ( mul-rational-fraction-ℤ
-                  ( in-fraction-ℤ (int-ℕ n))
-                  ( fraction-ℚ x)) ∙
-                ap-binary
-                  ( mul-ℚ)
-                  ( is-retraction-rational-fraction-ℚ (rational-ℤ (int-ℕ n)))
-                  ( is-retraction-rational-fraction-ℚ x))
-              ( preserves-le-rational-fraction-ℤ
-                ( fraction-ℚ y)
-                ( in-fraction-ℤ (int-ℕ n) *fraction-ℤ fraction-ℚ x) nx<y)))
-      ( archimedean-property-fraction-ℤ
-        ( fraction-ℚ x)
-        ( fraction-ℚ y)
-        ( positive-x))
+  archimedean-property-ℚ x y pos-x =
+    unit-trunc-Prop (bound-archimedean-property-ℚ x y pos-x)
 ```