# Theory Chebyshev1

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

theory Chebyshev1 = Complex + PrimeFactorsList + RealLib:

```(*  Title:      Chebyshev1.thy
Author:     Paul Raff and Jeremy Avigad
*)

theory Chebyshev1 = Complex + PrimeFactorsList + RealLib:;

consts
lprime ::      "nat => real"
Lambda ::      "nat => real"
theta ::       "nat => real"
psi ::         "nat => real"
char_prime ::  "nat => real"
pi         ::  "nat => real"
nmult      ::  "nat => nat => nat"

defs
lprime_def: "lprime(x) == (if (x : prime)
then (ln(real(x)))
else 0)"
theta_def:  "theta(x) == sumr 0 (x+1) lprime"

Lambda_def: "Lambda(x) == if (EX p a. (p:prime) & (p^a = x) & 0 < a)
then ln(real(THE p. (EX a. (p:prime) & (p^a = x))))
else 0"
psi_def:    "psi(x) == sumr 0 (x+1) Lambda"

char_prime_def: "char_prime(x) == if (x:prime)
then 1
else 0"
pi_def: "pi(x) == real(card({y. y<=x & y:prime}))"

nmult_def: "nmult x y == multiplicity (int x) (int y)";

locale l =
fixes x::"nat"
and  A::"nat set"
and  B::"nat set"
and  C::"(nat*nat) set"
and  D::"(nat*nat) set"
and  E::"(nat*nat) set"
and  F::"nat set"
and  f::"nat*nat => nat"
and  g:: "nat => (nat*nat)"
and  G::"nat set"
and  H::"nat => nat set"
and  J::"nat set"

defines
A_def:"A == {y. (y:{0..x} & (EX p a. (p:prime & 0<a & p^a=y)))}"
and B_def:"B == {y. (y:{0..x} & ~(EX p a. (p:prime & 0<a & p^a=y)))}"
and C_def:"C == {(p,a). (p:prime & 0<a & p^a:{0..x})}"
and D_def:"D == {(p,a). (p:prime & a = 1 & p^a:{0..x})}"
and E_def:"E == {(p,a). (p:prime & 1 < a & p^a:{0..x})}"
and F_def:"F == {p. p:prime & p:{0..x}}"
and f_def:"f y == (fst y)^(snd y)"
and g_def:"g z == (z,1)"
and G_def:"G == {d. 0 < d & d dvd x}"
and H_def:"H(p) == {y. y:{0..x} & (EX a. (0 < a & p^a = y))}"
and J_def:"J == {p. p : prime & p dvd x}";

subsection {* Miscellaneaous *}

lemma prime_prop2: "a:prime ==> b:prime ==> (0<n) ==> a dvd b^n ==> a=b";
apply (frule prime_dvd_power);
apply (assumption);

lemma dvd_self_exp [rule_format]: "0 < n --> (m::nat) dvd m^n";
apply (induct_tac n);
by auto;

lemma prime_prop: "a:prime ==> b:prime ==> 0<c ==> 0<d ==> a^c = b^d ==> a=b";
apply (subgoal_tac "a dvd b^d");
apply (erule prime_prop2);
prefer 3;
apply (assumption)+;
apply (subgoal_tac "a dvd a^c");
apply simp;
by (erule dvd_self_exp);

lemma  power_lemma [rule_format]:  "(1::nat) < a --> (0::nat) < c --> 1 < a^c";
apply (induct_tac c);
apply force;
apply auto;
apply (subgoal_tac "1 < a * a^n");
apply force;
apply (subgoal_tac "1 < a");
apply (simp only: power_gt1_lemma);
apply auto;
done;

lemma prime_prop_lzero: "a:prime ==> b:prime ==> 0<c ==> a^c = b^d ==> a=b";
apply (case_tac "0=d");
apply auto;
apply (subgoal_tac "1 < a");
apply (subgoal_tac "1 < a^c");
apply (force);
apply (rule power_lemma);
apply force;
apply force;
apply (subgoal_tac "2 <= a");
apply force;
apply (rule prime_ge_2);
apply force;
apply (rule prime_prop);
apply auto;
done;

lemma prime_prop_rzero: "a:prime ==> b:prime ==> 0<d ==> a^c = b^d ==> a=b";
apply (subgoal_tac "b^d = a^c");
apply (subgoal_tac "b=a");
apply force;
apply (rule prime_prop_lzero);
apply auto;
done;

lemma prime_prop2: "a:prime ==> b:prime ==> (0<c) ==> (0<d) ==>
a^c = b^d ==> c=d";
apply (frule prime_prop);
prefer 4;
apply (assumption)+;
apply simp;

lemma prime_prop_pair: "(fst x):prime ==> (fst y):prime ==> 0<(snd x) ==> 0<(snd y) ==> (fst x)^(snd x) = (fst y)^(snd y) ==> x=y";
apply (frule prime_prop2);
apply auto;
apply (subgoal_tac "fst x  = fst y");
apply (subgoal_tac "snd x = snd y");
apply (auto simp add: prime_prop prime_prop2);
done;

lemma real_addition: "(c::real) * real(Suc x) = c + c * real(x)";

lemma setsum_bound_real: "finite A ==> ALL x:A. (f(x) <= (c::real)) ==> setsum f A <= c * real(card A)";
apply (induct set: Finites, auto);
done;

lemma sumr_suc: "sumr 0 x f + f x = sumr 0 (x+1) f";
apply auto;
done;

lemma real_power: "((a::nat)^b <= x) = ((real a) ^ b <= real(x))";
apply (simp only: real_of_nat_le_iff [THEN sym]);
done;

lemma zprime_pos: "x : zprime ==> 0 < x";
done;

lemma int_nat_inj: "nat x = nat y ==> 0 < x ==> 0 < y ==> x = y";
apply (subgoal_tac "int (nat x) = int (nat y)");
apply auto;
done;

lemma setprod_multiplicity_real: "0 < n ==> real n =
setprod (%p. (real p)^(multiplicity p n))
{p. p : zprime & p dvd n}";
apply (frule n_eq_setprod_multiplicity);
apply (subgoal_tac "real (∏p∈{p. p ∈ zprime ∧ p dvd n}.
p ^ multiplicity p n) = (∏p∈{p. p ∈ zprime ∧ p dvd n}.
(real p) ^ multiplicity p n)");
apply force;
apply (subst setprod_real_of_int);
apply (rule setprod_cong);
apply (rule refl);
apply (subst real_of_int_power);
apply (rule refl);
done;

lemma multiplicity_nmult_eq: "multiplicity x y = nmult (nat x) (nat y)";
apply (subgoal_tac "x ~: zprime");
apply (subgoal_tac "0 ~: zprime");
apply (auto simp add: not_zprime_multiplicity_eq_0 zprime_def);
done;

subsection {* Basic properties *}

lemma Lambda_eq_aux: "[|p ∈ prime; 0 < a|]
==> (THE pa. pa ∈ prime ∧ (∃aa. pa ^ aa = p ^ a)) = p";
apply (rule the_equality);
apply auto;
apply (erule prime_prop);
apply assumption;
prefer 3;
apply assumption;
apply (subgoal_tac "aa ~= 0");
apply force;
apply (subgoal_tac "p^a ~= 1");
apply (rule notI2);
apply assumption;
apply simp;
apply (subgoal_tac "1 < p^a");
apply force;
apply (rule power_lemma);
apply assumption+;
done;

lemma Lambda_eq: "p:prime ==> 0 < a ==> Lambda(p^a) = ln(real p)";
apply (unfold Lambda_def);
apply auto;
apply (subst Lambda_eq_aux);
apply auto;
done;

lemma Lambda_eq2: "~ (EX p a. p : prime & p ^ a = x & 0 < a) ==>
Lambda x = 0";
apply (unfold Lambda_def);
apply auto;
done;

lemma Lambda_zero: "Lambda 0 = 0";
apply (subst Lambda_eq2);
done;

lemma Lambda_ge_zero: "0 <= Lambda x";
apply (case_tac "EX p a. p : prime & p ^ a = x & 0 < a");
apply (auto simp add: Lambda_eq Lambda_eq2);
apply (rule ln_ge_zero);
done;

lemma psi_diff1: "psi (x + 1) - psi x = Lambda (x+1)";

lemma psi_diff2: "1 <= x ==> Lambda x = psi x - psi (x - 1)";
apply (subgoal_tac "x = (x - 1) + 1");
apply (erule ssubst);
apply (subst psi_diff1 [THEN sym]);
apply simp;
apply simp;
done;

lemma psi_zero: "psi 0 = 0";

lemma psi_plus_one: "psi(x + 1) = psi x + Lambda(x + 1)";
apply (unfold psi_def);
apply auto;
done;

lemma psi_def_alt: "psi x = (∑i=1..x. Lambda i)";
apply (induct x);
apply (subgoal_tac "Suc n = n + 1");
apply (erule ssubst);back;
apply (subst psi_plus_one);
apply (case_tac "n = 0");
apply simp;
apply (subst setsum_range_plus_one_nat);
apply auto;
done;

lemma psi_mono: "x <= y ==> psi x <= psi y";
apply (unfold psi_def);
apply (case_tac "x = y");
apply simp;
apply (rule sumr_le);
apply clarify;
apply (rule Lambda_ge_zero);
apply simp;
done;

lemma psi_ge_zero: "0 <= psi x";
apply (unfold psi_def);
apply (rule sumr_ge_zero);
apply (rule allI);
apply (rule Lambda_ge_zero);
done;

lemma theta_geq_zero: "0 <= theta n";
apply (unfold theta_def);
apply (rule sumr_ge_zero);
apply (unfold lprime_def);
apply auto;
apply (rule ln_ge_zero);
done;

lemma theta_zero: "theta 0 = 0";
apply (unfold theta_def);
apply simp;
apply (unfold lprime_def);
done;

lemma theta_1_is_0: "theta(1) = 0";
by (simp add: theta_def lprime_def prime_def);

lemma big_lemma1: "pi(2) = 1";
apply (subgoal_tac "{y::nat. y <= (2::nat) & y : prime} = {2}");
apply (erule ssubst);
apply auto;
apply (case_tac "x=0");
apply simp;
apply (case_tac "x=1");
apply auto;
done;

subsection {* Comparing psi and theta *}

lemma theta_setsum_eq1: "theta(x) = setsum lprime {0..x}";
apply (simp only: theta_def);
done;

lemma prime_partition: "{p. p<x} = {p. p<x & p:prime} Un {p. p<x & p~:prime}";
apply auto;
done;

lemma prime_partition_le: "{p. p<=x} = {p. p<=x & p:prime} Un
{p. p<=x & p~:prime}";
by auto;

lemma all_nonprime_set_l: "[| finite A;  ALL x:A. x ~: prime |] ==>
setsum lprime A = 0";
apply (rule setsum_0');
done;

lemma (in l) finite_A: "finite A";
apply (rule finite_subset [of "{y. y <= x &
(EX p. p : prime & (EX a. 0 < a & p ^ a = y))}" "{..x}"]);
apply auto;
done;

lemma (in l) finite_B: "finite B";
apply (rule finite_subset [of "{y. y <= x & (
ALL p. p : prime --> (ALL a. a = 0 | p ^ a ~= y))}" "{..x}"]);
apply auto;
done;

lemma (in l) A_B_disjoint: "A Int B = {}";
apply (unfold A_def B_def);
apply blast;
done;

lemma (in l) A_B_all: "A Un B = {y. y<=x}";
apply (unfold A_def B_def);
apply auto;
done;

lemma (in l) cor_psi_sum: "psi(x) = setsum Lambda A + setsum Lambda B";
apply (unfold psi_def);
apply (subst setsum_sumr2 [THEN sym]);
apply (subst setsum_Un_disjoint [THEN sym]);
apply (rule finite_A, rule finite_B, rule A_B_disjoint);
apply (subgoal_tac "{0..x} = A Un B");
apply force;
apply (unfold A_def B_def);
apply blast;
done;

lemma (in l) B_kernel_for_Lambda: "y:B ==> Lambda(y) = 0";
apply (auto simp add: B_def Lambda_def);
apply (drule_tac x = p in spec);
apply (clarify);
apply (drule_tac x = a in spec);
by auto;

lemma (in l) sum_over_B_of_Lambda_zero: "setsum Lambda B = 0";
apply (rule setsum_0');
apply (rule ballI);
apply (rule B_kernel_for_Lambda);
apply assumption;
done;

lemma (in l) inj_on_C: "inj_on f C";
apply (rule inj_onI);
apply (unfold C_def f_def);
apply (subgoal_tac "(fst xa):prime");
apply (subgoal_tac "(fst y):prime" "0<(snd xa)" "0<snd y");
done;

lemma (in l) range_of_C_is_A: "f`C = A";
apply (auto simp add: C_def A_def f_def image_def);
done;

