Theory PrimeNumberTheorem

Up to index of Isabelle/HOL/HOL-Complex/NumberTheory

theory PrimeNumberTheorem = Error:

(*  Title:      PrimeNumberTheorem.thy
    Author:     Jeremy Avigad
*)

header {* The prime number theorem *}

theory PrimeNumberTheorem = Error:;

lemma PNT1_aux1: "0 < C ==> 0 <= D ==> 
  EX C0. ALL eps. 0 < eps --> eps < 1 --> 
    (ALL K. exp (C0 / eps) < K --> 
      2 < K & D < ln K & C / (ln K - D) < eps)";
proof;
  assume a: "0 < C" and b: "0 <= D";
  let ?C0 = "3 * max (max C D) (ln 2)"
  show "ALL eps. 0 < eps --> eps < 1 --> 
    (ALL K. exp (?C0 / eps) < K --> 
      2 < K & D < ln K & C / (ln K - D) < eps)";
  proof (clarify);
    fix eps::"real";
    fix K::"real";
    assume "0 < eps" and "eps < 1"; 
    assume "exp (?C0 / eps) < K";
    show "2 < K & D < ln K & C / (ln K - D) < eps";
      apply (rule conjI); 
      apply (rule order_le_less_trans);
      prefer 2;
      apply (rule prems);
      apply (subgoal_tac "2 = exp (ln 2)");
      apply (erule ssubst);
      apply (subst exp_le_cancel_iff);
      apply (subst pos_le_divide_eq);
      apply (rule prems);
      apply (rule order_trans);
      apply (subgoal_tac "ln 2 * eps <= ln 2 * 1");
      apply assumption;
      apply (rule mult_left_mono);
      apply (rule order_less_imp_le);
      apply (rule prems);
      apply force;
      apply (subst mult_commute);
      apply (rule mult_mono);
      apply simp;
      apply (rule le_maxI2);
      apply force;
      apply simp;
      apply (rule order_trans);
      prefer 2;
      apply (rule le_maxI2);
      apply auto;
      apply (rule order_le_less_trans);
      prefer 2;
      apply (subgoal_tac "ln (exp (?C0 / eps)) < ln K");
      apply assumption;
      apply (subst ln_less_cancel_iff);
      apply force;
      apply (rule order_less_trans);
      prefer 2;
      apply (rule prems);
      apply force;
      apply (rule prems);
      apply simp;
      apply (rule order_trans);
      apply (subgoal_tac "D <= 3 * D");
      apply assumption;
      apply simp;
      apply (rule prems)+;
      apply (subst pos_le_divide_eq);
      apply (rule prems);
      apply simp;
      apply (rule order_trans);
      apply (subgoal_tac "D * eps <= D * 1");
      apply assumption;
      apply (rule mult_left_mono);
      apply (rule order_less_imp_le);
      apply (rule prems);
      apply (rule prems);
      apply simp;
      apply (rule order_trans);
      apply (rule le_maxI2);
      apply (rule le_maxI1);
      apply (subst pos_divide_less_eq);
      apply simp;
      apply (rule order_le_less_trans);
      prefer 2;
      apply (subgoal_tac "ln (exp (?C0 / eps)) < ln K");
      apply assumption;
      apply (subst ln_less_cancel_iff);
      apply force;
      apply (rule order_less_trans);
      prefer 2;
      apply (rule prems);
      apply force;
      apply (rule prems);
      apply simp;
      apply (rule order_trans);
      apply (subgoal_tac "D <= 3 * D");
      apply assumption;
      apply simp;
      apply (rule prems)+;
      apply (subst pos_le_divide_eq);
      apply (rule prems);
      apply simp;
      apply (rule order_trans);
      apply (subgoal_tac "D * eps <= D * 1");
      apply assumption;
      apply (rule mult_left_mono);
      apply (rule order_less_imp_le);
      apply (rule prems);
      apply (rule prems);
      apply simp;
      apply (rule order_trans);
      apply (rule le_maxI2);
      apply (rule le_maxI1);
      apply (subgoal_tac "C = eps * (C / eps)");
      apply (erule ssubst);
      apply (rule mult_strict_left_mono);
      apply (simp add: compare_rls);
      apply (rule order_less_le_trans);
      prefer 2;
      apply (subst ln_le_cancel_iff);
      prefer 3;
      apply (rule order_less_imp_le);
      apply (rule prems);
      apply force;
      apply (rule order_less_trans);
      prefer 2;
      apply (rule prems);
      apply force;
      apply simp;
      apply (subgoal_tac "C / eps <= max (max C D) (ln 2) / eps");
      apply (subgoal_tac "D <= max (max C D) (ln 2) / eps");
      apply (subgoal_tac "0 < max (max C D) (ln 2) / eps");
      apply (subgoal_tac "3 * max (max C D) (ln 2) / eps = 
        2 * (max (max C D) (ln 2) / eps) + max (max C D) (ln 2) / eps");
      apply (erule ssubst);
      apply arith;
      apply (subgoal_tac "3 = 2 + 1");
      apply (erule ssubst);
      apply (simp only: ring_eq_simps add_divide_distrib);
      apply simp+;
      apply (subst pos_less_divide_eq);
      apply (rule prems);
      apply simp;
      apply (rule order_less_le_trans);
      apply (rule a);
      apply (rule order_trans);
      apply (rule le_maxI1);
      apply (rule le_maxI1);
      apply (subst pos_le_divide_eq);
      apply (rule prems);
      apply (rule order_trans);
      apply (subgoal_tac "D * eps <= D * 1");
      apply assumption;
      apply (rule mult_left_mono);
      apply (rule order_less_imp_le);
      apply (rule prems)+;
      apply simp;
      apply (rule order_trans);
      apply (rule le_maxI2);
      apply (rule le_maxI1);
      apply (rule divide_right_mono);
      apply (rule order_trans);
      apply (rule le_maxI1);
      apply (rule le_maxI1);
      apply (rule order_less_imp_le);
      apply (rule prems)+;
      apply (subgoal_tac "eps ~= 0");
      apply simp;
      apply (rule less_imp_neq [THEN not_sym]);
      apply (rule prems);
      done;
  qed;
qed;

lemma PNT1_aux2: "EX C. ALL x. abs(ln (abs x + 1) - 
    (∑ i = 1..natfloor (abs x) + 1. 1 / real i)) < C";
  apply (insert ln_sum_real2);
  apply (drule set_plus_imp_minus);
  apply (simp only: func_diff);
  apply (simp only: bigo_alt_def);
  apply clarsimp;
  apply (rule_tac x = "c + c" in exI);
  apply (rule allI);
  apply (drule_tac x = x in spec);
  apply (erule order_le_less_trans);
  apply arith;
done;

lemma PNT1_aux3: "EX C. ALL x. (1 <= x --> abs(ln x - 
    (∑ i = 1..natfloor x. 1 / real i)) < C)";
  apply (insert PNT1_aux2);
  apply clarsimp;
  apply (rule_tac x = C in exI);
  apply (rule allI);
  apply (rule impI);
  apply (subgoal_tac "ln x = ln((x - 1) + 1)");
  apply (erule ssubst);
  apply (subgoal_tac "natfloor x = natfloor (x - 1) + 1");
  apply (erule ssubst);
  apply (subgoal_tac "x - 1 = abs(x - 1)");
  apply (erule ssubst);
  apply (erule spec);
  apply (subst abs_nonneg);
  apply auto;
  apply (subst natfloor_add [THEN sym]);
  apply auto;
done;

lemma PNT1_aux4: "EX C. ALL x. (1 <= x --> abs(ln x - 
    (∑ i = 1..natfloor x. 1 / real (i + 1))) < C)";
  apply (insert PNT1_aux3);
  apply clarify;
  apply (rule_tac x = "C + 1" in exI);
  apply clarify;
  apply (drule_tac x = x in spec);
  apply (subgoal_tac 
    "(∑ i = 2..natfloor x + 1. 1 / real i) = 
    (∑ i = 1..natfloor x. 1 / real (i + 1))");
  prefer 2;
  apply (rule setsum_reindex_cong');
  apply force;
  apply (subgoal_tac "inj_on (%x. x + 1) ?t");
  apply assumption;
  apply (simp add: inj_on_def);
  apply (clarsimp simp add: image_def);
  apply (rule equalityI);
  apply clarify;
  apply (rule_tac x = "xa - 1" in bexI);
  apply force;
  apply clarsimp;
  apply (rule conjI);
  apply arith;
  apply arith;
  apply clarsimp;
  apply (rule refl);
  apply (erule subst);
  apply (subgoal_tac "ln x - (∑ i = 2..natfloor x + 1. 1 / real i) =
    (ln x - (∑ i = 1..natfloor x. 1 / real i)) +
    (1 - 1 / real (natfloor x + 1))");
  apply (erule ssubst);
  apply (rule order_le_less_trans);
  apply (rule abs_triangle_ineq);
  apply (rule real_add_less_le_mono);
  apply (erule mp);
  apply assumption;
  apply (subst abs_nonneg);
  apply simp;
  apply (subst pos_divide_le_eq);
  apply force;
  apply force;
  apply simp;
  apply (simp add: compare_rls);
  apply (subgoal_tac "(∑ i = 2..natfloor x + 1. 1 / real i) = 
    (∑ i = 1..natfloor x. 1 / real i) - 
    (∑ i : {1::nat}. 1 / real i) + 
    (∑ i : {natfloor x + 1}. 1 / real i)");
  apply (erule ssubst);
  apply simp;
  apply (simp only: compare_rls);
  apply (subst setsum_Un_disjoint [THEN sym]);
  apply force;
  apply force;
  apply force;
  apply (subst setsum_Un_disjoint [THEN sym]);
  apply force;
  apply force;
  apply force;
  apply (rule setsum_cong);
  apply force;
  apply (rule refl);
done;

lemma PNT1_aux5: "EX D. ALL x. ALL K. 1 <= x --> 1 <= K --> 
  abs (ln K -
    (∑ n | natfloor x < n & n <= natfloor (K * x). 1 / real (n + 1)))
      <= D";
proof -;
  obtain C where "ALL x. (1 <= x --> abs(ln x - 
    (∑ i = 1..natfloor x. 1 / real (i + 1))) < C)";
    by (insert PNT1_aux4, auto);
  show ?thesis;
  proof;
  show "ALL x. ALL K. 1 <= x --> 1 <= K --> 
      abs (ln K -
        (∑ n | natfloor x < n & n <= natfloor (K * x). 1 / real (n + 1)))
          <= C + C";
    proof (clarify);
      fix x::"real"; fix K::"real";
      assume "1 <= x" and "1 <= K";
    have a: "(∑ n | natfloor x < n & n <= natfloor (K * x). 
      1 / real (n + 1)) = 
      (∑n=1..natfloor (K * x). 1 / real (n + 1)) - 
      (∑n=1..natfloor x. 1 / real (n + 1))"
        (is "?LHS1 = ?RHS1a - ?RHS1b");
      apply (simp add: compare_rls);
      apply (subst setsum_Un_disjoint [THEN sym]);
      apply (rule bounded_nat_set_is_finite);
      apply clarsimp;
      apply (subgoal_tac "i < natfloor (K * x) + 1");
      apply assumption;
      apply arith;
      apply force;
      apply force;
      apply (rule setsum_cong);
      apply auto;
      apply (rule order_trans);
      prefer 2;
      apply (subgoal_tac "natfloor (1 * ?x) <= natfloor (K * ?x)");
      apply assumption;
      apply (rule natfloor_mono);
      apply (rule mult_right_mono);
      apply (rule prems);
      apply (insert prems, arith);
      apply simp;
      done;
    have b: "ln K = ln (K * x) - ln x"
      apply (subst ln_mult);
      apply (insert prems);
      apply auto;
      done;
    have "ln K - ?LHS1 = (ln (K * x) - ?RHS1a) + (?RHS1b - ln x)"
      by (simp only: a b compare_rls);
    then have "abs(ln K - ?LHS1) = abs(...)";
      by simp;
    also have "... <= abs(ln (K * x) - ?RHS1a) + abs(?RHS1b - ln x)";
      by (rule abs_triangle_ineq);
    also have "... <= C + C";
      apply (rule add_mono);
      apply (insert prems);
      apply (drule_tac x = "K * x" in spec);
      apply (subgoal_tac "1 <= K * x");
      apply force;
      apply (subgoal_tac "1 * 1 <= K * x");
      apply simp;
      apply (rule mult_mono);
      apply assumption+;
      apply arith;
      apply force;
      apply (subst abs_diff);
      apply (drule_tac x = x in spec);
      apply force;
      done;
    finally; show "abs (ln K -
      (∑ n | natfloor x < n & n <= natfloor (K * x). 1 / real (n + 1)))
      <= C + C";.;
    qed;
  qed;
qed;

lemma PNT1_aux6: "EX D. ALL x. ALL K. 1 <= x --> 1 <= K --> ln K - D <= 
    (∑ n | natfloor x < n & n <= natfloor (K * x). 1 / real (n + 1))";
  apply (insert PNT1_aux5);
  apply (erule exE);
  apply (rule_tac x = D in exI);
  apply (clarsimp);
  apply (drule_tac x = x in spec);
  apply clarsimp;
  apply (drule_tac x = K in spec);
  apply clarsimp;
  apply (frule abs_le_D1);
  apply auto;
done;

lemma PNT1_aux7: "0 < C ==> EX C0. ALL eps. 0 < eps --> eps < 1 -->
    (ALL K. ALL x. 1 <= x --> exp (C0 / eps) < K --> 
      2 < K &
      C / (∑ n | natfloor x < n & n <= natfloor (K * x). 
        1 / real (n + 1)) < eps)";
proof -;
  assume a: "0 < C";
  obtain D where d: "ALL x. ALL K. 1 <= K --> 1 <= x --> ln K - D <= 
    (∑ n | natfloor x < n & n <= natfloor (K * x). 1 / real (n + 1))";
    by (insert PNT1_aux6, auto);
  let ?D = "max D 0";
  have "EX C0. ALL eps. 0 < eps --> eps < 1 -->
      (ALL K. exp (C0 / eps) < K -->
        2 < K & ?D < ln K & C / (ln K - ?D) < eps)";
    apply (rule PNT1_aux1);
    apply (rule a);
    apply (rule le_maxI2);
    done;
  then obtain C0 where C0: "ALL eps. 0 < eps --> eps < 1 -->
      (ALL K. exp (C0 / eps) < K -->
        2 < K & ?D < ln K & C / (ln K - ?D) < eps)";..;
  show ?thesis;
  proof; 
  show "ALL eps. 0 < eps --> eps < 1 -->
    (ALL K. ALL x. 1 <= x --> exp (C0 / eps) < K --> 2 < K &
      C / (∑ n | natfloor x < n & n <= natfloor (K * x). 
        1 / real (n + 1)) < eps)";
  proof (clarify);
    fix eps::"real"
    fix K::"real";
    fix x::"real";
    assume "0 < eps";
    assume "eps < 1";
    assume "1 <= x";
    assume "exp (C0 / eps) < K";
    have c0: "ALL K. exp (C0 / eps) < K --> 2 < K & ?D < ln K & 
      C / (ln K - ?D) < eps";
      by (insert C0 prems, blast);
    show "2 < K & 
        C / (∑ n | natfloor x < n & n <= natfloor (K * x). 
          1 / real (n + 1)) < eps";
      apply (rule conjI);
      apply (insert c0);
      apply (drule_tac x = K in spec);
      apply (force simp add: prems);
      apply (case_tac 
        "(∑ n | natfloor x < n & n <= natfloor (K * x). 
           1 / real (n + 1)) = 0");
      apply (simp add: prems);
      apply (subst pos_divide_less_eq);
      apply (subgoal_tac "0 <= 
        (∑ n | natfloor x < n & n <= natfloor (K * x). 
          1 / real (n + 1))");
      apply arith;
      apply (rule setsum_nonneg');
      apply force;
      apply (rule order_less_le_trans);
      apply (subgoal_tac "C < eps * (ln K - max D 0)");
      apply assumption;
      apply (subst pos_divide_less_eq [THEN sym]);
      apply (simp add: compare_rls);
      apply (insert d);
      apply (drule_tac x = x in spec);
      apply (drule_tac x = K in spec);
      apply (clarsimp simp add: prems);
      apply (insert c0);
      apply (drule_tac x = K in spec);
      apply (clarsimp simp add: prems);
      apply (drule_tac x = K in spec);
      apply (clarsimp simp add: prems);
      apply (rule mult_left_mono);
      apply (rule order_trans);
      apply (subgoal_tac "ln K - max D 0 <= ln K - D");
      apply assumption;
      apply simp;
      apply (rule le_maxI1);
      apply (drule_tac x = x in spec);
      apply (drule_tac x = K in spec);back;
      apply (subgoal_tac "1 <= K");
      apply (clarsimp simp add: prems);
      apply (subgoal_tac "2 < K");
      apply simp;
      apply (force simp add: prems);
      apply (rule order_less_imp_le);
      apply (rule prems);
      done;
  qed;
  qed;
qed;

lemma PNT1_aux8: "~((0 <= (x::real)) = (0 <= y)) ==> abs x <= abs (y - x)";
  by auto;

lemma PNT1_aux9:
  "(ALL k < (j::nat). ((0 <= (f(i + k)::real)) = (0 <= f(i + (k + 1))))) ==> 
    (ALL k <= j. (0 <= f(i + k))) | (ALL k <= j. (f(i + k) < 0))";
  apply (case_tac "0 <= f i");
  apply (rule disjI1);
  apply (rule allI);
  apply (induct_tac k);
  apply force;
  apply clarify;
  apply (subgoal_tac "n <= j");
  apply clarify;
  apply (subgoal_tac "n < j");
  apply (drule_tac x = n in spec);
  apply (frule mp);
  apply assumption;
  apply (subgoal_tac "i + Suc n = i + (n + 1)");
  apply (erule ssubst);back;
  apply force;
  apply simp;
  apply arith;
  apply arith;
  apply (rule disjI2);
  apply (rule allI);
  apply (induct_tac k);
  apply force;
  apply clarify;
  apply (subgoal_tac "n <= j");
  apply clarify;
  apply (subgoal_tac "n < j");
  apply (drule_tac x = n in spec);
  apply (frule mp);
  apply assumption;
  apply (subgoal_tac "i + Suc n = i + (n + 1)");
  apply (erule ssubst);back;
  apply force;
  apply simp;
  apply arith;
  apply arith;
done;

lemma PNT1_aux10: "(i::nat) <= j ==> (ALL n. i < n & n <= j --> 
    (((0::real) <= f(n)) = (0 <= f(n+1)))) ==> 
      (ALL n. i < n & n <= j --> 0 <= f n) |
      (ALL n. i < n & n <= j --> f n < 0)";
  apply (subgoal_tac "
    (ALL k <= j - i. (0 <= f((i + 1) + k))) | 
    (ALL k <= j - i. (f((i + 1) + k) < 0))");
  apply (erule disjE);
  apply (rule disjI1);
  apply clarify;
  apply (drule_tac x = "n - (i + 1)" in spec);back;
  apply (subgoal_tac "n - (i + 1) <= j - i");
  apply clarify;
  apply (subgoal_tac "(i + 1) + (n - (i + 1)) = n");
  apply simp;
  apply arith+;
  apply (rule disjI2);
  apply clarify;
  apply (drule_tac x = "n - (i + 1)" in spec);back;
  apply (subgoal_tac "n - (i + 1) <= j - i");
  apply clarify;
  apply (subgoal_tac "(i + 1) + (n - (i + 1)) = n");
  apply simp;
  apply arith+;
  apply (rule PNT1_aux9);
  apply clarify;
  apply (drule_tac x = "i + 1 + k" in spec);
  apply (drule mp);
  apply arith;
  apply (simp add: add_ac);
done;

lemma PNT1_aux11: "EX C. ALL i. (1::nat) <= i -->
    abs(∑n=1..i. R(real n) / ((real n) * (real (n + 1)))) <= C";
proof -;
  have "EX C. ALL x. abs(∑ n=1..natfloor (abs x).
      R(real n) / ((real n) * (real (n + 1)))) <= C";
    apply (insert error1);
    apply (unfold bigo_def);
    apply clarsimp;
    done;
  thus ?thesis;
    apply clarsimp;
    apply (rule_tac x = C in exI);
    apply (rule allI);
    apply (rule impI);
    apply (drule_tac x = "real i" in spec);
    apply (subgoal_tac "abs(real i) = real i");
    apply simp_all;
    done;
qed;

lemma PNT1_aux12: "EX C. ALL (i::nat). ALL j. 1 <= i --> i <= j --> 
    abs (∑ n | i < n & n <= j. R(real n) / ((real n) * (real (n +
      1)))) < C";
  apply (insert PNT1_aux11);
  apply (erule exE);
  apply (rule_tac x = "C + C + 1" in exI);
  apply clarify;
  apply (rule order_le_less_trans);
  prefer 2;
  apply (subgoal_tac "C + C < C + C + 1");
  apply assumption;
  apply arith;
  apply (subgoal_tac "(∑ n | i < n & n <= j. 
       R (real n) / (real n * real (n + 1))) = 
    (∑n=1..j. R(real n) / ((real n) * (real (n + 1)))) - 
    (∑n=1..i. R(real n) / ((real n) * (real (n + 1))))");
  apply (erule ssubst);
  apply (rule order_trans);
  apply (rule abs_triangle_ineq4);
  apply (rule add_mono);
  apply force;
  apply force;
  apply (simp add: compare_rls);
  apply (subst setsum_Un_disjoint [THEN sym]);
  apply (rule bounded_nat_set_is_finite);
  apply clarify;
  apply (subgoal_tac "ia < j + 1");
  apply assumption;
  apply arith;
  apply simp;
  apply force;
  apply (rule setsum_cong);
  apply (auto simp only: atLeastAtMost_iff);
done;
 
lemma PNT1: "EX C0. ALL eps. 0 < eps --> eps < 1 --> (EX x0. ALL K x.
    exp (C0 / eps) < K --> x0 < x --> (EX n. 
      natfloor x < n & n <= natfloor (K * x) &
        abs(R(real n) / (real n)) < eps))";
