[STATEMENT]
lemma Carmichael_eq_totient_imp_primroot:
  assumes "n > 0" and "Carmichael n = totient n"
  shows   "\<exists>g. residue_primroot n g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. residue_primroot n g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>g. residue_primroot n g
[PROOF STEP]
from \<open>n > 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < n
[PROOF STEP]
obtain g where "g \<in> totatives n" and "ord n g = Carmichael n"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> totatives n; ord n g = Carmichael n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Carmichael_root_exists[of n]
[PROOF STATE]
proof (prove)
using this:
0 < n
\<lbrakk>0 < n; \<And>g. \<lbrakk>g \<in> totatives n; ord n g = Carmichael n\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> totatives n; ord n g = Carmichael n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
g \<in> totatives n
ord n g = Carmichael n

goal (1 subgoal):
 1. \<exists>g. residue_primroot n g
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < n
Carmichael n = totient n
g \<in> totatives n
ord n g = Carmichael n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < n
Carmichael n = totient n
g \<in> totatives n
ord n g = Carmichael n

goal (1 subgoal):
 1. \<exists>g. residue_primroot n g
[PROOF STEP]
by (auto simp: residue_primroot_def totatives_def coprime_commute)
[PROOF STATE]
proof (state)
this:
\<exists>g. residue_primroot n g

goal:
No subgoals!
[PROOF STEP]
qed