# Multiplication of positive, negative, nonnegative and nonpositive integers

Content created by Fredrik Bakke and malarbol.

Created on 2024-03-28.

module elementary-number-theory.multiplication-positive-and-negative-integers where

Imports
open import elementary-number-theory.addition-positive-and-negative-integers
open import elementary-number-theory.inequality-integers
open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.negative-integers
open import elementary-number-theory.nonnegative-integers
open import elementary-number-theory.nonpositive-integers
open import elementary-number-theory.positive-and-negative-integers
open import elementary-number-theory.positive-integers
open import elementary-number-theory.strict-inequality-integers

open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.identity-types
open import foundation.unit-type


## Idea

When we have information about the sign of the factors of an integer product, we can deduce the sign of their product too. The table below tabulates every case and displays the corresponding Agda definition.

pqp *ℤ qoperation
positivepositivepositivemul-positive-ℤ
positivenonnegativenonnegative
positivenegativenegative
positivenonpositivenonpositive
nonnegativepositivenonnegative
nonnegativenonnegativenonnegativemul-nonnegative-ℤ
nonnegativenegativenonpositive
nonnegativenonpositivenonpositive
negativepositivenegative
negativenonnegativenonpositive
negativenegativepositivemul-negative-ℤ
negativenonpositivenonnegative
nonpositivepositivenonpositive
nonpositivenonnegativenonpositive
nonpositivenegativenonpositive
nonpositivenonpositivenonnegativemul-nonpositive-ℤ

As a consequence, multiplication by a positive integer preserves and reflects strict inequality and multiplication by a nonpositive integer preserves inequality.

## Lemmas

### The product of two positive integers is positive

is-positive-mul-ℤ :
{x y : ℤ} → is-positive-ℤ x → is-positive-ℤ y → is-positive-ℤ (x *ℤ y)
is-positive-mul-ℤ {inr (inr zero-ℕ)} {y} H K = K
is-positive-mul-ℤ {inr (inr (succ-ℕ x))} {y} H K =
is-positive-add-ℤ K (is-positive-mul-ℤ {inr (inr x)} H K)


### The product of a positive and a nonnegative integer is nonnegative

is-nonnegative-mul-positive-nonnegative-ℤ :
{x y : ℤ} → is-positive-ℤ x → is-nonnegative-ℤ y → is-nonnegative-ℤ (x *ℤ y)
is-nonnegative-mul-positive-nonnegative-ℤ {inr (inr zero-ℕ)} {y} H K = K
is-nonnegative-mul-positive-nonnegative-ℤ {inr (inr (succ-ℕ x))} {y} H K =
( is-nonnegative-mul-positive-nonnegative-ℤ {inr (inr x)} H K)


### The product of a positive and a negative integer is negative

is-negative-mul-positive-negative-ℤ :
{x y : ℤ} → is-positive-ℤ x → is-negative-ℤ y → is-negative-ℤ (x *ℤ y)
is-negative-mul-positive-negative-ℤ {x} {y} H K =
is-negative-eq-ℤ
( neg-neg-ℤ (x *ℤ y))
( is-negative-neg-is-positive-ℤ
( is-positive-eq-ℤ
( right-negative-law-mul-ℤ x y)
( is-positive-mul-ℤ H (is-positive-neg-is-negative-ℤ K))))


### The product of a positive and a nonpositive integer is nonpositive

is-nonpositive-mul-positive-nonpositive-ℤ :
{x y : ℤ} → is-positive-ℤ x → is-nonpositive-ℤ y → is-nonpositive-ℤ (x *ℤ y)
is-nonpositive-mul-positive-nonpositive-ℤ {x} {y} H K =
is-nonpositive-eq-ℤ
( neg-neg-ℤ (x *ℤ y))
( is-nonpositive-neg-is-nonnegative-ℤ
( is-nonnegative-eq-ℤ
( right-negative-law-mul-ℤ x y)
( is-nonnegative-mul-positive-nonnegative-ℤ H
( is-nonnegative-neg-is-nonpositive-ℤ K))))


### The product of a nonnegative integer and a positive integer is nonnegative

is-nonnegative-mul-nonnegative-positive-ℤ :
{x y : ℤ} → is-nonnegative-ℤ x → is-positive-ℤ y → is-nonnegative-ℤ (x *ℤ y)
is-nonnegative-mul-nonnegative-positive-ℤ {x} {y} H K =
is-nonnegative-eq-ℤ
( commutative-mul-ℤ y x)
( is-nonnegative-mul-positive-nonnegative-ℤ K H)


### The product of two nonnegative integers is nonnegative

