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 )