[STATEMENT]
lemma line_integral_on_pair_path:
  fixes F::"('a::euclidean_space) \<Rightarrow> ('a)" and
    g::"real \<Rightarrow> 'a" and
    \<gamma>::"(real \<Rightarrow> 'a)" and
    i::'a
  assumes i_norm_1: "norm i = 1" and
    g_orthogonal_to_i: "\<forall>x. g(x) \<bullet> i = 0" and
    gamma_is_in_terms_of_i: "\<gamma> = (\<lambda>x. f(x) *\<^sub>R i + g(f(x)))" and
    gamma_smooth: "\<gamma> C1_differentiable_on {0 .. 1}" and
    g_continuous_on_f: "continuous_on (f ` {0..1}) g" and
    path_start_le_path_end: "(pathstart \<gamma>) \<bullet> i \<le> (pathfinish \<gamma>) \<bullet> i" and
    field_i_comp_cont: "continuous_on (path_image \<gamma>) (\<lambda>x. F x \<bullet> i)"
  shows "(line_integral F {i} \<gamma>)
                 = integral (cbox ((pathstart \<gamma>) \<bullet> i) ((pathfinish \<gamma>) \<bullet> i)) (\<lambda>f_var. (F (f_var *\<^sub>R i + g(f_var)) \<bullet> i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F {i} \<gamma> = integral (cbox (pathstart \<gamma> \<bullet> i) (pathfinish \<gamma> \<bullet> i)) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
proof (simp add: line_integral_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
have gamma_differentiable: "\<forall>x \<in> {0 .. 1}. \<gamma> differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. \<gamma> differentiable at x
[PROOF STEP]
using gamma_smooth  C1_differentiable_on_eq
[PROOF STATE]
proof (prove)
using this:
\<gamma> C1_differentiable_on {0..1}
(?f C1_differentiable_on ?S) = ((\<forall>x\<in>?S. ?f differentiable at x) \<and> continuous_on ?S (\<lambda>x. vector_derivative ?f (at x)))

goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. \<gamma> differentiable at x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1}. \<gamma> differentiable at x

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>{0..1}. \<gamma> differentiable at x
[PROOF STEP]
have gamma_i_component_smooth:
    "\<forall>x \<in> {0 .. 1}. (\<lambda>x. \<gamma> x \<bullet> i) differentiable at x"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. \<gamma> differentiable at x

goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. (\<lambda>x. \<gamma> x \<bullet> i) differentiable at x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1}. (\<lambda>x. \<gamma> x \<bullet> i) differentiable at x

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
have vec_deriv_i_comp_cont:
    "continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))
[PROOF STEP]
have "continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x) (at x within {0..1}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. vector_derivative \<gamma> (at x within {0..1}))
[PROOF STEP]
using gamma_smooth C1_differentiable_on_eq
[PROOF STATE]
proof (prove)
using this:
\<gamma> C1_differentiable_on {0..1}
(?f C1_differentiable_on ?S) = ((\<forall>x\<in>?S. ?f differentiable at x) \<and> continuous_on ?S (\<lambda>x. vector_derivative ?f (at x)))

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. vector_derivative \<gamma> (at x within {0..1}))
[PROOF STEP]
by (smt C1_differentiable_on_def atLeastAtMost_iff continuous_on_eq vector_derivative_at_within_ivl)
[PROOF STATE]
proof (state)
this:
continuous_on {0..1} (\<lambda>x. vector_derivative \<gamma> (at x within {0..1}))

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
continuous_on {0..1} (\<lambda>x. vector_derivative \<gamma> (at x within {0..1}))
[PROOF STEP]
have deriv_comp_cont:
      "continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x) (at x within {0..1}) \<bullet> i)"
[PROOF STATE]
proof (prove)
using this:
continuous_on {0..1} (\<lambda>x. vector_derivative \<gamma> (at x within {0..1}))

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)
[PROOF STEP]
by (simp add: continuous_intros)
[PROOF STATE]
proof (state)
this:
continuous_on {0..1} (\<lambda>x. vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))
[PROOF STEP]
using derivative_component_fun_component_at_within[OF gamma_differentiable, of "i"]
        continuous_on_eq[OF deriv_comp_cont, of "(\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))"]
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. vector_derivative \<gamma> (at x within {0..1}) \<bullet> i = vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})
(\<And>x. x \<in> {0..1} \<Longrightarrow> vector_derivative \<gamma> (at x within {0..1}) \<bullet> i = vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) \<Longrightarrow> continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
have field_cont_on_path:
    "continuous_on ((\<lambda>x. \<gamma> x \<bullet> i) ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on ((\<lambda>x. \<gamma> x \<bullet> i) ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. continuous_on ((\<lambda>x. \<gamma> x \<bullet> i) ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
have 0: "(\<lambda>x. \<gamma> x \<bullet> i) = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<gamma> x \<bullet> i) = f
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<gamma> x \<bullet> i = f x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<gamma> x \<bullet> i = f x
[PROOF STEP]
show "\<gamma> x \<bullet> i = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> x \<bullet> i = f x
[PROOF STEP]
using g_orthogonal_to_i i_norm_1
[PROOF STATE]
proof (prove)
using this:
\<forall>x. g x \<bullet> i = 0
norm i = 1

goal (1 subgoal):
 1. \<gamma> x \<bullet> i = f x
[PROOF STEP]
by (simp only: gamma_is_in_terms_of_i  real_inner_class.inner_add_left g_orthogonal_to_i inner_scaleR_left inner_same_Basis norm_eq_1)
[PROOF STATE]
proof (state)
this:
\<gamma> x \<bullet> i = f x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<gamma> x \<bullet> i) = f

goal (1 subgoal):
 1. continuous_on ((\<lambda>x. \<gamma> x \<bullet> i) ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on ((\<lambda>x. \<gamma> x \<bullet> i) ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
unfolding 0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on (f ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
apply (rule continuous_on_compose2 [of _ "(\<lambda>x. F(x)  \<bullet> i)" "f ` { 0..1}" "(\<lambda>x. x *\<^sub>R i + g x)"]
          field_i_comp_cont g_continuous_on_f field_i_comp_cont continuous_intros)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f_var. f_var *\<^sub>R i + g f_var) ` f ` {0..1} \<subseteq> path_image \<gamma>
[PROOF STEP]
by (auto simp add: gamma_is_in_terms_of_i path_image_def)
[PROOF STATE]
proof (state)
this:
continuous_on ((\<lambda>x. \<gamma> x \<bullet> i) ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
continuous_on ((\<lambda>x. \<gamma> x \<bullet> i) ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
have path_vector_deriv_line_integrals:
    "\<forall>x\<in>{0..1}. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative
                                          vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x))
                                                  (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x)) (at x)
[PROOF STEP]
using gamma_i_component_smooth and derivative_component_fun_component and
      vector_derivative_works
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. (\<lambda>x. \<gamma> x \<bullet> i) differentiable at x
?f differentiable at ?x \<Longrightarrow> vector_derivative ?f (at ?x) \<bullet> ?i = vector_derivative (\<lambda>x. ?f x \<bullet> ?i) (at ?x)
(?f differentiable ?net) = (?f has_vector_derivative vector_derivative ?f ?net) ?net

goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x)) (at x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1}. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x)) (at x)

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>{0..1}. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x)) (at x)
[PROOF STEP]
have "\<forall>x\<in>{0..1}. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative
                                          vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))
                                                  (at x within {0..1})"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x)) (at x)

goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) (at x within {0..1})
[PROOF STEP]
using has_vector_derivative_at_within vector_derivative_at_within_ivl
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x)) (at x)
(?f has_vector_derivative ?f') (at ?x) \<Longrightarrow> (?f has_vector_derivative ?f') (at ?x within ?S)
\<lbrakk>(?f has_vector_derivative ?f') (at ?x); ?a \<le> ?x; ?x \<le> ?b; ?a < ?b\<rbrakk> \<Longrightarrow> vector_derivative ?f (at ?x within {?a..?b}) = ?f'

goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) (at x within {0..1})
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1}. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) (at x within {0..1})

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>{0..1}. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) (at x within {0..1})
[PROOF STEP]
have substitute:
    "integral (cbox ((pathstart \<gamma>) \<bullet> i) ((pathfinish \<gamma>) \<bullet> i)) (\<lambda>f_var. (F (f_var *\<^sub>R i + g(f_var)) \<bullet> i))
                 = integral (cbox 0 1) (\<lambda>x. (F(\<gamma>(x)) \<bullet> i)*(vector_derivative (\<lambda>x. \<gamma>(x) \<bullet> i) (at x within {0..1})))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) (at x within {0..1})

goal (1 subgoal):
 1. integral (cbox (pathstart \<gamma> \<bullet> i) (pathfinish \<gamma> \<bullet> i)) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i) = integral (cbox 0 1) (\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))
[PROOF STEP]
using gauge_integral_by_substitution
      [of "0" "1" "(\<lambda>x. (\<gamma> x) \<bullet> i)"
        "(\<lambda>x. vector_derivative (\<lambda>x. \<gamma>(x) \<bullet> i) (at x within {0..1}))"
        "(\<lambda>f_var. (F (f_var *\<^sub>R i + g(f_var)) \<bullet> i))"] and
      path_start_le_path_end and vec_deriv_i_comp_cont and field_cont_on_path and
      gamma_is_in_terms_of_i i_norm_1
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) (at x within {0..1})
\<lbrakk>0 \<le> 1; \<gamma> 0 \<bullet> i \<le> \<gamma> 1 \<bullet> i; \<forall>x\<in>{0..1}. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) (at x within {0..1}); continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})); continuous_on ((\<lambda>x. \<gamma> x \<bullet> i) ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)\<rbrakk> \<Longrightarrow> integral {\<gamma> 0 \<bullet> i..\<gamma> 1 \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i) = integral {0..1} (\<lambda>x. F ((\<gamma> x \<bullet> i) *\<^sub>R i + g (\<gamma> x \<bullet> i)) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))
pathstart \<gamma> \<bullet> i \<le> pathfinish \<gamma> \<bullet> i
continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))
continuous_on ((\<lambda>x. \<gamma> x \<bullet> i) ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
\<gamma> = (\<lambda>x. f x *\<^sub>R i + g (f x))
norm i = 1

goal (1 subgoal):
 1. integral (cbox (pathstart \<gamma> \<bullet> i) (pathfinish \<gamma> \<bullet> i)) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i) = integral (cbox 0 1) (\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))
[PROOF STEP]
apply (auto simp add: pathstart_def pathfinish_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>{0..1}. ((\<lambda>x. (f x *\<^sub>R i + g (f x)) \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. (f x *\<^sub>R i + g (f x)) \<bullet> i) (at x within {0..1})) (at x within {0..1}); integral {(f 0 *\<^sub>R i + g (f 0)) \<bullet> i..(f 1 *\<^sub>R i + g (f 1)) \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i) = integral {0..1} (\<lambda>x. F (((f x *\<^sub>R i + g (f x)) \<bullet> i) *\<^sub>R i + g ((f x *\<^sub>R i + g (f x)) \<bullet> i)) \<bullet> i * vector_derivative (\<lambda>x. (f x *\<^sub>R i + g (f x)) \<bullet> i) (at x within {0..1})); (f 0 *\<^sub>R i + g (f 0)) \<bullet> i \<le> (f 1 *\<^sub>R i + g (f 1)) \<bullet> i; continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. (f x *\<^sub>R i + g (f x)) \<bullet> i) (at x within {0..1})); continuous_on ((\<lambda>x. (f x *\<^sub>R i + g (f x)) \<bullet> i) ` {0..1}) (\<lambda>x. F (x *\<^sub>R i + g x) \<bullet> i); \<gamma> = (\<lambda>x. f x *\<^sub>R i + g (f x)); norm i = 1\<rbrakk> \<Longrightarrow> integral {0..1} (\<lambda>x. F (((f x *\<^sub>R i + g (f x)) \<bullet> i) *\<^sub>R i + g ((f x *\<^sub>R i + g (f x)) \<bullet> i)) \<bullet> i * vector_derivative (\<lambda>x. (f x *\<^sub>R i + g (f x)) \<bullet> i) (at x within {0..1})) = integral {0..1} (\<lambda>x. F (f x *\<^sub>R i + g (f x)) \<bullet> i * vector_derivative (\<lambda>x. (f x *\<^sub>R i + g (f x)) \<bullet> i) (at x within {0..1}))
[PROOF STEP]
apply (simp only:  real_inner_class.inner_add_left inner_not_same_Basis g_orthogonal_to_i inner_scaleR_left norm_eq_1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>{0..1}. ((\<lambda>x. f x * 1 + 0) has_vector_derivative vector_derivative (\<lambda>x. f x * 1 + 0) (at x within {0..1})) (at x within {0..1}); integral {f 0 * 1 + 0..f 1 * 1 + 0} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i) = integral {0..1} (\<lambda>x. F ((f x * 1 + 0) *\<^sub>R i + g (f x * 1 + 0)) \<bullet> i * vector_derivative (\<lambda>x. f x * 1 + 0) (at x within {0..1})); f 0 * 1 + 0 \<le> f 1 * 1 + 0; continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. f x * 1 + 0) (at x within {0..1})); continuous_on ((\<lambda>x. f x * 1 + 0) ` {0..1}) (\<lambda>x. F (x *\<^sub>R i + g x) \<bullet> i); \<gamma> = (\<lambda>x. f x *\<^sub>R i + g (f x)); i \<bullet> i = 1\<rbrakk> \<Longrightarrow> integral {0..1} (\<lambda>x. F ((f x * 1 + 0) *\<^sub>R i + g (f x * 1 + 0)) \<bullet> i * vector_derivative (\<lambda>x. f x * 1 + 0) (at x within {0..1})) = integral {0..1} (\<lambda>x. F (f x *\<^sub>R i + g (f x)) \<bullet> i * vector_derivative (\<lambda>x. f x * 1 + 0) (at x within {0..1}))
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
integral (cbox (pathstart \<gamma> \<bullet> i) (pathfinish \<gamma> \<bullet> i)) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i) = integral (cbox 0 1) (\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
(*integration by substitution*)
[PROOF STATE]
proof (state)
this:
integral (cbox (pathstart \<gamma> \<bullet> i) (pathfinish \<gamma> \<bullet> i)) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i) = integral (cbox 0 1) (\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
have comp_in_eq_comp_out: "\<forall>x \<in> {0..1}.
            (vector_derivative (\<lambda>x. \<gamma>(x) \<bullet> i) (at x within {0..1}))
                = (vector_derivative \<gamma> (at x within {0..1})) \<bullet> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} \<Longrightarrow> vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
