Metamath Proof Explorer


Theorem addassnq

Description: Addition of positive fractions is associative. (Contributed by NM, 2-Sep-1995) (Revised by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion addassnq A+𝑸B+𝑸C=A+𝑸B+𝑸C

Proof

Step Hyp Ref Expression
1 addasspi 1stA𝑵2ndB𝑵2ndC+𝑵1stB𝑵2ndA𝑵2ndC+𝑵1stC𝑵2ndA𝑵2ndB=1stA𝑵2ndB𝑵2ndC+𝑵1stB𝑵2ndA𝑵2ndC+𝑵1stC𝑵2ndA𝑵2ndB
2 ovex 1stA𝑵2ndBV
3 ovex 1stB𝑵2ndAV
4 fvex 2ndCV
5 mulcompi x𝑵y=y𝑵x
6 distrpi x𝑵y+𝑵z=x𝑵y+𝑵x𝑵z
7 2 3 4 5 6 caovdir 1stA𝑵2ndB+𝑵1stB𝑵2ndA𝑵2ndC=1stA𝑵2ndB𝑵2ndC+𝑵1stB𝑵2ndA𝑵2ndC
8 mulasspi 1stA𝑵2ndB𝑵2ndC=1stA𝑵2ndB𝑵2ndC
9 8 oveq1i 1stA𝑵2ndB𝑵2ndC+𝑵1stB𝑵2ndA𝑵2ndC=1stA𝑵2ndB𝑵2ndC+𝑵1stB𝑵2ndA𝑵2ndC
10 7 9 eqtri 1stA𝑵2ndB+𝑵1stB𝑵2ndA𝑵2ndC=1stA𝑵2ndB𝑵2ndC+𝑵1stB𝑵2ndA𝑵2ndC
11 10 oveq1i 1stA𝑵2ndB+𝑵1stB𝑵2ndA𝑵2ndC+𝑵1stC𝑵2ndA𝑵2ndB=1stA𝑵2ndB𝑵2ndC+𝑵1stB𝑵2ndA𝑵2ndC+𝑵1stC𝑵2ndA𝑵2ndB
12 ovex 1stB𝑵2ndCV
13 ovex 1stC𝑵2ndBV
14 fvex 2ndAV
15 12 13 14 5 6 caovdir 1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵2ndA=1stB𝑵2ndC𝑵2ndA+𝑵1stC𝑵2ndB𝑵2ndA
16 fvex 1stBV
17 mulasspi x𝑵y𝑵z=x𝑵y𝑵z
18 16 4 14 5 17 caov32 1stB𝑵2ndC𝑵2ndA=1stB𝑵2ndA𝑵2ndC
19 mulasspi 1stC𝑵2ndB𝑵2ndA=1stC𝑵2ndB𝑵2ndA
20 mulcompi 2ndB𝑵2ndA=2ndA𝑵2ndB
21 20 oveq2i 1stC𝑵2ndB𝑵2ndA=1stC𝑵2ndA𝑵2ndB
22 19 21 eqtri 1stC𝑵2ndB𝑵2ndA=1stC𝑵2ndA𝑵2ndB
23 18 22 oveq12i 1stB𝑵2ndC𝑵2ndA+𝑵1stC𝑵2ndB𝑵2ndA=1stB𝑵2ndA𝑵2ndC+𝑵1stC𝑵2ndA𝑵2ndB
24 15 23 eqtri 1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵2ndA=1stB𝑵2ndA𝑵2ndC+𝑵1stC𝑵2ndA𝑵2ndB
25 24 oveq2i 1stA𝑵2ndB𝑵2ndC+𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵2ndA=1stA𝑵2ndB𝑵2ndC+𝑵1stB𝑵2ndA𝑵2ndC+𝑵1stC𝑵2ndA𝑵2ndB
26 1 11 25 3eqtr4i 1stA𝑵2ndB+𝑵1stB𝑵2ndA𝑵2ndC+𝑵1stC𝑵2ndA𝑵2ndB=1stA𝑵2ndB𝑵2ndC+𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵2ndA
27 mulasspi 2ndA𝑵2ndB𝑵2ndC=2ndA𝑵2ndB𝑵2ndC
28 26 27 opeq12i 1stA𝑵2ndB+𝑵1stB𝑵2ndA𝑵2ndC+𝑵1stC𝑵2ndA𝑵2ndB2ndA𝑵2ndB𝑵2ndC=1stA𝑵2ndB𝑵2ndC+𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵2ndA2ndA𝑵2ndB𝑵2ndC
29 elpqn A𝑸A𝑵×𝑵
30 29 3ad2ant1 A𝑸B𝑸C𝑸A𝑵×𝑵
31 elpqn B𝑸B𝑵×𝑵
32 31 3ad2ant2 A𝑸B𝑸C𝑸B𝑵×𝑵
33 addpipq2 A𝑵×𝑵B𝑵×𝑵A+𝑝𝑸B=1stA𝑵2ndB+𝑵1stB𝑵2ndA2ndA𝑵2ndB
34 30 32 33 syl2anc A𝑸B𝑸C𝑸A+𝑝𝑸B=1stA𝑵2ndB+𝑵1stB𝑵2ndA2ndA𝑵2ndB
35 relxp Rel𝑵×𝑵
36 elpqn C𝑸C𝑵×𝑵
37 36 3ad2ant3 A𝑸B𝑸C𝑸C𝑵×𝑵
38 1st2nd Rel𝑵×𝑵C𝑵×𝑵C=1stC2ndC
39 35 37 38 sylancr A𝑸B𝑸C𝑸C=1stC2ndC
40 34 39 oveq12d A𝑸B𝑸C𝑸A+𝑝𝑸B+𝑝𝑸C=1stA𝑵2ndB+𝑵1stB𝑵2ndA2ndA𝑵2ndB+𝑝𝑸1stC2ndC
41 xp1st A𝑵×𝑵1stA𝑵
42 30 41 syl A𝑸B𝑸C𝑸1stA𝑵
43 xp2nd B𝑵×𝑵2ndB𝑵
44 32 43 syl A𝑸B𝑸C𝑸2ndB𝑵
45 mulclpi 1stA𝑵2ndB𝑵1stA𝑵2ndB𝑵
46 42 44 45 syl2anc A𝑸B𝑸C𝑸1stA𝑵2ndB𝑵
47 xp1st B𝑵×𝑵1stB𝑵
48 32 47 syl A𝑸B𝑸C𝑸1stB𝑵
49 xp2nd A𝑵×𝑵2ndA𝑵
50 30 49 syl A𝑸B𝑸C𝑸2ndA𝑵
51 mulclpi 1stB𝑵2ndA𝑵1stB𝑵2ndA𝑵
52 48 50 51 syl2anc A𝑸B𝑸C𝑸1stB𝑵2ndA𝑵
53 addclpi 1stA𝑵2ndB𝑵1stB𝑵2ndA𝑵1stA𝑵2ndB+𝑵1stB𝑵2ndA𝑵
54 46 52 53 syl2anc A𝑸B𝑸C𝑸1stA𝑵2ndB+𝑵1stB𝑵2ndA𝑵
55 mulclpi 2ndA𝑵2ndB𝑵2ndA𝑵2ndB𝑵
56 50 44 55 syl2anc A𝑸B𝑸C𝑸2ndA𝑵2ndB𝑵
57 xp1st C𝑵×𝑵1stC𝑵
58 37 57 syl A𝑸B𝑸C𝑸1stC𝑵
59 xp2nd C𝑵×𝑵2ndC𝑵
60 37 59 syl A𝑸B𝑸C𝑸2ndC𝑵
61 addpipq 1stA𝑵2ndB+𝑵1stB𝑵2ndA𝑵2ndA𝑵2ndB𝑵1stC𝑵2ndC𝑵1stA𝑵2ndB+𝑵1stB𝑵2ndA2ndA𝑵2ndB+𝑝𝑸1stC2ndC=1stA𝑵2ndB+𝑵1stB𝑵2ndA𝑵2ndC+𝑵1stC𝑵2ndA𝑵2ndB2ndA𝑵2ndB𝑵2ndC
62 54 56 58 60 61 syl22anc A𝑸B𝑸C𝑸1stA𝑵2ndB+𝑵1stB𝑵2ndA2ndA𝑵2ndB+𝑝𝑸1stC2ndC=1stA𝑵2ndB+𝑵1stB𝑵2ndA𝑵2ndC+𝑵1stC𝑵2ndA𝑵2ndB2ndA𝑵2ndB𝑵2ndC
63 40 62 eqtrd A𝑸B𝑸C𝑸A+𝑝𝑸B+𝑝𝑸C=1stA𝑵2ndB+𝑵1stB𝑵2ndA𝑵2ndC+𝑵1stC𝑵2ndA𝑵2ndB2ndA𝑵2ndB𝑵2ndC
64 1st2nd Rel𝑵×𝑵A𝑵×𝑵A=1stA2ndA
65 35 30 64 sylancr A𝑸B𝑸C𝑸A=1stA2ndA
66 addpipq2 B𝑵×𝑵C𝑵×𝑵B+𝑝𝑸C=1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndB𝑵2ndC
67 32 37 66 syl2anc A𝑸B𝑸C𝑸B+𝑝𝑸C=1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndB𝑵2ndC
68 65 67 oveq12d A𝑸B𝑸C𝑸A+𝑝𝑸B+𝑝𝑸C=1stA2ndA+𝑝𝑸1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndB𝑵2ndC
69 mulclpi 1stB𝑵2ndC𝑵1stB𝑵2ndC𝑵
70 48 60 69 syl2anc A𝑸B𝑸C𝑸1stB𝑵2ndC𝑵
71 mulclpi 1stC𝑵2ndB𝑵1stC𝑵2ndB𝑵
72 58 44 71 syl2anc A𝑸B𝑸C𝑸1stC𝑵2ndB𝑵
73 addclpi 1stB𝑵2ndC𝑵1stC𝑵2ndB𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵
74 70 72 73 syl2anc A𝑸B𝑸C𝑸1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵
75 mulclpi 2ndB𝑵2ndC𝑵2ndB𝑵2ndC𝑵
76 44 60 75 syl2anc A𝑸B𝑸C𝑸2ndB𝑵2ndC𝑵
77 addpipq 1stA𝑵2ndA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵2ndB𝑵2ndC𝑵1stA2ndA+𝑝𝑸1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndB𝑵2ndC=1stA𝑵2ndB𝑵2ndC+𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵2ndA2ndA𝑵2ndB𝑵2ndC
78 42 50 74 76 77 syl22anc A𝑸B𝑸C𝑸1stA2ndA+𝑝𝑸1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndB𝑵2ndC=1stA𝑵2ndB𝑵2ndC+𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵2ndA2ndA𝑵2ndB𝑵2ndC
79 68 78 eqtrd A𝑸B𝑸C𝑸A+𝑝𝑸B+𝑝𝑸C=1stA𝑵2ndB𝑵2ndC+𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵2ndA2ndA𝑵2ndB𝑵2ndC
80 28 63 79 3eqtr4a A𝑸B𝑸C𝑸A+𝑝𝑸B+𝑝𝑸C=A+𝑝𝑸B+𝑝𝑸C
81 80 fveq2d A𝑸B𝑸C𝑸/𝑸A+𝑝𝑸B+𝑝𝑸C=/𝑸A+𝑝𝑸B+𝑝𝑸C
82 adderpq /𝑸A+𝑝𝑸B+𝑸/𝑸C=/𝑸A+𝑝𝑸B+𝑝𝑸C
83 adderpq /𝑸A+𝑸/𝑸B+𝑝𝑸C=/𝑸A+𝑝𝑸B+𝑝𝑸C
84 81 82 83 3eqtr4g A𝑸B𝑸C𝑸/𝑸A+𝑝𝑸B+𝑸/𝑸C=/𝑸A+𝑸/𝑸B+𝑝𝑸C
85 addpqnq A𝑸B𝑸A+𝑸B=/𝑸A+𝑝𝑸B
86 85 3adant3 A𝑸B𝑸C𝑸A+𝑸B=/𝑸A+𝑝𝑸B
87 nqerid C𝑸/𝑸C=C
88 87 eqcomd C𝑸C=/𝑸C
89 88 3ad2ant3 A𝑸B𝑸C𝑸C=/𝑸C
90 86 89 oveq12d A𝑸B𝑸C𝑸A+𝑸B+𝑸C=/𝑸A+𝑝𝑸B+𝑸/𝑸C
91 nqerid A𝑸/𝑸A=A
92 91 eqcomd A𝑸A=/𝑸A
93 92 3ad2ant1 A𝑸B𝑸C𝑸A=/𝑸A
94 addpqnq B𝑸C𝑸B+𝑸C=/𝑸B+𝑝𝑸C
95 94 3adant1 A𝑸B𝑸C𝑸B+𝑸C=/𝑸B+𝑝𝑸C
96 93 95 oveq12d A𝑸B𝑸C𝑸A+𝑸B+𝑸C=/𝑸A+𝑸/𝑸B+𝑝𝑸C
97 84 90 96 3eqtr4d A𝑸B𝑸C𝑸A+𝑸B+𝑸C=A+𝑸B+𝑸C
98 addnqf +𝑸:𝑸×𝑸𝑸
99 98 fdmi dom+𝑸=𝑸×𝑸
100 0nnq ¬𝑸
101 99 100 ndmovass ¬A𝑸B𝑸C𝑸A+𝑸B+𝑸C=A+𝑸B+𝑸C
102 97 101 pm2.61i A+𝑸B+𝑸C=A+𝑸B+𝑸C