The Theory %int%
 Parents
 sets
 Children
 Constants
 Is_ℤ_Rep (ℕ × ℕ) SET → BOOL ℕℤ ℕ → ℤ \$~Z ℤ → ℤ \$+Z ℤ → ℤ → ℤ \$-Z ℤ → ℤ → ℤ \$*Z ℤ → ℤ → ℤ \$≤Z ℤ → ℤ → BOOL \$Z ℤ → ℤ → BOOL \$AbsZ ℤ → ℤ \$ModZ ℤ → ℤ → ℤ \$DivZ ℤ → ℤ → ℤ
 Aliases
 + \$+Z : ℤ → ℤ → ℤ - \$-Z : ℤ → ℤ → ℤ ~ \$~Z : ℤ → ℤ * \$*Z : ℤ → ℤ → ℤ ≤ \$≤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 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 (λ (+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 ⇔ j < i AbsZ ⊢ ∀ i• Abs i = (if ℕℤ 0 ≤ i then i else ~ i) DivZ ModZ ⊢ ConstSpec (λ (DivZ', ModZ') • ∀ i j • ¬ j = ℕℤ 0 ⇒ i = DivZ' i j * j + ModZ' i j ∧ ℕℤ 0 ≤ ModZ' i j ∧ ModZ' 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 DivZ_consistent ModZ_consistent ⊢ Consistent (λ (DivZ', ModZ') • ∀ i j • ¬ j = ℕℤ 0 ⇒ i = DivZ' i j * j + ModZ' i j ∧ ℕℤ 0 ≤ ModZ' i j ∧ ModZ' 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) ⇒ (∃1 h • h (ℕℤ 0) = z ∧ (∀ i• h (i + ℕℤ 1) = f (h i)) ∧ (∀ i• h (i - ℕℤ 1) = g (h i)))

Created:

V