[STATEMENT]
lemma complex_quadratic_equation_monic_only_two_roots:
  fixes \<xi> :: complex
  assumes "\<xi>\<^sup>2 + b * \<xi> + c = 0"
  shows "\<xi> = (-b + ccsqrt(b\<^sup>2 - 4*c)) / 2 \<or> \<xi> = (-b - ccsqrt(b\<^sup>2 - 4*c)) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<xi>\<^sup>2 + b * \<xi> + c = 0

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<xi>\<^sup>2 + b * \<xi> + c = 0 \<Longrightarrow> \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<xi>\<^sup>2 + b * \<xi> + c = 0
[PROOF STEP]
have "(2 * (\<xi> + b/2))\<^sup>2 = b\<^sup>2 - 4*c"
[PROOF STATE]
proof (prove)
using this:
\<xi>\<^sup>2 + b * \<xi> + c = 0

goal (1 subgoal):
 1. (2 * (\<xi> + b / 2))\<^sup>2 = b\<^sup>2 - 4 * c
[PROOF STEP]
by (simp add: power2_eq_square field_simps)
       (metis (no_types, lifting) distrib_right_numeral mult.assoc mult_zero_left)
[PROOF STATE]
proof (state)
this:
(2 * (\<xi> + b / 2))\<^sup>2 = b\<^sup>2 - 4 * c

goal (1 subgoal):
 1. \<xi>\<^sup>2 + b * \<xi> + c = 0 \<Longrightarrow> \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2
[PROOF STEP]
hence "2 * (\<xi> + b/2) = ccsqrt (b\<^sup>2 - 4*c) \<or> 2 * (\<xi> + b/2) = - ccsqrt (b\<^sup>2 - 4*c)"
[PROOF STATE]
proof (prove)
using this:
(2 * (\<xi> + b / 2))\<^sup>2 = b\<^sup>2 - 4 * c

goal (1 subgoal):
 1. 2 * (\<xi> + b / 2) = ccsqrt (b\<^sup>2 - 4 * c) \<or> 2 * (\<xi> + b / 2) = - ccsqrt (b\<^sup>2 - 4 * c)
[PROOF STEP]
using ccsqrt[of "(2 * (\<xi> + b / 2))" "b\<^sup>2 - 4 * c"]
[PROOF STATE]
proof (prove)
using this:
(2 * (\<xi> + b / 2))\<^sup>2 = b\<^sup>2 - 4 * c
2 * (\<xi> + b / 2) * (2 * (\<xi> + b / 2)) = b\<^sup>2 - 4 * c \<Longrightarrow> 2 * (\<xi> + b / 2) = ccsqrt (b\<^sup>2 - 4 * c) \<or> 2 * (\<xi> + b / 2) = - ccsqrt (b\<^sup>2 - 4 * c)

goal (1 subgoal):
 1. 2 * (\<xi> + b / 2) = ccsqrt (b\<^sup>2 - 4 * c) \<or> 2 * (\<xi> + b / 2) = - ccsqrt (b\<^sup>2 - 4 * c)
