[STATEMENT]
lemma homotopic_paths_part_circlepath:
  assumes "a \<le> b" "b \<le> c"
  assumes "path_image (part_circlepath C r a c) \<subseteq> A" "r \<ge> 0"
  shows   "homotopic_paths A (part_circlepath C r a c)
             (part_circlepath C r a b +++ part_circlepath C r b c)"
  (is "homotopic_paths _ ?g (?h1 +++ ?h2)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
[PROOF STEP]
proof (cases "a = c")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = c \<Longrightarrow> homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
 2. a \<noteq> c \<Longrightarrow> homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> c

goal (2 subgoals):
 1. a = c \<Longrightarrow> homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
 2. a \<noteq> c \<Longrightarrow> homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
a \<le> b
b \<le> c
path_image (part_circlepath C r a c) \<subseteq> A
0 \<le> r
a \<noteq> c
[PROOF STEP]
have "a < c"
[PROOF STATE]
proof (prove)
using this:
a \<le> b
b \<le> c
path_image (part_circlepath C r a c) \<subseteq> A
0 \<le> r
a \<noteq> c

goal (1 subgoal):
 1. a < c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a < c

goal (2 subgoals):
 1. a = c \<Longrightarrow> homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
 2. a \<noteq> c \<Longrightarrow> homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
[PROOF STEP]
define slope where "slope = (b - a) / (c - a)"
[PROOF STATE]
proof (state)
this:
slope = (b - a) / (c - a)

goal (2 subgoals):
 1. a = c \<Longrightarrow> homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
 2. a \<noteq> c \<Longrightarrow> homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
[PROOF STEP]
from assms and \<open>a < c\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<le> b
b \<le> c
path_image (part_circlepath C r a c) \<subseteq> A
0 \<le> r
a < c
[PROOF STEP]
have slope: "slope \<in> {0..1}"
[PROOF STATE]
proof (prove)
using this:
a \<le> b
b \<le> c
path_image (part_circlepath C r a c) \<subseteq> A
0 \<le> r
a < c

goal (1 subgoal):
 1. slope \<in> {0..1}
[PROOF STEP]
by (auto simp: field_simps slope_def)
[PROOF STATE]
proof (state)
this:
slope \<in> {0..1}

goal (2 subgoals):
 1. a = c \<Longrightarrow> homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
 2. a \<noteq> c \<Longrightarrow> homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
[PROOF STEP]
define f :: "real \<Rightarrow> real" where
    "f = linepath 0 slope +++ linepath slope 1"
[PROOF STATE]
proof (state)
this:
f = linepath 0 slope +++ linepath slope 1

goal (2 subgoals):
 1. a = c \<Longrightarrow> homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
 2. a \<noteq> c \<Longrightarrow> homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
[PROOF STEP]
proof (rule homotopic_paths_reparametrize)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. path (part_circlepath C r a c)
 2. path_image (part_circlepath C r a c) \<subseteq> A
 3. continuous_on {0..1} ?f
 4. ?f ` {0..1} \<subseteq> {0..1}
 5. ?f 0 = 0
 6. ?f 1 = 1
 7. \<And>t. t \<in> {0..1} \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (?f t)
[PROOF STEP]
fix t :: real
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. path (part_circlepath C r a c)
 2. path_image (part_circlepath C r a c) \<subseteq> A
 3. continuous_on {0..1} ?f
 4. ?f ` {0..1} \<subseteq> {0..1}
 5. ?f 0 = 0
 6. ?f 1 = 1
 7. \<And>t. t \<in> {0..1} \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (?f t)
[PROOF STEP]
assume t: "t \<in> {0..1}"
[PROOF STATE]
proof (state)
this:
t \<in> {0..1}

goal (7 subgoals):
 1. path (part_circlepath C r a c)
 2. path_image (part_circlepath C r a c) \<subseteq> A
 3. continuous_on {0..1} ?f
 4. ?f ` {0..1} \<subseteq> {0..1}
 5. ?f 0 = 0
 6. ?f 1 = 1
 7. \<And>t. t \<in> {0..1} \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (?f t)
[PROOF STEP]
show "(?h1 +++ ?h2) t = ?g (f t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
proof (cases "t \<le> 1 / 2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
 2. \<not> t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
t \<le> 1 / 2

goal (2 subgoals):
 1. t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
 2. \<not> t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
hence "?g (f t) = C + r * cis ((1 - f t) * a + f t * c)"
[PROOF STATE]
proof (prove)
using this:
t \<le> 1 / 2

goal (1 subgoal):
 1. part_circlepath C r a c (f t) = C + complex_of_real r * cis ((1 - f t) * a + f t * c)
[PROOF STEP]
by (simp add: joinpaths_def part_circlepath_def exp_eq_polar linepath_def)
[PROOF STATE]
proof (state)
this:
part_circlepath C r a c (f t) = C + complex_of_real r * cis ((1 - f t) * a + f t * c)

goal (2 subgoals):
 1. t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
 2. \<not> t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
part_circlepath C r a c (f t) = C + complex_of_real r * cis ((1 - f t) * a + f t * c)

goal (2 subgoals):
 1. t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
 2. \<not> t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
from True \<open>a < c\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<le> 1 / 2
a < c
[PROOF STEP]
have "(1 - f t) * a + f t * c = (1 - 2 * t) * a + 2 * t * b"
[PROOF STATE]
proof (prove)
using this:
t \<le> 1 / 2
a < c

goal (1 subgoal):
 1. (1 - f t) * a + f t * c = (1 - 2 * t) * a + 2 * t * b
[PROOF STEP]
unfolding f_def slope_def linepath_def joinpaths_def
[PROOF STATE]
proof (prove)
using this:
t \<le> 1 / 2
a < c

goal (1 subgoal):
 1. (1 - (if t \<le> 1 / 2 then (1 - 2 * t) *\<^sub>R 0 + (2 * t) *\<^sub>R ((b - a) / (c - a)) else (1 - (2 * t - 1)) *\<^sub>R ((b - a) / (c - a)) + (2 * t - 1) *\<^sub>R 1)) * a + (if t \<le> 1 / 2 then (1 - 2 * t) *\<^sub>R 0 + (2 * t) *\<^sub>R ((b - a) / (c - a)) else (1 - (2 * t - 1)) *\<^sub>R ((b - a) / (c - a)) + (2 * t - 1) *\<^sub>R 1) * c = (1 - 2 * t) * a + 2 * t * b
[PROOF STEP]
by (simp add: divide_simps del: div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1)
           (simp add: algebra_simps)?
[PROOF STATE]
proof (state)
this:
(1 - f t) * a + f t * c = (1 - 2 * t) * a + 2 * t * b

goal (2 subgoals):
 1. t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
 2. \<not> t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1 - f t) * a + f t * c = (1 - 2 * t) * a + 2 * t * b

goal (2 subgoals):
 1. t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
 2. \<not> t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
t \<le> 1 / 2
[PROOF STEP]
have "C + r * cis \<dots> = (?h1 +++ ?h2) t"
[PROOF STATE]
proof (prove)
using this:
t \<le> 1 / 2

goal (1 subgoal):
 1. C + complex_of_real r * cis ((1 - 2 * t) * a + 2 * t * b) = (part_circlepath C r a b +++ part_circlepath C r b c) t
[PROOF STEP]
by (simp add: joinpaths_def part_circlepath_def exp_eq_polar linepath_def)
[PROOF STATE]
proof (state)
this:
C + complex_of_real r * cis ((1 - 2 * t) * a + 2 * t * b) = (part_circlepath C r a b +++ part_circlepath C r b c) t

goal (2 subgoals):
 1. t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
 2. \<not> t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
part_circlepath C r a c (f t) = (part_circlepath C r a b +++ part_circlepath C r b c) t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
part_circlepath C r a c (f t) = (part_circlepath C r a b +++ part_circlepath C r b c) t

goal (1 subgoal):
 1. (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)

goal (1 subgoal):
 1. \<not> t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> t \<le> 1 / 2

goal (1 subgoal):
 1. \<not> t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
hence "?g (f t) = C + r * cis ((1 - f t) * a + f t * c)"
[PROOF STATE]
proof (prove)
using this:
\<not> t \<le> 1 / 2

goal (1 subgoal):
 1. part_circlepath C r a c (f t) = C + complex_of_real r * cis ((1 - f t) * a + f t * c)
[PROOF STEP]
by (simp add: joinpaths_def part_circlepath_def exp_eq_polar linepath_def)
[PROOF STATE]
proof (state)
this:
part_circlepath C r a c (f t) = C + complex_of_real r * cis ((1 - f t) * a + f t * c)

goal (1 subgoal):
 1. \<not> t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
part_circlepath C r a c (f t) = C + complex_of_real r * cis ((1 - f t) * a + f t * c)

goal (1 subgoal):
 1. \<not> t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
from False \<open>a < c\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> t \<le> 1 / 2
a < c
[PROOF STEP]
have "(1 - f t) * a + f t * c = (2 - 2 * t) * b + (2 * t - 1) * c"
[PROOF STATE]
proof (prove)
using this:
\<not> t \<le> 1 / 2
a < c

goal (1 subgoal):
 1. (1 - f t) * a + f t * c = (2 - 2 * t) * b + (2 * t - 1) * c
[PROOF STEP]
unfolding f_def slope_def linepath_def joinpaths_def
[PROOF STATE]
proof (prove)
using this:
\<not> t \<le> 1 / 2
a < c

goal (1 subgoal):
 1. (1 - (if t \<le> 1 / 2 then (1 - 2 * t) *\<^sub>R 0 + (2 * t) *\<^sub>R ((b - a) / (c - a)) else (1 - (2 * t - 1)) *\<^sub>R ((b - a) / (c - a)) + (2 * t - 1) *\<^sub>R 1)) * a + (if t \<le> 1 / 2 then (1 - 2 * t) *\<^sub>R 0 + (2 * t) *\<^sub>R ((b - a) / (c - a)) else (1 - (2 * t - 1)) *\<^sub>R ((b - a) / (c - a)) + (2 * t - 1) *\<^sub>R 1) * c = (2 - 2 * t) * b + (2 * t - 1) * c
[PROOF STEP]
by (simp add: divide_simps del: div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1)
           (simp add: algebra_simps)?
[PROOF STATE]
proof (state)
this:
(1 - f t) * a + f t * c = (2 - 2 * t) * b + (2 * t - 1) * c

goal (1 subgoal):
 1. \<not> t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1 - f t) * a + f t * c = (2 - 2 * t) * b + (2 * t - 1) * c

goal (1 subgoal):
 1. \<not> t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
\<not> t \<le> 1 / 2
[PROOF STEP]
have "C + r * cis \<dots> = (?h1 +++ ?h2) t"
[PROOF STATE]
proof (prove)
using this:
\<not> t \<le> 1 / 2

goal (1 subgoal):
 1. C + complex_of_real r * cis ((2 - 2 * t) * b + (2 * t - 1) * c) = (part_circlepath C r a b +++ part_circlepath C r b c) t
[PROOF STEP]
by (simp add: joinpaths_def part_circlepath_def exp_eq_polar linepath_def)
[PROOF STATE]
proof (state)
this:
C + complex_of_real r * cis ((2 - 2 * t) * b + (2 * t - 1) * c) = (part_circlepath C r a b +++ part_circlepath C r b c) t

goal (1 subgoal):
 1. \<not> t \<le> 1 / 2 \<Longrightarrow> (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
part_circlepath C r a c (f t) = (part_circlepath C r a b +++ part_circlepath C r b c) t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
part_circlepath C r a c (f t) = (part_circlepath C r a b +++ part_circlepath C r b c) t

goal (1 subgoal):
 1. (part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(part_circlepath C r a b +++ part_circlepath C r b c) t = part_circlepath C r a c (f t)

goal (6 subgoals):
 1. path (part_circlepath C r a c)
 2. path_image (part_circlepath C r a c) \<subseteq> A
 3. continuous_on {0..1} f
 4. f ` {0..1} \<subseteq> {0..1}
 5. f 0 = 0
 6. f 1 = 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. path (part_circlepath C r a c)
 2. path_image (part_circlepath C r a c) \<subseteq> A
 3. continuous_on {0..1} f
 4. f ` {0..1} \<subseteq> {0..1}
 5. f 0 = 0
 6. f 1 = 1
[PROOF STEP]
from slope
[PROOF STATE]
proof (chain)
picking this:
slope \<in> {0..1}
[PROOF STEP]
have "path_image f \<subseteq> {0..1}"
[PROOF STATE]
proof (prove)
using this:
slope \<in> {0..1}

goal (1 subgoal):
 1. path_image f \<subseteq> {0..1}
[PROOF STEP]
by (auto simp: f_def path_image_join closed_segment_eq_real_ivl)
[PROOF STATE]
proof (state)
this:
path_image f \<subseteq> {0..1}

goal (6 subgoals):
 1. path (part_circlepath C r a c)
 2. path_image (part_circlepath C r a c) \<subseteq> A
 3. continuous_on {0..1} f
 4. f ` {0..1} \<subseteq> {0..1}
 5. f 0 = 0
 6. f 1 = 1
[PROOF STEP]
thus "f ` {0..1} \<subseteq> {0..1}"
[PROOF STATE]
proof (prove)
using this:
path_image f \<subseteq> {0..1}

goal (1 subgoal):
 1. f ` {0..1} \<subseteq> {0..1}
[PROOF STEP]
by (simp add: path_image_def)
[PROOF STATE]
proof (state)
this:
f ` {0..1} \<subseteq> {0..1}

goal (5 subgoals):
 1. path (part_circlepath C r a c)
 2. path_image (part_circlepath C r a c) \<subseteq> A
 3. continuous_on {0..1} f
 4. f 0 = 0
 5. f 1 = 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. path (part_circlepath C r a c)
 2. path_image (part_circlepath C r a c) \<subseteq> A
 3. continuous_on {0..1} f
 4. f 0 = 0
 5. f 1 = 1
[PROOF STEP]
have "path f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path f
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (linepath 0 slope +++ linepath slope 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path f

goal (5 subgoals):
 1. path (part_circlepath C r a c)
 2. path_image (part_circlepath C r a c) \<subseteq> A
 3. continuous_on {0..1} f
 4. f 0 = 0
 5. f 1 = 1
[PROOF STEP]
thus "continuous_on {0..1} f"
[PROOF STATE]
proof (prove)
using this:
path f

goal (1 subgoal):
 1. continuous_on {0..1} f
[PROOF STEP]
by (simp add: path_def)
[PROOF STATE]
proof (state)
this:
continuous_on {0..1} f

goal (4 subgoals):
 1. path (part_circlepath C r a c)
 2. path_image (part_circlepath C r a c) \<subseteq> A
 3. f 0 = 0
 4. f 1 = 1
[PROOF STEP]
qed (insert assms, auto simp: f_def joinpaths_def linepath_def)
[PROOF STATE]
proof (state)
this:
homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)

goal (1 subgoal):
 1. a = c \<Longrightarrow> homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = c \<Longrightarrow> homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
[PROOF STEP]
case [simp]: True
[PROOF STATE]
proof (state)
this:
a = c

goal (1 subgoal):
 1. a = c \<Longrightarrow> homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
a \<le> b
b \<le> c
path_image (part_circlepath C r a c) \<subseteq> A
0 \<le> r
a = c
[PROOF STEP]
have [simp]: "b = c"
[PROOF STATE]
proof (prove)
using this:
a \<le> b
b \<le> c
path_image (part_circlepath C r a c) \<subseteq> A
0 \<le> r
a = c

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

goal (1 subgoal):
 1. a = c \<Longrightarrow> homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
[PROOF STEP]
have "part_circlepath C r c c +++ part_circlepath C r c c = part_circlepath C r c c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. part_circlepath C r c c +++ part_circlepath C r c c = part_circlepath C r c c
[PROOF STEP]
by (simp add: fun_eq_iff joinpaths_def part_circlepath_def)
[PROOF STATE]
proof (state)
this:
part_circlepath C r c c +++ part_circlepath C r c c = part_circlepath C r c c

goal (1 subgoal):
 1. a = c \<Longrightarrow> homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
part_circlepath C r c c +++ part_circlepath C r c c = part_circlepath C r c c

goal (1 subgoal):
 1. homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
part_circlepath C r c c +++ part_circlepath C r c c = part_circlepath C r c c
a \<le> b
b \<le> c
path_image (part_circlepath C r a c) \<subseteq> A
0 \<le> r

goal (1 subgoal):
 1. homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma has_contour_integral_mirror_iff:
  assumes "valid_path g"
  shows   "(f has_contour_integral I) (-g) \<longleftrightarrow> ((\<lambda>x. -f (- x)) has_contour_integral I) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f has_contour_integral I) (- g) = ((\<lambda>x. - f (- x)) has_contour_integral I) g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (f has_contour_integral I) (- g) = ((\<lambda>x. - f (- x)) has_contour_integral I) g
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
valid_path g
[PROOF STEP]
have "g piecewise_differentiable_on {0..1}"
[PROOF STATE]
proof (prove)
using this:
valid_path g

goal (1 subgoal):
 1. g piecewise_differentiable_on {0..1}
[PROOF STEP]
by (auto simp: valid_path_def piecewise_C1_imp_differentiable)
[PROOF STATE]
proof (state)
this:
g piecewise_differentiable_on {0..1}

goal (1 subgoal):
 1. (f has_contour_integral I) (- g) = ((\<lambda>x. - f (- x)) has_contour_integral I) g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g piecewise_differentiable_on {0..1}
[PROOF STEP]
obtain S where S: "finite S" "\<And>x. x \<in> {0..1} - S \<Longrightarrow> g differentiable at x within {0..1}"
[PROOF STATE]
proof (prove)
using this:
g piecewise_differentiable_on {0..1}

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>finite S; \<And>x. x \<in> {0..1} - S \<Longrightarrow> g differentiable at x within {0..1}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding piecewise_differentiable_on_def
[PROOF STATE]
proof (prove)
using this:
continuous_on {0..1} g \<and> (\<exists>S. finite S \<and> (\<forall>x\<in>{0..1} - S. g differentiable at x within {0..1}))

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>finite S; \<And>x. x \<in> {0..1} - S \<Longrightarrow> g differentiable at x within {0..1}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite S
?x \<in> {0..1} - S \<Longrightarrow> g differentiable at ?x within {0..1}

goal (1 subgoal):
 1. (f has_contour_integral I) (- g) = ((\<lambda>x. - f (- x)) has_contour_integral I) g
[PROOF STEP]
have S': "g differentiable at x" if "x \<in> {0..1} - ({0, 1} \<union> S)" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g differentiable at x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g differentiable at x
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
x \<in> {0..1} - ({0, 1} \<union> S)
[PROOF STEP]
have "x \<in> interior {0..1}"
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..1} - ({0, 1} \<union> S)

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

