Step |
Hyp |
Ref |
Expression |
1 |
|
xdivcld.1 |
|- ( ph -> A e. RR* ) |
2 |
|
xdivcld.2 |
|- ( ph -> B e. RR ) |
3 |
|
xdivcld.3 |
|- ( ph -> B =/= 0 ) |
4 |
|
xdivval |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( A /e B ) = ( iota_ x e. RR* ( B *e x ) = A ) ) |
5 |
1 2 3 4
|
syl3anc |
|- ( ph -> ( A /e B ) = ( iota_ x e. RR* ( B *e x ) = A ) ) |
6 |
|
xreceu |
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> E! x e. RR* ( B *e x ) = A ) |
7 |
1 2 3 6
|
syl3anc |
|- ( ph -> E! x e. RR* ( B *e x ) = A ) |
8 |
|
riotacl |
|- ( E! x e. RR* ( B *e x ) = A -> ( iota_ x e. RR* ( B *e x ) = A ) e. RR* ) |
9 |
7 8
|
syl |
|- ( ph -> ( iota_ x e. RR* ( B *e x ) = A ) e. RR* ) |
10 |
5 9
|
eqeltrd |
|- ( ph -> ( A /e B ) e. RR* ) |