# Theory EulerPhi

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

theory EulerPhi = NatIntLib:

```(*  Title:      EulerPhi.thy
Author:     David Gray
*)

header {* Euler's phi function *}

theory EulerPhi = NatIntLib:;

constdefs
phi :: "int => int"
"phi n == int (card({(x::int). (1 <= x) & (x <= n) & (zgcd(x, n) = 1)}))";

locale PHI =
fixes n  :: "int"
fixes S  :: "int set"
fixes I  :: "int set"
fixes I2 :: "int set"
fixes A  :: "int => int set"
fixes B  :: "int => int set"
fixes f  :: "int => int"

assumes n_ge_1:  "1 <= n"

defines S_def:  "S   == {x. 1 <= x & x <= n}"
defines I_def:  "I   == {d. 0 <= d & d dvd n}"
defines I2_def: "I2  == {d. 1 <= d & d dvd n}"
defines A_def:  "A d == {k. (k:S) & zgcd(k, n) = d}"
defines B_def:  "B d == {l. (1::int) <= l & l <= (n div d) & zgcd(l, (n div d)) = 1}"
defines f_def:  "f d == n div d";

lemma (in PHI) n_dvd_range: "[| d dvd n; 0 <= d|] ==> 1 <= d & d <= n";
proof -;
assume "d dvd n" and "0 <= d";
then have "1 <= d";
apply (insert prems n_ge_1, auto);
apply (subgoal_tac "0 ~= d", auto);
done;
moreover have "d <= n";
apply (insert prems n_ge_1, auto);
apply (frule zdvd_bounds, auto);
done;
ultimately show ?thesis by auto;
qed;

lemma (in PHI) n_zgcd_range: "[| 1 <= x; x <= n |] ==> 1 <= zgcd (x, n) & zgcd (x, n) <= n";
apply (insert zgcd_zdvd2 [of x n]);
apply (rule n_dvd_range, auto simp add: zgcd_def);
done;

lemma (in PHI) zgcd_elem_S: "[| 1 <= x; x <= n |] ==> zgcd (x, n):S";
by (auto simp add: S_def n_zgcd_range);

lemma (in PHI) S_finite: "finite S";
apply (subgoal_tac "S <= {1..n}");
apply (erule finite_subset);
apply simp;
apply (unfold S_def);
apply auto;
done;

lemma (in PHI) I_sub_S: "I <= S";
by (auto simp add: S_def I_def n_dvd_range );

lemma (in PHI) I_finite: "finite I";
by (insert I_sub_S S_finite, auto simp add: finite_subset);

lemma (in PHI) I_elem_prop: "d:I ==> 1 <= d";
apply (subgoal_tac "d ~= 0");
apply (insert n_ge_1, auto simp add: I_def);
done;

lemma (in PHI) I_eq_I2: "I = I2";
by (auto simp add: n_ge_1 I_def I2_def n_dvd_range);

lemma (in PHI) A_sub_S: "A(d) <= S";
by (auto simp add: S_def A_def);

lemma (in PHI) A_finite: "finite(A(d))";
by (insert A_sub_S [of d] S_finite, auto simp add: finite_subset);

lemma (in PHI) B_sub_S: "d:I ==> B(d) <= S";
proof;
fix x;
assume "d:I" and "x:B(d)";
then have "x <= n";
proof-;
from prems have "x <= n div d" by auto;
also have "n div d <= n div 1";
proof-;
from PHI_def prems have "1 <= n"; by auto;
then have "0 <= n" by auto;
moreover have "(0::int) < 1" by auto;
moreover from prems have "1 <= d" by (insert prems, auto simp add: I_elem_prop);
ultimately show "n div d <= n div 1" by (rule zdiv_mono2);
qed;
also have "n div 1 = n" by auto;
finally show "x <= n".;
qed;
moreover from prems have "1 <= x" by auto;
ultimately show "x:S" by (auto simp add: S_def);
qed;

lemma (in PHI) B_finite: "d:I ==> finite(B(d))";
apply (drule B_sub_S, insert S_finite);
apply (auto simp add: finite_subset);
done;

(* "Lemma 1" *)
lemma (in PHI) S_eq_UNION_A: "S = UNION I A";
proof -;
have "UNION I A <= S" by (auto simp add: S_def A_def);
moreover have "S <= UNION I A";
proof -;
have "S <= UNION I2 A"
by (insert n_zgcd_range, auto simp add: S_def A_def I2_def);
also have "I2 = I" by (auto simp add: I_eq_I2);
finally show "S <= UNION I A".;
qed;
ultimately show ?thesis by auto;
qed;

(* "Lemma 2" *)
lemma (in PHI) A_disj_prop: "ALL d1:I. ALL d2:I. d1 ~= d2 --> A(d1) Int A(d2) = {}";
by (auto simp add: A_def);

(* "Lemma 3" *)
lemma (in PHI) n_eq_Sum_card_A: "n = setsum (%x. int(card (A(x)))) I";
proof -;
have "n = int(card S)";
apply (insert n_ge_1, auto simp add: S_def);
apply (subgoal_tac "{x. 1 <= x & x <= n} = {x. 0 < x & x <= n}");
apply (rule ssubst, force);
apply (subgoal_tac "{x. 0 < x & x <= n} = {)0..n}");
apply (erule ssubst);back;
apply simp;
apply force;
apply auto;
done;
also have "S = UNION I A" by (rule S_eq_UNION_A);
also have "int (card (UNION I A)) = setsum (%x. int (card (A(x)))) I";
apply (subst card_UN_disjoint);
apply (auto simp add: I_finite A_finite A_disj_prop);
apply (subst int_setsum);
apply (simp add: o_def);
done;
finally show ?thesis .;
qed;

(* "Lemma 4" *)
lemma (in PHI) zgcd_div_prop: "d:S ==> (zgcd(k, n) = d) =
(d dvd k & d dvd n & zgcd(k div d, n div d) = 1)";
proof -;
assume "d: S";
with S_def have "0 < d"; by auto;
thus ?thesis;
by (rule zgcd_equiv);
qed;

(* "Lemma 5" *)
lemma (in PHI) A_inj_prop: "d:I ==> inj_on (%(k::int). k div d) (A(d))";
proof (auto simp add: inj_on_def);
fix x and y;
assume "d:I" and "x div d = y div d" and
p1: "x:A(d)" and p2: "y:A(d)";
then have "(x div d) * d = (y div d) * d" by auto;
also have "(x div d) * d = x";
proof -;
have "d dvd x" by (insert p1, auto simp add: A_def);
then show "(x div d) * d = x" by (auto simp add: dvd_def);
qed;
also have "(y div d) * d = y";
proof -;
have "d dvd y" by (insert p2, auto simp add: A_def);
then show "(y div d) * d = y" by (auto simp add: dvd_def);
qed;
finally; show "x = y" .;
qed;

(* "Lemma 6" *)
lemma (in PHI) image_A_eq_B: "d:I ==> (%(k::int). k div d) ` A(d) = B(d)";
proof (auto);
fix k;
assume "d:I" and "k:A(d)";
then show "(k div d):B(d)";
proof -;
from prems have "1 <= k div d";
proof (auto simp add: A_def I_def S_def);
assume "1 <= k";
then have "0 < k & 0 < zgcd(k,n) & zgcd(k,n) dvd k" by (auto simp add: zgcd_gr_zero1);
then have "0 < k div zgcd(k,n)" by (auto simp add: zdiv_gr_zero);
thus "1 <= k div zgcd(k,n)" by arith;
qed;
moreover from prems have "k div d <= n div d";
proof (auto simp add: A_def I_def S_def);
assume "1 <= k";
then have "0 < zgcd(k,n)" by (auto simp add: zgcd_gr_zero1);
thus "k div zgcd (k, n) <= n div zgcd (k, n)";
by (insert prems, auto simp add: zdiv_mono1);
qed;
moreover from prems have "zgcd(k div d, n div d) = 1";
proof (auto simp add: A_def I_def S_def);
assume "1 <= k" and "k <= n";
then have p1:"zgcd (k, n):S" by (auto simp add: zgcd_elem_S);
thus "zgcd (k div zgcd (k, n), n div zgcd (k, n)) = 1";
apply (insert p1);
apply (frule zgcd_div_prop, auto);
done;
qed;
ultimately show "(k div d):B(d)" by (auto simp add: B_def);
qed;
next;
fix y;
assume q: "d:I" and "y:B(d)";
then show "y:(%k. k div d) ` A d";
proof (auto simp add: image_def);
have a1:"(y * d):A(d)";
proof-;
have "1 <= y * d";
proof-;
from prems have "0 < (y * d)"
by (insert I_elem_prop [of d], auto simp add: mult_pos);
thus "1 <= (y * d)" by arith;
qed;
moreover have "y * d <= n";
proof-;
from prems have "y <= n div d" by auto;
with prems have "y * d <= (n div d) * d"
by (auto simp add: mult_right_mono);
also have "... = n";
proof -;
from prems have "d dvd n" by auto;
thus "(n div d) * d = n" by (auto simp add: dvd_def);
qed;
finally show "y * d <= n".;
qed;
moreover have "zgcd(y * d, n) = d";
proof-;
from prems have p1: "d dvd (y * d) & d dvd n & zgcd( (y * d) div d, n div d) = 1";
by (auto simp add: B_def);
moreover from prems have p2: "d:S" by (insert prems I_sub_S, auto);
ultimately show "zgcd(y * d, n) = d"
by (insert p1 p2 zgcd_div_prop [of d "y * d"], auto);
qed;
ultimately show "(y * d):A(d)" by (auto simp add: A_def S_def);
qed;
moreover have a2: "y = (y * d) div d" by (insert prems, auto simp add: dvd_def);
ultimately show "EX x:A d. y = x div d"
apply (insert a1 a2)
apply (rule bexI, auto);
done;
qed;
qed;

