Description: Multiplication of positive fractions is associative. (Contributed by NM, 1-Sep-1995) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | mulassnq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mulasspi | |
|
2 | mulasspi | |
|
3 | 1 2 | opeq12i | |
4 | elpqn | |
|
5 | 4 | 3ad2ant1 | |
6 | elpqn | |
|
7 | 6 | 3ad2ant2 | |
8 | mulpipq2 | |
|
9 | 5 7 8 | syl2anc | |
10 | relxp | |
|
11 | elpqn | |
|
12 | 11 | 3ad2ant3 | |
13 | 1st2nd | |
|
14 | 10 12 13 | sylancr | |
15 | 9 14 | oveq12d | |
16 | xp1st | |
|
17 | 5 16 | syl | |
18 | xp1st | |
|
19 | 7 18 | syl | |
20 | mulclpi | |
|
21 | 17 19 20 | syl2anc | |
22 | xp2nd | |
|
23 | 5 22 | syl | |
24 | xp2nd | |
|
25 | 7 24 | syl | |
26 | mulclpi | |
|
27 | 23 25 26 | syl2anc | |
28 | xp1st | |
|
29 | 12 28 | syl | |
30 | xp2nd | |
|
31 | 12 30 | syl | |
32 | mulpipq | |
|
33 | 21 27 29 31 32 | syl22anc | |
34 | 15 33 | eqtrd | |
35 | 1st2nd | |
|
36 | 10 5 35 | sylancr | |
37 | mulpipq2 | |
|
38 | 7 12 37 | syl2anc | |
39 | 36 38 | oveq12d | |
40 | mulclpi | |
|
41 | 19 29 40 | syl2anc | |
42 | mulclpi | |
|
43 | 25 31 42 | syl2anc | |
44 | mulpipq | |
|
45 | 17 23 41 43 44 | syl22anc | |
46 | 39 45 | eqtrd | |
47 | 3 34 46 | 3eqtr4a | |
48 | 47 | fveq2d | |
49 | mulerpq | |
|
50 | mulerpq | |
|
51 | 48 49 50 | 3eqtr4g | |
52 | mulpqnq | |
|
53 | 52 | 3adant3 | |
54 | nqerid | |
|
55 | 54 | eqcomd | |
56 | 55 | 3ad2ant3 | |
57 | 53 56 | oveq12d | |
58 | nqerid | |
|
59 | 58 | eqcomd | |
60 | 59 | 3ad2ant1 | |
61 | mulpqnq | |
|
62 | 61 | 3adant1 | |
63 | 60 62 | oveq12d | |
64 | 51 57 63 | 3eqtr4d | |
65 | mulnqf | |
|
66 | 65 | fdmi | |
67 | 0nnq | |
|
68 | 66 67 | ndmovass | |
69 | 64 68 | pm2.61i | |