[STATEMENT]
lemma gen_binomial_complex':
  fixes x y :: real and a :: complex
  assumes "\<bar>x\<bar> < \<bar>y\<bar>"
  shows   "(\<lambda>n. (a gchoose n) * of_real x^n * of_real y powr (a - of_nat n)) sums
               of_real (x + y) powr a" (is "?P x y")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
fix x y :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
assume xy: "\<bar>x\<bar> < \<bar>y\<bar>" "y \<ge> 0"
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
hence "y > 0"
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y

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

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
note xy = xy this
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y
0 < y

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
from xy
[PROOF STATE]
proof (chain)
picking this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y
0 < y
[PROOF STEP]
have "(\<lambda>n. (a gchoose n) * of_real (x / y) ^ n) sums (1 + of_real (x / y)) powr a"
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y
0 < y

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n) sums (1 + complex_of_real (x / y)) powr a
[PROOF STEP]
by (intro gen_binomial_complex) (simp add: norm_divide)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n) sums (1 + complex_of_real (x / y)) powr a

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
hence "(\<lambda>n. (a gchoose n) * of_real (x / y) ^ n * y powr a) sums
               ((1 + of_real (x / y)) powr a * y powr a)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n) sums (1 + complex_of_real (x / y)) powr a

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n * complex_of_real y powr a) sums ((1 + complex_of_real (x / y)) powr a * complex_of_real y powr a)
[PROOF STEP]
by (rule sums_mult2)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n * complex_of_real y powr a) sums ((1 + complex_of_real (x / y)) powr a * complex_of_real y powr a)

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n * complex_of_real y powr a) sums ((1 + complex_of_real (x / y)) powr a * complex_of_real y powr a)

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
have "(1 + complex_of_real (x / y)) = complex_of_real (1 + x/y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + complex_of_real (x / y) = complex_of_real (1 + x / y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 + complex_of_real (x / y) = complex_of_real (1 + x / y)

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 + complex_of_real (x / y) = complex_of_real (1 + x / y)

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
from xy
[PROOF STATE]
proof (chain)
picking this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y
0 < y
[PROOF STEP]
have "\<dots> powr a * of_real y powr a = (\<dots> * y) powr a"
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y
0 < y

goal (1 subgoal):
 1. complex_of_real (1 + x / y) powr a * complex_of_real y powr a = (complex_of_real (1 + x / y) * complex_of_real y) powr a
[PROOF STEP]
by (subst powr_times_real[symmetric]) (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
complex_of_real (1 + x / y) powr a * complex_of_real y powr a = (complex_of_real (1 + x / y) * complex_of_real y) powr a

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
complex_of_real (1 + x / y) powr a * complex_of_real y powr a = (complex_of_real (1 + x / y) * complex_of_real y) powr a

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
from xy
[PROOF STATE]
proof (chain)
picking this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y
0 < y
[PROOF STEP]
have "complex_of_real (1 + x / y) * complex_of_real y = of_real (x + y)"
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y
0 < y

goal (1 subgoal):
 1. complex_of_real (1 + x / y) * complex_of_real y = complex_of_real (x + y)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
complex_of_real (1 + x / y) * complex_of_real y = complex_of_real (x + y)

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n * complex_of_real y powr a) sums complex_of_real (x + y) powr a
[PROOF STEP]
have "?P x y"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n * complex_of_real y powr a) sums complex_of_real (x + y) powr a

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
using xy
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n * complex_of_real y powr a) sums complex_of_real (x + y) powr a
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y
0 < y

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
by (simp add: field_simps powr_diff powr_nat)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<bar>?xa2\<bar> < \<bar>?ya2\<bar>; 0 \<le> ?ya2\<rbrakk> \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real ?xa2 ^ n * complex_of_real ?ya2 powr (a - of_nat n)) sums complex_of_real (?xa2 + ?ya2) powr a

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
note A = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<bar>?xa2\<bar> < \<bar>?ya2\<bar>; 0 \<le> ?ya2\<rbrakk> \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real ?xa2 ^ n * complex_of_real ?ya2 powr (a - of_nat n)) sums complex_of_real (?xa2 + ?ya2) powr a

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
proof (cases "y < 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
assume y: "y < 0"
[PROOF STATE]
proof (state)
this:
y < 0

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<bar>x\<bar> < \<bar>y\<bar>
y < 0
[PROOF STEP]
have xy: "x + y < 0"
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> < \<bar>y\<bar>
y < 0

goal (1 subgoal):
 1. x + y < 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x + y < 0

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<bar>x\<bar> < \<bar>y\<bar>
x + y < 0
[PROOF STEP]
have "\<bar>-x\<bar> < \<bar>-y\<bar>" "-y \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> < \<bar>y\<bar>
x + y < 0

goal (1 subgoal):
 1. \<bar>- x\<bar> < \<bar>- y\<bar> &&& 0 \<le> - y
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<bar>- x\<bar> < \<bar>- y\<bar>
0 \<le> - y

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
note A[OF this]
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n)) sums complex_of_real (- x + - y) powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n)) sums complex_of_real (- x + - y) powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
have "complex_of_real (-x + -y) = - complex_of_real (x + y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_of_real (- x + - y) = - complex_of_real (x + y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
complex_of_real (- x + - y) = - complex_of_real (x + y)

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
complex_of_real (- x + - y) = - complex_of_real (x + y)

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
from xy assms
[PROOF STATE]
proof (chain)
picking this:
x + y < 0
\<bar>x\<bar> < \<bar>y\<bar>
[PROOF STEP]
have "... powr a = (-1) powr -a * of_real (x + y) powr a"
[PROOF STATE]
proof (prove)
using this:
x + y < 0
\<bar>x\<bar> < \<bar>y\<bar>

