Nonzero integers

Content created by Fredrik Bakke, Egbert Rijke and malarbol.

Created on 2023-10-06.

module elementary-number-theory.nonzero-integers where

Imports
open import elementary-number-theory.integers
open import elementary-number-theory.natural-numbers

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


Idea

An integer k is said to be nonzero if the proposition

  k ≠ 0


holds.

Definition

The predicate of being a nonzero integer

is-nonzero-prop-ℤ : ℤ → Prop lzero
is-nonzero-prop-ℤ k = neg-type-Prop (k ＝ zero-ℤ)

is-nonzero-ℤ : ℤ → UU lzero
is-nonzero-ℤ k = type-Prop (is-nonzero-prop-ℤ k)

is-prop-is-nonzero-ℤ : (k : ℤ) → is-prop (is-nonzero-ℤ k)
is-prop-is-nonzero-ℤ k = is-prop-type-Prop (is-nonzero-prop-ℤ k)


The nonzero integers

nonzero-ℤ : UU lzero
nonzero-ℤ = type-subtype is-nonzero-prop-ℤ

module _
(k : nonzero-ℤ)
where

int-nonzero-ℤ : ℤ
int-nonzero-ℤ = pr1 k

is-nonzero-nonzero-ℤ : is-nonzero-ℤ int-nonzero-ℤ
is-nonzero-nonzero-ℤ = pr2 k


The nonzero integer 1

is-nonzero-one-ℤ : is-nonzero-ℤ one-ℤ
is-nonzero-one-ℤ ()

one-nonzero-ℤ : nonzero-ℤ
pr1 one-nonzero-ℤ = one-ℤ
pr2 one-nonzero-ℤ = is-nonzero-one-ℤ


Properties

The integer image of a nonzero natural number is nonzero

is-nonzero-int-ℕ : (n : ℕ) → is-nonzero-ℕ n → is-nonzero-ℤ (int-ℕ n)
is-nonzero-int-ℕ zero-ℕ H p = H refl


The negative of a nonzero integer is nonzero

is-nonzero-neg-nonzero-ℤ : (x : ℤ) → is-nonzero-ℤ x → is-nonzero-ℤ (neg-ℤ x)
is-nonzero-neg-nonzero-ℤ x H K = H (is-zero-is-zero-neg-ℤ x K)