The Theory %int%

Parents

sets

Children

dyadic

Constants

Is_ℤ_Rep	(ℕ × ℕ) SET → BOOL
ℕℤ	ℕ → ℤ
$~_Z	ℤ → ℤ
$+_Z	ℤ → ℤ → ℤ
$-_Z	ℤ → ℤ → ℤ
$*_Z	ℤ → ℤ → ℤ
$≤_Z	ℤ → ℤ → BOOL
$<_Z	ℤ → ℤ → BOOL
$≥_Z	ℤ → ℤ → BOOL
$>_Z	ℤ → ℤ → BOOL
$Abs_Z	ℤ → ℤ
$Mod_Z	ℤ → ℤ → ℤ
$Div_Z	ℤ → ℤ → ℤ

Aliases

+	$+_Z : ℤ → ℤ → ℤ
-	$-_Z : ℤ → ℤ → ℤ
~	$~_Z : ℤ → ℤ
*	$*_Z : ℤ → ℤ → ℤ
≤	$≤_Z : ℤ → ℤ → BOOL
<	$<_Z : ℤ → ℤ → BOOL
≥	$≥_Z : ℤ → ℤ → BOOL
>	$>_Z : ℤ → ℤ → BOOL
Abs	$Abs_Z : ℤ → ℤ
Div	$Div_Z : ℤ → ℤ → ℤ
Mod	$Mod_Z : ℤ → ℤ → ℤ

Types

ℤ

Fixity

Left Infix 305:

-_Z

Left Infix 315:

Div_Z

Mod_Z

Right Infix 210:

<_Z

>_Z

≤_Z

≥_Z

Right Infix 300:

+_Z

Right Infix 310:

*_Z

Prefix 350:

Abs_Z

~_Z

Definitions

