odzdvds - Metamath Proof Explorer

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

Theorem odzdvds 14752

Description: The only powers of

that are congruent to

are the multiples of the order of

. (Contributed by Mario Carneiro, 28-Feb-2014.) (Proof shortened by AV, 26-Sep-2020.)

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

Proof of Theorem odzdvds Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nn0re 10885	. . . . . . . . 9
2	1	adantl 468	. . . . . . . 8 $/\$ $/\$ $/\$
3		odzcl 14750	. . . . . . . . . 10 $/\$ $/\$
4	3	adantr 467	. . . . . . . . 9 $/\$ $/\$ $/\$
5	4	nnrpd 11346	. . . . . . . 8 $/\$ $/\$ $/\$
6		modlt 12114	. . . . . . . 8 $/\$
7	2, 5, 6	syl2anc 667	. . . . . . 7 $/\$ $/\$ $/\$
8		nn0z 10967	. . . . . . . . . . 11
9	8	adantl 468	. . . . . . . . . 10 $/\$ $/\$ $/\$
10	9, 4	zmodcld 12124	. . . . . . . . 9 $/\$ $/\$ $/\$
11	10	nn0red 10933	. . . . . . . 8 $/\$ $/\$ $/\$
12	4	nnred 10631	. . . . . . . 8 $/\$ $/\$ $/\$
13	11, 12	ltnled 9787	. . . . . . 7 $/\$ $/\$ $/\$
14	7, 13	mpbid 214	. . . . . 6 $/\$ $/\$ $/\$
15		oveq2 6303	. . . . . . . . . . . 12
16	15	oveq1d 6310	. . . . . . . . . . 11
17	16	breq2d 4417	. . . . . . . . . 10
18	17	elrab 3198	. . . . . . . . 9 $/\$
19		ssrab2 3516	. . . . . . . . . . 11
20		nnuz 11201	. . . . . . . . . . 11
21	19, 20	sseqtri 3466	. . . . . . . . . 10
22		infssuzle 11251	. . . . . . . . . 10 $/\$ inf
23	21, 22	mpan 677	. . . . . . . . 9 inf
24	18, 23	sylbir 217	. . . . . . . 8 $/\$ inf
25	24	ancoms 455	. . . . . . 7 $/\$ inf
26		odzval 14748	. . . . . . . . 9 $/\$ $/\$ inf
27	26	adantr 467	. . . . . . . 8 $/\$ $/\$ $/\$ inf
28	27	breq1d 4415	. . . . . . 7 $/\$ $/\$ $/\$ inf
29	25, 28	syl5ibr 225	. . . . . 6 $/\$ $/\$ $/\$ $/\$
30	14, 29	mtod 181	. . . . 5 $/\$ $/\$ $/\$ $/\$
31		imnan 424	. . . . 5 $/\$
32	30, 31	sylibr 216	. . . 4 $/\$ $/\$ $/\$
33		elnn0 10878	. . . . . 6 $\/$
34	10, 33	sylib 200	. . . . 5 $/\$ $/\$ $/\$ $\/$
35	34	ord 379	. . . 4 $/\$ $/\$ $/\$
36	32, 35	syld 45	. . 3 $/\$ $/\$ $/\$
37		simpl1 1012	. . . . . . 7 $/\$ $/\$ $/\$
38	37	nnzd 11046	. . . . . 6 $/\$ $/\$ $/\$
39		dvds0 14330	. . . . . 6
40	38, 39	syl 17	. . . . 5 $/\$ $/\$ $/\$
41		simpl2 1013	. . . . . . . . 9 $/\$ $/\$ $/\$
42	41	zcnd 11048	. . . . . . . 8 $/\$ $/\$ $/\$
43	42	exp0d 12417	. . . . . . 7 $/\$ $/\$ $/\$
44	43	oveq1d 6310	. . . . . 6 $/\$ $/\$ $/\$
45		1m1e0 10685	. . . . . 6
46	44, 45	syl6eq 2503	. . . . 5 $/\$ $/\$ $/\$
47	40, 46	breqtrrd 4432	. . . 4 $/\$ $/\$ $/\$
48		oveq2 6303	. . . . . 6
49	48	oveq1d 6310	. . . . 5
50	49	breq2d 4417	. . . 4
51	47, 50	syl5ibrcom 226	. . 3 $/\$ $/\$ $/\$
52	36, 51	impbid 194	. 2 $/\$ $/\$ $/\$
53	4	nnnn0d 10932	. . . . . . . . 9 $/\$ $/\$ $/\$
54	2, 4	nndivred 10665	. . . . . . . . . 10 $/\$ $/\$ $/\$
55		nn0ge0 10902	. . . . . . . . . . . 12
56	55	adantl 468	. . . . . . . . . . 11 $/\$ $/\$ $/\$
57	4	nngt0d 10660	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
58		ge0div 10479	. . . . . . . . . . . 12 $/\$ $/\$
59	2, 12, 57, 58	syl3anc 1269	. . . . . . . . . . 11 $/\$ $/\$ $/\$
60	56, 59	mpbid 214	. . . . . . . . . 10 $/\$ $/\$ $/\$
61		flge0nn0 12061	. . . . . . . . . 10 $/\$
62	54, 60, 61	syl2anc 667	. . . . . . . . 9 $/\$ $/\$ $/\$
63	53, 62	nn0mulcld 10937	. . . . . . . 8 $/\$ $/\$ $/\$
64		zexpcl 12294	. . . . . . . 8 $/\$
65	41, 63, 64	syl2anc 667	. . . . . . 7 $/\$ $/\$ $/\$
66	65	zred 11047	. . . . . 6 $/\$ $/\$ $/\$
67		1red 9663	. . . . . 6 $/\$ $/\$ $/\$
68		zexpcl 12294	. . . . . . 7 $/\$
69	41, 10, 68	syl2anc 667	. . . . . 6 $/\$ $/\$ $/\$
70	37	nnrpd 11346	. . . . . 6 $/\$ $/\$ $/\$
71	42, 62, 53	expmuld 12426	. . . . . . . 8 $/\$ $/\$ $/\$
72	71	oveq1d 6310	. . . . . . 7 $/\$ $/\$ $/\$
73		zexpcl 12294	. . . . . . . . 9 $/\$
74	41, 53, 73	syl2anc 667	. . . . . . . 8 $/\$ $/\$ $/\$
75		1zzd 10975	. . . . . . . 8 $/\$ $/\$ $/\$
76		odzid 14751	. . . . . . . . . 10 $/\$ $/\$
77	76	adantr 467	. . . . . . . . 9 $/\$ $/\$ $/\$
78		moddvds 14324	. . . . . . . . . 10 $/\$ $/\$
79	37, 74, 75, 78	syl3anc 1269	. . . . . . . . 9 $/\$ $/\$ $/\$
80	77, 79	mpbird 236	. . . . . . . 8 $/\$ $/\$ $/\$
81		modexp 12414	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
82	74, 75, 62, 70, 80, 81	syl221anc 1280	. . . . . . 7 $/\$ $/\$ $/\$
83	54	flcld 12041	. . . . . . . . 9 $/\$ $/\$ $/\$
84		1exp 12308	. . . . . . . . 9
85	83, 84	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$
86	85	oveq1d 6310	. . . . . . 7 $/\$ $/\$ $/\$
87	72, 82, 86	3eqtrd 2491	. . . . . 6 $/\$ $/\$ $/\$
88		modmul1 12150	. . . . . 6 $/\$ $/\$ $/\$ $/\$
89	66, 67, 69, 70, 87, 88	syl221anc 1280	. . . . 5 $/\$ $/\$ $/\$
90	42, 10, 63	expaddd 12425	. . . . . . 7 $/\$ $/\$ $/\$
91		modval 12105	. . . . . . . . . . 11 $/\$
92	2, 5, 91	syl2anc 667	. . . . . . . . . 10 $/\$ $/\$ $/\$
93	92	oveq2d 6311	. . . . . . . . 9 $/\$ $/\$ $/\$
94	63	nn0cnd 10934	. . . . . . . . . 10 $/\$ $/\$ $/\$
95	2	recnd 9674	. . . . . . . . . 10 $/\$ $/\$ $/\$
96	94, 95	pncan3d 9994	. . . . . . . . 9 $/\$ $/\$ $/\$
97	93, 96	eqtrd 2487	. . . . . . . 8 $/\$ $/\$ $/\$
98	97	oveq2d 6311	. . . . . . 7 $/\$ $/\$ $/\$
99	90, 98	eqtr3d 2489	. . . . . 6 $/\$ $/\$ $/\$
100	99	oveq1d 6310	. . . . 5 $/\$ $/\$ $/\$
101	69	zcnd 11048	. . . . . . 7 $/\$ $/\$ $/\$
102	101	mulid2d 9666	. . . . . 6 $/\$ $/\$ $/\$
103	102	oveq1d 6310	. . . . 5 $/\$ $/\$ $/\$
104	89, 100, 103	3eqtr3d 2495	. . . 4 $/\$ $/\$ $/\$
105	104	eqeq1d 2455	. . 3 $/\$ $/\$ $/\$
106		zexpcl 12294	. . . . 5 $/\$
107	41, 106	sylancom 674	. . . 4 $/\$ $/\$ $/\$
108		moddvds 14324	. . . 4 $/\$ $/\$
109	37, 107, 75, 108	syl3anc 1269	. . 3 $/\$ $/\$ $/\$
110		moddvds 14324	. . . 4 $/\$ $/\$
111	37, 69, 75, 110	syl3anc 1269	. . 3 $/\$ $/\$ $/\$
112	105, 109, 111	3bitr3d 287	. 2 $/\$ $/\$ $/\$
113		dvdsval3 14321	. . 3 $/\$
114	4, 9, 113	syl2anc 667	. 2 $/\$ $/\$ $/\$
115	52, 112, 114	3bitr4d 289	1 $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $/\$ w3a 986

