crt - Metamath Proof Explorer

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

Theorem crt 14308

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

**Hypotheses**
Ref	Expression
crt.1
crt.2
crt.3
crt.4

**Assertion**
Ref	Expression
crt

Distinct variable groups: ,M , ,S , ,N

Proof of Theorem crt Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfzoelz 11829	. . . . . 6
2		crt.1	. . . . . 6
3	1, 2	eleq2s 2565	. . . . 5
4		simpr 461	. . . . . . . 8
5		crt.4	. . . . . . . . . 10
6	5	simp1d 1008	. . . . . . . . 9
7	6	adantr 465	. . . . . . . 8
8		zmodfzo 12018	. . . . . . . 8
9	4, 7, 8	syl2anc 661	. . . . . . 7
10	5	simp2d 1009	. . . . . . . . 9
11	10	adantr 465	. . . . . . . 8
12		zmodfzo 12018	. . . . . . . 8
13	4, 11, 12	syl2anc 661	. . . . . . 7
14		opelxpi 5036	. . . . . . 7
15	9, 13, 14	syl2anc 661	. . . . . 6
16		crt.2	. . . . . 6
17	15, 16	syl6eleqr 2556	. . . . 5
18	3, 17	sylan2 474	. . . 4
19		crt.3	. . . 4
20	18, 19	fmptd 6055	. . 3
21		oveq1 6303	. . . . . . . . . 10
22		oveq1 6303	. . . . . . . . . 10
23	21, 22	opeq12d 4225	. . . . . . . . 9
24		opex 4716	. . . . . . . . 9
25	23, 19, 24	fvmpt 5956	. . . . . . . 8
26	25	ad2antrl 727	. . . . . . 7
27		oveq1 6303	. . . . . . . . . 10
28		oveq1 6303	. . . . . . . . . 10
29	27, 28	opeq12d 4225	. . . . . . . . 9
30		opex 4716	. . . . . . . . 9
31	29, 19, 30	fvmpt 5956	. . . . . . . 8
32	31	ad2antll 728	. . . . . . 7
33	26, 32	eqeq12d 2479	. . . . . 6
34		ovex 6324	. . . . . . 7
35		ovex 6324	. . . . . . 7
36	34, 35	opth 4726	. . . . . 6
37	33, 36	syl6bb 261	. . . . 5
38	6	adantr 465	. . . . . . . 8
39	38	nnzd 10993	. . . . . . 7
40	10	adantr 465	. . . . . . . 8
41	40	nnzd 10993	. . . . . . 7
42		simprl 756	. . . . . . . . . 10
43	42, 2	syl6eleq 2555	. . . . . . . . 9
44		elfzoelz 11829	. . . . . . . . 9
45	43, 44	syl 16	. . . . . . . 8
46		simprr 757	. . . . . . . . . 10
47	46, 2	syl6eleq 2555	. . . . . . . . 9
48		elfzoelz 11829	. . . . . . . . 9
49	47, 48	syl 16	. . . . . . . 8
50	45, 49	zsubcld 10999	. . . . . . 7
51	5	simp3d 1010	. . . . . . . 8
52	51	adantr 465	. . . . . . 7
53		coprmdvds2 14244	. . . . . . 7
54	39, 41, 50, 52, 53	syl31anc 1231	. . . . . 6
55		moddvds 13993	. . . . . . . 8
56	38, 45, 49, 55	syl3anc 1228	. . . . . . 7
57		moddvds 13993	. . . . . . . 8
58	40, 45, 49, 57	syl3anc 1228	. . . . . . 7
59	56, 58	anbi12d 710	. . . . . 6
60	45	zred 10994	. . . . . . . . 9
61	38, 40	nnmulcld 10608	. . . . . . . . . 10
62	61	nnrpd 11284	. . . . . . . . 9
63		elfzole1 11836	. . . . . . . . . 10
64	43, 63	syl 16	. . . . . . . . 9
65		elfzolt2 11837	. . . . . . . . . 10
66	43, 65	syl 16	. . . . . . . . 9
67		modid 12020	. . . . . . . . 9
68	60, 62, 64, 66, 67	syl22anc 1229	. . . . . . . 8
69	49	zred 10994	. . . . . . . . 9
70		elfzole1 11836	. . . . . . . . . 10
71	47, 70	syl 16	. . . . . . . . 9
72		elfzolt2 11837	. . . . . . . . . 10
73	47, 72	syl 16	. . . . . . . . 9
74		modid 12020	. . . . . . . . 9
75	69, 62, 71, 73, 74	syl22anc 1229	. . . . . . . 8
76	68, 75	eqeq12d 2479	. . . . . . 7
77		moddvds 13993	. . . . . . . 8
78	61, 45, 49, 77	syl3anc 1228	. . . . . . 7
79	76, 78	bitr3d 255	. . . . . 6
80	54, 59, 79	3imtr4d 268	. . . . 5
81	37, 80	sylbid 215	. . . 4
82	81	ralrimivva 2878	. . 3
83		dff13 6166	. . 3
84	20, 82, 83	sylanbrc 664	. 2
85		nnnn0 10827	. . . . . 6
86		nnnn0 10827	. . . . . 6
87		nn0mulcl 10857	. . . . . . . . 9
88		hashfzo0 12488	. . . . . . . . 9
89	87, 88	syl 16	. . . . . . . 8
90		fzofi 12084	. . . . . . . . . 10
91		fzofi 12084	. . . . . . . . . 10
92		hashxp 12492	. . . . . . . . . 10
93	90, 91, 92	mp2an 672	. . . . . . . . 9
94		hashfzo0 12488	. . . . . . . . . 10
95		hashfzo0 12488	. . . . . . . . . 10
96	94, 95	oveqan12d 6315	. . . . . . . . 9
97	93, 96	syl5eq 2510	. . . . . . . 8
98	89, 97	eqtr4d 2501	. . . . . . 7
99		fzofi 12084	. . . . . . . 8
100		xpfi 7811	. . . . . . . . 9
101	90, 91, 100	mp2an 672	. . . . . . . 8
102		hashen 12420	. . . . . . . 8
103	99, 101, 102	mp2an 672	. . . . . . 7
104	98, 103	sylib 196	. . . . . 6
105	85, 86, 104	syl2an 477	. . . . 5
106	6, 10, 105	syl2anc 661	. . . 4
107	106, 2, 16	3brtr4g 4484	. . 3
108	16, 101	eqeltri 2541	. . 3
109		f1finf1o 7766	. . 3
110	107, 108, 109	sylancl 662	. 2
111	84, 110	mpbid 210	1

