[STATEMENT]
theorem pell_solution_exists: "\<exists>(x::nat) (y::nat). y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
define S where "S = {(t :: int, u :: nat). u > 0 \<and> coprime u t \<and> \<bar>t - u * sqrt D\<bar> < 1 / u}"
[PROOF STATE]
proof (state)
this:
S = {(t, u). 0 < u \<and> coprime (int u) t \<and> \<bar>real_of_int t - real u * sqrt (real D)\<bar> < 1 / real u}

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
let ?f = "\<lambda>(t :: int, u :: nat). t\<^sup>2 - u\<^sup>2 * D"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
define M where "M = \<lfloor>1 + 2 * sqrt D\<rfloor>"
[PROOF STATE]
proof (state)
this:
M = \<lfloor>1 + 2 * sqrt (real D)\<rfloor>

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
have infinite: "\<not>finite S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite S
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {(t, u). 0 < u \<and> coprime (int u) t \<and> \<bar>real_of_int t - real u * sqrt (real D)\<bar> < 1 / real u}
[PROOF STEP]
by (intro pell_approximation_corollary irrat_sqrt_nonsquare nonsquare_D)
[PROOF STATE]
proof (state)
this:
infinite S

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
have subset: "?f ` S \<subseteq> {-M..M}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(t, u). t\<^sup>2 - int (u\<^sup>2 * D)) ` S \<subseteq> {- M..M}
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
fix u :: nat and t :: int
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
assume tu: "(t, u) \<in> S"
[PROOF STATE]
proof (state)
this:
(t, u) \<in> S

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
from tu
[PROOF STATE]
proof (chain)
picking this:
(t, u) \<in> S
[PROOF STEP]
have [simp]: "u > 0"
[PROOF STATE]
proof (prove)
using this:
(t, u) \<in> S

goal (1 subgoal):
 1. 0 < u
[PROOF STEP]
by (auto simp: S_def)
[PROOF STATE]
proof (state)
this:
0 < u

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
have "\<bar>t + u * sqrt D\<bar> = \<bar>t - u * sqrt D + 2 * u * sqrt D\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real_of_int t + real u * sqrt (real D)\<bar> = \<bar>real_of_int t - real u * sqrt (real D) + real (2 * u) * sqrt (real D)\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t + real u * sqrt (real D)\<bar> = \<bar>real_of_int t - real u * sqrt (real D) + real (2 * u) * sqrt (real D)\<bar>

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t + real u * sqrt (real D)\<bar> = \<bar>real_of_int t - real u * sqrt (real D) + real (2 * u) * sqrt (real D)\<bar>

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
have "\<dots> \<le> \<bar>t - u * sqrt D\<bar> + \<bar>2 * u * sqrt D\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real_of_int t - real u * sqrt (real D) + real (2 * u) * sqrt (real D)\<bar> \<le> \<bar>real_of_int t - real u * sqrt (real D)\<bar> + \<bar>real (2 * u) * sqrt (real D)\<bar>
[PROOF STEP]
by (rule abs_triangle_ineq)
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t - real u * sqrt (real D) + real (2 * u) * sqrt (real D)\<bar> \<le> \<bar>real_of_int t - real u * sqrt (real D)\<bar> + \<bar>real (2 * u) * sqrt (real D)\<bar>

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t - real u * sqrt (real D) + real (2 * u) * sqrt (real D)\<bar> \<le> \<bar>real_of_int t - real u * sqrt (real D)\<bar> + \<bar>real (2 * u) * sqrt (real D)\<bar>

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
have "\<bar>2 * u * sqrt D\<bar> = 2 * u * sqrt D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real (2 * u) * sqrt (real D)\<bar> = real (2 * u) * sqrt (real D)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>real (2 * u) * sqrt (real D)\<bar> = real (2 * u) * sqrt (real D)

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>real (2 * u) * sqrt (real D)\<bar> = real (2 * u) * sqrt (real D)

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
have "\<bar>t - u * sqrt D\<bar> \<le> 1 / u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real_of_int t - real u * sqrt (real D)\<bar> \<le> 1 / real u
[PROOF STEP]
using tu
[PROOF STATE]
proof (prove)
using this:
(t, u) \<in> S

goal (1 subgoal):
 1. \<bar>real_of_int t - real u * sqrt (real D)\<bar> \<le> 1 / real u
[PROOF STEP]
by (simp add: S_def)
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t - real u * sqrt (real D)\<bar> \<le> 1 / real u

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> x + real (2 * u) * sqrt (real D) \<le> y + real (2 * u) * sqrt (real D)) \<Longrightarrow> \<bar>real_of_int t + real u * sqrt (real D)\<bar> \<le> 1 / real u + real (2 * u) * sqrt (real D)
[PROOF STEP]
have le: "\<bar>t + u * sqrt D\<bar> \<le> 1 / u + 2 * u * sqrt D"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> x + real (2 * u) * sqrt (real D) \<le> y + real (2 * u) * sqrt (real D)) \<Longrightarrow> \<bar>real_of_int t + real u * sqrt (real D)\<bar> \<le> 1 / real u + real (2 * u) * sqrt (real D)

goal (1 subgoal):
 1. \<bar>real_of_int t + real u * sqrt (real D)\<bar> \<le> 1 / real u + real (2 * u) * sqrt (real D)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t + real u * sqrt (real D)\<bar> \<le> 1 / real u + real (2 * u) * sqrt (real D)

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
have "\<bar>t\<^sup>2 - u\<^sup>2 * D\<bar> = \<bar>t - u * sqrt D\<bar> * \<bar>t + u * sqrt D\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int \<bar>t\<^sup>2 - int (u\<^sup>2 * D)\<bar> = \<bar>real_of_int t - real u * sqrt (real D)\<bar> * \<bar>real_of_int t + real u * sqrt (real D)\<bar>
[PROOF STEP]
by (subst abs_mult [symmetric]) (simp add: algebra_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
real_of_int \<bar>t\<^sup>2 - int (u\<^sup>2 * D)\<bar> = \<bar>real_of_int t - real u * sqrt (real D)\<bar> * \<bar>real_of_int t + real u * sqrt (real D)\<bar>

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_int \<bar>t\<^sup>2 - int (u\<^sup>2 * D)\<bar> = \<bar>real_of_int t - real u * sqrt (real D)\<bar> * \<bar>real_of_int t + real u * sqrt (real D)\<bar>

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
have "\<dots> \<le> 1 / u * (1 / u + 2 * u * sqrt D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real_of_int t - real u * sqrt (real D)\<bar> * \<bar>real_of_int t + real u * sqrt (real D)\<bar> \<le> 1 / real u * (1 / real u + real (2 * u) * sqrt (real D))
[PROOF STEP]
using tu
[PROOF STATE]
proof (prove)
using this:
(t, u) \<in> S

goal (1 subgoal):
 1. \<bar>real_of_int t - real u * sqrt (real D)\<bar> * \<bar>real_of_int t + real u * sqrt (real D)\<bar> \<le> 1 / real u * (1 / real u + real (2 * u) * sqrt (real D))
[PROOF STEP]
by (intro mult_mono le) (auto simp: S_def)
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t - real u * sqrt (real D)\<bar> * \<bar>real_of_int t + real u * sqrt (real D)\<bar> \<le> 1 / real u * (1 / real u + real (2 * u) * sqrt (real D))

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int t - real u * sqrt (real D)\<bar> * \<bar>real_of_int t + real u * sqrt (real D)\<bar> \<le> 1 / real u * (1 / real u + real (2 * u) * sqrt (real D))

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
have "\<dots> = 1 / real u ^ 2 + 2 * sqrt D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / real u * (1 / real u + real (2 * u) * sqrt (real D)) = 1 / (real u)\<^sup>2 + 2 * sqrt (real D)
[PROOF STEP]
by (simp add: algebra_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
1 / real u * (1 / real u + real (2 * u) * sqrt (real D)) = 1 / (real u)\<^sup>2 + 2 * sqrt (real D)

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 / real u * (1 / real u + real (2 * u) * sqrt (real D)) = 1 / (real u)\<^sup>2 + 2 * sqrt (real D)

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
from \<open>u > 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < u
[PROOF STEP]
have "real u \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
0 < u

goal (1 subgoal):
 1. 1 \<le> real u
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
1 \<le> real u

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
hence "1 / real u ^ 2 \<le> 1 / 1 ^ 2"
[PROOF STATE]
proof (prove)
using this:
1 \<le> real u

goal (1 subgoal):
 1. 1 / (real u)\<^sup>2 \<le> 1 / 1\<^sup>2
[PROOF STEP]
by (intro divide_left_mono power_mono) auto
[PROOF STATE]
proof (state)
this:
1 / (real u)\<^sup>2 \<le> 1 / 1\<^sup>2

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> x + 2 * sqrt (real D) \<le> y + 2 * sqrt (real D)) \<Longrightarrow> real_of_int \<bar>t\<^sup>2 - int (u\<^sup>2 * D)\<bar> \<le> 1 / 1\<^sup>2 + 2 * sqrt (real D)
[PROOF STEP]
have "\<bar>t\<^sup>2 - u\<^sup>2 * D\<bar> \<le> 1 + 2 * sqrt D"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> x + 2 * sqrt (real D) \<le> y + 2 * sqrt (real D)) \<Longrightarrow> real_of_int \<bar>t\<^sup>2 - int (u\<^sup>2 * D)\<bar> \<le> 1 / 1\<^sup>2 + 2 * sqrt (real D)

goal (1 subgoal):
 1. real_of_int \<bar>t\<^sup>2 - int (u\<^sup>2 * D)\<bar> \<le> 1 + 2 * sqrt (real D)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real_of_int \<bar>t\<^sup>2 - int (u\<^sup>2 * D)\<bar> \<le> 1 + 2 * sqrt (real D)

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
hence "t\<^sup>2 - u\<^sup>2 * D \<ge> -M" "t\<^sup>2 - u\<^sup>2 * D \<le> M"
[PROOF STATE]
proof (prove)
using this:
real_of_int \<bar>t\<^sup>2 - int (u\<^sup>2 * D)\<bar> \<le> 1 + 2 * sqrt (real D)

goal (1 subgoal):
 1. - M \<le> t\<^sup>2 - int (u\<^sup>2 * D) &&& t\<^sup>2 - int (u\<^sup>2 * D) \<le> M
[PROOF STEP]
unfolding M_def
[PROOF STATE]
proof (prove)
using this:
real_of_int \<bar>t\<^sup>2 - int (u\<^sup>2 * D)\<bar> \<le> 1 + 2 * sqrt (real D)

goal (1 subgoal):
 1. - \<lfloor>1 + 2 * sqrt (real D)\<rfloor> \<le> t\<^sup>2 - int (u\<^sup>2 * D) &&& t\<^sup>2 - int (u\<^sup>2 * D) \<le> \<lfloor>1 + 2 * sqrt (real D)\<rfloor>