fix x:: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} \<Longrightarrow> vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
assume x_bounds: "x \<in> {0..1}"
[PROOF STATE]
proof (state)
this:
x \<in> {0..1}

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} \<Longrightarrow> vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> {0..1}
[PROOF STEP]
have "\<gamma> differentiable at x"
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..1}

goal (1 subgoal):
 1. \<gamma> differentiable at x
[PROOF STEP]
using gamma_differentiable
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..1}
\<forall>x\<in>{0..1}. \<gamma> differentiable at x

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

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} \<Longrightarrow> vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<gamma> differentiable at x
[PROOF STEP]
have dotprod_in_is_out:
      "vector_derivative (\<lambda>x. \<gamma>(x) \<bullet> i) (at x)
                         = (vector_derivative \<gamma> (at x)) \<bullet> i"
[PROOF STATE]
proof (prove)
using this:
\<gamma> differentiable at x

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative \<gamma> (at x) \<bullet> i
[PROOF STEP]
using derivative_component_fun_component
[PROOF STATE]
proof (prove)
using this:
\<gamma> differentiable at x
?f differentiable at ?x \<Longrightarrow> vector_derivative ?f (at ?x) \<bullet> ?i = vector_derivative (\<lambda>x. ?f x \<bullet> ?i) (at ?x)

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative \<gamma> (at x) \<bullet> i
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative \<gamma> (at x) \<bullet> i

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} \<Longrightarrow> vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative \<gamma> (at x) \<bullet> i
[PROOF STEP]
have 0: "(vector_derivative \<gamma> (at x)) \<bullet> i
                         = (vector_derivative \<gamma> (at x within {0..1})) \<bullet> i"
[PROOF STATE]
proof (prove)
using this:
vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative \<gamma> (at x) \<bullet> i

goal (1 subgoal):
 1. vector_derivative \<gamma> (at x) \<bullet> i = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
using has_vector_derivative_at_within and x_bounds and vector_derivative_at_within_ivl
[PROOF STATE]
proof (prove)
using this:
vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative \<gamma> (at x) \<bullet> i
(?f has_vector_derivative ?f') (at ?x) \<Longrightarrow> (?f has_vector_derivative ?f') (at ?x within ?S)
x \<in> {0..1}
\<lbrakk>(?f has_vector_derivative ?f') (at ?x); ?a \<le> ?x; ?x \<le> ?b; ?a < ?b\<rbrakk> \<Longrightarrow> vector_derivative ?f (at ?x within {?a..?b}) = ?f'

goal (1 subgoal):
 1. vector_derivative \<gamma> (at x) \<bullet> i = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
by (smt atLeastAtMost_iff gamma_differentiable inner_commute vector_derivative_works)
[PROOF STATE]
proof (state)
this:
vector_derivative \<gamma> (at x) \<bullet> i = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} \<Longrightarrow> vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
have 1: "vector_derivative (\<lambda>x. \<gamma>(x) \<bullet> i) (at x) = vector_derivative (\<lambda>x. \<gamma>(x) \<bullet> i) (at x within {0..1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})
[PROOF STEP]
using path_vector_deriv_line_integrals and vector_derivative_at_within_ivl and
        x_bounds
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x)) (at x)
\<lbrakk>(?f has_vector_derivative ?f') (at ?x); ?a \<le> ?x; ?x \<le> ?b; ?a < ?b\<rbrakk> \<Longrightarrow> vector_derivative ?f (at ?x within {?a..?b}) = ?f'
x \<in> {0..1}

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} \<Longrightarrow> vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
show "vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
using 0 and 1 and dotprod_in_is_out
[PROOF STATE]
proof (prove)
using this:
vector_derivative \<gamma> (at x) \<bullet> i = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})
vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative \<gamma> (at x) \<bullet> i

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1}. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
show "integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) =
                   integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
using substitute and comp_in_eq_comp_out and
      Henstock_Kurzweil_Integration.integral_cong
      [of "{0..1}" "(\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i))"
        "(\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))"]
[PROOF STATE]
proof (prove)
using this:
integral (cbox (pathstart \<gamma> \<bullet> i) (pathfinish \<gamma> \<bullet> i)) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i) = integral (cbox 0 1) (\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))
\<forall>x\<in>{0..1}. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
(\<And>x. x \<in> {0..1} \<Longrightarrow> F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i) = F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) \<Longrightarrow> integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma content_box_cases:
  "content (box a b) = (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then prod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. content (box a b) = (if \<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i then \<Prod>i\<in>Basis. b \<bullet> i - a \<bullet> i else 0)
[PROOF STEP]
by (simp add: measure_lborel_box_eq inner_diff)


[STATEMENT]
lemma content_box_cbox:
  shows "content (box a b) = content (cbox a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. content (box a b) = content (cbox a b)
[PROOF STEP]
by (simp add: content_box_cases content_cbox_cases)


[STATEMENT]
lemma content_eq_0: "content (box a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (content (box a b) = 0) = (\<exists>i\<in>Basis. b \<bullet> i \<le> a \<bullet> i)
[PROOF STEP]
by (auto simp: content_box_cases not_le intro: less_imp_le antisym eq_refl)


[STATEMENT]
lemma content_pos_lt_eq: "0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < content (cbox a b)) = (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)
[PROOF STEP]
by (auto simp add: content_cbox_cases less_le prod_nonneg)


[STATEMENT]
lemma content_lt_nz: "0 < content (box a b) \<longleftrightarrow> content (box a b) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < content (box a b)) = (content (box a b) \<noteq> 0)
[PROOF STEP]
using Paths.content_eq_0 zero_less_measure_iff
[PROOF STATE]
proof (prove)
using this:
(content (box ?a ?b) = 0) = (\<exists>i\<in>Basis. ?b \<bullet> i \<le> ?a \<bullet> i)
(0 < Sigma_Algebra.measure ?M ?A) = (Sigma_Algebra.measure ?M ?A \<noteq> 0)

goal (1 subgoal):
 1. (0 < content (box a b)) = (content (box a b) \<noteq> 0)
[PROOF STEP]
by blast


