Metamath Proof Explorer


Theorem distrnq

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

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

Proof

Step Hyp Ref Expression
1 mulcompi 1stA𝑵1stB=1stB𝑵1stA
2 1 oveq1i 1stA𝑵1stB𝑵2ndA𝑵2ndC=1stB𝑵1stA𝑵2ndA𝑵2ndC
3 fvex 1stBV
4 fvex 1stAV
5 fvex 2ndAV
6 mulcompi x𝑵y=y𝑵x
7 mulasspi x𝑵y𝑵z=x𝑵y𝑵z
8 fvex 2ndCV
9 3 4 5 6 7 8 caov411 1stB𝑵1stA𝑵2ndA𝑵2ndC=2ndA𝑵1stA𝑵1stB𝑵2ndC
10 2 9 eqtri 1stA𝑵1stB𝑵2ndA𝑵2ndC=2ndA𝑵1stA𝑵1stB𝑵2ndC
11 mulcompi 1stA𝑵1stC=1stC𝑵1stA
12 11 oveq1i 1stA𝑵1stC𝑵2ndA𝑵2ndB=1stC𝑵1stA𝑵2ndA𝑵2ndB
13 fvex 1stCV
14 fvex 2ndBV
15 13 4 5 6 7 14 caov411 1stC𝑵1stA𝑵2ndA𝑵2ndB=2ndA𝑵1stA𝑵1stC𝑵2ndB
16 12 15 eqtri 1stA𝑵1stC𝑵2ndA𝑵2ndB=2ndA𝑵1stA𝑵1stC𝑵2ndB
17 10 16 oveq12i 1stA𝑵1stB𝑵2ndA𝑵2ndC+𝑵1stA𝑵1stC𝑵2ndA𝑵2ndB=2ndA𝑵1stA𝑵1stB𝑵2ndC+𝑵2ndA𝑵1stA𝑵1stC𝑵2ndB
18 distrpi 2ndA𝑵1stA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB=2ndA𝑵1stA𝑵1stB𝑵2ndC+𝑵2ndA𝑵1stA𝑵1stC𝑵2ndB
19 mulasspi 2ndA𝑵1stA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB=2ndA𝑵1stA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB
20 17 18 19 3eqtr2i 1stA𝑵1stB𝑵2ndA𝑵2ndC+𝑵1stA𝑵1stC𝑵2ndA𝑵2ndB=2ndA𝑵1stA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB
21 mulasspi 2ndA𝑵2ndB𝑵2ndA𝑵2ndC=2ndA𝑵2ndB𝑵2ndA𝑵2ndC
22 14 5 8 6 7 caov12 2ndB𝑵2ndA𝑵2ndC=2ndA𝑵2ndB𝑵2ndC
23 22 oveq2i 2ndA𝑵2ndB𝑵2ndA𝑵2ndC=2ndA𝑵2ndA𝑵2ndB𝑵2ndC
24 21 23 eqtri 2ndA𝑵2ndB𝑵2ndA𝑵2ndC=2ndA𝑵2ndA𝑵2ndB𝑵2ndC
25 20 24 opeq12i 1stA𝑵1stB𝑵2ndA𝑵2ndC+𝑵1stA𝑵1stC𝑵2ndA𝑵2ndB2ndA𝑵2ndB𝑵2ndA𝑵2ndC=2ndA𝑵1stA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndA𝑵2ndA𝑵2ndB𝑵2ndC
26 elpqn A𝑸A𝑵×𝑵
27 26 3ad2ant1 A𝑸B𝑸C𝑸A𝑵×𝑵
28 xp2nd A𝑵×𝑵2ndA𝑵
29 27 28 syl A𝑸B𝑸C𝑸2ndA𝑵
30 xp1st A𝑵×𝑵1stA𝑵
31 27 30 syl A𝑸B𝑸C𝑸1stA𝑵
32 elpqn B𝑸B𝑵×𝑵
33 32 3ad2ant2 A𝑸B𝑸C𝑸B𝑵×𝑵
34 xp1st B𝑵×𝑵1stB𝑵
35 33 34 syl A𝑸B𝑸C𝑸1stB𝑵
36 elpqn C𝑸C𝑵×𝑵
37 36 3ad2ant3 A𝑸B𝑸C𝑸C𝑵×𝑵
38 xp2nd C𝑵×𝑵2ndC𝑵
39 37 38 syl A𝑸B𝑸C𝑸2ndC𝑵
40 mulclpi 1stB𝑵2ndC𝑵1stB𝑵2ndC𝑵
41 35 39 40 syl2anc A𝑸B𝑸C𝑸1stB𝑵2ndC𝑵
42 xp1st C𝑵×𝑵1stC𝑵
43 37 42 syl A𝑸B𝑸C𝑸1stC𝑵
44 xp2nd B𝑵×𝑵2ndB𝑵
45 33 44 syl A𝑸B𝑸C𝑸2ndB𝑵
46 mulclpi 1stC𝑵2ndB𝑵1stC𝑵2ndB𝑵
47 43 45 46 syl2anc A𝑸B𝑸C𝑸1stC𝑵2ndB𝑵
48 addclpi 1stB𝑵2ndC𝑵1stC𝑵2ndB𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵
49 41 47 48 syl2anc A𝑸B𝑸C𝑸1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵
50 mulclpi 1stA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵1stA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵
51 31 49 50 syl2anc A𝑸B𝑸C𝑸1stA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵
52 mulclpi 2ndB𝑵2ndC𝑵2ndB𝑵2ndC𝑵
53 45 39 52 syl2anc A𝑸B𝑸C𝑸2ndB𝑵2ndC𝑵
54 mulclpi 2ndA𝑵2ndB𝑵2ndC𝑵2ndA𝑵2ndB𝑵2ndC𝑵
55 29 53 54 syl2anc A𝑸B𝑸C𝑸2ndA𝑵2ndB𝑵2ndC𝑵
56 mulcanenq 2ndA𝑵1stA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵2ndA𝑵2ndB𝑵2ndC𝑵2ndA𝑵1stA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndA𝑵2ndA𝑵2ndB𝑵2ndC~𝑸1stA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndA𝑵2ndB𝑵2ndC
57 29 51 55 56 syl3anc A𝑸B𝑸C𝑸2ndA𝑵1stA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndA𝑵2ndA𝑵2ndB𝑵2ndC~𝑸1stA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndA𝑵2ndB𝑵2ndC
58 25 57 eqbrtrid A𝑸B𝑸C𝑸1stA𝑵1stB𝑵2ndA𝑵2ndC+𝑵1stA𝑵1stC𝑵2ndA𝑵2ndB2ndA𝑵2ndB𝑵2ndA𝑵2ndC~𝑸1stA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndA𝑵2ndB𝑵2ndC
59 mulpipq2 A𝑵×𝑵B𝑵×𝑵A𝑝𝑸B=1stA𝑵1stB2ndA𝑵2ndB
60 27 33 59 syl2anc A𝑸B𝑸C𝑸A𝑝𝑸B=1stA𝑵1stB2ndA𝑵2ndB
61 mulpipq2 A𝑵×𝑵C𝑵×𝑵A𝑝𝑸C=1stA𝑵1stC2ndA𝑵2ndC
62 27 37 61 syl2anc A𝑸B𝑸C𝑸A𝑝𝑸C=1stA𝑵1stC2ndA𝑵2ndC
63 60 62 oveq12d A𝑸B𝑸C𝑸A𝑝𝑸B+𝑝𝑸A𝑝𝑸C=1stA𝑵1stB2ndA𝑵2ndB+𝑝𝑸1stA𝑵1stC2ndA𝑵2ndC
64 mulclpi 1stA𝑵1stB𝑵1stA𝑵1stB𝑵
65 31 35 64 syl2anc A𝑸B𝑸C𝑸1stA𝑵1stB𝑵
66 mulclpi 2ndA𝑵2ndB𝑵2ndA𝑵2ndB𝑵
67 29 45 66 syl2anc A𝑸B𝑸C𝑸2ndA𝑵2ndB𝑵
68 mulclpi 1stA𝑵1stC𝑵1stA𝑵1stC𝑵
69 31 43 68 syl2anc A𝑸B𝑸C𝑸1stA𝑵1stC𝑵
70 mulclpi 2ndA𝑵2ndC𝑵2ndA𝑵2ndC𝑵
71 29 39 70 syl2anc A𝑸B𝑸C𝑸2ndA𝑵2ndC𝑵
72 addpipq 1stA𝑵1stB𝑵2ndA𝑵2ndB𝑵1stA𝑵1stC𝑵2ndA𝑵2ndC𝑵1stA𝑵1stB2ndA𝑵2ndB+𝑝𝑸1stA𝑵1stC2ndA𝑵2ndC=1stA𝑵1stB𝑵2ndA𝑵2ndC+𝑵1stA𝑵1stC𝑵2ndA𝑵2ndB2ndA𝑵2ndB𝑵2ndA𝑵2ndC
73 65 67 69 71 72 syl22anc A𝑸B𝑸C𝑸1stA𝑵1stB2ndA𝑵2ndB+𝑝𝑸1stA𝑵1stC2ndA𝑵2ndC=1stA𝑵1stB𝑵2ndA𝑵2ndC+𝑵1stA𝑵1stC𝑵2ndA𝑵2ndB2ndA𝑵2ndB𝑵2ndA𝑵2ndC
74 63 73 eqtrd A𝑸B𝑸C𝑸A𝑝𝑸B+𝑝𝑸A𝑝𝑸C=1stA𝑵1stB𝑵2ndA𝑵2ndC+𝑵1stA𝑵1stC𝑵2ndA𝑵2ndB2ndA𝑵2ndB𝑵2ndA𝑵2ndC
75 relxp Rel𝑵×𝑵
76 1st2nd Rel𝑵×𝑵A𝑵×𝑵A=1stA2ndA
77 75 27 76 sylancr A𝑸B𝑸C𝑸A=1stA2ndA
78 addpipq2 B𝑵×𝑵C𝑵×𝑵B+𝑝𝑸C=1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndB𝑵2ndC
79 33 37 78 syl2anc A𝑸B𝑸C𝑸B+𝑝𝑸C=1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndB𝑵2ndC
80 77 79 oveq12d A𝑸B𝑸C𝑸A𝑝𝑸B+𝑝𝑸C=1stA2ndA𝑝𝑸1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndB𝑵2ndC
81 mulpipq 1stA𝑵2ndA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB𝑵2ndB𝑵2ndC𝑵1stA2ndA𝑝𝑸1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndB𝑵2ndC=1stA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndA𝑵2ndB𝑵2ndC
82 31 29 49 53 81 syl22anc A𝑸B𝑸C𝑸1stA2ndA𝑝𝑸1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndB𝑵2ndC=1stA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndA𝑵2ndB𝑵2ndC
83 80 82 eqtrd A𝑸B𝑸C𝑸A𝑝𝑸B+𝑝𝑸C=1stA𝑵1stB𝑵2ndC+𝑵1stC𝑵2ndB2ndA𝑵2ndB𝑵2ndC
84 58 74 83 3brtr4d A𝑸B𝑸C𝑸A𝑝𝑸B+𝑝𝑸A𝑝𝑸C~𝑸A𝑝𝑸B+𝑝𝑸C
85 mulpqf 𝑝𝑸:𝑵×𝑵×𝑵×𝑵𝑵×𝑵
86 85 fovcl A𝑵×𝑵B𝑵×𝑵A𝑝𝑸B𝑵×𝑵
87 27 33 86 syl2anc A𝑸B𝑸C𝑸A𝑝𝑸B𝑵×𝑵
88 85 fovcl A𝑵×𝑵C𝑵×𝑵A𝑝𝑸C𝑵×𝑵
89 27 37 88 syl2anc A𝑸B𝑸C𝑸A𝑝𝑸C𝑵×𝑵
90 addpqf +𝑝𝑸:𝑵×𝑵×𝑵×𝑵𝑵×𝑵
91 90 fovcl A𝑝𝑸B𝑵×𝑵A𝑝𝑸C𝑵×𝑵A𝑝𝑸B+𝑝𝑸A𝑝𝑸C𝑵×𝑵
92 87 89 91 syl2anc A𝑸B𝑸C𝑸A𝑝𝑸B+𝑝𝑸A𝑝𝑸C𝑵×𝑵
93 90 fovcl B𝑵×𝑵C𝑵×𝑵B+𝑝𝑸C𝑵×𝑵
94 33 37 93 syl2anc A𝑸B𝑸C𝑸B+𝑝𝑸C𝑵×𝑵
95 85 fovcl A𝑵×𝑵B+𝑝𝑸C𝑵×𝑵A𝑝𝑸B+𝑝𝑸C𝑵×𝑵
96 27 94 95 syl2anc A𝑸B𝑸C𝑸A𝑝𝑸B+𝑝𝑸C𝑵×𝑵
97 nqereq A𝑝𝑸B+𝑝𝑸A𝑝𝑸C𝑵×𝑵A𝑝𝑸B+𝑝𝑸C𝑵×𝑵A𝑝𝑸B+𝑝𝑸A𝑝𝑸C~𝑸A𝑝𝑸B+𝑝𝑸C/𝑸A𝑝𝑸B+𝑝𝑸A𝑝𝑸C=/𝑸A𝑝𝑸B+𝑝𝑸C
98 92 96 97 syl2anc A𝑸B𝑸C𝑸A𝑝𝑸B+𝑝𝑸A𝑝𝑸C~𝑸A𝑝𝑸B+𝑝𝑸C/𝑸A𝑝𝑸B+𝑝𝑸A𝑝𝑸C=/𝑸A𝑝𝑸B+𝑝𝑸C
99 84 98 mpbid A𝑸B𝑸C𝑸/𝑸A𝑝𝑸B+𝑝𝑸A𝑝𝑸C=/𝑸A𝑝𝑸B+𝑝𝑸C
100 99 eqcomd A𝑸B𝑸C𝑸/𝑸A𝑝𝑸B+𝑝𝑸C=/𝑸A𝑝𝑸B+𝑝𝑸A𝑝𝑸C
101 mulerpq /𝑸A𝑸/𝑸B+𝑝𝑸C=/𝑸A𝑝𝑸B+𝑝𝑸C
102 adderpq /𝑸A𝑝𝑸B+𝑸/𝑸A𝑝𝑸C=/𝑸A𝑝𝑸B+𝑝𝑸A𝑝𝑸C
103 100 101 102 3eqtr4g A𝑸B𝑸C𝑸/𝑸A𝑸/𝑸B+𝑝𝑸C=/𝑸A𝑝𝑸B+𝑸/𝑸A𝑝𝑸C
104 nqerid A𝑸/𝑸A=A
105 104 eqcomd A𝑸A=/𝑸A
106 105 3ad2ant1 A𝑸B𝑸C𝑸A=/𝑸A
107 addpqnq B𝑸C𝑸B+𝑸C=/𝑸B+𝑝𝑸C
108 107 3adant1 A𝑸B𝑸C𝑸B+𝑸C=/𝑸B+𝑝𝑸C
109 106 108 oveq12d A𝑸B𝑸C𝑸A𝑸B+𝑸C=/𝑸A𝑸/𝑸B+𝑝𝑸C
110 mulpqnq A𝑸B𝑸A𝑸B=/𝑸A𝑝𝑸B
111 110 3adant3 A𝑸B𝑸C𝑸A𝑸B=/𝑸A𝑝𝑸B
112 mulpqnq A𝑸C𝑸A𝑸C=/𝑸A𝑝𝑸C
113 112 3adant2 A𝑸B𝑸C𝑸A𝑸C=/𝑸A𝑝𝑸C
114 111 113 oveq12d A𝑸B𝑸C𝑸A𝑸B+𝑸A𝑸C=/𝑸A𝑝𝑸B+𝑸/𝑸A𝑝𝑸C
115 103 109 114 3eqtr4d A𝑸B𝑸C𝑸A𝑸B+𝑸C=A𝑸B+𝑸A𝑸C
116 addnqf +𝑸:𝑸×𝑸𝑸
117 116 fdmi dom+𝑸=𝑸×𝑸
118 0nnq ¬𝑸
119 mulnqf 𝑸:𝑸×𝑸𝑸
120 119 fdmi dom𝑸=𝑸×𝑸
121 117 118 120 ndmovdistr ¬A𝑸B𝑸C𝑸A𝑸B+𝑸C=A𝑸B+𝑸A𝑸C
122 115 121 pm2.61i A𝑸B+𝑸C=A𝑸B+𝑸A𝑸C