Theory "int_arith"

Parents integer gcd

Signature

Constant	Type
bmarker	:bool -> bool

Definitions

bmarker_def

⊢ ∀b. bmarker b ⇔ b

Theorems

not_less

⊢ ¬(x < y) ⇔ y < x + 1

elim_eq

⊢ x = y ⇔ x < y + 1 ∧ y < x + 1

less_to_leq_samel

⊢ ∀x y. x < y ⇔ x ≤ y + -1

less_to_leq_samer

⊢ ∀x y. x < y ⇔ x + 1 ≤ y

lt_move_all_right

⊢ ∀x y. x < y ⇔ 0 < y + -x

lt_move_all_left

⊢ ∀x y. x < y ⇔ x + -y < 0

lt_move_left_left

⊢ ∀x y z. x < y + z ⇔ x + -y < z

lt_move_left_right

⊢ ∀x y z. x + y < z ⇔ y < z + -x

le_move_right_left

⊢ ∀x y z. x ≤ y + z ⇔ x + -z ≤ y

le_move_all_right

⊢ ∀x y. x ≤ y ⇔ 0 ≤ y + -x

eq_move_all_right

⊢ ∀x y. x = y ⇔ 0 = y + -x

eq_move_all_left

⊢ ∀x y. x = y ⇔ x + -y = 0

eq_move_left_left

⊢ ∀x y z. x = y + z ⇔ x + -y = z

eq_move_left_right

⊢ ∀x y z. x + y = z ⇔ y = z + -x

eq_move_right_left

⊢ ∀x y z. x = y + z ⇔ x + -z = y

lcm_eliminate

⊢ ∀P c. (∃x. P (c * x)) ⇔ ∃x. P x ∧ c int_divides x

lt_justify_multiplication

⊢ ∀n x y. 0 < n ⇒ (x < y ⇔ n * x < n * y)

eq_justify_multiplication

⊢ ∀n x y. 0 < n ⇒ (x = y ⇔ n * x = n * y)

justify_divides

⊢ ∀n x y. 0 < n ⇒ (x int_divides y ⇔ n * x int_divides n * y)

justify_divides2

⊢ ∀n c x y.
      n * x int_divides n * y + c ⇔
      n * x int_divides n * y + c ∧ n int_divides c

justify_divides3

⊢ ∀n x c. n int_divides n * x + c ⇔ n int_divides c

INT_SUB_SUB3

⊢ ∀x y z. x − (y − z) = x + z − y

move_sub

⊢ ∀c b a. a − c + b = a + b − c

can_get_small

⊢ ∀x y d. 0 < d ⇒ ∃c. 0 < c ∧ y − c * d < x

can_get_big

⊢ ∀x y d. 0 < d ⇒ ∃c. 0 < c ∧ x < y + c * d

positive_product_implication

⊢ ∀c d. 0 < c ∧ 0 < d ⇒ 0 < c * d

restricted_quantification_simp

⊢ ∀low high x.
      low < x ∧ x ≤ high ⇔ low < high ∧ (x = high ∨ low < x ∧ x ≤ high − 1)

top_and_lessers

⊢ ∀P d x0. (∀x. P x ⇒ P (x − d)) ∧ P x0 ⇒ ∀c. 0 < c ⇒ P (x0 − c * d)

bot_and_greaters

⊢ ∀P d x0. (∀x. P x ⇒ P (x + d)) ∧ P x0 ⇒ ∀c. 0 < c ⇒ P (x0 + c * d)

in_additive_range

⊢ ∀low d x. low < x ∧ x ≤ low + d ⇔ ∃j. x = low + j ∧ 0 < j ∧ j ≤ d

in_subtractive_range

⊢ ∀high d x. high − d ≤ x ∧ x < high ⇔ ∃j. x = high − j ∧ 0 < j ∧ j ≤ d

subtract_to_small

⊢ ∀x d. 0 < d ⇒ ∃k. 0 < x − k * d ∧ x − k * d ≤ d

add_to_great

⊢ ∀x d. 0 < d ⇒ ∃k. 0 < x + k * d ∧ x + k * d ≤ d

INT_LT_ADD_NUMERAL

⊢ ∀x y.
      x < x + &NUMERAL (BIT1 y) ∧ x < x + &NUMERAL (BIT2 y) ∧
      ¬(x < x + -&NUMERAL y)

INT_NUM_FORALL

⊢ (∀n. P (&n)) ⇔ ∀x. 0 ≤ x ⇒ P x

INT_NUM_EXISTS

⊢ (∃n. P (&n)) ⇔ ∃x. 0 ≤ x ∧ P x

INT_NUM_UEXISTS

⊢ (∃!n. P (&n)) ⇔ ∃!x. 0 ≤ x ∧ P x

INT_NUM_SUB

⊢ ∀n m. &(n − m) = if &n < &m then 0 else &n − &m

INT_NUM_COND

⊢ ∀b n m. &(if b then n else m) = if b then &n else &m

