This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 x. N ) )
crth.2 
|- T = ( ( 0 ..^ M ) X. ( 0 ..^ N ) )
crth.3 
|- F = ( x e. S |-> <. ( x mod M ) , ( x mod N ) >. )
crth.4 
|- ( ph -> ( M e. NN /\ N e. NN /\ ( M gcd N ) = 1 ) )
Assertion crth 
|- ( ph -> F : S -1-1-onto-> T )

Proof

Step Hyp Ref Expression
1 crth.1 
 |-  S = ( 0 ..^ ( M x. N ) )
2 crth.2 
 |-  T = ( ( 0 ..^ M ) X. ( 0 ..^ N ) )
3 crth.3 
 |-  F = ( x e. S |-> <. ( x mod M ) , ( x mod N ) >. )
4 crth.4 
 |-  ( ph -> ( M e. NN /\ N e. NN /\ ( M gcd N ) = 1 ) )
5 elfzoelz 
 |-  ( x e. ( 0 ..^ ( M x. N ) ) -> x e. ZZ )
6 5 1 eleq2s 
 |-  ( x e. S -> x e. ZZ )
7 simpr 
 |-  ( ( ph /\ x e. ZZ ) -> x e. ZZ )
8 4 simp1d 
 |-  ( ph -> M e. NN )
9 8 adantr 
 |-  ( ( ph /\ x e. ZZ ) -> M e. NN )
10 zmodfzo 
 |-  ( ( x e. ZZ /\ M e. NN ) -> ( x mod M ) e. ( 0 ..^ M ) )
11 7 9 10 syl2anc 
 |-  ( ( ph /\ x e. ZZ ) -> ( x mod M ) e. ( 0 ..^ M ) )
12 4 simp2d 
 |-  ( ph -> N e. NN )
13 12 adantr 
 |-  ( ( ph /\ x e. ZZ ) -> N e. NN )
14 zmodfzo 
 |-  ( ( x e. ZZ /\ N e. NN ) -> ( x mod N ) e. ( 0 ..^ N ) )
15 7 13 14 syl2anc 
 |-  ( ( ph /\ x e. ZZ ) -> ( x mod N ) e. ( 0 ..^ N ) )
16 11 15 opelxpd 
 |-  ( ( ph /\ x e. ZZ ) -> <. ( x mod M ) , ( x mod N ) >. e. ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) )
17 16 2 eleqtrrdi 
 |-  ( ( ph /\ x e. ZZ ) -> <. ( x mod M ) , ( x mod N ) >. e. T )
18 6 17 sylan2 
 |-  ( ( ph /\ x e. S ) -> <. ( x mod M ) , ( x mod N ) >. e. T )
19 18 3 fmptd 
 |-  ( ph -> F : S --> T )
20 oveq1 
 |-  ( x = y -> ( x mod M ) = ( y mod M ) )
21 oveq1 
 |-  ( x = y -> ( x mod N ) = ( y mod N ) )
22 20 21 opeq12d 
 |-  ( x = y -> <. ( x mod M ) , ( x mod N ) >. = <. ( y mod M ) , ( y mod N ) >. )
23 opex 
 |-  <. ( y mod M ) , ( y mod N ) >. e. _V
24 22 3 23 fvmpt 
 |-  ( y e. S -> ( F ` y ) = <. ( y mod M ) , ( y mod N ) >. )
25 24 ad2antrl 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( F ` y ) = <. ( y mod M ) , ( y mod N ) >. )
26 oveq1 
 |-  ( x = z -> ( x mod M ) = ( z mod M ) )
27 oveq1 
 |-  ( x = z -> ( x mod N ) = ( z mod N ) )
28 26 27 opeq12d 
 |-  ( x = z -> <. ( x mod M ) , ( x mod N ) >. = <. ( z mod M ) , ( z mod N ) >. )
29 opex 
 |-  <. ( z mod M ) , ( z mod N ) >. e. _V
30 28 3 29 fvmpt 
 |-  ( z e. S -> ( F ` z ) = <. ( z mod M ) , ( z mod N ) >. )
31 30 ad2antll 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( F ` z ) = <. ( z mod M ) , ( z mod N ) >. )
32 25 31 eqeq12d 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( ( F ` y ) = ( F ` z ) <-> <. ( y mod M ) , ( y mod N ) >. = <. ( z mod M ) , ( z mod N ) >. ) )
33 ovex 
 |-  ( y mod M ) e. _V
34 ovex 
 |-  ( y mod N ) e. _V
