Metamath Proof Explorer


Theorem infm3lem

Description: Lemma for infm3 . (Contributed by NM, 14-Jun-2005)

Ref Expression
Assertion infm3lem ( 𝑥 ∈ ℝ → ∃ 𝑦 ∈ ℝ 𝑥 = - 𝑦 )

Proof

Step Hyp Ref Expression
1 renegcl ( 𝑥 ∈ ℝ → - 𝑥 ∈ ℝ )
2 recn ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
3 2 negnegd ( 𝑥 ∈ ℝ → - - 𝑥 = 𝑥 )
4 3 eqcomd ( 𝑥 ∈ ℝ → 𝑥 = - - 𝑥 )
5 negeq ( 𝑦 = - 𝑥 → - 𝑦 = - - 𝑥 )
6 5 rspceeqv ( ( - 𝑥 ∈ ℝ ∧ 𝑥 = - - 𝑥 ) → ∃ 𝑦 ∈ ℝ 𝑥 = - 𝑦 )
7 1 4 6 syl2anc ( 𝑥 ∈ ℝ → ∃ 𝑦 ∈ ℝ 𝑥 = - 𝑦 )