[STATEMENT]
lemma content_subset: "cbox a b \<subseteq> box c d \<Longrightarrow> content (cbox a b) \<le> content (box c d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cbox a b \<subseteq> box c d \<Longrightarrow> content (cbox a b) \<le> content (box c d)
[PROOF STEP]
unfolding measure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cbox a b \<subseteq> box c d \<Longrightarrow> enn2real (emeasure lborel (cbox a b)) \<le> enn2real (emeasure lborel (box c d))
[PROOF STEP]
by (intro enn2real_mono emeasure_mono) (auto simp: emeasure_lborel_cbox_eq emeasure_lborel_box_eq)


[STATEMENT]
lemma sum_content_null:
  assumes "content (box a b) = 0"
    and "p tagged_division_of (box a b)"
  shows "sum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) = (0::'a)
[PROOF STEP]
proof (rule sum.neutral, rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> p \<Longrightarrow> (case x of (x, k) \<Rightarrow> content k *\<^sub>R f x) = (0::'a)
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> p \<Longrightarrow> (case x of (x, k) \<Rightarrow> content k *\<^sub>R f x) = (0::'a)
[PROOF STEP]
assume y: "y \<in> p"
[PROOF STATE]
proof (state)
this:
y \<in> p

goal (1 subgoal):
 1. \<And>x. x \<in> p \<Longrightarrow> (case x of (x, k) \<Rightarrow> content k *\<^sub>R f x) = (0::'a)
[PROOF STEP]
obtain x k where xk: "y = (x, k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x k. y = (x, k) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using surj_pair[of y]
[PROOF STATE]
proof (prove)
using this:
\<exists>x ya. y = (x, ya)

goal (1 subgoal):
 1. (\<And>x k. y = (x, k) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y = (x, k)

goal (1 subgoal):
 1. \<And>x. x \<in> p \<Longrightarrow> (case x of (x, k) \<Rightarrow> content k *\<^sub>R f x) = (0::'a)
[PROOF STEP]
note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]]
[PROOF STATE]
proof (state)
this:
k \<subseteq> box a b
\<exists>a b. k = cbox a b

goal (1 subgoal):
 1. \<And>x. x \<in> p \<Longrightarrow> (case x of (x, k) \<Rightarrow> content k *\<^sub>R f x) = (0::'a)
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
\<exists>a b. k = cbox a b
[PROOF STEP]
obtain c d where k: "k = cbox c d"
[PROOF STATE]
proof (prove)
using this:
\<exists>a b. k = cbox a b

goal (1 subgoal):
 1. (\<And>c d. k = cbox c d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k = cbox c d

goal (1 subgoal):
 1. \<And>x. x \<in> p \<Longrightarrow> (case x of (x, k) \<Rightarrow> content k *\<^sub>R f x) = (0::'a)
[PROOF STEP]
have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case y of (x, k) \<Rightarrow> content k *\<^sub>R f x) = content k *\<^sub>R f x
[PROOF STEP]
unfolding xk
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (x, k) of (x, k) \<Rightarrow> content k *\<^sub>R f x) = content k *\<^sub>R f x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(case y of (x, k) \<Rightarrow> content k *\<^sub>R f x) = content k *\<^sub>R f x

goal (1 subgoal):
 1. \<And>x. x \<in> p \<Longrightarrow> (case x of (x, k) \<Rightarrow> content k *\<^sub>R f x) = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(case y of (x, k) \<Rightarrow> content k *\<^sub>R f x) = content k *\<^sub>R f x

goal (1 subgoal):
 1. \<And>x. x \<in> p \<Longrightarrow> (case x of (x, k) \<Rightarrow> content k *\<^sub>R f x) = (0::'a)
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. content k *\<^sub>R f x = (0::'a)
[PROOF STEP]
using content_subset[OF assm(1)[unfolded k]] content_pos_le[of "cbox c d"]
[PROOF STATE]
proof (prove)
using this:
content (cbox c d) \<le> content (box a b)
0 \<le> content (cbox c d)

goal (1 subgoal):
 1. content k *\<^sub>R f x = (0::'a)
[PROOF STEP]
unfolding assms(1) k
[PROOF STATE]
proof (prove)
using this:
content (cbox c d) \<le> 0
0 \<le> content (cbox c d)

goal (1 subgoal):
 1. content (cbox c d) *\<^sub>R f x = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
content k *\<^sub>R f x = (0::'a)

goal (1 subgoal):
 1. \<And>x. x \<in> p \<Longrightarrow> (case x of (x, k) \<Rightarrow> content k *\<^sub>R f x) = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(case y of (x, k) \<Rightarrow> content k *\<^sub>R f x) = (0::'a)
[PROOF STEP]
show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0"
[PROOF STATE]
proof (prove)
using this:
(case y of (x, k) \<Rightarrow> content k *\<^sub>R f x) = (0::'a)

goal (1 subgoal):
 1. (case y of (x, k) \<Rightarrow> content k *\<^sub>R f x) = (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(case y of (x, k) \<Rightarrow> content k *\<^sub>R f x) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma has_integral_null [intro]: "content(box a b) = 0 \<Longrightarrow> (f has_integral 0) (box a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. content (box a b) = 0 \<Longrightarrow> (f has_integral (0::'b)) (box a b)
[PROOF STEP]
by (simp add: content_box_cbox content_eq_0_interior)


[STATEMENT]
lemma line_integral_distrib:
  assumes "line_integral_exists f basis g1"
    "line_integral_exists f basis g2"
    "valid_path g1" "valid_path g2"
  shows "line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2"
    "line_integral_exists f basis (g1 +++ g2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2 &&& line_integral_exists f basis (g1 +++ g2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2
 2. line_integral_exists f basis (g1 +++ g2)
[PROOF STEP]
obtain s1 s2
    where s1: "finite s1" "\<forall>x\<in>{0..1} - s1. g1 differentiable at x"
      and s2: "finite s2" "\<forall>x\<in>{0..1} - s2. g2 differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1 s2. \<lbrakk>finite s1; \<forall>x\<in>{0..1} - s1. g1 differentiable at x; finite s2; \<forall>x\<in>{0..1} - s2. g2 differentiable at x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
line_integral_exists f basis g1
line_integral_exists f basis g2
valid_path g1
valid_path g2

goal (1 subgoal):
 1. (\<And>s1 s2. \<lbrakk>finite s1; \<forall>x\<in>{0..1} - s1. g1 differentiable at x; finite s2; \<forall>x\<in>{0..1} - s2. g2 differentiable at x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
[PROOF STATE]
proof (state)
this:
finite s1
\<forall>x\<in>{0..1} - s1. g1 differentiable at x
finite s2
\<forall>x\<in>{0..1} - s2. g2 differentiable at x

goal (2 subgoals):
 1. line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2
 2. line_integral_exists f basis (g1 +++ g2)
[PROOF STEP]
obtain i1 i2
    where 1: "((\<lambda>x. \<Sum>b\<in>basis. f (g1 x) \<bullet> b * (vector_derivative g1 (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1}"
      and 2: "((\<lambda>x. \<Sum>b\<in>basis. f (g2 x) \<bullet> b * (vector_derivative g2 (at x within {0..1}) \<bullet> b)) has_integral i2) {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i1 i2. \<lbrakk>((\<lambda>x. \<Sum>b\<in>basis. f (g1 x) \<bullet> b * (vector_derivative g1 (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1}; ((\<lambda>x. \<Sum>b\<in>basis. f (g2 x) \<bullet> b * (vector_derivative g2 (at x within {0..1}) \<bullet> b)) has_integral i2) {0..1}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
line_integral_exists f basis g1
line_integral_exists f basis g2
valid_path g1
valid_path g2

goal (1 subgoal):
 1. (\<And>i1 i2. \<lbrakk>((\<lambda>x. \<Sum>b\<in>basis. f (g1 x) \<bullet> b * (vector_derivative g1 (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1}; ((\<lambda>x. \<Sum>b\<in>basis. f (g2 x) \<bullet> b * (vector_derivative g2 (at x within {0..1}) \<bullet> b)) has_integral i2) {0..1}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: line_integral_exists_def)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<Sum>b\<in>basis. f (g1 x) \<bullet> b * (vector_derivative g1 (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1}
((\<lambda>x. \<Sum>b\<in>basis. f (g2 x) \<bullet> b * (vector_derivative g2 (at x within {0..1}) \<bullet> b)) has_integral i2) {0..1}

goal (2 subgoals):
 1. line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2
 2. line_integral_exists f basis (g1 +++ g2)
[PROOF STEP]
have i1: "((\<lambda>x. 2 * (\<Sum>b\<in>basis. f (g1 (2 * x)) \<bullet> b * (vector_derivative g1 (at (2 * x) within {0..1}) \<bullet> b))) has_integral i1) {0..1/2}"
   and i2: "((\<lambda>x. 2 * (\<Sum>b\<in>basis. f (g2 (2 * x - 1)) \<bullet> b * (vector_derivative g2 (at ((2 * x) - 1) within {0..1}) \<bullet> b))) has_integral i2) {1/2..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. 2 * (\<Sum>b\<in>basis. f (g1 (2 * x)) \<bullet> b * (vector_derivative g1 (at (2 * x) within {0..1}) \<bullet> b))) has_integral i1) {0..1 / 2} &&& ((\<lambda>x. 2 * (\<Sum>b\<in>basis. f (g2 (2 * x - 1)) \<bullet> b * (vector_derivative g2 (at (2 * x - 1) within {0..1}) \<bullet> b))) has_integral i2) {1 / 2..1}
[PROOF STEP]
using has_integral_affinity01 [OF 1, where m= 2 and c=0, THEN has_integral_cmul [where c=2]]
      has_integral_affinity01 [OF 2, where m= 2 and c="-1", THEN has_integral_cmul [where c=2]]
[PROOF STATE]
proof (prove)
using this:
2 \<noteq> 0 \<Longrightarrow> ((\<lambda>x. 2 *\<^sub>R (\<Sum>b\<in>basis. f (g1 (2 * x + 0)) \<bullet> b * (vector_derivative g1 (at (2 * x + 0) within {0..1}) \<bullet> b))) has_integral 2 *\<^sub>R (1 / \<bar>2\<bar>) *\<^sub>R i1) ((\<lambda>x. x / 2 - 0 / 2) ` {0..1})
2 \<noteq> 0 \<Longrightarrow> ((\<lambda>x. 2 *\<^sub>R (\<Sum>b\<in>basis. f (g2 (2 * x + - 1)) \<bullet> b * (vector_derivative g2 (at (2 * x + - 1) within {0..1}) \<bullet> b))) has_integral 2 *\<^sub>R (1 / \<bar>2\<bar>) *\<^sub>R i2) ((\<lambda>x. x / 2 - - 1 / 2) ` {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. 2 * (\<Sum>b\<in>basis. f (g1 (2 * x)) \<bullet> b * (vector_derivative g1 (at (2 * x) within {0..1}) \<bullet> b))) has_integral i1) {0..1 / 2} &&& ((\<lambda>x. 2 * (\<Sum>b\<in>basis. f (g2 (2 * x - 1)) \<bullet> b * (vector_derivative g2 (at (2 * x - 1) within {0..1}) \<bullet> b))) has_integral i2) {1 / 2..1}
[PROOF STEP]
by (simp_all only: image_affinity_atLeastAtMost_div_diff, simp_all add: scaleR_conv_of_real mult_ac)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. 2 * (\<Sum>b\<in>basis. f (g1 (2 * x)) \<bullet> b * (vector_derivative g1 (at (2 * x) within {0..1}) \<bullet> b))) has_integral i1) {0..1 / 2}
((\<lambda>x. 2 * (\<Sum>b\<in>basis. f (g2 (2 * x - 1)) \<bullet> b * (vector_derivative g2 (at (2 * x - 1) within {0..1}) \<bullet> b))) has_integral i2) {1 / 2..1}

goal (2 subgoals):
 1. line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2
 2. line_integral_exists f basis (g1 +++ g2)
[PROOF STEP]
have g1: "\<lbrakk>0 \<le> z; z*2 < 1; z*2 \<notin> s1\<rbrakk> \<Longrightarrow>
            vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at z within {0..1}) =
            2 *\<^sub>R vector_derivative g1 (at (z*2) within {0..1})" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})
[PROOF STEP]
have i:"\<lbrakk>0 \<le> z; z*2 < 1; z*2 \<notin> s1\<rbrakk> \<Longrightarrow>
              vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))
[PROOF STEP]
have g1_at_z:"\<lbrakk>0 \<le> z; z*2 < 1; z*2 \<notin> s1\<rbrakk> \<Longrightarrow>
                         ((\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) has_vector_derivative
                         2 *\<^sub>R vector_derivative g1 (at (z*2))) (at z)" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> ((\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g1 (at (z * 2))) (at z)
[PROOF STEP]
apply (rule has_vector_derivative_transform_at [of "\<bar>z - 1/2\<bar>" _ "(\<lambda>x. g1(2*x))"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> 0 < \<bar>z - 1 / 2\<bar>
 2. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> \<forall>x'. dist x' z < \<bar>z - 1 / 2\<bar> \<longrightarrow> g1 (2 * x') = (if x' * 2 \<le> 1 then g1 (2 * x') else g2 (2 * x' - 1))
 3. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> ((\<lambda>x. g1 (2 * x)) has_vector_derivative 2 *\<^sub>R vector_derivative g1 (at (z * 2))) (at z)
[PROOF STEP]
apply (simp_all add: dist_real_def abs_if split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> ((\<lambda>x. g1 (2 * x)) has_vector_derivative 2 *\<^sub>R vector_derivative g1 (at (z * 2))) (at z)
[PROOF STEP]
apply (rule vector_diff_chain_at [of "\<lambda>x. 2*x" 2 _ g1, simplified o_def])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> ((*) 2 has_vector_derivative 2) (at z)
 2. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> (g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (2 * z))
[PROOF STEP]
apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> (g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (2 * z))
[PROOF STEP]
using s1
[PROOF STATE]
proof (prove)
using this:
finite s1
\<forall>x\<in>{0..1} - s1. g1 differentiable at x

goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> (g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (2 * z))
[PROOF STEP]
apply (auto simp: algebra_simps vector_derivative_works)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> ?z; ?z * 2 < 1; ?z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> ((\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g1 (at (?z * 2))) (at ?z)

goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))
[PROOF STEP]
assume ass: "0 \<le> z" "z*2 < 1" "z*2 \<notin> s1"
[PROOF STATE]
proof (state)
this:
0 \<le> z
z * 2 < 1
z * 2 \<notin> s1

goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> z
z * 2 < 1
z * 2 \<notin> s1
[PROOF STEP]
have z_ge: "z\<le> 1"
[PROOF STATE]
proof (prove)
using this:
0 \<le> z
z * 2 < 1
z * 2 \<notin> s1

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

goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))
[PROOF STEP]
show "vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))
[PROOF STEP]
using Derivative.vector_derivative_at_within_ivl[OF g1_at_z[OF ass] ass(1) z_ge]
[PROOF STATE]
proof (prove)
using this:
0 < 1 \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> ?z; ?z * 2 < 1; ?z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at ?z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (?z * 2))

goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})
[PROOF STEP]
assume ass: "0 \<le> z" "z*2 < 1" "z*2 \<notin> s1"
[PROOF STATE]
proof (state)
this:
0 \<le> z
z * 2 < 1
z * 2 \<notin> s1

goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> z
z * 2 < 1
z * 2 \<notin> s1
[PROOF STEP]
have "(g1 has_vector_derivative ((vector_derivative g1 (at (z*2))))) (at (z*2))"
[PROOF STATE]
proof (prove)
using this:
0 \<le> z
z * 2 < 1
z * 2 \<notin> s1

goal (1 subgoal):
 1. (g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (z * 2))
[PROOF STEP]
using s1
[PROOF STATE]
proof (prove)
using this:
0 \<le> z
z * 2 < 1
z * 2 \<notin> s1
finite s1
\<forall>x\<in>{0..1} - s1. g1 differentiable at x

goal (1 subgoal):
 1. (g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (z * 2))
[PROOF STEP]
by (auto simp: algebra_simps vector_derivative_works)
[PROOF STATE]
proof (state)
this:
(g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (z * 2))

goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (z * 2))
[PROOF STEP]
have ii: "(vector_derivative g1 (at (z*2) within {0..1})) = (vector_derivative g1 (at (z*2)))"
[PROOF STATE]
proof (prove)
using this:
(g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (z * 2))

goal (1 subgoal):
 1. vector_derivative g1 (at (z * 2) within {0..1}) = vector_derivative g1 (at (z * 2))
[PROOF STEP]
using Derivative.vector_derivative_at_within_ivl ass
[PROOF STATE]
proof (prove)
using this:
(g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (z * 2))
\<lbrakk>(?f has_vector_derivative ?f') (at ?x); ?a \<le> ?x; ?x \<le> ?b; ?a < ?b\<rbrakk> \<Longrightarrow> vector_derivative ?f (at ?x within {?a..?b}) = ?f'
0 \<le> z
z * 2 < 1
z * 2 \<notin> s1

goal (1 subgoal):
 1. vector_derivative g1 (at (z * 2) within {0..1}) = vector_derivative g1 (at (z * 2))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
vector_derivative g1 (at (z * 2) within {0..1}) = vector_derivative g1 (at (z * 2))

goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})
[PROOF STEP]
show "vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})
[PROOF STEP]
using i[OF ass] ii
[PROOF STATE]
proof (prove)
using this:
vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))
vector_derivative g1 (at (z * 2) within {0..1}) = vector_derivative g1 (at (z * 2))

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> ?z; ?z * 2 < 1; ?z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at ?z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (?z * 2) within {0..1})

goal (2 subgoals):
 1. line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2
 2. line_integral_exists f basis (g1 +++ g2)
[PROOF STEP]
have g2: "\<lbrakk>1 < z*2; z \<le> 1; z*2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow>
            vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at z within {0..1}) =
            2 *\<^sub>R vector_derivative g2 (at (z*2 - 1) within {0..1})" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})
[PROOF STEP]
have i:"\<lbrakk>1 < z*2; z \<le> 1; z*2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow>
              vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1})
                   = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
have g2_at_z:"\<lbrakk>1 < z*2; z \<le> 1; z*2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow>
                      ((\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at (z*2 - 1))) (at z)" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> ((\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))) (at z)
[PROOF STEP]
apply (rule has_vector_derivative_transform_at [of "\<bar>z - 1/2\<bar>" _ "(\<lambda>x. g2 (2*x - 1))"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> 0 < \<bar>z - 1 / 2\<bar>
 2. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> \<forall>x'. dist x' z < \<bar>z - 1 / 2\<bar> \<longrightarrow> g2 (2 * x' - 1) = (if x' * 2 \<le> 1 then g1 (2 * x') else g2 (2 * x' - 1))
 3. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> ((\<lambda>x. g2 (2 * x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))) (at z)
[PROOF STEP]
apply (simp_all add: dist_real_def abs_if split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> ((\<lambda>x. g2 (2 * x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))) (at z)
[PROOF STEP]
apply (rule vector_diff_chain_at [of "\<lambda>x. 2*x - 1" 2 _ g2, simplified o_def])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> ((\<lambda>x. 2 * x - 1) has_vector_derivative 2) (at z)
 2. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> (g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (2 * z - 1))
[PROOF STEP]
apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> (g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (2 * z - 1))
[PROOF STEP]
using s2
[PROOF STATE]
proof (prove)
using this:
finite s2
\<forall>x\<in>{0..1} - s2. g2 differentiable at x

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> (g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (2 * z - 1))
[PROOF STEP]
apply (auto simp: algebra_simps vector_derivative_works)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<lbrakk>1 < ?z * 2; ?z \<le> 1; ?z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> ((\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at (?z * 2 - 1))) (at ?z)

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
assume ass: "1 < z*2" "z \<le> 1" "z*2 - 1 \<notin> s2"
[PROOF STATE]
proof (state)
this:
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2
[PROOF STEP]
have z_le: "z\<le> 1"
[PROOF STATE]
proof (prove)
using this:
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2

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

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
have z_ge: "0 \<le> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> z
[PROOF STEP]
using ass
[PROOF STATE]
proof (prove)
using this:
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2

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

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
show "vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1})
                                = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
using Derivative.vector_derivative_at_within_ivl[OF g2_at_z[OF ass] z_ge z_le]
[PROOF STATE]
proof (prove)
using this:
0 < 1 \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>1 < ?z * 2; ?z \<le> 1; ?z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at ?z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (?z * 2 - 1))

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})
[PROOF STEP]
assume ass: "1 < z*2" "z \<le> 1" "z*2 - 1 \<notin> s2"
[PROOF STATE]
proof (state)
this:
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2
[PROOF STEP]
have "(g2 has_vector_derivative ((vector_derivative g2 (at (z*2 - 1))))) (at (z*2 - 1))"
[PROOF STATE]
proof (prove)
using this:
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2

goal (1 subgoal):
 1. (g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (z * 2 - 1))
[PROOF STEP]
using s2
[PROOF STATE]
proof (prove)
using this:
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2
finite s2
\<forall>x\<in>{0..1} - s2. g2 differentiable at x

goal (1 subgoal):
 1. (g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (z * 2 - 1))
[PROOF STEP]
by (auto simp: algebra_simps vector_derivative_works)
[PROOF STATE]
proof (state)
this:
(g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (z * 2 - 1))

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (z * 2 - 1))
[PROOF STEP]
have ii: "(vector_derivative g2 (at (z*2 - 1) within {0..1})) = (vector_derivative g2 (at (z*2 - 1)))"
[PROOF STATE]
proof (prove)
using this:
(g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (z * 2 - 1))