[PROOF STEP]
by linarith+
[PROOF STATE]
proof (state)
this:
- M \<le> t\<^sup>2 - int (u\<^sup>2 * D)
t\<^sup>2 - int (u\<^sup>2 * D) \<le> M

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> S \<Longrightarrow> a\<^sup>2 - int (b\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
thus "t\<^sup>2 - u\<^sup>2 * D \<in> {-M..M}"
[PROOF STATE]
proof (prove)
using this:
- M \<le> t\<^sup>2 - int (u\<^sup>2 * D)
t\<^sup>2 - int (u\<^sup>2 * D) \<le> M

goal (1 subgoal):
 1. t\<^sup>2 - int (u\<^sup>2 * D) \<in> {- M..M}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t\<^sup>2 - int (u\<^sup>2 * D) \<in> {- M..M}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>(t, u). t\<^sup>2 - int (u\<^sup>2 * D)) ` S \<subseteq> {- M..M}

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
hence fin: "finite (?f ` S)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>(t, u). t\<^sup>2 - int (u\<^sup>2 * D)) ` S \<subseteq> {- M..M}

goal (1 subgoal):
 1. finite ((\<lambda>(t, u). t\<^sup>2 - int (u\<^sup>2 * D)) ` S)
[PROOF STEP]
by (rule finite_subset) auto
[PROOF STATE]
proof (state)
this:
finite ((\<lambda>(t, u). t\<^sup>2 - int (u\<^sup>2 * D)) ` S)

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
from pigeonhole_infinite[OF infinite fin]
[PROOF STATE]
proof (chain)
picking this:
\<exists>a0\<in>S. infinite {a \<in> S. (case a of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = (case a0 of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D))}
[PROOF STEP]
obtain z where z: "z \<in> S" "infinite {z' \<in> S. ?f z' = ?f z}"
[PROOF STATE]
proof (prove)
using this:
\<exists>a0\<in>S. infinite {a \<in> S. (case a of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = (case a0 of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D))}

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> S; infinite {z' \<in> S. (case z' of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D))}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z \<in> S
infinite {z' \<in> S. (case z' of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D))}

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
define k where "k = ?f z"
[PROOF STATE]
proof (state)
this:
k = (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D))

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
with subset and z
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>(t, u). t\<^sup>2 - int (u\<^sup>2 * D)) ` S \<subseteq> {- M..M}
z \<in> S
infinite {z' \<in> S. (case z' of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D))}
k = (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D))
[PROOF STEP]
have k: "k \<in> {-M..M}" "infinite {z\<in>S. ?f z = k}"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>(t, u). t\<^sup>2 - int (u\<^sup>2 * D)) ` S \<subseteq> {- M..M}
z \<in> S
infinite {z' \<in> S. (case z' of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D))}
k = (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D))

goal (1 subgoal):
 1. k \<in> {- M..M} &&& infinite {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k}
[PROOF STEP]
by (auto simp: k_def)
[PROOF STATE]
proof (state)
this:
k \<in> {- M..M}
infinite {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k}

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
have k_nz: "k \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<noteq> 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k = 0 \<Longrightarrow> False
[PROOF STEP]
assume [simp]: "k = 0"
[PROOF STATE]
proof (state)
this:
k = 0

goal (1 subgoal):
 1. k = 0 \<Longrightarrow> False
[PROOF STEP]
note k(2)
[PROOF STATE]
proof (state)
this:
infinite {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k}

goal (1 subgoal):
 1. k = 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
infinite {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k}

goal (1 subgoal):
 1. k = 0 \<Longrightarrow> False
[PROOF STEP]
have "?f z \<noteq> 0" if "z \<in> S" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) \<noteq> 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = 0 \<Longrightarrow> False
[PROOF STEP]
assume *: "?f z = 0"
[PROOF STATE]
proof (state)
this:
(case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = 0

goal (1 subgoal):
 1. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = 0 \<Longrightarrow> False
[PROOF STEP]
obtain t u where [simp]: "z = (t, u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t u. z = (t, u) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases z)
[PROOF STATE]
proof (state)
this:
z = (t, u)

goal (1 subgoal):
 1. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = 0 \<Longrightarrow> False
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
(case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = 0
[PROOF STEP]
have "t ^ 2 = int u ^ 2 * int D"
[PROOF STATE]
proof (prove)
using this:
(case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = 0

goal (1 subgoal):
 1. t\<^sup>2 = (int u)\<^sup>2 * int D
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t\<^sup>2 = (int u)\<^sup>2 * int D

goal (1 subgoal):
 1. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = 0 \<Longrightarrow> False
[PROOF STEP]
hence "int u ^ 2 dvd t ^ 2"
[PROOF STATE]
proof (prove)
using this:
t\<^sup>2 = (int u)\<^sup>2 * int D

goal (1 subgoal):
 1. (int u)\<^sup>2 dvd t\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(int u)\<^sup>2 dvd t\<^sup>2

goal (1 subgoal):
 1. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = 0 \<Longrightarrow> False
[PROOF STEP]
hence "int u dvd t"
[PROOF STATE]
proof (prove)
using this:
(int u)\<^sup>2 dvd t\<^sup>2

goal (1 subgoal):
 1. int u dvd t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
int u dvd t

goal (1 subgoal):
 1. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = 0 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
int u dvd t
[PROOF STEP]
obtain k where [simp]: "t = int u * k"
[PROOF STATE]
proof (prove)
using this:
int u dvd t

goal (1 subgoal):
 1. (\<And>k. t = int u * k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim!: dvdE)
[PROOF STATE]
proof (state)
this:
t = int u * k

goal (1 subgoal):
 1. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = 0 \<Longrightarrow> False
[PROOF STEP]
from * and \<open>z \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
(case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = 0
z \<in> S
[PROOF STEP]
have "k ^ 2 = int D"
[PROOF STATE]
proof (prove)
using this:
(case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = 0
z \<in> S

goal (1 subgoal):
 1. k\<^sup>2 = int D
[PROOF STEP]
by (auto simp: power_mult_distrib S_def)
[PROOF STATE]
proof (state)
this:
k\<^sup>2 = int D

goal (1 subgoal):
 1. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
k\<^sup>2 = int D

goal (1 subgoal):
 1. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = 0 \<Longrightarrow> False
[PROOF STEP]
have "k ^ 2 = int (nat \<bar>k\<bar> ^ 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k\<^sup>2 = int ((nat \<bar>k\<bar>)\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k\<^sup>2 = int ((nat \<bar>k\<bar>)\<^sup>2)

goal (1 subgoal):
 1. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = 0 \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
int ((nat \<bar>k\<bar>)\<^sup>2) = int D
[PROOF STEP]
have "D = nat \<bar>k\<bar> ^ 2"
[PROOF STATE]
proof (prove)
using this:
int ((nat \<bar>k\<bar>)\<^sup>2) = int D

goal (1 subgoal):
 1. D = (nat \<bar>k\<bar>)\<^sup>2
[PROOF STEP]
by (simp only: of_nat_eq_iff)
[PROOF STATE]
proof (state)
this:
D = (nat \<bar>k\<bar>)\<^sup>2

goal (1 subgoal):
 1. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = 0 \<Longrightarrow> False
[PROOF STEP]
hence "is_square D"
[PROOF STATE]
proof (prove)
using this:
D = (nat \<bar>k\<bar>)\<^sup>2

goal (1 subgoal):
 1. is_square D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_square D

goal (1 subgoal):
 1. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = 0 \<Longrightarrow> False
[PROOF STEP]
with nonsquare_D
[PROOF STATE]
proof (chain)
picking this:
\<not> is_square D
is_square D
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> is_square D
is_square D

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?z \<in> S \<Longrightarrow> (case ?z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) \<noteq> 0

goal (1 subgoal):
 1. k = 0 \<Longrightarrow> False
[PROOF STEP]
hence "{z\<in>S. ?f z = k} = {}"
[PROOF STATE]
proof (prove)
using this:
?z \<in> S \<Longrightarrow> (case ?z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) \<noteq> 0

goal (1 subgoal):
 1. {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k} = {}

goal (1 subgoal):
 1. k = 0 \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
infinite {}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
infinite {}

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:
k \<noteq> 0

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
let ?h = "\<lambda>(t :: int, u :: nat). (t mod (abs k), u mod (abs k))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
have "?h ` {z\<in>S. ?f z = k} \<subseteq> {0..<abs k} \<times> {0..< abs k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(t, x). (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>)) ` {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k} \<subseteq> {0..<\<bar>k\<bar>} \<times> {0..<\<bar>k\<bar>}
[PROOF STEP]
using k_nz
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0

goal (1 subgoal):
 1. (\<lambda>(t, x). (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>)) ` {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k} \<subseteq> {0..<\<bar>k\<bar>} \<times> {0..<\<bar>k\<bar>}
[PROOF STEP]
by (auto simp: case_prod_unfold)
[PROOF STATE]
proof (state)
this:
(\<lambda>(t, x). (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>)) ` {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k} \<subseteq> {0..<\<bar>k\<bar>} \<times> {0..<\<bar>k\<bar>}

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
hence "finite (?h ` {z\<in>S. ?f z = k})"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>(t, x). (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>)) ` {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k} \<subseteq> {0..<\<bar>k\<bar>} \<times> {0..<\<bar>k\<bar>}

goal (1 subgoal):
 1. finite ((\<lambda>(t, x). (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>)) ` {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k})
[PROOF STEP]
by (rule finite_subset) auto
[PROOF STATE]
proof (state)
this:
finite ((\<lambda>(t, x). (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>)) ` {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k})

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
from pigeonhole_infinite[OF k(2) this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>a0\<in>{z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k}. infinite {a \<in> {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k}. (case a of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>)) = (case a0 of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>))}
[PROOF STEP]
obtain z'
    where z': "z' \<in> S" "?f z' = k" "infinite {z''\<in>{z\<in>S. ?f z = k}. ?h z'' = ?h z'}"
[PROOF STATE]
proof (prove)
using this:
\<exists>a0\<in>{z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k}. infinite {a \<in> {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k}. (case a of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>)) = (case a0 of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>))}

goal (1 subgoal):
 1. (\<And>z'. \<lbrakk>z' \<in> S; (case z' of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k; infinite {z'' \<in> {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k}. (case z'' of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>)) = (case z' of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>))}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z' \<in> S
