Package natural-exp-log-thm: Properties of natural number logarithm

Information

namenatural-exp-log-thm
version1.12
descriptionProperties of natural number logarithm
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2014-11-01
checksum9674a0608e9c3dee442680330f83d3db4a8e8aab
requiresbool
natural-add
natural-def
natural-div
natural-exp-def
natural-exp-log-def
natural-exp-thm
natural-mult
natural-numeral
natural-order
natural-thm
showData.Bool
Number.Natural

Files

Theorems

k. 1 < k log k 1 = 0

k m. 1 < k log k (k m) = m

k n. 1 < k ¬(n = 0) k log k n n

k m n. 1 < k k m n m log k n

k m. 1 < k log k (k (m + 1) - 1) = m

k n. 1 < k ¬(n = 0) (log k n = 0 n < k)

k n. 1 < k ¬(n = 0) n < k log k n = 0

k n. 1 < k ¬(n = 0) n < k (log k n + 1)

k n1 n2. 1 < k ¬(n1 = 0) n1 n2 log k n1 log k n2

k m n. 1 < k ¬(n = 0) n < k m log k n < m

k n.
    1 < k ¬(n = 0) log k n = if n < k then 0 else log k (n div k) + 1

k n m. 1 < k ¬(n = 0) (log k n = m k m n n < k (m + 1))

k n1 n2.
    1 < k ¬(n1 = 0) ¬(n2 = 0)
    log k (n1 * n2) log k n1 + (log k n2 + 1)

External Type Operators

External Constants

Assumptions

¬

bit0 0 = 0

t. t t

n. 0 n

n. n n

p. p

t. t ¬t

n. n < suc n

(¬) = λp. p

() = λp. p = λx.

t. ( t) t

t. (t ) t

t. t

t. t t

t. t t

t. t

t. t t

t. t t

t. t

n. ¬(suc n = 0)

n. 0 + n = n

t. (t ) ¬t

t. t ¬t

n. bit1 n = suc (bit0 n)

m. m 0 = 1

n. n 1 = n

m. 1 * m = m

m n. m m + n

() = λp q. p q p

m. suc m = m + 1

m. m 0 m = 0

n. suc n - 1 = n

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

n. 0 < n ¬(n = 0)

n. bit0 (suc n) = suc (suc (bit0 n))

m n. m * n = n * m

m n. m + n = n + m

m n. m < n m n

m n. ¬(m < n) n m

m n. ¬(m n) n < m

m n. m < suc n m n

m n. suc m n m < n

m. m = 0 n. m = suc n

() = λp q. (λf. f p q) = λf. f

() = λp. q. (x. p x q) q

t1 t2. ¬t1 ¬t2 t2 t1

m n. m + suc n = suc (m + n)

m n. suc m + n = suc (m + n)

m n. suc m suc n m n

m n. m * suc n = m + m * n

m n. m suc n = m * m n

m n. ¬(n = 0) m mod n < n

() = λp q. r. (p r) (q r) r

k n. 1 < k m. n k m

m n p. m + (n + p) = m + n + p

m n p. m + n < m + p n < p

m n p. m + n m + p n p

m n p. m < n n < p m < p

m n p. m < n n p m < p

m n p. m n n p m p

m n. m * n = 0 m = 0 n = 0

m n. ¬(n = 0) (m div n = 0 m < n)

m n. m n = 0 m = 0 ¬(n = 0)

m n p. m (n + p) = m n * m p

m n. ¬(n = 0) (m div n) * n + m mod n = m

m n p. m * n m * p m = 0 n p

m n p. m * p n * p m n p = 0

p. (n. p n) p ((minimal) p) m. m < (minimal) p ¬p m

m n p. m * n < m * p ¬(m = 0) n < p

m n p. m * p < n * p m < n ¬(p = 0)

k n m. k m n n < k (m + 1) log k n = m

x m n. x m x n if x = 0 then m = 0 n = 0 else x = 1 m n

x m n. x m < x n 2 x m < n x = 0 ¬(m = 0) n = 0