odzdvds - Metamath Proof Explorer

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

Theorem odzdvds 14698

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 10867	. . . . . . . . 9
2	1	adantl 467	. . . . . . . 8 $/\$ $/\$ $/\$
3		odzcl 14696	. . . . . . . . . 10 $/\$ $/\$
4	3	adantr 466	. . . . . . . . 9 $/\$ $/\$ $/\$
5	4	nnrpd 11328	. . . . . . . 8 $/\$ $/\$ $/\$
6		modlt 12093	. . . . . . . 8 $/\$
7	2, 5, 6	syl2anc 665	. . . . . . 7 $/\$ $/\$ $/\$
8		nn0z 10949	. . . . . . . . . . 11
9	8	adantl 467	. . . . . . . . . 10 $/\$ $/\$ $/\$
10	9, 4	zmodcld 12103	. . . . . . . . 9 $/\$ $/\$ $/\$
11	10	nn0red 10915	. . . . . . . 8 $/\$ $/\$ $/\$
12	4	nnred 10613	. . . . . . . 8 $/\$ $/\$ $/\$
13	11, 12	ltnled 9771	. . . . . . 7 $/\$ $/\$ $/\$
14	7, 13	mpbid 213	. . . . . 6 $/\$ $/\$ $/\$
15		oveq2 6304	. . . . . . . . . . . 12
16	15	oveq1d 6311	. . . . . . . . . . 11
17	16	breq2d 4429	. . . . . . . . . 10
18	17	elrab 3226	. . . . . . . . 9 $/\$
19		ssrab2 3543	. . . . . . . . . . 11
20		nnuz 11183	. . . . . . . . . . 11
21	19, 20	sseqtri 3493	. . . . . . . . . 10
22		infmssuzleOLD 11235	. . . . . . . . . 10 $/\$
23	21, 22	mpan 674	. . . . . . . . 9
24	18, 23	sylbir 216	. . . . . . . 8 $/\$
25	24	ancoms 454	. . . . . . 7 $/\$
26		odzval 14694	. . . . . . . . 9 $/\$ $/\$
27	26	adantr 466	. . . . . . . 8 $/\$ $/\$ $/\$
28	27	breq1d 4427	. . . . . . 7 $/\$ $/\$ $/\$
29	25, 28	syl5ibr 224	. . . . . 6 $/\$ $/\$ $/\$ $/\$
30	14, 29	mtod 180	. . . . 5 $/\$ $/\$ $/\$ $/\$
31		imnan 423	. . . . 5 $/\$
32	30, 31	sylibr 215	. . . 4 $/\$ $/\$ $/\$
33		elnn0 10860	. . . . . 6 $\/$
34	10, 33	sylib 199	. . . . 5 $/\$ $/\$ $/\$ $\/$
35	34	ord 378	. . . 4 $/\$ $/\$ $/\$
36	32, 35	syld 45	. . 3 $/\$ $/\$ $/\$
37		simpl1 1008	. . . . . . 7 $/\$ $/\$ $/\$
38	37	nnzd 11028	. . . . . 6 $/\$ $/\$ $/\$
39		dvds0 14285	. . . . . 6
40	38, 39	syl 17	. . . . 5 $/\$ $/\$ $/\$
41		simpl2 1009	. . . . . . . . 9 $/\$ $/\$ $/\$
42	41	zcnd 11030	. . . . . . . 8 $/\$ $/\$ $/\$
43	42	exp0d 12396	. . . . . . 7 $/\$ $/\$ $/\$
44	43	oveq1d 6311	. . . . . 6 $/\$ $/\$ $/\$
45		1m1e0 10667	. . . . . 6
46	44, 45	syl6eq 2477	. . . . 5 $/\$ $/\$ $/\$
47	40, 46	breqtrrd 4443	. . . 4 $/\$ $/\$ $/\$
48		oveq2 6304	. . . . . 6
49	48	oveq1d 6311	. . . . 5
50	49	breq2d 4429	. . . 4
51	47, 50	syl5ibrcom 225	. . 3 $/\$ $/\$ $/\$
52	36, 51	impbid 193	. 2 $/\$ $/\$ $/\$
53	4	nnnn0d 10914	. . . . . . . . 9 $/\$ $/\$ $/\$
54	2, 4	nndivred 10647	. . . . . . . . . 10 $/\$ $/\$ $/\$
55		nn0ge0 10884	. . . . . . . . . . . 12
56	55	adantl 467	. . . . . . . . . . 11 $/\$ $/\$ $/\$
57	4	nngt0d 10642	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
58		ge0div 10461	. . . . . . . . . . . 12 $/\$ $/\$
59	2, 12, 57, 58	syl3anc 1264	. . . . . . . . . . 11 $/\$ $/\$ $/\$
60	56, 59	mpbid 213	. . . . . . . . . 10 $/\$ $/\$ $/\$
61		flge0nn0 12040	. . . . . . . . . 10 $/\$
62	54, 60, 61	syl2anc 665	. . . . . . . . 9 $/\$ $/\$ $/\$
63	53, 62	nn0mulcld 10919	. . . . . . . 8 $/\$ $/\$ $/\$
64		zexpcl 12273	. . . . . . . 8 $/\$
65	41, 63, 64	syl2anc 665	. . . . . . 7 $/\$ $/\$ $/\$
66	65	zred 11029	. . . . . 6 $/\$ $/\$ $/\$
67		1red 9647	. . . . . 6 $/\$ $/\$ $/\$
68		zexpcl 12273	. . . . . . 7 $/\$
69	41, 10, 68	syl2anc 665	. . . . . 6 $/\$ $/\$ $/\$
70	37	nnrpd 11328	. . . . . 6 $/\$ $/\$ $/\$
71	42, 62, 53	expmuld 12405	. . . . . . . 8 $/\$ $/\$ $/\$
72	71	oveq1d 6311	. . . . . . 7 $/\$ $/\$ $/\$
73		zexpcl 12273	. . . . . . . . 9 $/\$
74	41, 53, 73	syl2anc 665	. . . . . . . 8 $/\$ $/\$ $/\$
75		1zzd 10957	. . . . . . . 8 $/\$ $/\$ $/\$
76		odzid 14697	. . . . . . . . . 10 $/\$ $/\$
77	76	adantr 466	. . . . . . . . 9 $/\$ $/\$ $/\$
78		moddvds 14279	. . . . . . . . . 10 $/\$ $/\$
79	37, 74, 75, 78	syl3anc 1264	. . . . . . . . 9 $/\$ $/\$ $/\$
80	77, 79	mpbird 235	. . . . . . . 8 $/\$ $/\$ $/\$
81		modexp 12393	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
82	74, 75, 62, 70, 80, 81	syl221anc 1275	. . . . . . 7 $/\$ $/\$ $/\$
83	54	flcld 12020	. . . . . . . . 9 $/\$ $/\$ $/\$
84		1exp 12287	. . . . . . . . 9
85	83, 84	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$
86	85	oveq1d 6311	. . . . . . 7 $/\$ $/\$ $/\$
87	72, 82, 86	3eqtrd 2465	. . . . . 6 $/\$ $/\$ $/\$
88		modmul1 12129	. . . . . 6 $/\$ $/\$ $/\$ $/\$
89	66, 67, 69, 70, 87, 88	syl221anc 1275	. . . . 5 $/\$ $/\$ $/\$
90	42, 10, 63	expaddd 12404	. . . . . . 7 $/\$ $/\$ $/\$
91		modval 12084	. . . . . . . . . . 11 $/\$
92	2, 5, 91	syl2anc 665	. . . . . . . . . 10 $/\$ $/\$ $/\$
93	92	oveq2d 6312	. . . . . . . . 9 $/\$ $/\$ $/\$
94	63	nn0cnd 10916	. . . . . . . . . 10 $/\$ $/\$ $/\$
95	2	recnd 9658	. . . . . . . . . 10 $/\$ $/\$ $/\$
96	94, 95	pncan3d 9978	. . . . . . . . 9 $/\$ $/\$ $/\$
97	93, 96	eqtrd 2461	. . . . . . . 8 $/\$ $/\$ $/\$
98	97	oveq2d 6312	. . . . . . 7 $/\$ $/\$ $/\$
99	90, 98	eqtr3d 2463	. . . . . 6 $/\$ $/\$ $/\$
100	99	oveq1d 6311	. . . . 5 $/\$ $/\$ $/\$
101	69	zcnd 11030	. . . . . . 7 $/\$ $/\$ $/\$
102	101	mulid2d 9650	. . . . . 6 $/\$ $/\$ $/\$
103	102	oveq1d 6311	. . . . 5 $/\$ $/\$ $/\$
104	89, 100, 103	3eqtr3d 2469	. . . 4 $/\$ $/\$ $/\$
105	104	eqeq1d 2422	. . 3 $/\$ $/\$ $/\$
106		zexpcl 12273	. . . . 5 $/\$
107	41, 106	sylancom 671	. . . 4 $/\$ $/\$ $/\$
108		moddvds 14279	. . . 4 $/\$ $/\$
109	37, 107, 75, 108	syl3anc 1264	. . 3 $/\$ $/\$ $/\$
110		moddvds 14279	. . . 4 $/\$ $/\$
111	37, 69, 75, 110	syl3anc 1264	. . 3 $/\$ $/\$ $/\$
112	105, 109, 111	3bitr3d 286	. 2 $/\$ $/\$ $/\$
113		dvdsval3 14276	. . 3 $/\$
114	4, 9, 113	syl2anc 665	. 2 $/\$ $/\$ $/\$
115	52, 112, 114	3bitr4d 288	1 $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1867

