This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )