Metamath Proof Explorer


Theorem resubeqsub

Description: Equivalence between real subtraction and subtraction. (Contributed by SN, 5-May-2024)

Ref Expression
Assertion resubeqsub
|- ( ( A e. RR /\ B e. RR ) -> ( A -R B ) = ( A - B ) )

Proof

Step Hyp Ref Expression
1 ax-resscn
 |-  RR C_ CC
2 resubeu
 |-  ( ( B e. RR /\ A e. RR ) -> E! x e. RR ( B + x ) = A )
3 reurex
 |-  ( E! x e. RR ( B + x ) = A -> E. x e. RR ( B + x ) = A )
4 2 3 syl
 |-  ( ( B e. RR /\ A e. RR ) -> E. x e. RR ( B + x ) = A )
5 recn
 |-  ( B e. RR -> B e. CC )
6 recn
 |-  ( A e. RR -> A e. CC )
7 sn-subeu
 |-  ( ( B e. CC /\ A e. CC ) -> E! x e. CC ( B + x ) = A )
8 5 6 7 syl2an
 |-  ( ( B e. RR /\ A e. RR ) -> E! x e. CC ( B + x ) = A )
9 riotass
 |-  ( ( RR C_ CC /\ E. x e. RR ( B + x ) = A /\ E! x e. CC ( B + x ) = A ) -> ( iota_ x e. RR ( B + x ) = A ) = ( iota_ x e. CC ( B + x ) = A ) )
10 1 4 8 9 mp3an2i
 |-  ( ( B e. RR /\ A e. RR ) -> ( iota_ x e. RR ( B + x ) = A ) = ( iota_ x e. CC ( B + x ) = A ) )
11 10 ancoms
 |-  ( ( A e. RR /\ B e. RR ) -> ( iota_ x e. RR ( B + x ) = A ) = ( iota_ x e. CC ( B + x ) = A ) )
12 resubval
 |-  ( ( A e. RR /\ B e. RR ) -> ( A -R B ) = ( iota_ x e. RR ( B + x ) = A ) )
13 subval
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) = ( iota_ x e. CC ( B + x ) = A ) )
14 6 5 13 syl2an
 |-  ( ( A e. RR /\ B e. RR ) -> ( A - B ) = ( iota_ x e. CC ( B + x ) = A ) )
15 11 12 14 3eqtr4d
 |-  ( ( A e. RR /\ B e. RR ) -> ( A -R B ) = ( A - B ) )