proof -;
  from PNT1_aux12 obtain C where C: "ALL (i::nat). ALL j. 
    1 <= i --> i <= j --> 
      abs (∑ n | i < n & n <= j. R(real n) / ((real n) * (real (n +
        1)))) < C";..;
  have "EX C0. ALL eps. 0 < eps --> eps < 1 -->
    (ALL K. ALL x. 1 <= x --> exp (C0 / eps) < K --> 
      2 < K & C / (∑ n | natfloor x < n & n <= natfloor (K * x). 
        1 / real (n + 1)) < eps)";
    apply (rule PNT1_aux7);
    apply (insert prems);
    apply (drule_tac x = 1 in spec)+;
    apply (drule mp, simp)+;
    apply arith;
    done; 
  then obtain C0 where C0temp: "ALL eps. 0 < eps --> eps < 1 -->
    (ALL K. ALL x. 1 <= x --> exp (C0 / eps) < K --> 
      2 < K & C / (∑ n | natfloor x < n & n <= natfloor (K * x). 
        1 / real (n + 1)) < eps)";..;
  show ?thesis; 
  proof ((rule exI)+, clarify);
    fix eps::"real";
    assume "0 < eps";
    assume "eps < 1";assume "eps < 1";
    show "EX x0. ALL K x. exp (C0 / eps) < K --> x0 < x -->
      (EX n. natfloor x < n & n <= natfloor (K * x) & 
        abs (R (real n) / real n) < eps)";
  proof;
    let ?x0 = "max (exp 2 + 1) (exp (4 / eps) + 1)";
    show "ALL K x. exp (C0 / eps) < K --> ?x0 < x -->
      (EX n. natfloor x < n & n <= natfloor (K * x) & 
        abs (R (real n) / real n) < eps)";
  proof (clarify);
    fix K::"real"; fix x::"real"; 
    assume "exp (C0 / eps) < K"; 
    assume "?x0 < x";
    have C0: "ALL K. ALL x. 1 <= x --> exp (C0 / eps) < K --> 
      2 < K & 
      C / (∑ n | natfloor x < n & n <= natfloor (K * x). 
        1 / real (n + 1)) < eps";
      by (insert C0temp prems, blast);
    have a: "exp 2 + 1 <= x"; 
      apply (intro order_less_imp_le);
      apply (rule order_le_less_trans);
      prefer 2;
      apply assumption;
      apply (rule le_maxI1);
      done;
    have b: "exp (4 / eps) + 1 <= x";
      apply (intro order_less_imp_le);
      apply (rule order_le_less_trans);
      prefer 2;
      apply (rule prems);
      apply (rule le_maxI2);
      done;
    have d: "exp (4 / eps) <= real(natfloor x)";
      apply (rule order_less_imp_le);
      apply (rule ge_natfloor_plus_one_imp_gt);
      apply (subst natfloor_add [THEN sym]);
      apply (subgoal_tac "0 < exp (4 / eps)");
      apply arith;
      apply force;
      apply simp;
      apply (rule natfloor_mono);
      apply (rule b);
      done;
    show "EX n. natfloor x < n &
      n <= natfloor (K * x) & abs (R (real n) / real n) < eps";
    proof (cases);
      assume "EX n. natfloor x < n & n <= natfloor (K * x) &
        ~((0 <= R(real n)) = (0 <= R(real (n + 1))))";
      then obtain n where c: "natfloor x < n & n <= natfloor (K * x) &
        ~((0 <= R(real n)) = (0 <= R(real (n + 1))))";..;
      have c: "exp 2 < real n";
        apply (rule ge_natfloor_plus_one_imp_gt);
        apply (subgoal_tac "natfloor x < n");
        apply (subgoal_tac "natfloor (exp 2) + 1 <= natfloor x");
        apply arith;
        apply (subst natfloor_add [THEN sym]);
        apply force;
        apply (rule natfloor_mono);
        apply simp;
        apply (rule a);
        apply (insert prems, auto);
        done;
      have "abs (R(real n)) <= abs(R(real (n + 1)) - R(real n))"; 
        by (insert prems, intro PNT1_aux8, simp);
      also have "R(real(n + 1)) - R(real n) = psi(n + 1) - psi(n) - 1";
        apply (unfold R_def);
        apply simp;
        apply (subgoal_tac "real n + 1 = real(n + 1)");
        apply (erule ssubst);
        apply (subst natfloor_real_id); 
        apply simp_all;
        done;
      also have "abs(...) < ln (real n)";
        apply (subst psi_plus_one);
        apply simp;
        apply (case_tac "EX p a. p : prime & p ^ a = (n + 1) & 0 < a");
        apply (clarsimp);
        apply (subgoal_tac "n + 1 = p ^ a");
        apply (erule ssubst);back;
        apply (subst Lambda_eq);
        apply assumption+;
        apply (case_tac "real p < exp 1");
        apply (rule order_le_less_trans);
        apply (rule abs_triangle_ineq4);
        apply simp;
        apply (subst abs_nonneg);
        apply (rule ln_ge_zero);
        apply (subgoal_tac "real (1::nat) <= real p");
        apply simp;
        apply (rule le_imp_real_of_nat_le);
        apply (erule primes_always_ge_1);  
        apply (rule order_less_le_trans);
        apply (subgoal_tac "ln(real p) + 1 < ln (exp 1) + 1");
        apply assumption;
        apply (rule add_strict_right_mono);
        apply (subst ln_less_cancel_iff);
        apply (subgoal_tac "1 <= p");
        apply arith;
        apply (erule primes_always_ge_1);
        apply force;
        apply assumption;
        apply simp;
        apply (subgoal_tac "ln (exp 2) <= ln (real n)");
        apply simp;
        apply (subst ln_le_cancel_iff);
        apply force;
        apply (rule order_le_less_trans);
        prefer 2;
        apply (rule c);
        apply force;
        apply (rule order_less_imp_le);
        apply (rule c);
        apply (subst abs_nonneg);
        apply simp;
        apply (subgoal_tac "ln (exp 1) <= ln (real p)");
        apply simp;
        apply (subst ln_le_cancel_iff);
        apply force;
        apply (frule primes_always_ge_1);
        apply arith;
        apply arith;
        apply (simp add: compare_rls);
        apply (rule order_le_less_trans);
        apply (subgoal_tac "ln (real p) <= ln(real (n + 1))");
        apply assumption;
        apply (subst ln_le_cancel_iff);
        apply (frule primes_always_ge_1);
        apply arith;
        apply arith;
        apply (rule le_imp_real_of_nat_le);
        apply (erule subst);
        apply (subgoal_tac "p^1 <= p^a");
        apply simp;
        apply (rule power_increasing);
        apply arith;
        apply (erule primes_always_ge_1);
        apply simp;
        apply (subgoal_tac "ln (real n + 1) - ln (real n) < 1");
        apply simp;
        apply (subst ln_div [THEN sym]);
        apply force;
        apply (rule order_le_less_trans);
        prefer 2;
        apply (rule c);
        apply force;
        apply (subgoal_tac "(real n + 1) / real n = 1 + 1 / real n");
        apply (erule ssubst);back;
        apply (rule order_le_less_trans);
        apply (rule ln_add_one_self_le_self);
        apply force;
        apply (subst pos_divide_less_eq);
        apply (rule order_le_less_trans);
        prefer 2;
        apply (rule c, force);
        apply simp;
        apply (rule order_le_less_trans);
        prefer 2;
        apply (rule c); 
        apply (subgoal_tac "exp 0 <= exp 2");
        apply simp;
        apply (subst exp_le_cancel_iff);
        apply force;
        apply (simp add: add_divide_distrib);
        apply (subgoal_tac "0 < real n");
        apply arith;
        apply (rule order_le_less_trans);
        prefer 2;
        apply (rule c);
        apply force;
        apply simp;
        apply (subst Lambda_eq2);
        apply assumption;
        apply simp;
        apply (subgoal_tac "ln(exp 1) < ln(real n)");
        apply simp;
        apply (subst ln_less_cancel_iff);
        apply force;
        apply (rule order_le_less_trans);
        prefer 2;
        apply (rule c);
        apply force;
        apply (rule order_le_less_trans);
        prefer 2;
        apply (rule c);
        apply simp;
        done;
      finally have "abs (R(real n)) < ln (real n)";.;
      then have "abs (R(real n)) / (real n) < ln (real n) / (real n)";
        apply (rule real_div_pos_less_mono);
        apply (rule order_le_less_trans);
        prefer 2;
        apply (rule c);
        apply force;
        done;
      also have "... <= ln (real (natfloor x)) / (real (natfloor x))";
        apply (rule ln_x_over_x_mono);
        apply (rule order_less_imp_le);
        apply (rule ge_natfloor_plus_one_imp_gt);
        apply (subst natfloor_add [THEN sym]);
        apply force;
        apply simp;
        apply (rule natfloor_mono);
        apply (rule order_trans);
        prefer 2;
        apply (rule a);
        apply simp;
        apply simp;
        apply (rule order_less_imp_le);
        apply (simp add: prems);
        done;
      also have "... <= ((real (natfloor x) powr (1 / 2)) / (1 / 2)) / 
        (real (natfloor x))";
        apply (rule divide_right_mono);
        apply (rule ln_powr_bound);
        apply (rule order_less_imp_le);
        apply (rule ge_natfloor_plus_one_imp_gt);
        apply (subst natfloor_add [THEN sym]);
        apply force;
        apply simp;
        apply (rule natfloor_mono);
        apply (rule order_trans);
        prefer 2;
        apply (rule a);
        apply simp;
        apply (subgoal_tac "exp 0 <= exp 2");
        apply simp;
        apply force;
        apply force;
        apply simp;
        done;
      also have "... = 2 * ((real (natfloor x) powr (1 / 2)) / 
        real (natfloor x) powr 1)"; 
        apply (simp add: mult_ac);
        apply (rule sym);
        apply (subst powr_one_gt_zero_iff);
        apply simp;
        apply (rule order_less_le_trans);
        prefer 2;
        apply (rule real_le_natfloor);
        apply (subgoal_tac "real 1 <= x");
        apply assumption;
        apply simp;
        apply (rule order_trans);
        prefer 2;
        apply (rule a);
        apply simp;
        apply simp;
        done;
      also have "... = 2 * (real (natfloor x) powr (1 / 2 - 1))";
        apply (rule arg_cong);back;
        apply (rule powr_divide2);
        done;
      also have "(1 / 2 - (1::real)) = - (1 / 2)";
        by simp;
      also have "2 * (real (natfloor x) powr - (1 / 2)) = 
        2 / (real (natfloor x) powr (1 / 2))";
        apply (subst powr_minus_divide);
        apply simp;
        done;
      also have "... <= 2 / (exp (4 / eps) powr (1 / 2))";
        apply (rule divide_left_mono);
        apply (rule power_mono2);
        apply force;
        apply force;
        apply (rule d);
        apply force;
        apply (rule mult_pos);
        apply force;
        apply force;
        done;
      also have "... = 2 / (exp (2 / eps))";
        by (simp add: powr_def);
      also have "... < 2 / (2 / eps)";
        apply (rule divide_strict_left_mono);
        apply (rule order_less_le_trans);
        prefer 2;
        apply (rule exp_ge_add_one_self);
        apply (rule real_ge_zero_div_gt_zero);
        apply force;
        apply (rule prems);
        apply arith;
        apply auto; 
        apply (rule pos_div_pos);
        apply (rule mult_pos);
        apply auto;
        apply (rule prems);
        done;
      also have "... = eps";
        by simp;
      finally; show ?thesis;
        apply (rule_tac x = n in exI);
        apply (auto simp add: prems);
        apply (subst abs_div [THEN sym]);
        apply (subgoal_tac "0 < real n");
        apply arith;
        apply (rule order_le_less_trans);
        prefer 2;
        apply (rule c);
        apply force;
        apply simp;
        done;
    next assume no_sign_change:"~ (EX n. natfloor x < n & 
        n <= natfloor (K * x) &
          ~((0 <= R(real n)) = (0 <= R(real (n + 1)))))";
      then have "
        (ALL n. natfloor x < n & n <= natfloor (K * x) --> 0 <= R(real n)) |
        (ALL n. natfloor x < n & n <= natfloor (K * x) --> R(real n) < 0)";
        apply (intro PNT1_aux10);
        apply (rule natfloor_mono);
        apply (subgoal_tac "1 * x <= K * x");
        apply simp;
        apply (rule mult_right_mono);
        apply (rule order_less_imp_le);
        apply (insert C0);
        apply (drule_tac x = K in spec);
        apply (drule_tac x = 1 in spec);
        apply (force simp add: prems);
        apply (rule order_trans);
        prefer 2;
        apply (rule a);
        apply (rule nonneg_plus_nonneg);
        apply force;
        apply force;
        apply force;
        done;
      then have "(∑ n | natfloor x < n & n <= natfloor (K * x).
         abs (R(real n)) / ((real n) * (real (n + 1)))) = 
       abs(∑ n | natfloor x < n & n <= natfloor (K * x).
         R(real n) / ((real n) * (real (n + 1))))";
        apply (elim disjE);
        apply (subst abs_nonneg);
        apply (rule setsum_nonneg');
        apply clarify;
        apply (rule real_ge_zero_div_gt_zero);
        apply force;
        apply (rule mult_pos);
        apply (insert a);
        apply (subgoal_tac "1 < exp 2 + 1");
        apply arith;
        apply force;
        apply (insert a);
        apply (subgoal_tac "1 < exp 2 + 1");
        apply arith;
        apply force;
        apply (rule setsum_cong2);
        apply (subst abs_nonneg);
        apply force;
        apply (rule refl);
        apply (subst abs_nonpos);
        apply (rule setsum_nonpos');
        apply clarify;
        apply (rule order_less_imp_le);
        apply (subst pos_divide_less_eq);
        apply (rule mult_pos);
        apply (insert a);
        apply (subgoal_tac "1 < exp 2 + 1");
        apply arith;
        apply force;
        apply (insert a);
        apply (subgoal_tac "1 < exp 2 + 1");
        apply arith;
        apply force;
        apply force;
        apply (subst setsum_negf' [THEN sym]);
        apply (rule setsum_cong2);
        apply (subst abs_nonpos);
        apply force;
        apply simp;
        done;
      also have "... < C";
        apply (insert C);
        apply (drule spec)+;
        apply (drule mp);
        prefer 2;
        apply (drule mp);
        prefer 2;
        apply assumption;
        apply (rule natfloor_mono);
        apply (subgoal_tac "1 * x < K * x");
        apply force;
        apply (rule mult_strict_right_mono);
        apply (insert C0);
        apply (drule_tac x = K in spec);
        apply (drule_tac x = 1 in spec);
        apply (force simp add: prems);
        apply (insert a);
        apply (subgoal_tac "0 < exp 2");
        apply arith;
        apply force;
        apply (rule real_le_natfloor);
        apply (insert a);
        apply (subgoal_tac "0 < exp 2");
        apply arith;
        apply force;
        done;
      finally; have e: "(∑ n | natfloor x < n & n <= natfloor (K * x).
          abs (R (real n)) / (real n * real (n + 1))) < C";.;
      have "~ (ALL n. natfloor x < n & n <= natfloor (K * x) -->
          C / (∑ n | natfloor x < n & n <= natfloor (K * x).
          1 / (real (n + 1))) <=  abs (R (real n)) / (real n))";
      proof;
        assume f: "ALL n. natfloor x < n & n <= natfloor (K * x) -->
          C / (∑ n | natfloor x < n & n <= natfloor (K * x). 
          1 / real (n + 1)) <= abs (R (real n)) / real n";
        have "(∑ n | natfloor x < n & n <= natfloor (K * x).
            abs (R (real n)) / (real n * real (n + 1))) = 
          (∑ n | natfloor x < n & n <= natfloor (K * x).
            abs (R (real n)) / (real n)  * (1 / real (n + 1)))"; 
          apply (rule setsum_cong2);
          apply simp;
          done;
        also have "(∑ n | natfloor x < n & n <= natfloor (K * x).
          (C / (∑ n | natfloor x < n & n <= natfloor (K * x). 
          1 / real (n + 1))) * (1 / real (n + 1))) <= ..."
            (is "?LHS <= ?RHS"); 
          apply (rule setsum_le_cong);
          apply (rule mult_right_mono);
          apply (insert f);
          apply auto;
          done;
        also have "?LHS = C";
          apply (subst setsum_const_times);
          apply simp;
          apply (subgoal_tac "0 < (∑ n | natfloor x < n &
              n <= natfloor (K * x). 1 / (real n + 1))"); 
          apply force;
          apply (subgoal_tac "(∑ n | natfloor x < n &
              n <= natfloor (K * x). 1 / (real n + 1)) = 
            (∑ n : {natfloor x + 1}. 1 / (real n + 1)) + 
            (∑ n | natfloor x + 1 < n &
              n <= natfloor (K * x). 1 / (real n + 1))");
          apply (erule ssubst);
          apply simp;
          apply (rule order_less_le_trans);
          prefer 2;
          apply (rule setsum_nonneg');
          apply force;
          apply force;
          apply (subst setsum_Un_disjoint [THEN sym]);
          apply force;
          apply (rule bounded_nat_set_is_finite);
          apply clarify;
          apply (subgoal_tac "i < natfloor (K * x) + 1");
          apply assumption;
          apply arith;
          apply force;
          apply (rule setsum_cong);
          apply auto;
          apply (subst natfloor_add [THEN sym]);
          apply (rule order_trans);
          prefer 2;
          apply (rule a);
          apply (subgoal_tac "0 < exp 2");
          apply arith;
          apply force;
          apply simp;
          apply (rule natfloor_mono);
          apply (rule order_trans);
          apply (subgoal_tac "x + 1 <= 2 * x");
          apply assumption;
          apply (insert a);
          apply (subgoal_tac "0 < exp 2");
          apply arith;
          apply force;
          apply (rule mult_right_mono);
          apply (rule order_less_imp_le);
          apply (insert C0);
          apply (drule_tac x = K in spec);
          apply (drule_tac x = 1 in spec);
          apply (force simp add: prems);
          apply (insert a);
          apply (subgoal_tac "0 < exp 2");
          apply arith;
          apply force;
          done;
        finally show "False";
          by (insert e, auto);
      qed;
    then have "EX n. natfloor x < n & n <= natfloor (K * x) &
          abs (R (real n)) / real n < C /
        (∑ n | natfloor x < n & n <= natfloor (K * x). 
           1 / real (n + 1))";
        by auto;
    then show "EX n. natfloor x < n & n <= natfloor (K * x) &
          abs (R (real n) / real n) < eps";
      apply auto;
      apply (rule_tac x = n in exI);
      apply auto;
      apply (subst abs_div [THEN sym]);
      apply force;
      apply (subst abs_nonneg);
      apply force;
      apply (erule order_less_le_trans);
      apply (insert C0);
      apply (drule_tac x = K in spec);
      apply (drule_tac x = x in spec);
      apply (rule order_less_imp_le);
      apply (subgoal_tac "1 <= x");
      apply (force simp add: prems);
      apply (insert a); 
      apply (subgoal_tac "0 < exp 2");
      apply arith;
      apply force;
      done;
    qed;
  qed;
qed; qed; qed;

lemma PNT1a: "EX C0. ALL eps. 0 < eps --> eps < 1 --> (EX x0. ALL K x.
    exp (C0 / eps) < K --> x0 < x --> (EX n::nat. 
      x < real n & real n <= K * x &
        abs(R(real n) / (real n)) < eps))";
  apply (insert PNT1);
  apply clarify;
  apply (rule_tac x = "C0" in exI);
  apply clarify;
  apply (drule_tac x = "eps" in spec);
  apply clarify;
  apply (rule_tac x = "max x0 0" in exI);
  apply clarify;
  apply (drule_tac x = K in spec);
  apply (drule_tac x = x in spec);
  apply clarify;
  apply (subgoal_tac "x0 < x");
  apply clarify;
  apply (rule_tac x = n in exI);
  apply (rule conjI);
  apply (rule ge_natfloor_plus_one_imp_gt);
  apply arith;
  apply (rule conjI);
  apply (rule nat_le_natfloor);
  apply (rule nonneg_times_nonneg);
  apply (rule order_less_imp_le);
  apply (rule order_le_less_trans);
  prefer 2;
  apply assumption;
  apply force;
  apply arith;
  apply assumption;
  apply assumption;
  apply simp;
done;

lemma PNT2_aux1: "EX C. ALL x. 1 <= x -->
   abs (psi (natfloor x) * ln x + (∑ d = 1..natfloor x.
     Lambda d * psi ((natfloor x) div d)) - 
   2 * x * ln x) <= C * x";
  apply (insert Selberg4a);
  apply (drule set_plus_imp_minus);
  apply (simp add: func_plus func_diff);
  apply (unfold bigo_def);
  apply clarsimp;
  apply (rule_tac x = c in exI);
  apply clarify;
  apply (drule_tac x = "x - 1" in spec);
  apply (subgoal_tac "natfloor (abs(x - 1)) + 1 = natfloor (abs(x - 1) + 1)");
  apply simp;
  apply (subst natfloor_add [THEN sym]);
  apply force;
  apply simp;
done;