goal (1 subgoal):
 1. g differentiable at x
[PROOF STEP]
with S(2)[of x] that
[PROOF STATE]
proof (chain)
picking this:
x \<in> {0..1} - S \<Longrightarrow> g differentiable at x within {0..1}
x \<in> {0..1} - ({0, 1} \<union> S)
x \<in> interior {0..1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..1} - S \<Longrightarrow> g differentiable at x within {0..1}
x \<in> {0..1} - ({0, 1} \<union> S)
x \<in> interior {0..1}

goal (1 subgoal):
 1. g differentiable at x
[PROOF STEP]
by (auto simp: at_within_interior[of _ "{0..1}"])
[PROOF STATE]
proof (state)
this:
g differentiable at x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> {0..1} - ({0, 1} \<union> S) \<Longrightarrow> g differentiable at ?x

goal (1 subgoal):
 1. (f has_contour_integral I) (- g) = ((\<lambda>x. - f (- x)) has_contour_integral I) g
[PROOF STEP]
have "(f has_contour_integral I) (-g) \<longleftrightarrow>
          ((\<lambda>x. f (- g x) * vector_derivative (-g) (at x)) has_integral I) {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f has_contour_integral I) (- g) = ((\<lambda>x. f (- g x) * vector_derivative (- g) (at x)) has_integral I) {0..1}
[PROOF STEP]
by (simp add: has_contour_integral)
[PROOF STATE]
proof (state)
this:
(f has_contour_integral I) (- g) = ((\<lambda>x. f (- g x) * vector_derivative (- g) (at x)) has_integral I) {0..1}

goal (1 subgoal):
 1. (f has_contour_integral I) (- g) = ((\<lambda>x. - f (- x)) has_contour_integral I) g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f has_contour_integral I) (- g) = ((\<lambda>x. f (- g x) * vector_derivative (- g) (at x)) has_integral I) {0..1}

goal (1 subgoal):
 1. (f has_contour_integral I) (- g) = ((\<lambda>x. - f (- x)) has_contour_integral I) g
