Theory "intExtension"

Signature

Definitions

SGN_def

⊢ ∀x. SGN x = if x = 0 then 0 else if x < 0 then -1 else 1

Theorems

INT_SGN_TOTAL

⊢ ∀a. SGN a = -1 ∨ SGN a = 0 ∨ SGN a = 1

INT_SGN_MUL2

⊢ ∀x y. SGN (x * y) = SGN x * SGN y

INT_SGN_MUL

⊢ ∀x1 x2 y1 y2. SGN x1 = y1 ⇒ SGN x2 = y2 ⇒ SGN (x1 * x2) = y1 * y2

INT_SGN_CLAUSES

⊢ ∀x. (SGN x = -1 ⇔ x < 0) ∧ (SGN x = 0 ⇔ x = 0) ∧ (SGN x = 1 ⇔ x > 0)

INT_NOT0_SGNNOT0

⊢ ∀x. x ≠ 0 ⇒ SGN x ≠ 0

INT_ABS_CALCULATE_POS

⊢ ∀a. 0 < a ⇒ ABS a = a

INT_ABS_CALCULATE_0

⊢ ABS 0 = 0

INT_ABS_CALCULATE_NEG

⊢ ∀a. a < 0 ⇒ ABS a = -a

INT_GT_RMUL_EXP

⊢ ∀a b n. 0 < n ⇒ (a > b ⇔ a * n > b * n)

INT_LT_RMUL_EXP

⊢ ∀a b n. 0 < n ⇒ (a < b ⇔ a * n < b * n)

INT_EQ_RMUL_EXP

⊢ ∀a b n. 0 < n ⇒ (a = b ⇔ a * n = b * n)

LESS_IMP_NOT_0

⊢ ∀n. 0 < n ⇒ n ≠ 0

ABS_EQ_MUL_SGN

⊢ ABS x = x * SGN x

MUL_ABS_SGN

⊢ ABS x * SGN x = x

INT_MUL_POS_SIGN

⊢ ∀a b. 0 < a ⇒ 0 < b ⇒ 0 < a * b

INT_NE_IMP_LTGT

⊢ ∀x. x ≠ 0 ⇔ 0 < x ∨ x < 0

INT_NOTGT_IMP_EQLT

⊢ ∀n. ¬(n < 0) ⇔ 0 = n ∨ 0 < n

INT_NO_ZERODIV

⊢ ∀x y. x = 0 ∨ y = 0 ⇔ x * y = 0

INT_NOTPOS0_NEG

⊢ ∀a. ¬(0 < a) ⇒ a ≠ 0 ⇒ 0 < -a

INT_NOT0_MUL

⊢ ∀a b. a ≠ 0 ⇒ b ≠ 0 ⇒ a * b ≠ 0

INT_GT0_IMP_NOT0

⊢ ∀a. 0 < a ⇒ a ≠ 0

INT_NOTLTEQ_GT

⊢ ∀a. ¬(a < 0) ⇒ a ≠ 0 ⇒ 0 < a

INT_ABS_NOT0POS

⊢ ∀x. x ≠ 0 ⇒ 0 < ABS x

INT_SGN_NOTPOSNEG

⊢ ∀x. SGN x ≠ -1 ⇒ SGN x ≠ 1 ⇒ SGN x = 0

INT_SGN_CASES

⊢ ∀a P. (SGN a = -1 ⇒ P) ∧ (SGN a = 0 ⇒ P) ∧ (SGN a = 1 ⇒ P) ⇒ P

INT_LT_ADD_NEG

⊢ ∀x y. x < 0 ∧ y < 0 ⇒ x + y < 0