2
$\begingroup$

Check the Edited too, please:
i have a simple equation which i expect to get TRUE from Implies but it just returns the same thing to me. Implies works well for easier examples but I have some more complicated equations need to verify. please help me if yu know:

FullSimplify[Implies[xP == x + 1 && yP == y - 1 , x + y == xP + yP]]

the output:
1 + x != xP || x + y == xP + yP || y != 1 + yP

I need to verify some quations like this if implies to TRUE of FALSE. what could be the alternative if Implies does not works for these type of calculations? thanks

EDITED

based on good answers below, I tried my another equations. I see that for this new equation With works and Resolve[Implies[...]] does not work. So is there something wrong with my implies? i need to know any consequences around this because I have too many equations like these.

Resolve[ForAll[{x, xP, y, yP},Implies[xP == x + 1 && yP == 2*y ,  y/(2^x) == yP/(2^(xP))],Integers]] 

output:
    (x,y,....) xP == 1 + x && yP == 2 y \[Implies] 2^-x y == 2^(1 - xP) y

But With makes it True

With[{yP = 2*y  , xP = x + 1},  y/(2^x) == (yP)/(2^(xP))]
True
$\endgroup$
6
  • 2
    $\begingroup$ Why not the simple With[{xP = x + 1, yP = y - 1}, x + y == xP + yP] which returns True? $\endgroup$
    – bmf
    Apr 22 at 14:46
  • $\begingroup$ @bmf that's great answer but could you see my edited. really appreciate $\endgroup$
    – Azzurro94
    Apr 22 at 16:53
  • $\begingroup$ I just saw the edited comment. Not sure what to add, since what I suggested works fine. You might be interested in knowing that Resolve[ForAll[{x, xP, y, yP}, Implies[xP == x + 1 && yP == 2*y, y/(2^x) == yP/(2^(xP))]]] yields True for your second expression. $\endgroup$
    – bmf
    Apr 22 at 17:16
  • 1
    $\begingroup$ And of course, this Resolve[ForAll[{x, xP, y, yP}, Implies[xP == x + 1 && yP == 2*y, y/(2^x) == yP/(2^(xP))]], Integers] also gives True if you want to insist on Integers $\endgroup$
    – bmf
    Apr 22 at 17:17
  • 1
    $\begingroup$ Yes, you need to be a bit careful with all the brackets. Glad I was able to help :) $\endgroup$
    – bmf
    Apr 22 at 18:24

2 Answers 2

4
$\begingroup$

The ForAll quantifier does the job:

Resolve[ForAll[{xP, yP, x, y},   Implies[xP == x + 1 && yP == y - 1, x + y == xP + yP]]]

True

$\endgroup$
1
  • $\begingroup$ that works great for it, but could you see my Edited. really appreciate $\endgroup$
    – Azzurro94
    Apr 22 at 16:54
3
$\begingroup$

I want to summarize all I learned here and my mistake for second equation. both function Implies and With works, my mistake for my second expression was putting Integers inside the ForAll, so the right answer is below:

Resolve[ForAll[{x, xP, y, yP},Implies[xP == x + 1 && yP == 2*y ,  y/(2^x) == yP/(2^(xP))]],Integers] 

Also With works same.

With[{yP = 2*y  , xP = x + 1},  y/(2^x) == (yP)/(2^(xP))]
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.