(case z' of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k
infinite {z'' \<in> {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k}. (case z'' of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>)) = (case z' of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>))}

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
define l1 and l2 where "l1 = fst (?h z')" and "l2 = snd (?h z')"
[PROOF STATE]
proof (state)
this:
l1 = fst (case z' of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>))
l2 = snd (case z' of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>))

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
define S' where "S' = {(t,u) \<in> S. ?f (t,u) = k \<and> t mod abs k = l1 \<and> u mod abs k = l2}"
[PROOF STATE]
proof (state)
this:
S' = {(t, u). (t, u) \<in> S \<and> (case (t, u) of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k \<and> t mod \<bar>k\<bar> = l1 \<and> int u mod \<bar>k\<bar> = l2}

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
note z'(3)
[PROOF STATE]
proof (state)
this:
infinite {z'' \<in> {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k}. (case z'' of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>)) = (case z' of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>))}

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
infinite {z'' \<in> {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k}. (case z'' of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>)) = (case z' of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>))}

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
have "{z''\<in>{z\<in>S. ?f z = k}. ?h z'' = ?h z'} = S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {z'' \<in> {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k}. (case z'' of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>)) = (case z' of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>))} = S'
[PROOF STEP]
by (auto simp: l1_def l2_def case_prod_unfold S'_def)
[PROOF STATE]
proof (state)
this:
{z'' \<in> {z \<in> S. (case z of (t, u) \<Rightarrow> t\<^sup>2 - int (u\<^sup>2 * D)) = k}. (case z'' of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>)) = (case z' of (t, x) \<Rightarrow> (t mod \<bar>k\<bar>, int x mod \<bar>k\<bar>))} = S'

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
infinite S'
[PROOF STEP]
have infinite: "infinite S'"
[PROOF STATE]
proof (prove)
using this:
infinite S'

goal (1 subgoal):
 1. infinite S'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
infinite S'

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
from z'(1) and k_nz
[PROOF STATE]
proof (chain)
picking this:
z' \<in> S
k \<noteq> 0
[PROOF STEP]
have l12: "l1 \<in> {0..<abs k}" "l2 \<in> {0..<abs k}"
[PROOF STATE]
proof (prove)
using this:
z' \<in> S
k \<noteq> 0

goal (1 subgoal):
 1. l1 \<in> {0..<\<bar>k\<bar>} &&& l2 \<in> {0..<\<bar>k\<bar>}
[PROOF STEP]
by (auto simp: l1_def l2_def case_prod_unfold)
[PROOF STATE]
proof (state)
this:
l1 \<in> {0..<\<bar>k\<bar>}
l2 \<in> {0..<\<bar>k\<bar>}

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
from infinite_arbitrarily_large[OF infinite]
[PROOF STATE]
proof (chain)
picking this:
\<exists>B. finite B \<and> card B = ?n \<and> B \<subseteq> S'
[PROOF STEP]
obtain X where X: "finite X" "card X = 2" "X \<subseteq> S'"
[PROOF STATE]
proof (prove)
using this:
\<exists>B. finite B \<and> card B = ?n \<and> B \<subseteq> S'

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>finite X; card X = 2; X \<subseteq> S'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite X
card X = 2
X \<subseteq> S'

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
from finite_distinct_list[OF this(1)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>xs. set xs = X \<and> distinct xs
[PROOF STEP]
obtain xs where xs: "set xs = X" "distinct xs"
[PROOF STATE]
proof (prove)
using this:
\<exists>xs. set xs = X \<and> distinct xs

goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>set xs = X; distinct xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set xs = X
distinct xs

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
with X
[PROOF STATE]
proof (chain)
picking this:
finite X
card X = 2
X \<subseteq> S'
set xs = X
distinct xs
[PROOF STEP]
have "length xs = 2"
[PROOF STATE]
proof (prove)
using this:
finite X
card X = 2
X \<subseteq> S'
set xs = X
distinct xs

goal (1 subgoal):
 1. length xs = 2
[PROOF STEP]
using distinct_card[of xs]
[PROOF STATE]
proof (prove)
using this:
finite X
card X = 2
X \<subseteq> S'
set xs = X
distinct xs
distinct xs \<Longrightarrow> card (set xs) = length xs

goal (1 subgoal):
 1. length xs = 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length xs = 2

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs = 2
[PROOF STEP]
obtain z1 z2 where [simp]: "xs = [z1, z2]"
[PROOF STATE]
proof (prove)
using this:
length xs = 2

goal (1 subgoal):
 1. (\<And>z1 z2. xs = [z1, z2] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: length_Suc_conv eval_nat_numeral)
[PROOF STATE]
proof (state)
this:
xs = [z1, z2]

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
from X xs
[PROOF STATE]
proof (chain)
picking this:
finite X
card X = 2
X \<subseteq> S'
set xs = X
distinct xs
[PROOF STEP]
have S': "z1 \<in> S'" "z2 \<in> S'" and neq: "z1 \<noteq> z2"
[PROOF STATE]
proof (prove)
using this:
finite X
card X = 2
X \<subseteq> S'
set xs = X
distinct xs

goal (1 subgoal):
 1. (z1 \<in> S' &&& z2 \<in> S') &&& z1 \<noteq> z2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z1 \<in> S'
z2 \<in> S'
z1 \<noteq> z2

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
define t1 u1 t2 u2 where "t1 = fst z1" and "u1 = snd z1" and "t2 = fst z2" and "u2 = snd z2"
[PROOF STATE]
proof (state)
this:
t1 = fst z1
u1 = snd z1
t2 = fst z2
u2 = snd z2

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
have [simp]: "z1 = (t1, u1)" "z2 = (t2, u2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z1 = (t1, u1) &&& z2 = (t2, u2)
[PROOF STEP]
by (simp_all add: t1_def u1_def t2_def u2_def)
[PROOF STATE]
proof (state)
this:
z1 = (t1, u1)
z2 = (t2, u2)

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
from S'
[PROOF STATE]
proof (chain)
picking this:
z1 \<in> S'
z2 \<in> S'
[PROOF STEP]
have * [simp]: "t1 mod abs k = l1" "t2 mod abs k = l1" "u1 mod abs k = l2" "u2 mod abs k = l2"
[PROOF STATE]
proof (prove)
using this:
z1 \<in> S'
z2 \<in> S'

goal (1 subgoal):
 1. (t1 mod \<bar>k\<bar> = l1 &&& t2 mod \<bar>k\<bar> = l1) &&& int u1 mod \<bar>k\<bar> = l2 &&& int u2 mod \<bar>k\<bar> = l2
[PROOF STEP]
by (simp_all add: S'_def)
[PROOF STATE]
proof (state)
this:
t1 mod \<bar>k\<bar> = l1
t2 mod \<bar>k\<bar> = l1
int u1 mod \<bar>k\<bar> = l2
int u2 mod \<bar>k\<bar> = l2

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
define x where "x = (t1 * t2 - D * u1 * u2) div k"
[PROOF STATE]
proof (state)
this:
x = (t1 * t2 - int (D * u1 * u2)) div k

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
define y where "y = (t1 * u2 - t2 * u1) div k"
[PROOF STATE]
proof (state)
this:
y = (t1 * int u2 - t2 * int u1) div k

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
from S'
[PROOF STATE]
proof (chain)
picking this:
z1 \<in> S'
z2 \<in> S'
[PROOF STEP]
have "(t1\<^sup>2 - u1\<^sup>2 * D) = k" "(t2\<^sup>2 - u2\<^sup>2 * D) = k"
[PROOF STATE]
proof (prove)
using this:
z1 \<in> S'
z2 \<in> S'

goal (1 subgoal):
 1. t1\<^sup>2 - int (u1\<^sup>2 * D) = k &&& t2\<^sup>2 - int (u2\<^sup>2 * D) = k
[PROOF STEP]
by (auto simp: S'_def)
[PROOF STATE]
proof (state)
this:
t1\<^sup>2 - int (u1\<^sup>2 * D) = k
t2\<^sup>2 - int (u2\<^sup>2 * D) = k

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
hence "(t1\<^sup>2 - u1\<^sup>2 * D) * (t2\<^sup>2 - u2\<^sup>2 * D) = k ^ 2"
[PROOF STATE]
proof (prove)
using this:
t1\<^sup>2 - int (u1\<^sup>2 * D) = k
t2\<^sup>2 - int (u2\<^sup>2 * D) = k

goal (1 subgoal):
 1. (t1\<^sup>2 - int (u1\<^sup>2 * D)) * (t2\<^sup>2 - int (u2\<^sup>2 * D)) = k\<^sup>2
[PROOF STEP]
unfolding power2_eq_square
[PROOF STATE]
proof (prove)
using this:
t1 * t1 - int (u1 * u1 * D) = k
t2 * t2 - int (u2 * u2 * D) = k

goal (1 subgoal):
 1. (t1 * t1 - int (u1 * u1 * D)) * (t2 * t2 - int (u2 * u2 * D)) = k * k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(t1\<^sup>2 - int (u1\<^sup>2 * D)) * (t2\<^sup>2 - int (u2\<^sup>2 * D)) = k\<^sup>2

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(t1\<^sup>2 - int (u1\<^sup>2 * D)) * (t2\<^sup>2 - int (u2\<^sup>2 * D)) = k\<^sup>2

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
have "(t1\<^sup>2 - u1\<^sup>2 * D) * (t2\<^sup>2 - u2\<^sup>2 * D) =
               (t1 * t2 - D * u1 * u2) ^ 2 - D * (t1 * u2 - t2 * u1) ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t1\<^sup>2 - int (u1\<^sup>2 * D)) * (t2\<^sup>2 - int (u2\<^sup>2 * D)) = (t1 * t2 - int (D * u1 * u2))\<^sup>2 - int D * (t1 * int u2 - t2 * int u1)\<^sup>2
[PROOF STEP]
by (simp add: power2_eq_square algebra_simps)
[PROOF STATE]
proof (state)
this:
(t1\<^sup>2 - int (u1\<^sup>2 * D)) * (t2\<^sup>2 - int (u2\<^sup>2 * D)) = (t1 * t2 - int (D * u1 * u2))\<^sup>2 - int D * (t1 * int u2 - t2 * int u1)\<^sup>2

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(t1 * t2 - int (D * u1 * u2))\<^sup>2 - int D * (t1 * int u2 - t2 * int u1)\<^sup>2 = k\<^sup>2
[PROOF STEP]
have eq: "(t1 * t2 - D * u1 * u2)\<^sup>2 - D * (t1 * u2 - t2 * u1)\<^sup>2 = k\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
(t1 * t2 - int (D * u1 * u2))\<^sup>2 - int D * (t1 * int u2 - t2 * int u1)\<^sup>2 = k\<^sup>2

goal (1 subgoal):
 1. (t1 * t2 - int (D * u1 * u2))\<^sup>2 - int D * (t1 * int u2 - t2 * int u1)\<^sup>2 = k\<^sup>2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(t1 * t2 - int (D * u1 * u2))\<^sup>2 - int D * (t1 * int u2 - t2 * int u1)\<^sup>2 = k\<^sup>2

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
have "(t1 * u2 - t2 * u1) mod abs k = (l1 * l2 - l1 * l2) mod abs k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t1 * int u2 - t2 * int u1) mod \<bar>k\<bar> = (l1 * l2 - l1 * l2) mod \<bar>k\<bar>
[PROOF STEP]
using l12
[PROOF STATE]
proof (prove)
using this:
l1 \<in> {0..<\<bar>k\<bar>}
l2 \<in> {0..<\<bar>k\<bar>}

goal (1 subgoal):
 1. (t1 * int u2 - t2 * int u1) mod \<bar>k\<bar> = (l1 * l2 - l1 * l2) mod \<bar>k\<bar>
[PROOF STEP]
by (intro mod_diff_cong mod_mult_cong) (auto simp: mod_pos_pos_trivial)
[PROOF STATE]
proof (state)
this:
(t1 * int u2 - t2 * int u1) mod \<bar>k\<bar> = (l1 * l2 - l1 * l2) mod \<bar>k\<bar>

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
hence dvd1: "k dvd t1 * u2 - t2 * u1"
[PROOF STATE]
proof (prove)
using this:
(t1 * int u2 - t2 * int u1) mod \<bar>k\<bar> = (l1 * l2 - l1 * l2) mod \<bar>k\<bar>

goal (1 subgoal):
 1. k dvd t1 * int u2 - t2 * int u1
[PROOF STEP]
by (simp add: mod_eq_0_iff_dvd)
[PROOF STATE]
proof (state)
this:
k dvd t1 * int u2 - t2 * int u1

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
have "k\<^sup>2 dvd k\<^sup>2 + D * (t1 * u2 - t2 * u1)\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k\<^sup>2 dvd k\<^sup>2 + int D * (t1 * int u2 - t2 * int u1)\<^sup>2
[PROOF STEP]
using dvd1
[PROOF STATE]
proof (prove)
using this:
k dvd t1 * int u2 - t2 * int u1

goal (1 subgoal):
 1. k\<^sup>2 dvd k\<^sup>2 + int D * (t1 * int u2 - t2 * int u1)\<^sup>2
[PROOF STEP]
by (intro dvd_add) auto
[PROOF STATE]
proof (state)
this:
k\<^sup>2 dvd k\<^sup>2 + int D * (t1 * int u2 - t2 * int u1)\<^sup>2

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
k\<^sup>2 dvd k\<^sup>2 + int D * (t1 * int u2 - t2 * int u1)\<^sup>2

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
from eq
[PROOF STATE]
proof (chain)
picking this:
(t1 * t2 - int (D * u1 * u2))\<^sup>2 - int D * (t1 * int u2 - t2 * int u1)\<^sup>2 = k\<^sup>2
[PROOF STEP]
have "\<dots> = (t1 * t2 - D * u1 * u2)\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
(t1 * t2 - int (D * u1 * u2))\<^sup>2 - int D * (t1 * int u2 - t2 * int u1)\<^sup>2 = k\<^sup>2

goal (1 subgoal):
 1. k\<^sup>2 + int D * (t1 * int u2 - t2 * int u1)\<^sup>2 = (t1 * t2 - int (D * u1 * u2))\<^sup>2
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
k\<^sup>2 + int D * (t1 * int u2 - t2 * int u1)\<^sup>2 = (t1 * t2 - int (D * u1 * u2))\<^sup>2

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
k\<^sup>2 dvd (t1 * t2 - int (D * u1 * u2))\<^sup>2
[PROOF STEP]
have dvd2: "k dvd t1 * t2 - D * u1 * u2"
[PROOF STATE]
proof (prove)
using this:
k\<^sup>2 dvd (t1 * t2 - int (D * u1 * u2))\<^sup>2

goal (1 subgoal):
 1. k dvd t1 * t2 - int (D * u1 * u2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k dvd t1 * t2 - int (D * u1 * u2)

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
note eq
[PROOF STATE]
proof (state)
this:
(t1 * t2 - int (D * u1 * u2))\<^sup>2 - int D * (t1 * int u2 - t2 * int u1)\<^sup>2 = k\<^sup>2

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(t1 * t2 - int (D * u1 * u2))\<^sup>2 - int D * (t1 * int u2 - t2 * int u1)\<^sup>2 = k\<^sup>2

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
from dvd2
[PROOF STATE]
proof (chain)
picking this:
k dvd t1 * t2 - int (D * u1 * u2)
[PROOF STEP]
have "t1 * t2 - D * u1 * u2 = k * x"
[PROOF STATE]
proof (prove)
using this:
k dvd t1 * t2 - int (D * u1 * u2)

goal (1 subgoal):
 1. t1 * t2 - int (D * u1 * u2) = k * x
[PROOF STEP]
by (simp add: x_def)
[PROOF STATE]
proof (state)
this:
t1 * t2 - int (D * u1 * u2) = k * x

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
t1 * t2 - int (D * u1 * u2) = k * x

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
from dvd1
[PROOF STATE]
proof (chain)
picking this:
k dvd t1 * int u2 - t2 * int u1
[PROOF STEP]
have "t1 * u2 - t2 * u1 = k * y"
[PROOF STATE]
proof (prove)
using this:
k dvd t1 * int u2 - t2 * int u1

goal (1 subgoal):
 1. t1 * int u2 - t2 * int u1 = k * y
[PROOF STEP]
by (simp add: y_def)
[PROOF STATE]
proof (state)
this:
t1 * int u2 - t2 * int u1 = k * y

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
t1 * int u2 - t2 * int u1 = k * y

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
have "(k * x)\<^sup>2 - D * (k * y)\<^sup>2 = k\<^sup>2 * (x\<^sup>2 - D * y\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (k * x)\<^sup>2 - int D * (k * y)\<^sup>2 = k\<^sup>2 * (x\<^sup>2 - int D * y\<^sup>2)
[PROOF STEP]
by (simp add: power_mult_distrib algebra_simps)
[PROOF STATE]
proof (state)
this:
(k * x)\<^sup>2 - int D * (k * y)\<^sup>2 = k\<^sup>2 * (x\<^sup>2 - int D * y\<^sup>2)

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
k\<^sup>2 * (x\<^sup>2 - int D * y\<^sup>2) = k\<^sup>2
[PROOF STEP]
have eq': "x\<^sup>2 - D * y\<^sup>2 = 1"
[PROOF STATE]
proof (prove)
using this:
k\<^sup>2 * (x\<^sup>2 - int D * y\<^sup>2) = k\<^sup>2

goal (1 subgoal):
 1. x\<^sup>2 - int D * y\<^sup>2 = 1
[PROOF STEP]
using k_nz
[PROOF STATE]
proof (prove)
using this:
k\<^sup>2 * (x\<^sup>2 - int D * y\<^sup>2) = k\<^sup>2
k \<noteq> 0

goal (1 subgoal):
 1. x\<^sup>2 - int D * y\<^sup>2 = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x\<^sup>2 - int D * y\<^sup>2 = 1

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
hence "x\<^sup>2 = 1 + D * y\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
x\<^sup>2 - int D * y\<^sup>2 = 1

goal (1 subgoal):
 1. x\<^sup>2 = 1 + int D * y\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x\<^sup>2 = 1 + int D * y\<^sup>2

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x\<^sup>2 = 1 + int D * y\<^sup>2

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
have "x\<^sup>2 = int (nat \<bar>x\<bar> ^ 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>2 = int ((nat \<bar>x\<bar>)\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x\<^sup>2 = int ((nat \<bar>x\<bar>)\<^sup>2)

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x\<^sup>2 = int ((nat \<bar>x\<bar>)\<^sup>2)

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
have "1 + D * y\<^sup>2 = int (1 + D * nat \<bar>y\<bar> ^ 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + int D * y\<^sup>2 = int (1 + D * (nat \<bar>y\<bar>)\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 + int D * y\<^sup>2 = int (1 + D * (nat \<bar>y\<bar>)\<^sup>2)

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 + int D * y\<^sup>2 = int (1 + D * (nat \<bar>y\<bar>)\<^sup>2)

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
note of_nat_eq_iff
[PROOF STATE]
proof (state)
this:
(of_nat ?m = of_nat ?n) = (?m = ?n)

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(nat \<bar>x\<bar>)\<^sup>2 = 1 + D * (nat \<bar>y\<bar>)\<^sup>2
[PROOF STEP]
have eq'': "(nat \<bar>x\<bar>)\<^sup>2 = 1 + D * (nat \<bar>y\<bar>)\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
(nat \<bar>x\<bar>)\<^sup>2 = 1 + D * (nat \<bar>y\<bar>)\<^sup>2

goal (1 subgoal):
 1. (nat \<bar>x\<bar>)\<^sup>2 = 1 + D * (nat \<bar>y\<bar>)\<^sup>2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(nat \<bar>x\<bar>)\<^sup>2 = 1 + D * (nat \<bar>y\<bar>)\<^sup>2

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
have "t1 * u2 \<noteq> t2 * u1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t1 * int u2 \<noteq> t2 * int u1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t1 * int u2 = t2 * int u1 \<Longrightarrow> False
[PROOF STEP]
assume *: "t1 * u2 = t2 * u1"
[PROOF STATE]
proof (state)
this:
t1 * int u2 = t2 * int u1

goal (1 subgoal):
 1. t1 * int u2 = t2 * int u1 \<Longrightarrow> False
[PROOF STEP]
hence "\<bar>t1\<bar> * \<bar>u2\<bar> = \<bar>t2\<bar> * \<bar>u1\<bar>"
[PROOF STATE]
proof (prove)
using this:
t1 * int u2 = t2 * int u1

goal (1 subgoal):
 1. \<bar>t1\<bar> * \<bar>int u2\<bar> = \<bar>t2\<bar> * \<bar>int u1\<bar>
[PROOF STEP]
by (simp only: abs_mult [symmetric])
[PROOF STATE]
proof (state)
this:
\<bar>t1\<bar> * \<bar>int u2\<bar> = \<bar>t2\<bar> * \<bar>int u1\<bar>

goal (1 subgoal):
 1. t1 * int u2 = t2 * int u1 \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>t1\<bar> * \<bar>int u2\<bar> = \<bar>t2\<bar> * \<bar>int u1\<bar>

goal (1 subgoal):
 1. t1 * int u2 = t2 * int u1 \<Longrightarrow> False
[PROOF STEP]
from S'
[PROOF STATE]
proof (chain)
picking this:
z1 \<in> S'
z2 \<in> S'
[PROOF STEP]
have "coprime u1 t1" "coprime u2 t2"
[PROOF STATE]
proof (prove)
using this:
z1 \<in> S'
z2 \<in> S'

goal (1 subgoal):
 1. coprime (int u1) t1 &&& coprime (int u2) t2
[PROOF STEP]
by (auto simp: S'_def S_def)
[PROOF STATE]
proof (state)
this:
coprime (int u1) t1
coprime (int u2) t2

goal (1 subgoal):
 1. t1 * int u2 = t2 * int u1 \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>t1\<bar> * \<bar>int u2\<bar> = \<bar>t2\<bar> * \<bar>int u1\<bar>
coprime (int u1) t1
coprime (int u2) t2
[PROOF STEP]
have eq: "\<bar>t1\<bar> = \<bar>t2\<bar> \<and> u1 = u2"
[PROOF STATE]
proof (prove)
using this:
\<bar>t1\<bar> * \<bar>int u2\<bar> = \<bar>t2\<bar> * \<bar>int u1\<bar>
coprime (int u1) t1
coprime (int u2) t2

goal (1 subgoal):
 1. \<bar>t1\<bar> = \<bar>t2\<bar> \<and> u1 = u2
[PROOF STEP]
by (subst (asm) coprime_crossproduct_int) (auto simp: S'_def S_def gcd.commute coprime_commute)
[PROOF STATE]
proof (state)
this:
\<bar>t1\<bar> = \<bar>t2\<bar> \<and> u1 = u2

goal (1 subgoal):
 1. t1 * int u2 = t2 * int u1 \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>t1\<bar> = \<bar>t2\<bar> \<and> u1 = u2

goal (1 subgoal):
 1. t1 * int u2 = t2 * int u1 \<Longrightarrow> False
[PROOF STEP]
from S'
[PROOF STATE]
proof (chain)
picking this:
z1 \<in> S'
z2 \<in> S'
[PROOF STEP]
have "u1 \<noteq> 0" "u2 \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
z1 \<in> S'
z2 \<in> S'

goal (1 subgoal):
 1. u1 \<noteq> 0 &&& u2 \<noteq> 0
[PROOF STEP]
by (auto simp: S'_def S_def)
[PROOF STATE]
proof (state)
this:
u1 \<noteq> 0
u2 \<noteq> 0

goal (1 subgoal):
 1. t1 * int u2 = t2 * int u1 \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>t1\<bar> = \<bar>t2\<bar> \<and> u1 = u2
u1 \<noteq> 0
u2 \<noteq> 0
[PROOF STEP]
have "t1 = t2"
[PROOF STATE]
proof (prove)
using this:
\<bar>t1\<bar> = \<bar>t2\<bar> \<and> u1 = u2
u1 \<noteq> 0
u2 \<noteq> 0

goal (1 subgoal):
 1. t1 = t2
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<bar>t1\<bar> = \<bar>t2\<bar> \<and> u1 = u2
u1 \<noteq> 0
u2 \<noteq> 0
t1 * int u2 = t2 * int u1

goal (1 subgoal):
 1. t1 = t2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t1 = t2

goal (1 subgoal):
 1. t1 * int u2 = t2 * int u1 \<Longrightarrow> False
[PROOF STEP]
with eq and neq
[PROOF STATE]
proof (chain)
picking this:
\<bar>t1\<bar> = \<bar>t2\<bar> \<and> u1 = u2
z1 \<noteq> z2
t1 = t2
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<bar>t1\<bar> = \<bar>t2\<bar> \<and> u1 = u2
z1 \<noteq> z2
t1 = t2

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t1 * int u2 \<noteq> t2 * int u1

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
with dvd1
[PROOF STATE]
proof (chain)
picking this:
k dvd t1 * int u2 - t2 * int u1
t1 * int u2 \<noteq> t2 * int u1
[PROOF STEP]
have "y \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
k dvd t1 * int u2 - t2 * int u1
t1 * int u2 \<noteq> t2 * int u1

goal (1 subgoal):
 1. y \<noteq> 0
[PROOF STEP]
by (auto simp add: y_def dvd_div_eq_0_iff)
[PROOF STATE]
proof (state)
this:
y \<noteq> 0

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
hence "nat \<bar>y\<bar> \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
y \<noteq> 0

goal (1 subgoal):
 1. nat \<bar>y\<bar> \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat \<bar>y\<bar> \<noteq> 0

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
with eq''
[PROOF STATE]
proof (chain)
picking this:
(nat \<bar>x\<bar>)\<^sup>2 = 1 + D * (nat \<bar>y\<bar>)\<^sup>2
nat \<bar>y\<bar> \<noteq> 0
[PROOF STEP]
show "\<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
(nat \<bar>x\<bar>)\<^sup>2 = 1 + D * (nat \<bar>y\<bar>)\<^sup>2
nat \<bar>y\<bar> \<noteq> 0

goal (1 subgoal):
 1. \<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nontriv_solution_altdef: "nontriv_solution z \<longleftrightarrow> solution z \<and> z \<noteq> (1, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nontriv_solution z = (solution z \<and> z \<noteq> (1::'a, 0::'a))
[PROOF STEP]
by (auto simp: solution_def nontriv_solution_def)


[STATEMENT]
lemma solution_trivial_nat [simp, intro]: "solution (Suc 0, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution (Suc 0, 0)
[PROOF STEP]
by (simp add: solution_def)


[STATEMENT]
lemma solution_trivial [simp, intro]: "solution (1, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution (1::'a, 0::'a)
[PROOF STEP]
by (simp add: solution_def)


[STATEMENT]
lemma solution_uminus_left [simp]: "solution (-x, y :: 'a :: comm_ring_1) \<longleftrightarrow> solution (x, y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution (- x, y) = solution (x, y)
[PROOF STEP]
by (simp add: solution_def)


[STATEMENT]
lemma solution_uminus_right [simp]: "solution (x, -y :: 'a :: comm_ring_1) \<longleftrightarrow> solution (x, y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution (x, - y) = solution (x, y)
[PROOF STEP]
by (simp add: solution_def)


[STATEMENT]
lemma solution_0_snd_nat_iff [simp]: "solution (a :: nat, 0) \<longleftrightarrow> a = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution (a, 0) = (a = 1)
[PROOF STEP]
by (auto simp: solution_def)


[STATEMENT]
lemma solution_0_snd_iff [simp]: "solution (a :: 'a :: idom, 0) \<longleftrightarrow> a \<in> {1, -1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution (a, 0::'a) = (a \<in> {1::'a, - (1::'a)})
[PROOF STEP]
by (auto simp: solution_def power2_eq_1_iff)


[STATEMENT]
lemma no_solution_0_fst_nat [simp]: "\<not>solution (0, b :: nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> solution (0, b)
[PROOF STEP]
by (auto simp: solution_def)


[STATEMENT]
lemma no_solution_0_fst_int [simp]: "\<not>solution (0, b :: int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> solution (0, b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> solution (0, b)
[PROOF STEP]
have "1 + int D * b\<^sup>2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 + int D * b\<^sup>2
[PROOF STEP]
by (intro add_pos_nonneg) auto
[PROOF STATE]
proof (state)
this:
0 < 1 + int D * b\<^sup>2

goal (1 subgoal):
 1. \<not> solution (0, b)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < 1 + int D * b\<^sup>2

goal (1 subgoal):
 1. \<not> solution (0, b)
[PROOF STEP]
by (auto simp add: solution_def)
[PROOF STATE]
proof (state)
this:
\<not> solution (0, b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma solution_of_nat_of_nat [simp]:
  "solution (of_nat a, of_nat b :: 'a :: {comm_ring_1, ring_char_0}) \<longleftrightarrow> solution (a, b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution (of_nat a, of_nat b) = solution (a, b)
[PROOF STEP]
by (simp only: solution_def prod.case of_nat_power [symmetric]
                 of_nat_1 [symmetric, where ?'a = 'a] of_nat_add [symmetric]
                 of_nat_mult [symmetric] of_nat_eq_iff of_nat_id)


[STATEMENT]
lemma solution_of_nat_of_nat' [simp]:
  "solution (case z of (a, b) \<Rightarrow> (of_nat a, of_nat b :: 'a :: {comm_ring_1, ring_char_0})) \<longleftrightarrow>
     solution z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution (case z of (a, b) \<Rightarrow> (of_nat a, of_nat b)) = solution z
[PROOF STEP]
by (auto simp: case_prod_unfold)


[STATEMENT]
lemma solution_nat_abs_nat_abs [simp]:
  "solution (nat \<bar>x\<bar>, nat \<bar>y\<bar>) \<longleftrightarrow> solution (x, y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution (nat \<bar>x\<bar>, nat \<bar>y\<bar>) = solution (x, y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. solution (nat \<bar>x\<bar>, nat \<bar>y\<bar>) = solution (x, y)
[PROOF STEP]
define x' and y' where "x' = nat \<bar>x\<bar>" and "y' = nat \<bar>y\<bar>"
[PROOF STATE]
proof (state)
this:
x' = nat \<bar>x\<bar>
y' = nat \<bar>y\<bar>

goal (1 subgoal):
 1. solution (nat \<bar>x\<bar>, nat \<bar>y\<bar>) = solution (x, y)
[PROOF STEP]
have x: "x = sgn x * x'" and y: "y = sgn y * y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = sgn x * int x' &&& y = sgn y * int y'
[PROOF STEP]
by (auto simp: x'_def y'_def sgn_if)
[PROOF STATE]
proof (state)
this:
x = sgn x * int x'
y = sgn y * int y'

goal (1 subgoal):
 1. solution (nat \<bar>x\<bar>, nat \<bar>y\<bar>) = solution (x, y)
[PROOF STEP]
have [simp]: "x = 0 \<longleftrightarrow> x' = 0" "y = 0 \<longleftrightarrow> y' = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x = 0) = (x' = 0) &&& (y = 0) = (y' = 0)
[PROOF STEP]
by (auto simp: x'_def y'_def)
[PROOF STATE]
proof (state)
this:
(x = 0) = (x' = 0)
(y = 0) = (y' = 0)

goal (1 subgoal):
 1. solution (nat \<bar>x\<bar>, nat \<bar>y\<bar>) = solution (x, y)
[PROOF STEP]
show "solution (x', y') \<longleftrightarrow> solution (x, y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution (x', y') = solution (x, y)
[PROOF STEP]
by (subst x, subst y) (auto simp: sgn_if)
[PROOF STATE]
proof (state)
this:
solution (x', y') = solution (x, y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nontriv_solution_of_nat_of_nat [simp]:
  "nontriv_solution (of_nat a, of_nat b :: 'a :: {comm_ring_1, ring_char_0}) \<longleftrightarrow> nontriv_solution (a, b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nontriv_solution (of_nat a, of_nat b) = nontriv_solution (a, b)
[PROOF STEP]
by (auto simp: nontriv_solution_altdef)


[STATEMENT]
lemma nontriv_solution_of_nat_of_nat' [simp]:
  "nontriv_solution (case z of (a, b) \<Rightarrow> (of_nat a, of_nat b :: 'a :: {comm_ring_1, ring_char_0})) \<longleftrightarrow>
     nontriv_solution z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nontriv_solution (case z of (a, b) \<Rightarrow> (of_nat a, of_nat b)) = nontriv_solution z
[PROOF STEP]
by (auto simp: case_prod_unfold)


[STATEMENT]
lemma nontriv_solution_imp_solution [dest]: "nontriv_solution z \<Longrightarrow> solution z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nontriv_solution z \<Longrightarrow> solution z
[PROOF STEP]
by (auto simp: nontriv_solution_altdef)


[STATEMENT]
lemma pell_valuation_uminus_uminus [simp]: "pell_valuation (-x, -y) = -pell_valuation (x, y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pell_valuation (- x, - y) = - pell_valuation (x, y)
[PROOF STEP]
by (simp add: pell_valuation_def)


[STATEMENT]
lemma pell_valuation_eq_iff [simp]:
  "pell_valuation z1 = pell_valuation z2 \<longleftrightarrow> z1 = z2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pell_valuation z1 = pell_valuation z2) = (z1 = z2)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pell_valuation z1 = pell_valuation z2 \<Longrightarrow> z1 = z2
 2. z1 = z2 \<Longrightarrow> pell_valuation z1 = pell_valuation z2
[PROOF STEP]
assume *: "pell_valuation z1 = pell_valuation z2"
[PROOF STATE]
proof (state)
this:
pell_valuation z1 = pell_valuation z2

goal (2 subgoals):
 1. pell_valuation z1 = pell_valuation z2 \<Longrightarrow> z1 = z2
 2. z1 = z2 \<Longrightarrow> pell_valuation z1 = pell_valuation z2
[PROOF STEP]
obtain a b where [simp]: "z1 = (a, b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. z1 = (a, b) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases z1)
[PROOF STATE]
proof (state)
this:
z1 = (a, b)

goal (2 subgoals):
 1. pell_valuation z1 = pell_valuation z2 \<Longrightarrow> z1 = z2
 2. z1 = z2 \<Longrightarrow> pell_valuation z1 = pell_valuation z2
[PROOF STEP]
obtain u v where [simp]: "z2 = (u, v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u v. z2 = (u, v) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases z2)
[PROOF STATE]
proof (state)
this:
z2 = (u, v)

goal (2 subgoals):
 1. pell_valuation z1 = pell_valuation z2 \<Longrightarrow> z1 = z2
 2. z1 = z2 \<Longrightarrow> pell_valuation z1 = pell_valuation z2
[PROOF STEP]
have "b = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b = v
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> v \<Longrightarrow> False
[PROOF STEP]
assume "b \<noteq> v"
[PROOF STATE]
proof (state)
this:
b \<noteq> v

goal (1 subgoal):
 1. b \<noteq> v \<Longrightarrow> False
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
pell_valuation z1 = pell_valuation z2
b \<noteq> v
[PROOF STEP]
have "sqrt D = (u - a) / (b - v)"
[PROOF STATE]
proof (prove)
using this:
pell_valuation z1 = pell_valuation z2
b \<noteq> v

goal (1 subgoal):
 1. sqrt (real D) = real_of_int (u - a) / real_of_int (b - v)
[PROOF STEP]
by (simp add: field_simps pell_valuation_def)
[PROOF STATE]
proof (state)
this:
sqrt (real D) = real_of_int (u - a) / real_of_int (b - v)

goal (1 subgoal):
 1. b \<noteq> v \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sqrt (real D) = real_of_int (u - a) / real_of_int (b - v)

goal (1 subgoal):
 1. b \<noteq> v \<Longrightarrow> False
[PROOF STEP]
have "\<dots> \<in> \<rat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (u - a) / real_of_int (b - v) \<in> \<rat>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int (u - a) / real_of_int (b - v) \<in> \<rat>

goal (1 subgoal):
 1. b \<noteq> v \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sqrt (real D) \<in> \<rat>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
sqrt (real D) \<in> \<rat>

goal (1 subgoal):
 1. False
[PROOF STEP]
using irrat_sqrt_nonsquare nonsquare_D
[PROOF STATE]
proof (prove)
using this:
sqrt (real D) \<in> \<rat>
\<not> is_square ?n \<Longrightarrow> sqrt (real ?n) \<notin> \<rat>
\<not> is_square D

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

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

goal (2 subgoals):
 1. pell_valuation z1 = pell_valuation z2 \<Longrightarrow> z1 = z2
 2. z1 = z2 \<Longrightarrow> pell_valuation z1 = pell_valuation z2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b = v

goal (2 subgoals):
 1. pell_valuation z1 = pell_valuation z2 \<Longrightarrow> z1 = z2
 2. z1 = z2 \<Longrightarrow> pell_valuation z1 = pell_valuation z2
[PROOF STEP]
from this and *
[PROOF STATE]
proof (chain)
picking this:
b = v
pell_valuation z1 = pell_valuation z2
[PROOF STEP]
have "a = u"
[PROOF STATE]
proof (prove)
using this:
b = v
pell_valuation z1 = pell_valuation z2

goal (1 subgoal):
 1. a = u
[PROOF STEP]
by (simp add: pell_valuation_def)
[PROOF STATE]
proof (state)
this:
a = u

goal (2 subgoals):
 1. pell_valuation z1 = pell_valuation z2 \<Longrightarrow> z1 = z2
 2. z1 = z2 \<Longrightarrow> pell_valuation z1 = pell_valuation z2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b = v
a = u
[PROOF STEP]
show "z1 = z2"
[PROOF STATE]
proof (prove)
using this:
b = v
a = u

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

goal (1 subgoal):
 1. z1 = z2 \<Longrightarrow> pell_valuation z1 = pell_valuation z2
[PROOF STEP]
qed auto


[STATEMENT]
lemma solutions_linorder:
  fixes a b x y :: nat
  assumes "solution (a, b)" "solution (x, y)"
  shows   "a \<le> x \<and> b \<le> y \<or> a \<ge> x \<and> b \<ge> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> x \<and> b \<le> y \<or> x \<le> a \<and> y \<le> b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<le> x \<and> b \<le> y \<or> x \<le> a \<and> y \<le> b
[PROOF STEP]
have "b \<le> y" if "a \<le> x" "solution (a, b)" "solution (x, y)" for a b x y :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<le> y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<le> y
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
a \<le> x
solution (a, b)
solution (x, y)
[PROOF STEP]
have "a ^ 2 \<le> x ^ 2"
[PROOF STATE]
proof (prove)
using this:
a \<le> x
solution (a, b)
solution (x, y)

goal (1 subgoal):
 1. a\<^sup>2 \<le> x\<^sup>2
[PROOF STEP]
by (intro power_mono) auto
[PROOF STATE]
proof (state)
this:
a\<^sup>2 \<le> x\<^sup>2

goal (1 subgoal):
 1. b \<le> y
[PROOF STEP]
with that and D_gt_1
[PROOF STATE]
proof (chain)
picking this:
a \<le> x
solution (a, b)
solution (x, y)
1 < D
a\<^sup>2 \<le> x\<^sup>2
[PROOF STEP]
have "b\<^sup>2 \<le> y\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
a \<le> x
solution (a, b)
solution (x, y)
1 < D
a\<^sup>2 \<le> x\<^sup>2

goal (1 subgoal):
 1. b\<^sup>2 \<le> y\<^sup>2
[PROOF STEP]
by (simp add: solution_def)
[PROOF STATE]
proof (state)
this:
b\<^sup>2 \<le> y\<^sup>2

goal (1 subgoal):
 1. b \<le> y
[PROOF STEP]
thus "b \<le> y"
[PROOF STATE]
proof (prove)
using this:
b\<^sup>2 \<le> y\<^sup>2

goal (1 subgoal):
 1. b \<le> y
[PROOF STEP]
by (simp add: power2_nat_le_eq_le)
[PROOF STATE]
proof (state)
this:
b \<le> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a2 \<le> ?x2; solution (?a2, ?b2); solution (?x2, ?y2)\<rbrakk> \<Longrightarrow> ?b2 \<le> ?y2

goal (1 subgoal):
 1. a \<le> x \<and> b \<le> y \<or> x \<le> a \<and> y \<le> b
[PROOF STEP]
from this[of a x b y] and this[of x a y b] and assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a \<le> x; solution (a, b); solution (x, y)\<rbrakk> \<Longrightarrow> b \<le> y
\<lbrakk>x \<le> a; solution (x, y); solution (a, b)\<rbrakk> \<Longrightarrow> y \<le> b
solution (a, b)
solution (x, y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<le> x; solution (a, b); solution (x, y)\<rbrakk> \<Longrightarrow> b \<le> y
\<lbrakk>x \<le> a; solution (x, y); solution (a, b)\<rbrakk> \<Longrightarrow> y \<le> b
solution (a, b)
solution (x, y)

goal (1 subgoal):
 1. a \<le> x \<and> b \<le> y \<or> x \<le> a \<and> y \<le> b
[PROOF STEP]
by (cases "a \<le> x") auto
[PROOF STATE]
proof (state)
this:
a \<le> x \<and> b \<le> y \<or> x \<le> a \<and> y \<le> b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma solutions_linorder_strict:
  fixes a b x y :: nat
  assumes "solution (a, b)" "solution (x, y)"
  shows   "(a, b) = (x, y) \<or> a < x \<and> b < y \<or> a > x \<and> b > y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) = (x, y) \<or> a < x \<and> b < y \<or> x < a \<and> y < b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a, b) = (x, y) \<or> a < x \<and> b < y \<or> x < a \<and> y < b
[PROOF STEP]
have "b = y" if "a = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b = y
[PROOF STEP]
using that assms and D_gt_1
[PROOF STATE]
proof (prove)
using this:
a = x
solution (a, b)
solution (x, y)
1 < D

goal (1 subgoal):
 1. b = y
[PROOF STEP]
by (simp add: solution_def)
[PROOF STATE]
proof (state)
this:
a = x \<Longrightarrow> b = y

goal (1 subgoal):
 1. (a, b) = (x, y) \<or> a < x \<and> b < y \<or> x < a \<and> y < b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a = x \<Longrightarrow> b = y

goal (1 subgoal):
 1. (a, b) = (x, y) \<or> a < x \<and> b < y \<or> x < a \<and> y < b
[PROOF STEP]
have "a = x" if "b = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = x
[PROOF STEP]
from that and assms
[PROOF STATE]
proof (chain)
picking this:
b = y
solution (a, b)
solution (x, y)
[PROOF STEP]
have "a\<^sup>2 = Suc (D * y\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
b = y
solution (a, b)
solution (x, y)

goal (1 subgoal):
 1. a\<^sup>2 = Suc (D * y\<^sup>2)
[PROOF STEP]
by (simp add: solution_def)
[PROOF STATE]
proof (state)
this:
a\<^sup>2 = Suc (D * y\<^sup>2)

goal (1 subgoal):
 1. a = x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a\<^sup>2 = Suc (D * y\<^sup>2)

goal (1 subgoal):
 1. a = x
[PROOF STEP]
from that and assms
[PROOF STATE]
proof (chain)
picking this:
b = y
solution (a, b)
solution (x, y)
[PROOF STEP]
have "\<dots> = x\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
b = y
solution (a, b)
solution (x, y)

goal (1 subgoal):
 1. Suc (D * y\<^sup>2) = x\<^sup>2
[PROOF STEP]
by (simp add: solution_def)
[PROOF STATE]
proof (state)
this:
Suc (D * y\<^sup>2) = x\<^sup>2

goal (1 subgoal):
 1. a = x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a\<^sup>2 = x\<^sup>2
[PROOF STEP]
show "a = x"
[PROOF STATE]
proof (prove)
using this:
a\<^sup>2 = x\<^sup>2

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
b = y \<Longrightarrow> a = x

goal (1 subgoal):
 1. (a, b) = (x, y) \<or> a < x \<and> b < y \<or> x < a \<and> y < b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a = x \<Longrightarrow> b = y
b = y \<Longrightarrow> a = x
[PROOF STEP]
have [simp]: "a = x \<longleftrightarrow> b = y"
[PROOF STATE]
proof (prove)
using this:
a = x \<Longrightarrow> b = y
b = y \<Longrightarrow> a = x

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

goal (1 subgoal):
 1. (a, b) = (x, y) \<or> a < x \<and> b < y \<or> x < a \<and> y < b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) = (x, y) \<or> a < x \<and> b < y \<or> x < a \<and> y < b
[PROOF STEP]
using solutions_linorder[OF assms]
[PROOF STATE]
proof (prove)
using this:
a \<le> x \<and> b \<le> y \<or> x \<le> a \<and> y \<le> b

goal (1 subgoal):
 1. (a, b) = (x, y) \<or> a < x \<and> b < y \<or> x < a \<and> y < b
[PROOF STEP]
by (cases a x rule: linorder_cases; cases b y rule: linorder_cases) simp_all
[PROOF STATE]
proof (state)
this:
(a, b) = (x, y) \<or> a < x \<and> b < y \<or> x < a \<and> y < b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma solutions_le_iff_pell_valuation_le:
  fixes a b x y :: nat
  assumes "solution (a, b)" "solution (x, y)"
  shows   "a \<le> x \<and> b \<le> y \<longleftrightarrow> pell_valuation (a, b) \<le> pell_valuation (x, y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le> x \<and> b \<le> y) = (pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<le> x \<and> b \<le> y \<Longrightarrow> pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y))
 2. pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) \<Longrightarrow> a \<le> x \<and> b \<le> y
[PROOF STEP]
assume "a \<le> x \<and> b \<le> y"
[PROOF STATE]
proof (state)
this:
a \<le> x \<and> b \<le> y

goal (2 subgoals):
 1. a \<le> x \<and> b \<le> y \<Longrightarrow> pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y))
 2. pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) \<Longrightarrow> a \<le> x \<and> b \<le> y
[PROOF STEP]
thus "pell_valuation (a, b) \<le> pell_valuation (x, y)"
[PROOF STATE]
proof (prove)
using this:
a \<le> x \<and> b \<le> y

goal (1 subgoal):
 1. pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
unfolding pell_valuation_def prod.case
[PROOF STATE]
proof (prove)
using this:
a \<le> x \<and> b \<le> y

goal (1 subgoal):
 1. real_of_int (int a) + real_of_int (int b) * sqrt (real D) \<le> real_of_int (int x) + real_of_int (int y) * sqrt (real D)
[PROOF STEP]
using D_gt_1
[PROOF STATE]
proof (prove)
using this:
a \<le> x \<and> b \<le> y
1 < D

goal (1 subgoal):
 1. real_of_int (int a) + real_of_int (int b) * sqrt (real D) \<le> real_of_int (int x) + real_of_int (int y) * sqrt (real D)
[PROOF STEP]
by (intro add_mono mult_right_mono) auto
[PROOF STATE]
proof (state)
this:
pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) \<Longrightarrow> a \<le> x \<and> b \<le> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) \<Longrightarrow> a \<le> x \<and> b \<le> y
[PROOF STEP]
assume *: "pell_valuation (a, b) \<le> pell_valuation (x, y)"
[PROOF STATE]
proof (state)
this:
pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) \<Longrightarrow> a \<le> x \<and> b \<le> y
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
solution (a, b)
solution (x, y)
[PROOF STEP]
have "a \<le> x \<and> b \<le> y \<or> x \<le> a \<and> y \<le> b"
[PROOF STATE]
proof (prove)
using this:
solution (a, b)
solution (x, y)

goal (1 subgoal):
 1. a \<le> x \<and> b \<le> y \<or> x \<le> a \<and> y \<le> b
[PROOF STEP]
by (rule solutions_linorder)
[PROOF STATE]
proof (state)
this:
a \<le> x \<and> b \<le> y \<or> x \<le> a \<and> y \<le> b

goal (1 subgoal):
 1. pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) \<Longrightarrow> a \<le> x \<and> b \<le> y
[PROOF STEP]
thus "a \<le> x \<and> b \<le> y"
[PROOF STATE]
proof (prove)
using this:
a \<le> x \<and> b \<le> y \<or> x \<le> a \<and> y \<le> b

goal (1 subgoal):
 1. a \<le> x \<and> b \<le> y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<le> x \<and> b \<le> y \<Longrightarrow> a \<le> x \<and> b \<le> y
 2. x \<le> a \<and> y \<le> b \<Longrightarrow> a \<le> x \<and> b \<le> y
[PROOF STEP]
assume "x \<le> a \<and> y \<le> b"
[PROOF STATE]
proof (state)
this:
x \<le> a \<and> y \<le> b

goal (2 subgoals):
 1. a \<le> x \<and> b \<le> y \<Longrightarrow> a \<le> x \<and> b \<le> y
 2. x \<le> a \<and> y \<le> b \<Longrightarrow> a \<le> x \<and> b \<le> y
[PROOF STEP]
hence "pell_valuation (a, b) \<ge> pell_valuation (x, y)"
[PROOF STATE]
proof (prove)
using this:
x \<le> a \<and> y \<le> b

goal (1 subgoal):
 1. pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
unfolding pell_valuation_def prod.case
[PROOF STATE]
proof (prove)
using this:
x \<le> a \<and> y \<le> b

goal (1 subgoal):
 1. real_of_int (int x) + real_of_int (int y) * sqrt (real D) \<le> real_of_int (int a) + real_of_int (int b) * sqrt (real D)
[PROOF STEP]
using D_gt_1
[PROOF STATE]
proof (prove)
using this:
x \<le> a \<and> y \<le> b
1 < D

goal (1 subgoal):
 1. real_of_int (int x) + real_of_int (int y) * sqrt (real D) \<le> real_of_int (int a) + real_of_int (int b) * sqrt (real D)
[PROOF STEP]
by (intro add_mono mult_right_mono) auto
[PROOF STATE]
proof (state)
this:
pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y))

goal (2 subgoals):
 1. a \<le> x \<and> b \<le> y \<Longrightarrow> a \<le> x \<and> b \<le> y
 2. x \<le> a \<and> y \<le> b \<Longrightarrow> a \<le> x \<and> b \<le> y
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y))
pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
have "pell_valuation (a, b) = pell_valuation (x, y)"
[PROOF STATE]
proof (prove)
using this:
pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y))
pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y))

goal (2 subgoals):
 1. a \<le> x \<and> b \<le> y \<Longrightarrow> a \<le> x \<and> b \<le> y
 2. x \<le> a \<and> y \<le> b \<Longrightarrow> a \<le> x \<and> b \<le> y
[PROOF STEP]
hence "(a, b) = (x, y)"
[PROOF STATE]
proof (prove)
using this:
pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. (a, b) = (x, y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(a, b) = (x, y)

goal (2 subgoals):
 1. a \<le> x \<and> b \<le> y \<Longrightarrow> a \<le> x \<and> b \<le> y
 2. x \<le> a \<and> y \<le> b \<Longrightarrow> a \<le> x \<and> b \<le> y
[PROOF STEP]
thus "a \<le> x \<and> b \<le> y"
[PROOF STATE]
proof (prove)
using this:
(a, b) = (x, y)

goal (1 subgoal):
 1. a \<le> x \<and> b \<le> y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<le> x \<and> b \<le> y

goal (1 subgoal):
 1. a \<le> x \<and> b \<le> y \<Longrightarrow> a \<le> x \<and> b \<le> y
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
a \<le> x \<and> b \<le> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma solutions_less_iff_pell_valuation_less:
  fixes a b x y :: nat
  assumes "solution (a, b)" "solution (x, y)"
  shows   "a < x \<and> b < y \<longleftrightarrow> pell_valuation (a, b) < pell_valuation (x, y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a < x \<and> b < y) = (pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a < x \<and> b < y \<Longrightarrow> pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y))
 2. pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) \<Longrightarrow> a < x \<and> b < y
[PROOF STEP]
assume "a < x \<and> b < y"
[PROOF STATE]
proof (state)
this:
a < x \<and> b < y

goal (2 subgoals):
 1. a < x \<and> b < y \<Longrightarrow> pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y))
 2. pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) \<Longrightarrow> a < x \<and> b < y
