I have this code:
xP = x - 1; implication3 = Implies[xP == x - 1 && x \[Element] Integers && x > 1 && Mod[x, 2] == 1, Floor[Log[2, x]] == Floor[Log[2, xP]]]; simpleImplication3 = FullSimplify[implication3]; isValid3 = Resolve[ForAll[{x, xP}, implication3]]
I want isValid3 to either return True or False depending on whether the Implication I have provided is True (it should return True given the conditions). But it just returns the implication back. I have used this general form of proving implications before on less complex expressions and it has returned either True or False. What am I doing wrong here? Maybe Resolve doesn't do what I think it does?
I doubt that Mathematica can do this, since it cannot even do the following:
Reduce[ForAll[k, Element[k, PositiveIntegers], Element[2^k, Integers]]]
or this:
Reduce[ForAll[k, Element[k, PositiveIntegers], Element[1/k, Integers]]]
I am thinking that the combination of Floor and Log is making this difficult. Is there any way that you could eliminate those and write the problem in terms of 2*n+1<2*n+1+1<2*(n+1)+1 and from that the conclusion must be True?
Floor
Log
2*n+1<2*n+1+1<2*(n+1)+1
