Entry	Value
Package Name	natural-mult-thm
Count	33
Theorems	BOUNDS_DIVIDED : !p. (?b. !n. p n <= b) <=> (?a b. !n. n * p n <= a * n + b) BOUNDS_LINEAR : !a b c. (!n. a * n <= b * n + c) <=> a <= b BOUNDS_LINEAR_0 : !a b. (!n. a * n <= b) <=> a = 0 BOUNDS_NOTZERO : !p a b. p 0 0 = 0 /\ (!m n. p m n <= a * (m + n) + b) ==> (?c. !m n. p m n <= c * (m + n)) EQ_MULTL : !m n. m = m * n <=> m = 0 \/ n = 1 EQ_MULTR : !m n. m = n * m <=> m = 0 \/ n = 1 EQ_MULT_LCANCEL : !m n p. m * n = m * p <=> m = 0 \/ n = p EQ_MULT_RCANCEL : !m n p. m * p = n * p <=> m = n \/ p = 0 LEFT_ADD_DISTRIB : !m n p. m * (n + p) = m * n + m * p LEFT_SUB_DISTRIB : !m n p. p <= n ==> m * (n - p) = m * n - m * p LE_MULT2 : !m n p q. m <= n /\ p <= q ==> m * p <= n * q LE_MULT_LCANCEL : !m n p. m * n <= m * p <=> m = 0 \/ n <= p LE_MULT_RCANCEL : !m n p. m * p <= n * p <=> m <= n \/ p = 0 LE_SQUARE_REFL : !n. n <= n * n LT_LMULT : !m n p. ~(m = 0) /\ n < p ==> m * n < m * p LT_MULT : !m n. 0 < m * n <=> 0 < m /\ 0 < n LT_MULT2 : !m n p q. m < n /\ p < q ==> m * p < n * q LT_MULT_LCANCEL : !m n p. m * n < m * p <=> ~(m = 0) /\ n < p LT_MULT_RCANCEL : !m n p. m * p < n * p <=> m < n /\ ~(p = 0) MULTL_EQ : !m n. m * n = m <=> m = 0 \/ n = 1 MULTR_EQ : !m n. n * m = m <=> m = 0 \/ n = 1 MULT_0 : !m. m * 0 = 0 MULT_1 : !m. m * 1 = m MULT_2 : !n. 2 * n = n + n MULT_ASSOC : !m n p. m * n * p = (m * n) * p MULT_EQ_0 : !m n. m * n = 0 <=> m = 0 \/ n = 0 MULT_EQ_1 : !m n. m * n = 1 <=> m = 1 /\ n = 1 MULT_LASSOC : !m n p. m * n * p = n * m * p MULT_SUC : !m n. m * SUC n = m + m * n MULT_SYM : !m n. m * n = n * m ONE_MULT : !m. 1 * m = m RIGHT_ADD_DISTRIB : !m n p. (m + n) * p = m * p + n * p RIGHT_SUB_DISTRIB : !m n p. n <= m ==> (m - n) * p = m * p - n * p

Back to main package page