[PROOF STEP]
have "\<dots> \<longleftrightarrow> ((\<lambda>x. -f (- g x) * vector_derivative g (at x)) has_integral I) {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f (- g x) * vector_derivative (- g) (at x)) has_integral I) {0..1} = ((\<lambda>x. - f (- g x) * vector_derivative g (at x)) has_integral I) {0..1}
[PROOF STEP]
by (intro has_integral_spike_finite_eq[of "S \<union> {0, 1}"])
       (insert \<open>finite S\<close> S', auto simp: o_def fun_Compl_def)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (- g x) * vector_derivative (- g) (at x)) has_integral I) {0..1} = ((\<lambda>x. - f (- g x) * vector_derivative g (at x)) has_integral I) {0..1}

goal (1 subgoal):
 1. (f has_contour_integral I) (- g) = ((\<lambda>x. - f (- x)) has_contour_integral I) g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (- g x) * vector_derivative (- g) (at x)) has_integral I) {0..1} = ((\<lambda>x. - f (- g x) * vector_derivative g (at x)) has_integral I) {0..1}

goal (1 subgoal):
 1. (f has_contour_integral I) (- g) = ((\<lambda>x. - f (- x)) has_contour_integral I) g
[PROOF STEP]
have "\<dots> \<longleftrightarrow> ((\<lambda>x. -f (-x)) has_contour_integral I) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. - f (- g x) * vector_derivative g (at x)) has_integral I) {0..1} = ((\<lambda>x. - f (- x)) has_contour_integral I) g
[PROOF STEP]
by (simp add: has_contour_integral)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. - f (- g x) * vector_derivative g (at x)) has_integral I) {0..1} = ((\<lambda>x. - f (- x)) has_contour_integral I) g

goal (1 subgoal):
 1. (f has_contour_integral I) (- g) = ((\<lambda>x. - f (- x)) has_contour_integral I) g
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(f has_contour_integral I) (- g) = ((\<lambda>x. - f (- x)) has_contour_integral I) g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(f has_contour_integral I) (- g) = ((\<lambda>x. - f (- x)) has_contour_integral I) g

goal (1 subgoal):
 1. (f has_contour_integral I) (- g) = ((\<lambda>x. - f (- x)) has_contour_integral I) g
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(f has_contour_integral I) (- g) = ((\<lambda>x. - f (- x)) has_contour_integral I) g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma contour_integral_on_mirror_iff:
  assumes "valid_path g"
  shows   "f contour_integrable_on (-g) \<longleftrightarrow> (\<lambda>x. -f (- x)) contour_integrable_on g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f contour_integrable_on - g) = ((\<lambda>x. - f (- x)) contour_integrable_on g)
[PROOF STEP]
by (auto simp: contour_integrable_on_def has_contour_integral_mirror_iff assms)


[STATEMENT]
lemma contour_integral_mirror:
  assumes "valid_path g"
  shows   "contour_integral (-g) f = contour_integral g (\<lambda>x. -f (- x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
[PROOF STEP]
proof (cases "f contour_integrable_on (-g)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f contour_integrable_on - g \<Longrightarrow> contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
 2. \<not> f contour_integrable_on - g \<Longrightarrow> contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
f contour_integrable_on - g

goal (2 subgoals):
 1. f contour_integrable_on - g \<Longrightarrow> contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
 2. \<not> f contour_integrable_on - g \<Longrightarrow> contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f contour_integrable_on - g
[PROOF STEP]
obtain I where I: "(f has_contour_integral I) (-g)"
[PROOF STATE]
proof (prove)
using this:
f contour_integrable_on - g

goal (1 subgoal):
 1. (\<And>I. (f has_contour_integral I) (- g) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: contour_integrable_on_def)
[PROOF STATE]
proof (state)
this:
(f has_contour_integral I) (- g)

goal (2 subgoals):
 1. f contour_integrable_on - g \<Longrightarrow> contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
 2. \<not> f contour_integrable_on - g \<Longrightarrow> contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f has_contour_integral I) (- g)

goal (2 subgoals):
 1. f contour_integrable_on - g \<Longrightarrow> contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
 2. \<not> f contour_integrable_on - g \<Longrightarrow> contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
[PROOF STEP]
note has_contour_integral_mirror_iff[OF assms]
[PROOF STATE]
proof (state)
this:
(?f has_contour_integral ?I) (- g) = ((\<lambda>x. - ?f (- x)) has_contour_integral ?I) g

goal (2 subgoals):
 1. f contour_integrable_on - g \<Longrightarrow> contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
 2. \<not> f contour_integrable_on - g \<Longrightarrow> contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. - f (- x)) has_contour_integral I) g
[PROOF STEP]
have "((\<lambda>x. - f (- x)) has_contour_integral I) g"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. - f (- x)) has_contour_integral I) g

goal (1 subgoal):
 1. ((\<lambda>x. - f (- x)) has_contour_integral I) g
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
((\<lambda>x. - f (- x)) has_contour_integral I) g

goal (2 subgoals):
 1. f contour_integrable_on - g \<Longrightarrow> contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
 2. \<not> f contour_integrable_on - g \<Longrightarrow> contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
[PROOF STEP]
with I
[PROOF STATE]
proof (chain)
picking this:
(f has_contour_integral I) (- g)
((\<lambda>x. - f (- x)) has_contour_integral I) g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(f has_contour_integral I) (- g)
((\<lambda>x. - f (- x)) has_contour_integral I) g

goal (1 subgoal):
 1. contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
[PROOF STEP]
using contour_integral_unique
[PROOF STATE]
proof (prove)
using this:
(f has_contour_integral I) (- g)
((\<lambda>x. - f (- x)) has_contour_integral I) g
(?f has_contour_integral ?i) ?g \<Longrightarrow> contour_integral ?g ?f = ?i

goal (1 subgoal):
 1. contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))

goal (1 subgoal):
 1. \<not> f contour_integrable_on - g \<Longrightarrow> contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> f contour_integrable_on - g \<Longrightarrow> contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> f contour_integrable_on - g

goal (1 subgoal):
 1. \<not> f contour_integrable_on - g \<Longrightarrow> contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
[PROOF STEP]
hence "\<not>(\<lambda>x. -f (-x)) contour_integrable_on g"
[PROOF STATE]
proof (prove)
using this:
\<not> f contour_integrable_on - g

goal (1 subgoal):
 1. \<not> (\<lambda>x. - f (- x)) contour_integrable_on g
[PROOF STEP]
by (auto simp: contour_integral_on_mirror_iff assms)
[PROOF STATE]
proof (state)
this:
\<not> (\<lambda>x. - f (- x)) contour_integrable_on g

goal (1 subgoal):
 1. \<not> f contour_integrable_on - g \<Longrightarrow> contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
[PROOF STEP]
from False and this
[PROOF STATE]
proof (chain)
picking this:
\<not> f contour_integrable_on - g
\<not> (\<lambda>x. - f (- x)) contour_integrable_on g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> f contour_integrable_on - g
\<not> (\<lambda>x. - f (- x)) contour_integrable_on g

goal (1 subgoal):
 1. contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))