(* Cor 1 *)
lemma (in PHI) card_A_eq_phi: "d:I ==> int(card (A(d))) = phi(n div d)";
proof-;
assume "d:I";
have "card(A(d)) = card((%(k::int). k div d) ` A(d))";
proof-;
have "finite( A(d))" by (auto simp add: A_finite);
moreover have "inj_on (%(k::int). k div d) (A(d))";
by (rule A_inj_prop, insert prems, auto);
ultimately show "card(A(d)) = card((%(k::int). k div d) ` A(d))";
by (auto simp add: card_image);
qed;
also have "(%(k::int). k div d) ` A(d) = B(d)";
by (rule image_A_eq_B, insert prems, auto);
finally have "int(card (A(d)) ) = int (card (B(d)))" by (auto);
also have "... = phi (n div d)";
by (auto simp add: B_def phi_def);
finally show ?thesis .;
qed;

(* Cor 2 *)
lemma (in PHI) n_eq_setsum_phi: "n = setsum (phi ˆ f) I";
proof-;
have "n = setsum (%x. int(card (A(x)))) I";
by (auto simp add: n_eq_Sum_card_A);
also have "... = setsum (%d. phi (n div d)) I";
proof-;
have "finite I" by (auto simp add: I_finite);
moreover have "ALL x:I. (%x. int(card (A(x)))) x =  (%d. phi (n div d)) x";
by (auto simp add: card_A_eq_phi);
ultimately show "setsum (%x. int(card (A(x)))) I = setsum (%d. phi (n div d)) I"
apply (intro setsum_cong);
apply auto;
done;
qed;
also have "... = setsum (phi ˆ f) I";
proof-;
have "finite I" by (auto simp add: I_finite);
moreover have "ALL x:I. (%d. phi (n div d)) x = (phi ˆ f) x";
by (auto simp add: f_def);
ultimately show "setsum (%d. phi (n div d)) I = setsum (phi ˆ f) I";
by (intro setsum_cong, auto);
qed;
finally show ?thesis .;
qed;

lemma (in PHI) I_inj_prop: "inj_on f I";
proof (auto simp add: inj_on_def f_def I_def);
fix x and y;
assume x1:"x dvd n" and x2: "0 <= x" and
y1:"y dvd n" and y2: "0 <= y" and "n div x = n div y";
then have p1: "y * (n div x) * x = y * (n div y) * x";
by (auto);
also have "y * (n div x) * x = y * n";
by (insert x1 x2 p1, auto simp add: dvd_def);
also have "y * (n div y) * x = n * x";
by (insert y1 y2 p1, auto simp add: dvd_def);
finally have "n * x = n * y" by auto;
thus "x = y" by (insert n_ge_1, auto);
qed;

lemma (in PHI) f_image_I_eq_I: "f ` I = I";
proof (auto);
fix x;
assume "x:I";
thus "(f x):I";
proof-;
have "0 <= n div x";
proof-;
have "0 <= n & 0 < x" by (insert prems, frule I_elem_prop,
auto simp add: PHI_def);
then have "0 div x <= n div x"
apply (clarify);
apply (rule zdiv_mono1, auto);
done;
also have "0 div x = 0" by auto;
finally show "0 <= n div x".;
qed;
moreover have "(n div x) dvd n" by (insert prems, auto simp add: I_def dvd_def);
ultimately show "(f x):I" by (auto simp add: f_def I_def);
qed;
next;
fix x;
assume "x:I";
thus "x : f ` I";
proof (auto simp add: image_def f_def);
have a1: "(n div x):I";
proof-;
have "0 <= n div x";
proof-;
have "0 <= n & 0 < x" by (insert prems, frule I_elem_prop,
auto simp add: PHI_def);
then have "0 div x <= n div x"
apply (clarify);
apply (rule zdiv_mono1, auto);
done;
also have "0 div x = 0" by auto;
finally show "0 <= n div x".;
qed;
moreover have "(n div x) dvd n" by (insert prems, auto simp add: I_def dvd_def);
ultimately show "(n div x):I" by (auto simp add: I_def);
qed;
moreover have a2: "x = n div (n div x)";
proof -;
from prems and PHI_def have "0 < n" by auto;
moreover have "0 < x"
apply (insert prems);
apply (frule I_elem_prop, auto);
done;
moreover from prems have "x dvd n" by auto;
ultimately have "n div (n div x) = x" by (auto simp add: zdiv_zdiv_prop);
thus "x = n div (n div x)" by auto;
qed;
ultimately show "EX y:I. x = n div y";
apply (insert a1 a2);
apply (rule bexI, auto);
done;
qed;
qed;

