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