Description: Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | mulclnq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mulpqnq | |
|
2 | elpqn | |
|
3 | elpqn | |
|
4 | mulpqf | |
|
5 | 4 | fovcl | |
6 | 2 3 5 | syl2an | |
7 | nqercl | |
|
8 | 6 7 | syl | |
9 | 1 8 | eqeltrd | |