[PROOF STEP]
thus "pell_valuation (a, b) < pell_valuation (x, y)"
[PROOF STATE]
proof (prove)
using this:
a < x \<and> b < y

goal (1 subgoal):
 1. pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
unfolding pell_valuation_def prod.case
[PROOF STATE]
proof (prove)
using this:
a < x \<and> b < y

goal (1 subgoal):
 1. real_of_int (int a) + real_of_int (int b) * sqrt (real D) < real_of_int (int x) + real_of_int (int y) * sqrt (real D)
[PROOF STEP]
using D_gt_1
[PROOF STATE]
proof (prove)
using this:
a < x \<and> b < y
1 < D

goal (1 subgoal):
 1. real_of_int (int a) + real_of_int (int b) * sqrt (real D) < real_of_int (int x) + real_of_int (int y) * sqrt (real D)
[PROOF STEP]
by (intro add_strict_mono mult_strict_right_mono) auto
[PROOF STATE]
proof (state)
this:
pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) \<Longrightarrow> a < x \<and> b < y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) \<Longrightarrow> a < x \<and> b < y
[PROOF STEP]
assume *: "pell_valuation (a, b) < pell_valuation (x, y)"
[PROOF STATE]
proof (state)
this:
pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) \<Longrightarrow> a < x \<and> b < y
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
solution (a, b)
solution (x, y)
[PROOF STEP]
have "(a, b) = (x, y) \<or> a < x \<and> b < y \<or> x < a \<and> y < b"
[PROOF STATE]
proof (prove)
using this:
solution (a, b)
solution (x, y)

