Theorem resubid

Description: Subtraction of a real number from itself (compare subid ). (Contributed by SN, 23-Jan-2024)

	Ref	Expression
Assertion	resubid	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 −ℝ 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		re0m0e0	⊢ ( 0 −ℝ 0 ) = 0
2	1	oveq2i	⊢ ( 𝐴 · ( 0 −ℝ 0 ) ) = ( 𝐴 · 0 )
3		sn-00idlem1	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · ( 0 −ℝ 0 ) ) = ( 𝐴 −ℝ 𝐴 ) )
4		remul01	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) = 0 )
5	2 3 4	3eqtr3a	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 −ℝ 𝐴 ) = 0 )