The Theory %int%
Parents
sets
Children
dyadic
Constants
Is_ℤ_Rep
(ℕ × ℕ) SET → BOOL
ℕℤ
ℕ → ℤ
$~Z
ℤ → ℤ
$+Z
ℤ → ℤ → ℤ
$-Z
ℤ → ℤ → ℤ
$*Z
ℤ → ℤ → ℤ
$≤Z
ℤ → ℤ → BOOL
$<Z
ℤ → ℤ → BOOL
$≥Z
ℤ → ℤ → BOOL
$>Z
ℤ → ℤ → BOOL
$AbsZ
ℤ → ℤ
$ModZ
ℤ → ℤ → ℤ
$DivZ
ℤ → ℤ → ℤ
Aliases
+
$+Z : ℤ → ℤ → ℤ
-
$-Z : ℤ → ℤ → ℤ
~
$~Z : ℤ → ℤ
*
$*Z : ℤ → ℤ → ℤ
$≤Z : ℤ → ℤ → BOOL
<
$<Z : ℤ → ℤ → BOOL
$≥Z : ℤ → ℤ → BOOL
>
$>Z : ℤ → ℤ → BOOL
Abs
$AbsZ : ℤ → ℤ
Div
$DivZ : ℤ → ℤ → ℤ
Mod
$ModZ : ℤ → ℤ → ℤ
Types
Fixity
Left Infix 305:
-Z
Left Infix 315:
DivZ ModZ
Right Infix 210:
<Z >Z Z Z
Right Infix 300:
+Z
Right Infix 310:
*Z
Prefix 350: AbsZ ~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
fill(λ (+Z', ~Z', $"ℕℤ'")
fill• (∀ i j k
fill• +Z' (+Z' i j) k = +Z' i (+Z' j k)
fill∧ +Z' i j = +Z' j i
fill∧ +Z' i (~Z' i) = $"ℕℤ'" 0
fill∧ +Z' i ($"ℕℤ'" 0) = i)
fill∧ (∀ m n
fill• +Z' ($"ℕℤ'" m) ($"ℕℤ'" n)
fill= $"ℕℤ'" (m + n))
fill∧ OneOne $"ℕℤ'"
fill∧ (∀ i
fill• ∃ m• i = $"ℕℤ'" m ∨ i = ~Z' ($"ℕℤ'" m)))
fill($+, ~, ℕℤ)
-Z
⊢ ∀ i j• i - j = i + ~ j
*Z
⊢ ConstSpec
fill(λ *Z'
fill• ∀ i j k
fill• *Z' i (j + k) = *Z' i j + *Z' i k
fill∧ *Z' i (ℕℤ 1) = i)
fill$*
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
AbsZ
⊢ ∀ i• Abs i = (if ℕℤ 0 ≤ i then i else ~ i)
DivZ
ModZ
⊢ ConstSpec
fill(λ (DivZ', ModZ')
fill• ∀ i j
fill• ¬ j = ℕℤ 0
fill⇒ i = DivZ' i j * j + ModZ' i j
fill∧ ℕℤ 0 ≤ ModZ' i j
fill∧ ModZ' i j < Abs j)
fill($Div, $Mod)
Theorems
is_ℤ_rep_consistent_thm
⊢ ∃ a• Is_ℤ_Rep a
+Z_consistent
~Z_consistent
ℕℤ_consistent
⊢ Consistent
fill(λ (+Z', ~Z', $"ℕℤ'")
fill• (∀ i j k
fill• +Z' (+Z' i j) k = +Z' i (+Z' j k)
fill∧ +Z' i j = +Z' j i
fill∧ +Z' i (~Z' i) = $"ℕℤ'" 0
fill∧ +Z' i ($"ℕℤ'" 0) = i)
fill∧ (∀ m n
fill• +Z' ($"ℕℤ'" m) ($"ℕℤ'" n)
fill= $"ℕℤ'" (m + n))
fill∧ OneOne $"ℕℤ'"
fill∧ (∀ i
fill• ∃ 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
fill• j + i = i + j
fill∧ (i + j) + k = i + j + k
fill∧ 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
fill• ~ (~ i) = i
fill∧ i + ~ i = ℕℤ 0
fill∧ ~ i + i = ℕℤ 0
fill∧ ~ (i + j) = ~ i + ~ j
fill∧ ~ (ℕℤ 0) = ℕℤ 0
ℤ_cases_thm1
⊢ ∀ i• ∃ m• i = ℕℤ m ∨ i = ~ (ℕℤ (m + 1))
ℤ_induction_thm
⊢ ∀ p
fill• p (ℕℤ 1)
fill∧ (∀ i• p i ⇒ p (~ i))
fill∧ (∀ i j• p i ∧ p j ⇒ p (i + j))
fill⇒ (∀ i• p i)
ℕℤ_one_one_thm
⊢ ∀ m n• ℕℤ m = ℕℤ n ⇔ m = n
ℤ_plus_clauses
⊢ ∀ i j k
fill• (i + k = j + k ⇔ i = j)
fill∧ (k + i = j + k ⇔ i = j)
fill∧ (i + k = k + j ⇔ i = j)
fill∧ (k + i = k + j ⇔ i = j)
fill∧ (i + k = k ⇔ i = ℕℤ 0)
fill∧ (k + i = k ⇔ i = ℕℤ 0)
fill∧ (k = k + j ⇔ j = ℕℤ 0)
fill∧ (k = j + k ⇔ j = ℕℤ 0)
fill∧ i + ℕℤ 0 = i
fill∧ ℕℤ 0 + i = i
fill∧ ¬ ℕℤ 1 = ℕℤ 0
fill∧ ¬ ℕℤ 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
fill• (i + k ≤ j + k ⇔ i ≤ j)
fill∧ (k + i ≤ j + k ⇔ i ≤ j)
fill∧ (i + k ≤ k + j ⇔ i ≤ j)
fill∧ (k + i ≤ k + j ⇔ i ≤ j)
fill∧ (i + k ≤ k ⇔ i ≤ ℕℤ 0)
fill∧ (k + i ≤ k ⇔ i ≤ ℕℤ 0)
fill∧ (k ≤ k + j ⇔ ℕℤ 0 ≤ j)
fill∧ (k ≤ j + k ⇔ ℕℤ 0 ≤ j)
fill∧ i ≤ i
fill∧ ¬ ℕℤ 1 ≤ ℕℤ 0
fill∧ ℕℤ 0 ≤ ℕℤ 1
ℕℤ_≤_thm
⊢ ∀ m n• ℕℤ m ≤ ℕℤ n ⇔ m ≤ n
*Z_consistent
⊢ Consistent
fill(λ *Z'
fill• ∀ i j k
fill• *Z' i (j + k) = *Z' i j + *Z' i k
fill∧ *Z' i (ℕℤ 1) = i)
ℕℤ_times_homomorphism_thm
⊢ ∀ m n• ℕℤ (m * n) = ℕℤ m * ℕℤ n
ℤ_times_minus_thm
⊢ ∀ i j
fill• ~ i * j = ~ (i * j)
fill∧ i * ~ j = ~ (i * j)
fill∧ ~ 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
DivZ_consistent
ModZ_consistent
⊢ Consistent
fill(λ (DivZ', ModZ')
fill• ∀ i j
fill• ¬ j = ℕℤ 0
fill⇒ i = DivZ' i j * j + ModZ' i j
fill∧ ℕℤ 0 ≤ ModZ' i j
fill∧ ModZ' i j < Abs j)
ℕℤ_plus_homomorphism_thm1
⊢ ∀ m n• ℕℤ m + ℕℤ n = ℕℤ (m + n)
ℤ_ℕ_induction_thm
⊢ ∀ p
fill• p (ℕℤ 0) ∧ (∀ i• ℕℤ 0 ≤ i ∧ p i ⇒ p (i + ℕℤ 1))
fill⇒ (∀ 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
fill• ~ (~ i) = i
fill∧ i + ~ i = ℕℤ 0
fill∧ ~ i + i = ℕℤ 0
fill∧ ~ (i + j) = ~ i + ~ j
fill∧ ~ (ℕℤ 0) = ℕℤ 0
ℤ_ℕ_cases_thm
⊢ ∀ i
fill• ℕℤ 0 ≤ i
fill⇒ 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
fill• j * i = i * j
fill∧ (i * j) * k = i * j * k
fill∧ 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
fill• i * (j + k) = i * j + i * k
fill∧ (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
fill• ℕℤ 0 * i = ℕℤ 0
fill∧ i * ℕℤ 0 = ℕℤ 0
fill∧ i * ℕℤ 1 = i
fill∧ ℕℤ 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
fill• (i + k < j + k ⇔ i < j)
fill∧ (k + i < j + k ⇔ i < j)
fill∧ (i + k < k + j ⇔ i < j)
fill∧ (k + i < k + j ⇔ i < j)
fill∧ (i + k < k ⇔ i < ℕℤ 0)
fill∧ (k + i < k ⇔ i < ℕℤ 0)
fill∧ (i < k + i ⇔ ℕℤ 0 < k)
fill∧ (i < i + k ⇔ ℕℤ 0 < k)
fill∧ ¬ i < i
fill∧ ℕℤ 0 < ℕℤ 1
fill∧ ¬ ℕℤ 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
fill• ℕℤ 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
fill• ¬ j = ℕℤ 0
fill⇒ d * j + r = ℕℤ 0 ∧ ℕℤ 0 ≤ r ∧ r < Abs j
fill⇒ d = ℕℤ 0 ∧ r = ℕℤ 0
ℤ_div_mod_unique_lemma3
⊢ ∀ i j d r D R
fill• ¬ j = ℕℤ 0
fill⇒ D * j + R = d * j + r
fill∧ ℕℤ 0 ≤ r
fill∧ r ≤ R
fill∧ R < Abs j
fill⇒ D = d ∧ R = r
ℤ_div_mod_unique_thm
⊢ ∀ i j d r
fill• ¬ j = ℕℤ 0
fill⇒ (i = d * j + r ∧ ℕℤ 0 ≤ r ∧ r < Abs j
fill⇔ d = i Div j ∧ r = i Mod j)
ℤ_≤_induction_thm
⊢ ∀ j p
fill• p j ∧ (∀ i• j ≤ i ∧ p i ⇒ p (i + ℕℤ 1))
fill⇒ (∀ i• j ≤ i ⇒ p i)
ℤ_cov_induction_thm
⊢ ∀ j p
fill• (∀ i• j ≤ i ∧ (∀ k• j ≤ k ∧ k < i ⇒ p k) ⇒ p i)
fill⇒ (∀ i• j ≤ i ⇒ p i)
ℤ_fun_∃_thm
⊢ ∀ f g z
fill• (∀ x• g (f x) = x) ∧ (∀ y• f (g y) = y)
fill⇒ (∃1 h
fill• h (ℕℤ 0) = z
fill∧ (∀ i• h (i + ℕℤ 1) = f (h i))
fill∧ (∀ i• h (i - ℕℤ 1) = g (h i)))

up quick index

privacy policy

Created:

V