100/bertrand.ml

   1 (* ========================================================================= *)
   2 (* Proof of Bertrand conjecture and weak form of prime number theorem.       *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/prime.ml";;
   6 needs "Library/pocklington.ml";;
   7 needs "Library/analysis.ml";;
   8 needs "Library/transc.ml";;
   9 needs "Library/calc_real.ml";;
  10 needs "Library/floor.ml";;
  11
  12 prioritize_real();;
  13
  14 (* ------------------------------------------------------------------------- *)
  15 (* A ridiculous ommission from the OCaml Num library.                        *)
  16 (* ------------------------------------------------------------------------- *)
  17
  18 let num_of_float =
  19   let p22 = Pervasives.( ** ) 2.0 22.0
  20   and p44 = Pervasives.( ** ) 2.0 44.0
  21   and p66 = Pervasives.( ** ) 2.0 66.0
  22   and q22 = pow2 22 and q44 = pow2 44 and q66 = pow2 66 in
  23   fun x ->
  24     let y0,n = frexp x in
  25     let u0 = int_of_float(y0 *. p22) in
  26     let y1 = p22 *. y0 -. float_of_int u0 in
  27     let u1 = int_of_float(y1 *. p22) in
  28     let y2 = p22 *. y1 -. float_of_int u1 in
  29     let u2 = int_of_float(y2 *. p22) in
  30     let y3 = p22 *. y2 -. float_of_int u2 in
  31     if y3 <> 0.0 then failwith "num_of_float: inexactness!" else
  32     (Int u0 // q22 +/ Int u1 // q44 +/ Int u2 // q66) */ pow2 n;;
  33
  34 (* ------------------------------------------------------------------------- *)
  35 (* Integer truncated square root                                             *)
  36 (* ------------------------------------------------------------------------- *)
  37
  38 let ISQRT = new_definition
  39   `ISQRT n = @m. m EXP 2 <= n /\ n < (m + 1) EXP 2`;;
  40
  41 let ISQRT_WORKS = prove
  42  (`!n. ISQRT(n) EXP 2 <= n /\ n < (ISQRT(n) + 1) EXP 2`,
  43   GEN_TAC THEN REWRITE_TAC[ISQRT] THEN CONV_TAC SELECT_CONV THEN
  44   SUBGOAL_THEN `(?m. m EXP 2 <= n) /\ (?a. !m. m EXP 2 <= n ==> m <= a)`
  45   MP_TAC THENL
  46    [ALL_TAC;
  47     ONCE_REWRITE_TAC[num_MAX] THEN
  48     MATCH_MP_TAC MONO_EXISTS THEN
  49     MESON_TAC[ARITH_RULE `~(m + 1 <= m)`; NOT_LE]] THEN
  50   CONJ_TAC THENL [EXISTS_TAC `0` THEN REWRITE_TAC[ARITH; LE_0]; ALL_TAC] THEN
  51   EXISTS_TAC `n:num` THEN X_GEN_TAC `m:num` THEN
  52   MESON_TAC[LE_SQUARE_REFL; EXP_2; LE_TRANS]);;
  53
  54 let ISQRT_0 = prove
  55  (`ISQRT 0 = 0`,
  56   MP_TAC(SPEC `0` ISQRT_WORKS) THEN
  57   SIMP_TAC[ARITH_RULE `x <= 0 <=> (x = 0)`; EXP_EQ_0; ARITH_EQ]);;
  58
  59 let ISQRT_UNIQUE = prove
  60  (`!m n. (ISQRT n = m) <=> m EXP 2 <= n /\ n < (m + 1) EXP 2`,
  61   REPEAT GEN_TAC THEN EQ_TAC THEN MP_TAC (SPEC `n:num` ISQRT_WORKS) THENL
  62    [MESON_TAC[]; ALL_TAC] THEN
  63   REPEAT STRIP_TAC THEN
  64   SUBGOAL_THEN `(ISQRT n) EXP 2 < (m + 1) EXP 2 /\
  65                 m EXP 2 < (ISQRT n + 1) EXP 2`
  66   MP_TAC THENL
  67    [ASM_MESON_TAC[LT_SUC_LE; LE_SUC_LT; LET_TRANS; LTE_TRANS];
  68     SIMP_TAC[num_CONV `2`; EXP_MONO_LT_SUC; GSYM LE_ANTISYM] THEN ARITH_TAC]);;
  69
  70 let ISQRT_SUC = prove
  71  (`!n. ISQRT(SUC n) =
  72        if ?m. SUC n = m EXP 2 then SUC(ISQRT n) else ISQRT n`,
  73   GEN_TAC THEN REWRITE_TAC[ISQRT_UNIQUE] THEN COND_CASES_TAC THENL
  74    [ALL_TAC;
  75     ASM_MESON_TAC[ISQRT_WORKS; ARITH_RULE
  76      `a <= n /\ n < b /\ ~(SUC n = a) /\ ~(SUC n = b)
  77       ==> a <= SUC n /\ SUC n < b`]] THEN
  78   CONJ_TAC THENL
  79    [ALL_TAC;
  80     MP_TAC(CONJUNCT2(SPEC `n:num` ISQRT_WORKS)) THEN
  81     REWRITE_TAC[EXP_2; GSYM ADD1; MULT_CLAUSES; ADD_CLAUSES; LT_SUC] THEN
  82     ARITH_TAC] THEN
  83   POP_ASSUM(X_CHOOSE_TAC `m:num`) THEN
  84   SUBGOAL_THEN `m = SUC(ISQRT n)` SUBST_ALL_TAC THENL
  85    [ALL_TAC; ASM_REWRITE_TAC[LE_REFL]] THEN
  86   SUBGOAL_THEN `ISQRT(n) EXP 2 < m EXP 2 /\ m EXP 2 <= SUC(ISQRT n) EXP 2`
  87   MP_TAC THENL
  88    [ALL_TAC;
  89     REWRITE_TAC[num_CONV `2`; EXP_MONO_LE_SUC; EXP_MONO_LT_SUC] THEN ARITH_TAC] THEN
  90   MP_TAC(SPEC `n:num` ISQRT_WORKS) THEN REWRITE_TAC[ADD1] THEN
  91   FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[LT_SUC_LE; LE_SUC_LT]);;
  92
  93 (* ------------------------------------------------------------------------- *)
  94 (* To allow us to deal with ln(2) numerically using standard conversion.     *)
  95 (* ------------------------------------------------------------------------- *)
  96
  97 let LN_2_COMPOSITION = prove
  98  (`ln(&2) =
  99    &7 * ln(&1 + inv(&8)) - &2 * ln(&1 + inv(&24)) - &4 * ln(&1 + inv(&80))`,
 100   CONV_TAC(GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 4
 101         [GSYM LN_POW; GSYM LN_MUL; GSYM LN_DIV; REAL_POW_LT; real_div;
 102          REAL_LT_ADD; REAL_LT_MUL; REAL_LT_INV_EQ; REAL_OF_NUM_LT; ARITH]) THEN
 103   AP_TERM_TAC THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
 104
 105 (* ------------------------------------------------------------------------- *)
 106 (* Automatically process any ln(n) to allow us to use standard conversions.  *)
 107 (* ------------------------------------------------------------------------- *)
 108
 109 let LN_N_CONV =
 110   let pth = prove
 111    (`x = (&1 + inv(&8)) pow n * (x / (&1 + inv(&8)) pow n)`,
 112     CONV_TAC REAL_RAT_REDUCE_CONV THEN
 113     CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_DIV_LMUL THEN
 114     MATCH_MP_TAC REAL_POW_NZ THEN CONV_TAC REAL_RAT_REDUCE_CONV)
 115   and qth = prove
 116    (`&0 < x
 117      ==> (ln((&1 + inv(&8)) pow n * x / (&1 + inv(&8)) pow n) =
 118           &n * ln(&1 + inv(&8)) + ln(&1 + (x / (&1 + inv(&8)) pow n - &1)))`,
 119     REWRITE_TAC[REAL_ARITH `&1 + (x - &1) = x`] THEN
 120     SIMP_TAC[LN_MUL; LN_POW; REAL_LT_DIV; REAL_POW_LT;
 121              REAL_RAT_REDUCE_CONV `&0 < &1 + inv(&8)`])
 122   and ln_tm = `ln` and x_tm = `x:real` and n_tm = `n:num` in
 123   fun tm0 ->
 124     let ltm,tm = dest_comb tm0 in
 125     if ltm <> ln_tm then failwith "expected ln(ratconst)" else
 126     let x = rat_of_term tm in
 127     let rec dlog n y =
 128       let y' = y +/ y // Int 8 in
 129       if y' </ x then dlog (n + 1) y' else n in
 130     let n = dlog 0 (Int 1) in
 131     let th1 = INST [mk_small_numeral n,n_tm; tm,x_tm] pth in
 132     let th2 = AP_TERM ltm th1 in
 133     let th3 = PART_MATCH (lhs o rand) qth (rand(concl th2)) in
 134     let th4 = MP th3 (EQT_ELIM(REAL_RAT_REDUCE_CONV(lhand(concl th3)))) in
 135     let th5 = TRANS th2 th4 in
 136     CONV_RULE(funpow 4 RAND_CONV REAL_RAT_REDUCE_CONV) th5;;
 137
 138 (* ------------------------------------------------------------------------- *)
 139 (* Coarser version subtracting off multiples of ln(2) first, then using it.  *)
 140 (* ------------------------------------------------------------------------- *)
 141
 142 let LN_N2_CONV =
 143   let pth = prove
 144    (`x = &2 pow n * (x / &2 pow n)`,
 145     CONV_TAC REAL_RAT_REDUCE_CONV THEN
 146     CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_DIV_LMUL THEN
 147     MATCH_MP_TAC REAL_POW_NZ THEN CONV_TAC REAL_RAT_REDUCE_CONV)
 148   and qth = prove
 149    (`&0 < x
 150      ==> (ln(&2 pow n * x / &2 pow n) =
 151           &n * ln(&2) + ln(&1 + (x / &2 pow n - &1)))`,
 152     REWRITE_TAC[REAL_ARITH `&1 + (x - &1) = x`] THEN
 153     SIMP_TAC[LN_MUL; LN_POW; REAL_LT_DIV; REAL_POW_LT;
 154              REAL_RAT_REDUCE_CONV `&0 < &2`])
 155   and ln_tm = `ln` and x_tm = `x:real` and n_tm = `n:num` in
 156   fun tm0 ->
 157     let ltm,tm = dest_comb tm0 in
 158     if ltm <> ln_tm then failwith "expected ln(ratconst)" else
 159     let x = rat_of_term tm in
 160     let rec dlog n y =
 161       let y' = y */ Int 2 in
 162       if y' </ x then dlog (n + 1) y' else n in
 163     let n = dlog 0 (Int 1) in
 164     let th1 = INST [mk_small_numeral n,n_tm; tm,x_tm] pth in
 165     let th2 = AP_TERM ltm th1 in
 166     let th3 = PART_MATCH (lhs o rand) qth (rand(concl th2)) in
 167     let th4 = MP th3 (EQT_ELIM(REAL_RAT_REDUCE_CONV(lhand(concl th3)))) in
 168     let th5 = TRANS th2 th4 in
 169     let th6 = CONV_RULE(funpow 4 RAND_CONV REAL_RAT_REDUCE_CONV) th5 in
 170     let th7 = CONV_RULE (funpow 3 RAND_CONV REAL_RAT_REDUCE_CONV) th6 in
 171     CONV_RULE(RAND_CONV(ONCE_DEPTH_CONV LN_N_CONV)) th7;;
 172
 173 (* ------------------------------------------------------------------------- *)
 174 (* Lemmas about floor and frac.                                              *)
 175 (* ------------------------------------------------------------------------- *)
 176
 177 let FLOOR_DOUBLE_NUM = prove
 178  (`!n r d.
 179         d < 2 /\ 0 < r
 180         ==> &2 * floor(&n / &r) <= floor(&(2 * n + d) / &r) /\
 181             floor(&(2 * n + d) / &r) <= &2 * floor(&n / &r) + &1`,
 182   REPEAT GEN_TAC THEN STRIP_TAC THEN
 183   SUBGOAL_THEN `floor(&n / &r) = floor((&n + &d / &2) / &r)` SUBST1_TAC THENL
 184    [ALL_TAC;
 185     REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] THEN
 186     SUBGOAL_THEN `&2 * &n + &d = &2 * (&n + &d / &2)` SUBST1_TAC THENL
 187      [SIMP_TAC[REAL_ADD_LDISTRIB; REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH_EQ];
 188       ALL_TAC] THEN
 189     REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; GSYM REAL_MUL_ASSOC; real_div] THEN
 190     REWRITE_TAC[GSYM real_div; FLOOR_DOUBLE]] THEN
 191   CONV_TAC SYM_CONV THEN REWRITE_TAC[GSYM FLOOR_UNIQUE] THEN
 192   MP_TAC(SPEC `&n / &r` FLOOR) THEN SIMP_TAC[] THEN REPEAT STRIP_TAC THENL
 193    [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&n / &r` THEN
 194     ASM_REWRITE_TAC[] THEN
 195     REWRITE_TAC[real_div; REAL_ADD_RDISTRIB; REAL_LE_ADDR] THEN
 196     SIMP_TAC[REAL_LE_MUL; REAL_POS; REAL_LE_INV_EQ];
 197     ALL_TAC] THEN
 198   UNDISCH_TAC `&n / &r < floor (&n / &r) + &1` THEN
 199   ASM_SIMP_TAC[REAL_LT_LDIV_EQ; REAL_OF_NUM_LT] THEN
 200   SIMP_TAC[REAL_LT_INTEGERS; FLOOR; INTEGER_CLOSED] THEN
 201   MATCH_MP_TAC(REAL_ARITH `b < a ==> n + a <= c ==> n + b < c`) THEN
 202   ASM_SIMP_TAC[REAL_LT_LDIV_EQ; REAL_MUL_LID; REAL_OF_NUM_LT; ARITH]);;
 203
 204 (* ------------------------------------------------------------------------- *)
 205 (* Range bounds on ln(n!).                                                   *)
 206 (* ------------------------------------------------------------------------- *)
 207
 208 let LN_FACT = prove
 209  (`!n. ln(&(FACT n)) = sum(1,n) (\d. ln(&d))`,
 210   INDUCT_TAC THEN REWRITE_TAC[FACT; sum; LN_1] THEN
 211   SIMP_TAC[GSYM REAL_OF_NUM_MUL; LN_MUL; REAL_OF_NUM_LT; FACT_LT; LT_0] THEN
 212   ASM_REWRITE_TAC[ADD1] THEN REWRITE_TAC[ADD_AC; REAL_ADD_AC]);;
 213
 214 let LN_FACT_BOUNDS = prove
 215  (`!n. ~(n = 0) ==> abs(ln(&(FACT n)) - (&n * ln(&n) - &n)) <= &1 + ln(&n)`,
 216   SUBGOAL_THEN
 217    `!n. ~(n = 0)
 218         ==> ?z. &n < z /\ z < &(n + 1) /\
 219                 (&(n + 1) * ln(&(n + 1)) - &n * ln(&n) = ln(z) + &1)`
 220   MP_TAC THENL
 221    [REPEAT STRIP_TAC THEN
 222     MP_TAC(SPECL [`\x. x * ln(x)`; `\x. ln(x) + &1`; `&n`; `&(n + 1)`]
 223                  MVT_ALT) THEN
 224     REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN
 225     REWRITE_TAC[REAL_ARITH `(n + &1) - n = &1`] THEN
 226     REWRITE_TAC[REAL_MUL_LID] THEN DISCH_THEN MATCH_MP_TAC THEN
 227     REWRITE_TAC[REAL_ARITH `a < a + &1`] THEN
 228     X_GEN_TAC `x:real` THEN STRIP_TAC THEN
 229     MP_TAC(SPEC `x:real` (DIFF_CONV `\x. x * ln(x)`)) THEN
 230     SIMP_TAC[REAL_MUL_LID; REAL_MUL_RID; REAL_MUL_LINV; REAL_LT_IMP_NZ] THEN
 231     DISCH_THEN MATCH_MP_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN
 232     EXISTS_TAC `&n` THEN ASM_REWRITE_TAC[REAL_OF_NUM_LT] THEN
 233     UNDISCH_TAC `~(n = 0)` THEN ARITH_TAC;
 234     ALL_TAC] THEN
 235   REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN
 236   DISCH_THEN(X_CHOOSE_TAC `k:num->real`) THEN
 237   SUBGOAL_THEN
 238    `!n. &(n + 1) * ln(&(n + 1)) = sum(1,n) (\i. ln(k i) + &1)`
 239   MP_TAC THENL
 240    [INDUCT_TAC THEN REWRITE_TAC[NOT_SUC] THEN
 241     REWRITE_TAC[sum; ADD_CLAUSES; LN_1; REAL_MUL_RZERO] THEN
 242     FIRST_X_ASSUM(MP_TAC o SPEC `n + 1`) THEN
 243     REWRITE_TAC[ADD_EQ_0; ARITH_EQ] THEN
 244     REWRITE_TAC[ARITH_RULE `(n + 1) + 1 = n + 2`;
 245                 ARITH_RULE `SUC(n + 1) = n + 2`] THEN
 246     DISCH_THEN(MP_TAC o last o CONJUNCTS) THEN
 247     REWRITE_TAC[REAL_ARITH `(a - b = c) <=> (a = b + c)`] THEN
 248     DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[] THEN
 249     REWRITE_TAC[ADD_AC];
 250     ALL_TAC] THEN
 251   REWRITE_TAC[SUM_ADD] THEN
 252   CONV_TAC(LAND_CONV(BINDER_CONV(RAND_CONV(RAND_CONV(LAND_CONV
 253     (LAND_CONV num_CONV)))))) THEN
 254   REWRITE_TAC[ADD1; SUM_REINDEX; SUM_CONST] THEN
 255   ONCE_REWRITE_TAC[REAL_ARITH `(a = b + c * &1) <=> (b = a - c)`] THEN
 256   DISCH_TAC THEN
 257   SUBGOAL_THEN
 258    `!n. abs(sum(1,n+1) (\i. ln(&i)) - (&(n + 1) * ln (&(n + 1)) - &(n + 1)))
 259         <= &1 + ln(&(n + 1))`
 260   ASSUME_TAC THENL
 261    [GEN_TAC THEN
 262     GEN_REWRITE_TAC (LAND_CONV o funpow 3 RAND_CONV)
 263      [GSYM REAL_OF_NUM_ADD] THEN
 264     MATCH_MP_TAC(REAL_ARITH
 265      `abs(x - (y - z)) <= a ==> abs(x - (y - (z + &1))) <= &1 + a`) THEN
 266     FIRST_ASSUM(fun th -> GEN_REWRITE_TAC
 267       (LAND_CONV o RAND_CONV o RAND_CONV) [GSYM th]) THEN
 268     SUBGOAL_THEN
 269      `sum(1,n + 1) (\i. ln (&i)) = sum(1,n) (\i. ln(&(i + 1)))`
 270     SUBST1_TAC THENL
 271      [GEN_REWRITE_TAC RAND_CONV [SUM_DIFF] THEN
 272       REWRITE_TAC[SUM_1; ADD_CLAUSES; LN_1; REAL_SUB_RZERO] THEN
 273       GEN_REWRITE_TAC (funpow 3 LAND_CONV) [SYM(NUM_REDUCE_CONV `0 + 1`)] THEN
 274       REWRITE_TAC[SUM_REINDEX] THEN REWRITE_TAC[ADD_AC];
 275       ALL_TAC] THEN
 276     REWRITE_TAC[GSYM SUM_SUB] THEN
 277     MATCH_MP_TAC REAL_LE_TRANS THEN
 278     EXISTS_TAC `sum(1,n) (\n. abs(ln(&(n + 1)) - ln(k n)))` THEN
 279     REWRITE_TAC[ABS_SUM] THEN
 280     MATCH_MP_TAC REAL_LE_TRANS THEN
 281     EXISTS_TAC `sum(1,n) (\i. ln(&(i + 1)) - ln(&i))` THEN CONJ_TAC THENL
 282      [MATCH_MP_TAC SUM_LE THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
 283       REWRITE_TAC[] THEN
 284       MATCH_MP_TAC(REAL_ARITH `a < b /\ b < c ==> abs(c - b) <= c - a`) THEN
 285       SUBGOAL_THEN `&0 < &r /\ &r < k r /\ k r < &(r + 1)` MP_TAC THENL
 286        [ALL_TAC; MESON_TAC[LN_MONO_LT; REAL_LT_TRANS]] THEN
 287       ASM_SIMP_TAC[REAL_OF_NUM_LT; ARITH_RULE `0 < r <=> 1 <= r`;
 288                    ARITH_RULE `~(r = 0) <=> 1 <= r`];
 289       ALL_TAC] THEN
 290     REWRITE_TAC[SUM_SUB] THEN
 291     REWRITE_TAC[GSYM(SPECL [`f:num->real`; `m:num`; `1`] SUM_REINDEX)] THEN
 292     ONCE_REWRITE_TAC[SUM_DIFF] THEN
 293     REWRITE_TAC[ARITH; SUM_2; SUM_1; LN_1; REAL_ADD_RID] THEN
 294     ONCE_REWRITE_TAC[ARITH_RULE `2 + n = SUC(1 + n)`] THEN
 295     REWRITE_TAC[sum; ADD_CLAUSES] THEN
 296     REWRITE_TAC[ADD_AC] THEN
 297     REWRITE_TAC[REAL_ARITH `(a + b) - c - (a - c) = b`; REAL_LE_REFL];
 298     ALL_TAC] THEN
 299   INDUCT_TAC THEN REWRITE_TAC[NOT_SUC] THEN
 300   ASM_REWRITE_TAC[ADD1; LN_FACT]);;
 301
 302 (* ------------------------------------------------------------------------- *)
 303 (* Some extra number-theoretic odds and ends are useful.                     *)
 304 (* ------------------------------------------------------------------------- *)
 305
 306 let primepow = new_definition
 307   `primepow q <=> ?p k. 1 <= k /\ prime p /\ (q = p EXP k)`;;
 308
 309 let aprimedivisor = new_definition
 310   `aprimedivisor q = @p. prime p /\ p divides q`;;
 311
 312 let PRIMEPOW_GE_2 = prove
 313  (`!q. primepow q ==> 2 <= q`,
 314   REWRITE_TAC[primepow; LEFT_IMP_EXISTS_THM] THEN
 315   MAP_EVERY X_GEN_TAC [`q:num`; `p:num`; `k:num`] THEN
 316   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 317   DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `p:num` THEN
 318   ASM_SIMP_TAC[PRIME_GE_2] THEN GEN_REWRITE_TAC LAND_CONV [GSYM EXP_1] THEN
 319   REWRITE_TAC[LE_EXP] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH]);;
 320
 321 let PRIMEPOW_0 = prove
 322  (`~(primepow 0)`,
 323   MESON_TAC[NUM_REDUCE_CONV `2 <= 0`; PRIMEPOW_GE_2]);;
 324
 325 let APRIMEDIVISOR_PRIMEPOW = prove
 326  (`!p k. prime p /\ 1 <= k ==> (aprimedivisor(p EXP k) = p)`,
 327   REPEAT STRIP_TAC THEN REWRITE_TAC[aprimedivisor] THEN
 328   MATCH_MP_TAC SELECT_UNIQUE THEN REWRITE_TAC[] THEN
 329   X_GEN_TAC `q:num` THEN
 330   FIRST_ASSUM(SUBST1_TAC o MATCH_MP (ARITH_RULE
 331    `1 <= k ==> (k = SUC(k - 1))`)) THEN
 332   REWRITE_TAC[EXP] THEN
 333   ASM_MESON_TAC[DIVIDES_REFL; DIVIDES_RMUL; PRIME_DIVEXP; PRIME_DIVPROD;
 334                 prime; PRIME_1]);;
 335
 336 let APRIMEDIVISOR = prove
 337  (`!n. ~(n = 1) ==> prime(aprimedivisor n) /\ (aprimedivisor n) divides n`,
 338   GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[aprimedivisor] THEN
 339   CONV_TAC SELECT_CONV THEN ASM_SIMP_TAC[PRIME_FACTOR]);;
 340
 341 let BIG_POWER_LEMMA = prove
 342  (`!m n. 2 <= m ==> ?k. n <= m EXP k`,
 343   REPEAT STRIP_TAC THEN EXISTS_TAC `SUC n` THEN
 344   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `2 EXP (SUC n)` THEN
 345   ASM_REWRITE_TAC[EXP_MONO_LE_SUC] THEN
 346   SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
 347   REWRITE_TAC[EXP; ARITH] THEN
 348   UNDISCH_TAC `n <= 2 EXP SUC n` THEN REWRITE_TAC[EXP] THEN
 349   MP_TAC(SPECL [`2:num`; `n:num`] EXP_EQ_0) THEN
 350   REWRITE_TAC[ARITH] THEN SPEC_TAC(`2 EXP n`,`m:num`) THEN ARITH_TAC);;
 351
 352 let PRIME_PRIMEPOW = prove
 353  (`!p. prime p ==> primepow p`,
 354   MESON_TAC[prime; primepow; LE_REFL; EXP_1]);;
 355
 356 (* ------------------------------------------------------------------------- *)
 357 (* Derive Bezout-type identity by finding gcd.                               *)
 358 (* ------------------------------------------------------------------------- *)
 359
 360 let rec bezout (m,n) =
 361   if m =/ Int 0 then (Int 0,Int 1) else if n =/ Int 0 then (Int 1,Int 0)
 362   else if m <=/ n then
 363     let q = quo_num n m and r = mod_num n m in
 364     let (x,y) = bezout(m,r) in
 365     (x -/ q */ y,y)
 366   else let (x,y) = bezout(n,m) in (y,x);;
 367
 368 (* ------------------------------------------------------------------------- *)
 369 (* Conversion for "primepow" applied to particular numeral.                  *)
 370 (* ------------------------------------------------------------------------- *)
 371
 372 let PRIMEPOW_CONV =
 373   let pth0 = prove
 374    (`primepow 0 <=> F`,
 375     REWRITE_TAC[primepow] THEN MESON_TAC[EXP_EQ_0; PRIME_0])
 376   and pth1 = prove
 377    (`primepow 1 <=> F`,
 378     REWRITE_TAC[primepow] THEN
 379     MESON_TAC[EXP_EQ_1; PRIME_1; NUM_REDUCE_CONV `1 <= 0`])
 380   and pth2 = prove
 381    (`prime p ==> 1 <= k /\ (q = p EXP k) ==> (primepow q <=> T)`,
 382     MESON_TAC[primepow])
 383   and pth3 = prove
 384    (`(p * x = r * y + 1) /\ ~(p = 1) /\ ~(r = 1) /\ (q = p * r * d)
 385      ==> (primepow q <=> F)`,
 386     REPEAT STRIP_TAC THEN REWRITE_TAC[primepow] THEN
 387     DISCH_THEN(X_CHOOSE_THEN `P:num` MP_TAC) THEN
 388     DISCH_THEN(X_CHOOSE_THEN `k:num` MP_TAC) THEN
 389     REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 390     DISCH_THEN SUBST_ALL_TAC THEN
 391     MP_TAC(SPEC `r:num` PRIME_FACTOR) THEN
 392     MP_TAC(SPEC `p:num` PRIME_FACTOR) THEN
 393     ASM_REWRITE_TAC[] THEN
 394     DISCH_THEN(X_CHOOSE_THEN `P_p:num` MP_TAC) THEN
 395     REWRITE_TAC[divides] THEN
 396     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 397     DISCH_THEN(X_CHOOSE_THEN `d_p:num` SUBST_ALL_TAC) THEN
 398     DISCH_THEN(X_CHOOSE_THEN `P_r:num` MP_TAC) THEN
 399     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 400     DISCH_THEN(X_CHOOSE_THEN `d_r:num` SUBST_ALL_TAC) THEN
 401     SUBGOAL_THEN `P_p divides P /\ P_r divides P` ASSUME_TAC THENL
 402      [CONJ_TAC THEN MATCH_MP_TAC PRIME_DIVEXP THEN EXISTS_TAC `k:num` THEN
 403       ASM_MESON_TAC[divides; MULT_AC]; ALL_TAC] THEN
 404     SUBGOAL_THEN `(P_p = P) /\ (P_r = P:num)` (CONJUNCTS_THEN SUBST_ALL_TAC)
 405     THENL [ASM_MESON_TAC[prime]; ALL_TAC] THEN
 406     ASM_MESON_TAC[DIVIDES_ADD_REVR; divides; MULT_AC; DIVIDES_ONE; prime])
 407   and p_tm = `p:num` and k_tm = `k:num` and q_tm = `q:num`
 408   and r_tm = `r:num` and d_tm = `d:num`
 409   and x_tm = `x:num` and y_tm = `y:num` and primepow_tm = `primepow` in
 410   fun tm0 ->
 411     let ptm,tm = dest_comb tm0 in
 412     if ptm <> primepow_tm then failwith "expected primepow(numeral)" else
 413     let q = dest_numeral tm in
 414     if q =/ Int 0 then pth0
 415     else if q =/ Int 1 then pth1 else
 416     match factor q with
 417       [] -> failwith "internal failure in PRIMEPOW_CONV"
 418     | [p,k] -> let th1 = INST [mk_numeral q,q_tm;
 419                                mk_numeral p,p_tm;
 420                                mk_numeral k,k_tm] pth2 in
 421                let th2 = MP th1 (EQT_ELIM(PRIME_CONV(lhand(concl th1)))) in
 422                MP th2 (EQT_ELIM(NUM_REDUCE_CONV(lhand(concl th2))))
 423     | (p,_)::(r,_)::_ ->
 424                let d = q // (p */ r) in
 425                let (x,y) = bezout(p,r) in
 426                let p,r,x,y =
 427                  if x </ Int 0 then r,p,y,minus_num x
 428                  else p,r,x,minus_num y in
 429                let th1 = INST [mk_numeral q,q_tm;
 430                                mk_numeral p,p_tm;
 431                                mk_numeral r,r_tm;
 432                                mk_numeral x,x_tm;
 433                                mk_numeral y,y_tm;
 434                                mk_numeral d,d_tm] pth3 in
 435                MP th1 (EQT_ELIM(NUM_REDUCE_CONV(lhand(concl th1))));;
 436
 437 (* ------------------------------------------------------------------------- *)
 438 (* Conversion for "aprimedivisor" applied to prime power (only).             *)
 439 (* ------------------------------------------------------------------------- *)
 440
 441 let APRIMEDIVISOR_CONV =
 442   let pth = prove
 443    (`prime p ==> 1 <= k /\ (q = p EXP k) ==> (aprimedivisor q = p)`,
 444     MESON_TAC[APRIMEDIVISOR_PRIMEPOW])
 445   and p_tm = `p:num` and k_tm = `k:num` and q_tm = `q:num`
 446   and aprimedivisor_tm = `aprimedivisor` in
 447   fun tm0 ->
 448     let ptm,tm = dest_comb tm0 in
 449     if ptm <> aprimedivisor_tm then failwith "expected primepow(numeral)" else
 450     let q = dest_numeral tm in
 451     if q =/ Int 0 then failwith "APRIMEDIVISOR_CONV: not a prime power" else
 452     match factor q with
 453       [p,k] -> let th1 = INST [mk_numeral q,q_tm;
 454                                mk_numeral p,p_tm;
 455                                mk_numeral k,k_tm] pth in
 456                let th2 = MP th1 (EQT_ELIM(PRIME_CONV(lhand(concl th1)))) in
 457                MP th2 (EQT_ELIM(NUM_REDUCE_CONV(lhand(concl th2))))
 458     | _ -> failwith "APRIMEDIVISOR_CONV: not a prime power";;
 459
 460 (* ------------------------------------------------------------------------- *)
 461 (* The Mangoldt function.                                                    *)
 462 (* ------------------------------------------------------------------------- *)
 463
 464 let mangoldt = new_definition
 465   `mangoldt d = if primepow d then ln(&(aprimedivisor d)) else &0`;;
 466
 467 let MANGOLDT_POS = prove
 468  (`!d. &0 <= mangoldt d`,
 469   GEN_TAC THEN REWRITE_TAC[mangoldt] THEN
 470   COND_CASES_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN
 471   ASM_MESON_TAC[APRIMEDIVISOR_PRIMEPOW; ARITH_RULE `2 <= a ==> 1 <= a`;
 472                 PRIME_GE_2; LN_POS; REAL_OF_NUM_LE; primepow]);;
 473
 474 (* ------------------------------------------------------------------------- *)
 475 (* The key lemma.                                                            *)
 476 (* ------------------------------------------------------------------------- *)
 477
 478 let LN_PRIMEFACT = prove
 479  (`!n. ~(n = 0)
 480        ==> (ln(&n) =
 481             sum(1,n) (\d. if primepow d /\ d divides n
 482                           then ln(&(aprimedivisor d)) else &0))`,
 483   MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN REPEAT STRIP_TAC THEN
 484   ASM_CASES_TAC `n = 1` THENL
 485    [MATCH_MP_TAC EQ_TRANS THEN
 486     EXISTS_TAC `sum(1,n) (\d. &0)` THEN CONJ_TAC THENL
 487      [ASM_REWRITE_TAC[SUM_0; LN_1]; ALL_TAC] THEN
 488     MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
 489     REWRITE_TAC[] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 490     ASM_MESON_TAC[PRIMEPOW_GE_2; DIVIDES_LE; NUM_REDUCE_CONV `2 <= 1`;
 491                   LE_TRANS];
 492     ALL_TAC] THEN
 493   FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_FACTOR) THEN
 494   DISCH_THEN(X_CHOOSE_THEN `p:num` MP_TAC) THEN
 495   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 496   GEN_REWRITE_TAC LAND_CONV [divides] THEN
 497   DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
 498   FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN
 499   RULE_ASSUM_TAC(REWRITE_RULE[MULT_EQ_0; DE_MORGAN_THM]) THEN
 500   ANTS_TAC THENL
 501    [ONCE_REWRITE_TAC[ARITH_RULE `m < p * m <=> 1 * m < p * m`] THEN
 502     SIMP_TAC[LT_MULT_RCANCEL; ARITH_RULE `1 < p <=> 2 <= p`] THEN
 503     ASM_SIMP_TAC[PRIME_GE_2];
 504     ALL_TAC] THEN
 505   ASM_REWRITE_TAC[] THEN
 506   REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
 507   ASM_SIMP_TAC[LN_MUL; REAL_OF_NUM_LT; ARITH_RULE `0 < n <=> ~(n = 0)`] THEN
 508   DISCH_THEN(K ALL_TAC) THEN
 509   SUBGOAL_THEN `?k. 1 <= k /\ (p EXP k) divides (p * m)` MP_TAC THENL
 510    [EXISTS_TAC `1` THEN SIMP_TAC[EXP_1; DIVIDES_RMUL; DIVIDES_REFL; LE_REFL];
 511     ALL_TAC] THEN
 512   SUBGOAL_THEN `?k. !j. 1 <= j /\ (p EXP j) divides (p * m) ==> j <= k`
 513   MP_TAC THENL
 514    [MP_TAC(SPECL [`p:num`; `p * m:num`] BIG_POWER_LEMMA) THEN
 515     ASM_SIMP_TAC[PRIME_GE_2] THEN
 516     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `k:num` THEN
 517     REPEAT STRIP_TAC THEN
 518     FIRST_X_ASSUM(MP_TAC o MATCH_MP DIVIDES_LE) THEN
 519     ASM_REWRITE_TAC[MULT_EQ_0] THEN
 520     ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[NOT_LE] THEN
 521     DISCH_TAC THEN MATCH_MP_TAC LET_TRANS THEN EXISTS_TAC `p EXP k` THEN
 522     ASM_REWRITE_TAC[LT_EXP] THEN ASM_SIMP_TAC[PRIME_GE_2];
 523     ALL_TAC] THEN
 524   GEN_REWRITE_TAC I [TAUT `a ==> b ==> c <=> b /\ a ==> c`] THEN
 525   GEN_REWRITE_TAC LAND_CONV [num_MAX] THEN
 526   DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN
 527   SUBGOAL_THEN
 528    `sum (1,m)
 529      (\d. if primepow d /\ d divides m then ln (&(aprimedivisor d)) else &0) =
 530     sum (1,p * m)
 531      (\d. if primepow d /\ d divides m then ln (&(aprimedivisor d)) else &0)`
 532   SUBST1_TAC THENL
 533    [ONCE_REWRITE_TAC[SUM_DIFF] THEN
 534     AP_THM_TAC THEN AP_TERM_TAC THEN
 535     SUBGOAL_THEN `1 + p * m = (1 + m) + (p * m - m)` SUBST1_TAC THENL
 536      [MATCH_MP_TAC(ARITH_RULE
 537         `1 * y <= x ==> (1 + x = (1 + y) + (x - y))`) THEN
 538       SIMP_TAC[LE_MULT_RCANCEL] THEN
 539       ASM_MESON_TAC[PRIME_GE_2; ARITH_RULE `2 <= p ==> 1 <= p`];
 540       ALL_TAC] THEN
 541     GEN_REWRITE_TAC RAND_CONV [GSYM SUM_TWO] THEN
 542     MATCH_MP_TAC(REAL_ARITH `(b = &0) ==> (a = a + b)`) THEN
 543     SUBGOAL_THEN
 544      `!d. d >= 1 + m
 545           ==> ((if primepow d /\ d divides m then ln (&(aprimedivisor d))
 546                 else &0) = &0)`
 547     MP_TAC THENL
 548      [X_GEN_TAC `d:num` THEN REWRITE_TAC[GE] THEN DISCH_TAC THEN
 549       COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 550       ASM_MESON_TAC[DIVIDES_LE; ARITH_RULE `~(1 + m <= d /\ d <= m)`];
 551       ALL_TAC] THEN
 552     DISCH_THEN(MP_TAC o MATCH_MP SUM_ZERO) THEN DISCH_THEN MATCH_MP_TAC THEN
 553     ARITH_TAC;
 554     ALL_TAC] THEN
 555   ONCE_REWRITE_TAC[SUM_DIFF] THEN REWRITE_TAC[SUM_1] THEN
 556   REWRITE_TAC[PRIMEPOW_0; REAL_SUB_RZERO] THEN
 557   SUBGOAL_THEN `1 + p * m = p EXP k + 1 + (p * m - p EXP k)` SUBST1_TAC THENL
 558    [MATCH_MP_TAC(ARITH_RULE `k <= p ==> (1 + p = k + 1 + (p - k))`) THEN
 559     ASM_MESON_TAC[DIVIDES_LE; MULT_EQ_0];
 560     ALL_TAC] THEN
 561   REWRITE_TAC[GSYM SUM_TWO] THEN
 562   MATCH_MP_TAC(REAL_ARITH
 563    `(a = a') /\ (l + b = c) ==> (l + a + b = a' + c)`) THEN
 564   CONJ_TAC THENL
 565    [MATCH_MP_TAC SUM_EQ THEN
 566     X_GEN_TAC `d:num` THEN REWRITE_TAC[ADD_CLAUSES; LE_0] THEN STRIP_TAC THEN
 567     ASM_CASES_TAC `primepow d` THEN ASM_REWRITE_TAC[] THEN
 568     SUBGOAL_THEN `d divides (p * m) <=> d divides m`
 569      (fun th -> REWRITE_TAC[th]) THEN
 570     UNDISCH_TAC `primepow d` THEN REWRITE_TAC[primepow] THEN
 571     DISCH_THEN(X_CHOOSE_THEN `q:num` MP_TAC) THEN
 572     DISCH_THEN(X_CHOOSE_THEN `j:num` MP_TAC) THEN
 573     REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 574     DISCH_THEN SUBST_ALL_TAC THEN ASM_CASES_TAC `q = p:num` THENL
 575      [FIRST_X_ASSUM SUBST_ALL_TAC THEN
 576       MATCH_MP_TAC(TAUT `(b ==> a) /\ b ==> (a <=> b)`) THEN
 577       REWRITE_TAC[DIVIDES_LMUL] THEN
 578       MATCH_MP_TAC DIVIDES_TRANS THEN
 579       EXISTS_TAC `p EXP (k - 1)` THEN CONJ_TAC THENL
 580        [REWRITE_TAC[divides] THEN EXISTS_TAC `p EXP ((k - 1) - j)` THEN
 581         REWRITE_TAC[GSYM EXP_ADD] THEN AP_TERM_TAC THEN
 582         UNDISCH_TAC `p EXP j < p EXP k` THEN ASM_REWRITE_TAC[LT_EXP] THEN
 583         ARITH_TAC;
 584         ALL_TAC] THEN
 585       UNDISCH_TAC `p EXP k divides (p * m)` THEN
 586       FIRST_ASSUM((fun th -> GEN_REWRITE_TAC (funpow 2 LAND_CONV o RAND_CONV)
 587                   [th]) o MATCH_MP
 588           (ARITH_RULE `1 <= k ==> (k = SUC(k - 1))`)) THEN
 589       REWRITE_TAC[divides; EXP] THEN MATCH_MP_TAC MONO_EXISTS THEN
 590       SIMP_TAC[GSYM MULT_ASSOC; EQ_MULT_LCANCEL] THEN
 591       ASM_REWRITE_TAC[];
 592       ALL_TAC] THEN
 593     EQ_TAC THEN REWRITE_TAC[DIVIDES_LMUL] THEN
 594     REWRITE_TAC[divides] THEN DISCH_THEN(X_CHOOSE_THEN `r:num` MP_TAC) THEN
 595     DISCH_THEN(fun th -> ASSUME_TAC th THEN
 596       MP_TAC(AP_TERM `(divides) p` th)) THEN
 597     SIMP_TAC[DIVIDES_RMUL; DIVIDES_REFL] THEN DISCH_TAC THEN
 598     SUBGOAL_THEN `p divides (q EXP j) \/ p divides r` MP_TAC THENL
 599      [ASM_MESON_TAC[PRIME_DIVPROD]; ALL_TAC] THEN
 600     DISCH_THEN DISJ_CASES_TAC THENL
 601      [SUBGOAL_THEN `p divides q` MP_TAC THENL
 602        [ASM_MESON_TAC[PRIME_DIVEXP]; ALL_TAC] THEN
 603       ASM_MESON_TAC[prime; PRIME_1];
 604       ALL_TAC] THEN
 605     UNDISCH_TAC `p * m = q EXP j * r` THEN
 606     UNDISCH_TAC `p divides r` THEN
 607     REWRITE_TAC[divides] THEN DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN
 608     ONCE_REWRITE_TAC[ARITH_RULE `a * b * c = b * a * c:num`] THEN
 609     SIMP_TAC[EQ_MULT_LCANCEL] THEN ASM_MESON_TAC[];
 610     ALL_TAC] THEN
 611   ONCE_REWRITE_TAC[GSYM SUM_SPLIT] THEN REWRITE_TAC[SUM_1] THEN
 612   REWRITE_TAC[REAL_ADD_ASSOC] THEN BINOP_TAC THENL
 613    [SUBGOAL_THEN `primepow (p EXP k)` ASSUME_TAC THENL
 614      [ASM_MESON_TAC[primepow]; ALL_TAC] THEN
 615     ASM_REWRITE_TAC[] THEN
 616     SUBGOAL_THEN `~((p EXP k) divides m)` ASSUME_TAC THENL
 617      [REWRITE_TAC[divides] THEN
 618       DISCH_THEN(X_CHOOSE_THEN `r:num` SUBST_ALL_TAC) THEN
 619       MP_TAC(ARITH_RULE `~(k + 1 <= k)`) THEN REWRITE_TAC[] THEN
 620       FIRST_ASSUM MATCH_MP_TAC THEN
 621       REWRITE_TAC[ARITH_RULE `1 <= k + 1`] THEN
 622       ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[EXP_ADD; EXP_1] THEN
 623       MESON_TAC[MULT_ASSOC; DIVIDES_REFL; DIVIDES_RMUL];
 624       ALL_TAC] THEN
 625     ASM_REWRITE_TAC[REAL_ADD_RID] THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
 626     ASM_MESON_TAC[APRIMEDIVISOR_PRIMEPOW];
 627     ALL_TAC] THEN
 628   MATCH_MP_TAC SUM_EQ THEN
 629   X_GEN_TAC `d:num` THEN REWRITE_TAC[ADD_CLAUSES; LE_0] THEN STRIP_TAC THEN
 630   ASM_CASES_TAC `primepow d` THEN ASM_REWRITE_TAC[] THEN
 631   SUBGOAL_THEN `d divides (p * m) <=> d divides m`
 632    (fun th -> REWRITE_TAC[th]) THEN
 633   UNDISCH_TAC `primepow d` THEN REWRITE_TAC[primepow] THEN
 634   DISCH_THEN(X_CHOOSE_THEN `q:num` MP_TAC) THEN
 635   DISCH_THEN(X_CHOOSE_THEN `j:num` MP_TAC) THEN
 636   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 637   ASM_CASES_TAC `q = p:num` THENL
 638    [UNDISCH_THEN `q = p:num` SUBST_ALL_TAC THEN
 639     DISCH_THEN SUBST_ALL_TAC THEN
 640     MATCH_MP_TAC(TAUT `(b ==> a) /\ ~a ==> (a <=> b)`) THEN
 641     REWRITE_TAC[DIVIDES_LMUL] THEN DISCH_TAC THEN
 642     FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE `a + 1 <= b ==> a < b`)) THEN
 643     REWRITE_TAC[LT_EXP] THEN ASM_SIMP_TAC[PRIME_GE_2; NOT_LT];
 644     ALL_TAC] THEN
 645   DISCH_THEN SUBST_ALL_TAC THEN EQ_TAC THEN REWRITE_TAC[DIVIDES_LMUL] THEN
 646   REWRITE_TAC[divides] THEN DISCH_THEN(X_CHOOSE_THEN `r:num` MP_TAC) THEN
 647   DISCH_THEN(fun th -> ASSUME_TAC th THEN
 648     MP_TAC(AP_TERM `(divides) p` th)) THEN
 649   SIMP_TAC[DIVIDES_RMUL; DIVIDES_REFL] THEN DISCH_TAC THEN
 650   SUBGOAL_THEN `p divides (q EXP j) \/ p divides r` MP_TAC THENL
 651    [ASM_MESON_TAC[PRIME_DIVPROD]; ALL_TAC] THEN
 652   DISCH_THEN DISJ_CASES_TAC THENL
 653    [SUBGOAL_THEN `p divides q` MP_TAC THENL
 654      [ASM_MESON_TAC[PRIME_DIVEXP]; ALL_TAC] THEN
 655     ASM_MESON_TAC[prime; PRIME_1];
 656     ALL_TAC] THEN
 657   UNDISCH_TAC `p * m = q EXP j * r` THEN
 658   UNDISCH_TAC `p divides r` THEN
 659   REWRITE_TAC[divides] THEN DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN
 660   ONCE_REWRITE_TAC[ARITH_RULE `a * b * c = b * a * c:num`] THEN
 661   SIMP_TAC[EQ_MULT_LCANCEL] THEN ASM_MESON_TAC[]);;
 662
 663 (* ------------------------------------------------------------------------- *)
 664 (* The key expansion using the Mangoldt function.                            *)
 665 (* ------------------------------------------------------------------------- *)
 666
 667 let MANGOLDT = prove
 668  (`!n. ln(&(FACT n)) = sum(1,n) (\d. mangoldt(d) * floor(&n / &d))`,
 669   GEN_TAC THEN REWRITE_TAC[LN_FACT] THEN MATCH_MP_TAC EQ_TRANS THEN
 670   EXISTS_TAC
 671    `sum(1,n) (\m. sum(1,n) (\d. if primepow d /\ d divides m
 672                                 then ln (&(aprimedivisor d))
 673                                 else &0))` THEN
 674   CONJ_TAC THENL
 675    [MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `d:num` THEN STRIP_TAC THEN
 676     ASM_SIMP_TAC[LN_PRIMEFACT; ARITH_RULE `~(n = 0) <=> 1 <= n`] THEN
 677     FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
 678      `d < n + 1 ==> (n = d + (n - d))`)) THEN
 679     DISCH_THEN(fun th ->
 680      GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV) [th]) THEN
 681     REWRITE_TAC[GSYM SUM_SPLIT] THEN
 682     REWRITE_TAC[REAL_ARITH `(a = a + b) <=> (b = &0)`] THEN
 683     MATCH_MP_TAC EQ_TRANS THEN
 684     EXISTS_TAC `sum(1 + d,n - d) (\k. &0)` THEN CONJ_TAC THENL
 685      [ALL_TAC; REWRITE_TAC[SUM_0]] THEN
 686     MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
 687     REWRITE_TAC[] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 688     ASM_MESON_TAC[DIVIDES_LE; ARITH_RULE
 689      `1 <= d /\ 1 + d <= r /\ (r <= d \/ (d = 0)) ==> F`];
 690     ALL_TAC] THEN
 691   ONCE_REWRITE_TAC[SUM_SWAP] THEN MATCH_MP_TAC SUM_EQ THEN
 692   X_GEN_TAC `d:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN
 693   REWRITE_TAC[mangoldt] THEN
 694   ASM_CASES_TAC `primepow d` THEN ASM_REWRITE_TAC[SUM_0; REAL_MUL_LZERO] THEN
 695   FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE `1 <= d ==> ~(d = 0)`)) THEN
 696   DISCH_THEN(MP_TAC o MATCH_MP DIVISION) THEN
 697   DISCH_THEN(MP_TAC o SPEC `n:num`) THEN
 698   MAP_EVERY ABBREV_TAC [`q = n DIV d`; `r = n MOD d`] THEN
 699   DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
 700   SUBGOAL_THEN `floor (&(q * d + r) / &d) = &q` SUBST1_TAC THENL
 701    [ONCE_REWRITE_TAC[GSYM FLOOR_UNIQUE] THEN
 702     REWRITE_TAC[INTEGER_CLOSED] THEN
 703     ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LT_LDIV_EQ;
 704                  REAL_OF_NUM_LT; ARITH_RULE `0 < d <=> 1 <= d`] THEN
 705     REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_MUL] THEN
 706     REWRITE_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN
 707     UNDISCH_TAC `r < d:num` THEN ARITH_TAC;
 708     ALL_TAC] THEN
 709   ONCE_REWRITE_TAC[GSYM SUM_SPLIT] THEN
 710   MATCH_MP_TAC(REAL_ARITH `(b = &0) /\ (a = c) ==> (a + b = c)`) THEN
 711   CONJ_TAC THENL
 712    [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `sum(1 + q * d,r) (\x. &0)` THEN
 713     CONJ_TAC THENL [ALL_TAC; REWRITE_TAC[SUM_0]] THEN
 714     MATCH_MP_TAC SUM_EQ THEN REWRITE_TAC[] THEN
 715     X_GEN_TAC `s:num` THEN STRIP_TAC THEN
 716     COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 717     UNDISCH_TAC `d divides s` THEN REWRITE_TAC[divides] THEN
 718     DISCH_THEN(X_CHOOSE_THEN `t:num` SUBST_ALL_TAC) THEN
 719     FIRST_X_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
 720      `1 + x <= y * z ==> x < z * y`)) THEN
 721     ASM_SIMP_TAC[LT_MULT_RCANCEL; ARITH_RULE `1 <= d ==> ~(d = 0)`] THEN
 722     REWRITE_TAC[LT_EXISTS] THEN
 723     DISCH_THEN(X_CHOOSE_THEN `e:num` SUBST_ALL_TAC) THEN
 724     UNDISCH_TAC `d * (q + SUC e) < r + 1 + q * d` THEN
 725     ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN DISCH_TAC THEN
 726     REWRITE_TAC[LEFT_ADD_DISTRIB; MULT_CLAUSES; GSYM ADD_ASSOC] THEN
 727     REWRITE_TAC[ARITH_RULE `d * q + x < y + 1 + q * d <=> x <= y`] THEN
 728     DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE `a + b <= c ==> a <= c:num`)) THEN
 729     ASM_REWRITE_TAC[NOT_LE];
 730     ALL_TAC] THEN
 731   ONCE_REWRITE_TAC[SUM_DIFF] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
 732   REWRITE_TAC[GSYM SUM_TWO] THEN
 733   SIMP_TAC[SUM_1; DIVIDES_0; DIVIDES_LMUL; DIVIDES_REFL] THEN
 734   REWRITE_TAC[REAL_ARITH `(a + b) - b = a`] THEN
 735   REWRITE_TAC[GSYM SUM_GROUP] THEN
 736   MATCH_MP_TAC EQ_TRANS THEN
 737   EXISTS_TAC `sum(0,q) (\x. ln (&(aprimedivisor d)))` THEN CONJ_TAC THENL
 738    [ALL_TAC; REWRITE_TAC[SUM_CONST; REAL_MUL_AC]] THEN
 739   MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `m:num` THEN STRIP_TAC THEN
 740   REWRITE_TAC[] THEN
 741   FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
 742     `1 <= d ==> (d = 1 + (d - 1))`)) THEN
 743   DISCH_THEN(fun th -> GEN_REWRITE_TAC
 744     (funpow 2 LAND_CONV o RAND_CONV) [th]) THEN
 745   REWRITE_TAC[GSYM SUM_SPLIT; SUM_1] THEN
 746   SIMP_TAC[DIVIDES_LMUL; DIVIDES_REFL] THEN
 747   MATCH_MP_TAC(REAL_ARITH `(b = &0) ==> (a + b = a)`) THEN
 748   MATCH_MP_TAC EQ_TRANS THEN
 749   EXISTS_TAC `sum(m * d + 1,d - 1) (\x. &0)` THEN CONJ_TAC THENL
 750    [ALL_TAC; REWRITE_TAC[SUM_0]] THEN
 751   MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `s:num` THEN
 752   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 753   GEN_REWRITE_TAC LAND_CONV [LE_EXISTS] THEN
 754   REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
 755   DISCH_THEN(X_CHOOSE_THEN `t:num` SUBST_ALL_TAC) THEN
 756   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 757   SUBGOAL_THEN `~(d divides (t + 1))` MP_TAC THENL
 758    [DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN
 759     UNDISCH_TAC `t + m * d + 1 < d - 1 + m * d + 1` THEN
 760     REWRITE_TAC[LT_ADD_RCANCEL] THEN
 761     UNDISCH_TAC `d divides (t + m * d + 1)` THEN
 762     ASM_CASES_TAC `t = 0` THEN ASM_REWRITE_TAC[ADD_CLAUSES] THENL
 763      [ASM_MESON_TAC[DIVIDES_REFL; DIVIDES_LMUL; DIVIDES_ADD_REVR;
 764                     DIVIDES_ONE; PRIMEPOW_GE_2; NUM_REDUCE_CONV `2 <= 1`];
 765       DISCH_TAC THEN ARITH_TAC];
 766     ALL_TAC] THEN
 767   UNDISCH_TAC `d divides (t + m * d + 1)` THEN
 768   ONCE_REWRITE_TAC[ARITH_RULE `t + m * d + 1 = (t + 1) + m * d`] THEN
 769   MESON_TAC[DIVIDES_REFL; DIVIDES_LMUL; DIVIDES_ADD_REVL]);;
 770
 771 (* ------------------------------------------------------------------------- *)
 772 (* The Chebyshev psi function.                                               *)
 773 (* ------------------------------------------------------------------------- *)
 774
 775 let psi = new_definition
 776   `psi(n) = sum(1,n) (\d. mangoldt(d))`;;
 777
 778 (* ------------------------------------------------------------------------- *)
 779 (* The key bounds on the psi function.                                       *)
 780 (* ------------------------------------------------------------------------- *)
 781
 782 let PSI_BOUNDS_LN_FACT = prove
 783  (`!n. ln(&(FACT(n))) - &2 * ln(&(FACT(n DIV 2))) <= psi(n) /\
 784        psi(n) - psi(n DIV 2) <= ln(&(FACT(n))) - &2 * ln(&(FACT(n DIV 2)))`,
 785   X_GEN_TAC `k:num` THEN MP_TAC(SPECL [`k:num`; `2`] DIVISION) THEN
 786   REWRITE_TAC[ARITH_EQ] THEN
 787   MAP_EVERY ABBREV_TAC [`n = k DIV 2`; `d = k MOD 2`] THEN
 788   POP_ASSUM_LIST(K ALL_TAC) THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
 789   DISCH_THEN(CONJUNCTS_THEN2 SUBST1_TAC ASSUME_TAC) THEN
 790   REWRITE_TAC[psi; MANGOLDT] THEN
 791   SUBGOAL_THEN
 792    `sum (1,n) (\d. mangoldt d * floor (&n / &d)) =
 793     sum (1,2 * n + d) (\d. mangoldt d * floor (&n / &d))`
 794   SUBST1_TAC THENL
 795    [REWRITE_TAC[ARITH_RULE `2 * n + d = n + (n + d)`] THEN
 796     ONCE_REWRITE_TAC[GSYM SUM_SPLIT] THEN
 797     REWRITE_TAC[REAL_ARITH `(a = a + b) <=> (b = &0)`] THEN
 798     MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `sum(1 + n,n + d) (\k. &0)` THEN
 799     CONJ_TAC THENL [ALL_TAC; REWRITE_TAC[SUM_0]] THEN
 800     MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
 801     REWRITE_TAC[REAL_ENTIRE] THEN DISJ2_TAC THEN REWRITE_TAC[FLOOR_EQ_0] THEN
 802     FIRST_ASSUM(ASSUME_TAC o MATCH_MP (ARITH_RULE
 803      `1 + n <= r ==> 0 < r`)) THEN
 804     ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LT_LDIV_EQ; REAL_OF_NUM_LT] THEN
 805     REWRITE_TAC[REAL_MUL_LZERO; REAL_POS; REAL_MUL_LID; REAL_OF_NUM_LT] THEN
 806     UNDISCH_TAC `1 + n <= r` THEN ARITH_TAC;
 807     ALL_TAC] THEN
 808   CONJ_TAC THENL
 809    [REWRITE_TAC[GSYM SUM_CMUL; GSYM SUM_SUB] THEN
 810     MATCH_MP_TAC SUM_LE THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
 811     REWRITE_TAC[REAL_ARITH `m * f - &2 * m * f' = m * (f - &2 * f')`] THEN
 812     GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
 813     MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[MANGOLDT_POS] THEN
 814     MATCH_MP_TAC(REAL_ARITH
 815      `&2 * a <= b /\ b <= &2 * a + &1
 816       ==> b - &2 * a <= &1`) THEN
 817     ASM_SIMP_TAC[FLOOR_DOUBLE_NUM; ARITH_RULE `0 < r <=> 1 <= r`];
 818     ALL_TAC] THEN
 819   SUBGOAL_THEN
 820    `sum(1,2 * n + d) (\d. mangoldt d) - sum(1,n) (\d. mangoldt d) =
 821     sum(1,2 * n + d) (\d. if d <= n then &0 else mangoldt d)`
 822   SUBST1_TAC THENL
 823    [REWRITE_TAC[ARITH_RULE `2 * n + d = n + (n + d)`] THEN
 824     ONCE_REWRITE_TAC[GSYM SUM_SPLIT] THEN
 825     MATCH_MP_TAC(REAL_ARITH
 826      `(c = &0) /\ (b = d) ==> ((a + b) - a = c + d)`) THEN
 827     CONJ_TAC THENL
 828      [MATCH_MP_TAC EQ_TRANS THEN
 829       EXISTS_TAC `sum(1,n) (\k. &0)` THEN CONJ_TAC THENL
 830        [ALL_TAC; REWRITE_TAC[SUM_0]] THEN
 831       MATCH_MP_TAC SUM_EQ THEN
 832       SIMP_TAC[ARITH_RULE `r < n + 1 <=> r <= n`];
 833       ALL_TAC] THEN
 834     MATCH_MP_TAC SUM_EQ THEN
 835     SIMP_TAC[ARITH_RULE `1 + n <= r ==> ~(r <= n)`];
 836     ALL_TAC] THEN
 837   REWRITE_TAC[GSYM SUM_CMUL; GSYM SUM_SUB] THEN MATCH_MP_TAC SUM_LE THEN
 838   X_GEN_TAC `r:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN
 839   REWRITE_TAC[REAL_ARITH `m * a - &2 * m * b = m * (a - &2 * b)`] THEN
 840   COND_CASES_TAC THENL
 841    [MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[MANGOLDT_POS] THEN
 842     ASM_SIMP_TAC[REAL_SUB_LE; FLOOR_DOUBLE_NUM; ARITH_RULE `0 < r <=> 1 <= r`];
 843     ALL_TAC] THEN
 844   GEN_REWRITE_TAC LAND_CONV [REAL_ARITH `a = a * &1`] THEN
 845   MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[MANGOLDT_POS] THEN
 846   MATCH_MP_TAC(REAL_ARITH `(b = &0) /\ &1 <= a ==> &1 <= a - &2 * b`) THEN
 847   CONJ_TAC THENL
 848    [REWRITE_TAC[FLOOR_EQ_0] THEN
 849     ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LT_LDIV_EQ; REAL_OF_NUM_LT;
 850                  ARITH_RULE `0 < r <=> 1 <= r`] THEN
 851     REWRITE_TAC[REAL_MUL_LZERO; REAL_MUL_LID; REAL_POS] THEN
 852     ASM_REWRITE_TAC[REAL_OF_NUM_LT] THEN ASM_REWRITE_TAC[GSYM NOT_LE];
 853     ALL_TAC] THEN
 854   MATCH_MP_TAC(REAL_ARITH `(a = &1) ==> &1 <= a`) THEN
 855   REWRITE_TAC[GSYM FLOOR_UNIQUE; INTEGER_CLOSED] THEN
 856   ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LT_LDIV_EQ; REAL_OF_NUM_LT;
 857                ARITH_RULE `0 < r <=> 1 <= r`] THEN
 858   REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
 859   REWRITE_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_LT; REAL_OF_NUM_MUL;
 860               REAL_OF_NUM_ADD] THEN
 861   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN ARITH_TAC);;
 862
 863 (* ------------------------------------------------------------------------- *)
 864 (* Map the middle term into multiples of log(n).                             *)
 865 (* ------------------------------------------------------------------------- *)
 866
 867 let LN_FACT_DIFF_BOUNDS = prove
 868  (`!n. abs((ln(&(FACT(n))) - &2 * ln(&(FACT(n DIV 2)))) - &n * ln(&2))
 869        <= &4 * ln(if n = 0 then &1 else &n) + &3`,
 870   REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THENL
 871    [ASM_SIMP_TAC[FACT; MULT_CLAUSES; LN_1; DIV_0; ARITH_EQ] THEN
 872     REWRITE_TAC[REAL_MUL_LZERO] THEN CONV_TAC REAL_RAT_REDUCE_CONV;
 873     ALL_TAC] THEN
 874   MP_TAC(SPECL [`n:num`; `2`] DIVISION) THEN ASM_REWRITE_TAC[ARITH_EQ] THEN
 875   MAP_EVERY ABBREV_TAC [`q = n DIV 2`; `r = n MOD 2`] THEN
 876   DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
 877   ASM_CASES_TAC `q = 0` THENL
 878    [UNDISCH_TAC `~(q * 2 + r = 0)` THEN
 879     ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
 880     ASM_SIMP_TAC[ARITH_RULE `r < 2 ==> ((r = 0) <=> ~(r = 1))`] THEN
 881     DISCH_THEN SUBST_ALL_TAC THEN
 882     REWRITE_TAC[num_CONV `1`; FACT; MULT_CLAUSES] THEN
 883     CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[LN_1] THEN
 884     REWRITE_TAC[REAL_MUL_RZERO; REAL_SUB_LZERO; REAL_SUB_RZERO] THEN
 885     REWRITE_TAC[REAL_NEG_0; REAL_SUB_LZERO; REAL_ADD_LID; REAL_MUL_LID] THEN
 886     REWRITE_TAC[REAL_ABS_NEG] THEN
 887     MATCH_MP_TAC(REAL_ARITH `x <= &2 ==> x <= &3`) THEN
 888     SUBST1_TAC(REAL_ARITH `&2 = &1 + &1`) THEN
 889     MATCH_MP_TAC(REAL_ARITH
 890      `&0 <= x /\ x <= &1 ==> abs(x) <= &1 + &1`) THEN
 891     ASM_SIMP_TAC[LN_POS; LN_LE; REAL_OF_NUM_LE; ARITH; REAL_LE_ADDL];
 892     ALL_TAC] THEN
 893   MATCH_MP_TAC(REAL_ARITH
 894    `!a'. abs((a' - b) - c) <= d - abs(a' - a) ==> abs((a - b) - c) <= d`) THEN
 895   EXISTS_TAC `ln(&(FACT(q * 2)))` THEN
 896   MP_TAC(SPEC `q:num` LN_FACT_BOUNDS) THEN
 897   MP_TAC(SPEC `q * 2` LN_FACT_BOUNDS) THEN
 898   ASM_REWRITE_TAC[MULT_EQ_0; ARITH_EQ] THEN
 899   MATCH_MP_TAC(REAL_ARITH
 900    `abs(a - (a2 - &2 * a1)) <= b - &2 * b1 - b2
 901     ==> abs(l2 - a2) <= b2
 902         ==> abs(l1 - a1) <= b1
 903             ==> abs((l2 - &2 * l1) - a) <= b`) THEN
 904   REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] THEN
 905   ASM_SIMP_TAC[LN_MUL; REAL_OF_NUM_LT; ARITH;
 906                ARITH_RULE `0 < q <=> ~(q = 0)`] THEN
 907   REWRITE_TAC[REAL_ARITH
 908    `(q * &2 + r) * l2 - ((q * &2) * (lq + l2) - q * &2 - &2 * (q * lq - q)) =
 909     r * l2`] THEN
 910   ONCE_REWRITE_TAC[REAL_ARITH
 911    `x <= a - b - c - d <=> x + b <= a - c - d`] THEN
 912   MATCH_MP_TAC REAL_LE_TRANS THEN
 913   EXISTS_TAC `ln(&2) + ln(&q * &2 + &r)` THEN CONJ_TAC THENL
 914    [MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL
 915      [MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ x <= &1 * y ==> abs(x) <= y`) THEN
 916       SIMP_TAC[LN_POS_LT; REAL_LT_IMP_LE; REAL_LE_RMUL_EQ;
 917                REAL_LE_MUL; REAL_POS; REAL_OF_NUM_LT; ARITH] THEN
 918       REWRITE_TAC[REAL_OF_NUM_LE] THEN UNDISCH_TAC `r < 2` THEN ARITH_TAC;
 919       ALL_TAC] THEN
 920     FIRST_ASSUM(DISJ_CASES_THEN SUBST1_TAC o MATCH_MP (ARITH_RULE
 921      `r < 2 ==> (r = 0) \/ (r = 1)`))
 922     THENL
 923      [REWRITE_TAC[ADD_CLAUSES; REAL_SUB_REFL; REAL_ADD_RID; REAL_ABS_NUM] THEN
 924       MATCH_MP_TAC LN_POS THEN
 925       REWRITE_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_MUL] THEN
 926       UNDISCH_TAC `~(q = 0)` THEN ARITH_TAC;
 927       ALL_TAC] THEN
 928     REWRITE_TAC[GSYM ADD1; FACT] THEN
 929     SIMP_TAC[GSYM REAL_OF_NUM_MUL; LN_MUL; REAL_OF_NUM_LT;
 930              FACT_LT; LT_0] THEN
 931     REWRITE_TAC[REAL_ARITH `abs(b - (a + b)) = abs a`] THEN
 932     REWRITE_TAC[ADD1; GSYM REAL_OF_NUM_SUC; GSYM REAL_OF_NUM_ADD;
 933                 GSYM REAL_OF_NUM_MUL] THEN
 934     MATCH_MP_TAC(REAL_ARITH `&0 <= x ==> abs(x) <= x`) THEN
 935     MATCH_MP_TAC LN_POS THEN
 936     REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_MUL; REAL_OF_NUM_LE] THEN
 937     ARITH_TAC;
 938     ALL_TAC] THEN
 939   REWRITE_TAC[REAL_ARITH
 940    `l2 + lnn <= (&4 * lnn + &3) - a - b
 941     <=> a + b + l2 <= &3 * lnn + &3`] THEN
 942   MATCH_MP_TAC REAL_LE_TRANS THEN
 943   EXISTS_TAC `&3 * ln(&q * &2) + &3` THEN CONJ_TAC THENL
 944    [ALL_TAC;
 945     SIMP_TAC[REAL_LE_RADD; REAL_LE_LMUL_EQ; REAL_OF_NUM_LT; ARITH] THEN
 946     ASM_SIMP_TAC[LN_MONO_LE; REAL_POS; REAL_OF_NUM_LT;
 947                  ARITH_RULE `0 < q <=> ~(q = 0)`;
 948                  REAL_ARITH `&0 < q /\ &0 <= r ==> &0 < q * &2 + r`;
 949                  REAL_ARITH `&0 < q ==> &0 < q * &2`] THEN
 950     REWRITE_TAC[REAL_LE_ADDR; REAL_POS]] THEN
 951   ASM_SIMP_TAC[LN_MUL; REAL_OF_NUM_LT; ARITH;
 952                ARITH_RULE `0 < q <=> ~(q = 0)`] THEN
 953   SUBGOAL_THEN `&0 <= ln(&2)` (fun th -> MP_TAC th THEN REAL_ARITH_TAC) THEN
 954   MATCH_MP_TAC LN_POS THEN REWRITE_TAC[REAL_OF_NUM_LE; ARITH]);;
 955
 956 (* ------------------------------------------------------------------------- *)
 957 (* Hence overall bounds in terms of n * log(2) + constant.                   *)
 958 (* ------------------------------------------------------------------------- *)
 959
 960 let PSI_BOUNDS_INDUCT = prove
 961  (`!n. &n * ln(&2) - (&4 * ln (if n = 0 then &1 else &n) + &3) <= psi(n) /\
 962        psi(n) - psi(n DIV 2)
 963        <= &n * ln(&2) + (&4 * ln (if n = 0 then &1 else &n) + &3)`,
 964   MESON_TAC[PSI_BOUNDS_LN_FACT; LN_FACT_DIFF_BOUNDS; REAL_ARITH
 965              `m <= a /\ b <= m /\ abs(m - n) <= k
 966               ==> n - k <= a /\ b <= n + k`]);;
 967
 968 (* ------------------------------------------------------------------------- *)
 969 (* Evaluation of mangoldt(numeral).                                          *)
 970 (* ------------------------------------------------------------------------- *)
 971
 972 let MANGOLDT_CONV =
 973   GEN_REWRITE_CONV I [mangoldt] THENC
 974   RATOR_CONV(LAND_CONV PRIMEPOW_CONV) THENC
 975   GEN_REWRITE_CONV I [COND_CLAUSES] THENC
 976   TRY_CONV(funpow 2 RAND_CONV APRIMEDIVISOR_CONV);;
 977
 978 (* ------------------------------------------------------------------------- *)
 979 (* More efficient version without two primality tests.                       *)
 980 (* ------------------------------------------------------------------------- *)
 981
 982 let MANGOLDT_CONV =
 983   let pth0 = prove
 984    (`mangoldt 0 = ln(&1)`,
 985     REWRITE_TAC[mangoldt; primepow; LN_1] THEN
 986     COND_CASES_TAC THEN ASM_MESON_TAC[EXP_EQ_0; PRIME_0])
 987   and pth1 = prove
 988    (`mangoldt 1 = ln(&1)`,
 989     REWRITE_TAC[mangoldt; primepow; LN_1] THEN COND_CASES_TAC THEN
 990     ASM_MESON_TAC[EXP_EQ_1; PRIME_1; NUM_REDUCE_CONV `1 <= 0`])
 991   and pth2 = prove
 992    (`prime p ==> 1 <= k /\ (q = p EXP k) ==> (mangoldt q = ln(&p))`,
 993     SIMP_TAC[mangoldt; APRIMEDIVISOR_PRIMEPOW] THEN
 994     COND_CASES_TAC THEN ASM_MESON_TAC[primepow])
 995   and pth3 = prove
 996    (`(p * x = r * y + 1) /\ ~(p = 1) /\ ~(r = 1) /\ (q = p * r * d)
 997      ==> (mangoldt q = ln(&1))`,
 998     REPEAT STRIP_TAC THEN
 999     SUBGOAL_THEN `~(primepow q)`
1000      (fun th -> REWRITE_TAC[LN_1; th; mangoldt]) THEN
1001     REWRITE_TAC[primepow] THEN
1002     DISCH_THEN(X_CHOOSE_THEN `P:num` MP_TAC) THEN
1003     DISCH_THEN(X_CHOOSE_THEN `k:num` MP_TAC) THEN
1004     REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1005     DISCH_THEN SUBST_ALL_TAC THEN
1006     MP_TAC(SPEC `r:num` PRIME_FACTOR) THEN
1007     MP_TAC(SPEC `p:num` PRIME_FACTOR) THEN
1008     ASM_REWRITE_TAC[] THEN
1009     DISCH_THEN(X_CHOOSE_THEN `P_p:num` MP_TAC) THEN
1010     REWRITE_TAC[divides] THEN
1011     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1012     DISCH_THEN(X_CHOOSE_THEN `d_p:num` SUBST_ALL_TAC) THEN
1013     DISCH_THEN(X_CHOOSE_THEN `P_r:num` MP_TAC) THEN
1014     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1015     DISCH_THEN(X_CHOOSE_THEN `d_r:num` SUBST_ALL_TAC) THEN
1016     SUBGOAL_THEN `P_p divides P /\ P_r divides P` ASSUME_TAC THENL
1017      [CONJ_TAC THEN MATCH_MP_TAC PRIME_DIVEXP THEN EXISTS_TAC `k:num` THEN
1018       ASM_MESON_TAC[divides; MULT_AC]; ALL_TAC] THEN
1019     SUBGOAL_THEN `(P_p = P) /\ (P_r = P:num)` (CONJUNCTS_THEN SUBST_ALL_TAC)
1020     THENL [ASM_MESON_TAC[prime]; ALL_TAC] THEN
1021     ASM_MESON_TAC[DIVIDES_ADD_REVR; divides; MULT_AC; DIVIDES_ONE; prime])
1022   and p_tm = `p:num` and k_tm = `k:num` and q_tm = `q:num`
1023   and r_tm = `r:num` and d_tm = `d:num`
1024   and x_tm = `x:num` and y_tm = `y:num` and mangoldt_tm = `mangoldt` in
1025   fun tm0 ->
1026     let ptm,tm = dest_comb tm0 in
1027     if ptm <> mangoldt_tm then failwith "expected mangoldt(numeral)" else
1028     let q = dest_numeral tm in
1029     if q =/ Int 0 then pth0
1030     else if q =/ Int 1 then pth1 else
1031     match factor q with
1032       [] -> failwith "internal failure in MANGOLDT_CONV"
1033     | [p,k] -> let th1 = INST [mk_numeral q,q_tm;
1034                                mk_numeral p,p_tm;
1035                                mk_numeral k,k_tm] pth2 in
1036                let th2 = MP th1 (EQT_ELIM(PRIME_CONV(lhand(concl th1)))) in
1037                MP th2 (EQT_ELIM(NUM_REDUCE_CONV(lhand(concl th2))))
1038     | (p,_)::(r,_)::_ ->
1039                let d = q // (p */ r) in
1040                let (x,y) = bezout(p,r) in
1041                let p,r,x,y =
1042                  if x </ Int 0 then r,p,y,minus_num x
1043                  else p,r,x,minus_num y in
1044                let th1 = INST [mk_numeral q,q_tm;
1045                                mk_numeral p,p_tm;
1046                                mk_numeral r,r_tm;
1047                                mk_numeral x,x_tm;
1048                                mk_numeral y,y_tm;
1049                                mk_numeral d,d_tm] pth3 in
1050                MP th1 (EQT_ELIM(NUM_REDUCE_CONV(lhand(concl th1))));;
1051
1052 (* ------------------------------------------------------------------------- *)
1053 (* Hence an evaluation function for psi, applied to all n <= some N.         *)
1054 (* ------------------------------------------------------------------------- *)
1055
1056 let PSI_LIST =
1057   let PSI_0 = prove
1058    (`psi(0) = ln(&1)`,
1059     REWRITE_TAC[psi; sum; LN_1])
1060   and PSI_SUC = prove
1061    (`psi(SUC n) = psi(n) + mangoldt(SUC n)`,
1062     REWRITE_TAC[psi; sum; ADD1] THEN REWRITE_TAC[ADD_AC])
1063   and n_tm = `n:num`
1064   and SIMPER_CONV =
1065     SIMP_CONV [REAL_ADD_RID; GSYM LN_MUL; REAL_OF_NUM_MUL;
1066                REAL_OF_NUM_LT; ARITH] in
1067   let rec PSI_LIST n =
1068     if n = 0 then [PSI_0] else
1069     let ths = PSI_LIST (n - 1) in
1070     let th1 = INST [mk_small_numeral(n-1),n_tm] PSI_SUC in
1071     let th2 = GEN_REWRITE_RULE (RAND_CONV o LAND_CONV) [hd ths] th1 in
1072     let th3 = CONV_RULE(COMB_CONV (funpow 2 RAND_CONV NUM_SUC_CONV)) th2 in
1073     let th4 = CONV_RULE (funpow 2 RAND_CONV MANGOLDT_CONV) th3 in
1074     (CONV_RULE(RAND_CONV SIMPER_CONV) th4)::ths in
1075   PSI_LIST;;
1076
1077 (* ------------------------------------------------------------------------- *)
1078 (* Run it up to 300.                                                         *)
1079 (* ------------------------------------------------------------------------- *)
1080
1081 let PSI_LIST_300 = PSI_LIST 300;;
1082
1083 (* ------------------------------------------------------------------------- *)
1084 (* Prove a sharpish linear bound on psi(n) for n <= 128.                     *)
1085 (* ------------------------------------------------------------------------- *)
1086
1087 let PSI_UBOUND_128 = prove
1088  (`!n. n <= 128 ==> psi(n) <= &133 / &128 * &n`,
1089   let lemma = prove
1090    (`a <= b /\ l <= a /\ rest ==> l <= a /\ l <= b /\ rest`,
1091     MESON_TAC[REAL_LE_TRANS])
1092   and tac = time (CONV_TAC(LAND_CONV LN_N2_CONV THENC REALCALC_REL_CONV)) in
1093   REWRITE_TAC[ARITH_RULE `n <= 128 <=> n < 129`] THEN
1094   CONV_TAC EXPAND_CASES_CONV THEN REWRITE_TAC(PSI_LIST_300) THEN
1095   REWRITE_TAC[LN_1] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
1096   REPEAT
1097    ((MATCH_MP_TAC lemma THEN
1098      CONV_TAC(LAND_CONV REAL_RAT_REDUCE_CONV) THEN
1099      GEN_REWRITE_TAC I [TAUT `T /\ a <=> a`])
1100     ORELSE
1101      (CONJ_TAC THENL [tac THEN NO_TAC; ALL_TAC])
1102     ORELSE tac));;
1103
1104 (* ------------------------------------------------------------------------- *)
1105 (* As a multiple of log(2) is often more useful.                             *)
1106 (* ------------------------------------------------------------------------- *)
1107
1108 let PSI_UBOUND_128_LOG = prove
1109  (`!n. n <= 128 ==> psi(n) <= (&3 / &2 * ln(&2)) * &n`,
1110   GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP PSI_UBOUND_128) THEN
1111   MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
1112   MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_POS] THEN
1113   CONV_TAC(ONCE_DEPTH_CONV LN_N2_CONV THENC REALCALC_REL_CONV));;
1114
1115 (* ------------------------------------------------------------------------- *)
1116 (* Useful "overpowering" lemma.                                              *)
1117 (* ------------------------------------------------------------------------- *)
1118
1119 let OVERPOWER_LEMMA = prove
1120  (`!f g d a.
1121         f(a) <= g(a) /\
1122         (!x. a <= x ==> ((\x. g(x) - f(x)) diffl (d(x)))(x)) /\
1123         (!x. a <= x ==> &0 <= d(x))
1124         ==> !x. a <= x ==> f(x) <= g(x)`,
1125   REPEAT STRIP_TAC THEN
1126   MP_TAC(SPECL [`\x:real. g(x) - f(x)`; `d:real->real`; `a:real`; `x:real`]
1127                MVT_ALT) THEN
1128   UNDISCH_TAC `a <= x` THEN GEN_REWRITE_TAC LAND_CONV [REAL_LE_LT] THEN
1129   ASM_CASES_TAC `x:real = a` THEN ASM_REWRITE_TAC[] THEN
1130   ASM_SIMP_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
1131   DISCH_THEN(X_CHOOSE_THEN `z:real` MP_TAC) THEN
1132   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1133   MATCH_MP_TAC(REAL_ARITH
1134    `fa <= ga /\ &0 <= d ==> (gx - fx - (ga - fa) = d) ==> fx <= gx`) THEN
1135   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_MUL THEN
1136   ASM_SIMP_TAC[REAL_SUB_LE; REAL_LT_IMP_LE]);;
1137
1138 (* ------------------------------------------------------------------------- *)
1139 (* Repeatedly extend range of explicit cases using recurrence.               *)
1140 (* ------------------------------------------------------------------------- *)
1141
1142 let DOUBLE_CASES_RULE th =
1143   let bod = snd(dest_forall(concl th)) in
1144   let ant,cons = dest_imp bod in
1145   let m = dest_numeral (rand ant)
1146   and c = rat_of_term (lhand(lhand(rand cons))) in
1147   let x = float_of_num(m +/ Int 1) in
1148   let d = (4.0 *. log x +. 3.0) /. (x *. log 2.0) in
1149   let c' = c // Int 2 +/ Int 1 +/
1150            (floor_num(num_of_float(1024.0 *. d)) +/ Int 2) // Int 1024 in
1151   let c'' = max_num c c' in
1152   let tm = mk_forall
1153    (`n:num`,
1154     subst [mk_numeral(Int 2 */ m),rand ant;
1155           term_of_rat c'',lhand(lhand(rand cons))] bod) in
1156   prove(tm,
1157     REPEAT STRIP_TAC THEN
1158     ASM_CASES_TAC (mk_comb(`(<=) (n:num)`,mk_numeral m)) THENL
1159      [FIRST_ASSUM(MP_TAC o MATCH_MP th) THEN
1160       MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
1161       MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_POS] THEN
1162       MATCH_MP_TAC REAL_LE_RMUL THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
1163       MATCH_MP_TAC LN_POS THEN CONV_TAC REAL_RAT_REDUCE_CONV;
1164       ALL_TAC] THEN
1165     MP_TAC(SPEC `n:num` PSI_BOUNDS_INDUCT) THEN
1166     SUBGOAL_THEN `~(n = 0)` (fun th -> REWRITE_TAC[th]) THENL
1167      [FIRST_ASSUM(UNDISCH_TAC o check is_neg o concl) THEN ARITH_TAC;
1168       ALL_TAC] THEN
1169     MATCH_MP_TAC(REAL_ARITH
1170      `pn2 <= ((a - &1) * l2) * n - logtm
1171       ==> u <= v /\ pn - pn2 <= n * l2 + logtm ==> pn <= (a * l2) * n`) THEN
1172     MP_TAC(SPEC `n DIV 2` th) THEN
1173     ANTS_TAC THENL
1174      [ASM_SIMP_TAC[LE_LDIV_EQ; ARITH] THEN
1175       FIRST_ASSUM(UNDISCH_TAC o check ((not) o is_neg) o concl) THEN
1176       ARITH_TAC;
1177       ALL_TAC] THEN
1178     MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
1179     W(fun (asl,w) ->
1180        MATCH_MP_TAC REAL_LE_TRANS THEN
1181        EXISTS_TAC(mk_comb(rator(lhand w),`&n / &2`))) THEN
1182     CONJ_TAC THENL
1183      [MATCH_MP_TAC REAL_LE_LMUL THEN CONJ_TAC THENL
1184        [MATCH_MP_TAC REAL_LE_MUL THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
1185         MATCH_MP_TAC LN_POS THEN CONV_TAC REAL_RAT_REDUCE_CONV;
1186         ALL_TAC] THEN
1187       SIMP_TAC[REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
1188       REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_LE] THEN
1189       MP_TAC(SPECL [`n:num`; `2`] DIVISION) THEN ARITH_TAC;
1190       ALL_TAC] THEN
1191     GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [real_div] THEN
1192     MATCH_MP_TAC(REAL_ARITH
1193      `logtm <= ((c - a * b) * l2) * n
1194       ==> (a * l2) * n * b <= (c * l2) * n - logtm`) THEN
1195     CONV_TAC REAL_RAT_REDUCE_CONV THEN
1196     SUBST1_TAC(REAL_ARITH `&n = &1 + (&n - &1)`) THEN
1197     FIRST_X_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
1198      `~(n <= b) ==> b + 1 <= n`)) THEN
1199     GEN_REWRITE_TAC LAND_CONV [GSYM REAL_OF_NUM_LE] THEN
1200     DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
1201      `a <= n ==> a - &1 <= n - &1`)) THEN
1202     ABBREV_TAC `x = &n - &1` THEN
1203     CONV_TAC(LAND_CONV NUM_REDUCE_CONV THENC REAL_RAT_REDUCE_CONV) THEN
1204     SPEC_TAC(`x:real`,`x:real`) THEN POP_ASSUM_LIST(K ALL_TAC) THEN
1205     MATCH_MP_TAC OVERPOWER_LEMMA THEN
1206     W(fun (asl,w) ->
1207         let th = DIFF_CONV
1208          (lhand(rator(rand(body(rand(lhand(rand(body(rand w))))))))) in
1209         MP_TAC th) THEN
1210     GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV)
1211      [REAL_MUL_LZERO; REAL_ADD_LID; REAL_ADD_RID;
1212       REAL_MUL_RID; REAL_MUL_LID] THEN
1213     W(fun (asl,w) ->
1214         let tm = mk_abs(`x:real`,rand(rator(rand(body(rand(lhand w)))))) in
1215         DISCH_TAC THEN EXISTS_TAC tm) THEN
1216     CONJ_TAC THENL
1217      [CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[real_sub] THEN
1218       CONV_TAC(ONCE_DEPTH_CONV LN_N2_CONV) THEN
1219       CONV_TAC REALCALC_REL_CONV;
1220       ALL_TAC] THEN
1221     REWRITE_TAC[] THEN CONJ_TAC THENL
1222      [GEN_TAC THEN
1223       DISCH_THEN(fun th -> FIRST_ASSUM MATCH_MP_TAC THEN MP_TAC th) THEN
1224       REAL_ARITH_TAC;
1225       ALL_TAC] THEN
1226     X_GEN_TAC `x:real` THEN DISCH_TAC THEN REWRITE_TAC[REAL_SUB_LE] THEN
1227     SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
1228     FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
1229      `a <= x ==> inv(&1 + x) <= inv(&1 + a) /\
1230                  inv(&1 + a) <= b ==> inv(&1 + x) <= b`)) THEN
1231     CONJ_TAC THENL
1232      [MATCH_MP_TAC REAL_LE_INV2 THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
1233       POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
1234       ALL_TAC] THEN
1235     SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
1236     GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
1237     SIMP_TAC[GSYM REAL_LE_LDIV_EQ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
1238     CONV_TAC REAL_RAT_REDUCE_CONV THEN
1239     CONV_TAC(ONCE_DEPTH_CONV LN_N2_CONV) THEN CONV_TAC REALCALC_REL_CONV);;
1240
1241 (* ------------------------------------------------------------------------- *)
1242 (* Bring it to the self-sustaining point.                                    *)
1243 (* ------------------------------------------------------------------------- *)
1244
1245 let PSI_UBOUND_1024_LOG = funpow 3 DOUBLE_CASES_RULE PSI_UBOUND_128_LOG;;
1246
1247 (* ------------------------------------------------------------------------- *)
1248 (* A generic proof of the same kind that we're self-sustaining.              *)
1249 (* ------------------------------------------------------------------------- *)
1250
1251 let PSI_BOUNDS_SUSTAINED_INDUCT = prove
1252  (`&4 * ln(&1 + &2 pow j) + &3 <= (d * ln(&2)) * (&1 + &2 pow j) /\
1253    &4 / (&1 + &2 pow j) <= d * ln(&2) /\ &0 <= c /\ c / &2 + d + &1 <= c
1254    ==> !k. j <= k /\
1255            (!n. n <= 2 EXP k ==> psi(n) <= (c * ln(&2)) * &n)
1256            ==> !n. n <= 2 EXP (SUC k) ==> psi(n) <= (c * ln(&2)) * &n`,
1257   REPEAT STRIP_TAC THEN ASM_CASES_TAC `n <= 2 EXP k` THEN ASM_SIMP_TAC[] THEN
1258   MP_TAC(SPEC `n:num` PSI_BOUNDS_INDUCT) THEN
1259   SUBGOAL_THEN `~(n = 0)` (fun th -> REWRITE_TAC[th]) THENL
1260    [MATCH_MP_TAC(ARITH_RULE `!a. ~(a = 0) /\ ~(n <= a) ==> ~(n = 0)`) THEN
1261     EXISTS_TAC `2 EXP k` THEN ASM_REWRITE_TAC[EXP_EQ_0; ARITH_EQ];
1262     ALL_TAC] THEN
1263   MATCH_MP_TAC(REAL_ARITH
1264    `pn2 <= ((a - &1) * l2) * n - logtm
1265     ==> u <= v /\ pn - pn2 <= n * l2 + logtm ==> pn <= (a * l2) * n`) THEN
1266   FIRST_X_ASSUM(MP_TAC o SPEC `n DIV 2`) THEN
1267   ANTS_TAC THENL
1268    [ASM_SIMP_TAC[LE_LDIV_EQ; ARITH] THEN
1269     MATCH_MP_TAC(ARITH_RULE `n <= 2 * k ==> n < 2 * (k + 1)`) THEN
1270     ASM_REWRITE_TAC[GSYM(CONJUNCT2 EXP)];
1271     ALL_TAC] THEN
1272   MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
1273   W(fun (asl,w) ->
1274      MATCH_MP_TAC REAL_LE_TRANS THEN
1275      EXISTS_TAC(mk_comb(rator(lhand w),`&n / &2`))) THEN
1276   CONJ_TAC THENL
1277    [MATCH_MP_TAC REAL_LE_LMUL THEN CONJ_TAC THENL
1278      [MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN
1279       MATCH_MP_TAC LN_POS THEN CONV_TAC REAL_RAT_REDUCE_CONV;
1280       ALL_TAC] THEN
1281     SIMP_TAC[REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
1282     REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_LE] THEN
1283     MP_TAC(SPECL [`n:num`; `2`] DIVISION) THEN ARITH_TAC;
1284     ALL_TAC] THEN
1285   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [real_div] THEN
1286   MATCH_MP_TAC(REAL_ARITH
1287    `logtm <= ((c - a * b) * l2) * n
1288     ==> (a * l2) * n * b <= (c * l2) * n - logtm`) THEN
1289   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(d * ln (&2)) * &n` THEN
1290   CONJ_TAC THENL
1291    [ALL_TAC;
1292     MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_POS] THEN
1293     MATCH_MP_TAC REAL_LE_RMUL THEN SIMP_TAC[LN_POS; REAL_OF_NUM_LE; ARITH] THEN
1294     REWRITE_TAC[GSYM real_div] THEN
1295     ASM_REWRITE_TAC[REAL_ARITH `d <= c - &1 - c2 <=> c2 + d + &1 <= c`]] THEN
1296   SUBST1_TAC(REAL_ARITH `&n = &1 + (&n - &1)`) THEN
1297   SUBGOAL_THEN `&2 pow j <= &n - &1` MP_TAC THENL
1298    [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 pow k` THEN CONJ_TAC THENL
1299      [ASM_SIMP_TAC[REAL_POW_MONO; REAL_OF_NUM_LE; ARITH]; ALL_TAC] THEN
1300     FIRST_X_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
1301       `~(n <= b) ==> b + 1 <= n`)) THEN
1302     GEN_REWRITE_TAC LAND_CONV [GSYM REAL_OF_NUM_LE] THEN
1303     REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_POW] THEN
1304     REAL_ARITH_TAC;
1305     ALL_TAC] THEN
1306   ABBREV_TAC `x = &n - &1` THEN SPEC_TAC(`x:real`,`x:real`) THEN
1307   MATCH_MP_TAC OVERPOWER_LEMMA THEN
1308   W(fun (asl,w) ->
1309       let th = DIFF_CONV
1310        (lhand(rator(rand(body(rand(lhand(rand(body(rand w))))))))) in
1311       MP_TAC th) THEN
1312   GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV)
1313    [REAL_MUL_LZERO; REAL_ADD_LID; REAL_ADD_RID;
1314     REAL_MUL_RID; REAL_MUL_LID] THEN
1315   W(fun (asl,w) ->
1316       let tm = mk_abs(`x:real`,rand(rator(rand(body(rand(lhand w)))))) in
1317       DISCH_TAC THEN EXISTS_TAC tm) THEN
1318   CONJ_TAC THENL
1319    [FIRST_ASSUM ACCEPT_TAC; ALL_TAC] THEN
1320   REWRITE_TAC[] THEN CONJ_TAC THENL
1321    [GEN_TAC THEN
1322     DISCH_THEN(fun th -> FIRST_ASSUM MATCH_MP_TAC THEN MP_TAC th) THEN
1323     MATCH_MP_TAC(REAL_ARITH `&0 < a ==> a <= x ==> &0 < &1 + x`) THEN
1324     SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; ARITH];
1325     ALL_TAC] THEN
1326   X_GEN_TAC `z:real` THEN DISCH_TAC THEN REWRITE_TAC[REAL_SUB_LE] THEN
1327   SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
1328   FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
1329    `a <= x ==> inv(&1 + x) <= inv(&1 + a) /\
1330                inv(&1 + a) <= b ==> inv(&1 + x) <= b`)) THEN
1331   CONJ_TAC THENL
1332    [MATCH_MP_TAC REAL_LE_INV2 THEN ASM_REWRITE_TAC[REAL_LE_LADD] THEN
1333     ASM_SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; ARITH; REAL_ARITH
1334      `&0 < x ==> &0 < &1 + x`];
1335     ALL_TAC] THEN
1336   SIMP_TAC[REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
1337   GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
1338   ASM_REWRITE_TAC[GSYM real_div]);;
1339
1340 let PSI_BOUNDS_SUSTAINED = prove
1341  (`(!n. n <= 2 EXP k ==> psi(n) <= (c * ln(&2)) * &n)
1342    ==> &4 * ln(&1 + &2 pow k) + &3
1343          <= ((c / &2 - &1) * ln(&2)) * (&1 + &2 pow k) /\
1344        &4 / (&1 + &2 pow k) <= (c / &2 - &1) * ln(&2) /\ &0 <= c
1345            ==> !n. psi(n) <= (c * ln(&2)) * &n`,
1346   let lemma = prove
1347    (`c / &2 + (c / &2 - &1) + &1 <= c`,
1348     REWRITE_TAC[REAL_ARITH `c2 + (c2 - &1) + &1 = &2 * c2`] THEN
1349     SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH_EQ; REAL_LE_REFL]) in
1350   REPEAT GEN_TAC THEN DISCH_TAC THEN
1351   DISCH_THEN(MP_TAC o C CONJ lemma) THEN
1352   ABBREV_TAC `d = c / &2 - &1` THEN REWRITE_TAC[GSYM CONJ_ASSOC] THEN
1353   DISCH_THEN(ASSUME_TAC o MATCH_MP PSI_BOUNDS_SUSTAINED_INDUCT) THEN
1354   X_GEN_TAC `m:num` THEN
1355   SUBGOAL_THEN `?j. m <= 2 EXP j` MP_TAC THENL
1356    [EXISTS_TAC `m:num` THEN SPEC_TAC(`m:num`,`m:num`) THEN
1357     POP_ASSUM_LIST(K ALL_TAC) THEN INDUCT_TAC THEN REWRITE_TAC[ARITH] THEN
1358     REWRITE_TAC[EXP] THEN MATCH_MP_TAC(ARITH_RULE
1359      `~(a = 0) /\ m <= a ==> SUC m <= 2 * a`) THEN
1360     ASM_REWRITE_TAC[EXP_EQ_0; ARITH_EQ];
1361     ALL_TAC] THEN
1362   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN SPEC_TAC(`m:num`,`m:num`) THEN
1363   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN INDUCT_TAC THENL
1364    [REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
1365     MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `2 EXP 0` THEN ASM_REWRITE_TAC[] THEN
1366     ASM_REWRITE_TAC[LE_EXP; ARITH_EQ; LE_0];
1367     ALL_TAC] THEN
1368   ASM_CASES_TAC `k <= j:num` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
1369   SUBGOAL_THEN `2 EXP (SUC j) <= 2 EXP k`
1370    (fun th -> ASM_MESON_TAC[th; LE_TRANS]) THEN
1371   ASM_REWRITE_TAC[LE_EXP; ARITH] THEN
1372   UNDISCH_TAC `~(k <= j:num)` THEN ARITH_TAC);;
1373
1374 (* ------------------------------------------------------------------------- *)
1375 (* Now apply it and get our reasonable bound.                                *)
1376 (* ------------------------------------------------------------------------- *)
1377
1378 let PSI_UBOUND_LOG = prove
1379  (`!n. psi(n) <= (&4407 / &2048 * ln (&2)) * &n`,
1380   MP_TAC PSI_UBOUND_1024_LOG THEN
1381   SUBST1_TAC(SYM(NUM_REDUCE_CONV `2 EXP 10`)) THEN
1382   DISCH_THEN(MATCH_MP_TAC o MATCH_MP PSI_BOUNDS_SUSTAINED) THEN
1383   CONV_TAC REAL_RAT_REDUCE_CONV THEN
1384   CONV_TAC(ONCE_DEPTH_CONV LN_N2_CONV) THEN
1385   CONJ_TAC THEN CONV_TAC REALCALC_REL_CONV);;
1386
1387 let PSI_UBOUND_3_2 = prove
1388  (`!n. psi(n) <= &3 / &2 * &n`,
1389   GEN_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1390   EXISTS_TAC `(&4407 / &2048 * ln (&2)) * &n` THEN
1391   REWRITE_TAC[PSI_UBOUND_LOG] THEN
1392   MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_POS] THEN
1393   CONV_TAC(ONCE_DEPTH_CONV LN_N2_CONV) THEN
1394   CONV_TAC REALCALC_REL_CONV);;
1395
1396 (* ------------------------------------------------------------------------- *)
1397 (* Now get a lower bound.                                                    *)
1398 (* ------------------------------------------------------------------------- *)
1399
1400 let PSI_LBOUND_3_5 = prove
1401  (`!n. 4 <= n ==> &3 / &5 * &n <= psi(n)`,
1402   let lemma = prove
1403    (`a <= b /\ b <= l /\ rest ==> a <= l /\ b <= l /\ rest`,
1404     MESON_TAC[REAL_LE_TRANS])
1405   and tac = time (CONV_TAC(RAND_CONV LN_N2_CONV THENC REALCALC_REL_CONV)) in
1406   GEN_TAC THEN ASM_CASES_TAC `n < 300` THENL
1407    [POP_ASSUM MP_TAC THEN SPEC_TAC(`n:num`,`n:num`) THEN
1408     CONV_TAC EXPAND_CASES_CONV THEN
1409     REWRITE_TAC(PSI_LIST_300) THEN
1410     REWRITE_TAC[LN_1; ARITH] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
1411     REPEAT
1412      ((MATCH_MP_TAC lemma THEN
1413        CONV_TAC(LAND_CONV REAL_RAT_REDUCE_CONV) THEN
1414        GEN_REWRITE_TAC I [TAUT `T /\ a <=> a`])
1415       ORELSE
1416        (CONJ_TAC THENL [tac THEN NO_TAC; ALL_TAC])
1417       ORELSE tac);
1418     ALL_TAC] THEN
1419   DISCH_THEN(K ALL_TAC) THEN
1420   MP_TAC(CONJUNCT1 (SPEC `n:num` PSI_BOUNDS_INDUCT)) THEN
1421   MATCH_MP_TAC(REAL_ARITH `a <= b ==> b <= x ==> a <= x`) THEN
1422   ASM_SIMP_TAC[ARITH_RULE `~(n < 300) ==> ~(n = 0)`] THEN
1423   MATCH_MP_TAC(REAL_ARITH `c <= n * (b - a) ==> a * n <= n * b - c`) THEN
1424   GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
1425   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&1 / &11 * &n` THEN
1426   CONJ_TAC THENL
1427    [ALL_TAC;
1428     MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_POS] THEN
1429     REWRITE_TAC[real_sub] THEN CONV_TAC(ONCE_DEPTH_CONV LN_N2_CONV) THEN
1430     CONV_TAC REALCALC_REL_CONV] THEN
1431   ABBREV_TAC `x = &n - &1` THEN
1432   SUBGOAL_THEN `&n = &1 + x` SUBST1_TAC THENL
1433    [EXPAND_TAC "x" THEN REAL_ARITH_TAC; ALL_TAC] THEN
1434   SUBGOAL_THEN `&299 <= x` MP_TAC THENL
1435    [EXPAND_TAC "x" THEN REWRITE_TAC[REAL_LE_SUB_LADD] THEN
1436     REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE; ARITH] THEN
1437     UNDISCH_TAC `~(n < 300)` THEN ARITH_TAC;
1438     ALL_TAC] THEN
1439   SPEC_TAC(`x:real`,`x:real`) THEN POP_ASSUM_LIST(K ALL_TAC) THEN
1440   MATCH_MP_TAC OVERPOWER_LEMMA THEN
1441   W(fun (asl,w) ->
1442       let th = DIFF_CONV
1443        (lhand(rator(rand(body(rand(lhand(rand(body(rand w))))))))) in
1444       MP_TAC th) THEN
1445   GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV)
1446    [REAL_MUL_LZERO; REAL_ADD_LID; REAL_ADD_RID;
1447     REAL_MUL_RID; REAL_MUL_LID] THEN
1448   W(fun (asl,w) ->
1449       let tm = mk_abs(`x:real`,rand(rator(rand(body(rand(lhand w)))))) in
1450       DISCH_TAC THEN EXISTS_TAC tm) THEN
1451   CONJ_TAC THENL
1452    [CONV_TAC REAL_RAT_REDUCE_CONV THEN
1453     CONV_TAC(ONCE_DEPTH_CONV LN_N2_CONV) THEN
1454     CONV_TAC REALCALC_REL_CONV;
1455     ALL_TAC] THEN
1456   REWRITE_TAC[] THEN CONJ_TAC THENL
1457    [GEN_TAC THEN
1458     DISCH_THEN(fun th -> FIRST_ASSUM MATCH_MP_TAC THEN MP_TAC th) THEN
1459     REAL_ARITH_TAC;
1460     ALL_TAC] THEN
1461   POP_ASSUM_LIST(K ALL_TAC) THEN GEN_TAC THEN DISCH_TAC THEN
1462   REWRITE_TAC[REAL_SUB_LE] THEN
1463   SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
1464   MATCH_MP_TAC REAL_LE_TRANS THEN
1465   EXISTS_TAC `inv(&1 + &299)` THEN CONJ_TAC THENL
1466    [ALL_TAC; CONV_TAC REAL_RAT_REDUCE_CONV] THEN
1467   MATCH_MP_TAC REAL_LE_INV2 THEN
1468   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
1469
1470 (* ========================================================================= *)
1471 (* Now the related theta function.                                           *)
1472 (* ========================================================================= *)
1473
1474 let theta = new_definition
1475   `theta(n) = sum(1,n) (\p. if prime p then ln(&p) else &0)`;;
1476
1477 (* ------------------------------------------------------------------------- *)
1478 (* An optimized rule to give theta(n) for all n <= some N.                   *)
1479 (* ------------------------------------------------------------------------- *)
1480
1481 let THETA_LIST =
1482   let THETA_0 = prove
1483    (`theta(0) = ln(&1)`,
1484     REWRITE_TAC[theta; sum; LN_1])
1485   and THETA_SUC = prove
1486    (`theta(SUC n) = theta(n) + (if prime(SUC n) then ln(&(SUC n)) else &0)`,
1487     REWRITE_TAC[theta; sum; ADD1] THEN REWRITE_TAC[ADD_AC])
1488   and n_tm = `n:num`
1489   and SIMPER_CONV =
1490     NUM_REDUCE_CONV THENC
1491     ONCE_DEPTH_CONV PRIME_CONV THENC
1492     GEN_REWRITE_CONV TOP_DEPTH_CONV
1493      [COND_CLAUSES; REAL_ADD_LID; REAL_ADD_RID] THENC
1494     SIMP_CONV [GSYM LN_MUL; REAL_OF_NUM_MUL; REAL_OF_NUM_LT; ARITH] in
1495   let rec THETA_LIST n =
1496     if n = 0 then [THETA_0] else
1497     let ths = THETA_LIST (n - 1) in
1498     let th1 = INST [mk_small_numeral(n-1),n_tm] THETA_SUC in
1499     let th2 = GEN_REWRITE_RULE (RAND_CONV o LAND_CONV) [hd ths] th1 in
1500     CONV_RULE SIMPER_CONV th2::ths in
1501   THETA_LIST;;
1502
1503 (* ------------------------------------------------------------------------- *)
1504 (* Split up the psi sum to show close relationship with theta.               *)
1505 (* ------------------------------------------------------------------------- *)
1506
1507 let PRIMEPOW_ODD_EVEN = prove
1508  (`!p q j k.
1509      ~(prime(p) /\ prime(q) /\ 1 <= j /\ (p EXP (2 * j) = q EXP (2 * k + 1)))`,
1510   REPEAT STRIP_TAC THEN
1511   SUBGOAL_THEN `q divides p` ASSUME_TAC THENL
1512    [MATCH_MP_TAC PRIME_DIVEXP THEN EXISTS_TAC `2 * j` THEN
1513     UNDISCH_TAC `p EXP (2 * j) = q EXP (2 * k + 1)` THEN
1514     REWRITE_TAC[EXP_ADD; EXP_1] THEN
1515     ASM_MESON_TAC[divides; MULT_SYM];
1516     ALL_TAC] THEN
1517   SUBGOAL_THEN `q = p:num` SUBST_ALL_TAC THENL
1518    [ASM_MESON_TAC[prime]; ALL_TAC] THEN
1519   UNDISCH_TAC `p EXP (2 * j) = p EXP (2 * k + 1)` THEN
1520   REWRITE_TAC[GSYM LE_ANTISYM] THEN REWRITE_TAC[LE_EXP] THEN
1521   COND_CASES_TAC THENL [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
1522   REWRITE_TAC[] THEN
1523   SUBGOAL_THEN `~(p = 1)` (fun th -> REWRITE_TAC[th]) THENL
1524    [ASM_MESON_TAC[PRIME_1]; ALL_TAC] THEN
1525   REWRITE_TAC[LE_ANTISYM] THEN
1526   DISCH_THEN(MP_TAC o AP_TERM `EVEN`) THEN
1527   REWRITE_TAC[EVEN_ADD; EVEN_MULT; ARITH_EVEN]);;
1528
1529 let PSI_SPLIT = prove
1530  (`psi(n) = theta(n) +
1531             sum(1,n) (\d. if ?p k. 1 <= k /\ prime p /\ (d = p EXP (2 * k))
1532                           then ln(&(aprimedivisor d)) else &0) +
1533             sum(1,n) (\d. if ?p k. 1 <= k /\ prime p /\ (d = p EXP (2 * k + 1))
1534                           then ln(&(aprimedivisor d)) else &0)`,
1535   REWRITE_TAC[psi; theta; GSYM SUM_ADD] THEN
1536   MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
1537   REWRITE_TAC[mangoldt; primepow] THEN
1538   ASM_CASES_TAC `?p k. 1 <= k /\ prime p /\ (r = p EXP k)` THEN
1539   ASM_REWRITE_TAC[] THENL
1540    [ALL_TAC;
1541     SUBGOAL_THEN `~(?p k. 1 <= k /\ prime p /\ (r = p EXP (2 * k))) /\
1542                   ~(?p k. 1 <= k /\ prime p /\ (r = p EXP (2 * k + 1))) /\
1543                   ~(prime r)`
1544      (fun th -> REWRITE_TAC[th; REAL_ADD_LID]) THEN
1545     ASM_MESON_TAC[ARITH_RULE `1 <= k ==> 1 <= 2 * k /\ 1 <= 2 * k + 1`;
1546                   EXP_1; LE_REFL]] THEN
1547   FIRST_X_ASSUM(X_CHOOSE_THEN `p:num` (X_CHOOSE_THEN `m:num` MP_TAC)) THEN
1548   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1549   DISCH_THEN SUBST_ALL_TAC THEN
1550   MP_TAC(SPECL [`m:num`; `2`] DIVISION) THEN REWRITE_TAC[ARITH_EQ] THEN
1551   MAP_EVERY ABBREV_TAC [`k = m DIV 2`; `d = m MOD 2`] THEN
1552   DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
1553   ASM_SIMP_TAC[APRIMEDIVISOR_PRIMEPOW] THEN
1554   FIRST_ASSUM(DISJ_CASES_THEN SUBST_ALL_TAC o MATCH_MP (ARITH_RULE
1555    `d < 2 ==> (d = 0) \/ (d = 1)`)) THEN
1556   ASM_REWRITE_TAC[PRIME_EXP; ADD_EQ_0; MULT_EQ_0; ARITH_EQ] THENL
1557    [UNDISCH_TAC `1 <= k * 2 + 0` THEN REWRITE_TAC[ADD_CLAUSES] THEN
1558     ASM_CASES_TAC `k = 0` THEN ASM_REWRITE_TAC[ARITH] THEN DISCH_TAC THEN
1559     SUBGOAL_THEN `~(k * 2 = 1)` (fun th -> REWRITE_TAC[th]) THENL
1560      [DISCH_THEN(MP_TAC o AP_TERM `EVEN`) THEN
1561       REWRITE_TAC[EVEN_MULT; ARITH_EVEN]; ALL_TAC] THEN
1562     REPEAT(COND_CASES_TAC THEN
1563            ASM_REWRITE_TAC[REAL_ADD_LID; REAL_ADD_RID]) THEN
1564     ASM_MESON_TAC[PRIMEPOW_ODD_EVEN; MULT_SYM;
1565                   ARITH_RULE `~(k = 0) ==> 1 <= k`];
1566     ALL_TAC] THEN
1567   ASM_CASES_TAC `k = 0` THENL
1568    [MATCH_MP_TAC(REAL_ARITH
1569      `(a = a') /\ (b = &0) /\ (c = &0) ==> (a = a' + b + c)`) THEN
1570     CONJ_TAC THENL
1571      [ASM_REWRITE_TAC[ARITH; EXP_1]; ALL_TAC] THEN
1572     CONJ_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
1573      [ASM_MESON_TAC[PRIMEPOW_ODD_EVEN; MULT_SYM]; ALL_TAC] THEN
1574     FIRST_X_ASSUM(X_CHOOSE_THEN `q:num` MP_TAC) THEN
1575     DISCH_THEN(X_CHOOSE_THEN `j:num` MP_TAC) THEN STRIP_TAC THEN
1576     SUBGOAL_THEN `q divides p` ASSUME_TAC THENL
1577      [MATCH_MP_TAC PRIME_DIVEXP THEN EXISTS_TAC `k * 2 + 1` THEN
1578       UNDISCH_TAC `p EXP (k * 2 + 1) = q EXP (2 * j + 1)` THEN
1579       REWRITE_TAC[EXP_ADD; EXP_1] THEN
1580       ASM_MESON_TAC[divides; MULT_SYM];
1581       ALL_TAC] THEN
1582     SUBGOAL_THEN `q = p:num` SUBST_ALL_TAC THENL
1583      [ASM_MESON_TAC[prime]; ALL_TAC] THEN
1584     UNDISCH_TAC `p EXP (k * 2 + 1) = p EXP (2 * j + 1)` THEN
1585     REWRITE_TAC[GSYM LE_ANTISYM] THEN REWRITE_TAC[LE_EXP] THEN
1586     ASM_CASES_TAC `p = 0` THENL [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
1587     ASM_REWRITE_TAC[] THEN
1588     ASM_CASES_TAC `p = 1` THENL [ASM_MESON_TAC[PRIME_1]; ALL_TAC] THEN
1589     ASM_REWRITE_TAC[] THEN
1590     REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
1591     REWRITE_TAC[LE_ANTISYM] THEN
1592     ASM_SIMP_TAC[ARITH_RULE `1 <= j ==> ~(1 = 2 * j + 1)`];
1593     ALL_TAC] THEN
1594   ASM_REWRITE_TAC[ARITH_RULE `(k * 2 + 1 = 1) <=> (k = 0)`; ARITH_EQ] THEN
1595   REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_ADD_LID; REAL_ADD_RID]) THEN
1596   ASM_MESON_TAC[PRIMEPOW_ODD_EVEN; MULT_SYM; ARITH_RULE
1597    `~(k = 0) ==> 1 <= k`]);;
1598
1599 (* ------------------------------------------------------------------------- *)
1600 (* General lemma about sums.                                                 *)
1601 (* ------------------------------------------------------------------------- *)
1602
1603 let SUM_SURJECT = prove
1604  (`!f i m n p q.
1605         (!r. m <= r /\ r < m + n ==> &0 <= f(i r)) /\
1606         (!s. p <= s /\ s < p + q /\ ~(f(s) = &0)
1607              ==> ?r. m <= r /\ r < m + n /\ (i r = s))
1608         ==> sum(p,q) f <= sum(m,n) (\r. f(i r))`,
1609   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1610   EXISTS_TAC `sum(m,n) (\r. if p:num <= i(r) /\ i(r) < p + q
1611                             then f(i(r)) else &0)` THEN
1612   CONJ_TAC THENL
1613    [ALL_TAC;
1614     MATCH_MP_TAC SUM_LE THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
1615     REWRITE_TAC[] THEN COND_CASES_TAC THEN
1616     ASM_MESON_TAC[REAL_LE_REFL; ADD_AC]] THEN
1617   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
1618   SPEC_TAC(`q:num`,`q:num`) THEN INDUCT_TAC THENL
1619    [STRIP_TAC THEN REWRITE_TAC[sum] THEN
1620     REWRITE_TAC[ARITH_RULE `~(p <= q /\ q < p + 0)`] THEN
1621     REWRITE_TAC[SUM_0; REAL_LE_REFL];
1622     ALL_TAC] THEN
1623   DISCH_THEN(fun th -> POP_ASSUM MP_TAC THEN STRIP_ASSUME_TAC th) THEN
1624   ANTS_TAC THENL
1625    [ASM_REWRITE_TAC[] THEN
1626     REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
1627     ASM_MESON_TAC[ARITH_RULE `s < p + q ==> s < p + SUC q`];
1628     ALL_TAC] THEN
1629   REWRITE_TAC[sum] THEN
1630   SUBGOAL_THEN
1631    `sum(m,n) (\r. if p <= i r /\ i r < p + SUC q then f (i r) else &0) =
1632     sum(m,n) (\r. if p <= i r /\ i r < p + q then f (i r) else &0) +
1633     sum(m,n) (\r. if i r = p + q then f(i r) else &0)`
1634   SUBST1_TAC THENL
1635    [REWRITE_TAC[GSYM SUM_ADD] THEN MATCH_MP_TAC SUM_EQ THEN
1636     X_GEN_TAC `r:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN
1637     ASM_CASES_TAC `(i:num->num) r = p + q` THEN ASM_REWRITE_TAC[] THENL
1638      [REWRITE_TAC[LE_ADD; LT_REFL; ARITH_RULE `p + q < p + SUC q`] THEN
1639       REWRITE_TAC[REAL_ADD_LID; REAL_ADD_RID];
1640       ALL_TAC] THEN
1641     ASM_REWRITE_TAC[ARITH_RULE
1642        `r < p + SUC q <=> (r = p + q) \/ r < p + q`] THEN
1643     REWRITE_TAC[REAL_ADD_RID];
1644     ALL_TAC] THEN
1645   MATCH_MP_TAC(REAL_ARITH `f <= s'' ==> s <= s' ==> s + f <= s' + s''`) THEN
1646   UNDISCH_TAC
1647    `!s. p <= s /\ s < p + SUC q /\ ~(f s = &0)
1648            ==> (?r:num. m <= r /\ r < m + n /\ (i r = s))` THEN
1649   DISCH_THEN(MP_TAC o SPEC `p + q:num`) THEN
1650   ASM_CASES_TAC `f(p + q:num) = &0` THEN ASM_REWRITE_TAC[] THENL
1651    [MATCH_MP_TAC REAL_LE_TRANS THEN
1652     EXISTS_TAC `sum(m,n) (\r. &0)` THEN CONJ_TAC THENL
1653      [REWRITE_TAC[SUM_0; REAL_LE_REFL]; ALL_TAC] THEN
1654     MATCH_MP_TAC SUM_LE THEN X_GEN_TAC `r:num` THEN
1655     REWRITE_TAC[] THEN COND_CASES_TAC THEN
1656     REWRITE_TAC[REAL_LE_REFL] THEN ASM_MESON_TAC[ADD_SYM];
1657     ALL_TAC] THEN
1658   ANTS_TAC THENL [ARITH_TAC; ALL_TAC] THEN
1659   DISCH_THEN(X_CHOOSE_THEN `s:num` STRIP_ASSUME_TAC) THEN
1660   SUBGOAL_THEN `n = (s - m) + 1 + ((m + n) - (s + 1))` SUBST1_TAC THENL
1661    [MAP_EVERY UNDISCH_TAC [`m <= s:num`; `s < m + n:num`] THEN ARITH_TAC;
1662     ALL_TAC] THEN
1663   REWRITE_TAC[GSYM SUM_SPLIT] THEN
1664   ASM_SIMP_TAC[SUM_1; ARITH_RULE `m <= s ==> (m + (s - m) = s:num)`] THEN
1665   MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ &0 <= y ==> a <= x + a + y`) THEN
1666   CONJ_TAC THENL
1667    [MATCH_MP_TAC REAL_LE_TRANS THEN
1668     EXISTS_TAC `sum(m,s - m) (\r. &0)` THEN CONJ_TAC THENL
1669      [REWRITE_TAC[SUM_0; REAL_LE_REFL]; ALL_TAC] THEN
1670     MATCH_MP_TAC SUM_LE THEN REPEAT STRIP_TAC THEN REWRITE_TAC[] THEN
1671     COND_CASES_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN
1672     FIRST_ASSUM(SUBST1_TAC o SYM) THEN FIRST_ASSUM MATCH_MP_TAC THEN
1673     MAP_EVERY UNDISCH_TAC
1674       [`m <= r:num`; `r < s - m + m:num`; `s < m + n:num`; `m <= s:num`] THEN
1675     ARITH_TAC;
1676     MATCH_MP_TAC REAL_LE_TRANS THEN
1677     EXISTS_TAC `sum(s + 1,(m + n) - (s + 1)) (\r. &0)` THEN CONJ_TAC THENL
1678      [REWRITE_TAC[SUM_0; REAL_LE_REFL]; ALL_TAC] THEN
1679     MATCH_MP_TAC SUM_LE THEN REPEAT STRIP_TAC THEN REWRITE_TAC[] THEN
1680     COND_CASES_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN
1681     FIRST_ASSUM(SUBST1_TAC o SYM) THEN FIRST_ASSUM MATCH_MP_TAC THEN
1682     MAP_EVERY UNDISCH_TAC
1683       [`r < (m + n) - (s + 1) + s + 1:num`;
1684        `s + 1 <= r`; `s < m + n:num`; `m <= s:num`] THEN
1685     ARITH_TAC]);;
1686
1687 (* ------------------------------------------------------------------------- *)
1688 (* Apply this to show that one of the residuals is bounded by the other.     *)
1689 (* ------------------------------------------------------------------------- *)
1690
1691 let PSI_RESIDUES_COMPARE_2 = prove
1692  (`sum(2,n) (\d. if ?p k. 1 <= k /\ prime p /\ (d = p EXP (2 * k + 1))
1693                  then ln(&(aprimedivisor d)) else &0)
1694    <= sum(2,n) (\d. if ?p k. 1 <= k /\ prime p /\ (d = p EXP (2 * k))
1695                     then ln(&(aprimedivisor d)) else &0)`,
1696   MP_TAC(SPECL
1697    [`\d. if ?p k. 1 <= k /\ prime p /\ (d = p EXP (2 * k + 1))
1698                     then ln(&(aprimedivisor d)) else &0`;
1699     `\d. if ?p k. 1 <= k /\ prime p /\ (d = p EXP k)
1700                   then d * (aprimedivisor d) else d`;
1701     `2`; `n:num`; `2`; `n:num`] SUM_SURJECT) THEN
1702   REWRITE_TAC[] THEN ANTS_TAC THENL
1703    [CONJ_TAC THENL
1704      [X_GEN_TAC `r:num` THEN STRIP_TAC THEN
1705       ASM_CASES_TAC `?p k. 1 <= k /\ prime p /\ (r = p EXP k)` THEN
1706       ASM_REWRITE_TAC[] THENL
1707        [ALL_TAC;
1708         COND_CASES_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN
1709         ASM_MESON_TAC[ARITH_RULE `1 <= k ==> 1 <= 2 * k + 1`]] THEN
1710       FIRST_X_ASSUM(X_CHOOSE_THEN `p:num` MP_TAC) THEN
1711       DISCH_THEN(X_CHOOSE_THEN `k:num` MP_TAC) THEN
1712       REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1713       DISCH_THEN SUBST_ALL_TAC THEN
1714       ASM_SIMP_TAC[APRIMEDIVISOR_PRIMEPOW] THEN
1715       COND_CASES_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN
1716       SUBGOAL_THEN `p EXP k * p = p EXP (k + 1)` SUBST1_TAC THENL
1717        [REWRITE_TAC[EXP_ADD; EXP_1; MULT_AC]; ALL_TAC] THEN
1718       ASM_SIMP_TAC[APRIMEDIVISOR_PRIMEPOW; ARITH_RULE `1 <= k + 1`] THEN
1719       ASM_MESON_TAC[LN_POS; REAL_OF_NUM_LE; PRIME_GE_2; REAL_LE_REFL;
1720                     ARITH_RULE `2 <= n ==> 1 <= n`];
1721       ALL_TAC] THEN
1722     X_GEN_TAC `s:num` THEN
1723     ASM_CASES_TAC `?p k. 1 <= k /\ prime p /\ (s = p EXP (2 * k + 1))` THEN
1724     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1725     FIRST_X_ASSUM(X_CHOOSE_THEN `p:num` MP_TAC) THEN
1726     DISCH_THEN(X_CHOOSE_THEN `k:num` MP_TAC) THEN
1727     REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1728     DISCH_THEN SUBST_ALL_TAC THEN
1729     EXISTS_TAC `p EXP (2 * k)` THEN
1730     COND_CASES_TAC THENL
1731      [ALL_TAC; ASM_MESON_TAC[ARITH_RULE `1 <= k ==> 1 <= 2 * k`]] THEN
1732     ASM_SIMP_TAC[APRIMEDIVISOR_PRIMEPOW; EXP_ADD; EXP_1;
1733                  ARITH_RULE `1 <= k ==> 1 <= 2 * k`] THEN
1734     CONJ_TAC THENL
1735      [REWRITE_TAC[ARITH_RULE `2 <= n <=> ~(n = 0) /\ ~(n = 1)`;
1736                   EXP_EQ_0; EXP_EQ_1] THEN
1737       ASM_MESON_TAC[PRIME_1; PRIME_0;
1738                     ARITH_RULE `1 <= k ==> ~(2 * k = 0)`];
1739       ALL_TAC] THEN
1740     MATCH_MP_TAC LET_TRANS THEN EXISTS_TAC `p EXP (2 * k + 1)` THEN
1741     ASM_REWRITE_TAC[LE_EXP] THEN
1742     COND_CASES_TAC THEN UNDISCH_TAC `1 <= k` THEN ARITH_TAC;
1743     ALL_TAC] THEN
1744   MATCH_MP_TAC(REAL_ARITH `b <= c ==> a <= b ==> a <= c`) THEN
1745   MATCH_MP_TAC SUM_LE THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
1746   REWRITE_TAC[] THEN
1747   ASM_CASES_TAC `?p k. 1 <= k /\ prime p /\ (r = p EXP k)` THEN
1748   ASM_REWRITE_TAC[] THENL
1749    [ALL_TAC;
1750     REPEAT COND_CASES_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN
1751     ASM_MESON_TAC[ARITH_RULE `1 <= k ==> 1 <= 2 * k /\ 1 <= 2 * k + 1`]] THEN
1752   FIRST_X_ASSUM(CHOOSE_THEN (K ALL_TAC)) THEN
1753   ASM_CASES_TAC `?p k. 1 <= k /\ prime p /\ (r = p EXP (2 * k))` THEN
1754   ASM_REWRITE_TAC[] THENL
1755    [FIRST_X_ASSUM(X_CHOOSE_THEN `p:num` MP_TAC) THEN
1756     DISCH_THEN(X_CHOOSE_THEN `k:num` MP_TAC) THEN
1757     REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1758     DISCH_THEN SUBST_ALL_TAC THEN
1759     ASM_SIMP_TAC[APRIMEDIVISOR_PRIMEPOW;
1760                  ARITH_RULE `1 <= k ==> 1 <= 2 * k`] THEN
1761     SUBGOAL_THEN `p EXP (2 * k) * p = p EXP (2 * k + 1)` SUBST1_TAC THENL
1762      [REWRITE_TAC[EXP_ADD; EXP_1; MULT_AC]; ALL_TAC] THEN
1763     COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
1764     ASM_SIMP_TAC[APRIMEDIVISOR_PRIMEPOW; REAL_LE_REFL;
1765                  ARITH_RULE `1 <= k ==> 1 <= 2 * k + 1`];
1766     ALL_TAC] THEN
1767   COND_CASES_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN
1768   FIRST_X_ASSUM(X_CHOOSE_THEN `p:num` MP_TAC) THEN
1769   DISCH_THEN(X_CHOOSE_THEN `k:num` MP_TAC) THEN
1770   FIRST_ASSUM(UNDISCH_TAC o check is_neg o concl) THEN
1771   MATCH_MP_TAC(TAUT `(b ==> a) ==> ~a ==> b ==> c`) THEN
1772   STRIP_TAC THEN MAP_EVERY EXISTS_TAC [`p:num`; `k:num`] THEN
1773   ASM_REWRITE_TAC[] THEN
1774   MP_TAC(SPEC `r:num` APRIMEDIVISOR) THEN
1775   ASM_SIMP_TAC[ARITH_RULE `2 <= n ==> ~(n = 1)`] THEN
1776   ABBREV_TAC `q = aprimedivisor r` THEN STRIP_TAC THEN
1777   SUBGOAL_THEN `q divides p` ASSUME_TAC THENL
1778    [MATCH_MP_TAC PRIME_DIVEXP THEN EXISTS_TAC `2 * k + 1` THEN
1779     ASM_MESON_TAC[divides; MULT_SYM];
1780     ALL_TAC] THEN
1781   SUBGOAL_THEN `q = p:num` SUBST_ALL_TAC THENL
1782    [ASM_MESON_TAC[prime]; ALL_TAC] THEN
1783   UNDISCH_TAC `r * p = p EXP (2 * k + 1)` THEN
1784   REWRITE_TAC[EXP_ADD; EXP_1; EQ_MULT_RCANCEL] THEN
1785   ASM_MESON_TAC[PRIME_0]);;
1786
1787 let PSI_RESIDUES_COMPARE = prove
1788  (`!n. sum(1,n) (\d. if ?p k. 1 <= k /\ prime p /\ (d = p EXP (2 * k + 1))
1789                      then ln(&(aprimedivisor d)) else &0)
1790        <= sum(1,n) (\d. if ?p k. 1 <= k /\ prime p /\ (d = p EXP (2 * k))
1791                         then ln(&(aprimedivisor d)) else &0)`,
1792   GEN_TAC THEN
1793   ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[sum; REAL_LE_REFL] THEN
1794   FIRST_ASSUM(SUBST1_TAC o MATCH_MP (ARITH_RULE
1795    `~(n = 0) ==> (n = 1 + (n - 1))`)) THEN
1796   REWRITE_TAC[GSYM SUM_SPLIT; SUM_1] THEN
1797   MATCH_MP_TAC(REAL_ARITH
1798    `b <= d /\ (a = &0) /\ (c = &0) ==> a + b <= c + d`) THEN
1799   REWRITE_TAC[PSI_RESIDUES_COMPARE_2; ARITH] THEN
1800   REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
1801   ASM_MESON_TAC[EXP_EQ_1; PRIME_1; ARITH_RULE
1802     `1 <= k ==> ~(2 * k = 0) /\ ~(2 * k + 1 = 0)`]);;
1803
1804 (* ------------------------------------------------------------------------- *)
1805 (* The even residual reduces to the square root case.                        *)
1806 (* ------------------------------------------------------------------------- *)
1807
1808 let PSI_SQRT = prove
1809  (`!n. psi(ISQRT(n)) =
1810         sum(1,n) (\d. if ?p k. 1 <= k /\ prime p /\ (d = p EXP (2 * k))
1811                       then ln(&(aprimedivisor d)) else &0)`,
1812   REWRITE_TAC[psi] THEN INDUCT_TAC THEN
1813   REWRITE_TAC[ISQRT_0; sum; ISQRT_SUC] THEN
1814   ASM_CASES_TAC `?m. SUC n = m EXP 2` THENL
1815    [ALL_TAC;
1816     SUBGOAL_THEN `~(?p k. 1 <= k /\ prime p /\ (1 + n = p EXP (2 * k)))`
1817     ASSUME_TAC THENL
1818      [ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[EXP_MULT] THEN
1819       ASM_MESON_TAC[ARITH_RULE `1 + n = SUC n`];
1820       ALL_TAC] THEN
1821     ASM_REWRITE_TAC[REAL_ADD_RID]] THEN
1822   ASM_REWRITE_TAC[REAL_EQ_ADD_LCANCEL; sum] THEN
1823   FIRST_X_ASSUM(X_CHOOSE_TAC `m:num`) THEN
1824   SUBGOAL_THEN `1 + ISQRT n = m` SUBST1_TAC THENL
1825    [SUBGOAL_THEN `(1 + ISQRT n) EXP 2 = SUC n` MP_TAC THENL
1826      [ALL_TAC;
1827       ASM_REWRITE_TAC[num_CONV `2`; GSYM LE_ANTISYM] THEN
1828       REWRITE_TAC[EXP_MONO_LE_SUC; EXP_MONO_LT_SUC]] THEN
1829     MP_TAC(SPEC `n:num` ISQRT_SUC) THEN
1830     COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
1831     REWRITE_TAC[ARITH_RULE `1 + n = SUC n`] THEN
1832     DISCH_THEN(SUBST1_TAC o SYM) THEN
1833     MP_TAC(SPEC `SUC n` ISQRT_WORKS) THEN ASM_REWRITE_TAC[] THEN
1834     REWRITE_TAC[num_CONV `2`; GSYM LE_ANTISYM] THEN
1835     REWRITE_TAC[EXP_MONO_LE_SUC; EXP_MONO_LT_SUC] THEN ARITH_TAC;
1836     ALL_TAC] THEN
1837   ASM_REWRITE_TAC[ARITH_RULE `1 + n = SUC n`] THEN
1838   REWRITE_TAC[mangoldt; primepow] THEN
1839   ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[EXP_MULT] THEN
1840   REWRITE_TAC[GSYM LE_ANTISYM; EXP_MONO_LE_SUC; num_CONV `2`] THEN
1841   REWRITE_TAC[LE_ANTISYM] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
1842   REWRITE_TAC[aprimedivisor] THEN
1843   REPEAT AP_TERM_TAC THEN ABS_TAC THEN
1844   MATCH_MP_TAC(TAUT `(a ==> (b <=> c)) ==> (a /\ b <=> a /\ c)`) THEN
1845   DISCH_TAC THEN REWRITE_TAC[EXP; EXP_1] THEN
1846   ASM_MESON_TAC[DIVIDES_LMUL; PRIME_DIVPROD]);;
1847
1848 (* ------------------------------------------------------------------------- *)
1849 (* Hence the main comparison result.                                         *)
1850 (* ------------------------------------------------------------------------- *)
1851
1852 let PSI_THETA = prove
1853  (`!n. theta(n) + psi(ISQRT n) <= psi(n) /\
1854        psi(n) <= theta(n) + &2 * psi(ISQRT n)`,
1855   GEN_TAC THEN
1856   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [PSI_SPLIT] THEN
1857   GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [PSI_SPLIT] THEN
1858   MP_TAC(SPEC `n:num` PSI_RESIDUES_COMPARE) THEN
1859   REWRITE_TAC[GSYM PSI_SQRT] THEN
1860   SIMP_TAC[REAL_MUL_2; GSYM REAL_ADD_ASSOC; REAL_LE_LADD; REAL_LE_ADDR] THEN
1861   DISCH_THEN(K ALL_TAC) THEN
1862   MATCH_MP_TAC SUM_POS_GEN THEN X_GEN_TAC `r:num` THEN DISCH_TAC THEN
1863   REWRITE_TAC[] THEN COND_CASES_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN
1864   FIRST_X_ASSUM(X_CHOOSE_THEN `p:num` MP_TAC) THEN
1865   DISCH_THEN(X_CHOOSE_THEN `k:num` MP_TAC) THEN
1866   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1867   DISCH_THEN SUBST1_TAC THEN
1868   ASM_SIMP_TAC[APRIMEDIVISOR_PRIMEPOW;
1869     ARITH_RULE `1 <= k ==> 1 <= 2 * k + 1`] THEN
1870   MATCH_MP_TAC LN_POS THEN REWRITE_TAC[REAL_OF_NUM_LE] THEN
1871   ASM_MESON_TAC[PRIME_0; ARITH_RULE `~(p = 0) ==> 1 <= p`]);;
1872
1873 (* ------------------------------------------------------------------------- *)
1874 (* A trivial one-way comparison is immediate.                                *)
1875 (* ------------------------------------------------------------------------- *)
1876
1877 let THETA_LE_PSI = prove
1878  (`!n. theta(n) <= psi(n)`,
1879   GEN_TAC THEN REWRITE_TAC[theta; psi] THEN MATCH_MP_TAC SUM_LE THEN
1880   X_GEN_TAC `p:num` THEN STRIP_TAC THEN
1881   ASM_CASES_TAC `prime p` THEN ASM_REWRITE_TAC[MANGOLDT_POS] THEN
1882   ASM_SIMP_TAC[mangoldt; PRIME_PRIMEPOW] THEN
1883   SUBGOAL_THEN `aprimedivisor p = p`
1884    (fun th -> REWRITE_TAC[th; REAL_LE_REFL]) THEN
1885   ASM_MESON_TAC[APRIMEDIVISOR_PRIMEPOW; EXP_1; LE_REFL]);;
1886
1887 (* ------------------------------------------------------------------------- *)
1888 (* A tighter bound on psi on a smaller range, to reduce later case analysis. *)
1889 (* ------------------------------------------------------------------------- *)
1890
1891 let PSI_UBOUND_30 = prove
1892  (`!n. n <= 30 ==> psi(n) <= &65 / &64 * &n`,
1893   let lemma = prove
1894    (`a <= b /\ l <= a /\ rest ==> l <= a /\ l <= b /\ rest`,
1895     MESON_TAC[REAL_LE_TRANS])
1896   and tac = time (CONV_TAC(LAND_CONV LN_N2_CONV THENC REALCALC_REL_CONV)) in
1897   REWRITE_TAC[ARITH_RULE `n <= 30 <=> n < 31`] THEN
1898   CONV_TAC EXPAND_CASES_CONV THEN REWRITE_TAC(PSI_LIST_300) THEN
1899   REWRITE_TAC[LN_1] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
1900   REPEAT
1901    ((MATCH_MP_TAC lemma THEN
1902      CONV_TAC(LAND_CONV REAL_RAT_REDUCE_CONV) THEN
1903      GEN_REWRITE_TAC I [TAUT `T /\ a <=> a`])
1904     ORELSE
1905      (CONJ_TAC THENL [tac THEN NO_TAC; ALL_TAC])
1906     ORELSE tac));;
1907
1908 (* ------------------------------------------------------------------------- *)
1909 (* Bounds for theta, derived from those for psi.                             *)
1910 (* ------------------------------------------------------------------------- *)
1911
1912 let THETA_UBOUND_3_2 = prove
1913  (`!n. theta(n) <= &3 / &2 * &n`,
1914   MESON_TAC[REAL_LE_TRANS; PSI_UBOUND_3_2; THETA_LE_PSI]);;
1915
1916 let THETA_LBOUND_1_2 = prove
1917  (`!n. 5 <= n ==> &1 / &2 * &n <= theta(n)`,
1918   let lemma = prove
1919    (`a <= b /\ b <= l /\ rest ==> a <= l /\ b <= l /\ rest`,
1920     MESON_TAC[REAL_LE_TRANS])
1921   and tac = time (CONV_TAC(RAND_CONV LN_N2_CONV THENC REALCALC_REL_CONV)) in
1922   REPEAT STRIP_TAC THEN ASM_CASES_TAC `n >= 900` THENL
1923    [MP_TAC(CONJUNCT2(SPEC `n:num` PSI_THETA)) THEN
1924     MP_TAC(SPEC `n:num` PSI_LBOUND_3_5) THEN
1925     ASM_SIMP_TAC[ARITH_RULE `n >= 900 ==> 4 <= n`] THEN
1926     MATCH_MP_TAC(REAL_ARITH
1927      `d <= (a - b) * n ==> a * n <= ps ==> ps <= th + d ==> b * n <= th`) THEN
1928     ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
1929     SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
1930     REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
1931     CONV_TAC REAL_RAT_REDUCE_CONV THEN
1932     MATCH_MP_TAC REAL_LE_TRANS THEN
1933     EXISTS_TAC `&3 / &2 * &(ISQRT n)` THEN
1934     REWRITE_TAC[PSI_UBOUND_3_2] THEN
1935     GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
1936     SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
1937     REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
1938     CONV_TAC REAL_RAT_REDUCE_CONV THEN
1939     SUBGOAL_THEN `&(ISQRT n) pow 2 <= (&n * &1 / &30) pow 2` MP_TAC THENL
1940      [ALL_TAC;
1941       ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[REAL_NOT_LE] THEN
1942       DISCH_TAC THEN MATCH_MP_TAC REAL_POW_LT2 THEN
1943       ASM_REWRITE_TAC[] THEN CONV_TAC NUM_REDUCE_CONV THEN
1944       MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_POS] THEN
1945       CONV_TAC REAL_RAT_REDUCE_CONV] THEN
1946     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&n` THEN CONJ_TAC THENL
1947      [REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_LE; ISQRT_WORKS];
1948       ALL_TAC] THEN
1949     REWRITE_TAC[REAL_POW_2; REAL_ARITH
1950      `(a * b) * (a * b) = a * a * b * b`] THEN
1951     GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_RID] THEN
1952     MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN
1953     SIMP_TAC[REAL_MUL_ASSOC; GSYM REAL_LE_LDIV_EQ;
1954              REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
1955     CONV_TAC REAL_RAT_REDUCE_CONV THEN
1956     REWRITE_TAC[REAL_OF_NUM_LE] THEN
1957     UNDISCH_TAC `n >= 900` THEN ARITH_TAC;
1958     ALL_TAC] THEN
1959   ASM_CASES_TAC `n < 413` THENL
1960    [UNDISCH_TAC `5 <= n` THEN UNDISCH_TAC `n < 413` THEN
1961     SPEC_TAC(`n:num`,`n:num`) THEN POP_ASSUM_LIST(K ALL_TAC) THEN
1962     CONV_TAC EXPAND_CASES_CONV THEN CONV_TAC NUM_REDUCE_CONV THEN
1963     REWRITE_TAC(THETA_LIST 412) THEN
1964     REWRITE_TAC[LN_1; ARITH] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
1965     REPEAT
1966      ((MATCH_MP_TAC lemma THEN
1967        CONV_TAC(LAND_CONV REAL_RAT_REDUCE_CONV) THEN
1968        GEN_REWRITE_TAC I [TAUT `T /\ a <=> a`])
1969       ORELSE
1970        (CONJ_TAC THENL [tac THEN NO_TAC; ALL_TAC])
1971       ORELSE tac);
1972     ALL_TAC] THEN
1973   MP_TAC(CONJUNCT2(SPEC `n:num` PSI_THETA)) THEN
1974   MP_TAC(SPEC `n:num` PSI_LBOUND_3_5) THEN
1975   ASM_SIMP_TAC[ARITH_RULE `5 <= n ==> 4 <= n`] THEN
1976   MATCH_MP_TAC(REAL_ARITH
1977    `d <= (a - b) * n ==> a * n <= ps ==> ps <= th + d ==> b * n <= th`) THEN
1978   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
1979   SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
1980   REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
1981   CONV_TAC REAL_RAT_REDUCE_CONV THEN
1982   MATCH_MP_TAC REAL_LE_TRANS THEN
1983   EXISTS_TAC `&65 / &64 * &(ISQRT n)` THEN CONJ_TAC THENL
1984    [MATCH_MP_TAC PSI_UBOUND_30 THEN
1985     SUBGOAL_THEN `(ISQRT n) EXP (SUC 1) <= 30 EXP (SUC 1)` MP_TAC THENL
1986      [ALL_TAC; REWRITE_TAC[EXP_MONO_LE_SUC]] THEN
1987     MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `n:num` THEN
1988     REWRITE_TAC[ARITH; ISQRT_WORKS] THEN
1989     UNDISCH_TAC `~(n >= 900)` THEN ARITH_TAC;
1990     ALL_TAC] THEN
1991   GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
1992   SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
1993   REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
1994   CONV_TAC REAL_RAT_REDUCE_CONV THEN
1995   SUBGOAL_THEN `&(ISQRT n) pow 2 <= (&n * &16 / &325) pow 2` MP_TAC THENL
1996    [ALL_TAC;
1997     ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[REAL_NOT_LE] THEN
1998     DISCH_TAC THEN MATCH_MP_TAC REAL_POW_LT2 THEN
1999     ASM_REWRITE_TAC[] THEN CONV_TAC NUM_REDUCE_CONV THEN
2000     MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_POS] THEN
2001     CONV_TAC REAL_RAT_REDUCE_CONV] THEN
2002   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&n` THEN CONJ_TAC THENL
2003    [REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_LE; ISQRT_WORKS];
2004     ALL_TAC] THEN
2005   REWRITE_TAC[REAL_POW_2; REAL_ARITH
2006    `(a * b) * (a * b) = a * a * b * b`] THEN
2007   GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_RID] THEN
2008   MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN
2009   CONV_TAC REAL_RAT_REDUCE_CONV THEN
2010   SIMP_TAC[GSYM REAL_LE_LDIV_EQ;
2011            REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
2012   CONV_TAC REAL_RAT_REDUCE_CONV THEN
2013   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&413` THEN
2014   CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_OF_NUM_LE] THEN
2015   UNDISCH_TAC `~(n < 413)` THEN ARITH_TAC);;
2016
2017 (* ========================================================================= *)
2018 (* Tighten the bounds on weak PNT to get the Bertrand conjecture.            *)
2019 (* ========================================================================= *)
2020
2021 let FLOOR_POS = prove
2022  (`!x. &0 <= x ==> &0 <= floor x`,
2023   GEN_TAC THEN STRIP_TAC THEN ASM_CASES_TAC `x < &1` THENL
2024    [ASM_MESON_TAC[FLOOR_EQ_0; REAL_LE_REFL]; ALL_TAC] THEN
2025   MP_TAC(last(CONJUNCTS(SPEC `x:real` FLOOR))) THEN
2026   UNDISCH_TAC `~(x < &1)` THEN REAL_ARITH_TAC);;
2027
2028 let FLOOR_NUM_EXISTS = prove
2029  (`!x. &0 <= x ==> ?k. floor x = &k`,
2030   REPEAT STRIP_TAC THEN MP_TAC(CONJUNCT1(SPEC `x:real` FLOOR)) THEN
2031   REWRITE_TAC[integer] THEN
2032   ASM_MESON_TAC[FLOOR_POS; REAL_ARITH `&0 <= x ==> (abs x = x)`]);;
2033
2034 let FLOOR_DIV_INTERVAL = prove
2035  (`!n d k. ~(d = 0)
2036            ==> ((floor(&n / &d) = &k) =
2037                   if k = 0 then &n < &d
2038                   else &n / &(k + 1) < &d /\ &d <= &n / &k)`,
2039   REPEAT STRIP_TAC THEN ASM_CASES_TAC `k = 0` THENL
2040    [ASM_REWRITE_TAC[FLOOR_EQ_0] THEN
2041     ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LT_LDIV_EQ; REAL_OF_NUM_LT;
2042                  ARITH_RULE `0 < d <=> ~(d = 0)`] THEN
2043     ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_POS; REAL_MUL_LID; REAL_OF_NUM_LT];
2044     ALL_TAC] THEN
2045   REWRITE_TAC[GSYM FLOOR_UNIQUE; INTEGER_CLOSED] THEN
2046   ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LT_LDIV_EQ; REAL_OF_NUM_LT;
2047                  ARITH_RULE `0 < d <=> ~(d = 0)`; ARITH_RULE `0 < k + 1`] THEN
2048   REWRITE_TAC[REAL_MUL_AC; CONJ_ACI; REAL_OF_NUM_ADD]);;
2049
2050 let FLOOR_DIV_EXISTS = prove
2051  (`!n d. ~(d = 0)
2052          ==> ?k. (floor(&n / &d) = &k) /\
2053                  d * k <= n /\ n < d * (k + 1)`,
2054   REPEAT STRIP_TAC THEN
2055   SUBGOAL_THEN `?k. floor (&n / &d) = &k` MP_TAC THENL
2056    [ASM_SIMP_TAC[FLOOR_NUM_EXISTS; REAL_LE_DIV; REAL_POS]; ALL_TAC] THEN
2057   MATCH_MP_TAC MONO_EXISTS THEN
2058   X_GEN_TAC `k:num` THEN SIMP_TAC[] THEN ASM_SIMP_TAC[FLOOR_DIV_INTERVAL] THEN
2059   COND_CASES_TAC THEN
2060   ASM_REWRITE_TAC[MULT_CLAUSES; LE_0; ADD_CLAUSES; REAL_OF_NUM_LT] THEN
2061   ASM_SIMP_TAC[REAL_LT_LDIV_EQ; REAL_LE_RDIV_EQ; REAL_OF_NUM_LT;
2062                ARITH_RULE `0 < k + 1 /\ (~(k = 0) ==> 0 < k)`] THEN
2063   REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_LT; REAL_OF_NUM_LE] THEN
2064   REWRITE_TAC[CONJ_ACI]);;
2065
2066 let FLOOR_HALF_INTERVAL = prove
2067  (`!n d. ~(d = 0)
2068          ==> (floor (&n / &d) - &2 * floor (&(n DIV 2) / &d) =
2069                 if ?k. ODD k /\ n DIV (k + 1) < d /\ d <= n DIV k
2070                 then &1 else &0)`,
2071   let lemma = prove(`ODD(k) ==> ~(k = 0)`,MESON_TAC[EVEN; NOT_EVEN]) in
2072   REPEAT STRIP_TAC THEN
2073   FIRST_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP FLOOR_DIV_EXISTS) THEN
2074   FIRST_ASSUM(MP_TAC o SPEC `n DIV 2` o MATCH_MP FLOOR_DIV_EXISTS) THEN
2075   DISCH_THEN(X_CHOOSE_THEN `k1:num`
2076    (CONJUNCTS_THEN2 SUBST1_TAC STRIP_ASSUME_TAC)) THEN
2077   DISCH_THEN(X_CHOOSE_THEN `k2:num`
2078    (CONJUNCTS_THEN2 SUBST1_TAC STRIP_ASSUME_TAC)) THEN
2079   MAP_EVERY UNDISCH_TAC [`n DIV 2 < d * (k1 + 1)`; `d * k1 <= n DIV 2`] THEN
2080   ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> ~(a ==> ~(b /\ c))`] THEN
2081   SIMP_TAC[GSYM NOT_LE; LE_LDIV_EQ; LE_RDIV_EQ; ARITH_EQ; lemma; ADD_EQ_0] THEN
2082   REWRITE_TAC[NOT_LE; NOT_IMP] THEN DISCH_TAC THEN DISCH_TAC THEN
2083   SUBGOAL_THEN `d * 2 * k1 < d * (k2 + 1) /\ d * k2 < d * 2 * (k1 + 1)`
2084   MP_TAC THENL [ASM_MESON_TAC[LET_TRANS; MULT_AC]; ALL_TAC] THEN
2085   ASM_REWRITE_TAC[LT_MULT_LCANCEL] THEN
2086   DISCH_THEN(MP_TAC o MATCH_MP
2087    (ARITH_RULE
2088      `2 * k1 < k2 + 1 /\ k2 < 2 * (k1 + 1)
2089       ==> (k2 = 2 * k1) \/ (k2 = 2 * k1 + 1)`)) THEN
2090   DISCH_THEN(DISJ_CASES_THEN SUBST_ALL_TAC) THEN
2091   REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL;
2092               REAL_ADD_SUB; REAL_SUB_REFL] THEN
2093   COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_OF_NUM_EQ; ARITH_EQ] THENL
2094    [ALL_TAC;
2095     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EXISTS_THM]) THEN
2096     DISCH_THEN(MP_TAC o SPEC `2 * k1 + 1`) THEN
2097     ASM_REWRITE_TAC[ARITH_ODD; ODD_ADD; ODD_MULT] THEN
2098     ASM_MESON_TAC[MULT_AC]] THEN
2099   FIRST_X_ASSUM(X_CHOOSE_THEN `k:num` MP_TAC) THEN
2100   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
2101   REWRITE_TAC[ODD_EXISTS; ADD1] THEN
2102   DISCH_THEN(X_CHOOSE_THEN `k3:num` SUBST_ALL_TAC) THEN
2103   SUBGOAL_THEN `d * 2 * k1 < d * ((2 * k3 + 1) + 1) /\
2104                 d * (2 * k3 + 1) < d * 2 * (k1 + 1)`
2105   MP_TAC THENL [ASM_MESON_TAC[LET_TRANS; MULT_AC]; ALL_TAC] THEN
2106   ASM_REWRITE_TAC[LT_MULT_LCANCEL] THEN
2107   DISCH_THEN(SUBST_ALL_TAC o MATCH_MP (ARITH_RULE
2108    `2 * k1 < (2 * k3 + 1) + 1 /\ 2 * k3 + 1 < 2 * (k1 + 1)
2109     ==> (k3 = k1)`)) THEN
2110   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN ARITH_TAC);;
2111
2112 let SUM_EXPAND_LEMMA = prove
2113  (`!n m k. (m + 2 * k = n)
2114          ==> (sum (1,n DIV (2 * k + 1))
2115                   (\d. if ?k. ODD k /\ n DIV (k + 1) < d /\ d <= n DIV k
2116                        then mangoldt d else &0) =
2117               sum (1,n) (\d. --(&1) pow (d + 1) * psi (n DIV d)) -
2118               sum (1,2 * k)
2119                   (\d. --(&1) pow (d + 1) * psi (n DIV d)))`,
2120   GEN_TAC THEN ASM_CASES_TAC `n = 0` THENL
2121    [ASM_SIMP_TAC[DIV_0; ADD_EQ_0; ARITH_EQ; REAL_SUB_REFL; sum]; ALL_TAC] THEN
2122   MATCH_MP_TAC num_WF THEN X_GEN_TAC `m:num` THEN ASM_CASES_TAC `m = 0` THENL
2123    [DISCH_THEN(K ALL_TAC) THEN ASM_SIMP_TAC[ADD_CLAUSES] THEN
2124     ASM_SIMP_TAC[DIV_REFL; SUM_1; DIV_1; REAL_SUB_REFL] THEN
2125     SUBGOAL_THEN `n DIV (n + 1) = 0` (fun th -> REWRITE_TAC[th; sum]) THEN
2126     ASM_MESON_TAC[DIV_EQ_0; ARITH_RULE `n < n + 1 /\ ~(n + 1 = 0)`];
2127     ALL_TAC] THEN
2128   ASM_CASES_TAC `m = 1` THENL
2129    [DISCH_THEN(K ALL_TAC) THEN ASM_REWRITE_TAC[] THEN
2130     X_GEN_TAC `k:num` THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
2131     REWRITE_TAC[GSYM ADD1; ARITH_RULE `1 + n = SUC n`] THEN
2132     SIMP_TAC[DIV_REFL; NOT_SUC; sum; SUM_1] THEN
2133     REWRITE_TAC[REAL_ADD_SUB; mangoldt] THEN
2134     CONV_TAC(ONCE_DEPTH_CONV PRIMEPOW_CONV) THEN
2135     REWRITE_TAC[COND_ID] THEN CONV_TAC SYM_CONV THEN
2136     REWRITE_TAC[REAL_ENTIRE] THEN DISJ2_TAC THEN
2137     REWRITE_TAC[ARITH_RULE `1 + n = SUC n`] THEN
2138     SIMP_TAC[DIV_REFL; NOT_SUC] THEN REWRITE_TAC(LN_1::PSI_LIST 1);
2139     ALL_TAC] THEN
2140   DISCH_THEN(MP_TAC o SPEC `m - 2`) THEN
2141   ASM_SIMP_TAC[ARITH_RULE `~(m = 0) ==> m - 2 < m`] THEN
2142   DISCH_TAC THEN X_GEN_TAC `k:num` THEN DISCH_TAC THEN
2143   FIRST_X_ASSUM(MP_TAC o SPEC `SUC k`) THEN ANTS_TAC THENL
2144    [POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN ARITH_TAC;
2145     ALL_TAC] THEN
2146   GEN_REWRITE_TAC (LAND_CONV o funpow 2 RAND_CONV o TOP_DEPTH_CONV)
2147    [ARITH_RULE `2 * SUC k = SUC(SUC(2 * k))`; sum] THEN
2148   MATCH_MP_TAC(REAL_ARITH
2149    `(s - ss = x + y) ==> (ss = a - ((b + x) + y)) ==> (s = a - b)`) THEN
2150   REWRITE_TAC[REAL_POW_NEG; EVEN_ADD; ARITH_EVEN; EVEN; EVEN_MULT] THEN
2151   REWRITE_TAC[REAL_POW_ONE; REAL_MUL_LID; REAL_MUL_LNEG] THEN
2152   GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [ADD_SYM] THEN
2153   REWRITE_TAC[psi; GSYM real_sub] THEN
2154   MATCH_MP_TAC(REAL_ARITH `!b. (a - b = d) /\ (b = c) ==> (a - c = d)`) THEN
2155   EXISTS_TAC `sum (1,n DIV (SUC (2 * k) + 1))
2156                   (\d. if ?k. ODD k /\ n DIV (k + 1) < d /\ d <= n DIV k
2157                        then mangoldt d else &0)` THEN
2158   CONJ_TAC THENL
2159    [MATCH_MP_TAC SUM_DIFFERENCES_EQ THEN CONJ_TAC THENL
2160      [MATCH_MP_TAC DIV_MONO2 THEN ARITH_TAC; ALL_TAC] THEN
2161     X_GEN_TAC `r:num` THEN REPEAT STRIP_TAC THEN REWRITE_TAC[] THEN
2162     COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
2163     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EXISTS_THM]) THEN
2164     DISCH_THEN(MP_TAC o SPEC `2 * k + 1`) THEN
2165     REWRITE_TAC[ODD_ADD; ODD_MULT; ARITH_ODD] THEN
2166     ASM_REWRITE_TAC[ARITH_RULE `n <= r <=> n < 1 + r`] THEN
2167     ASM_REWRITE_TAC[ARITH_RULE `n < r <=> 1 + n <= r`] THEN
2168     ASM_REWRITE_TAC[ARITH_RULE `(2 * k + 1) + 1 = SUC(2 * k) + 1`];
2169     ALL_TAC] THEN
2170   MATCH_MP_TAC SUM_MORETERMS_EQ THEN CONJ_TAC THENL
2171    [MATCH_MP_TAC DIV_MONO2 THEN ARITH_TAC; ALL_TAC] THEN
2172   X_GEN_TAC `r:num` THEN
2173   REWRITE_TAC[ARITH_RULE `2 * SUC k + 1 = 2 * k + 3`] THEN
2174   REWRITE_TAC[ARITH_RULE `SUC(2 * k) + 1 = 2 * k + 2`] THEN STRIP_TAC THEN
2175   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
2176   FIRST_X_ASSUM(X_CHOOSE_THEN `oj:num` MP_TAC) THEN
2177   REWRITE_TAC[ODD_EXISTS] THEN
2178   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2179   FIRST_X_ASSUM(X_CHOOSE_THEN `j:num` SUBST1_TAC) THEN
2180   REWRITE_TAC[ARITH_RULE `SUC(2 * k) + 1 = 2 * k + 2`] THEN
2181   REWRITE_TAC[ARITH_RULE `SUC(2 * k) = 2 * k + 1`] THEN
2182   FIRST_X_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE `1 + a <= b ==> a < b`)) THEN
2183   FIRST_X_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE `a < 1 + b ==> a <= b`)) THEN
2184   SIMP_TAC[GSYM NOT_LE; LE_RDIV_EQ; LE_LDIV_EQ; ADD_EQ_0; ARITH_EQ] THEN
2185   REWRITE_TAC[NOT_LE] THEN REPEAT STRIP_TAC THEN
2186   SUBGOAL_THEN `(2 * j + 1) * r < (2 * k + 3) * r /\
2187                 (2 * k + 2) * r < (2 * j + 2) * r`
2188   MP_TAC THENL [ASM_MESON_TAC[LET_TRANS]; ALL_TAC] THEN
2189   ASM_REWRITE_TAC[LT_MULT_RCANCEL] THEN
2190   ASM_CASES_TAC `r = 0` THEN ASM_REWRITE_TAC[] THEN
2191   DISCH_THEN(SUBST_ALL_TAC o MATCH_MP (ARITH_RULE
2192    `2 * j + 1 < 2 * k + 3 /\ 2 * k + 2 < 2 * j + 2 ==> (j = k)`)) THEN
2193   ASM_MESON_TAC[LET_TRANS; LT_REFL; MULT_AC]);;
2194
2195 let FACT_EXPAND_PSI = prove
2196  (`!n. ln(&(FACT(n))) - &2 * ln(&(FACT(n DIV 2))) =
2197           sum(1,n) (\d. --(&1) pow (d + 1) * psi(n DIV d))`,
2198   GEN_TAC THEN REWRITE_TAC[MANGOLDT] THEN
2199   SUBGOAL_THEN
2200    `sum (1,n DIV 2) (\d. mangoldt d * floor (&(n DIV 2) / &d)) =
2201     sum (1,n) (\d. mangoldt d * floor (&(n DIV 2) / &d))`
2202   SUBST1_TAC THENL
2203    [SUBGOAL_THEN `n = n DIV 2 + (n - n DIV 2)`
2204      (fun th -> GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV) [th])
2205     THENL [MESON_TAC[SUB_ADD; DIV_LE; ADD_SYM; NUM_REDUCE_CONV `2 = 0`];
2206            ALL_TAC] THEN
2207     REWRITE_TAC[GSYM SUM_SPLIT] THEN
2208     MATCH_MP_TAC(REAL_ARITH `(b = &0) ==> (a = a + b)`) THEN
2209     MATCH_MP_TAC SUM_EQ_0 THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
2210     REWRITE_TAC[REAL_ENTIRE; FLOOR_EQ_0] THEN DISJ2_TAC THEN
2211     SIMP_TAC[REAL_LE_DIV; REAL_POS] THEN
2212     SUBGOAL_THEN `0 < r /\ n DIV 2 < r` MP_TAC THENL
2213      [UNDISCH_TAC `1 + n DIV 2 <= r` THEN ARITH_TAC; ALL_TAC] THEN
2214     SIMP_TAC[REAL_LT_LDIV_EQ; REAL_OF_NUM_LT; REAL_MUL_LID];
2215     ALL_TAC] THEN
2216   REWRITE_TAC[GSYM SUM_CMUL; GSYM SUM_SUB] THEN
2217   REWRITE_TAC[REAL_ARITH `m * x - &2 * m * y = m * (x - &2 * y)`] THEN
2218   MATCH_MP_TAC EQ_TRANS THEN
2219   EXISTS_TAC
2220    `sum(1,n) (\d. if ?k. ODD k /\ n DIV (k + 1) < d /\ d <= n DIV k
2221                   then mangoldt d else &0)` THEN
2222   CONJ_TAC THENL
2223    [MATCH_MP_TAC SUM_EQ THEN
2224     X_GEN_TAC `r:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN
2225     ASM_SIMP_TAC[FLOOR_HALF_INTERVAL; ARITH_RULE `1 <= d ==> ~(d = 0)`] THEN
2226     COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_MUL_RID; REAL_MUL_RZERO];
2227     ALL_TAC] THEN
2228   MP_TAC(SPECL [`n:num`; `n:num`; `0`] SUM_EXPAND_LEMMA) THEN
2229   REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES; sum; REAL_SUB_RZERO; DIV_1]);;
2230
2231 (* ------------------------------------------------------------------------- *)
2232 (* Show that we can get bounds by cutting off at odd/even points.            *)
2233 (* ------------------------------------------------------------------------- *)
2234
2235 let PSI_MONO = prove
2236  (`!m n. m <= n ==> psi(m) <= psi(n)`,
2237   SIMP_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM; psi] THEN
2238   REWRITE_TAC[GSYM SUM_SPLIT] THEN
2239   REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_LE_ADDR] THEN
2240   MATCH_MP_TAC SUM_POS_GEN THEN REWRITE_TAC[MANGOLDT_POS]);;
2241
2242 let PSI_POS = prove
2243  (`!n. &0 <= psi(n)`,
2244   SUBGOAL_THEN `psi(0) = &0` (fun th -> MESON_TAC[th; PSI_MONO; LE_0]) THEN
2245   REWRITE_TAC(LN_1::PSI_LIST 0));;
2246
2247 let PSI_EXPANSION_CUTOFF = prove
2248  (`!n m p. m <= p
2249          ==> sum(1,2 * m) (\d. --(&1) pow (d + 1) * psi(n DIV d))
2250                <= sum(1,2 * p) (\d. --(&1) pow (d + 1) * psi(n DIV d)) /\
2251              sum(1,2 * p + 1) (\d. --(&1) pow (d + 1) * psi(n DIV d))
2252                <= sum(1,2 * m + 1) (\d. --(&1) pow (d + 1) * psi(n DIV d))`,
2253   GEN_TAC THEN SIMP_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM] THEN
2254   GEN_REWRITE_TAC BINDER_CONV [SWAP_FORALL_THM] THEN
2255   SIMP_TAC[LEFT_FORALL_IMP_THM; EXISTS_REFL] THEN
2256   X_GEN_TAC `m:num` THEN INDUCT_TAC THEN
2257   REWRITE_TAC[ADD_CLAUSES; REAL_LE_REFL] THEN
2258   REWRITE_TAC[ARITH_RULE `2 * SUC n = SUC(SUC(2 * n))`;
2259               ARITH_RULE `SUC(SUC n) + 1 = SUC(SUC(n + 1))`; sum] THEN
2260   FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
2261    `s1 <= s1' /\ s2' <= s2
2262     ==> &0 <= a + b /\ &0 <= --c + --d
2263         ==> s1 <= (s1' + a) + b /\ (s2' + c) + d <= s2`)) THEN
2264   REWRITE_TAC[REAL_POW_NEG; EVEN_ADD; EVEN_MULT; ARITH_EVEN; EVEN] THEN
2265   REWRITE_TAC[REAL_POW_ONE; REAL_MUL_LID; REAL_MUL_LNEG; REAL_NEG_NEG] THEN
2266   REWRITE_TAC[REAL_ARITH `&0 <= a + --b <=> b <= a`] THEN
2267   CONJ_TAC THEN MATCH_MP_TAC PSI_MONO THEN
2268   MATCH_MP_TAC DIV_MONO2 THEN ARITH_TAC);;
2269
2270 let FACT_PSI_BOUND_ODD = prove
2271  (`!n k. ODD(k)
2272          ==> ln(&(FACT n)) - &2 * ln(&(FACT (n DIV 2)))
2273              <= sum(1,k) (\d. --(&1) pow (d + 1) * psi(n DIV d))`,
2274   REPEAT STRIP_TAC THEN REWRITE_TAC[FACT_EXPAND_PSI] THEN
2275   ASM_CASES_TAC `k <= n:num` THENL
2276    [ALL_TAC;
2277     MATCH_MP_TAC(REAL_ARITH `(b = a) ==> a <= b`) THEN
2278     MATCH_MP_TAC SUM_MORETERMS_EQ THEN
2279     ASM_SIMP_TAC[ARITH_RULE `~(k <= n) ==> n <= k:num`] THEN
2280     X_GEN_TAC `r:num` THEN STRIP_TAC THEN REWRITE_TAC[REAL_ENTIRE] THEN
2281     DISJ2_TAC THEN SUBGOAL_THEN `n DIV r = 0` SUBST1_TAC THENL
2282      [ASM_MESON_TAC[DIV_EQ_0; ARITH_RULE `1 + n <= r ==> n < r /\ ~(r = 0)`];
2283       REWRITE_TAC(LN_1::PSI_LIST 0)]] THEN
2284   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ODD_EXISTS]) THEN
2285   DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
2286   MATCH_MP_TAC REAL_LE_TRANS THEN
2287   EXISTS_TAC `sum(1,SUC(2 * n DIV 2))
2288                  (\d. -- &1 pow (d + 1) * psi (n DIV d))` THEN
2289   CONJ_TAC THENL
2290    [ALL_TAC;
2291     SUBGOAL_THEN `m <= n DIV 2`
2292      (fun th -> SIMP_TAC[th; ADD1; PSI_EXPANSION_CUTOFF]) THEN
2293     SIMP_TAC[LE_RDIV_EQ; ARITH_EQ] THEN
2294     POP_ASSUM MP_TAC THEN ARITH_TAC] THEN
2295   MP_TAC(SPECL [`n:num`; `2`] DIVISION) THEN REWRITE_TAC[ARITH_EQ] THEN
2296   MAP_EVERY ABBREV_TAC [`q = n DIV 2`; `r = n MOD 2`] THEN
2297   DISCH_THEN(CONJUNCTS_THEN2
2298    (fun th -> GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o RAND_CONV) [th])
2299    MP_TAC) THEN
2300   REWRITE_TAC[ARITH_RULE `r < 2 <=> (r = 0) \/ (r = 1)`] THEN
2301   DISCH_THEN(DISJ_CASES_THEN SUBST_ALL_TAC) THEN
2302   REWRITE_TAC[ADD1; MULT_AC; REAL_LE_REFL] THEN
2303   REWRITE_TAC[GSYM ADD1; ADD_CLAUSES; sum; REAL_LE_ADDR] THEN
2304   REWRITE_TAC[REAL_POW_NEG; EVEN; EVEN_ADD; EVEN_MULT; ARITH_EVEN] THEN
2305   REWRITE_TAC[REAL_POW_ONE; REAL_MUL_LID; PSI_POS]);;
2306
2307 let FACT_PSI_BOUND_EVEN = prove
2308  (`!n k. EVEN(k)
2309          ==> sum(1,k) (\d. --(&1) pow (d + 1) * psi(n DIV d))
2310              <= ln(&(FACT n)) - &2 * ln(&(FACT (n DIV 2)))`,
2311   REPEAT STRIP_TAC THEN REWRITE_TAC[FACT_EXPAND_PSI] THEN
2312   ASM_CASES_TAC `k <= n:num` THENL
2313    [ALL_TAC;
2314     MATCH_MP_TAC(REAL_ARITH `(a = b) ==> a <= b`) THEN
2315     MATCH_MP_TAC SUM_MORETERMS_EQ THEN
2316     ASM_SIMP_TAC[ARITH_RULE `~(k <= n) ==> n <= k:num`] THEN
2317     X_GEN_TAC `r:num` THEN STRIP_TAC THEN REWRITE_TAC[REAL_ENTIRE] THEN
2318     DISJ2_TAC THEN SUBGOAL_THEN `n DIV r = 0` SUBST1_TAC THENL
2319      [ASM_MESON_TAC[DIV_EQ_0; ARITH_RULE `1 + n <= r ==> n < r /\ ~(r = 0)`];
2320       REWRITE_TAC(LN_1::PSI_LIST 0)]] THEN
2321   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [EVEN_EXISTS]) THEN
2322   DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
2323   MATCH_MP_TAC REAL_LE_TRANS THEN
2324   EXISTS_TAC `sum(1,2 * n DIV 2)
2325                  (\d. -- &1 pow (d + 1) * psi (n DIV d))` THEN
2326   CONJ_TAC THENL
2327    [SUBGOAL_THEN `m <= n DIV 2`
2328      (fun th -> SIMP_TAC[th; ADD1; PSI_EXPANSION_CUTOFF]) THEN
2329     SIMP_TAC[LE_RDIV_EQ; ARITH_EQ] THEN
2330     POP_ASSUM MP_TAC THEN ARITH_TAC;
2331     ALL_TAC] THEN
2332   MP_TAC(SPECL [`n:num`; `2`] DIVISION) THEN REWRITE_TAC[ARITH_EQ] THEN
2333   MAP_EVERY ABBREV_TAC [`q = n DIV 2`; `r = n MOD 2`] THEN
2334   DISCH_THEN(CONJUNCTS_THEN2
2335    (fun th -> GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV) [th])
2336    MP_TAC) THEN
2337   REWRITE_TAC[ARITH_RULE `r < 2 <=> (r = 0) \/ (r = 1)`] THEN
2338   DISCH_THEN(DISJ_CASES_THEN SUBST_ALL_TAC) THEN
2339   REWRITE_TAC[ADD1; MULT_AC; ADD_CLAUSES; REAL_LE_REFL] THEN
2340   REWRITE_TAC[GSYM ADD1; ADD_CLAUSES; sum; REAL_LE_ADDR] THEN
2341   REWRITE_TAC[REAL_POW_NEG; EVEN; EVEN_ADD; EVEN_MULT; ARITH_EVEN] THEN
2342   REWRITE_TAC[REAL_POW_ONE; REAL_MUL_LID; PSI_POS]);;
2343
2344 (* ------------------------------------------------------------------------- *)
2345 (* In particular, we will use these.                                         *)
2346 (* ------------------------------------------------------------------------- *)
2347
2348 let FACT_PSI_BOUND_2_3 = prove
2349  (`!n. psi(n) - psi(n DIV 2)
2350        <= ln(&(FACT n)) - &2 * ln(&(FACT (n DIV 2))) /\
2351        ln(&(FACT n)) - &2 * ln(&(FACT (n DIV 2)))
2352        <= psi(n) - psi(n DIV 2) + psi(n DIV 3)`,
2353   GEN_TAC THEN
2354   MP_TAC(SPECL [`n:num`; `2`] FACT_PSI_BOUND_EVEN) THEN
2355   MP_TAC(SPECL [`n:num`; `3`] FACT_PSI_BOUND_ODD) THEN
2356   REWRITE_TAC[ARITH] THEN
2357   CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN
2358   REWRITE_TAC[ARITH; REAL_ADD_LID; DIV_1] THEN
2359   REWRITE_TAC[REAL_POW_NEG; ARITH; REAL_POW_ONE; REAL_MUL_LID] THEN
2360   REAL_ARITH_TAC);;
2361
2362 (* ------------------------------------------------------------------------- *)
2363 (* Hence get a good lower bound on psi(n) - psi(n/2).                        *)
2364 (* ------------------------------------------------------------------------- *)
2365
2366 let PSI_DOUBLE_LEMMA = prove
2367  (`!n. n >= 1200 ==> &n / &6 <= psi(n) - psi(n DIV 2)`,
2368   REPEAT STRIP_TAC THEN MP_TAC(SPEC `n:num` FACT_PSI_BOUND_2_3) THEN
2369   MATCH_MP_TAC(REAL_ARITH
2370    `b + p3 <= a ==> u <= v /\ a <= p - p2 + p3 ==> b <= p - p2`) THEN
2371   MATCH_MP_TAC REAL_LE_TRANS THEN
2372   EXISTS_TAC `&n / &6 + &n / &2` THEN CONJ_TAC THENL
2373    [REWRITE_TAC[REAL_LE_LADD] THEN MP_TAC(SPEC `n DIV 3` PSI_UBOUND_3_2) THEN
2374     MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
2375     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&3 / &2 * &n / &3` THEN
2376     CONJ_TAC THENL
2377      [MATCH_MP_TAC REAL_LE_LMUL THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
2378       SIMP_TAC[REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
2379       REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_LE] THEN
2380       MP_TAC(SPECL [`n:num`; `3`] DIVISION) THEN ARITH_TAC;
2381       ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
2382       REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
2383       CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_LE_REFL]];
2384     ALL_TAC] THEN
2385   MP_TAC(SPEC `n:num` LN_FACT_DIFF_BOUNDS) THEN
2386   MATCH_MP_TAC(REAL_ARITH
2387    `ltm <= nl2 - a ==> abs(lf - nl2) <= ltm ==> a <= lf`) THEN
2388   ASM_SIMP_TAC[ARITH_RULE `n >= 1200 ==> ~(n = 0)`] THEN
2389   REWRITE_TAC[real_div; GSYM REAL_SUB_LDISTRIB; GSYM REAL_ADD_LDISTRIB] THEN
2390   MATCH_MP_TAC REAL_LE_TRANS THEN
2391   EXISTS_TAC `&n * &1 / &38` THEN CONJ_TAC THENL
2392    [ALL_TAC;
2393     MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN
2394     SIMP_TAC[REAL_LE_SUB_LADD] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
2395     CONV_TAC(RAND_CONV LN_N2_CONV) THEN CONV_TAC REALCALC_REL_CONV] THEN
2396   SUBST1_TAC(REAL_ARITH `&n = &1 + (&n - &1)`) THEN
2397   FIRST_X_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
2398    `n >= b ==> b <= n:num`)) THEN
2399   GEN_REWRITE_TAC LAND_CONV [GSYM REAL_OF_NUM_LE] THEN
2400   DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
2401    `a <= n ==> a - &1 <= n - &1`)) THEN
2402   ABBREV_TAC `x = &n - &1` THEN
2403   CONV_TAC(LAND_CONV NUM_REDUCE_CONV THENC REAL_RAT_REDUCE_CONV) THEN
2404   SPEC_TAC(`x:real`,`x:real`) THEN POP_ASSUM_LIST(K ALL_TAC) THEN
2405   MATCH_MP_TAC OVERPOWER_LEMMA THEN
2406   W(fun (asl,w) ->
2407       let th = DIFF_CONV
2408        (lhand(rator(rand(body(rand(lhand(rand(body(rand w))))))))) in
2409       MP_TAC th) THEN
2410   GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV)
2411    [REAL_MUL_LZERO; REAL_ADD_LID; REAL_ADD_RID;
2412     REAL_MUL_RID; REAL_MUL_LID] THEN
2413   W(fun (asl,w) ->
2414       let tm = mk_abs(`x:real`,rand(rator(rand(body(rand(lhand w)))))) in
2415       DISCH_TAC THEN EXISTS_TAC tm) THEN
2416   CONJ_TAC THENL
2417    [CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[real_sub] THEN
2418     CONV_TAC(ONCE_DEPTH_CONV LN_N2_CONV) THEN
2419     CONV_TAC REALCALC_REL_CONV;
2420     ALL_TAC] THEN
2421   REWRITE_TAC[] THEN CONJ_TAC THENL
2422    [GEN_TAC THEN
2423     DISCH_THEN(fun th -> FIRST_ASSUM MATCH_MP_TAC THEN MP_TAC th) THEN
2424     REAL_ARITH_TAC;
2425     ALL_TAC] THEN
2426   X_GEN_TAC `x:real` THEN DISCH_TAC THEN REWRITE_TAC[REAL_SUB_LE] THEN
2427   SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
2428   FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
2429    `a <= x ==> inv(&1 + x) <= inv(&1 + a) /\
2430                inv(&1 + a) <= b ==> inv(&1 + x) <= b`)) THEN
2431   CONJ_TAC THENL
2432    [MATCH_MP_TAC REAL_LE_INV2 THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
2433     POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
2434     ALL_TAC] THEN
2435   CONV_TAC REAL_RAT_REDUCE_CONV);;
2436
2437 (* ------------------------------------------------------------------------- *)
2438 (* Hence show that theta changes (could get a lower bound like n/10).        *)
2439 (* ------------------------------------------------------------------------- *)
2440
2441 let THETA_DOUBLE_LEMMA = prove
2442  (`!n. n >= 1200 ==> theta(n DIV 2) < theta(n)`,
2443   REPEAT STRIP_TAC THEN
2444   MP_TAC(CONJUNCT2 (SPEC `n:num` PSI_THETA)) THEN
2445   MP_TAC(CONJUNCT1 (SPEC `n DIV 2` PSI_THETA)) THEN
2446   FIRST_ASSUM(MP_TAC o MATCH_MP PSI_DOUBLE_LEMMA) THEN
2447   MP_TAC(SPEC `ISQRT(n DIV 2)` PSI_POS) THEN
2448   SUBGOAL_THEN
2449    `&2 * psi (ISQRT n) < &n / &6`
2450    (fun th -> MP_TAC th THEN REAL_ARITH_TAC) THEN
2451   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
2452   SIMP_TAC[GSYM REAL_LT_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
2453   REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
2454   MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `&3 / &2 * &(ISQRT n)` THEN
2455   REWRITE_TAC[PSI_UBOUND_3_2] THEN
2456   GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
2457   SIMP_TAC[GSYM REAL_LT_RDIV_EQ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
2458   REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
2459   CONV_TAC REAL_RAT_REDUCE_CONV THEN
2460   REWRITE_TAC[real_div; REAL_MUL_LID] THEN
2461   SIMP_TAC[GSYM real_div; REAL_LT_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
2462   REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_LT] THEN
2463   SUBGOAL_THEN `(ISQRT n * 18) EXP (SUC 1) < n EXP (SUC 1)` MP_TAC THENL
2464    [ALL_TAC; REWRITE_TAC[EXP_MONO_LT_SUC]] THEN
2465   REWRITE_TAC[EXP; EXP_1] THEN
2466   MATCH_MP_TAC(ARITH_RULE `324 * i * i < a ==> (i * 18) * (i * 18) < a`) THEN
2467   MATCH_MP_TAC LET_TRANS THEN EXISTS_TAC `324 * n` THEN CONJ_TAC THENL
2468    [REWRITE_TAC[GSYM EXP_2; ISQRT_WORKS; LE_MULT_LCANCEL];
2469     REWRITE_TAC[LT_MULT_RCANCEL] THEN POP_ASSUM MP_TAC THEN ARITH_TAC]);;
2470
2471 (* ------------------------------------------------------------------------- *)
2472 (* Hence Bertrand for sufficiently large n.                                  *)
2473 (* ------------------------------------------------------------------------- *)
2474
2475 let BIG_BERTRAND = prove
2476  (`!n. n >= 2400 ==> ?p. prime(p) /\ n <= p /\ p <= 2 * n`,
2477   REPEAT STRIP_TAC THEN MP_TAC(SPEC `2 * n` THETA_DOUBLE_LEMMA) THEN
2478   ANTS_TAC THENL [POP_ASSUM MP_TAC THEN ARITH_TAC; ALL_TAC] THEN
2479   SIMP_TAC[DIV_MULT; ARITH_EQ] THEN
2480   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
2481   REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(a /\ b /\ c) <=> b /\ c ==> ~a`] THEN
2482   DISCH_TAC THEN
2483   SUBGOAL_THEN `sum(n + 1,n) (\p. if prime p then ln (&p) else &0) = &0`
2484   MP_TAC THENL
2485    [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `sum(n + 1,n) (\r. &0)` THEN
2486     CONJ_TAC THENL [ALL_TAC; REWRITE_TAC[SUM_0]] THEN
2487     MATCH_MP_TAC SUM_EQ THEN
2488     ASM_SIMP_TAC[ARITH_RULE
2489      `n + 1 <= r /\ r < n + n + 1 ==> n <= r /\ r <= 2 * n`];
2490     ALL_TAC] THEN
2491   MATCH_MP_TAC(REAL_ARITH `(b + a = c) ==> (a = &0) ==> ~(b < c)`) THEN
2492   REWRITE_TAC[theta] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
2493   REWRITE_TAC[SUM_SPLIT] THEN
2494   REWRITE_TAC[MULT_2]);;
2495
2496 (* ------------------------------------------------------------------------- *)
2497 (* Landau trick. Should be automatic but ARITH_RULE is a bit slow.           *)
2498 (* (Direct use of ARITH_RULE takes about 3 minutes on my current laptop.)    *)
2499 (* ------------------------------------------------------------------------- *)
2500
2501 let LANDAU_TRICK = prove
2502  (`!n. 0 < n /\ n < 2400
2503        ==> n <= 2 /\ 2 <= 2 * n \/
2504            n <= 3 /\ 3 <= 2 * n \/
2505            n <= 5 /\ 5 <= 2 * n \/
2506            n <= 7 /\ 7 <= 2 * n \/
2507            n <= 13 /\ 13 <= 2 * n \/
2508            n <= 23 /\ 23 <= 2 * n \/
2509            n <= 43 /\ 43 <= 2 * n \/
2510            n <= 83 /\ 83 <= 2 * n \/
2511            n <= 163 /\ 163 <= 2 * n \/
2512            n <= 317 /\ 317 <= 2 * n \/
2513            n <= 631 /\ 631 <= 2 * n \/
2514            n <= 1259 /\ 1259 <= 2 * n \/
2515            n <= 2503 /\ 2503 <= 2 * n`,
2516   let lemma = TAUT
2517    `(p /\ b1 ==> a1) /\ (~b1 ==> a2) ==> p ==> b1 /\ a1 \/ a2` in
2518   GEN_TAC THEN ONCE_REWRITE_TAC[TAUT `a /\ b ==> c <=> a ==> c \/ ~b`] THEN
2519   REWRITE_TAC[GSYM DISJ_ASSOC] THEN
2520   REPEAT(MATCH_MP_TAC lemma THEN CONJ_TAC THENL [ARITH_TAC; ALL_TAC]) THEN
2521   ARITH_TAC);;
2522
2523 (* ------------------------------------------------------------------------- *)
2524 (* Bertrand for all nonzero n using "Landau trick".                          *)
2525 (* ------------------------------------------------------------------------- *)
2526
2527 let BERTRAND = prove
2528  (`!n. ~(n = 0) ==> ?p. prime p /\ n <= p /\ p <= 2 * n`,
2529   REPEAT STRIP_TAC THEN
2530   DISJ_CASES_TAC(ARITH_RULE `n >= 2400 \/ n < 2400`) THEN
2531   ASM_SIMP_TAC[BIG_BERTRAND] THEN MP_TAC(SPEC `n:num` LANDAU_TRICK) THEN
2532   ASM_REWRITE_TAC[ARITH_RULE `0 < n <=> ~(n = 0)`] THEN
2533   STRIP_TAC THEN
2534   ASM_MESON_TAC(map (PRIME_CONV o curry mk_comb `prime` o mk_small_numeral)
2535                     [2;3;5;7;13;23;43;83;163;317;631;1259;2503]));;
2536
2537 (* ========================================================================= *)
2538 (* Weak form of the Prime Number Theorem.                                    *)
2539 (* ========================================================================= *)
2540
2541 let pii = new_definition
2542   `pii(n) = sum(1,n) (\p. if prime(p) then &1 else &0)`;;
2543
2544 (* ------------------------------------------------------------------------- *)
2545 (* An optimized rule to give pii(n) for all n <= some N.                     *)
2546 (* ------------------------------------------------------------------------- *)
2547
2548 let PII_LIST =
2549   let PII_0 = prove
2550    (`pii(0) = &0`,
2551     REWRITE_TAC[pii; sum])
2552   and PII_SUC = prove
2553    (`pii(SUC n) = pii(n) + (if prime(SUC n) then &1 else &0)`,
2554     REWRITE_TAC[pii; sum; ADD1] THEN REWRITE_TAC[ADD_AC])
2555   and n_tm = `n:num`
2556   and SIMPER_CONV =
2557     NUM_REDUCE_CONV THENC
2558     ONCE_DEPTH_CONV PRIME_CONV THENC
2559     GEN_REWRITE_CONV TOP_DEPTH_CONV [COND_CLAUSES] THENC
2560     REAL_RAT_REDUCE_CONV in
2561   let rec PII_LIST n =
2562     if n = 0 then [PII_0] else
2563     let ths = PII_LIST (n - 1) in
2564     let th1 = INST [mk_small_numeral(n-1),n_tm] PII_SUC in
2565     let th2 = GEN_REWRITE_RULE (RAND_CONV o LAND_CONV) [hd ths] th1 in
2566     CONV_RULE SIMPER_CONV th2::ths in
2567   PII_LIST;;
2568
2569 (* ------------------------------------------------------------------------- *)
2570 (* Prove the usual characterization.                                         *)
2571 (* ------------------------------------------------------------------------- *)
2572
2573 let PRIMES_FINITE = prove
2574  (`!n. FINITE {p | p <= n /\ prime(p)}`,
2575   GEN_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
2576   EXISTS_TAC `{p | p < SUC n}` THEN REWRITE_TAC[FINITE_NUMSEG_LT] THEN
2577   REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN ARITH_TAC);;
2578
2579 let PII = prove
2580  (`!n. pii(n) = &(CARD {p | p <= n /\ prime(p)})`,
2581   INDUCT_TAC THENL
2582    [SUBGOAL_THEN `{p | p <= 0 /\ prime p} = {}`
2583      (fun th -> REWRITE_TAC(th::CARD_CLAUSES::PII_LIST 0)) THEN
2584     REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
2585     MESON_TAC[LE; PRIME_0; NOT_IN_EMPTY];
2586     ALL_TAC] THEN
2587   SUBGOAL_THEN `{p | p <= SUC n /\ prime p} =
2588                 if prime(SUC n) then (SUC n) INSERT {p | p <= n /\ prime p}
2589                 else {p | p <= n /\ prime p}`
2590   SUBST1_TAC THENL
2591    [COND_CASES_TAC THEN ASM_REWRITE_TAC[EXTENSION; IN_INSERT; IN_ELIM_THM] THEN
2592     ASM_MESON_TAC[LE];
2593     ALL_TAC] THEN
2594   REWRITE_TAC[pii; sum] THEN REWRITE_TAC[GSYM pii] THEN
2595   REWRITE_TAC[ARITH_RULE `1 + n = SUC n`] THEN
2596   COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_ADD_RID] THEN
2597   SIMP_TAC[CARD_CLAUSES; PRIMES_FINITE] THEN COND_CASES_TAC THENL
2598    [RULE_ASSUM_TAC(REWRITE_RULE[IN_ELIM_THM]) THEN
2599     ASM_MESON_TAC[ARITH_RULE `~(SUC n <= n)`];
2600     REWRITE_TAC[REAL_OF_NUM_SUC]]);;
2601
2602 (* ------------------------------------------------------------------------- *)
2603 (* One bound is a simple consequence of the one for theta.                   *)
2604 (* ------------------------------------------------------------------------- *)
2605
2606 let PII_LBOUND = prove
2607  (`!n. 3 <= n ==> &1 / &2 * (&n / ln(&n)) <= pii(n)`,
2608   REPEAT STRIP_TAC THEN REWRITE_TAC[real_div; REAL_MUL_ASSOC] THEN
2609   ASM_SIMP_TAC[GSYM real_div; REAL_LE_LDIV_EQ; LN_POS_LT; REAL_OF_NUM_LT;
2610                ARITH_RULE `3 <= n ==> 1 < n`] THEN
2611   GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
2612   FIRST_X_ASSUM(REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC o MATCH_MP
2613    (ARITH_RULE `3 <= n ==> (n = 3) \/ (n = 4) \/ 5 <= n`)) THEN
2614   ASM_REWRITE_TAC(PII_LIST 4) THENL
2615    [CONV_TAC(ONCE_DEPTH_CONV LN_N2_CONV) THEN CONV_TAC REALCALC_REL_CONV;
2616     CONV_TAC(ONCE_DEPTH_CONV LN_N2_CONV) THEN CONV_TAC REALCALC_REL_CONV;
2617     ALL_TAC] THEN
2618   FIRST_ASSUM(MP_TAC o MATCH_MP THETA_LBOUND_1_2) THEN
2619   MATCH_MP_TAC(REAL_ARITH `x <= y ==> a <= x ==> a <= y`) THEN
2620   REWRITE_TAC[theta; pii; GSYM SUM_CMUL] THEN
2621   MATCH_MP_TAC SUM_LE THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
2622   REWRITE_TAC[] THEN COND_CASES_TAC THEN
2623   REWRITE_TAC[REAL_MUL_RZERO; REAL_MUL_RID; REAL_LE_REFL] THEN
2624   SUBGOAL_THEN `&0 < &r /\ &r <= &n`
2625    (fun th -> MESON_TAC[th; LN_MONO_LE; REAL_LTE_TRANS]) THEN
2626   REWRITE_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_LE] THEN
2627   UNDISCH_TAC `1 <= r` THEN UNDISCH_TAC `r < n + 1` THEN ARITH_TAC);;
2628
2629 (* ------------------------------------------------------------------------- *)
2630 (* First prove the upper bound for the first 50 numbers, to start with.      *)
2631 (* ------------------------------------------------------------------------- *)
2632
2633 let PII_UBOUND_CASES_50 = prove
2634  (`!n. n < 50 ==> 3 <= n ==> ln(&n) * pii(n) <= &5 * &n`,
2635   let tac = CONV_TAC(ONCE_DEPTH_CONV LN_N2_CONV THENC REALCALC_REL_CONV) in
2636   CONV_TAC EXPAND_CASES_CONV THEN CONV_TAC NUM_REDUCE_CONV THEN
2637   CONV_TAC REAL_RAT_REDUCE_CONV THEN
2638   REWRITE_TAC(PII_LIST 49) THEN
2639   SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
2640   CONV_TAC REAL_RAT_REDUCE_CONV THEN
2641   REPEAT(CONJ_TAC THENL [tac THEN NO_TAC; ALL_TAC]) THEN tac);;
2642
2643 (* ------------------------------------------------------------------------- *)
2644 (* An extra trivial pair of lemmas.                                          *)
2645 (* ------------------------------------------------------------------------- *)
2646
2647 let THETA_POS = prove
2648  (`!n. &0 <= theta n`,
2649   GEN_TAC THEN REWRITE_TAC[theta] THEN
2650   MATCH_MP_TAC SUM_POS_GEN THEN
2651   X_GEN_TAC `p:num` THEN DISCH_TAC THEN REWRITE_TAC[] THEN
2652   COND_CASES_TAC THEN
2653   ASM_SIMP_TAC[LE_REFL; LN_POS; REAL_OF_NUM_LE]);;
2654
2655 let PII_MONO = prove
2656  (`!m n. m <= n ==> pii(m) <= pii(n)`,
2657   SIMP_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM; pii] THEN
2658   REWRITE_TAC[GSYM SUM_SPLIT] THEN
2659   REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_LE_ADDR] THEN
2660   MATCH_MP_TAC SUM_POS_GEN THEN
2661   GEN_TAC THEN REWRITE_TAC[] THEN COND_CASES_TAC THEN
2662   CONV_TAC REAL_RAT_REDUCE_CONV);;
2663
2664 let PII_POS = prove
2665  (`!n. &0 <= pii(n)`,
2666   SUBGOAL_THEN `pii(0) = &0` (fun th -> MESON_TAC[th; PII_MONO; LE_0]) THEN
2667   REWRITE_TAC(LN_1::PII_LIST 0));;
2668
2669 (* ------------------------------------------------------------------------- *)
2670 (* The induction principle we can use.                                       *)
2671 (* ------------------------------------------------------------------------- *)
2672
2673 let PII_CHANGE = prove
2674  (`!m n. ~(m = 0) ==> ln(&m) * (pii n - pii m) <= &3 / &2 * &n`,
2675   REPEAT STRIP_TAC THEN ASM_CASES_TAC `m <= n:num` THENL
2676    [ALL_TAC;
2677     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&0` THEN CONJ_TAC THENL
2678      [ALL_TAC;
2679       MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_POS] THEN
2680       CONV_TAC REAL_RAT_REDUCE_CONV] THEN
2681     MATCH_MP_TAC(REAL_ARITH `&0 <= a * (c - b) ==> a * (b - c) <= &0`) THEN
2682     MATCH_MP_TAC REAL_LE_MUL THEN
2683     ASM_SIMP_TAC[LN_POS; REAL_OF_NUM_LE; ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN
2684     REWRITE_TAC[REAL_SUB_LE] THEN MATCH_MP_TAC PII_MONO THEN
2685     UNDISCH_TAC `~(m <= n:num)` THEN ARITH_TAC] THEN
2686   MATCH_MP_TAC REAL_LE_TRANS THEN
2687   EXISTS_TAC `theta n` THEN REWRITE_TAC[THETA_UBOUND_3_2] THEN
2688   MP_TAC(SPEC `m:num` THETA_POS) THEN
2689   MATCH_MP_TAC(REAL_ARITH `a <= n - m ==> &0 <= m ==> a <= n`) THEN
2690   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LE_EXISTS]) THEN
2691   DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
2692   REWRITE_TAC[pii; theta; GSYM SUM_SPLIT; REAL_ADD_SUB] THEN
2693   REWRITE_TAC[GSYM SUM_CMUL] THEN
2694   MATCH_MP_TAC SUM_LE THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
2695   REWRITE_TAC[] THEN COND_CASES_TAC THEN
2696   REWRITE_TAC[REAL_MUL_RZERO; REAL_LE_REFL; REAL_MUL_RID] THEN
2697   SUBGOAL_THEN `&0 < &m /\ &m <= &r`
2698    (fun th -> MESON_TAC[th; LN_MONO_LE; REAL_LTE_TRANS]) THEN
2699   REWRITE_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_LE] THEN
2700   UNDISCH_TAC `1 + m <= r` THEN UNDISCH_TAC `~(m = 0)` THEN ARITH_TAC);;
2701
2702 let PII_ISQRT_INDUCT = prove
2703  (`!n. 50 <= n
2704        ==> ln(&n) * pii(n)
2705            <= &9 / &4 * (&3 / &2 * &n + ln(&(ISQRT(n))) * pii(ISQRT(n)))`,
2706   REPEAT STRIP_TAC THEN
2707   GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
2708   SIMP_TAC[GSYM REAL_LE_LDIV_EQ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
2709   GEN_REWRITE_TAC LAND_CONV [real_div] THEN
2710   GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
2711   REWRITE_TAC[REAL_MUL_ASSOC] THEN
2712   MP_TAC(SPECL [`ISQRT n`; `n:num`] PII_CHANGE) THEN
2713   SUBGOAL_THEN `~(ISQRT n = 0)` ASSUME_TAC THENL
2714    [MP_TAC(SPEC `n:num` ISQRT_WORKS) THEN
2715     ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN SIMP_TAC[ARITH] THEN
2716     DISCH_TAC THEN UNDISCH_TAC `50 <= n` THEN ARITH_TAC;
2717     ALL_TAC] THEN
2718   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH
2719    `a * p <= ls * p ==> ls * (p - ps) <= an ==> a * p <= an + ls * ps`) THEN
2720   MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[PII_POS] THEN
2721   CONV_TAC REAL_RAT_REDUCE_CONV THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
2722   SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
2723   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `ln((&(ISQRT n) + &1) pow 2)` THEN
2724   CONJ_TAC THENL
2725    [SUBGOAL_THEN `&0 < &n /\ &n <= (&(ISQRT n) + &1) pow 2`
2726      (fun th -> MESON_TAC[th; REAL_LTE_TRANS; LN_MONO_LE]) THEN
2727     REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_POW; REAL_OF_NUM_LE;
2728                 REAL_OF_NUM_LT] THEN
2729     SIMP_TAC[ISQRT_WORKS; LT_IMP_LE] THEN
2730     UNDISCH_TAC `50 <= n` THEN ARITH_TAC;
2731     ALL_TAC] THEN
2732   SIMP_TAC[LN_POW; REAL_POS; REAL_ARITH `&0 <= x ==> &0 < x + &1`] THEN
2733   GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
2734   SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
2735   REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
2736   CONV_TAC REAL_RAT_REDUCE_CONV THEN
2737   MATCH_MP_TAC(REAL_ARITH `a - b <= b * (d - &1) ==> a <= b * d`) THEN
2738   ASM_SIMP_TAC[GSYM LN_DIV; REAL_ARITH `&0 < x ==> &0 < x + &1`;
2739                REAL_OF_NUM_LT; ARITH_RULE `0 < n <=> ~(n = 0)`] THEN
2740   REWRITE_TAC[real_div; REAL_ADD_RDISTRIB] THEN
2741   ASM_SIMP_TAC[REAL_MUL_RINV; REAL_OF_NUM_EQ; ARITH; REAL_MUL_LID] THEN
2742   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&(ISQRT n))` THEN
2743   ASM_SIMP_TAC[LN_LE; REAL_POS; REAL_LE_INV_EQ] THEN
2744   CONV_TAC REAL_RAT_REDUCE_CONV THEN
2745   REWRITE_TAC[real_div; REAL_MUL_LID] THEN REWRITE_TAC[GSYM real_div] THEN
2746   SIMP_TAC[REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
2747   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
2748   ASM_SIMP_TAC[GSYM real_div; REAL_LE_LDIV_EQ; REAL_OF_NUM_LT;
2749                ARITH_RULE `0 < n <=> ~(n = 0)`] THEN
2750   SUBGOAL_THEN `&7 <= &(ISQRT n)` MP_TAC THENL
2751    [REWRITE_TAC[REAL_OF_NUM_LE] THEN
2752     SUBGOAL_THEN `7 EXP 2 < (ISQRT n + 1) EXP 2` MP_TAC THENL
2753      [MATCH_MP_TAC LET_TRANS THEN EXISTS_TAC `n:num` THEN
2754       REWRITE_TAC[ISQRT_WORKS] THEN CONV_TAC NUM_REDUCE_CONV THEN
2755       UNDISCH_TAC `50 <= n` THEN ARITH_TAC;
2756       ALL_TAC] THEN
2757     REWRITE_TAC[num_CONV `2`; EXP_MONO_LT_SUC] THEN ARITH_TAC;
2758     ALL_TAC] THEN
2759   SPEC_TAC(`&(ISQRT n)`,`x:real`) THEN
2760   MATCH_MP_TAC OVERPOWER_LEMMA THEN
2761   W(fun (asl,w) ->
2762       let th = DIFF_CONV
2763        (lhand(rator(rand(body(rand(lhand(rand(body(rand w))))))))) in
2764       MP_TAC th) THEN
2765   GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV)
2766    [REAL_MUL_LZERO; REAL_ADD_LID; REAL_ADD_RID;
2767     REAL_MUL_RID; REAL_MUL_LID] THEN
2768   SIMP_TAC[REAL_MUL_LINV; REAL_LT_IMP_NZ] THEN
2769   W(fun (asl,w) ->
2770       let tm = mk_abs(`x:real`,rand(rator(rand(body(rand(lhand w)))))) in
2771       DISCH_TAC THEN EXISTS_TAC tm) THEN
2772   CONJ_TAC THENL
2773    [CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[real_sub] THEN
2774     CONV_TAC(ONCE_DEPTH_CONV LN_N2_CONV) THEN
2775     CONV_TAC REALCALC_REL_CONV;
2776     ALL_TAC] THEN
2777   REWRITE_TAC[] THEN CONJ_TAC THENL
2778    [GEN_TAC THEN
2779     DISCH_THEN(fun th -> FIRST_ASSUM MATCH_MP_TAC THEN MP_TAC th) THEN
2780     REAL_ARITH_TAC;
2781     ALL_TAC] THEN
2782   X_GEN_TAC `x:real` THEN REWRITE_TAC[REAL_SUB_RZERO] THEN
2783   SIMP_TAC[LN_POS; REAL_LE_ADD; REAL_POS; REAL_ARITH `&7 <= x ==> &1 <= x`]);;
2784
2785 (* ------------------------------------------------------------------------- *)
2786 (* Hence a bound by wellfounded induction.                                   *)
2787 (* ------------------------------------------------------------------------- *)
2788
2789 let PII_UBOUND_5 = prove
2790  (`!n. 3 <= n ==> pii(n) <= &5 * (&n / ln(&n))`,
2791   REWRITE_TAC[real_div; REAL_MUL_ASSOC] THEN
2792   SIMP_TAC[GSYM real_div; REAL_LE_RDIV_EQ; LN_POS_LT; REAL_OF_NUM_LT;
2793            ARITH_RULE `3 <= n ==> 1 < n`] THEN
2794   GEN_REWRITE_TAC (BINDER_CONV o RAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN
2795   MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN
2796   ASM_CASES_TAC `n < 50` THEN ASM_SIMP_TAC[PII_UBOUND_CASES_50] THEN
2797   DISCH_THEN(MP_TAC o SPEC `ISQRT n`) THEN
2798   RULE_ASSUM_TAC(REWRITE_RULE[NOT_LT]) THEN
2799   SUBGOAL_THEN `7 <= ISQRT n` ASSUME_TAC THENL
2800    [REWRITE_TAC[REAL_OF_NUM_LE] THEN
2801     SUBGOAL_THEN `7 EXP 2 < (ISQRT n + 1) EXP 2` MP_TAC THENL
2802      [MATCH_MP_TAC LET_TRANS THEN EXISTS_TAC `n:num` THEN
2803       REWRITE_TAC[ISQRT_WORKS] THEN CONV_TAC NUM_REDUCE_CONV THEN
2804       UNDISCH_TAC `50 <= n` THEN ARITH_TAC;
2805       ALL_TAC] THEN
2806     REWRITE_TAC[num_CONV `2`; EXP_MONO_LT_SUC] THEN ARITH_TAC;
2807     ALL_TAC] THEN
2808   ASM_SIMP_TAC[ARITH_RULE `7 <= n ==> 3 <= n`;
2809                ARITH_RULE `50 <= n ==> 3 <= n`] THEN
2810   ANTS_TAC THENL
2811    [SUBGOAL_THEN `(ISQRT n) EXP 2 < n EXP 2` MP_TAC THENL
2812      [MATCH_MP_TAC LET_TRANS THEN EXISTS_TAC `n:num` THEN
2813       REWRITE_TAC[ISQRT_WORKS] THEN REWRITE_TAC[EXP_2] THEN
2814       MATCH_MP_TAC(ARITH_RULE `1 * n < m ==> n < m`) THEN
2815       REWRITE_TAC[LT_MULT_RCANCEL] THEN
2816       UNDISCH_TAC `50 <= n` THEN ARITH_TAC;
2817       ALL_TAC] THEN
2818     REWRITE_TAC[num_CONV `2`; EXP_MONO_LT_SUC];
2819     ALL_TAC] THEN
2820   DISCH_TAC THEN
2821   FIRST_ASSUM(MP_TAC o MATCH_MP PII_ISQRT_INDUCT) THEN
2822   MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
2823   MATCH_MP_TAC REAL_LE_TRANS THEN
2824   EXISTS_TAC `&9 / &4 * (&3 / &2 * &n + &5 * &(ISQRT n))` THEN
2825   CONJ_TAC THENL
2826    [MATCH_MP_TAC REAL_LE_LMUL THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
2827     ASM_REWRITE_TAC[REAL_LE_LADD];
2828     ALL_TAC] THEN
2829   MATCH_MP_TAC(REAL_ARITH
2830    `i * (a * c) <= n * (d - a * b) ==> a * (b * n + c * i) <= d * n`) THEN
2831   CONV_TAC REAL_RAT_REDUCE_CONV THEN
2832   SIMP_TAC[GSYM REAL_LE_LDIV_EQ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
2833   REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
2834   CONV_TAC REAL_RAT_REDUCE_CONV THEN
2835   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&(ISQRT n) * &7` THEN
2836   CONJ_TAC THENL
2837    [MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN
2838     CONV_TAC REAL_RAT_REDUCE_CONV;
2839     ALL_TAC] THEN
2840   REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_LE] THEN
2841   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `ISQRT n * ISQRT n` THEN CONJ_TAC THENL
2842    [ASM_REWRITE_TAC[LE_MULT_LCANCEL];
2843     REWRITE_TAC[GSYM EXP_2; ISQRT_WORKS]]);;