(* Finally! *)
theorem (in PHI) big_prop1: "n = setsum (%d. phi(d)) I";
proof-;
have "n = setsum (phi ˆ f) I" by (auto simp add: n_eq_setsum_phi);
also have "... = setsum (%d. phi(d)) (f ` I)";
proof -;
have "finite I" by (auto simp add: I_finite);
moreover have "inj_on f I" by (auto simp add: I_inj_prop);
ultimately have "setsum (%d. phi(d)) (f ` I) = setsum (phi ˆ f) I";
by (rule setsum_reindex);
thus "setsum (phi ˆ f) I = setsum (%d. phi(d)) (f ` I)" by auto;
qed;
also have "... = setsum (%d. phi(d)) I";
by (auto simp add: f_image_I_eq_I);
finally show ?thesis .;
qed;

lemma card_gcd_set: "[| p:zprime; 0 < k |] ==>
int(card({x. 1 <= x & x <= p^k & zgcd(x,p^k) ~= 1})) = p^(k - 1)";
proof-;
assume "p:zprime" and "0 < k";
then have "{x. 1 <= x & x <= p^k & zgcd(x,p^k) ~= 1} =
{x. 1 <= x & x <= p^k & p dvd x}";
by (auto simp add: gcd_prime_power_iff_zdvd_prop);
also have "... = {x. EX y.(1 <= y & y <= p^(k - 1) & x = p * y)}";
proof;
show "{x. 1 <= x & x <= p ^ k & p dvd x} <=
{x. EX y. 1 <= y & y <= p ^ (k - 1) & x = p * y}";
proof (auto, rule_tac x = "x div p" in exI, auto);
fix x;
assume "1 <= x" and "x <= p ^ k" and "p dvd x";
thus "1 <= x div p";
proof -;
have "0 < x & 0 < p & 0 < x div p";
by (insert prems, auto simp add: zprime_def zdiv_gr_zero);
thus "1 <= x div p" by auto;
qed;
next;
fix x;
assume "1 <= x" and "x <= p ^ k" and "p dvd x";
thus "x div p <= p ^ (k - Suc 0)";
proof -;
have "x div p <= (p ^ k) div p";
by (insert prems, auto simp add: zprime_def zdiv_mono1);
also have "(p ^ k) div p = p ^ (k - 1)";
by (insert prems, auto simp add: zpower_minus_one zprime_def);
finally show "x div p <= p ^ (k - Suc 0)" by auto;
qed;
next;
fix x;
assume "1 <= x" and "x <= p ^ k" and "p dvd x";
thus "x = p * (x div p)" by (auto simp add: dvd_def);
qed;
next;
show "{x. EX y. 1 <= y & y <= p ^ (k - 1) & x = p * y} <= {x. 1 <= x & x <= p ^ k & p dvd x}";
proof (auto);
fix y;
assume "1 <= y" and "y <= p ^ (k - Suc 0)";
thus "1 <= p * y";
proof -;
have "0 < y & 0 < p" by (insert prems, auto simp add: zprime_def);
then have "0 < p * y" by (auto simp add: mult_pos);
thus "1 <= p * y" by auto;
qed;
next;
fix y;
assume "1 <= y" and "y <= p ^ (k - Suc 0)";
thus "p * y <= p ^ k";
proof -;
have "y * p <= (p ^ (k - 1)) * p";
by (insert prems, auto simp add: zprime_def mult_right_mono);
also have "(p ^ (k - 1)) * p = p ^ k";
by (insert prems, auto simp add: zpower_zmult zprime_def);
finally show "p * y <= p ^ k" by (auto simp add: zmult_ac);
qed;
qed;
qed;
finally; have "card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1} =
card {x. EX y. 1 <= y & y <= p ^ (k - 1) & x = p * y}"; by auto;
also have "... = card {y. 1 <= y & y <= p^(k - 1)}";
proof-;
have "finite({y. 1 <= y & y <= p ^ (k - 1)})";
proof-;
have "finite({y. 0 < y & y <= p ^ (k - 1)})";
apply (subgoal_tac "{y. 0 < y ∧ y ≤ p ^ (k - 1)} =
{)0..p ^ (k - 1)}");
apply (erule ssubst);
apply auto;
done;
also have "{y. 0 < y & y <= p ^ (k - 1)} =
{y. 1 <= y & y <= p ^ (k - 1)}" by auto;
finally show "finite({y. 1 <= y & y <= p ^ (k - 1)})".;
qed;
moreover have "inj_on (%y.(p::int)*y) {y. 1 <= y & y <= p ^ (k - 1)}";
by (insert prems, auto simp add: inj_on_def zprime_def);
ultimately have "card ((%y.(p::int)*y) ` {y. 1 <= y & y <= p ^ (k - 1)}) =
card {y. 1 <= y & y <= p ^ (k - 1)}";
by (rule_tac A = "{y. 1 <= y & y <= p ^ (k - 1)}" in card_image);
also have "(%y.(p::int)*y) ` {y. 1 <= y & y <= p ^ (k - 1)} =
{x. EX y. 1 <= y & y <= p ^ (k - 1) & x = p * y}" by (auto);
finally show "card {x. EX y. 1 <= y & y <= p ^ (k - 1) & x = p * y} =
card {y. 1 <= y & y <= p ^ (k - 1)}".;
qed;
also have "{y. 1 <= y & y <= p ^ (k - 1)} = {y. 0 < y & y <= p ^ (k - 1)}" by auto;
finally have "int (card({x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1})) =
int (card({y. 0 < y & y <= p ^ (k - 1)}))";
by auto;
also have "... = p ^ (k - 1)";
apply (subgoal_tac "{y. 0 < y ∧ y ≤ p ^ (k - 1)} = {)0.. p^(k - 1)}");
apply (erule ssubst);
apply (subgoal_tac "0 <= p ^ (k - 1)");
apply simp;
apply (rule zero_le_power);
apply (rule order_less_imp_le);
apply (insert prems, auto simp add: zprime_def);
done;
finally show "int (card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}) = p ^ (k - 1)".;
qed;