[PROOF STEP]
by (simp add: not_integrable_contour_integral)
[PROOF STATE]
proof (state)
this:
contour_integral (- g) f = contour_integral g (\<lambda>x. - f (- x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma contour_integrable_neg_iff:
  "(\<lambda>x. -f x) contour_integrable_on g \<longleftrightarrow> f contour_integrable_on g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. - f x) contour_integrable_on g) = (f contour_integrable_on g)
[PROOF STEP]
using contour_integrable_neg[of f g] contour_integrable_neg[of "\<lambda>x. -f x" g]
[PROOF STATE]
proof (prove)
using this:
f contour_integrable_on g \<Longrightarrow> (\<lambda>x. - f x) contour_integrable_on g
(\<lambda>x. - f x) contour_integrable_on g \<Longrightarrow> (\<lambda>x. - (- f x)) contour_integrable_on g

goal (1 subgoal):
 1. ((\<lambda>x. - f x) contour_integrable_on g) = (f contour_integrable_on g)
[PROOF STEP]
by auto


[STATEMENT]
lemma contour_integral_neg:
  shows "contour_integral g (\<lambda>x. -f x) = -contour_integral g f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contour_integral g (\<lambda>x. - f x) = - contour_integral g f
[PROOF STEP]
proof (cases "f contour_integrable_on g")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f contour_integrable_on g \<Longrightarrow> contour_integral g (\<lambda>x. - f x) = - contour_integral g f
 2. \<not> f contour_integrable_on g \<Longrightarrow> contour_integral g (\<lambda>x. - f x) = - contour_integral g f
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
f contour_integrable_on g

goal (2 subgoals):
 1. f contour_integrable_on g \<Longrightarrow> contour_integral g (\<lambda>x. - f x) = - contour_integral g f
 2. \<not> f contour_integrable_on g \<Longrightarrow> contour_integral g (\<lambda>x. - f x) = - contour_integral g f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f contour_integrable_on g

goal (1 subgoal):
 1. contour_integral g (\<lambda>x. - f x) = - contour_integral g f
[PROOF STEP]
by (simp add: contour_integral_neg)
[PROOF STATE]
proof (state)
this:
contour_integral g (\<lambda>x. - f x) = - contour_integral g f

goal (1 subgoal):
 1. \<not> f contour_integrable_on g \<Longrightarrow> contour_integral g (\<lambda>x. - f x) = - contour_integral g f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> f contour_integrable_on g \<Longrightarrow> contour_integral g (\<lambda>x. - f x) = - contour_integral g f
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> f contour_integrable_on g

goal (1 subgoal):
 1. \<not> f contour_integrable_on g \<Longrightarrow> contour_integral g (\<lambda>x. - f x) = - contour_integral g f
[PROOF STEP]
hence "\<not>(\<lambda>x. -f x) contour_integrable_on g"
[PROOF STATE]
proof (prove)
using this:
\<not> f contour_integrable_on g

goal (1 subgoal):
 1. \<not> (\<lambda>x. - f x) contour_integrable_on g
[PROOF STEP]
by (simp add: contour_integrable_neg_iff)
[PROOF STATE]
proof (state)
this:
\<not> (\<lambda>x. - f x) contour_integrable_on g

goal (1 subgoal):
 1. \<not> f contour_integrable_on g \<Longrightarrow> contour_integral g (\<lambda>x. - f x) = - contour_integral g f
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> f contour_integrable_on g
\<not> (\<lambda>x. - f x) contour_integrable_on g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> f contour_integrable_on g
\<not> (\<lambda>x. - f x) contour_integrable_on g

goal (1 subgoal):
 1. contour_integral g (\<lambda>x. - f x) = - contour_integral g f
[PROOF STEP]
by (simp add: not_integrable_contour_integral)
[PROOF STATE]
proof (state)
this:
contour_integral g (\<lambda>x. - f x) = - contour_integral g f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma minus_cis: "-cis x = cis (x + pi)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - cis x = cis (x + pi)
[PROOF STEP]
by (simp add: complex_eq_iff)


[STATEMENT]
lemma path_image_part_circlepath_subset:
  assumes "a \<le> a'" "a' \<le> b'" "b' \<le> b"
  shows   "path_image (part_circlepath c r a' b') \<subseteq> path_image (part_circlepath c r a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_image (part_circlepath c r a' b') \<subseteq> path_image (part_circlepath c r a b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<le> a'
a' \<le> b'
b' \<le> b

goal (1 subgoal):
 1. path_image (part_circlepath c r a' b') \<subseteq> path_image (part_circlepath c r a b)
[PROOF STEP]
by (subst (1 2) path_image_part_circlepath) auto


[STATEMENT]
lemma part_circlepath_mirror:
  assumes "a' = a + pi + 2 * pi * of_int k" "b' = b + pi + 2 * pi * of_int k" "c' = -c"
  shows   "-part_circlepath c r a b = part_circlepath c' r a' b'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - part_circlepath c r a b = part_circlepath c' r a' b'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (- part_circlepath c r a b) x = part_circlepath c' r a' b' x
[PROOF STEP]
fix x :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (- part_circlepath c r a b) x = part_circlepath c' r a' b' x
[PROOF STEP]
have "part_circlepath c' r a' b' x = c' + r * cis (linepath a b x + pi + k * (2 * pi))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. part_circlepath c' r a' b' x = c' + complex_of_real r * cis (linepath a b x + pi + real_of_int k * (2 * pi))
[PROOF STEP]
by (simp add: part_circlepath_def exp_eq_polar assms linepath_translate_right mult_ac)
[PROOF STATE]
proof (state)
this:
part_circlepath c' r a' b' x = c' + complex_of_real r * cis (linepath a b x + pi + real_of_int k * (2 * pi))

goal (1 subgoal):
 1. \<And>x. (- part_circlepath c r a b) x = part_circlepath c' r a' b' x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
part_circlepath c' r a' b' x = c' + complex_of_real r * cis (linepath a b x + pi + real_of_int k * (2 * pi))

goal (1 subgoal):
 1. \<And>x. (- part_circlepath c r a b) x = part_circlepath c' r a' b' x
[PROOF STEP]
have "cis (linepath a b x + pi + k * (2 * pi)) = cis (linepath a b x + pi)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (linepath a b x + pi + real_of_int k * (2 * pi)) = cis (linepath a b x + pi)
[PROOF STEP]
by (rule cis.plus_of_int)
[PROOF STATE]
proof (state)
this:
cis (linepath a b x + pi + real_of_int k * (2 * pi)) = cis (linepath a b x + pi)

goal (1 subgoal):
 1. \<And>x. (- part_circlepath c r a b) x = part_circlepath c' r a' b' x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cis (linepath a b x + pi + real_of_int k * (2 * pi)) = cis (linepath a b x + pi)

goal (1 subgoal):
 1. \<And>x. (- part_circlepath c r a b) x = part_circlepath c' r a' b' x
[PROOF STEP]
have "\<dots> = -cis (linepath a b x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (linepath a b x + pi) = - cis (linepath a b x)
[PROOF STEP]
by (simp add: minus_cis)
[PROOF STATE]
proof (state)
this:
cis (linepath a b x + pi) = - cis (linepath a b x)

goal (1 subgoal):
 1. \<And>x. (- part_circlepath c r a b) x = part_circlepath c' r a' b' x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cis (linepath a b x + pi) = - cis (linepath a b x)

goal (1 subgoal):
 1. \<And>x. (- part_circlepath c r a b) x = part_circlepath c' r a' b' x
[PROOF STEP]
have "c' + r * \<dots> = -part_circlepath c r a b x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c' + complex_of_real r * - cis (linepath a b x) = - part_circlepath c r a b x
[PROOF STEP]
by (simp add: part_circlepath_def assms exp_eq_polar)
[PROOF STATE]
proof (state)
this:
c' + complex_of_real r * - cis (linepath a b x) = - part_circlepath c r a b x

goal (1 subgoal):
 1. \<And>x. (- part_circlepath c r a b) x = part_circlepath c' r a' b' x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
part_circlepath c' r a' b' x = - part_circlepath c r a b x
[PROOF STEP]
show "(- part_circlepath c r a b) x = part_circlepath c' r a' b' x"
[PROOF STATE]
proof (prove)
using this:
part_circlepath c' r a' b' x = - part_circlepath c r a b x

goal (1 subgoal):
 1. (- part_circlepath c r a b) x = part_circlepath c' r a' b' x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(- part_circlepath c r a b) x = part_circlepath c' r a' b' x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_mirror [intro]: "path (g :: _ \<Rightarrow> 'b::topological_group_add) \<Longrightarrow> path (-g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path g \<Longrightarrow> path (- g)
[PROOF STEP]
by (auto simp: path_def intro!: continuous_intros)


[STATEMENT]
lemma path_mirror_iff [simp]: "path (-g :: _ \<Rightarrow> 'b::topological_group_add) \<longleftrightarrow> path g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (- g) = path g
[PROOF STEP]
using path_mirror[of g] path_mirror[of "-g"]
[PROOF STATE]
proof (prove)
using this:
path g \<Longrightarrow> path (- g)
path (- g) \<Longrightarrow> path (- (- g))

goal (1 subgoal):
 1. path (- g) = path g
[PROOF STEP]
by (auto simp: fun_Compl_def)


[STATEMENT]
lemma valid_path_mirror [intro]: "valid_path g \<Longrightarrow> valid_path (-g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path g \<Longrightarrow> valid_path (- g)
[PROOF STEP]
by (auto simp: valid_path_def fun_Compl_def piecewise_C1_differentiable_neg)


[STATEMENT]
lemma valid_path_mirror_iff [simp]: "valid_path (-g) \<longleftrightarrow> valid_path g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (- g) = valid_path g
[PROOF STEP]
using valid_path_mirror[of g] valid_path_mirror[of "-g"]
[PROOF STATE]
proof (prove)
using this:
valid_path g \<Longrightarrow> valid_path (- g)
valid_path (- g) \<Longrightarrow> valid_path (- (- g))

goal (1 subgoal):
 1. valid_path (- g) = valid_path g
[PROOF STEP]
by (auto simp: fun_Compl_def)


[STATEMENT]
lemma pathstart_mirror [simp]: "pathstart (-g) = -pathstart g"
  and pathfinish_mirror [simp]: "pathfinish (-g) = -pathfinish g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pathstart (- g) = - pathstart g &&& pathfinish (- g) = - pathfinish g
[PROOF STEP]
by (simp_all add: pathstart_def pathfinish_def)


[STATEMENT]
lemma path_image_mirror: "path_image (-g) = uminus ` path_image g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_image (- g) = uminus ` path_image g
[PROOF STEP]
by (auto simp: path_image_def)


[STATEMENT]
lemma contour_integral_bound_part_circlepath:
  assumes "f contour_integrable_on part_circlepath c r a b"
  assumes "B \<ge> 0" "r \<ge> 0" "\<And>x. x \<in> path_image (part_circlepath c r a b) \<Longrightarrow> norm (f x) \<le> B"
  shows   "norm (contour_integral (part_circlepath c r a b) f) \<le> B * r * \<bar>b - a\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (contour_integral (part_circlepath c r a b) f) \<le> B * r * \<bar>b - a\<bar>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod (contour_integral (part_circlepath c r a b) f) \<le> B * r * \<bar>b - a\<bar>
[PROOF STEP]
let ?I = "integral {0..1} (\<lambda>x. f (part_circlepath c r a b x) * \<i> * of_real (r * (b - a)) *
              exp (\<i> * linepath a b x))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod (contour_integral (part_circlepath c r a b) f) \<le> B * r * \<bar>b - a\<bar>
[PROOF STEP]
have "norm ?I \<le> integral {0..1} (\<lambda>x::real. B * 1 * (r * \<bar>b - a\<bar>) * 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (integral {0..1} (\<lambda>x. f (part_circlepath c r a b x) * \<i> * complex_of_real (r * (b - a)) * exp (\<i> * complex_of_real (linepath a b x)))) \<le> integral {0..1} (\<lambda>x. B * 1 * (r * \<bar>b - a\<bar>) * 1)
[PROOF STEP]
proof (rule integral_norm_bound_integral, goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (\<lambda>x. f (part_circlepath c r a b x) * \<i> * complex_of_real (r * (b - a)) * exp (\<i> * complex_of_real (linepath a b x))) integrable_on {0..1}
 2. (\<lambda>x. B * 1 * (r * \<bar>b - a\<bar>) * 1) integrable_on {0..1}
 3. \<And>x. x \<in> {0..1} \<Longrightarrow> cmod (f (part_circlepath c r a b x) * \<i> * complex_of_real (r * (b - a)) * exp (\<i> * complex_of_real (linepath a b x))) \<le> B * 1 * (r * \<bar>b - a\<bar>) * 1
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. (\<lambda>x. f (part_circlepath c r a b x) * \<i> * complex_of_real (r * (b - a)) * exp (\<i> * complex_of_real (linepath a b x))) integrable_on {0..1}
 2. (\<lambda>x. B * 1 * (r * \<bar>b - a\<bar>) * 1) integrable_on {0..1}
 3. \<And>x. x \<in> {0..1} \<Longrightarrow> cmod (f (part_circlepath c r a b x) * \<i> * complex_of_real (r * (b - a)) * exp (\<i> * complex_of_real (linepath a b x))) \<le> B * 1 * (r * \<bar>b - a\<bar>) * 1
[PROOF STEP]
with assms(1)
[PROOF STATE]
proof (chain)
picking this:
f contour_integrable_on part_circlepath c r a b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
f contour_integrable_on part_circlepath c r a b

goal (1 subgoal):
 1. (\<lambda>x. f (part_circlepath c r a b x) * \<i> * complex_of_real (r * (b - a)) * exp (\<i> * complex_of_real (linepath a b x))) integrable_on {0..1}
[PROOF STEP]
by (simp add: contour_integrable_on vector_derivative_part_circlepath mult_ac)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f (part_circlepath c r a b x) * \<i> * complex_of_real (r * (b - a)) * exp (\<i> * complex_of_real (linepath a b x))) integrable_on {0..1}

goal (2 subgoals):
 1. (\<lambda>x. B * 1 * (r * \<bar>b - a\<bar>) * 1) integrable_on {0..1}
 2. \<And>x. x \<in> {0..1} \<Longrightarrow> cmod (f (part_circlepath c r a b x) * \<i> * complex_of_real (r * (b - a)) * exp (\<i> * complex_of_real (linepath a b x))) \<le> B * 1 * (r * \<bar>b - a\<bar>) * 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>x. B * 1 * (r * \<bar>b - a\<bar>) * 1) integrable_on {0..1}
 2. \<And>x. x \<in> {0..1} \<Longrightarrow> cmod (f (part_circlepath c r a b x) * \<i> * complex_of_real (r * (b - a)) * exp (\<i> * complex_of_real (linepath a b x))) \<le> B * 1 * (r * \<bar>b - a\<bar>) * 1
