Metamath Proof Explorer


Theorem xaddid2d

Description: 0 is a left identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis xaddid2d.1 ( 𝜑𝐴 ∈ ℝ* )
Assertion xaddid2d ( 𝜑 → ( 0 +𝑒 𝐴 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 xaddid2d.1 ( 𝜑𝐴 ∈ ℝ* )
2 xaddid2 ( 𝐴 ∈ ℝ* → ( 0 +𝑒 𝐴 ) = 𝐴 )
3 1 2 syl ( 𝜑 → ( 0 +𝑒 𝐴 ) = 𝐴 )