Theory prime

⊢ ∀n d.
    coprimes_by n d = if 0 < n ∧ d divides n then coprimes (n DIV d) else ∅

⊢ ∀n. divisors n = {d | 0 < d ∧ d ≤ n ∧ d divides n}

⊢ ∀n d. gcd_matches n d = {j | j ∈ natural n ∧ gcd j n = d}

⊢ halves =
  WFREC (@R. WF R ∧ ∀n. n ≠ 0 ⇒ R (HALF n) n)
    (λhalves a. I (if a = 0 then 0 else SUC (halves (HALF a))))

⊢ lcm_fun 0 = 1 ∧
  ∀n. lcm_fun (SUC n) =
      if n = 0 then 1
      else
        case some p. ∃k. 0 < k ∧ prime p ∧ SUC n = p ** k of
          NONE => lcm_fun n
        | SOME p => p * lcm_fun n

⊢ ∀m n. m multiples_upto n = {x | m divides x ∧ 0 < x ∧ x ≤ n}

⊢ ∀n m. n power_of m ⇔ ∃e. n = m ** e

⊢ ∀n. phi n = CARD (coprimes n)

⊢ ∀n. power_free n ⇔ ∀m e. n = m ** e ⇒ m = n ∧ e = 1

⊢ ∀n. power_free_test n ⇔ 1 < n ∧ n power_free_upto ulog n

⊢ ∀n k. n power_free_upto k ⇔ ∀j. 1 < j ∧ j ≤ k ⇒ ROOT j n ** j ≠ n

⊢ ∀n. prime_divisors n = {p | prime p ∧ p divides n}

⊢ ∀n. prime_factors n = {p | prime p ∧ p ∈ divisors n}

⊢ ∀n. prime_power_divisors n = IMAGE (λp. p ** ppidx n) (prime_divisors n)

⊢ ∀p n.
    0 < n ∧ prime p ⇒
    p ** ppidx n divides n ∧ coprime p (n DIV p ** ppidx n)

⊢ ∀n. prime_powers_upto n = IMAGE (λp. p ** LOG p n) (primes_upto n)

⊢ ∀n. prime_test n ⇔ if n ≤ 1 then F else factor_seek n (1 + SQRT n) 2 = n

⊢ ∀n. primes_upto n = {p | prime p ∧ p ≤ n}

