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 ⊢ 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C = 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C
2 mulasspi ⊢ 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C = 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C
3 1 2 opeq12i ⊢ 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C = 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C
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 = 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B
9 5 7 8 syl2anc ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → A ⋅ 𝑝𝑸 B = 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B
10 relxp ⊢ Rel ⁡ 𝑵 × 𝑵
11 elpqn ⊢ C ∈ 𝑸 → C ∈ 𝑵 × 𝑵
12 11 3ad2ant3 ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → C ∈ 𝑵 × 𝑵
13 1st2nd ⊢ Rel ⁡ 𝑵 × 𝑵 ∧ C ∈ 𝑵 × 𝑵 → C = 1 st ⁡ C 2 nd ⁡ C
14 10 12 13 sylancr ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → C = 1 st ⁡ C 2 nd ⁡ C
15 9 14 oveq12d ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → A ⋅ 𝑝𝑸 B ⋅ 𝑝𝑸 C = 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B ⋅ 𝑝𝑸 1 st ⁡ C 2 nd ⁡ C
16 xp1st ⊢ A ∈ 𝑵 × 𝑵 → 1 st ⁡ A ∈ 𝑵
17 5 16 syl ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 1 st ⁡ A ∈ 𝑵
18 xp1st ⊢ B ∈ 𝑵 × 𝑵 → 1 st ⁡ B ∈ 𝑵
19 7 18 syl ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 1 st ⁡ B ∈ 𝑵
20 mulclpi ⊢ 1 st ⁡ A ∈ 𝑵 ∧ 1 st ⁡ B ∈ 𝑵 → 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B ∈ 𝑵
21 17 19 20 syl2anc ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B ∈ 𝑵
22 xp2nd ⊢ A ∈ 𝑵 × 𝑵 → 2 nd ⁡ A ∈ 𝑵
23 5 22 syl ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 2 nd ⁡ A ∈ 𝑵
24 xp2nd ⊢ B ∈ 𝑵 × 𝑵 → 2 nd ⁡ B ∈ 𝑵
25 7 24 syl ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 2 nd ⁡ B ∈ 𝑵
26 mulclpi ⊢ 2 nd ⁡ A ∈ 𝑵 ∧ 2 nd ⁡ B ∈ 𝑵 → 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B ∈ 𝑵
27 23 25 26 syl2anc ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B ∈ 𝑵
28 xp1st ⊢ C ∈ 𝑵 × 𝑵 → 1 st ⁡ C ∈ 𝑵
29 12 28 syl ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 1 st ⁡ C ∈ 𝑵
30 xp2nd ⊢ C ∈ 𝑵 × 𝑵 → 2 nd ⁡ C ∈ 𝑵
31 12 30 syl ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 2 nd ⁡ C ∈ 𝑵
32 mulpipq ⊢ 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B ∈ 𝑵 ∧ 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B ∈ 𝑵 ∧ 1 st ⁡ C ∈ 𝑵 ∧ 2 nd ⁡ C ∈ 𝑵 → 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B ⋅ 𝑝𝑸 1 st ⁡ C 2 nd ⁡ C = 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C
33 21 27 29 31 32 syl22anc ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B ⋅ 𝑝𝑸 1 st ⁡ C 2 nd ⁡ C = 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C
34 15 33 eqtrd ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → A ⋅ 𝑝𝑸 B ⋅ 𝑝𝑸 C = 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C
35 1st2nd ⊢ Rel ⁡ 𝑵 × 𝑵 ∧ A ∈ 𝑵 × 𝑵 → A = 1 st ⁡ A 2 nd ⁡ A
36 10 5 35 sylancr ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → A = 1 st ⁡ A 2 nd ⁡ A
37 mulpipq2 ⊢ B ∈ 𝑵 × 𝑵 ∧ C ∈ 𝑵 × 𝑵 → B ⋅ 𝑝𝑸 C = 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C
38 7 12 37 syl2anc ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → B ⋅ 𝑝𝑸 C = 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C
39 36 38 oveq12d ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → A ⋅ 𝑝𝑸 B ⋅ 𝑝𝑸 C = 1 st ⁡ A 2 nd ⁡ A ⋅ 𝑝𝑸 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C
40 mulclpi ⊢ 1 st ⁡ B ∈ 𝑵 ∧ 1 st ⁡ C ∈ 𝑵 → 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C ∈ 𝑵
41 19 29 40 syl2anc ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C ∈ 𝑵
42 mulclpi ⊢ 2 nd ⁡ B ∈ 𝑵 ∧ 2 nd ⁡ C ∈ 𝑵 → 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C ∈ 𝑵
43 25 31 42 syl2anc ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C ∈ 𝑵
44 mulpipq ⊢ 1 st ⁡ A ∈ 𝑵 ∧ 2 nd ⁡ A ∈ 𝑵 ∧ 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C ∈ 𝑵 ∧ 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C ∈ 𝑵 → 1 st ⁡ A 2 nd ⁡ A ⋅ 𝑝𝑸 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C = 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C
45 17 23 41 43 44 syl22anc ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 1 st ⁡ A 2 nd ⁡ A ⋅ 𝑝𝑸 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C = 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C
46 39 45 eqtrd ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → A ⋅ 𝑝𝑸 B ⋅ 𝑝𝑸 C = 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 1 st ⁡ C 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ C
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