The cross-multiplication difference of two integer fractions

Content created by malarbol and Fredrik Bakke.

Created on 2024-02-27.
Last modified on 2024-04-09.

module elementary-number-theory.cross-multiplication-difference-integer-fractions where
Imports
open import elementary-number-theory.addition-integers
open import elementary-number-theory.difference-integers
open import elementary-number-theory.integer-fractions
open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-integers

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.negation
open import foundation.propositions

Idea

The cross-multiplication difference of two integer fractions a/b and c/d is the difference of the products of the numerator of each fraction with the denominator of the other: c * b - a * d.

Definitions

The cross-multiplication difference of two fractions

cross-mul-diff-fraction-ℤ : fraction-ℤ  fraction-ℤ  
cross-mul-diff-fraction-ℤ x y =
  diff-ℤ
    ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x)
    ( numerator-fraction-ℤ x *ℤ denominator-fraction-ℤ y)

Properties

Swapping the fractions changes the sign of the cross-multiplication difference

skew-commutative-cross-mul-diff-fraction-ℤ :
  (x y : fraction-ℤ) 
  Id
    ( neg-ℤ (cross-mul-diff-fraction-ℤ x y))
    ( cross-mul-diff-fraction-ℤ y x)
skew-commutative-cross-mul-diff-fraction-ℤ x y =
  distributive-neg-diff-ℤ
    ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x)
    ( numerator-fraction-ℤ x *ℤ denominator-fraction-ℤ y)

Two fractions are similar when their cross-multiplication difference is zero

module _
  (x y : fraction-ℤ)
  where

  is-zero-cross-mul-diff-sim-fraction-ℤ :
    sim-fraction-ℤ x y 
    is-zero-ℤ (cross-mul-diff-fraction-ℤ x y)
  is-zero-cross-mul-diff-sim-fraction-ℤ H =
    is-zero-diff-ℤ (inv H)

  sim-is-zero-coss-mul-diff-fraction-ℤ :
    is-zero-ℤ (cross-mul-diff-fraction-ℤ x y) 
    sim-fraction-ℤ x y
  sim-is-zero-coss-mul-diff-fraction-ℤ H = inv (eq-diff-ℤ H)

The transitive-additive property for the cross-multiplication difference

Given three fractions a/b, x/y and m/n, the pairwise cross-multiplication differences satisfy a transitive-additive property:

  y * (m * b - a * n) = b * (m * y - x * n) + n * (x * b - a * y)
lemma-add-cross-mul-diff-fraction-ℤ :
  (p q r : fraction-ℤ) 
  Id
    ( add-ℤ
      ( denominator-fraction-ℤ p *ℤ cross-mul-diff-fraction-ℤ q r)
      ( denominator-fraction-ℤ r *ℤ cross-mul-diff-fraction-ℤ p q))
    ( denominator-fraction-ℤ q *ℤ cross-mul-diff-fraction-ℤ p r)