goal (1 subgoal):
 1. (a, b) = (x, y) \<or> a < x \<and> b < y \<or> x < a \<and> y < b
[PROOF STEP]
by (rule solutions_linorder_strict)
[PROOF STATE]
proof (state)
this:
(a, b) = (x, y) \<or> a < x \<and> b < y \<or> x < a \<and> y < b

goal (1 subgoal):
 1. pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) \<Longrightarrow> a < x \<and> b < y
[PROOF STEP]
thus "a < x \<and> b < y"
[PROOF STATE]
proof (prove)
using this:
(a, b) = (x, y) \<or> a < x \<and> b < y \<or> x < a \<and> y < b

goal (1 subgoal):
 1. a < x \<and> b < y
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (a, b) = (x, y) \<Longrightarrow> a < x \<and> b < y
 2. a < x \<and> b < y \<Longrightarrow> a < x \<and> b < y
 3. x < a \<and> y < b \<Longrightarrow> a < x \<and> b < y
[PROOF STEP]
assume "x < a \<and> y < b"
[PROOF STATE]
proof (state)
this:
x < a \<and> y < b

goal (3 subgoals):
 1. (a, b) = (x, y) \<Longrightarrow> a < x \<and> b < y
 2. a < x \<and> b < y \<Longrightarrow> a < x \<and> b < y
 3. x < a \<and> y < b \<Longrightarrow> a < x \<and> b < y
