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