Metamath Proof Explorer

Theorem resubeulem1

Description: Lemma for resubeu . A value which when added to zero, results in negative zero. (Contributed by Steven Nguyen, 7-Jan-2023)

Ref Expression
Assertion resubeulem1 ( 𝐴 ∈ ℝ → ( 0 + ( 0 −ℝ ( 0 + 0 ) ) ) = ( 0 −ℝ 0 ) )

Proof

Step Hyp Ref Expression
1 elre0re ⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
2 1 recnd ⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℂ )
3 1 1 readdcld ⊢ ( 𝐴 ∈ ℝ → ( 0 + 0 ) ∈ ℝ )
4 rernegcl ⊢ ( ( 0 + 0 ) ∈ ℝ → ( 0 −ℝ ( 0 + 0 ) ) ∈ ℝ )
5 3 4 syl ⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ ( 0 + 0 ) ) ∈ ℝ )
6 5 recnd ⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ ( 0 + 0 ) ) ∈ ℂ )
7 2 2 6 addassd ⊢ ( 𝐴 ∈ ℝ → ( ( 0 + 0 ) + ( 0 −ℝ ( 0 + 0 ) ) ) = ( 0 + ( 0 + ( 0 −ℝ ( 0 + 0 ) ) ) ) )
8 renegid ⊢ ( ( 0 + 0 ) ∈ ℝ → ( ( 0 + 0 ) + ( 0 −ℝ ( 0 + 0 ) ) ) = 0 )
9 3 8 syl ⊢ ( 𝐴 ∈ ℝ → ( ( 0 + 0 ) + ( 0 −ℝ ( 0 + 0 ) ) ) = 0 )
10 7 9 eqtr3d ⊢ ( 𝐴 ∈ ℝ → ( 0 + ( 0 + ( 0 −ℝ ( 0 + 0 ) ) ) ) = 0 )
11 1 5 readdcld ⊢ ( 𝐴 ∈ ℝ → ( 0 + ( 0 −ℝ ( 0 + 0 ) ) ) ∈ ℝ )
12 renegadd ⊢ ( ( 0 ∈ ℝ ∧ ( 0 + ( 0 −ℝ ( 0 + 0 ) ) ) ∈ ℝ ) → ( ( 0 −ℝ 0 ) = ( 0 + ( 0 −ℝ ( 0 + 0 ) ) ) ↔ ( 0 + ( 0 + ( 0 −ℝ ( 0 + 0 ) ) ) ) = 0 ) )
13 1 11 12 syl2anc ⊢ ( 𝐴 ∈ ℝ → ( ( 0 −ℝ 0 ) = ( 0 + ( 0 −ℝ ( 0 + 0 ) ) ) ↔ ( 0 + ( 0 + ( 0 −ℝ ( 0 + 0 ) ) ) ) = 0 ) )
14 10 13 mpbird ⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ 0 ) = ( 0 + ( 0 −ℝ ( 0 + 0 ) ) ) )
15 14 eqcomd ⊢ ( 𝐴 ∈ ℝ → ( 0 + ( 0 −ℝ ( 0 + 0 ) ) ) = ( 0 −ℝ 0 ) )