is-nonnegative-mul-ℤ :
{x y : ℤ} →
is-nonnegative-ℤ x → is-nonnegative-ℤ y → is-nonnegative-ℤ (x *ℤ y)
is-nonnegative-mul-ℤ {inr (inl star)} {y} H K = star
is-nonnegative-mul-ℤ {inr (inr x)} {inr (inl star)} H K =
is-nonnegative-eq-ℤ (inv (right-zero-law-mul-ℤ (inr (inr x)))) star
is-nonnegative-mul-ℤ {inr (inr x)} {inr (inr y)} H K =
is-nonnegative-eq-ℤ (inv (compute-mul-ℤ (inr (inr x)) (inr (inr y)))) star


### The product of a nonnegative and a negative integer is nonpositive

is-nonpositive-mul-nonnegative-negative-ℤ :
{x y : ℤ} → is-nonnegative-ℤ x → is-negative-ℤ y → is-nonpositive-ℤ (x *ℤ y)
is-nonpositive-mul-nonnegative-negative-ℤ {x} {y} H K =
is-nonpositive-eq-ℤ
( neg-neg-ℤ (x *ℤ y))
( is-nonpositive-neg-is-nonnegative-ℤ
( is-nonnegative-eq-ℤ
( right-negative-law-mul-ℤ x y)
( is-nonnegative-mul-nonnegative-positive-ℤ H
( is-positive-neg-is-negative-ℤ K))))


### The product of a nonnegative and a nonpositive integer is nonpositive

is-nonpositive-mul-nonnegative-nonpositive-ℤ :
{x y : ℤ} →
is-nonnegative-ℤ x → is-nonpositive-ℤ y → is-nonpositive-ℤ (x *ℤ y)
is-nonpositive-mul-nonnegative-nonpositive-ℤ {x} {y} H K =
is-nonpositive-eq-ℤ
( neg-neg-ℤ (x *ℤ y))
( is-nonpositive-neg-is-nonnegative-ℤ
( is-nonnegative-eq-ℤ
( right-negative-law-mul-ℤ x y)
( is-nonnegative-mul-ℤ H
( is-nonnegative-neg-is-nonpositive-ℤ K))))


### The product of a negative and a positive integer is negative

is-negative-mul-negative-positive-ℤ :
{x y : ℤ} → is-negative-ℤ x → is-positive-ℤ y → is-negative-ℤ (x *ℤ y)
is-negative-mul-negative-positive-ℤ {x} {y} H K =
is-negative-eq-ℤ
( commutative-mul-ℤ y x)
( is-negative-mul-positive-negative-ℤ K H)


### The product of a negative and a nonnegative integer is nonpositive

is-nonpositive-mul-negative-nonnegative-ℤ :
{x y : ℤ} → is-negative-ℤ x → is-nonnegative-ℤ y → is-nonpositive-ℤ (x *ℤ y)
is-nonpositive-mul-negative-nonnegative-ℤ {x} {y} H K =
is-nonpositive-eq-ℤ
( commutative-mul-ℤ y x)
( is-nonpositive-mul-nonnegative-negative-ℤ K H)


### The product of two negative integers is positive

is-positive-mul-negative-ℤ :
{x y : ℤ} → is-negative-ℤ x → is-negative-ℤ y → is-positive-ℤ (x *ℤ y)
is-positive-mul-negative-ℤ {x} {y} H K =
is-positive-eq-ℤ
( double-negative-law-mul-ℤ x y)
( is-positive-mul-ℤ
( is-positive-neg-is-negative-ℤ H)
( is-positive-neg-is-negative-ℤ K))


### The product of a negative and a nonpositive integer is nonnegative

is-nonnegative-mul-negative-nonpositive-ℤ :
{x y : ℤ} → is-negative-ℤ x → is-nonpositive-ℤ y → is-nonnegative-ℤ (x *ℤ y)
is-nonnegative-mul-negative-nonpositive-ℤ {x} {y} H K =
is-nonnegative-eq-ℤ
( double-negative-law-mul-ℤ x y)
( is-nonnegative-mul-positive-nonnegative-ℤ
( is-positive-neg-is-negative-ℤ H)
( is-nonnegative-neg-is-nonpositive-ℤ K))


### The product of a nonpositive and a positive integer is nonpositive

is-nonpositive-mul-nonpositive-positive-ℤ :
{x y : ℤ} → is-nonpositive-ℤ x → is-positive-ℤ y → is-nonpositive-ℤ (x *ℤ y)
is-nonpositive-mul-nonpositive-positive-ℤ {x} {y} H K =
is-nonpositive-eq-ℤ
( commutative-mul-ℤ y x)
( is-nonpositive-mul-positive-nonpositive-ℤ K H)


### The product of a nonpositive and a nonnegative integer is nonpositive

