Metamath Proof Explorer

Theorem resubid

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

Ref Expression
Assertion resubid 
|- ( A e. RR -> ( A -R A ) = 0 )

Proof

Step Hyp Ref Expression
1 re0m0e0 
 |-  ( 0 -R 0 ) = 0
2 1 oveq2i 
 |-  ( A x. ( 0 -R 0 ) ) = ( A x. 0 )
3 sn-00idlem1 
 |-  ( A e. RR -> ( A x. ( 0 -R 0 ) ) = ( A -R A ) )
4 remul01 
 |-  ( A e. RR -> ( A x. 0 ) = 0 )
5 2 3 4 3eqtr3a 
 |-  ( A e. RR -> ( A -R A ) = 0 )