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 )