theorem big_prop2: " [| p : zprime; 0 < k |] ==> phi(p^k) = (p^k) - (p^(k - 1))";
proof -;
assume "p : zprime" and "0 < k";
then have p:"0 <= p ^ k"
proof-;
have "0 < p" by (insert prems, auto simp add: zprime_def);
then have "0 < p ^ k" by (rule zpower_gr_0);
thus "0 <= p ^ k" by auto;
qed;
then have "p^k = int (card {x. 0 < x & x <= p^k})";
apply (subgoal_tac "{x. 0 < x & x <= p^k} = {)0..p^k}");
apply auto;
done;
also have "{x. 0 < x & x <= p^k} = {x. 1 <= x & x <= p^k}" by auto;
also have "... = {x. 1 <= x & x <= p^k & zgcd(x,p^k) = 1} Un
{x. 1 <= x & x <= p^k & zgcd(x,p^k) ~= 1}" by auto;
finally have "p ^ k = int (card ({x. 1 <= x & x <= p^k & zgcd(x,p^k) = 1} Un
{x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}))".;
also have "card ({x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1} Un
{x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}) =
card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1} +
card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}";
proof-;
have "finite {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1}";
proof-;
have "finite {x. 1 <= x & x <= p ^ k}";
proof-;
from p have "finite {x. 0 < x & x <= p ^ k}";
apply (subgoal_tac "{x. 0 < x & x <= p ^ k} = {)0..p^k}");
apply auto;
done;
also have "{x. 0 < x & x <= p ^ k} = {x. 1 <= x & x <= p ^ k}"
by (auto);
finally show "finite {x. 1 <= x & x <= p ^ k}".;
qed;
moreover have "{x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1} <=
{x. 1 <= x & x <= p ^ k}";
by auto;
ultimately show "finite {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1}";
by (auto simp add: finite_subset);
qed;
moreover have "finite {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}";
proof-;
have "finite {x. 1 <= x & x <= p ^ k}";
proof-;
from p have "finite {x. 0 < x & x <= p ^ k}";
apply (subgoal_tac "{x. 0 < x & x <= p ^ k} = {)0..p^k}");
apply auto;
done;
also have "{x. 0 < x & x <= p ^ k} = {x. 1 <= x & x <= p ^ k}"
by (auto);
finally show "finite {x. 1 <= x & x <= p ^ k}".;
qed;
moreover have "{x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1} <=
{x. 1 <= x & x <= p ^ k}";
by auto;
ultimately show "finite {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}";
by (auto simp add: finite_subset);
qed;
moreover have "{x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1} Int
{x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1} = {}";
by auto;
ultimately show "card ({x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1} Un
{x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}) =
card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1} +
card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}";
by (rule_tac A = "{x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1}"
in card_Un_disjoint, auto);
qed;
also; have "int (card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1} +
card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}) =
int (card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1}) +
int (card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1})";
by (auto);
also have "int( card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}) =
p ^ (k - 1)";
by (insert prems, auto simp add: card_gcd_set);
also have "int( card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1})
= phi(p^k)";
by (auto simp add: phi_def);
finally have "p ^ k = phi (p ^ k) + p ^ (k - 1)".;
thus "phi (p ^ k) = p ^ k - p ^ (k - 1)";
by (auto);
qed;

locale PHI2 =
fixes n        :: "int"
fixes m        :: "int"
fixes f        :: "int => (int * int)"
fixes SR       :: "int => int set"
fixes ResUnits :: "int => int set"

assumes n_ge_1:  "1 <= n"
assumes m_ge_1:  "1 <= m"
assumes m_n_gcd: "zgcd(m, n) = 1"

defines f_def:        "f x == (x mod m, x mod n)"
defines SR_def:       "SR y == {x. (0 <= x) & (x < y)}"
defines ResUnits_def: "ResUnits y == {x. (x:(SR(y))) & zgcd(x,y) = 1}";

lemma (in PHI2) SR_m_mod_prop: "a:SR(m) ==> a mod m = a";
apply (insert m_ge_1);
apply (auto simp add: SR_def mod_pos_pos_trivial);
done;

lemma (in PHI2) SR_n_mod_prop: "a:SR(n) ==> a mod n = a";
apply (insert n_ge_1);
apply (auto simp add: SR_def mod_pos_pos_trivial);
done;

lemma (in PHI2) SR_mn_mod_prop: "a:SR(m*n) ==> a mod (m*n) = a";
apply (insert n_ge_1 m_ge_1);
apply (auto simp add: SR_def mod_pos_pos_trivial);
done;

lemma (in PHI2) SR_m_finite: "finite(SR(m))";
apply (insert m_ge_1);
apply (auto simp add: SR_def);
apply (subgoal_tac "{x. 0 ≤ x ∧ x < m} = {0..m(}");
apply auto;
done;

lemma (in PHI2) SR_m_card: "int(card(SR(m))) = m";
apply (insert m_ge_1);
apply (auto simp add: SR_def);
apply (subgoal_tac "{x. 0 ≤ x ∧ x < m} = {0..m(}");
apply auto;
done;

lemma (in PHI2) SR_n_finite: "finite(SR(n))";
apply (insert n_ge_1);
apply (unfold SR_def);
apply (subgoal_tac "{x. 0 ≤ x ∧ x < n} = {0..n(}");
apply auto;
done;

lemma (in PHI2) SR_n_card: "int(card(SR(n))) = n";
apply (insert n_ge_1);
apply (auto simp add: SR_def);
apply (subgoal_tac "{x. 0 ≤ x ∧ x < n} = {0..n(}");
apply auto;
done;

lemma (in PHI2) SR_mn_finite: "finite(SR(m*n))";
apply (insert m_ge_1 n_ge_1);
apply (auto simp add: SR_def);
apply (subgoal_tac "{x. 0 ≤ x ∧ x < m * n} = {0..m*n(}");
apply auto;
done;

lemma (in PHI2) SR_mn_card: "int(card(SR(m*n))) = m * n";
apply (insert m_ge_1 n_ge_1);
apply (auto simp add: SR_def);
apply (subgoal_tac "{x. 0 ≤ x ∧ x < m * n} = {0..m*n(}");
apply (erule ssubst);
apply auto;
apply (subgoal_tac "0 < m*n");
apply auto;
apply (rule mult_pos);
apply auto;
done;

lemma (in PHI2) ResUnits_m_finite: "finite(ResUnits(m))";
proof-;
have "ResUnits(m) <= SR(m)" by (auto simp add: ResUnits_def);
with SR_m_finite show ?thesis by (auto simp add: finite_subset);
qed;

lemma (in PHI2) ResUnits_n_finite: "finite(ResUnits(n))";
proof-;
have "ResUnits(n) <= SR(n)" by (auto simp add: ResUnits_def);
with SR_n_finite show ?thesis by (auto simp add: finite_subset);
qed;

lemma (in PHI2) ResUnits_mn_finite: "finite(ResUnits(m * n))";
proof-;
have "ResUnits(m * n) <= SR(m * n)" by (auto simp add: ResUnits_def);
with SR_mn_finite show ?thesis by (auto simp add: finite_subset);
qed;

lemma (in PHI2) zgcd_zmult_prop: "(zgcd(m * n, x) = 1) = ((zgcd(m, x) = 1) & (zgcd(n, x) = 1))";
proof;
assume p1: "zgcd (m * n, x) = 1";
have "zgcd(n, x) dvd zgcd(m * n, x) & zgcd(m, x) dvd zgcd(m * n, x)";
apply (insert zgcd_zdvd_zgcd_zmult [of m x n]);
apply (auto simp add: zgcd_zdvd_zgcd_zmult zmult_ac);
done;
thus "zgcd(m, x) = 1 & zgcd(n , x) = 1";
apply (insert p1, insert PHI2_def, auto);
apply (drule_tac n = "zgcd(m,x)" in zdvd_bounds, auto);
apply (subgoal_tac "0 < m");
apply (drule_tac b = x in zgcd_gr_zero1, auto); defer;
apply (drule zdvd_bounds, auto);
apply (subgoal_tac "0 < n");
apply (drule_tac b = x in zgcd_gr_zero1);
apply (insert prems, auto);
done;
next;
assume "zgcd (m, x) = 1 & zgcd (n, x) = 1";
thus "zgcd (m * n, x) = 1";
by (auto simp add: zgcd_zgcd_zmult);
qed;