lemma (in l) finite_C: "finite C";
apply (rule finite_imageD);
apply (subst range_of_C_is_A);
apply (rule finite_A, rule inj_on_C);
done;

lemma (in l) D_subset_C: "D <= C";
by (auto simp add: D_def C_def);

lemma (in l) E_subset_C: "E <= C";
by (auto simp add: E_def C_def);

lemma (in l) Lambda_reindex_1: "setsum Lambda (f`C) = setsum (Lambda o f) C";
apply (rule setsum_reindex);
done;

lemma (in l) psi_Lambda_eq_over_C: "psi(x) = setsum (Lambda o f) C";
apply (simp add: Lambda_reindex_1 [THEN sym]);
apply (subst range_of_C_is_A);
apply (subst cor_psi_sum);
apply (subst sum_over_B_of_Lambda_zero);
apply simp;
done;

lemma psi_alt_def: "psi(x) = (∑u:{(p,a). (p:prime & 0<a & p^a:{0..x})}.
Lambda((fst u)^(snd u)))";
apply (subst l.psi_Lambda_eq_over_C);
apply (unfold o_def);
apply (rule refl);
done;

lemma (in l) C_eq_D_Un_E: "C = D Un E";
apply (auto simp add: C_def D_def E_def);
done;

lemma (in l) D_Int_E_empty: "D Int E = {}";
by (auto simp add: D_def E_def);

lemma (in l) finite_D: "finite D";
apply (rule finite_subset);
apply (rule D_subset_C);
apply (rule finite_C);
done;

lemma (in l) finite_E: "finite E";
apply (rule finite_subset);
apply (rule E_subset_C);
apply (rule finite_C);
done;

lemma (in l) setsum_C_D_E: "setsum (Lambda o f) C = setsum (Lambda o f) D +
setsum (Lambda o f) E";
apply (subgoal_tac "C = D Un E");
apply simp;
apply (rule setsum_Un_disjoint);
apply (rule finite_D, rule finite_E, rule D_Int_E_empty, rule C_eq_D_Un_E);
done;

lemma (in l) psi_Lambda_eq: "psi(x) = setsum (Lambda o f) D +
setsum (Lambda o f) E";
apply (subst setsum_C_D_E [THEN sym]);
apply (rule psi_Lambda_eq_over_C);
done;

lemma (in l) inj_on_g_F: "inj_on g F";
apply (auto simp add: inj_on_def F_def g_def);
done;

lemma (in l) g_image_F_is_D: "g`F = D";
apply (auto simp add: g_def F_def D_def);
done;

lemma (in l) finite_F: "finite F";
apply (unfold F_def);
apply (subgoal_tac "finite {..x}");
apply (rule finite_subset);
prefer 2;
apply assumption;
apply auto;
done;

lemma (in l) reindex_Lambda_f_g: "setsum (Lambda o f) D =
setsum (Lambda o f o g) F";
apply (insert g_image_F_is_D [THEN sym] inj_on_g_F finite_F);
done;

lemma aux1 [rule_format]: "1 < (a::nat) --> 0 < b --> Suc 0 < a^b";
apply (induct_tac b);
apply force;
apply clarsimp;
apply (case_tac "n = 0");
apply auto;
apply (rule one_less_mult);
apply auto;
done;

lemma aux2 [rule_format]: "1 < (a::nat) & 1 < b --> a < a^b";
apply (induct_tac "b");
apply force;
apply clarify;
apply simp;
apply (rule aux1);
apply auto;
done;

lemma aux3: "p:prime ==> 1 < a ==> ~ (p^a : prime)";
apply (unfold prime_def);
apply (clarsimp);
apply (rule_tac x = "p" in exI)
apply (rule conjI);
apply (rule dvd_self_exp);
apply force;
apply (rule conjI);
apply force;
apply (subgoal_tac "p < p^a");
apply force;
apply (rule aux2);
by auto;

lemma prime_power_must_be_one: "p:prime ==> p^a:prime ==> a=1";
apply auto;
apply (case_tac "a=0");
apply simp;
apply (case_tac "a=1");
done;

lemma (in l) F_prop: "p:F --> (Lambda(f(g(p)))) = ln(real(p))";
apply (unfold F_def f_def g_def);
apply clarify;
apply simp;
apply (unfold Lambda_def);
apply auto;
apply (subgoal_tac "(THE pa::nat. pa : prime &
(EX aa::nat. pa ^ aa = p ^ a)) = p^a");
apply (erule ssubst);
apply (simp);
apply (rule the_equality);
apply (rule_tac x = "1" in exI);
apply simp;
apply (subgoal_tac "a=1");
apply simp;
apply (subgoal_tac "aa=1");
apply simp;
apply (subgoal_tac "pa^aa : prime");
prefer 2;
apply simp;
apply (simp only: prime_power_must_be_one);
apply (simp only: prime_power_must_be_one);
apply (drule_tac x = "p" in spec);
apply simp;
apply (drule_tac x = "1" in spec);
apply auto;
done;

lemma (in l) sum_over_F: "setsum (Lambda o f o g) F = setsum (ln o real) F";
apply (rule setsum_cong);
done;