is-nonpositive-mul-nonpositive-nonnegative-ℤ :
{x y : ℤ} →
is-nonpositive-ℤ x → is-nonnegative-ℤ y → is-nonpositive-ℤ (x *ℤ y)
is-nonpositive-mul-nonpositive-nonnegative-ℤ {x} {y} H K =
is-nonpositive-eq-ℤ
( commutative-mul-ℤ y x)
( is-nonpositive-mul-nonnegative-nonpositive-ℤ K H)


### The product of a nonpositive integer and a negative integer is nonnegative

is-nonnegative-mul-nonpositive-negative-ℤ :
{ x y : ℤ} → is-nonpositive-ℤ x → is-negative-ℤ y → is-nonnegative-ℤ (x *ℤ y)
is-nonnegative-mul-nonpositive-negative-ℤ {x} {y} H K =
is-nonnegative-eq-ℤ
( commutative-mul-ℤ y x)
( is-nonnegative-mul-negative-nonpositive-ℤ K H)


### The product of two nonpositive integers is nonnegative

is-nonnegative-mul-nonpositive-ℤ :
{x y : ℤ} →
is-nonpositive-ℤ x → is-nonpositive-ℤ y → is-nonnegative-ℤ (x *ℤ y)
is-nonnegative-mul-nonpositive-ℤ {x} {y} H K =
is-nonnegative-eq-ℤ
( double-negative-law-mul-ℤ x y)
( is-nonnegative-mul-ℤ
( is-nonnegative-neg-is-nonpositive-ℤ H)
( is-nonnegative-neg-is-nonpositive-ℤ K))


### The left factor of a positive product with a positive right factor is positive

is-positive-left-factor-mul-ℤ :
{x y : ℤ} → is-positive-ℤ (x *ℤ y) → is-positive-ℤ y → is-positive-ℤ x
is-positive-left-factor-mul-ℤ {inl x} {inr (inr y)} H K =
is-positive-eq-ℤ (compute-mul-ℤ (inl x) (inr (inr y))) H
is-positive-left-factor-mul-ℤ {inr (inl star)} {inr (inr y)} H K =
is-positive-eq-ℤ (compute-mul-ℤ zero-ℤ (inr (inr y))) H
is-positive-left-factor-mul-ℤ {inr (inr x)} {inr (inr y)} H K = star


### The right factor of a positive product with a positive left factor is positive

is-positive-right-factor-mul-ℤ :
{x y : ℤ} → is-positive-ℤ (x *ℤ y) → is-positive-ℤ x → is-positive-ℤ y
is-positive-right-factor-mul-ℤ {x} {y} H =
is-positive-left-factor-mul-ℤ (is-positive-eq-ℤ (commutative-mul-ℤ x y) H)


### The left factor of a nonnegative product with a positive right factor is nonnegative

is-nonnegative-left-factor-mul-ℤ :
{x y : ℤ} → is-nonnegative-ℤ (x *ℤ y) → is-positive-ℤ y → is-nonnegative-ℤ x
is-nonnegative-left-factor-mul-ℤ {inl x} {inr (inr y)} H K =
ex-falso (is-nonnegative-eq-ℤ (compute-mul-ℤ (inl x) (inr (inr y))) H)
is-nonnegative-left-factor-mul-ℤ {inr x} {inr y} H K = star


### The right factor of a nonnegative product with a positive left factor is nonnegative

is-nonnegative-right-factor-mul-ℤ :
{x y : ℤ} → is-nonnegative-ℤ (x *ℤ y) → is-positive-ℤ x → is-nonnegative-ℤ y
is-nonnegative-right-factor-mul-ℤ {x} {y} H =
is-nonnegative-left-factor-mul-ℤ
( is-nonnegative-eq-ℤ (commutative-mul-ℤ x y) H)


## Definitions

### Multiplication by a signed integer

int-mul-positive-ℤ : positive-ℤ → ℤ → ℤ
int-mul-positive-ℤ x y = int-positive-ℤ x *ℤ y

int-mul-positive-ℤ' : positive-ℤ → ℤ → ℤ
int-mul-positive-ℤ' x y = y *ℤ int-positive-ℤ x

int-mul-nonnegative-ℤ : nonnegative-ℤ → ℤ → ℤ
int-mul-nonnegative-ℤ x y = int-nonnegative-ℤ x *ℤ y

int-mul-nonnegative-ℤ' : nonnegative-ℤ → ℤ → ℤ
int-mul-nonnegative-ℤ' x y = y *ℤ int-nonnegative-ℤ x

int-mul-negative-ℤ : negative-ℤ → ℤ → ℤ
int-mul-negative-ℤ x y = int-negative-ℤ x *ℤ y

