odzdvds - Metamath Proof Explorer

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

Theorem odzdvds 13136

Description: The only powers of

that are congruent to

are the multiples of the order of

. (Contributed by Mario Carneiro, 28-Feb-2014.)

**Assertion**
Ref	Expression
odzdvds	$/\$ $/\$ $/\$

Proof of Theorem odzdvds Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nn0re 10186	. . . . . . . . 9
2	1	adantl 453	. . . . . . . 8 $/\$ $/\$ $/\$
3		odzcl 13134	. . . . . . . . . 10 $/\$ $/\$
4	3	adantr 452	. . . . . . . . 9 $/\$ $/\$ $/\$
5	4	nnrpd 10603	. . . . . . . 8 $/\$ $/\$ $/\$
6		modlt 11213	. . . . . . . 8 $/\$
7	2, 5, 6	syl2anc 643	. . . . . . 7 $/\$ $/\$ $/\$
8		nn0z 10260	. . . . . . . . . . 11
9	8	adantl 453	. . . . . . . . . 10 $/\$ $/\$ $/\$
10	9, 4	zmodcld 11222	. . . . . . . . 9 $/\$ $/\$ $/\$
11	10	nn0red 10231	. . . . . . . 8 $/\$ $/\$ $/\$
12	4	nnred 9971	. . . . . . . 8 $/\$ $/\$ $/\$
13	11, 12	ltnled 9176	. . . . . . 7 $/\$ $/\$ $/\$
14	7, 13	mpbid 202	. . . . . 6 $/\$ $/\$ $/\$
15		oveq2 6048	. . . . . . . . . . . 12
16	15	oveq1d 6055	. . . . . . . . . . 11
17	16	breq2d 4184	. . . . . . . . . 10
18	17	elrab 3052	. . . . . . . . 9 $/\$
19		ssrab2 3388	. . . . . . . . . . 11
20		nnuz 10477	. . . . . . . . . . 11
21	19, 20	sseqtri 3340	. . . . . . . . . 10
22		infmssuzle 10514	. . . . . . . . . 10 $/\$
23	21, 22	mpan 652	. . . . . . . . 9
24	18, 23	sylbir 205	. . . . . . . 8 $/\$
25	24	ancoms 440	. . . . . . 7 $/\$
26		odzval 13132	. . . . . . . . 9 $/\$ $/\$
27	26	adantr 452	. . . . . . . 8 $/\$ $/\$ $/\$
28	27	breq1d 4182	. . . . . . 7 $/\$ $/\$ $/\$
29	25, 28	syl5ibr 213	. . . . . 6 $/\$ $/\$ $/\$ $/\$
30	14, 29	mtod 170	. . . . 5 $/\$ $/\$ $/\$ $/\$
31		imnan 412	. . . . 5 $/\$
32	30, 31	sylibr 204	. . . 4 $/\$ $/\$ $/\$
33		elnn0 10179	. . . . . 6 $\/$
34	10, 33	sylib 189	. . . . 5 $/\$ $/\$ $/\$ $\/$
35	34	ord 367	. . . 4 $/\$ $/\$ $/\$
36	32, 35	syld 42	. . 3 $/\$ $/\$ $/\$
37		simpl1 960	. . . . . . 7 $/\$ $/\$ $/\$
38	37	nnzd 10330	. . . . . 6 $/\$ $/\$ $/\$
39		dvds0 12820	. . . . . 6
40	38, 39	syl 16	. . . . 5 $/\$ $/\$ $/\$
41		simpl2 961	. . . . . . . . 9 $/\$ $/\$ $/\$
42	41	zcnd 10332	. . . . . . . 8 $/\$ $/\$ $/\$
43	42	exp0d 11472	. . . . . . 7 $/\$ $/\$ $/\$
44	43	oveq1d 6055	. . . . . 6 $/\$ $/\$ $/\$
45		1m1e0 10024	. . . . . 6
46	44, 45	syl6eq 2452	. . . . 5 $/\$ $/\$ $/\$
47	40, 46	breqtrrd 4198	. . . 4 $/\$ $/\$ $/\$
48		oveq2 6048	. . . . . 6
49	48	oveq1d 6055	. . . . 5
50	49	breq2d 4184	. . . 4
51	47, 50	syl5ibrcom 214	. . 3 $/\$ $/\$ $/\$
52	36, 51	impbid 184	. 2 $/\$ $/\$ $/\$
53	4	nnnn0d 10230	. . . . . . . . 9 $/\$ $/\$ $/\$
54	2, 4	nndivred 10004	. . . . . . . . . 10 $/\$ $/\$ $/\$
55		nn0ge0 10203	. . . . . . . . . . . 12
56	55	adantl 453	. . . . . . . . . . 11 $/\$ $/\$ $/\$
57	4	nngt0d 9999	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
58		ge0div 9833	. . . . . . . . . . . 12 $/\$ $/\$
59	2, 12, 57, 58	syl3anc 1184	. . . . . . . . . . 11 $/\$ $/\$ $/\$
60	56, 59	mpbid 202	. . . . . . . . . 10 $/\$ $/\$ $/\$
61		flge0nn0 11180	. . . . . . . . . 10 $/\$
62	54, 60, 61	syl2anc 643	. . . . . . . . 9 $/\$ $/\$ $/\$
63	53, 62	nn0mulcld 10235	. . . . . . . 8 $/\$ $/\$ $/\$
64		zexpcl 11351	. . . . . . . 8 $/\$
65	41, 63, 64	syl2anc 643	. . . . . . 7 $/\$ $/\$ $/\$
66	65	zred 10331	. . . . . 6 $/\$ $/\$ $/\$
67		1re 9046	. . . . . . 7
68	67	a1i 11	. . . . . 6 $/\$ $/\$ $/\$
69		zexpcl 11351	. . . . . . 7 $/\$
70	41, 10, 69	syl2anc 643	. . . . . 6 $/\$ $/\$ $/\$
71	37	nnrpd 10603	. . . . . 6 $/\$ $/\$ $/\$
72	42, 62, 53	expmuld 11481	. . . . . . . 8 $/\$ $/\$ $/\$
73	72	oveq1d 6055	. . . . . . 7 $/\$ $/\$ $/\$
74		zexpcl 11351	. . . . . . . . 9 $/\$
75	41, 53, 74	syl2anc 643	. . . . . . . 8 $/\$ $/\$ $/\$
76		1z 10267	. . . . . . . . 9
77	76	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
78		odzid 13135	. . . . . . . . . 10 $/\$ $/\$
79	78	adantr 452	. . . . . . . . 9 $/\$ $/\$ $/\$
80		moddvds 12814	. . . . . . . . . 10 $/\$ $/\$
81	37, 75, 77, 80	syl3anc 1184	. . . . . . . . 9 $/\$ $/\$ $/\$
82	79, 81	mpbird 224	. . . . . . . 8 $/\$ $/\$ $/\$
83		modexp 11469	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
84	75, 77, 62, 71, 82, 83	syl221anc 1195	. . . . . . 7 $/\$ $/\$ $/\$
85	54	flcld 11162	. . . . . . . . 9 $/\$ $/\$ $/\$
86		1exp 11364	. . . . . . . . 9
87	85, 86	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$
88	87	oveq1d 6055	. . . . . . 7 $/\$ $/\$ $/\$
89	73, 84, 88	3eqtrd 2440	. . . . . 6 $/\$ $/\$ $/\$
90		modmul1 11234	. . . . . 6 $/\$ $/\$ $/\$ $/\$
91	66, 68, 70, 71, 89, 90	syl221anc 1195	. . . . 5 $/\$ $/\$ $/\$
92	42, 10, 63	expaddd 11480	. . . . . . 7 $/\$ $/\$ $/\$
93		modval 11207	. . . . . . . . . . 11 $/\$
94	2, 5, 93	syl2anc 643	. . . . . . . . . 10 $/\$ $/\$ $/\$
95	94	oveq2d 6056	. . . . . . . . 9 $/\$ $/\$ $/\$
96	63	nn0cnd 10232	. . . . . . . . . 10 $/\$ $/\$ $/\$
97	2	recnd 9070	. . . . . . . . . 10 $/\$ $/\$ $/\$
98	96, 97	pncan3d 9370	. . . . . . . . 9 $/\$ $/\$ $/\$
99	95, 98	eqtrd 2436	. . . . . . . 8 $/\$ $/\$ $/\$
100	99	oveq2d 6056	. . . . . . 7 $/\$ $/\$ $/\$
101	92, 100	eqtr3d 2438	. . . . . 6 $/\$ $/\$ $/\$
102	101	oveq1d 6055	. . . . 5 $/\$ $/\$ $/\$
103	70	zcnd 10332	. . . . . . 7 $/\$ $/\$ $/\$
104	103	mulid2d 9062	. . . . . 6 $/\$ $/\$ $/\$
105	104	oveq1d 6055	. . . . 5 $/\$ $/\$ $/\$
106	91, 102, 105	3eqtr3d 2444	. . . 4 $/\$ $/\$ $/\$
107	106	eqeq1d 2412	. . 3 $/\$ $/\$ $/\$
108		zexpcl 11351	. . . . 5 $/\$
109	41, 108	sylancom 649	. . . 4 $/\$ $/\$ $/\$
110		moddvds 12814	. . . 4 $/\$ $/\$
111	37, 109, 77, 110	syl3anc 1184	. . 3 $/\$ $/\$ $/\$
112		moddvds 12814	. . . 4 $/\$ $/\$
113	37, 70, 77, 112	syl3anc 1184	. . 3 $/\$ $/\$ $/\$
114	107, 111, 113	3bitr3d 275	. 2 $/\$ $/\$ $/\$
115		dvdsval3 12811	. . 3 $/\$
116	4, 9, 115	syl2anc 643	. 2 $/\$ $/\$ $/\$
117	52, 114, 116	3bitr4d 277	1 $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $\/$ wo 358 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

crab 2670

wss 3280 class class class wbr 4172

ccnv 4836

cfv 5413 (class class class)co 6040

csup 7403

cr 8945

cc0 8946

c1 8947

caddc 8949

cmul 8951

clt 9076

cle 9077

cmin 9247

cdiv 9633

cn 9956

cn0 10177

cz 10238

cuz 10444

crp 10568

cfl 11156

cmo 11205

cexp 11337

cdivides 12807

cgcd 12961

codz 13107

This theorem is referenced by: odzphi 13137 pockthlem 13228

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-oadd 6687 df-er 6864 df-map 6979 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-sup 7404 df-card 7782 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-n0 10178 df-z 10239 df-uz 10445 df-rp 10569 df-fz 11000 df-fzo 11091 df-fl 11157 df-mod 11206 df-seq 11279 df-exp 11338 df-hash 11574 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-dvds 12808 df-gcd 12962 df-odz 13109 df-phi 13110

W3C validator