Metamath Proof Explorer


Theorem mulassnq

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 A𝑸B𝑸C=A𝑸B𝑸C

Proof

Step Hyp Ref Expression
1 mulasspi 1stA𝑵1stB𝑵1stC=1stA𝑵1stB𝑵1stC
2 mulasspi 2ndA𝑵2ndB𝑵2ndC=2ndA𝑵2ndB𝑵2ndC
3 1 2 opeq12i 1stA𝑵1stB𝑵1stC2ndA𝑵2ndB𝑵2ndC=1stA𝑵1stB𝑵1stC2ndA𝑵2ndB𝑵2ndC
4 elpqn A𝑸A𝑵×𝑵
5 4 3ad2ant1 A𝑸B𝑸C𝑸A𝑵×𝑵
6 elpqn B𝑸B𝑵×𝑵
7 6 3ad2ant2 A𝑸B𝑸C𝑸B𝑵×𝑵
8 mulpipq2 A𝑵×𝑵B𝑵×𝑵A𝑝𝑸B=1stA𝑵1stB2ndA𝑵2ndB
9 5 7 8 syl2anc A𝑸B𝑸C𝑸A𝑝𝑸B=1stA𝑵1stB2ndA𝑵2ndB
10 relxp Rel𝑵×𝑵
11 elpqn C𝑸C𝑵×𝑵
12 11 3ad2ant3 A𝑸B𝑸C𝑸C𝑵×𝑵
13 1st2nd Rel𝑵×𝑵C𝑵×𝑵C=1stC2ndC
14 10 12 13 sylancr A𝑸B𝑸C𝑸C=1stC2ndC
15 9 14 oveq12d A𝑸B𝑸C𝑸A𝑝𝑸B𝑝𝑸C=1stA𝑵1stB2ndA𝑵2ndB𝑝𝑸1stC2ndC
16 xp1st A𝑵×𝑵1stA𝑵
17 5 16 syl A𝑸B𝑸C𝑸1stA𝑵
18 xp1st B𝑵×𝑵1stB𝑵
19 7 18 syl A𝑸B𝑸C𝑸1stB𝑵
20 mulclpi 1stA𝑵1stB𝑵1stA𝑵1stB𝑵
21 17 19 20 syl2anc A𝑸B𝑸C𝑸1stA𝑵1stB𝑵
22 xp2nd A𝑵×𝑵2ndA𝑵
23 5 22 syl A𝑸B𝑸C𝑸2ndA𝑵
24 xp2nd B𝑵×𝑵2ndB𝑵
25 7 24 syl A𝑸B𝑸C𝑸2ndB𝑵
26 mulclpi 2ndA𝑵2ndB𝑵2ndA𝑵2ndB𝑵
27 23 25 26 syl2anc A𝑸B𝑸C𝑸2ndA𝑵2ndB𝑵
28 xp1st C𝑵×𝑵1stC𝑵
29 12 28 syl A𝑸B𝑸C𝑸1stC𝑵
30 xp2nd C𝑵×𝑵2ndC𝑵
31 12 30 syl A𝑸B𝑸C𝑸2ndC𝑵
32 mulpipq 1stA𝑵1stB𝑵2ndA𝑵2ndB𝑵1stC𝑵2ndC𝑵1stA𝑵1stB2ndA𝑵2ndB𝑝𝑸1stC2ndC=1stA𝑵1stB𝑵1stC2ndA𝑵2ndB𝑵2ndC
33 21 27 29 31 32 syl22anc A𝑸B𝑸C𝑸1stA𝑵1stB2ndA𝑵2ndB𝑝𝑸1stC2ndC=1stA𝑵1stB𝑵1stC2ndA𝑵2ndB𝑵2ndC
34 15 33 eqtrd A𝑸B𝑸C𝑸A𝑝𝑸B𝑝𝑸C=1stA𝑵1stB𝑵1stC2ndA𝑵2ndB𝑵2ndC
35 1st2nd Rel𝑵×𝑵A𝑵×𝑵A=1stA2ndA
36 10 5 35 sylancr A𝑸B𝑸C𝑸A=1stA2ndA
37 mulpipq2 B𝑵×𝑵C𝑵×𝑵B𝑝𝑸C=1stB𝑵1stC2ndB𝑵2ndC
38 7 12 37 syl2anc A𝑸B𝑸C𝑸B𝑝𝑸C=1stB𝑵1stC2ndB𝑵2ndC
39 36 38 oveq12d A𝑸B𝑸C𝑸A𝑝𝑸B𝑝𝑸C=1stA2ndA𝑝𝑸1stB𝑵1stC2ndB𝑵2ndC
40 mulclpi 1stB𝑵1stC𝑵1stB𝑵1stC𝑵
41 19 29 40 syl2anc A𝑸B𝑸C𝑸1stB𝑵1stC𝑵
42 mulclpi 2ndB𝑵2ndC𝑵2ndB𝑵2ndC𝑵
43 25 31 42 syl2anc A𝑸B𝑸C𝑸2ndB𝑵2ndC𝑵
44 mulpipq 1stA𝑵2ndA𝑵1stB𝑵1stC𝑵2ndB𝑵2ndC𝑵1stA2ndA𝑝𝑸1stB𝑵1stC2ndB𝑵2ndC=1stA𝑵1stB𝑵1stC2ndA𝑵2ndB𝑵2ndC
45 17 23 41 43 44 syl22anc A𝑸B𝑸C𝑸1stA2ndA𝑝𝑸1stB𝑵1stC2ndB𝑵2ndC=1stA𝑵1stB𝑵1stC2ndA𝑵2ndB𝑵2ndC
46 39 45 eqtrd A𝑸B𝑸C𝑸A𝑝𝑸B𝑝𝑸C=1stA𝑵1stB𝑵1stC2ndA𝑵2ndB𝑵2ndC
47 3 34 46 3eqtr4a A𝑸B𝑸C𝑸A𝑝𝑸B𝑝𝑸C=A𝑝𝑸B𝑝𝑸C
48 47 fveq2d A𝑸B𝑸C𝑸/𝑸A𝑝𝑸B𝑝𝑸C=/𝑸A𝑝𝑸B𝑝𝑸C
49 mulerpq /𝑸A𝑝𝑸B𝑸/𝑸C=/𝑸A𝑝𝑸B𝑝𝑸C
50 mulerpq /𝑸A𝑸/𝑸B𝑝𝑸C=/𝑸A𝑝𝑸B𝑝𝑸C
51 48 49 50 3eqtr4g A𝑸B𝑸C𝑸/𝑸A𝑝𝑸B𝑸/𝑸C=/𝑸A𝑸/𝑸B𝑝𝑸C
52 mulpqnq A𝑸B𝑸A𝑸B=/𝑸A𝑝𝑸B
53 52 3adant3 A𝑸B𝑸C𝑸A𝑸B=/𝑸A𝑝𝑸B
54 nqerid C𝑸/𝑸C=C
55 54 eqcomd C𝑸C=/𝑸C
56 55 3ad2ant3 A𝑸B𝑸C𝑸C=/𝑸C
57 53 56 oveq12d A𝑸B𝑸C𝑸A𝑸B𝑸C=/𝑸A𝑝𝑸B𝑸/𝑸C
58 nqerid A𝑸/𝑸A=A
59 58 eqcomd A𝑸A=/𝑸A
60 59 3ad2ant1 A𝑸B𝑸C𝑸A=/𝑸A
61 mulpqnq B𝑸C𝑸B𝑸C=/𝑸B𝑝𝑸C
62 61 3adant1 A𝑸B𝑸C𝑸B𝑸C=/𝑸B𝑝𝑸C
63 60 62 oveq12d A𝑸B𝑸C𝑸A𝑸B𝑸C=/𝑸A𝑸/𝑸B𝑝𝑸C
64 51 57 63 3eqtr4d A𝑸B𝑸C𝑸A𝑸B𝑸C=A𝑸B𝑸C
65 mulnqf 𝑸:𝑸×𝑸𝑸
66 65 fdmi dom𝑸=𝑸×𝑸
67 0nnq ¬𝑸
68 66 67 ndmovass ¬A𝑸B𝑸C𝑸A𝑸B𝑸C=A𝑸B𝑸C
69 64 68 pm2.61i A𝑸B𝑸C=A𝑸B𝑸C