35 33 34 opth 
 |-  ( <. ( y mod M ) , ( y mod N ) >. = <. ( z mod M ) , ( z mod N ) >. <-> ( ( y mod M ) = ( z mod M ) /\ ( y mod N ) = ( z mod N ) ) )
36 32 35 bitrdi 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( ( F ` y ) = ( F ` z ) <-> ( ( y mod M ) = ( z mod M ) /\ ( y mod N ) = ( z mod N ) ) ) )
37 8 adantr 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> M e. NN )
38 37 nnzd 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> M e. ZZ )
39 12 adantr 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> N e. NN )
40 39 nnzd 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> N e. ZZ )
41 simprl 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> y e. S )
42 41 1 eleqtrdi 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> y e. ( 0 ..^ ( M x. N ) ) )
43 elfzoelz 
 |-  ( y e. ( 0 ..^ ( M x. N ) ) -> y e. ZZ )
44 42 43 syl 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> y e. ZZ )
45 simprr 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> z e. S )
46 45 1 eleqtrdi 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> z e. ( 0 ..^ ( M x. N ) ) )
47 elfzoelz 
 |-  ( z e. ( 0 ..^ ( M x. N ) ) -> z e. ZZ )
48 46 47 syl 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> z e. ZZ )
49 44 48 zsubcld 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( y - z ) e. ZZ )
50 4 simp3d 
 |-  ( ph -> ( M gcd N ) = 1 )
51 50 adantr 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( M gcd N ) = 1 )
52 coprmdvds2 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ ( y - z ) e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( M || ( y - z ) /\ N || ( y - z ) ) -> ( M x. N ) || ( y - z ) ) )
53 38 40 49 51 52 syl31anc 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( ( M || ( y - z ) /\ N || ( y - z ) ) -> ( M x. N ) || ( y - z ) ) )
54 moddvds 
 |-  ( ( M e. NN /\ y e. ZZ /\ z e. ZZ ) -> ( ( y mod M ) = ( z mod M ) <-> M || ( y - z ) ) )
55 37 44 48 54 syl3anc 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( ( y mod M ) = ( z mod M ) <-> M || ( y - z ) ) )
56 moddvds 
 |-  ( ( N e. NN /\ y e. ZZ /\ z e. ZZ ) -> ( ( y mod N ) = ( z mod N ) <-> N || ( y - z ) ) )
57 39 44 48 56 syl3anc 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( ( y mod N ) = ( z mod N ) <-> N || ( y - z ) ) )
58 55 57 anbi12d 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( ( ( y mod M ) = ( z mod M ) /\ ( y mod N ) = ( z mod N ) ) <-> ( M || ( y - z ) /\ N || ( y - z ) ) ) )
59 44 zred 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> y e. RR )
60 37 39 nnmulcld 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( M x. N ) e. NN )
61 60 nnrpd 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( M x. N ) e. RR+ )
62 elfzole1 
 |-  ( y e. ( 0 ..^ ( M x. N ) ) -> 0 <_ y )
63 42 62 syl 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> 0 <_ y )
64 elfzolt2 
 |-  ( y e. ( 0 ..^ ( M x. N ) ) -> y < ( M x. N ) )
65 42 64 syl 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> y < ( M x. N ) )
66 modid 
 |-  ( ( ( y e. RR /\ ( M x. N ) e. RR+ ) /\ ( 0 <_ y /\ y < ( M x. N ) ) ) -> ( y mod ( M x. N ) ) = y )
67 59 61 63 65 66 syl22anc 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( y mod ( M x. N ) ) = y )
68 48 zred 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> z e. RR )
69 elfzole1 
 |-  ( z e. ( 0 ..^ ( M x. N ) ) -> 0 <_ z )
70 46 69 syl 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> 0 <_ z )
71 elfzolt2 
 |-  ( z e. ( 0 ..^ ( M x. N ) ) -> z < ( M x. N ) )
72 46 71 syl 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> z < ( M x. N ) )
73 modid 
 |-  ( ( ( z e. RR /\ ( M x. N ) e. RR+ ) /\ ( 0 <_ z /\ z < ( M x. N ) ) ) -> ( z mod ( M x. N ) ) = z )
74 68 61 70 72 73 syl22anc 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( z mod ( M x. N ) ) = z )
75 67 74 eqeq12d 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( ( y mod ( M x. N ) ) = ( z mod ( M x. N ) ) <-> y = z ) )
76 moddvds 
 |-  ( ( ( M x. N ) e. NN /\ y e. ZZ /\ z e. ZZ ) -> ( ( y mod ( M x. N ) ) = ( z mod ( M x. N ) ) <-> ( M x. N ) || ( y - z ) ) )