lemma (in l) sum_over_F2_lemma1: "setsum lprime {0..x} =
setsum lprime ({p. p<=x & p:prime} Un {p. p<=x & p~:prime})";
apply (subgoal_tac "{0..x} = {p. p<=x}");
apply (erule ssubst);
apply (subgoal_tac "{p. p<=x} =
({p::nat. p <= x & p : prime} Un {p::nat. p <= x & p ~: prime})");
apply (erule ssubst);
apply simp;
done;

lemma (in l) sum_over_F2_lemma2:
"setsum lprime ({p. p<=x & p:prime} Un {p. p<=x & p~:prime}) =
setsum lprime {p. p<=x & p:prime} + setsum lprime {p. p<=x & p~:prime}";
apply (rule setsum_Un_disjoint);
apply auto;
apply (rule finite_subset_AtMost_nat);
apply force;
apply (rule finite_subset_AtMost_nat);
apply force;
done;

lemma (in l) l_set_of_primes: "ALL x:P. x:prime ==>
setsum lprime P = setsum (ln o real) P";
apply (rule setsum_cong);
done;

lemma (in l) sum_over_F2: "setsum (ln o real) F = theta(x)";
apply (unfold F_def theta_def);
apply (subst setsum_sumr2 [THEN sym]);
apply (subst l_set_of_primes [THEN sym]);
apply force;
apply (subgoal_tac "setsum lprime {0..x} =
setsum lprime ({p. p:prime & p<=x} Un {p. p~:prime & p<=x})");
apply (erule ssubst);
apply (subst setsum_Un_disjoint);
apply (rule finite_subset_AtMost_nat);
apply auto;
apply (rule finite_subset_AtMost_nat);
apply auto;
apply (subst all_nonprime_set_l);
apply (rule finite_subset_AtMost_nat);
apply auto;
apply (subgoal_tac "{0..x} =
{p. p:prime & p<=x} Un {p. p~:prime & p<=x}");
apply auto;
done;

lemma (in l) psi_theta_sum: "psi(x) = theta(x) + setsum (Lambda o f) E";
apply (subst sum_over_F2 [THEN sym]);
apply (subst sum_over_F [THEN sym]);
apply (subst reindex_Lambda_f_g [THEN sym]);
apply (rule psi_Lambda_eq);
done;

lemma exponent_eq_0_iff: "2 <= p ==> Suc 0 = p^a ==> a = 0";
apply (case_tac a);
done;

lemma (in l) Lambda_positive: "ALL x:E. 0 <= Lambda(f(x))";
apply (auto simp add: E_def Lambda_def f_def);
apply (subgoal_tac "0 = ln 1");
apply (erule ssubst [of "(0::real)" "ln (1::real)" _]);
apply (subgoal_tac "0 < real((THE p::nat. p : prime &
(EX aa::nat. p ^ aa = a ^ b)))");
apply (simp only: ln_le_cancel_iff);
apply (subgoal_tac "(1 :: real) = real(1::nat)");
apply (erule ssubst [of "(1::real)" "real (1::nat)" _]);
apply (simp only: real_of_nat_le_iff);
apply (auto);
apply (rule Suc_leI);
apply simp;
apply (rule theI2);
apply auto;
prefer 2;
apply (case_tac "aaa = 0");
prefer 2;
apply (subgoal_tac "0 < aaa");
prefer 2;
apply simp;
apply (subgoal_tac "p^aa = pa^aaa");
apply (simp only: prime_prop);
apply simp;
apply auto;
apply (subgoal_tac "Suc 0 = p^aa");
prefer 2;
apply simp;
apply (subgoal_tac "2 <= p");
apply (subgoal_tac "0 = aa");
prefer 2;
prefer 2;
apply (simp only: order_less_imp_not_eq [of "0" "aa"]);
done

lemma real_power_ln: "1 < a ==> 0<x ==> ((a::nat)^b <= x) =
(real(b) <= ln(real x)/ln(real a))";
apply (simp only: real_power);
apply (subgoal_tac "0 < real a ^ b");
apply (subgoal_tac "0 < real(x)");
apply (simp only: ln_le_cancel_iff [THEN sym]);
apply (subgoal_tac "0 < ln (real a)");
apply (subgoal_tac "1 < real a");
apply force;
apply force;
apply (subgoal_tac "0 < a");
apply (subgoal_tac "0 < a^b");
apply force;
done;

(*
lemma (in l) extent_of_E: "E <= {1..x} <*>
{1..nat(floor(ln(real x)/ln(2)))}";
apply (subgoal_tac "2 <=a");
apply force;
apply (subgoal_tac "2 <= a");
apply (subgoal_tac "2 <= b");
apply (subgoal_tac "a <= a^2");
apply (subgoal_tac "a^2 <= a^b");
apply force;
apply (subgoal_tac "0 <= a");
apply (subgoal_tac "(a <= a^2) = (a^1 <= a^2)");
apply (erule ssubst);
apply (simp only: power_increasing);
apply force;
apply force;
apply force;
apply (subst real_of_nat_le_iff [THEN sym]);
apply (subgoal_tac "2^b <= x");
apply (subgoal_tac "0 < x");
apply (subgoal_tac "1 < a");
apply (simp only: real_power_ln);
apply (subgoal_tac "real(2::nat) = 2");
apply (erule ssubst);
apply (subgoal_tac "2 <= a");
apply force;
apply (subgoal_tac "0 < a");
apply (subgoal_tac "0 < a^b");
apply (simp only: less_le_trans [of "0" "a^b" "x"]);
apply (subgoal_tac "2 <= a");
apply force;
apply (subgoal_tac "2 <= a");
apply (subgoal_tac "2^b <= a^b");
apply force;
apply (auto simp add: power_mono prime_ge_2);
done;
*)

lemma (in l) extent_of_E2: "E <= {1..nat(floor(real(x) powr (1/2)))} <*>
{1..nat(floor(ln(real x)/ln(2)))}";
apply (subgoal_tac "2 <=a");
apply force;
apply (subgoal_tac "a <= natfloor(real x powr (1/2))");
apply (subgoal_tac "a^2 <= x");
apply (subgoal_tac "(real a) powr (real (2::nat)) <= real x");
apply (subgoal_tac "((real a) powr (real (2::nat))) powr (1/2) <= (real x) powr (1/2)");
apply auto;
apply (subgoal_tac "real a <= real x powr (1/2)");
apply (rule real_le_natfloor);
apply auto;
apply (subgoal_tac "real a powr 1 = real a");
apply force;
apply (subst powr_one_gt_zero_iff);
apply (subgoal_tac "2 <= a");
apply arith;
apply (rule power_mono2);
apply force+;
apply (subgoal_tac "(2::real) = real (2::nat)");
apply (erule ssubst);
apply (subst powr_realpow);
apply (subgoal_tac "2 <= a");
apply arith;
apply (subgoal_tac "real a ^ 2 = real (a^2)");
apply force;
apply (rule realpow_real_of_nat);
apply force+;
apply (subgoal_tac "a^2 <= a^b");
apply force;
apply (rule power_increasing);
apply force;
apply (frule prime_ge_2);
apply arith;
(* FIRST PART DONE! YAY! *)
apply (subgoal_tac "2^b <= x");
apply (subgoal_tac "0 < x");
apply (subgoal_tac "1 < a");
apply (simp only: real_power_ln);
apply (subgoal_tac "real(2::nat) = 2");
apply (erule ssubst);
apply (subgoal_tac "2 <= a");
apply force;
apply (subgoal_tac "0 < a");
apply (subgoal_tac "0 < a^b");
apply (simp only: less_le_trans [of "0" "a^b" "x"]);
apply (subgoal_tac "2 <= a");
apply force;
apply (subgoal_tac "2 <= a");
apply (subgoal_tac "2^b <= a^b");
apply force;
apply (auto simp add: power_mono prime_ge_2);
done;

(*
lemma (in l) card_E_lemma: "card E <=
card ({1..x} <*> {1..nat(floor(ln(real x)/ln(2)))})";
apply (rule card_mono);
prefer 2;
apply (rule extent_of_E);
apply simp;
done;
*)

lemma (in l) card_E2_lemma: "card E <=
card ({1..nat(floor(real(x) powr (1/2)))} <*> {1..nat(floor(ln(real x)/ln(2)))})";
apply (rule card_mono);
prefer 2;
apply (rule extent_of_E2);
apply simp;
done;

(*
lemma (in l) card_E_lemma2:
"card ({1..x} <*> {1..nat(floor(ln(real x)/ln(2)))}) =
card {1..x} * card {1..nat(floor(ln(real x)/ln(2)))}";
apply simp;
done;
*)

lemma (in l) card_E2_lemma2:
"card ({1..nat(floor(real(x) powr (1/2)))} <*> {1..nat(floor(ln(real x)/ln(2)))}) =
card {1..nat(floor(real(x) powr (1/2)))} * card {1..nat(floor(ln(real x)/ln(2)))}";
apply simp;
done;

(*
lemma (in l) card_E_lemma3:
"card ({1..x} <*> {1..nat(floor(ln(real x)/ln(2)))}) <=
card {1..x} * card {1..nat(floor(ln(real x)/ln(2)))}";
done;
*)

lemma (in l) card_E2_lemma3:
"card ({1..nat(floor(real(x) powr (1/2)))} <*> {1..nat(floor(ln(real x)/ln(2)))}) <=
card {1..nat(floor(real(x) powr (1/2)))} * card {1..nat(floor(ln(real x)/ln(2)))}";
done;

(*
lemma (in l) card_E:
"card E <= card {1..x} * card {1..nat(floor(ln(real x)/ln(2)))}";
apply (insert card_E_lemma3);
apply (insert card_E_lemma);
apply (erule le_trans);
apply assumption;
done;
*)

lemma (in l) card_E2:
"card E <= card {1..nat(floor(real(x) powr (1/2)))} * card {1..nat(floor(ln(real x)/ln(2)))}";
apply (insert card_E2_lemma3);
apply (insert card_E2_lemma);
apply (erule le_trans);
apply assumption;
done;

(*
lemma card_E_real_lemma4: "real(floor(ln(real x)/ln(2))) <= ln(real x)/ln(2)";
done;
*)

lemma card_E2_real_lemma4: "real(floor(ln(real x)/ln(2))) <= ln(real x)/ln(2)";
done;

(*
lemma (in l) real_card_E: "real(card E) <=
real(card {1..x} * card {1..nat(floor(ln(real x)/ln(2)))})";
apply (simp only: real_of_nat_le_iff);
apply (rule card_E);
done;
*)

lemma (in l) real_card_E2: "real(card E) <=
real(card {1..nat(floor(real(x) powr (1/2)))} * card {1..nat(floor(ln(real x)/ln(2)))})";
apply (simp only: real_of_nat_le_iff);
apply (rule card_E2);
done;

(*
lemma (in l) card_E_real_lemma6: "0 < x ==>
real(card {1..nat(floor(ln(real x)/ln(2)))}) <= ln(real x)/ln(2)";
apply simp;
apply (subgoal_tac "0 <= ln(real x) / ln 2");
apply (rule real_nat_floor);
apply auto;
done;
*)

lemma (in l) card_E2_real_lemma6: "0 < x ==>
real(card {1..nat(floor(ln(real x)/ln(2)))}) <= ln(real x)/ln(2)";
apply simp;
apply (subgoal_tac "0 <= ln(real x) / ln 2");
apply (rule real_nat_floor);
apply auto;
done;

(*
lemma (in l) card_E_real: "0 < x ==> real(card E) <=
real(x) * ln(real x)/ln(2)";
proof-;
assume pos: "0 < x";
have step1: "real(card E) <=
real(card {1..x} * card {1..nat(floor(ln(real x)/ln(2)))})";
by (rule real_card_E);
also have step2: "... =
real(card {1..x}) * real(card {1..nat(floor(ln(real x)/ln(2)))})";
by (rule real_of_nat_mult);
also have step3: "... <= real(x) * ln(real x)/ln(2)";
apply (subgoal_tac "real x * ln (real x) / ln 2 =
real x * (ln (real x) / ln 2)");
apply (erule ssubst);
apply (rule mult_left_mono);
apply (subgoal_tac "0<= ln(real x)/ln 2");
apply (rule real_nat_floor);
apply force;
apply (subgoal_tac "1<= real x");
apply (drule ln_ge_zero);
apply (subgoal_tac "0 < ln 2");
apply auto;
apply (subgoal_tac "1<=x");
done;
finally show ?thesis;.;
qed;
*)

lemma (in l) card_E2_real: "0 < x ==> real(card E) <=
real(nat(floor(real(x) powr (1/2)))) * ln(real x)/ln(2)";
proof-;
assume pos: "0 < x";
have step1: "real(card E) <=
real(card {1..nat(floor(real(x) powr (1/2)))} * card {1..nat(floor(ln(real x)/ln(2)))})";
by (rule real_card_E2);
also have step2: "... =
real(card {1..nat(floor(real(x) powr (1/2)))}) * real(card {1..nat(floor(ln(real x)/ln(2)))})";
by (rule real_of_nat_mult);
also have step3: "... <= real(nat(floor(real(x) powr (1/2)))) * ln(real x)/ln(2)";
apply (subgoal_tac "real (nat(floor(real(x) powr (1/2)))) * ln (real x) / ln 2 =
real (nat(floor(real(x) powr (1/2)))) * (ln (real x) / ln 2)");
apply (erule ssubst);
apply (rule mult_left_mono);
apply (subgoal_tac "0<= ln(real x)/ln 2");
apply (rule real_nat_floor);
apply force;
apply (subgoal_tac "1<= real x");
apply (drule ln_ge_zero);
apply (subgoal_tac "0 < ln 2");
apply auto;
apply (subgoal_tac "1<=x");
done;
finally show ?thesis;.;
qed;

lemma (in l) E_bound_with_f: "y:E --> f(y) <= x";
done;

lemma Lambda_prop: "ALL x. (0 < x --> Lambda(x) <= ln(real(x)))";
apply (rule theI2);
apply auto;
apply (rule prime_prop_rzero);
apply auto;
apply (case_tac "aa=0");
apply auto;
apply (subgoal_tac "Suc 0 < p^1");
apply (subgoal_tac "p^1 <= p^a");
apply force;
apply (rule power_increasing);
apply force;
apply force;
apply (subgoal_tac "2 <= p^1");
apply force;
apply (subgoal_tac "2 <= p");
apply (subgoal_tac "p = p^1");
apply force;
apply (rule power_one_right [THEN sym]);
apply (subgoal_tac "x = p");
apply (subgoal_tac "real(x) = real(p)");
apply auto;
apply (subgoal_tac "p^1 <= p^a");
apply force;
apply (rule power_increasing);
apply force;
apply force;
apply (rule prime_prop_rzero);
apply auto;
done;

lemma (in l) E_bound: "0 < x ==> y:E ==> (Lambda o f)(y) <= ln(real(x))";
apply (subgoal_tac "0 < xa^y");
apply (subgoal_tac "Lambda(xa^y) <= ln(real(xa^y))");
apply (subgoal_tac "ln(real(xa^y)) <= ln(real(x))");
apply force;
apply (simp only: ln_le_cancel_iff);
apply (subgoal_tac "xa^1 <= xa^y");
apply (subgoal_tac "0 < xa");
apply force;
apply (subgoal_tac "2 <= xa");
apply force;
apply (subgoal_tac "1 <= y");
apply (rule power_increasing);
apply auto;
apply (subgoal_tac "2 <= xa");
apply force;
done;

(*
lemma (in l) sum_over_E_of_Lambda_o_f: "0 < x ==>
setsum (Lambda o f) E <=  real(x) * ln(real(x)) * ln(real(x)) / ln 2";
apply (subgoal_tac "setsum (Lambda o f) E <= real(card E) * ln(real(x))");
apply (subgoal_tac "real(card E) <= real(x) * ln(real x)/ln(2)");
apply (subgoal_tac "real(card E) * ln(real(x)) <=
real(x) * ln(real x)/ln(2) * ln(real(x))");
apply (subgoal_tac "setsum (Lambda o f) E <=
real(x) * ln(real x)/ln(2) * ln(real(x))");
apply force;
apply force;
apply (subgoal_tac "0 <= ln(real(x))");
apply (rule mult_right_mono);
apply force;
apply (subgoal_tac "1 <= x");
apply force;
apply (subgoal_tac "1 <= x");
apply force;
apply (subgoal_tac "real (card E) * ln (real x) =
ln (real x) * real (card E)");
apply (erule ssubst);
apply (rule setsum_bound_real);
apply (rule ballI);
apply (rule E_bound);
apply auto;
done;
*)

lemma (in l) sum_over_E2_of_Lambda_o_f: "0 < x ==>
setsum (Lambda o f) E <=  real(nat(floor(real(x) powr (1/2)))) * ln(real(x)) * ln(real(x)) / ln 2";
apply (subgoal_tac "setsum (Lambda o f) E <= real(card E) * ln(real(x))");
apply (subgoal_tac "real(card E) <= real(nat(floor(real(x) powr (1/2)))) * ln(real x)/ln(2)");
apply (subgoal_tac "real(card E) * ln(real(x)) <=
real(nat(floor(real(x) powr (1/2)))) * ln(real x)/ln(2) * ln(real(x))");
apply (subgoal_tac "setsum (Lambda o f) E <=
real(nat(floor(real(x) powr (1/2)))) * ln(real x)/ln(2) * ln(real(x))");
apply force;
apply force;
apply (subgoal_tac "0 <= ln(real(x))");
apply (rule mult_right_mono);
apply force;
apply (subgoal_tac "1 <= x");
apply force;
apply (subgoal_tac "1 <= x");
apply force;
apply (subgoal_tac "real (card E) * ln (real x) =
ln (real x) * real (card E)");
apply (erule ssubst);
apply (rule setsum_bound_real);
apply (rule ballI);
apply (rule E_bound);
apply auto;
done;

(*
lemma (in l) psi_theta_bound: "0 < x ==> psi(x) <=
theta(x) + real(x) * ln(real(x)) * ln(real(x)) / ln 2";
apply (subgoal_tac "psi(x) = theta(x) + setsum (Lambda o f) E");
apply (subgoal_tac "setsum (Lambda o f) E <=
real(x) * ln(real(x)) * ln(real(x)) / ln 2");
apply auto;
apply (auto simp add: psi_theta_sum sum_over_E_of_Lambda_o_f);
done;
*)

lemma (in l) psi_theta_bound_for_real_aux: "0 < x ==> psi(x) <=
theta(x) + real(nat(floor(real(x) powr (1/2)))) * ln(real(x)) * ln(real(x)) / ln 2";
apply (subgoal_tac "psi(x) = theta(x) + setsum (Lambda o f) E");
apply (subgoal_tac "setsum (Lambda o f) E <=
real(nat(floor(real(x) powr (1/2)))) * ln(real(x)) * ln(real(x)) / ln 2");
apply auto;
apply (auto simp add: psi_theta_sum sum_over_E2_of_Lambda_o_f);
done;

lemma psi_theta_bound_for_real: "0 < x ==> psi(x) <=
theta(x) + real(x) powr (1/2) * ln(real(x)) * ln(real(x)) / ln 2";
apply (rule order_trans);
apply (erule l.psi_theta_bound_for_real_aux);
apply (rule divide_right_mono);
apply (rule mult_right_mono)+;
apply (subgoal_tac "nat(floor (?t)) = natfloor(?t)");
apply (erule ssubst);
apply (rule real_natfloor_le);
apply (rule order_less_imp_le);
apply (rule powr_gt_zero);
apply auto;
done;

subsection {* Comparing pi and theta *}

lemma pi_set_zero: "finite A ==> ALL x:A.  x~:prime ==>
setsum char_prime A = 0";
apply (rule setsum_0');
apply (unfold char_prime_def);
apply auto;
done;

lemma setsum_prime_split: "setsum f {p. p<=x} =
setsum f {p. p<=x & p:prime} + setsum f {p. p<=x & p~:prime}";
apply (rule setsum_Un_disjoint);
apply auto;
apply (auto intro: finite_subset_AtMost_nat);
done;

lemma setsum_char_prime_zero: "setsum char_prime {p. p<=x & p~:prime} = 0";
apply (rule pi_set_zero);
by (auto intro: finite_subset_AtMost_nat);

lemma pi_setsum_equiv: "pi(x) = setsum char_prime {p. p<=x}";
apply (auto simp add: pi_def char_prime_def);
apply (subgoal_tac "setsum char_prime {p::nat. p <= x & p : prime} =
setsum (%x. 1) {p::nat. p <= x & p : prime}");
apply (erule ssubst);
apply (subst real_card_eq_setsum);
apply (force intro: finite_subset_AtMost_nat);
apply simp;
apply (rule setsum_cong [of "{p::nat. p <= x & p : prime}"
"{p::nat. p <= x & p : prime}" "char_prime" "%x. 1"]);
done;

lemma pi_sumr_equiv: "pi(x) = sumr 0 (x+1) char_prime";
apply (simp only: pi_setsum_equiv);
apply (subgoal_tac "{p::nat. p <= x} = {0..x}");
apply (erule ssubst);
done;

lemma pi_Suc: "pi(Suc x) = char_prime(Suc x) + pi(x)";
apply (case_tac "(Suc x):prime");
apply (subgoal_tac "{y::nat. y <= Suc x & y : prime} =
{y::nat. y <= x & y : prime} Un {Suc x}");
apply (erule ssubst);
apply (subst card_Un_disjoint);
apply (force intro: finite_subset_AtMost_nat);
apply simp;
apply force;
apply simp;
apply auto;
apply (rule arg_cong);back;
apply auto;
apply (case_tac "xa = Suc x");
apply auto;
done;

lemma char_prime_def_eq: "1 <= n ==>
(theta(n+1) - theta(n)) / ln(real(n+1)) = char_prime(n+1)";
apply (case_tac "Suc n:prime");
apply (auto simp add: lprime_def char_prime_def real_divide_def);
done;

lemma nat_int_inj_on: "inj_on (%x. nat x) {p. p:zprime & (p dvd x)}";
apply (rule inj_onI);
apply auto;
apply (rule int_nat_inj);
done;

lemma int_nat_inj_on: "inj_on int {p. p:prime & p dvd x}";
apply (rule inj_onI);
apply auto;
done;

subsection {* Expressing ln in terms of Lambda *}

lemma ln_product_sum: "finite A ==> ALL x:A. (0 < f(x)) ==>
ln (setprod f A) = setsum (ln o f) A";
apply (induct set: Finites);
apply (subst ln_mult);
apply (auto simp add: setprod_pos o_def);
done;

lemma multiplicity_eq_1: "1 < n ==> ln(real n) =
ln(setprod (%p. (real p)^(multiplicity p n)) {p. 0 < p & p : zprime &
p dvd n})";
apply (subst ln_inj_iff);
apply force;
apply (rule setprod_pos);
apply auto;
apply (subgoal_tac "{p. 0 < p ∧ p ∈ zprime ∧ p dvd n} =
{p. p ∈ zprime ∧ p dvd n}");
apply (erule ssubst);
apply (rule setprod_multiplicity_real);
done;

lemma divisor_set_fact:  "1 < n ==> {p::int. 0 < p & p : zprime & p dvd n} <=
{-n..n}";
apply auto;
apply (subgoal_tac "(-n <= x) = (-x <= n)");
apply (erule ssubst);
apply auto;
done;

lemma multiplicity_eq_2: "1 < n ==> ln(real n) =
setsum (%p. ln ((real p)^(multiplicity p n))) {p. 0 < p & p : zprime &
p dvd n}";
apply (subst multiplicity_eq_1);
apply (assumption);
apply (subst ln_product_sum);
apply (force intro: finite_subset_GreaterThan0AtMost_int zdvd_imp_le);
apply force;
done;

lemma multiplicity_eq_3: "1 < n ==> ln(real n) =
setsum (%p. real(multiplicity p n) * ln(real p)) {p. 0 < p & p : zprime &
p dvd n}";
apply (subst multiplicity_eq_2, assumption);
apply (rule setsum_cong);
apply (rule refl);
apply (subst ln_realpow);
apply force;
apply (rule refl);
done;

lemma (in l) finite_G: "0 < x ==> finite G";
apply (unfold G_def);
apply (rule finite_subset_GreaterThan0AtMost_nat);
apply (auto intro: dvd_imp_le);
done;

lemma (in l) G_fact: "0 < x ==> G = (G Int A) Un (G Int B)";
by (auto simp add: G_def A_def B_def dvd_def);

lemma (in l) Lambda_over_G_lemma1: "0 < x ==>
setsum Lambda G = setsum Lambda ((G Int A) Un (G Int B))";
apply (rule setsum_cong);
apply (simp only: G_fact [THEN sym]);
by auto;

lemma (in l) Lambda_over_G_lemma2: "0 < x ==>
setsum Lambda G = setsum Lambda (G Int A) + setsum Lambda (G Int B)";
apply (subgoal_tac "setsum Lambda G =
setsum Lambda ((G Int A) Un (G Int B))");
apply (erule ssubst);
apply (subst setsum_Un_disjoint);
apply (subgoal_tac "G Int A Int (G Int B) = G Int (A Int B)");
apply (erule ssubst);
apply force;
apply (rule refl);
apply (subst G_fact [THEN sym]);
apply assumption;
apply (rule refl);
done;

lemma (in l) Lambda_over_G_lemma3: "0 < x ==> setsum Lambda (G Int B) = 0";
apply (rule setsum_0');
apply (insert B_kernel_for_Lambda, blast);
done;

lemma (in l) Lambda_over_G_lemma4: "0 < x ==>
setsum Lambda G = setsum Lambda (G Int A)";
apply (auto simp add: Lambda_over_G_lemma2 Lambda_over_G_lemma3);
done;

lemma (in l) G_Int_A_Un_over_J: "G Int A = UNION J (%p. H(p) Int G)";
apply (auto simp add: G_def A_def J_def H_def);
apply (rule_tac x = "p" in exI);
apply auto;
apply (subgoal_tac "p dvd p^a");
prefer 2;
apply (case_tac a);
apply auto;
apply (rule dvd_trans);
apply auto;
done;

lemma (in l) finite_J: "0 < x ==> finite J";
apply (rule finite_subset_GreaterThan0AtMost_nat);
apply auto;
apply (erule prime_pos);
apply (erule dvd_imp_le);
apply assumption;
done;

lemma (in l) finite_H_p: "0 < x ==> finite (H(p))";
apply (rule finite_subset_AtMost_nat);
apply auto;
done;

lemma (in l) different_H: "0 < x ==> p1:prime ==> p2:prime ==>
p1 ~= p2 ==> H(p1) Int H(p2) = {}";
done;

lemma (in l) setsum_Lambda_G_lemma1: "0 < x ==> setsum Lambda G =
setsum (%p. setsum Lambda (H(p) Int G)) J";
apply (simp only: G_Int_A_Un_over_J);
apply (rule setsum_UN_disjoint [of "J" "(%p. H(p) Int G)" "Lambda"]);
apply (rule finite_J);
apply (assumption);
apply (force intro: finite_H_p);
apply auto;
apply (subgoal_tac "xa: H p Int H j");
apply (subgoal_tac "H p Int H j = {}");
apply simp;
apply (rule IntI);
apply auto;
done;

lemma (in l) inj_on_prime_power: "inj_on (%x. (p::nat)^x) {1..nmult p x}";
apply (auto);
apply (rule inj_onI);
apply (case_tac "p:prime");
apply (subgoal_tac "multiplicity (int p) (int x) = 0");
apply simp;
apply (subgoal_tac "(int p)~:zprime");
apply (rule not_zprime_multiplicity_eq_0 [of "int p" "int x"]);
apply auto;
done;

lemma nat_int_dvd: "(int(x) dvd int(y)) = (x dvd y)";
apply (simp only: zdvd_iff_zmod_eq_0);
apply (simp only: dvd_eq_mod_eq_0);
apply auto;
apply (case_tac "0 <= q");
apply (rule_tac x = "nat q" in exI);
apply (rule_tac x = "int q" in exI);
done;

lemma nat_zmult_multiplicity_lemma1:
"(int p) ^ multiplicity (int p) (int n) dvd (int n)";
done;

lemma nat_zmult_multiplicity_lemma2:
"int (p ^ multiplicity (int p) (int n)) dvd (int n)";
apply (auto simp add: zpow_int nat_zmult_multiplicity_lemma1);
done;

lemma nat_zmult_multiplicity: "p ^ multiplicity (int p) (int n) dvd n";
apply (auto simp add: nat_int_dvd [THEN sym]);
done;

lemma power_dvd_prop: "p^b dvd (x::nat) ==> a <= b ==> p^a dvd x";
apply (rule_tac x = "k * (p ^ (b-a))" in exI);
apply auto;
done;

lemma power_le_prop1 [rule_format]: "1 <= (p::nat) ==> a <= b --> p^a <= p^b";
apply (induct_tac b);
apply auto;
apply (subgoal_tac "a = Suc n");
apply auto;
apply (subgoal_tac "p^n <= p*p^n");
apply (simp only: le_trans [of "p^a" "p^n" "p*p^n"]);
apply auto;
done;

lemma power_le_prop: "1 < p ==> p^b <= (x::nat) ==> a <= b ==> p^a <= x";
apply (subgoal_tac "p^a <= p^b");
apply auto;
done;

lemma nat_zmult_multiplicity_le: "0<n ==>
p ^ multiplicity (int p) (int n) <= n";
apply (subgoal_tac "p^multiplicity (int p) (int n) dvd n");
done;

lemma multiplicity_power_dvd: "0<n ==> p:prime ==>
(k <= multiplicity (int p) (int n)) = (p^k dvd n)";
apply auto;
apply (subgoal_tac "p^multiplicity (int p) (int n) dvd n");
apply (rule power_dvd_prop);
apply assumption+;
apply (subgoal_tac "(int p):zprime");
apply (subgoal_tac "(int p)^k dvd (int n)");
apply (subgoal_tac "int p ^ k = int(p^k)");
apply (erule ssubst);
apply (simp only: nat_int_dvd [THEN sym]);
apply (simp only: zpow_int [THEN sym]);
done;

lemma multiplicity_power_dvd_imp1: "0 < n ==> p : prime ==>
p ^ k dvd n ==> k <= multiplicity (int p) (int n)";
apply (subst multiplicity_power_dvd);
apply assumption+;
done;

lemma (in l) G_Int_Hp_eq: "0 < x ==> p:prime ==>
(%x. p^x) ` {1..nmult p x} = G Int H(p)";
apply auto;
apply auto;
apply (subgoal_tac "2 <= p");
apply (simp);
apply (subgoal_tac "1 < p");
apply (subgoal_tac "p ^ multiplicity (int p) (int x) dvd x");
apply (rule power_dvd_prop);
apply assumption+;
apply (subgoal_tac "2 <= p");
apply simp;
apply (rule prime_ge_2,assumption);
apply (unfold H_def nmult_def);
apply clarsimp;
apply (rule conjI);
apply (subgoal_tac "1 < p");
apply (subgoal_tac "p ^ multiplicity (int p) (int x) <= x");
apply (rule power_le_prop);
apply assumption+;
apply (subgoal_tac "p ^ multiplicity (int p) (int x) <= x");
apply (subgoal_tac "1 < p");
apply (rule power_le_prop);
apply assumption+;
apply force;
apply assumption;
apply (subgoal_tac "2 <= p");
apply simp;
apply (erule prime_ge_2);
apply (rule_tac x = "xa" in exI);
apply simp;
apply (unfold G_def image_def);
apply simp;
apply clarify;
apply (rule_tac x = a in bexI);
apply (rule refl);
apply auto;
apply (subst multiplicity_power_dvd);
apply auto;
apply (subgoal_tac "0 < p ^ a");
apply (erule order_less_le_trans);back;back;
apply assumption;
apply auto;
done;

lemma (in l) card_multiplicity_eq: "0 < x ==> p:prime ==>
card(G Int H(p)) = multiplicity (int p) (int x)";
apply (subst G_Int_Hp_eq [THEN sym]);
apply assumption+;
apply (subst card_image);
apply simp;
apply (rule inj_on_prime_power);
done;

lemma (in l) setsum_Lambda_G_int_Hp: "0 < x ==> p:prime ==>
setsum Lambda (G Int H(p)) = ln (real p) *
real (multiplicity (int p) (int x))";
proof -;
assume "0 < x" and "p:prime";
have "ALL x:(G Int H(p)). Lambda x = ln (real p)";
by (auto simp add: G_def H_def prems Lambda_eq);
then have "setsum Lambda (G Int H(p)) =
setsum (%x. ln (real p)) (G Int H(p))";
apply (intro setsum_cong);
apply (rule refl);
apply (erule bspec);
apply assumption;
done;
also have "… = real(card (G Int H(p))) * ln (real p)";
apply (subst setsum_constant);
apply (rule finite_subset);
prefer 2;
apply (rule finite_G);
apply (rule prems);
apply force;
done;
also have "card (G ∩ H p) = multiplicity (int p) (int x)"
by (rule card_multiplicity_eq);
finally show ?thesis;
by simp;
qed;

lemma (in l) setsum_Lambda_G_lemma2: "0 < x ==> setsum Lambda G =
setsum (%p. ln (real p) * real (multiplicity (int p) (int x))) J";
apply (subst setsum_Lambda_G_lemma1);
apply assumption;
apply (rule setsum_cong);
apply (rule refl);
apply (subgoal_tac "H xa Int G = G Int H xa");
apply (erule ssubst);
apply (erule setsum_Lambda_G_int_Hp);
apply auto;
done;

lemma multiplicity_eq_4: "0 < n ==> ln(real n) =
setsum (%p. real(multiplicity p n) * ln(real p)) {p. 0 < p & p : zprime &
p dvd n}";
apply (subgoal_tac "n = 1 | 1 < n");
apply (erule disjE);
apply (elim multiplicity_eq_3);
apply force;
done;

lemma multiplicity_eq_5: "0 < n ==> ln(real n) =
setsum (%p. real(multiplicity (int p) (int n)) * ln(real p))
{p. 0 < p & p : prime & p dvd n}";
apply (subgoal_tac "real n = real (int n)");
apply (erule ssubst);
apply (subst multiplicity_eq_4);
apply force;
apply (rule setsum_reindex_cong);
apply (rule finite_subset_AtMost_nat);
apply clarify;
apply (erule dvd_imp_le);
apply assumption;
apply (subgoal_tac "inj_on int {p. 0 < p ∧ p ∈ prime ∧ p dvd n}");
apply assumption;
apply (unfold image_def);
apply auto;
apply (rule_tac x = "nat x" in exI);
apply (subgoal_tac "nat x dvd nat (int n)");
apply simp;
apply (rule nat_int_dvd_prop);
apply assumption;
apply assumption;
apply (rule ext);
apply (unfold o_def);
apply (subgoal_tac "real p = real (int p)");
apply (erule subst);
apply (rule refl);
apply simp;
done;

lemma ln_eq_setsum_Lambda: "0 < (n::nat) ==> ln (real n) =
setsum Lambda {d. d dvd n}";
apply (subgoal_tac "{d. d dvd n} = {d. 0 < d & d dvd n}");
apply (erule ssubst);
apply (subst l.setsum_Lambda_G_lemma2);
apply assumption;
apply (subst multiplicity_eq_5);
apply assumption;
apply (rule setsum_cong);
apply auto;
apply (rule prime_pos);
apply assumption;
apply (erule dvd_pos_pos);
apply assumption;
done;

lemma ln_eq_setsum_Lambda2: "0 < n ==> ln (real n) =
(∑x:{(p, a). 0 < a & p : prime & p ^ a dvd n}.
ln (real (fst x)))";
proof -;
assume "0 < (n::nat)";
have "ln (real n) = (∑d:{d. d dvd n}. Lambda d)";
by (rule ln_eq_setsum_Lambda);
also have "... =
(∑d:{d. d dvd n & (EX p a. 0 < a & p : prime & d = p ^ a)}.
Lambda d) +
(∑d:{d. d dvd n & ~(EX p a. 0 < a & p : prime & d = p ^ a)}.
Lambda d)" (is "... = ?term1 + ?term2");
apply (subst setsum_Un_disjoint [THEN sym]);
apply (rule finite_subset);
prefer 2;
apply (rule finite_nat_dvd_set);
apply (rule prems);
apply force;
apply (rule finite_subset);
prefer 2;
apply (rule finite_nat_dvd_set);
apply (rule prems);
apply force;
apply blast;
apply (rule setsum_cong);
apply blast;
apply force;
done;
also have "?term2 = 0";
apply (rule setsum_0');
apply (rule ballI);
apply (rule Lambda_eq2);
apply auto;
done;
also have "?term1 + 0 = ?term1";
by simp;
also have "... = (∑x:{(p,a). 0 < a & p : prime & p^a dvd n}.
Lambda((%x. (fst x)^(snd x))x))";
apply (subst setsum_reindex' [THEN sym]);back;
apply (rule finite_subset);
prefer 2;
apply (rule l.finite_C [of n]);
apply auto;
apply (erule dvd_imp_le);
apply (rule prems);
apply (rule subset_inj_on);
prefer 2;
apply (rule l.inj_on_C);
apply auto;
apply (erule dvd_imp_le);
apply (rule prems);
apply (rule setsum_cong);
done;
finally show ?thesis;
apply (elim ssubst);
apply (rule setsum_cong2);
apply (rule Lambda_eq);
apply auto;
done;
qed;

end;
```

### Miscellaneaous

lemma prime_prop2:

`  [| a ∈ prime; b ∈ prime; 0 < n; a dvd b ^ n |] ==> a = b`

lemma dvd_self_exp:

`  0 < n ==> m dvd m ^ n`

lemma prime_prop:

`  [| a ∈ prime; b ∈ prime; 0 < c; 0 < d; a ^ c = b ^ d |] ==> a = b`

lemma power_lemma:

`  [| 1 < a; 0 < c |] ==> 1 < a ^ c`

lemma prime_prop_lzero:

`  [| a ∈ prime; b ∈ prime; 0 < c; a ^ c = b ^ d |] ==> a = b`

lemma prime_prop_rzero:

`  [| a ∈ prime; b ∈ prime; 0 < d; a ^ c = b ^ d |] ==> a = b`

lemma prime_prop2:

`  [| a ∈ prime; b ∈ prime; 0 < c; 0 < d; a ^ c = b ^ d |] ==> c = d`

lemma prime_prop_pair:

```  [| fst x ∈ prime; fst y ∈ prime; 0 < snd x; 0 < snd y;
fst x ^ snd x = fst y ^ snd y |]
==> x = y```

`  c * real (Suc x) = c + c * real x`

lemma setsum_bound_real:

`  [| finite A; ∀x∈A. f x ≤ c |] ==> setsum f A ≤ c * real (card A)`

lemma sumr_suc:

`  sumr 0 x f + f x = sumr 0 (x + 1) f`

lemma real_power:

`  (a ^ b ≤ x) = (real a ^ b ≤ real x)`

lemma zprime_pos:

`  x ∈ zprime ==> 0 < x`

lemma int_nat_inj:

`  [| nat x = nat y; 0 < x; 0 < y |] ==> x = y`

lemma setprod_multiplicity_real:

`  0 < n ==> real n = (∏p∈{p. p ∈ zprime ∧ p dvd n}. real p ^ multiplicity p n)`

lemma multiplicity_nmult_eq:

`  multiplicity x y = nmult (nat x) (nat y)`

### Basic properties

lemma Lambda_eq_aux:

`  [| p ∈ prime; 0 < a |] ==> (THE pa. pa ∈ prime ∧ (∃aa. pa ^ aa = p ^ a)) = p`

lemma Lambda_eq:

`  [| p ∈ prime; 0 < a |] ==> Lambda (p ^ a) = ln (real p)`

lemma Lambda_eq2:

`  ¬ (∃p a. p ∈ prime ∧ p ^ a = x ∧ 0 < a) ==> Lambda x = 0`

lemma Lambda_zero:

`  Lambda 0 = 0`

lemma Lambda_ge_zero:

`  0 ≤ Lambda x`

lemma psi_diff1:

`  psi (x + 1) - psi x = Lambda (x + 1)`

lemma psi_diff2:

`  1 ≤ x ==> Lambda x = psi x - psi (x - 1)`

lemma psi_zero:

`  psi 0 = 0`

lemma psi_plus_one:

`  psi (x + 1) = psi x + Lambda (x + 1)`

lemma psi_def_alt:

`  psi x = setsum Lambda {1..x}`

lemma psi_mono:

`  x ≤ y ==> psi x ≤ psi y`

lemma psi_ge_zero:

`  0 ≤ psi x`

lemma theta_geq_zero:

`  0 ≤ theta n`

lemma theta_zero:

`  theta 0 = 0`

lemma theta_1_is_0:

`  theta 1 = 0`

lemma big_lemma1:

`  Chebyshev1.pi 2 = 1`

### Comparing psi and theta

lemma theta_setsum_eq1:

`  theta x = setsum lprime {0..x}`

lemma prime_partition:

`  {p. p < x} = {p. p < x ∧ p ∈ prime} ∪ {p. p < x ∧ p ∉ prime}`

lemma prime_partition_le:

`  {p. p ≤ x} = {p. p ≤ x ∧ p ∈ prime} ∪ {p. p ≤ x ∧ p ∉ prime}`

lemma all_nonprime_set_l:

`  [| finite A; ∀x∈A. x ∉ prime |] ==> setsum lprime A = 0`

lemma finite_A:

`  finite {y. y ∈ {0..x} ∧ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)}`

lemma finite_B:

`  finite {y. y ∈ {0..x} ∧ ¬ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)}`

lemma A_B_disjoint:

```  {y. y ∈ {0..x} ∧ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)} ∩
{y. y ∈ {0..x} ∧ ¬ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)} =
{}```

lemma A_B_all:

```  {y. y ∈ {0..x} ∧ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)} ∪
{y. y ∈ {0..x} ∧ ¬ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)} =
{y. y ≤ x}```

lemma cor_psi_sum:

```  psi x =
setsum Lambda {y. y ∈ {0..x} ∧ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)} +
setsum Lambda {y. y ∈ {0..x} ∧ ¬ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)}```

lemma B_kernel_for_Lambda:

`  y ∈ {y. y ∈ {0..x} ∧ ¬ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)} ==> Lambda y = 0`

lemma sum_over_B_of_Lambda_zero:

`  setsum Lambda {y. y ∈ {0..x} ∧ ¬ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)} = 0`

lemma inj_on_C:

`  inj_on (%y. fst y ^ snd y) {(p, a). p ∈ prime ∧ 0 < a ∧ p ^ a ∈ {0..x}}`

lemma range_of_C_is_A:

```  (%y. fst y ^ snd y) ` {(p, a). p ∈ prime ∧ 0 < a ∧ p ^ a ∈ {0..x}} =
{y. y ∈ {0..x} ∧ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)}```

lemma finite_C:

`  finite {(p, a). p ∈ prime ∧ 0 < a ∧ p ^ a ∈ {0..x}}`

lemma D_subset_C:

```  {(p, a). p ∈ prime ∧ a = 1 ∧ p ^ a ∈ {0..x}}
⊆ {(p, a). p ∈ prime ∧ 0 < a ∧ p ^ a ∈ {0..x}}```

lemma E_subset_C:

```  {(p, a). p ∈ prime ∧ 1 < a ∧ p ^ a ∈ {0..x}}
⊆ {(p, a). p ∈ prime ∧ 0 < a ∧ p ^ a ∈ {0..x}}```

lemma Lambda_reindex_1:

```  setsum Lambda
((%y. fst y ^ snd y) ` {(p, a). p ∈ prime ∧ 0 < a ∧ p ^ a ∈ {0..x}}) =
setsum (Lambda ˆ (%y. fst y ^ snd y))
{(p, a). p ∈ prime ∧ 0 < a ∧ p ^ a ∈ {0..x}}```

lemma psi_Lambda_eq_over_C:

```  psi x =
setsum (Lambda ˆ (%y. fst y ^ snd y))
{(p, a). p ∈ prime ∧ 0 < a ∧ p ^ a ∈ {0..x}}```

lemma psi_alt_def:

```  psi x =
(∑u∈{(p, a). p ∈ prime ∧ 0 < a ∧ p ^ a ∈ {0..x}}. Lambda (fst u ^ snd u))```

lemma C_eq_D_Un_E:

```  {(p, a). p ∈ prime ∧ 0 < a ∧ p ^ a ∈ {0..x}} =
{(p, a). p ∈ prime ∧ a = 1 ∧ p ^ a ∈ {0..x}} ∪
{(p, a). p ∈ prime ∧ 1 < a ∧ p ^ a ∈ {0..x}}```

lemma D_Int_E_empty:

```  {(p, a). p ∈ prime ∧ a = 1 ∧ p ^ a ∈ {0..x}} ∩
{(p, a). p ∈ prime ∧ 1 < a ∧ p ^ a ∈ {0..x}} =
{}```

lemma finite_D:

`  finite {(p, a). p ∈ prime ∧ a = 1 ∧ p ^ a ∈ {0..x}}`

lemma finite_E:

`  finite {(p, a). p ∈ prime ∧ 1 < a ∧ p ^ a ∈ {0..x}}`

lemma setsum_C_D_E:

```  setsum (Lambda ˆ (%y. fst y ^ snd y))
{(p, a). p ∈ prime ∧ 0 < a ∧ p ^ a ∈ {0..x}} =
setsum (Lambda ˆ (%y. fst y ^ snd y))
{(p, a). p ∈ prime ∧ a = 1 ∧ p ^ a ∈ {0..x}} +
setsum (Lambda ˆ (%y. fst y ^ snd y))
{(p, a). p ∈ prime ∧ 1 < a ∧ p ^ a ∈ {0..x}}```

lemma psi_Lambda_eq:

```  psi x =
setsum (Lambda ˆ (%y. fst y ^ snd y))
{(p, a). p ∈ prime ∧ a = 1 ∧ p ^ a ∈ {0..x}} +
setsum (Lambda ˆ (%y. fst y ^ snd y))
{(p, a). p ∈ prime ∧ 1 < a ∧ p ^ a ∈ {0..x}}```

lemma inj_on_g_F:

`  inj_on (%z. (z, 1)) {p. p ∈ prime ∧ p ∈ {0..x}}`

lemma g_image_F_is_D:

```  (%z. (z, 1)) ` {p. p ∈ prime ∧ p ∈ {0..x}} =
{(p, a). p ∈ prime ∧ a = 1 ∧ p ^ a ∈ {0..x}}```

lemma finite_F:

`  finite {p. p ∈ prime ∧ p ∈ {0..x}}`

lemma reindex_Lambda_f_g:

```  setsum (Lambda ˆ (%y. fst y ^ snd y))
{(p, a). p ∈ prime ∧ a = 1 ∧ p ^ a ∈ {0..x}} =
setsum (Lambda ˆ (%y. fst y ^ snd y) ˆ (%z. (z, 1))) {p. p ∈ prime ∧ p ∈ {0..x}}```

lemma aux1:

`  [| 1 < a; 0 < b |] ==> Suc 0 < a ^ b`

lemma aux2:

`  1 < a ∧ 1 < b ==> a < a ^ b`

lemma aux3:

`  [| p ∈ prime; 1 < a |] ==> p ^ a ∉ prime`

lemma prime_power_must_be_one:

`  [| p ∈ prime; p ^ a ∈ prime |] ==> a = 1`

lemma F_prop:

```  p ∈ {p. p ∈ prime ∧ p ∈ {0..x}} -->
Lambda (fst (p, 1) ^ snd (p, 1)) = ln (real p)```

lemma sum_over_F:

```  setsum (Lambda ˆ (%y. fst y ^ snd y) ˆ (%z. (z, 1)))
{p. p ∈ prime ∧ p ∈ {0..x}} =
setsum (ln ˆ real) {p. p ∈ prime ∧ p ∈ {0..x}}```

lemma sum_over_F2_lemma1:

```  setsum lprime {0..x} =
setsum lprime ({p. p ≤ x ∧ p ∈ prime} ∪ {p. p ≤ x ∧ p ∉ prime})```

lemma sum_over_F2_lemma2:

```  setsum lprime ({p. p ≤ x ∧ p ∈ prime} ∪ {p. p ≤ x ∧ p ∉ prime}) =
setsum lprime {p. p ≤ x ∧ p ∈ prime} + setsum lprime {p. p ≤ x ∧ p ∉ prime}```

lemma l_set_of_primes:

`  ∀x∈P. x ∈ prime ==> setsum lprime P = setsum (ln ˆ real) P`

lemma sum_over_F2:

`  setsum (ln ˆ real) {p. p ∈ prime ∧ p ∈ {0..x}} = theta x`

lemma psi_theta_sum:

```  psi x =
theta x +
setsum (Lambda ˆ (%y. fst y ^ snd y))
{(p, a). p ∈ prime ∧ 1 < a ∧ p ^ a ∈ {0..x}}```

lemma exponent_eq_0_iff:

`  [| 2 ≤ p; Suc 0 = p ^ a |] ==> a = 0`

lemma Lambda_positive:

`  ∀x∈{(p, a). p ∈ prime ∧ 1 < a ∧ p ^ a ∈ {0..x}}. 0 ≤ Lambda (fst x ^ snd x)`

lemma real_power_ln:

`  [| 1 < a; 0 < x |] ==> (a ^ b ≤ x) = (real b ≤ ln (real x) / ln (real a))`

lemma extent_of_E2:

```  {(p, a). p ∈ prime ∧ 1 < a ∧ p ^ a ∈ {0..x}}
⊆ {1..nat ⌊real x powr (1 / 2)⌋} × {1..nat ⌊ln (real x) / ln 2⌋}```

lemma card_E2_lemma:

```  card {(p, a). p ∈ prime ∧ 1 < a ∧ p ^ a ∈ {0..x}}
≤ card ({1..nat ⌊real x powr (1 / 2)⌋} × {1..nat ⌊ln (real x) / ln 2⌋})```

lemma card_E2_lemma2:

```  card ({1..nat ⌊real x powr (1 / 2)⌋} × {1..nat ⌊ln (real x) / ln 2⌋}) =
card {1..nat ⌊real x powr (1 / 2)⌋} * card {1..nat ⌊ln (real x) / ln 2⌋}```

lemma card_E2_lemma3:

```  card ({1..nat ⌊real x powr (1 / 2)⌋} × {1..nat ⌊ln (real x) / ln 2⌋})
≤ card {1..nat ⌊real x powr (1 / 2)⌋} * card {1..nat ⌊ln (real x) / ln 2⌋}```

lemma card_E2:

```  card {(p, a). p ∈ prime ∧ 1 < a ∧ p ^ a ∈ {0..x}}
≤ card {1..nat ⌊real x powr (1 / 2)⌋} * card {1..nat ⌊ln (real x) / ln 2⌋}```

lemma card_E2_real_lemma4:

`  real ⌊ln (real x) / ln 2⌋ ≤ ln (real x) / ln 2`

lemma real_card_E2:

```  real (card {(p, a). p ∈ prime ∧ 1 < a ∧ p ^ a ∈ {0..x}})
≤ real (card {1..nat ⌊real x powr (1 / 2)⌋} *
card {1..nat ⌊ln (real x) / ln 2⌋})```

lemma card_E2_real_lemma6:

`  0 < x ==> real (card {1..nat ⌊ln (real x) / ln 2⌋}) ≤ ln (real x) / ln 2`

lemma card_E2_real:

```  0 < x
==> real (card {(p, a). p ∈ prime ∧ 1 < a ∧ p ^ a ∈ {0..x}})
≤ real (nat ⌊real x powr (1 / 2)⌋) * ln (real x) / ln 2```

lemma E_bound_with_f:

`  y ∈ {(p, a). p ∈ prime ∧ 1 < a ∧ p ^ a ∈ {0..x}} --> fst y ^ snd y ≤ x`

lemma Lambda_prop:

`  ∀x. 0 < x --> Lambda x ≤ ln (real x)`

lemma E_bound:

```  [| 0 < x; y ∈ {(p, a). p ∈ prime ∧ 1 < a ∧ p ^ a ∈ {0..x}} |]
==> (Lambda ˆ (%y. fst y ^ snd y)) y ≤ ln (real x)```

lemma sum_over_E2_of_Lambda_o_f:

```  0 < x
==> setsum (Lambda ˆ (%y. fst y ^ snd y))
{(p, a). p ∈ prime ∧ 1 < a ∧ p ^ a ∈ {0..x}}
≤ real (nat ⌊real x powr (1 / 2)⌋) * ln (real x) * ln (real x) / ln 2```

lemma psi_theta_bound_for_real_aux:

```  0 < x
==> psi x
≤ theta x +
real (nat ⌊real x powr (1 / 2)⌋) * ln (real x) * ln (real x) / ln 2```

lemma psi_theta_bound_for_real:

```  0 < x
==> psi x ≤ theta x + real x powr (1 / 2) * ln (real x) * ln (real x) / ln 2```

### Comparing pi and theta

lemma pi_set_zero:

`  [| finite A; ∀x∈A. x ∉ prime |] ==> setsum char_prime A = 0`

lemma setsum_prime_split:

```  setsum f {p. p ≤ x} =
setsum f {p. p ≤ x ∧ p ∈ prime} + setsum f {p. p ≤ x ∧ p ∉ prime}```

lemma setsum_char_prime_zero:

`  setsum char_prime {p. p ≤ x ∧ p ∉ prime} = 0`

lemma pi_setsum_equiv:

`  Chebyshev1.pi x = setsum char_prime {p. p ≤ x}`

lemma pi_sumr_equiv:

`  Chebyshev1.pi x = sumr 0 (x + 1) char_prime`

lemma pi_Suc:

`  Chebyshev1.pi (Suc x) = char_prime (Suc x) + Chebyshev1.pi x`

lemma char_prime_def_eq:

`  1 ≤ n ==> (theta (n + 1) - theta n) / ln (real (n + 1)) = char_prime (n + 1)`

lemma nat_int_inj_on:

`  inj_on nat {p. p ∈ zprime ∧ p dvd x}`

lemma int_nat_inj_on:

`  inj_on int {p. p ∈ prime ∧ p dvd x}`

### Expressing ln in terms of Lambda

lemma ln_product_sum:

`  [| finite A; ∀x∈A. 0 < f x |] ==> ln (setprod f A) = setsum (ln ˆ f) A`

lemma multiplicity_eq_1:

```  1 < n
==> ln (real n) =
ln (∏p∈{p. 0 < p ∧ p ∈ zprime ∧ p dvd n}. real p ^ multiplicity p n)```

lemma divisor_set_fact:

`  1 < n ==> {p. 0 < p ∧ p ∈ zprime ∧ p dvd n} ⊆ {- n..n}`

lemma multiplicity_eq_2:

```  1 < n
==> ln (real n) =
(∑p | 0 < p ∧ p ∈ zprime ∧ p dvd n. ln (real p ^ multiplicity p n))```

lemma multiplicity_eq_3:

```  1 < n
==> ln (real n) =
(∑p | 0 < p ∧ p ∈ zprime ∧ p dvd n. real (multiplicity p n) * ln (real p))```

lemma finite_G:

`  0 < x ==> finite {d. 0 < d ∧ d dvd x}`

lemma G_fact:

```  0 < x
==> {d. 0 < d ∧ d dvd x} =
{d. 0 < d ∧ d dvd x} ∩
{y. y ∈ {0..x} ∧ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)} ∪
{d. 0 < d ∧ d dvd x} ∩
{y. y ∈ {0..x} ∧ ¬ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)}```

lemma Lambda_over_G_lemma1:

```  0 < x
==> setsum Lambda {d. 0 < d ∧ d dvd x} =
setsum Lambda
({d. 0 < d ∧ d dvd x} ∩
{y. y ∈ {0..x} ∧ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)} ∪
{d. 0 < d ∧ d dvd x} ∩
{y. y ∈ {0..x} ∧ ¬ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)})```

lemma Lambda_over_G_lemma2:

```  0 < x
==> setsum Lambda {d. 0 < d ∧ d dvd x} =
setsum Lambda
({d. 0 < d ∧ d dvd x} ∩
{y. y ∈ {0..x} ∧ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)}) +
setsum Lambda
({d. 0 < d ∧ d dvd x} ∩
{y. y ∈ {0..x} ∧ ¬ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)})```

lemma Lambda_over_G_lemma3:

```  0 < x
==> setsum Lambda
({d. 0 < d ∧ d dvd x} ∩
{y. y ∈ {0..x} ∧ ¬ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)}) =
0```

lemma Lambda_over_G_lemma4:

```  0 < x
==> setsum Lambda {d. 0 < d ∧ d dvd x} =
setsum Lambda
({d. 0 < d ∧ d dvd x} ∩
{y. y ∈ {0..x} ∧ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)})```

lemma G_Int_A_Un_over_J:

```  {d. 0 < d ∧ d dvd x} ∩ {y. y ∈ {0..x} ∧ (∃p a. p ∈ prime ∧ 0 < a ∧ p ^ a = y)} =
(UN p:{p. p ∈ prime ∧ p dvd x}.
{y. y ∈ {0..x} ∧ (∃a. 0 < a ∧ p ^ a = y)} ∩ {d. 0 < d ∧ d dvd x})```

lemma finite_J:

`  0 < x ==> finite {p. p ∈ prime ∧ p dvd x}`

lemma finite_H_p:

`  0 < x ==> finite {y. y ∈ {0..x} ∧ (∃a. 0 < a ∧ p ^ a = y)}`

lemma different_H:

```  [| 0 < x; p1 ∈ prime; p2 ∈ prime; p1 ≠ p2 |]
==> {y. y ∈ {0..x} ∧ (∃a. 0 < a ∧ p1 ^ a = y)} ∩
{y. y ∈ {0..x} ∧ (∃a. 0 < a ∧ p2 ^ a = y)} =
{}```

lemma setsum_Lambda_G_lemma1:

```  0 < x
==> setsum Lambda {d. 0 < d ∧ d dvd x} =
(∑p | p ∈ prime ∧ p dvd x.
setsum Lambda
({y. y ∈ {0..x} ∧ (∃a. 0 < a ∧ p ^ a = y)} ∩ {d. 0 < d ∧ d dvd x}))```

lemma inj_on_prime_power:

`  inj_on (op ^ p) {1..nmult p x}`

lemma nat_int_dvd:

`  (int x dvd int y) = (x dvd y)`

lemma nat_zmult_multiplicity_lemma1:

`  int p ^ multiplicity (int p) (int n) dvd int n`

lemma nat_zmult_multiplicity_lemma2:

`  int (p ^ multiplicity (int p) (int n)) dvd int n`

lemma nat_zmult_multiplicity:

`  p ^ multiplicity (int p) (int n) dvd n`

lemma power_dvd_prop:

`  [| p ^ b dvd x; a ≤ b |] ==> p ^ a dvd x`

lemma power_le_prop1:

`  [| 1 ≤ p; a ≤ b |] ==> p ^ a ≤ p ^ b`

lemma power_le_prop:

`  [| 1 < p; p ^ b ≤ x; a ≤ b |] ==> p ^ a ≤ x`

lemma nat_zmult_multiplicity_le:

`  0 < n ==> p ^ multiplicity (int p) (int n) ≤ n`

lemma multiplicity_power_dvd:

`  [| 0 < n; p ∈ prime |] ==> (k ≤ multiplicity (int p) (int n)) = (p ^ k dvd n)`

lemma multiplicity_power_dvd_imp1:

`  [| 0 < n; p ∈ prime; p ^ k dvd n |] ==> k ≤ multiplicity (int p) (int n)`

lemma G_Int_Hp_eq:

```  [| 0 < x; p ∈ prime |]
==> op ^ p ` {1..nmult p x} =
{d. 0 < d ∧ d dvd x} ∩ {y. y ∈ {0..x} ∧ (∃a. 0 < a ∧ p ^ a = y)}```

lemma card_multiplicity_eq:

```  [| 0 < x; p ∈ prime |]
==> card ({d. 0 < d ∧ d dvd x} ∩ {y. y ∈ {0..x} ∧ (∃a. 0 < a ∧ p ^ a = y)}) =
multiplicity (int p) (int x)```

lemma setsum_Lambda_G_int_Hp:

```  [| 0 < x; p ∈ prime |]
==> setsum Lambda
({d. 0 < d ∧ d dvd x} ∩ {y. y ∈ {0..x} ∧ (∃a. 0 < a ∧ p ^ a = y)}) =
ln (real p) * real (multiplicity (int p) (int x))```

lemma setsum_Lambda_G_lemma2:

```  0 < x
==> setsum Lambda {d. 0 < d ∧ d dvd x} =
(∑p | p ∈ prime ∧ p dvd x.
ln (real p) * real (multiplicity (int p) (int x)))```

lemma multiplicity_eq_4:

```  0 < n
==> ln (real n) =
(∑p | 0 < p ∧ p ∈ zprime ∧ p dvd n. real (multiplicity p n) * ln (real p))```

lemma multiplicity_eq_5:

```  0 < n
==> ln (real n) =
(∑p | 0 < p ∧ p ∈ prime ∧ p dvd n.
real (multiplicity (int p) (int n)) * ln (real p))```

lemma ln_eq_setsum_Lambda:

`  0 < n ==> ln (real n) = setsum Lambda {d. d dvd n}`

lemma ln_eq_setsum_Lambda2:

```  0 < n
==> ln (real n) =
(∑x∈{(p, a). 0 < a ∧ p ∈ prime ∧ p ^ a dvd n}. ln (real (fst x)))```