Description: Closure law for positive fraction reciprocal. (Contributed by NM, 6-Mar-1996) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | recclnq | |- ( A e. Q. -> ( *Q ` A ) e. Q. ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recidnq | |- ( A e. Q. -> ( A .Q ( *Q ` A ) ) = 1Q ) |
|
2 | 1nq | |- 1Q e. Q. |
|
3 | 1 2 | eqeltrdi | |- ( A e. Q. -> ( A .Q ( *Q ` A ) ) e. Q. ) |
4 | mulnqf | |- .Q : ( Q. X. Q. ) --> Q. |
|
5 | 4 | fdmi | |- dom .Q = ( Q. X. Q. ) |
6 | 0nnq | |- -. (/) e. Q. |
|
7 | 5 6 | ndmovrcl | |- ( ( A .Q ( *Q ` A ) ) e. Q. -> ( A e. Q. /\ ( *Q ` A ) e. Q. ) ) |
8 | 3 7 | syl | |- ( A e. Q. -> ( A e. Q. /\ ( *Q ` A ) e. Q. ) ) |
9 | 8 | simprd | |- ( A e. Q. -> ( *Q ` A ) e. Q. ) |