This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem renegcli

Description: Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl is deprecated, but is retained for its demonstration value.) (Contributed by NM, 17-Jan-1997) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Hypothesis renegcl.1 ⊢ A ∈ ℝ
Assertion renegcli ⊢ − A ∈ ℝ

Proof

Step Hyp Ref Expression
1 renegcl.1 ⊢ A ∈ ℝ
2 ax-rnegex ⊢ A ∈ ℝ → ∃ x ∈ ℝ A + x = 0
3 recn ⊢ x ∈ ℝ → x ∈ ℂ
4 df-neg ⊢ − A = 0 − A
5 4 eqeq1i ⊢ − A = x ↔ 0 − A = x
6 0cn ⊢ 0 ∈ ℂ
7 1 recni ⊢ A ∈ ℂ
8 subadd ⊢ 0 ∈ ℂ ∧ A ∈ ℂ ∧ x ∈ ℂ → 0 − A = x ↔ A + x = 0
9 6 7 8 mp3an12 ⊢ x ∈ ℂ → 0 − A = x ↔ A + x = 0
10 5 9 bitrid ⊢ x ∈ ℂ → − A = x ↔ A + x = 0
11 3 10 syl ⊢ x ∈ ℝ → − A = x ↔ A + x = 0
12 eleq1a ⊢ x ∈ ℝ → − A = x → − A ∈ ℝ
13 11 12 sylbird ⊢ x ∈ ℝ → A + x = 0 → − A ∈ ℝ
14 13 rexlimiv ⊢ ∃ x ∈ ℝ A + x = 0 → − A ∈ ℝ
15 1 2 14 mp2b ⊢ − A ∈ ℝ