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

Theorem dvdsmulf1o 20932
 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:   ,   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem dvdsmulf1o
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-mulf 9026 . . . . . . 7
2 ffn 5550 . . . . . . 7
31, 2ax-mp 8 . . . . . 6
4 dvdsmulf1o.x . . . . . . . . 9
5 ssrab2 3388 . . . . . . . . 9
64, 5eqsstri 3338 . . . . . . . 8
7 nnsscn 9961 . . . . . . . 8
86, 7sstri 3317 . . . . . . 7
9 dvdsmulf1o.y . . . . . . . . 9
10 ssrab2 3388 . . . . . . . . 9
119, 10eqsstri 3338 . . . . . . . 8
1211, 7sstri 3317 . . . . . . 7
13 xpss12 4940 . . . . . . 7
148, 12, 13mp2an 654 . . . . . 6
15 fnssres 5517 . . . . . 6
163, 14, 15mp2an 654 . . . . 5
1716a1i 11 . . . 4
18 ovres 6172 . . . . . . 7
1918adantl 453 . . . . . 6
20 breq1 4175 . . . . . . . . . . 11
2120, 4elrab2 3054 . . . . . . . . . 10
2221simplbi 447 . . . . . . . . 9
2322ad2antrl 709 . . . . . . . 8
24 breq1 4175 . . . . . . . . . . 11
2524, 9elrab2 3054 . . . . . . . . . 10
2625simplbi 447 . . . . . . . . 9
2726ad2antll 710 . . . . . . . 8
2823, 27nnmulcld 10003 . . . . . . 7
2925simprbi 451 . . . . . . . . 9
3029ad2antll 710 . . . . . . . 8
3121simprbi 451 . . . . . . . . 9
3231ad2antrl 709 . . . . . . . 8
3327nnzd 10330 . . . . . . . . . 10
34 dvdsmulf1o.2 . . . . . . . . . . . 12
3534adantr 452 . . . . . . . . . . 11
3635nnzd 10330 . . . . . . . . . 10
3723nnzd 10330 . . . . . . . . . 10
38 dvdscmul 12831 . . . . . . . . . 10
3933, 36, 37, 38syl3anc 1184 . . . . . . . . 9
40 dvdsmulf1o.1 . . . . . . . . . . . 12
4140adantr 452 . . . . . . . . . . 11
4241nnzd 10330 . . . . . . . . . 10
43 dvdsmulc 12832 . . . . . . . . . 10
4437, 42, 36, 43syl3anc 1184 . . . . . . . . 9
4528nnzd 10330 . . . . . . . . . 10
4637, 36zmulcld 10337 . . . . . . . . . 10
4742, 36zmulcld 10337 . . . . . . . . . 10
48 dvdstr 12838 . . . . . . . . . 10
4945, 46, 47, 48syl3anc 1184 . . . . . . . . 9
5039, 44, 49syl2and 470 . . . . . . . 8
5130, 32, 50mp2and 661 . . . . . . 7
52 breq1 4175 . . . . . . . 8
53 dvdsmulf1o.z . . . . . . . 8
5452, 53elrab2 3054 . . . . . . 7
5528, 51, 54sylanbrc 646 . . . . . 6
5619, 55eqeltrd 2478 . . . . 5
5756ralrimivva 2758 . . . 4
58 ffnov 6133 . . . 4
5917, 57, 58sylanbrc 646 . . 3
6023adantr 452 . . . . . . . . . 10
6160nnnn0d 10230 . . . . . . . . 9
62 simprll 739 . . . . . . . . . . 11
63 breq1 4175 . . . . . . . . . . . . 13
6463, 4elrab2 3054 . . . . . . . . . . . 12
6564simplbi 447 . . . . . . . . . . 11
6662, 65syl 16 . . . . . . . . . 10
6766nnnn0d 10230 . . . . . . . . 9
6860nnzd 10330 . . . . . . . . . . . 12
6927adantr 452 . . . . . . . . . . . . 13
7069nnzd 10330 . . . . . . . . . . . 12
71 dvdsmul1 12826 . . . . . . . . . . . 12
7268, 70, 71syl2anc 643 . . . . . . . . . . 11
73 simprr 734 . . . . . . . . . . . 12
748, 62sseldi 3306 . . . . . . . . . . . . 13
75 simprlr 740 . . . . . . . . . . . . . . 15
76 breq1 4175 . . . . . . . . . . . . . . . . 17
7776, 9elrab2 3054 . . . . . . . . . . . . . . . 16
7877simplbi 447 . . . . . . . . . . . . . . 15
7975, 78syl 16 . . . . . . . . . . . . . 14
8079nncnd 9972 . . . . . . . . . . . . 13
8174, 80mulcomd 9065 . . . . . . . . . . . 12
8273, 81eqtrd 2436 . . . . . . . . . . 11
8372, 82breqtrd 4196 . . . . . . . . . 10
8479nnzd 10330 . . . . . . . . . . 11
8536adantr 452 . . . . . . . . . . 11
86 gcdcom 12975 . . . . . . . . . . . . 13
8768, 85, 86syl2anc 643 . . . . . . . . . . . 12
8842adantr 452 . . . . . . . . . . . . 13
8934nnzd 10330 . . . . . . . . . . . . . . . 16
9040nnzd 10330 . . . . . . . . . . . . . . . 16
91 gcdcom 12975 . . . . . . . . . . . . . . . 16
9289, 90, 91syl2anc 643 . . . . . . . . . . . . . . 15
93 dvdsmulf1o.3 . . . . . . . . . . . . . . 15
9492, 93eqtrd 2436 . . . . . . . . . . . . . 14
9594ad2antrr 707 . . . . . . . . . . . . 13
9632adantr 452 . . . . . . . . . . . . 13
97 rpdvds 13079 . . . . . . . . . . . . 13
9885, 68, 88, 95, 96, 97syl32anc 1192 . . . . . . . . . . . 12
9987, 98eqtrd 2436 . . . . . . . . . . 11
10077simprbi 451 . . . . . . . . . . . 12
10175, 100syl 16 . . . . . . . . . . 11
102 rpdvds 13079 . . . . . . . . . . 11
10368, 84, 85, 99, 101, 102syl32anc 1192 . . . . . . . . . 10
10466nnzd 10330 . . . . . . . . . . 11
105 coprmdvds 13057 . . . . . . . . . . 11
10668, 84, 104, 105syl3anc 1184 . . . . . . . . . 10
10783, 103, 106mp2and 661 . . . . . . . . 9
108 dvdsmul1 12826 . . . . . . . . . . . 12
109104, 84, 108syl2anc 643 . . . . . . . . . . 11
11060nncnd 9972 . . . . . . . . . . . . 13
11169nncnd 9972 . . . . . . . . . . . . 13
112110, 111mulcomd 9065 . . . . . . . . . . . 12
11373, 112eqtr3d 2438 . . . . . . . . . . 11
114109, 113breqtrd 4196 . . . . . . . . . 10
115 gcdcom 12975 . . . . . . . . . . . . 13
116104, 85, 115syl2anc 643 . . . . . . . . . . . 12
11764simprbi 451 . . . . . . . . . . . . . 14
11862, 117syl 16 . . . . . . . . . . . . 13
119 rpdvds 13079 . . . . . . . . . . . . 13
12085, 104, 88, 95, 118, 119syl32anc 1192 . . . . . . . . . . . 12
121116, 120eqtrd 2436 . . . . . . . . . . 11
12230adantr 452 . . . . . . . . . . 11
123 rpdvds 13079 . . . . . . . . . . 11
124104, 70, 85, 121, 122, 123syl32anc 1192 . . . . . . . . . 10
125 coprmdvds 13057 . . . . . . . . . . 11
126104, 70, 68, 125syl3anc 1184 . . . . . . . . . 10
127114, 124, 126mp2and 661 . . . . . . . . 9
128 dvdseq 12852 . . . . . . . . 9
12961, 67, 107, 127, 128syl22anc 1185 . . . . . . . 8
13060nnne0d 10000 . . . . . . . . 9
131129oveq1d 6055 . . . . . . . . . 10
13273, 131eqtr4d 2439 . . . . . . . . 9
133111, 80, 110, 130, 132mulcanad 9613 . . . . . . . 8
134129, 133opeq12d 3952 . . . . . . 7
135134expr 599 . . . . . 6
136135ralrimivva 2758 . . . . 5
137136ralrimivva 2758 . . . 4
138 fvres 5704 . . . . . . . . 9
139 fvres 5704 . . . . . . . . 9
140138, 139eqeqan12d 2419 . . . . . . . 8
141140imbi1d 309 . . . . . . 7
142141ralbidva 2682 . . . . . 6
143142ralbiia 2698 . . . . 5
144 fveq2 5687 . . . . . . . . . . 11
145 df-ov 6043 . . . . . . . . . . 11
146144, 145syl6eqr 2454 . . . . . . . . . 10
147146eqeq2d 2415 . . . . . . . . 9
148 eqeq2 2413 . . . . . . . . 9
149147, 148imbi12d 312 . . . . . . . 8
150149ralxp 4975 . . . . . . 7
151 fveq2 5687 . . . . . . . . . . 11
152 df-ov 6043 . . . . . . . . . . 11
153151, 152syl6eqr 2454 . . . . . . . . . 10
154153eqeq1d 2412 . . . . . . . . 9
155 eqeq1 2410 . . . . . . . . 9
156154, 155imbi12d 312 . . . . . . . 8
1571562ralbidv 2708 . . . . . . 7
158150, 157syl5bb 249 . . . . . 6
159158ralxp 4975 . . . . 5
160143, 159bitri 241 . . . 4
161137, 160sylibr 204 . . 3
162 dff13 5963 . . 3
16359, 161, 162sylanbrc 646 . 2
164 breq1 4175 . . . . . . . . . . . 12
165164, 53elrab2 3054 . . . . . . . . . . 11
166165simplbi 447 . . . . . . . . . 10
167166adantl 453 . . . . . . . . 9
168167nnzd 10330 . . . . . . . 8
16940adantr 452 . . . . . . . . 9
170169nnzd 10330 . . . . . . . 8
171169nnne0d 10000 . . . . . . . . 9
172 simpr 448 . . . . . . . . . 10
173172necon3ai 2607 . . . . . . . . 9
174171, 173syl 16 . . . . . . . 8
175 gcdn0cl 12969 . . . . . . . 8
176168, 170, 174, 175syl21anc 1183 . . . . . . 7
177 gcddvds 12970 . . . . . . . . 9
178168, 170, 177syl2anc 643 . . . . . . . 8
179178simprd 450 . . . . . . 7
180 breq1 4175 . . . . . . . 8
181180, 4elrab2 3054 . . . . . . 7
182176, 179, 181sylanbrc 646 . . . . . 6
18334adantr 452 . . . . . . . . 9
184183nnzd 10330 . . . . . . . 8
185183nnne0d 10000 . . . . . . . . 9
186 simpr 448 . . . . . . . . . 10
187186necon3ai 2607 . . . . . . . . 9
188185, 187syl 16 . . . . . . . 8
189 gcdn0cl 12969 . . . . . . . 8
190168, 184, 188, 189syl21anc 1183 . . . . . . 7
191 gcddvds 12970 . . . . . . . . 9
192168, 184, 191syl2anc 643 . . . . . . . 8
193192simprd 450 . . . . . . 7
194 breq1 4175 . . . . . . . 8
195194, 9elrab2 3054 . . . . . . 7
196190, 193, 195sylanbrc 646 . . . . . 6
197 opelxpi 4869 . . . . . 6
198182, 196, 197syl2anc 643 . . . . 5
199 fvres 5704 . . . . . . 7
200198, 199syl 16 . . . . . 6
20193adantr 452 . . . . . . . 8
202 rpmulgcd2 13060 . . . . . . . 8
203168, 170, 184, 201, 202syl31anc 1187 . . . . . . 7
204 df-ov 6043 . . . . . . 7
205203, 204syl6eq 2452 . . . . . 6
206165simprbi 451 . . . . . . . 8
207206adantl 453 . . . . . . 7
20840, 34nnmulcld 10003 . . . . . . . 8
209 gcdeq 13007 . . . . . . . 8
210166, 208, 209syl2anr 465 . . . . . . 7
211207, 210mpbird 224 . . . . . 6
212200, 205, 2113eqtr2rd 2443 . . . . 5
213 fveq2 5687 . . . . . . 7
214213eqeq2d 2415 . . . . . 6
215214rspcev 3012 . . . . 5
216198, 212, 215syl2anc 643 . . . 4
217216ralrimiva 2749 . . 3
218 dffo3 5843 . . 3
21959, 217, 218sylanbrc 646 . 2
220 df-f1o 5420 . 2
221163, 219, 220sylanbrc 646 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359   wceq 1649   wcel 1721   wne 2567  wral 2666  wrex 2667  crab 2670   wss 3280  cop 3777   class class class wbr 4172   cxp 4835   cres 4839   wfn 5408  wf 5409  wf1 5410  wfo 5411  wf1o 5412  cfv 5413  (class class class)co 6040  cc 8944  cc0 8946  c1 8947   cmul 8951  cn 9956  cn0 10177  cz 10238   cdivides 12807   cgcd 12961 This theorem is referenced by:  fsumdvdsmul  20933 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-mulf 9026 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-sup 7404  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-rp 10569  df-fl 11157  df-mod 11206  df-seq 11279  df-exp 11338  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-dvds 12808  df-gcd 12962
 Copyright terms: Public domain W3C validator