lemma PNT2_aux2: "EX C. ALL x y. 1 <= y --> y <= x --> 
    (psi (natfloor x) * ln x - psi (natfloor y) * ln y) <= 
    (2 * x * ln x - 2 * y * ln y) + C * x";
proof -;
  from PNT2_aux1 obtain C where "ALL x. 1 <= x -->
    abs (psi (natfloor x) * ln x + (∑ d = 1..natfloor x.
      Lambda d * psi ((natfloor x) div d)) - 
     2 * x * ln x) <= C * x";..;
  show ?thesis;
  proof ((rule exI)+, clarify);
    fix x; fix y;
    assume "(1::real) <= y";
    assume "y <= x";
    show "(psi (natfloor x) * ln x - psi (natfloor y) * ln y) <= 
      (2 * x * ln x - 2 * y * ln y) + (C + C) * x";
    proof -;
      have a: "0 <= (∑ d = 1..natfloor x.
          Lambda d * psi ((natfloor x) div d)) -
        (∑ d = 1..natfloor y.
          Lambda d * psi ((natfloor y) div d))"
          (is "0 <= ?term1");
        apply (subgoal_tac "
          (∑ d = 1..natfloor x. Lambda d * psi (natfloor x div d)) = 
          (∑ d = 1..natfloor y. 
            Lambda d * psi (natfloor x div d)) + 
          (∑ d = natfloor y + 1..natfloor x. 
            Lambda d * psi (natfloor x div d))"); 
        apply (erule ssubst);
        apply (subgoal_tac "(∑ d = 1..natfloor y. 
            Lambda d * psi (natfloor y div d)) <= 
              (∑ d = 1..natfloor y. 
            Lambda d * psi (natfloor x div d))");
        apply (subgoal_tac "0 <= (∑ d = natfloor y + 1..natfloor x. 
            Lambda d * psi (natfloor x div d))");
        apply arith;
        apply (rule setsum_nonneg');
        apply clarsimp;
        apply (rule nonneg_times_nonneg);
        apply (rule Lambda_ge_zero);
        apply (rule psi_ge_zero);
        apply (rule setsum_le_cong);
        apply (rule mult_left_mono);
        apply (rule psi_mono);
        apply (rule div_le_mono);
        apply (rule natfloor_mono);
        apply (rule prems);
        apply (rule Lambda_ge_zero);
        apply (subst setsum_Un_disjoint [THEN sym]);
        apply force;
        apply (rule bounded_nat_set_is_finite);
        apply (rule ballI);
        apply (subgoal_tac "i < natfloor x + 1");
        apply assumption;
        apply force;
        apply force;
        apply (rule setsum_cong);
        apply auto;
        apply (erule order_trans);
        apply (rule natfloor_mono);
        apply (rule prems);
        done;
      have "abs((psi (natfloor x) * ln x - psi (natfloor y) * ln y) + ?term1) -
          abs(2 * x * ln x - 2 * y * ln y) <= 
        abs((psi (natfloor x) * ln x - psi (natfloor y) * ln y) + ?term1 -
          (2 * x * ln x - 2 * y * ln y))";
        by (rule abs_triangle_ineq2);
      also have "... = abs((psi(natfloor x) * ln x + 
          (∑ d = 1..natfloor x. Lambda d * psi ((natfloor x) div d))
           - 2 * x * ln x) - 
         (psi(natfloor y) * ln y + 
          (∑ d = 1..natfloor y. Lambda d * psi ((natfloor y) div d))
           - 2 * y * ln y))";
        apply (rule arg_cong); back;
        apply (simp add: compare_rls);
        done;
      also have "... <= abs(psi(natfloor x) * ln x + 
          (∑ d = 1..natfloor x. Lambda d * psi ((natfloor x) div d))
           - 2 * x * ln x) + 
        abs(psi(natfloor y) * ln y + 
          (∑ d = 1..natfloor y. Lambda d * psi ((natfloor y) div d))
           - 2 * y * ln y)";
        by (rule abs_triangle_ineq4);
      also have "... <= C * x + C * y";
        apply (rule add_mono);
        apply (insert prems);
        apply auto;
        done;
      also have "... <= C * x + C * x";
        apply simp;
        apply (rule mult_left_mono);
        apply (rule prems);
        apply (insert prems);
        apply (drule_tac x = 1 in spec);
        apply simp;
        apply (rule order_trans);
        prefer 2;
        apply assumption;
        apply (rule nonneg_times_nonneg);
        apply auto;
        done;
      also have "... = (C + C) * x";
        by (simp add: ring_eq_simps);
      also; have "abs (psi (natfloor x) * ln x - psi (natfloor y) * ln y +
       ((∑ d = 1..natfloor x. Lambda d * psi (natfloor x div d)) -
        (∑ d = 1..natfloor y. Lambda d * psi (natfloor y div d)))) = 
        psi (natfloor x) * ln x - psi (natfloor y) * ln y +
       ((∑ d = 1..natfloor x. Lambda d * psi (natfloor x div d)) -
        (∑ d = 1..natfloor y. Lambda d * psi (natfloor y div d)))";
        apply (rule abs_nonneg);
        apply (rule nonneg_plus_nonneg);
        apply simp;
        apply (rule mult_mono);
        apply (rule psi_mono);
        apply (rule natfloor_mono);
        apply (rule prems);
        apply (subst ln_le_cancel_iff);
        apply (insert prems, arith);
        apply arith;
        apply assumption;
        apply (rule psi_ge_zero);
        apply force;
        apply (rule a);
        done;
      also; have "abs (2 * x * ln x - 2 * y * ln y) = 
          2 * x * ln x - 2 * y * ln y";
        apply (rule abs_nonneg);
        apply simp;
        apply (rule mult_mono);
        apply (rule prems);
        apply (subst ln_le_cancel_iff);
        apply (insert prems);
        apply auto;
        done;
      finally show ?thesis;
        by (insert a, arith);
    qed;
  qed;
qed;

lemma PNT2_aux3: "EX E. ALL x y. 1 <= y --> y < x --> x <= D * y -->
    (psi(natfloor x) - psi(natfloor y)) <= 2 * (x - y) + E * (x / ln x)";
proof -;
  from PNT2_aux2 obtain C where C: "ALL x y. 1 <= y --> y <= x --> 
    (psi (natfloor x) * ln x - psi (natfloor y) * ln y) <= 
    (2 * x * ln x - 2 * y * ln y) + C * x";..;
  show ?thesis;
  proof ((rule exI), clarify);;
    fix x::"real";
    fix y::"real";
    assume "1 <= y";
    assume "y < x";
    assume "x <= D * y";
    have "(psi (natfloor x) * ln x - psi (natfloor y) * ln y) <= 
        (2 * x * ln x - 2 * y * ln y) + C * x";
      by (insert C prems, auto);
    also have "psi(natfloor x) * ln x - psi(natfloor y) * ln y = 
        ln x * (psi(natfloor x) - psi(natfloor y)) + 
        psi (natfloor y) * (ln x - ln y)";
      by (simp add: ring_eq_simps);
    also have "(2 * x * ln x - 2 * y * ln y) = 
        2 * (x - y) * ln x + 2 * y * (ln x - ln y)";
      by (simp add: ring_eq_simps);
    also have "ln x - ln y = ln (x / y)";
      apply (rule ln_div [THEN sym]);
      apply (insert prems);
      apply arith+;
      done;
    finally; have "ln x * (psi (natfloor x) - psi (natfloor y))
          <= 2 * (x - y) * ln x + 2 * y * ln (x / y) + C * x";
      apply (subgoal_tac "0 <= psi(natfloor y) * ln(x / y)");
      apply arith;
      apply (rule nonneg_times_nonneg);
      apply (rule psi_ge_zero);
      apply (rule ln_ge_zero);
      apply (subst pos_le_divide_eq);
      apply (insert prems, arith);
      apply simp;
      done;
    also have "... <= 2 * (x - y) * ln x + 2 * x * ln D + C * x";
      apply (rule add_right_mono);
      apply (rule add_left_mono);
      apply (rule mult_mono);
      apply (rule mult_left_mono);
      apply (rule order_less_imp_le, rule prems);
      apply force;
      apply (subst ln_le_cancel_iff);
      apply (rule pos_div_pos);
      apply (insert prems, arith);
      apply arith;
      prefer 2;
      apply (subst pos_divide_le_eq);
      apply arith;
      apply assumption;
      apply (rule order_less_le_trans);
      apply (subgoal_tac "0 < x / y");
      apply assumption;
      apply (rule pos_div_pos);
      apply arith;
      apply arith;
      apply (subst pos_divide_le_eq);
      apply arith;
      apply assumption;
      apply arith;
      apply (rule ln_ge_zero);
      apply (subst pos_le_divide_eq);
      apply arith;
      apply simp;
      done;
    also have "... = 2 * (x - y) * ln x + (2 * ln D + C) * x";
      by (simp add: ring_eq_simps);
    finally have "ln x * (psi (natfloor x) - psi (natfloor y))
        <= 2 * (x - y) * ln x + (2 * ln D + C) * x" (is "?LHS <= ?RHS");.;
    then have "?LHS / ln x <= ?RHS / ln x";
      apply (rule divide_right_mono);
      apply (rule ln_ge_zero);
      apply (insert prems, arith);
      done;
    also have "?LHS / ln x = (psi (natfloor x) - psi (natfloor y))";
      apply (subgoal_tac "0 < ln x"); 
      apply simp;
      apply (rule ln_gt_zero);
      apply (insert prems, arith);
      done;
    also have "?RHS / ln x = 2 * (x - y) + (2 * ln D + C) * (x / ln x)"; 
      apply (subgoal_tac "0 < ln x");
      apply (subst add_divide_distrib);
      apply simp;
      apply (rule ln_gt_zero);
      apply (insert prems, arith);
      done;
    finally show "psi (natfloor x) - psi (natfloor y) <= 2 * (x - y) + 
        (2 * ln D + C) * (x / ln x)";.;
  qed;
qed;

lemma PNT2_aux4: "EX C. ALL x. abs (R(x) / x) < C";
  apply (insert error0);
  apply (simp only: bigo_alt_def);
  apply clarsimp;
  apply (rule_tac x = "c + 1" in exI);
  apply (rule allI);
  apply (drule_tac x = x in spec);
  apply (case_tac "x = 0");
  apply simp;
  apply (subst abs_divide);
  apply (subst pos_divide_less_eq);
  apply arith;
  apply (simp add: ring_eq_simps);
  apply arith;
done;

lemma PNT2_aux5: "0 < eps ==> EX x. ALL y. (x < y --> 1 / ln y < eps)";
  apply (rule_tac x = "max 1 (exp (1 / eps))" in exI);
  apply clarify;
  apply (subst pos_divide_less_eq);
  apply (rule ln_gt_zero);
  apply force;
  apply (subst mult_commute);
  apply (subst pos_divide_less_eq [THEN sym]);
  apply assumption;
  apply (subgoal_tac "1 / eps = ln (exp (1 / eps))");
  apply (erule ssubst);
  apply (subst ln_less_cancel_iff);
  apply auto;
done;

lemma PNT2: "EX lambda C1. 0 < lambda & lambda < 1 & 
    (ALL eps. 0 < eps --> eps < 1 --> (EX x1. ALL K x.
      exp (C1 / eps) < K --> x1 < x --> (EX xstar.
        x < xstar & (1 + lambda * eps) * xstar < K * x & (ALL u. 
          xstar <= u & u <= (1 + lambda * eps) * xstar -->
            abs(R u) < eps * u))))" (is "EX lambda C1. ?P lambda C1");
