[STATEMENT]
lemma rsa_bijection:
  assumes coprime: "coprime e ((P-1)*(Q-1))"
    and prime_P: "prime (P::nat)"
    and prime_Q: "prime Q"
    and P_neq_Q: "P \<noteq> Q"
    and x_lt_pq: "x < P * Q"
    and y_lt_pd: "y < P * Q"
    and rsa_map_eq: "x ^ e mod (P * Q) = y ^ e mod (P * Q)"
  shows "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
have flt_xP: "[x ^ P = x] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ P = x] (mod P)
[PROOF STEP]
using fermat_little prime_P
[PROOF STATE]
proof (prove)
using this:
prime ?P \<Longrightarrow> [?x ^ ?P = ?x] (mod ?P)
prime P

goal (1 subgoal):
 1. [x ^ P = x] (mod P)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[x ^ P = x] (mod P)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have flt_yP: "[y ^ P = y] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y ^ P = y] (mod P)
[PROOF STEP]
using fermat_little prime_P
[PROOF STATE]
proof (prove)
using this:
prime ?P \<Longrightarrow> [?x ^ ?P = ?x] (mod ?P)
prime P

goal (1 subgoal):
 1. [y ^ P = y] (mod P)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[y ^ P = y] (mod P)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have flt_xQ: "[x ^ Q = x] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ Q = x] (mod Q)
[PROOF STEP]
using fermat_little prime_Q
[PROOF STATE]
proof (prove)
using this:
prime ?P \<Longrightarrow> [?x ^ ?P = ?x] (mod ?P)
prime Q

