Well, given the hypothesis that x=1, you can do the following:
(%i1) x;
(%o1)
3*((3-2^(3/2))*log(17-3*2^(5/2))+(6-2^(5/2))*log(3-2^(3/2))-3*2^(7/2)+32)
/((3*2^(9/2)-72)*(log(sqrt(2)+1)+sqrt(2)))
(%i2) logcontract(gfactor(%))=1;
(%o2)
(2^(7/2)-log(-(2^(3/2)-3)^2*(3*2^(5/2)-17)))/(log((sqrt(2)+1)^8)+2^(7/2)) =
1
(%i3) %*part(%,1,2);
(%o3) 2^(7/2)-log(-(2^(3/2)-3)^2*(3*2^(5/2)-17)) =
log((sqrt(2)+1)^8)+2^(7/2)
(%i4) map(exp,%);
(%o4) -%e^2^(7/2)/((2^(3/2)-3)^2*(3*2^(5/2)-17)) = (sqrt(2)+1)^8*%e^2^(7/2)
(%i5) ratsimp(lhs(%)/rhs(%));
(%o5) 1
Each step here preserves truth of the equation reversibly (no
multiplications by 0 etc.).
-s
On Wed, May 16, 2012 at 11:31 PM, Raymond Toy <toy.raymond at gmail.com> wrote:
> On 5/14/12 3:42 PM, Richard Fateman wrote:
> > xnum :
> >
> ((6-4*sqrt(2))*log(3-2*sqrt(2))+(3-2*sqrt(2))*log(17-12*sqrt(2))+32-24*sqrt(2));
> >
> > xden :(48*sqrt(2)-72)*(log(sqrt(2)+1)+sqrt(2))/3;
> > x : xnum/xden;
> >
>
> Can you get maxima to prove that x = 1?
>
> I can get:
>
> factor(expand(logcontract(gfactor(x))))
> -> -(log(577-51*2^(7/2))-2^(7/2))/(log(51*2^(7/2)+577)+2^(7/2))
>
> If I stare at it, I can see that the numerator and the denominator are
> exactly the same except for the arg of the logs. But a quick check
> shows that 1/(51*2^(7/2)+577) = 577-51*2^(7/2), so, in fact, x = 1.
>
> But how do I get maxima to do this for me, other doing what I described
> above by hand?
>
> I'm just curious.
>
> Ray
>
>
> _______________________________________________
> Maxima mailing list
> Maxima at math.utexas.edu
> http://www.math.utexas.edu/mailman/listinfo/maxima
>