# Performing an inductive proof

I have an expression which depends on a variable n and am certain it evaluates to 1 for all n with n=1/2,1,3/2,...

I want to do an inductive proof that this is true but the actual formula is too messy so want mathematica to do it for me. Say the sum depending on n is f[n]. How do I impose the required conditions on f[n] and get it to check for f[n+1/2]?

f[n_]=(1/(4 n)!)(-1)^(1 + 2 n) I^(1 + 4 n) ((2 n)!)^2 Pochhammer[-2 n - I (\[Theta][1] -\[Theta][2]),
1 + 4 n] \!$$\*UnderoverscriptBox[\(\[Sum]$$, $$k[1] = 0$$, $$2\ n$$]$$\*UnderoverscriptBox[\(\[Sum]$$, $$k[2] = 0$$, $$2\ n$$]$$(\*SuperscriptBox[\((\(-1$$)\),$$\(-1$$ - 2\ n - k[1] + k[2]\)]\ \*SuperscriptBox[$$I$$, $$\(-4$$\ n\)]\ $$(\(-I$$\ $$(k[1] - k[2])$$ + \[Theta][1] - \[Theta][2])\)\ \*SuperscriptBox[$$(I\ \((2\ n -k[1] - k[2])$$ + \[Theta][          1] + \[Theta][2])\), $$4\ n$$])\)/$$(\(\((2\ n - k[1])$$!\)\ $$k[1]!$$\ $$\((2\ n - k[2])$$!\)\ $$k[ 2]!$$\ Pochhammer[$$-k[2]$$ +
I\ $$(\[Theta][1] - \[Theta][2])$$,
1 + 2\ n]\ Pochhammer[$$-k[1]$$ - I\ \[Theta][1] +
I\ \[Theta][2], 1 + 2\ n])\)\)\)


Copying and pasting this into mathematica gives the correct function.

As you can test, setting n=1/2,1,3/2,... does indeed give 1. But I dont think mathematica can show this in general.

[Theta][1] and [Theta][2] are fixed complex numbers. k[1] and k[2] are just summation parameters, each one is summed between 0 and 2n.

• Please post the equation in copyable form. Mar 6, 2015 at 19:24
• Please post code as input text (Edit>Copy As). Mar 7, 2015 at 8:36
• There are undefined functions (k & \[Theta]) in your definition of f. Mar 7, 2015 at 13:30
• Fixed @Karsten7. Mar 7, 2015 at 13:45
• Welcome to Mathematica.SE! I suggest that: 1) You take the introductory Tour now! 2) When you see good questions and answers, vote them up by clicking the gray triangles, because the credibility of the system is based on the reputation gained by users sharing their knowledge. Also, please remember to accept the answer, if any, that solves your problem, by clicking the checkmark sign! 3) As you receive help, try to give it too, by answering questions in your area of expertise. Mar 9, 2015 at 3:28

f[n_] := Sin[n Pi]^2

Assuming[n ∈ Integers, Simplify[f[1/2] == f[n + 1/2] == 1]]

True


Or

Solve[f[1/2] == f[n + 1/2] == 1, n, Integers]

{{n -> ConditionalExpression[C[1], C[1] ∈ Integers]}}


Or

Reduce[f[1/2] == f[n + 1/2] == 1, n, Integers]

C[1] ∈ Integers && n == C[1]

• I've added the actual function to my first post. Unfortunately your method is not working for me. Mar 6, 2015 at 21:11

One example: we wish to prove that the $n$th triangular number is $n(n+1)/2$. We know the recurrence relation:

$$f(n) = f(n-1) + n$$

To check that our expression is correct, we simply substitute it in to our relation, like so:

f[n] == f[n - 1] + n /. {f -> (# (# + 1)/2 &)}
(* 1/2 n (1 + n) == n + 1/2 (-1 + n) n *)


Then we can use Reduce to check that the above statement holds:

Reduce[%]
(* True *)


You'll just use your specific inductive relation, with f[n + 1/2] == g[f[n],n] or something similar.

Side note: you may be able to use RSolve to get the closed-form expression, like this:

f[n] /. RSolve[f[n] == f[n - 1] + n && f[0] == 0, f, n]
(* {1/2 n (1 + n)} *)


(Note that to find the solution, you need to provide the base case(s), in this case f[0] == 0.)