proof -;
  from PNT2_aux4 obtain Cstar where Cstar: "ALL x. abs (R(x) / x) < Cstar";..;
  have Cstar0: "0 < Cstar";
    apply (insert Cstar);
    apply (drule_tac x = 0 in spec);
    apply simp;
    done;
  let ?lambda = "1 / (3 * (Cstar + 3))";
  have lambda0: "0 < ?lambda";
    apply (rule pos_div_pos);
    apply force;
    apply (rule mult_pos);
    apply force;
    apply (rule pos_plus_pos);
    apply (rule Cstar0);
    apply force;
    done;
  have lambda1: "?lambda < 1";
    apply (subst pos_divide_less_eq);
    apply (rule mult_pos);
    apply force;
    apply (insert Cstar0, arith);
    apply simp;
    done;
  from PNT1a obtain C0 where C0temp: "ALL eps. 0 < eps -->
    eps < 1 --> (EX x0. ALL K x. exp (C0 / eps) < K -->
      x0 < x --> (EX n::nat. x < real n &
        real n <= K * x & abs (R (real n) / real n) < eps))";..;
  let ?C1 = "3 * C0 + ln 2";
  show ?thesis;
  proof (rule exI)+;
  show "?P ?lambda ?C1";
    apply (rule conjI);
    apply (rule lambda0);
    apply (rule conjI);
    apply (rule lambda1);
    apply clarify;
  proof -;
    fix eps::"real";
    assume eps0: "0 < eps";
    assume eps1: "eps < 1";
    have "EX x0. ALL K x. 
      exp (C0 / (eps / 3)) < K --> x0 < x --> (EX (n::nat). 
        x < real n & real n <= K * x &
          abs(R(real n) / (real n)) < eps / 3)";
      apply (insert eps0 eps1 C0temp);
      apply (drule_tac x = "eps / 3" in spec);
      apply (drule mp);
      apply arith;
      apply (drule mp);
      apply arith;
      apply assumption;
      done;
    then obtain x0 where C0x0: "ALL K x. 
      exp (C0 / (eps / 3)) < K --> x0 < x --> 
        (EX (n::nat). x < real n & real n <= K * x &
          abs(R(real n) / (real n)) < eps / 3)"; by auto;
    have C1: "!!K. exp (?C1 / eps) < K ==> 2 * exp (C0 / (eps / 3)) < K";
      apply (rule order_le_less_trans);
      prefer 2;
      apply assumption;
      apply (subgoal_tac "(3 * C0 + ln 2) / eps = 
          ln 2 / eps + (3 * C0 / eps)");
      apply (erule ssubst);
      apply (subst exp_add);
      apply simp;
      apply (rule mult_mono);
      apply (subgoal_tac "2 = exp (ln 2)");
      apply (erule ssubst);
      apply (subst exp_le_cancel_iff);
      apply simp;
      apply (subst pos_le_divide_eq);
      apply (rule eps0);
      apply (subgoal_tac "ln 2 * eps <= ln 2 * 1");
      apply simp;
      apply (rule mult_left_mono);
      apply (rule order_less_imp_le, rule eps1);
      apply force;
      apply simp;
      apply (simp add: mult_ac);
      apply force;
      apply force;
      apply (simp add: ring_eq_simps add_divide_distrib);
      done;
    from PNT2_aux3 obtain E where E: "ALL x y. 1 <= y --> y < x --> 
      x <= 2 * y --> (psi(natfloor x) - psi(natfloor y)) <= 
        2 * (x - y) + E * (x / ln x)"; ..;
    let ?E2 = "max E 1";
    have E2a: "0 < ?E2";
      apply (subgoal_tac "1 <= ?E2"); 
      apply arith;
      apply (rule le_maxI2);
      done;
    have E2b: "ALL x y. 1 <= y --> y < x --> 
      x <= 2 * y --> (psi(natfloor x) - psi(natfloor y)) <= 
        2 * (x - y) + ?E2 * (x / ln x)";
      apply (clarify);
      apply (insert E);
      apply (drule_tac x = x in spec);
      apply (drule_tac x = y in spec);
      apply clarify;
      apply (subgoal_tac "E * (x / ln x) <= ?E2 * (x / ln x)");
      apply arith;
      apply (rule mult_right_mono);
      apply (rule le_maxI1);
      apply (rule order_less_imp_le);
      apply (rule pos_div_pos);
      apply arith;
      apply (rule ln_gt_zero);
      apply arith;
      done;
    have "EX x. ALL y. (x < y --> 1 / ln y < 
        eps / (3 * ?E2 * (1 + ?lambda * eps)))"; 
      apply (rule PNT2_aux5);
      apply (rule pos_div_pos);
      apply (rule eps0);
      apply (rule mult_pos);
      apply (rule mult_pos);
      apply force;
      apply (rule E2a);
      apply (rule pos_plus_pos);
      apply force;
      apply (rule mult_pos);
      apply (rule lambda0);
      apply (rule eps0);
      done;
    then obtain xtemp where xtemp: 
      "ALL y. (xtemp < y --> 1 / ln y < 
         eps / (3 * ?E2 * (1 + ?lambda * eps)))";..;
    let ?x1 = "max (max xtemp x0) 1";
    have x1a: "1 <= ?x1"; by (rule le_maxI2);
    have x1b: "x0 <= ?x1";
      apply (rule order_trans);
      apply (rule le_maxI2);
      apply (rule le_maxI1);
      done;
    have x1c: "xtemp <= ?x1";
      apply (rule order_trans);
      apply (rule le_maxI1);
      apply (rule le_maxI1);
      done;
    show "EX x1. ALL K x. exp (?C1 / eps) < K --> x1 < x -->
        (EX xstar. x < xstar &
          (1 + 1 / (3 * (Cstar + 3)) * eps) * xstar < K * x &
            (ALL u. xstar <= u &
              u <= (1 + 1 / (3 * (Cstar + 3)) * eps) * xstar -->
                abs (R u) < eps * u))" (is "EX x1. ?P x1");
    proof ((rule exI)+, clarify);
    fix K;
    fix x;
    assume K: "exp (?C1 / eps) < K";
    assume x: "?x1 < x";
    have xa: "1 < x";
      apply (rule order_le_less_trans);
      prefer 2;
      apply (rule x);
      apply (rule x1a);
      done;
    have xb: "x0 < x";
      apply (rule order_le_less_trans);
      prefer 2;
      apply (rule x);
      apply (rule x1b);
      done;
    have xc: "xtemp < x";
      apply (rule order_le_less_trans);
      prefer 2;
      apply (rule x);
      apply (rule x1c);
      done;
    have "EX (n::nat). x < real n & real n <= (K / 2) * x &
        abs(R(real n) / (real n)) < eps / 3";
      apply (insert C0x0);
      apply (drule_tac x = "K / 2" in spec);
      apply (drule_tac x = x in spec);
      apply (drule mp);
      apply (subst pos_less_divide_eq);
      apply force;
      apply (subst mult_commute);
      apply (rule C1);
      apply (rule K);
      apply (drule mp);
      apply (rule xb);
      apply assumption;
      done;
    then obtain n::"nat" where n: "x < real n &
           real n <= K / 2 * x & abs (R (real n) / real n) < eps / 3";..;
    from n have n1: "x < real n";..; 
    from n have n2: "real n <= (K / 2) * x"; by auto;
    from n have n3: "abs (R (real n) / real n) < eps / 3"; by auto;
    show "EX xstar. x < xstar &  
      (1 + 1 / (3 * (Cstar + 3)) * eps) * xstar < K * x &
        (ALL u. xstar <= u &
          u <= (1 + 1 / (3 * (Cstar + 3)) * eps) * xstar -->
            abs (R u) < eps * u)" (is "EX xstar. ?P xstar");
    proof;
    let ?xstar = "real n";
    show "?P ?xstar";
      apply (rule conjI);
      apply (rule n1);
      apply (rule conjI);
      apply (rule order_le_less_trans);
      apply (subgoal_tac "(1 + ?lambda * eps) * real n <= 
        (1 + ?lambda * eps) * ((K / 2) * x)");
      apply assumption;
      apply (rule mult_left_mono);
      apply (rule n2);
      apply (rule nonneg_plus_nonneg);
      apply force;
      apply (rule nonneg_times_nonneg);
      apply (rule order_less_imp_le);
      apply (rule pos_div_pos);
      apply force;
      apply (rule mult_pos);
      apply force;
      apply (rule pos_plus_pos);
      apply (rule Cstar0);
      apply force;
      apply (rule order_less_imp_le);
      apply (rule eps0);
      apply (rule order_less_le_trans);
      apply (subgoal_tac "(1 + ?lambda * eps) * (K / 2 * x) < 
          2 * (K / 2 * x)");
      apply assumption;
      apply (rule mult_strict_right_mono);
      apply simp;
      apply (subst pos_divide_less_eq);
      apply (insert Cstar0, arith);
      apply (insert eps1, simp);
      apply (rule mult_pos);
      apply (subgoal_tac "0 < K");
      apply arith;
      apply (rule order_le_less_trans);
      prefer 2;
      apply (rule prems);
      apply force;
      apply (insert xa, arith);
      apply simp;
      apply clarify;
      proof -;
        fix u;
        assume xstar1: "?xstar <= u";
        assume xstar2: "u <= (1 + ?lambda * eps) * ?xstar";
        show "abs (R u) < eps * u";
        proof -;

(* reset indentation for convenience, and rename xstar to n *)
  let ?n = "?xstar";
  have "abs (R(u) / u - R(?n) / ?n) = abs(R(u) * (1 / u - 1 / ?n) + 
      (R(u) - R(?n)) / ?n)";
    apply (simp add: ring_eq_simps diff_divide_distrib); 
    done;
  also have "... <= abs (R(u) * (1 / u - 1 / ?n)) + abs ((R(u) - R(?n)) / ?n)";
    by (rule abs_triangle_ineq);
  also have "abs (R(u) * (1 / u - 1 / ?n)) = 
     abs (R(u) / u) * abs (1 - u / ?n)";
    apply (subst abs_mult [THEN sym]);
    apply (rule arg_cong);back;
    apply (simp add: ring_eq_simps);
    apply (rule nonzero_mult_divide_cancel_left);
    apply (insert n1 xa xstar1);
    apply arith;
    apply arith;
    done;
  also have "abs (1 - u / ?n) = u / ?n - 1";
    apply (subst abs_nonpos);
    apply simp;
    apply (subst pos_le_divide_eq);
    apply (insert n1 xa, arith);
    apply (simp add: xstar1);
    apply (simp add: ring_eq_simps);
    done;
  also have "abs ((R(u) - R(?n)) / ?n) = 1 / ?n * abs(R(u) - R(?n))";
    apply (subst abs_divide);
    apply simp;
    done;
  also have "R(u) - R(?n) = psi(natfloor(u)) - psi(natfloor(?n)) - 
      (u - ?n)";
    by (simp add: R_def);
  finally have "abs (R u / u - R ?n / ?n) <= 
    abs (R u / u) * (u / ?n - 1) +
      1 / ?n * abs (psi (natfloor u) - psi (natfloor ?n) - (u - ?n))";.;
  also have "... <= abs (R u / u) * (u / ?n - 1) +
      1 / ?n * (abs (psi (natfloor u) - psi (natfloor ?n)) + abs(u - ?n))";
    apply (rule add_left_mono);
    apply (rule mult_left_mono);
    apply (rule abs_triangle_ineq4);
    apply (subst pos_le_divide_eq);
    apply (insert n1 xa, arith);
    apply simp;
    done;
  also have "1 / ?n * (abs (psi (natfloor u) - psi (natfloor ?n)) + 
      abs(u - ?n))
        = (psi (natfloor u) - psi(natfloor ?n)) / ?n + (u / ?n - 1)";
    apply (subst abs_nonneg);
    apply (simp add: xstar1);
    apply (subst abs_nonneg);
    apply (simp del: natfloor_real_id);
    apply (rule psi_mono);
    apply (rule natfloor_mono);
    apply (rule prems);
    apply (simp add: ring_eq_simps diff_divide_distrib); 
    apply (insert prems, arith);
    done;
  also have "abs (R u / u) * (u / ?n - 1) +
      ((psi (natfloor u) - psi (natfloor ?n)) / ?n + (u / ?n - 1)) = 
    (u / ?n - 1) * (abs (R u / u) + 1) + 
      (psi (natfloor u) - psi (natfloor ?n)) / ?n";
    by (simp add: ring_eq_simps);
  finally have "abs (R u / u - R ?n / ?n) <= 
      (u / ?n - 1) * (abs (R u / u) + 1) +
        (psi (natfloor u) - psi (natfloor ?n)) / ?n";.;
  also have "... <= (u / ?n - 1) * (abs (R u / u) + 1) + 
      (2 * (u - ?n) + ?E2 * (u / ln u)) / ?n";
    apply (rule add_left_mono);
    apply (rule divide_right_mono);
    apply (case_tac "u = ?n");
    apply simp;
    apply (rule order_less_imp_le);
    apply (rule pos_div_pos);
    apply (rule mult_pos);
    apply (rule E2a);
    apply (insert n1 xa, arith);
    apply (rule ln_gt_zero);
    apply arith;
    apply (insert E2b);
    apply (drule_tac x = u in spec);
    apply (drule_tac x = ?n in spec);
    apply (drule_tac mp);
    apply (insert n1 xa, arith);
    apply (drule_tac mp);
    apply (insert xstar1, arith);
    apply (drule_tac mp);
    apply (rule order_trans);
    apply (rule xstar2);
    apply (rule mult_right_mono);
    apply simp;
    apply (subst pos_divide_le_eq);
    apply (insert Cstar0, arith);
    apply simp;
    apply (insert eps1, arith);
    apply arith;
    apply assumption;
    apply arith;
    done;
  also have "... = (u / ?n - 1) * (abs (R u / u) + 3) + 
      (?E2 * u / ?n) * (1 / ln u)" (is "?temp = ?term1 + ?term2");
    apply (simp add: ring_eq_simps add_divide_distrib diff_divide_distrib);
    apply auto;
    apply (insert n1 xa, arith);
    apply (subst add_divide_distrib [THEN sym]);
    apply simp;
    done;
  also have "... <= ?term1 + (?E2 * (1 + ?lambda * eps) * x / x) * 
      (1 / ln x)";
    apply (rule add_left_mono);
    apply (rule mult_mono);
    apply (subst times_divide_eq_right [THEN sym]);back;
    apply (subst mult_assoc);
    apply (subst times_divide_eq_right [THEN sym]);
    apply (rule mult_left_mono);
    apply (rule real_fraction_le);
    apply (insert xa, arith);
    apply (insert n, arith);
    apply (simp only: times_ac1);
    apply (subst mult_commute);back;back;back;back;
    apply (rule mult_left_mono);
    apply (subst mult_commute);
    apply (subst mult_commute);back;
    apply (rule xstar2);
    apply arith;
    apply (rule order_less_imp_le, rule E2a);
    apply (rule real_one_div_le_anti_mono);
    apply (rule ln_gt_zero);
    apply assumption;
    apply (subst ln_le_cancel_iff);
    apply arith;
    apply (insert xstar1 n1, arith);
    apply arith;
    apply (rule order_less_imp_le);
    apply (rule pos_div_pos);
    apply (rule mult_pos)+;
    apply (rule E2a);
    apply (rule pos_plus_pos);
    apply force;
    apply (rule mult_pos);
    apply (rule pos_div_pos);
    apply force;
    apply simp;
    apply (insert Cstar0, arith);
    apply (rule eps0);
    apply arith;
    apply arith;
    apply (rule order_less_imp_le);
    apply (rule pos_div_pos);
    apply force;
    apply (rule ln_gt_zero);
    apply arith;
    done;
  also have "... = ?term1 + (?E2 * (1 + ?lambda * eps)) * (1 / ln x)";
    apply (subgoal_tac "x ~= 0");
    apply simp;
    apply (insert xa, arith);
    done;
  finally; have "abs (R u / u - R ?n / ?n)
    <= (u / ?n - 1) * (abs (R u / u) + 3) +
      max E 1 * (1 + 1 / (3 * (Cstar + 3)) * eps) * (1 / ln x)"
       (is "?LHS <= ?RHS");.;
  then have a: "?LHS + abs (R ?n / ?n) <= ?RHS + abs(R ?n / ?n)";
    by (intro add_right_mono);
  have "abs (R u / u) = abs (R u / u - R ?n / ?n + R ?n / ?n)";
    by simp;
  also have "... <= ?LHS + abs (R ?n / ?n)";
    by (rule abs_triangle_ineq);
  also note a;
  also have "?RHS + abs(R ?n / ?n) < eps / 3 + eps / 3 + eps / 3";
    apply (rule add_le_less_mono);
    apply (rule add_mono);
    apply (rule order_trans);
    apply (subgoal_tac "(u / real n - 1) * (abs (R u / u) + 3) <=
      (?lambda * eps) * (Cstar + 3)");
    apply assumption;
    apply (rule mult_mono);
    apply (simp only: compare_rls);
    apply (subst add_commute);
    apply (subst pos_divide_le_eq);
    apply (insert n1 xa, arith);
    apply (rule prems);
    apply simp;
    apply (rule order_less_imp_le);
    apply (insert Cstar);
    apply (erule spec);
    apply (rule nonneg_times_nonneg);
    apply (rule order_less_imp_le);
    apply (rule pos_div_pos);
    apply force;
    apply simp;
    apply (insert Cstar0, arith);
    apply (insert eps0, arith);
    apply arith;
    apply simp;
    apply (subst pos_divide_le_eq);
    apply arith;
    apply (simp add: ring_eq_simps);
    apply (rule order_trans);
    apply (insert xtemp);
    apply (drule_tac x = x in spec);back;
    apply (drule mp);
    apply (rule xc);
    apply (rule mult_left_mono);
    apply (rule order_less_imp_le);
    apply assumption;
    apply (rule nonneg_times_nonneg);
    apply arith;
    apply (rule nonneg_plus_nonneg);
    apply force;
    apply (rule nonneg_times_nonneg);
    apply simp;
    apply simp;
    apply (subgoal_tac "?E2 ~= 0");
    apply simp;
    apply (subst pos_divide_le_eq);
    apply (rule pos_plus_pos);
    apply force;
    apply (rule pos_div_pos);
    apply arith;
    apply arith;
    apply (simp add: ring_eq_simps);
    apply (insert E2a);
    apply arith;
    apply (rule n3);
    done;
  also have "... = eps";
    apply simp;
    apply (subst add_divide_distrib [THEN sym]);
    apply simp;
    done;
  finally show ?thesis;
    apply (simp add: abs_divide);
    apply (subgoal_tac "abs u = u");
    apply simp;
    apply (subst pos_divide_less_eq [THEN sym]);
    apply (insert xstar1 n1 xa, arith);
    apply assumption;
    apply (rule abs_nonneg);
    apply arith;
    done;
qed;qed;qed;qed;qed;qed;qed;

lemma PNT2a: "EX lambda C1. 0 < lambda & lambda < 1 & 1 <= C1 & 
    (ALL eps. 0 < eps --> eps < 1 --> (EX x1. 1 <= x1 & (ALL K x.
      exp (C1 / eps) <= K --> x1 <= x --> (EX xstar.
        x < xstar & (1 + lambda * eps) * xstar < K * x & (ALL u. 
          xstar <= u & u <= (1 + lambda * eps) * xstar -->
            abs(R u) < eps * u)))))"; 
  apply (insert PNT2);
  apply (erule exE);
  apply (erule exE);
  apply (rule_tac x = lambda in exI);
  apply (rule_tac x = "max C1 1 + 1" in exI);
  apply clarify;
  apply (rule conjI);
  apply simp;
  apply (rule order_trans);
  prefer 2;
  apply (rule le_maxI2);
  apply force;
  apply clarify;
  apply (drule_tac x = eps in spec);
  apply clarify;
  apply (rule_tac x = "max (x1 + 1) 1" in exI);
  apply (rule conjI);
  apply (rule le_maxI2);
  apply clarify;
  apply (drule_tac x = K in spec);
  apply (drule_tac x = x in spec);
  apply (subgoal_tac "exp (C1 / eps) < K");
  apply (subgoal_tac "x1 < x");
  apply clarify;
  apply (subgoal_tac "x1 + 1 <= x");
  apply arith;
  apply (rule order_trans);
  prefer 2;
  apply assumption;
  apply (rule le_maxI1);
  apply (rule order_less_le_trans); 
  prefer 2;
  apply assumption;
  apply (subst exp_less_cancel_iff);
  apply (rule divide_strict_right_mono);
  apply simp;
  apply (rule order_le_less_trans);
  apply (subgoal_tac "C1 <= max C1 1");
  apply assumption;
  apply (rule le_maxI1);
  apply arith;
  apply assumption;
done;

lemma PNT3_aux1: "EX C. ALL x. 1 <= x -->
    abs (R (x)) * (ln x) ^ 2 <= 
      2 * (∑ n = 1..natfloor x. abs (R (x / real n)) * ln (real n)) +
                C * abs (x * (1 + ln x))";
  apply (insert bigo_lesso5 [OF error7]);
  apply clarsimp;
  apply (rule_tac x = C in exI);
  apply (rule allI);
  apply (drule_tac x = "x - 1" in spec);
  apply clarsimp;
  apply (subgoal_tac "natfloor (x - 1) + 1 = natfloor x");
  apply simp;
  apply (subst natfloor_add [THEN sym]);
  apply simp;
  apply simp;
done;

lemma PNT3_aux1a: "EX C. 0 <= C & (ALL x. 2 <= x -->
    abs (R (x)) * (ln x) ^ 2 <= 
      2 * (∑ n = 1..natfloor x. abs (R (x / real n)) * ln (real n)) +
                C * x * ln x)";
  apply (insert PNT3_aux1);
  apply clarsimp;
  apply (subgoal_tac "0 <= C");
  prefer 2;
  apply (drule_tac x = 1 in spec);
  apply simp;
  apply (rule_tac x = "C + C / ln 2" in exI);
  apply (rule conjI);
  apply (rule nonneg_plus_nonneg);
  apply assumption;
  apply (subst pos_le_divide_eq);
  apply force;
  apply simp;
  apply clarify;
  apply (drule_tac x = x in spec);
  apply clarsimp;
  apply (erule order_trans);
  apply (rule add_left_mono);
  apply (subst abs_nonneg);
  apply (subgoal_tac "0 <= ln x");
  apply arith;
  apply force;
  apply (simp add: mult_ac);
  apply (subst mult_left_commute);back;
  apply (rule mult_left_mono);
  apply (simp add: ring_eq_simps);
  apply (subst pos_le_divide_eq);
  apply force;
  apply (rule mult_left_mono);
  apply auto;  
done;

lemma PNT3_aux2: "EX C. ALL x. 0 <= x --> abs (R x) <= C * x";
  apply (insert R_bigo);
  apply (clarsimp simp add: bigo_alt_def);
  apply (rule_tac x = c in exI);
  apply clarify;
  apply (drule_tac x = x in spec);
  apply simp;
done;

lemma PNT3_aux2a: "EX C. 0 < C & (ALL x. 0 <= x --> abs (R x) <= C * x)";
  apply (insert PNT3_aux2);
  apply clarify;
  apply (rule_tac x = "C + 1" in exI);
  apply (rule conjI);
  apply (subgoal_tac "0 <= C");
  apply simp;
  apply (drule_tac x = 1 in spec);
  apply clarsimp;
  apply arith;
  apply clarify;
  apply (drule_tac x = x in spec);
  apply (auto simp add: ring_eq_simps);
done;

lemma PNT3_aux3: "EX C. ALL x. 1 <= x -->
    abs((∑ i = 1..natfloor x. ln (real i) / real i) - 
      (ln x) ^ 2 / 2) <= C"; 
  apply (insert identity_four_real_b_cor);
  apply (drule set_plus_imp_minus);
  apply (simp only: func_diff);
  apply (simp only: bigo_alt_def);
  apply clarsimp;
  apply (rule_tac x = c in exI);
  apply (rule allI);
  apply (drule_tac x = "(x - 1)" in spec);
  apply clarify;
  apply (subgoal_tac "natfloor (abs (x - 1)) + 1 = natfloor x");
  apply (subgoal_tac "abs (x - 1) + 1 = x");
  apply (simp only:);
  apply (erule Selberg.aux2);
  apply (erule Selberg.aux);
done;

lemma PNT3_aux4: "EX C. ALL x x2. 1 <= x2 --> x2 <= x --> 
    (∑ n = natfloor (x / x2) + 1..natfloor x. 
      ln (real n) / real n) <= 
        ln x2 * ln x + C";
proof -;
  from PNT3_aux3 obtain C where C: "ALL x. 1 <= x -->
    abs((∑ i = 1..natfloor x. ln (real i) / real i) - 
      (ln x) ^ 2 / 2) <= C";..;
  show ?thesis;
  proof (rule exI, clarify);
  fix x::"real";
  fix x2::"real";
  assume a: "1 <= x2";
  assume b: "x2 <= x";
  show "(∑ n = natfloor (x / x2) + 1..natfloor x. 
      ln (real n) / real n) <= 
    ln x2 * ln x + (C + C)";
  proof -;
  let ?term1 = "(((ln x) ^ 2 / 2) - (ln (x / x2))^2 / 2)";
  have "(∑n:{natfloor (x / x2) + 1..natfloor x}. 
          ln (real n) / real n) = 
      (∑n:{1..natfloor x}. ln (real n) / real n) - 
      (∑n:{1..natfloor (x / x2)}. ln (real n) / real n)";
    apply (simp add: compare_rls);
    apply (subst setsum_Un_disjoint [THEN sym]);
    apply simp;
    apply simp;
    apply force;
    apply (rule setsum_cong);
    apply auto;
    apply (erule order_trans); 
    apply (rule natfloor_mono);
    apply (subst pos_divide_le_eq);
    apply (insert a, arith);
    apply (subgoal_tac "?x * 1 <= ?x * x2");
    apply simp;
    apply (rule mult_left_mono);
    apply assumption;
    apply (insert b, arith);
    done;
  then have "abs( ?term1 - (∑n:{natfloor (x / x2) + 1..natfloor x}. 
          ln (real n) / real n)) = 
      (abs (?term1 - ...))"; by simp;
  also have "... = abs( 
    (ln x ^ 2 / 2 - 
     (∑ n = 1..natfloor x. ln(real n) / real n)) +
    ((∑ n = 1..natfloor (x / x2). ln (real n) / real n) - 
     ln (x / x2) ^ 2 / 2))";
    by (simp add: ring_eq_simps);
  also have "... <= abs((ln x ^ 2 / 2 - 
     (∑ n = 1..natfloor x. ln(real n) / real n))) +
    abs((∑ n = 1..natfloor (x / x2). ln (real n) / real n) - 
     ln (x / x2) ^ 2 / 2)";
    by (rule abs_triangle_ineq);
  also have "... <= C + C";
    apply (rule add_mono);
    apply (subst abs_diff);
    apply (insert prems, force); 
    apply (subgoal_tac "1 <= x / x2");
    apply force;
    apply (subst pos_le_divide_eq);
    apply arith;
    apply simp;
    done;
  also; have "?term1 = (2 * ln x * ln x2 - ln x2 ^ 2) / 2";
    apply (subst ln_div);
    apply (insert a b, arith);
    apply arith;
    apply (simp add: power2_eq_square diff_divide_distrib
      ring_eq_simps);
    done;
  also have "... = ln x2 * (2 * ln x - ln x2) / 2";
    by (simp add: ring_eq_simps power2_eq_square);
  finally; have x: "
    abs((∑ n = natfloor (x / x2) + 1..natfloor x. ln (real n) / real n) -
      ln x2 * (2 * ln x - ln x2) / 2) <=
    C + C";
    apply (subst abs_diff);
    apply assumption;
    done;
  have "(∑ n = natfloor (x / x2) + 1..natfloor x. 
      ln (real n) / real n) - ln x2 * (2 * ln x - ln x2) / 2 <= 
    C + C";
    apply (rule order_trans);
    prefer 2;
    apply (rule x);
    apply (rule abs_ge_self);
    done;
  then have "(∑ n = natfloor (x / x2) + 1..natfloor x. 
      ln (real n) / real n) <= 
    ln x2 * (2 * ln x - ln x2) / 2 + (C + C)";
    by arith;
  also have "ln x2 * (2 * ln x - ln x2) / 2 <= ln x2 * ln x";
    apply (subst pos_divide_le_eq);
    apply force;
    apply (subst mult_assoc);
    apply (rule mult_left_mono);
    apply simp;
    apply (insert a b, auto);
    done;
  finally; show ?thesis; by auto;
qed;qed;qed;