goal (1 subgoal):
 1. (- complex_of_real (x + y)) powr a = (- 1) powr - a * complex_of_real (x + y) powr a
[PROOF STEP]
by (subst powr_neg_real_complex) (simp add: abs_real_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
(- complex_of_real (x + y)) powr a = (- 1) powr - a * complex_of_real (x + y) powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(- complex_of_real (x + y)) powr a = (- 1) powr - a * complex_of_real (x + y) powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(- complex_of_real (x + y)) powr a = (- 1) powr - a * complex_of_real (x + y) powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
from y
[PROOF STATE]
proof (chain)
picking this:
y < 0
[PROOF STEP]
have "(a gchoose n) * of_real (-x) ^ n * of_real (-y) powr (a - of_nat n) =
                       (a gchoose n) * (-of_real x / -of_real y) ^ n * (- of_real y) powr a"
[PROOF STATE]
proof (prove)
using this:
y < 0

goal (1 subgoal):
 1. (a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n) = (a gchoose n) * (- complex_of_real x / - complex_of_real y) ^ n * (- complex_of_real y) powr a
[PROOF STEP]
by (subst power_divide) (simp add: powr_diff powr_nat)
[PROOF STATE]
proof (state)
this:
(a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n) = (a gchoose n) * (- complex_of_real x / - complex_of_real y) ^ n * (- complex_of_real y) powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n) = (a gchoose n) * (- complex_of_real x / - complex_of_real y) ^ n * (- complex_of_real y) powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
from y
[PROOF STATE]
proof (chain)
picking this:
y < 0
[PROOF STEP]
have "(- of_real y) powr a = (-1) powr -a * of_real y powr a"
[PROOF STATE]
proof (prove)
using this:
y < 0

goal (1 subgoal):
 1. (- complex_of_real y) powr a = (- 1) powr - a * complex_of_real y powr a
[PROOF STEP]
by (subst powr_neg_real_complex) simp
[PROOF STATE]
proof (state)
this:
(- complex_of_real y) powr a = (- 1) powr - a * complex_of_real y powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(- complex_of_real y) powr a = (- 1) powr - a * complex_of_real y powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
have "-complex_of_real x / -complex_of_real y = complex_of_real x / complex_of_real y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - complex_of_real x / - complex_of_real y = complex_of_real x / complex_of_real y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- complex_of_real x / - complex_of_real y = complex_of_real x / complex_of_real y

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- complex_of_real x / - complex_of_real y = complex_of_real x / complex_of_real y

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
have "... ^ n = of_real x ^ n / of_real y ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (complex_of_real x / complex_of_real y) ^ n = complex_of_real x ^ n / complex_of_real y ^ n
[PROOF STEP]
by (simp add: power_divide)
[PROOF STATE]
proof (state)
this:
(complex_of_real x / complex_of_real y) ^ n = complex_of_real x ^ n / complex_of_real y ^ n

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(complex_of_real x / complex_of_real y) ^ n = complex_of_real x ^ n / complex_of_real y ^ n

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
have "(a gchoose n) * ... * ((-1) powr -a * of_real y powr a) =
                   (-1) powr -a * ((a gchoose n) * of_real x ^ n * of_real y powr (a - n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a gchoose n) * (complex_of_real x ^ n / complex_of_real y ^ n) * ((- 1) powr - a * complex_of_real y powr a) = (- 1) powr - a * ((a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n))
[PROOF STEP]
by (simp add: algebra_simps powr_diff powr_nat)
[PROOF STATE]
proof (state)
this:
(a gchoose n) * (complex_of_real x ^ n / complex_of_real y ^ n) * ((- 1) powr - a * complex_of_real y powr a) = (- 1) powr - a * ((a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n))

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n) = (- 1) powr - a * ((a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n))
[PROOF STEP]
have "(a gchoose n) * of_real (- x) ^ n * of_real (- y) powr (a - of_nat n) =
                      (-1) powr -a * ((a gchoose n) * of_real x ^ n * of_real y powr (a - of_nat n))"
[PROOF STATE]
proof (prove)
using this:
(a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n) = (- 1) powr - a * ((a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n))

goal (1 subgoal):
 1. (a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n) = (- 1) powr - a * ((a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n) = (- 1) powr - a * ((a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n))

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(a gchoose ?n2) * complex_of_real (- x) ^ ?n2 * complex_of_real (- y) powr (a - of_nat ?n2) = (- 1) powr - a * ((a gchoose ?n2) * complex_of_real x ^ ?n2 * complex_of_real y powr (a - of_nat ?n2))

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
note sums_cong[OF this]
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose ?n3 n) * complex_of_real (- x) ^ ?n3 n * complex_of_real (- y) powr (a - of_nat (?n3 n))) sums ?c = (\<lambda>n. (- 1) powr - a * ((a gchoose ?n3 n) * complex_of_real x ^ ?n3 n * complex_of_real y powr (a - of_nat (?n3 n)))) sums ?c

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. (- 1) powr - a * ((a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n))) sums ((- 1) powr - a * complex_of_real (x + y) powr a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (- 1) powr - a * ((a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n))) sums ((- 1) powr - a * complex_of_real (x + y) powr a)

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
by (simp add: sums_mult_iff)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a

goal (1 subgoal):
 1. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
qed (insert A[of x y] assms, simp_all add: not_less)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a

goal:
No subgoals!
[PROOF STEP]
qed