[STATEMENT]
lemma complex_vector_affinity_eq:
  fixes x :: "'a :: complex_vector"
  assumes m0: "m \<noteq> 0"
  shows "m *\<^sub>C x + c = y \<longleftrightarrow> x = inverse m *\<^sub>C y - (inverse m *\<^sub>C c)"
    (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (m *\<^sub>C x + c = y) = (x = y /\<^sub>C m - c /\<^sub>C m)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m *\<^sub>C x + c = y \<Longrightarrow> x = y /\<^sub>C m - c /\<^sub>C m
 2. x = y /\<^sub>C m - c /\<^sub>C m \<Longrightarrow> m *\<^sub>C x + c = y
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
m *\<^sub>C x + c = y

goal (2 subgoals):
 1. m *\<^sub>C x + c = y \<Longrightarrow> x = y /\<^sub>C m - c /\<^sub>C m
 2. x = y /\<^sub>C m - c /\<^sub>C m \<Longrightarrow> m *\<^sub>C x + c = y
[PROOF STEP]
hence "m *\<^sub>C x = y - c"
[PROOF STATE]
proof (prove)
using this:
m *\<^sub>C x + c = y

goal (1 subgoal):
 1. m *\<^sub>C x = y - c
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
m *\<^sub>C x = y - c

goal (2 subgoals):
 1. m *\<^sub>C x + c = y \<Longrightarrow> x = y /\<^sub>C m - c /\<^sub>C m
 2. x = y /\<^sub>C m - c /\<^sub>C m \<Longrightarrow> m *\<^sub>C x + c = y
[PROOF STEP]
hence "inverse m *\<^sub>C (m *\<^sub>C x) = inverse m *\<^sub>C (y - c)"
[PROOF STATE]
proof (prove)
using this:
m *\<^sub>C x = y - c

goal (1 subgoal):
 1. m *\<^sub>C x /\<^sub>C m = (y - c) /\<^sub>C m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m *\<^sub>C x /\<^sub>C m = (y - c) /\<^sub>C m

goal (2 subgoals):
 1. m *\<^sub>C x + c = y \<Longrightarrow> x = y /\<^sub>C m - c /\<^sub>C m
 2. x = y /\<^sub>C m - c /\<^sub>C m \<Longrightarrow> m *\<^sub>C x + c = y
[PROOF STEP]
thus "x = inverse m *\<^sub>C y - (inverse m *\<^sub>C c)"
[PROOF STATE]
proof (prove)
using this:
m *\<^sub>C x /\<^sub>C m = (y - c) /\<^sub>C m

goal (1 subgoal):
 1. x = y /\<^sub>C m - c /\<^sub>C m
[PROOF STEP]
using m0
[PROOF STATE]
proof (prove)
using this:
m *\<^sub>C x /\<^sub>C m = (y - c) /\<^sub>C m
m \<noteq> 0

goal (1 subgoal):
 1. x = y /\<^sub>C m - c /\<^sub>C m
[PROOF STEP]
by (simp add: complex_vector.scale_right_diff_distrib)
[PROOF STATE]
proof (state)
this:
x = y /\<^sub>C m - c /\<^sub>C m

goal (1 subgoal):
 1. x = y /\<^sub>C m - c /\<^sub>C m \<Longrightarrow> m *\<^sub>C x + c = y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = y /\<^sub>C m - c /\<^sub>C m \<Longrightarrow> m *\<^sub>C x + c = y
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
x = y /\<^sub>C m - c /\<^sub>C m

goal (1 subgoal):
 1. x = y /\<^sub>C m - c /\<^sub>C m \<Longrightarrow> m *\<^sub>C x + c = y
[PROOF STEP]
with m0
[PROOF STATE]
proof (chain)
picking this:
m \<noteq> 0
x = y /\<^sub>C m - c /\<^sub>C m
[PROOF STEP]
show "m *\<^sub>C x + c = y"
[PROOF STATE]
proof (prove)
using this:
m \<noteq> 0
x = y /\<^sub>C m - c /\<^sub>C m

goal (1 subgoal):
 1. m *\<^sub>C x + c = y
[PROOF STEP]
by (simp add: complex_vector.scale_right_diff_distrib)
[PROOF STATE]
proof (state)
this:
m *\<^sub>C x + c = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complex_vector_eq_affinity: "m \<noteq> 0 \<Longrightarrow> y = m *\<^sub>C x + c \<longleftrightarrow> inverse m *\<^sub>C y - (inverse m *\<^sub>C c) = x"
  for x :: "'a::complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> (y = m *\<^sub>C x + c) = (y /\<^sub>C m - c /\<^sub>C m = x)
[PROOF STEP]
using complex_vector_affinity_eq[where m=m and x=x and y=y and c=c]
[PROOF STATE]
proof (prove)
using this:
m \<noteq> 0 \<Longrightarrow> (m *\<^sub>C x + c = y) = (x = y /\<^sub>C m - c /\<^sub>C m)

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> (y = m *\<^sub>C x + c) = (y /\<^sub>C m - c /\<^sub>C m = x)
[PROOF STEP]
by metis


[STATEMENT]
lemma scaleC_eq_iff [simp]: "b + u *\<^sub>C a = a + u *\<^sub>C b \<longleftrightarrow> a = b \<or> u = 1"
  for a :: "'a::complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b + u *\<^sub>C a = a + u *\<^sub>C b) = (a = b \<or> u = 1)
[PROOF STEP]
proof (cases "u = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = 1 \<Longrightarrow> (b + u *\<^sub>C a = a + u *\<^sub>C b) = (a = b \<or> u = 1)
 2. u \<noteq> 1 \<Longrightarrow> (b + u *\<^sub>C a = a + u *\<^sub>C b) = (a = b \<or> u = 1)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
u = 1

goal (2 subgoals):
 1. u = 1 \<Longrightarrow> (b + u *\<^sub>C a = a + u *\<^sub>C b) = (a = b \<or> u = 1)
 2. u \<noteq> 1 \<Longrightarrow> (b + u *\<^sub>C a = a + u *\<^sub>C b) = (a = b \<or> u = 1)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
u = 1

goal (1 subgoal):
 1. (b + u *\<^sub>C a = a + u *\<^sub>C b) = (a = b \<or> u = 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(b + u *\<^sub>C a = a + u *\<^sub>C b) = (a = b \<or> u = 1)

goal (1 subgoal):
 1. u \<noteq> 1 \<Longrightarrow> (b + u *\<^sub>C a = a + u *\<^sub>C b) = (a = b \<or> u = 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<noteq> 1 \<Longrightarrow> (b + u *\<^sub>C a = a + u *\<^sub>C b) = (a = b \<or> u = 1)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
u \<noteq> 1

goal (1 subgoal):
 1. u \<noteq> 1 \<Longrightarrow> (b + u *\<^sub>C a = a + u *\<^sub>C b) = (a = b \<or> u = 1)
[PROOF STEP]
have "a = b" if "b + u *\<^sub>C a = a + u *\<^sub>C b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
b + u *\<^sub>C a = a + u *\<^sub>C b
[PROOF STEP]
have "(u - 1) *\<^sub>C a = (u - 1) *\<^sub>C b"
[PROOF STATE]
proof (prove)
using this:
b + u *\<^sub>C a = a + u *\<^sub>C b

goal (1 subgoal):
 1. (u - 1) *\<^sub>C a = (u - 1) *\<^sub>C b
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
(u - 1) *\<^sub>C a = (u - 1) *\<^sub>C b

goal (1 subgoal):
 1. a = b
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
u \<noteq> 1
(u - 1) *\<^sub>C a = (u - 1) *\<^sub>C b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<noteq> 1
(u - 1) *\<^sub>C a = (u - 1) *\<^sub>C b

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
b + u *\<^sub>C a = a + u *\<^sub>C b \<Longrightarrow> a = b

goal (1 subgoal):
 1. u \<noteq> 1 \<Longrightarrow> (b + u *\<^sub>C a = a + u *\<^sub>C b) = (a = b \<or> u = 1)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
b + u *\<^sub>C a = a + u *\<^sub>C b \<Longrightarrow> a = b

goal (1 subgoal):
 1. (b + u *\<^sub>C a = a + u *\<^sub>C b) = (a = b \<or> u = 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(b + u *\<^sub>C a = a + u *\<^sub>C b) = (a = b \<or> u = 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scaleC_collapse [simp]: "(1 - u) *\<^sub>C a + u *\<^sub>C a = a"
  for a :: "'a::complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - u) *\<^sub>C a + u *\<^sub>C a = a
[PROOF STEP]
by (simp add: algebra_simps)


[STATEMENT]
lemma scaleC_conv_of_complex: "scaleC r x = of_complex r * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r *\<^sub>C x = of_complex r * x
[PROOF STEP]
by (simp add: of_complex_def)


[STATEMENT]
lemma of_complex_0 [simp]: "of_complex 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex 0 = (0::'a)
[PROOF STEP]
by (simp add: of_complex_def)


[STATEMENT]
lemma of_complex_1 [simp]: "of_complex 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex 1 = (1::'a)
[PROOF STEP]
by (simp add: of_complex_def)


[STATEMENT]
lemma of_complex_add [simp]: "of_complex (x + y) = of_complex x + of_complex y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (x + y) = of_complex x + of_complex y
[PROOF STEP]
by (simp add: of_complex_def scaleC_add_left)


[STATEMENT]
lemma of_complex_minus [simp]: "of_complex (- x) = - of_complex x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (- x) = - of_complex x
[PROOF STEP]
by (simp add: of_complex_def)


[STATEMENT]
lemma of_complex_diff [simp]: "of_complex (x - y) = of_complex x - of_complex y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (x - y) = of_complex x - of_complex y
[PROOF STEP]
by (simp add: of_complex_def scaleC_diff_left)


[STATEMENT]
lemma of_complex_sum[simp]: "of_complex (sum f s) = (\<Sum>x\<in>s. of_complex (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (sum f s) = (\<Sum>x\<in>s. of_complex (f x))
[PROOF STEP]
by (induct s rule: infinite_finite_induct) auto


[STATEMENT]
lemma of_complex_prod[simp]: "of_complex (prod f s) = (\<Prod>x\<in>s. of_complex (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (prod f s) = (\<Prod>x\<in>s. of_complex (f x))
[PROOF STEP]
by (induct s rule: infinite_finite_induct) auto


[STATEMENT]
lemma nonzero_of_complex_inverse:
  "x \<noteq> 0 \<Longrightarrow> of_complex (inverse x) = inverse (of_complex x :: 'a::complex_div_algebra)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> of_complex (inverse x) = inverse (of_complex x)
[PROOF STEP]
by (simp add: of_complex_def nonzero_inverse_scaleC_distrib)


[STATEMENT]
lemma of_complex_inverse [simp]:
  "of_complex (inverse x) = inverse (of_complex x :: 'a::{complex_div_algebra,division_ring})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (inverse x) = inverse (of_complex x)
[PROOF STEP]
by (simp add: of_complex_def inverse_scaleC_distrib)


[STATEMENT]
lemma nonzero_of_complex_divide:
  "y \<noteq> 0 \<Longrightarrow> of_complex (x / y) = (of_complex x / of_complex y :: 'a::complex_field)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<noteq> 0 \<Longrightarrow> of_complex (x / y) = of_complex x / of_complex y
[PROOF STEP]
by (simp add: divide_inverse nonzero_of_complex_inverse)


[STATEMENT]
lemma of_complex_divide [simp]:
  "of_complex (x / y) = (of_complex x / of_complex y :: 'a::complex_div_algebra)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (x / y) = of_complex x / of_complex y
[PROOF STEP]
by (simp add: divide_inverse)


[STATEMENT]
lemma of_complex_power [simp]:
  "of_complex (x ^ n) = (of_complex x :: 'a::{complex_algebra_1}) ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (x ^ n) = of_complex x ^ n
[PROOF STEP]
by (induct n) simp_all


[STATEMENT]
lemma of_complex_power_int [simp]:
  "of_complex (power_int x n) = power_int (of_complex x :: 'a :: {complex_div_algebra,division_ring}) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (x powi n) = of_complex x powi n
[PROOF STEP]
by (auto simp: power_int_def)


[STATEMENT]
lemma of_complex_eq_iff [simp]: "of_complex x = of_complex y \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_complex x = of_complex y) = (x = y)
[PROOF STEP]
by (simp add: of_complex_def)


[STATEMENT]
lemma inj_of_complex: "inj of_complex"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj of_complex
[PROOF STEP]
by (auto intro: injI)


[STATEMENT]
lemma minus_of_complex_eq_of_complex_iff [simp]: "-of_complex x = of_complex y \<longleftrightarrow> -x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- of_complex x = of_complex y) = (- x = y)
[PROOF STEP]
using of_complex_eq_iff[of "-x" y]
[PROOF STATE]
proof (prove)
using this:
(of_complex (- x) = of_complex y) = (- x = y)

goal (1 subgoal):
 1. (- of_complex x = of_complex y) = (- x = y)
[PROOF STEP]
by (simp only: of_complex_minus)


[STATEMENT]
lemma of_complex_eq_minus_of_complex_iff [simp]: "of_complex x = -of_complex y \<longleftrightarrow> x = -y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_complex x = - of_complex y) = (x = - y)
[PROOF STEP]
using of_complex_eq_iff[of x "-y"]
[PROOF STATE]
proof (prove)
using this:
(of_complex x = of_complex (- y)) = (x = - y)

goal (1 subgoal):
 1. (of_complex x = - of_complex y) = (x = - y)
[PROOF STEP]
by (simp only: of_complex_minus)


[STATEMENT]
lemma of_complex_eq_id [simp]: "of_complex = (id :: complex \<Rightarrow> complex)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex = id
[PROOF STEP]
by (rule ext) (simp add: of_complex_def)


[STATEMENT]
lemma of_complex_of_nat_eq [simp]: "of_complex (of_nat n) = of_nat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (of_nat n) = of_nat n
[PROOF STEP]
by (induct n) auto


[STATEMENT]
lemma of_complex_of_int_eq [simp]: "of_complex (of_int z) = of_int z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (of_int z) = of_int z
[PROOF STEP]
by (cases z rule: int_diff_cases) simp


[STATEMENT]
lemma of_complex_numeral [simp]: "of_complex (numeral w) = numeral w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (numeral w) = numeral w
[PROOF STEP]
using of_complex_of_int_eq [of "numeral w"]
[PROOF STATE]
proof (prove)
using this:
of_complex (of_int (numeral w)) = of_int (numeral w)

goal (1 subgoal):
 1. of_complex (numeral w) = numeral w
[PROOF STEP]
by simp


[STATEMENT]
lemma of_complex_neg_numeral [simp]: "of_complex (- numeral w) = - numeral w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (- numeral w) = - numeral w
[PROOF STEP]
using of_complex_of_int_eq [of "- numeral w"]
[PROOF STATE]
proof (prove)
using this:
of_complex (of_int (- numeral w)) = of_int (- numeral w)

goal (1 subgoal):
 1. of_complex (- numeral w) = - numeral w
[PROOF STEP]
by simp


[STATEMENT]
lemma of_complex_eq_numeral_power_int_cancel_iff [simp]:
  "(of_complex y :: 'a :: {complex_div_algebra, division_ring}) = power_int (numeral x) n \<longleftrightarrow>
     y = power_int (numeral x) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_complex y = numeral x powi n) = (y = numeral x powi n)
[PROOF STEP]
by (subst (1 2) eq_commute) simp


[STATEMENT]
lemma of_complex_eq_of_complex_power_int_cancel_iff [simp]:
  "power_int (of_complex b :: 'a :: {complex_div_algebra, division_ring}) w = of_complex x \<longleftrightarrow>
     power_int b w = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_complex b powi w = of_complex x) = (b powi w = x)
[PROOF STEP]
by (metis of_complex_power_int of_complex_eq_iff)


[STATEMENT]
lemma of_complex_in_Ints_iff [simp]: "of_complex x \<in> \<int> \<longleftrightarrow> x \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_complex x \<in> \<int>) = (x \<in> \<int>)
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. of_complex x \<in> \<int> \<Longrightarrow> x \<in> \<int>
 2. x \<in> \<int> \<Longrightarrow> of_complex x \<in> \<int>
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. of_complex x \<in> \<int> \<Longrightarrow> x \<in> \<int>
 2. x \<in> \<int> \<Longrightarrow> of_complex x \<in> \<int>
[PROOF STEP]
assume "(of_complex x :: 'a) \<in> \<int>"
[PROOF STATE]
proof (state)
this:
of_complex x \<in> \<int>

goal (2 subgoals):
 1. of_complex x \<in> \<int> \<Longrightarrow> x \<in> \<int>
 2. x \<in> \<int> \<Longrightarrow> of_complex x \<in> \<int>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
of_complex x \<in> \<int>
[PROOF STEP]
obtain n where "(of_complex x :: 'a) = of_int n"
[PROOF STATE]
proof (prove)
using this:
of_complex x \<in> \<int>

goal (1 subgoal):
 1. (\<And>n. of_complex x = of_int n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: Ints_def)
[PROOF STATE]
proof (state)
this:
of_complex x = of_int n

goal (2 subgoals):
 1. of_complex x \<in> \<int> \<Longrightarrow> x \<in> \<int>
 2. x \<in> \<int> \<Longrightarrow> of_complex x \<in> \<int>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_complex x = of_int n

goal (2 subgoals):
 1. of_complex x \<in> \<int> \<Longrightarrow> x \<in> \<int>
 2. x \<in> \<int> \<Longrightarrow> of_complex x \<in> \<int>
[PROOF STEP]
have "of_int n = of_complex (of_int n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int n = of_complex (of_int n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
of_int n = of_complex (of_int n)

goal (2 subgoals):
 1. of_complex x \<in> \<int> \<Longrightarrow> x \<in> \<int>
 2. x \<in> \<int> \<Longrightarrow> of_complex x \<in> \<int>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
of_complex x = of_complex (of_int n)
[PROOF STEP]
have "x = of_int n"
[PROOF STATE]
proof (prove)
using this:
of_complex x = of_complex (of_int n)

goal (1 subgoal):
 1. x = of_int n
[PROOF STEP]
by (subst (asm) of_complex_eq_iff)
[PROOF STATE]
proof (state)
this:
x = of_int n

goal (2 subgoals):
 1. of_complex x \<in> \<int> \<Longrightarrow> x \<in> \<int>
 2. x \<in> \<int> \<Longrightarrow> of_complex x \<in> \<int>
[PROOF STEP]
thus "x \<in> \<int>"
[PROOF STATE]
proof (prove)
using this:
x = of_int n

goal (1 subgoal):
 1. x \<in> \<int>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> \<int>

goal (1 subgoal):
 1. x \<in> \<int> \<Longrightarrow> of_complex x \<in> \<int>
[PROOF STEP]
qed (auto simp: Ints_def)


[STATEMENT]
lemma Ints_of_complex [intro]: "x \<in> \<int> \<Longrightarrow> of_complex x \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<int> \<Longrightarrow> of_complex x \<in> \<int>
[PROOF STEP]
by simp


[STATEMENT]
lemma fraction_scaleC_times [simp]:
  fixes a :: "'a::complex_algebra_1"
  shows "(numeral u / numeral v) *\<^sub>C (numeral w * a) = (numeral u * numeral w / numeral v) *\<^sub>C a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (numeral u / numeral v) *\<^sub>C (numeral w * a) = (numeral u * numeral w / numeral v) *\<^sub>C a
[PROOF STEP]
by (metis (no_types, lifting) of_complex_numeral scaleC_conv_of_complex scaleC_scaleC times_divide_eq_left)


[STATEMENT]
lemma inverse_scaleC_times [simp]:
  fixes a :: "'a::complex_algebra_1"
  shows "(1 / numeral v) *\<^sub>C (numeral w * a) = (numeral w / numeral v) *\<^sub>C a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 / numeral v) *\<^sub>C (numeral w * a) = (numeral w / numeral v) *\<^sub>C a
[PROOF STEP]
by (metis divide_inverse_commute inverse_eq_divide of_complex_numeral scaleC_conv_of_complex scaleC_scaleC)


[STATEMENT]
lemma scaleC_times [simp]:
  fixes a :: "'a::complex_algebra_1"
  shows "(numeral u) *\<^sub>C (numeral w * a) = (numeral u * numeral w) *\<^sub>C a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. numeral u *\<^sub>C (numeral w * a) = (numeral u * numeral w) *\<^sub>C a
[PROOF STEP]
by (simp add: scaleC_conv_of_complex)


[STATEMENT]
lemma Complexs_of_complex [simp]: "of_complex r \<in> \<complex>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex r \<in> \<complex>
[PROOF STEP]
by (simp add: Complexs_def)


[STATEMENT]
lemma Complexs_of_int [simp]: "of_int z \<in> \<complex>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int z \<in> \<complex>
[PROOF STEP]
by (subst of_complex_of_int_eq [symmetric], rule Complexs_of_complex)


[STATEMENT]
lemma Complexs_of_nat [simp]: "of_nat n \<in> \<complex>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat n \<in> \<complex>
[PROOF STEP]
by (subst of_complex_of_nat_eq [symmetric], rule Complexs_of_complex)


[STATEMENT]
lemma Complexs_numeral [simp]: "numeral w \<in> \<complex>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. numeral w \<in> \<complex>
[PROOF STEP]
by (subst of_complex_numeral [symmetric], rule Complexs_of_complex)


[STATEMENT]
lemma Complexs_0 [simp]: "0 \<in> \<complex>" and Complexs_1 [simp]: "1 \<in> \<complex>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<in> \<complex> &&& (1::'b) \<in> \<complex>
[PROOF STEP]
by (simp_all add: Complexs_def)


[STATEMENT]
lemma Complexs_add [simp]: "a \<in> \<complex> \<Longrightarrow> b \<in> \<complex> \<Longrightarrow> a + b \<in> \<complex>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> \<complex>; b \<in> \<complex>\<rbrakk> \<Longrightarrow> a + b \<in> \<complex>
[PROOF STEP]
apply (auto simp add: Complexs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>a = of_complex x; b = of_complex xa\<rbrakk> \<Longrightarrow> of_complex x + of_complex xa \<in> range of_complex
[PROOF STEP]
by (metis of_complex_add range_eqI)


[STATEMENT]
lemma Complexs_minus [simp]: "a \<in> \<complex> \<Longrightarrow> - a \<in> \<complex>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> \<complex> \<Longrightarrow> - a \<in> \<complex>
[PROOF STEP]
by (auto simp: Complexs_def)


[STATEMENT]
lemma Complexs_minus_iff [simp]: "- a \<in> \<complex> \<longleftrightarrow> a \<in> \<complex>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- a \<in> \<complex>) = (a \<in> \<complex>)
[PROOF STEP]
using Complexs_minus
[PROOF STATE]
proof (prove)
using this:
?a \<in> \<complex> \<Longrightarrow> - ?a \<in> \<complex>

goal (1 subgoal):
 1. (- a \<in> \<complex>) = (a \<in> \<complex>)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma Complexs_diff [simp]: "a \<in> \<complex> \<Longrightarrow> b \<in> \<complex> \<Longrightarrow> a - b \<in> \<complex>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> \<complex>; b \<in> \<complex>\<rbrakk> \<Longrightarrow> a - b \<in> \<complex>
[PROOF STEP]
by (metis Complexs_add Complexs_minus_iff add_uminus_conv_diff)


[STATEMENT]
lemma Complexs_mult [simp]: "a \<in> \<complex> \<Longrightarrow> b \<in> \<complex> \<Longrightarrow> a * b \<in> \<complex>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> \<complex>; b \<in> \<complex>\<rbrakk> \<Longrightarrow> a * b \<in> \<complex>
[PROOF STEP]
apply (auto simp add: Complexs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>a = of_complex x; b = of_complex xa\<rbrakk> \<Longrightarrow> of_complex x * of_complex xa \<in> range of_complex
[PROOF STEP]
by (metis of_complex_mult rangeI)


[STATEMENT]
lemma Complexs_inverse: "a \<in> \<complex> \<Longrightarrow> inverse a \<in> \<complex>"
  for a :: "'a::{complex_div_algebra,division_ring}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> \<complex> \<Longrightarrow> inverse a \<in> \<complex>
[PROOF STEP]
using nonzero_Complexs_inverse
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<in> \<complex>; ?a \<noteq> (0::?'a)\<rbrakk> \<Longrightarrow> inverse ?a \<in> \<complex>

goal (1 subgoal):
 1. a \<in> \<complex> \<Longrightarrow> inverse a \<in> \<complex>
[PROOF STEP]
by fastforce


[STATEMENT]
lemma Complexs_inverse_iff [simp]: "inverse x \<in> \<complex> \<longleftrightarrow> x \<in> \<complex>"
  for x :: "'a::{complex_div_algebra,division_ring}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inverse x \<in> \<complex>) = (x \<in> \<complex>)
[PROOF STEP]
by (metis Complexs_inverse inverse_inverse_eq)


[STATEMENT]
lemma nonzero_Complexs_divide: "a \<in> \<complex> \<Longrightarrow> b \<in> \<complex> \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a / b \<in> \<complex>"
  for a b :: "'a::complex_field"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> \<complex>; b \<in> \<complex>; b \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> a / b \<in> \<complex>
[PROOF STEP]
by (simp add: divide_inverse)


[STATEMENT]
lemma Complexs_divide [simp]: "a \<in> \<complex> \<Longrightarrow> b \<in> \<complex> \<Longrightarrow> a / b \<in> \<complex>"
  for a b :: "'a::{complex_field,field}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> \<complex>; b \<in> \<complex>\<rbrakk> \<Longrightarrow> a / b \<in> \<complex>
[PROOF STEP]
using nonzero_Complexs_divide
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<in> \<complex>; ?b \<in> \<complex>; ?b \<noteq> (0::?'a)\<rbrakk> \<Longrightarrow> ?a / ?b \<in> \<complex>

goal (1 subgoal):
 1. \<lbrakk>a \<in> \<complex>; b \<in> \<complex>\<rbrakk> \<Longrightarrow> a / b \<in> \<complex>
[PROOF STEP]
by fastforce


[STATEMENT]
lemma Complexs_power [simp]: "a \<in> \<complex> \<Longrightarrow> a ^ n \<in> \<complex>"
  for a :: "'a::complex_algebra_1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> \<complex> \<Longrightarrow> a ^ n \<in> \<complex>
[PROOF STEP]
apply (auto simp add: Complexs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. a = of_complex x \<Longrightarrow> of_complex x ^ n \<in> range of_complex
[PROOF STEP]
by (metis range_eqI of_complex_power[symmetric])


[STATEMENT]
lemma Complexs_cases [cases set: Complexs]:
  assumes "q \<in> \<complex>"
  obtains (of_complex) c where "q = of_complex c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. q = of_complex c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Complexs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. q = of_complex c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c. q = of_complex c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>q \<in> \<complex>\<close>
[PROOF STATE]
proof (chain)
picking this:
q \<in> \<complex>
[PROOF STEP]
have "q \<in> range of_complex"
[PROOF STATE]
proof (prove)
using this:
q \<in> \<complex>

goal (1 subgoal):
 1. q \<in> range of_complex
[PROOF STEP]
unfolding Complexs_def
[PROOF STATE]
proof (prove)
using this:
q \<in> range of_complex

goal (1 subgoal):
 1. q \<in> range of_complex
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
q \<in> range of_complex

goal (1 subgoal):
 1. (\<And>c. q = of_complex c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> range of_complex
[PROOF STEP]
obtain c where "q = of_complex c"
[PROOF STATE]
proof (prove)
using this:
q \<in> range of_complex

goal (1 subgoal):
 1. (\<And>c. q = of_complex c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
q = of_complex c

goal (1 subgoal):
 1. (\<And>c. q = of_complex c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q = of_complex c
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
q = of_complex c

goal (1 subgoal):
 1. thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_in_Complexs [intro,simp]: "(\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<complex>) \<Longrightarrow> sum f s \<in> \<complex>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<complex>) \<Longrightarrow> sum f s \<in> \<complex>
[PROOF STEP]
proof (induct s rule: infinite_finite_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>i. i \<in> A \<Longrightarrow> f i \<in> \<complex>\<rbrakk> \<Longrightarrow> sum f A \<in> \<complex>
 2. (\<And>i. i \<in> {} \<Longrightarrow> f i \<in> \<complex>) \<Longrightarrow> sum f {} \<in> \<complex>
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>i. i \<in> F \<Longrightarrow> f i \<in> \<complex>) \<Longrightarrow> sum f F \<in> \<complex>; \<And>i. i \<in> insert x F \<Longrightarrow> f i \<in> \<complex>\<rbrakk> \<Longrightarrow> sum f (insert x F) \<in> \<complex>
[PROOF STEP]
case infinite
[PROOF STATE]
proof (state)
this:
infinite A_
?i \<in> A_ \<Longrightarrow> f ?i \<in> \<complex>

goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>i. i \<in> A \<Longrightarrow> f i \<in> \<complex>\<rbrakk> \<Longrightarrow> sum f A \<in> \<complex>
 2. (\<And>i. i \<in> {} \<Longrightarrow> f i \<in> \<complex>) \<Longrightarrow> sum f {} \<in> \<complex>
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>i. i \<in> F \<Longrightarrow> f i \<in> \<complex>) \<Longrightarrow> sum f F \<in> \<complex>; \<And>i. i \<in> insert x F \<Longrightarrow> f i \<in> \<complex>\<rbrakk> \<Longrightarrow> sum f (insert x F) \<in> \<complex>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite A_
?i \<in> A_ \<Longrightarrow> f ?i \<in> \<complex>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
infinite A_
?i \<in> A_ \<Longrightarrow> f ?i \<in> \<complex>

goal (1 subgoal):
 1. sum f A_ \<in> \<complex>
[PROOF STEP]
by (metis Complexs_0 sum.infinite)
[PROOF STATE]
proof (state)
this:
sum f A_ \<in> \<complex>

goal (2 subgoals):
 1. (\<And>i. i \<in> {} \<Longrightarrow> f i \<in> \<complex>) \<Longrightarrow> sum f {} \<in> \<complex>
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>i. i \<in> F \<Longrightarrow> f i \<in> \<complex>) \<Longrightarrow> sum f F \<in> \<complex>; \<And>i. i \<in> insert x F \<Longrightarrow> f i \<in> \<complex>\<rbrakk> \<Longrightarrow> sum f (insert x F) \<in> \<complex>
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma prod_in_Complexs [intro,simp]: "(\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<complex>) \<Longrightarrow> prod f s \<in> \<complex>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<complex>) \<Longrightarrow> prod f s \<in> \<complex>
[PROOF STEP]
proof (induct s rule: infinite_finite_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>i. i \<in> A \<Longrightarrow> f i \<in> \<complex>\<rbrakk> \<Longrightarrow> prod f A \<in> \<complex>
 2. (\<And>i. i \<in> {} \<Longrightarrow> f i \<in> \<complex>) \<Longrightarrow> prod f {} \<in> \<complex>
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>i. i \<in> F \<Longrightarrow> f i \<in> \<complex>) \<Longrightarrow> prod f F \<in> \<complex>; \<And>i. i \<in> insert x F \<Longrightarrow> f i \<in> \<complex>\<rbrakk> \<Longrightarrow> prod f (insert x F) \<in> \<complex>
[PROOF STEP]
case infinite
[PROOF STATE]
proof (state)
this:
infinite A_
?i \<in> A_ \<Longrightarrow> f ?i \<in> \<complex>

goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>i. i \<in> A \<Longrightarrow> f i \<in> \<complex>\<rbrakk> \<Longrightarrow> prod f A \<in> \<complex>
 2. (\<And>i. i \<in> {} \<Longrightarrow> f i \<in> \<complex>) \<Longrightarrow> prod f {} \<in> \<complex>
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>i. i \<in> F \<Longrightarrow> f i \<in> \<complex>) \<Longrightarrow> prod f F \<in> \<complex>; \<And>i. i \<in> insert x F \<Longrightarrow> f i \<in> \<complex>\<rbrakk> \<Longrightarrow> prod f (insert x F) \<in> \<complex>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite A_
?i \<in> A_ \<Longrightarrow> f ?i \<in> \<complex>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
infinite A_
?i \<in> A_ \<Longrightarrow> f ?i \<in> \<complex>

goal (1 subgoal):
 1. prod f A_ \<in> \<complex>
[PROOF STEP]
by (metis Complexs_1 prod.infinite)
[PROOF STATE]
proof (state)
this:
prod f A_ \<in> \<complex>

goal (2 subgoals):
 1. (\<And>i. i \<in> {} \<Longrightarrow> f i \<in> \<complex>) \<Longrightarrow> prod f {} \<in> \<complex>
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>i. i \<in> F \<Longrightarrow> f i \<in> \<complex>) \<Longrightarrow> prod f F \<in> \<complex>; \<And>i. i \<in> insert x F \<Longrightarrow> f i \<in> \<complex>\<rbrakk> \<Longrightarrow> prod f (insert x F) \<in> \<complex>
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma Complexs_induct [case_names of_complex, induct set: Complexs]:
  "q \<in> \<complex> \<Longrightarrow> (\<And>r. P (of_complex r)) \<Longrightarrow> P q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q \<in> \<complex>; \<And>r. P (of_complex r)\<rbrakk> \<Longrightarrow> P q
[PROOF STEP]
by (rule Complexs_cases) auto


[STATEMENT]
lemma scaleC_mono:
  "a \<le> b \<Longrightarrow> x \<le> y \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> x \<Longrightarrow> a *\<^sub>C x \<le> b *\<^sub>C y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; x \<le> y; 0 \<le> b; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> a *\<^sub>C x \<le> b *\<^sub>C y
[PROOF STEP]
by (meson order_trans scaleC_left_mono scaleC_right_mono)


[STATEMENT]
lemma scaleC_mono':
  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a *\<^sub>C c \<le> b *\<^sub>C d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; c \<le> d; 0 \<le> a; (0::'a) \<le> c\<rbrakk> \<Longrightarrow> a *\<^sub>C c \<le> b *\<^sub>C d
[PROOF STEP]
by (rule scaleC_mono) (auto intro: order.trans)


[STATEMENT]
lemma pos_le_divideC_eq [field_simps]:
  "a \<le> b /\<^sub>C c \<longleftrightarrow> c *\<^sub>C a \<le> b" (is "?P \<longleftrightarrow> ?Q") if "0 < c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le> b /\<^sub>C c) = (c *\<^sub>C a \<le> b)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<le> b /\<^sub>C c \<Longrightarrow> c *\<^sub>C a \<le> b
 2. c *\<^sub>C a \<le> b \<Longrightarrow> a \<le> b /\<^sub>C c
[PROOF STEP]
assume ?P
[PROOF STATE]
proof (state)
this:
a \<le> b /\<^sub>C c

goal (2 subgoals):
 1. a \<le> b /\<^sub>C c \<Longrightarrow> c *\<^sub>C a \<le> b
 2. c *\<^sub>C a \<le> b \<Longrightarrow> a \<le> b /\<^sub>C c
[PROOF STEP]
with scaleC_left_mono that
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x \<le> ?y; 0 \<le> ?a\<rbrakk> \<Longrightarrow> ?a *\<^sub>C ?x \<le> ?a *\<^sub>C ?y
0 < c
a \<le> b /\<^sub>C c
[PROOF STEP]
have "c *\<^sub>C a \<le> c *\<^sub>C (b /\<^sub>C c)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<le> ?y; 0 \<le> ?a\<rbrakk> \<Longrightarrow> ?a *\<^sub>C ?x \<le> ?a *\<^sub>C ?y
0 < c
a \<le> b /\<^sub>C c

goal (1 subgoal):
 1. c *\<^sub>C a \<le> c *\<^sub>C (b /\<^sub>C c)
[PROOF STEP]
using preorder_class.less_imp_le
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<le> ?y; 0 \<le> ?a\<rbrakk> \<Longrightarrow> ?a *\<^sub>C ?x \<le> ?a *\<^sub>C ?y
0 < c
a \<le> b /\<^sub>C c
?x < ?y \<Longrightarrow> ?x \<le> ?y

goal (1 subgoal):
 1. c *\<^sub>C a \<le> c *\<^sub>C (b /\<^sub>C c)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c *\<^sub>C a \<le> c *\<^sub>C (b /\<^sub>C c)

goal (2 subgoals):
 1. a \<le> b /\<^sub>C c \<Longrightarrow> c *\<^sub>C a \<le> b
 2. c *\<^sub>C a \<le> b \<Longrightarrow> a \<le> b /\<^sub>C c
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
0 < c
c *\<^sub>C a \<le> c *\<^sub>C (b /\<^sub>C c)
[PROOF STEP]
show ?Q
[PROOF STATE]
proof (prove)
using this:
0 < c
c *\<^sub>C a \<le> c *\<^sub>C (b /\<^sub>C c)

goal (1 subgoal):
 1. c *\<^sub>C a \<le> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c *\<^sub>C a \<le> b

goal (1 subgoal):
 1. c *\<^sub>C a \<le> b \<Longrightarrow> a \<le> b /\<^sub>C c
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c *\<^sub>C a \<le> b \<Longrightarrow> a \<le> b /\<^sub>C c
[PROOF STEP]
assume ?Q
[PROOF STATE]
proof (state)
this:
c *\<^sub>C a \<le> b

goal (1 subgoal):
 1. c *\<^sub>C a \<le> b \<Longrightarrow> a \<le> b /\<^sub>C c
[PROOF STEP]
with scaleC_left_mono that
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x \<le> ?y; 0 \<le> ?a\<rbrakk> \<Longrightarrow> ?a *\<^sub>C ?x \<le> ?a *\<^sub>C ?y
0 < c
c *\<^sub>C a \<le> b
[PROOF STEP]
have "c *\<^sub>C a /\<^sub>C c \<le> b /\<^sub>C c"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<le> ?y; 0 \<le> ?a\<rbrakk> \<Longrightarrow> ?a *\<^sub>C ?x \<le> ?a *\<^sub>C ?y
0 < c
c *\<^sub>C a \<le> b

goal (1 subgoal):
 1. c *\<^sub>C a /\<^sub>C c \<le> b /\<^sub>C c
[PROOF STEP]
using less_complex_def less_eq_complex_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<le> ?y; 0 \<le> ?a\<rbrakk> \<Longrightarrow> ?a *\<^sub>C ?x \<le> ?a *\<^sub>C ?y
0 < c
c *\<^sub>C a \<le> b
(?x < ?y) = (Re ?x < Re ?y \<and> Im ?x = Im ?y)
(?x \<le> ?y) = (Re ?x \<le> Re ?y \<and> Im ?x = Im ?y)

goal (1 subgoal):
 1. c *\<^sub>C a /\<^sub>C c \<le> b /\<^sub>C c
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
c *\<^sub>C a /\<^sub>C c \<le> b /\<^sub>C c

goal (1 subgoal):
 1. c *\<^sub>C a \<le> b \<Longrightarrow> a \<le> b /\<^sub>C c
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
0 < c
c *\<^sub>C a /\<^sub>C c \<le> b /\<^sub>C c
[PROOF STEP]
show ?P
[PROOF STATE]
proof (prove)
using this:
0 < c
c *\<^sub>C a /\<^sub>C c \<le> b /\<^sub>C c

goal (1 subgoal):
 1. a \<le> b /\<^sub>C c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<le> b /\<^sub>C c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pos_divideC_le_eq [field_simps]:
  "b /\<^sub>C c \<le> a \<longleftrightarrow> b \<le> c *\<^sub>C a" if "c > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b /\<^sub>C c \<le> a) = (b \<le> c *\<^sub>C a)
[PROOF STEP]
using that pos_le_divideC_eq [of "inverse c" b a]
    less_complex_def
[PROOF STATE]
proof (prove)
using this:
0 < c
0 < inverse c \<Longrightarrow> (b \<le> a /\<^sub>C inverse c) = (b /\<^sub>C c \<le> a)
(?x < ?y) = (Re ?x < Re ?y \<and> Im ?x = Im ?y)

goal (1 subgoal):
 1. (b /\<^sub>C c \<le> a) = (b \<le> c *\<^sub>C a)
[PROOF STEP]
by auto


[STATEMENT]
lemma pos_divideC_less_eq [field_simps]:
  "b /\<^sub>C c < a \<longleftrightarrow> b < c *\<^sub>C a" if "c > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b /\<^sub>C c < a) = (b < c *\<^sub>C a)
[PROOF STEP]
using that pos_less_divideC_eq [of "inverse c" b a]
[PROOF STATE]
proof (prove)
using this:
0 < c
0 < inverse c \<Longrightarrow> (b < a /\<^sub>C inverse c) = (b /\<^sub>C c < a)

goal (1 subgoal):
 1. (b /\<^sub>C c < a) = (b < c *\<^sub>C a)
[PROOF STEP]
by (simp add: local.less_le_not_le local.pos_divideC_le_eq local.pos_le_divideC_eq)


[STATEMENT]
lemma pos_le_minus_divideC_eq [field_simps]:
  "a \<le> - (b /\<^sub>C c) \<longleftrightarrow> c *\<^sub>C a \<le> - b" if "c > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le> - (b /\<^sub>C c)) = (c *\<^sub>C a \<le> - b)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. (a \<le> - (b /\<^sub>C c)) = (c *\<^sub>C a \<le> - b)
[PROOF STEP]
by (metis local.ab_left_minus local.add.inverse_unique local.add.right_inverse local.add_minus_cancel local.le_minus_iff local.pos_divideC_le_eq local.scaleC_add_right local.scaleC_one local.scaleC_scaleC)


[STATEMENT]
lemma pos_less_minus_divideC_eq [field_simps]:
  "a < - (b /\<^sub>C c) \<longleftrightarrow> c *\<^sub>C a < - b" if "c > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a < - (b /\<^sub>C c)) = (c *\<^sub>C a < - b)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. (a < - (b /\<^sub>C c)) = (c *\<^sub>C a < - b)
[PROOF STEP]
by (metis le_less less_le_not_le pos_divideC_le_eq pos_divideC_less_eq pos_le_minus_divideC_eq)


[STATEMENT]
lemma pos_minus_divideC_le_eq [field_simps]:
  "- (b /\<^sub>C c) \<le> a \<longleftrightarrow> - b \<le> c *\<^sub>C a" if "c > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- (b /\<^sub>C c) \<le> a) = (- b \<le> c *\<^sub>C a)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. (- (b /\<^sub>C c) \<le> a) = (- b \<le> c *\<^sub>C a)
[PROOF STEP]
by (metis local.add_minus_cancel local.left_minus local.pos_divideC_le_eq local.scaleC_add_right)


[STATEMENT]
lemma pos_minus_divideC_less_eq [field_simps]:
  "- (b /\<^sub>C c) < a \<longleftrightarrow> - b < c *\<^sub>C a" if "c > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- (b /\<^sub>C c) < a) = (- b < c *\<^sub>C a)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. (- (b /\<^sub>C c) < a) = (- b < c *\<^sub>C a)
[PROOF STEP]
by (simp add: less_le_not_le pos_le_minus_divideC_eq pos_minus_divideC_le_eq)


[STATEMENT]
lemma scaleC_image_atLeastAtMost: "c > 0 \<Longrightarrow> scaleC c ` {x..y} = {c *\<^sub>C x..c *\<^sub>C y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < c \<Longrightarrow> (*\<^sub>C) c ` {x..y} = {c *\<^sub>C x..c *\<^sub>C y}
[PROOF STEP]
apply (auto intro!: scaleC_left_mono simp: image_iff Bex_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>0 < c; c *\<^sub>C x \<le> xa; xa \<le> c *\<^sub>C y\<rbrakk> \<Longrightarrow> \<exists>xb\<ge>x. xb \<le> y \<and> xa = c *\<^sub>C xb
[PROOF STEP]
by (meson order.eq_iff local.order.refl pos_divideC_le_eq pos_le_divideC_eq)


[STATEMENT]
lemma neg_le_divideC_eq [field_simps]:
  "a \<le> b /\<^sub>C c \<longleftrightarrow> b \<le> c *\<^sub>C a" (is "?P \<longleftrightarrow> ?Q") if "c < 0"
    for a b :: "'a :: ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le> b /\<^sub>C c) = (b \<le> c *\<^sub>C a)
[PROOF STEP]
using that pos_le_divideC_eq [of "- c" a "- b"]
[PROOF STATE]
proof (prove)
using this:
c < 0
0 < - c \<Longrightarrow> (a \<le> - b /\<^sub>C - c) = (- c *\<^sub>C a \<le> - b)

goal (1 subgoal):
 1. (a \<le> b /\<^sub>C c) = (b \<le> c *\<^sub>C a)
[PROOF STEP]
by (simp add: less_complex_def)


[STATEMENT]
lemma neg_less_divideC_eq [field_simps]:
  "a < b /\<^sub>C c \<longleftrightarrow> b < c *\<^sub>C a" if "c < 0"
    for a b :: "'a :: ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a < b /\<^sub>C c) = (b < c *\<^sub>C a)
[PROOF STEP]
using that neg_le_divideC_eq [of c a b]
[PROOF STATE]
proof (prove)
using this:
c < 0
c < 0 \<Longrightarrow> (a \<le> b /\<^sub>C c) = (b \<le> c *\<^sub>C a)

goal (1 subgoal):
 1. (a < b /\<^sub>C c) = (b < c *\<^sub>C a)
[PROOF STEP]
by (smt (verit, ccfv_SIG) neg_le_divideC_eq antisym_conv2 complex_vector.scale_minus_right dual_order.strict_implies_order le_less_trans neg_le_iff_le scaleC_scaleC)


[STATEMENT]
lemma neg_divideC_le_eq [field_simps]:
  "b /\<^sub>C c \<le> a \<longleftrightarrow> c *\<^sub>C a \<le> b" if "c < 0"
    for a b :: "'a :: ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b /\<^sub>C c \<le> a) = (c *\<^sub>C a \<le> b)
[PROOF STEP]
using that pos_divideC_le_eq [of "- c" "- b" a]
[PROOF STATE]
proof (prove)
using this:
c < 0
0 < - c \<Longrightarrow> (- b /\<^sub>C - c \<le> a) = (- b \<le> - c *\<^sub>C a)

goal (1 subgoal):
 1. (b /\<^sub>C c \<le> a) = (c *\<^sub>C a \<le> b)
[PROOF STEP]
by (simp add: less_complex_def)


[STATEMENT]
lemma neg_divideC_less_eq [field_simps]:
  "b /\<^sub>C c < a \<longleftrightarrow> c *\<^sub>C a < b" if "c < 0"
    for a b :: "'a :: ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b /\<^sub>C c < a) = (c *\<^sub>C a < b)
[PROOF STEP]
using that neg_divideC_le_eq [of c b a]
[PROOF STATE]
proof (prove)
using this:
c < 0
c < 0 \<Longrightarrow> (b /\<^sub>C c \<le> a) = (c *\<^sub>C a \<le> b)

goal (1 subgoal):
 1. (b /\<^sub>C c < a) = (c *\<^sub>C a < b)
[PROOF STEP]
by (meson neg_le_divideC_eq less_le_not_le)


[STATEMENT]
lemma neg_le_minus_divideC_eq [field_simps]:
  "a \<le> - (b /\<^sub>C c) \<longleftrightarrow> - b \<le> c *\<^sub>C a" if "c < 0"
    for a b :: "'a :: ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le> - (b /\<^sub>C c)) = (- b \<le> c *\<^sub>C a)
[PROOF STEP]
using that pos_le_minus_divideC_eq [of "- c" a "- b"]
[PROOF STATE]
proof (prove)
using this:
c < 0
0 < - c \<Longrightarrow> (a \<le> - (- b /\<^sub>C - c)) = (- c *\<^sub>C a \<le> - (- b))

goal (1 subgoal):
 1. (a \<le> - (b /\<^sub>C c)) = (- b \<le> c *\<^sub>C a)
[PROOF STEP]
by (metis neg_le_divideC_eq complex_vector.scale_minus_right)


[STATEMENT]
lemma neg_less_minus_divideC_eq [field_simps]:
  "a < - (b /\<^sub>C c) \<longleftrightarrow> - b < c *\<^sub>C a" if "c < 0"
    for a b :: "'a :: ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a < - (b /\<^sub>C c)) = (- b < c *\<^sub>C a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a < - (b /\<^sub>C c)) = (- b < c *\<^sub>C a)
[PROOF STEP]
have *: "- b = c *\<^sub>C a \<longleftrightarrow> b = - (c *\<^sub>C a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- b = c *\<^sub>C a) = (b = - (c *\<^sub>C a))
[PROOF STEP]
by (metis add.inverse_inverse)
[PROOF STATE]
proof (state)
this:
(- b = c *\<^sub>C a) = (b = - (c *\<^sub>C a))

goal (1 subgoal):
 1. (a < - (b /\<^sub>C c)) = (- b < c *\<^sub>C a)
[PROOF STEP]
from that neg_le_minus_divideC_eq [of c a b]
[PROOF STATE]
proof (chain)
picking this:
c < 0
c < 0 \<Longrightarrow> (a \<le> - (b /\<^sub>C c)) = (- b \<le> c *\<^sub>C a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c < 0
c < 0 \<Longrightarrow> (a \<le> - (b /\<^sub>C c)) = (- b \<le> c *\<^sub>C a)

goal (1 subgoal):
 1. (a < - (b /\<^sub>C c)) = (- b < c *\<^sub>C a)
[PROOF STEP]
by (auto simp add: le_less *)
[PROOF STATE]
proof (state)
this:
(a < - (b /\<^sub>C c)) = (- b < c *\<^sub>C a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma neg_minus_divideC_le_eq [field_simps]:
  "- (b /\<^sub>C c) \<le> a \<longleftrightarrow> c *\<^sub>C a \<le> - b" if "c < 0"
for a b :: "'a :: ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- (b /\<^sub>C c) \<le> a) = (c *\<^sub>C a \<le> - b)
[PROOF STEP]
using that pos_minus_divideC_le_eq [of "- c" "- b" a]
[PROOF STATE]
proof (prove)
using this:
c < 0
0 < - c \<Longrightarrow> (- (- b /\<^sub>C - c) \<le> a) = (- (- b) \<le> - c *\<^sub>C a)

goal (1 subgoal):
 1. (- (b /\<^sub>C c) \<le> a) = (c *\<^sub>C a \<le> - b)
[PROOF STEP]
by (metis Complex_Vector_Spaces0.neg_divideC_le_eq complex_vector.scale_minus_right)


[STATEMENT]
lemma neg_minus_divideC_less_eq [field_simps]:
  "- (b /\<^sub>C c) < a \<longleftrightarrow> c *\<^sub>C a < - b" if "c < 0"
for a b :: "'a :: ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- (b /\<^sub>C c) < a) = (c *\<^sub>C a < - b)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
c < 0

goal (1 subgoal):
 1. (- (b /\<^sub>C c) < a) = (c *\<^sub>C a < - b)
[PROOF STEP]
by (simp add: less_le_not_le neg_le_minus_divideC_eq neg_minus_divideC_le_eq)


[STATEMENT]
lemma divideC_field_splits_simps_1 [field_split_simps]: (* In Real_Vector_Spaces, these lemmas are unnamed *)
  "a = b /\<^sub>C c \<longleftrightarrow> (if c = 0 then a = 0 else c *\<^sub>C a = b)"
  "b /\<^sub>C c = a \<longleftrightarrow> (if c = 0 then a = 0 else b = c *\<^sub>C a)"
  "a + b /\<^sub>C c = (if c = 0 then a else (c *\<^sub>C a + b) /\<^sub>C c)"
  "a /\<^sub>C c + b = (if c = 0 then b else (a + c *\<^sub>C b) /\<^sub>C c)"
  "a - b /\<^sub>C c = (if c = 0 then a else (c *\<^sub>C a - b) /\<^sub>C c)"
  "a /\<^sub>C c - b = (if c = 0 then - b else (a - c *\<^sub>C b) /\<^sub>C c)"
  "- (a /\<^sub>C c) + b = (if c = 0 then b else (- a + c *\<^sub>C b) /\<^sub>C c)"
  "- (a /\<^sub>C c) - b = (if c = 0 then - b else (- a - c *\<^sub>C b) /\<^sub>C c)"
  for a b :: "'a :: complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((a = b /\<^sub>C c) = (if c = 0 then a = (0::'a) else c *\<^sub>C a = b) &&& (b /\<^sub>C c = a) = (if c = 0 then a = (0::'a) else b = c *\<^sub>C a)) &&& a + b /\<^sub>C c = (if c = 0 then a else (c *\<^sub>C a + b) /\<^sub>C c) &&& a /\<^sub>C c + b = (if c = 0 then b else (a + c *\<^sub>C b) /\<^sub>C c)) &&& (a - b /\<^sub>C c = (if c = 0 then a else (c *\<^sub>C a - b) /\<^sub>C c) &&& a /\<^sub>C c - b = (if c = 0 then - b else (a - c *\<^sub>C b) /\<^sub>C c)) &&& - (a /\<^sub>C c) + b = (if c = 0 then b else (- a + c *\<^sub>C b) /\<^sub>C c) &&& - (a /\<^sub>C c) - b = (if c = 0 then - b else (- a - c *\<^sub>C b) /\<^sub>C c)
[PROOF STEP]
by (auto simp add: field_simps)


[STATEMENT]
lemma divideC_field_splits_simps_2 [field_split_simps]: (* In Real_Vector_Spaces, these lemmas are unnamed *)
  "0 < c \<Longrightarrow> a \<le> b /\<^sub>C c \<longleftrightarrow> (if c > 0 then c *\<^sub>C a \<le> b else if c < 0 then b \<le> c *\<^sub>C a else a \<le> 0)"
  "0 < c \<Longrightarrow> a < b /\<^sub>C c \<longleftrightarrow> (if c > 0 then c *\<^sub>C a < b else if c < 0 then b < c *\<^sub>C a else a < 0)"
  "0 < c \<Longrightarrow> b /\<^sub>C c \<le> a \<longleftrightarrow> (if c > 0 then b \<le> c *\<^sub>C a else if c < 0 then c *\<^sub>C a \<le> b else a \<ge> 0)"
  "0 < c \<Longrightarrow> b /\<^sub>C c < a \<longleftrightarrow> (if c > 0 then b < c *\<^sub>C a else if c < 0 then c *\<^sub>C a < b else a > 0)"
  "0 < c \<Longrightarrow> a \<le> - (b /\<^sub>C c) \<longleftrightarrow> (if c > 0 then c *\<^sub>C a \<le> - b else if c < 0 then - b \<le> c *\<^sub>C a else a \<le> 0)"
  "0 < c \<Longrightarrow> a < - (b /\<^sub>C c) \<longleftrightarrow> (if c > 0 then c *\<^sub>C a < - b else if c < 0 then - b < c *\<^sub>C a else a < 0)"
  "0 < c \<Longrightarrow> - (b /\<^sub>C c) \<le> a \<longleftrightarrow> (if c > 0 then - b \<le> c *\<^sub>C a else if c < 0 then c *\<^sub>C a \<le> - b else a \<ge> 0)"
  "0 < c \<Longrightarrow> - (b /\<^sub>C c) < a \<longleftrightarrow> (if c > 0 then - b < c *\<^sub>C a else if c < 0 then c *\<^sub>C a < - b else a > 0)"
  for a b :: "'a :: ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((0 < c \<Longrightarrow> (a \<le> b /\<^sub>C c) = (if 0 < c then c *\<^sub>C a \<le> b else if c < 0 then b \<le> c *\<^sub>C a else a \<le> (0::'a))) &&& (0 < c \<Longrightarrow> (a < b /\<^sub>C c) = (if 0 < c then c *\<^sub>C a < b else if c < 0 then b < c *\<^sub>C a else a < (0::'a)))) &&& (0 < c \<Longrightarrow> (b /\<^sub>C c \<le> a) = (if 0 < c then b \<le> c *\<^sub>C a else if c < 0 then c *\<^sub>C a \<le> b else (0::'a) \<le> a)) &&& (0 < c \<Longrightarrow> (b /\<^sub>C c < a) = (if 0 < c then b < c *\<^sub>C a else if c < 0 then c *\<^sub>C a < b else (0::'a) < a))) &&& ((0 < c \<Longrightarrow> (a \<le> - (b /\<^sub>C c)) = (if 0 < c then c *\<^sub>C a \<le> - b else if c < 0 then - b \<le> c *\<^sub>C a else a \<le> (0::'a))) &&& (0 < c \<Longrightarrow> (a < - (b /\<^sub>C c)) = (if 0 < c then c *\<^sub>C a < - b else if c < 0 then - b < c *\<^sub>C a else a < (0::'a)))) &&& (0 < c \<Longrightarrow> (- (b /\<^sub>C c) \<le> a) = (if 0 < c then - b \<le> c *\<^sub>C a else if c < 0 then c *\<^sub>C a \<le> - b else (0::'a) \<le> a)) &&& (0 < c \<Longrightarrow> (- (b /\<^sub>C c) < a) = (if 0 < c then - b < c *\<^sub>C a else if c < 0 then c *\<^sub>C a < - b else (0::'a) < a))
[PROOF STEP]
by (clarsimp intro!: field_simps)+


[STATEMENT]
lemma scaleC_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> a *\<^sub>C x"
  for x :: "'a::ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> (0::'a) \<le> a *\<^sub>C x
[PROOF STEP]
using scaleC_left_mono [of 0 x a]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(0::'a) \<le> x; 0 \<le> a\<rbrakk> \<Longrightarrow> a *\<^sub>C (0::'a) \<le> a *\<^sub>C x

goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> (0::'a) \<le> a *\<^sub>C x
[PROOF STEP]
by simp


[STATEMENT]
lemma scaleC_nonneg_nonpos: "0 \<le> a \<Longrightarrow> x \<le> 0 \<Longrightarrow> a *\<^sub>C x \<le> 0"
  for x :: "'a::ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; x \<le> (0::'a)\<rbrakk> \<Longrightarrow> a *\<^sub>C x \<le> (0::'a)
[PROOF STEP]
using scaleC_left_mono [of x 0 a]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<le> (0::'a); 0 \<le> a\<rbrakk> \<Longrightarrow> a *\<^sub>C x \<le> a *\<^sub>C (0::'a)

goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; x \<le> (0::'a)\<rbrakk> \<Longrightarrow> a *\<^sub>C x \<le> (0::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma scaleC_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> x \<Longrightarrow> a *\<^sub>C x \<le> 0"
  for x :: "'a::ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> 0; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> a *\<^sub>C x \<le> (0::'a)
[PROOF STEP]
using scaleC_right_mono [of a 0 x]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<le> 0; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> a *\<^sub>C x \<le> 0 *\<^sub>C x

goal (1 subgoal):
 1. \<lbrakk>a \<le> 0; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> a *\<^sub>C x \<le> (0::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma split_scaleC_neg_le: "(0 \<le> a \<and> x \<le> 0) \<or> (a \<le> 0 \<and> 0 \<le> x) \<Longrightarrow> a *\<^sub>C x \<le> 0"
  for x :: "'a::ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> a \<and> x \<le> (0::'a) \<or> a \<le> 0 \<and> (0::'a) \<le> x \<Longrightarrow> a *\<^sub>C x \<le> (0::'a)
[PROOF STEP]
by (auto simp: scaleC_nonneg_nonpos scaleC_nonpos_nonneg)


[STATEMENT]
lemma cle_add_iff1: "a *\<^sub>C e + c \<le> b *\<^sub>C e + d \<longleftrightarrow> (a - b) *\<^sub>C e + c \<le> d"
  for c d e :: "'a::ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a *\<^sub>C e + c \<le> b *\<^sub>C e + d) = ((a - b) *\<^sub>C e + c \<le> d)
[PROOF STEP]
by (simp add: algebra_simps)


[STATEMENT]
lemma cle_add_iff2: "a *\<^sub>C e + c \<le> b *\<^sub>C e + d \<longleftrightarrow> c \<le> (b - a) *\<^sub>C e + d"
  for c d e :: "'a::ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a *\<^sub>C e + c \<le> b *\<^sub>C e + d) = (c \<le> (b - a) *\<^sub>C e + d)
[PROOF STEP]
by (simp add: algebra_simps)


[STATEMENT]
lemma scaleC_left_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c *\<^sub>C a \<le> c *\<^sub>C b"
  for a b :: "'a::ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<le> a; c \<le> 0\<rbrakk> \<Longrightarrow> c *\<^sub>C a \<le> c *\<^sub>C b
[PROOF STEP]
by (drule scaleC_left_mono [of _ _ "- c"], simp_all add: less_eq_complex_def)


[STATEMENT]
lemma scaleC_right_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a *\<^sub>C c \<le> b *\<^sub>C c"
  for c :: "'a::ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<le> a; c \<le> (0::'a)\<rbrakk> \<Longrightarrow> a *\<^sub>C c \<le> b *\<^sub>C c
[PROOF STEP]
by (drule scaleC_right_mono [of _ _ "- c"], simp_all)


[STATEMENT]
lemma scaleC_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a *\<^sub>C b"
  for b :: "'a::ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> 0; b \<le> (0::'a)\<rbrakk> \<Longrightarrow> (0::'a) \<le> a *\<^sub>C b
[PROOF STEP]
using scaleC_right_mono_neg [of a 0 b]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<le> 0; b \<le> (0::'a)\<rbrakk> \<Longrightarrow> 0 *\<^sub>C b \<le> a *\<^sub>C b

goal (1 subgoal):
 1. \<lbrakk>a \<le> 0; b \<le> (0::'a)\<rbrakk> \<Longrightarrow> (0::'a) \<le> a *\<^sub>C b
[PROOF STEP]
by simp


[STATEMENT]
lemma split_scaleC_pos_le: "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a *\<^sub>C b"
  for b :: "'a::ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> a \<and> (0::'a) \<le> b \<or> a \<le> 0 \<and> b \<le> (0::'a) \<Longrightarrow> (0::'a) \<le> a *\<^sub>C b
[PROOF STEP]
by (auto simp: scaleC_nonneg_nonneg scaleC_nonpos_nonpos)


[STATEMENT]
lemma zero_le_scaleC_iff:
  fixes b :: "'a::ordered_complex_vector"
  assumes "a \<in> \<real>" (* Not present in Real_Vector_Spaces.thy *)
  shows "0 \<le> a *\<^sub>C b \<longleftrightarrow> 0 < a \<and> 0 \<le> b \<or> a < 0 \<and> b \<le> 0 \<or> a = 0"
    (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((0::'a) \<le> a *\<^sub>C b) = (0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0)
[PROOF STEP]
proof (cases "a = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = 0 \<Longrightarrow> ((0::'a) \<le> a *\<^sub>C b) = (0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0)
 2. a \<noteq> 0 \<Longrightarrow> ((0::'a) \<le> a *\<^sub>C b) = (0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = 0

goal (2 subgoals):
 1. a = 0 \<Longrightarrow> ((0::'a) \<le> a *\<^sub>C b) = (0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0)
 2. a \<noteq> 0 \<Longrightarrow> ((0::'a) \<le> a *\<^sub>C b) = (0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = 0

goal (1 subgoal):
 1. ((0::'a) \<le> a *\<^sub>C b) = (0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((0::'a) \<le> a *\<^sub>C b) = (0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0)

goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> ((0::'a) \<le> a *\<^sub>C b) = (0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> ((0::'a) \<le> a *\<^sub>C b) = (0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> 0

goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> ((0::'a) \<le> a *\<^sub>C b) = (0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((0::'a) \<le> a *\<^sub>C b) = (0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (0::'a) \<le> a *\<^sub>C b \<Longrightarrow> 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0
 2. 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0 \<Longrightarrow> (0::'a) \<le> a *\<^sub>C b
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> a *\<^sub>C b

goal (2 subgoals):
 1. (0::'a) \<le> a *\<^sub>C b \<Longrightarrow> 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0
 2. 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0 \<Longrightarrow> (0::'a) \<le> a *\<^sub>C b
[PROOF STEP]
from \<open>a \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> 0
[PROOF STEP]
consider "a > 0" | "a < 0"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>0 < a \<Longrightarrow> thesis; a < 0 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms complex_is_Real_iff less_complex_def less_eq_complex_def not_le order.not_eq_order_implies_strict that(1) zero_complex.sel(2))
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < a \<Longrightarrow> ?thesis; a < 0 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (2 subgoals):
 1. (0::'a) \<le> a *\<^sub>C b \<Longrightarrow> 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0
 2. 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0 \<Longrightarrow> (0::'a) \<le> a *\<^sub>C b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 < a \<Longrightarrow> ?thesis; a < 0 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < a \<Longrightarrow> ?thesis; a < 0 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < a \<Longrightarrow> 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0
 2. a < 0 \<Longrightarrow> 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
0 < a

goal (2 subgoals):
 1. 0 < a \<Longrightarrow> 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0
 2. a < 0 \<Longrightarrow> 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0
[PROOF STEP]
with \<open>?lhs\<close>
[PROOF STATE]
proof (chain)
picking this:
(0::'a) \<le> a *\<^sub>C b
0 < a
[PROOF STEP]
have "inverse a *\<^sub>C 0 \<le> inverse a *\<^sub>C (a *\<^sub>C b)"
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> a *\<^sub>C b
0 < a

goal (1 subgoal):
 1. (0::'a) /\<^sub>C a \<le> a *\<^sub>C b /\<^sub>C a
[PROOF STEP]
by (metis complex_vector.scale_zero_right ordered_complex_vector_class.pos_le_divideC_eq)
[PROOF STATE]
proof (state)
this:
(0::'a) /\<^sub>C a \<le> a *\<^sub>C b /\<^sub>C a

goal (2 subgoals):
 1. 0 < a \<Longrightarrow> 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0
 2. a < 0 \<Longrightarrow> 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
0 < a
(0::'a) /\<^sub>C a \<le> a *\<^sub>C b /\<^sub>C a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < a
(0::'a) /\<^sub>C a \<le> a *\<^sub>C b /\<^sub>C a

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

goal (1 subgoal):
 1. a < 0 \<Longrightarrow> 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a < 0 \<Longrightarrow> 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
a < 0

goal (1 subgoal):
 1. a < 0 \<Longrightarrow> 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0
[PROOF STEP]
with \<open>?lhs\<close>
[PROOF STATE]
proof (chain)
picking this:
(0::'a) \<le> a *\<^sub>C b
a < 0
[PROOF STEP]
have "- inverse a *\<^sub>C 0 \<le> - inverse a *\<^sub>C (a *\<^sub>C b)"
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> a *\<^sub>C b
a < 0

goal (1 subgoal):
 1. - inverse a *\<^sub>C (0::'a) \<le> - inverse a *\<^sub>C a *\<^sub>C b
[PROOF STEP]
by (metis Complex_Vector_Spaces0.neg_le_minus_divideC_eq complex_vector.scale_zero_right neg_le_0_iff_le scaleC_left.minus)
[PROOF STATE]
proof (state)
this:
- inverse a *\<^sub>C (0::'a) \<le> - inverse a *\<^sub>C a *\<^sub>C b

goal (1 subgoal):
 1. a < 0 \<Longrightarrow> 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
a < 0
- inverse a *\<^sub>C (0::'a) \<le> - inverse a *\<^sub>C a *\<^sub>C b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a < 0
- inverse a *\<^sub>C (0::'a) \<le> - inverse a *\<^sub>C a *\<^sub>C b

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0

goal (1 subgoal):
 1. 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0 \<Longrightarrow> (0::'a) \<le> a *\<^sub>C b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0 \<Longrightarrow> (0::'a) \<le> a *\<^sub>C b
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0

goal (1 subgoal):
 1. 0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0 \<Longrightarrow> (0::'a) \<le> a *\<^sub>C b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0

goal (1 subgoal):
 1. (0::'a) \<le> a *\<^sub>C b
[PROOF STEP]
using less_imp_le split_scaleC_pos_le
[PROOF STATE]
proof (prove)
using this:
0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0
?x < ?y \<Longrightarrow> ?x \<le> ?y
0 \<le> ?a \<and> (0::?'a) \<le> ?b \<or> ?a \<le> 0 \<and> ?b \<le> (0::?'a) \<Longrightarrow> (0::?'a) \<le> ?a *\<^sub>C ?b

goal (1 subgoal):
 1. (0::'a) \<le> a *\<^sub>C b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> a *\<^sub>C b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((0::'a) \<le> a *\<^sub>C b) = (0 < a \<and> (0::'a) \<le> b \<or> a < 0 \<and> b \<le> (0::'a) \<or> a = 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scaleC_le_0_iff:
  "a *\<^sub>C b \<le> 0 \<longleftrightarrow> 0 < a \<and> b \<le> 0 \<or> a < 0 \<and> 0 \<le> b \<or> a = 0"
  if "a \<in> \<real>" (* Not present in Real_Vector_Spaces *)
  for b::"'a::ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a *\<^sub>C b \<le> (0::'a)) = (0 < a \<and> b \<le> (0::'a) \<or> a < 0 \<and> (0::'a) \<le> b \<or> a = 0)
[PROOF STEP]
apply (insert zero_le_scaleC_iff [of "-a" b])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- a \<in> \<real> \<Longrightarrow> ((0::'a) \<le> - a *\<^sub>C b) = (0 < - a \<and> (0::'a) \<le> b \<or> - a < 0 \<and> b \<le> (0::'a) \<or> - a = 0)) \<Longrightarrow> (a *\<^sub>C b \<le> (0::'a)) = (0 < a \<and> b \<le> (0::'a) \<or> a < 0 \<and> (0::'a) \<le> b \<or> a = 0)
[PROOF STEP]
using less_complex_def that
[PROOF STATE]
proof (prove)
using this:
(?x < ?y) = (Re ?x < Re ?y \<and> Im ?x = Im ?y)
a \<in> \<real>

goal (1 subgoal):
 1. (- a \<in> \<real> \<Longrightarrow> ((0::'a) \<le> - a *\<^sub>C b) = (0 < - a \<and> (0::'a) \<le> b \<or> - a < 0 \<and> b \<le> (0::'a) \<or> - a = 0)) \<Longrightarrow> (a *\<^sub>C b \<le> (0::'a)) = (0 < a \<and> b \<le> (0::'a) \<or> a < 0 \<and> (0::'a) \<le> b \<or> a = 0)
[PROOF STEP]
by force


[STATEMENT]
lemma scaleC_le_cancel_left: "c *\<^sub>C a \<le> c *\<^sub>C b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  if "c \<in> \<real>" (* Not present in Real_Vector_Spaces *)
  for b :: "'a::ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c *\<^sub>C a \<le> c *\<^sub>C b) = ((0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a))
[PROOF STEP]
by (smt (verit, ccfv_threshold) Complex_Vector_Spaces0.neg_divideC_le_eq complex_vector.scale_cancel_left complex_vector.scale_zero_right dual_order.eq_iff dual_order.trans ordered_complex_vector_class.pos_le_divideC_eq that zero_le_scaleC_iff)


[STATEMENT]
lemma scaleC_le_cancel_left_pos: "0 < c \<Longrightarrow> c *\<^sub>C a \<le> c *\<^sub>C b \<longleftrightarrow> a \<le> b"
  for b :: "'a::ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < c \<Longrightarrow> (c *\<^sub>C a \<le> c *\<^sub>C b) = (a \<le> b)
[PROOF STEP]
by (simp add: complex_is_Real_iff less_complex_def scaleC_le_cancel_left)


[STATEMENT]
lemma scaleC_le_cancel_left_neg: "c < 0 \<Longrightarrow> c *\<^sub>C a \<le> c *\<^sub>C b \<longleftrightarrow> b \<le> a"
  for b :: "'a::ordered_complex_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c < 0 \<Longrightarrow> (c *\<^sub>C a \<le> c *\<^sub>C b) = (b \<le> a)
[PROOF STEP]
by (simp add: complex_is_Real_iff less_complex_def scaleC_le_cancel_left)


[STATEMENT]
lemma scaleC_left_le_one_le: "0 \<le> x \<Longrightarrow> a \<le> 1 \<Longrightarrow> a *\<^sub>C x \<le> x"
  for x :: "'a::ordered_complex_vector" and a :: complex
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; a \<le> 1\<rbrakk> \<Longrightarrow> a *\<^sub>C x \<le> x
[PROOF STEP]
using scaleC_right_mono[of a 1 x]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<le> 1; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> a *\<^sub>C x \<le> 1 *\<^sub>C x

goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; a \<le> 1\<rbrakk> \<Longrightarrow> a *\<^sub>C x \<le> x
[PROOF STEP]
by simp


[STATEMENT]
lemma (in complex_normed_algebra_1) scaleC_power [simp]: "(scaleC x y) ^ n = scaleC (x^n) (y^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x *\<^sub>C y) ^ n = x ^ n *\<^sub>C y ^ n
[PROOF STEP]
by (induct n) (simp_all add: mult_ac)


[STATEMENT]
lemma dist_scaleC [simp]: "dist (x *\<^sub>C a) (y *\<^sub>C a) = \<bar>x - y\<bar> * norm a"
  for a :: "'a::complex_normed_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (complex_of_real x *\<^sub>C a) (complex_of_real y *\<^sub>C a) = \<bar>x - y\<bar> * norm a
[PROOF STEP]
by (metis dist_scaleR scaleR_scaleC)


[STATEMENT]
lemma norm_of_complex [simp]: "norm (of_complex c :: 'a::complex_normed_algebra_1) = cmod c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (of_complex c) = cmod c
[PROOF STEP]
by (simp add: of_complex_def)


[STATEMENT]
lemma norm_of_complex_add1 [simp]: "norm (of_complex x + 1 :: 'a :: complex_normed_div_algebra) = cmod (x + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (of_complex x + (1::'a)) = cmod (x + 1)
[PROOF STEP]
by (metis norm_of_complex of_complex_1 of_complex_add)


[STATEMENT]
lemma norm_of_complex_addn [simp]:
  "norm (of_complex x + numeral b :: 'a :: complex_normed_div_algebra) = cmod (x + numeral b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (of_complex x + numeral b) = cmod (x + numeral b)
[PROOF STEP]
by (metis norm_of_complex of_complex_add of_complex_numeral)


[STATEMENT]
lemma norm_of_complex_diff [simp]:
  "norm (of_complex b - of_complex a :: 'a::complex_normed_algebra_1) \<le> cmod (b - a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (of_complex b - of_complex a) \<le> cmod (b - a)
[PROOF STEP]
by (metis norm_of_complex of_complex_diff order_refl)


[STATEMENT]
lemma dist_of_complex [simp]: "dist (of_complex x :: 'a) (of_complex y) = dist x y"
  for a :: "'a::complex_normed_div_algebra"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (of_complex x) (of_complex y) = dist x y
[PROOF STEP]
by (metis dist_norm norm_of_complex of_complex_diff)


[STATEMENT]
lemma closed_complex_atMost: \<open>closed {..a::complex}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed {..a}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closed {..a}
[PROOF STEP]
have \<open>{..a} = Im -` {Im a} \<inter> Re -` {..Re a}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..a} = Im -` {Im a} \<inter> Re -` {..Re a}
[PROOF STEP]
by (auto simp: less_eq_complex_def)
[PROOF STATE]
proof (state)
this:
{..a} = Im -` {Im a} \<inter> Re -` {..Re a}

goal (1 subgoal):
 1. closed {..a}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{..a} = Im -` {Im a} \<inter> Re -` {..Re a}

goal (1 subgoal):
 1. closed {..a}
[PROOF STEP]
have \<open>closed \<dots>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (Im -` {Im a} \<inter> Re -` {..Re a})
[PROOF STEP]
by (auto intro!: closed_Int closed_vimage continuous_on_Im continuous_on_Re)
[PROOF STATE]
proof (state)
this:
closed (Im -` {Im a} \<inter> Re -` {..Re a})

goal (1 subgoal):
 1. closed {..a}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
closed {..a}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
closed {..a}

goal (1 subgoal):
 1. closed {..a}
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
closed {..a}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closed_complex_atLeast: \<open>closed {a::complex..}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed {a..}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closed {a..}
[PROOF STEP]
have \<open>{a..} = Im -` {Im a} \<inter> Re -` {Re a..}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a..} = Im -` {Im a} \<inter> Re -` {Re a..}
[PROOF STEP]
by (auto simp: less_eq_complex_def)
[PROOF STATE]
proof (state)
this:
{a..} = Im -` {Im a} \<inter> Re -` {Re a..}

goal (1 subgoal):
 1. closed {a..}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{a..} = Im -` {Im a} \<inter> Re -` {Re a..}

goal (1 subgoal):
 1. closed {a..}
[PROOF STEP]
have \<open>closed \<dots>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (Im -` {Im a} \<inter> Re -` {Re a..})
[PROOF STEP]
by (auto intro!: closed_Int closed_vimage continuous_on_Im continuous_on_Re)
[PROOF STATE]
proof (state)
this:
closed (Im -` {Im a} \<inter> Re -` {Re a..})

goal (1 subgoal):
 1. closed {a..}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
closed {a..}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
closed {a..}

goal (1 subgoal):
 1. closed {a..}
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
closed {a..}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closed_complex_atLeastAtMost: \<open>closed {a::complex .. b}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed {a..b}
[PROOF STEP]
proof (cases \<open>Im a = Im b\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Im a = Im b \<Longrightarrow> closed {a..b}
 2. Im a \<noteq> Im b \<Longrightarrow> closed {a..b}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Im a = Im b

goal (2 subgoals):
 1. Im a = Im b \<Longrightarrow> closed {a..b}
 2. Im a \<noteq> Im b \<Longrightarrow> closed {a..b}
[PROOF STEP]
have \<open>{a..b} = Im -` {Im a} \<inter> Re -` {Re a..Re b}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a..b} = Im -` {Im a} \<inter> Re -` {Re a..Re b}
[PROOF STEP]
by (auto simp add: less_eq_complex_def intro!: True)
[PROOF STATE]
proof (state)
this:
{a..b} = Im -` {Im a} \<inter> Re -` {Re a..Re b}

goal (2 subgoals):
 1. Im a = Im b \<Longrightarrow> closed {a..b}
 2. Im a \<noteq> Im b \<Longrightarrow> closed {a..b}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{a..b} = Im -` {Im a} \<inter> Re -` {Re a..Re b}

goal (2 subgoals):
 1. Im a = Im b \<Longrightarrow> closed {a..b}
 2. Im a \<noteq> Im b \<Longrightarrow> closed {a..b}
[PROOF STEP]
have \<open>closed \<dots>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (Im -` {Im a} \<inter> Re -` {Re a..Re b})
[PROOF STEP]
by (auto intro!: closed_Int closed_vimage continuous_on_Im continuous_on_Re)
[PROOF STATE]
proof (state)
this:
closed (Im -` {Im a} \<inter> Re -` {Re a..Re b})

goal (2 subgoals):
 1. Im a = Im b \<Longrightarrow> closed {a..b}
 2. Im a \<noteq> Im b \<Longrightarrow> closed {a..b}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
closed {a..b}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
closed {a..b}

goal (1 subgoal):
 1. closed {a..b}
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
closed {a..b}

goal (1 subgoal):
 1. Im a \<noteq> Im b \<Longrightarrow> closed {a..b}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Im a \<noteq> Im b \<Longrightarrow> closed {a..b}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Im a \<noteq> Im b

goal (1 subgoal):
 1. Im a \<noteq> Im b \<Longrightarrow> closed {a..b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Im a \<noteq> Im b
[PROOF STEP]
have *: \<open>{a..b} = {}\<close>
[PROOF STATE]
proof (prove)
using this:
Im a \<noteq> Im b

goal (1 subgoal):
 1. {a..b} = {}
[PROOF STEP]
using less_eq_complex_def
[PROOF STATE]
proof (prove)
using this:
Im a \<noteq> Im b
(?x \<le> ?y) = (Re ?x \<le> Re ?y \<and> Im ?x = Im ?y)

goal (1 subgoal):
 1. {a..b} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{a..b} = {}

goal (1 subgoal):
 1. Im a \<noteq> Im b \<Longrightarrow> closed {a..b}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed {a..b}
[PROOF STEP]
by (simp add: *)
[PROOF STATE]
proof (state)
this:
closed {a..b}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sgn_scaleC: "sgn (scaleC r x) = scaleC (sgn r) (sgn x)"
  for x :: "'a::complex_normed_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgn (r *\<^sub>C x) = sgn r *\<^sub>C sgn x
[PROOF STEP]
by (simp add: scaleR_scaleC sgn_div_norm ac_simps)


[STATEMENT]
lemma sgn_of_complex: "sgn (of_complex r :: 'a::complex_normed_algebra_1) = of_complex (sgn r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgn (of_complex r) = of_complex (sgn r)
[PROOF STEP]
unfolding of_complex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgn (r *\<^sub>C (1::'a)) = sgn r *\<^sub>C (1::'a)
[PROOF STEP]
by (simp only: sgn_scaleC sgn_one)


[STATEMENT]
lemma complex_sgn_eq: "sgn x = x / \<bar>x\<bar>"
  for x :: complex
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgn x = x / \<bar>x\<bar>
[PROOF STEP]
by (simp add: abs_complex_def scaleR_scaleC sgn_div_norm divide_inverse)


[STATEMENT]
lemma czero_le_sgn_iff [simp]: "0 \<le> sgn x \<longleftrightarrow> 0 \<le> x"
  for x :: complex
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 \<le> sgn x) = (0 \<le> x)
[PROOF STEP]
using cmod_eq_Re divide_eq_0_iff less_eq_complex_def
[PROOF STATE]
proof (prove)
using this:
Im ?z = 0 \<Longrightarrow> cmod ?z = \<bar>Re ?z\<bar>
(?a / ?b = (0::?'a)) = (?a = (0::?'a) \<or> ?b = (0::?'a))
(?x \<le> ?y) = (Re ?x \<le> Re ?y \<and> Im ?x = Im ?y)

goal (1 subgoal):
 1. (0 \<le> sgn x) = (0 \<le> x)
[PROOF STEP]
by auto


[STATEMENT]
lemma csgn_le_0_iff [simp]: "sgn x \<le> 0 \<longleftrightarrow> x \<le> 0"
  for x :: complex
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sgn x \<le> 0) = (x \<le> 0)
[PROOF STEP]
by (smt (verit, best) czero_le_sgn_iff Im_sgn Re_sgn divide_eq_0_iff dual_order.eq_iff less_eq_complex_def sgn_zero_iff zero_complex.sel(1) zero_complex.sel(2))


[STATEMENT]
lemma clinearI: "clinear f"
  if "\<And>b1 b2. f (b1 + b2) = f b1 + f b2"
    "\<And>r b. f (r *\<^sub>C b) = r *\<^sub>C f b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear f
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
f (?b1.0 + ?b2.0) = f ?b1.0 + f ?b2.0
f (?r *\<^sub>C ?b) = ?r *\<^sub>C f ?b

goal (1 subgoal):
 1. clinear f
[PROOF STEP]
by unfold_locales (auto simp: algebra_simps)


[STATEMENT]
lemma clinear_iff:
  "clinear f \<longleftrightarrow> (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>C x) = c *\<^sub>C f x)"
  (is "clinear f \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear f = ((\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>C x) = c *\<^sub>C f x))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. clinear f \<Longrightarrow> (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>C x) = c *\<^sub>C f x)
 2. (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>C x) = c *\<^sub>C f x) \<Longrightarrow> clinear f
[PROOF STEP]
assume "clinear f"
[PROOF STATE]
proof (state)
this:
clinear f

goal (2 subgoals):
 1. clinear f \<Longrightarrow> (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>C x) = c *\<^sub>C f x)
 2. (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>C x) = c *\<^sub>C f x) \<Longrightarrow> clinear f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
clinear f
[PROOF STEP]
interpret f: clinear f
[PROOF STATE]
proof (prove)
using this:
clinear f

goal (1 subgoal):
 1. clinear f
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. clinear f \<Longrightarrow> (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>C x) = c *\<^sub>C f x)
 2. (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>C x) = c *\<^sub>C f x) \<Longrightarrow> clinear f
[PROOF STEP]
show "?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>C x) = c *\<^sub>C f x)
[PROOF STEP]
by (simp add: f.add f.scale complex_vector.linear_scale f.clinear_axioms)
[PROOF STATE]
proof (state)
this:
(\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>C x) = c *\<^sub>C f x)

goal (1 subgoal):
 1. (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>C x) = c *\<^sub>C f x) \<Longrightarrow> clinear f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>C x) = c *\<^sub>C f x) \<Longrightarrow> clinear f
[PROOF STEP]
assume "?rhs"
[PROOF STATE]
proof (state)
this:
(\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>C x) = c *\<^sub>C f x)

goal (1 subgoal):
 1. (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>C x) = c *\<^sub>C f x) \<Longrightarrow> clinear f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>C x) = c *\<^sub>C f x)
[PROOF STEP]
show "clinear f"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>C x) = c *\<^sub>C f x)

goal (1 subgoal):
 1. clinear f
[PROOF STEP]
by (intro clinearI) auto
[PROOF STATE]
proof (state)
this:
clinear f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma clinear_times_of_complex: "clinear (\<lambda>x. a * of_complex x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear (\<lambda>x. a * of_complex x)
[PROOF STEP]
by (auto intro!: clinearI simp: distrib_left)
    (metis mult_scaleC_right scaleC_conv_of_complex)


[STATEMENT]
lemma clinear: "clinear f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear f
[PROOF STEP]
by (fact local.clinear_axioms)


[STATEMENT]
lemma bounded_clinear_intro:
  assumes "\<And>x y. f (x + y) = f x + f y"
    and "\<And>r x. f (scaleC r x) = scaleC r (f x)"
    and "\<And>x. norm (f x) \<le> norm x * K"
  shows "bounded_clinear f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear f
[PROOF STEP]
by standard (blast intro: assms)+


[STATEMENT]
lemma bounded_clinear_left: "bounded_clinear (\<lambda>a. a ** b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>a. a ** b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>a. a ** b)
[PROOF STEP]
obtain K where "\<And>a b. norm (a ** b) \<le> norm a * norm b * K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>K. (\<And>a b. norm (a ** b) \<le> norm a * norm b * K) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pos_bounded
[PROOF STATE]
proof (prove)
using this:
\<exists>K>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K

goal (1 subgoal):
 1. (\<And>K. (\<And>a b. norm (a ** b) \<le> norm a * norm b * K) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
norm (?a ** ?b) \<le> norm ?a * norm ?b * K

goal (1 subgoal):
 1. bounded_clinear (\<lambda>a. a ** b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
norm (?a ** ?b) \<le> norm ?a * norm ?b * K
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
norm (?a ** ?b) \<le> norm ?a * norm ?b * K

goal (1 subgoal):
 1. bounded_clinear (\<lambda>a. a ** b)
[PROOF STEP]
by (rule_tac K="norm b * K" in bounded_clinear_intro) (auto simp: algebra_simps scaleC_left add_left)
[PROOF STATE]
proof (state)
this:
bounded_clinear (\<lambda>a. a ** b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bounded_clinear_right: "bounded_clinear (\<lambda>b. a ** b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear ((**) a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bounded_clinear ((**) a)
[PROOF STEP]
obtain K where "\<And>a b. norm (a ** b) \<le> norm a * norm b * K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>K. (\<And>a b. norm (a ** b) \<le> norm a * norm b * K) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pos_bounded
[PROOF STATE]
proof (prove)
using this:
\<exists>K>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K

goal (1 subgoal):
 1. (\<And>K. (\<And>a b. norm (a ** b) \<le> norm a * norm b * K) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
norm (?a ** ?b) \<le> norm ?a * norm ?b * K

goal (1 subgoal):
 1. bounded_clinear ((**) a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
norm (?a ** ?b) \<le> norm ?a * norm ?b * K
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
norm (?a ** ?b) \<le> norm ?a * norm ?b * K

goal (1 subgoal):
 1. bounded_clinear ((**) a)
[PROOF STEP]
by (rule_tac K="norm a * K" in bounded_clinear_intro) (auto simp: algebra_simps scaleC_right add_right)
[PROOF STATE]
proof (state)
this:
bounded_clinear ((**) a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma flip: "bounded_cbilinear (\<lambda>x y. y ** x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_cbilinear (\<lambda>x y. y ** x)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a a' b. b ** (a + a') = b ** a + b ** a'
 2. \<And>a b b'. (b + b') ** a = b ** a + b' ** a
 3. \<And>r a b. b ** r *\<^sub>C a = r *\<^sub>C (b ** a)
 4. \<And>a r b. r *\<^sub>C b ** a = r *\<^sub>C (b ** a)
 5. \<exists>K. \<forall>a b. norm (b ** a) \<le> norm a * norm b * K
[PROOF STEP]
show "\<exists>K. \<forall>a b. norm (b ** a) \<le> norm a * norm b * K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>K. \<forall>a b. norm (b ** a) \<le> norm a * norm b * K
[PROOF STEP]
by (metis bounded mult.commute)
[PROOF STATE]
proof (state)
this:
\<exists>K. \<forall>a b. norm (b ** a) \<le> norm a * norm b * K

goal (4 subgoals):
 1. \<And>a a' b. b ** (a + a') = b ** a + b ** a'
 2. \<And>a b b'. (b + b') ** a = b ** a + b' ** a
 3. \<And>r a b. b ** r *\<^sub>C a = r *\<^sub>C (b ** a)
 4. \<And>a r b. r *\<^sub>C b ** a = r *\<^sub>C (b ** a)
[PROOF STEP]
qed (simp_all add: add_right add_left scaleC_right scaleC_left)


[STATEMENT]
lemma comp1:
  assumes "bounded_clinear g"
  shows "bounded_cbilinear (\<lambda>x. (**) (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_cbilinear (\<lambda>x. (**) (g x))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a a' b. g (a + a') ** b = g a ** b + g a' ** b
 2. \<And>a b b'. g a ** (b + b') = g a ** b + g a ** b'
 3. \<And>r a b. g (r *\<^sub>C a) ** b = r *\<^sub>C (g a ** b)
 4. \<And>a r b. g a ** r *\<^sub>C b = r *\<^sub>C (g a ** b)
 5. \<exists>K. \<forall>a b. norm (g a ** b) \<le> norm a * norm b * K
[PROOF STEP]
interpret g: bounded_clinear g
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear g
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a a' b. g (a + a') ** b = g a ** b + g a' ** b
 2. \<And>a b b'. g a ** (b + b') = g a ** b + g a ** b'
 3. \<And>r a b. g (r *\<^sub>C a) ** b = r *\<^sub>C (g a ** b)
 4. \<And>a r b. g a ** r *\<^sub>C b = r *\<^sub>C (g a ** b)
 5. \<exists>K. \<forall>a b. norm (g a ** b) \<le> norm a * norm b * K
[PROOF STEP]
show "\<And>a a' b. g (a + a') ** b = g a ** b + g a' ** b"
    "\<And>a b b'. g a ** (b + b') = g a ** b + g a ** b'"
    "\<And>r a b. g (r *\<^sub>C a) ** b = r *\<^sub>C (g a ** b)"
    "\<And>a r b. g a ** (r *\<^sub>C b) = r *\<^sub>C (g a ** b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>a a' b. g (a + a') ** b = g a ** b + g a' ** b) &&& (\<And>a b b'. g a ** (b + b') = g a ** b + g a ** b')) &&& (\<And>r a b. g (r *\<^sub>C a) ** b = r *\<^sub>C (g a ** b)) &&& (\<And>a r b. g a ** r *\<^sub>C b = r *\<^sub>C (g a ** b))
[PROOF STEP]
by (auto simp: g.add add_left add_right g.scaleC scaleC_left scaleC_right)
[PROOF STATE]
proof (state)
this:
g (?a + ?a') ** ?b = g ?a ** ?b + g ?a' ** ?b
g ?a ** (?b + ?b') = g ?a ** ?b + g ?a ** ?b'
g (?r *\<^sub>C ?a) ** ?b = ?r *\<^sub>C (g ?a ** ?b)
g ?a ** ?r *\<^sub>C ?b = ?r *\<^sub>C (g ?a ** ?b)

goal (1 subgoal):
 1. \<exists>K. \<forall>a b. norm (g a ** b) \<le> norm a * norm b * K
[PROOF STEP]
have "bounded_bilinear (\<lambda>a b. g a ** b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_bilinear (\<lambda>a. (**) (g a))
[PROOF STEP]
using g.real.bounded_linear
[PROOF STATE]
proof (prove)
using this:
bounded_linear g

goal (1 subgoal):
 1. bounded_bilinear (\<lambda>a. (**) (g a))
[PROOF STEP]
by (rule real.comp1)
[PROOF STATE]
proof (state)
this:
bounded_bilinear (\<lambda>a. (**) (g a))

goal (1 subgoal):
 1. \<exists>K. \<forall>a b. norm (g a ** b) \<le> norm a * norm b * K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bounded_bilinear (\<lambda>a. (**) (g a))
[PROOF STEP]
show "\<exists>K. \<forall>a b. norm (g a ** b) \<le> norm a * norm b * K"
[PROOF STATE]
proof (prove)
using this:
bounded_bilinear (\<lambda>a. (**) (g a))

goal (1 subgoal):
 1. \<exists>K. \<forall>a b. norm (g a ** b) \<le> norm a * norm b * K
[PROOF STEP]
by (rule bounded_bilinear.bounded)
[PROOF STATE]
proof (state)
this:
\<exists>K. \<forall>a b. norm (g a ** b) \<le> norm a * norm b * K

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bounded_clinear_ident[simp]: "bounded_clinear (\<lambda>x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>x. x)
[PROOF STEP]
by standard (auto intro!: exI[of _ 1])


[STATEMENT]
lemma bounded_clinear_zero[simp]: "bounded_clinear (\<lambda>x. 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>x. 0::'b)
[PROOF STEP]
by standard (auto intro!: exI[of _ 1])


[STATEMENT]
lemma bounded_clinear_add:
  assumes "bounded_clinear f"
    and "bounded_clinear g"
  shows "bounded_clinear (\<lambda>x. f x + g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>x. f x + g x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>x. f x + g x)
[PROOF STEP]
interpret f: bounded_clinear f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear f
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>x. f x + g x)
[PROOF STEP]
interpret g: bounded_clinear g
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear g
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>x. f x + g x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>x. f x + g x)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>b1 b2. f (b1 + b2) + g (b1 + b2) = f b1 + g b1 + (f b2 + g b2)
 2. \<And>r b. f (r *\<^sub>C b) + g (r *\<^sub>C b) = r *\<^sub>C (f b + g b)
 3. \<exists>K. \<forall>x. norm (f x + g x) \<le> norm x * K
[PROOF STEP]
from f.bounded
[PROOF STATE]
proof (chain)
picking this:
\<exists>K. \<forall>x. norm (f x) \<le> norm x * K
[PROOF STEP]
obtain Kf where Kf: "norm (f x) \<le> norm x * Kf" for x
[PROOF STATE]
proof (prove)
using this:
\<exists>K. \<forall>x. norm (f x) \<le> norm x * K

goal (1 subgoal):
 1. (\<And>Kf. (\<And>x. norm (f x) \<le> norm x * Kf) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
norm (f ?x) \<le> norm ?x * Kf

goal (3 subgoals):
 1. \<And>b1 b2. f (b1 + b2) + g (b1 + b2) = f b1 + g b1 + (f b2 + g b2)
 2. \<And>r b. f (r *\<^sub>C b) + g (r *\<^sub>C b) = r *\<^sub>C (f b + g b)
 3. \<exists>K. \<forall>x. norm (f x + g x) \<le> norm x * K
[PROOF STEP]
from g.bounded
[PROOF STATE]
proof (chain)
picking this:
\<exists>K. \<forall>x. norm (g x) \<le> norm x * K
[PROOF STEP]
obtain Kg where Kg: "norm (g x) \<le> norm x * Kg" for x
[PROOF STATE]
proof (prove)
using this:
\<exists>K. \<forall>x. norm (g x) \<le> norm x * K

goal (1 subgoal):
 1. (\<And>Kg. (\<And>x. norm (g x) \<le> norm x * Kg) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
norm (g ?x) \<le> norm ?x * Kg

goal (3 subgoals):
 1. \<And>b1 b2. f (b1 + b2) + g (b1 + b2) = f b1 + g b1 + (f b2 + g b2)
 2. \<And>r b. f (r *\<^sub>C b) + g (r *\<^sub>C b) = r *\<^sub>C (f b + g b)
 3. \<exists>K. \<forall>x. norm (f x + g x) \<le> norm x * K
[PROOF STEP]
show "\<exists>K. \<forall>x. norm (f x + g x) \<le> norm x * K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>K. \<forall>x. norm (f x + g x) \<le> norm x * K
[PROOF STEP]
using add_mono[OF Kf Kg]
[PROOF STATE]
proof (prove)
using this:
norm (f ?x2) + norm (g ?x1) \<le> norm ?x2 * Kf + norm ?x1 * Kg

goal (1 subgoal):
 1. \<exists>K. \<forall>x. norm (f x + g x) \<le> norm x * K
[PROOF STEP]
by (intro exI[of _ "Kf + Kg"]) (auto simp: field_simps intro: norm_triangle_ineq order_trans)
[PROOF STATE]
proof (state)
this:
\<exists>K. \<forall>x. norm (f x + g x) \<le> norm x * K

goal (2 subgoals):
 1. \<And>b1 b2. f (b1 + b2) + g (b1 + b2) = f b1 + g b1 + (f b2 + g b2)
 2. \<And>r b. f (r *\<^sub>C b) + g (r *\<^sub>C b) = r *\<^sub>C (f b + g b)
[PROOF STEP]
qed (simp_all add: f.add g.add f.scaleC g.scaleC scaleC_add_right)
[PROOF STATE]
proof (state)
this:
bounded_clinear (\<lambda>x. f x + g x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bounded_clinear_minus:
  assumes "bounded_clinear f"
  shows "bounded_clinear (\<lambda>x. - f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>x. - f x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>x. - f x)
[PROOF STEP]
interpret f: bounded_clinear f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear f
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>x. - f x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear (\<lambda>x. - f x)
[PROOF STEP]
by unfold_locales (simp_all add: f.add f.scaleC f.bounded)
[PROOF STATE]
proof (state)
this:
bounded_clinear (\<lambda>x. - f x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bounded_clinear_sub: "bounded_clinear f \<Longrightarrow> bounded_clinear g \<Longrightarrow> bounded_clinear (\<lambda>x. f x - g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bounded_clinear f; bounded_clinear g\<rbrakk> \<Longrightarrow> bounded_clinear (\<lambda>x. f x - g x)
[PROOF STEP]
using bounded_clinear_add[of f "\<lambda>x. - g x"] bounded_clinear_minus[of g]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bounded_clinear f; bounded_clinear (\<lambda>x. - g x)\<rbrakk> \<Longrightarrow> bounded_clinear (\<lambda>x. f x + - g x)
bounded_clinear g \<Longrightarrow> bounded_clinear (\<lambda>x. - g x)

goal (1 subgoal):
 1. \<lbrakk>bounded_clinear f; bounded_clinear g\<rbrakk> \<Longrightarrow> bounded_clinear (\<lambda>x. f x - g x)
[PROOF STEP]
by (auto simp: algebra_simps)


[STATEMENT]
lemma bounded_clinear_sum:
  fixes f :: "'i \<Rightarrow> 'a::complex_normed_vector \<Rightarrow> 'b::complex_normed_vector"
  shows "(\<And>i. i \<in> I \<Longrightarrow> bounded_clinear (f i)) \<Longrightarrow> bounded_clinear (\<lambda>x. \<Sum>i\<in>I. f i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. i \<in> I \<Longrightarrow> bounded_clinear (f i)) \<Longrightarrow> bounded_clinear (\<lambda>x. \<Sum>i\<in>I. f i x)
[PROOF STEP]
by (induct I rule: infinite_finite_induct) (auto intro!: bounded_clinear_add)