odzdvds - Metamath Proof Explorer

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

Theorem odzdvds 14180

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 10803	. . . . . . . . 9
2	1	adantl 466	. . . . . . . 8 $/\$ $/\$ $/\$
3		odzcl 14178	. . . . . . . . . 10 $/\$ $/\$
4	3	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$
5	4	nnrpd 11254	. . . . . . . 8 $/\$ $/\$ $/\$
6		modlt 11973	. . . . . . . 8 $/\$
7	2, 5, 6	syl2anc 661	. . . . . . 7 $/\$ $/\$ $/\$
8		nn0z 10886	. . . . . . . . . . 11
9	8	adantl 466	. . . . . . . . . 10 $/\$ $/\$ $/\$
10	9, 4	zmodcld 11983	. . . . . . . . 9 $/\$ $/\$ $/\$
11	10	nn0red 10852	. . . . . . . 8 $/\$ $/\$ $/\$
12	4	nnred 10550	. . . . . . . 8 $/\$ $/\$ $/\$
13	11, 12	ltnled 9730	. . . . . . 7 $/\$ $/\$ $/\$
14	7, 13	mpbid 210	. . . . . 6 $/\$ $/\$ $/\$
15		oveq2 6291	. . . . . . . . . . . 12
16	15	oveq1d 6298	. . . . . . . . . . 11
17	16	breq2d 4459	. . . . . . . . . 10
18	17	elrab 3261	. . . . . . . . 9 $/\$
19		ssrab2 3585	. . . . . . . . . . 11
20		nnuz 11116	. . . . . . . . . . 11
21	19, 20	sseqtri 3536	. . . . . . . . . 10
22		infmssuzle 11163	. . . . . . . . . 10 $/\$
23	21, 22	mpan 670	. . . . . . . . 9
24	18, 23	sylbir 213	. . . . . . . 8 $/\$
25	24	ancoms 453	. . . . . . 7 $/\$
26		odzval 14176	. . . . . . . . 9 $/\$ $/\$
27	26	adantr 465	. . . . . . . 8 $/\$ $/\$ $/\$
28	27	breq1d 4457	. . . . . . 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 10796	. . . . . 6 $\/$
34	10, 33	sylib 196	. . . . 5 $/\$ $/\$ $/\$ $\/$
35	34	ord 377	. . . 4 $/\$ $/\$ $/\$
36	32, 35	syld 44	. . 3 $/\$ $/\$ $/\$
37		simpl1 999	. . . . . . 7 $/\$ $/\$ $/\$
38	37	nnzd 10964	. . . . . 6 $/\$ $/\$ $/\$
39		dvds0 13859	. . . . . 6
40	38, 39	syl 16	. . . . 5 $/\$ $/\$ $/\$
41		simpl2 1000	. . . . . . . . 9 $/\$ $/\$ $/\$
42	41	zcnd 10966	. . . . . . . 8 $/\$ $/\$ $/\$
43	42	exp0d 12271	. . . . . . 7 $/\$ $/\$ $/\$
44	43	oveq1d 6298	. . . . . 6 $/\$ $/\$ $/\$
45		1m1e0 10603	. . . . . 6
46	44, 45	syl6eq 2524	. . . . 5 $/\$ $/\$ $/\$
47	40, 46	breqtrrd 4473	. . . 4 $/\$ $/\$ $/\$
48		oveq2 6291	. . . . . 6
49	48	oveq1d 6298	. . . . 5
50	49	breq2d 4459	. . . 4
51	47, 50	syl5ibrcom 222	. . 3 $/\$ $/\$ $/\$
52	36, 51	impbid 191	. 2 $/\$ $/\$ $/\$
53	4	nnnn0d 10851	. . . . . . . . 9 $/\$ $/\$ $/\$
54	2, 4	nndivred 10583	. . . . . . . . . 10 $/\$ $/\$ $/\$
55		nn0ge0 10820	. . . . . . . . . . . 12
56	55	adantl 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$
57	4	nngt0d 10578	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
58		ge0div 10408	. . . . . . . . . . . 12 $/\$ $/\$
59	2, 12, 57, 58	syl3anc 1228	. . . . . . . . . . 11 $/\$ $/\$ $/\$
60	56, 59	mpbid 210	. . . . . . . . . 10 $/\$ $/\$ $/\$
61		flge0nn0 11921	. . . . . . . . . 10 $/\$
62	54, 60, 61	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$
63	53, 62	nn0mulcld 10856	. . . . . . . 8 $/\$ $/\$ $/\$
64		zexpcl 12148	. . . . . . . 8 $/\$
65	41, 63, 64	syl2anc 661	. . . . . . 7 $/\$ $/\$ $/\$
66	65	zred 10965	. . . . . 6 $/\$ $/\$ $/\$
67		1red 9610	. . . . . 6 $/\$ $/\$ $/\$
68		zexpcl 12148	. . . . . . 7 $/\$
69	41, 10, 68	syl2anc 661	. . . . . 6 $/\$ $/\$ $/\$
70	37	nnrpd 11254	. . . . . 6 $/\$ $/\$ $/\$
71	42, 62, 53	expmuld 12280	. . . . . . . 8 $/\$ $/\$ $/\$
72	71	oveq1d 6298	. . . . . . 7 $/\$ $/\$ $/\$
73		zexpcl 12148	. . . . . . . . 9 $/\$
74	41, 53, 73	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$
75		1zzd 10894	. . . . . . . 8 $/\$ $/\$ $/\$
76		odzid 14179	. . . . . . . . . 10 $/\$ $/\$
77	76	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$
78		moddvds 13853	. . . . . . . . . 10 $/\$ $/\$
79	37, 74, 75, 78	syl3anc 1228	. . . . . . . . 9 $/\$ $/\$ $/\$
80	77, 79	mpbird 232	. . . . . . . 8 $/\$ $/\$ $/\$
81		modexp 12268	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
82	74, 75, 62, 70, 80, 81	syl221anc 1239	. . . . . . 7 $/\$ $/\$ $/\$
83	54	flcld 11902	. . . . . . . . 9 $/\$ $/\$ $/\$
84		1exp 12162	. . . . . . . . 9
85	83, 84	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$
86	85	oveq1d 6298	. . . . . . 7 $/\$ $/\$ $/\$
87	72, 82, 86	3eqtrd 2512	. . . . . 6 $/\$ $/\$ $/\$
88		modmul1 12007	. . . . . 6 $/\$ $/\$ $/\$ $/\$
89	66, 67, 69, 70, 87, 88	syl221anc 1239	. . . . 5 $/\$ $/\$ $/\$
90	42, 10, 63	expaddd 12279	. . . . . . 7 $/\$ $/\$ $/\$
91		modval 11965	. . . . . . . . . . 11 $/\$
92	2, 5, 91	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$
93	92	oveq2d 6299	. . . . . . . . 9 $/\$ $/\$ $/\$
94	63	nn0cnd 10853	. . . . . . . . . 10 $/\$ $/\$ $/\$
95	2	recnd 9621	. . . . . . . . . 10 $/\$ $/\$ $/\$
96	94, 95	pncan3d 9932	. . . . . . . . 9 $/\$ $/\$ $/\$
97	93, 96	eqtrd 2508	. . . . . . . 8 $/\$ $/\$ $/\$
98	97	oveq2d 6299	. . . . . . 7 $/\$ $/\$ $/\$
99	90, 98	eqtr3d 2510	. . . . . 6 $/\$ $/\$ $/\$
100	99	oveq1d 6298	. . . . 5 $/\$ $/\$ $/\$
101	69	zcnd 10966	. . . . . . 7 $/\$ $/\$ $/\$
102	101	mulid2d 9613	. . . . . 6 $/\$ $/\$ $/\$
103	102	oveq1d 6298	. . . . 5 $/\$ $/\$ $/\$
104	89, 100, 103	3eqtr3d 2516	. . . 4 $/\$ $/\$ $/\$
105	104	eqeq1d 2469	. . 3 $/\$ $/\$ $/\$
106		zexpcl 12148	. . . . 5 $/\$
107	41, 106	sylancom 667	. . . 4 $/\$ $/\$ $/\$
108		moddvds 13853	. . . 4 $/\$ $/\$
109	37, 107, 75, 108	syl3anc 1228	. . 3 $/\$ $/\$ $/\$
110		moddvds 13853	. . . 4 $/\$ $/\$
111	37, 69, 75, 110	syl3anc 1228	. . 3 $/\$ $/\$ $/\$
112	105, 109, 111	3bitr3d 283	. 2 $/\$ $/\$ $/\$
113		dvdsval3 13850	. . 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 973