[PROOF STEP]
hence "pell_valuation (a, b) > pell_valuation (x, y)"
[PROOF STATE]
proof (prove)
using this:
x < a \<and> y < b

goal (1 subgoal):
 1. pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
unfolding pell_valuation_def prod.case
[PROOF STATE]
proof (prove)
using this:
x < a \<and> y < b

goal (1 subgoal):
 1. real_of_int (int x) + real_of_int (int y) * sqrt (real D) < real_of_int (int a) + real_of_int (int b) * sqrt (real D)
[PROOF STEP]
using D_gt_1
[PROOF STATE]
proof (prove)
using this:
x < a \<and> y < b
1 < D

goal (1 subgoal):
 1. real_of_int (int x) + real_of_int (int y) * sqrt (real D) < real_of_int (int a) + real_of_int (int b) * sqrt (real D)
[PROOF STEP]
by (intro add_strict_mono mult_strict_right_mono) auto
[PROOF STATE]
proof (state)
this:
pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y))

goal (3 subgoals):
 1. (a, b) = (x, y) \<Longrightarrow> a < x \<and> b < y
 2. a < x \<and> b < y \<Longrightarrow> a < x \<and> b < y
 3. x < a \<and> y < b \<Longrightarrow> a < x \<and> b < y
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y))
pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y))
pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) < pell_valuation (case (a, b) of (x, y) \<Rightarrow> (int x, int y))

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