int-mul-negative-ℤ' : negative-ℤ → ℤ → ℤ
int-mul-negative-ℤ' x y = y *ℤ int-negative-ℤ x

int-mul-nonpositive-ℤ : nonpositive-ℤ → ℤ → ℤ
int-mul-nonpositive-ℤ x y = int-nonpositive-ℤ x *ℤ y

int-mul-nonpositive-ℤ' : nonpositive-ℤ → ℤ → ℤ
int-mul-nonpositive-ℤ' x y = y *ℤ int-nonpositive-ℤ x


### Multiplication of positive integers

mul-positive-ℤ : positive-ℤ → positive-ℤ → positive-ℤ
mul-positive-ℤ (x , H) (y , K) = (mul-ℤ x y , is-positive-mul-ℤ H K)


### Multiplication of nonnegative integers

mul-nonnegative-ℤ : nonnegative-ℤ → nonnegative-ℤ → nonnegative-ℤ
mul-nonnegative-ℤ (x , H) (y , K) = (mul-ℤ x y , is-nonnegative-mul-ℤ H K)


### Multiplication of negative integers

mul-negative-ℤ : negative-ℤ → negative-ℤ → positive-ℤ
mul-negative-ℤ (x , H) (y , K) = (mul-ℤ x y , is-positive-mul-negative-ℤ H K)


### Multiplication of nonpositive integers

mul-nonpositive-ℤ : nonpositive-ℤ → nonpositive-ℤ → nonnegative-ℤ
mul-nonpositive-ℤ (x , H) (y , K) =
(mul-ℤ x y , is-nonnegative-mul-nonpositive-ℤ H K)


## Properties

### Multiplication by a positive integer preserves and reflects the strict ordering

module _
(z : positive-ℤ) (x y : ℤ)
where

preserves-le-right-mul-positive-ℤ :
le-ℤ x y → le-ℤ (int-mul-positive-ℤ z x) (int-mul-positive-ℤ z y)
preserves-le-right-mul-positive-ℤ K =
is-positive-eq-ℤ
( left-distributive-mul-diff-ℤ (int-positive-ℤ z) y x)
( is-positive-mul-ℤ (is-positive-int-positive-ℤ z) K)

preserves-le-left-mul-positive-ℤ :
le-ℤ x y → le-ℤ (int-mul-positive-ℤ' z x) (int-mul-positive-ℤ' z y)
preserves-le-left-mul-positive-ℤ K =
is-positive-eq-ℤ
( right-distributive-mul-diff-ℤ y x (int-positive-ℤ z))
( is-positive-mul-ℤ K (is-positive-int-positive-ℤ z))

reflects-le-right-mul-positive-ℤ :
le-ℤ (int-mul-positive-ℤ z x) (int-mul-positive-ℤ z y) → le-ℤ x y
reflects-le-right-mul-positive-ℤ K =
is-positive-right-factor-mul-ℤ
( is-positive-eq-ℤ
( inv (left-distributive-mul-diff-ℤ (int-positive-ℤ z) y x))
( K))
( is-positive-int-positive-ℤ z)

reflects-le-left-mul-positive-ℤ :
le-ℤ (int-mul-positive-ℤ' z x) (int-mul-positive-ℤ' z y) → le-ℤ x y
reflects-le-left-mul-positive-ℤ K =
is-positive-left-factor-mul-ℤ
( is-positive-eq-ℤ
( inv (right-distributive-mul-diff-ℤ y x (int-positive-ℤ z)))
( K))
( is-positive-int-positive-ℤ z)


### Multiplication by a nonnegative integer preserves inequality

module _
(z : nonnegative-ℤ) (x y : ℤ)
where

preserves-leq-right-mul-nonnegative-ℤ :
leq-ℤ x y → leq-ℤ (int-mul-nonnegative-ℤ z x) (int-mul-nonnegative-ℤ z y)
preserves-leq-right-mul-nonnegative-ℤ K =
is-nonnegative-eq-ℤ
( left-distributive-mul-diff-ℤ (int-nonnegative-ℤ z) y x)
( is-nonnegative-mul-ℤ (is-nonnegative-int-nonnegative-ℤ z) K)

preserves-leq-left-mul-nonnegative-ℤ :
leq-ℤ x y → leq-ℤ (int-mul-nonnegative-ℤ' z x) (int-mul-nonnegative-ℤ' z y)
preserves-leq-left-mul-nonnegative-ℤ K =
is-nonnegative-eq-ℤ
( right-distributive-mul-diff-ℤ y x (int-nonnegative-ℤ z))
( is-nonnegative-mul-ℤ K (is-nonnegative-int-nonnegative-ℤ z))