lemma PNT3_aux5: "EX C. 0 <= C & (ALL x. 1 <= x -->
    (∑ i = 1..natfloor x. ln (real i) / real i) <= 
      (ln x) ^ 2 / 2 + C)";
  apply (insert PNT3_aux3);
  apply clarify;
  apply (rule_tac x = C in exI);
  apply (rule conjI);
  apply (drule_tac x = 1 in spec);
  apply simp;
  apply clarify;
  apply (drule_tac x = x in spec);
  apply clarify;
  apply (subgoal_tac "(∑ i = 1..natfloor x. ln (real i) / real i) -
               ln x ^ 2 / 2 <= C");
  apply arith;
  apply (rule order_trans);
  prefer 2;
  apply assumption;
  apply (rule abs_ge_self);
  done;

lemma PNT3: "EX G. ALL x x2 S eps alpha. 
  0 < eps --> 0 < alpha --> alpha < c -->
    2 <= x2 --> exp 1 <= x2 --> x2 <= x -->
      (ALL x. x2 <= x --> abs(R x) <= alpha * x) -->
        S <= {1..natfloor x} -->
          (ALL n:S. abs(R(x / real n)) <= eps * (x / real n)) -->
  abs (R x)
    <= alpha * x -
      2 * (alpha - eps) * x * (∑n:S. ln (real n) / real n) / ln x ^ 2 +
       G * x * ln x2 / ln x";
proof -;
  from PNT3_aux1a obtain C where C: "0 <= C & (ALL x. 2 <= x --> 
    abs (R (x)) * (ln x) ^ 2 <= 
      2 * (∑ n = 1..natfloor x. abs (R (x / real n)) * ln (real n)) +
                C * x * ln x)";..;
  then have C1: "ALL x. 2 <= x --> 
    abs (R (x)) * (ln x) ^ 2 <= 
      2 * (∑ n = 1..natfloor x. abs (R (x / real n)) * ln (real n)) +
                C * x * ln x"; by blast;
  from C have C2: "0 <= C"; by blast;
  from PNT3_aux2 obtain D where D: "ALL x. 0 <= x --> abs (R x) <= D * x";..;
  then have D': "0 <= D";
    apply (drule_tac x = 1 in spec);
    apply simp;
    apply arith;
    done;
  from PNT3_aux4 obtain E where E: "ALL x x2. 1 <= x2 --> x2 <= x -->
    (∑ n = natfloor (x / x2) + 1..natfloor x. ln (real n) / real n) <= 
    ln x2 * ln x + E";..;
  then have E': "0 <= E";
    apply (drule_tac x = 1 in spec);
    apply (drule_tac x = 1 in spec);
    apply simp;
    done;
  from PNT3_aux5 obtain F where F: "0 <= F & (ALL x. 1 <= x -->
    (∑ i = 1..natfloor x. ln (real i) / real i) <= 
      (ln x) ^ 2 / 2 + F)";..;
  then have F1: "ALL x. 1 <= x -->
    (∑ i = 1..natfloor x. ln (real i) / real i) <= 
      (ln x) ^ 2 / 2 + F"; by blast;
  from F have F2: "0 <= F" by blast;
  show ?thesis; 
  proof ((rule exI)+, clarify);
  fix eps::"real";
  fix alpha::"real";
  fix x::"real";
  fix x2::"real";
  fix S::"nat set";
  assume a: "0 < eps";
  assume aa: "0 < alpha";
  assume aaa: "alpha < c";
  assume b: "2 <= x2";
  assume bb: "exp 1 <= x2";
  assume c: "x2 <= x";
  assume d: "ALL x. x2 <= x --> abs(R x) <= alpha * x";
  assume e: "S <= {1..natfloor x}";
  assume f: "ALL n:S. abs(R(x / real n)) <= eps * (x / real n)";
  have "(∑ n = 1..natfloor x. abs (R (x / real n)) * ln (real n)) = 
    (∑ n:{1..natfloor x} Int S. abs (R (x / real n)) * ln (real n)) +
    (∑ n:{1..natfloor x} - S. abs (R (x / real n)) * ln (real n))";
    apply (subst setsum_Un_disjoint [THEN sym]);
    apply (rule finite_subset);
    apply (subgoal_tac "?t <= {1..natfloor x}");
    apply assumption;
    apply force;
    apply force;
    apply (rule finite_subset);
    apply (subgoal_tac "?t <= {1..natfloor x}");
    apply assumption;
    apply force;
    apply force;
    apply force;
    apply (rule setsum_cong);
    apply force;
    apply (rule refl);
    done;
  also have "
      (∑n:{1..natfloor x} - S. abs (R (x / real n)) * ln (real n)) = 
      (∑n:{1..natfloor (x / x2)} - S. 
        abs (R (x / real n)) * ln (real n)) + 
      (∑n:{natfloor (x / x2) + 1..natfloor x} - S. 
        abs (R (x / real n)) * ln (real n))";
    apply (subst setsum_Un_disjoint [THEN sym]);
    apply (rule finite_subset);
    apply (subgoal_tac "?t <= {1..natfloor (x / x2)}");
    apply assumption;
    apply force;
    apply force;
    apply (rule finite_subset);
    apply (subgoal_tac "?t <= {natfloor (x / x2)..natfloor x}");
    apply assumption;
    apply force;
    apply force;
    apply force;
    apply (rule setsum_cong);
    apply auto;
    apply (erule order_trans);
    apply (rule natfloor_mono);
    apply (subst pos_divide_le_eq);
    apply (insert b, arith);
    apply (subgoal_tac "?x * 1 <= ?x * x2");
    apply simp;
    apply (rule mult_left_mono);
    apply (insert b, arith);
    apply (insert c, arith);
    done;
  also have "
    (∑ n:{1..natfloor x} Int S. abs (R (x / real n)) * ln (real n)) <= 
    (∑ n:{1..natfloor x} Int S. eps * (x / real n) * ln (real n))";
    apply (rule setsum_le_cong);
    apply (rule mult_right_mono);
    apply (insert f, force);
    apply force;
    done;
  also have "... = eps * x * 
      (∑ n:{1..natfloor x} Int S. ln (real n) / real n)";
    apply (subst setsum_const_times [THEN sym]);
    apply (rule setsum_cong2);
    apply simp;
    done;
  also have "(∑n:{1..natfloor (x / x2)} - S. 
        abs (R (x / real n)) * ln (real n)) <= 
      (∑n:{1..natfloor (x / x2)} - S. 
        alpha * (x / real n) * ln (real n))";
    apply (rule setsum_le_cong);
    apply (rule mult_right_mono);
    apply clarsimp;
    apply (insert d);
    apply (drule spec);
    apply (drule mp);
    prefer 2;
    apply (rule order_trans);
    apply assumption;
    apply simp;
    apply (subst pos_le_divide_eq);
    apply force;
    apply (subst mult_commute);
    apply (subst pos_le_divide_eq [THEN sym]);
    apply (insert b, arith);
    apply (rule nat_le_natfloor);
    apply (rule order_less_imp_le);
    apply (rule pos_div_pos);
    apply (insert c, arith);
    apply arith;
    apply assumption;
    apply simp;
    apply force;
    done;
  also have "... = alpha * x * (∑n:{1..natfloor (x / x2)} - S. 
      ln (real n) / real n)";
    apply (subst setsum_const_times [THEN sym]);
    apply (rule setsum_cong2);
    apply simp;
    done;
  also; have "(∑n:{natfloor (x / x2) + 1..natfloor x} - S. 
      abs (R (x / real n)) * ln (real n)) <= 
    (∑n:{natfloor (x / x2) + 1..natfloor x}. 
      abs (R (x / real n)) * ln (real n))";
    apply (rule setsum_le_cong2);
    apply simp;
    apply force;
    apply (rule nonneg_times_nonneg);
    apply auto;
    done;
  also; have "alpha * x * 
      (∑n:{1..natfloor (x / x2)} - S. ln (real n) / real n) <= 
    alpha * x *
       (∑n:{1..natfloor x} - S. ln (real n) / real n)";
    apply (rule mult_left_mono);
    apply (rule setsum_le_cong2);
    apply (rule finite_subset);
    apply (subgoal_tac "{1..natfloor x} - S <= {1..natfloor x}");
    apply assumption;
    apply force;
    apply simp;
    apply clarsimp;
    apply (erule order_trans);
    apply (rule natfloor_mono);
    apply (subst pos_divide_le_eq);
    apply (insert b c, arith);
    apply (subgoal_tac "?x * 1 <= ?x * x2");
    apply simp;
    apply (rule mult_left_mono);
    apply arith;
    apply simp;
    apply (rule real_ge_zero_div_gt_zero);
    apply force;
    apply force;
    apply (rule nonneg_times_nonneg);
    apply (insert d);
    apply (drule_tac x = x in spec);
    apply clarsimp;
    apply (rule order_trans);
    apply (subgoal_tac "0 <= abs(R x) / x");
    apply assumption;
    apply (rule real_ge_zero_div_gt_zero);
    apply force;
    apply arith;
    apply (subst pos_divide_le_eq);
    apply arith;
    apply assumption;
    apply arith;
    done;
  finally; have 
    "(∑ n = 1..natfloor x. abs (R (x / real n)) * ln (real n))
      <= eps * x * (∑n:{1..natfloor x} Int S. ln (real n) / real n) +
         (alpha * x * (∑n:{1..natfloor x} - S. ln (real n) / real n) +
          (∑ n = natfloor (x / x2) + 1..natfloor x.
           abs (R (x / real n)) * ln (real n)))";
    by arith;
  also have "... = 
    alpha * x * (∑n:{1..natfloor x}. ln (real n) / real n) 
      - ((alpha - eps) * x * 
        (∑n:{1..natfloor x} Int S. ln (real n) / real n)) +
          (∑ n = natfloor (x / x2) + 1..natfloor x.
           abs (R (x / real n)) * ln (real n))";
    apply (simp add: ring_eq_simps);
    apply (subst right_distrib [THEN sym]);
    apply (rule arg_cong);back;
    apply (subst right_distrib [THEN sym]);
    apply (rule arg_cong);back;
    apply (subst setsum_Un_disjoint [THEN sym]);
    apply (rule finite_subset);
    apply (subgoal_tac "?t <= {1..natfloor x}");
    apply assumption;
    apply force;
    apply simp;
    apply (rule finite_subset);
    apply (subgoal_tac "?t <= {1..natfloor x}");
    apply assumption;
    apply force;
    apply simp;
    apply force;
    apply (rule setsum_cong);
    apply force;
    apply (rule refl);
    done;
  finally; have g: "
      (∑ n = 1..natfloor x. abs (R (x / real n)) * ln (real n))
    <= alpha * x * (∑ n = 1..natfloor x. ln (real n) / real n) -
      (alpha - eps) * x * 
          (∑n:{1..natfloor x} Int S. ln (real n) / real n) +
      (∑ n = natfloor (x / x2) + 1..natfloor x.
        abs (R (x / real n)) * ln (real n))";.;
  have "abs (R (x)) * (ln x) ^ 2 <= 
      2 * (∑ n = 1..natfloor x. abs (R (x / real n)) * ln (real n)) +
        C * x * ln x";
    by (insert C b c, auto);
  also note g;
  also; have "(∑ n = natfloor (x / x2) + 1..natfloor x.
      abs (R (x / real n)) * ln (real n)) <= 
    (∑ n = natfloor (x / x2) + 1..natfloor x.
           D * (x / real n) * ln (real n))";
    apply (rule setsum_le_cong);
    apply (rule mult_right_mono);
    apply (insert D);
    apply (subgoal_tac "0 <= ?x / real x");
    apply force;
    apply (subst pos_le_divide_eq);
    apply simp;
    apply arith;
    apply (insert b c);
    apply simp;
    apply force;
    done;
  also have "... = D * x * (∑ n = natfloor (x / x2) + 1..natfloor x.
        (ln (real n) / real n))";
    apply (subst setsum_const_times [THEN sym]);
    apply (rule setsum_cong2);
    apply simp;
    done;
  also have "... <= D * x * (ln x2 * ln x + E)";
    apply (rule mult_left_mono);
    apply (insert E b c, force);
    apply (rule nonneg_times_nonneg);
    apply (rule D');
    apply arith;
    done;
  also have "alpha * x * (∑ n = 1..natfloor x. ln (real n) / real n) <=
      alpha * x * ((ln x)^2 / 2 + F)";
    apply (rule mult_left_mono);
    apply (insert F b c, force);
    apply (rule nonneg_times_nonneg);
    apply (insert aa, auto);
    done;
  also have "{1..natfloor x} Int S = S";
    apply (insert e);
    apply blast;
    done;
  finally; have "abs (R x) * ln x ^ 2
      <= 2 *
         (alpha * x * (ln x ^ 2 / 2 + F) -
          (alpha - eps) * x *
          (∑n:S. ln (real n) / real n) +
          D * x * (ln x2 * ln x + E)) +
         C * x * ln x"; by auto;
  also have "... = alpha * x * ln x ^ 2 - 
      2 * (alpha - eps) * x * (∑n:S. ln (real n) / real n) + 
      (x * ln x * ((2 * D) * ln x2 + C) + x * ((2 * F) * alpha + 2 * D * E))";
    by (simp add: ring_eq_simps);
  also have "... <= 
      alpha * x * ln x ^ 2 - 
      2 * (alpha - eps) * x * (∑n:S. ln (real n) / real n) + 
            (x * ln x * ((2 * D) * ln x2 + C * ln x2) + 
            (x * ln x * ln x2) * ((2 * F) * c + 2 * D * E))";
    apply (rule add_left_mono);
    apply (rule add_mono);
    apply (rule mult_left_mono);
    apply (rule add_left_mono);
    apply (subgoal_tac "C * ln (exp 1) <= C * ln x2");
    apply simp;
    apply (rule mult_left_mono);
    apply (subst ln_le_cancel_iff);
    apply force;
    apply (insert a aa aaa b bb c);
    apply arith;
    apply (rule bb);
    apply (rule C2);
    apply (rule nonneg_times_nonneg);
    apply arith;
    apply (rule ln_ge_zero);
    apply arith;
    apply (rule mult_mono);
    apply (subgoal_tac "x * ln (exp 1) * ln (exp 1) <= x * ln x * ln x2");
    apply simp;
    apply (rule mult_mono);
    apply (rule mult_left_mono);
    apply (subst ln_le_cancel_iff);
    apply (force, force, force, force);
    apply (subst ln_le_cancel_iff);
    apply (force, force, force);
    apply (rule nonneg_times_nonneg);
    apply force;
    apply (rule ln_ge_zero);
    apply force;
    apply force;
    apply (rule add_right_mono);
    apply (rule mult_left_mono);
    apply (erule order_less_imp_le);
    apply (rule nonneg_times_nonneg);
    apply force;
    apply (rule F2);
    apply (rule nonneg_times_nonneg)+;
    apply force;
    apply (rule ln_ge_zero);
    apply arith;
    apply (rule ln_ge_zero);
    apply arith;
    apply (rule nonneg_plus_nonneg);
    apply (rule nonneg_times_nonneg);
    apply (rule nonneg_times_nonneg);
    apply force;
    apply (rule F2);
    apply arith;
    apply (rule nonneg_times_nonneg)+;
    apply force;
    apply (rule D');
    apply (rule E');
    done;
  finally have x: "abs (R x) * ln x ^ 2
    <= alpha * x * ln x ^ 2 -
        2 * (alpha - eps) * x * (∑n:S. ln (real n) / real n) + 
           x * ln x * ln x2 * (2 * D + C + 2 * F * c + 2 * D * E)"
     (is "?term1 <= ?term2 - ?term3 + ?term4 * ?term5");
    by (simp add: ring_eq_simps);
  have y: "ln x ~= 0";
    apply (rule less_imp_neq [THEN not_sym]);
    apply (rule ln_gt_zero);
    apply (insert b c, arith);
    done;
  have z: "(ln x ^ 2) ~= 0";
    apply (rule less_imp_neq [THEN not_sym]);
    apply (subst power2_eq_square);
    apply (rule mult_pos);
    apply (rule ln_gt_zero);
    apply (insert b c, arith);
    apply (rule ln_gt_zero);
    apply (insert b c, arith);
    done;
  from x have "?term1 / (ln x ^ 2) <= 
      (?term2 - ?term3 + ?term4 * ?term5) / (ln x ^ 2)";
    apply (rule divide_right_mono);
    apply force;
    done;
  also have "?term1 / (ln x^2) = abs (R x)";
    by (insert y, simp);
  also have "(?term2 - ?term3 + ?term4 * ?term5) / (ln x ^ 2) = 
    ?term2 / (ln x ^ 2) - ?term3 / (ln x ^ 2) + ?term4 / (ln x ^ 2) * ?term5";
    by (simp add: ring_eq_simps add_divide_distrib diff_divide_distrib);
  also have "?term2 / (ln x ^ 2) = alpha * x";
    by (insert z, simp);
  also have "?term4 / (ln x ^ 2) * ?term5 = ?term5 * x * ln x2 / ln x";
    by (simp add: power2_eq_square y);
  finally; show "abs (R x)
    <= alpha * x -
      2 * (alpha - eps) * x * (∑n:S. ln (real n) / real n) / ln x ^ 2 +
        ?term5 * x * ln x2 / ln x";.;
qed;qed;

lemma PNT4_aux1: "1 < c2 ==> EX C. 0 < C & (ALL alpha.
  0 < alpha --> alpha < c2 --> 
    (EX xlarge. ALL x. xlarge <= x -->
      (EX S. S <= {1..natfloor x} & 
        (ALL n:S. abs(R(x / real n)) <= (alpha / c2) * (x / real n)) & 
          C * alpha^2 * (ln x)^2 
            <= (∑ n:S. ln(real n) / (real n)))))";
proof -;
  assume c2_gt_1: "1 < c2";
  from PNT2a obtain lambda c1 where lambdac1: "0 < lambda &
    lambda < 1 & 1 <= c1 & (ALL eps. 0 < eps --> eps < 1 -->
      (EX x1. 1 <= x1 & (ALL K x. exp (c1 / eps) <= K --> x1 <= x -->
        (EX xstar. x < xstar &
           (1 + lambda * eps) * xstar < K * x &
             (ALL u. xstar <= u & u <= (1 + lambda * eps) * xstar -->
               abs (R u) < eps * u)))))"; by blast;
  from lambdac1 have lambda_gt_0: "0 < lambda" by blast;
  from lambdac1 have lambda_le_1: "lambda < 1"; by blast;
  from lambdac1 have c1_gt_1: "1 <= c1"; by blast;
  show ?thesis;
proof;
  let ?C = "lambda / (32 * c1 * c2 ^ 2)";
  show "0 < ?C & (ALL alpha.
    0 < alpha --> alpha < c2 -->
      (EX xlarge. ALL x. xlarge <= x -->
        (EX S. S <= {1..natfloor x} & 
          (ALL n:S. abs(R(x / real n)) <= (alpha / c2) * (x / real n)) & 
            ?C * alpha^2 * (ln x)^2 
              <= (∑ n:S. ln(real n) / (real n)))))";
proof;
  show "0 < ?C";
    apply (rule pos_div_pos);
    apply (rule lambda_gt_0);
    apply (rule mult_pos);
    apply (rule mult_pos);
    apply force;
    apply (insert c1_gt_1, arith);
    apply (subst power2_eq_square);
    apply (rule mult_pos);
    apply (insert c2_gt_1, arith, arith);
    done;
next show "ALL alpha.
    0 < alpha --> alpha < c2 -->
      (EX xlarge. ALL x. xlarge <= x -->
        (EX S. S <= {1..natfloor x} & 
          (ALL n:S. abs(R(x / real n)) <= (alpha / c2) * (x / real n)) & 
            ?C * alpha^2 * (ln x)^2 
              <= (∑ n:S. ln(real n) / (real n))))";
proof (clarify);
  fix alpha::"real";
  assume alpha_gt_0: "0 < (alpha::real)";
  assume alpha_lt_c2: "alpha < c2";
  let ?eps = "alpha / c2";
  have eps_gt_0: "0 < ?eps";
    apply (rule pos_div_pos);
    apply (rule alpha_gt_0);
    apply (insert c2_gt_1, arith);
    done;
  have eps_lt_1: "?eps < 1";
    apply (subst pos_divide_less_eq);
    apply (insert alpha_gt_0 alpha_lt_c2, arith);
    apply simp;
    done;
  from lambdac1 eps_gt_0 eps_lt_1 have "EX x1. 1 <= x1 & (ALL K x.
      exp (c1 / ?eps) <= K --> x1 <= x --> (EX xstar.
        x < xstar & (1 + lambda * ?eps) * xstar < K * x & (ALL u. 
          xstar <= u & u <= (1 + lambda * ?eps) * xstar -->
            abs(R u) < ?eps * u)))"; by blast;
  then obtain x1 where x1c1: "1 <= x1 & (ALL K x.
      exp (c1 / ?eps) <= K --> x1 <= x --> (EX xstar.
        x < xstar & (1 + lambda * ?eps) * xstar < K * x & (ALL u. 
          xstar <= u & u <= (1 + lambda * ?eps) * xstar -->
            abs(R u) < ?eps * u)))";..;
  then have x1_ge_1: "1 <= x1"; by blast;
  let ?K = "exp (c1 / ?eps)";
  have K_gt_1: "1 < ?K";
    apply (subgoal_tac "exp 0 < ?K");
    apply simp;
    apply (subst exp_less_cancel_iff);
    apply (rule pos_div_pos);
    apply (insert c1_gt_1, arith);
    apply (insert eps_gt_0, arith);
    done;
  from x1c1 have x1K: "ALL x. x1 <= x --> (EX xstar.
        x < xstar & (1 + lambda * ?eps) * xstar < ?K * x & (ALL u. 
          xstar <= u & u <= (1 + lambda * ?eps) * xstar -->
            abs(R u) < ?eps * u))"
    by auto;
  let ?xlarge = "max (max (max (max (max (max (max 
      2 (?K powr 2)) (exp 2 + 1))
       ((2 / (1 - 1 / (1 + lambda * ?eps))) powr 2))
         (exp ((alpha * (ln x1 * 2) + c1 * (c2 * 4)) / alpha)))
           (exp (2 * (c1 * c2) / alpha)))
             (x1 powr 8))
               (exp (3 / (alpha / (8 * (c1 * c2)))))";
  show "EX xlarge. ALL x. xlarge <= x --> (EX S<={1..natfloor x}.
      (ALL n:S. abs (R (x / real n)) <= alpha / c2 * (x / real n)) &
         ?C * alpha ^ 2 * ln x ^ 2
          <= (∑n:S. ln (real n) / real n))";
