Theorem readdid1

Description: Real number version of addid1 , without ax-mulcom . (Contributed by SN, 23-Jan-2024)

	Ref	Expression
Assertion	readdid1	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 0 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		resubid	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 −ℝ 𝐴 ) = 0 )
2		id	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
3		elre0re	⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
4	2 2 3	resubaddd	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 −ℝ 𝐴 ) = 0 ↔ ( 𝐴 + 0 ) = 𝐴 ) )
5	1 4	mpbid	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 0 ) = 𝐴 )