[STATEMENT]
lemma invariant_1_2_of_rat: assumes rc: "invariant_1_2 rai" 
  shows "real_of_1 rai \<noteq> of_rat x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_1 rai \<noteq> real_of_rat x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_1 rai \<noteq> real_of_rat x
[PROOF STEP]
obtain p l r where rai: "rai = (p, l, r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p l r. rai = (p, l, r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases rai, auto)
[PROOF STATE]
proof (state)
this:
rai = (p, l, r)

goal (1 subgoal):
 1. real_of_1 rai \<noteq> real_of_rat x
[PROOF STEP]
from rc[unfolded rai]
[PROOF STATE]
proof (chain)
picking this:
invariant_1_2 (p, l, r)
[PROOF STEP]
have "poly_cond2 p" "ipoly p (the_unique_root (p, l, r)) = 0"
[PROOF STATE]
proof (prove)
using this:
invariant_1_2 (p, l, r)

goal (1 subgoal):
 1. poly_cond2 p &&& poly (real_of_int_poly p) (real_of_1 (p, l, r)) = 0
[PROOF STEP]
by (auto elim!: invariant_1E)
[PROOF STATE]
proof (state)
this:
poly_cond2 p
poly (real_of_int_poly p) (real_of_1 (p, l, r)) = 0

goal (1 subgoal):
 1. real_of_1 rai \<noteq> real_of_rat x
[PROOF STEP]
from poly_cond2_no_rat_root[OF this(1), of x] this(2)
[PROOF STATE]
proof (chain)
picking this:
poly (real_of_int_poly p) (real_of_rat x) \<noteq> 0
poly (real_of_int_poly p) (real_of_1 (p, l, r)) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poly (real_of_int_poly p) (real_of_rat x) \<noteq> 0
poly (real_of_int_poly p) (real_of_1 (p, l, r)) = 0

goal (1 subgoal):
 1. real_of_1 rai \<noteq> real_of_rat x
[PROOF STEP]
unfolding rai
[PROOF STATE]
proof (prove)
using this:
poly (real_of_int_poly p) (real_of_rat x) \<noteq> 0
poly (real_of_int_poly p) (real_of_1 (p, l, r)) = 0

goal (1 subgoal):
 1. real_of_1 (p, l, r) \<noteq> real_of_rat x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_1 rai \<noteq> real_of_rat x

goal:
No subgoals!
[PROOF STEP]
qed