crab 2777

wss 3433 class class class wbr 4417

ccnv 4844

cfv 5592 (class class class)co 6296

csup 7951

cr 9527

cc0 9528

c1 9529

caddc 9531

cmul 9533

clt 9664

cle 9665

cmin 9849

cdiv 10258

cn 10598

cn0 10858

cz 10926

cuz 11148

crp 11291

cfl 12012

cmo 12082

cexp 12258

cdvds 14272

cgcd 14431

codz 14669

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1838 ax-8 1869 ax-9 1871 ax-10 1886 ax-11 1891 ax-12 1904 ax-13 2052 ax-ext 2398 ax-rep 4529 ax-sep 4539 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6588 ax-cnex 9584 ax-resscn 9585 ax-1cn 9586 ax-icn 9587 ax-addcl 9588 ax-addrcl 9589 ax-mulcl 9590 ax-mulrcl 9591 ax-mulcom 9592 ax-addass 9593 ax-mulass 9594 ax-distr 9595 ax-i2m1 9596 ax-1ne0 9597 ax-1rid 9598 ax-rnegex 9599 ax-rrecex 9600 ax-cnre 9601 ax-pre-lttri 9602 ax-pre-lttrn 9603 ax-pre-ltadd 9604 ax-pre-mulgt0 9605 ax-pre-sup 9606

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2267 df-mo 2268 df-clab 2406 df-cleq 2412 df-clel 2415 df-nfc 2570 df-ne 2618 df-nel 2619 df-ral 2778 df-rex 2779 df-reu 2780 df-rmo 2781 df-rab 2782 df-v 3080 df-sbc 3297 df-csb 3393 df-dif 3436 df-un 3438 df-in 3440 df-ss 3447 df-pss 3449 df-nul 3759 df-if 3907 df-pw 3978 df-sn 3994 df-pr 3996 df-tp 3998 df-op 4000 df-uni 4214 df-int 4250 df-iun 4295 df-br 4418 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4756 df-id 4760 df-po 4766 df-so 4767 df-fr 4804 df-we 4806 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-pred 5390 df-ord 5436 df-on 5437 df-lim 5438 df-suc 5439 df-iota 5556 df-fun 5594 df-fn 5595 df-f 5596 df-f1 5597 df-fo 5598 df-f1o 5599 df-fv 5600 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6698 df-1st 6798 df-2nd 6799 df-wrecs 7027 df-recs 7089 df-rdg 7127 df-1o 7181 df-oadd 7185 df-er 7362 df-map 7473 df-en 7569 df-dom 7570 df-sdom 7571 df-fin 7572 df-sup 7953 df-inf 7954 df-card 8363 df-pnf 9666 df-mnf 9667 df-xr 9668 df-ltxr 9669 df-le 9670 df-sub 9851 df-neg 9852 df-div 10259 df-nn 10599 df-2 10657 df-3 10658 df-n0 10859 df-z 10927 df-uz 11149 df-rp 11292 df-fz 11772 df-fzo 11903 df-fl 12014 df-mod 12083 df-seq 12200 df-exp 12259 df-hash 12502 df-cj 13130 df-re 13131 df-im 13132 df-sqrt 13266 df-abs 13267 df-dvds 14273 df-gcd 14432 df-odz 14671 df-phi 14672

This theorem is referenced by: odzphi 14699 pockthlem 14801

W3C validator