Divisibility of natural numbers

module elementary-number-theory.divisibility-natural-numbers where
Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.distance-natural-numbers
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.strict-inequality-natural-numbers

open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.propositional-maps
open import foundation.propositions
open import foundation.type-arithmetic-empty-type
open import foundation.unit-type
open import foundation.universe-levels

Idea

A natural number m is said to divide a natural number n if there exists a natural number k equipped with an identification km = n. Using the Curry-Howard interpretation of logic into type theory, we express divisibility as follows:

  div-ℕ m n := Σ (k : ℕ), k *ℕ m = n.

If n is a nonzero natural number, then div-ℕ m n is always a proposition in the sense that the type div-ℕ m n contains at most one element.

Definitions

div-ℕ :     UU lzero
div-ℕ m n = Σ   k  k *ℕ m  n)

quotient-div-ℕ : (x y : )  div-ℕ x y  
quotient-div-ℕ x y H = pr1 H

eq-quotient-div-ℕ :
  (x y : ) (H : div-ℕ x y)  (quotient-div-ℕ x y H) *ℕ x  y
eq-quotient-div-ℕ x y H = pr2 H

eq-quotient-div-ℕ' :
  (x y : ) (H : div-ℕ x y)  x *ℕ (quotient-div-ℕ x y H)  y
eq-quotient-div-ℕ' x y H =
  commutative-mul-ℕ x (quotient-div-ℕ x y H)  eq-quotient-div-ℕ x y H

div-quotient-div-ℕ :
  (d x : ) (H : div-ℕ d x)  div-ℕ (quotient-div-ℕ d x H) x
pr1 (div-quotient-div-ℕ d x (u , p)) = d
pr2 (div-quotient-div-ℕ d x (u , p)) = commutative-mul-ℕ d u  p

Concatenating equality and divisibility

concatenate-eq-div-ℕ :
  {x y z : }  x  y  div-ℕ y z  div-ℕ x z
concatenate-eq-div-ℕ refl p = p

concatenate-div-eq-ℕ :
  {x y z : }  div-ℕ x y  y  z  div-ℕ x z
concatenate-div-eq-ℕ p refl = p

concatenate-eq-div-eq-ℕ :
  {x y z w : }  x  y  div-ℕ y z  z  w  div-ℕ x w
concatenate-eq-div-eq-ℕ refl p refl = p

Properties

The quotients of a natural number n by two natural numbers p and q are equal if p and q are equal

eq-quotient-div-eq-div-ℕ :
  (x y z : )  is-nonzero-ℕ x  x  y 
  (H : div-ℕ x z)  (I : div-ℕ y z) 
  quotient-div-ℕ x z H  quotient-div-ℕ y z I
eq-quotient-div-eq-div-ℕ x y z n e H I =
  is-injective-left-mul-ℕ
    ( x)
    ( n)
  ( tr
    ( λ p 
      x *ℕ (quotient-div-ℕ x z H) 
      p *ℕ (quotient-div-ℕ y z I))
    ( inv e)
    ( commutative-mul-ℕ x (quotient-div-ℕ x z H) 
      ( eq-quotient-div-ℕ x z H 
        ( inv (eq-quotient-div-ℕ y z I) 
           commutative-mul-ℕ (quotient-div-ℕ y z I) y))))

Divisibility by a nonzero natural number is a property

is-prop-div-ℕ : (k x : )  is-nonzero-ℕ k  is-prop (div-ℕ k x)
is-prop-div-ℕ k x f = is-prop-map-is-emb (is-emb-right-mul-ℕ k f) x

The divisibility relation is a partial order on the natural numbers

refl-div-ℕ : (x : )  div-ℕ x x
pr1 (refl-div-ℕ x) = 1
pr2 (refl-div-ℕ x) = left-unit-law-mul-ℕ x

div-eq-ℕ : (x y : )  x  y  div-ℕ x y
div-eq-ℕ x .x refl = refl-div-ℕ x

antisymmetric-div-ℕ :
  (x y : )  div-ℕ x y  div-ℕ y x  x  y
antisymmetric-div-ℕ zero-ℕ zero-ℕ H K = refl
antisymmetric-div-ℕ zero-ℕ (succ-ℕ y) (pair k p) K =
  inv (right-zero-law-mul-ℕ k)  p
antisymmetric-div-ℕ (succ-ℕ x) zero-ℕ H (pair l q) =
  inv q  right-zero-law-mul-ℕ l
