The Archimedean property of the natural numbers

Content created by Louis Wasserman.

Created on 2025-01-31.
Last modified on 2025-02-03.

module elementary-number-theory.archimedean-property-natural-numbers where
Imports 
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
open import elementary-number-theory.nonzero-natural-numbers
open import elementary-number-theory.strict-inequality-natural-numbers

open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.transport-along-identifications

Definition

The Archimedean property of the natural numbers is that for any nonzero natural number x and any natural number y, there is an n : ℕ such that y < n *ℕ x.

abstract
  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)))

Recent changes