The mediant fraction of two integer fractions

Content created by Fredrik Bakke, malarbol and Louis Wasserman.

Created on 2024-02-27.
Last modified on 2025-12-16.

module elementary-number-theory.mediant-integer-fractions where
Imports 
open import elementary-number-theory.addition-integers
open import elementary-number-theory.addition-positive-and-negative-integers
open import elementary-number-theory.cross-multiplication-difference-integer-fractions
open import elementary-number-theory.difference-integers
open import elementary-number-theory.divisibility-integers
open import elementary-number-theory.greatest-common-divisor-integers
open import elementary-number-theory.integer-fractions
open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.negative-integers
open import elementary-number-theory.positive-and-negative-integers
open import elementary-number-theory.reduced-integer-fractions

open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.identity-types
open import foundation.transport-along-identifications

Idea

The mediant of two fractions is the quotient of the sum of the numerators by the sum of the denominators.

Definitions

The mediant of two fractions

mediant-fraction-ℤ : fraction-ℤ → fraction-ℤ → fraction-ℤ
mediant-fraction-ℤ (a , b) (c , d) = (add-ℤ a c , add-positive-ℤ b d)

Properties

The mediant preserves the cross-multiplication difference

abstract
  cross-mul-diff-left-mediant-fraction-ℤ :
    (x y : fraction-ℤ) →
    cross-mul-diff-fraction-ℤ x y ＝
    cross-mul-diff-fraction-ℤ x ( mediant-fraction-ℤ x y)
  cross-mul-diff-left-mediant-fraction-ℤ (nx , dx , px) (ny , dy , py) =
    equational-reasoning
    (ny *ℤ dx -ℤ nx *ℤ dy)
    ＝ (nx *ℤ dx +ℤ ny *ℤ dx) -ℤ (nx *ℤ dx +ℤ nx *ℤ dy)
      by inv
        ( left-translation-diff-ℤ
          ( mul-ℤ ny dx)
          ( mul-ℤ nx dy)
          ( mul-ℤ nx dx))
    ＝ (nx +ℤ ny) *ℤ dx -ℤ nx *ℤ (dx +ℤ dy)
      by ap-diff-ℤ
        ( inv (right-distributive-mul-add-ℤ nx ny dx))
        ( inv (left-distributive-mul-add-ℤ nx dx dy))

  cross-mul-diff-right-mediant-fraction-ℤ :
    (x y : fraction-ℤ) →
    cross-mul-diff-fraction-ℤ x y ＝
    cross-mul-diff-fraction-ℤ (mediant-fraction-ℤ x y) y
  cross-mul-diff-right-mediant-fraction-ℤ (nx , dx , px) (ny , dy , py) =
    equational-reasoning
    (ny *ℤ dx -ℤ nx *ℤ dy)
    ＝ (ny *ℤ dx +ℤ ny *ℤ dy) -ℤ (nx *ℤ dy +ℤ ny *ℤ dy)
      by inv
        ( right-translation-diff-ℤ
          ( mul-ℤ ny dx)
          ( mul-ℤ nx dy)
          ( mul-ℤ ny dy))
    ＝ ny *ℤ (dx +ℤ dy) -ℤ (nx +ℤ ny) *ℤ dy
      by ap-diff-ℤ
        ( inv (left-distributive-mul-add-ℤ ny dx dy))
        ( inv (right-distributive-mul-add-ℤ nx ny dy))

Common divisors of the numerator and denominator of the mediant of two integer fractions divide their cross-multiplication difference

div-cross-mul-diff-common-divisor-mediant-fraction-ℤ :
  (x y : fraction-ℤ) →
  (k : ℤ) →
  is-common-divisor-ℤ
    ( numerator-fraction-ℤ (mediant-fraction-ℤ x y))
    ( denominator-fraction-ℤ (mediant-fraction-ℤ x y))
    ( k) →
  div-ℤ k (cross-mul-diff-fraction-ℤ x y)
div-cross-mul-diff-common-divisor-mediant-fraction-ℤ
  x@(nx , dx , _) y@(ny , dy , _) k (div-N , div-D) =
  inv-tr
    ( div-ℤ k)
    ( cross-mul-diff-left-mediant-fraction-ℤ x y)
    ( div-add-ℤ
      ( k)
      ( (nx +ℤ ny) *ℤ dx)
      ( neg-ℤ (nx *ℤ (dx +ℤ dy)))
      ( inv-tr
        ( div-ℤ k)
        ( commutative-mul-ℤ (nx +ℤ ny) dx)
        ( div-mul-ℤ dx k (nx +ℤ ny) div-N))
      ( div-neg-ℤ
        ( k)
        ( nx *ℤ (dx +ℤ dy))
        ( div-mul-ℤ
          ( nx)
          ( k)
          ( dx +ℤ dy)
          ( div-D))))

If the cross-multiplication difference of two fractions is 1 their mediant integer fraction is reduced

abstract
  is-reduced-mediant-is-one-cross-mul-diff-fraction-ℤ :
    (x y : fraction-ℤ) →
    is-one-ℤ (cross-mul-diff-fraction-ℤ x y) →
    is-reduced-fraction-ℤ (mediant-fraction-ℤ x y)
  is-reduced-mediant-is-one-cross-mul-diff-fraction-ℤ x y H =
    let
      n = numerator-fraction-ℤ (mediant-fraction-ℤ x y)
      d = denominator-fraction-ℤ (mediant-fraction-ℤ x y)

      is-unit-gcd-mediant : is-unit-ℤ (gcd-ℤ n d)
      is-unit-gcd-mediant =
        tr
          ( div-ℤ (gcd-ℤ n d))
          ( H)
          ( div-cross-mul-diff-common-divisor-mediant-fraction-ℤ
            ( x)
            ( y)
            ( gcd-ℤ n d)
            ( is-common-divisor-gcd-ℤ n d))
    in
      rec-coproduct
        ( λ K → K)
        ( λ K →
          ex-falso
            ( is-not-negative-and-nonnegative-ℤ
              ( gcd-ℤ n d)
              ( ( inv-tr
                  ( is-negative-ℤ)
                  ( K)
                  ( _)) ,
                ( is-nonnegative-gcd-ℤ n d))))
        ( is-one-or-neg-one-is-unit-ℤ
          ( gcd-ℤ n d)
          ( is-unit-gcd-mediant))

Recent changes