Is_ℤ_Rep	⊢ ∀ a• Is_ℤ_Rep a ⇔ (∃ m n• a = {(x, y)\|m + y = n + x})
ℤ ℤ_def	⊢ ∃ f• TypeDefn Is_ℤ_Rep f
+_Z ~_Z ℕℤ	⊢ ConstSpec (λ (+_Z', ~_Z', $"ℕℤ'") • (∀ i j k • +_Z' (+_Z' i j) k = +_Z' i (+_Z' j k) ∧ +_Z' i j = +_Z' j i ∧ +_Z' i (~_Z' i) = $"ℕℤ'" 0 ∧ +_Z' i ($"ℕℤ'" 0) = i) ∧ (∀ m n • +_Z' ($"ℕℤ'" m) ($"ℕℤ'" n) = $"ℕℤ'" (m + n)) ∧ OneOne $"ℕℤ'" ∧ (∀ i • ∃ m• i = $"ℕℤ'" m ∨ i = ~_Z' ($"ℕℤ'" m))) ($+, ~, ℕℤ)
-_Z	⊢ ∀ i j• i - j = i + ~ j
*_Z	⊢ ConstSpec (λ _Z' • ∀ i j k • _Z' i (j + k) = _Z' i j + _Z' i k ∧ _Z' i (ℕℤ 1) = i) $
≤_Z	⊢ ∀ i j• i ≤ j ⇔ (∃ m• i + ℕℤ m = j)
<_Z	⊢ ∀ i j• i < j ⇔ i + ℕℤ 1 ≤ j
≥_Z	⊢ ∀ i j• i ≥ j ⇔ j ≤ i
>_Z	⊢ ∀ i j• i > j ⇔ j < i
Abs_Z	⊢ ∀ i• Abs i = (if ℕℤ 0 ≤ i then i else ~ i)
Div_Z Mod_Z	⊢ ConstSpec (λ (Div_Z', Mod_Z') • ∀ i j • ¬ j = ℕℤ 0 ⇒ i = Div_Z' i j * j + Mod_Z' i j ∧ ℕℤ 0 ≤ Mod_Z' i j ∧ Mod_Z' i j < Abs j) ($Div, $Mod)

Theorems

is_ℤ_rep_consistent_thm	⊢ ∃ a• Is_ℤ_Rep a
+_Z_consistent ~_Z_consistent ℕℤ_consistent	⊢ Consistent (λ (+_Z', ~_Z', $"ℕℤ'") • (∀ i j k • +_Z' (+_Z' i j) k = +_Z' i (+_Z' j k) ∧ +_Z' i j = +_Z' j i ∧ +_Z' i (~_Z' i) = $"ℕℤ'" 0 ∧ +_Z' i ($"ℕℤ'" 0) = i) ∧ (∀ m n • +_Z' ($"ℕℤ'" m) ($"ℕℤ'" n) = $"ℕℤ'" (m + n)) ∧ OneOne $"ℕℤ'" ∧ (∀ i • ∃ m• i = $"ℕℤ'" m ∨ i = ~_Z' ($"ℕℤ'" m)))
ℤ_plus_comm_thm	⊢ ∀ i j• i + j = j + i
ℤ_plus_assoc_thm	⊢ ∀ i j k• (i + j) + k = i + j + k
ℤ_plus_assoc_thm1	⊢ ∀ i j k• i + j + k = (i + j) + k
ℤ_plus_order_thm	⊢ ∀ i j k • j + i = i + j ∧ (i + j) + k = i + j + k ∧ j + i + k = i + j + k
ℤ_cases_thm	⊢ ∀ i• ∃ m• i = ℕℤ m ∨ i = ~ (ℕℤ m)
ℤ_plus0_thm	⊢ ∀ i• i + ℕℤ 0 = i ∧ ℕℤ 0 + i = i
ℤ_plus_minus_thm	⊢ ∀ i• i + ~ i = ℕℤ 0 ∧ ~ i + i = ℕℤ 0
ℤ_eq_thm	⊢ ∀ i j• i = j ⇔ i + ~ j = ℕℤ 0
ℕℤ_plus_homomorphism_thm	⊢ ∀ m n• ℕℤ (m + n) = ℕℤ m + ℕℤ n
ℤ_minus_clauses	⊢ ∀ i j • ~ (~ i) = i ∧ i + ~ i = ℕℤ 0 ∧ ~ i + i = ℕℤ 0 ∧ ~ (i + j) = ~ i + ~ j ∧ ~ (ℕℤ 0) = ℕℤ 0
ℤ_cases_thm1	⊢ ∀ i• ∃ m• i = ℕℤ m ∨ i = ~ (ℕℤ (m + 1))
ℤ_induction_thm	⊢ ∀ p • p (ℕℤ 1) ∧ (∀ i• p i ⇒ p (~ i)) ∧ (∀ i j• p i ∧ p j ⇒ p (i + j)) ⇒ (∀ i• p i)
ℕℤ_one_one_thm	⊢ ∀ m n• ℕℤ m = ℕℤ n ⇔ m = n
ℤ_plus_clauses	⊢ ∀ i j k • (i + k = j + k ⇔ i = j) ∧ (k + i = j + k ⇔ i = j) ∧ (i + k = k + j ⇔ i = j) ∧ (k + i = k + j ⇔ i = j) ∧ (i + k = k ⇔ i = ℕℤ 0) ∧ (k + i = k ⇔ i = ℕℤ 0) ∧ (k = k + j ⇔ j = ℕℤ 0) ∧ (k = j + k ⇔ j = ℕℤ 0) ∧ i + ℕℤ 0 = i ∧ ℕℤ 0 + i = i ∧ ¬ ℕℤ 1 = ℕℤ 0 ∧ ¬ ℕℤ 0 = ℕℤ 1
ℤ_≤_≤_0_thm	⊢ ∀ i j• i ≤ j ⇔ i + ~ j ≤ ℕℤ 0
ℤ_minus_≤_thm	⊢ ∀ i j• ~ i ≤ ~ j ⇔ j ≤ i
ℤ_≤_minus_thm	⊢ ∀ i j• i ≤ j ⇔ ~ j ≤ ~ i
ℤ_≤_clauses	⊢ ∀ i j k • (i + k ≤ j + k ⇔ i ≤ j) ∧ (k + i ≤ j + k ⇔ i ≤ j) ∧ (i + k ≤ k + j ⇔ i ≤ j) ∧ (k + i ≤ k + j ⇔ i ≤ j) ∧ (i + k ≤ k ⇔ i ≤ ℕℤ 0) ∧ (k + i ≤ k ⇔ i ≤ ℕℤ 0) ∧ (k ≤ k + j ⇔ ℕℤ 0 ≤ j) ∧ (k ≤ j + k ⇔ ℕℤ 0 ≤ j) ∧ i ≤ i ∧ ¬ ℕℤ 1 ≤ ℕℤ 0 ∧ ℕℤ 0 ≤ ℕℤ 1
ℕℤ_≤_thm	⊢ ∀ m n• ℕℤ m ≤ ℕℤ n ⇔ m ≤ n
*_Z_consistent	⊢ Consistent (λ _Z' • ∀ i j k • _Z' i (j + k) = _Z' i j + _Z' i k ∧ *_Z' i (ℕℤ 1) = i)
ℕℤ_times_homomorphism_thm	⊢ ∀ m n• ℕℤ (m * n) = ℕℤ m * ℕℤ n
ℤ_times_minus_thm	⊢ ∀ i j • ~ i * j = ~ (i * j) ∧ i * ~ j = ~ (i * j) ∧ ~ i * ~ j = i * j
ℤ_times_comm_thm	⊢ ∀ i j• i * j = j * i
ℤ_times_assoc_thm	⊢ ∀ i j k• (i * j) * k = i * j * k
Div_Z_consistent Mod_Z_consistent	⊢ Consistent (λ (Div_Z', Mod_Z') • ∀ i j • ¬ j = ℕℤ 0 ⇒ i = Div_Z' i j * j + Mod_Z' i j ∧ ℕℤ 0 ≤ Mod_Z' i j ∧ Mod_Z' i j < Abs j)
ℕℤ_plus_homomorphism_thm1	⊢ ∀ m n• ℕℤ m + ℕℤ n = ℕℤ (m + n)
ℤ_ℕ_induction_thm	⊢ ∀ p • p (ℕℤ 0) ∧ (∀ i• ℕℤ 0 ≤ i ∧ p i ⇒ p (i + ℕℤ 1)) ⇒ (∀ m• ℕℤ 0 ≤ m ⇒ p m)
ℤ_ℕ_plus_thm	⊢ ∀ i j• ℕℤ 0 ≤ i ∧ ℕℤ 0 ≤ j ⇒ ℕℤ 0 ≤ i + j
ℤ_ℕ_plus1_thm	⊢ ∀ i• ℕℤ 0 ≤ i ⇒ ℕℤ 0 ≤ i + ℕℤ 1
ℤ_minus_thm	⊢ ∀ i j • ~ (~ i) = i ∧ i + ~ i = ℕℤ 0 ∧ ~ i + i = ℕℤ 0 ∧ ~ (i + j) = ~ i + ~ j ∧ ~ (ℕℤ 0) = ℕℤ 0
ℤ_ℕ_cases_thm	⊢ ∀ i • ℕℤ 0 ≤ i ⇒ i = ℕℤ 0 ∨ (∃ j• ℕℤ 0 ≤ j ∧ i = j + ℕℤ 1)
ℤ_ℕ_¬_minus_thm	⊢ ∀ i• ℕℤ 0 ≤ i ⇒ i = ℕℤ 0 ∨ ¬ ℕℤ 0 ≤ ~ i
ℤ_¬_ℕ_thm	⊢ ∀ i• ¬ ℕℤ 0 ≤ i ⇒ ℕℤ 0 ≤ ~ i
ℤ_plus_eq_thm	⊢ ∀ i j k• i + j = k ⇔ i = k + ~ j
ℤ_ℕ_¬_plus1_thm	⊢ ∀ i• ℕℤ 0 ≤ i ⇒ ¬ i + ℕℤ 1 = ℕℤ 0
ℤ_times_assoc_thm1	⊢ ∀ i j k• i * j * k = (i * j) * k
ℤ_times_order_thm	⊢ ∀ i j k • j * i = i * j ∧ (i * j) * k = i * j * k ∧ j * i * k = i * j * k
ℕℤ_times_homomorphism_thm1	⊢ ∀ m n• ℕℤ m * ℕℤ n = ℕℤ (m * n)
ℤ_times1_thm	⊢ ∀ i• i * ℕℤ 1 = i ∧ ℕℤ 1 * i = i
ℤ_times_plus_distrib_thm	⊢ ∀ i j k • i * (j + k) = i * j + i * k ∧ (i + j) * k = i * k + j * k
ℤ_times0_thm	⊢ ∀ i• ℕℤ 0 * i = ℕℤ 0 ∧ i * ℕℤ 0 = ℕℤ 0
ℤ_eq_thm1	⊢ ∀ i j• i = j ⇔ ~ i + j = ℕℤ 0
ℤ_times_eq_0_thm	⊢ ∀ i j• i * j = ℕℤ 0 ⇔ i = ℕℤ 0 ∨ j = ℕℤ 0
ℤ_times_clauses	⊢ ∀ i j • ℕℤ 0 * i = ℕℤ 0 ∧ i * ℕℤ 0 = ℕℤ 0 ∧ i * ℕℤ 1 = i ∧ ℕℤ 1 * i = i
ℤ_ℕ_times_thm	⊢ ∀ i j• ℕℤ 0 ≤ i ∧ ℕℤ 0 ≤ j ⇒ ℕℤ 0 ≤ i * j
ℤ_≤_trans_thm	⊢ ∀ i j k• i ≤ j ∧ j ≤ k ⇒ i ≤ k
ℤ_≤_cases_thm	⊢ ∀ i j• i ≤ j ∨ j ≤ i
ℤ_≤_refl_thm	⊢ ∀ i• i ≤ i
ℤ_≤_≤_0_thm1	⊢ ∀ i j• i ≤ j ⇔ ℕℤ 0 ≤ j + ~ i
ℤ_≤_antisym_thm	⊢ ∀ i j• i ≤ j ∧ j ≤ i ⇒ i = j
ℤ_less_trans_thm	⊢ ∀ i j k• i < j ∧ j < k ⇒ i < k
ℤ_less_irrefl_thm	⊢ ∀ i j• ¬ (i < j ∧ j < i)
ℤ_less_cases_thm	⊢ ∀ i j• i < j ∨ i = j ∨ j < i
ℕℤ_less_thm	⊢ ∀ m n• ℕℤ m < ℕℤ n ⇔ m < n
ℤ_less_less_0_thm	⊢ ∀ i j• i < j ⇔ i + ~ j < ℕℤ 0
ℤ_less_less_0_thm1	⊢ ∀ i j• i < j ⇔ ℕℤ 0 < j + ~ i
ℤ_minus_less_thm	⊢ ∀ i j• ~ i < ~ j ⇔ j < i
ℤ_¬_less_thm	⊢ ∀ i j• ¬ i < j ⇔ j ≤ i
ℤ_¬_≤_thm	⊢ ∀ i j• ¬ i ≤ j ⇔ j < i
ℤ_≤_less_eq_thm	⊢ ∀ i j• i ≤ j ⇔ i < j ∨ i = j
ℤ_less_≤_trans_thm	⊢ ∀ i j k• i < j ∧ j ≤ k ⇒ i < k
ℤ_≤_less_trans_thm	⊢ ∀ i j k• i ≤ j ∧ j < k ⇒ i < k
ℤ_minus_ℕ_≤_thm	⊢ ∀ i m• i + ~ (ℕℤ m) ≤ i
ℤ_≤_plus_ℕ_thm	⊢ ∀ i m• i ≤ i + ℕℤ m
ℤ_∈_ℕ_thm	⊢ ∀ i• ℕℤ 0 ≤ i ⇔ (∃ m• i = ℕℤ m)
ℤ_less_clauses	⊢ ∀ i j k • (i + k < j + k ⇔ i < j) ∧ (k + i < j + k ⇔ i < j) ∧ (i + k < k + j ⇔ i < j) ∧ (k + i < k + j ⇔ i < j) ∧ (i + k < k ⇔ i < ℕℤ 0) ∧ (k + i < k ⇔ i < ℕℤ 0) ∧ (i < k + i ⇔ ℕℤ 0 < k) ∧ (i < i + k ⇔ ℕℤ 0 < k) ∧ ¬ i < i ∧ ℕℤ 0 < ℕℤ 1 ∧ ¬ ℕℤ 1 < ℕℤ 0
ℤ_ℕ_abs_thm	⊢ ∀ m• Abs (ℕℤ m) = ℕℤ m ∧ Abs (~ (ℕℤ m)) = ℕℤ m
ℤ_abs_thm	⊢ ∀ i• ℕℤ 0 ≤ i ⇒ Abs i = i ∧ Abs (~ i) = i
ℤ_abs_ℕ_thm	⊢ ∀ i• ℕℤ 0 ≤ Abs i
ℤ_abs_eq_0_thm	⊢ ∀ i• Abs i = ℕℤ 0 ⇔ i = ℕℤ 0
ℤ_abs_minus_thm	⊢ ∀ i• Abs (~ i) = Abs i
ℤ_ℕ_abs_minus_thm	⊢ ∀ i j • ℕℤ 0 ≤ i ∧ ℕℤ 0 ≤ j ∧ j ≤ i ⇒ Abs (i + ~ j) ≤ i
ℤ_abs_times_thm	⊢ ∀ i j• Abs (i * j) = Abs i * Abs j
ℤ_abs_plus_thm	⊢ ∀ i j• Abs (i + j) ≤ Abs i + Abs j
ℤ_div_mod_unique_lemma1	⊢ ∀ i j• ℕℤ 0 ≤ i ∧ ℕℤ 0 ≤ j ∧ i * j < j ⇒ i = ℕℤ 0
ℤ_div_mod_unique_lemma2	⊢ ∀ j d r • ¬ j = ℕℤ 0 ⇒ d * j + r = ℕℤ 0 ∧ ℕℤ 0 ≤ r ∧ r < Abs j ⇒ d = ℕℤ 0 ∧ r = ℕℤ 0
ℤ_div_mod_unique_lemma3	⊢ ∀ i j d r D R • ¬ j = ℕℤ 0 ⇒ D * j + R = d * j + r ∧ ℕℤ 0 ≤ r ∧ r ≤ R ∧ R < Abs j ⇒ D = d ∧ R = r
ℤ_div_mod_unique_thm	⊢ ∀ i j d r • ¬ j = ℕℤ 0 ⇒ (i = d * j + r ∧ ℕℤ 0 ≤ r ∧ r < Abs j ⇔ d = i Div j ∧ r = i Mod j)
ℤ_≤_induction_thm	⊢ ∀ j p • p j ∧ (∀ i• j ≤ i ∧ p i ⇒ p (i + ℕℤ 1)) ⇒ (∀ i• j ≤ i ⇒ p i)
ℤ_cov_induction_thm	⊢ ∀ j p • (∀ i• j ≤ i ∧ (∀ k• j ≤ k ∧ k < i ⇒ p k) ⇒ p i) ⇒ (∀ i• j ≤ i ⇒ p i)
ℤ_fun_∃_thm	⊢ ∀ f g z • (∀ x• g (f x) = x) ∧ (∀ y• f (g y) = y) ⇒ (∃₁ h • h (ℕℤ 0) = z ∧ (∀ i• h (i + ℕℤ 1) = f (h i)) ∧ (∀ i• h (i - ℕℤ 1) = g (h i)))

Created: