It's slightly subtle. To get a sense of why your In[3]
returns True
you need to see how the expression is evaluated. The short answer is that the expression inside of it,
Sum[q^k, {k, Infinity}] == -q/(-1 + q)
is evaluated before the other things are evaluated. So it first is turned into
-q/(-1 + q) == -q/(-1 + q)
and then the rest of your quantifiers are subsequently being applied to the simple expression which is just the symbol
True
which of course is always True
. To see this unfold make use of TracePrint
to see some the evaluations that Mathematica is doing
ForAll[q, Element[q, Reals],
Sum[q^k, {k, Infinity}] == -q/(-1 + q)] // TracePrint
which gives (it displays in a notebook differently but I have changed it to InputForm
for readability in this forum):
HoldForm[ForAll[q, Element[q, Reals], Sum[q^k, {k, Infinity}] == -q/(-1 + q)]]
HoldForm[ForAll]
HoldForm[ForAll[q, Element[q, Reals], True]]
HoldForm[ForAll]
HoldForm[True]