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

Metamath Proof Explorer

Theorem resubeu

Description: Existential uniqueness of real differences. (Contributed by Steven Nguyen, 7-Jan-2023)

Ref Expression
Assertion resubeu 
|- ( ( A e. RR /\ B e. RR ) -> E! x e. RR ( A + x ) = B )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
2 rernegcl 
 |-  ( A e. RR -> ( 0 -R A ) e. RR )
3 2 adantr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 -R A ) e. RR )
4 elre0re 
 |-  ( A e. RR -> 0 e. RR )
5 4 4 readdcld 
 |-  ( A e. RR -> ( 0 + 0 ) e. RR )
6 rernegcl 
 |-  ( ( 0 + 0 ) e. RR -> ( 0 -R ( 0 + 0 ) ) e. RR )
7 5 6 syl 
 |-  ( A e. RR -> ( 0 -R ( 0 + 0 ) ) e. RR )
8 7 adantr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 -R ( 0 + 0 ) ) e. RR )
9 simpr 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
10 8 9 readdcld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 -R ( 0 + 0 ) ) + B ) e. RR )
11 3 10 readdcld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 -R A ) + ( ( 0 -R ( 0 + 0 ) ) + B ) ) e. RR )
12 resubeulem2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + ( ( 0 -R A ) + ( ( 0 -R ( 0 + 0 ) ) + B ) ) ) = B )
13 oveq2 
 |-  ( x = ( ( 0 -R A ) + ( ( 0 -R ( 0 + 0 ) ) + B ) ) -> ( A + x ) = ( A + ( ( 0 -R A ) + ( ( 0 -R ( 0 + 0 ) ) + B ) ) ) )
14 13 eqeq1d 
 |-  ( x = ( ( 0 -R A ) + ( ( 0 -R ( 0 + 0 ) ) + B ) ) -> ( ( A + x ) = B <-> ( A + ( ( 0 -R A ) + ( ( 0 -R ( 0 + 0 ) ) + B ) ) ) = B ) )
15 14 rspcev 
 |-  ( ( ( ( 0 -R A ) + ( ( 0 -R ( 0 + 0 ) ) + B ) ) e. RR /\ ( A + ( ( 0 -R A ) + ( ( 0 -R ( 0 + 0 ) ) + B ) ) ) = B ) -> E. x e. RR ( A + x ) = B )
16 11 12 15 syl2anc 
 |-  ( ( A e. RR /\ B e. RR ) -> E. x e. RR ( A + x ) = B )
17 1 16 renegeulem 
 |-  ( ( A e. RR /\ B e. RR ) -> E! x e. RR ( A + x ) = B )