lemma-add-cross-mul-diff-fraction-ℤ
  (np , dp , hp)
  (nq , dq , hq)
  (nr , dr , hr) =
  equational-reasoning
  add-ℤ
    (dp *ℤ (nr *ℤ dq -ℤ nq *ℤ dr))
    (dr *ℤ (nq *ℤ dp -ℤ np *ℤ dq))
   add-ℤ
      (dp *ℤ (nr *ℤ dq) -ℤ dp *ℤ (nq *ℤ dr))
      (dr *ℤ (nq *ℤ dp) -ℤ dr *ℤ (np *ℤ dq))
    by
      ap-add-ℤ
        ( left-distributive-mul-diff-ℤ dp (nr *ℤ dq) (nq *ℤ dr))
        ( left-distributive-mul-diff-ℤ dr (nq *ℤ dp) (np *ℤ dq))
   diff-ℤ
      (dp *ℤ (nr *ℤ dq) +ℤ dr *ℤ (nq *ℤ dp))
      (dp *ℤ (nq *ℤ dr) +ℤ dr *ℤ (np *ℤ dq))
    by
      interchange-law-add-diff-ℤ
        ( mul-ℤ dp ( mul-ℤ nr dq))
        ( mul-ℤ dp ( mul-ℤ nq dr))
        ( mul-ℤ dr ( mul-ℤ nq dp))
        ( mul-ℤ dr ( mul-ℤ np dq))
   diff-ℤ
      (dq *ℤ (nr *ℤ dp) +ℤ dr *ℤ (nq *ℤ dp))
      (dr *ℤ (nq *ℤ dp) +ℤ dq *ℤ (np *ℤ dr))
    by
      ap-diff-ℤ
        ( ap-add-ℤ
          ( lemma-interchange-mul-ℤ dp nr dq)
          ( refl))
        ( ap-add-ℤ
          ( lemma-interchange-mul-ℤ dp nq dr)
          ( lemma-interchange-mul-ℤ dr np dq))
   diff-ℤ
      (dq *ℤ (nr *ℤ dp) +ℤ dr *ℤ (nq *ℤ dp))
      ((dq *ℤ (np *ℤ dr)) +ℤ (dr *ℤ (nq *ℤ dp)))
    by
      ap
        ( diff-ℤ (dq *ℤ (nr *ℤ dp) +ℤ dr *ℤ (nq *ℤ dp)))
        ( commutative-add-ℤ (dr *ℤ (nq *ℤ dp)) (dq *ℤ (np *ℤ dr)))
   (dq *ℤ (nr *ℤ dp)) -ℤ (dq *ℤ (np *ℤ dr))
    by
      right-translation-diff-ℤ
        (dq *ℤ (nr *ℤ dp))
        (dq *ℤ (np *ℤ dr))
        (dr *ℤ (nq *ℤ dp))
   dq *ℤ (nr *ℤ dp -ℤ np *ℤ dr)
    by inv (left-distributive-mul-diff-ℤ dq (nr *ℤ dp) (np *ℤ dr))
  where
  lemma-interchange-mul-ℤ : (a b c : )  (a *ℤ (b *ℤ c))  (c *ℤ (b *ℤ a))
  lemma-interchange-mul-ℤ a b c =
    inv (associative-mul-ℤ a b c) 
    ap (mul-ℤ' c) (commutative-mul-ℤ a b) 
    commutative-mul-ℤ (b *ℤ a) c

lemma-left-sim-cross-mul-diff-fraction-ℤ :
  (a a' b : fraction-ℤ) 
  sim-fraction-ℤ a a' 
  Id
    ( denominator-fraction-ℤ a *ℤ cross-mul-diff-fraction-ℤ a' b)
    ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b)
lemma-left-sim-cross-mul-diff-fraction-ℤ a a' b H =
  equational-reasoning
  ( denominator-fraction-ℤ a *ℤ cross-mul-diff-fraction-ℤ a' b)
   ( add-ℤ
        ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b)
        ( denominator-fraction-ℤ b *ℤ cross-mul-diff-fraction-ℤ a' a))
    by inv (lemma-add-cross-mul-diff-fraction-ℤ a' a b)
   ( add-ℤ
      ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b)
      ( zero-ℤ))
    by
      ap
        ( add-ℤ
          ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b))
          ( ( ap
              ( mul-ℤ (denominator-fraction-ℤ b))
              ( is-zero-cross-mul-diff-sim-fraction-ℤ a' a H')) 
            ( right-zero-law-mul-ℤ (denominator-fraction-ℤ b)))
   denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b
    by
      right-unit-law-add-ℤ
        ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b)
  where
  H' : sim-fraction-ℤ a' a
  H' = symmetric-sim-fraction-ℤ a a' H

lemma-right-sim-cross-mul-diff-fraction-ℤ :
  (a b b' : fraction-ℤ) 
  sim-fraction-ℤ b b' 
  Id
    ( denominator-fraction-ℤ b *ℤ cross-mul-diff-fraction-ℤ a b')
    ( denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b)
lemma-right-sim-cross-mul-diff-fraction-ℤ a b b' H =
  equational-reasoning
  ( denominator-fraction-ℤ b *ℤ cross-mul-diff-fraction-ℤ a b')
   ( add-ℤ
      ( denominator-fraction-ℤ a *ℤ cross-mul-diff-fraction-ℤ b b')
      ( denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b))
    by inv (lemma-add-cross-mul-diff-fraction-ℤ a b b')
   ( add-ℤ
      ( zero-ℤ)
      ( denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b))
    by
      ap
        ( add-ℤ' (denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b))
        ( ( ap
          ( mul-ℤ (denominator-fraction-ℤ a))
          ( is-zero-cross-mul-diff-sim-fraction-ℤ b b' H)) 
          ( right-zero-law-mul-ℤ (denominator-fraction-ℤ a)))
   denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b
    by
      left-unit-law-add-ℤ
        ( denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b)

Recent changes