[STATEMENT]
theorem prime_card_elements_with_ord_eq_totient:
  assumes "prime n"
  shows   "\<psi> d = (if d dvd n - 1 then totient d else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
proof (cases "d dvd totient n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. d dvd totient n \<Longrightarrow> \<psi> d = (if d dvd n - 1 then totient d else 0)
 2. \<not> d dvd totient n \<Longrightarrow> \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> d dvd totient n

goal (2 subgoals):
 1. d dvd totient n \<Longrightarrow> \<psi> d = (if d dvd n - 1 then totient d else 0)
 2. \<not> d dvd totient n \<Longrightarrow> \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> d dvd totient n

goal (1 subgoal):
 1. \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
using order_divides_totient[of n] assms
[PROOF STATE]
proof (prove)
using this:
\<not> d dvd totient n
coprime n ?a \<Longrightarrow> ord n ?a dvd totient n
prime n

goal (1 subgoal):
 1. \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
by (auto simp: \<psi>_def totient_prime totatives_def coprime_commute[of n])
[PROOF STATE]
proof (state)
this:
\<psi> d = (if d dvd n - 1 then totient d else 0)

goal (1 subgoal):
 1. d dvd totient n \<Longrightarrow> \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d dvd totient n \<Longrightarrow> \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
d dvd totient n

goal (1 subgoal):
 1. d dvd totient n \<Longrightarrow> \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
have "\<psi> d = totient d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> d = totient d
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
assume neq: "\<psi> d \<noteq> totient d"
[PROOF STATE]
proof (state)
this:
\<psi> d \<noteq> totient d

goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
have le: "\<psi> d \<le> totient d" if "d dvd totient n" for d
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> d \<le> totient d
[PROOF STEP]
using prime_card_elements_with_ord[of d] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<psi> d \<noteq> 0; prime n\<rbrakk> \<Longrightarrow> \<psi> d = totient d
prime n

goal (1 subgoal):
 1. \<psi> d \<le> totient d
[PROOF STEP]
by (cases "\<psi> d = 0") auto
[PROOF STATE]
proof (state)
this:
?d dvd totient n \<Longrightarrow> \<psi> ?d \<le> totient ?d

goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
from neq and le[of d] and True
[PROOF STATE]
proof (chain)
picking this:
\<psi> d \<noteq> totient d
d dvd totient n \<Longrightarrow> \<psi> d \<le> totient d
d dvd totient n
[PROOF STEP]
have less: "\<psi> d < totient d"
[PROOF STATE]
proof (prove)
using this:
\<psi> d \<noteq> totient d
d dvd totient n \<Longrightarrow> \<psi> d \<le> totient d
d dvd totient n

goal (1 subgoal):
 1. \<psi> d < totient d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<psi> d < totient d

goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
have "totient n = (\<Sum>d | d dvd totient n. \<psi> d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. totient n = (\<Sum>d | d dvd totient n. \<psi> d)
[PROOF STEP]
using prime_sum_card_elements_with_ord_eq_totient
[PROOF STATE]
proof (prove)
using this:
(\<Sum>d | d dvd totient n. \<psi> d) = totient n

goal (1 subgoal):
 1. totient n = (\<Sum>d | d dvd totient n. \<psi> d)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
totient n = (\<Sum>d | d dvd totient n. \<psi> d)

goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
totient n = (\<Sum>d | d dvd totient n. \<psi> d)

goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
have "\<dots> < (\<Sum>d | d dvd totient n. totient d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d | d dvd totient n. \<psi> d) < (\<Sum>d | d dvd totient n. totient d)
[PROOF STEP]
by (rule sum_strict_mono_ex1)
         (use n le less assms True in \<open>auto intro!: finite_divisors_nat\<close>)
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd totient n. \<psi> d) < (\<Sum>d | d dvd totient n. totient d)

goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd totient n. \<psi> d) < (\<Sum>d | d dvd totient n. totient d)

goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = totient n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d | d dvd totient n. totient d) = totient n
[PROOF STEP]
using totient_divisor_sum
[PROOF STATE]
proof (prove)
using this:
(\<Sum>d | d dvd ?n. totient d) = ?n

goal (1 subgoal):
 1. (\<Sum>d | d dvd totient n. totient d) = totient n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd totient n. totient d) = totient n

goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
totient n < totient n
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
totient n < totient n

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<psi> d = totient d

goal (1 subgoal):
 1. d dvd totient n \<Longrightarrow> \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
d dvd totient n
\<psi> d = totient d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d dvd totient n
\<psi> d = totient d

goal (1 subgoal):
 1. \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
d dvd totient n
\<psi> d = totient d
prime n

goal (1 subgoal):
 1. \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
by (simp add: totient_prime)
[PROOF STATE]
proof (state)
this:
\<psi> d = (if d dvd n - 1 then totient d else 0)

goal:
No subgoals!
[PROOF STEP]
qed