77 60 44 48 76 syl3anc 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( ( y mod ( M x. N ) ) = ( z mod ( M x. N ) ) <-> ( M x. N ) || ( y - z ) ) )
78 75 77 bitr3d 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( y = z <-> ( M x. N ) || ( y - z ) ) )
79 53 58 78 3imtr4d 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( ( ( y mod M ) = ( z mod M ) /\ ( y mod N ) = ( z mod N ) ) -> y = z ) )
80 36 79 sylbid 
 |-  ( ( ph /\ ( y e. S /\ z e. S ) ) -> ( ( F ` y ) = ( F ` z ) -> y = z ) )
81 80 ralrimivva 
 |-  ( ph -> A. y e. S A. z e. S ( ( F ` y ) = ( F ` z ) -> y = z ) )
82 dff13 
 |-  ( F : S -1-1-> T <-> ( F : S --> T /\ A. y e. S A. z e. S ( ( F ` y ) = ( F ` z ) -> y = z ) ) )
83 19 81 82 sylanbrc 
 |-  ( ph -> F : S -1-1-> T )
84 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
85 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
86 nn0mulcl 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M x. N ) e. NN0 )
87 hashfzo0 
 |-  ( ( M x. N ) e. NN0 -> ( # ` ( 0 ..^ ( M x. N ) ) ) = ( M x. N ) )
88 86 87 syl 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( # ` ( 0 ..^ ( M x. N ) ) ) = ( M x. N ) )
89 fzofi 
 |-  ( 0 ..^ M ) e. Fin
90 fzofi 
 |-  ( 0 ..^ N ) e. Fin
91 hashxp 
 |-  ( ( ( 0 ..^ M ) e. Fin /\ ( 0 ..^ N ) e. Fin ) -> ( # ` ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) ) = ( ( # ` ( 0 ..^ M ) ) x. ( # ` ( 0 ..^ N ) ) ) )
92 89 90 91 mp2an 
 |-  ( # ` ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) ) = ( ( # ` ( 0 ..^ M ) ) x. ( # ` ( 0 ..^ N ) ) )
93 hashfzo0 
 |-  ( M e. NN0 -> ( # ` ( 0 ..^ M ) ) = M )
94 hashfzo0 
 |-  ( N e. NN0 -> ( # ` ( 0 ..^ N ) ) = N )
95 93 94 oveqan12d 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( # ` ( 0 ..^ M ) ) x. ( # ` ( 0 ..^ N ) ) ) = ( M x. N ) )
96 92 95 eqtrid 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( # ` ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) ) = ( M x. N ) )
97 88 96 eqtr4d 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( # ` ( 0 ..^ ( M x. N ) ) ) = ( # ` ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) ) )
98 fzofi 
 |-  ( 0 ..^ ( M x. N ) ) e. Fin
99 xpfi 
 |-  ( ( ( 0 ..^ M ) e. Fin /\ ( 0 ..^ N ) e. Fin ) -> ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) e. Fin )
100 89 90 99 mp2an 
 |-  ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) e. Fin
101 hashen 
 |-  ( ( ( 0 ..^ ( M x. N ) ) e. Fin /\ ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) e. Fin ) -> ( ( # ` ( 0 ..^ ( M x. N ) ) ) = ( # ` ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) ) <-> ( 0 ..^ ( M x. N ) ) ~~ ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) ) )
102 98 100 101 mp2an 
 |-  ( ( # ` ( 0 ..^ ( M x. N ) ) ) = ( # ` ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) ) <-> ( 0 ..^ ( M x. N ) ) ~~ ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) )
103 97 102 sylib 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( 0 ..^ ( M x. N ) ) ~~ ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) )
104 84 85 103 syl2an 
 |-  ( ( M e. NN /\ N e. NN ) -> ( 0 ..^ ( M x. N ) ) ~~ ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) )
105 8 12 104 syl2anc 
 |-  ( ph -> ( 0 ..^ ( M x. N ) ) ~~ ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) )
106 105 1 2 3brtr4g 
 |-  ( ph -> S ~~ T )
107 2 100 eqeltri 
 |-  T e. Fin
108 f1finf1o 
 |-  ( ( S ~~ T /\ T e. Fin ) -> ( F : S -1-1-> T <-> F : S -1-1-onto-> T ) )
109 106 107 108 sylancl 
 |-  ( ph -> ( F : S -1-1-> T <-> F : S -1-1-onto-> T ) )
110 83 109 mpbid 
 |-  ( ph -> F : S -1-1-onto-> T )