Colors of variables: wff setvar class

Syntax hints: ->wi 4 <->wb 184 /\wa 369 /\w3a 973 =wceq 1395 e.wcel 1818 A.wral 2807 <.cop 4035 class class class wbr 4452 e.cmpt 4510 X.cxp 5002 -->wf 5589 -1-1->wf1 5590 -1-1-onto->wf1o 5592 `cfv 5593 (class class class)co 6296 cen 7533 cfn 7536 cr 9512 0cc0 9513 1c1 9514 cmul 9518 clt 9649 cle 9650 cmin 9828 cn 10561 cn0 10820 cz 10889 crp 11249 cfzo 11824 cmo 11996 chash 12405 cdvds 13986 cgcd 14144

This theorem is referenced by: phimullem 14309

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704 ax-6 1747 ax-7 1790 ax-8 1820 ax-9 1822 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 ax-rep 4563 ax-sep 4573 ax-nul 4581 ax-pow 4630 ax-pr 4691 ax-un 6592 ax-cnex 9569 ax-resscn 9570 ax-1cn 9571 ax-icn 9572 ax-addcl 9573 ax-addrcl 9574 ax-mulcl 9575 ax-mulrcl 9576 ax-mulcom 9577 ax-addass 9578 ax-mulass 9579 ax-distr 9580 ax-i2m1 9581 ax-1ne0 9582 ax-1rid 9583 ax-rnegex 9584 ax-rrecex 9585 ax-cnre 9586 ax-pre-lttri 9587 ax-pre-lttrn 9588 ax-pre-ltadd 9589 ax-pre-mulgt0 9590 ax-pre-sup 9591

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-eu 2286 df-mo 2287 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3435 df-dif 3478 df-un 3480 df-in 3482 df-ss 3489 df-pss 3491 df-nul 3785 df-if 3942 df-pw 4014 df-sn 4030 df-pr 4032 df-tp 4034 df-op 4036 df-uni 4250 df-int 4287 df-iun 4332 df-br 4453 df-opab 4511 df-mpt 4512 df-tr 4546 df-eprel 4796 df-id 4800 df-po 4805 df-so 4806 df-fr 4843 df-we 4845 df-ord 4886 df-on 4887 df-lim 4888 df-suc 4889 df-xp 5010 df-rel 5011 df-cnv 5012 df-co 5013 df-dm 5014 df-rn 5015 df-res 5016 df-ima 5017 df-iota 5556 df-fun 5595 df-fn 5596 df-f 5597 df-f1 5598 df-fo 5599 df-f1o 5600 df-fv 5601 df-riota 6257 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6701 df-1st 6800 df-2nd 6801 df-recs 7061 df-rdg 7095 df-1o 7149 df-oadd 7153 df-er 7330 df-map 7441 df-en 7537 df-dom 7538 df-sdom 7539 df-fin 7540 df-sup 7921 df-card 8341 df-cda 8569 df-pnf 9651 df-mnf 9652 df-xr 9653 df-ltxr 9654 df-le 9655 df-sub 9830 df-neg 9831 df-div 10232 df-nn 10562 df-2 10619 df-3 10620 df-n0 10821 df-z 10890 df-uz 11111 df-rp 11250 df-fz 11702 df-fzo 11825 df-fl 11929 df-mod 11997 df-seq 12108 df-exp 12167 df-hash 12406 df-cj 12932 df-re 12933 df-im 12934 df-sqrt 13068 df-abs 13069 df-dvds 13987 df-gcd 14145

W3C validator