odzdvds - Metamath Proof Explorer

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

Theorem odzdvds 13879

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 10600	. . . . . . . . 9
2	1	adantl 466	. . . . . . . 8 $/\$ $/\$ $/\$
3		odzcl 13877	. . . . . . . . . 10 $/\$ $/\$
4	3	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$
5	4	nnrpd 11038	. . . . . . . 8 $/\$ $/\$ $/\$
6		modlt 11730	. . . . . . . 8 $/\$
7	2, 5, 6	syl2anc 661	. . . . . . 7 $/\$ $/\$ $/\$
8		nn0z 10681	. . . . . . . . . . 11
9	8	adantl 466	. . . . . . . . . 10 $/\$ $/\$ $/\$
10	9, 4	zmodcld 11740	. . . . . . . . 9 $/\$ $/\$ $/\$
11	10	nn0red 10649	. . . . . . . 8 $/\$ $/\$ $/\$
12	4	nnred 10349	. . . . . . . 8 $/\$ $/\$ $/\$
13	11, 12	ltnled 9533	. . . . . . 7 $/\$ $/\$ $/\$
14	7, 13	mpbid 210	. . . . . 6 $/\$ $/\$ $/\$
15		oveq2 6111	. . . . . . . . . . . 12
16	15	oveq1d 6118	. . . . . . . . . . 11
17	16	breq2d 4316	. . . . . . . . . 10
18	17	elrab 3129	. . . . . . . . 9 $/\$
19		ssrab2 3449	. . . . . . . . . . 11
20		nnuz 10908	. . . . . . . . . . 11
21	19, 20	sseqtri 3400	. . . . . . . . . 10
22		infmssuzle 10949	. . . . . . . . . 10 $/\$
23	21, 22	mpan 670	. . . . . . . . 9
24	18, 23	sylbir 213	. . . . . . . 8 $/\$
25	24	ancoms 453	. . . . . . 7 $/\$
26		odzval 13875	. . . . . . . . 9 $/\$ $/\$
27	26	adantr 465	. . . . . . . 8 $/\$ $/\$ $/\$
28	27	breq1d 4314	. . . . . . 7 $/\$ $/\$ $/\$
29	25, 28	syl5ibr 221	. . . . . 6 $/\$ $/\$ $/\$ $/\$
30	14, 29	mtod 177	. . . . 5 $/\$ $/\$ $/\$ $/\$
31		imnan 422	. . . . 5 $/\$
32	30, 31	sylibr 212	. . . 4 $/\$ $/\$ $/\$
33		elnn0 10593	. . . . . 6 $\/$
34	10, 33	sylib 196	. . . . 5 $/\$ $/\$ $/\$ $\/$
35	34	ord 377	. . . 4 $/\$ $/\$ $/\$
36	32, 35	syld 44	. . 3 $/\$ $/\$ $/\$
37		simpl1 991	. . . . . . 7 $/\$ $/\$ $/\$
38	37	nnzd 10758	. . . . . 6 $/\$ $/\$ $/\$
39		dvds0 13560	. . . . . 6
40	38, 39	syl 16	. . . . 5 $/\$ $/\$ $/\$
41		simpl2 992	. . . . . . . . 9 $/\$ $/\$ $/\$
42	41	zcnd 10760	. . . . . . . 8 $/\$ $/\$ $/\$
43	42	exp0d 12014	. . . . . . 7 $/\$ $/\$ $/\$
44	43	oveq1d 6118	. . . . . 6 $/\$ $/\$ $/\$
45		1m1e0 10402	. . . . . 6
46	44, 45	syl6eq 2491	. . . . 5 $/\$ $/\$ $/\$
47	40, 46	breqtrrd 4330	. . . 4 $/\$ $/\$ $/\$
48		oveq2 6111	. . . . . 6
49	48	oveq1d 6118	. . . . 5
50	49	breq2d 4316	. . . 4
51	47, 50	syl5ibrcom 222	. . 3 $/\$ $/\$ $/\$
52	36, 51	impbid 191	. 2 $/\$ $/\$ $/\$
53	4	nnnn0d 10648	. . . . . . . . 9 $/\$ $/\$ $/\$
54	2, 4	nndivred 10382	. . . . . . . . . 10 $/\$ $/\$ $/\$
55		nn0ge0 10617	. . . . . . . . . . . 12
56	55	adantl 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$
57	4	nngt0d 10377	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
58		ge0div 10208	. . . . . . . . . . . 12 $/\$ $/\$
59	2, 12, 57, 58	syl3anc 1218	. . . . . . . . . . 11 $/\$ $/\$ $/\$
60	56, 59	mpbid 210	. . . . . . . . . 10 $/\$ $/\$ $/\$
61		flge0nn0 11678	. . . . . . . . . 10 $/\$
62	54, 60, 61	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$
63	53, 62	nn0mulcld 10653	. . . . . . . 8 $/\$ $/\$ $/\$
64		zexpcl 11892	. . . . . . . 8 $/\$
65	41, 63, 64	syl2anc 661	. . . . . . 7 $/\$ $/\$ $/\$
66	65	zred 10759	. . . . . 6 $/\$ $/\$ $/\$
67		1red 9413	. . . . . 6 $/\$ $/\$ $/\$
68		zexpcl 11892	. . . . . . 7 $/\$
69	41, 10, 68	syl2anc 661	. . . . . 6 $/\$ $/\$ $/\$
70	37	nnrpd 11038	. . . . . 6 $/\$ $/\$ $/\$
71	42, 62, 53	expmuld 12023	. . . . . . . 8 $/\$ $/\$ $/\$
72	71	oveq1d 6118	. . . . . . 7 $/\$ $/\$ $/\$
73		zexpcl 11892	. . . . . . . . 9 $/\$
74	41, 53, 73	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$
75		1zzd 10689	. . . . . . . 8 $/\$ $/\$ $/\$
76		odzid 13878	. . . . . . . . . 10 $/\$ $/\$
77	76	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$
78		moddvds 13554	. . . . . . . . . 10 $/\$ $/\$
79	37, 74, 75, 78	syl3anc 1218	. . . . . . . . 9 $/\$ $/\$ $/\$
80	77, 79	mpbird 232	. . . . . . . 8 $/\$ $/\$ $/\$
81		modexp 12011	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
82	74, 75, 62, 70, 80, 81	syl221anc 1229	. . . . . . 7 $/\$ $/\$ $/\$
83	54	flcld 11660	. . . . . . . . 9 $/\$ $/\$ $/\$
84		1exp 11905	. . . . . . . . 9
85	83, 84	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$
86	85	oveq1d 6118	. . . . . . 7 $/\$ $/\$ $/\$
87	72, 82, 86	3eqtrd 2479	. . . . . 6 $/\$ $/\$ $/\$
88		modmul1 11764	. . . . . 6 $/\$ $/\$ $/\$ $/\$
89	66, 67, 69, 70, 87, 88	syl221anc 1229	. . . . 5 $/\$ $/\$ $/\$
90	42, 10, 63	expaddd 12022	. . . . . . 7 $/\$ $/\$ $/\$
91		modval 11722	. . . . . . . . . . 11 $/\$
92	2, 5, 91	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$
93	92	oveq2d 6119	. . . . . . . . 9 $/\$ $/\$ $/\$
94	63	nn0cnd 10650	. . . . . . . . . 10 $/\$ $/\$ $/\$
95	2	recnd 9424	. . . . . . . . . 10 $/\$ $/\$ $/\$
96	94, 95	pncan3d 9734	. . . . . . . . 9 $/\$ $/\$ $/\$
97	93, 96	eqtrd 2475	. . . . . . . 8 $/\$ $/\$ $/\$
98	97	oveq2d 6119	. . . . . . 7 $/\$ $/\$ $/\$
99	90, 98	eqtr3d 2477	. . . . . 6 $/\$ $/\$ $/\$
100	99	oveq1d 6118	. . . . 5 $/\$ $/\$ $/\$
101	69	zcnd 10760	. . . . . . 7 $/\$ $/\$ $/\$
102	101	mulid2d 9416	. . . . . 6 $/\$ $/\$ $/\$
103	102	oveq1d 6118	. . . . 5 $/\$ $/\$ $/\$
104	89, 100, 103	3eqtr3d 2483	. . . 4 $/\$ $/\$ $/\$
105	104	eqeq1d 2451	. . 3 $/\$ $/\$ $/\$
106		zexpcl 11892	. . . . 5 $/\$
107	41, 106	sylancom 667	. . . 4 $/\$ $/\$ $/\$
108		moddvds 13554	. . . 4 $/\$ $/\$
109	37, 107, 75, 108	syl3anc 1218	. . 3 $/\$ $/\$ $/\$
110		moddvds 13554	. . . 4 $/\$ $/\$
111	37, 69, 75, 110	syl3anc 1218	. . 3 $/\$ $/\$ $/\$
112	105, 109, 111	3bitr3d 283	. 2 $/\$ $/\$ $/\$
113		dvdsval3 13551	. . 3 $/\$
114	4, 9, 113	syl2anc 661	. 2 $/\$ $/\$ $/\$
115	52, 112, 114	3bitr4d 285	1 $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wcel 1756

crab 2731

wss 3340 class class class wbr 4304

ccnv 4851

cfv 5430 (class class class)co 6103

csup 7702

cr 9293

cc0 9294

c1 9295

caddc 9297

cmul 9299

clt 9430

cle 9431

cmin 9607

cdiv 10005

cn 10334

cn0 10591

cz 10658

cuz 10873

crp 11003

cfl 11652

cmo 11720

cexp 11877

cdivides 13547

cgcd 13702

codz 13850

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4415 ax-sep 4425 ax-nul 4433 ax-pow 4482 ax-pr 4543 ax-un 6384 ax-cnex 9350 ax-resscn 9351 ax-1cn 9352 ax-icn 9353 ax-addcl 9354 ax-addrcl 9355 ax-mulcl 9356 ax-mulrcl 9357 ax-mulcom 9358 ax-addass 9359 ax-mulass 9360 ax-distr 9361 ax-i2m1 9362 ax-1ne0 9363 ax-1rid 9364 ax-rnegex 9365 ax-rrecex 9366 ax-cnre 9367 ax-pre-lttri 9368 ax-pre-lttrn 9369 ax-pre-ltadd 9370 ax-pre-mulgt0 9371 ax-pre-sup 9372

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2620 df-nel 2621 df-ral 2732 df-rex 2733 df-reu 2734 df-rmo 2735 df-rab 2736 df-v 2986 df-sbc 3199 df-csb 3301 df-dif 3343 df-un 3345 df-in 3347 df-ss 3354 df-pss 3356 df-nul 3650 df-if 3804 df-pw 3874 df-sn 3890 df-pr 3892 df-tp 3894 df-op 3896 df-uni 4104 df-int 4141 df-iun 4185 df-br 4305 df-opab 4363 df-mpt 4364 df-tr 4398 df-eprel 4644 df-id 4648 df-po 4653 df-so 4654 df-fr 4691 df-we 4693 df-ord 4734 df-on 4735 df-lim 4736 df-suc 4737 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-iota 5393 df-fun 5432 df-fn 5433 df-f 5434 df-f1 5435 df-fo 5436 df-f1o 5437 df-fv 5438 df-riota 6064 df-ov 6106 df-oprab 6107 df-mpt2 6108 df-om 6489 df-1st 6589 df-2nd 6590 df-recs 6844 df-rdg 6878 df-1o 6932 df-oadd 6936 df-er 7113 df-map 7228 df-en 7323 df-dom 7324 df-sdom 7325 df-fin 7326 df-sup 7703 df-card 8121 df-pnf 9432 df-mnf 9433 df-xr 9434 df-ltxr 9435 df-le 9436 df-sub 9609 df-neg 9610 df-div 10006 df-nn 10335 df-2 10392 df-3 10393 df-n0 10592 df-z 10659 df-uz 10874 df-rp 11004 df-fz 11450 df-fzo 11561 df-fl 11654 df-mod 11721 df-seq 11819 df-exp 11878 df-hash 12116 df-cj 12600 df-re 12601 df-im 12602 df-sqr 12736 df-abs 12737 df-dvds 13548 df-gcd 13703 df-odz 13852 df-phi 13853

This theorem is referenced by: odzphi 13880 pockthlem 13978

W3C validator