Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvdsmulf1o Unicode version

Theorem dvdsmulf1o 21015
 Description: If and are two coprime integers, multiplication forms a bijection from the set of pairs where and , to the set of divisors of . (Contributed by Mario Carneiro, 2-Jul-2015.)
Hypotheses
Ref Expression
dvdsmulf1o.1
dvdsmulf1o.2
dvdsmulf1o.3
dvdsmulf1o.x
dvdsmulf1o.y
dvdsmulf1o.z
Assertion
Ref Expression
dvdsmulf1o
Distinct variable groups:   ,M   ,N
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem dvdsmulf1o
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-mulf 9125 . . . . . . 7
2 ffn 5642 . . . . . . 7
31, 2ax-mp 5 . . . . . 6
4 dvdsmulf1o.x . . . . . . . . 9
5 ssrab2 3421 . . . . . . . . 9
64, 5eqsstri 3371 . . . . . . . 8
7 nnsscn 10060 . . . . . . . 8
86, 7sstri 3350 . . . . . . 7
9 dvdsmulf1o.y . . . . . . . . 9
10 ssrab2 3421 . . . . . . . . 9
119, 10eqsstri 3371 . . . . . . . 8
1211, 7sstri 3350 . . . . . . 7
13 xpss12 5027 . . . . . . 7
148, 12, 13mp2an 655 . . . . . 6
15 fnssres 5609 . . . . . 6
163, 14, 15mp2an 655 . . . . 5
1716a1i 11 . . . 4
18 ovres 6267 . . . . . . 7
1918adantl 454 . . . . . 6
20 breq1 4250 . . . . . . . . . . 11
2120, 4elrab2 3107 . . . . . . . . . 10
2221simplbi 448 . . . . . . . . 9
2322ad2antrl 710 . . . . . . . 8
24 breq1 4250 . . . . . . . . . . 11
2524, 9elrab2 3107 . . . . . . . . . 10
2625simplbi 448 . . . . . . . . 9
2726ad2antll 711 . . . . . . . 8
2823, 27nnmulcld 10102 . . . . . . 7
2925simprbi 452 . . . . . . . . 9
3029ad2antll 711 . . . . . . . 8
3121simprbi 452 . . . . . . . . 9
3231ad2antrl 710 . . . . . . . 8
3327nnzd 10429 . . . . . . . . . 10
34 dvdsmulf1o.2 . . . . . . . . . . . 12
3534adantr 453 . . . . . . . . . . 11
3635nnzd 10429 . . . . . . . . . 10
3723nnzd 10429 . . . . . . . . . 10
38 dvdscmul 12931 . . . . . . . . . 10
3933, 36, 37, 38syl3anc 1185 . . . . . . . . 9
40 dvdsmulf1o.1 . . . . . . . . . . . 12
4140adantr 453 . . . . . . . . . . 11
4241nnzd 10429 . . . . . . . . . 10
43 dvdsmulc 12932 . . . . . . . . . 10
4437, 42, 36, 43syl3anc 1185 . . . . . . . . 9
4528nnzd 10429 . . . . . . . . . 10
4637, 36zmulcld 10436 . . . . . . . . . 10
4742, 36zmulcld 10436 . . . . . . . . . 10
48 dvdstr 12938 . . . . . . . . . 10
4945, 46, 47, 48syl3anc 1185 . . . . . . . . 9
5039, 44, 49syl2and 471 . . . . . . . 8
5130, 32, 50mp2and 662 . . . . . . 7
52 breq1 4250 . . . . . . . 8
53 dvdsmulf1o.z . . . . . . . 8
5452, 53elrab2 3107 . . . . . . 7
5528, 51, 54sylanbrc 647 . . . . . 6
5619, 55eqeltrd 2521 . . . . 5
5756ralrimivva 2809 . . . 4
58 ffnov 6228 . . . 4
5917, 57, 58sylanbrc 647 . . 3
6023adantr 453 . . . . . . . . . 10
6160nnnn0d 10329 . . . . . . . . 9
62 simprll 740 . . . . . . . . . . 11
63 breq1 4250 . . . . . . . . . . . . 13
6463, 4elrab2 3107 . . . . . . . . . . . 12
6564simplbi 448 . . . . . . . . . . 11
6662, 65syl 16 . . . . . . . . . 10
6766nnnn0d 10329 . . . . . . . . 9
6860nnzd 10429 . . . . . . . . . . . 12
6927adantr 453 . . . . . . . . . . . . 13
7069nnzd 10429 . . . . . . . . . . . 12
71 dvdsmul1 12926 . . . . . . . . . . . 12
7268, 70, 71syl2anc 644 . . . . . . . . . . 11
73 simprr 735 . . . . . . . . . . . 12
748, 62sseldi 3339 . . . . . . . . . . . . 13
75 simprlr 741 . . . . . . . . . . . . . . 15
76 breq1 4250 . . . . . . . . . . . . . . . . 17
7776, 9elrab2 3107 . . . . . . . . . . . . . . . 16
7877simplbi 448 . . . . . . . . . . . . . . 15
7975, 78syl 16 . . . . . . . . . . . . . 14
8079nncnd 10071 . . . . . . . . . . . . 13
8174, 80mulcomd 9164 . . . . . . . . . . . 12
8273, 81eqtrd 2479 . . . . . . . . . . 11
8372, 82breqtrd 4271 . . . . . . . . . 10
8479nnzd 10429 . . . . . . . . . . 11
8536adantr 453 . . . . . . . . . . 11
86 gcdcom 13075 . . . . . . . . . . . . 13
8768, 85, 86syl2anc 644 . . . . . . . . . . . 12
8842adantr 453 . . . . . . . . . . . . 13
8934nnzd 10429 . . . . . . . . . . . . . . . 16
9040nnzd 10429 . . . . . . . . . . . . . . . 16
91 gcdcom 13075 . . . . . . . . . . . . . . . 16
9289, 90, 91syl2anc 644 . . . . . . . . . . . . . . 15
93 dvdsmulf1o.3 . . . . . . . . . . . . . . 15
9492, 93eqtrd 2479 . . . . . . . . . . . . . 14
9594ad2antrr 708 . . . . . . . . . . . . 13
9632adantr 453 . . . . . . . . . . . . 13
97 rpdvds 13179 . . . . . . . . . . . . 13
9885, 68, 88, 95, 96, 97syl32anc 1193 . . . . . . . . . . . 12
9987, 98eqtrd 2479 . . . . . . . . . . 11
10077simprbi 452 . . . . . . . . . . . 12
10175, 100syl 16 . . . . . . . . . . 11
102 rpdvds 13179 . . . . . . . . . . 11
10368, 84, 85, 99, 101, 102syl32anc 1193 . . . . . . . . . 10
10466nnzd 10429 . . . . . . . . . . 11
105 coprmdvds 13157 . . . . . . . . . . 11
10668, 84, 104, 105syl3anc 1185 . . . . . . . . . 10
10783, 103, 106mp2and 662 . . . . . . . . 9
108 dvdsmul1 12926 . . . . . . . . . . . 12
109104, 84, 108syl2anc 644 . . . . . . . . . . 11
11060nncnd 10071 . . . . . . . . . . . . 13
11169nncnd 10071 . . . . . . . . . . . . 13
112110, 111mulcomd 9164 . . . . . . . . . . . 12
11373, 112eqtr3d 2481 . . . . . . . . . . 11
114109, 113breqtrd 4271 . . . . . . . . . 10
115 gcdcom 13075 . . . . . . . . . . . . 13
116104, 85, 115syl2anc 644 . . . . . . . . . . . 12
11764simprbi 452 . . . . . . . . . . . . . 14
11862, 117syl 16 . . . . . . . . . . . . 13
119 rpdvds 13179 . . . . . . . . . . . . 13
12085, 104, 88, 95, 118, 119syl32anc 1193 . . . . . . . . . . . 12
121116, 120eqtrd 2479 . . . . . . . . . . 11
12230adantr 453 . . . . . . . . . . 11
123 rpdvds 13179 . . . . . . . . . . 11
124104, 70, 85, 121, 122, 123syl32anc 1193 . . . . . . . . . 10
125 coprmdvds 13157 . . . . . . . . . . 11
126104, 70, 68, 125syl3anc 1185 . . . . . . . . . 10
127114, 124, 126mp2and 662 . . . . . . . . 9
128 dvdseq 12952 . . . . . . . . 9
12961, 67, 107, 127, 128syl22anc 1186 . . . . . . . 8
13060nnne0d 10099 . . . . . . . . 9
131129oveq1d 6148 . . . . . . . . . 10
13273, 131eqtr4d 2482 . . . . . . . . 9
133111, 80, 110, 130, 132mulcanad 9712 . . . . . . . 8
134129, 133opeq12d 4024 . . . . . . 7
135134expr 600 . . . . . 6
136135ralrimivva 2809 . . . . 5
137136ralrimivva 2809 . . . 4
138 fvres 5792 . . . . . . . . 9
139 fvres 5792 . . . . . . . . 9
140138, 139eqeqan12d 2462 . . . . . . . 8
141140imbi1d 310 . . . . . . 7
142141ralbidva 2732 . . . . . 6
143142ralbiia 2748 . . . . 5
144 fveq2 5779 . . . . . . . . . . 11
145 df-ov 6136 . . . . . . . . . . 11
146144, 145syl6eqr 2497 . . . . . . . . . 10
147146eqeq2d 2458 . . . . . . . . 9
148 eqeq2 2456 . . . . . . . . 9
149147, 148imbi12d 313 . . . . . . . 8
150149ralxp 5062 . . . . . . 7
151 fveq2 5779 . . . . . . . . . . 11
152 df-ov 6136 . . . . . . . . . . 11
153151, 152syl6eqr 2497 . . . . . . . . . 10
154153eqeq1d 2455 . . . . . . . . 9
155 eqeq1 2453 . . . . . . . . 9
156154, 155imbi12d 313 . . . . . . . 8
1571562ralbidv 2758 . . . . . . 7
158150, 157syl5bb 250 . . . . . 6
159158ralxp 5062 . . . . 5
160143, 159bitri 242 . . . 4
161137, 160sylibr 205 . . 3
162 dff13 6056 . . 3
16359, 161, 162sylanbrc 647 . 2
164 breq1 4250 . . . . . . . . . . . 12
165164, 53elrab2 3107 . . . . . . . . . . 11
166165simplbi 448 . . . . . . . . . 10
167166adantl 454 . . . . . . . . 9
168167nnzd 10429 . . . . . . . 8
16940adantr 453 . . . . . . . . 9
170169nnzd 10429 . . . . . . . 8
171169nnne0d 10099 . . . . . . . . 9
172 simpr 449 . . . . . . . . . 10
173172necon3ai 2655 . . . . . . . . 9
174171, 173syl 16 . . . . . . . 8
175 gcdn0cl 13069 . . . . . . . 8
176168, 170, 174, 175syl21anc 1184 . . . . . . 7
177 gcddvds 13070 . . . . . . . . 9
178168, 170, 177syl2anc 644 . . . . . . . 8
179178simprd 451 . . . . . . 7
180 breq1 4250 . . . . . . . 8
181180, 4elrab2 3107 . . . . . . 7
182176, 179, 181sylanbrc 647 . . . . . 6
18334adantr 453 . . . . . . . . 9
184183nnzd 10429 . . . . . . . 8
185183nnne0d 10099 . . . . . . . . 9
186 simpr 449 . . . . . . . . . 10
187186necon3ai 2655 . . . . . . . . 9
188185, 187syl 16 . . . . . . . 8
189 gcdn0cl 13069 . . . . . . . 8
190168, 184, 188, 189syl21anc 1184 . . . . . . 7
191 gcddvds 13070 . . . . . . . . 9
192168, 184, 191syl2anc 644 . . . . . . . 8
193192simprd 451 . . . . . . 7
194 breq1 4250 . . . . . . . 8
195194, 9elrab2 3107 . . . . . . 7
196190, 193, 195sylanbrc 647 . . . . . 6
197 opelxpi 4954 . . . . . 6
198182, 196, 197syl2anc 644 . . . . 5
199 fvres 5792 . . . . . . 7
200198, 199syl 16 . . . . . 6
20193adantr 453 . . . . . . . 8
202 rpmulgcd2 13160 . . . . . . . 8
203168, 170, 184, 201, 202syl31anc 1188 . . . . . . 7
204 df-ov 6136 . . . . . . 7
205203, 204syl6eq 2495 . . . . . 6
206165simprbi 452 . . . . . . . 8
207206adantl 454 . . . . . . 7
20840, 34nnmulcld 10102 . . . . . . . 8
209 gcdeq 13107 . . . . . . . 8
210166, 208, 209syl2anr 466 . . . . . . 7
211207, 210mpbird 225 . . . . . 6
212200, 205, 2113eqtr2rd 2486 . . . . 5
213 fveq2 5779 . . . . . . 7
214213eqeq2d 2458 . . . . . 6
215214rspcev 3065 . . . . 5
216198, 212, 215syl2anc 644 . . . 4
217216ralrimiva 2800 . . 3
218 dffo3 5936 . . 3
21959, 217, 218sylanbrc 647 . 2
220 df-f1o 5512 . 2
221163, 219, 220sylanbrc 647 1
 Colors of variables: wff set class Syntax hints:  -.wn 3  ->wi 4  <->wb 178  /\wa 360  =wceq 1654  e.wcel 1728  =/=wne 2610  A.wral 2716  E.wrex&nb