Description: Negative zero is a left additive identity. (Contributed by Steven Nguyen, 7-Jan-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | reneg0addid2 | ⊢ ( 𝐴 ∈ ℝ → ( ( 0 −ℝ 0 ) + 𝐴 ) = 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elre0re | ⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ ) | |
2 | rernegcl | ⊢ ( 0 ∈ ℝ → ( 0 −ℝ 0 ) ∈ ℝ ) | |
3 | elre0re | ⊢ ( 0 ∈ ℝ → 0 ∈ ℝ ) | |
4 | renegid | ⊢ ( 0 ∈ ℝ → ( 0 + ( 0 −ℝ 0 ) ) = 0 ) | |
5 | 2 3 4 | readdid1addid2d | ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 0 −ℝ 0 ) + 𝐴 ) = 𝐴 ) |
6 | 1 5 | mpancom | ⊢ ( 𝐴 ∈ ℝ → ( ( 0 −ℝ 0 ) + 𝐴 ) = 𝐴 ) |