lemma (in PHI2) specialized_chinese: "ALL a. ALL b. EX x. ([x = a] (mod m) & [x = b] (mod n))";
proof (auto);
fix a b;
have "0 < n" by (insert prems, auto simp add: PHI2_def);
with m_n_gcd obtain u where p1:"[m*u = 1] (mod n)" using zcong_lineq_ex by auto;
have "zgcd(n, m) = 1" by (insert prems, auto simp add: zgcd_commute PHI2_def);
moreover have "0 < m" by (insert prems, auto simp add: PHI2_def);
ultimately obtain v where p2:"[n * v = 1] (mod m)" using zcong_lineq_ex by auto;
from p1 have "[m*u*b = 1*b] (mod n)" by (rule zcong_scalar);
then have "[m*u*b = b] (mod n)" by auto;
then have "[m*u*b + n*(v*a) = b] (mod n)" by (rule zcong_m_scalar_prop);
then have p3: "[m*u*b + n*v*a = b] (mod n)" by (auto simp add: zmult_ac);
from p2 have "[n*v*a = 1*a] (mod m)" by (rule zcong_scalar);
then have "[n*v*a = a] (mod m)" by auto;
then have "[n*v*a + m*(u*b) = a] (mod m)" by (rule zcong_m_scalar_prop);
then have "[n*v*a + m*u*b = a] (mod m)" by (auto simp add: zmult_ac);
then have p4: "[m*u*b + n*v*a = a] (mod m)" by (auto simp add: zadd_ac);
have "[m*u*b + n*v*a = a] (mod m) & [m*u*b + n*v*a = b] (mod n)";
by (insert p3 p4, auto);
thus "EX x. [x = a] (mod m) & [x = b] (mod n)" by (auto);
qed;

lemma (in PHI2) SR_inj_on_f: "inj_on f (SR(m * n))";
apply (auto simp add: inj_on_def f_def);
proof-;
fix x y;
assume "x : SR (m * n)" and "y : SR (m * n)" and
"x mod m = y mod m" and "x mod n = y mod n";
have p1: "0 < m & 0 < n"  by (insert m_ge_1 n_ge_1, auto);
then have "[x = y] (mod m) & [x = y] (mod n)";
by (insert prems, auto simp add: zcong_zmod_eq);
then have p2: "[x = y] (mod m * n)";
apply (auto);
apply (insert prems);
apply (rule zcong_zgcd_zmult_zmod, auto simp add: PHI2_def);
done;
from p1 have p3: "0 < m * n" by (auto simp add: mult_pos);
have p4: "x mod (m*n) = y mod (m*n)";
by (insert p2 p3 zcong_zmod_eq [of "m*n" x y], auto);
have "0 <= x & 0 <= y & x < (m*n) & y < (m*n)" by (insert prems, auto simp add: SR_def);
thus "x = y";
apply (auto);
apply (insert p1 p4, auto);
apply (drule mod_pos_pos_trivial, auto)+;
done;
qed;

lemma (in PHI2) f_SR_card: "card (f ` (SR(m*n))) = card(SR(m) <*> SR(n))";
proof-;
have "card (f ` (SR(m*n))) = card( SR(m*n))";
apply (insert SR_mn_finite SR_inj_on_f);
apply (auto simp add: card_image);
done;
also have "... = card(SR(m) <*> SR(n))";
proof-;
have "int(card(SR(m * n))) = int(card(SR(m) <*> SR(n)))";
apply (insert SR_m_finite SR_n_finite SR_mn_finite);
apply (insert SR_m_card SR_n_card SR_mn_card);
apply (auto simp add: zmult_int [THEN sym]);
done;
thus ?thesis by auto;
qed;
finally show ?thesis by auto;
qed;

lemma (in PHI2) SR_image_prop: "f ` SR(m * n) <= SR(m) <*> SR(n)";
apply (insert m_ge_1 n_ge_1);
apply (auto simp add: SR_def f_def pos_mod_sign pos_mod_bound);
done;

lemma (in PHI2) SR_prod_finite: "finite( SR(m) <*> SR(n))";
by (auto simp add: SR_m_finite SR_n_finite);

lemma (in PHI2) image_SR_prop: "f ` SR(m * n) = SR(m) <*> SR(n)";
apply (insert SR_prod_finite SR_image_prop f_SR_card);
apply (auto simp add: card_seteq);
done;

lemma (in PHI2) ResUnits_inj_on_f: "inj_on f (ResUnits(m * n))";
proof-;
have "(ResUnits(m * n)) <= SR(m * n)";
by (auto simp add: ResUnits_def SR_def);
with SR_inj_on_f show ?thesis by (auto simp add: subset_inj_on);
qed;

lemma (in PHI2) ResUnits_prod_finite: "finite( ResUnits(m) <*> ResUnits(n))";
by (auto simp add: ResUnits_m_finite ResUnits_n_finite);

lemma (in PHI2) aux1_ResUnits_image_prop: "f ` ResUnits(m * n) <= ResUnits(m) <*> ResUnits(n)";
apply (auto simp add: image_def f_def);
proof -;
fix x;
assume "x : ResUnits (m * n)";
then have "zgcd(m*n, x) = 1" by (auto simp add: ResUnits_def zgcd_commute);
then have "zgcd(m,x) = 1" by (auto simp add: zgcd_zmult_prop);
also have "zgcd(m,x) = zgcd(m,x mod m)" by (insert zgcd_eq2 [of m x], auto);
finally have "zgcd (m, x mod m) = 1" .;
thus "x mod m : ResUnits m";
apply (auto simp add: ResUnits_def zgcd_commute SR_def);
apply (insert m_ge_1, auto simp add: pos_mod_sign pos_mod_bound);
done;
next;
fix x;
assume "x : ResUnits (m * n)";
then have "zgcd(m*n, x) = 1" by (auto simp add: ResUnits_def zgcd_commute);
then have "zgcd(n,x) = 1" by (auto simp add: zgcd_zmult_prop);
also have "zgcd(n,x) = zgcd(n,x mod n)" by (insert zgcd_eq2 [of n x], auto);
finally have "zgcd (n, x mod n) = 1" .;
thus "x mod n : ResUnits n";
apply (auto simp add: ResUnits_def zgcd_commute SR_def);
apply (insert n_ge_1, auto simp add: pos_mod_sign pos_mod_bound);
done;
qed;

