Proofs involving multiple quantifiers?

Question

I'll just give this simple example to illustrate my point:

There exists a real number $x$ such that for every real number $y$, we have $xy=y$.

If I wish to prove this statement in a non-constructive way, that is to say, without explicitly assigning to $x$ the value $1$ and thereby proving the statement, I don't know how to do it.

My first problem arises in translating the sentence into logical connectives. I could say:

$$(\exists x )[x \in \mathbb{R} \, \land \forall y(y \in \mathbb{R} \implies xy=y) ]$$

But then, how could I take - for example - something like the contrapositive of the implication when it's all embedded in these quantifiers, not to mention the conjunction? Surely I can't just take the contrapositive of the embedded implication as if it were a standalone implication, considering all the intertwined connectives and quantifiers surrounding it?

Edit: Allow me to add in this quick edit. My problem is in part that I have no clue how I would go about deriving a contradiction from the negated statement above. If I wish to do a proof by contradiction, I first negate the above expression to the shorthand $\forall x \in \mathbb{R}, \exists y \in \mathbb{R}, xy \neq y$. However, what's next? I presume it would start off like:

Let $x$ be an arbitrary real number. Then...

But I don't quite understand what I would do in this particular case.

Answer 1

I'm not sure why you'd want to prove a statement nonconstructively if a constructive proof is available, as is the case in this example, but in any case, a general tactic would be to double-negate the entire expression, commute the inner negation operator, and prove the resulting (equivalent) statement by contradiction.

In your examples, the statement is $$\exists x \in \mathbb{R},\, \forall y \in \mathbb{R},\, xy=x$$ Double-negating the expression, we obtain the equivalent expression: $$\neg \neg (\exists x \in \mathbb{R},\, \forall y \in \mathbb{R},\, xy=x)$$ Commuting the inner negation operator, we obtain the equivalent expression: $$\neg (\forall x \in \mathbb{R},\, \exists y \in \mathbb{R},\, xy \ne x)$$ So now, your task is to assume $\forall x \in \mathbb{R},\, \exists y \in \mathbb{R},\, xy \ne x$ and derive a contradiction.

Note that I've used $\forall x \in \mathbb{R},\, p(x)$ and $\exists x \in \mathbb{R},\, q(x)$ to abbreviate $\forall x (x \in \mathbb{R} \Rightarrow p(x))$ and $\exists x (x \in \mathbb{R} \wedge q(x))$, as is standard.

To address your specific question about contrapositives: you can replace any subformula of a formula by an equivalent subformula, and you'll obtain an equivalent formula. Since the contrapositive of an implication is equivalent to the original implication, this means that you can replace any implications you like by their contrapositives, even if they're embedded in a larger formula.