goal (1 subgoal):
 1. vector_derivative g2 (at (z * 2 - 1) within {0..1}) = vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
using Derivative.vector_derivative_at_within_ivl ass
[PROOF STATE]
proof (prove)
using this:
(g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (z * 2 - 1))
\<lbrakk>(?f has_vector_derivative ?f') (at ?x); ?a \<le> ?x; ?x \<le> ?b; ?a < ?b\<rbrakk> \<Longrightarrow> vector_derivative ?f (at ?x within {?a..?b}) = ?f'
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2

goal (1 subgoal):
 1. vector_derivative g2 (at (z * 2 - 1) within {0..1}) = vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
vector_derivative g2 (at (z * 2 - 1) within {0..1}) = vector_derivative g2 (at (z * 2 - 1))

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})
[PROOF STEP]
show "vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})
[PROOF STEP]
using i[OF ass] ii
[PROOF STATE]
proof (prove)
using this:
vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
vector_derivative g2 (at (z * 2 - 1) within {0..1}) = vector_derivative g2 (at (z * 2 - 1))

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>1 < ?z * 2; ?z \<le> 1; ?z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at ?z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (?z * 2 - 1) within {0..1})

goal (2 subgoals):
 1. line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2
 2. line_integral_exists f basis (g1 +++ g2)