lemma (in PHI2) aux2_ResUnits_image_prop: "ResUnits(m) <*> ResUnits(n) <= f ` ResUnits(m * n)";
apply (auto simp add: image_def f_def);
apply (auto simp add: ResUnits_def);
apply (insert specialized_chinese);
apply (drule_tac x = a in allE, auto);
apply (drule_tac x = b in allE, auto);
apply (rule_tac x = "x mod (m*n)" in exI);
apply (auto);
proof-;
fix a b x;
have "0 < m * n" by (insert m_ge_1 n_ge_1, auto simp add: mult_pos);
thus "x mod (m*n) : SR(m*n)" by (auto simp add: SR_def pos_mod_sign pos_mod_bound);
next;
fix a b x;
assume p1: "a : SR m" and p2: "b : SR n" and
p3: "zgcd (a, m) = 1" and p4: "zgcd (b, n) = 1" and
"[x = a] (mod m)" and "[x = b] (mod n)";
moreover have "0 < m & 0 < n" by (insert n_ge_1 m_ge_1, auto);
ultimately have "x mod m = a mod m & x mod n = b mod n";
by (auto simp add: zcong_zmod_eq);
also have "a mod m = a" by (insert p1, auto simp add: SR_m_mod_prop);
also have "b mod n = b" by (insert p2, auto simp add: SR_n_mod_prop);
finally have "x mod m = a & x mod n = b" .;
with p3 p4 have "zgcd (x mod m, m) = 1 & zgcd (x mod n, n) = 1" by auto;
with zgcd_ac have  "zgcd (m, x mod m) = 1 & zgcd (n, x mod n) = 1" by auto;
with zgcd_eq2 have "zgcd (m, x) = 1 & zgcd(n, x) = 1" by auto;
with zgcd_zmult_prop have "zgcd(m * n, x) = 1" by auto;
with zgcd_eq2 have "zgcd(m*n, x mod (m*n)) = 1" by auto;
thus "zgcd (x mod (m * n), m * n) = 1" by (auto simp add: zgcd_ac);
next;
fix a b x;
assume p1: "a : SR m" and p2: "zgcd (a, m) = 1" and p3: "[x = a] (mod m)";
then have "a = a mod m" by (auto simp add: SR_m_mod_prop);
also have "... = x mod m";
proof-;
have "0 < m" by (insert m_ge_1, auto);
with p3 zcong_sym show ?thesis;
by (auto simp add:  zcong_zmod_eq [THEN sym]);
qed;
also have "... = x mod (m*n) mod m";
by (insert m_ge_1, auto simp add: zmod_zmult_zmod);
finally show "a = x mod (m * n) mod m" .;
next;
fix a b x;
assume p1: "b : SR n" and p2: "zgcd (b, n) = 1" and p3: "[x = b] (mod n)";
then have "b = b mod n" by (auto simp add: SR_n_mod_prop);
also have "... = x mod n";
proof-;
have "0 < n" by (insert n_ge_1, auto);
with p3 zcong_sym show ?thesis;
by (auto simp add:  zcong_zmod_eq [THEN sym]);
qed;
also have "... = x mod (m*n) mod n";
by (insert n_ge_1, auto simp add: zmod_zmult_zmod2);
finally show "b = x mod (m * n) mod n" .;
qed;

lemma (in PHI2) ResUnits_image_prop: "f ` ResUnits(m * n) = ResUnits(m) <*> ResUnits(n)";
by (insert aux1_ResUnits_image_prop aux2_ResUnits_image_prop, auto);

lemma (in PHI2) mn_prop: "m ~= 1 | n ~= 1 ==> 1 < m * n";
proof-;
assume "m ~= 1 | n ~= 1";
then have "1 ~= m * n";
by (auto, insert n_ge_1 m_ge_1 zmult_eq_1_iff [of m n], auto);
moreover from n_ge_1 m_ge_1 have "0 < m * n";
by (auto simp add: mult_pos);
ultimately show ?thesis by arith;
qed;

lemma (in PHI2) aux1_big_prop3: "m ~= 1 | n ~= 1 ==>
{x. 1 <= x & x <= m * n & zgcd (x, m * n) = 1} = ResUnits(m*n)";
apply (auto simp add: PHI2_def ResUnits_def SR_def);
apply (case_tac "x = m * n");
apply (insert mn_prop);
apply (auto);
apply (case_tac "x = m * n");
apply (insert mn_prop);
apply (auto);
apply (case_tac "x = 0", auto);
apply (case_tac "x = 0", auto);
done;

lemma (in PHI2) aux2_big_prop3: "m ~= 1 ==>
{x. 1 <= x & x <= m & zgcd (x, m) = 1} = ResUnits(m)";
apply (auto simp add: ResUnits_def SR_def);
apply (case_tac "x = m", auto);
apply (case_tac "x = 0", auto);
done;

lemma (in PHI2) aux3_big_prop3: "n ~= 1 ==>
{x. 1 <= x & x <= n & zgcd (x, n) = 1} = ResUnits(n)";
apply (auto simp add: ResUnits_def SR_def);
apply (case_tac "x = n", auto);
apply (case_tac "x = 0", auto);
done;

(* FINALLY *)

theorem (in PHI2) big_prop3: "phi(m * n) = phi(m) * phi(n)";
proof-;
have "phi(m*n) = int(card(ResUnits(m*n)))";
apply (auto simp add: phi_def);
apply (case_tac "m = 1");
apply (case_tac "n = 1");defer;defer;
apply (case_tac "n = 1");
proof-;
assume "m ~= 1";
then show "card {x. 1 <= x & x <= m * n & zgcd (x, m * n) = 1} = card (ResUnits (m * n))";
by (auto simp add: aux1_big_prop3);
next;
assume "m ~= 1";
then show "card {x. 1 <= x & x <= m * n & zgcd (x, m * n) = 1} = card (ResUnits (m * n))";
by (auto simp add: aux1_big_prop3);
next;
assume "m = 1" and "n = 1";
then have "card {x. 1 <= x & x <= m * n & zgcd (x, m * n) = 1} = card {x. (1::int) <= x & x <= 1}";
by(auto);
also have "{x. (1::int) <= x & x <= 1} = {x. (0::int) < x & x <= 1}";
by (auto);
also have "card {x. (0::int) < x & x <= 1} = nat 1";
apply (subgoal_tac "{x. (0::int) < x & x <= 1} = {)0..1}");
apply auto;
done;
finally have p1: "card {x. 1 <= x & x <= m * n & zgcd (x, m * n) = 1} = nat 1" .;
from prems have "card (ResUnits (m * n)) = card {x. (0::int) <= x & x < 1}";
by (auto);
also have "... = nat 1"
apply (subgoal_tac "{x. (0::int) <= x & x < 1} = {0..1(}");
apply auto;
done;
finally have "card (ResUnits (m * n)) = nat 1" .;
with p1 show "card {x. 1 <= x & x <= m * n & zgcd (x, m * n) = 1} = card (ResUnits (m * n))";
by (auto);
next;
assume "n ~= 1";
then show "card {x. 1 <= x & x <= m * n & zgcd (x, m * n) = 1} = card (ResUnits (m * n))";
by (auto simp add: aux1_big_prop3);
qed;
also have "card (ResUnits (m * n)) = card (f ` ResUnits (m * n))";
apply (insert ResUnits_mn_finite ResUnits_inj_on_f);
apply (auto simp add: card_image);
done;
also have "f ` ResUnits (m * n) = ResUnits(m) <*> ResUnits(n)";
by (auto simp add: ResUnits_image_prop);
also have "card (ResUnits m <*> ResUnits n) = card (ResUnits m) * card (ResUnits n)";
apply (insert ResUnits_m_finite ResUnits_n_finite);
by (simp add: setsum_constant);
also have "int (card (ResUnits m) * card (ResUnits n)) = int (card (ResUnits m)) * int (card (ResUnits n))";
by (auto simp add: zmult_int);
also have "int (card (ResUnits m)) = phi (m)";
apply (auto simp add: phi_def);
apply (case_tac "m = 1");
proof-;
assume "m = 1";
then have "card {x. 1 <= x & x <= m & zgcd (x, m) = 1} = card {x. (1::int) <= x & x <= 1}";
by(auto);
also have "{x. (1::int) <= x & x <= 1} = {x. (0::int) < x & x <= 1}";
by (auto);
also have "card {x. (0::int) < x & x <= 1} = nat 1";
by (subgoal_tac "{x. (0::int) < x & x <= 1} = {)0..1}", auto);
finally have p1: "card {x. 1 <= x & x <= m & zgcd (x, m) = 1} = nat 1" .;
from prems have "card (ResUnits (m)) = card {x. (0::int) <= x & x < 1}";
by (auto);
also have "... = nat 1"
apply (subgoal_tac "{x. 0 ≤ x ∧ x < 1} = {0..1(}");
apply (erule ssubst);
apply auto;
done;
finally have "card (ResUnits (m)) = nat 1" .;
with p1 have "card {x. 1 <= x & x <= m & zgcd (x, m) = 1} = card (ResUnits (m))";
by (auto);
then show "card (ResUnits m) = card {x. 1 <= x & x <= m & zgcd (x, m) = 1}"
by auto;
next;
assume "m ~= 1";
then show "card (ResUnits m) = card {x. 1 <= x & x <= m & zgcd (x, m) = 1}"
by(auto simp add: aux2_big_prop3);
qed;
also have "int (card (ResUnits n)) = phi (n)";
apply (auto simp add: phi_def);
apply (case_tac "n = 1");
proof-;
assume "n = 1";
then have "card {x. 1 <= x & x <= n & zgcd (x, n) = 1} = card {x. (1::int) <= x & x <= 1}";
by(auto);
also have "{x. (1::int) <= x & x <= 1} = {x. (0::int) < x & x <= 1}";
by (auto);
also have "card {x. (0::int) < x & x <= 1} = nat 1";
apply (subgoal_tac "{x. (0::int) < x & x <= 1} = {)0..1}");
apply (erule ssubst);
apply auto;
done;
finally have p1: "card {x. 1 <= x & x <= n & zgcd (x, n) = 1} = nat 1" .;
from prems have "card (ResUnits (n)) = card {x. (0::int) <= x & x < 1}";
by (auto);
also have "... = nat 1"
apply (subgoal_tac "{x. 0 ≤ x ∧ x < 1} = {0..1(}");
apply (erule ssubst, auto);
done;
finally have "card (ResUnits (n)) = nat 1" .;
with p1 have "card {x. 1 <= x & x <= n & zgcd (x, n) = 1} = card (ResUnits (n))";
by (auto);
then show "card (ResUnits n) = card {x. 1 <= x & x <= n & zgcd (x, n) = 1}"
by auto;
next;
assume "n ~= 1";
then show "card (ResUnits n) = card {x. 1 <= x & x <= n & zgcd (x, n) = 1}"
by(auto simp add: aux3_big_prop3);
qed;
finally show ?thesis .;
qed;