[PROOF STEP]
case (3 x)
[PROOF STATE]
proof (state)
this:
x \<in> {0..1}

goal (2 subgoals):
 1. (\<lambda>x. B * 1 * (r * \<bar>b - a\<bar>) * 1) integrable_on {0..1}
 2. \<And>x. x \<in> {0..1} \<Longrightarrow> cmod (f (part_circlepath c r a b x) * \<i> * complex_of_real (r * (b - a)) * exp (\<i> * complex_of_real (linepath a b x))) \<le> B * 1 * (r * \<bar>b - a\<bar>) * 1
[PROOF STEP]
with assms(2-)
[PROOF STATE]
proof (chain)
picking this:
0 \<le> B
0 \<le> r
?x \<in> path_image (part_circlepath c r a b) \<Longrightarrow> cmod (f ?x) \<le> B
x \<in> {0..1}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 \<le> B
0 \<le> r
?x \<in> path_image (part_circlepath c r a b) \<Longrightarrow> cmod (f ?x) \<le> B
x \<in> {0..1}

goal (1 subgoal):
 1. cmod (f (part_circlepath c r a b x) * \<i> * complex_of_real (r * (b - a)) * exp (\<i> * complex_of_real (linepath a b x))) \<le> B * 1 * (r * \<bar>b - a\<bar>) * 1
[PROOF STEP]
unfolding norm_mult norm_of_real abs_mult
[PROOF STATE]
proof (prove)
using this:
0 \<le> B
0 \<le> r
?x \<in> path_image (part_circlepath c r a b) \<Longrightarrow> cmod (f ?x) \<le> B
x \<in> {0..1}

goal (1 subgoal):
 1. cmod (f (part_circlepath c r a b x)) * cmod \<i> * (\<bar>r\<bar> * \<bar>b - a\<bar>) * cmod (exp (\<i> * complex_of_real (linepath a b x))) \<le> B * 1 * (r * \<bar>b - a\<bar>) * 1
[PROOF STEP]
by (intro mult_mono) (auto simp: path_image_def)
[PROOF STATE]
proof (state)
this:
cmod (f (part_circlepath c r a b x) * \<i> * complex_of_real (r * (b - a)) * exp (\<i> * complex_of_real (linepath a b x))) \<le> B * 1 * (r * \<bar>b - a\<bar>) * 1

goal (1 subgoal):
 1. (\<lambda>x. B * 1 * (r * \<bar>b - a\<bar>) * 1) integrable_on {0..1}
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
cmod (integral {0..1} (\<lambda>x. f (part_circlepath c r a b x) * \<i> * complex_of_real (r * (b - a)) * exp (\<i> * complex_of_real (linepath a b x)))) \<le> integral {0..1} (\<lambda>x. B * 1 * (r * \<bar>b - a\<bar>) * 1)

goal (1 subgoal):
 1. cmod (contour_integral (part_circlepath c r a b) f) \<le> B * r * \<bar>b - a\<bar>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod (integral {0..1} (\<lambda>x. f (part_circlepath c r a b x) * \<i> * complex_of_real (r * (b - a)) * exp (\<i> * complex_of_real (linepath a b x)))) \<le> integral {0..1} (\<lambda>x. B * 1 * (r * \<bar>b - a\<bar>) * 1)

goal (1 subgoal):
 1. cmod (contour_integral (part_circlepath c r a b) f) \<le> B * r * \<bar>b - a\<bar>
[PROOF STEP]
have "?I = contour_integral (part_circlepath c r a b) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. f (part_circlepath c r a b x) * \<i> * complex_of_real (r * (b - a)) * exp (\<i> * complex_of_real (linepath a b x))) = contour_integral (part_circlepath c r a b) f
[PROOF STEP]
by (simp add: contour_integral_integral vector_derivative_part_circlepath mult_ac)
[PROOF STATE]
proof (state)
this:
integral {0..1} (\<lambda>x. f (part_circlepath c r a b x) * \<i> * complex_of_real (r * (b - a)) * exp (\<i> * complex_of_real (linepath a b x))) = contour_integral (part_circlepath c r a b) f

goal (1 subgoal):
 1. cmod (contour_integral (part_circlepath c r a b) f) \<le> B * r * \<bar>b - a\<bar>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cmod (contour_integral (part_circlepath c r a b) f) \<le> integral {0..1} (\<lambda>x. B * 1 * (r * \<bar>b - a\<bar>) * 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cmod (contour_integral (part_circlepath c r a b) f) \<le> integral {0..1} (\<lambda>x. B * 1 * (r * \<bar>b - a\<bar>) * 1)

goal (1 subgoal):
 1. cmod (contour_integral (part_circlepath c r a b) f) \<le> B * r * \<bar>b - a\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cmod (contour_integral (part_circlepath c r a b) f) \<le> B * r * \<bar>b - a\<bar>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma contour_integral_spike_finite_simple_path:
  assumes "finite A" "simple_path g" "g = g'" "\<And>x. x \<in> path_image g - A \<Longrightarrow> f x = f' x"
  shows   "contour_integral g f = contour_integral g' f'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contour_integral g f = contour_integral g' f'
[PROOF STEP]
unfolding contour_integral_integral
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. f (g x) * vector_derivative g (at x)) = integral {0..1} (\<lambda>x. f' (g' x) * vector_derivative g' (at x))
[PROOF STEP]
proof (rule integral_spike)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. negligible ?S
 2. \<And>x. x \<in> {0..1} - ?S \<Longrightarrow> f' (g' x) * vector_derivative g' (at x) = f (g x) * vector_derivative g (at x)
[PROOF STEP]
have "finite (g -` A \<inter> {0<..<1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (g -` A \<inter> {0<..<1})
[PROOF STEP]
using \<open>simple_path g\<close> \<open>finite A\<close>
[PROOF STATE]
proof (prove)
using this:
simple_path g
finite A

goal (1 subgoal):
 1. finite (g -` A \<inter> {0<..<1})
[PROOF STEP]
by (intro finite_vimage_IntI simple_path_inj_on) auto
[PROOF STATE]
proof (state)
this:
finite (g -` A \<inter> {0<..<1})

goal (2 subgoals):
 1. negligible ?S
 2. \<And>x. x \<in> {0..1} - ?S \<Longrightarrow> f' (g' x) * vector_derivative g' (at x) = f (g x) * vector_derivative g (at x)
[PROOF STEP]
hence "finite ({0, 1} \<union> g -` A \<inter> {0<..<1})"
[PROOF STATE]
proof (prove)
using this:
finite (g -` A \<inter> {0<..<1})

goal (1 subgoal):
 1. finite ({0, 1} \<union> g -` A \<inter> {0<..<1})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite ({0, 1} \<union> g -` A \<inter> {0<..<1})

goal (2 subgoals):
 1. negligible ?S
 2. \<And>x. x \<in> {0..1} - ?S \<Longrightarrow> f' (g' x) * vector_derivative g' (at x) = f (g x) * vector_derivative g (at x)
[PROOF STEP]
thus "negligible ({0, 1} \<union> g -` A \<inter> {0<..<1})"
[PROOF STATE]
proof (prove)
using this:
finite ({0, 1} \<union> g -` A \<inter> {0<..<1})

goal (1 subgoal):
 1. negligible ({0, 1} \<union> g -` A \<inter> {0<..<1})
[PROOF STEP]
by (rule negligible_finite)
[PROOF STATE]
proof (state)
this:
negligible ({0, 1} \<union> g -` A \<inter> {0<..<1})

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - ({0, 1} \<union> g -` A \<inter> {0<..<1}) \<Longrightarrow> f' (g' x) * vector_derivative g' (at x) = f (g x) * vector_derivative g (at x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - ({0, 1} \<union> g -` A \<inter> {0<..<1}) \<Longrightarrow> f' (g' x) * vector_derivative g' (at x) = f (g x) * vector_derivative g (at x)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - ({0, 1} \<union> g -` A \<inter> {0<..<1}) \<Longrightarrow> f' (g' x) * vector_derivative g' (at x) = f (g x) * vector_derivative g (at x)
[PROOF STEP]
assume "x \<in> {0..1} - ({0, 1} \<union> g -` A \<inter> {0<..<1})"
[PROOF STATE]
proof (state)
this:
x \<in> {0..1} - ({0, 1} \<union> g -` A \<inter> {0<..<1})

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - ({0, 1} \<union> g -` A \<inter> {0<..<1}) \<Longrightarrow> f' (g' x) * vector_derivative g' (at x) = f (g x) * vector_derivative g (at x)
[PROOF STEP]
hence "g x \<in> path_image g - A"
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..1} - ({0, 1} \<union> g -` A \<inter> {0<..<1})

goal (1 subgoal):
 1. g x \<in> path_image g - A
[PROOF STEP]
by (auto simp: path_image_def)
[PROOF STATE]
proof (state)
this:
g x \<in> path_image g - A

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - ({0, 1} \<union> g -` A \<inter> {0<..<1}) \<Longrightarrow> f' (g' x) * vector_derivative g' (at x) = f (g x) * vector_derivative g (at x)
[PROOF STEP]
from assms(4)[OF this] and assms(3)
[PROOF STATE]
proof (chain)
picking this:
f (g x) = f' (g x)
g = g'
[PROOF STEP]
show "f' (g' x) * vector_derivative g' (at x) = f (g x) * vector_derivative g (at x)"
[PROOF STATE]
proof (prove)
using this:
f (g x) = f' (g x)
g = g'