⊢ rec_phi =
  WFREC
    (@R. WF R ∧ ∀n a. n ≠ 0 ∧ n ≠ 1 ∧ a ∈ {m | m < n ∧ m divides n} ⇒ R a n)
    (λrec_phi a'.
         I
           (if a' = 0 then 0
            else if a' = 1 then 1
            else a' − ∑ (λa. rec_phi a) {m | m < a' ∧ m divides a'}))

⊢ ∀n. square n ⇔ ∃k. n = SQ k

⊢ ∀n. square_free n ⇔ ∀p. prime p ∧ p divides n ⇒ ¬(SQ p divides n)

⊢ ∀n. ulog n = count_up n 1 0

⊢ ∀n. ∑ phi (divisors n) = n

⊢ ∀n. 1 < n ⇒ LOG2 n = 1 + LOG2 (HALF n)

⊢ ∀n m. 2 ** m < n ⇒ LOG2 (n DIV 2 ** m) = LOG2 n − m

⊢ ∀n. 1 < n ⇒ LOG2 (HALF n) = LOG2 n − 1

⊢ ∀n m. 1 < m ⇒ 0 < SUC (LOG2 n) * HALF m²

⊢ ∀n. LOG2 n = if n = 0 then LOG2 0 else halves n − 1

⊢ ∀b n.
    1 < b ∧ 0 < n ⇒
    LOG b (SUC n) = LOG b n + if SUC n power_of b then 1 else 0

⊢ ∀r n.
    0 < r ⇒
    ROOT r n =
    (let
       m = TWICE (ROOT r (n DIV 2 ** r))
     in
       m + if (m + 1) ** r ≤ n then 1 else 0)

⊢ ∀n m. SQRT n ≤ m ⇒ n ≤ 3 * m²

⊢ ∀n. SQRT n ≤ n

⊢ ∀n m. SQRT n * SQRT m ≤ SQRT (n * m)

⊢ ∀n. SQRT (SQ n) = n

⊢ ∀n. SQ (SQRT n) ≤ n

⊢ ∀n. (SQRT n)² ≤ n

⊢ ∀n. ¬square n ⇒ SQ (SQRT n) < n

⊢ ∀n. ¬square n ⇒ (SQRT n)² < n

⊢ ∀n. 0 < n ⇒ n = PROD_SET (IMAGE (λp. p ** ppidx n) (prime_divisors n))

⊢ ∀m n p.
    p ∈ common_prime_divisors m n ⇔
    p ∈ prime_divisors m ∧ p ∈ prime_divisors n

⊢ ∀m n. 0 < m ∧ 0 < n ⇒ FINITE (common_prime_divisors m n)

⊢ ∀m n x y.
    x ∈
    IMAGE (λp. p ** MIN (ppidx m) (ppidx n)) (common_prime_divisors m n) ∧
    y ∈
    IMAGE (λp. p ** MIN (ppidx m) (ppidx n)) (common_prime_divisors m n) ∧
    x ≠ y ⇒
    coprime x y

⊢ ∀m n x y.
    x ∈ common_prime_divisors m n ∧ y ∈ common_prime_divisors m n ∧ x ≠ y ⇒
    coprime x y

⊢ ∀d. coprimes_by 0 d = ∅

⊢ ∀n. coprimes_by n 0 = ∅

⊢ ∀n. 0 < n ⇒ coprimes_by n 1 = coprimes n

⊢ ∀n d. 0 < n ∧ d divides n ⇒ coprimes_by n d = coprimes (n DIV d)

⊢ ∀n. 0 < n ⇒ coprimes_by n n = {1}

⊢ ∀n x. x ∈ divisors n ⇒ (CARD ∘ coprimes_by n) x = (λd. phi (n DIV d)) x

⊢ ∀n d j.
    j ∈ coprimes_by n d ⇔ 0 < n ∧ d divides n ∧ j ∈ coprimes (n DIV d)

⊢ ∀n d. 0 < n ⇒ (coprimes_by n d = ∅ ⇔ ¬(d divides n))

⊢ ∀n d. FINITE (coprimes_by n d)

⊢ ∀n. 0 < n ⇒
      CARD ∘ coprimes_by n =
      (λd. phi (if d ∈ divisors n then n DIV d else 0))

⊢ ∀n. 1 < n ⇒ coprimes n = Euler n

⊢ INJ coprimes (𝕌(:num) DIFF {1}) 𝕌(:num -> bool)

⊢ ∀m n.
    coprime m n ⇒
    INJ (λ(x,y). if m * n = 1 then 1 else (x * n + y * m) MOD (m * n))
      (coprimes m × coprimes n) 𝕌(:num)

⊢ ∀m n.
    coprime m n ⇒
    coprimes (m * n) =
    IMAGE (λ(x,y). if m * n = 1 then 1 else (x * n + y * m) MOD (m * n))
      (coprimes m × coprimes n)

⊢ ∀n. prime n ⇒ coprimes n = residue n

⊢ ∀p n.
    prime p ⇒
    coprimes (p ** n) = natural (p ** n) DIFF p multiples_upto p ** n

⊢ ∀n. coprimes n = set (FILTER (λj. coprime j n) (GENLIST SUC n))

⊢ ∀n m k.
    count_up n m k =
    if m = 0 then 0 else if n ≤ m then k else count_up n (TWICE m) (SUC k)

⊢ ∀m n. m ≠ 0 ∧ n ≤ m ⇒ ∀k. count_up n m k = k

⊢ ∀m. m ≠ 0 ⇒
      ∀n t.
        2 ** t * m < TWICE n ∧ n ≤ 2 ** t * m ⇒ ∀k. count_up n m k = k + t

⊢ ∀P. (∀n m k. (m ≠ 0 ∧ ¬(n ≤ m) ⇒ P n (TWICE m) (SUC k)) ⇒ P n m k) ⇒
      ∀v v1 v2. P v v1 v2

⊢ ∀m n. m ≠ 0 ∧ m < n ⇒ ∀k. count_up n m k = count_up n (TWICE m) (SUC k)

⊢ ∀m. m ≠ 0 ⇒
      ∀n t.
        2 ** t * m < n ⇒
        ∀k. count_up n m k = count_up n (2 ** SUC t * m) (SUC k + t)

⊢ ∀n p. 0 < p ∧ p divides n ∧ SQRT n < p ⇒ n DIV p ≤ SQRT n

⊢ ∀n p. 0 < p ∧ p divides n ∧ p ≤ SQRT n ⇒ SQRT n ≤ n DIV p

⊢ ∀m n.
    0 < n ∧ m divides n ⇒
    m = PROD_SET (IMAGE (λp. p ** ppidx m) (prime_divisors n))

⊢ divisors 0 = ∅

⊢ divisors 1 = {1}

⊢ ∀n. CARD (divisors n) ≤ TWICE (SQRT n)

⊢ ∀n. INJ (λj. n DIV j) (divisors n) 𝕌(:num)

⊢ ∀n. divisors n DELETE n = {m | 0 < m ∧ m < n ∧ m divides n}

⊢ ∀n. (λd. n DIV d) PERMUTES divisors n

⊢ ∀n d. d ∈ divisors n ⇔ 0 < d ∧ d ≤ n ∧ d divides n

⊢ ∀n. 0 < n ⇒ ∀d. d ∈ divisors n ⇔ d divides n

⊢ ∀n. divisors n = ∅ ⇔ n = 0

⊢ ∀n. divisors n = IMAGE (gcd n) (natural n)

⊢ ∀n. divisors n = IMAGE (gcd n) (count n)

⊢ ∀n. divisors n = IMAGE (gcd n) (natural n)

⊢ ∀n. 0 < n ⇒ divisors n = IMAGE (gcd n) (upto n)

⊢ ∀n. divisors n =
      IMAGE (λj. if j + 1 divides n then j + 1 else 1) (count n)

⊢ ∀n. FINITE (divisors n)

⊢ ∀n. 0 < n ⇒ 1 ∈ divisors n

⊢ ∀n d. d ∈ divisors n ⇒ n DIV d ∈ divisors n

⊢ ∀n d. d ∈ divisors n ⇒ 0 < n

⊢ ∀n p q. 0 < n ∧ n = p * q ⇒ p ∈ divisors n ∧ q ∈ divisors n

⊢ ∀n. 0 < n ⇒ n ∈ divisors n

⊢ ∀n d. d ∈ divisors n ⇒ 0 < d

⊢ ∀n. 0 < n ⇒ divisors n ≠ ∅

⊢ ∀n. divisors n ⊆ natural n

⊢ ∀s n.
    n ∈ even_sq_free s ⇔
    n ∈ s ∧ square_free n ∧ EVEN (CARD (prime_factors n))

⊢ ∀s. FINITE s ⇒ FINITE (even_sq_free s)

⊢ ∀s. even_sq_free s ⊆ s

⊢ ∀m n. n ≤ 2 ** m ⇒ ulog n ≤ m

⊢ ∀n c q. 0 < n ⇒ factor_seek n c q ≤ n

⊢ ∀q n c.
    factor_seek n c q =
    if c ≤ q then n
    else if 1 < q ∧ n MOD q = 0 then q
    else factor_seek n c (q + 1)

⊢ ∀P. (∀n c q.
         (¬(c ≤ q) ∧ ¬(1 < q ∧ n MOD q = 0) ⇒ P n c (q + 1)) ⇒ P n c q) ⇒
      ∀v v1 v2. P v v1 v2

⊢ ∀n c q.
    1 < q ∧ q ≤ c ∧ c ≤ n ⇒
    (factor_seek n c q = n ⇔ ∀p. q ≤ p ∧ p < c ⇒ ¬(p divides n))

⊢ ∀n. partition (feq (gcd n)) (count n) =
      IMAGE (preimage (gcd n) (count n)) (divisors n)

⊢ ∀n d. preimage (gcd n) (natural n) d = gcd_matches n d

⊢ ∀n. preimage (gcd n) (natural n) = gcd_matches n

⊢ ∀n. feq (gcd n) equiv_on count n

⊢ ∀n. feq (gcd n) equiv_on natural n

⊢ ∀n. feq (gcd n) equiv_on upto n

⊢ ∀n. partition (feq (gcd n)) (natural n) =
      IMAGE (preimage (gcd n) (natural n)) (divisors n)

⊢ ∀n. partition (feq (gcd n)) (natural n) =
      IMAGE (gcd_matches n) (divisors n)

⊢ ∀n. 0 < n ⇒
      partition (feq (gcd n)) (upto n) =
      IMAGE (preimage (gcd n) (upto n)) (divisors n)

⊢ ∀d. gcd_matches 0 d = ∅

⊢ ∀d. gcd_matches 1 d = if d = 1 then {1} else ∅

⊢ ∀n d. gcd_matches n d = natural n ∩ {j | gcd j n = d}

⊢ ∀n. CARD ∘ gcd_matches n = CARD ∘ coprimes_by n

⊢ ∀n d.
    0 < n ∧ d divides n ⇒
    BIJ (λj. j DIV d) (gcd_matches n d) (coprimes (n DIV d))

⊢ ∀n d. d divides n ⇒ BIJ (λj. j DIV d) (gcd_matches n d) (coprimes_by n d)

⊢ ∀n d. d divides n ⇒ ∀j. j ∈ gcd_matches n d ⇒ j DIV d ∈ coprimes_by n d

⊢ ∀n d j. j ∈ gcd_matches n d ⇔ 0 < j ∧ j ≤ n ∧ gcd j n = d

⊢ ∀n d j. j ∈ gcd_matches n d ⇒ d divides j ∧ d divides n

⊢ ∀n d. 0 < n ⇒ (gcd_matches n d = ∅ ⇔ ¬(d divides n))

⊢ ∀n d. FINITE (gcd_matches n d)

⊢ ∀n. INJ (gcd_matches n) (divisors n) 𝕌(:num -> bool)

⊢ ∀n d. 0 < n ∧ d divides n ⇒ d ∈ gcd_matches n d

⊢ ∀n d. gcd_matches n d ⊆ natural n

⊢ ∀n. gcd_matches n 0 = ∅

⊢ ∀m n.
    0 < m ∧ 0 < n ⇒
    (let a = park m n; b = gcd m n DIV a in gcd m n = a * b ∧ coprime a b)

⊢ ∀m n.
    0 < m ∧ 0 < n ⇒
    (let
       a = park m n;
       b = gcd m n DIV a
     in
       b = PROD_SET (IMAGE (λp. p ** ppidx n) (park_off m n)) ∧
       gcd m n = a * b ∧ coprime a b)

⊢ ∀m n.
    0 < m ∧ 0 < n ⇒
    gcd m n =
    PROD_SET
      (IMAGE (λp. p ** MIN (ppidx m) (ppidx n)) (common_prime_divisors m n))

⊢ ∀a b p.
    0 < a ∧ 0 < b ∧ prime p ⇒
    coprime p (gcd (a DIV p ** ppidx a) (b DIV p ** ppidx b))

⊢ ∀a b p.
    0 < a ∧ 0 < b ∧ prime p ⇒
    ∀k. p ** k divides gcd a b ⇒ k ≤ MIN (ppidx a) (ppidx b)

⊢ ∀a b p.
    0 < a ∧ 0 < b ∧ prime p ⇒
    gcd a b =
    p ** MIN (ppidx a) (ppidx b) *
    gcd (a DIV p ** ppidx a) (b DIV p ** ppidx b)

⊢ ∀a b p.
    0 < a ∧ 0 < b ∧ prime p ⇒ p ** MIN (ppidx a) (ppidx b) divides gcd a b

⊢ ∀a b p.
    0 < a ∧ 0 < b ∧ prime p ⇒ ppidx (gcd a b) = MIN (ppidx a) (ppidx b)

⊢ halves 0 = 0

⊢ halves 1 = SUC (halves 0)

⊢ halves 2 = SUC (SUC (halves 0))

⊢ ∀n. halves n = if n = 0 then 0 else 1 + halves (HALF n)

⊢ ∀n. 0 < n ⇒ halves n = 1 + LOG2 n

⊢ ∀n. halves n = if n = 0 then 0 else SUC (halves (HALF n))

⊢ ∀n. halves n = 0 ⇔ n = 0

⊢ ∀n. halves n = 1 ⇔ n = 1

⊢ ∀P. (∀n. (n ≠ 0 ⇒ P (HALF n)) ⇒ P n) ⇒ ∀v. P v

⊢ MONO halves

⊢ ∀n. 0 < n ⇒ 0 < halves n

⊢ lcm_fun 0 = 1

⊢ lcm_fun 1 = 1

⊢ lcm_fun 2 = 2

⊢ ∀n. lcm_fun (SUC n) =
      if n = 0 then 1
      else
        case some p. ∃k. 0 < k ∧ prime p ∧ SUC n = p ** k of
          NONE => lcm_fun n
        | SOME p => p * lcm_fun n

⊢ lcm_fun 0 = 1 ∧
  (∀n. lcm_fun (NUMERAL (BIT1 n)) =
       if NUMERAL (BIT1 n) − 1 = 0 then 1
       else
         case some p. ∃k. 0 < k ∧ prime p ∧ NUMERAL (BIT1 n) = p ** k of
           NONE => lcm_fun (NUMERAL (BIT1 n) − 1)
         | SOME p => p * lcm_fun (NUMERAL (BIT1 n) − 1)) ∧
  ∀n. lcm_fun (NUMERAL (BIT2 n)) =
      if NUMERAL (BIT1 n) = 0 then 1
      else
        case some p. ∃k. 0 < k ∧ prime p ∧ NUMERAL (BIT2 n) = p ** k of
          NONE => lcm_fun (NUMERAL (BIT1 n))
        | SOME p => p * lcm_fun (NUMERAL (BIT1 n))

⊢ ∀n. 2 ** n ≤ lcm_fun (n + 1)

⊢ ∀n. 0 < n ⇒ 2 ** (n − 1) ≤ lcm_fun n

⊢ ∀n. ¬(∃p k. 0 < k ∧ prime p ∧ SUC n = p ** k) ⇒
      lcm_fun (SUC n) = lcm_fun n

⊢ ∀n p.
    prime p ∧ (∃k. 0 < k ∧ SUC n = p ** k) ⇒
    lcm_fun (SUC n) = p * lcm_fun n

⊢ ∀m n.
    0 < m ∧ 0 < n ⇒
    (let
       a = park m n;
       b = gcd m n DIV a;
       p = m DIV a;
       q = a * n DIV gcd m n
     in
       lcm m n = p * q ∧ coprime p q ∧ gcd m n = a * b ∧ m = a * p ∧
       n = b * q)

⊢ ∀m n.
    0 < m ∧ 0 < n ⇒
    (let
       a = park m n;
       p = m DIV a;
       q = a * n DIV gcd m n
     in
       lcm m n = p * q ∧ coprime p q)

⊢ ∀m n.
    0 < m ∧ 0 < n ⇒
    (let
       a = park m n;
       b = gcd m n DIV a;
       p = m DIV a;
       q = a * n DIV gcd m n
     in
       b = PROD_SET (IMAGE (λp. p ** ppidx n) (park_off m n)) ∧
       p =
       PROD_SET
         (IMAGE (λp. p ** ppidx m) (prime_divisors m DIFF park_on m n)) ∧
       q =
       PROD_SET
         (IMAGE (λp. p ** ppidx n) (prime_divisors n DIFF park_off m n)) ∧
       lcm m n = p * q ∧ coprime p q ∧ gcd m n = a * b ∧ m = a * p ∧
       n = b * q)

⊢ ∀m n.
    0 < m ∧ 0 < n ⇒
    lcm m n =
    PROD_SET
      (IMAGE (λp. p ** MAX (ppidx m) (ppidx n)) (total_prime_divisors m n))

⊢ ∀a b p.
    0 < a ∧ 0 < b ∧ prime p ⇒
    coprime p (lcm (a DIV p ** ppidx a) (b DIV p ** ppidx b))

⊢ ∀a b p.
    0 < a ∧ 0 < b ∧ prime p ⇒
    ∀k. p ** k divides lcm a b ⇒ k ≤ MAX (ppidx a) (ppidx b)

⊢ ∀a b p.
    0 < a ∧ 0 < b ∧ prime p ⇒
    lcm a b =
    p ** MAX (ppidx a) (ppidx b) *
    lcm (a DIV p ** ppidx a) (b DIV p ** ppidx b)

⊢ ∀a b p.
    0 < a ∧ 0 < b ∧ prime p ⇒ p ** MAX (ppidx a) (ppidx b) divides lcm a b

⊢ ∀a b p.
    0 < a ∧ 0 < b ∧ prime p ⇒ ppidx (lcm a b) = MAX (ppidx a) (ppidx b)

⊢ ∀n. lcm_run n = PROD_SET (prime_powers_upto n)

⊢ ∀n. lcm_run n = set_lcm (prime_powers_upto n)

⊢ ∀n. SQRT (n ** primes_count n) ≤ lcm_run n

⊢ ∀n. PROD_SET (primes_upto n) ≤ lcm_run n

⊢ ∀n. lcm_run n ≤ n ** primes_count n

⊢ ∀n a b.
    n = a * b ∧ coprime a b ⇒ ∀m. a divides m ∧ b divides m ⇒ lcm n m = m

⊢ ∀p. prime p ⇒ ∀m n. n = p ** SUC (ppidx m) ⇒ lcm n m = p * m

⊢ less_divisors 0 = ∅

⊢ less_divisors 1 = ∅

⊢ ∀n x. x ∈ less_divisors n ⇔ 0 < x ∧ x < n ∧ x divides n

⊢ ∀n. FINITE (less_divisors n)

⊢ ∀n. 1 < n ⇒ 1 ∈ less_divisors n

⊢ ∀n d. 1 < d ∧ d ∈ less_divisors n ⇒ n DIV d ∈ less_divisors n

⊢ ∀n. MAX_SET (less_divisors n) ≤ HALF n

⊢ ∀n. 1 < n ⇒ MIN_SET (less_divisors n) = 1

⊢ ∀n x. x ∈ less_divisors n ⇒ 0 < x

⊢ ∀n. prime n ⇒ less_divisors n = {1}

⊢ ∀n. less_divisors n ⊆ divisors n

⊢ ∀n. less_divisors n ⊆ natural (HALF n)

⊢ ∀n. ¬SING (prime_divisors (n + 1)) ⇒ lcm_run (n + 1) = lcm_run n

⊢ ∀n. SING (prime_divisors (n + 1)) ⇒
      lcm_run (n + 1) = CHOICE (prime_divisors (n + 1)) * lcm_run n

⊢ ∀n. lcm_run (n + 1) = lcm_fun (n + 1)

⊢ ∀n. (∀p. prime_divisors (n + 1) ≠ {p}) ⇒ lcm_run (n + 1) = lcm_run n

⊢ ∀n p. prime_divisors (n + 1) = {p} ⇒ lcm_run (n + 1) = p * lcm_run n

⊢ ∀n. lcm_run (n + 1) =
      case some p. prime_divisors (n + 1) = {p} of
        NONE => lcm_run n
      | SOME p => p * lcm_run n

⊢ ∀l p.
    prime p ∧ POSITIVE l ⇒
    ∀k. p ** k divides list_lcm l ⇒ k ≤ MAX_LIST (MAP ppidx l)

⊢ ∀l p. prime p ⇒ p ** MAX_LIST (MAP ppidx l) divides list_lcm l

⊢ ∀l p.
    prime p ∧ l ≠ [] ∧ POSITIVE l ⇒
    ∀k. p ** k divides list_lcm l ⇒ ∃x. MEM x l ∧ p ** k divides x

⊢ ∀l p. prime p ∧ POSITIVE l ⇒ ppidx (list_lcm l) = MAX_LIST (MAP ppidx l)

⊢ ∀l p.
    prime p ∧ l ≠ [] ∧ POSITIVE l ⇒
    ∀x. MEM x l ⇒ ppidx x ≤ ppidx (list_lcm l)

⊢ ∀n. lcm_run (n + 1) =
      (let
         s = prime_divisors (n + 1)
       in
         if SING s then CHOICE s * lcm_run n else lcm_run n)

⊢ ∀n. (∀p k. k = 0 ∨ ¬prime p ∨ n + 2 ≠ p ** k) ⇒
      lcm_run (n + 2) = lcm_run (n + 1)

⊢ ∀n p k. prime p ∧ n + 2 = p ** k ⇒ lcm_run (n + 2) = p * lcm_run (n + 1)

⊢ ∀n. 0 multiples_upto n = ∅

⊢ ∀n. 1 multiples_upto n = natural n

⊢ ∀m n. m multiples_upto n = {x | ∃k. x = k * m ∧ 0 < x ∧ x ≤ n}

⊢ ∀m n. CARD (m multiples_upto n) = if m = 0 then 0 else n DIV m

⊢ ∀m n x. x ∈ m multiples_upto n ⇔ m divides x ∧ 0 < x ∧ x ≤ n

⊢ ∀m n x. x ∈ m multiples_upto n ⇔ ∃k. x = k * m ∧ 0 < x ∧ x ≤ n

⊢ ∀m n. m multiples_upto n = {x | m divides x ∧ x ∈ natural n}

⊢ ∀m n. FINITE (m multiples_upto n)

⊢ ∀m. m multiples_upto 0 = ∅

⊢ ∀m. m multiples_upto 1 = if m = 1 then {1} else ∅

⊢ ∀m n. m multiples_upto n ⊆ natural n

⊢ ∀m n.
    m multiples_upto n =
    if m = 0 then ∅ else IMAGE ($* m) (natural (n DIV m))

⊢ ∀n. 1 < n ∧ ¬(∃p k. 0 < k ∧ prime p ∧ n = p ** k) ⇒
      ∃a b. n = a * b ∧ coprime a b ∧ 1 < a ∧ a < n ∧ 1 < b ∧ b < n

⊢ ∀s n. n ∈ non_sq_free s ⇔ n ∈ s ∧ ¬square_free n

⊢ ∀s. FINITE s ⇒ FINITE (non_sq_free s)

⊢ ∀s. non_sq_free s ⊆ s

⊢ ∀s n.
    n ∈ odd_sq_free s ⇔
    n ∈ s ∧ square_free n ∧ ODD (CARD (prime_factors n))

⊢ ∀s. FINITE s ⇒ FINITE (odd_sq_free s)

⊢ ∀s. odd_sq_free s ⊆ s

⊢ ∀n m. ¬square n ⇒ ((TWICE m + 1)² < n ⇔ m < HALF (1 + SQRT n))

⊢ ∀s f. s ⊆ prime ⇒ PAIRWISE_COPRIME (IMAGE (λp. p ** f p) s)

⊢ ∀m n. park_off m n = common_prime_divisors m n DIFF park_on m n

⊢ ∀m n p.
    p ∈ park_off m n ⇔
    p ∈ prime_divisors m ∧ p ∈ prime_divisors n ∧ ppidx n < ppidx m

⊢ ∀m n. 1 ∉ IMAGE (λp. p ** ppidx m) (park_off m n)

⊢ ∀m n. park_off m n ⊆ common_prime_divisors m n

⊢ ∀m n. park_off m n ⊆ total_prime_divisors m n

⊢ ∀m n p.
    p ∈ park_on m n ⇔
    p ∈ prime_divisors m ∧ p ∈ prime_divisors n ∧ ppidx m ≤ ppidx n

⊢ ∀m n.
    (let
       s =
         IMAGE (λp. p ** MIN (ppidx m) (ppidx n))
           (common_prime_divisors m n);
       u = IMAGE (λp. p ** ppidx m) (park_on m n);
       v = IMAGE (λp. p ** ppidx n) (park_off m n)
     in
       0 < m ⇒ s =|= u # v)

⊢ ∀m n. common_prime_divisors m n =|= park_on m n # park_off m n

⊢ ∀m n.
    (let
       s =
         IMAGE (λp. p ** MAX (ppidx m) (ppidx n))
           (total_prime_divisors m n);
       u = IMAGE (λp. p ** ppidx m) (prime_divisors m DIFF park_on m n);
       v = IMAGE (λp. p ** ppidx n) (prime_divisors n DIFF park_off m n)
     in
       0 < m ∧ 0 < n ⇒ s =|= u # v)

⊢ ∀m n. park_on m n ⊆ common_prime_divisors m n

⊢ ∀m n. park_on m n ⊆ total_prime_divisors m n

⊢ ∀m. 0 power_of m ⇔ m = 0

⊢ ∀m. 1 power_of m

⊢ ∀n. n power_of 2 ⇒ (ODD n ⇔ n = 1)

⊢ ∀n. 0 < n ⇒ ∀m. n power_of m ⇔ ∃k. k ≤ LOG2 n ∧ n = m ** k

⊢ ∀n. 0 < n ⇒ ∀m. n power_of m ⇔ ∃k. k ≤ ulog n ∧ n = m ** k

⊢ ∀n p. 0 < p ∧ p divides n ⇒ (n power_of p ⇔ n DIV p power_of p)

⊢ ∀n p. 0 < n ∧ p divides n ⇒ (n power_of p ⇔ n DIV p power_of p)

⊢ ∀p q. prime p ∧ (∃x y. 0 < x ∧ p ** x = q ** y) ⇒ q power_of p

⊢ ∀p n. 1 < p ∧ 0 < n ⇒ TWICE (p ** HALF n) ≤ p ** n

⊢ ∀p n.
    1 < p ∧ 0 < n ⇒
    (p ** HALF n − 2) * p ** HALF n ≤ p ** n − TWICE (p ** HALF n)

⊢ ∀n m. 0 < m ∧ 1 < n ∧ n MOD m = 0 ⇒ (n power_of m ⇔ n DIV m power_of m)

⊢ ∀n m. 0 < m ∧ 1 < n ∧ n MOD m ≠ 0 ⇒ ¬(n power_of m)

⊢ ∀n. n power_of 0 ⇔ n = 0 ∨ n = 1

⊢ ∀n. n power_of 1 ⇔ n = 1

⊢ ∀m n. 1 < m ∧ 1 < n ∧ n power_of m ⇒ ¬(SUC n power_of m)

⊢ ∀n. n power_of n

⊢ ∀p. 1 < p ⇒ ∀n. p * tops p n < (p − 1) * TWICE (p ** n)

⊢ ∀m n. 1 < m ∧ n power_of m ∧ SUC n power_of m ⇒ m = 2 ∧ n = 1

⊢ ∀n m.
    n power_of m ⇔
    if n = 0 then m = 0
    else if n = 1 then T
    else if m = 0 then n ≤ 1
    else if m = 1 then n = 1
    else if n MOD m = 0 then n DIV m power_of m
    else F

⊢ phi 0 = 0

⊢ phi 1 = 1

⊢ phi 2 = 1

⊢ ∀n. phi n = 0 ⇔ n = 0

⊢ ∀n. 1 < n ⇒ phi n = totient n

⊢ phi = CARD ∘ coprimes

⊢ ∀n. 2 < n ⇒ 1 < phi n

⊢ ∀n. phi n ≤ n

⊢ ∀n. 1 < n ⇒ phi n < n

⊢ ∀m n. coprime m n ⇒ phi (m * n) = phi m * phi n

⊢ ∀n. 0 < n ⇒ 0 < phi n

⊢ ∀n. prime n ⇒ phi n = n − 1

⊢ ∀p n. prime p ⇒ phi (p ** SUC n) = (p − 1) * p ** n

⊢ ∀p. prime p ⇒ phi (SQ p) = p * (p − 1)

⊢ ∀p q.
    prime p ∧ prime q ⇒
    phi (p * q) = if p = q then p * (p − 1) else (p − 1) * (q − 1)

⊢ ∀p q. prime p ∧ prime q ∧ p ≠ q ⇒ phi (p * q) = (p − 1) * (q − 1)

⊢ ∀n. phi n = LENGTH (FILTER (λj. coprime j n) (GENLIST SUC n))

⊢ power_free 0 ⇔ F

⊢ power_free 1 ⇔ F

⊢ power_free 2

⊢ power_free 3

⊢ power_free n ⇔ 1 < n ∧ ∀m. n power_of m ⇒ n = m

⊢ ∀n. power_free n ⇔ 1 < n ∧ power_index n (LOG2 n) = 1

⊢ ∀n. power_free n ⇔ 1 < n ∧ power_index n (ulog n) = 1

⊢ ∀n. power_free n ⇔ 1 < n ∧ ∀j. 1 < j ⇒ ROOT j n ** j ≠ n

⊢ ∀n b. LOG2 n ≤ b ⇒ (power_free n ⇔ 1 < n ∧ n power_free_upto b)

⊢ ∀n. power_free n ⇔ 1 < n ∧ n power_free_upto LOG2 n

⊢ ∀n. power_free n ⇔ 1 < n ∧ n power_free_upto ulog n

⊢ ∀n. power_free n ⇒ 1 < n

⊢ ∀m n. power_free n ∧ n power_of m ⇒ n = m

⊢ ∀n. power_free n ⇒ ∀j. 1 < j ⇒ ROOT j n ** j ≠ n

⊢ ∀n. power_free_test n ⇔ power_free n

⊢ ∀n. power_free n ⇔ 1 < n ∧ ∀j. 1 < j ∧ j ≤ LOG2 n ⇒ ROOT j n ** j ≠ n

⊢ ∀n. power_free n ⇔ 1 < n ∧ ∀j. 1 < j ∧ j ≤ ulog n ⇒ ROOT j n ** j ≠ n

⊢ ∀n. n power_free_upto 0 ⇔ T

⊢ ∀n. n power_free_upto 1 ⇔ T

⊢ ∀n k.
    0 < k ∧ n power_free_upto k ⇒
    (n power_free_upto k + 1 ⇔ ROOT (k + 1) n ** (k + 1) ≠ n)

⊢ ∀n. power_index n 0 = 1

⊢ ∀n. power_index n 1 = 1

⊢ ∀n k.
    power_index n k =
    if k ≤ 1 then 1
    else if ROOT k n ** k = n then k
    else power_index n (k − 1)

⊢ ∀n k. ROOT (power_index n k) n ** power_index n k = n

⊢ ∀m n k.
    0 < k ∧ k ≤ m ⇒
    (power_index n m = power_index n k ⇔
     ∀j. k < j ∧ j ≤ m ⇒ ROOT j n ** j ≠ n)

⊢ ∀n k. 0 < k ∧ ROOT k n ** k = n ⇒ power_index n k = k

⊢ ∀P. (∀n k. (¬(k ≤ 1) ∧ ROOT k n ** k ≠ n ⇒ P n (k − 1)) ⇒ P n k) ⇒
      ∀v v1. P v v1

⊢ ∀m n k. k ≤ m ∧ ROOT k n ** k = n ⇒ k ≤ power_index n m

⊢ ∀m n k.
    k ≤ m ∧ (∀j. k < j ∧ j ≤ m ⇒ ROOT j n ** j ≠ n) ⇒
    power_index n m = power_index n k

⊢ ∀n k. ROOT k n ** k ≠ n ⇒ power_index n k = power_index n (k − 1)

⊢ ∀k. power_index 1 k = if k = 0 then 1 else k

⊢ ∀n k. 0 < power_index n k

⊢ ∀m n k. power_index n m = k ⇒ ∀j. k < j ∧ j ≤ m ⇒ ROOT j n ** j ≠ n

⊢ ∀n k. n power_of ROOT (power_index n k) n

⊢ ∀n k. 0 < k ⇒ power_index n k ≤ k

⊢ ∀p. prime p ⇔ 1 < p ∧ ∀q. 1 < q ∧ q ≤ SQRT p ⇒ ¬(q divides p)

⊢ prime_divisors 0 = {p | prime p}

⊢ ¬SING (prime_divisors 0)

⊢ prime_divisors 1 = ∅

⊢ ∀n m x.
    x divides m ∧ x divides n ⇒
    prime_divisors x ⊆ common_prime_divisors m n

⊢ ∀n m x.
    m divides x ∧ n divides x ⇒ total_prime_divisors m n ⊆ prime_divisors x

⊢ ∀m n. m divides n ⇒ prime_divisors m ⊆ prime_divisors n

⊢ ∀n p. p ∈ prime_divisors n ⇔ prime p ∧ p divides n

⊢ ∀n. prime_divisors n = ∅ ⇔ n = 1

⊢ ∀n. 0 < n ⇒ FINITE (prime_divisors n)

⊢ ∀n. 1 < n ⇒ prime_divisors n ≠ ∅

⊢ ∀n. prime n ⇒ prime_divisors n = {n}

⊢ ∀n. prime n ⇒ ∀k. 0 < k ⇒ prime_divisors (n ** k) = {n}

⊢ ∀n. SING (prime_divisors n) ⇔ ∃p k. prime p ∧ 0 < k ∧ n = p ** k

⊢ ∀n p. prime_divisors n = {p} ⇔ ∃k. prime p ∧ 0 < k ∧ n = p ** k

⊢ ∀n. SING (prime_divisors n) ⇒
      (let p = CHOICE (prime_divisors n) in prime p ∧ n = p ** ppidx n)

⊢ ∀n. 0 < n ⇒ prime_divisors n ⊆ natural n

⊢ ∀n. prime_divisors n ⊆ prime

⊢ ∀n. 1 < n ⇒ (¬prime n ⇔ ∃p. prime p ∧ p divides n ∧ p ≤ SQRT n)

⊢ ∀n. 0 < n ⇒ n = PROD_SET (prime_power_divisors n)

⊢ ∀n p. p ∈ prime_factors n ⇔ prime p ∧ p ≤ n ∧ p divides n

⊢ ∀n. FINITE (prime_factors n)

⊢ ∀n. prime_factors n ⊆ divisors n

⊢ ∀n. prime n ⇒ power_free n

⊢ ∀p. prime p ⇒ ¬square p

⊢ ∀n p. 0 < n ∧ prime p ⇒ coprime p (n DIV p ** ppidx n)

⊢ ∀n p. 0 < n ∧ prime p ⇒ ∀k. p ** k divides n ⇔ k ≤ ppidx n

⊢ prime_power_divisors 1 = ∅

⊢ ∀n x.
    x ∈ prime_power_divisors n ⇔
    ∃p. x = p ** ppidx n ∧ prime p ∧ p divides n

⊢ ∀p n. prime p ∧ p divides n ⇒ p ** ppidx n ∈ prime_power_divisors n

⊢ ∀n. 0 < n ⇒ FINITE (prime_power_divisors n)

⊢ ∀n x y.
    x ∈ prime_power_divisors n ∧ y ∈ prime_power_divisors n ∧ x ≠ y ⇒
    coprime x y

⊢ ∀n p. 0 < n ∧ prime p ⇒ n = p ** ppidx n * (n DIV p ** ppidx n)

⊢ ∀n p. prime p ⇒ p ** ppidx n divides n

⊢ ∀p. prime p ⇒ ppidx 1 = 0

⊢ ∀n m x.
    0 < m ∧ 0 < n ∧ x divides m ∧ x divides n ⇒
    ∀p. prime p ⇒ ppidx x ≤ MIN (ppidx m) (ppidx n)

⊢ ∀n m x.
    0 < x ∧ m divides x ∧ n divides x ⇒
    ∀p. prime p ⇒ MAX (ppidx m) (ppidx n) ≤ ppidx x

⊢ ∀n p. 0 < n ∧ prime p ∧ ¬(p divides n) ⇒ ppidx n = 0

⊢ ∀n p.
    0 < n ∧ prime p ⇒
    (let q = n DIV p ** ppidx n in n = p ** ppidx n * q ∧ coprime p q)

⊢ ∀n p. 0 < n ∧ prime p ⇒ ∃m. p ** m divides n ∧ coprime p (n DIV p ** m)

⊢ ∀n p. 0 < n ∧ prime p ⇒ ppidx n ≤ LOG p n

⊢ ∀n p. 0 < n ∧ prime p ⇒ ∀k. k > ppidx n ⇒ ¬(p ** k divides n)

⊢ ∀m n. 0 < n ∧ m divides n ⇒ ∀p. prime p ⇒ ppidx m ≤ ppidx n

⊢ ∀n p. 0 < n ∧ prime p ∧ p divides n ⇒ 0 < ppidx n

⊢ ∀p. prime p ⇒ ppidx p = 1

⊢ ∀p. prime p ⇒ ∀k. ppidx (p ** k) = k

⊢ ∀n p.
    0 < n ∧ prime p ∧ n + 1 = p ** ppidx (n + 1) ⇒
    ppidx (n + 1) = 1 + ppidx (lcm_run n)

⊢ ∀n p.
    0 < n ∧ prime p ∧ SUC n = p ** ppidx (SUC n) ⇒
    ppidx (SUC n) = SUC (ppidx (lcm_run n))

⊢ ∀n p.
    0 < n ∧ prime p ⇒ ∀k. k = ppidx n ⇔ ∃q. n = p ** k * q ∧ coprime p q

⊢ ∀n. 1 < n ⇒
      (∃p k. 0 < k ∧ prime p ∧ n = p ** k) ∨
      ∃a b. n = a * b ∧ coprime a b ∧ 1 < a ∧ 1 < b ∧ a < n ∧ b < n

⊢ prime_powers_upto 0 = ∅

⊢ prime_powers_upto 1 = ∅

⊢ ∀n x. x ∈ prime_powers_upto n ⇔ ∃p. x = p ** LOG p n ∧ prime p ∧ p ≤ n

⊢ ∀p n. prime p ∧ p ≤ n ⇒ p ** LOG p n ∈ prime_powers_upto n

⊢ ∀n. FINITE (prime_powers_upto n)

⊢ ∀n x. 0 < x ∧ x ≤ n ⇒ x divides set_lcm (prime_powers_upto n)

⊢ ∀n p. prime p ∧ p ≤ n ⇒ p divides set_lcm (prime_powers_upto n)

⊢ ∀n p.
    prime p ∧ p ≤ n ⇒ p ** LOG p n divides set_lcm (prime_powers_upto n)

⊢ ∀n p.
    prime p ∧ p ≤ n ⇒ p ** ppidx n divides set_lcm (prime_powers_upto n)

⊢ ∀n x.
    MEM x (SET_TO_LIST (prime_powers_upto n)) ⇔
    ∃p. x = p ** LOG p n ∧ prime p ∧ p ≤ n

⊢ ∀n x y.
    x ∈ prime_powers_upto n ∧ y ∈ prime_powers_upto n ∧ x ≠ y ⇒ coprime x y

⊢ ∀n. PROD_SET (primes_upto n) ≤ PROD_SET (prime_powers_upto n)

⊢ ∀n. PROD_SET (prime_powers_upto n) ≤ n ** primes_count n

⊢ ∀n. n ** primes_count n ≤
      PROD_SET (primes_upto n) * PROD_SET (prime_powers_upto n)

⊢ ∀n. prime n ⇔ prime_test n

⊢ primes_count 0 = 0

⊢ primes_count 1 = 0

⊢ ∀n. n ** primes_count n ≤ (lcm_run n)²

⊢ ∀n. n ** primes_count n ≤ PROD_SET (primes_upto n) * lcm_run n

⊢ primes_upto 0 = ∅

⊢ primes_upto 1 = ∅

⊢ ∀n p. p ∈ primes_upto n ⇔ prime p ∧ p ≤ n

⊢ ∀n. FINITE (primes_upto n)

⊢ ∀n x y. x ∈ primes_upto n ∧ y ∈ primes_upto n ∧ x ≠ y ⇒ coprime x y

⊢ ∀n. primes_upto n ⊆ natural n

⊢ proper_divisors 0 = ∅

⊢ proper_divisors 1 = ∅

⊢ ∀n. proper_divisors n = less_divisors n DELETE 1

⊢ ∀n x. x ∈ proper_divisors n ⇔ 1 < x ∧ x < n ∧ x divides n

⊢ ∀n. FINITE (proper_divisors n)

⊢ ∀n d. d ∈ proper_divisors n ⇒ n DIV d ∈ proper_divisors n

⊢ ∀n. proper_divisors n ≠ ∅ ⇒
      MAX_SET (proper_divisors n) = n DIV MIN_SET (proper_divisors n) ∧
      MIN_SET (proper_divisors n) = n DIV MAX_SET (proper_divisors n)

⊢ ∀n. proper_divisors n ≠ ∅ ⇒ 1 < MIN_SET (proper_divisors n)

⊢ ∀n. 1 ∉ proper_divisors n

⊢ ∀n. prime n ⇒ proper_divisors n = ∅

⊢ ∀n. proper_divisors n ⊆ less_divisors n

⊢ rec_phi 0 = 0

⊢ rec_phi 1 = 1

⊢ ∀n. rec_phi n =
      if n = 0 then 0
      else if n = 1 then 1
      else n − ∑ (λa. rec_phi a) {m | m < n ∧ m divides n}

⊢ ∀n. rec_phi n = phi n

⊢ ∀P. (∀n. (∀a. n ≠ 0 ∧ n ≠ 1 ∧ a ∈ {m | m < n ∧ m divides n} ⇒ P a) ⇒ P n) ⇒
      ∀v. P v

⊢ ∀n x. MEM x [1 .. n] ⇒ MEM (x ** LOG x n) [1 .. n]

⊢ ∀n. set_lcm (prime_powers_upto n) = PROD_SET (prime_powers_upto n)

⊢ ∀p. 1 < p ⇒
      ∀f. (∀n. 0 < n ⇒ p ** n = ∑ (λd. d * f d) (divisors n)) ⇒
          (∀n. 0 < n ⇒ n * f n ≤ p ** n) ∧
          ∀n. 0 < n ⇒ p ** n − TWICE (p ** HALF n) < n * f n

⊢ ∀p. 1 < p ⇒
      ∀f. (∀n. 0 < n ⇒ p ** n = ∑ (λd. d * f d) (divisors n)) ⇒
          (∀n. 0 < n ⇒ n * f n ≤ p ** n) ∧
          ∀n. 0 < n ⇒ (p ** HALF n − 2) * p ** HALF n < n * f n

⊢ ∀s. DISJOINT (sq_free s) (non_sq_free s)

⊢ ∀s. DISJOINT (even_sq_free s) (odd_sq_free s)

⊢ ∀s n. n ∈ sq_free s ⇔ n ∈ s ∧ square_free n

⊢ ∀s. FINITE s ⇒ FINITE (sq_free s)

⊢ ∀s. sq_free s ∩ non_sq_free s = ∅

⊢ ∀s. even_sq_free s ∩ odd_sq_free s = ∅

⊢ ∀s. s = sq_free s ∪ non_sq_free s ∧ sq_free s ∩ non_sq_free s = ∅

⊢ ∀s. sq_free s = even_sq_free s ∪ odd_sq_free s ∧
      even_sq_free s ∩ odd_sq_free s = ∅

⊢ ∀s. sq_free s ⊆ s

⊢ ∀s. s = sq_free s ∪ non_sq_free s

⊢ ∀s. sq_free s = even_sq_free s ∪ odd_sq_free s

⊢ ∀n. SQRT n ≤ 2 ** ulog n

⊢ square 0

⊢ square 1

⊢ ∀n. square n ⇔ ∃k. n = k²

⊢ ∀n. square n ⇔ (SQRT n)² = n

⊢ square_free 1

⊢ ∀n. prime n ⇒ square_free n

⊢ ∀f g. f 0 = g 0 ∧ (∀n. ∑ f (divisors n) = ∑ g (divisors n)) ⇒ f = g

⊢ ∀f n.
    ∑ f (count n) =
    ∑ (∑ f) (IMAGE (preimage (gcd n) (count n)) (divisors n))

⊢ ∀f n. ∑ f (count n) = ∑ (∑ f) (partition (feq (gcd n)) (count n))

⊢ ∀f n. ∑ f (natural n) = ∑ (∑ f) (IMAGE (gcd_matches n) (divisors n))

⊢ ∀f n. ∑ f (natural n) = ∑ (∑ f) (partition (feq (gcd n)) (natural n))

⊢ ∀f n.
    ∑ f (natural n) =
    ∑ (∑ f) (IMAGE (preimage (gcd n) (natural n)) (divisors n))

⊢ ∀f n.
    0 < n ⇒
    ∑ f (upto n) = ∑ (∑ f) (IMAGE (preimage (gcd n) (upto n)) (divisors n))

⊢ ∀f n. ∑ f (upto n) = ∑ (∑ f) (partition (feq (gcd n)) (upto n))

⊢ ∀m n p.
    p ∈ total_prime_divisors m n ⇔
    p ∈ prime_divisors m ∨ p ∈ prime_divisors n

⊢ ∀m n. 0 < m ∧ 0 < n ⇒ FINITE (total_prime_divisors m n)

⊢ ∀m n x y.
    x ∈ IMAGE (λp. p ** MAX (ppidx m) (ppidx n)) (total_prime_divisors m n) ∧
    y ∈ IMAGE (λp. p ** MAX (ppidx m) (ppidx n)) (total_prime_divisors m n) ∧
    x ≠ y ⇒
    coprime x y

⊢ ∀m n x y.
    x ∈ total_prime_divisors m n ∧ y ∈ total_prime_divisors m n ∧ x ≠ y ⇒
    coprime x y

⊢ ∀n a b. n = a * b ⇒ a ≤ SQRT n ∨ b ≤ SQRT n

⊢ ∀n a b. n = a * b ∧ a < SQRT n ⇒ SQRT n ≤ b

⊢ ∀n a b. n = a * b ∧ SQRT n < a ⇒ b ≤ SQRT n

⊢ ulog 0 = 0

⊢ ulog 1 = 0

⊢ ulog 2 = 1

⊢ ∀n. ulog (2 ** n) = n

⊢ ∀n. 0 < n ⇒ LOG2 n ≤ ulog n ∧ ulog n ≤ 1 + LOG2 n

⊢ ∀n. ulog n =
      if n = 0 then 0 else if n power_of 2 then LOG2 n else SUC (LOG2 n)

⊢ ulog 0 = 0 ∧ ∀n. 0 < n ⇒ ∀m. ulog n = m ⇔ n ≤ 2 ** m ∧ 2 ** m < TWICE n

⊢ ∀n. ulog n = 0 ⇔ n = 0 ∨ n = 1

⊢ ∀n. ulog n = 1 ⇔ n = 2

⊢ ∀n. ulog n = n ⇔ n = 0

⊢ ∀n. ulog n = if 1 < n then SUC (LOG2 (n − 1)) else 0

⊢ ∀n. 0 < n ∧ EVEN n ⇒ ulog n = 1 + ulog (HALF n)

⊢ ∀m n. ulog (m ** n) ≤ n * ulog m

⊢ ∀n. 2 ** ulog n = n ⇔ n power_of 2

⊢ ∀n. ¬(n power_of 2) ⇒ 2 ** ulog n ≠ n

⊢ ∀n. 1 < n ⇒ 1 ≤ ulog n

⊢ ∀n. 1 < n ⇒ ulog (HALF n) + 1 ≤ ulog n

⊢ ∀m n. n ≤ m ⇒ ulog n ≤ ulog m

⊢ ∀n. ulog n ≤ 1 ⇔ n ≤ 2

⊢ ∀n. ulog n ≤ n

⊢ ∀m n. n < m ⇒ ulog n ≤ ulog m

⊢ ∀n. 0 < n ⇒ ulog n < n

⊢ ∀m n. ulog (m * n) ≤ ulog m + ulog n

⊢ ∀n. 1 < n ∧ ODD n ⇒ ulog (HALF n) + 1 ≤ ulog n

⊢ ∀n. 1 < n ⇒ 0 < ulog n

⊢ ∀n. 0 < n ⇒ 2 ** ulog n < TWICE n ∧ n ≤ 2 ** ulog n

⊢ ∀n. 0 < n ∧ ¬(n power_of 2) ⇒ n < 2 ** ulog n

⊢ ∀n. 1 < n ∧ ODD n ⇒ n < 2 ** ulog n

⊢ ∀n. 2 < n ⇒ 1 < (ulog n)²

⊢ ∀n. 0 < n ⇒ ulog (SUC n) = SUC (LOG2 n)

⊢ ∀n. 0 < n ⇒ ∀m. ulog n = m ⇔ 2 ** m < TWICE n ∧ n ≤ 2 ** m

⊢ ∀n. 1 < n ⇒ 4 ≤ (TWICE (ulog n))²

⊢ ∀m n. 2 ** m < TWICE n ∧ n ≤ 2 ** m ⇒ ulog n = m