end
```

lemma n_dvd_range:

`  [| PHI n; d dvd n; 0 ≤ d |] ==> 1 ≤ d ∧ d ≤ n`

lemma n_zgcd_range:

`  [| PHI n; 1 ≤ x; x ≤ n |] ==> 1 ≤ zgcd (x, n) ∧ zgcd (x, n) ≤ n`

lemma zgcd_elem_S:

`  [| PHI n; 1 ≤ x; x ≤ n |] ==> zgcd (x, n) ∈ {x. 1 ≤ x ∧ x ≤ n}`

lemma S_finite:

`  PHI n ==> finite {x. 1 ≤ x ∧ x ≤ n}`

lemma I_sub_S:

`  PHI n ==> {d. 0 ≤ d ∧ d dvd n} ⊆ {x. 1 ≤ x ∧ x ≤ n}`

lemma I_finite:

`  PHI n ==> finite {d. 0 ≤ d ∧ d dvd n}`

lemma I_elem_prop:

`  [| PHI n; d ∈ {d. 0 ≤ d ∧ d dvd n} |] ==> 1 ≤ d`

lemma I_eq_I2:

`  PHI n ==> {d. 0 ≤ d ∧ d dvd n} = {d. 1 ≤ d ∧ d dvd n}`

lemma A_sub_S:

`  PHI n ==> {k. k ∈ {x. 1 ≤ x ∧ x ≤ n} ∧ zgcd (k, n) = d} ⊆ {x. 1 ≤ x ∧ x ≤ n}`

lemma A_finite:

`  PHI n ==> finite {k. k ∈ {x. 1 ≤ x ∧ x ≤ n} ∧ zgcd (k, n) = d}`

lemma B_sub_S:

```  [| PHI n; d ∈ {d. 0 ≤ d ∧ d dvd n} |]
==> {l. 1 ≤ l ∧ l ≤ n div d ∧ zgcd (l, n div d) = 1} ⊆ {x. 1 ≤ x ∧ x ≤ n}```

lemma B_finite:

```  [| PHI n; d ∈ {d. 0 ≤ d ∧ d dvd n} |]
==> finite {l. 1 ≤ l ∧ l ≤ n div d ∧ zgcd (l, n div d) = 1}```

lemma S_eq_UNION_A:

```  PHI n
==> {x. 1 ≤ x ∧ x ≤ n} =
(UN d:{d. 0 ≤ d ∧ d dvd n}. {k. k ∈ {x. 1 ≤ x ∧ x ≤ n} ∧ zgcd (k, n) = d})```

lemma A_disj_prop:

```  PHI n
==> ∀d1∈{d. 0 ≤ d ∧ d dvd n}.
∀d2∈{d. 0 ≤ d ∧ d dvd n}.
d1 ≠ d2 -->
{k. k ∈ {x. 1 ≤ x ∧ x ≤ n} ∧ zgcd (k, n) = d1} ∩
{k. k ∈ {x. 1 ≤ x ∧ x ≤ n} ∧ zgcd (k, n) = d2} =
{}```

lemma n_eq_Sum_card_A:

```  PHI n
==> n = (∑x∈{d. 0 ≤ d ∧
d dvd
n}. int (card {k. k ∈ {x. 1 ≤ x ∧ x ≤ n} ∧ zgcd (k, n) = x}))```

lemma zgcd_div_prop:

```  [| PHI n; d ∈ {x. 1 ≤ x ∧ x ≤ n} |]
==> (zgcd (k, n) = d) = (d dvd k ∧ d dvd n ∧ zgcd (k div d, n div d) = 1)```

lemma A_inj_prop:

```  [| PHI n; d ∈ {d. 0 ≤ d ∧ d dvd n} |]
==> inj_on (%k. k div d) {k. k ∈ {x. 1 ≤ x ∧ x ≤ n} ∧ zgcd (k, n) = d}```

lemma image_A_eq_B:

```  [| PHI n; d ∈ {d. 0 ≤ d ∧ d dvd n} |]
==> (%k. k div d) ` {k. k ∈ {x. 1 ≤ x ∧ x ≤ n} ∧ zgcd (k, n) = d} =
{l. 1 ≤ l ∧ l ≤ n div d ∧ zgcd (l, n div d) = 1}```

lemma card_A_eq_phi:

```  [| PHI n; d ∈ {d. 0 ≤ d ∧ d dvd n} |]
==> int (card {k. k ∈ {x. 1 ≤ x ∧ x ≤ n} ∧ zgcd (k, n) = d}) =
EulerPhi.phi (n div d)```

lemma n_eq_setsum_phi:

`  PHI n ==> n = setsum (EulerPhi.phi ˆ op div n) {d. 0 ≤ d ∧ d dvd n}`

lemma I_inj_prop:

`  PHI n ==> inj_on (op div n) {d. 0 ≤ d ∧ d dvd n}`