goal (1 subgoal):
 1. f' (g' x) * vector_derivative g' (at x) = f (g x) * vector_derivative g (at x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f' (g' x) * vector_derivative g' (at x) = f (g x) * vector_derivative g (at x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cos_le_zero:
  assumes "x \<in> {pi/2..3*pi/2}"
  shows   "cos x \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cos x \<le> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cos x \<le> 0
[PROOF STEP]
have "cos x = -cos (x - pi)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cos x = - cos (x - pi)
[PROOF STEP]
by (simp add: cos_diff)
[PROOF STATE]
proof (state)
this:
cos x = - cos (x - pi)

goal (1 subgoal):
 1. cos x \<le> 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cos x = - cos (x - pi)

goal (1 subgoal):
 1. cos x \<le> 0
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x \<in> {pi / 2..3 * pi / 2}
[PROOF STEP]
have "cos (x - pi) \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
x \<in> {pi / 2..3 * pi / 2}

goal (1 subgoal):
 1. 0 \<le> cos (x - pi)
[PROOF STEP]
by (intro cos_ge_zero) auto
[PROOF STATE]
proof (state)
this:
0 \<le> cos (x - pi)

goal (1 subgoal):
 1. cos x \<le> 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cos x = - cos (x - pi)
0 \<le> cos (x - pi)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cos x = - cos (x - pi)
0 \<le> cos (x - pi)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cos_le_zero': "x \<in> {-3*pi/2..-pi/2} \<Longrightarrow> cos x \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {- 3 * pi / 2..- pi / 2} \<Longrightarrow> cos x \<le> 0
[PROOF STEP]
using cos_le_zero[of "-x"]
[PROOF STATE]
proof (prove)
using this:
- x \<in> {pi / 2..3 * pi / 2} \<Longrightarrow> cos (- x) \<le> 0

goal (1 subgoal):
 1. x \<in> {- 3 * pi / 2..- pi / 2} \<Longrightarrow> cos x \<le> 0
[PROOF STEP]
by simp


[STATEMENT]
lemma cis_minus_pi_half [simp]: "cis (- (pi / 2)) = -\<i>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (- (pi / 2)) = - \<i>
[PROOF STEP]
by (simp add: complex_eq_iff)


[STATEMENT]
lemma winding_number_join_pos_combined':
     "\<lbrakk>valid_path \<gamma>1 \<and> z \<notin> path_image \<gamma>1 \<and> 0 < Re (winding_number \<gamma>1 z);
       valid_path \<gamma>2 \<and> z \<notin> path_image \<gamma>2 \<and> 0 < Re (winding_number \<gamma>2 z);
       pathfinish \<gamma>1 = pathstart \<gamma>2\<rbrakk>
      \<Longrightarrow> valid_path(\<gamma>1 +++ \<gamma>2) \<and> z \<notin> path_image(\<gamma>1 +++ \<gamma>2) \<and> 0 < Re(winding_number(\<gamma>1 +++ \<gamma>2) z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_path \<gamma>1 \<and> z \<notin> path_image \<gamma>1 \<and> 0 < Re (winding_number \<gamma>1 z); valid_path \<gamma>2 \<and> z \<notin> path_image \<gamma>2 \<and> 0 < Re (winding_number \<gamma>2 z); pathfinish \<gamma>1 = pathstart \<gamma>2\<rbrakk> \<Longrightarrow> valid_path (\<gamma>1 +++ \<gamma>2) \<and> z \<notin> path_image (\<gamma>1 +++ \<gamma>2) \<and> 0 < Re (winding_number (\<gamma>1 +++ \<gamma>2) z)
[PROOF STEP]
by (simp add: valid_path_join path_image_join winding_number_join valid_path_imp_path)


[STATEMENT]
lemma Union_atLeastAtMost_real_of_nat:
  assumes "a < b"
  shows   "(\<Union>n\<in>{a..<b}. {real n..real (n + 1)}) = {real a..real b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>n\<in>{a..<b}. {real n..real (n + 1)}) = {real a..real b}
[PROOF STEP]
proof (intro equalityI subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)}) \<Longrightarrow> x \<in> {real a..real b}
 2. \<And>x. x \<in> {real a..real b} \<Longrightarrow> x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)}) \<Longrightarrow> x \<in> {real a..real b}
 2. \<And>x. x \<in> {real a..real b} \<Longrightarrow> x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
[PROOF STEP]
assume x: "x \<in> {real a..real b}"
[PROOF STATE]
proof (state)
this:
x \<in> {real a..real b}

goal (2 subgoals):
 1. \<And>x. x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)}) \<Longrightarrow> x \<in> {real a..real b}
 2. \<And>x. x \<in> {real a..real b} \<Longrightarrow> x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
[PROOF STEP]
thus "x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})"
[PROOF STATE]
proof (prove)
using this:
x \<in> {real a..real b}

goal (1 subgoal):
 1. x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
[PROOF STEP]
proof (cases "x = real b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x \<in> {real a..real b}; x = real b\<rbrakk> \<Longrightarrow> x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
 2. \<lbrakk>x \<in> {real a..real b}; x \<noteq> real b\<rbrakk> \<Longrightarrow> x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = real b

goal (2 subgoals):
 1. \<lbrakk>x \<in> {real a..real b}; x = real b\<rbrakk> \<Longrightarrow> x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
 2. \<lbrakk>x \<in> {real a..real b}; x \<noteq> real b\<rbrakk> \<Longrightarrow> x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
a < b
x = real b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a < b
x = real b

goal (1 subgoal):
 1. x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
[PROOF STEP]
by (auto intro!: bexI[of _ "b - 1"])
[PROOF STATE]
proof (state)
this:
x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})

goal (1 subgoal):
 1. \<lbrakk>x \<in> {real a..real b}; x \<noteq> real b\<rbrakk> \<Longrightarrow> x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<in> {real a..real b}; x \<noteq> real b\<rbrakk> \<Longrightarrow> x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> real b

goal (1 subgoal):
 1. \<lbrakk>x \<in> {real a..real b}; x \<noteq> real b\<rbrakk> \<Longrightarrow> x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
[PROOF STEP]
with x
[PROOF STATE]
proof (chain)
picking this:
x \<in> {real a..real b}
x \<noteq> real b
[PROOF STEP]
have x: "x \<ge> real a" "x < real b"
[PROOF STATE]
proof (prove)
using this:
x \<in> {real a..real b}
x \<noteq> real b

goal (1 subgoal):
 1. real a \<le> x &&& x < real b
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
real a \<le> x
x < real b

goal (1 subgoal):
 1. \<lbrakk>x \<in> {real a..real b}; x \<noteq> real b\<rbrakk> \<Longrightarrow> x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
[PROOF STEP]
hence "x \<ge> real (nat \<lfloor>x\<rfloor>)" "x \<le> real (Suc (nat \<lfloor>x\<rfloor>))"
[PROOF STATE]
proof (prove)
using this:
real a \<le> x
x < real b

goal (1 subgoal):
 1. real (nat \<lfloor>x\<rfloor>) \<le> x &&& x \<le> real (Suc (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
by linarith+
[PROOF STATE]
proof (state)
this:
real (nat \<lfloor>x\<rfloor>) \<le> x
x \<le> real (Suc (nat \<lfloor>x\<rfloor>))

goal (1 subgoal):
 1. \<lbrakk>x \<in> {real a..real b}; x \<noteq> real b\<rbrakk> \<Longrightarrow> x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
real (nat \<lfloor>x\<rfloor>) \<le> x
x \<le> real (Suc (nat \<lfloor>x\<rfloor>))

goal (1 subgoal):
 1. \<lbrakk>x \<in> {real a..real b}; x \<noteq> real b\<rbrakk> \<Longrightarrow> x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
real a \<le> x
x < real b
[PROOF STEP]
have "nat \<lfloor>x\<rfloor> \<ge> a" "nat \<lfloor>x\<rfloor> < b"
[PROOF STATE]
proof (prove)
using this:
real a \<le> x
x < real b

goal (1 subgoal):
 1. a \<le> nat \<lfloor>x\<rfloor> &&& nat \<lfloor>x\<rfloor> < b
[PROOF STEP]
by linarith+
[PROOF STATE]
proof (state)
this:
a \<le> nat \<lfloor>x\<rfloor>
nat \<lfloor>x\<rfloor> < b

goal (1 subgoal):
 1. \<lbrakk>x \<in> {real a..real b}; x \<noteq> real b\<rbrakk> \<Longrightarrow> x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
real (nat \<lfloor>x\<rfloor>) \<le> x
x \<le> real (Suc (nat \<lfloor>x\<rfloor>))
a \<le> nat \<lfloor>x\<rfloor>
nat \<lfloor>x\<rfloor> < b
[PROOF STEP]
have "\<exists>n\<in>{a..<b}. x \<in> {real n..real (n + 1)}"
[PROOF STATE]
proof (prove)
using this:
real (nat \<lfloor>x\<rfloor>) \<le> x
x \<le> real (Suc (nat \<lfloor>x\<rfloor>))
a \<le> nat \<lfloor>x\<rfloor>
nat \<lfloor>x\<rfloor> < b

goal (1 subgoal):
 1. \<exists>n\<in>{a..<b}. x \<in> {real n..real (n + 1)}
[PROOF STEP]
by (intro bexI[of _ "nat \<lfloor>x\<rfloor>"]) simp_all
[PROOF STATE]
proof (state)
this:
\<exists>n\<in>{a..<b}. x \<in> {real n..real (n + 1)}

goal (1 subgoal):
 1. \<lbrakk>x \<in> {real a..real b}; x \<noteq> real b\<rbrakk> \<Longrightarrow> x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>n\<in>{a..<b}. x \<in> {real n..real (n + 1)}

goal (1 subgoal):
 1. x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)})

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>n\<in>{a..<b}. {real n..real (n + 1)}) \<Longrightarrow> x \<in> {real a..real b}
[PROOF STEP]
qed auto


[STATEMENT]
lemma nat_sum_has_integral_floor:
  fixes f :: "nat \<Rightarrow> 'a :: banach"
  assumes mn: "m < n"
  shows "((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral sum f {m..<n}) {real m..real n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral sum f {m..<n}) {real m..real n}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral sum f {m..<n}) {real m..real n}
