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 ⊢ 𝐴 ∈ ℝ
Assertion renegcli - 𝐴 ∈ ℝ

Proof

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