goal (3 subgoals):
 1. (a, b) = (x, y) \<Longrightarrow> a < x \<and> b < y
 2. a < x \<and> b < y \<Longrightarrow> a < x \<and> b < y
 3. x < a \<and> y < b \<Longrightarrow> a < x \<and> b < y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. a < x \<and> b < y
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
a < x \<and> b < y

goal (2 subgoals):
 1. (a, b) = (x, y) \<Longrightarrow> a < x \<and> b < y
 2. a < x \<and> b < y \<Longrightarrow> a < x \<and> b < y
[PROOF STEP]
qed (insert *, auto)
[PROOF STATE]
proof (state)
this:
a < x \<and> b < y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem fund_sol_is_arg_min:
  "is_arg_min (pell_valuation :: nat \<times> nat \<Rightarrow> real) nontriv_solution fund_sol"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution fund_sol
[PROOF STEP]
unfolding fund_sol_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution (The (is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution))
[PROOF STEP]
proof (rule theI')
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!x. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution x
[PROOF STEP]
show "\<exists>!z::nat\<times>nat. is_arg_min (pell_valuation :: nat \<times> nat \<Rightarrow> real) nontriv_solution z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!z. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z
[PROOF STEP]
proof (rule ex_ex1I)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>z. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z
 2. \<And>z y. \<lbrakk>is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z; is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution y\<rbrakk> \<Longrightarrow> z = y
[PROOF STEP]
fix z1 z2 :: "nat \<times> nat"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>z. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z
 2. \<And>z y. \<lbrakk>is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z; is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution y\<rbrakk> \<Longrightarrow> z = y
[PROOF STEP]
assume "is_arg_min (pell_valuation :: nat \<times> nat \<Rightarrow> real) nontriv_solution z1"
           "is_arg_min (pell_valuation :: nat \<times> nat \<Rightarrow> real) nontriv_solution z2"
[PROOF STATE]
proof (state)
this:
is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z1
is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z2

goal (2 subgoals):
 1. \<exists>z. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z
 2. \<And>z y. \<lbrakk>is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z; is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution y\<rbrakk> \<Longrightarrow> z = y
[PROOF STEP]
hence "pell_valuation z1 = pell_valuation z2"
[PROOF STATE]
proof (prove)
using this:
is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z1
is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z2

goal (1 subgoal):
 1. pell_valuation (case z1 of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case z2 of (x, y) \<Rightarrow> (int x, int y))
[PROOF STEP]
by (cases z1, cases z2, intro antisym) (auto simp: is_arg_min_def not_less)
[PROOF STATE]
proof (state)
this:
pell_valuation (case z1 of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case z2 of (x, y) \<Rightarrow> (int x, int y))

goal (2 subgoals):
 1. \<exists>z. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z
 2. \<And>z y. \<lbrakk>is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z; is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution y\<rbrakk> \<Longrightarrow> z = y
[PROOF STEP]
thus "z1 = z2"
[PROOF STATE]
proof (prove)
using this:
pell_valuation (case z1 of (x, y) \<Rightarrow> (int x, int y)) = pell_valuation (case z2 of (x, y) \<Rightarrow> (int x, int y))

goal (1 subgoal):
 1. z1 = z2
[PROOF STEP]
by (auto split: prod.splits)
[PROOF STATE]
proof (state)
this:
z1 = z2

goal (1 subgoal):
 1. \<exists>z. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>z. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z
[PROOF STEP]
define y where "y = (LEAST y. y > 0 \<and> is_square (1 + D * y\<^sup>2))"
[PROOF STATE]
proof (state)
this:
y = (LEAST y. 0 < y \<and> is_square (1 + D * y\<^sup>2))

goal (1 subgoal):
 1. \<exists>z. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z
[PROOF STEP]
have "\<exists>y>0. is_square (1 + D * y\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y>0. is_square (1 + D * y\<^sup>2)
[PROOF STEP]
using pell_solution_exists
[PROOF STATE]
proof (prove)
using this:
\<exists>x y. y \<noteq> 0 \<and> x\<^sup>2 = 1 + D * y\<^sup>2

goal (1 subgoal):
 1. \<exists>y>0. is_square (1 + D * y\<^sup>2)
[PROOF STEP]
by (auto simp: eq_commute[of _ "Suc _"])
[PROOF STATE]
proof (state)
this:
\<exists>y>0. is_square (1 + D * y\<^sup>2)

goal (1 subgoal):
 1. \<exists>z. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z
[PROOF STEP]
hence y: "y > 0 \<and> is_square (1 + D * y\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
\<exists>y>0. is_square (1 + D * y\<^sup>2)

goal (1 subgoal):
 1. 0 < y \<and> is_square (1 + D * y\<^sup>2)
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
using this:
\<exists>y>0. is_square (1 + D * y\<^sup>2)

goal (1 subgoal):
 1. 0 < (LEAST y. 0 < y \<and> is_square (1 + D * y\<^sup>2)) \<and> is_square (1 + D * (LEAST y. 0 < y \<and> is_square (1 + D * y\<^sup>2))\<^sup>2)
[PROOF STEP]
by (rule LeastI_ex)
[PROOF STATE]
proof (state)
this:
0 < y \<and> is_square (1 + D * y\<^sup>2)

goal (1 subgoal):
 1. \<exists>z. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z
[PROOF STEP]
have y_le: "y \<le> y'" if "y' > 0" "is_square (1 + D * y'\<^sup>2)" for y'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> y'
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST y. 0 < y \<and> is_square (1 + D * y\<^sup>2)) \<le> y'
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
0 < y'
is_square (1 + D * y'\<^sup>2)

goal (1 subgoal):
 1. (LEAST y. 0 < y \<and> is_square (1 + D * y\<^sup>2)) \<le> y'
[PROOF STEP]
by (intro Least_le) auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < ?y'2; is_square (1 + D * ?y'2\<^sup>2)\<rbrakk> \<Longrightarrow> y \<le> ?y'2