[PROOF STEP]
define D where "D = (\<lambda>i. {real i..real (Suc i)}) ` {m..<n}"
[PROOF STATE]
proof (state)
this:
D = (\<lambda>i. {real i..real (Suc i)}) ` {m..<n}

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral sum f {m..<n}) {real m..real n}
[PROOF STEP]
have D: "D division_of {m..n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D division_of {real m..real n}
[PROOF STEP]
using Union_atLeastAtMost_real_of_nat[OF mn]
[PROOF STATE]
proof (prove)
using this:
(\<Union>n\<in>{m..<n}. {real n..real (n + 1)}) = {real m..real n}

goal (1 subgoal):
 1. D division_of {real m..real n}
[PROOF STEP]
by (simp add: division_of_def D_def)
[PROOF STATE]
proof (state)
this:
D division_of {real m..real n}

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral sum f {m..<n}) {real m..real n}
[PROOF STEP]
have "((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral (\<Sum>X\<in>D. f (nat \<lfloor>Inf X\<rfloor>))) {real m..real n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral (\<Sum>X\<in>D. f (nat \<lfloor>Inf X\<rfloor>))) {real m..real n}
[PROOF STEP]
proof (rule has_integral_combine_division)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. D division_of {real m..real n}
 2. \<And>k. k \<in> D \<Longrightarrow> ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral f (nat \<lfloor>Inf k\<rfloor>)) k
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. D division_of {real m..real n}
 2. \<And>k. k \<in> D \<Longrightarrow> ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral f (nat \<lfloor>Inf k\<rfloor>)) k
[PROOF STEP]
assume X: "X \<in> D"
[PROOF STATE]
proof (state)
this:
X \<in> D

goal (2 subgoals):
 1. D division_of {real m..real n}
 2. \<And>k. k \<in> D \<Longrightarrow> ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral f (nat \<lfloor>Inf k\<rfloor>)) k
[PROOF STEP]
have "nat \<lfloor>x\<rfloor> = nat \<lfloor>Inf X\<rfloor>" if "x \<in> X - {Sup X}" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat \<lfloor>x\<rfloor> = nat \<lfloor>Inf X\<rfloor>
[PROOF STEP]
using that X
[PROOF STATE]
proof (prove)
using this:
x \<in> X - {Sup X}
X \<in> D

goal (1 subgoal):
 1. nat \<lfloor>x\<rfloor> = nat \<lfloor>Inf X\<rfloor>
[PROOF STEP]
by (auto simp: D_def nat_eq_iff floor_eq_iff)
[PROOF STATE]
proof (state)
this:
?x \<in> X - {Sup X} \<Longrightarrow> nat \<lfloor>?x\<rfloor> = nat \<lfloor>Inf X\<rfloor>

goal (2 subgoals):
 1. D division_of {real m..real n}
 2. \<And>k. k \<in> D \<Longrightarrow> ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral f (nat \<lfloor>Inf k\<rfloor>)) k
[PROOF STEP]
hence "((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X \<longleftrightarrow>
           ((\<lambda>x. f (nat \<lfloor>Inf X\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X"
[PROOF STATE]
proof (prove)
using this:
?x \<in> X - {Sup X} \<Longrightarrow> nat \<lfloor>?x\<rfloor> = nat \<lfloor>Inf X\<rfloor>

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X = ((\<lambda>x. f (nat \<lfloor>Inf X\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X
[PROOF STEP]
using X
[PROOF STATE]
proof (prove)
using this:
?x \<in> X - {Sup X} \<Longrightarrow> nat \<lfloor>?x\<rfloor> = nat \<lfloor>Inf X\<rfloor>
X \<in> D

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X = ((\<lambda>x. f (nat \<lfloor>Inf X\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X
[PROOF STEP]
by (intro has_integral_spike_eq[of "{Sup X}"]) auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X = ((\<lambda>x. f (nat \<lfloor>Inf X\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X

goal (2 subgoals):
 1. D division_of {real m..real n}
 2. \<And>k. k \<in> D \<Longrightarrow> ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral f (nat \<lfloor>Inf k\<rfloor>)) k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X = ((\<lambda>x. f (nat \<lfloor>Inf X\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X

goal (2 subgoals):
 1. D division_of {real m..real n}
 2. \<And>k. k \<in> D \<Longrightarrow> ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral f (nat \<lfloor>Inf k\<rfloor>)) k
[PROOF STEP]
from X
[PROOF STATE]
proof (chain)
picking this:
X \<in> D
[PROOF STEP]
have "\<dots>"
[PROOF STATE]
proof (prove)
using this:
X \<in> D

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lfloor>Inf X\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X
[PROOF STEP]
using has_integral_const_real[of "f (nat \<lfloor>Inf X\<rfloor>)" "Inf X" "Sup X"]
[PROOF STATE]
proof (prove)
using this:
X \<in> D
((\<lambda>x. f (nat \<lfloor>Inf X\<rfloor>)) has_integral Henstock_Kurzweil_Integration.content {Inf X..Sup X} *\<^sub>R f (nat \<lfloor>Inf X\<rfloor>)) {Inf X..Sup X}

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lfloor>Inf X\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X
[PROOF STEP]
by (auto simp: D_def)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (nat \<lfloor>Inf X\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X

goal (2 subgoals):
 1. D division_of {real m..real n}
 2. \<And>k. k \<in> D \<Longrightarrow> ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral f (nat \<lfloor>Inf k\<rfloor>)) k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X
[PROOF STEP]
show "((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral f (nat \<lfloor>Inf X\<rfloor>)) X

goal (1 subgoal):
 1. D division_of {real m..real n}
[PROOF STEP]
qed fact+
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral (\<Sum>X\<in>D. f (nat \<lfloor>Inf X\<rfloor>))) {real m..real n}

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral sum f {m..<n}) {real m..real n}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral (\<Sum>X\<in>D. f (nat \<lfloor>Inf X\<rfloor>))) {real m..real n}

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral sum f {m..<n}) {real m..real n}
[PROOF STEP]
have "(\<Sum>X\<in>D. f (nat \<lfloor>Inf X\<rfloor>)) = (\<Sum>k\<in>{m..<n}. f k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>X\<in>D. f (nat \<lfloor>Inf X\<rfloor>)) = sum f {m..<n}
[PROOF STEP]
unfolding D_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>X\<in>(\<lambda>i. {real i..real (Suc i)}) ` {m..<n}. f (nat \<lfloor>Inf X\<rfloor>)) = sum f {m..<n}
[PROOF STEP]
by (subst sum.reindex) (auto simp: inj_on_def nat_add_distrib)
[PROOF STATE]
proof (state)
this:
(\<Sum>X\<in>D. f (nat \<lfloor>Inf X\<rfloor>)) = sum f {m..<n}

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral sum f {m..<n}) {real m..real n}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral sum f {m..<n}) {real m..real n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral sum f {m..<n}) {real m..real n}

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral sum f {m..<n}) {real m..real n}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (nat \<lfloor>x\<rfloor>)) has_integral sum f {m..<n}) {real m..real n}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nat_sum_has_integral_ceiling:
  fixes f :: "nat \<Rightarrow> 'a :: banach"
  assumes mn: "m < n"
  shows "((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral sum f {m<..n}) {real m..real n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral sum f {m<..n}) {real m..real n}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral sum f {m<..n}) {real m..real n}
[PROOF STEP]
define D where "D = (\<lambda>i. {real i..real (Suc i)}) ` {m..<n}"
[PROOF STATE]
proof (state)
this:
D = (\<lambda>i. {real i..real (Suc i)}) ` {m..<n}

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral sum f {m<..n}) {real m..real n}
[PROOF STEP]
have D: "D division_of {m..n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D division_of {real m..real n}
[PROOF STEP]
using Union_atLeastAtMost_real_of_nat[OF mn]
[PROOF STATE]
proof (prove)
using this:
(\<Union>n\<in>{m..<n}. {real n..real (n + 1)}) = {real m..real n}

goal (1 subgoal):
 1. D division_of {real m..real n}
[PROOF STEP]
by (simp add: division_of_def D_def)
[PROOF STATE]
proof (state)
this:
D division_of {real m..real n}

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral sum f {m<..n}) {real m..real n}
[PROOF STEP]
have "((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral (\<Sum>X\<in>D. f (nat \<lfloor>Sup X\<rfloor>))) {real m..real n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral (\<Sum>X\<in>D. f (nat \<lfloor>Sup X\<rfloor>))) {real m..real n}
[PROOF STEP]
proof (rule has_integral_combine_division)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. D division_of {real m..real n}
 2. \<And>k. k \<in> D \<Longrightarrow> ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral f (nat \<lfloor>Sup k\<rfloor>)) k
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. D division_of {real m..real n}
 2. \<And>k. k \<in> D \<Longrightarrow> ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral f (nat \<lfloor>Sup k\<rfloor>)) k
[PROOF STEP]
assume X: "X \<in> D"
[PROOF STATE]
proof (state)
this:
X \<in> D

goal (2 subgoals):
 1. D division_of {real m..real n}
 2. \<And>k. k \<in> D \<Longrightarrow> ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral f (nat \<lfloor>Sup k\<rfloor>)) k
[PROOF STEP]
have "nat \<lceil>x\<rceil> = nat \<lfloor>Sup X\<rfloor>" if "x \<in> X - {Inf X}" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat \<lceil>x\<rceil> = nat \<lfloor>Sup X\<rfloor>
[PROOF STEP]
using that X
[PROOF STATE]
proof (prove)
using this:
x \<in> X - {Inf X}
X \<in> D

goal (1 subgoal):
 1. nat \<lceil>x\<rceil> = nat \<lfloor>Sup X\<rfloor>
[PROOF STEP]
by (auto simp: D_def nat_eq_iff ceiling_eq_iff)
[PROOF STATE]
proof (state)
this:
?x \<in> X - {Inf X} \<Longrightarrow> nat \<lceil>?x\<rceil> = nat \<lfloor>Sup X\<rfloor>

goal (2 subgoals):
 1. D division_of {real m..real n}
 2. \<And>k. k \<in> D \<Longrightarrow> ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral f (nat \<lfloor>Sup k\<rfloor>)) k
[PROOF STEP]
hence "((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X \<longleftrightarrow>
           ((\<lambda>x. f (nat \<lfloor>Sup X\<rfloor>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X"
[PROOF STATE]
proof (prove)
using this:
?x \<in> X - {Inf X} \<Longrightarrow> nat \<lceil>?x\<rceil> = nat \<lfloor>Sup X\<rfloor>

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X = ((\<lambda>x. f (nat \<lfloor>Sup X\<rfloor>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X
[PROOF STEP]
using X
[PROOF STATE]
proof (prove)
using this:
?x \<in> X - {Inf X} \<Longrightarrow> nat \<lceil>?x\<rceil> = nat \<lfloor>Sup X\<rfloor>
X \<in> D

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X = ((\<lambda>x. f (nat \<lfloor>Sup X\<rfloor>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X
[PROOF STEP]
by (intro has_integral_spike_eq[of "{Inf X}"]) auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X = ((\<lambda>x. f (nat \<lfloor>Sup X\<rfloor>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X

goal (2 subgoals):
 1. D division_of {real m..real n}
 2. \<And>k. k \<in> D \<Longrightarrow> ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral f (nat \<lfloor>Sup k\<rfloor>)) k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X = ((\<lambda>x. f (nat \<lfloor>Sup X\<rfloor>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X

goal (2 subgoals):
 1. D division_of {real m..real n}
 2. \<And>k. k \<in> D \<Longrightarrow> ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral f (nat \<lfloor>Sup k\<rfloor>)) k
[PROOF STEP]
from X
[PROOF STATE]
proof (chain)
picking this:
X \<in> D
[PROOF STEP]
have "\<dots>"
[PROOF STATE]
proof (prove)
using this:
X \<in> D

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lfloor>Sup X\<rfloor>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X
[PROOF STEP]
using has_integral_const_real[of "f (nat \<lfloor>Sup X\<rfloor>)" "Inf X" "Sup X"]
[PROOF STATE]
proof (prove)
using this:
X \<in> D
((\<lambda>x. f (nat \<lfloor>Sup X\<rfloor>)) has_integral Henstock_Kurzweil_Integration.content {Inf X..Sup X} *\<^sub>R f (nat \<lfloor>Sup X\<rfloor>)) {Inf X..Sup X}

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lfloor>Sup X\<rfloor>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X
[PROOF STEP]
by (auto simp: D_def)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (nat \<lfloor>Sup X\<rfloor>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X

goal (2 subgoals):
 1. D division_of {real m..real n}
 2. \<And>k. k \<in> D \<Longrightarrow> ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral f (nat \<lfloor>Sup k\<rfloor>)) k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X
[PROOF STEP]
show "((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral f (nat \<lfloor>Sup X\<rfloor>)) X

goal (1 subgoal):
 1. D division_of {real m..real n}
[PROOF STEP]
qed fact+
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral (\<Sum>X\<in>D. f (nat \<lfloor>Sup X\<rfloor>))) {real m..real n}

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral sum f {m<..n}) {real m..real n}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral (\<Sum>X\<in>D. f (nat \<lfloor>Sup X\<rfloor>))) {real m..real n}

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral sum f {m<..n}) {real m..real n}
[PROOF STEP]
have "(\<Sum>X\<in>D. f (nat \<lfloor>Sup X\<rfloor>)) = (\<Sum>k\<in>{m..<n}. f (Suc k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>X\<in>D. f (nat \<lfloor>Sup X\<rfloor>)) = (\<Sum>k = m..<n. f (Suc k))
[PROOF STEP]
unfolding D_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>X\<in>(\<lambda>i. {real i..real (Suc i)}) ` {m..<n}. f (nat \<lfloor>Sup X\<rfloor>)) = (\<Sum>k = m..<n. f (Suc k))
[PROOF STEP]
by (subst sum.reindex) (auto simp: inj_on_def nat_add_distrib)
[PROOF STATE]
proof (state)
this:
(\<Sum>X\<in>D. f (nat \<lfloor>Sup X\<rfloor>)) = (\<Sum>k = m..<n. f (Suc k))

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral sum f {m<..n}) {real m..real n}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>X\<in>D. f (nat \<lfloor>Sup X\<rfloor>)) = (\<Sum>k = m..<n. f (Suc k))

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral sum f {m<..n}) {real m..real n}
[PROOF STEP]
have "\<dots> = (\<Sum>k\<in>{m<..n}. f k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k = m..<n. f (Suc k)) = sum f {m<..n}
[PROOF STEP]
by (intro sum.reindex_bij_witness[of _ "\<lambda>x. x - 1" Suc]) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>k = m..<n. f (Suc k)) = sum f {m<..n}

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral sum f {m<..n}) {real m..real n}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral sum f {m<..n}) {real m..real n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral sum f {m<..n}) {real m..real n}

