How to prove an implication involving logarithms?

Questions
,
1

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?

2

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?

3

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]]]