[PROOF STEP]
have lem1: "((\<lambda>x. \<Sum>b\<in>basis. f ((g1+++g2) x) \<bullet> b * (vector_derivative (g1+++g2) (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1/2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1 / 2}
[PROOF STEP]
apply (rule has_integral_spike_finite [OF _ _ i1, of "insert (1/2) ((*)2 -` s1)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite (insert (1 / 2) ((*) 2 -` s1))
 2. \<And>x. x \<in> {0..1 / 2} - insert (1 / 2) ((*) 2 -` s1) \<Longrightarrow> (\<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) = 2 * (\<Sum>b\<in>basis. f (g1 (2 * x)) \<bullet> b * (vector_derivative g1 (at (2 * x) within {0..1}) \<bullet> b))
[PROOF STEP]
using s1
[PROOF STATE]
proof (prove)
using this:
finite s1
\<forall>x\<in>{0..1} - s1. g1 differentiable at x

goal (2 subgoals):
 1. finite (insert (1 / 2) ((*) 2 -` s1))
 2. \<And>x. x \<in> {0..1 / 2} - insert (1 / 2) ((*) 2 -` s1) \<Longrightarrow> (\<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) = 2 * (\<Sum>b\<in>basis. f (g1 (2 * x)) \<bullet> b * (vector_derivative g1 (at (2 * x) within {0..1}) \<bullet> b))
[PROOF STEP]
apply (force intro: finite_vimageI [where h = "(*)2"] inj_onI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..1 / 2} - insert (1 / 2) ((*) 2 -` s1) \<Longrightarrow> (\<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) = 2 * (\<Sum>b\<in>basis. f (g1 (2 * x)) \<bullet> b * (vector_derivative g1 (at (2 * x) within {0..1}) \<bullet> b))
[PROOF STEP]
apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>0 \<le> x; x * 2 \<le> 1; x * 2 \<noteq> 1; x * 2 \<notin> s1\<rbrakk> \<Longrightarrow> (\<Sum>b\<in>basis. 2 * (f (g1 (x * 2)) \<bullet> b * (vector_derivative g1 (at (x * 2) within {0..1}) \<bullet> b))) = 2 * (\<Sum>b\<in>basis. f (g1 (x * 2)) \<bullet> b * (vector_derivative g1 (at (x * 2) within {0..1}) \<bullet> b))
[PROOF STEP]
by (simp add: sum_distrib_left)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1 / 2}

