Description: Multiplication identity element for positive fractions. (Contributed by NM, 3-Mar-1996) (Revised by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | mulidnq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1nq | |
|
2 | mulpqnq | |
|
3 | 1 2 | mpan2 | |
4 | relxp | |
|
5 | elpqn | |
|
6 | 1st2nd | |
|
7 | 4 5 6 | sylancr | |
8 | df-1nq | |
|
9 | 8 | a1i | |
10 | 7 9 | oveq12d | |
11 | xp1st | |
|
12 | 5 11 | syl | |
13 | xp2nd | |
|
14 | 5 13 | syl | |
15 | 1pi | |
|
16 | 15 | a1i | |
17 | mulpipq | |
|
18 | 12 14 16 16 17 | syl22anc | |
19 | mulidpi | |
|
20 | 11 19 | syl | |
21 | mulidpi | |
|
22 | 13 21 | syl | |
23 | 20 22 | opeq12d | |
24 | 5 23 | syl | |
25 | 10 18 24 | 3eqtrd | |
26 | 25 7 | eqtr4d | |
27 | 26 | fveq2d | |
28 | nqerid | |
|
29 | 3 27 28 | 3eqtrd | |