[STATEMENT]
lemma Rats_dense_in_real:
  fixes x :: real
  assumes "x < y"
  shows "\<exists>r\<in>\<rat>. x < r \<and> r < y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
from \<open>x < y\<close>
[PROOF STATE]
proof (chain)
picking this:
x < y
[PROOF STEP]
have "0 < y - x"
[PROOF STATE]
proof (prove)
using this:
x < y

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

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
with reals_Archimedean
[PROOF STATE]
proof (chain)
picking this:
(0::?'a) < ?x \<Longrightarrow> \<exists>n. inverse (of_nat (Suc n)) < ?x
0 < y - x
[PROOF STEP]
obtain q :: nat where q: "inverse (real q) < y - x" and "0 < q"
[PROOF STATE]
proof (prove)
using this:
(0::?'a) < ?x \<Longrightarrow> \<exists>n. inverse (of_nat (Suc n)) < ?x
0 < y - x

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>inverse (real q) < y - x; 0 < q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inverse (real q) < y - x
0 < q

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
define p where "p = \<lceil>y * real q\<rceil> - 1"
[PROOF STATE]
proof (state)
this:
p = \<lceil>y * real q\<rceil> - 1

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
define r where "r = of_int p / real q"
[PROOF STATE]
proof (state)
this:
r = real_of_int p / real q

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
from q
[PROOF STATE]
proof (chain)
picking this:
inverse (real q) < y - x
[PROOF STEP]
have "x < y - inverse (real q)"
[PROOF STATE]
proof (prove)
using this:
inverse (real q) < y - x

goal (1 subgoal):
 1. x < y - inverse (real q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x < y - inverse (real q)

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x < y - inverse (real q)

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
from \<open>0 < q\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < q
[PROOF STEP]
have "y - inverse (real q) \<le> r"
[PROOF STATE]
proof (prove)
using this:
0 < q

goal (1 subgoal):
 1. y - inverse (real q) \<le> r
[PROOF STEP]
by (simp add: r_def p_def le_divide_eq left_diff_distrib)
[PROOF STATE]
proof (state)
this:
y - inverse (real q) \<le> r

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x < r
[PROOF STEP]
have "x < r"
[PROOF STATE]
proof (prove)
using this:
x < r

goal (1 subgoal):
 1. x < r
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x < r

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x < r

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
from \<open>0 < q\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < q
[PROOF STEP]
have "r < y"
[PROOF STATE]
proof (prove)
using this:
0 < q

goal (1 subgoal):
 1. r < y
[PROOF STEP]
by (simp add: r_def p_def divide_less_eq diff_less_eq less_ceiling_iff [symmetric])
[PROOF STATE]
proof (state)
this:
r < y

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r < y

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
have "r \<in> \<rat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> \<rat>
[PROOF STEP]
by (simp add: r_def)
[PROOF STATE]
proof (state)
this:
r \<in> \<rat>

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x < r
r < y
r \<in> \<rat>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x < r
r < y
r \<in> \<rat>

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>\<rat>. x < r \<and> r < y

goal:
No subgoals!
[PROOF STEP]
qed