Description: Lemma for infm3 . (Contributed by NM, 14-Jun-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | infm3lem | ⊢ ( 𝑥 ∈ ℝ → ∃ 𝑦 ∈ ℝ 𝑥 = - 𝑦 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | renegcl | ⊢ ( 𝑥 ∈ ℝ → - 𝑥 ∈ ℝ ) | |
2 | recn | ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ ) | |
3 | 2 | negnegd | ⊢ ( 𝑥 ∈ ℝ → - - 𝑥 = 𝑥 ) |
4 | 3 | eqcomd | ⊢ ( 𝑥 ∈ ℝ → 𝑥 = - - 𝑥 ) |
5 | negeq | ⊢ ( 𝑦 = - 𝑥 → - 𝑦 = - - 𝑥 ) | |
6 | 5 | rspceeqv | ⊢ ( ( - 𝑥 ∈ ℝ ∧ 𝑥 = - - 𝑥 ) → ∃ 𝑦 ∈ ℝ 𝑥 = - 𝑦 ) |
7 | 1 4 6 | syl2anc | ⊢ ( 𝑥 ∈ ℝ → ∃ 𝑦 ∈ ℝ 𝑥 = - 𝑦 ) |