INT_NUM_ODD

⊢ ∀n. ODD n ⇔ ¬(2 int_divides &n)

INT_NUM_EVEN

⊢ ∀n. EVEN n ⇔ 2 int_divides &n

HO_SUB_ELIM

⊢ ∀P a b. P (&(a − b)) ⇔ &b ≤ &a ∧ P (&a + -&b) ∨ &a < &b ∧ P 0

CONJ_EQ_ELIM

⊢ ∀P v e. v = e ∧ P v ⇔ v = e ∧ P e

elim_neg_ones

⊢ ∀x. x + -1 + 1 = x

elim_minus_ones

⊢ ∀x. x + 1 − 1 = x

INT_NUM_DIVIDES

⊢ ∀n m. &n int_divides &m ⇔ divides n m

INT_LINEAR_GCD

⊢ ∀n m. ∃p q. p * &n + q * &m = &gcd n m

INT_DIVIDES_LRMUL

⊢ ∀p q r. q ≠ 0 ⇒ (p * q int_divides r * q ⇔ p int_divides r)

INT_DIVIDES_RELPRIME_MUL

⊢ ∀p q r. gcd p q = 1 ⇒ (&p int_divides &q * r ⇔ &p int_divides r)

gcdthm2

⊢ ∀m a x b d p q.
      d = gcd a m ∧ &d = p * &a + q * &m ∧ d ≠ 0 ∧ m ≠ 0 ∧ a ≠ 0 ⇒
      (&m int_divides &a * x + b ⇔
       &d int_divides b ∧ ∃t. x = -p * (b / &d) + t * (&m / &d))

gcd1thm

⊢ ∀m n p q. p * &m + q * &n = 1 ⇒ gcd m n = 1

gcd21_thm

⊢ ∀m a x b p q.
      p * &a + q * &m = 1 ∧ m ≠ 0 ∧ a ≠ 0 ⇒
      (&m int_divides &a * x + b ⇔ ∃t. x = -p * b + t * &m)

elim_lt_coeffs1

⊢ ∀n m x. m ≠ 0 ⇒ (&n < &m * x ⇔ &n / &m < x)

elim_lt_coeffs2

⊢ ∀n m x.
      m ≠ 0 ⇒
      (&m * x < &n ⇔ x < if &m int_divides &n then &n / &m else &n / &m + 1)

elim_le_coeffs

⊢ ∀m n x. 0 < m ⇒ (0 ≤ m * x + n ⇔ 0 ≤ x + n / m)

elim_eq_coeffs

⊢ ∀m x y. m ≠ 0 ⇒ (&m * x = y ⇔ &m int_divides y ∧ x = y / &m)

cooper_lemma_1

⊢ ∀m n a b u v p q x d.
      d = gcd (u * m) (a * n) ∧ &d = p * &u * &m + q * &a * &n ∧ m ≠ 0 ∧
      n ≠ 0 ∧ a ≠ 0 ∧ u ≠ 0 ⇒
      (&m int_divides &a * x + b ∧ &n int_divides &u * x + v ⇔
       &m * &n int_divides &d * x + v * &m * p + b * &n * q ∧
       &d int_divides &a * v − &u * b)

bmarker_rewrites

⊢ ∀p q r.
      (q ∧ bmarker p ⇔ bmarker p ∧ q) ∧
      (q ∧ bmarker p ∧ r ⇔ bmarker p ∧ q ∧ r) ∧
      ((bmarker p ∧ q) ∧ r ⇔ bmarker p ∧ q ∧ r)

NOT_INT_DIVIDES

⊢ ∀c d.
      c ≠ 0 ⇒
      (¬(c int_divides d) ⇔ ∃i. 1 ≤ i ∧ i ≤ ABS c − 1 ∧ c int_divides d + i)

NOT_INT_DIVIDES_POS

⊢ ∀n d.
      n ≠ 0 ⇒
      (¬(&n int_divides d) ⇔ ∃i. (1 ≤ i ∧ i ≤ &n − 1) ∧ &n int_divides d + i)

le_context_rwt1

⊢ 0 ≤ c + x ⇒ x ≤ y ⇒ (0 ≤ c + y ⇔ T)

le_context_rwt2

⊢ 0 ≤ c + x ⇒ y < -x ⇒ (0 ≤ -c + y ⇔ F)

le_context_rwt3

⊢ 0 ≤ c + x ⇒ x < y ⇒ (0 = c + y ⇔ F)

le_context_rwt4

⊢ 0 ≤ c + x ⇒ x < -y ⇒ (0 = -c + y ⇔ F)

le_context_rwt5

⊢ 0 ≤ c + x ⇒ (0 ≤ -c + -x ⇔ 0 = c + x)

eq_context_rwt1

⊢ 0 = c + x ⇒ (0 ≤ c + y ⇔ x ≤ y)

eq_context_rwt2

⊢ 0 = c + x ⇒ (0 ≤ -c + y ⇔ -x ≤ y)