Multiplication by nonnegative rational numbers

Content created by Louis Wasserman.

Created on 2025-10-03.
Last modified on 2025-10-17.

{-# OPTIONS --lossy-unification #-}

module elementary-number-theory.multiplication-nonnegative-rational-numbers where
Imports 
open import elementary-number-theory.decidable-total-order-rational-numbers
open import elementary-number-theory.inequality-integers
open import elementary-number-theory.inequality-nonnegative-rational-numbers
open import elementary-number-theory.inequality-rational-numbers
open import elementary-number-theory.maximum-rational-numbers
open import elementary-number-theory.minimum-rational-numbers
open import elementary-number-theory.multiplication-integer-fractions
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.multiplication-positive-and-negative-integers
open import elementary-number-theory.multiplication-rational-numbers
open import elementary-number-theory.nonnegative-integer-fractions
open import elementary-number-theory.nonnegative-rational-numbers
open import elementary-number-theory.rational-numbers

open import foundation.binary-transport
open import foundation.dependent-pair-types
open import foundation.identity-types

open import order-theory.order-preserving-maps-total-orders

Idea

The product of two nonnegative rational numbers is their product as rational numbers, and is itself nonnegative.

Definition

opaque
  unfolding is-nonnegative-ℚ mul-ℚ

  is-nonnegative-mul-ℚ :
    {p q : ℚ} → is-nonnegative-ℚ p → is-nonnegative-ℚ q →
    is-nonnegative-ℚ (p *ℚ q)
  is-nonnegative-mul-ℚ {p} {q} nonneg-p nonneg-q =
    is-nonnegative-rational-fraction-ℤ
      ( is-nonnegative-mul-nonnegative-fraction-ℤ
        { fraction-ℚ p}
        { fraction-ℚ q}
        ( nonneg-p)
        ( nonneg-q))

mul-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺
mul-ℚ⁰⁺ (p , nonneg-p) (q , nonneg-q) =
  ( p *ℚ q , is-nonnegative-mul-ℚ nonneg-p nonneg-q)

infixl 35 _*ℚ⁰⁺_
_*ℚ⁰⁺_ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺
_*ℚ⁰⁺_ = mul-ℚ⁰⁺

Properties

Multiplication of nonnegative rational numbers is commutative

abstract
  commutative-mul-ℚ⁰⁺ : (p q : ℚ⁰⁺) → p *ℚ⁰⁺ q ＝ q *ℚ⁰⁺ p
  commutative-mul-ℚ⁰⁺ (p , _) (q , _) = eq-ℚ⁰⁺ (commutative-mul-ℚ p q)

Multiplication by a nonnegative rational number preserves inequality

opaque
  unfolding is-nonnegative-ℚ leq-ℚ-Prop mul-ℚ

  preserves-leq-right-mul-ℚ⁰⁺ :
    (p : ℚ⁰⁺) (q r : ℚ) → leq-ℚ q r →
    leq-ℚ (q *ℚ rational-ℚ⁰⁺ p) (r *ℚ rational-ℚ⁰⁺ p)
  preserves-leq-right-mul-ℚ⁰⁺
    p⁺@((p@(np , dp , pos-dp) , _) , nonneg-np)
    (q@(nq , dq , _) , _)
    (r@(nr , dr , _) , _)
    q≤r =
    preserves-leq-rational-fraction-ℤ
      ( mul-fraction-ℤ q p)
      ( mul-fraction-ℤ r p)
      ( binary-tr
        ( leq-ℤ)
        ( interchange-law-mul-mul-ℤ _ _ _ _)
        ( interchange-law-mul-mul-ℤ _ _ _ _)
        ( preserves-leq-left-mul-nonnegative-ℤ
          ( np *ℤ dp ,
            is-nonnegative-mul-nonnegative-positive-ℤ nonneg-np pos-dp)
          ( nq *ℤ dr)
          ( nr *ℤ dq)
          ( q≤r)))

  preserves-leq-left-mul-ℚ⁰⁺ :
    (p : ℚ⁰⁺) (q r : ℚ) → leq-ℚ q r →
    leq-ℚ (rational-ℚ⁰⁺ p *ℚ q) (rational-ℚ⁰⁺ p *ℚ r)
  preserves-leq-left-mul-ℚ⁰⁺ p q r q≤r =
    binary-tr
      ( leq-ℚ)
      ( commutative-mul-ℚ q (rational-ℚ⁰⁺ p))
      ( commutative-mul-ℚ r (rational-ℚ⁰⁺ p))
      ( preserves-leq-right-mul-ℚ⁰⁺ p q r q≤r)

abstract
  preserves-leq-mul-ℚ⁰⁺ :
    (p q r s : ℚ⁰⁺) → leq-ℚ⁰⁺ p q → leq-ℚ⁰⁺ r s → leq-ℚ⁰⁺ (p *ℚ⁰⁺ r) (q *ℚ⁰⁺ s)
  preserves-leq-mul-ℚ⁰⁺ p q r s p≤q r≤s =
    transitive-leq-ℚ
      ( rational-ℚ⁰⁺ (p *ℚ⁰⁺ r))
      ( rational-ℚ⁰⁺ (p *ℚ⁰⁺ s))
      ( rational-ℚ⁰⁺ (q *ℚ⁰⁺ s))
      ( preserves-leq-right-mul-ℚ⁰⁺ s _ _ p≤q)
      ( preserves-leq-left-mul-ℚ⁰⁺ p _ _ r≤s)

Multiplication by a nonnegative rational number distributes over the minimum operation

abstract
  left-distributive-mul-min-ℚ⁰⁺ :
    (p : ℚ⁰⁺) (q r : ℚ) →
    rational-ℚ⁰⁺ p *ℚ min-ℚ q r ＝
    min-ℚ (rational-ℚ⁰⁺ p *ℚ q) (rational-ℚ⁰⁺ p *ℚ r)
  left-distributive-mul-min-ℚ⁰⁺ p⁰⁺@(p , _) =
    distributive-map-hom-min-Total-Order
      ( ℚ-Total-Order)
      ( ℚ-Total-Order)
      ( p *ℚ_ , preserves-leq-left-mul-ℚ⁰⁺ p⁰⁺)

Multiplication by a nonnegative rational number distributes over the maximum operation

abstract
  left-distributive-mul-max-ℚ⁰⁺ :
    (p : ℚ⁰⁺) (q r : ℚ) →
    rational-ℚ⁰⁺ p *ℚ max-ℚ q r ＝
    max-ℚ (rational-ℚ⁰⁺ p *ℚ q) (rational-ℚ⁰⁺ p *ℚ r)
  left-distributive-mul-max-ℚ⁰⁺ p⁰⁺@(p , _) =
    distributive-map-hom-max-Total-Order
      ( ℚ-Total-Order)
      ( ℚ-Total-Order)
      ( p *ℚ_ , preserves-leq-left-mul-ℚ⁰⁺ p⁰⁺)

Recent changes