antisymmetric-div-ℕ (succ-ℕ x) (succ-ℕ y) (pair k p) (pair l q) =
  ( inv (left-unit-law-mul-ℕ (succ-ℕ x))) 
  ( ( ap ( _*ℕ (succ-ℕ x))
         ( inv
           ( is-one-right-is-one-mul-ℕ l k
             ( is-one-is-left-unit-mul-ℕ (l *ℕ k) x
               ( ( associative-mul-ℕ l k (succ-ℕ x)) 
                 ( ap (l *ℕ_) p  q)))))) 
    ( p))

transitive-div-ℕ :
  (x y z : )  div-ℕ x y  div-ℕ y z  div-ℕ x z
pr1 (transitive-div-ℕ x y z (pair k p) (pair l q)) = l *ℕ k
pr2 (transitive-div-ℕ x y z (pair k p) (pair l q)) =
  associative-mul-ℕ l k x  (ap (l *ℕ_) p  q)

If x is nonzero and d | x, then d ≤ x

leq-div-succ-ℕ : (d x : )  div-ℕ d (succ-ℕ x)  leq-ℕ d (succ-ℕ x)
leq-div-succ-ℕ d x (pair (succ-ℕ k) p) =
  concatenate-leq-eq-ℕ d (leq-mul-ℕ' k d) p

leq-div-ℕ : (d x : )  is-nonzero-ℕ x  div-ℕ d x  leq-ℕ d x
leq-div-ℕ d x f H with is-successor-is-nonzero-ℕ f
... | (pair y refl) = leq-div-succ-ℕ d y H

leq-quotient-div-ℕ :
  (d x : )  is-nonzero-ℕ x  (H : div-ℕ d x)  leq-ℕ (quotient-div-ℕ d x H) x
leq-quotient-div-ℕ d x f H =
  leq-div-ℕ (quotient-div-ℕ d x H) x f (div-quotient-div-ℕ d x H)

leq-quotient-div-ℕ' :
  (d x : )  is-nonzero-ℕ d  (H : div-ℕ d x)  leq-ℕ (quotient-div-ℕ d x H) x
leq-quotient-div-ℕ' d zero-ℕ f (zero-ℕ , p) = star
leq-quotient-div-ℕ' d zero-ℕ f (succ-ℕ n , p) =
  f (is-zero-right-is-zero-add-ℕ _ d p)
leq-quotient-div-ℕ' d (succ-ℕ x) f H =
  leq-quotient-div-ℕ d (succ-ℕ x) (is-nonzero-succ-ℕ x) H

If x is nonzero, if d | x and d ≠ x, then d < x

le-div-succ-ℕ :
  (d x : )  div-ℕ d (succ-ℕ x)  ¬ (d  succ-ℕ x)  le-ℕ d (succ-ℕ x)
le-div-succ-ℕ d x H f = le-leq-neq-ℕ (leq-div-succ-ℕ d x H) f

le-div-ℕ : (d x : )  is-nonzero-ℕ x  div-ℕ d x  ¬ (d  x)  le-ℕ d x
le-div-ℕ d x H K f = le-leq-neq-ℕ (leq-div-ℕ d x H K) f

1 divides any number

div-one-ℕ :
  (x : )  div-ℕ 1 x
pr1 (div-one-ℕ x) = x
pr2 (div-one-ℕ x) = right-unit-law-mul-ℕ x

div-is-one-ℕ :
  (k x : )  is-one-ℕ k  div-ℕ k x
div-is-one-ℕ .1 x refl = div-one-ℕ x

x | 1 implies x = 1

is-one-div-one-ℕ : (x : )  div-ℕ x 1  is-one-ℕ x
is-one-div-one-ℕ x H = antisymmetric-div-ℕ x 1 H (div-one-ℕ x)

Any number divides 0

div-zero-ℕ :
  (k : )  div-ℕ k 0
pr1 (div-zero-ℕ k) = 0
pr2 (div-zero-ℕ k) = left-zero-law-mul-ℕ k

div-is-zero-ℕ :
  (k x : )  is-zero-ℕ x  div-ℕ k x
div-is-zero-ℕ k .zero-ℕ refl = div-zero-ℕ k

0 | x implies x = 0 and x | 1 implies x = 1

is-zero-div-zero-ℕ : (x : )  div-ℕ zero-ℕ x  is-zero-ℕ x
is-zero-div-zero-ℕ x H = antisymmetric-div-ℕ x zero-ℕ (div-zero-ℕ x) H

is-zero-is-zero-div-ℕ : (x y : )  div-ℕ x y  is-zero-ℕ x  is-zero-ℕ y
is-zero-is-zero-div-ℕ .zero-ℕ y d refl = is-zero-div-zero-ℕ y d

Any divisor of a nonzero number is nonzero

is-nonzero-div-ℕ :
  (d x : )  div-ℕ d x  is-nonzero-ℕ x  is-nonzero-ℕ d
is-nonzero-div-ℕ .zero-ℕ x H K refl = K (is-zero-div-zero-ℕ x H)

Any divisor of a number at least 1 is at least 1

leq-one-div-ℕ :
  (d x : )  div-ℕ d x  leq-ℕ 1 x  leq-ℕ 1 d
leq-one-div-ℕ d x H L =
  leq-one-is-nonzero-ℕ d (is-nonzero-div-ℕ d x H (is-nonzero-leq-one-ℕ x L))

If x < d and d | x, then x must be 0

is-zero-div-ℕ :
  (d x : )  le-ℕ x d  div-ℕ d x  is-zero-ℕ x
is-zero-div-ℕ d zero-ℕ H D = refl
is-zero-div-ℕ d (succ-ℕ x) H (pair (succ-ℕ k) p) =
  ex-falso
    ( contradiction-le-ℕ
      ( succ-ℕ x) d H
      ( concatenate-leq-eq-ℕ d
        ( leq-add-ℕ' d (k *ℕ d)) p))

If x divides y then x divides any multiple of y

div-mul-ℕ :
  (k x y : )  div-ℕ x y  div-ℕ x (k *ℕ y)
div-mul-ℕ k x y H =
  transitive-div-ℕ x y (k *ℕ y) H (pair k refl)

div-mul-ℕ' :
  (k x y : )  div-ℕ x y  div-ℕ x (y *ℕ k)
div-mul-ℕ' k x y H =
  tr (div-ℕ x) (commutative-mul-ℕ k y) (div-mul-ℕ k x y H)

A 3-for-2 property of division with respect to addition

div-add-ℕ :
  (d x y : )  div-ℕ d x  div-ℕ d y  div-ℕ d (x +ℕ y)
pr1 (div-add-ℕ d x y (pair n p) (pair m q)) = n +ℕ m
pr2 (div-add-ℕ d x y (pair n p) (pair m q)) =
  ( right-distributive-mul-add-ℕ n m d) 
  ( ap-add-ℕ p q)

div-left-summand-ℕ :
  (d x y : )  div-ℕ d y  div-ℕ d (x +ℕ y)  div-ℕ d x
div-left-summand-ℕ zero-ℕ x y (pair m q) (pair n p) =
  pair zero-ℕ
    ( ( inv (right-zero-law-mul-ℕ n)) 
      ( p  (ap (x +ℕ_) ((inv q)  (right-zero-law-mul-ℕ m)))))
pr1 (div-left-summand-ℕ (succ-ℕ d) x y (pair m q) (pair n p)) = dist-ℕ m n
pr2 (div-left-summand-ℕ (succ-ℕ d) x y (pair m q) (pair n p)) =
  is-injective-right-add-ℕ (m *ℕ (succ-ℕ d))
    ( ( inv
        ( ( right-distributive-mul-add-ℕ m (dist-ℕ m n) (succ-ℕ d)) 
          ( commutative-add-ℕ
            ( m *ℕ (succ-ℕ d))
            ( (dist-ℕ m n) *ℕ (succ-ℕ d))))) 
      ( ( ap
          ( _*ℕ (succ-ℕ d))
          ( is-additive-right-inverse-dist-ℕ m n
            ( reflects-order-mul-ℕ d m n
              ( concatenate-eq-leq-eq-ℕ q
                ( leq-add-ℕ' y x)
                ( inv p))))) 
        ( p  (ap (x +ℕ_) (inv q)))))

div-right-summand-ℕ :
  (d x y : )  div-ℕ d x  div-ℕ d (x +ℕ y)  div-ℕ d y
div-right-summand-ℕ d x y H1 H2 =
  div-left-summand-ℕ d y x H1 (concatenate-div-eq-ℕ H2 (commutative-add-ℕ x y))

If d divides both x and x + 1, then d = 1

is-one-div-ℕ : (x y : )  div-ℕ x y  div-ℕ x (succ-ℕ y)  is-one-ℕ x
is-one-div-ℕ x y H K = is-one-div-one-ℕ x (div-right-summand-ℕ x y 1 H K)

Multiplication preserves divisibility

preserves-div-mul-ℕ :
  (k x y : )  div-ℕ x y  div-ℕ (k *ℕ x) (k *ℕ y)
pr1 (preserves-div-mul-ℕ k x y (pair q p)) = q
pr2 (preserves-div-mul-ℕ k x y (pair q p)) =
  ( inv (associative-mul-ℕ q k x)) 
    ( ( ap (_*ℕ x) (commutative-mul-ℕ q k)) 
      ( ( associative-mul-ℕ k q x) 
        ( ap (k *ℕ_) p)))

Multiplication by a nonzero number reflects divisibility

reflects-div-mul-ℕ :
  (k x y : )  is-nonzero-ℕ k  div-ℕ (k *ℕ x) (k *ℕ y)  div-ℕ x y
pr1 (reflects-div-mul-ℕ k x y H (pair q p)) = q
pr2 (reflects-div-mul-ℕ k x y H (pair q p)) =
  is-injective-left-mul-ℕ k H
    ( ( inv (associative-mul-ℕ k q x)) 
      ( ( ap (_*ℕ x) (commutative-mul-ℕ k q)) 
        ( ( associative-mul-ℕ q k x) 
          ( p))))

If a nonzero number d divides y, then dx divides y if and only if x divides the quotient y/d

div-quotient-div-div-ℕ :
  (x y d : ) (H : div-ℕ d y)  is-nonzero-ℕ d 
  div-ℕ (d *ℕ x) y  div-ℕ x (quotient-div-ℕ d y H)
div-quotient-div-div-ℕ x y d H f K =
  reflects-div-mul-ℕ d x
    ( quotient-div-ℕ d y H)
    ( f)
    ( tr (div-ℕ (d *ℕ x)) (inv (eq-quotient-div-ℕ' d y H)) K)

div-div-quotient-div-ℕ :
  (x y d : ) (H : div-ℕ d y) 
  div-ℕ x (quotient-div-ℕ d y H)  div-ℕ (d *ℕ x) y
div-div-quotient-div-ℕ x y d H K =
  tr ( div-ℕ (d *ℕ x))
     ( eq-quotient-div-ℕ' d y H)
     ( preserves-div-mul-ℕ d x (quotient-div-ℕ d y H) K)

If d divides a nonzero number x, then the quotient x/d is also nonzero

is-nonzero-quotient-div-ℕ :
  {d x : } (H : div-ℕ d x) 
  is-nonzero-ℕ x  is-nonzero-ℕ (quotient-div-ℕ d x H)
is-nonzero-quotient-div-ℕ {d} {.(k *ℕ d)} (pair k refl) =
  is-nonzero-left-factor-mul-ℕ k d

If d divides a number 1 ≤ x, then 1 ≤ x/d

leq-one-quotient-div-ℕ :
  (d x : ) (H : div-ℕ d x)  leq-ℕ 1 x  leq-ℕ 1 (quotient-div-ℕ d x H)
leq-one-quotient-div-ℕ d x H K =
  leq-one-div-ℕ
    ( quotient-div-ℕ d x H)
    ( x)
    ( div-quotient-div-ℕ d x H)
    ( K)

a/a = 1

is-idempotent-quotient-div-ℕ :
  (a : )  is-nonzero-ℕ a  (H : div-ℕ a a)  is-one-ℕ (quotient-div-ℕ a a H)
is-idempotent-quotient-div-ℕ zero-ℕ nz (u , p) = ex-falso (nz refl)
is-idempotent-quotient-div-ℕ (succ-ℕ a) nz (u , p) =
  is-one-is-left-unit-mul-ℕ u a p

If b divides a and c divides b and c is nonzero, then a/b · b/c = a/c

simplify-mul-quotient-div-ℕ :
  {a b c : }  is-nonzero-ℕ c 
  (H : div-ℕ b a) (K : div-ℕ c b) (L : div-ℕ c a) 
  ( (quotient-div-ℕ b a H) *ℕ (quotient-div-ℕ c b K)) 
  ( quotient-div-ℕ c a L)
simplify-mul-quotient-div-ℕ {a} {b} {c} nz H K L =
  is-injective-right-mul-ℕ c nz
    ( equational-reasoning
      (a/b *ℕ b/c) *ℕ c
       a/b *ℕ (b/c *ℕ c)
        by associative-mul-ℕ a/b b/c c
       a/b *ℕ b
        by ap (a/b *ℕ_) (eq-quotient-div-ℕ c b K)
       a
        by eq-quotient-div-ℕ b a H
       a/c *ℕ c
        by inv (eq-quotient-div-ℕ c a L))
  where
  a/b : 
  a/b = quotient-div-ℕ b a H
  b/c : 
  b/c = quotient-div-ℕ c b K
  a/c : 
  a/c = quotient-div-ℕ c a L

If d | a and d is nonzero, then x | a/d if and only if xd | a

simplify-div-quotient-div-ℕ :
  {a d x : }  is-nonzero-ℕ d  (H : div-ℕ d a) 
  (div-ℕ x (quotient-div-ℕ d a H))  (div-ℕ (x *ℕ d) a)
pr1 (pr1 (simplify-div-quotient-div-ℕ nz H) (u , p)) = u
pr2 (pr1 (simplify-div-quotient-div-ℕ {a} {d} {x} nz H) (u , p)) =
  equational-reasoning
    u *ℕ (x *ℕ d)
     (u *ℕ x) *ℕ d
      by inv (associative-mul-ℕ u x d)
     (quotient-div-ℕ d a H) *ℕ d
      by ap (_*ℕ d) p
     a
      by eq-quotient-div-ℕ d a H
pr1 (pr2 (simplify-div-quotient-div-ℕ nz H) (u , p)) = u
pr2 (pr2 (simplify-div-quotient-div-ℕ {a} {d} {x} nz H) (u , p)) =
  is-injective-right-mul-ℕ d nz
    ( equational-reasoning
        (u *ℕ x) *ℕ d
         u *ℕ (x *ℕ d)
          by associative-mul-ℕ u x d
         a
          by p
         (quotient-div-ℕ d a H) *ℕ d
          by inv (eq-quotient-div-ℕ d a H))

Suppose H : b | a and K : c | b, where c is nonzero. If d divides b/c then d divides a/c.

div-quotient-div-div-quotient-div-ℕ :
  {a b c d : }  is-nonzero-ℕ c  (H : div-ℕ b a)
  (K : div-ℕ c b) (L : div-ℕ c a) 
  div-ℕ d (quotient-div-ℕ c b K) 
  div-ℕ d (quotient-div-ℕ c a L)
div-quotient-div-div-quotient-div-ℕ {a} {b} {c} {d} nz H K L M =
  tr
    ( div-ℕ d)
    ( simplify-mul-quotient-div-ℕ nz H K L)
    ( div-mul-ℕ
      ( quotient-div-ℕ b a H)
      ( d)
      ( quotient-div-ℕ c b K)
      ( M))

If x is nonzero and d | x, then x/d = 1 if and only if d = x

is-one-quotient-div-ℕ :
  (d x : )  is-nonzero-ℕ x  (H : div-ℕ d x)  (d  x) 
  is-one-ℕ (quotient-div-ℕ d x H)
is-one-quotient-div-ℕ d .d f H refl = is-idempotent-quotient-div-ℕ d f H

eq-is-one-quotient-div-ℕ :
  (d x : )  (H : div-ℕ d x)  is-one-ℕ (quotient-div-ℕ d x H)  d  x
eq-is-one-quotient-div-ℕ d x (.1 , q) refl = inv (left-unit-law-mul-ℕ d)  q

If x is nonzero and d | x, then x/d = x if and only if d = 1

compute-quotient-div-is-one-ℕ :
  (d x : )  (H : div-ℕ d x)  is-one-ℕ d  quotient-div-ℕ d x H  x
compute-quotient-div-is-one-ℕ .1 x (u , q) refl =
  inv (right-unit-law-mul-ℕ u)  q

is-one-divisor-ℕ :
  (d x : )  is-nonzero-ℕ x  (H : div-ℕ d x) 
  quotient-div-ℕ d x H  x  is-one-ℕ d
is-one-divisor-ℕ d x f (.x , q) refl =
  is-injective-left-mul-ℕ x f (q  inv (right-unit-law-mul-ℕ x))

If x is nonzero and d | x is a nontrivial divisor, then x/d < x

le-quotient-div-ℕ :
  (d x : )  is-nonzero-ℕ x  (H : div-ℕ d x)  ¬ (is-one-ℕ d) 
  le-ℕ (quotient-div-ℕ d x H) x
le-quotient-div-ℕ d x f H g =
  map-left-unit-law-coprod-is-empty
    ( quotient-div-ℕ d x H  x)
    ( le-ℕ (quotient-div-ℕ d x H) x)
    ( map-neg (is-one-divisor-ℕ d x f H) g)
    ( eq-or-le-leq-ℕ
      ( quotient-div-ℕ d x H)
      ( x)
      ( leq-quotient-div-ℕ d x f H))