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

Metamath Proof Explorer

Theorem reneg0addlid

Description: Negative zero is a left additive identity. (Contributed by Steven Nguyen, 7-Jan-2023)

Ref Expression
Assertion reneg0addlid ⊢ A ∈ ℝ → 0 - ℝ 0 + A = A

Proof

Step Hyp Ref Expression
1 elre0re ⊢ A ∈ ℝ → 0 ∈ ℝ
2 rernegcl ⊢ 0 ∈ ℝ → 0 - ℝ 0 ∈ ℝ
3 elre0re ⊢ 0 ∈ ℝ → 0 ∈ ℝ
4 renegid ⊢ 0 ∈ ℝ → 0 + 0 - ℝ 0 = 0
5 2 3 4 readdridaddlidd ⊢ 0 ∈ ℝ ∧ A ∈ ℝ → 0 - ℝ 0 + A = A
6 1 5 mpancom ⊢ A ∈ ℝ → 0 - ℝ 0 + A = A