proof (rule exI, clarify);
  fix x::"real";
  assume xlarge: "?xlarge <= x";
  then have x_gt_1: "1 < (x::real)" and
    x_ge_K_squared: "?K powr 2 <= x" and
    x_gt_exp2: "exp 2 < x" and
    x_ge_blah: "(2 / (1 - 1 / (1 + lambda * ?eps))) powr 2 <= x" and
    x_ge_blah2: "exp ((alpha * (ln x1 * 2) + c1 * (c2 * 4)) / alpha) 
      <= x" and
    x_ge_blah3: "exp (2 * (c1 * c2) / alpha) <= x" and
    x_ge_blah4: "x1 powr 8 <= x" and
    x_ge_blah5: "exp (3 / (alpha / (8 * (c1 * c2)))) <= x";
      by auto;

  let ?jstar = "natfloor (ln x1 / ln ?K) + 1";
  have jstar: "!!j. ?jstar < j ==> x1 <= ?K powr (real j)";
    apply (subst ln_le_cancel_iff [THEN sym]);
    apply simp;
    apply (insert x1_ge_1, arith);
    apply force;
    apply (subst ln_pwr);
    apply force;
    apply arith;
    apply (rule order_less_imp_le);
    apply (subst pos_divide_less_eq [THEN sym]);
    apply (rule ln_gt_zero);
    apply (rule exp_gt_one);
    apply (rule pos_div_pos);
    apply (insert c1_gt_1, arith);    
    apply (rule eps_gt_0);
    apply (rule ge_natfloor_plus_one_imp_gt);
    apply (erule order_less_imp_le);
    done;

  let ?jhat = "natfloor (ln x / (2 * ln ?K)) - 1";
  have jhat: "!!j. j <= ?jhat ==> ?K powr ((real j) + 1) <= x powr (1 / 2)";
    apply (subst ln_le_cancel_iff [THEN sym]);
    apply force;
    apply (rule powr_gt_zero);
    apply (subst ln_pwr);
    apply (insert x_gt_1, arith);
    apply simp;
    apply (subst ln_pwr);
    apply simp;
    apply simp;
    apply simp;
    apply (subst pos_divide_le_eq);
    apply (rule alpha_gt_0);
    apply (subgoal_tac "real (j + 1) * (c1 * (c2 * 2)) <= alpha * ln x"); 
    apply (simp add: ring_eq_simps compare_rls);
    apply (subst pos_le_divide_eq [THEN sym]);
    apply (rule mult_pos);
    apply (insert c1_gt_1, arith);
    apply (rule mult_pos);
    apply (insert c2_gt_1, arith);
    apply force;
    apply (rule nat_le_natfloor);
    apply (rule real_ge_zero_div_gt_zero);
    apply (rule nonneg_times_nonneg);
    apply (rule order_less_imp_le);
    apply (rule alpha_gt_0);
    apply (rule ln_ge_zero);
    apply (rule order_less_imp_le);
    apply (rule x_gt_1);
    apply (rule mult_pos);
    apply (insert c1_gt_1, arith);
    apply arith;    
    apply (simp add: mult_ac);
    apply (subgoal_tac "natfloor 1 <= 
      natfloor (alpha * ln x / (c1 * (c2 * 2)))");
    apply simp;
    apply arith;
    apply (rule natfloor_mono);
    apply (subst pos_le_divide_eq);
    apply (simp add: pos_le_divide_eq mult_ac);
    apply (rule mult_pos);
    apply arith;
    apply arith;
    apply simp;
    apply (insert x_ge_K_squared);
    apply (subgoal_tac "2 * ln (exp (c1 / (alpha / c2))) <= ln x");
    apply simp;
    apply (subst mult_commute);
    apply (subst pos_divide_le_eq [THEN sym]);
    apply (rule alpha_gt_0);
    apply (simp add: mult_ac);
    apply (subst ln_pwr [THEN sym]);
    apply auto;
    done;
  have xstar_aux: "!!j. ?jstar < j ==> 
    (EX xstar.
        ?K powr (real j) < xstar & (1 + lambda * ?eps) * xstar < 
        ?K * (?K powr (real j)) & (ALL u. 
          xstar <= u & u <= (1 + lambda * ?eps) * xstar -->
            abs(R u) < ?eps * u))";
    apply (insert x1K);
    apply (drule_tac x = "?K powr (real j)" in spec);
    apply (drule mp);
    apply (erule jstar);
    apply assumption;
    done;
  have "EX xstar. ALL j. ?jstar < j -->
    ?K powr (real j) < xstar j & (1 + lambda * ?eps) * 
       xstar j < ?K * (?K powr (real j)) & (ALL u. 
          xstar j <= u & u <= (1 + lambda * ?eps) * xstar j -->
            abs(R u) < ?eps * u)";
    apply (rule exI);
    apply (clarify);
    apply (drule xstar_aux);
    apply (erule someI_ex);
    done;
  then obtain xstar where xstar: "ALL j. ?jstar < j -->
    ?K powr (real j) < xstar j & (1 + lambda * ?eps) * 
       xstar j < ?K * (?K powr (real j)) & (ALL u. 
          xstar j <= u & u <= (1 + lambda * ?eps) * xstar j -->
            abs(R u) < ?eps * u)";..;
  then have xstar0: "!!j u. ?jstar < j ==> xstar j <= u ==>
      u <= (1 + lambda * ?eps) * xstar j ==>
        abs (R u) < ?eps * u"; by blast;
  from xstar have xstar1: "!!j. ?jstar < j ==> ?K powr (real j) < xstar j";
    by blast;
  have xstar1a: "!!j. ?jstar < j ==> 0 < xstar j";
    apply (rule order_le_less_trans);
    prefer 2;
    apply (erule xstar1);
    apply force;
    done;
  from xstar have xstar2: "!!j. ?jstar < j ==>
      (1 + lambda * ?eps) * xstar j < ?K * (?K powr (real j))"; by blast;
  have xstar2a: "!!j. ?jstar < j ==> 
      xstar j < ?K powr (real j + 1)";
    apply (rule order_less_trans);
    prefer 2;
    apply (subgoal_tac "?K powr (real j + 1) = 
      ?K * (?K powr (real j))");
    apply (erule ssubst);
    apply (erule xstar2);
    apply (simp add: powr_add);
    apply (subgoal_tac "1 * xstar j < ?t");
    apply simp;
    apply (rule mult_strict_right_mono);
    apply simp;
    apply (rule pos_div_pos);
    apply (rule mult_pos);
    apply (rule lambda_gt_0);
    apply (rule alpha_gt_0);
    apply (insert c2_gt_1, arith);
    apply (erule xstar1a);
    done;
  have xstar2b: "!!j. ?jstar < j ==> j <= ?jhat ==> 
      xstar j < x powr (1 / 2)";
    apply (rule order_less_le_trans);
    apply (erule xstar2a);
    apply (erule jhat);
    done;
  have xstar2c: "!!j. ?jstar < j ==> j <= ?jhat ==>
      x powr (1 / 2) < x / xstar j";
    apply (subst pos_less_divide_eq);
    apply (erule xstar1a);
    apply (subst mult_commute);
    apply (subst pos_less_divide_eq [THEN sym]);
    apply force;
    apply (subgoal_tac "x = x powr 1");
    apply (erule ssubst); back;back;
    apply (subst powr_divide2);
    apply simp;
    apply (rule xstar2b);
    apply force;
    apply force;
    apply (rule sym);
    apply (subst powr_one_gt_zero_iff);
    apply (insert x_gt_1, arith);
    done;
  from xstar have xstar3: "!!j. ?jstar < j ==> xstar j <= u ==>
      u <= (1 + lambda * ?eps) * xstar j ==> abs(R u) < ?eps * u"; by blast;
  have xstar4_aux: "!!j n. ?jstar < j ==> xstar j <= x / real (n::nat) ==>
      0 < real n";
    apply (subgoal_tac "~(n = 0)");
    apply arith;
    apply (rule notI);
    apply (frule xstar1a);
    apply simp;
    done;
  have xstar4: "!!j n. ?jstar < j ==> xstar j <= x / real (n::nat) ==>
      real n <= x / xstar j";
    apply (subst pos_le_divide_eq);
    apply (erule xstar1a);
    apply (subst mult_commute);
    apply (subst pos_le_divide_eq [THEN sym]);
    apply (erule xstar4_aux);
    apply assumption+;
    done;
  have xstar5: "!!j n. ?jstar < j ==> xstar j <= x / real (n::nat) ==>
      real n < x / (?K powr (real j))";
    apply (rule order_le_less_trans);
    apply (erule xstar4);
    apply assumption;
    apply (rule divide_strict_left_mono);
    apply (erule xstar1);
    apply (insert x_gt_1, arith);
    apply (rule mult_pos);
    apply (erule xstar1a);
    apply force;
    done;
  have xstar6: "!!j n. ?jstar < j ==>
    xstar j <= x / real (n::nat) ==>
      x / real n <= (1 + lambda * ?eps) * xstar j ==> 
        x / ((1 + lambda * ?eps) * xstar j) <= real n";
    apply (subst pos_divide_le_eq);
    apply (rule mult_pos);
    apply (rule pos_plus_pos);
    apply force;
    apply (rule mult_pos);
    apply (rule lambda_gt_0);
    apply (rule eps_gt_0);
    apply (erule xstar1a);
    apply (subst mult_commute);
    apply (subst pos_divide_le_eq [THEN sym]);
    apply (elim xstar4_aux);
    apply assumption+;
    done;
  have xstar7: "!!j n. ?jstar < j ==>
    xstar j <= x / real (n::nat) ==>
      x / real n <= (1 + lambda * ?eps) * xstar j ==> 
        x / (?K * (?K powr (real j))) < real n";
    apply (rule order_less_le_trans);
    prefer 2;
    apply (erule xstar6);
    apply (force, force);
    apply (rule divide_strict_left_mono);
    apply (erule xstar2);
    apply (insert x_gt_1, arith);
    apply (rule mult_pos);
    apply (rule mult_pos);
    apply force;
    apply force;
    apply (rule mult_pos);
    apply (rule pos_plus_pos);
    apply force;
    apply (rule mult_pos);
    apply (rule lambda_gt_0);
    apply (rule eps_gt_0);
    apply (erule xstar1a);
    done;
  have xstar8: "!!i j n. ?jstar < i ==> i < j ==> 
      xstar i <= x / real (n::nat) ==>
        x / real n <= (1 + lambda * ?eps) * xstar i ==> 
          xstar j <= x / real (n::nat) ==> False";
    apply (subgoal_tac "real n < x / (?K powr (real j))");
    apply (subgoal_tac "x / (?K * (?K powr (real i))) < real n"); 
    apply (subgoal_tac "x / (?K powr (real j)) <= 
      x / (?K * (?K powr (real i)))");
    apply arith;
    apply (subgoal_tac "?K * (?K powr (real i)) = ?K powr (real (i + 1))");
    apply (erule ssubst);
    apply (rule real_pos_div_le_mono);
    apply (rule powr_gt_zero);
    apply (rule powr_mono);
    apply arith;
    apply (insert K_gt_1, simp);
    apply (insert x_gt_1, arith);
    apply (simp add: powr_add);
    apply (rule xstar7);
    apply force;
    apply force;
    apply force;
    apply (rule xstar5);
    apply force;
    apply force;
    done;

  let ?S = "UN j:{?jstar + 1..?jhat}. 
      {n::nat. xstar j <= x / real n & 
               x / real n <= (1 + lambda * ?eps) * xstar j}";
  show "EX S<={1..natfloor x}.
      (ALL n:S. abs (R (x / real n)) <= alpha / c2 * (x / real n)) &
         ?C * alpha ^ 2 * ln x ^ 2
          <= (∑n:S. ln (real n) / real n)";
proof;
  show "?S <= {1..natfloor x} &
    (ALL n:?S. abs (R (x / real n)) <= alpha / c2 * (x / real n)) &
    ?C * alpha ^ 2 * ln x ^ 2 <= (∑n:?S. ln (real n) / real n)";
proof;
  show "?S <= {1..natfloor x}";
    apply clarsimp;
    apply (rule conjI);
    apply (subgoal_tac "0 < real x");
    apply arith;
    apply (rule xstar4_aux);
    prefer 2;
    apply assumption;
    apply force;
    apply (rule real_le_natfloor);
    apply (rule order_trans);
    apply (rule order_less_imp_le);
    apply (rule xstar5);
    prefer 2;
    apply assumption;
    apply force;
    apply (subst pos_divide_le_eq);
    apply force;
    apply (subgoal_tac "?x * 1 <= ?x * exp (c1 / (alpha / c2)) powr real j");
    apply simp;
    apply (rule mult_left_mono);
    apply (rule ge_one_powr_ge_zero);
    apply (subgoal_tac "exp 0 <= exp (c1 / ?eps)");
    apply simp;
    apply (subst exp_le_cancel_iff);
    apply (rule real_ge_zero_div_gt_zero);
    apply (insert c1_gt_1, arith);
    apply (rule eps_gt_0);
    apply simp;
    apply (insert x_gt_1, arith);
    done;
next show "(ALL n:?S. abs (R (x / real n)) <= alpha / c2 * (x / real n)) &
         ?C * alpha ^ 2 * ln x ^ 2 <= (∑n:?S. ln (real n) / real n)";
 proof;
  show "(ALL n:?S. abs (R (x / real n)) <= alpha / c2 * (x / real n))";
    apply clarify;
    apply (rule order_less_imp_le);
    apply (rule xstar0);
    prefer 2;
    apply assumption;
    apply force;
    apply assumption;
    done;
next show "?C * alpha ^ 2 * ln x ^ 2 <= (∑n:?S. ln (real n) / real n)";
proof -;
  have "(∑ n: ?S. ln (real n) / real n) = 
    (∑ j:{?jstar + 1..?jhat}.
       (∑ n::nat | xstar j <= x / real n & 
           x / real n <= (1 + lambda * ?eps) * xstar j.
         ln (real n) / real n))";
    apply (rule setsum_UN_disjoint);
    apply simp;
    apply clarsimp;
    apply (rule bounded_nat_set_is_finite);
    apply clarsimp;
    apply (subgoal_tac "i < natfloor (x / xstar j) + 1");
    apply assumption;
    apply (subgoal_tac "i <= natfloor (x / xstar j)");
    apply arith;
    apply (rule real_le_natfloor);
    apply (rule xstar4);
    apply force;
    apply force;
    apply (clarsimp simp add: Int_def);
    apply (subgoal_tac "ja < j | j < ja");
    apply (erule disjE);
    apply (rule xstar8);
    prefer 2;
    apply assumption;
    apply force;
    apply force;
    apply force;
    apply force;
    apply (rule xstar8);
    prefer 2;
    apply assumption;
    apply auto;
    done;
  also have "(∑ j:{?jstar + 1..?jhat}.
       (∑ n::nat | xstar j <= x / real n & 
           x / real n <= (1 + lambda * ?eps) * xstar j.
         ln (x / xstar j) / (x / xstar j))) <= ..." (is "?term1 <= ?temp");
    apply (rule setsum_le_cong);
    apply (rule setsum_le_cong);
    apply (rule ln_x_over_x_mono);
    apply clarsimp;
    apply (rule order_trans);
    prefer 2;
    apply (rule order_less_imp_le);
    apply (rule xstar7);
    prefer 2;
    apply force;
    apply force;
    apply force;
    apply (rule order_trans);
    apply (subgoal_tac "exp 1 <= ?x powr (1 / 2)");
    apply assumption;
    apply (subst ln_le_cancel_iff [THEN sym]);
    apply simp;
    apply simp;
    apply (simp add: powr_def);
    apply (subst exp_le_cancel_iff [THEN sym]);
    apply (subgoal_tac "exp (ln ?x) = ?x"); 
    apply (erule ssubst);
    apply (rule order_less_imp_le);
    apply (rule x_gt_exp2);
    apply (subst exp_ln_iff);
    apply (insert x_gt_1, arith);
    apply (subst pos_le_divide_eq);
    apply (rule mult_pos);
    apply (force, force);
    apply (subst mult_commute);
    apply (subst pos_le_divide_eq [THEN sym]);
    apply force;
    apply (subgoal_tac "?x / ?x powr (1 / 2) = ?x powr (1 / 2)");
    apply (erule ssubst);
    apply (rule order_trans);
    prefer 2;
    apply (rule jhat);
    apply (subgoal_tac "x <= ?t");
    apply assumption;
    apply force;
    apply (simp add: powr_add);
    apply (subst nonzero_divide_eq_eq);
    apply simp;
    apply (simp add: powr_add [THEN sym]);
    apply clarsimp;
    apply (rule xstar4);
    apply auto;
    done;
  also have "?term1 = (∑ j:{?jstar + 1..?jhat}. real (card
      {n::nat. xstar j <= x / real n &
            x / real n <= (1 + lambda * ?eps) * xstar j}) *
      (ln (x / xstar j) / (x / xstar j)))";
    apply (rule setsum_cong2);
    apply (subst setsum_constant);
    apply (rule bounded_nat_set_is_finite);
    apply clarsimp;
    apply (subgoal_tac "i <= natfloor (?x / xstar x)");
    prefer 2;
    apply (rule real_le_natfloor);
    apply (rule xstar4);
    apply force;
    apply arith;
    apply (subgoal_tac "i < Suc (natfloor (?x / xstar x))");
    apply assumption;
    apply (erule le_imp_less_Suc);
    apply (subst real_eq_of_nat [THEN sym]);
    apply (rule refl);
    done;
  also; have "(∑ j:{?jstar + 1..?jhat}. real (card
      {natfloor (x / ((1 + lambda * ?eps) * xstar j))+1..
        natfloor (x / xstar j)}) * 
      (ln (x / xstar j) / (x / xstar j))) <= ..." 
        (is "?term2 <= ?temp");
    apply (rule setsum_le_cong);
    apply (rule mult_right_mono);
    apply (rule le_imp_real_of_nat_le);
    apply (rule card_mono);
    apply (rule bounded_nat_set_is_finite);
    apply clarsimp;
    apply (subgoal_tac "i <= natfloor (?x / xstar x)");
    prefer 2;
    apply (rule real_le_natfloor);
    apply (rule xstar4);
    apply force;
    apply arith;
    apply (subgoal_tac "i < Suc (natfloor (?x / xstar x))");
    apply assumption;
    apply (erule le_imp_less_Suc);
    apply auto;
    apply (subst pos_le_divide_eq);
    apply simp;
    apply (subst mult_commute);
    apply (subst pos_le_divide_eq [THEN sym]);
    apply (rule xstar1a);
    apply force;
    apply (rule nat_le_natfloor);
    apply (rule order_less_imp_le);
    apply (rule pos_div_pos);
    apply (insert x_gt_1, arith);
    apply (rule xstar1a);
    apply force;
    apply assumption;
    apply (subst pos_divide_le_eq);
    apply simp;
    apply (subst mult_commute);
    apply (subst pos_divide_le_eq [THEN sym]);
    apply (rule mult_pos);
    apply (rule pos_plus_pos);
    apply force;
    apply (rule pos_div_pos);
    apply (rule mult_pos);
    apply (rule lambda_gt_0);
    apply (rule alpha_gt_0);
    apply (insert c2_gt_1, arith);
    apply (rule xstar1a);
    apply force;
    apply (rule order_less_imp_le);
    apply (erule ge_natfloor_plus_one_imp_gt);
    apply (rule real_ge_zero_div_gt_zero);
    apply (rule nonneg_times_nonneg);
    apply (rule ln_ge_zero);
    apply (rule order_trans);
    prefer 2;
    apply (rule order_less_imp_le);
    apply (rule xstar2c);
    apply (force, force);
    apply (subgoal_tac "1 powr (1 / 2) <= ?x powr (1 / 2)");
    apply (simp add: powr_one_eq_one);
    apply (rule power_mono2);
    apply (force, force);
    apply (rule order_less_imp_le);
    apply (rule x_gt_1);
    apply (rule order_less_imp_le);
    apply (rule xstar1a);
    apply force;
    apply force;
    done;
  also (order_trans2); have "?term2 = (∑ j:{?jstar + 1..?jhat}. 
      (real (natfloor (x / xstar j)) -
       real (natfloor (x / ((1 + lambda * alpha / c2) * xstar j)))) * 
            (ln (x / xstar j) / (x / xstar j)))";
    apply (rule setsum_cong2);
    apply (simp add: natfloor_plus_one);
    apply (subgoal_tac "Suc (natfloor (?x / xstar x)) -
                (natfloor (?x / ((1 + lambda * alpha / c2) * xstar x)) +
                 1) = natfloor (?x / xstar x) -
                natfloor (?x / ((1 + lambda * alpha / c2) * xstar x))"); 
    apply (erule ssubst);
    apply (subst real_of_nat_diff);
    apply (rule natfloor_mono);
    apply (rule real_pos_div_le_mono);
    apply (rule xstar1a);
    apply force;
    apply (simp add: ring_eq_simps);
    apply (rule order_less_imp_le);
    apply (rule pos_div_pos);
    apply (rule mult_pos);
    apply (rule alpha_gt_0);
    apply (rule mult_pos);
    apply (rule lambda_gt_0);
    apply (rule xstar1a);
    apply (simp add: mult_ac);
    apply arith;
    apply (insert c2_gt_1, simp);
    apply (insert x_gt_1, simp);
    apply simp;
    apply arith;
    done;
  also; have "(∑ j:{?jstar + 1..?jhat}. 
      ((x / xstar j - 1) -
      (x / ((1 + lambda * ?eps) * xstar j))) * 
            (ln (x / xstar j) / (x / xstar j))) <= ...";
    apply (rule setsum_le_cong);
    apply (rule mult_right_mono);
    apply (rename_tac xa);
    apply (subgoal_tac "real (natfloor (x / ((1 + lambda * alpha / c2) * 
        xstar xa))) <= x / ((1 + lambda * ?eps) * xstar xa)");
    apply (subgoal_tac "x / xstar xa <= real (natfloor (x / xstar xa)) + 1");
    apply arith;
    apply (rule real_natfloor_plus_one_ge);
    apply (rule nat_le_natfloor);
    apply (rule order_less_imp_le);
    apply (rule pos_div_pos);
    apply (insert x_gt_1, simp);
    apply (rule mult_pos);
    apply (rule pos_plus_pos);
    apply force;
    apply (rule mult_pos);
    apply (rule lambda_gt_0);
    apply (rule eps_gt_0);
    apply (rule xstar1a);
    apply force;
    apply simp;
    apply (rule real_ge_zero_div_gt_zero);
    apply (rule ln_ge_zero);
    apply (rule order_trans);
    prefer 2;
    apply (rule order_less_imp_le);
    apply (rule xstar2c);
    apply (force, force);
    apply (rename_tac xa);
    apply (subgoal_tac "1 powr (1 / 2) <= x powr (1 / 2)");
    apply (simp add: powr_one_eq_one);
    apply (rule power_mono2);
    apply (force, force);
    apply (rule order_less_imp_le);
    apply (rule x_gt_1);
    apply (rule pos_div_pos);
    apply force;
    apply (rule xstar1a);
    apply force;
    done;
  also (order_trans2) have "(∑ j:{?jstar + 1..?jhat}. ((x / xstar j - 1) -
      (x / ((1 + lambda * ?eps) * xstar j))) * 
            (ln (x / xstar j) / (x / xstar j))) = 
    (∑ j:{?jstar + 1..?jhat}. 
      ((1 - 1 / (1 + lambda * ?eps)) * (x / xstar j) - 1) *
            (ln (x / xstar j) / (x / xstar j)))";
    apply (rule setsum_cong2);
    apply (simp add: ring_eq_simps);
    done;
  also have "(∑ j:{?jstar + 1..?jhat}. 
      (1 / 2) * (1 - 1 / (1 + lambda * ?eps)) * (x / xstar j) *
            (ln (x / xstar j) / (x / xstar j))) <= ...";
    apply (rule setsum_le_cong);
    apply (rule mult_right_mono);
    apply (subst mult_assoc);
    apply (subst times_divide_eq_left);
    apply (subst pos_divide_le_eq);
    apply simp;
    apply (subst mult_commute);
    apply (subst right_diff_distrib);
    apply (rename_tac xa);
    apply (subgoal_tac "2 * 1 <= 
      2 * ((1 - 1 / (1 + lambda * (alpha / c2))) * (x / xstar xa)) -
      1 * ((1 - 1 / (1 + lambda * (alpha / c2))) * (x / xstar xa))");
    apply (simp only: compare_rls);
    apply (subst left_diff_distrib [THEN sym]);
    apply simp;
    apply (subst times_divide_eq_right [THEN sym]);
    apply (subst mult_commute);
    apply (subst pos_divide_le_eq [THEN sym]);
    apply simp;
    apply (subst pos_divide_less_eq);
    apply (rule pos_plus_pos);
    apply force;
    apply (rule pos_div_pos);
    apply (rule mult_pos);
    apply (rule lambda_gt_0);
    apply (rule alpha_gt_0);
    apply (insert c2_gt_1, arith);
    apply simp;
    apply (rule pos_div_pos);
    apply (rule mult_pos);
    apply (rule lambda_gt_0);
    apply (rule alpha_gt_0);
    apply (insert c2_gt_1, arith);
    apply (rule order_trans);
    prefer 2;
    apply (rule order_less_imp_le);
    apply (rule xstar2c);
    apply force;
    apply force;
    apply (subgoal_tac "2 / (1 - 1 / (1 + lambda * alpha / c2)) = 
      ((2 / (1 - 1 / (1 + lambda * alpha / c2))) powr 2) powr (1 / 2)");
    apply (erule ssubst);
    apply (rule power_mono2);
    apply force;
    apply force;
    apply (subst times_divide_eq_right [THEN sym]);
    apply (rule x_ge_blah);
    apply (simp add: powr_powr);
    apply (rule sym);
    apply (subst powr_one_gt_zero_iff);
    apply (rule pos_div_pos);
    apply force;
    apply simp;
    apply (subst pos_divide_less_eq);
    apply (rule pos_plus_pos);
    apply force;
    apply (rule pos_div_pos);
    apply (rule mult_pos);
    apply (rule lambda_gt_0);
    apply (rule alpha_gt_0);
    apply (insert c2_gt_1, arith);
    apply simp;
    apply (rule pos_div_pos);
    apply (rule mult_pos);
    apply (rule lambda_gt_0);
    apply (rule alpha_gt_0);
    apply (insert c2_gt_1, arith);
    apply (rule real_ge_zero_div_gt_zero);
    apply (rule ln_ge_zero);
    apply (rule order_trans);
    prefer 2;
    apply (rule order_less_imp_le);
    apply (rule xstar2c);
    apply (force, force);
    apply (subgoal_tac "1 powr (1 / 2) <= ?x powr (1 / 2)");
    apply (simp add: powr_one_eq_one);
    apply (rule power_mono2);
    apply (force, force);
    apply (rule order_less_imp_le);
    apply (rule x_gt_1);
    apply (rule pos_div_pos);
    apply (insert x_gt_1, arith);
    apply (rule xstar1a);
    apply auto;
    done;
  also (order_trans2); have "(∑ j:{?jstar + 1..?jhat}. 
      (1 / 2) * (1 - 1 / (1 + lambda * ?eps)) * (x / xstar j) *
            (ln (x / xstar j) / (x / xstar j))) = 
    (∑ j:{?jstar + 1..?jhat}. 
      (1 / 2) * (1 - 1 / (1 + lambda * ?eps)) * (ln (x / xstar j)))";
    apply (rule setsum_cong2);
    apply (rename_tac xa);
    apply (subgoal_tac "x / xstar xa ~= 0");
    apply simp;
    apply (subgoal_tac "0 < x / xstar xa");
    apply arith;
    apply (rule pos_div_pos);
    apply (insert x_gt_1, arith);
    apply (rule xstar1a);
    apply auto;
    done;
  also have "(∑ j:{?jstar + 1..?jhat}. 
      (1 / 2) * (1 - 1 / (1 + lambda * ?eps)) * (ln (x powr (1 / 2)))) <= ...";
    apply (rule setsum_le_cong);
    apply (rule mult_left_mono);
    apply (subst ln_le_cancel_iff);
    apply force;
    apply (rule pos_div_pos);
    apply (insert x_gt_1, arith);
    apply (rule xstar1a);
    apply force;
    apply (rule order_less_imp_le);
    apply (rule xstar2c);
    apply force;
    apply force;
    apply (rule nonneg_times_nonneg);
    apply force;
    apply simp;
    apply (subst pos_divide_le_eq);
    apply (rule pos_plus_pos);
    apply force;
    apply (rule pos_div_pos);
    apply (rule mult_pos);
    apply (rule lambda_gt_0);
    apply (rule alpha_gt_0);
    apply (insert c2_gt_1, arith);
    apply simp;
    apply (rule order_less_imp_le);
    apply (rule pos_div_pos);
    apply (rule mult_pos);
    apply (rule lambda_gt_0);
    apply (rule alpha_gt_0);
    apply (insert c2_gt_1, arith);
    done;
  also (order_trans2); have "(∑ j:{?jstar + 1..?jhat}. 
      (1 / 2) * (1 - 1 / (1 + lambda * ?eps)) * (ln (x powr (1 / 2)))) = 
    (∑ j:{?jstar + 1..?jhat}. 
      (1 / 4) * (1 - 1 / (1 + lambda * ?eps)) * (ln x))";
    apply (rule setsum_cong2);
    apply (subst ln_pwr);
    apply (insert x_gt_1, arith);
    apply force;
    apply simp;
    done;
  also have "... = (1 / 4) * (1 - 1 / (1 + lambda * ?eps)) * (ln x) * 
      real (card({?jstar + 1..?jhat}))";
    apply (subst setsum_constant);
    apply force;
    apply (subst real_eq_of_nat [THEN sym]);
    apply (rule mult_commute);
    done;
  also have "... = (1 / 4) * (1 - 1 / (1 + lambda * ?eps)) * (ln x) * 
       (real (natfloor (ln x / (2 * ln ?K))) -
       real (natfloor (ln x1 / ln ?K)) - 2)";
    apply (rule arg_cong); back;
    apply simp;
    apply (subgoal_tac "Suc (natfloor (ln x * alpha / (2 * (c1 * c2))) - 1)
      = natfloor (ln x * alpha / (2 * (c1 * c2)))");
    apply (erule ssubst);
    apply (subst real_of_nat_diff);
    apply (subst add_assoc);
    apply (subst natfloor_add [THEN sym]);
    apply (rule real_ge_zero_div_gt_zero);
    apply (rule nonneg_times_nonneg);
    apply (rule ln_ge_zero);
    apply (rule x1_ge_1);
    apply (rule order_less_imp_le, rule alpha_gt_0);
    apply (rule mult_pos);
    apply (insert c1_gt_1, arith);
    apply (insert c2_gt_1, arith);
    apply (rule natfloor_mono);
    apply simp;
    apply (subst pos_le_divide_eq);
    apply (rule mult_pos);
    apply force;
    apply (rule mult_pos);
    apply arith;
    apply arith;
    apply (simp add: ring_eq_simps);
    apply (subgoal_tac "alpha * ln x = ln x * alpha");
    apply (erule ssubst);
    apply (subst pos_divide_le_eq [THEN sym]);
    apply (rule alpha_gt_0);
    apply (subst exp_le_cancel_iff [THEN sym]);
    apply (subgoal_tac "exp (ln x) = x");
    apply (erule ssubst);
    apply (rule x_ge_blah2);
    apply (subst exp_ln_iff);
    apply (insert x_gt_1, arith);
    apply (rule mult_commute);
    apply arith;
    apply (subgoal_tac "1 <= natfloor (ln x * alpha / (2 * (c1 * c2)))");
    apply arith;
    apply (subgoal_tac "1 = natfloor 1");
    apply (erule ssubst);
    apply (rule natfloor_mono);
    apply (subst pos_le_divide_eq); 
    apply simp;
    apply (rule mult_pos);
    apply (insert c1_gt_1, arith);
    apply (insert c2_gt_1, arith);
    apply simp;
    apply (subst pos_divide_le_eq [THEN sym]);
    apply (rule alpha_gt_0);
    apply (subst exp_le_cancel_iff [THEN sym]);
    apply (subgoal_tac "exp (ln x) = x");
    apply (erule ssubst);
    apply (rule x_ge_blah3);
    apply (subst exp_ln_iff);
    apply (insert x_gt_1, arith);
    apply simp;
    done;
  also have "(1 / 4) * (lambda * ?eps / 2) * (ln x) * 
      ((1 / 4) * (ln x / ln ?K)) <= ...";
    apply (rule mult_mono);
    apply (rule mult_right_mono);
    apply (rule mult_left_mono);
    apply (subgoal_tac "1 - 1 / (1 + lambda * ?eps) = lambda * ?eps / 
        (1 + lambda * ?eps)");
    apply (erule ssubst);
    apply (rule divide_left_mono);
    apply (subgoal_tac "lambda * ?eps <= 1 * 1");
    apply simp;
    apply (rule mult_mono);
    apply (rule order_less_imp_le, rule lambda_le_1);
    apply (rule order_less_imp_le, rule eps_lt_1);
    apply force;
    apply (rule order_less_imp_le, rule eps_gt_0);
    apply (rule order_less_imp_le);
    apply (rule mult_pos);
    apply (rule lambda_gt_0);
    apply (rule eps_gt_0);
    apply (rule mult_pos);
    apply force;
    apply (rule pos_plus_pos);
    apply force;
    apply (rule mult_pos);
    apply (rule lambda_gt_0);
    apply (rule eps_gt_0);
    apply (rule lemma_divide_rearrange);
    apply (rule less_imp_neq [THEN not_sym]);
    apply (rule pos_plus_pos);
    apply force;
    apply (rule mult_pos);
    apply (rule lambda_gt_0);
    apply (rule eps_gt_0);
    apply simp;
    apply force;
    apply (rule ln_ge_zero);
    apply (insert x_gt_1, arith);
    apply (rule order_trans);
    apply (subgoal_tac "1 / 4  * (ln x / ln (exp (c1 / (alpha / c2)))) <=
      ((ln x / (2 * ln ?K)) - (ln x1 / ln ?K) - 3)");
    apply assumption;
    prefer 2;
    apply (subgoal_tac "(ln x / (2 * ln ?K)) <= 
        real (natfloor (ln x / (2 * ln ?K))) + 1");
    apply (subgoal_tac "real (natfloor (ln x1 / ln ?K)) <= 
        (ln x1 / ln ?K)");
    apply arith;
    apply (rule real_natfloor_le);
    apply simp;
    apply (rule real_ge_zero_div_gt_zero);
    apply (rule nonneg_times_nonneg);
    apply (rule ln_ge_zero);
    apply (rule x1_ge_1);
    apply (rule order_less_imp_le);
    apply (rule alpha_gt_0);
    apply (rule mult_pos);
    apply (insert c1_gt_1, arith);
    apply (insert c2_gt_1, arith);
    apply (rule real_natfloor_plus_one_ge);
    prefer 2;
    apply (rule nonneg_times_nonneg);
    apply (rule nonneg_times_nonneg);
    apply force;
    apply simp;
    apply (subst pos_divide_le_eq);
    apply (rule pos_plus_pos);
    apply force;
    apply (rule pos_div_pos);
    apply (rule mult_pos);
    apply (rule lambda_gt_0);
    apply (rule alpha_gt_0)
    apply (insert c2_gt_1, arith)
    apply simp;
    apply (rule order_less_imp_le);
    apply (rule pos_div_pos);
    apply (rule mult_pos);
    apply (rule lambda_gt_0);
    apply (rule alpha_gt_0);
    apply arith;
    apply (rule ln_ge_zero);
    apply (rule order_less_imp_le);
    apply (rule x_gt_1);
    apply (simp only: diff_minus);
    apply (subgoal_tac "1 / 4 = 1 / 2 + - (1 / 8) + - (1 / 8)");
    apply (erule ssubst);
    apply (subst left_distrib);
    apply (subst left_distrib);
    apply (rule add_mono);
    apply (rule add_mono);
    apply simp;
    apply (simp add: compare_rls);
    apply (subst times_divide_eq_right [THEN sym]);
    apply (subst pos_divide_le_eq [THEN sym]);
    apply (rule pos_div_pos);
    apply (rule alpha_gt_0);
    apply (rule mult_pos);
    apply force;
    apply (rule mult_pos);
    apply arith;
    apply arith;
    apply (subgoal_tac "alpha ~= 0");
    apply simp;
    apply (subst mult_commute);
    apply (subst ln_pwr [THEN sym]);
    apply (insert x1_ge_1, arith);
    apply force;
    apply (subst ln_le_cancel_iff);
    apply force;
    apply (insert x_gt_1, force);
    apply (rule x_ge_blah4);
    apply (rule less_imp_neq [THEN not_sym]);
    apply (rule alpha_gt_0);
    apply (simp add: compare_rls);
    apply (subst times_divide_eq_right [THEN sym]);
    apply (subst pos_divide_le_eq [THEN sym]);
    apply (rule pos_div_pos);
    apply (rule alpha_gt_0);
    apply (rule mult_pos);
    apply force;
    apply (rule mult_pos);
    apply arith;
    apply arith;
    apply (subst exp_le_cancel_iff [THEN sym]);
    apply (subgoal_tac "exp (ln x) = x"); 
    apply (erule ssubst);
    apply (rule x_ge_blah5);
    apply (subst exp_ln_iff);
    apply arith;
    apply simp;
    apply simp;
    apply (rule real_ge_zero_div_gt_zero);
    apply (rule nonneg_times_nonneg);
    apply (rule ln_ge_zero);
    apply arith;
    apply (rule order_less_imp_le);
    apply (rule alpha_gt_0);
    apply (rule mult_pos);
    apply force;
    apply (rule mult_pos);
    apply arith;
    apply arith;
    done;
  also (order_trans2) have "(1 / 4) * (lambda * ?eps / 2) * (ln x) * 
      ((1 / 4) * (ln x / ln ?K)) = 
    (lambda * alpha^2 * (ln x)^2) / (32 * c1 * c2^2)";
    by (simp add: mult_ac power2_eq_square);
  finally; show "lambda / (32 * c1 * c2 ^ 2) * alpha ^ 2 * ln x ^ 2 <= 
      (∑ n:?S. ln (real n) / real n)";
    by (simp add: ring_eq_simps);
qed;qed;qed;qed;qed;qed;qed;qed;qed;

lemma PNT4: "1 < (c2::real) ==> EX C. 0 < C & (ALL alpha1 x1. 0 < alpha1 -->
    alpha1 < c2 --> (ALL x. x1 <= x --> abs (R x) <= alpha1 * x) -->
    (EX x2. (ALL x. x2 <= x --> abs (R x) <= (alpha1 - C * alpha1^3) * x)))";
proof -;
  assume c2_gt_1: "1 < (c2::real)"; 
  have "EX C. 0 < C & (ALL alpha.
    0 < alpha --> alpha < c2 --> 
      (EX xlarge. ALL x. xlarge <= x -->
        (EX S. S <= {1..natfloor x} & 
          (ALL n:S. abs(R(x / real n)) <= (alpha / c2) * (x / real n)) & 
            C * alpha^2 * (ln x)^2 
              <= (∑ n:S. ln(real n) / (real n)))))";
    apply (rule PNT4_aux1);
    apply (rule prems);
    done;
  then obtain C where C_gt_0: "0 < C" and C': "(ALL alpha.
    0 < alpha --> alpha < c2 --> 
      (EX xlarge. ALL x. xlarge <= x -->
        (EX S. S <= {1..natfloor x} & 
          (ALL n:S. abs(R(x / real n)) <= (alpha / c2) * (x / real n)) & 
            C * alpha^2 * (ln x)^2 
              <= (∑ n:S. ln(real n) / (real n)))))"; by blast;
  from PNT3 obtain G where G: "ALL x x2 S eps alpha. 
    0 < eps --> 0 < alpha --> alpha < c2 -->
      2 <= x2 --> exp 1 <= x2 --> x2 <= x -->
        (ALL x. x2 <= x --> abs(R x) <= alpha * x) -->
          S <= {1..natfloor x} -->
            (ALL n:S. abs(R(x / real n)) <= eps * (x / real n)) -->
        abs (R x)
          <= alpha * x -
            2 * (alpha - eps) * x * 
              (∑n:S. ln (real n) / real n) / ln x ^ 2 +
                G * x * ln x2 / ln x";..;
  let ?C = "(1 - 1 / c2) * C";
  show ?thesis;
proof;
  show "0 < ?C & (ALL alpha1 x1. 0 < alpha1 -->
    alpha1 < c2 --> (ALL x. x1 <= x --> abs (R x) <= alpha1 * x) -->
    (EX x2. (ALL x. x2 <= x --> abs (R x) <= (alpha1 - ?C * alpha1^3) * x)))";
proof;
  show "0 < ?C";
    apply (rule mult_pos);
    apply simp;
    apply (subst pos_divide_less_eq);
    apply (insert c2_gt_1, arith);
    apply simp;
    apply (rule C_gt_0);
    done;
  next show "(ALL alpha1 x1. 0 < alpha1 -->
    alpha1 < c2 --> (ALL x. x1 <= x --> abs (R x) <= alpha1 * x) -->
    (EX x2. (ALL x. x2 <= x --> abs (R x) <= (alpha1 - ?C * alpha1^3) * x)))";
