Relatively prime natural numbers

module elementary-number-theory.relatively-prime-natural-numbers where
Imports
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.greatest-common-divisor-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.prime-numbers

open import foundation.decidable-propositions
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.negation
open import foundation.propositions
open import foundation.universe-levels

Idea

Two natural numbers x and y are said to be relatively prime if their greatest common divisor is 1.

Definition

is-relatively-prime-ℕ :     UU lzero
is-relatively-prime-ℕ x y = is-one-ℕ (gcd-ℕ x y)

Properties

Being relatively prime is a proposition

is-prop-is-relatively-prime-ℕ : (x y : )  is-prop (is-relatively-prime-ℕ x y)
is-prop-is-relatively-prime-ℕ x y = is-set-ℕ (gcd-ℕ x y) 1

is-relatively-prime-ℕ-Prop :     Prop lzero
pr1 (is-relatively-prime-ℕ-Prop x y) = is-relatively-prime-ℕ x y
pr2 (is-relatively-prime-ℕ-Prop x y) = is-prop-is-relatively-prime-ℕ x y

Being relatively prime is decidable

is-decidable-is-relatively-prime-ℕ :
  (x y : )  is-decidable (is-relatively-prime-ℕ x y)
is-decidable-is-relatively-prime-ℕ x y = is-decidable-is-one-ℕ (gcd-ℕ x y)

is-decidable-prop-is-relatively-prime-ℕ :
  (x y : )  is-decidable-prop (is-relatively-prime-ℕ x y)
pr1 (is-decidable-prop-is-relatively-prime-ℕ x y) =
  is-prop-is-relatively-prime-ℕ x y
pr2 (is-decidable-prop-is-relatively-prime-ℕ x y) =
  is-decidable-is-relatively-prime-ℕ x y

a and b are relatively prime if and only if any common divisor is equal to 1

is-one-is-common-divisor-is-relatively-prime-ℕ :
  (x y d : ) 
  is-relatively-prime-ℕ x y  is-common-divisor-ℕ x y d  is-one-ℕ d
is-one-is-common-divisor-is-relatively-prime-ℕ x y d H K =
  is-one-div-one-ℕ d
    ( tr
      ( div-ℕ d)
      ( H)
      ( div-gcd-is-common-divisor-ℕ x y d K))

is-relatively-prime-is-one-is-common-divisor-ℕ :
  (x y : ) 
  ((d : )  is-common-divisor-ℕ x y d  is-one-ℕ d)  is-relatively-prime-ℕ x y
is-relatively-prime-is-one-is-common-divisor-ℕ x y H =
  H (gcd-ℕ x y) (is-common-divisor-gcd-ℕ x y)

If a and b are relatively prime, then so are any divisors of a and b

is-relatively-prime-div-ℕ :
  (a b c d : )  div-ℕ c a  div-ℕ d b 
  is-relatively-prime-ℕ a b  is-relatively-prime-ℕ c d
is-relatively-prime-div-ℕ a b c d H K L =
  is-one-is-common-divisor-is-relatively-prime-ℕ a b
    ( gcd-ℕ c d)
    ( L)
    ( transitive-div-ℕ (gcd-ℕ c d) c a (div-left-factor-gcd-ℕ c d) H ,
      transitive-div-ℕ (gcd-ℕ c d) d b (div-right-factor-gcd-ℕ c d) K)

For any two natural numbers a and b such that a + b ≠ 0, the numbers a/gcd(a,b) and b/gcd(a,b) are relatively prime

is-relatively-prime-quotient-div-gcd-ℕ :
  (a b : )  is-nonzero-ℕ (a +ℕ b) 
  is-relatively-prime-ℕ
    ( quotient-div-ℕ (gcd-ℕ a b) a (div-left-factor-gcd-ℕ a b))
    ( quotient-div-ℕ (gcd-ℕ a b) b (div-right-factor-gcd-ℕ a b))
is-relatively-prime-quotient-div-gcd-ℕ a b nz =
  ( uniqueness-is-gcd-ℕ
    ( quotient-div-ℕ (gcd-ℕ a b) a (div-left-factor-gcd-ℕ a b))
    ( quotient-div-ℕ (gcd-ℕ a b) b (div-right-factor-gcd-ℕ a b))
    ( gcd-ℕ
      ( quotient-div-ℕ (gcd-ℕ a b) a (div-left-factor-gcd-ℕ a b))
      ( quotient-div-ℕ (gcd-ℕ a b) b (div-right-factor-gcd-ℕ a b)))
    ( quotient-div-ℕ
      ( gcd-ℕ a b)
      ( gcd-ℕ a b)
      ( div-gcd-is-common-divisor-ℕ a b
        ( gcd-ℕ a b)
        ( is-common-divisor-gcd-ℕ a b)))
    ( is-gcd-gcd-ℕ
      ( quotient-div-ℕ (gcd-ℕ a b) a (div-left-factor-gcd-ℕ a b))
      ( quotient-div-ℕ (gcd-ℕ a b) b (div-right-factor-gcd-ℕ a b)))
    ( is-gcd-quotient-div-gcd-ℕ
      ( is-nonzero-gcd-ℕ a b nz)
      ( is-common-divisor-gcd-ℕ a b))) 
  ( is-idempotent-quotient-div-ℕ
    ( gcd-ℕ a b)
    ( is-nonzero-gcd-ℕ a b nz)
    ( div-gcd-is-common-divisor-ℕ a b
      ( gcd-ℕ a b)
      ( is-common-divisor-gcd-ℕ a b)))

If a and b are prime and distinct, then they are relatively prime

module _
  (a b : )
  (pa : is-prime-ℕ a)
  (pb : is-prime-ℕ b)
  (n : ¬ (a  b))
  where

  is-one-is-common-divisor-is-prime-ℕ :
    (d : )  is-common-divisor-ℕ a b d  is-one-ℕ d
  is-one-is-common-divisor-is-prime-ℕ d c =
    pr1
      ( pa d)
      ( ( λ e 
          is-not-one-is-prime-ℕ
            ( a)
            ( pa)
            ( pr1 (pb a) (n , (tr  x  div-ℕ x b) e (pr2 c))))) ,
        ( pr1 c))

  is-relatively-prime-is-prime-ℕ :
     is-relatively-prime-ℕ a b
  is-relatively-prime-is-prime-ℕ =
    is-relatively-prime-is-one-is-common-divisor-ℕ
      ( a)
      ( b)
      ( is-one-is-common-divisor-is-prime-ℕ)