goal (2 subgoals):
 1. line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2
 2. line_integral_exists f basis (g1 +++ g2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1 / 2}

goal (2 subgoals):
 1. line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2
 2. line_integral_exists f basis (g1 +++ g2)
[PROOF STEP]
have lem2: "((\<lambda>x. \<Sum>b\<in>basis. f ((g1+++g2) x) \<bullet> b * (vector_derivative (g1+++g2) (at x within {0..1}) \<bullet> b)) has_integral i2) {1/2..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i2) {1 / 2..1}
[PROOF STEP]
apply (rule has_integral_spike_finite [OF _ _ i2, of "insert (1/2) ((\<lambda>x. 2*x-1) -` s2)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite (insert (1 / 2) ((\<lambda>x. 2 * x - 1) -` s2))
 2. \<And>x. x \<in> {1 / 2..1} - insert (1 / 2) ((\<lambda>x. 2 * x - 1) -` s2) \<Longrightarrow> (\<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) = 2 * (\<Sum>b\<in>basis. f (g2 (2 * x - 1)) \<bullet> b * (vector_derivative g2 (at (2 * x - 1) within {0..1}) \<bullet> b))
[PROOF STEP]
using s2
[PROOF STATE]
proof (prove)
using this:
finite s2
\<forall>x\<in>{0..1} - s2. g2 differentiable at x

goal (2 subgoals):
 1. finite (insert (1 / 2) ((\<lambda>x. 2 * x - 1) -` s2))
 2. \<And>x. x \<in> {1 / 2..1} - insert (1 / 2) ((\<lambda>x. 2 * x - 1) -` s2) \<Longrightarrow> (\<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) = 2 * (\<Sum>b\<in>basis. f (g2 (2 * x - 1)) \<bullet> b * (vector_derivative g2 (at (2 * x - 1) within {0..1}) \<bullet> b))
[PROOF STEP]
apply (force intro: finite_vimageI [where h = "\<lambda>x. 2*x-1"] inj_onI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {1 / 2..1} - insert (1 / 2) ((\<lambda>x. 2 * x - 1) -` s2) \<Longrightarrow> (\<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) = 2 * (\<Sum>b\<in>basis. f (g2 (2 * x - 1)) \<bullet> b * (vector_derivative g2 (at (2 * x - 1) within {0..1}) \<bullet> b))
[PROOF STEP]
apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>1 \<le> x * 2; x \<le> 1; x * 2 \<noteq> 1; x * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> (\<Sum>b\<in>basis. 2 * (f (g2 (x * 2 - 1)) \<bullet> b * (vector_derivative g2 (at (x * 2 - 1) within {0..1}) \<bullet> b))) = 2 * (\<Sum>b\<in>basis. f (g2 (x * 2 - 1)) \<bullet> b * (vector_derivative g2 (at (x * 2 - 1) within {0..1}) \<bullet> b))
[PROOF STEP]
by (simp add: sum_distrib_left)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i2) {1 / 2..1}