goal (1 subgoal):
 1. \<exists>z. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z
[PROOF STEP]
from y
[PROOF STATE]
proof (chain)
picking this:
0 < y \<and> is_square (1 + D * y\<^sup>2)
[PROOF STEP]
obtain x where x: "x\<^sup>2 = 1 + D * y\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
0 < y \<and> is_square (1 + D * y\<^sup>2)

goal (1 subgoal):
 1. (\<And>x. x\<^sup>2 = 1 + D * y\<^sup>2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: is_nth_powerE)
[PROOF STATE]
proof (state)
this:
x\<^sup>2 = 1 + D * y\<^sup>2

goal (1 subgoal):
 1. \<exists>z. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z
[PROOF STEP]
with y
[PROOF STATE]
proof (chain)
picking this:
0 < y \<and> is_square (1 + D * y\<^sup>2)
x\<^sup>2 = 1 + D * y\<^sup>2
[PROOF STEP]
have "nontriv_solution (x, y)"
[PROOF STATE]
proof (prove)
using this:
0 < y \<and> is_square (1 + D * y\<^sup>2)
x\<^sup>2 = 1 + D * y\<^sup>2

goal (1 subgoal):
 1. nontriv_solution (x, y)
[PROOF STEP]
by (auto simp: nontriv_solution_def)
[PROOF STATE]
proof (state)
this:
nontriv_solution (x, y)

goal (1 subgoal):
 1. \<exists>z. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z
[PROOF STEP]
have "is_arg_min (pell_valuation :: nat \<times> nat \<Rightarrow> real) nontriv_solution (x, y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution (x, y)
[PROOF STEP]
unfolding is_arg_min_linorder
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nontriv_solution (x, y) \<and> (\<forall>ya. nontriv_solution ya \<longrightarrow> pell_valuation (case (x, y) of (x, y) \<Rightarrow> (int x, int y)) \<le> pell_valuation (case ya of (x, y) \<Rightarrow> (int x, int y)))
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. nontriv_solution (x, y)
 2. \<And>a b. nontriv_solution (a, b) \<Longrightarrow> pell_valuation (int x, int y) \<le> pell_valuation (int a, int b)
[PROOF STEP]
fix a b :: nat
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. nontriv_solution (x, y)
 2. \<And>a b. nontriv_solution (a, b) \<Longrightarrow> pell_valuation (int x, int y) \<le> pell_valuation (int a, int b)
[PROOF STEP]
assume *: "nontriv_solution (a, b)"
[PROOF STATE]
proof (state)
this:
nontriv_solution (a, b)

goal (2 subgoals):
 1. nontriv_solution (x, y)
 2. \<And>a b. nontriv_solution (a, b) \<Longrightarrow> pell_valuation (int x, int y) \<le> pell_valuation (int a, int b)
[PROOF STEP]
hence "b > 0" and "Suc (D * b\<^sup>2) = a\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
nontriv_solution (a, b)

goal (1 subgoal):
 1. 0 < b &&& Suc (D * b\<^sup>2) = a\<^sup>2
[PROOF STEP]
by (auto simp: nontriv_solution_def intro!: Nat.gr0I)
[PROOF STATE]
proof (state)
this:
0 < b
Suc (D * b\<^sup>2) = a\<^sup>2

goal (2 subgoals):
 1. nontriv_solution (x, y)
 2. \<And>a b. nontriv_solution (a, b) \<Longrightarrow> pell_valuation (int x, int y) \<le> pell_valuation (int a, int b)
[PROOF STEP]
hence "is_square (1 + D * b\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
0 < b
Suc (D * b\<^sup>2) = a\<^sup>2

goal (1 subgoal):
 1. is_square (1 + D * b\<^sup>2)
[PROOF STEP]
by (auto simp: nontriv_solution_def)
[PROOF STATE]
proof (state)
this:
is_square (1 + D * b\<^sup>2)

goal (2 subgoals):
 1. nontriv_solution (x, y)
 2. \<And>a b. nontriv_solution (a, b) \<Longrightarrow> pell_valuation (int x, int y) \<le> pell_valuation (int a, int b)
[PROOF STEP]
from \<open>b > 0\<close> and this
[PROOF STATE]
proof (chain)
picking this:
0 < b
is_square (1 + D * b\<^sup>2)
[PROOF STEP]
have "y \<le> b"
[PROOF STATE]
proof (prove)
using this:
0 < b
is_square (1 + D * b\<^sup>2)

goal (1 subgoal):
 1. y \<le> b
[PROOF STEP]
by (rule y_le)
[PROOF STATE]
proof (state)
this:
y \<le> b

goal (2 subgoals):
 1. nontriv_solution (x, y)
 2. \<And>a b. nontriv_solution (a, b) \<Longrightarrow> pell_valuation (int x, int y) \<le> pell_valuation (int a, int b)
[PROOF STEP]
with \<open>nontriv_solution (x, y)\<close> and *
[PROOF STATE]
proof (chain)
picking this:
nontriv_solution (x, y)
nontriv_solution (a, b)
y \<le> b
[PROOF STEP]
have "x \<le> a"
[PROOF STATE]
proof (prove)
using this:
nontriv_solution (x, y)
nontriv_solution (a, b)
y \<le> b

goal (1 subgoal):
 1. x \<le> a
[PROOF STEP]
using solutions_linorder_strict[of x y a b]
[PROOF STATE]
proof (prove)
using this:
nontriv_solution (x, y)
nontriv_solution (a, b)
y \<le> b
\<lbrakk>solution (x, y); solution (a, b)\<rbrakk> \<Longrightarrow> (x, y) = (a, b) \<or> x < a \<and> y < b \<or> a < x \<and> b < y

goal (1 subgoal):
 1. x \<le> a
[PROOF STEP]
by (auto simp: nontriv_solution_altdef)
[PROOF STATE]
proof (state)
this:
x \<le> a

goal (2 subgoals):
 1. nontriv_solution (x, y)
 2. \<And>a b. nontriv_solution (a, b) \<Longrightarrow> pell_valuation (int x, int y) \<le> pell_valuation (int a, int b)
[PROOF STEP]
with \<open>y \<le> b\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<le> b
x \<le> a
[PROOF STEP]
show "pell_valuation (int x, int y) \<le> pell_valuation (int a, int b)"
[PROOF STATE]
proof (prove)
using this:
y \<le> b
x \<le> a

goal (1 subgoal):
 1. pell_valuation (int x, int y) \<le> pell_valuation (int a, int b)
[PROOF STEP]
unfolding pell_valuation_def prod.case
[PROOF STATE]
proof (prove)
using this:
y \<le> b
x \<le> a

goal (1 subgoal):
 1. real_of_int (int x) + real_of_int (int y) * sqrt (real D) \<le> real_of_int (int a) + real_of_int (int b) * sqrt (real D)
[PROOF STEP]
by (intro add_mono mult_right_mono) auto
[PROOF STATE]
proof (state)
this:
pell_valuation (int x, int y) \<le> pell_valuation (int a, int b)

goal (1 subgoal):
 1. nontriv_solution (x, y)
[PROOF STEP]
qed fact+
[PROOF STATE]
proof (state)
this:
is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution (x, y)

goal (1 subgoal):
 1. \<exists>z. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z
[PROOF STEP]
thus "\<exists>z. is_arg_min (pell_valuation :: nat \<times> nat \<Rightarrow> real) nontriv_solution z"
[PROOF STATE]
proof (prove)
using this:
is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution (x, y)

goal (1 subgoal):
 1. \<exists>z. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>z. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!z. is_arg_min (\<lambda>x. pell_valuation (case x of (x, y) \<Rightarrow> (int x, int y))) nontriv_solution z

goal:
No subgoals!
[PROOF STEP]
qed