Metamath Proof Explorer


Theorem crth

Description: The Chinese Remainder Theorem: the function that maps x to its remainder classes mod M and mod N is 1-1 and onto when M and N are coprime. (Contributed by Mario Carneiro, 24-Feb-2014) (Proof shortened by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses crth.1 S=0..^ M N
crth.2 T=0..^M×0..^N
crth.3 F=xSxmodMxmodN
crth.4 φMNMgcdN=1
Assertion crth φF:S1-1 ontoT

Proof

Step Hyp Ref Expression
1 crth.1 S=0..^ M N
2 crth.2 T=0..^M×0..^N
3 crth.3 F=xSxmodMxmodN
4 crth.4 φMNMgcdN=1
5 elfzoelz x0..^ M Nx
6 5 1 eleq2s xSx
7 simpr φxx
8 4 simp1d φM
9 8 adantr φxM
10 zmodfzo xMxmodM0..^M
11 7 9 10 syl2anc φxxmodM0..^M
12 4 simp2d φN
13 12 adantr φxN
14 zmodfzo xNxmodN0..^N
15 7 13 14 syl2anc φxxmodN0..^N
16 11 15 opelxpd φxxmodMxmodN0..^M×0..^N
17 16 2 eleqtrrdi φxxmodMxmodNT
18 6 17 sylan2 φxSxmodMxmodNT
19 18 3 fmptd φF:ST
20 oveq1 x=yxmodM=ymodM
21 oveq1 x=yxmodN=ymodN
22 20 21 opeq12d x=yxmodMxmodN=ymodMymodN
23 opex ymodMymodNV
24 22 3 23 fvmpt ySFy=ymodMymodN
25 24 ad2antrl φySzSFy=ymodMymodN
26 oveq1 x=zxmodM=zmodM
27 oveq1 x=zxmodN=zmodN
28 26 27 opeq12d x=zxmodMxmodN=zmodMzmodN
29 opex zmodMzmodNV
30 28 3 29 fvmpt zSFz=zmodMzmodN
31 30 ad2antll φySzSFz=zmodMzmodN
32 25 31 eqeq12d φySzSFy=FzymodMymodN=zmodMzmodN
33 ovex ymodMV
34 ovex ymodNV
35 33 34 opth ymodMymodN=zmodMzmodNymodM=zmodMymodN=zmodN
36 32 35 bitrdi φySzSFy=FzymodM=zmodMymodN=zmodN
37 8 adantr φySzSM
38 37 nnzd φySzSM
39 12 adantr φySzSN
40 39 nnzd φySzSN
41 simprl φySzSyS
42 41 1 eleqtrdi φySzSy0..^ M N
43 elfzoelz y0..^ M Ny
44 42 43 syl φySzSy
45 simprr φySzSzS
46 45 1 eleqtrdi φySzSz0..^ M N
47 elfzoelz z0..^ M Nz
48 46 47 syl φySzSz
49 44 48 zsubcld φySzSyz
50 4 simp3d φMgcdN=1
51 50 adantr φySzSMgcdN=1
52 coprmdvds2 MNyzMgcdN=1MyzNyz M Nyz
53 38 40 49 51 52 syl31anc φySzSMyzNyz M Nyz
54 moddvds MyzymodM=zmodMMyz
55 37 44 48 54 syl3anc φySzSymodM=zmodMMyz
56 moddvds NyzymodN=zmodNNyz
57 39 44 48 56 syl3anc φySzSymodN=zmodNNyz
58 55 57 anbi12d φySzSymodM=zmodMymodN=zmodNMyzNyz
59 44 zred φySzSy
60 37 39 nnmulcld φySzS M N
61 60 nnrpd φySzS M N+
62 elfzole1 y0..^ M N0y
63 42 62 syl φySzS0y
64 elfzolt2 y0..^ M Ny< M N
65 42 64 syl φySzSy< M N
66 modid y M N+0yy< M Nymod M N=y
67 59 61 63 65 66 syl22anc φySzSymod M N=y
68 48 zred φySzSz
69 elfzole1 z0..^ M N0z
70 46 69 syl φySzS0z
71 elfzolt2 z0..^ M Nz< M N
72 46 71 syl φySzSz< M N
73 modid z M N+0zz< M Nzmod M N=z
74 68 61 70 72 73 syl22anc φySzSzmod M N=z
75 67 74 eqeq12d φySzSymod M N=zmod M Ny=z
76 moddvds M Nyzymod M N=zmod M N M Nyz
77 60 44 48 76 syl3anc φySzSymod M N=zmod M N M Nyz
78 75 77 bitr3d φySzSy=z M Nyz
79 53 58 78 3imtr4d φySzSymodM=zmodMymodN=zmodNy=z
80 36 79 sylbid φySzSFy=Fzy=z
81 80 ralrimivva φySzSFy=Fzy=z
82 dff13 F:S1-1TF:STySzSFy=Fzy=z
83 19 81 82 sylanbrc φF:S1-1T
84 nnnn0 MM0
85 nnnn0 NN0
86 nn0mulcl M0N0 M N0
87 hashfzo0 M N00..^ M N= M N
88 86 87 syl M0N00..^ M N= M N
89 fzofi 0..^MFin
90 fzofi 0..^NFin
91 hashxp 0..^MFin0..^NFin0..^M×0..^N=0..^M0..^N
92 89 90 91 mp2an 0..^M×0..^N=0..^M0..^N
93 hashfzo0 M00..^M=M
94 hashfzo0 N00..^N=N
95 93 94 oveqan12d M0N00..^M0..^N= M N
96 92 95 eqtrid M0N00..^M×0..^N= M N
97 88 96 eqtr4d M0N00..^ M N=0..^M×0..^N
98 fzofi 0..^ M NFin
99 xpfi 0..^MFin0..^NFin0..^M×0..^NFin
100 89 90 99 mp2an 0..^M×0..^NFin
101 hashen 0..^ M NFin0..^M×0..^NFin0..^ M N=0..^M×0..^N0..^ M N0..^M×0..^N
102 98 100 101 mp2an 0..^ M N=0..^M×0..^N0..^ M N0..^M×0..^N
103 97 102 sylib M0N00..^ M N0..^M×0..^N
104 84 85 103 syl2an MN0..^ M N0..^M×0..^N
105 8 12 104 syl2anc φ0..^ M N0..^M×0..^N
106 105 1 2 3brtr4g φST
107 2 100 eqeltri TFin
108 f1finf1o STTFinF:S1-1TF:S1-1 ontoT
109 106 107 108 sylancl φF:S1-1TF:S1-1 ontoT
110 83 109 mpbid φF:S1-1 ontoT