[STATEMENT]
lemma assumes mon_conv: "x\<up>(y::real)"
  and less: "z < y"
  shows real_mon_conv_outgrow: "\<exists>n. \<forall>m. n \<le> m \<longrightarrow> z < x m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
from less
[PROOF STATE]
proof (chain)
picking this:
z < y
[PROOF STEP]
have less': "0 < y-z"
[PROOF STATE]
proof (prove)
using this:
z < y

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

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
have "\<exists>n.\<forall>m. n \<le> m \<longrightarrow> \<bar>x m - y\<bar> < y - z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z
[PROOF STEP]
from mon_conv
[PROOF STATE]
proof (chain)
picking this:
x\<up>y
[PROOF STEP]
have aux: "\<And>r. r > 0 \<Longrightarrow> \<exists>n. \<forall>m. n \<le> m \<longrightarrow> \<bar>x m - y\<bar> < r"
[PROOF STATE]
proof (prove)
using this:
x\<up>y

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < r
[PROOF STEP]
unfolding mon_conv_real_def lim_sequentially dist_real_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>n. x n \<le> x (Suc n)) \<and> (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. \<bar>x n - y\<bar> < r)

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < ?r \<Longrightarrow> \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < ?r

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z
[PROOF STEP]
with less'
[PROOF STATE]
proof (chain)
picking this:
0 < y - z
0 < ?r \<Longrightarrow> \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < ?r
[PROOF STEP]
show "\<exists>n. \<forall>m. n \<le> m \<longrightarrow> \<bar>x m - y\<bar> < y - z"
[PROOF STATE]
proof (prove)
using this:
0 < y - z
0 < ?r \<Longrightarrow> \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < ?r

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
from mon_conv
[PROOF STATE]
proof (chain)
picking this:
x\<up>y
[PROOF STEP]
have "x m \<le> y"
[PROOF STATE]
proof (prove)
using this:
x\<up>y

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

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
hence "\<bar>x m - y\<bar> = y - x m"
[PROOF STATE]
proof (prove)
using this:
x m \<le> y

goal (1 subgoal):
 1. \<bar>x m - y\<bar> = y - x m
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<bar>x m - y\<bar> = y - x m

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>x m - y\<bar> = y - x m

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
assume "\<bar>x m - y\<bar> < y - z"
[PROOF STATE]
proof (state)
this:
\<bar>x m - y\<bar> < y - z

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>x m - y\<bar> = y - x m
\<bar>x m - y\<bar> < y - z
[PROOF STEP]
have "z < x m"
[PROOF STATE]
proof (prove)
using this:
\<bar>x m - y\<bar> = y - x m
\<bar>x m - y\<bar> < y - z

goal (1 subgoal):
 1. z < x m
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
z < x m

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<bar>x ?m2 - y\<bar> < y - z \<Longrightarrow> z < x ?m2

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z
\<bar>x ?m2 - y\<bar> < y - z \<Longrightarrow> z < x ?m2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z
\<bar>x ?m2 - y\<bar> < y - z \<Longrightarrow> z < x ?m2

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. \<forall>m\<ge>n. z < x m

goal:
No subgoals!
[PROOF STEP]
qed