[STATEMENT]
lemma unity_periodic_arithmetic_mult:
  "periodic_arithmetic (\<lambda>n. unity_root k (m * int n)) k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. periodic_arithmetic (\<lambda>n. unity_root k (m * int n)) k
[PROOF STEP]
unfolding periodic_arithmetic_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. unity_root k (m * int (n + k)) = unity_root k (m * int n)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. unity_root k (m * int (n + k)) = unity_root k (m * int n)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. unity_root k (m * int (n + k)) = unity_root k (m * int n)
[PROOF STEP]
have "unity_root k (m * int (n + k)) = 
        unity_root k (m*n + m*k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unity_root k (m * int (n + k)) = unity_root k (m * int n + m * int k)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
unity_root k (m * int (n + k)) = unity_root k (m * int n + m * int k)

goal (1 subgoal):
 1. \<And>n. unity_root k (m * int (n + k)) = unity_root k (m * int n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
unity_root k (m * int (n + k)) = unity_root k (m * int n + m * int k)

goal (1 subgoal):
 1. \<And>n. unity_root k (m * int (n + k)) = unity_root k (m * int n)
[PROOF STEP]
have "\<dots> = unity_root k (m*n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unity_root k (m * int n + m * int k) = unity_root k (m * int n)
[PROOF STEP]
using unity_root_mod[of k "m * int n"] unity_root_mod[of k "m * int n + m * int k"] 
          mod_mult_self3
[PROOF STATE]
proof (prove)
using this:
unity_root k (m * int n mod int k) = unity_root k (m * int n)
unity_root k ((m * int n + m * int k) mod int k) = unity_root k (m * int n + m * int k)
(?c * ?b + ?a) mod ?b = ?a mod ?b

goal (1 subgoal):
 1. unity_root k (m * int n + m * int k) = unity_root k (m * int n)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
unity_root k (m * int n + m * int k) = unity_root k (m * int n)

goal (1 subgoal):
 1. \<And>n. unity_root k (m * int (n + k)) = unity_root k (m * int n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
unity_root k (m * int (n + k)) = unity_root k (m * int n)
[PROOF STEP]
show "unity_root k (m * int (n + k)) =
             unity_root k (m * int n)"
[PROOF STATE]
proof (prove)
using this:
unity_root k (m * int (n + k)) = unity_root k (m * int n)

goal (1 subgoal):
 1. unity_root k (m * int (n + k)) = unity_root k (m * int n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
unity_root k (m * int (n + k)) = unity_root k (m * int n)

goal:
No subgoals!
[PROOF STEP]
qed