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

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