wceq 1446

wcel 1889

crab 2743

wss 3406 class class class wbr 4405

cfv 5585 (class class class)co 6295 infcinf 7960

cr 9543

cc0 9544

c1 9545

caddc 9547

cmul 9549

clt 9680

cle 9681

cmin 9865

cdiv 10276

cn 10616

cn0 10876

cz 10944

cuz 11166

crp 11309

cfl 12033

cmo 12103

cexp 12279

cdvds 14317

cgcd 14480

codz 14721

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-rep 4518 ax-sep 4528 ax-nul 4537 ax-pow 4584 ax-pr 4642 ax-un 6588 ax-cnex 9600 ax-resscn 9601 ax-1cn 9602 ax-icn 9603 ax-addcl 9604 ax-addrcl 9605 ax-mulcl 9606 ax-mulrcl 9607 ax-mulcom 9608 ax-addass 9609 ax-mulass 9610 ax-distr 9611 ax-i2m1 9612 ax-1ne0 9613 ax-1rid 9614 ax-rnegex 9615 ax-rrecex 9616 ax-cnre 9617 ax-pre-lttri 9618 ax-pre-lttrn 9619 ax-pre-ltadd 9620 ax-pre-mulgt0 9621 ax-pre-sup 9622

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-nel 2627 df-ral 2744 df-rex 2745 df-reu 2746 df-rmo 2747 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-pss 3422 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-tp 3975 df-op 3977 df-uni 4202 df-int 4238 df-iun 4283 df-br 4406 df-opab 4465 df-mpt 4466 df-tr 4501 df-eprel 4748 df-id 4752 df-po 4758 df-so 4759 df-fr 4796 df-we 4798 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-pred 5383 df-ord 5429 df-on 5430 df-lim 5431 df-suc 5432 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593 df-riota 6257 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-om 6698 df-1st 6798 df-2nd 6799 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-1o 7187 df-oadd 7191 df-er 7368 df-map 7479 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-sup 7961 df-inf 7962 df-card 8378 df-pnf 9682 df-mnf 9683 df-xr 9684 df-ltxr 9685 df-le 9686 df-sub 9867 df-neg 9868 df-div 10277 df-nn 10617 df-2 10675 df-3 10676 df-n0 10877 df-z 10945 df-uz 11167 df-rp 11310 df-fz 11792 df-fzo 11923 df-fl 12035 df-mod 12104 df-seq 12221 df-exp 12280 df-hash 12523 df-cj 13174 df-re 13175 df-im 13176 df-sqrt 13310 df-abs 13311 df-dvds 14318 df-gcd 14481 df-odz 14724 df-phi 14726

This theorem is referenced by: odzphi 14753 pockthlem 14861

W3C validator