proof (clarify);
  fix alpha1::"real";
  fix x1::"real";
  assume alpha1_gt_0: "0 < alpha1"
  assume alpha1_lt_c2: "alpha1 < c2";
  assume x1_good: "ALL x. x1 <= x --> abs (R x) <= alpha1 * x";
  have "EX xlarge. ALL x. xlarge <= x -->
    (EX S. S <= {1..natfloor x} & 
      (ALL n:S. abs(R(x / real n)) <= (alpha1 / c2) * (x / real n)) & 
        C * alpha1^2 * (ln x)^2 
          <= (∑ n:S. ln(real n) / (real n)))";
    by (insert C' alpha1_gt_0 alpha1_lt_c2, blast);
  then obtain xlarge where xlarge: "ALL x. xlarge <= x -->
    (EX S. S <= {1..natfloor x} & 
      (ALL n:S. abs(R(x / real n)) <= (alpha1 / c2) * (x / real n)) & 
        C * alpha1^2 * (ln x)^2 
          <= (∑ n:S. ln(real n) / (real n)))";..;
  let ?x1' = "max x1 (max 2 (exp 1))";
  have x1prime_ge_x1: "x1 <= ?x1'"; by arith;
  have x1prime_ge_2: "2 <= ?x1'"; by arith;
  have x1prime_ge_exp1: "exp 1 <= ?x1'"; by arith;
  let ?messy_term = "exp (G * ln ?x1' /
             (C * ((1 - 1 / c2) * alpha1 ^ 3)))";
  let ?x2 = "max xlarge (max (max (max 2 (exp 1)) ?x1') ?messy_term)";
  show "EX x2. ALL x. x2 <= x --> abs (R x) <= (alpha1 - ?C * alpha1 ^ 3) * x";
proof;
  show "ALL x. ?x2 <= x --> abs (R x) <= (alpha1 - ?C * alpha1 ^ 3) * x";