[PROOF STEP]
by (simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
2 * (\<xi> + b / 2) = ccsqrt (b\<^sup>2 - 4 * c) \<or> 2 * (\<xi> + b / 2) = - ccsqrt (b\<^sup>2 - 4 * c)

goal (1 subgoal):
 1. \<xi>\<^sup>2 + b * \<xi> + c = 0 \<Longrightarrow> \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
2 * (\<xi> + b / 2) = ccsqrt (b\<^sup>2 - 4 * c) \<or> 2 * (\<xi> + b / 2) = - ccsqrt (b\<^sup>2 - 4 * c)

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2
[PROOF STEP]
using mult_cancel_right[of "b + \<xi> * 2" 2 "ccsqrt (b\<^sup>2 - 4*c)"]
[PROOF STATE]
proof (prove)
using this:
2 * (\<xi> + b / 2) = ccsqrt (b\<^sup>2 - 4 * c) \<or> 2 * (\<xi> + b / 2) = - ccsqrt (b\<^sup>2 - 4 * c)
((b + \<xi> * 2) * 2 = ccsqrt (b\<^sup>2 - 4 * c) * 2) = (2 = 0 \<or> b + \<xi> * 2 = ccsqrt (b\<^sup>2 - 4 * c))

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2
[PROOF STEP]
using mult_cancel_right[of "b + \<xi> * 2" 2 "-ccsqrt (b\<^sup>2 - 4*c)"]
[PROOF STATE]
proof (prove)
using this:
2 * (\<xi> + b / 2) = ccsqrt (b\<^sup>2 - 4 * c) \<or> 2 * (\<xi> + b / 2) = - ccsqrt (b\<^sup>2 - 4 * c)
((b + \<xi> * 2) * 2 = ccsqrt (b\<^sup>2 - 4 * c) * 2) = (2 = 0 \<or> b + \<xi> * 2 = ccsqrt (b\<^sup>2 - 4 * c))
((b + \<xi> * 2) * 2 = - ccsqrt (b\<^sup>2 - 4 * c) * 2) = (2 = 0 \<or> b + \<xi> * 2 = - ccsqrt (b\<^sup>2 - 4 * c))

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2
[PROOF STEP]
by (auto simp add: field_simps) (metis add_diff_cancel diff_minus_eq_add minus_diff_eq)
[PROOF STATE]
proof (state)
this:
\<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complex_quadratic_equation_monic_roots:
  fixes \<xi> :: complex
  assumes "\<xi> = (-b + ccsqrt(b\<^sup>2 - 4*c)) / 2 \<or>
           \<xi> = (-b - ccsqrt(b\<^sup>2 - 4*c)) / 2"
  shows  "\<xi>\<^sup>2 + b * \<xi> + c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<xi>\<^sup>2 + b * \<xi> + c = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2

goal (1 subgoal):
 1. \<xi>\<^sup>2 + b * \<xi> + c = 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<Longrightarrow> \<xi>\<^sup>2 + b * \<xi> + c = 0
 2. \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<Longrightarrow> \<xi>\<^sup>2 + b * \<xi> + c = 0
[PROOF STEP]
assume *: "\<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2"
[PROOF STATE]
proof (state)
this:
\<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2

goal (2 subgoals):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<Longrightarrow> \<xi>\<^sup>2 + b * \<xi> + c = 0
 2. \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<Longrightarrow> \<xi>\<^sup>2 + b * \<xi> + c = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<xi>\<^sup>2 + b * \<xi> + c = 0
[PROOF STEP]
by ((subst *)+) (subst power_divide, subst power2_sum, simp add: field_simps, simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
\<xi>\<^sup>2 + b * \<xi> + c = 0

goal (1 subgoal):
 1. \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<Longrightarrow> \<xi>\<^sup>2 + b * \<xi> + c = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<Longrightarrow> \<xi>\<^sup>2 + b * \<xi> + c = 0
[PROOF STEP]
assume *: "\<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2"
[PROOF STATE]
proof (state)
this:
\<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2

goal (1 subgoal):
 1. \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<Longrightarrow> \<xi>\<^sup>2 + b * \<xi> + c = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<xi>\<^sup>2 + b * \<xi> + c = 0
[PROOF STEP]
by ((subst *)+, subst power_divide, subst power2_diff, simp add: field_simps, simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
\<xi>\<^sup>2 + b * \<xi> + c = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complex_quadratic_equation_monic_distinct_roots:
  fixes b c :: complex
  assumes "b\<^sup>2 - 4*c \<noteq> 0"
  shows "\<exists> k\<^sub>1 k\<^sub>2. k\<^sub>1 \<noteq> k\<^sub>2 \<and> k\<^sub>1\<^sup>2 + b*k\<^sub>1 + c = 0 \<and> k\<^sub>2\<^sup>2 + b*k\<^sub>2 + c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k\<^sub>1 k\<^sub>2. k\<^sub>1 \<noteq> k\<^sub>2 \<and> k\<^sub>1\<^sup>2 + b * k\<^sub>1 + c = 0 \<and> k\<^sub>2\<^sup>2 + b * k\<^sub>2 + c = 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k\<^sub>1 k\<^sub>2. k\<^sub>1 \<noteq> k\<^sub>2 \<and> k\<^sub>1\<^sup>2 + b * k\<^sub>1 + c = 0 \<and> k\<^sub>2\<^sup>2 + b * k\<^sub>2 + c = 0
[PROOF STEP]
let ?\<xi>1 = "(-b + ccsqrt(b\<^sup>2 - 4*c)) / 2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k\<^sub>1 k\<^sub>2. k\<^sub>1 \<noteq> k\<^sub>2 \<and> k\<^sub>1\<^sup>2 + b * k\<^sub>1 + c = 0 \<and> k\<^sub>2\<^sup>2 + b * k\<^sub>2 + c = 0
[PROOF STEP]
let ?\<xi>2 = "(-b - ccsqrt(b\<^sup>2 - 4*c)) / 2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k\<^sub>1 k\<^sub>2. k\<^sub>1 \<noteq> k\<^sub>2 \<and> k\<^sub>1\<^sup>2 + b * k\<^sub>1 + c = 0 \<and> k\<^sub>2\<^sup>2 + b * k\<^sub>2 + c = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k\<^sub>1 k\<^sub>2. k\<^sub>1 \<noteq> k\<^sub>2 \<and> k\<^sub>1\<^sup>2 + b * k\<^sub>1 + c = 0 \<and> k\<^sub>2\<^sup>2 + b * k\<^sub>2 + c = 0
[PROOF STEP]
apply (rule_tac x="?\<xi>1" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k\<^sub>2. (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<noteq> k\<^sub>2 \<and> ((- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2)\<^sup>2 + b * ((- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2) + c = 0 \<and> k\<^sub>2\<^sup>2 + b * k\<^sub>2 + c = 0
[PROOF STEP]
apply (rule_tac x="?\<xi>2" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<noteq> (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<and> ((- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2)\<^sup>2 + b * ((- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2) + c = 0 \<and> ((- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2)\<^sup>2 + b * ((- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2) + c = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
b\<^sup>2 - 4 * c \<noteq> 0

goal (1 subgoal):
 1. (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<noteq> (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<and> ((- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2)\<^sup>2 + b * ((- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2) + c = 0 \<and> ((- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2)\<^sup>2 + b * ((- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2) + c = 0
[PROOF STEP]
using complex_quadratic_equation_monic_roots[of ?\<xi>1 b c]
[PROOF STATE]
proof (prove)
using this:
b\<^sup>2 - 4 * c \<noteq> 0
(- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 = (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<or> (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<Longrightarrow> ((- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2)\<^sup>2 + b * ((- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2) + c = 0

goal (1 subgoal):
 1. (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<noteq> (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<and> ((- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2)\<^sup>2 + b * ((- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2) + c = 0 \<and> ((- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2)\<^sup>2 + b * ((- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2) + c = 0
[PROOF STEP]
using complex_quadratic_equation_monic_roots[of ?\<xi>2 b c]
[PROOF STATE]
proof (prove)
using this:
b\<^sup>2 - 4 * c \<noteq> 0
(- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 = (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<or> (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<Longrightarrow> ((- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2)\<^sup>2 + b * ((- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2) + c = 0
(- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2 = (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<or> (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2 = (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<Longrightarrow> ((- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2)\<^sup>2 + b * ((- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2) + c = 0

goal (1 subgoal):
 1. (- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<noteq> (- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2 \<and> ((- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2)\<^sup>2 + b * ((- b + ccsqrt (b\<^sup>2 - 4 * c)) / 2) + c = 0 \<and> ((- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2)\<^sup>2 + b * ((- b - ccsqrt (b\<^sup>2 - 4 * c)) / 2) + c = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>k\<^sub>1 k\<^sub>2. k\<^sub>1 \<noteq> k\<^sub>2 \<and> k\<^sub>1\<^sup>2 + b * k\<^sub>1 + c = 0 \<and> k\<^sub>2\<^sup>2 + b * k\<^sub>2 + c = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complex_quadratic_equation_two_roots:
  fixes \<xi> :: complex
  assumes "a \<noteq> 0" and "a*\<xi>\<^sup>2 + b * \<xi> + c = 0"
  shows "\<xi> = (-b + ccsqrt(b\<^sup>2 - 4*a*c)) / (2*a) \<or>
         \<xi> = (-b - ccsqrt(b\<^sup>2 - 4*a*c)) / (2*a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> 0
a * \<xi>\<^sup>2 + b * \<xi> + c = 0
[PROOF STEP]
have "\<xi>\<^sup>2 + (b/a) * \<xi> + (c/a) = 0"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0
a * \<xi>\<^sup>2 + b * \<xi> + c = 0

goal (1 subgoal):
 1. \<xi>\<^sup>2 + b / a * \<xi> + c / a = 0
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
\<xi>\<^sup>2 + b / a * \<xi> + c / a = 0

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
hence "\<xi> = (-(b/a) + ccsqrt((b/a)\<^sup>2 - 4*(c/a))) / 2 \<or> \<xi> = (-(b/a) - ccsqrt((b/a)\<^sup>2 - 4*(c/a))) / 2"
[PROOF STATE]
proof (prove)
using this:
\<xi>\<^sup>2 + b / a * \<xi> + c / a = 0

goal (1 subgoal):
 1. \<xi> = (- (b / a) + ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2 \<or> \<xi> = (- (b / a) - ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2
[PROOF STEP]
using complex_quadratic_equation_monic_only_two_roots[of \<xi> "b/a" "c/a"]
[PROOF STATE]
proof (prove)
using this:
\<xi>\<^sup>2 + b / a * \<xi> + c / a = 0
\<xi>\<^sup>2 + b / a * \<xi> + c / a = 0 \<Longrightarrow> \<xi> = (- (b / a) + ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2 \<or> \<xi> = (- (b / a) - ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2

goal (1 subgoal):
 1. \<xi> = (- (b / a) + ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2 \<or> \<xi> = (- (b / a) - ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<xi> = (- (b / a) + ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2 \<or> \<xi> = (- (b / a) - ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
hence "\<exists> k. \<xi> = (-(b/a) + (-1)^k * ccsqrt((b/a)\<^sup>2 - 4*(c/a))) / 2"
[PROOF STATE]
proof (prove)
using this:
\<xi> = (- (b / a) + ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2 \<or> \<xi> = (- (b / a) - ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2

goal (1 subgoal):
 1. \<exists>k. \<xi> = (- (b / a) + (- 1) ^ k * ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2
[PROOF STEP]
by safe (rule_tac x="2" in exI, simp, rule_tac x="1" in exI, simp)
[PROOF STATE]
proof (state)
this:
\<exists>k. \<xi> = (- (b / a) + (- 1) ^ k * ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. \<xi> = (- (b / a) + (- 1) ^ k * ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2
[PROOF STEP]
obtain k1 where "\<xi> = (-(b/a) + (-1)^k1 * ccsqrt((b/a)\<^sup>2 - 4*(c/a))) / 2"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. \<xi> = (- (b / a) + (- 1) ^ k * ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2

goal (1 subgoal):
 1. (\<And>k1. \<xi> = (- (b / a) + (- 1) ^ k1 * ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<xi> = (- (b / a) + (- 1) ^ k1 * ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<xi> = (- (b / a) + (- 1) ^ k1 * ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
have "(b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4 * a * c) * (1 / a\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4 * a * c) * (1 / a\<^sup>2)
[PROOF STEP]
using \<open>a \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0

goal (1 subgoal):
 1. (b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4 * a * c) * (1 / a\<^sup>2)
[PROOF STEP]
by (simp add: field_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
(b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4 * a * c) * (1 / a\<^sup>2)

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
hence "ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1/a\<^sup>2) \<or>
         ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = - ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1/a\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
(b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4 * a * c) * (1 / a\<^sup>2)

goal (1 subgoal):
 1. ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2) \<or> ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = - ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2)
[PROOF STEP]
using ccsqrt_mult[of "b\<^sup>2 - 4 * a * c" "1/a\<^sup>2"]
[PROOF STATE]
proof (prove)
using this:
(b / a)\<^sup>2 - 4 * (c / a) = (b\<^sup>2 - 4 * a * c) * (1 / a\<^sup>2)
ccsqrt ((b\<^sup>2 - 4 * a * c) * (1 / a\<^sup>2)) = ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2) \<or> ccsqrt ((b\<^sup>2 - 4 * a * c) * (1 / a\<^sup>2)) = - ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2)

goal (1 subgoal):
 1. ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2) \<or> ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = - ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2) \<or> ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = - ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2)

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
hence "\<exists> k.  ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = (-1)^k * ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2) \<or> ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = - ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2)

goal (1 subgoal):
 1. \<exists>k. ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = (- 1) ^ k * ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2)
[PROOF STEP]
by safe (rule_tac x="2" in exI, simp, rule_tac x="1" in exI, simp)
[PROOF STATE]
proof (state)
this:
\<exists>k. ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = (- 1) ^ k * ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2)

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = (- 1) ^ k * ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2)
[PROOF STEP]
obtain k2 where "ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = (-1)^k2 * ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = (- 1) ^ k * ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2)

goal (1 subgoal):
 1. (\<And>k2. ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = (- 1) ^ k2 * ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = (- 1) ^ k2 * ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2)

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = (- 1) ^ k2 * ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2)

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
have "ccsqrt (1 / a\<^sup>2) = 1/a \<or> ccsqrt (1 / a\<^sup>2) = -1/a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccsqrt (1 / a\<^sup>2) = 1 / a \<or> ccsqrt (1 / a\<^sup>2) = - 1 / a
[PROOF STEP]
using ccsqrt[of "1/a" "1 / a\<^sup>2"]
[PROOF STATE]
proof (prove)
using this:
1 / a * (1 / a) = 1 / a\<^sup>2 \<Longrightarrow> 1 / a = ccsqrt (1 / a\<^sup>2) \<or> 1 / a = - ccsqrt (1 / a\<^sup>2)

goal (1 subgoal):
 1. ccsqrt (1 / a\<^sup>2) = 1 / a \<or> ccsqrt (1 / a\<^sup>2) = - 1 / a
[PROOF STEP]
by (auto simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
ccsqrt (1 / a\<^sup>2) = 1 / a \<or> ccsqrt (1 / a\<^sup>2) = - 1 / a

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
hence "\<exists> k. ccsqrt (1 / a\<^sup>2) = (-1)^k * 1/a"
[PROOF STATE]
proof (prove)
using this:
ccsqrt (1 / a\<^sup>2) = 1 / a \<or> ccsqrt (1 / a\<^sup>2) = - 1 / a

goal (1 subgoal):
 1. \<exists>k. ccsqrt (1 / a\<^sup>2) = (- 1) ^ k * 1 / a
[PROOF STEP]
by safe (rule_tac x="2" in exI, simp, rule_tac x="1" in exI, simp)
[PROOF STATE]
proof (state)
this:
\<exists>k. ccsqrt (1 / a\<^sup>2) = (- 1) ^ k * 1 / a

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. ccsqrt (1 / a\<^sup>2) = (- 1) ^ k * 1 / a
[PROOF STEP]
obtain k3 where "ccsqrt (1 / a\<^sup>2) = (-1)^k3 * 1/a"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. ccsqrt (1 / a\<^sup>2) = (- 1) ^ k * 1 / a

goal (1 subgoal):
 1. (\<And>k3. ccsqrt (1 / a\<^sup>2) = (- 1) ^ k3 * 1 / a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ccsqrt (1 / a\<^sup>2) = (- 1) ^ k3 * 1 / a

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<xi> = (- (b / a) + (- 1) ^ k1 * ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2
ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = (- 1) ^ k2 * ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2)
ccsqrt (1 / a\<^sup>2) = (- 1) ^ k3 * 1 / a
[PROOF STEP]
have "\<xi> = (- (b / a) + ((-1) ^ k1 * (-1) ^ k2 * (-1) ^ k3) * ccsqrt (b\<^sup>2 - 4 * a * c) * 1/a) / 2"
[PROOF STATE]
proof (prove)
using this:
\<xi> = (- (b / a) + (- 1) ^ k1 * ccsqrt ((b / a)\<^sup>2 - 4 * (c / a))) / 2
ccsqrt ((b / a)\<^sup>2 - 4 * (c / a)) = (- 1) ^ k2 * ccsqrt (b\<^sup>2 - 4 * a * c) * ccsqrt (1 / a\<^sup>2)
ccsqrt (1 / a\<^sup>2) = (- 1) ^ k3 * 1 / a

goal (1 subgoal):
 1. \<xi> = (- (b / a) + (- 1) ^ k1 * (- 1) ^ k2 * (- 1) ^ k3 * ccsqrt (b\<^sup>2 - 4 * a * c) * 1 / a) / 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<xi> = (- (b / a) + (- 1) ^ k1 * (- 1) ^ k2 * (- 1) ^ k3 * ccsqrt (b\<^sup>2 - 4 * a * c) * 1 / a) / 2

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<xi> = (- (b / a) + (- 1) ^ k1 * (- 1) ^ k2 * (- 1) ^ k3 * ccsqrt (b\<^sup>2 - 4 * a * c) * 1 / a) / 2

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
have "(-(1::complex)) ^ k1 * (-1) ^ k2 * (-1) ^ k3 = 1 \<or> (-(1::complex)) ^ k1 * (-1) ^ k2 * (-1) ^ k3 = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- 1) ^ k1 * (- 1) ^ k2 * (- 1) ^ k3 = 1 \<or> (- 1) ^ k1 * (- 1) ^ k2 * (- 1) ^ k3 = - 1
[PROOF STEP]
using neg_one_even_power[of "k1 + k2 + k3"]
[PROOF STATE]
proof (prove)
using this:
even (k1 + k2 + k3) \<Longrightarrow> (- (1::?'a)) ^ (k1 + k2 + k3) = (1::?'a)

goal (1 subgoal):
 1. (- 1) ^ k1 * (- 1) ^ k2 * (- 1) ^ k3 = 1 \<or> (- 1) ^ k1 * (- 1) ^ k2 * (- 1) ^ k3 = - 1
[PROOF STEP]
using neg_one_odd_power[of "k1 + k2 + k3"]
[PROOF STATE]
proof (prove)
using this:
even (k1 + k2 + k3) \<Longrightarrow> (- (1::?'a)) ^ (k1 + k2 + k3) = (1::?'a)
odd (k1 + k2 + k3) \<Longrightarrow> (- (1::?'a)) ^ (k1 + k2 + k3) = - (1::?'a)

goal (1 subgoal):
 1. (- 1) ^ k1 * (- 1) ^ k2 * (- 1) ^ k3 = 1 \<or> (- 1) ^ k1 * (- 1) ^ k2 * (- 1) ^ k3 = - 1
[PROOF STEP]
by (smt power_add)
[PROOF STATE]
proof (state)
this:
(- 1) ^ k1 * (- 1) ^ k2 * (- 1) ^ k3 = 1 \<or> (- 1) ^ k1 * (- 1) ^ k2 * (- 1) ^ k3 = - 1

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<xi> = (- (b / a) + (- 1) ^ k1 * (- 1) ^ k2 * (- 1) ^ k3 * ccsqrt (b\<^sup>2 - 4 * a * c) * 1 / a) / 2
(- 1) ^ k1 * (- 1) ^ k2 * (- 1) ^ k3 = 1 \<or> (- 1) ^ k1 * (- 1) ^ k2 * (- 1) ^ k3 = - 1
[PROOF STEP]
have "\<xi> = (- (b / a) + ccsqrt (b\<^sup>2 - 4 * a * c) * 1 / a) / 2 \<or> \<xi> = (- (b / a) - ccsqrt (b\<^sup>2 - 4 * a * c) * 1 / a) / 2"
[PROOF STATE]
proof (prove)
using this:
\<xi> = (- (b / a) + (- 1) ^ k1 * (- 1) ^ k2 * (- 1) ^ k3 * ccsqrt (b\<^sup>2 - 4 * a * c) * 1 / a) / 2
(- 1) ^ k1 * (- 1) ^ k2 * (- 1) ^ k3 = 1 \<or> (- 1) ^ k1 * (- 1) ^ k2 * (- 1) ^ k3 = - 1

goal (1 subgoal):
 1. \<xi> = (- (b / a) + ccsqrt (b\<^sup>2 - 4 * a * c) * 1 / a) / 2 \<or> \<xi> = (- (b / a) - ccsqrt (b\<^sup>2 - 4 * a * c) * 1 / a) / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<xi> = (- (b / a) + ccsqrt (b\<^sup>2 - 4 * a * c) * 1 / a) / 2 \<or> \<xi> = (- (b / a) - ccsqrt (b\<^sup>2 - 4 * a * c) * 1 / a) / 2

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<xi> = (- (b / a) + ccsqrt (b\<^sup>2 - 4 * a * c) * 1 / a) / 2 \<or> \<xi> = (- (b / a) - ccsqrt (b\<^sup>2 - 4 * a * c) * 1 / a) / 2

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
using \<open>a \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<xi> = (- (b / a) + ccsqrt (b\<^sup>2 - 4 * a * c) * 1 / a) / 2 \<or> \<xi> = (- (b / a) - ccsqrt (b\<^sup>2 - 4 * a * c) * 1 / a) / 2
a \<noteq> 0

goal (1 subgoal):
 1. \<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
\<xi> = (- b + ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a) \<or> \<xi> = (- b - ccsqrt (b\<^sup>2 - 4 * a * c)) / (2 * a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complex_quadratic_equation_only_two_roots:
  fixes x :: complex
  assumes "a \<noteq> 0"
  assumes "qf = (\<lambda> x. a*x\<^sup>2 + b*x + c)"
          "qf x1 = 0" and "qf x2 = 0" and "x1 \<noteq> x2"
          "qf x = 0"
  shows "x = x1 \<or> x = x2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x1 \<or> x = x2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0
qf = (\<lambda>x. a * x\<^sup>2 + b * x + c)
qf x1 = 0
qf x2 = 0
x1 \<noteq> x2
qf x = 0

goal (1 subgoal):
 1. x = x1 \<or> x = x2
[PROOF STEP]
using complex_quadratic_equation_two_roots
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0
qf = (\<lambda>x. a * x\<^sup>2 + b * x + c)
qf x1 = 0
qf x2 = 0
x1 \<noteq> x2
qf x = 0
\<lbrakk>?a \<noteq> 0; ?a * ?\<xi>\<^sup>2 + ?b * ?\<xi> + ?c = 0\<rbrakk> \<Longrightarrow> ?\<xi> = (- ?b + ccsqrt (?b\<^sup>2 - 4 * ?a * ?c)) / (2 * ?a) \<or> ?\<xi> = (- ?b - ccsqrt (?b\<^sup>2 - 4 * ?a * ?c)) / (2 * ?a)

goal (1 subgoal):
 1. x = x1 \<or> x = x2
[PROOF STEP]
by blast


[STATEMENT]
lemma quadratic_linear_at_most_2_intersections_help:
  fixes x y :: complex
  assumes "(a11, a12, a22) \<noteq> (0, 0, 0)" and "k2 \<noteq> 0"
          "qf = (\<lambda> x y. a11*x\<^sup>2 + 2*a12*x*y + a22*y\<^sup>2 + b1*x + b2*y + c)" and "lf = (\<lambda> x y. k1*x + k2*y + n)"
          "qf x y = 0" and "lf x y = 0"
          "pf = (\<lambda> x. (a11 - 2*a12*k1/k2 + a22*k1\<^sup>2/k2\<^sup>2)*x\<^sup>2 + (-2*a12*n/k2  + b1 + a22*2*n*k1/k2\<^sup>2 - b2*k1/k2)*x + a22*n\<^sup>2/k2\<^sup>2 - b2*n/k2 + c)"
          "yf = (\<lambda> x. (-n - k1*x) / k2)"
  shows "pf x = 0" and "y = yf x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pf x = 0 &&& y = yf x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pf x = 0
 2. y = yf x
[PROOF STEP]
show "y = yf x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = yf x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(a11, a12, a22) \<noteq> (0, 0, 0)
k2 \<noteq> 0
qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c)
lf = (\<lambda>x y. k1 * x + k2 * y + n)
qf x y = 0
lf x y = 0
pf = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c)
yf = (\<lambda>x. (- n - k1 * x) / k2)

goal (1 subgoal):
 1. y = yf x
[PROOF STEP]
by (simp add:field_simps eq_neg_iff_add_eq_0)
[PROOF STATE]
proof (state)
this:
y = yf x

goal (1 subgoal):
 1. pf x = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pf x = 0
[PROOF STEP]
have "2*a12*x*(-n - k1*x)/k2 = (-2*a12*n/k2)*x - (2*a12*k1/k2)*x\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * a12 * x * (- n - k1 * x) / k2 = - 2 * a12 * n / k2 * x - 2 * a12 * k1 / k2 * x\<^sup>2
[PROOF STEP]
by algebra
[PROOF STATE]
proof (state)
this:
2 * a12 * x * (- n - k1 * x) / k2 = - 2 * a12 * n / k2 * x - 2 * a12 * k1 / k2 * x\<^sup>2

goal (1 subgoal):
 1. pf x = 0
[PROOF STEP]
have "a22*((-n - k1*x)/k2)\<^sup>2 = a22*n\<^sup>2/k2\<^sup>2 + (a22*2*n*k1/k2\<^sup>2)*x + (a22*k1\<^sup>2/k2\<^sup>2)*x\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a22 * ((- n - k1 * x) / k2)\<^sup>2 = a22 * n\<^sup>2 / k2\<^sup>2 + a22 * 2 * n * k1 / k2\<^sup>2 * x + a22 * k1\<^sup>2 / k2\<^sup>2 * x\<^sup>2
[PROOF STEP]
by (simp add: power_divide) algebra
[PROOF STATE]
proof (state)
this:
a22 * ((- n - k1 * x) / k2)\<^sup>2 = a22 * n\<^sup>2 / k2\<^sup>2 + a22 * 2 * n * k1 / k2\<^sup>2 * x + a22 * k1\<^sup>2 / k2\<^sup>2 * x\<^sup>2

goal (1 subgoal):
 1. pf x = 0
[PROOF STEP]
have "2*a12*x*(-n - k1*x)/k2 = (-2*a12*n/k2)*x - (2*a12*k1/k2)*x\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * a12 * x * (- n - k1 * x) / k2 = - 2 * a12 * n / k2 * x - 2 * a12 * k1 / k2 * x\<^sup>2
[PROOF STEP]
by algebra
[PROOF STATE]
proof (state)
this:
2 * a12 * x * (- n - k1 * x) / k2 = - 2 * a12 * n / k2 * x - 2 * a12 * k1 / k2 * x\<^sup>2

goal (1 subgoal):
 1. pf x = 0
[PROOF STEP]
have "b2*(-n - k1*x)/k2 = -b2*n/k2 - (b2*k1/k2)*x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b2 * (- n - k1 * x) / k2 = - b2 * n / k2 - b2 * k1 / k2 * x
[PROOF STEP]
by algebra
[PROOF STATE]
proof (state)
this:
b2 * (- n - k1 * x) / k2 = - b2 * n / k2 - b2 * k1 / k2 * x

goal (1 subgoal):
 1. pf x = 0
[PROOF STEP]
have *: "y = (-n - k1*x)/k2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = (- n - k1 * x) / k2
[PROOF STEP]
using assms(2, 4, 6)
[PROOF STATE]
proof (prove)
using this:
k2 \<noteq> 0
lf = (\<lambda>x y. k1 * x + k2 * y + n)
lf x y = 0

goal (1 subgoal):
 1. y = (- n - k1 * x) / k2
[PROOF STEP]
by (simp add:field_simps eq_neg_iff_add_eq_0)
[PROOF STATE]
proof (state)
this:
y = (- n - k1 * x) / k2

goal (1 subgoal):
 1. pf x = 0
[PROOF STEP]
have "0 = a11*x\<^sup>2 + 2*a12*x*y + a22*y\<^sup>2 + b1*x + b2*y + c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(a11, a12, a22) \<noteq> (0, 0, 0)
k2 \<noteq> 0
qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c)
lf = (\<lambda>x y. k1 * x + k2 * y + n)
qf x y = 0
lf x y = 0
pf = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c)
yf = (\<lambda>x. (- n - k1 * x) / k2)

goal (1 subgoal):
 1. 0 = a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 = a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c

goal (1 subgoal):
 1. pf x = 0
[PROOF STEP]
hence "0 = a11*x\<^sup>2 + 2*a12*x*(-n - k1*x)/k2 + a22*((-n - k1*x)/k2)\<^sup>2 + b1*x + b2*(-n - k1*x)/k2 + c"
[PROOF STATE]
proof (prove)
using this:
0 = a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c

goal (1 subgoal):
 1. 0 = a11 * x\<^sup>2 + 2 * a12 * x * (- n - k1 * x) / k2 + a22 * ((- n - k1 * x) / k2)\<^sup>2 + b1 * x + b2 * (- n - k1 * x) / k2 + c
[PROOF STEP]
by (subst (asm) *, subst (asm) *, subst (asm) *) auto
[PROOF STATE]
proof (state)
this:
0 = a11 * x\<^sup>2 + 2 * a12 * x * (- n - k1 * x) / k2 + a22 * ((- n - k1 * x) / k2)\<^sup>2 + b1 * x + b2 * (- n - k1 * x) / k2 + c

goal (1 subgoal):
 1. pf x = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 = a11 * x\<^sup>2 + 2 * a12 * x * (- n - k1 * x) / k2 + a22 * ((- n - k1 * x) / k2)\<^sup>2 + b1 * x + b2 * (- n - k1 * x) / k2 + c

goal (1 subgoal):
 1. pf x = 0
[PROOF STEP]
have "... = (a11 - 2*a12*k1/k2 + a22*k1\<^sup>2/k2\<^sup>2)*x\<^sup>2 + (-2*a12*n/k2  + b1 + a22*2*n*k1/k2\<^sup>2 - b2*k1/k2)*x + a22*n\<^sup>2/k2\<^sup>2 -b2*n/k2 + c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a11 * x\<^sup>2 + 2 * a12 * x * (- n - k1 * x) / k2 + a22 * ((- n - k1 * x) / k2)\<^sup>2 + b1 * x + b2 * (- n - k1 * x) / k2 + c = (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c
[PROOF STEP]
using \<open>2*a12*x*(-n - k1*x)/k2 = (-2*a12*n/k2)*x - (2*a12*k1/k2)*x\<^sup>2\<close>
[PROOF STATE]
proof (prove)
using this:
2 * a12 * x * (- n - k1 * x) / k2 = - 2 * a12 * n / k2 * x - 2 * a12 * k1 / k2 * x\<^sup>2

goal (1 subgoal):
 1. a11 * x\<^sup>2 + 2 * a12 * x * (- n - k1 * x) / k2 + a22 * ((- n - k1 * x) / k2)\<^sup>2 + b1 * x + b2 * (- n - k1 * x) / k2 + c = (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c
[PROOF STEP]
using \<open>a22*((-n - k1*x)/k2)\<^sup>2 = a22*n\<^sup>2/k2\<^sup>2 + (a22*2*n*k1/k2\<^sup>2)*x + (a22*k1\<^sup>2/k2\<^sup>2)*x\<^sup>2\<close>
[PROOF STATE]
proof (prove)
using this:
2 * a12 * x * (- n - k1 * x) / k2 = - 2 * a12 * n / k2 * x - 2 * a12 * k1 / k2 * x\<^sup>2
a22 * ((- n - k1 * x) / k2)\<^sup>2 = a22 * n\<^sup>2 / k2\<^sup>2 + a22 * 2 * n * k1 / k2\<^sup>2 * x + a22 * k1\<^sup>2 / k2\<^sup>2 * x\<^sup>2

goal (1 subgoal):
 1. a11 * x\<^sup>2 + 2 * a12 * x * (- n - k1 * x) / k2 + a22 * ((- n - k1 * x) / k2)\<^sup>2 + b1 * x + b2 * (- n - k1 * x) / k2 + c = (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c
[PROOF STEP]
using \<open>b2*(-n - k1*x)/k2 = -b2*n/k2 - (b2*k1/k2)*x\<close>
[PROOF STATE]
proof (prove)
using this:
2 * a12 * x * (- n - k1 * x) / k2 = - 2 * a12 * n / k2 * x - 2 * a12 * k1 / k2 * x\<^sup>2
a22 * ((- n - k1 * x) / k2)\<^sup>2 = a22 * n\<^sup>2 / k2\<^sup>2 + a22 * 2 * n * k1 / k2\<^sup>2 * x + a22 * k1\<^sup>2 / k2\<^sup>2 * x\<^sup>2
b2 * (- n - k1 * x) / k2 = - b2 * n / k2 - b2 * k1 / k2 * x

goal (1 subgoal):
 1. a11 * x\<^sup>2 + 2 * a12 * x * (- n - k1 * x) / k2 + a22 * ((- n - k1 * x) / k2)\<^sup>2 + b1 * x + b2 * (- n - k1 * x) / k2 + c = (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c
[PROOF STEP]
by (simp add:field_simps)
[PROOF STATE]
proof (state)
this:
a11 * x\<^sup>2 + 2 * a12 * x * (- n - k1 * x) / k2 + a22 * ((- n - k1 * x) / k2)\<^sup>2 + b1 * x + b2 * (- n - k1 * x) / k2 + c = (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c

goal (1 subgoal):
 1. pf x = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 = (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c
[PROOF STEP]
show "pf x = 0"
[PROOF STATE]
proof (prove)
using this:
0 = (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c

goal (1 subgoal):
 1. pf x = 0
[PROOF STEP]
using assms(7)
[PROOF STATE]
proof (prove)
using this:
0 = (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c
pf = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c)

goal (1 subgoal):
 1. pf x = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pf x = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quadratic_linear_at_most_2_intersections_help':
  fixes x y :: complex
  assumes "qf = (\<lambda> x y. a11*x\<^sup>2 + 2*a12*x*y + a22*y\<^sup>2 + b1*x + b2*y + c)"
          "x = -n/k1" and "k1 \<noteq> 0" and "qf x y = 0"
          "yf = (\<lambda> y. k1\<^sup>2*a22*y\<^sup>2 + (-2*a12*n*k1 + b2*k1\<^sup>2)*y + a11*n\<^sup>2 - b1*n*k1 + c*k1\<^sup>2)"
  shows "yf y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. yf y = 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. yf y = 0
[PROOF STEP]
have "0 = a11*n\<^sup>2/k1\<^sup>2 - 2*a12*n*y/k1 + a22*y\<^sup>2 - b1*n/k1 + b2*y + c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = a11 * n\<^sup>2 / k1\<^sup>2 - 2 * a12 * n * y / k1 + a22 * y\<^sup>2 - b1 * n / k1 + b2 * y + c
[PROOF STEP]
using assms(1, 2, 4)
[PROOF STATE]
proof (prove)
using this:
qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c)
x = - n / k1
qf x y = 0

goal (1 subgoal):
 1. 0 = a11 * n\<^sup>2 / k1\<^sup>2 - 2 * a12 * n * y / k1 + a22 * y\<^sup>2 - b1 * n / k1 + b2 * y + c
[PROOF STEP]
by (simp add: power_divide)
[PROOF STATE]
proof (state)
this:
0 = a11 * n\<^sup>2 / k1\<^sup>2 - 2 * a12 * n * y / k1 + a22 * y\<^sup>2 - b1 * n / k1 + b2 * y + c

goal (1 subgoal):
 1. yf y = 0
[PROOF STEP]
hence "0 = a11*n\<^sup>2 - 2*a12*n*k1*y + a22*y\<^sup>2*k1\<^sup>2 - b1*n*k1 + b2*y*k1\<^sup>2 + c*k1\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
0 = a11 * n\<^sup>2 / k1\<^sup>2 - 2 * a12 * n * y / k1 + a22 * y\<^sup>2 - b1 * n / k1 + b2 * y + c

goal (1 subgoal):
 1. 0 = a11 * n\<^sup>2 - 2 * a12 * n * k1 * y + a22 * y\<^sup>2 * k1\<^sup>2 - b1 * n * k1 + b2 * y * k1\<^sup>2 + c * k1\<^sup>2
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
0 = a11 * n\<^sup>2 / k1\<^sup>2 - 2 * a12 * n * y / k1 + a22 * y\<^sup>2 - b1 * n / k1 + b2 * y + c
k1 \<noteq> 0

goal (1 subgoal):
 1. 0 = a11 * n\<^sup>2 - 2 * a12 * n * k1 * y + a22 * y\<^sup>2 * k1\<^sup>2 - b1 * n * k1 + b2 * y * k1\<^sup>2 + c * k1\<^sup>2
[PROOF STEP]
apply (simp add:field_simps power2_eq_square)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b1 * (k1 * (k1 * n)) + a12 * (k1 * (k1 * (n * (y * 2)))) = a11 * (k1 * (n * n)) + (c * (k1 * (k1 * k1)) + (b2 * (k1 * (k1 * (k1 * y))) + a22 * (k1 * (k1 * (k1 * (y * y)))))); k1 \<noteq> 0\<rbrakk> \<Longrightarrow> b1 * (k1 * n) + a12 * (k1 * (n * (y * 2))) = a11 * (n * n) + (c * (k1 * k1) + (b2 * (k1 * (k1 * y)) + a22 * (k1 * (k1 * (y * y)))))
[PROOF STEP]
by algebra
[PROOF STATE]
proof (state)
this:
0 = a11 * n\<^sup>2 - 2 * a12 * n * k1 * y + a22 * y\<^sup>2 * k1\<^sup>2 - b1 * n * k1 + b2 * y * k1\<^sup>2 + c * k1\<^sup>2

goal (1 subgoal):
 1. yf y = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 = a11 * n\<^sup>2 - 2 * a12 * n * k1 * y + a22 * y\<^sup>2 * k1\<^sup>2 - b1 * n * k1 + b2 * y * k1\<^sup>2 + c * k1\<^sup>2

goal (1 subgoal):
 1. yf y = 0
[PROOF STEP]
using assms(1, 4, 5)
[PROOF STATE]
proof (prove)
using this:
0 = a11 * n\<^sup>2 - 2 * a12 * n * k1 * y + a22 * y\<^sup>2 * k1\<^sup>2 - b1 * n * k1 + b2 * y * k1\<^sup>2 + c * k1\<^sup>2
qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c)
qf x y = 0
yf = (\<lambda>y. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2)

goal (1 subgoal):
 1. yf y = 0
[PROOF STEP]
by (simp add:field_simps)
[PROOF STATE]
proof (state)
this:
yf y = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quadratic_linear_at_most_2_intersections:
  fixes x y x1 y1 x2 y2 :: complex
  assumes "(a11, a12, a22) \<noteq> (0, 0, 0)" and "(k1, k2) \<noteq> (0, 0)"
  assumes "a11*k2\<^sup>2 - 2*a12*k1*k2 + a22*k1\<^sup>2 \<noteq> 0"
  assumes "qf = (\<lambda> x y. a11*x\<^sup>2 + 2*a12*x*y + a22*y\<^sup>2 + b1*x + b2*y + c)" and "lf = (\<lambda> x y. k1*x + k2*y + n)"
          "qf x1 y1 = 0" and "lf x1 y1 = 0"
          "qf x2 y2 = 0" and "lf x2 y2 = 0"
          "(x1, y1) \<noteq> (x2, y2)"
          "qf x y = 0" and "lf x y = 0"
  shows "(x, y) = (x1, y1) \<or> (x, y) = (x2, y2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
proof(cases "k2 = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k2 = 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
 2. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k2 = 0

goal (2 subgoals):
 1. k2 = 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
 2. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
hence "k1 \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
k2 = 0

goal (1 subgoal):
 1. k1 \<noteq> 0
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
k2 = 0
(k1, k2) \<noteq> (0, 0)

goal (1 subgoal):
 1. k1 \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k1 \<noteq> 0

goal (2 subgoals):
 1. k2 = 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
 2. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "a22*k1\<^sup>2 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a22 * k1\<^sup>2 \<noteq> 0
[PROOF STEP]
using assms(3) True
[PROOF STATE]
proof (prove)
using this:
a11 * k2\<^sup>2 - 2 * a12 * k1 * k2 + a22 * k1\<^sup>2 \<noteq> 0
k2 = 0

goal (1 subgoal):
 1. a22 * k1\<^sup>2 \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a22 * k1\<^sup>2 \<noteq> 0

goal (2 subgoals):
 1. k2 = 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
 2. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "x1 = -n/k1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 = - n / k1
[PROOF STEP]
using \<open>k1 \<noteq> 0\<close> assms(5, 7) True
[PROOF STATE]
proof (prove)
using this:
k1 \<noteq> 0
lf = (\<lambda>x y. k1 * x + k2 * y + n)
lf x1 y1 = 0
k2 = 0

goal (1 subgoal):
 1. x1 = - n / k1
[PROOF STEP]
by (metis add.right_neutral add_eq_0_iff2 mult_zero_left nonzero_mult_div_cancel_left)
[PROOF STATE]
proof (state)
this:
x1 = - n / k1

goal (2 subgoals):
 1. k2 = 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
 2. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "x2 = -n/k1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x2 = - n / k1
[PROOF STEP]
using \<open>k1 \<noteq> 0\<close> assms(5, 9) True
[PROOF STATE]
proof (prove)
using this:
k1 \<noteq> 0
lf = (\<lambda>x y. k1 * x + k2 * y + n)
lf x2 y2 = 0
k2 = 0

goal (1 subgoal):
 1. x2 = - n / k1
[PROOF STEP]
by (metis add.right_neutral add_eq_0_iff2 mult_zero_left nonzero_mult_div_cancel_left)
[PROOF STATE]
proof (state)
this:
x2 = - n / k1

goal (2 subgoals):
 1. k2 = 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
 2. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "x = -n/k1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = - n / k1
[PROOF STEP]
using \<open>k1 \<noteq> 0\<close> assms(5, 12) True
[PROOF STATE]
proof (prove)
using this:
k1 \<noteq> 0
lf = (\<lambda>x y. k1 * x + k2 * y + n)
lf x y = 0
k2 = 0

goal (1 subgoal):
 1. x = - n / k1
[PROOF STEP]
by (metis add.right_neutral add_eq_0_iff2 mult_zero_left nonzero_mult_div_cancel_left)
[PROOF STATE]
proof (state)
this:
x = - n / k1

goal (2 subgoals):
 1. k2 = 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
 2. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
let ?yf =  "(\<lambda> y. k1\<^sup>2*a22*y\<^sup>2 + (-2*a12*n*k1 + b2*k1\<^sup>2)*y + a11*n\<^sup>2 - b1*n*k1 + c*k1\<^sup>2)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k2 = 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
 2. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "?yf y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0
[PROOF STEP]
using quadratic_linear_at_most_2_intersections_help'[of qf a11 a12 a22 b1 b2 c x n k1 y ?yf]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); x = - n / k1; k1 \<noteq> 0; qf x y = 0; (\<lambda>y. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2) = (\<lambda>y. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2)\<rbrakk> \<Longrightarrow> k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0

goal (1 subgoal):
 1. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0
[PROOF STEP]
using assms(4, 11) \<open>k1 \<noteq> 0\<close> \<open>x = -n/k1\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); x = - n / k1; k1 \<noteq> 0; qf x y = 0; (\<lambda>y. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2) = (\<lambda>y. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2)\<rbrakk> \<Longrightarrow> k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0
qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c)
qf x y = 0
k1 \<noteq> 0
x = - n / k1

goal (1 subgoal):
 1. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0

goal (2 subgoals):
 1. k2 = 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
 2. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "?yf y1 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k1\<^sup>2 * a22 * y1\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y1 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0
[PROOF STEP]
using quadratic_linear_at_most_2_intersections_help'[of qf a11 a12 a22 b1 b2 c x1 n k1 y1 ?yf]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); x1 = - n / k1; k1 \<noteq> 0; qf x1 y1 = 0; (\<lambda>y. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2) = (\<lambda>y. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2)\<rbrakk> \<Longrightarrow> k1\<^sup>2 * a22 * y1\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y1 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0

goal (1 subgoal):
 1. k1\<^sup>2 * a22 * y1\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y1 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0
[PROOF STEP]
using assms(4, 6) \<open>k1 \<noteq> 0\<close> \<open>x1 = -n/k1\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); x1 = - n / k1; k1 \<noteq> 0; qf x1 y1 = 0; (\<lambda>y. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2) = (\<lambda>y. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2)\<rbrakk> \<Longrightarrow> k1\<^sup>2 * a22 * y1\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y1 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0
qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c)
qf x1 y1 = 0
k1 \<noteq> 0
x1 = - n / k1

goal (1 subgoal):
 1. k1\<^sup>2 * a22 * y1\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y1 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k1\<^sup>2 * a22 * y1\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y1 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0

goal (2 subgoals):
 1. k2 = 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
 2. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "?yf y2 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k1\<^sup>2 * a22 * y2\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y2 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0
[PROOF STEP]
using quadratic_linear_at_most_2_intersections_help'[of qf a11 a12 a22 b1 b2 c x2 n k1 y2 ?yf]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); x2 = - n / k1; k1 \<noteq> 0; qf x2 y2 = 0; (\<lambda>y. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2) = (\<lambda>y. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2)\<rbrakk> \<Longrightarrow> k1\<^sup>2 * a22 * y2\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y2 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0

goal (1 subgoal):
 1. k1\<^sup>2 * a22 * y2\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y2 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0
[PROOF STEP]
using assms(4, 8) \<open>k1 \<noteq> 0\<close> \<open>x2 = -n/k1\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); x2 = - n / k1; k1 \<noteq> 0; qf x2 y2 = 0; (\<lambda>y. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2) = (\<lambda>y. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2)\<rbrakk> \<Longrightarrow> k1\<^sup>2 * a22 * y2\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y2 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0
qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c)
qf x2 y2 = 0
k1 \<noteq> 0
x2 = - n / k1

goal (1 subgoal):
 1. k1\<^sup>2 * a22 * y2\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y2 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k1\<^sup>2 * a22 * y2\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y2 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0

goal (2 subgoals):
 1. k2 = 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
 2. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "y1 \<noteq> y2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y1 \<noteq> y2
[PROOF STEP]
using assms(10) \<open>x1 = -n/k1\<close> \<open>x2 = -n/k1\<close>
[PROOF STATE]
proof (prove)
using this:
(x1, y1) \<noteq> (x2, y2)
x1 = - n / k1
x2 = - n / k1

goal (1 subgoal):
 1. y1 \<noteq> y2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y1 \<noteq> y2

goal (2 subgoals):
 1. k2 = 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
 2. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "y = y1 \<or> y = y2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = y1 \<or> y = y2
[PROOF STEP]
using complex_quadratic_equation_only_two_roots[of "a22*k1\<^sup>2" ?yf "-2*a12*n*k1 + b2*k1\<^sup>2" "a11*n\<^sup>2 - b1*n*k1 + c*k1\<^sup>2"
                                                        y1 y2 y]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a22 * k1\<^sup>2 \<noteq> 0; (\<lambda>y. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2) = (\<lambda>x. a22 * k1\<^sup>2 * x\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * x + (a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2)); k1\<^sup>2 * a22 * y1\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y1 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0; k1\<^sup>2 * a22 * y2\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y2 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0; y1 \<noteq> y2; k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0\<rbrakk> \<Longrightarrow> y = y1 \<or> y = y2

goal (1 subgoal):
 1. y = y1 \<or> y = y2
[PROOF STEP]
using \<open>a22*k1\<^sup>2 \<noteq> 0\<close> \<open>?yf y1 = 0\<close> \<open>y1 \<noteq> y2\<close> \<open>?yf y2 = 0\<close> \<open>?yf y = 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a22 * k1\<^sup>2 \<noteq> 0; (\<lambda>y. k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2) = (\<lambda>x. a22 * k1\<^sup>2 * x\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * x + (a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2)); k1\<^sup>2 * a22 * y1\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y1 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0; k1\<^sup>2 * a22 * y2\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y2 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0; y1 \<noteq> y2; k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0\<rbrakk> \<Longrightarrow> y = y1 \<or> y = y2
a22 * k1\<^sup>2 \<noteq> 0
k1\<^sup>2 * a22 * y1\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y1 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0
y1 \<noteq> y2
k1\<^sup>2 * a22 * y2\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y2 + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0
k1\<^sup>2 * a22 * y\<^sup>2 + (- 2 * a12 * n * k1 + b2 * k1\<^sup>2) * y + a11 * n\<^sup>2 - b1 * n * k1 + c * k1\<^sup>2 = 0

goal (1 subgoal):
 1. y = y1 \<or> y = y2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
y = y1 \<or> y = y2

goal (2 subgoals):
 1. k2 = 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
 2. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
y = y1 \<or> y = y2

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
using \<open>x1 = -n/k1\<close> \<open>x2 = -n/k1\<close>  \<open>x = -n/k1\<close>
[PROOF STATE]
proof (prove)
using this:
y = y1 \<or> y = y2
x1 = - n / k1
x2 = - n / k1
x = - n / k1

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) = (x1, y1) \<or> (x, y) = (x2, y2)

goal (1 subgoal):
 1. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
k2 \<noteq> 0

goal (1 subgoal):
 1. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
let ?py = "(\<lambda> x. (-n - k1*x)/k2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
let ?pf = "(\<lambda> x. (a11 - 2*a12*k1/k2 + a22*k1\<^sup>2/k2\<^sup>2)*x\<^sup>2 + (-2*a12*n/k2  + b1 + a22*2*n*k1/k2\<^sup>2 - b2*k1/k2)*x + a22*n\<^sup>2/k2\<^sup>2 -b2*n/k2 + c)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "?pf x1 = 0" "y1 = ?py x1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x1\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x1 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0 &&& y1 = (- n - k1 * x1) / k2
[PROOF STEP]
using quadratic_linear_at_most_2_intersections_help[of a11 a12 a22 k2 qf b1 b2 c lf k1 n x1 y1]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(a11, a12, a22) \<noteq> (0, 0, 0); k2 \<noteq> 0; qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); lf = (\<lambda>x y. k1 * x + k2 * y + n); qf x1 y1 = 0; lf x1 y1 = 0; ?pf = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c); ?yf = (\<lambda>x. (- n - k1 * x) / k2)\<rbrakk> \<Longrightarrow> ?pf x1 = 0
\<lbrakk>(a11, a12, a22) \<noteq> (0, 0, 0); k2 \<noteq> 0; qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); lf = (\<lambda>x y. k1 * x + k2 * y + n); qf x1 y1 = 0; lf x1 y1 = 0; ?pf = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c); ?yf = (\<lambda>x. (- n - k1 * x) / k2)\<rbrakk> \<Longrightarrow> y1 = ?yf x1

goal (1 subgoal):
 1. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x1\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x1 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0 &&& y1 = (- n - k1 * x1) / k2
[PROOF STEP]
using assms(1, 4, 5, 6, 7) False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(a11, a12, a22) \<noteq> (0, 0, 0); k2 \<noteq> 0; qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); lf = (\<lambda>x y. k1 * x + k2 * y + n); qf x1 y1 = 0; lf x1 y1 = 0; ?pf = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c); ?yf = (\<lambda>x. (- n - k1 * x) / k2)\<rbrakk> \<Longrightarrow> ?pf x1 = 0
\<lbrakk>(a11, a12, a22) \<noteq> (0, 0, 0); k2 \<noteq> 0; qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); lf = (\<lambda>x y. k1 * x + k2 * y + n); qf x1 y1 = 0; lf x1 y1 = 0; ?pf = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c); ?yf = (\<lambda>x. (- n - k1 * x) / k2)\<rbrakk> \<Longrightarrow> y1 = ?yf x1
(a11, a12, a22) \<noteq> (0, 0, 0)
qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c)
lf = (\<lambda>x y. k1 * x + k2 * y + n)
qf x1 y1 = 0
lf x1 y1 = 0
k2 \<noteq> 0

goal (1 subgoal):
 1. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x1\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x1 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0 &&& y1 = (- n - k1 * x1) / k2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x1\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x1 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0
y1 = (- n - k1 * x1) / k2

goal (1 subgoal):
 1. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "?pf x2 = 0" "y2 = ?py x2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x2\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x2 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0 &&& y2 = (- n - k1 * x2) / k2
[PROOF STEP]
using quadratic_linear_at_most_2_intersections_help[of a11 a12 a22 k2 qf b1 b2 c lf k1 n x2 y2]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(a11, a12, a22) \<noteq> (0, 0, 0); k2 \<noteq> 0; qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); lf = (\<lambda>x y. k1 * x + k2 * y + n); qf x2 y2 = 0; lf x2 y2 = 0; ?pf = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c); ?yf = (\<lambda>x. (- n - k1 * x) / k2)\<rbrakk> \<Longrightarrow> ?pf x2 = 0
\<lbrakk>(a11, a12, a22) \<noteq> (0, 0, 0); k2 \<noteq> 0; qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); lf = (\<lambda>x y. k1 * x + k2 * y + n); qf x2 y2 = 0; lf x2 y2 = 0; ?pf = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c); ?yf = (\<lambda>x. (- n - k1 * x) / k2)\<rbrakk> \<Longrightarrow> y2 = ?yf x2

goal (1 subgoal):
 1. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x2\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x2 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0 &&& y2 = (- n - k1 * x2) / k2
[PROOF STEP]
using assms(1, 4, 5, 8, 9) False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(a11, a12, a22) \<noteq> (0, 0, 0); k2 \<noteq> 0; qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); lf = (\<lambda>x y. k1 * x + k2 * y + n); qf x2 y2 = 0; lf x2 y2 = 0; ?pf = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c); ?yf = (\<lambda>x. (- n - k1 * x) / k2)\<rbrakk> \<Longrightarrow> ?pf x2 = 0
\<lbrakk>(a11, a12, a22) \<noteq> (0, 0, 0); k2 \<noteq> 0; qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); lf = (\<lambda>x y. k1 * x + k2 * y + n); qf x2 y2 = 0; lf x2 y2 = 0; ?pf = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c); ?yf = (\<lambda>x. (- n - k1 * x) / k2)\<rbrakk> \<Longrightarrow> y2 = ?yf x2
(a11, a12, a22) \<noteq> (0, 0, 0)
qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c)
lf = (\<lambda>x y. k1 * x + k2 * y + n)
qf x2 y2 = 0
lf x2 y2 = 0
k2 \<noteq> 0

goal (1 subgoal):
 1. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x2\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x2 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0 &&& y2 = (- n - k1 * x2) / k2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x2\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x2 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0
y2 = (- n - k1 * x2) / k2

goal (1 subgoal):
 1. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "?pf x = 0" "y = ?py x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0 &&& y = (- n - k1 * x) / k2
[PROOF STEP]
using quadratic_linear_at_most_2_intersections_help[of a11 a12 a22 k2 qf b1 b2 c lf k1 n x y]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(a11, a12, a22) \<noteq> (0, 0, 0); k2 \<noteq> 0; qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); lf = (\<lambda>x y. k1 * x + k2 * y + n); qf x y = 0; lf x y = 0; ?pf = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c); ?yf = (\<lambda>x. (- n - k1 * x) / k2)\<rbrakk> \<Longrightarrow> ?pf x = 0
\<lbrakk>(a11, a12, a22) \<noteq> (0, 0, 0); k2 \<noteq> 0; qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); lf = (\<lambda>x y. k1 * x + k2 * y + n); qf x y = 0; lf x y = 0; ?pf = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c); ?yf = (\<lambda>x. (- n - k1 * x) / k2)\<rbrakk> \<Longrightarrow> y = ?yf x

goal (1 subgoal):
 1. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0 &&& y = (- n - k1 * x) / k2
[PROOF STEP]
using assms(1, 4, 5, 11, 12) False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(a11, a12, a22) \<noteq> (0, 0, 0); k2 \<noteq> 0; qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); lf = (\<lambda>x y. k1 * x + k2 * y + n); qf x y = 0; lf x y = 0; ?pf = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c); ?yf = (\<lambda>x. (- n - k1 * x) / k2)\<rbrakk> \<Longrightarrow> ?pf x = 0
\<lbrakk>(a11, a12, a22) \<noteq> (0, 0, 0); k2 \<noteq> 0; qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c); lf = (\<lambda>x y. k1 * x + k2 * y + n); qf x y = 0; lf x y = 0; ?pf = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c); ?yf = (\<lambda>x. (- n - k1 * x) / k2)\<rbrakk> \<Longrightarrow> y = ?yf x
(a11, a12, a22) \<noteq> (0, 0, 0)
qf = (\<lambda>x y. a11 * x\<^sup>2 + 2 * a12 * x * y + a22 * y\<^sup>2 + b1 * x + b2 * y + c)
lf = (\<lambda>x y. k1 * x + k2 * y + n)
qf x y = 0
lf x y = 0
k2 \<noteq> 0

goal (1 subgoal):
 1. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0 &&& y = (- n - k1 * x) / k2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0
y = (- n - k1 * x) / k2

goal (1 subgoal):
 1. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "x1 \<noteq> x2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 \<noteq> x2
[PROOF STEP]
using assms(10) \<open>y1 = ?py x1\<close> \<open>y2 = ?py x2\<close>
[PROOF STATE]
proof (prove)
using this:
(x1, y1) \<noteq> (x2, y2)
y1 = (- n - k1 * x1) / k2
y2 = (- n - k1 * x2) / k2

goal (1 subgoal):
 1. x1 \<noteq> x2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x1 \<noteq> x2

goal (1 subgoal):
 1. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "a11 - 2*a12*k1/k2 + a22*k1\<^sup>2/k2\<^sup>2 = (a11 * k2\<^sup>2 - 2 * a12 * k1 * k2 + a22 * k1\<^sup>2)/k2\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2 = (a11 * k2\<^sup>2 - 2 * a12 * k1 * k2 + a22 * k1\<^sup>2) / k2\<^sup>2
[PROOF STEP]
by (simp add: False power2_eq_square add_divide_distrib diff_divide_distrib)
[PROOF STATE]
proof (state)
this:
a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2 = (a11 * k2\<^sup>2 - 2 * a12 * k1 * k2 + a22 * k1\<^sup>2) / k2\<^sup>2

goal (1 subgoal):
 1. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2 = (a11 * k2\<^sup>2 - 2 * a12 * k1 * k2 + a22 * k1\<^sup>2) / k2\<^sup>2

goal (1 subgoal):
 1. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "...  \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a11 * k2\<^sup>2 - 2 * a12 * k1 * k2 + a22 * k1\<^sup>2) / k2\<^sup>2 \<noteq> 0
[PROOF STEP]
using False assms(3)
[PROOF STATE]
proof (prove)
using this:
k2 \<noteq> 0
a11 * k2\<^sup>2 - 2 * a12 * k1 * k2 + a22 * k1\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. (a11 * k2\<^sup>2 - 2 * a12 * k1 * k2 + a22 * k1\<^sup>2) / k2\<^sup>2 \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(a11 * k2\<^sup>2 - 2 * a12 * k1 * k2 + a22 * k1\<^sup>2) / k2\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2 \<noteq> 0
[PROOF STEP]
have "a11 - 2*a12*k1/k2 + a22*k1\<^sup>2/k2\<^sup>2 \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2 \<noteq> 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "x = x1 \<or> x = x2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x1 \<or> x = x2
[PROOF STEP]
using complex_quadratic_equation_only_two_roots[of "a11 - 2*a12*k1/k2 + a22*k1\<^sup>2/k2\<^sup>2" ?pf
                                                       "(- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2)"
                                                       "a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c" x1 x2 x]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2 \<noteq> 0; (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c) = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + (a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c)); (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x1\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x1 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0; (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x2\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x2 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0; x1 \<noteq> x2; (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0\<rbrakk> \<Longrightarrow> x = x1 \<or> x = x2

goal (1 subgoal):
 1. x = x1 \<or> x = x2
[PROOF STEP]
using \<open>?pf x2 = 0\<close> \<open>?pf x1 = 0\<close> \<open>?pf x = 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2 \<noteq> 0; (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c) = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + (a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c)); (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x1\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x1 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0; (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x2\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x2 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0; x1 \<noteq> x2; (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0\<rbrakk> \<Longrightarrow> x = x1 \<or> x = x2
(a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x2\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x2 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0
(a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x1\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x1 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0
(a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0

goal (1 subgoal):
 1. x = x1 \<or> x = x2
[PROOF STEP]
using \<open>a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2 \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2 \<noteq> 0; (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c) = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + (a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c)); (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x1\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x1 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0; (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x2\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x2 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0; x1 \<noteq> x2; (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0\<rbrakk> \<Longrightarrow> x = x1 \<or> x = x2
(a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x2\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x2 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0
(a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x1\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x1 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0
(a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0
a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. x = x1 \<or> x = x2
[PROOF STEP]
using \<open>x1 \<noteq> x2\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2 \<noteq> 0; (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c) = (\<lambda>x. (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + (a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c)); (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x1\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x1 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0; (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x2\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x2 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0; x1 \<noteq> x2; (a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0\<rbrakk> \<Longrightarrow> x = x1 \<or> x = x2
(a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x2\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x2 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0
(a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x1\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x1 + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0
(a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2) * x\<^sup>2 + (- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k2\<^sup>2 - b2 * k1 / k2) * x + a22 * n\<^sup>2 / k2\<^sup>2 - b2 * n / k2 + c = 0
a11 - 2 * a12 * k1 / k2 + a22 * k1\<^sup>2 / k2\<^sup>2 \<noteq> 0
x1 \<noteq> x2

goal (1 subgoal):
 1. x = x1 \<or> x = x2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x = x1 \<or> x = x2

goal (1 subgoal):
 1. k2 \<noteq> 0 \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = x1 \<or> x = x2

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
using \<open>y = ?py x\<close> \<open>y1 = ?py x1\<close> \<open>y2 = ?py x2\<close>
[PROOF STATE]
proof (prove)
using this:
x = x1 \<or> x = x2
y = (- n - k1 * x) / k2
y1 = (- n - k1 * x1) / k2
y2 = (- n - k1 * x2) / k2

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
by (cases "x = x1", auto)
[PROOF STATE]
proof (state)
this:
(x, y) = (x1, y1) \<or> (x, y) = (x2, y2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quadratic_quadratic_at_most_2_intersections':
  fixes x y x1 y1 x2 y2 :: complex
  assumes "b2 \<noteq> B2 \<or> b1 \<noteq> B1"
          "(b2 - B2)\<^sup>2 + (b1 - B1)\<^sup>2 \<noteq> 0"
  assumes "qf1 = (\<lambda> x y. x\<^sup>2 + y\<^sup>2 + b1*x + b2*y + c)"
          "qf2 = (\<lambda> x y. x\<^sup>2 + y\<^sup>2 + B1*x + B2*y + C)"
          "qf1 x1 y1 = 0" "qf2 x1 y1 = 0"
          "qf1 x2 y2 = 0" "qf2 x2 y2 = 0"
          "(x1, y1) \<noteq> (x2, y2)"
          "qf1 x y = 0" "qf2 x y = 0"
  shows "(x, y) = (x1, y1) \<or> (x, y) = (x2, y2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "x\<^sup>2 + y\<^sup>2 + b1*x + b2*y + c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>2 + y\<^sup>2 + b1 * x + b2 * y + c = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
b2 \<noteq> B2 \<or> b1 \<noteq> B1
(b2 - B2)\<^sup>2 + (b1 - B1)\<^sup>2 \<noteq> 0
qf1 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 * x + b2 * y + c)
qf2 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 * x + B2 * y + C)
qf1 x1 y1 = 0
qf2 x1 y1 = 0
qf1 x2 y2 = 0
qf2 x2 y2 = 0
(x1, y1) \<noteq> (x2, y2)
qf1 x y = 0
qf2 x y = 0

goal (1 subgoal):
 1. x\<^sup>2 + y\<^sup>2 + b1 * x + b2 * y + c = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x\<^sup>2 + y\<^sup>2 + b1 * x + b2 * y + c = 0

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "x\<^sup>2 + y\<^sup>2 + B1*x + B2*y + C = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>2 + y\<^sup>2 + B1 * x + B2 * y + C = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
b2 \<noteq> B2 \<or> b1 \<noteq> B1
(b2 - B2)\<^sup>2 + (b1 - B1)\<^sup>2 \<noteq> 0
qf1 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 * x + b2 * y + c)
qf2 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 * x + B2 * y + C)
qf1 x1 y1 = 0
qf2 x1 y1 = 0
qf1 x2 y2 = 0
qf2 x2 y2 = 0
(x1, y1) \<noteq> (x2, y2)
qf1 x y = 0
qf2 x y = 0

goal (1 subgoal):
 1. x\<^sup>2 + y\<^sup>2 + B1 * x + B2 * y + C = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x\<^sup>2 + y\<^sup>2 + B1 * x + B2 * y + C = 0

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
hence "0 = x\<^sup>2 + y\<^sup>2 + b1*x + b2*y + c - (x\<^sup>2 + y\<^sup>2 + B1*x + B2*y + C)"
[PROOF STATE]
proof (prove)
using this:
x\<^sup>2 + y\<^sup>2 + B1 * x + B2 * y + C = 0

goal (1 subgoal):
 1. 0 = x\<^sup>2 + y\<^sup>2 + b1 * x + b2 * y + c - (x\<^sup>2 + y\<^sup>2 + B1 * x + B2 * y + C)
[PROOF STEP]
using \<open>x\<^sup>2 + y\<^sup>2 + b1*x + b2*y + c = 0\<close>
[PROOF STATE]
proof (prove)
using this:
x\<^sup>2 + y\<^sup>2 + B1 * x + B2 * y + C = 0
x\<^sup>2 + y\<^sup>2 + b1 * x + b2 * y + c = 0

goal (1 subgoal):
 1. 0 = x\<^sup>2 + y\<^sup>2 + b1 * x + b2 * y + c - (x\<^sup>2 + y\<^sup>2 + B1 * x + B2 * y + C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 = x\<^sup>2 + y\<^sup>2 + b1 * x + b2 * y + c - (x\<^sup>2 + y\<^sup>2 + B1 * x + B2 * y + C)

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
hence "0 = (b1 - B1)*x + (b2 - B2)*y + c - C"
[PROOF STATE]
proof (prove)
using this:
0 = x\<^sup>2 + y\<^sup>2 + b1 * x + b2 * y + c - (x\<^sup>2 + y\<^sup>2 + B1 * x + B2 * y + C)

goal (1 subgoal):
 1. 0 = (b1 - B1) * x + (b2 - B2) * y + c - C
[PROOF STEP]
by (simp  add:field_simps)
[PROOF STATE]
proof (state)
this:
0 = (b1 - B1) * x + (b2 - B2) * y + c - C

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "x1\<^sup>2 + y1\<^sup>2 + b1*x1 + b2*y1 + c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1\<^sup>2 + y1\<^sup>2 + b1 * x1 + b2 * y1 + c = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
b2 \<noteq> B2 \<or> b1 \<noteq> B1
(b2 - B2)\<^sup>2 + (b1 - B1)\<^sup>2 \<noteq> 0
qf1 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 * x + b2 * y + c)
qf2 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 * x + B2 * y + C)
qf1 x1 y1 = 0
qf2 x1 y1 = 0
qf1 x2 y2 = 0
qf2 x2 y2 = 0
(x1, y1) \<noteq> (x2, y2)
qf1 x y = 0
qf2 x y = 0

goal (1 subgoal):
 1. x1\<^sup>2 + y1\<^sup>2 + b1 * x1 + b2 * y1 + c = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x1\<^sup>2 + y1\<^sup>2 + b1 * x1 + b2 * y1 + c = 0

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "x1\<^sup>2 + y1\<^sup>2 + B1*x1 + B2*y1 + C = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1\<^sup>2 + y1\<^sup>2 + B1 * x1 + B2 * y1 + C = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
b2 \<noteq> B2 \<or> b1 \<noteq> B1
(b2 - B2)\<^sup>2 + (b1 - B1)\<^sup>2 \<noteq> 0
qf1 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 * x + b2 * y + c)
qf2 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 * x + B2 * y + C)
qf1 x1 y1 = 0
qf2 x1 y1 = 0
qf1 x2 y2 = 0
qf2 x2 y2 = 0
(x1, y1) \<noteq> (x2, y2)
qf1 x y = 0
qf2 x y = 0

goal (1 subgoal):
 1. x1\<^sup>2 + y1\<^sup>2 + B1 * x1 + B2 * y1 + C = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x1\<^sup>2 + y1\<^sup>2 + B1 * x1 + B2 * y1 + C = 0

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
hence "0 = x1\<^sup>2 + y1\<^sup>2 + b1*x1 + b2*y1 + c - (x1\<^sup>2 + y1\<^sup>2 + B1*x1 + B2*y1 + C)"
[PROOF STATE]
proof (prove)
using this:
x1\<^sup>2 + y1\<^sup>2 + B1 * x1 + B2 * y1 + C = 0

goal (1 subgoal):
 1. 0 = x1\<^sup>2 + y1\<^sup>2 + b1 * x1 + b2 * y1 + c - (x1\<^sup>2 + y1\<^sup>2 + B1 * x1 + B2 * y1 + C)
[PROOF STEP]
using \<open>x1\<^sup>2 + y1\<^sup>2 + b1*x1 + b2*y1 + c = 0\<close>
[PROOF STATE]
proof (prove)
using this:
x1\<^sup>2 + y1\<^sup>2 + B1 * x1 + B2 * y1 + C = 0
x1\<^sup>2 + y1\<^sup>2 + b1 * x1 + b2 * y1 + c = 0

goal (1 subgoal):
 1. 0 = x1\<^sup>2 + y1\<^sup>2 + b1 * x1 + b2 * y1 + c - (x1\<^sup>2 + y1\<^sup>2 + B1 * x1 + B2 * y1 + C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 = x1\<^sup>2 + y1\<^sup>2 + b1 * x1 + b2 * y1 + c - (x1\<^sup>2 + y1\<^sup>2 + B1 * x1 + B2 * y1 + C)

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
hence "0 = (b1 - B1)*x1 + (b2 - B2)*y1 + c - C"
[PROOF STATE]
proof (prove)
using this:
0 = x1\<^sup>2 + y1\<^sup>2 + b1 * x1 + b2 * y1 + c - (x1\<^sup>2 + y1\<^sup>2 + B1 * x1 + B2 * y1 + C)

goal (1 subgoal):
 1. 0 = (b1 - B1) * x1 + (b2 - B2) * y1 + c - C
[PROOF STEP]
by (simp  add:field_simps)
[PROOF STATE]
proof (state)
this:
0 = (b1 - B1) * x1 + (b2 - B2) * y1 + c - C

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "x2\<^sup>2 + y2\<^sup>2 + b1*x2 + b2*y2 + c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x2\<^sup>2 + y2\<^sup>2 + b1 * x2 + b2 * y2 + c = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
b2 \<noteq> B2 \<or> b1 \<noteq> B1
(b2 - B2)\<^sup>2 + (b1 - B1)\<^sup>2 \<noteq> 0
qf1 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 * x + b2 * y + c)
qf2 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 * x + B2 * y + C)
qf1 x1 y1 = 0
qf2 x1 y1 = 0
qf1 x2 y2 = 0
qf2 x2 y2 = 0
(x1, y1) \<noteq> (x2, y2)
qf1 x y = 0
qf2 x y = 0

goal (1 subgoal):
 1. x2\<^sup>2 + y2\<^sup>2 + b1 * x2 + b2 * y2 + c = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x2\<^sup>2 + y2\<^sup>2 + b1 * x2 + b2 * y2 + c = 0

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "x2\<^sup>2 + y2\<^sup>2 + B1*x2 + B2*y2 + C = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x2\<^sup>2 + y2\<^sup>2 + B1 * x2 + B2 * y2 + C = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
b2 \<noteq> B2 \<or> b1 \<noteq> B1
(b2 - B2)\<^sup>2 + (b1 - B1)\<^sup>2 \<noteq> 0
qf1 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 * x + b2 * y + c)
qf2 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 * x + B2 * y + C)
qf1 x1 y1 = 0
qf2 x1 y1 = 0
qf1 x2 y2 = 0
qf2 x2 y2 = 0
(x1, y1) \<noteq> (x2, y2)
qf1 x y = 0
qf2 x y = 0

goal (1 subgoal):
 1. x2\<^sup>2 + y2\<^sup>2 + B1 * x2 + B2 * y2 + C = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x2\<^sup>2 + y2\<^sup>2 + B1 * x2 + B2 * y2 + C = 0

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
hence "0 = x2\<^sup>2 + y2\<^sup>2 + b1*x2 + b2*y2 + c - (x2\<^sup>2 + y2\<^sup>2 + B1*x2 + B2*y2 + C)"
[PROOF STATE]
proof (prove)
using this:
x2\<^sup>2 + y2\<^sup>2 + B1 * x2 + B2 * y2 + C = 0

goal (1 subgoal):
 1. 0 = x2\<^sup>2 + y2\<^sup>2 + b1 * x2 + b2 * y2 + c - (x2\<^sup>2 + y2\<^sup>2 + B1 * x2 + B2 * y2 + C)
[PROOF STEP]
using \<open>x2\<^sup>2 + y2\<^sup>2 + b1*x2 + b2*y2 + c = 0\<close>
[PROOF STATE]
proof (prove)
using this:
x2\<^sup>2 + y2\<^sup>2 + B1 * x2 + B2 * y2 + C = 0
x2\<^sup>2 + y2\<^sup>2 + b1 * x2 + b2 * y2 + c = 0

goal (1 subgoal):
 1. 0 = x2\<^sup>2 + y2\<^sup>2 + b1 * x2 + b2 * y2 + c - (x2\<^sup>2 + y2\<^sup>2 + B1 * x2 + B2 * y2 + C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 = x2\<^sup>2 + y2\<^sup>2 + b1 * x2 + b2 * y2 + c - (x2\<^sup>2 + y2\<^sup>2 + B1 * x2 + B2 * y2 + C)

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
hence "0 = (b1 - B1)*x2 + (b2 - B2)*y2 + c - C"
[PROOF STATE]
proof (prove)
using this:
0 = x2\<^sup>2 + y2\<^sup>2 + b1 * x2 + b2 * y2 + c - (x2\<^sup>2 + y2\<^sup>2 + B1 * x2 + B2 * y2 + C)

goal (1 subgoal):
 1. 0 = (b1 - B1) * x2 + (b2 - B2) * y2 + c - C
[PROOF STEP]
by (simp  add:field_simps)
[PROOF STATE]
proof (state)
this:
0 = (b1 - B1) * x2 + (b2 - B2) * y2 + c - C

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "(b1 - B1, b2 - B2) \<noteq> (0, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b1 - B1, b2 - B2) \<noteq> (0, 0)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
b2 \<noteq> B2 \<or> b1 \<noteq> B1

goal (1 subgoal):
 1. (b1 - B1, b2 - B2) \<noteq> (0, 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(b1 - B1, b2 - B2) \<noteq> (0, 0)

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
let ?lf = "(\<lambda> x y. (b1 - B1)*x + (b2 - B2)*y + c - C)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "?lf x y = 0" "?lf x1 y1 = 0" "?lf x2 y2 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b1 - B1) * x + (b2 - B2) * y + c - C = 0 &&& (b1 - B1) * x1 + (b2 - B2) * y1 + c - C = 0 &&& (b1 - B1) * x2 + (b2 - B2) * y2 + c - C = 0
[PROOF STEP]
using \<open>0 = (b1 - B1)*x2 + (b2 - B2)*y2 + c - C\<close>
          \<open>0 = (b1 - B1)*x1 + (b2 - B2)*y1 + c - C\<close>
          \<open>0 = (b1 - B1)*x + (b2 - B2)*y + c - C\<close>
[PROOF STATE]
proof (prove)
using this:
0 = (b1 - B1) * x2 + (b2 - B2) * y2 + c - C
0 = (b1 - B1) * x1 + (b2 - B2) * y1 + c - C
0 = (b1 - B1) * x + (b2 - B2) * y + c - C

goal (1 subgoal):
 1. (b1 - B1) * x + (b2 - B2) * y + c - C = 0 &&& (b1 - B1) * x1 + (b2 - B2) * y1 + c - C = 0 &&& (b1 - B1) * x2 + (b2 - B2) * y2 + c - C = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(b1 - B1) * x + (b2 - B2) * y + c - C = 0
(b1 - B1) * x1 + (b2 - B2) * y1 + c - C = 0
(b1 - B1) * x2 + (b2 - B2) * y2 + c - C = 0

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(b1 - B1) * x + (b2 - B2) * y + c - C = 0
(b1 - B1) * x1 + (b2 - B2) * y1 + c - C = 0
(b1 - B1) * x2 + (b2 - B2) * y2 + c - C = 0

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
using quadratic_linear_at_most_2_intersections[of 1 0 1 "b1 - B1" "b2 - B2" qf1 b1 b2 c ?lf "c - C" x1 y1 x2 y2 x y]
[PROOF STATE]
proof (prove)
using this:
(b1 - B1) * x + (b2 - B2) * y + c - C = 0
(b1 - B1) * x1 + (b2 - B2) * y1 + c - C = 0
(b1 - B1) * x2 + (b2 - B2) * y2 + c - C = 0
\<lbrakk>(1, 0, 1) \<noteq> (0, 0, 0); (b1 - B1, b2 - B2) \<noteq> (0, 0); 1 * (b2 - B2)\<^sup>2 - 2 * 0 * (b1 - B1) * (b2 - B2) + 1 * (b1 - B1)\<^sup>2 \<noteq> 0; qf1 = (\<lambda>x y. 1 * x\<^sup>2 + 2 * 0 * x * y + 1 * y\<^sup>2 + b1 * x + b2 * y + c); (\<lambda>x y. (b1 - B1) * x + (b2 - B2) * y + c - C) = (\<lambda>x y. (b1 - B1) * x + (b2 - B2) * y + (c - C)); qf1 x1 y1 = 0; (b1 - B1) * x1 + (b2 - B2) * y1 + c - C = 0; qf1 x2 y2 = 0; (b1 - B1) * x2 + (b2 - B2) * y2 + c - C = 0; (x1, y1) \<noteq> (x2, y2); qf1 x y = 0; (b1 - B1) * x + (b2 - B2) * y + c - C = 0\<rbrakk> \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
using \<open>(b1 - B1, b2 - B2) \<noteq> (0, 0)\<close>
[PROOF STATE]
proof (prove)
using this:
(b1 - B1) * x + (b2 - B2) * y + c - C = 0
(b1 - B1) * x1 + (b2 - B2) * y1 + c - C = 0
(b1 - B1) * x2 + (b2 - B2) * y2 + c - C = 0
\<lbrakk>(1, 0, 1) \<noteq> (0, 0, 0); (b1 - B1, b2 - B2) \<noteq> (0, 0); 1 * (b2 - B2)\<^sup>2 - 2 * 0 * (b1 - B1) * (b2 - B2) + 1 * (b1 - B1)\<^sup>2 \<noteq> 0; qf1 = (\<lambda>x y. 1 * x\<^sup>2 + 2 * 0 * x * y + 1 * y\<^sup>2 + b1 * x + b2 * y + c); (\<lambda>x y. (b1 - B1) * x + (b2 - B2) * y + c - C) = (\<lambda>x y. (b1 - B1) * x + (b2 - B2) * y + (c - C)); qf1 x1 y1 = 0; (b1 - B1) * x1 + (b2 - B2) * y1 + c - C = 0; qf1 x2 y2 = 0; (b1 - B1) * x2 + (b2 - B2) * y2 + c - C = 0; (x1, y1) \<noteq> (x2, y2); qf1 x y = 0; (b1 - B1) * x + (b2 - B2) * y + c - C = 0\<rbrakk> \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
(b1 - B1, b2 - B2) \<noteq> (0, 0)

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
using assms \<open>(b1 - B1, b2 - B2) \<noteq> (0, 0)\<close>
[PROOF STATE]
proof (prove)
using this:
(b1 - B1) * x + (b2 - B2) * y + c - C = 0
(b1 - B1) * x1 + (b2 - B2) * y1 + c - C = 0
(b1 - B1) * x2 + (b2 - B2) * y2 + c - C = 0
\<lbrakk>(1, 0, 1) \<noteq> (0, 0, 0); (b1 - B1, b2 - B2) \<noteq> (0, 0); 1 * (b2 - B2)\<^sup>2 - 2 * 0 * (b1 - B1) * (b2 - B2) + 1 * (b1 - B1)\<^sup>2 \<noteq> 0; qf1 = (\<lambda>x y. 1 * x\<^sup>2 + 2 * 0 * x * y + 1 * y\<^sup>2 + b1 * x + b2 * y + c); (\<lambda>x y. (b1 - B1) * x + (b2 - B2) * y + c - C) = (\<lambda>x y. (b1 - B1) * x + (b2 - B2) * y + (c - C)); qf1 x1 y1 = 0; (b1 - B1) * x1 + (b2 - B2) * y1 + c - C = 0; qf1 x2 y2 = 0; (b1 - B1) * x2 + (b2 - B2) * y2 + c - C = 0; (x1, y1) \<noteq> (x2, y2); qf1 x y = 0; (b1 - B1) * x + (b2 - B2) * y + c - C = 0\<rbrakk> \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
(b1 - B1, b2 - B2) \<noteq> (0, 0)
b2 \<noteq> B2 \<or> b1 \<noteq> B1
(b2 - B2)\<^sup>2 + (b1 - B1)\<^sup>2 \<noteq> 0
qf1 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 * x + b2 * y + c)
qf2 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 * x + B2 * y + C)
qf1 x1 y1 = 0
qf2 x1 y1 = 0
qf1 x2 y2 = 0
qf2 x2 y2 = 0
(x1, y1) \<noteq> (x2, y2)
qf1 x y = 0
qf2 x y = 0
(b1 - B1, b2 - B2) \<noteq> (0, 0)

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
using \<open>(b1 - B1) * x + (b2 - B2) * y + c - C = 0\<close> \<open>(b1 - B1) * x1 + (b2 - B2) * y1 + c - C = 0\<close>
[PROOF STATE]
proof (prove)
using this:
(b1 - B1) * x + (b2 - B2) * y + c - C = 0
(b1 - B1) * x1 + (b2 - B2) * y1 + c - C = 0
(b1 - B1) * x2 + (b2 - B2) * y2 + c - C = 0
\<lbrakk>(1, 0, 1) \<noteq> (0, 0, 0); (b1 - B1, b2 - B2) \<noteq> (0, 0); 1 * (b2 - B2)\<^sup>2 - 2 * 0 * (b1 - B1) * (b2 - B2) + 1 * (b1 - B1)\<^sup>2 \<noteq> 0; qf1 = (\<lambda>x y. 1 * x\<^sup>2 + 2 * 0 * x * y + 1 * y\<^sup>2 + b1 * x + b2 * y + c); (\<lambda>x y. (b1 - B1) * x + (b2 - B2) * y + c - C) = (\<lambda>x y. (b1 - B1) * x + (b2 - B2) * y + (c - C)); qf1 x1 y1 = 0; (b1 - B1) * x1 + (b2 - B2) * y1 + c - C = 0; qf1 x2 y2 = 0; (b1 - B1) * x2 + (b2 - B2) * y2 + c - C = 0; (x1, y1) \<noteq> (x2, y2); qf1 x y = 0; (b1 - B1) * x + (b2 - B2) * y + c - C = 0\<rbrakk> \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
(b1 - B1, b2 - B2) \<noteq> (0, 0)
b2 \<noteq> B2 \<or> b1 \<noteq> B1
(b2 - B2)\<^sup>2 + (b1 - B1)\<^sup>2 \<noteq> 0
qf1 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 * x + b2 * y + c)
qf2 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 * x + B2 * y + C)
qf1 x1 y1 = 0
qf2 x1 y1 = 0
qf1 x2 y2 = 0
qf2 x2 y2 = 0
(x1, y1) \<noteq> (x2, y2)
qf1 x y = 0
qf2 x y = 0
(b1 - B1, b2 - B2) \<noteq> (0, 0)
(b1 - B1) * x + (b2 - B2) * y + c - C = 0
(b1 - B1) * x1 + (b2 - B2) * y1 + c - C = 0

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
by (simp add: add_diff_eq)
[PROOF STATE]
proof (state)
this:
(x, y) = (x1, y1) \<or> (x, y) = (x2, y2)

goal:
No subgoals!
[PROOF STEP]
qed