lemma f_image_I_eq_I:

`  PHI n ==> op div n ` {d. 0 ≤ d ∧ d dvd n} = {d. 0 ≤ d ∧ d dvd n}`

theorem big_prop1:

`  PHI n ==> n = setsum EulerPhi.phi {d. 0 ≤ d ∧ d dvd n}`

lemma card_gcd_set:

```  [| p ∈ zprime; 0 < k |]
==> int (card {x. 1 ≤ x ∧ x ≤ p ^ k ∧ zgcd (x, p ^ k) ≠ 1}) = p ^ (k - 1)```

theorem big_prop2:

`  [| p ∈ zprime; 0 < k |] ==> EulerPhi.phi (p ^ k) = p ^ k - p ^ (k - 1)`

lemma SR_m_mod_prop:

`  [| PHI2 n m; a ∈ {x. 0 ≤ x ∧ x < m} |] ==> a mod m = a`

lemma SR_n_mod_prop:

`  [| PHI2 n m; a ∈ {x. 0 ≤ x ∧ x < n} |] ==> a mod n = a`

lemma SR_mn_mod_prop:

`  [| PHI2 n m; a ∈ {x. 0 ≤ x ∧ x < m * n} |] ==> a mod (m * n) = a`

lemma SR_m_finite:

`  PHI2 n m ==> finite {x. 0 ≤ x ∧ x < m}`

lemma SR_m_card:

`  PHI2 n m ==> int (card {x. 0 ≤ x ∧ x < m}) = m`

lemma SR_n_finite:

`  PHI2 n m ==> finite {x. 0 ≤ x ∧ x < n}`

lemma SR_n_card:

`  PHI2 n m ==> int (card {x. 0 ≤ x ∧ x < n}) = n`

lemma SR_mn_finite:

`  PHI2 n m ==> finite {x. 0 ≤ x ∧ x < m * n}`

lemma SR_mn_card:

`  PHI2 n m ==> int (card {x. 0 ≤ x ∧ x < m * n}) = m * n`

lemma ResUnits_m_finite:

`  PHI2 n m ==> finite {x. x ∈ {x. 0 ≤ x ∧ x < m} ∧ zgcd (x, m) = 1}`

lemma ResUnits_n_finite:

`  PHI2 n m ==> finite {x. x ∈ {x. 0 ≤ x ∧ x < n} ∧ zgcd (x, n) = 1}`

lemma ResUnits_mn_finite:

`  PHI2 n m ==> finite {x. x ∈ {x. 0 ≤ x ∧ x < m * n} ∧ zgcd (x, m * n) = 1}`

lemma zgcd_zmult_prop:

`  PHI2 n m ==> (zgcd (m * n, x) = 1) = (zgcd (m, x) = 1 ∧ zgcd (n, x) = 1)`

lemma specialized_chinese:

`  PHI2 n m ==> ∀a b. ∃x. [x = a] (mod m) ∧ [x = b] (mod n)`

lemma SR_inj_on_f:

`  PHI2 n m ==> inj_on (%x. (x mod m, x mod n)) {x. 0 ≤ x ∧ x < m * n}`

lemma f_SR_card:

```  PHI2 n m
==> card ((%x. (x mod m, x mod n)) ` {x. 0 ≤ x ∧ x < m * n}) =
card ({x. 0 ≤ x ∧ x < m} × {x. 0 ≤ x ∧ x < n})```

lemma SR_image_prop:

```  PHI2 n m
==> (%x. (x mod m, x mod n)) ` {x. 0 ≤ x ∧ x < m * n}
⊆ {x. 0 ≤ x ∧ x < m} × {x. 0 ≤ x ∧ x < n}```

lemma SR_prod_finite:

`  PHI2 n m ==> finite ({x. 0 ≤ x ∧ x < m} × {x. 0 ≤ x ∧ x < n})`

lemma image_SR_prop:

```  PHI2 n m
==> (%x. (x mod m, x mod n)) ` {x. 0 ≤ x ∧ x < m * n} =
{x. 0 ≤ x ∧ x < m} × {x. 0 ≤ x ∧ x < n}```

lemma ResUnits_inj_on_f:

```  PHI2 n m
==> inj_on (%x. (x mod m, x mod n))
{x. x ∈ {x. 0 ≤ x ∧ x < m * n} ∧ zgcd (x, m * n) = 1}```

lemma ResUnits_prod_finite:

```  PHI2 n m
==> finite
({x. x ∈ {x. 0 ≤ x ∧ x < m} ∧
zgcd (x, m) = 1} × {x. x ∈ {x. 0 ≤ x ∧ x < n} ∧ zgcd (x, n) = 1})```

lemma aux1_ResUnits_image_prop:

```  PHI2 n m
==> (%x. (x mod m, x mod n)) `
{x. x ∈ {x. 0 ≤ x ∧ x < m * n} ∧ zgcd (x, m * n) = 1}
⊆ {x. x ∈ {x. 0 ≤ x ∧ x < m} ∧
zgcd (x, m) = 1} × {x. x ∈ {x. 0 ≤ x ∧ x < n} ∧ zgcd (x, n) = 1}```

lemma aux2_ResUnits_image_prop:

```  PHI2 n m
==> {x. x ∈ {x. 0 ≤ x ∧ x < m} ∧
zgcd (x, m) = 1} × {x. x ∈ {x. 0 ≤ x ∧ x < n} ∧ zgcd (x, n) = 1}
⊆ (%x. (x mod m, x mod n)) `
{x. x ∈ {x. 0 ≤ x ∧ x < m * n} ∧ zgcd (x, m * n) = 1}```

lemma ResUnits_image_prop:

```  PHI2 n m
==> (%x. (x mod m, x mod n)) `
{x. x ∈ {x. 0 ≤ x ∧ x < m * n} ∧ zgcd (x, m * n) = 1} =
{x. x ∈ {x. 0 ≤ x ∧ x < m} ∧
zgcd (x, m) = 1} × {x. x ∈ {x. 0 ≤ x ∧ x < n} ∧ zgcd (x, n) = 1}```

lemma mn_prop:

`  [| PHI2 n m; m ≠ 1 ∨ n ≠ 1 |] ==> 1 < m * n`

lemma aux1_big_prop3:

```  [| PHI2 n m; m ≠ 1 ∨ n ≠ 1 |]
==> {x. 1 ≤ x ∧ x ≤ m * n ∧ zgcd (x, m * n) = 1} =
{x. x ∈ {x. 0 ≤ x ∧ x < m * n} ∧ zgcd (x, m * n) = 1}```

lemma aux2_big_prop3:

```  [| PHI2 n m; m ≠ 1 |]
==> {x. 1 ≤ x ∧ x ≤ m ∧ zgcd (x, m) = 1} =
{x. x ∈ {x. 0 ≤ x ∧ x < m} ∧ zgcd (x, m) = 1}```

lemma aux3_big_prop3:

```  [| PHI2 n m; n ≠ 1 |]
==> {x. 1 ≤ x ∧ x ≤ n ∧ zgcd (x, n) = 1} =
{x. x ∈ {x. 0 ≤ x ∧ x < n} ∧ zgcd (x, n) = 1}```

theorem big_prop3:

`  PHI2 n m ==> EulerPhi.phi (m * n) = EulerPhi.phi m * EulerPhi.phi n`