proof (clarify);  
  fix x::"real";
  assume x_ge_x2: "?x2 <= x"; 
  have x_ge_xlarge: "xlarge <= x";
    apply (rule order_trans);
    prefer 2;
    apply (rule x_ge_x2);
    apply (rule le_maxI1);
    done;
  have x2_ge_2: "2 <= ?x2";
    by arith;
  have x2_ge_exp1: "exp 1 <= ?x2";
    by arith;
  have x2_ge_x1: "x1 <= ?x2";
    by arith;
  have x2_ge_x1prime: "?x1' <= ?x2";
    apply auto;
    apply arith;
    apply arith;
    apply arith;
    done;
  have messy_term: "?messy_term <= ?x2";
    apply arith;
    done;
  have "EX S. S <= {1..natfloor x} & 
      (ALL n:S. abs(R(x / real n)) <= (alpha1 / c2) * (x / real n)) & 
        C * alpha1^2 * (ln x)^2 
          <= (∑ n:S. ln(real n) / (real n))";
    apply (insert xlarge);
    apply (drule_tac x = x in spec);
    apply (insert x_ge_xlarge);
    apply clarify;
    done;
  then obtain S where S1: "S <= {1..natfloor x}" and 
    S2: "(ALL n:S. abs(R(x / real n)) <= (alpha1 / c2) * (x / real n))" and
    S3: "C * alpha1^2 * (ln x)^2 <= (∑ n:S. ln(real n) / (real n))";
      by blast;
  have "abs (R x) <= alpha1 * x -
    2 * (alpha1 - alpha1 / c2) * x * 
      (∑n:S. ln (real n) / real n) / ln x ^ 2 +
        G * x * ln ?x1' / ln x";
    apply (insert G);
    apply (drule_tac x = x in spec);
    apply (drule_tac x = ?x1' in spec);
    apply (drule_tac x = S in spec);
    apply (drule_tac x = "(alpha1 / c2)" in spec); 
    apply (drule_tac x = alpha1 in spec);
    apply (drule mp);
    apply (rule pos_div_pos);
    apply (rule alpha1_gt_0);
    apply (insert c2_gt_1, arith);
    apply (drule mp);
    apply (rule alpha1_gt_0);
    apply (drule mp);
    apply (rule alpha1_lt_c2);
    apply (drule mp);
    apply (rule x1prime_ge_2);
    apply (drule mp);
    apply (rule x1prime_ge_exp1);
    apply (drule mp);
    apply (rule order_trans);
    apply (rule x2_ge_x1prime);
    apply (rule x_ge_x2);
    apply (drule mp);
    apply (rule allI);
    apply (rename_tac xa);
    apply (rule impI);
    apply (insert x1_good);
    apply (drule_tac x = xa in spec);
    apply (drule mp);
    apply arith;
    apply assumption;
    apply (drule mp);
    apply (rule S1);
    apply (drule mp);
    apply (rule S2);
    apply assumption;
    done;
  also have "... <= alpha1 * x -
        2 * (alpha1 - alpha1 / c2) * x * 
          (C * alpha1 ^ 2 * ln x ^ 2) / ln x ^ 2 +
        G * x * ln (?x1') / ln x";
    apply (subst diff_minus)+;
    apply (rule add_right_mono);
    apply (rule add_left_mono);
    apply (rule le_imp_neg_le);
    apply (rule real_div_pos_le_mono);
    apply (rule mult_left_mono);
    apply (rule S3);
    apply (rule nonneg_times_nonneg);
    apply (rule nonneg_times_nonneg);
    apply force;
    apply simp;
    apply (subst pos_divide_le_eq);
    apply (insert c2_gt_1, arith);
    apply (subgoal_tac "alpha1 * 1 <= alpha1 * c2");
    apply simp;
    apply (rule mult_left_mono);
    apply (erule order_less_imp_le);
    apply (insert alpha1_gt_0, arith);
    apply (insert x_ge_x2 x2_ge_2, arith);
    apply force;
    done;
  also have "... = x * (alpha1 - 2 * alpha1^3 * (1 - 1 / c2) * C + 
      (G * ln ?x1' / ln x))";
    apply (subgoal_tac "ln x ~= 0");
    apply (simp add: ring_eq_simps power3_eq_cube power2_eq_square
      add_divide_distrib diff_divide_distrib);
    apply (rule less_imp_neq [THEN not_sym]);
    apply (rule ln_gt_zero);
    apply (insert x_ge_x2 x2_ge_2, arith);
    done;
  also have "... <= x * (alpha1 - 2 * alpha1^3 * (1 - 1 / c2) * C + 
      alpha1^3 * (1 - 1 / c2) * C)";
    apply (rule mult_left_mono);
    apply simp;
    apply (subst pos_divide_le_eq);
    apply (rule ln_gt_zero);
    apply (insert x_ge_x2 x2_ge_2, arith);
    apply (subst mult_commute);
    apply (subst pos_divide_le_eq [THEN sym]);
    apply (rule mult_pos);
    apply (rule C_gt_0);
    apply (rule mult_pos);
    apply simp;
    apply (subst pos_divide_less_eq);
    apply (insert c2_gt_1, arith);
    apply simp;
    apply (subst power3_eq_cube);
    apply (rule mult_pos);
    apply (rule mult_pos);
    apply (rule alpha1_gt_0)+;
    apply (subst exp_le_cancel_iff [THEN sym]);
    apply (subgoal_tac "exp (ln x) = x");
    apply (erule ssubst);
    apply (rule order_trans);
    apply (rule messy_term);
    apply (rule x_ge_x2);
    apply (subst exp_ln_iff);
    apply (insert x_ge_x2 x2_ge_2, arith);
    apply arith;
    done;
  also have "... = x * (alpha1 - alpha1 ^ 3 * (1 - 1 / c2) * C)"; 
    by simp;
  finally show "abs (R x) <= (alpha1 - (1 - 1 / c2) * C * alpha1 ^ 3) * x";
    by (simp add: ring_eq_simps);
qed;qed;qed;qed;qed;qed;

constdefs
  PNT_alpha0::"real"
  "PNT_alpha0 == (SOME C. 0 < C & (ALL x. 0 <= x --> abs (R x) <= C * x))";

lemma PNT_alpha0: "0 < PNT_alpha0 & 
    (ALL x. 0 <= x --> abs (R x) <= PNT_alpha0 * x)";
  apply (unfold PNT_alpha0_def);
  apply (rule someI_ex);
  apply (rule PNT3_aux2a);
done;

constdefs
  PNT_C::"real"
  "PNT_C == SOME C. 0 < C & (ALL alpha1 x1. 0 < alpha1 -->
    alpha1 < max (PNT_alpha0 + 1) 2 --> 
    (ALL x. x1 <= x --> abs (R x) <= alpha1 * x) -->
    (EX x2. (ALL x. x2 <= x --> abs (R x) <= (alpha1 - C * alpha1^3) * x)))";

lemma PNT_C: "0 < PNT_C & (ALL alpha1 x1. 0 < alpha1 -->
    alpha1 < max (PNT_alpha0 + 1) 2 --> 
    (ALL x. x1 <= x --> abs (R x) <= alpha1 * x) -->
    (EX x2. (ALL x. x2 <= x --> abs (R x) <= 
      (alpha1 - PNT_C * alpha1^3) * x)))";
  apply (unfold PNT_C_def);
  apply (rule someI_ex);
  apply (rule PNT4);
  apply arith;
done;

consts
  PNT_alpha :: "nat => real"

primrec
  PNT_alpha_0: "PNT_alpha 0 = PNT_alpha0"
  PNT_alpha_Suc: "PNT_alpha (Suc n) = PNT_alpha n - PNT_C * (PNT_alpha n)^3";

lemma PNT5_aux1: "0 <= PNT_alpha n & PNT_alpha (Suc n) <= PNT_alpha n & 
    PNT_alpha n < max (PNT_alpha0 + 1) 2 & 
    (EX x2. (ALL x. x2 <= x --> abs (R x) <= 
      PNT_alpha n * x))";
  apply (induct_tac n);
  apply (rule conjI);
  apply (rule order_less_imp_le);
  apply (force simp add: PNT_alpha0);
  apply (rule conjI);
  apply simp;
  apply (rule nonneg_times_nonneg);
  apply (rule order_less_imp_le);
  apply (force simp add: PNT_C);
  apply (subgoal_tac "0 <= PNT_alpha0");
  apply (subst power3_eq_cube);
  apply (rule nonneg_times_nonneg)+;
  apply assumption+;
  apply (rule order_less_imp_le);
  apply (force simp add: PNT_alpha0);
  apply (rule conjI);
  apply (rule order_less_le_trans);
  prefer 2;
  apply (rule le_maxI1);
  apply simp;
  apply (rule_tac x = 1 in exI);
  apply simp;
  apply (force simp add: PNT_alpha0);
  apply (subgoal_tac "(EX x2. ALL x. x2 <= x --> 
      abs (R x) <= PNT_alpha (Suc n) * x)");
  apply (subgoal_tac "0 <= PNT_alpha (Suc n)");
  apply (rule conjI);
  apply assumption;
  apply (rule conjI);
  apply (subst PNT_alpha_Suc);back;
  apply (simp del: PNT_alpha_Suc);
  apply (rule nonneg_times_nonneg);
  apply (rule order_less_imp_le);
  apply (force simp add: PNT_C);
  apply (subst power3_eq_cube);
  apply (rule nonneg_times_nonneg)+;
  apply assumption+;
  apply (rule conjI);
  apply (rule order_le_less_trans);
  apply clarify;
  apply assumption;
  apply force;
  apply assumption;
  apply clarify;
  apply (drule_tac x = "max x2 1" in spec);
  apply (drule mp);
  apply arith;
  apply (rule order_trans);
  apply (subgoal_tac "0 <= abs (R (max x2 1)) / (max x2 1)"); 
  apply assumption;back;
  apply (rule real_ge_zero_div_gt_zero);
  apply force;
  apply arith;
  apply (subst pos_divide_le_eq);
  apply arith;
  apply assumption;
  apply simp;
  apply (case_tac "PNT_alpha n = 0");
  apply clarify;
  apply (simp add: power3_eq_cube);
  apply (rule_tac x = x2 in exI);
  apply assumption;
  apply (insert PNT_C);
  apply clarify;
  apply (drule_tac x = "PNT_alpha n" in spec);
  apply (drule_tac x = x2 in spec);back;
  apply (subgoal_tac "0 < PNT_alpha n");
  apply clarify;
  apply arith;
done;

lemma PNT5_aux2: "convergent PNT_alpha";
  apply (rule Bseq_monoseq_convergent);
  apply (unfold Bseq_def);
  apply (insert PNT5_aux1);
  apply (rule_tac x = "max (PNT_alpha0 + 1) 2" in exI);
  apply (rule conjI);
  apply arith;
  apply (rule allI);
  apply (subst abs_nonneg);
  apply force;
  apply (rule order_less_imp_le);
  apply force;
  apply (subst monoseq_Suc);
  apply (rule disjI2);
  apply force;
done;

lemma PNT5_aux3: "EX L. PNT_alpha ----> L";
  apply (insert PNT5_aux2);
  apply (unfold convergent_def);
  apply assumption;
done;

lemma PNT5_aux4: "PNT_alpha ----> L ==> L = 0";
proof -;
  assume a: "PNT_alpha ----> L"; 
  then have b: "(%n. PNT_alpha (Suc n)) ----> L";
    by (rule LIMSEQ_Suc);
  have c: "(%n. PNT_alpha n - 
    PNT_C * PNT_alpha n * PNT_alpha n * PNT_alpha n) ---->
      L - PNT_C * L * L * L";
    apply (rule LIMSEQ_diff);
    apply (rule a);
    apply (rule LIMSEQ_mult)+;
    apply (rule LIMSEQ_const);
    apply (rule a)+;
    done;
  also have "(%n. PNT_alpha n - 
    PNT_C * PNT_alpha n * PNT_alpha n * PNT_alpha n) = 
    (%n. PNT_alpha (Suc n))";
    by (rule ext, simp add: power3_eq_cube mult_ac);
  finally have c: "(%n. PNT_alpha (Suc n)) ----> L - PNT_C * L * L * L";.;
  then have "L - PNT_C * L * L * L = L";
    apply (rule LIMSEQ_unique);
    apply (rule b);
    done;
  then show "L = 0";
    apply (subgoal_tac "PNT_C ~= 0"); 
    apply simp;
    apply (rule less_imp_neq [THEN not_sym]);
    apply (insert PNT_C, force);
    done;
qed;

lemma PNT5_aux5: "PNT_alpha ----> 0";
  by (insert PNT5_aux3 PNT5_aux4, auto);

lemma PNT5: "ALL eps. (0 < eps -->
     (EX z. ALL x. (z <= x --> abs (R x) < eps * x)))";
proof (clarify);
  fix eps::"real";
  assume "0 < eps";
  have "EX n. PNT_alpha n < eps";
    apply (insert PNT5_aux5);
    apply (unfold LIMSEQ_def);
    apply (drule_tac x = eps in spec);
    apply (insert prems, clarify);
    apply (rule_tac x = no in exI);
    apply (drule_tac x = no in spec);
    apply (subgoal_tac "abs(PNT_alpha no) = PNT_alpha no");
    apply auto;
    apply (rule abs_nonneg);
    apply (insert PNT5_aux1, force);
    done;
  then obtain n where n: "PNT_alpha n < eps";..;
  have "EX z. (ALL x. z <= x --> abs (R x) <= 
      PNT_alpha n * x)";
    by (insert PNT5_aux1, force);
  thus "EX z. ALL x. (z <= x --> abs (R x) < eps * x)";
    apply clarify;
    apply (rule_tac x = "max z 1" in exI);
    apply clarify;
    apply (drule_tac x = x in spec);
    apply (subgoal_tac "z <= x");
    apply clarify;
    apply (erule order_le_less_trans);
    apply (rule mult_strict_right_mono);
    apply (rule n);
    apply arith;
    apply arith;
    done;
qed;

lemma PrimeNumberTheorem1: "(%x. psi x / (real x)) ----> 1";
  apply (rule R_bound_imp_PNT);
  apply (rule PNT5);
done;

lemma PrimeNumberTheorem2: "(%x. theta x / (real x)) ----> 1";
  apply (rule psi_theta_lim4);
  apply (rule PrimeNumberTheorem1);
done;

lemma PrimeNumberTheorem: "(%x. pi x * ln (real x) / (real x)) ----> 1";
  apply (rule theta_limit_imp_pi_limit);
  apply (rule PrimeNumberTheorem2);
done;

end;

lemma PNT1_aux1:

  [| 0 < C; 0 ≤ D |]
  ==> ∃C0. ∀eps. 0 < eps -->
                 eps < 1 -->
                 (∀K. exp (C0 / eps) < K -->
                      2 < KD < ln KC / (ln K - D) < eps)

lemma PNT1_aux2:

C. ∀x. ¦ln (¦x¦ + 1) - (∑i = 1..natfloor ¦x¦ + 1. 1 / real i)¦ < C

lemma PNT1_aux3:

C. ∀x. 1 ≤ x --> ¦ln x - (∑i = 1..natfloor x. 1 / real i)¦ < C

lemma PNT1_aux4:

C. ∀x. 1 ≤ x --> ¦ln x - (∑i = 1..natfloor x. 1 / real (i + 1))¦ < C

lemma PNT1_aux5:

D. ∀x K. 1 ≤ x -->
            1 ≤ K -->
            ¦ln K -
             (∑n | natfloor x < nn ≤ natfloor (K * x). 1 / real (n + 1))¦
            ≤ D

lemma PNT1_aux6:

D. ∀x K. 1 ≤ x -->
            1 ≤ K -->
            ln K - D
            ≤ (∑n | natfloor x < nn ≤ natfloor (K * x). 1 / real (n + 1))

lemma PNT1_aux7:

  0 < C
  ==> ∃C0. ∀eps. 0 < eps -->
                 eps < 1 -->
                 (∀K x. 1 ≤ x -->
                        exp (C0 / eps) < K -->
                        2 < KC / (∑n | natfloor x < nn ≤ natfloor (K * x).
                                1 / real (n + 1))
                        < eps)

lemma PNT1_aux8:

  (0 ≤ x) ≠ (0 ≤ y) ==> ¦x¦ ≤ ¦y - x¦

lemma PNT1_aux9:

k<j. (0 ≤ f (i + k)) = (0 ≤ f (i + (k + 1)))
  ==> (∀kj. 0 ≤ f (i + k)) ∨ (∀kj. f (i + k) < 0)

lemma PNT1_aux10:

  [| ij; ∀n. i < nnj --> (0 ≤ f n) = (0 ≤ f (n + 1)) |]
  ==> (∀n. i < nnj --> 0 ≤ f n) ∨ (∀n. i < nnj --> f n < 0)

lemma PNT1_aux11:

C. ∀i. 1 ≤ i --> ¦∑n = 1..i. R (real n) / (real n * real (n + 1))¦ ≤ C

lemma PNT1_aux12:

C. ∀i j. 1 ≤ i -->
            ij -->
            ¦∑n | i < nnj. R (real n) / (real n * real (n + 1))¦ < C

lemma PNT1:

C0. ∀eps. 0 < eps -->
             eps < 1 -->
             (∃x0. ∀K x. exp (C0 / eps) < K -->
                         x0 < x -->
                         (∃n. natfloor x < nn ≤ natfloor (K * x) ∧ ¦R (real n) / real n¦ < eps))

lemma PNT1a:

C0. ∀eps. 0 < eps -->
             eps < 1 -->
             (∃x0. ∀K x. exp (C0 / eps) < K -->
                         x0 < x -->
                         (∃n. x < real n ∧
                              real nK * x ∧ ¦R (real n) / real n¦ < eps))

lemma PNT2_aux1:

C. ∀x. 1 ≤ x -->
          ¦psi (natfloor x) * ln x +
           (∑d = 1..natfloor x. Lambda d * psi (natfloor x div d)) -
           2 * x * ln x¦
          ≤ C * x

lemma PNT2_aux2:

C. ∀x y. 1 ≤ y -->
            yx -->
            psi (natfloor x) * ln x - psi (natfloor y) * ln y
            ≤ 2 * x * ln x - 2 * y * ln y + C * x

lemma PNT2_aux3:

E. ∀x y. 1 ≤ y -->
            y < x -->
            xD * y -->
            psi (natfloor x) - psi (natfloor y) ≤ 2 * (x - y) + E * (x / ln x)

lemma PNT2_aux4:

C. ∀x. ¦R x / x¦ < C

lemma PNT2_aux5:

  0 < eps ==> ∃x. ∀y. x < y --> 1 / ln y < eps

lemma PNT2:

lambda C1.
     0 < lambdalambda < 1 ∧
     (∀eps. 0 < eps -->
            eps < 1 -->
            (∃x1. ∀K x. exp (C1 / eps) < K -->
                        x1 < x -->
                        (∃xstar.
                            x < xstar ∧
                            (1 + lambda * eps) * xstar < K * x ∧
                            (∀u. xstaruu ≤ (1 + lambda * eps) * xstar -->
                                 ¦R u¦ < eps * u))))

lemma PNT2a:

lambda C1.
     0 < lambdalambda < 1 ∧
     1 ≤ C1 ∧
     (∀eps. 0 < eps -->
            eps < 1 -->
            (∃x1. 1 ≤ x1 ∧
                  (∀K x. exp (C1 / eps) ≤ K -->
                         x1x -->
                         (∃xstar.
                             x < xstar ∧
                             (1 + lambda * eps) * xstar < K * x ∧
                             (∀u. xstaruu ≤ (1 + lambda * eps) * xstar -->
                                  ¦R u¦ < eps * u)))))

lemma PNT3_aux1:

C. ∀x. 1 ≤ x -->
          ¦R x¦ * (ln x)²
          ≤ 2 * (∑n = 1..natfloor x. ¦R (x / real n)¦ * ln (real n)) +
            C * ¦x * (1 + ln x

lemma PNT3_aux1a:

C. 0 ≤ C ∧
      (∀x. 2 ≤ x -->
           ¦R x¦ * (ln x)²
           ≤ 2 * (∑n = 1..natfloor x. ¦R (x / real n)¦ * ln (real n)) +
             C * x * ln x)

lemma PNT3_aux2:

C. ∀x. 0 ≤ x --> ¦R x¦ ≤ C * x

lemma PNT3_aux2a:

C. 0 < C ∧ (∀x. 0 ≤ x --> ¦R x¦ ≤ C * x)

lemma PNT3_aux3:

C. ∀x. 1 ≤ x --> ¦(∑i = 1..natfloor x. ln (real i) / real i) - (ln x)² / 2¦ ≤ C

lemma PNT3_aux4:

C. ∀x x2. 1 ≤ x2 -->
             x2x -->
             (∑n = natfloor (x / x2) + 1..natfloor x. ln (real n) / real n)
             ≤ ln x2 * ln x + C

lemma PNT3_aux5:

C. 0 ≤ C ∧
      (∀x. 1 ≤ x --> (∑i = 1..natfloor x. ln (real i) / real i) ≤ (ln x)² / 2 + C)

lemma PNT3:

G. ∀x x2 S eps alpha.
         0 < eps -->
         0 < alpha -->
         alpha < c -->
         2 ≤ x2 -->
         exp 1 ≤ x2 -->
         x2x -->
         (∀x. x2x --> ¦R x¦ ≤ alpha * x) -->
         S ⊆ {1..natfloor x} -->
         (∀nS. ¦R (x / real n)¦ ≤ eps * (x / real n)) -->
         ¦R x¦
         ≤ alpha * x -
           2 * (alpha - eps) * x * (∑nS. ln (real n) / real n) / (ln x)² +
           G * x * ln x2 / ln x

lemma PNT4_aux1:

  1 < c2
  ==> ∃C. 0 < C ∧
          (∀alpha.
              0 < alpha -->
              alpha < c2 -->
              (∃xlarge.
                  ∀x. xlargex -->
                      (∃S≤{1..natfloor x}.
                          (∀nS. ¦R (x / real n)¦ ≤ alpha / c2 * (x / real n)) ∧
                          C * alpha² * (ln x)² ≤ (∑nS. ln (real n) / real n))))

lemma PNT4:

  1 < c2
  ==> ∃C. 0 < C ∧
          (∀alpha1 x1.
              0 < alpha1 -->
              alpha1 < c2 -->
              (∀x. x1x --> ¦R x¦ ≤ alpha1 * x) -->
              (∃x2. ∀x. x2x --> ¦R x¦ ≤ (alpha1 - C * alpha1 ^ 3) * x))

lemma PNT_alpha0:

  0 < PNT_alpha0 ∧ (∀x. 0 ≤ x --> ¦R x¦ ≤ PNT_alpha0 * x)

lemma PNT_C:

  0 < PNT_C ∧
  (∀alpha1 x1.
      0 < alpha1 -->
      alpha1 < max (PNT_alpha0 + 1) 2 -->
      (∀x. x1x --> ¦R x¦ ≤ alpha1 * x) -->
      (∃x2. ∀x. x2x --> ¦R x¦ ≤ (alpha1 - PNT_C * alpha1 ^ 3) * x))

lemma PNT5_aux1:

  0 ≤ PNT_alpha n ∧
  PNT_alpha (Suc n) ≤ PNT_alpha n ∧
  PNT_alpha n < max (PNT_alpha0 + 1) 2 ∧
  (∃x2. ∀x. x2x --> ¦R x¦ ≤ PNT_alpha n * x)

lemma PNT5_aux2:

  convergent PNT_alpha

lemma PNT5_aux3:

L. PNT_alpha ----> L

lemma PNT5_aux4:

  PNT_alpha ----> L ==> L = 0

lemma PNT5_aux5:

  PNT_alpha ----> 0

lemma PNT5:

eps. 0 < eps --> (∃z. ∀x. zx --> ¦R x¦ < eps * x)

lemma PrimeNumberTheorem1:

  (%x. psi x / real x) ----> 1

lemma PrimeNumberTheorem2:

  (%x. theta x / real x) ----> 1

lemma PrimeNumberTheorem:

  (%x. Chebyshev1.pi x * ln (real x) / real x) ----> 1