goal (1 subgoal):
 1. ((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral sum f {m<..n}) {real m..real n}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (nat \<lceil>x\<rceil>)) has_integral sum f {m<..n}) {real m..real n}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zeta_partial_sum_le:
  fixes x :: real and m :: nat
  assumes x: "x \<in> {0<..1}"
  shows "(\<Sum>k=1..m. real k powr (x - 1)) \<le> real m powr x / x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
consider "m = 0" | "m = 1" | "m > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m = 0 \<Longrightarrow> thesis; m = 1 \<Longrightarrow> thesis; 1 < m \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>m = 0 \<Longrightarrow> ?thesis; m = 1 \<Longrightarrow> ?thesis; 1 < m \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>m = 0 \<Longrightarrow> ?thesis; m = 1 \<Longrightarrow> ?thesis; 1 < m \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. m = 0 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 2. m = 1 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 3. 1 < m \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
assume m: "m > 1"
[PROOF STATE]
proof (state)
this:
1 < m

goal (3 subgoals):
 1. m = 0 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 2. m = 1 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 3. 1 < m \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
hence "{1..m} = insert 1 {1<..m}"
[PROOF STATE]
proof (prove)
using this:
1 < m

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

goal (3 subgoals):
 1. m = 0 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 2. m = 1 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 3. 1 < m \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{1..m} = insert 1 {1<..m}

goal (3 subgoals):
 1. m = 0 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 2. m = 1 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 3. 1 < m \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
have "(\<Sum>k\<in>\<dots>. real k powr (x - 1)) = 1 + (\<Sum>k\<in>{1<..m}. real k powr (x - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<in>insert 1 {1<..m}. real k powr (x - 1)) = 1 + (\<Sum>k\<in>{1<..m}. real k powr (x - 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<in>insert 1 {1<..m}. real k powr (x - 1)) = 1 + (\<Sum>k\<in>{1<..m}. real k powr (x - 1))

goal (3 subgoals):
 1. m = 0 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 2. m = 1 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 3. 1 < m \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<in>insert 1 {1<..m}. real k powr (x - 1)) = 1 + (\<Sum>k\<in>{1<..m}. real k powr (x - 1))

goal (3 subgoals):
 1. m = 0 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 2. m = 1 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 3. 1 < m \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
have "(\<Sum>k\<in>{1<..m}. real k powr (x - 1)) \<le> real m powr x / x - 1 / x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<in>{1<..m}. real k powr (x - 1)) \<le> real m powr x / x - 1 / x
[PROOF STEP]
proof (rule has_integral_le)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (?f has_integral (\<Sum>k\<in>{1<..m}. real k powr (x - 1))) ?S
 2. (?g has_integral real m powr x / x - 1 / x) ?S
 3. \<And>x. x \<in> ?S \<Longrightarrow> ?f x \<le> ?g x
[PROOF STEP]
show "((\<lambda>t. (nat \<lceil>t\<rceil>) powr (x - 1)) has_integral (\<Sum>n\<in>{1<..m}. n powr (x - 1))) {real 1..m}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. real (nat \<lceil>t\<rceil>) powr (x - 1)) has_integral (\<Sum>n\<in>{1<..m}. real n powr (x - 1))) {real 1..real m}
[PROOF STEP]
using m
[PROOF STATE]
proof (prove)
using this:
1 < m

goal (1 subgoal):
 1. ((\<lambda>t. real (nat \<lceil>t\<rceil>) powr (x - 1)) has_integral (\<Sum>n\<in>{1<..m}. real n powr (x - 1))) {real 1..real m}
[PROOF STEP]
by (intro nat_sum_has_integral_ceiling) auto
[PROOF STATE]
proof (state)
this:
((\<lambda>t. real (nat \<lceil>t\<rceil>) powr (x - 1)) has_integral (\<Sum>n\<in>{1<..m}. real n powr (x - 1))) {real 1..real m}

goal (2 subgoals):
 1. (?g has_integral real m powr x / x - 1 / x) {real 1..real m}
 2. \<And>xa. xa \<in> {real 1..real m} \<Longrightarrow> real (nat \<lceil>xa\<rceil>) powr (x - 1) \<le> ?g xa
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (?g has_integral real m powr x / x - 1 / x) {real 1..real m}
 2. \<And>xa. xa \<in> {real 1..real m} \<Longrightarrow> real (nat \<lceil>xa\<rceil>) powr (x - 1) \<le> ?g xa
[PROOF STEP]
have "((\<lambda>t. t powr (x - 1)) has_integral (real m powr x / x - real 1 powr x / x))
              {real 1..real m}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. t powr (x - 1)) has_integral real m powr x / x - real 1 powr x / x) {real 1..real m}
[PROOF STEP]
by (intro fundamental_theorem_of_calculus)
           (insert x m, auto simp flip: has_real_derivative_iff_has_vector_derivative
                             intro!: derivative_eq_intros)
[PROOF STATE]
proof (state)
this:
((\<lambda>t. t powr (x - 1)) has_integral real m powr x / x - real 1 powr x / x) {real 1..real m}

goal (2 subgoals):
 1. (?g has_integral real m powr x / x - 1 / x) {real 1..real m}
 2. \<And>xa. xa \<in> {real 1..real m} \<Longrightarrow> real (nat \<lceil>xa\<rceil>) powr (x - 1) \<le> ?g xa
[PROOF STEP]
thus "((\<lambda>t. t powr (x - 1)) has_integral (real m powr x / x - 1 / x)) {real 1..real m}"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>t. t powr (x - 1)) has_integral real m powr x / x - real 1 powr x / x) {real 1..real m}

goal (1 subgoal):
 1. ((\<lambda>t. t powr (x - 1)) has_integral real m powr x / x - 1 / x) {real 1..real m}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((\<lambda>t. t powr (x - 1)) has_integral real m powr x / x - 1 / x) {real 1..real m}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {real 1..real m} \<Longrightarrow> real (nat \<lceil>xa\<rceil>) powr (x - 1) \<le> xa powr (x - 1)
[PROOF STEP]
qed (insert x, auto intro!: powr_mono2')
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<in>{1<..m}. real k powr (x - 1)) \<le> real m powr x / x - 1 / x

goal (3 subgoals):
 1. m = 0 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 2. m = 1 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 3. 1 < m \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<in>{1<..m}. real k powr (x - 1)) \<le> real m powr x / x - 1 / x

goal (3 subgoals):
 1. m = 0 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 2. m = 1 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 3. 1 < m \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
have "1 + (real m powr x / x - 1 / x) \<le> real m powr x / x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + (real m powr x / x - 1 / x) \<le> real m powr x / x
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x \<in> {0<..1}

goal (1 subgoal):
 1. 1 + (real m powr x / x - 1 / x) \<le> real m powr x / x
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
1 + (real m powr x / x - 1 / x) \<le> real m powr x / x

goal (3 subgoals):
 1. m = 0 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 2. m = 1 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 3. 1 < m \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> 1 + x \<le> 1 + y) \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> 1 + x \<le> 1 + y) \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x

goal (1 subgoal):
 1. (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x

goal (2 subgoals):
 1. m = 0 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
 2. m = 1 \<Longrightarrow> (\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
qed (use assms in auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>k = 1..m. real k powr (x - 1)) \<le> real m powr x / x

goal:
No subgoals!
[PROOF STEP]
qed