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

Metamath Proof Explorer

Theorem renegcl

Description: Closure law for negative of reals. The weak deduction theorem dedth is used to convert hypothesis of the inference (deduction) form of this theorem, renegcli , to an antecedent. (Contributed by NM, 20-Jan-1997) (Proof modification is discouraged.)

Ref Expression
Assertion renegcl ⊢ A ∈ ℝ → − A ∈ ℝ

Proof

Step Hyp Ref Expression
1 negeq ⊢ A = if A ∈ ℝ A 1 → − A = − if A ∈ ℝ A 1
2 1 eleq1d ⊢ A = if A ∈ ℝ A 1 → − A ∈ ℝ ↔ − if A ∈ ℝ A 1 ∈ ℝ
3 1re ⊢ 1 ∈ ℝ
4 3 elimel ⊢ if A ∈ ℝ A 1 ∈ ℝ
5 4 renegcli ⊢ − if A ∈ ℝ A 1 ∈ ℝ
6 2 5 dedth ⊢ A ∈ ℝ → − A ∈ ℝ