[STATEMENT]
lemma contour_integral_split:
  assumes f: "continuous_on (closed_segment a b) f"
      and k: "0 \<le> k" "k \<le> 1"
      and c: "c - a = k *\<^sub>R (b - a)"
    shows "contour_integral(linepath a b) f = contour_integral(linepath a c) f + contour_integral(linepath c b) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f
[PROOF STEP]
have c': "c = (1 - k) *\<^sub>R a + k *\<^sub>R b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c = (1 - k) *\<^sub>R a + k *\<^sub>R b
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
c - a = k *\<^sub>R (b - a)

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

goal (1 subgoal):
 1. contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f
[PROOF STEP]
have "closed_segment a c \<subseteq> closed_segment a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_segment a c \<subseteq> closed_segment a b
[PROOF STEP]
by (metis c' ends_in_segment(1) in_segment(1) k subset_closed_segment)
[PROOF STATE]
proof (state)
this:
closed_segment a c \<subseteq> closed_segment a b

goal (1 subgoal):
 1. contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
closed_segment a c \<subseteq> closed_segment a b

goal (1 subgoal):
 1. contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f
[PROOF STEP]
have "closed_segment c b \<subseteq> closed_segment a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_segment c b \<subseteq> closed_segment a b
[PROOF STEP]
by (metis c' ends_in_segment(2) in_segment(1) k subset_closed_segment)
[PROOF STATE]
proof (state)
this:
closed_segment c b \<subseteq> closed_segment a b

goal (1 subgoal):
 1. contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
closed_segment a c \<subseteq> closed_segment a b
closed_segment c b \<subseteq> closed_segment a b
[PROOF STEP]
have *: "continuous_on (closed_segment a c) f" "continuous_on (closed_segment c b) f"
[PROOF STATE]
proof (prove)
using this:
closed_segment a c \<subseteq> closed_segment a b
closed_segment c b \<subseteq> closed_segment a b

goal (1 subgoal):
 1. continuous_on (closed_segment a c) f &&& continuous_on (closed_segment c b) f
[PROOF STEP]
by (auto intro: continuous_on_subset [OF f])
[PROOF STATE]
proof (state)
this:
continuous_on (closed_segment a c) f
continuous_on (closed_segment c b) f

goal (1 subgoal):
 1. contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f
[PROOF STEP]
by (rule contour_integral_unique) (meson "*" c contour_integrable_continuous_linepath has_contour_integral_integral has_contour_integral_split k)
[PROOF STATE]
proof (state)
this:
contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f

goal:
No subgoals!
[PROOF STEP]
qed