goal (2 subgoals):
 1. line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2
 2. line_integral_exists f basis (g1 +++ g2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1 / 2}
((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i2) {1 / 2..1}
[PROOF STEP]
show "line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1 / 2}
((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i2) {1 / 2..1}

goal (1 subgoal):
 1. line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2
[PROOF STEP]
apply (simp add: line_integral_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1 / 2}; ((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i2) {1 / 2..1}\<rbrakk> \<Longrightarrow> integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. f (g1 x) \<bullet> b * (vector_derivative g1 (at x within {0..1}) \<bullet> b)) + integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. f (g2 x) \<bullet> b * (vector_derivative g2 (at x within {0..1}) \<bullet> b))
[PROOF STEP]
apply (rule integral_unique [OF has_integral_combine [where c = "1/2"]])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1 / 2}; ((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i2) {1 / 2..1}\<rbrakk> \<Longrightarrow> 0 \<le> 1 / 2
 2. \<lbrakk>((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1 / 2}; ((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i2) {1 / 2..1}\<rbrakk> \<Longrightarrow> 1 / 2 \<le> 1
 3. \<lbrakk>((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1 / 2}; ((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i2) {1 / 2..1}\<rbrakk> \<Longrightarrow> ((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. f (g1 x) \<bullet> b * (vector_derivative g1 (at x within {0..1}) \<bullet> b))) {0..1 / 2}
 4. \<lbrakk>((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1 / 2}; ((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i2) {1 / 2..1}\<rbrakk> \<Longrightarrow> ((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. f (g2 x) \<bullet> b * (vector_derivative g2 (at x within {0..1}) \<bullet> b))) {1 / 2..1}
[PROOF STEP]
using 1 2 integral_unique
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. \<Sum>b\<in>basis. f (g1 x) \<bullet> b * (vector_derivative g1 (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1}
((\<lambda>x. \<Sum>b\<in>basis. f (g2 x) \<bullet> b * (vector_derivative g2 (at x within {0..1}) \<bullet> b)) has_integral i2) {0..1}
(?f has_integral ?y) ?k \<Longrightarrow> integral ?k ?f = ?y

goal (4 subgoals):
 1. \<lbrakk>((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1 / 2}; ((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i2) {1 / 2..1}\<rbrakk> \<Longrightarrow> 0 \<le> 1 / 2
 2. \<lbrakk>((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1 / 2}; ((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i2) {1 / 2..1}\<rbrakk> \<Longrightarrow> 1 / 2 \<le> 1
 3. \<lbrakk>((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1 / 2}; ((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i2) {1 / 2..1}\<rbrakk> \<Longrightarrow> ((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. f (g1 x) \<bullet> b * (vector_derivative g1 (at x within {0..1}) \<bullet> b))) {0..1 / 2}
 4. \<lbrakk>((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1 / 2}; ((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i2) {1 / 2..1}\<rbrakk> \<Longrightarrow> ((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. f (g2 x) \<bullet> b * (vector_derivative g2 (at x within {0..1}) \<bullet> b))) {1 / 2..1}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2

goal (1 subgoal):
 1. line_integral_exists f basis (g1 +++ g2)
[PROOF STEP]
show "line_integral_exists f basis (g1 +++ g2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists f basis (g1 +++ g2)
[PROOF STEP]
proof (simp add: line_integral_exists_def integrable_on_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y. ((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral y) {0..1}
[PROOF STEP]
have "(1::real) \<le> 1 * 2 \<and> (0::real) \<le> 1 / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> 1 * 2 \<and> 0 \<le> 1 / 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<le> 1 * 2 \<and> 0 \<le> 1 / 2

goal (1 subgoal):
 1. \<exists>y. ((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral y) {0..1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 \<le> 1 * 2 \<and> 0 \<le> 1 / 2
[PROOF STEP]
show "\<exists>r. ((\<lambda>r. \<Sum>a\<in>basis. f ((g1 +++ g2) r) \<bullet> a * (vector_derivative (g1 +++ g2) (at r within {0..1}) \<bullet> a)) has_integral r) {0..1}"
[PROOF STATE]
proof (prove)
using this:
1 \<le> 1 * 2 \<and> 0 \<le> 1 / 2

goal (1 subgoal):
 1. \<exists>r. ((\<lambda>r. \<Sum>a\<in>basis. f ((g1 +++ g2) r) \<bullet> a * (vector_derivative (g1 +++ g2) (at r within {0..1}) \<bullet> a)) has_integral r) {0..1}
[PROOF STEP]
using has_integral_combine [where c = "1/2"] 1 2 divide_le_eq_numeral1(1) lem1 lem2
[PROOF STATE]
proof (prove)
using this:
1 \<le> 1 * 2 \<and> 0 \<le> 1 / 2
\<lbrakk>?a \<le> 1 / 2; 1 / 2 \<le> ?b; (?f has_integral ?i) {?a..1 / 2}; (?f has_integral ?j) {1 / 2..?b}\<rbrakk> \<Longrightarrow> (?f has_integral ?i + ?j) {?a..?b}
((\<lambda>x. \<Sum>b\<in>basis. f (g1 x) \<bullet> b * (vector_derivative g1 (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1}
((\<lambda>x. \<Sum>b\<in>basis. f (g2 x) \<bullet> b * (vector_derivative g2 (at x within {0..1}) \<bullet> b)) has_integral i2) {0..1}
(?b / numeral ?w \<le> ?a) = (?b \<le> ?a * numeral ?w)
((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i1) {0..1 / 2}
((\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) has_integral i2) {1 / 2..1}

goal (1 subgoal):
 1. \<exists>r. ((\<lambda>r. \<Sum>a\<in>basis. f ((g1 +++ g2) r) \<bullet> a * (vector_derivative (g1 +++ g2) (at r within {0..1}) \<bullet> a)) has_integral r) {0..1}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>r. ((\<lambda>r. \<Sum>a\<in>basis. f ((g1 +++ g2) r) \<bullet> a * (vector_derivative (g1 +++ g2) (at r within {0..1}) \<bullet> a)) has_integral r) {0..1}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
line_integral_exists f basis (g1 +++ g2)

goal:
No subgoals!
[PROOF STEP]
qed