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