goal (1 subgoal):
 1. [x ^ Q = x] (mod Q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[x ^ Q = x] (mod Q)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have flt_yQ: "[y ^ Q = y] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y ^ Q = y] (mod Q)
[PROOF STEP]
using fermat_little prime_Q
[PROOF STATE]
proof (prove)
using this:
prime ?P \<Longrightarrow> [?x ^ ?P = ?x] (mod ?P)
prime Q

goal (1 subgoal):
 1. [y ^ Q = y] (mod Q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[y ^ Q = y] (mod Q)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof(cases "y \<ge> x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x = y
 2. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x = y
 2. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
hence ye_gt_xe: "y^e \<ge> x^e"
[PROOF STATE]
proof (prove)
using this:
x \<le> y

goal (1 subgoal):
 1. x ^ e \<le> y ^ e
[PROOF STEP]
by (simp add: power_mono)
[PROOF STATE]
proof (state)
this:
x ^ e \<le> y ^ e

goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x = y
 2. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have x_y_exp_e: "[x^e = y^e] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ e = y ^ e] (mod P)
[PROOF STEP]
using cong_modulus_mult_nat  cong_altdef_nat True ye_gt_xe cong_sym cong_def assms
[PROOF STATE]
proof (prove)
using this:
[?x = ?y] (mod ?m * ?n) \<Longrightarrow> [?x = ?y] (mod ?m)
?b \<le> ?a \<Longrightarrow> [?a = ?b] (mod ?m) = (?m dvd ?a - ?b)
x \<le> y
x ^ e \<le> y ^ e
[?b = ?c] (mod ?a) \<Longrightarrow> [?c = ?b] (mod ?a)
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)
coprime e ((P - 1) * (Q - 1))
prime P
prime Q
P \<noteq> Q
x < P * Q
y < P * Q
x ^ e mod (P * Q) = y ^ e mod (P * Q)

goal (1 subgoal):
 1. [x ^ e = y ^ e] (mod P)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[x ^ e = y ^ e] (mod P)

goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x = y
 2. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
obtain d where d:  "[e*d = 1] (mod (P-1)) \<and> d \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d. [e * d = 1] (mod P - 1) \<and> d \<noteq> 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex_inverse assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>coprime ?e ((?P - 1) * (?Q - 1)); prime ?P; prime ?Q; ?P \<noteq> ?Q\<rbrakk> \<Longrightarrow> \<exists>d. [?e * d = 1] (mod ?P - 1) \<and> d \<noteq> 0
coprime e ((P - 1) * (Q - 1))
prime P
prime Q
P \<noteq> Q
x < P * Q
y < P * Q
x ^ e mod (P * Q) = y ^ e mod (P * Q)

goal (1 subgoal):
 1. (\<And>d. [e * d = 1] (mod P - 1) \<and> d \<noteq> 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[e * d = 1] (mod P - 1) \<and> d \<noteq> 0

goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x = y
 2. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[e * d = 1] (mod P - 1) \<and> d \<noteq> 0
[PROOF STEP]
obtain k where k: "e*d = 1 + k*(P-1)"
[PROOF STATE]
proof (prove)
using this:
[e * d = 1] (mod P - 1) \<and> d \<noteq> 0

goal (1 subgoal):
 1. (\<And>k. e * d = 1 + k * (P - 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex_k_mod assms
[PROOF STATE]
proof (prove)
using this:
[e * d = 1] (mod P - 1) \<and> d \<noteq> 0
\<lbrakk>coprime ?e ((?P - 1) * (?Q - 1)); ?P \<noteq> ?Q; prime ?P; prime ?Q; ?d \<noteq> 0; [?e * ?d = 1] (mod ?P - 1)\<rbrakk> \<Longrightarrow> \<exists>k. ?e * ?d = 1 + k * (?P - 1)
coprime e ((P - 1) * (Q - 1))
prime P
prime Q
P \<noteq> Q
x < P * Q
y < P * Q
x ^ e mod (P * Q) = y ^ e mod (P * Q)

goal (1 subgoal):
 1. (\<And>k. e * d = 1 + k * (P - 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
e * d = 1 + k * (P - 1)

goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x = y
 2. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
hence xk_yk: "[x^(1 + k*(P-1)) = y^(1 + k*(P-1))] (mod P)"
[PROOF STATE]
proof (prove)
using this:
e * d = 1 + k * (P - 1)

goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = y ^ (1 + k * (P - 1))] (mod P)
[PROOF STEP]
by(metis k power_mult x_y_exp_e cong_pow)
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k * (P - 1)) = y ^ (1 + k * (P - 1))] (mod P)

goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x = y
 2. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have xk_x: "[x^(1 + k*(P-1)) = x] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = x] (mod P)
[PROOF STEP]
proof(induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [x ^ (1 + 0 * (P - 1)) = x] (mod P)
 2. \<And>k. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. [x ^ (1 + 0 * (P - 1)) = x] (mod P)
 2. \<And>k. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ (1 + 0 * (P - 1)) = x] (mod P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x ^ (1 + 0 * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. \<And>k. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. \<And>k. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
assume  asm: "[x ^ (1 + k * (P - 1)) = x] (mod P)"
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. \<And>k. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[x ^ (1 + k * (P - 1)) = x] (mod P)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[x ^ (1 + k * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
have exp_rewrite: "(k * (P - 1) + P) = (1 + (k + 1) * (P - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k * (P - 1) + P = 1 + (k + 1) * (P - 1)
[PROOF STEP]
by (smt add.assoc add.commute le_add_diff_inverse nat_le_linear not_add_less1 prime_P prime_gt_1_nat semiring_normalization_rules(3))
[PROOF STATE]
proof (state)
this:
k * (P - 1) + P = 1 + (k + 1) * (P - 1)

goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
have "[x * x ^ (k * (P - 1)) = x] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x * x ^ (k * (P - 1)) = x] (mod P)
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
[x ^ (1 + k * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. [x * x ^ (k * (P - 1)) = x] (mod P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x * x ^ (k * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
hence "[x ^ (k * (P - 1)) * x ^ P = x] (mod P)"
[PROOF STATE]
proof (prove)
using this:
[x * x ^ (k * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. [x ^ (k * (P - 1)) * x ^ P = x] (mod P)
[PROOF STEP]
using flt_xP
[PROOF STATE]
proof (prove)
using this:
[x * x ^ (k * (P - 1)) = x] (mod P)
[x ^ P = x] (mod P)

goal (1 subgoal):
 1. [x ^ (k * (P - 1)) * x ^ P = x] (mod P)
[PROOF STEP]
by (metis cong_scalar_right cong_trans mult.commute)
[PROOF STATE]
proof (state)
this:
[x ^ (k * (P - 1)) * x ^ P = x] (mod P)

goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
hence "[x ^ (k * (P - 1) + P) = x] (mod P)"
[PROOF STATE]
proof (prove)
using this:
[x ^ (k * (P - 1)) * x ^ P = x] (mod P)

goal (1 subgoal):
 1. [x ^ (k * (P - 1) + P) = x] (mod P)
[PROOF STEP]
by (simp add: power_add)
[PROOF STATE]
proof (state)
this:
[x ^ (k * (P - 1) + P) = x] (mod P)

goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
hence "[x ^ (1 + (k + 1) * (P - 1)) = x] (mod P)"
[PROOF STATE]
proof (prove)
using this:
[x ^ (k * (P - 1) + P) = x] (mod P)

goal (1 subgoal):
 1. [x ^ (1 + (k + 1) * (P - 1)) = x] (mod P)
[PROOF STEP]
using exp_rewrite
[PROOF STATE]
proof (prove)
using this:
[x ^ (k * (P - 1) + P) = x] (mod P)
k * (P - 1) + P = 1 + (k + 1) * (P - 1)

goal (1 subgoal):
 1. [x ^ (1 + (k + 1) * (P - 1)) = x] (mod P)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
[x ^ (1 + (k + 1) * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[x ^ (1 + (k + 1) * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x ^ (1 + Suc k * (P - 1)) = x] (mod P)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[x ^ (1 + Suc k * (P - 1)) = x] (mod P)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k * (P - 1)) = x] (mod P)

goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x = y
 2. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have yk_y: "[y^(1 + k*(P-1)) = y] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y ^ (1 + k * (P - 1)) = y] (mod P)
[PROOF STEP]
proof(induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [y ^ (1 + 0 * (P - 1)) = y] (mod P)
 2. \<And>k. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. [y ^ (1 + 0 * (P - 1)) = y] (mod P)
 2. \<And>k. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y ^ (1 + 0 * (P - 1)) = y] (mod P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[y ^ (1 + 0 * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. \<And>k. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
[y ^ (1 + k * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. \<And>k. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
assume  asm: "[y ^ (1 + k * (P - 1)) = y] (mod P)"
[PROOF STATE]
proof (state)
this:
[y ^ (1 + k * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. \<And>k. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[y ^ (1 + k * (P - 1)) = y] (mod P)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[y ^ (1 + k * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
have exp_rewrite: "(k * (P - 1) + P) = (1 + (k + 1) * (P - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k * (P - 1) + P = 1 + (k + 1) * (P - 1)
[PROOF STEP]
by (smt add.assoc add.commute le_add_diff_inverse nat_le_linear not_add_less1 prime_P prime_gt_1_nat semiring_normalization_rules(3))
[PROOF STATE]
proof (state)
this:
k * (P - 1) + P = 1 + (k + 1) * (P - 1)

goal (1 subgoal):
 1. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
have "[y * y ^ (k * (P - 1)) = y] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y * y ^ (k * (P - 1)) = y] (mod P)
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
[y ^ (1 + k * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. [y * y ^ (k * (P - 1)) = y] (mod P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[y * y ^ (k * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
hence "[y ^ (k * (P - 1)) * y ^ P = y] (mod P)"
[PROOF STATE]
proof (prove)
using this:
[y * y ^ (k * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. [y ^ (k * (P - 1)) * y ^ P = y] (mod P)
[PROOF STEP]
using flt_yP
[PROOF STATE]
proof (prove)
using this:
[y * y ^ (k * (P - 1)) = y] (mod P)
[y ^ P = y] (mod P)

goal (1 subgoal):
 1. [y ^ (k * (P - 1)) * y ^ P = y] (mod P)
[PROOF STEP]
by (metis cong_scalar_right cong_trans mult.commute)
[PROOF STATE]
proof (state)
this:
[y ^ (k * (P - 1)) * y ^ P = y] (mod P)

goal (1 subgoal):
 1. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
hence "[y ^ (k * (P - 1) + P) = y] (mod P)"
[PROOF STATE]
proof (prove)
using this:
[y ^ (k * (P - 1)) * y ^ P = y] (mod P)

goal (1 subgoal):
 1. [y ^ (k * (P - 1) + P) = y] (mod P)
[PROOF STEP]
by (simp add: power_add)
[PROOF STATE]
proof (state)
this:
[y ^ (k * (P - 1) + P) = y] (mod P)

goal (1 subgoal):
 1. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
hence "[y ^ (1 + (k + 1) * (P - 1)) = y] (mod P)"
[PROOF STATE]
proof (prove)
using this:
[y ^ (k * (P - 1) + P) = y] (mod P)

goal (1 subgoal):
 1. [y ^ (1 + (k + 1) * (P - 1)) = y] (mod P)
[PROOF STEP]
using exp_rewrite
[PROOF STATE]
proof (prove)
using this:
[y ^ (k * (P - 1) + P) = y] (mod P)
k * (P - 1) + P = 1 + (k + 1) * (P - 1)

goal (1 subgoal):
 1. [y ^ (1 + (k + 1) * (P - 1)) = y] (mod P)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
[y ^ (1 + (k + 1) * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[y ^ (1 + (k + 1) * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[y ^ (1 + Suc k * (P - 1)) = y] (mod P)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[y ^ (1 + Suc k * (P - 1)) = y] (mod P)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[y ^ (1 + k * (P - 1)) = y] (mod P)

goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x = y
 2. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have "[x^e = y^e] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ e = y ^ e] (mod Q)
[PROOF STEP]
by (metis rsa_map_eq cong_modulus_mult_nat cong_def mult.commute)
[PROOF STATE]
proof (state)
this:
[x ^ e = y ^ e] (mod Q)

goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x = y
 2. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
obtain d' where d':  "[e*d' = 1] (mod (Q-1)) \<and> d' \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d'. [e * d' = 1] (mod Q - 1) \<and> d' \<noteq> 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis mult.commute ex_inverse prime_P prime_Q P_neq_Q coprime)
[PROOF STATE]
proof (state)
this:
[e * d' = 1] (mod Q - 1) \<and> d' \<noteq> 0

goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x = y
 2. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[e * d' = 1] (mod Q - 1) \<and> d' \<noteq> 0
[PROOF STEP]
obtain k' where k': "e*d' = 1 + k'*(Q-1)"
[PROOF STATE]
proof (prove)
using this:
[e * d' = 1] (mod Q - 1) \<and> d' \<noteq> 0

goal (1 subgoal):
 1. (\<And>k'. e * d' = 1 + k' * (Q - 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(metis ex_k_mod mult.commute prime_P prime_Q P_neq_Q coprime)
[PROOF STATE]
proof (state)
this:
e * d' = 1 + k' * (Q - 1)

goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x = y
 2. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
hence xk_yk': "[x^(1 + k'*(Q-1)) = y^(1 + k'*(Q-1))] (mod Q)"
[PROOF STATE]
proof (prove)
using this:
e * d' = 1 + k' * (Q - 1)

goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = y ^ (1 + k' * (Q - 1))] (mod Q)
[PROOF STEP]
by(metis k' power_mult \<open>[x ^ e = y ^ e] (mod Q)\<close> cong_pow)
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k' * (Q - 1)) = y ^ (1 + k' * (Q - 1))] (mod Q)

goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x = y
 2. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have xk_x': "[x^(1 + k'*(Q-1)) = x] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
proof(induct k')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [x ^ (1 + 0 * (Q - 1)) = x] (mod Q)
 2. \<And>k'. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. [x ^ (1 + 0 * (Q - 1)) = x] (mod Q)
 2. \<And>k'. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ (1 + 0 * (Q - 1)) = x] (mod Q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x ^ (1 + 0 * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. \<And>k'. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k'. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
case (Suc k')
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k' * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. \<And>k'. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
assume  asm: "[x ^ (1 + k' * (Q - 1)) = x] (mod Q)"
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k' * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. \<And>k'. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[x ^ (1 + k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[x ^ (1 + k' * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
have exp_rewrite: "(k' * (Q - 1) + Q) = (1 + (k' + 1) * (Q - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' * (Q - 1) + Q = 1 + (k' + 1) * (Q - 1)
[PROOF STEP]
by (smt add.assoc add.commute le_add_diff_inverse nat_le_linear not_add_less1 prime_Q prime_gt_1_nat semiring_normalization_rules(3))
[PROOF STATE]
proof (state)
this:
k' * (Q - 1) + Q = 1 + (k' + 1) * (Q - 1)

goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
have "[x * x ^ (k' * (Q - 1)) = x] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x * x ^ (k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
[x ^ (1 + k' * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. [x * x ^ (k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x * x ^ (k' * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
hence "[x ^ (k' * (Q - 1)) * x ^ Q = x] (mod Q)"
[PROOF STATE]
proof (prove)
using this:
[x * x ^ (k' * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (k' * (Q - 1)) * x ^ Q = x] (mod Q)
[PROOF STEP]
using flt_xQ
[PROOF STATE]
proof (prove)
using this:
[x * x ^ (k' * (Q - 1)) = x] (mod Q)
[x ^ Q = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (k' * (Q - 1)) * x ^ Q = x] (mod Q)
[PROOF STEP]
by (metis cong_scalar_right cong_trans mult.commute)
[PROOF STATE]
proof (state)
this:
[x ^ (k' * (Q - 1)) * x ^ Q = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
hence "[x ^ (k' * (Q - 1) + Q) = x] (mod Q)"
[PROOF STATE]
proof (prove)
using this:
[x ^ (k' * (Q - 1)) * x ^ Q = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (k' * (Q - 1) + Q) = x] (mod Q)
[PROOF STEP]
by (simp add: power_add)
[PROOF STATE]
proof (state)
this:
[x ^ (k' * (Q - 1) + Q) = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
hence "[x ^ (1 + (k' + 1) * (Q - 1)) = x] (mod Q)"
[PROOF STATE]
proof (prove)
using this:
[x ^ (k' * (Q - 1) + Q) = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (1 + (k' + 1) * (Q - 1)) = x] (mod Q)
[PROOF STEP]
using exp_rewrite
[PROOF STATE]
proof (prove)
using this:
[x ^ (k' * (Q - 1) + Q) = x] (mod Q)
k' * (Q - 1) + Q = 1 + (k' + 1) * (Q - 1)

goal (1 subgoal):
 1. [x ^ (1 + (k' + 1) * (Q - 1)) = x] (mod Q)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
[x ^ (1 + (k' + 1) * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[x ^ (1 + (k' + 1) * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k' * (Q - 1)) = x] (mod Q)

goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x = y
 2. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have yk_y': "[y^(1 + k'*(Q-1)) = y] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y ^ (1 + k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
proof(induct k')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [y ^ (1 + 0 * (Q - 1)) = y] (mod Q)
 2. \<And>k'. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. [y ^ (1 + 0 * (Q - 1)) = y] (mod Q)
 2. \<And>k'. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y ^ (1 + 0 * (Q - 1)) = y] (mod Q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[y ^ (1 + 0 * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. \<And>k'. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k'. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
case (Suc k')
[PROOF STATE]
proof (state)
this:
[y ^ (1 + k' * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. \<And>k'. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
assume  asm: "[y ^ (1 + k' * (Q - 1)) = y] (mod Q)"
[PROOF STATE]
proof (state)
this:
[y ^ (1 + k' * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. \<And>k'. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[y ^ (1 + k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[y ^ (1 + k' * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
have exp_rewrite: "(k' * (Q - 1) + Q) = (1 + (k' + 1) * (Q - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' * (Q - 1) + Q = 1 + (k' + 1) * (Q - 1)
[PROOF STEP]
by (smt add.assoc add.commute le_add_diff_inverse nat_le_linear not_add_less1 prime_Q prime_gt_1_nat semiring_normalization_rules(3))
[PROOF STATE]
proof (state)
this:
k' * (Q - 1) + Q = 1 + (k' + 1) * (Q - 1)

goal (1 subgoal):
 1. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
have "[y * y ^ (k' * (Q - 1)) = y] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y * y ^ (k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
[y ^ (1 + k' * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. [y * y ^ (k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[y * y ^ (k' * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
hence "[y ^ (k' * (Q - 1)) * y ^ Q = y] (mod Q)"
[PROOF STATE]
proof (prove)
using this:
[y * y ^ (k' * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (k' * (Q - 1)) * y ^ Q = y] (mod Q)
[PROOF STEP]
using flt_yQ
[PROOF STATE]
proof (prove)
using this:
[y * y ^ (k' * (Q - 1)) = y] (mod Q)
[y ^ Q = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (k' * (Q - 1)) * y ^ Q = y] (mod Q)
[PROOF STEP]
by (metis cong_scalar_right cong_trans mult.commute)
[PROOF STATE]
proof (state)
this:
[y ^ (k' * (Q - 1)) * y ^ Q = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
hence "[y ^ (k' * (Q - 1) + Q) = y] (mod Q)"
[PROOF STATE]
proof (prove)
using this:
[y ^ (k' * (Q - 1)) * y ^ Q = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (k' * (Q - 1) + Q) = y] (mod Q)
[PROOF STEP]
by (simp add: power_add)
[PROOF STATE]
proof (state)
this:
[y ^ (k' * (Q - 1) + Q) = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
hence "[y ^ (1 + (k' + 1) * (Q - 1)) = y] (mod Q)"
[PROOF STATE]
proof (prove)
using this:
[y ^ (k' * (Q - 1) + Q) = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (1 + (k' + 1) * (Q - 1)) = y] (mod Q)
[PROOF STEP]
using exp_rewrite
[PROOF STATE]
proof (prove)
using this:
[y ^ (k' * (Q - 1) + Q) = y] (mod Q)
k' * (Q - 1) + Q = 1 + (k' + 1) * (Q - 1)

goal (1 subgoal):
 1. [y ^ (1 + (k' + 1) * (Q - 1)) = y] (mod Q)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
[y ^ (1 + (k' + 1) * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[y ^ (1 + (k' + 1) * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[y ^ (1 + k' * (Q - 1)) = y] (mod Q)

goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x = y
 2. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have P_dvd_xy: "P dvd (y - x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P dvd y - x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P dvd y - x
[PROOF STEP]
have "[x = y] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x = y] (mod P)
[PROOF STEP]
using xk_x yk_y xk_yk
[PROOF STATE]
proof (prove)
using this:
[x ^ (1 + k * (P - 1)) = x] (mod P)
[y ^ (1 + k * (P - 1)) = y] (mod P)
[x ^ (1 + k * (P - 1)) = y ^ (1 + k * (P - 1))] (mod P)

goal (1 subgoal):
 1. [x = y] (mod P)
[PROOF STEP]
by (simp add: cong_def)
[PROOF STATE]
proof (state)
this:
[x = y] (mod P)

goal (1 subgoal):
 1. P dvd y - x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[x = y] (mod P)

goal (1 subgoal):
 1. P dvd y - x
[PROOF STEP]
using cong_altdef_nat cong_sym True
[PROOF STATE]
proof (prove)
using this:
[x = y] (mod P)
?b \<le> ?a \<Longrightarrow> [?a = ?b] (mod ?m) = (?m dvd ?a - ?b)
[?b = ?c] (mod ?a) \<Longrightarrow> [?c = ?b] (mod ?a)
x \<le> y

goal (1 subgoal):
 1. P dvd y - x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P dvd y - x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P dvd y - x

goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x = y
 2. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have Q_dvd_xy: "Q dvd (y - x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q dvd y - x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q dvd y - x
[PROOF STEP]
have "[x = y] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x = y] (mod Q)
[PROOF STEP]
using xk_x' yk_y' xk_yk'
[PROOF STATE]
proof (prove)
using this:
[x ^ (1 + k' * (Q - 1)) = x] (mod Q)
[y ^ (1 + k' * (Q - 1)) = y] (mod Q)
[x ^ (1 + k' * (Q - 1)) = y ^ (1 + k' * (Q - 1))] (mod Q)

goal (1 subgoal):
 1. [x = y] (mod Q)
[PROOF STEP]
by (simp add: cong_def)
[PROOF STATE]
proof (state)
this:
[x = y] (mod Q)

goal (1 subgoal):
 1. Q dvd y - x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[x = y] (mod Q)

goal (1 subgoal):
 1. Q dvd y - x
[PROOF STEP]
using cong_altdef_nat cong_sym True
[PROOF STATE]
proof (prove)
using this:
[x = y] (mod Q)
?b \<le> ?a \<Longrightarrow> [?a = ?b] (mod ?m) = (?m dvd ?a - ?b)
[?b = ?c] (mod ?a) \<Longrightarrow> [?c = ?b] (mod ?a)
x \<le> y

goal (1 subgoal):
 1. Q dvd y - x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Q dvd y - x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Q dvd y - x

goal (2 subgoals):
 1. x \<le> y \<Longrightarrow> x = y
 2. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
have "P*Q dvd (y - x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * Q dvd y - x
[PROOF STEP]
using P_dvd_xy  Q_dvd_xy
[PROOF STATE]
proof (prove)
using this:
P dvd y - x
Q dvd y - x

goal (1 subgoal):
 1. P * Q dvd y - x
[PROOF STEP]
by (simp add: assms divides_mult primes_coprime)
[PROOF STATE]
proof (state)
this:
P * Q dvd y - x

goal (1 subgoal):
 1. x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P * Q dvd y - x
[PROOF STEP]
have "[x = y] (mod P*Q)"
[PROOF STATE]
proof (prove)
using this:
P * Q dvd y - x

goal (1 subgoal):
 1. [x = y] (mod P * Q)
[PROOF STEP]
by (simp add: cong_altdef_nat cong_sym True)
[PROOF STATE]
proof (state)
this:
[x = y] (mod P * Q)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
hence "x mod P*Q = y mod P*Q"
[PROOF STATE]
proof (prove)
using this:
[x = y] (mod P * Q)

goal (1 subgoal):
 1. x mod P * Q = y mod P * Q
[PROOF STEP]
using  cong_def xk_x xk_yk yk_y
[PROOF STATE]
proof (prove)
using this:
[x = y] (mod P * Q)
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)
[x ^ (1 + k * (P - 1)) = x] (mod P)
[x ^ (1 + k * (P - 1)) = y ^ (1 + k * (P - 1))] (mod P)
[y ^ (1 + k * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. x mod P * Q = y mod P * Q
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
x mod P * Q = y mod P * Q

goal (1 subgoal):
 1. x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x mod P * Q = y mod P * Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x mod P * Q = y mod P * Q

goal (1 subgoal):
 1. x = y
[PROOF STEP]
using \<open>[x = y] (mod P * Q)\<close> cong_less_modulus_unique_nat x_lt_pq y_lt_pd
[PROOF STATE]
proof (prove)
using this:
x mod P * Q = y mod P * Q
[x = y] (mod P * Q)
\<lbrakk>[?x = ?y] (mod ?m); ?x < ?m; ?y < ?m\<rbrakk> \<Longrightarrow> ?x = ?y
x < P * Q
y < P * Q

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x \<le> y

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
hence ye_gt_xe: "x^e \<ge> y^e"
[PROOF STATE]
proof (prove)
using this:
\<not> x \<le> y

goal (1 subgoal):
 1. y ^ e \<le> x ^ e
[PROOF STEP]
by (simp add: power_mono)
[PROOF STATE]
proof (state)
this:
y ^ e \<le> x ^ e

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have pow_eq: "[x^e = y^e] (mod P*Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ e = y ^ e] (mod P * Q)
[PROOF STEP]
by (simp add: cong_def assms)
[PROOF STATE]
proof (state)
this:
[x ^ e = y ^ e] (mod P * Q)

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[x ^ e = y ^ e] (mod P * Q)
[PROOF STEP]
have PQ_dvd_ye_xe: "(P*Q) dvd (x^e - y^e)"
[PROOF STATE]
proof (prove)
using this:
[x ^ e = y ^ e] (mod P * Q)

goal (1 subgoal):
 1. P * Q dvd x ^ e - y ^ e
[PROOF STEP]
using cong_altdef_nat False ye_gt_xe cong_sym
[PROOF STATE]
proof (prove)
using this:
[x ^ e = y ^ e] (mod P * Q)
?b \<le> ?a \<Longrightarrow> [?a = ?b] (mod ?m) = (?m dvd ?a - ?b)
\<not> x \<le> y
y ^ e \<le> x ^ e
[?b = ?c] (mod ?a) \<Longrightarrow> [?c = ?b] (mod ?a)

goal (1 subgoal):
 1. P * Q dvd x ^ e - y ^ e
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P * Q dvd x ^ e - y ^ e

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P * Q dvd x ^ e - y ^ e
[PROOF STEP]
have "[x^e = y^e] (mod P)"
[PROOF STATE]
proof (prove)
using this:
P * Q dvd x ^ e - y ^ e

goal (1 subgoal):
 1. [x ^ e = y ^ e] (mod P)
[PROOF STEP]
using cong_modulus_mult_nat pow_eq
[PROOF STATE]
proof (prove)
using this:
P * Q dvd x ^ e - y ^ e
[?x = ?y] (mod ?m * ?n) \<Longrightarrow> [?x = ?y] (mod ?m)
[x ^ e = y ^ e] (mod P * Q)

goal (1 subgoal):
 1. [x ^ e = y ^ e] (mod P)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[x ^ e = y ^ e] (mod P)

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
obtain d where d:  "[e*d = 1] (mod (P-1)) \<and> d \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d. [e * d = 1] (mod P - 1) \<and> d \<noteq> 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex_inverse assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>coprime ?e ((?P - 1) * (?Q - 1)); prime ?P; prime ?Q; ?P \<noteq> ?Q\<rbrakk> \<Longrightarrow> \<exists>d. [?e * d = 1] (mod ?P - 1) \<and> d \<noteq> 0
coprime e ((P - 1) * (Q - 1))
prime P
prime Q
P \<noteq> Q
x < P * Q
y < P * Q
x ^ e mod (P * Q) = y ^ e mod (P * Q)

goal (1 subgoal):
 1. (\<And>d. [e * d = 1] (mod P - 1) \<and> d \<noteq> 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[e * d = 1] (mod P - 1) \<and> d \<noteq> 0

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[e * d = 1] (mod P - 1) \<and> d \<noteq> 0
[PROOF STEP]
obtain k where k: "e*d = 1 + k*(P-1)"
[PROOF STATE]
proof (prove)
using this:
[e * d = 1] (mod P - 1) \<and> d \<noteq> 0

goal (1 subgoal):
 1. (\<And>k. e * d = 1 + k * (P - 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex_k_mod assms
[PROOF STATE]
proof (prove)
using this:
[e * d = 1] (mod P - 1) \<and> d \<noteq> 0
\<lbrakk>coprime ?e ((?P - 1) * (?Q - 1)); ?P \<noteq> ?Q; prime ?P; prime ?Q; ?d \<noteq> 0; [?e * ?d = 1] (mod ?P - 1)\<rbrakk> \<Longrightarrow> \<exists>k. ?e * ?d = 1 + k * (?P - 1)
coprime e ((P - 1) * (Q - 1))
prime P
prime Q
P \<noteq> Q
x < P * Q
y < P * Q
x ^ e mod (P * Q) = y ^ e mod (P * Q)

goal (1 subgoal):
 1. (\<And>k. e * d = 1 + k * (P - 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
e * d = 1 + k * (P - 1)

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have xk_yk: "[x^(1 + k*(P-1)) = y^(1 + k*(P-1))] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = y ^ (1 + k * (P - 1))] (mod P)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = y ^ (1 + k * (P - 1))] (mod P)
[PROOF STEP]
have "[(x^e)^d = (y^e)^d] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(x ^ e) ^ d = (y ^ e) ^ d] (mod P)
[PROOF STEP]
using \<open>[x ^ e = y ^ e] (mod P)\<close> cong_pow
[PROOF STATE]
proof (prove)
using this:
[x ^ e = y ^ e] (mod P)
[?b = ?c] (mod ?a) \<Longrightarrow> [?b ^ ?n = ?c ^ ?n] (mod ?a)

goal (1 subgoal):
 1. [(x ^ e) ^ d = (y ^ e) ^ d] (mod P)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[(x ^ e) ^ d = (y ^ e) ^ d] (mod P)

goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = y ^ (1 + k * (P - 1))] (mod P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x ^ e) ^ d = (y ^ e) ^ d] (mod P)
[PROOF STEP]
have "[x^(e*d) = y^(e*d)] (mod P)"
[PROOF STATE]
proof (prove)
using this:
[(x ^ e) ^ d = (y ^ e) ^ d] (mod P)

goal (1 subgoal):
 1. [x ^ (e * d) = y ^ (e * d)] (mod P)
[PROOF STEP]
by (simp add: power_mult)
[PROOF STATE]
proof (state)
this:
[x ^ (e * d) = y ^ (e * d)] (mod P)

goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = y ^ (1 + k * (P - 1))] (mod P)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[x ^ (e * d) = y ^ (e * d)] (mod P)

goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = y ^ (1 + k * (P - 1))] (mod P)
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
[x ^ (e * d) = y ^ (e * d)] (mod P)
e * d = 1 + k * (P - 1)

goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = y ^ (1 + k * (P - 1))] (mod P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k * (P - 1)) = y ^ (1 + k * (P - 1))] (mod P)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k * (P - 1)) = y ^ (1 + k * (P - 1))] (mod P)

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have xk_x: "[x^(1 + k*(P-1)) = x] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = x] (mod P)
[PROOF STEP]
proof(induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [x ^ (1 + 0 * (P - 1)) = x] (mod P)
 2. \<And>k. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. [x ^ (1 + 0 * (P - 1)) = x] (mod P)
 2. \<And>k. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ (1 + 0 * (P - 1)) = x] (mod P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x ^ (1 + 0 * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. \<And>k. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. \<And>k. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
assume  asm: "[x ^ (1 + k * (P - 1)) = x] (mod P)"
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. \<And>k. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[x ^ (1 + k * (P - 1)) = x] (mod P)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[x ^ (1 + k * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
have exp_rewrite: "(k * (P - 1) + P) = (1 + (k + 1) * (P - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k * (P - 1) + P = 1 + (k + 1) * (P - 1)
[PROOF STEP]
by (smt add.assoc add.commute le_add_diff_inverse nat_le_linear not_add_less1 prime_P prime_gt_1_nat semiring_normalization_rules(3))
[PROOF STATE]
proof (state)
this:
k * (P - 1) + P = 1 + (k + 1) * (P - 1)

goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
have "[x * x ^ (k * (P - 1)) = x] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x * x ^ (k * (P - 1)) = x] (mod P)
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
[x ^ (1 + k * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. [x * x ^ (k * (P - 1)) = x] (mod P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x * x ^ (k * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
hence "[x ^ (k * (P - 1)) * x ^ P = x] (mod P)"
[PROOF STATE]
proof (prove)
using this:
[x * x ^ (k * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. [x ^ (k * (P - 1)) * x ^ P = x] (mod P)
[PROOF STEP]
using flt_xP
[PROOF STATE]
proof (prove)
using this:
[x * x ^ (k * (P - 1)) = x] (mod P)
[x ^ P = x] (mod P)

goal (1 subgoal):
 1. [x ^ (k * (P - 1)) * x ^ P = x] (mod P)
[PROOF STEP]
by (metis cong_scalar_right cong_trans mult.commute)
[PROOF STATE]
proof (state)
this:
[x ^ (k * (P - 1)) * x ^ P = x] (mod P)

goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
hence "[x ^ (k * (P - 1) + P) = x] (mod P)"
[PROOF STATE]
proof (prove)
using this:
[x ^ (k * (P - 1)) * x ^ P = x] (mod P)

goal (1 subgoal):
 1. [x ^ (k * (P - 1) + P) = x] (mod P)
[PROOF STEP]
by (simp add: power_add)
[PROOF STATE]
proof (state)
this:
[x ^ (k * (P - 1) + P) = x] (mod P)

goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
hence "[x ^ (1 + (k + 1) * (P - 1)) = x] (mod P)"
[PROOF STATE]
proof (prove)
using this:
[x ^ (k * (P - 1) + P) = x] (mod P)

goal (1 subgoal):
 1. [x ^ (1 + (k + 1) * (P - 1)) = x] (mod P)
[PROOF STEP]
using exp_rewrite
[PROOF STATE]
proof (prove)
using this:
[x ^ (k * (P - 1) + P) = x] (mod P)
k * (P - 1) + P = 1 + (k + 1) * (P - 1)

goal (1 subgoal):
 1. [x ^ (1 + (k + 1) * (P - 1)) = x] (mod P)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
[x ^ (1 + (k + 1) * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. [x ^ (1 + k * (P - 1)) = x] (mod P) \<Longrightarrow> [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[x ^ (1 + (k + 1) * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. [x ^ (1 + Suc k * (P - 1)) = x] (mod P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x ^ (1 + Suc k * (P - 1)) = x] (mod P)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[x ^ (1 + Suc k * (P - 1)) = x] (mod P)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k * (P - 1)) = x] (mod P)

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have yk_y: "[y^(1 + k*(P-1)) = y] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y ^ (1 + k * (P - 1)) = y] (mod P)
[PROOF STEP]
proof(induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [y ^ (1 + 0 * (P - 1)) = y] (mod P)
 2. \<And>k. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. [y ^ (1 + 0 * (P - 1)) = y] (mod P)
 2. \<And>k. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y ^ (1 + 0 * (P - 1)) = y] (mod P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[y ^ (1 + 0 * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. \<And>k. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
[y ^ (1 + k * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. \<And>k. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
assume  asm: "[y ^ (1 + k * (P - 1)) = y] (mod P)"
[PROOF STATE]
proof (state)
this:
[y ^ (1 + k * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. \<And>k. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[y ^ (1 + k * (P - 1)) = y] (mod P)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[y ^ (1 + k * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
have exp_rewrite: "(k * (P - 1) + P) = (1 + (k + 1) * (P - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k * (P - 1) + P = 1 + (k + 1) * (P - 1)
[PROOF STEP]
by (smt add.assoc add.commute le_add_diff_inverse nat_le_linear not_add_less1 prime_P prime_gt_1_nat semiring_normalization_rules(3))
[PROOF STATE]
proof (state)
this:
k * (P - 1) + P = 1 + (k + 1) * (P - 1)

goal (1 subgoal):
 1. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
have "[y * y ^ (k * (P - 1)) = y] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y * y ^ (k * (P - 1)) = y] (mod P)
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
[y ^ (1 + k * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. [y * y ^ (k * (P - 1)) = y] (mod P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[y * y ^ (k * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
hence "[y ^ (k * (P - 1)) * y ^ P = y] (mod P)"
[PROOF STATE]
proof (prove)
using this:
[y * y ^ (k * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. [y ^ (k * (P - 1)) * y ^ P = y] (mod P)
[PROOF STEP]
using flt_yP
[PROOF STATE]
proof (prove)
using this:
[y * y ^ (k * (P - 1)) = y] (mod P)
[y ^ P = y] (mod P)

goal (1 subgoal):
 1. [y ^ (k * (P - 1)) * y ^ P = y] (mod P)
[PROOF STEP]
by (metis cong_scalar_right cong_trans mult.commute)
[PROOF STATE]
proof (state)
this:
[y ^ (k * (P - 1)) * y ^ P = y] (mod P)

goal (1 subgoal):
 1. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
hence "[y ^ (k * (P - 1) + P) = y] (mod P)"
[PROOF STATE]
proof (prove)
using this:
[y ^ (k * (P - 1)) * y ^ P = y] (mod P)

goal (1 subgoal):
 1. [y ^ (k * (P - 1) + P) = y] (mod P)
[PROOF STEP]
by (simp add: power_add)
[PROOF STATE]
proof (state)
this:
[y ^ (k * (P - 1) + P) = y] (mod P)

goal (1 subgoal):
 1. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
hence "[y ^ (1 + (k + 1) * (P - 1)) = y] (mod P)"
[PROOF STATE]
proof (prove)
using this:
[y ^ (k * (P - 1) + P) = y] (mod P)

goal (1 subgoal):
 1. [y ^ (1 + (k + 1) * (P - 1)) = y] (mod P)
[PROOF STEP]
using exp_rewrite
[PROOF STATE]
proof (prove)
using this:
[y ^ (k * (P - 1) + P) = y] (mod P)
k * (P - 1) + P = 1 + (k + 1) * (P - 1)

goal (1 subgoal):
 1. [y ^ (1 + (k + 1) * (P - 1)) = y] (mod P)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
[y ^ (1 + (k + 1) * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. [y ^ (1 + k * (P - 1)) = y] (mod P) \<Longrightarrow> [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[y ^ (1 + (k + 1) * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. [y ^ (1 + Suc k * (P - 1)) = y] (mod P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[y ^ (1 + Suc k * (P - 1)) = y] (mod P)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[y ^ (1 + Suc k * (P - 1)) = y] (mod P)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[y ^ (1 + k * (P - 1)) = y] (mod P)

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have P_dvd_xy: "P dvd (x - y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P dvd x - y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P dvd x - y
[PROOF STEP]
have "[x = y] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x = y] (mod P)
[PROOF STEP]
using xk_x yk_y xk_yk
[PROOF STATE]
proof (prove)
using this:
[x ^ (1 + k * (P - 1)) = x] (mod P)
[y ^ (1 + k * (P - 1)) = y] (mod P)
[x ^ (1 + k * (P - 1)) = y ^ (1 + k * (P - 1))] (mod P)

goal (1 subgoal):
 1. [x = y] (mod P)
[PROOF STEP]
by (simp add: cong_def)
[PROOF STATE]
proof (state)
this:
[x = y] (mod P)

goal (1 subgoal):
 1. P dvd x - y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[x = y] (mod P)

goal (1 subgoal):
 1. P dvd x - y
[PROOF STEP]
using cong_altdef_nat cong_sym False
[PROOF STATE]
proof (prove)
using this:
[x = y] (mod P)
?b \<le> ?a \<Longrightarrow> [?a = ?b] (mod ?m) = (?m dvd ?a - ?b)
[?b = ?c] (mod ?a) \<Longrightarrow> [?c = ?b] (mod ?a)
\<not> x \<le> y

goal (1 subgoal):
 1. P dvd x - y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P dvd x - y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P dvd x - y

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have "[x^e = y^e] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ e = y ^ e] (mod Q)
[PROOF STEP]
using cong_modulus_mult_nat pow_eq PQ_dvd_ye_xe cong_dvd_modulus_nat dvd_triv_right
[PROOF STATE]
proof (prove)
using this:
[?x = ?y] (mod ?m * ?n) \<Longrightarrow> [?x = ?y] (mod ?m)
[x ^ e = y ^ e] (mod P * Q)
P * Q dvd x ^ e - y ^ e
\<lbrakk>[?x = ?y] (mod ?m); ?n dvd ?m\<rbrakk> \<Longrightarrow> [?x = ?y] (mod ?n)
?a dvd ?b * ?a

goal (1 subgoal):
 1. [x ^ e = y ^ e] (mod Q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[x ^ e = y ^ e] (mod Q)

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
obtain d' where d':  "[e*d' = 1] (mod (Q-1)) \<and> d' \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d'. [e * d' = 1] (mod Q - 1) \<and> d' \<noteq> 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis mult.commute ex_inverse prime_P prime_Q coprime P_neq_Q)
[PROOF STATE]
proof (state)
this:
[e * d' = 1] (mod Q - 1) \<and> d' \<noteq> 0

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[e * d' = 1] (mod Q - 1) \<and> d' \<noteq> 0
[PROOF STEP]
obtain k' where k': "e*d' = 1 + k'*(Q-1)"
[PROOF STATE]
proof (prove)
using this:
[e * d' = 1] (mod Q - 1) \<and> d' \<noteq> 0

goal (1 subgoal):
 1. (\<And>k'. e * d' = 1 + k' * (Q - 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(metis ex_k_mod mult.commute prime_P prime_Q coprime P_neq_Q)
[PROOF STATE]
proof (state)
this:
e * d' = 1 + k' * (Q - 1)

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have xk_yk': "[x^(1 + k'*(Q-1)) = y^(1 + k'*(Q-1))] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = y ^ (1 + k' * (Q - 1))] (mod Q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = y ^ (1 + k' * (Q - 1))] (mod Q)
[PROOF STEP]
have "[(x^e)^d' = (y^e)^d'] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(x ^ e) ^ d' = (y ^ e) ^ d'] (mod Q)
[PROOF STEP]
using \<open>[x ^ e = y ^ e] (mod Q)\<close> cong_pow
[PROOF STATE]
proof (prove)
using this:
[x ^ e = y ^ e] (mod Q)
[?b = ?c] (mod ?a) \<Longrightarrow> [?b ^ ?n = ?c ^ ?n] (mod ?a)

goal (1 subgoal):
 1. [(x ^ e) ^ d' = (y ^ e) ^ d'] (mod Q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[(x ^ e) ^ d' = (y ^ e) ^ d'] (mod Q)

goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = y ^ (1 + k' * (Q - 1))] (mod Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x ^ e) ^ d' = (y ^ e) ^ d'] (mod Q)
[PROOF STEP]
have "[x^(e*d') = y^(e*d')] (mod Q)"
[PROOF STATE]
proof (prove)
using this:
[(x ^ e) ^ d' = (y ^ e) ^ d'] (mod Q)

goal (1 subgoal):
 1. [x ^ (e * d') = y ^ (e * d')] (mod Q)
[PROOF STEP]
by (simp add: power_mult)
[PROOF STATE]
proof (state)
this:
[x ^ (e * d') = y ^ (e * d')] (mod Q)

goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = y ^ (1 + k' * (Q - 1))] (mod Q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[x ^ (e * d') = y ^ (e * d')] (mod Q)

goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = y ^ (1 + k' * (Q - 1))] (mod Q)
[PROOF STEP]
using k'
[PROOF STATE]
proof (prove)
using this:
[x ^ (e * d') = y ^ (e * d')] (mod Q)
e * d' = 1 + k' * (Q - 1)

goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = y ^ (1 + k' * (Q - 1))] (mod Q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k' * (Q - 1)) = y ^ (1 + k' * (Q - 1))] (mod Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k' * (Q - 1)) = y ^ (1 + k' * (Q - 1))] (mod Q)

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have xk_x': "[x^(1 + k'*(Q-1)) = x] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
proof(induct k')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [x ^ (1 + 0 * (Q - 1)) = x] (mod Q)
 2. \<And>k'. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. [x ^ (1 + 0 * (Q - 1)) = x] (mod Q)
 2. \<And>k'. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x ^ (1 + 0 * (Q - 1)) = x] (mod Q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x ^ (1 + 0 * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. \<And>k'. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k'. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
case (Suc k')
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k' * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. \<And>k'. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
assume  asm: "[x ^ (1 + k' * (Q - 1)) = x] (mod Q)"
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k' * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. \<And>k'. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[x ^ (1 + k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[x ^ (1 + k' * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
have exp_rewrite: "(k' * (Q - 1) + Q) = (1 + (k' + 1) * (Q - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' * (Q - 1) + Q = 1 + (k' + 1) * (Q - 1)
[PROOF STEP]
by (smt add.assoc add.commute le_add_diff_inverse nat_le_linear not_add_less1 prime_Q prime_gt_1_nat semiring_normalization_rules(3))
[PROOF STATE]
proof (state)
this:
k' * (Q - 1) + Q = 1 + (k' + 1) * (Q - 1)

goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
have "[x * x ^ (k' * (Q - 1)) = x] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x * x ^ (k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
[x ^ (1 + k' * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. [x * x ^ (k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x * x ^ (k' * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
hence "[x ^ (k' * (Q - 1)) * x ^ Q = x] (mod Q)"
[PROOF STATE]
proof (prove)
using this:
[x * x ^ (k' * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (k' * (Q - 1)) * x ^ Q = x] (mod Q)
[PROOF STEP]
using flt_xQ
[PROOF STATE]
proof (prove)
using this:
[x * x ^ (k' * (Q - 1)) = x] (mod Q)
[x ^ Q = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (k' * (Q - 1)) * x ^ Q = x] (mod Q)
[PROOF STEP]
by (metis cong_scalar_right cong_trans mult.commute)
[PROOF STATE]
proof (state)
this:
[x ^ (k' * (Q - 1)) * x ^ Q = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
hence "[x ^ (k' * (Q - 1) + Q) = x] (mod Q)"
[PROOF STATE]
proof (prove)
using this:
[x ^ (k' * (Q - 1)) * x ^ Q = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (k' * (Q - 1) + Q) = x] (mod Q)
[PROOF STEP]
by (simp add: power_add)
[PROOF STATE]
proof (state)
this:
[x ^ (k' * (Q - 1) + Q) = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
hence "[x ^ (1 + (k' + 1) * (Q - 1)) = x] (mod Q)"
[PROOF STATE]
proof (prove)
using this:
[x ^ (k' * (Q - 1) + Q) = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (1 + (k' + 1) * (Q - 1)) = x] (mod Q)
[PROOF STEP]
using exp_rewrite
[PROOF STATE]
proof (prove)
using this:
[x ^ (k' * (Q - 1) + Q) = x] (mod Q)
k' * (Q - 1) + Q = 1 + (k' + 1) * (Q - 1)

goal (1 subgoal):
 1. [x ^ (1 + (k' + 1) * (Q - 1)) = x] (mod Q)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
[x ^ (1 + (k' + 1) * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (1 + k' * (Q - 1)) = x] (mod Q) \<Longrightarrow> [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[x ^ (1 + (k' + 1) * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. [x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[x ^ (1 + Suc k' * (Q - 1)) = x] (mod Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[x ^ (1 + k' * (Q - 1)) = x] (mod Q)

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have yk_y': "[y^(1 + k'*(Q-1)) = y] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y ^ (1 + k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
proof(induct k')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [y ^ (1 + 0 * (Q - 1)) = y] (mod Q)
 2. \<And>k'. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. [y ^ (1 + 0 * (Q - 1)) = y] (mod Q)
 2. \<And>k'. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y ^ (1 + 0 * (Q - 1)) = y] (mod Q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[y ^ (1 + 0 * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. \<And>k'. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k'. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
case (Suc k')
[PROOF STATE]
proof (state)
this:
[y ^ (1 + k' * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. \<And>k'. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
assume  asm: "[y ^ (1 + k' * (Q - 1)) = y] (mod Q)"
[PROOF STATE]
proof (state)
this:
[y ^ (1 + k' * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. \<And>k'. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[y ^ (1 + k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[y ^ (1 + k' * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
have exp_rewrite: "(k' * (Q - 1) + Q) = (1 + (k' + 1) * (Q - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' * (Q - 1) + Q = 1 + (k' + 1) * (Q - 1)
[PROOF STEP]
by (smt add.assoc add.commute le_add_diff_inverse nat_le_linear not_add_less1 prime_Q prime_gt_1_nat semiring_normalization_rules(3))
[PROOF STATE]
proof (state)
this:
k' * (Q - 1) + Q = 1 + (k' + 1) * (Q - 1)

goal (1 subgoal):
 1. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
have "[y * y ^ (k' * (Q - 1)) = y] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y * y ^ (k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
[y ^ (1 + k' * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. [y * y ^ (k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[y * y ^ (k' * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
hence "[y ^ (k' * (Q - 1)) * y ^ Q = y] (mod Q)"
[PROOF STATE]
proof (prove)
using this:
[y * y ^ (k' * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (k' * (Q - 1)) * y ^ Q = y] (mod Q)
[PROOF STEP]
using flt_yQ
[PROOF STATE]
proof (prove)
using this:
[y * y ^ (k' * (Q - 1)) = y] (mod Q)
[y ^ Q = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (k' * (Q - 1)) * y ^ Q = y] (mod Q)
[PROOF STEP]
by (metis cong_scalar_right cong_trans mult.commute)
[PROOF STATE]
proof (state)
this:
[y ^ (k' * (Q - 1)) * y ^ Q = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
hence "[y ^ (k' * (Q - 1) + Q) = y] (mod Q)"
[PROOF STATE]
proof (prove)
using this:
[y ^ (k' * (Q - 1)) * y ^ Q = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (k' * (Q - 1) + Q) = y] (mod Q)
[PROOF STEP]
by (simp add: power_add)
[PROOF STATE]
proof (state)
this:
[y ^ (k' * (Q - 1) + Q) = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
hence "[y ^ (1 + (k' + 1) * (Q - 1)) = y] (mod Q)"
[PROOF STATE]
proof (prove)
using this:
[y ^ (k' * (Q - 1) + Q) = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (1 + (k' + 1) * (Q - 1)) = y] (mod Q)
[PROOF STEP]
using exp_rewrite
[PROOF STATE]
proof (prove)
using this:
[y ^ (k' * (Q - 1) + Q) = y] (mod Q)
k' * (Q - 1) + Q = 1 + (k' + 1) * (Q - 1)

goal (1 subgoal):
 1. [y ^ (1 + (k' + 1) * (Q - 1)) = y] (mod Q)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
[y ^ (1 + (k' + 1) * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (1 + k' * (Q - 1)) = y] (mod Q) \<Longrightarrow> [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[y ^ (1 + (k' + 1) * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. [y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[y ^ (1 + Suc k' * (Q - 1)) = y] (mod Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[y ^ (1 + k' * (Q - 1)) = y] (mod Q)

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
have Q_dvd_xy: "Q dvd (x - y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q dvd x - y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q dvd x - y
[PROOF STEP]
have "[x = y] (mod Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x = y] (mod Q)
[PROOF STEP]
using xk_x' yk_y' xk_yk'
[PROOF STATE]
proof (prove)
using this:
[x ^ (1 + k' * (Q - 1)) = x] (mod Q)
[y ^ (1 + k' * (Q - 1)) = y] (mod Q)
[x ^ (1 + k' * (Q - 1)) = y ^ (1 + k' * (Q - 1))] (mod Q)

goal (1 subgoal):
 1. [x = y] (mod Q)
[PROOF STEP]
by (simp add: cong_def)
[PROOF STATE]
proof (state)
this:
[x = y] (mod Q)

goal (1 subgoal):
 1. Q dvd x - y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[x = y] (mod Q)

goal (1 subgoal):
 1. Q dvd x - y
[PROOF STEP]
using cong_altdef_nat cong_sym False
[PROOF STATE]
proof (prove)
using this:
[x = y] (mod Q)
?b \<le> ?a \<Longrightarrow> [?a = ?b] (mod ?m) = (?m dvd ?a - ?b)
[?b = ?c] (mod ?a) \<Longrightarrow> [?c = ?b] (mod ?a)
\<not> x \<le> y

goal (1 subgoal):
 1. Q dvd x - y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Q dvd x - y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Q dvd x - y

goal (1 subgoal):
 1. \<not> x \<le> y \<Longrightarrow> x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
have "P*Q dvd (x - y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * Q dvd x - y
[PROOF STEP]
using P_dvd_xy Q_dvd_xy
[PROOF STATE]
proof (prove)
using this:
P dvd x - y
Q dvd x - y

goal (1 subgoal):
 1. P * Q dvd x - y
[PROOF STEP]
by (simp add: assms divides_mult primes_coprime)
[PROOF STATE]
proof (state)
this:
P * Q dvd x - y

goal (1 subgoal):
 1. x = y
[PROOF STEP]
hence 1: "[x = y] (mod P*Q)"
[PROOF STATE]
proof (prove)
using this:
P * Q dvd x - y

goal (1 subgoal):
 1. [x = y] (mod P * Q)
[PROOF STEP]
using False cong_altdef_nat linear
[PROOF STATE]
proof (prove)
using this:
P * Q dvd x - y
\<not> x \<le> y
?b \<le> ?a \<Longrightarrow> [?a = ?b] (mod ?m) = (?m dvd ?a - ?b)
?x \<le> ?y \<or> ?y \<le> ?x

goal (1 subgoal):
 1. [x = y] (mod P * Q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[x = y] (mod P * Q)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
hence "x mod P*Q = y mod P*Q"
[PROOF STATE]
proof (prove)
using this:
[x = y] (mod P * Q)

goal (1 subgoal):
 1. x mod P * Q = y mod P * Q
[PROOF STEP]
using cong_less_modulus_unique_nat x_lt_pq y_lt_pd
[PROOF STATE]
proof (prove)
using this:
[x = y] (mod P * Q)
\<lbrakk>[?x = ?y] (mod ?m); ?x < ?m; ?y < ?m\<rbrakk> \<Longrightarrow> ?x = ?y
x < P * Q
y < P * Q

goal (1 subgoal):
 1. x mod P * Q = y mod P * Q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x mod P * Q = y mod P * Q

goal (1 subgoal):
 1. x = y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x mod P * Q = y mod P * Q

goal (1 subgoal):
 1. x = y
[PROOF STEP]
using 1 cong_less_modulus_unique_nat x_lt_pq y_lt_pd
[PROOF STATE]
proof (prove)
using this:
x mod P * Q = y mod P * Q
[x = y] (mod P * Q)
\<lbrakk>[?x = ?y] (mod ?m); ?x < ?m; ?y < ?m\<rbrakk> \<Longrightarrow> ?x = ?y
x < P * Q
y < P * Q

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rsa_bij_betw:
  assumes "coprime e ((P - 1)*(Q - 1))"
    and "prime P"
    and "prime Q"
    and "P \<noteq> Q"
  shows "bij_betw (F ((P * Q), e)) (range ((P * Q), e)) (range ((P * Q), e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (F (P * Q, e)) (local.range (P * Q, e)) (local.range (P * Q, e))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bij_betw (F (P * Q, e)) (local.range (P * Q, e)) (local.range (P * Q, e))
[PROOF STEP]
have PQ_not_0: "prime P \<longrightarrow> prime Q \<longrightarrow> P * Q \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime P \<longrightarrow> prime Q \<longrightarrow> P * Q \<noteq> 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
coprime e ((P - 1) * (Q - 1))
prime P
prime Q
P \<noteq> Q

goal (1 subgoal):
 1. prime P \<longrightarrow> prime Q \<longrightarrow> P * Q \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prime P \<longrightarrow> prime Q \<longrightarrow> P * Q \<noteq> 0

goal (1 subgoal):
 1. bij_betw (F (P * Q, e)) (local.range (P * Q, e)) (local.range (P * Q, e))
[PROOF STEP]
have "inj_on (\<lambda>x. x ^ snd (P * Q, e) mod fst (P * Q, e)) {..<fst (P * Q, e)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>x. x ^ snd (P * Q, e) mod fst (P * Q, e)) {..<fst (P * Q, e)}
[PROOF STEP]
apply(simp add: inj_on_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{..<P * Q}. \<forall>y\<in>{..<P * Q}. x ^ e mod (P * Q) = y ^ e mod (P * Q) \<longrightarrow> x = y
[PROOF STEP]
using rsa_bijection assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>coprime ?e ((?P - 1) * (?Q - 1)); prime ?P; prime ?Q; ?P \<noteq> ?Q; ?x < ?P * ?Q; ?y < ?P * ?Q; ?x ^ ?e mod (?P * ?Q) = ?y ^ ?e mod (?P * ?Q)\<rbrakk> \<Longrightarrow> ?x = ?y
coprime e ((P - 1) * (Q - 1))
prime P
prime Q
P \<noteq> Q

goal (1 subgoal):
 1. \<forall>x\<in>{..<P * Q}. \<forall>y\<in>{..<P * Q}. x ^ e mod (P * Q) = y ^ e mod (P * Q) \<longrightarrow> x = y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>x. x ^ snd (P * Q, e) mod fst (P * Q, e)) {..<fst (P * Q, e)}

goal (1 subgoal):
 1. bij_betw (F (P * Q, e)) (local.range (P * Q, e)) (local.range (P * Q, e))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>x. x ^ snd (P * Q, e) mod fst (P * Q, e)) {..<fst (P * Q, e)}

goal (1 subgoal):
 1. bij_betw (F (P * Q, e)) (local.range (P * Q, e)) (local.range (P * Q, e))
[PROOF STEP]
have "(\<lambda>x. x ^ snd (P * Q, e) mod fst (P * Q, e)) ` {..<fst (P * Q, e)} = {..<fst (P * Q, e)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x ^ snd (P * Q, e) mod fst (P * Q, e)) ` {..<fst (P * Q, e)} = {..<fst (P * Q, e)}
[PROOF STEP]
apply(simp add: assms(2) assms(3) prime_gt_0_nat PQ_not_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x ^ e mod (P * Q)) ` {..<P * Q} = {..<P * Q}
[PROOF STEP]
apply(rule endo_inj_surj; auto simp add: assms(2) assms(3) image_subsetI prime_gt_0_nat PQ_not_0 inj_on_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x < P * Q; y < P * Q; x ^ e mod (P * Q) = y ^ e mod (P * Q)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
using rsa_bijection assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>coprime ?e ((?P - 1) * (?Q - 1)); prime ?P; prime ?Q; ?P \<noteq> ?Q; ?x < ?P * ?Q; ?y < ?P * ?Q; ?x ^ ?e mod (?P * ?Q) = ?y ^ ?e mod (?P * ?Q)\<rbrakk> \<Longrightarrow> ?x = ?y
coprime e ((P - 1) * (Q - 1))
prime P
prime Q
P \<noteq> Q

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x < P * Q; y < P * Q; x ^ e mod (P * Q) = y ^ e mod (P * Q)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x ^ snd (P * Q, e) mod fst (P * Q, e)) ` {..<fst (P * Q, e)} = {..<fst (P * Q, e)}

goal (1 subgoal):
 1. bij_betw (F (P * Q, e)) (local.range (P * Q, e)) (local.range (P * Q, e))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inj_on (\<lambda>x. x ^ snd (P * Q, e) mod fst (P * Q, e)) {..<fst (P * Q, e)}
(\<lambda>x. x ^ snd (P * Q, e) mod fst (P * Q, e)) ` {..<fst (P * Q, e)} = {..<fst (P * Q, e)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>x. x ^ snd (P * Q, e) mod fst (P * Q, e)) {..<fst (P * Q, e)}
(\<lambda>x. x ^ snd (P * Q, e) mod fst (P * Q, e)) ` {..<fst (P * Q, e)} = {..<fst (P * Q, e)}

goal (1 subgoal):
 1. bij_betw (F (P * Q, e)) (local.range (P * Q, e)) (local.range (P * Q, e))
[PROOF STEP]
unfolding bij_betw_def F_def range_def
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>x. x ^ snd (P * Q, e) mod fst (P * Q, e)) {..<fst (P * Q, e)}
(\<lambda>x. x ^ snd (P * Q, e) mod fst (P * Q, e)) ` {..<fst (P * Q, e)} = {..<fst (P * Q, e)}

goal (1 subgoal):
 1. inj_on (\<lambda>x. x ^ snd (P * Q, e) mod fst (P * Q, e)) {..<fst (P * Q, e)} \<and> (\<lambda>x. x ^ snd (P * Q, e) mod fst (P * Q, e)) ` {..<fst (P * Q, e)} = {..<fst (P * Q, e)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bij_betw (F (P * Q, e)) (local.range (P * Q, e)) (local.range (P * Q, e))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_betw1:
  assumes "((N,e),d) \<in> set_spmf I"
  shows "bij_betw (F ((N), e)) (range ((N), e)) (range ((N), e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (F (N, e)) (local.range (N, e)) (local.range (N, e))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bij_betw (F (N, e)) (local.range (N, e)) (local.range (N, e))
[PROOF STEP]
obtain P Q where "N = P * Q" and "bij_betw (F ((P*Q), e)) (range ((P*Q), e)) (range ((P*Q), e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P Q. \<lbrakk>N = P * Q; bij_betw (F (P * Q, e)) (local.range (P * Q, e)) (local.range (P * Q, e))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>P Q. \<lbrakk>N = P * Q; bij_betw (F (P * Q, e)) (local.range (P * Q, e)) (local.range (P * Q, e))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain P Q where "prime P" and "prime Q" and "N = P * Q" and "P \<noteq> Q" and "coprime e ((P - 1)*(Q - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P Q. \<lbrakk>prime P; prime Q; N = P * Q; P \<noteq> Q; coprime e ((P - 1) * (Q - 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using set_spmf_I_N assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>((?N, ?e), ?d) \<in> set_spmf I; \<And>P Q. \<lbrakk>?N = P * Q; P \<noteq> Q; prime P; prime Q; coprime ?e ((P - 1) * (Q - 1)); ?d = nat (fst (bezw ?e ((P - 1) * (Q - 1))) mod int ((P - 1) * (Q - 1)))\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
((N, e), d) \<in> set_spmf I

goal (1 subgoal):
 1. (\<And>P Q. \<lbrakk>prime P; prime Q; N = P * Q; P \<noteq> Q; coprime e ((P - 1) * (Q - 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
prime P
prime Q
N = P * Q
P \<noteq> Q
coprime e ((P - 1) * (Q - 1))

goal (1 subgoal):
 1. (\<And>P Q. \<lbrakk>N = P * Q; bij_betw (F (P * Q, e)) (local.range (P * Q, e)) (local.range (P * Q, e))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prime P
prime Q
N = P * Q
P \<noteq> Q
coprime e ((P - 1) * (Q - 1))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prime P
prime Q
N = P * Q
P \<noteq> Q
coprime e ((P - 1) * (Q - 1))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using rsa_bij_betw that
[PROOF STATE]
proof (prove)
using this:
prime P
prime Q
N = P * Q
P \<noteq> Q
coprime e ((P - 1) * (Q - 1))
\<lbrakk>coprime ?e ((?P - 1) * (?Q - 1)); prime ?P; prime ?Q; ?P \<noteq> ?Q\<rbrakk> \<Longrightarrow> bij_betw (F (?P * ?Q, ?e)) (local.range (?P * ?Q, ?e)) (local.range (?P * ?Q, ?e))
\<lbrakk>N = ?P * ?Q; bij_betw (F (?P * ?Q, e)) (local.range (?P * ?Q, e)) (local.range (?P * ?Q, e))\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
N = P * Q
bij_betw (F (P * Q, e)) (local.range (P * Q, e)) (local.range (P * Q, e))

goal (1 subgoal):
 1. bij_betw (F (N, e)) (local.range (N, e)) (local.range (N, e))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
N = P * Q
bij_betw (F (P * Q, e)) (local.range (P * Q, e)) (local.range (P * Q, e))

goal (1 subgoal):
 1. bij_betw (F (N, e)) (local.range (N, e)) (local.range (N, e))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bij_betw (F (N, e)) (local.range (N, e)) (local.range (N, e))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma
  assumes "P dvd x"
shows "[x = 0] (mod P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x = 0::'a] (mod P)
[PROOF STEP]
using assms cong_def
[PROOF STATE]
proof (prove)
using this:
P dvd x
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)

goal (1 subgoal):
 1. [x = 0::'a] (mod P)
[PROOF STEP]
by force