wceq 1379

wcel 1767

crab 2818

wss 3476 class class class wbr 4447

ccnv 4998

cfv 5587 (class class class)co 6283

csup 7899

cr 9490

cc0 9491

c1 9492

caddc 9494

cmul 9496

clt 9627

cle 9628

cmin 9804

cdiv 10205

cn 10535

cn0 10794

cz 10863

cuz 11081

crp 11219

cfl 11894

cmo 11963

cexp 12133

cdivides 13846

cgcd 14002

codz 14151

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6575 ax-cnex 9547 ax-resscn 9548 ax-1cn 9549 ax-icn 9550 ax-addcl 9551 ax-addrcl 9552 ax-mulcl 9553 ax-mulrcl 9554 ax-mulcom 9555 ax-addass 9556 ax-mulass 9557 ax-distr 9558 ax-i2m1 9559 ax-1ne0 9560 ax-1rid 9561 ax-rnegex 9562 ax-rrecex 9563 ax-cnre 9564 ax-pre-lttri 9565 ax-pre-lttrn 9566 ax-pre-ltadd 9567 ax-pre-mulgt0 9568 ax-pre-sup 9569

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5550 df-fun 5589 df-fn 5590 df-f 5591 df-f1 5592 df-fo 5593 df-f1o 5594 df-fv 5595 df-riota 6244 df-ov 6286 df-oprab 6287 df-mpt2 6288 df-om 6680 df-1st 6784 df-2nd 6785 df-recs 7042 df-rdg 7076 df-1o 7130 df-oadd 7134 df-er 7311 df-map 7422 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-sup 7900 df-card 8319 df-pnf 9629 df-mnf 9630 df-xr 9631 df-ltxr 9632 df-le 9633 df-sub 9806 df-neg 9807 df-div 10206 df-nn 10536 df-2 10593 df-3 10594 df-n0 10795 df-z 10864 df-uz 11082 df-rp 11220 df-fz 11672 df-fzo 11792 df-fl 11896 df-mod 11964 df-seq 12075 df-exp 12134 df-hash 12373 df-cj 12894 df-re 12895 df-im 12896 df-sqrt 13030 df-abs 13031 df-dvds 13847 df-gcd 14003 df-odz 14153 df-phi 14154

This theorem is referenced by: odzphi 14181 pockthlem 14281

W3C validator