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 \cdot N)$
	crth.2	$⊢ T = (0 ..^M) \times (0 ..^N)$
	crth.3	$⊢ F = (x \in S ⟼ ⟨x \mod M, x \mod N⟩)$
	crth.4	$⊢ φ \to (M \in ℕ \land N \in ℕ \land M \gcd N = 1)$
Assertion	crth	$⊢ φ \to F : S \underset{1-1 onto}{⟶} T$

Proof

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

Metamath Proof Explorer

Theorem crth

Proof