eulerthlem2 - Metamath Proof Explorer

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

Theorem eulerthlem2 15487

Description: Lemma for eulerth 15488. (Contributed by Mario Carneiro, 28-Feb-2014.)

**Hypotheses**
Ref	Expression
eulerth.1	$/\$ $/\$
eulerth.2	..^
eulerth.3
eulerth.4
eulerth.5

**Assertion**
Ref	Expression
eulerthlem2

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem eulerthlem2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eulerth.1	. . . . . . . . . . 11 $/\$ $/\$
2	1	simp1d 1073	. . . . . . . . . 10
3	2	phicld 15477	. . . . . . . . 9
4	3	nnred 11035	. . . . . . . 8
5	4	leidd 10594	. . . . . . 7
6	3	adantr 481	. . . . . . . 8 $/\$
7		breq1 4656	. . . . . . . . . . 11
8	7	anbi2d 740	. . . . . . . . . 10 $/\$ $/\$
9		oveq2 6658	. . . . . . . . . . . . . 14
10		fveq2 6191	. . . . . . . . . . . . . 14
11	9, 10	oveq12d 6668	. . . . . . . . . . . . 13
12	11	oveq1d 6665	. . . . . . . . . . . 12
13		fveq2 6191	. . . . . . . . . . . . 13
14	13	oveq1d 6665	. . . . . . . . . . . 12
15	12, 14	eqeq12d 2637	. . . . . . . . . . 11
16	10	oveq2d 6666	. . . . . . . . . . . 12
17	16	eqeq1d 2624	. . . . . . . . . . 11
18	15, 17	anbi12d 747	. . . . . . . . . 10 $/\$ $/\$
19	8, 18	imbi12d 334	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
20		breq1 4656	. . . . . . . . . . 11
21	20	anbi2d 740	. . . . . . . . . 10 $/\$ $/\$
22		oveq2 6658	. . . . . . . . . . . . . 14
23		fveq2 6191	. . . . . . . . . . . . . 14
24	22, 23	oveq12d 6668	. . . . . . . . . . . . 13
25	24	oveq1d 6665	. . . . . . . . . . . 12
26		fveq2 6191	. . . . . . . . . . . . 13
27	26	oveq1d 6665	. . . . . . . . . . . 12
28	25, 27	eqeq12d 2637	. . . . . . . . . . 11
29	23	oveq2d 6666	. . . . . . . . . . . 12
30	29	eqeq1d 2624	. . . . . . . . . . 11
31	28, 30	anbi12d 747	. . . . . . . . . 10 $/\$ $/\$
32	21, 31	imbi12d 334	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
33		breq1 4656	. . . . . . . . . . 11
34	33	anbi2d 740	. . . . . . . . . 10 $/\$ $/\$
35		oveq2 6658	. . . . . . . . . . . . . 14
36		fveq2 6191	. . . . . . . . . . . . . 14
37	35, 36	oveq12d 6668	. . . . . . . . . . . . 13
38	37	oveq1d 6665	. . . . . . . . . . . 12
39		fveq2 6191	. . . . . . . . . . . . 13
40	39	oveq1d 6665	. . . . . . . . . . . 12
41	38, 40	eqeq12d 2637	. . . . . . . . . . 11
42	36	oveq2d 6666	. . . . . . . . . . . 12
43	42	eqeq1d 2624	. . . . . . . . . . 11
44	41, 43	anbi12d 747	. . . . . . . . . 10 $/\$ $/\$
45	34, 44	imbi12d 334	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
46		breq1 4656	. . . . . . . . . . 11
47	46	anbi2d 740	. . . . . . . . . 10 $/\$ $/\$
48		oveq2 6658	. . . . . . . . . . . . . 14
49		fveq2 6191	. . . . . . . . . . . . . 14
50	48, 49	oveq12d 6668	. . . . . . . . . . . . 13
51	50	oveq1d 6665	. . . . . . . . . . . 12
52		fveq2 6191	. . . . . . . . . . . . 13
53	52	oveq1d 6665	. . . . . . . . . . . 12
54	51, 53	eqeq12d 2637	. . . . . . . . . . 11
55	49	oveq2d 6666	. . . . . . . . . . . 12
56	55	eqeq1d 2624	. . . . . . . . . . 11
57	54, 56	anbi12d 747	. . . . . . . . . 10 $/\$ $/\$
58	47, 57	imbi12d 334	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
59	1	simp2d 1074	. . . . . . . . . . . . . . 15
60		eulerth.4	. . . . . . . . . . . . . . . . . . . 20
61		f1of 6137	. . . . . . . . . . . . . . . . . . . 20
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . 19
63		nnuz 11723	. . . . . . . . . . . . . . . . . . . . . 22
64	3, 63	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . 21
65		eluzfz1 12348	. . . . . . . . . . . . . . . . . . . . 21
66	64, 65	syl 17	. . . . . . . . . . . . . . . . . . . 20
67		eulerth.3	. . . . . . . . . . . . . . . . . . . 20
68	66, 67	syl6eleqr 2712	. . . . . . . . . . . . . . . . . . 19
69	62, 68	ffvelrnd 6360	. . . . . . . . . . . . . . . . . 18
70		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20
71	70	eqeq1d 2624	. . . . . . . . . . . . . . . . . . 19
72		eulerth.2	. . . . . . . . . . . . . . . . . . 19 ..^
73	71, 72	elrab2 3366	. . . . . . . . . . . . . . . . . 18 ..^ $/\$
74	69, 73	sylib 208	. . . . . . . . . . . . . . . . 17 ..^ $/\$
75	74	simpld 475	. . . . . . . . . . . . . . . 16 ..^
76		elfzoelz 12470	. . . . . . . . . . . . . . . 16 ..^
77	75, 76	syl 17	. . . . . . . . . . . . . . 15
78	59, 77	zmulcld 11488	. . . . . . . . . . . . . 14
79	78	zred 11482	. . . . . . . . . . . . 13
80	2	nnrpd 11870	. . . . . . . . . . . . 13
81		modabs2 12704	. . . . . . . . . . . . 13 $/\$
82	79, 80, 81	syl2anc 693	. . . . . . . . . . . 12
83		1z 11407	. . . . . . . . . . . . . 14
84		fveq2 6191	. . . . . . . . . . . . . . . . . 18
85	84	oveq2d 6666	. . . . . . . . . . . . . . . . 17
86	85	oveq1d 6665	. . . . . . . . . . . . . . . 16
87		eulerth.5	. . . . . . . . . . . . . . . 16
88		ovex 6678	. . . . . . . . . . . . . . . 16
89	86, 87, 88	fvmpt 6282	. . . . . . . . . . . . . . 15
90	68, 89	syl 17	. . . . . . . . . . . . . 14
91	83, 90	seq1i 12815	. . . . . . . . . . . . 13
92	91	oveq1d 6665	. . . . . . . . . . . 12
93	59	zcnd 11483	. . . . . . . . . . . . . . 15
94	93	exp1d 13003	. . . . . . . . . . . . . 14
95		seq1 12814	. . . . . . . . . . . . . . . 16
96	83, 95	ax-mp 5	. . . . . . . . . . . . . . 15
97	96	a1i 11	. . . . . . . . . . . . . 14
98	94, 97	oveq12d 6668	. . . . . . . . . . . . 13
99	98	oveq1d 6665	. . . . . . . . . . . 12
100	82, 92, 99	3eqtr4rd 2667	. . . . . . . . . . 11
101	96	oveq2i 6661	. . . . . . . . . . . 12
102	2	nnzd 11481	. . . . . . . . . . . . . 14
103		gcdcom 15235	. . . . . . . . . . . . . 14 $/\$
104	102, 77, 103	syl2anc 693	. . . . . . . . . . . . 13
105	74	simprd 479	. . . . . . . . . . . . 13
106	104, 105	eqtrd 2656	. . . . . . . . . . . 12
107	101, 106	syl5eq 2668	. . . . . . . . . . 11
108	100, 107	jca 554	. . . . . . . . . 10 $/\$
109	108	adantr 481	. . . . . . . . 9 $/\$ $/\$
110		nnre 11027	. . . . . . . . . . . . . . 15
111	110	adantr 481	. . . . . . . . . . . . . 14 $/\$
112	111	lep1d 10955	. . . . . . . . . . . . 13 $/\$
113		peano2re 10209	. . . . . . . . . . . . . . 15
114	111, 113	syl 17	. . . . . . . . . . . . . 14 $/\$
115	4	adantl 482	. . . . . . . . . . . . . 14 $/\$
116		letr 10131	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
117	111, 114, 115, 116	syl3anc 1326	. . . . . . . . . . . . 13 $/\$ $/\$
118	112, 117	mpand 711	. . . . . . . . . . . 12 $/\$
119	118	imdistanda 729	. . . . . . . . . . 11 $/\$ $/\$
120	119	imim1d 82	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
121	59	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
122		nnnn0 11299	. . . . . . . . . . . . . . . . . . . 20
123	122	ad2antrl 764	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
124		zexpcl 12875	. . . . . . . . . . . . . . . . . . 19 $/\$
125	121, 123, 124	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
126		simprl 794	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
127	126, 63	syl6eleq 2711	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
128	110	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
129	128, 113	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
130	4	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
131	128	lep1d 10955	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
132		simprr 796	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
133	128, 129, 130, 131, 132	letrd 10194	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
134		nnz 11399	. . . . . . . . . . . . . . . . . . . . . . . . . 26
135	134	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
136	3	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . . . . . 26
137	136	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
138		eluz 11701	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
139	135, 137, 138	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
140	133, 139	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
141		fzss2 12381	. . . . . . . . . . . . . . . . . . . . . . 23
142	140, 141	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
143	142, 67	syl6sseqr 3652	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
144	143	sselda 3603	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
145	62	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
146		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . 26
147	146	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . 25
148	147, 72	elrab2 3366	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ $/\$
149	145, 148	sylib 208	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
150	149	simpld 475	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^
151		elfzoelz 12470	. . . . . . . . . . . . . . . . . . . . . 22 ..^
152	150, 151	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$
153	152	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
154	144, 153	syldan 487	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
155		zmulcl 11426	. . . . . . . . . . . . . . . . . . . 20 $/\$
156	155	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
157	127, 154, 156	seqcl 12821	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
158	125, 157	zmulcld 11488	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
159	158	zred 11482	. . . . . . . . . . . . . . . 16 $/\$ $/\$
160		ssrab2 3687	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
161	72, 160	eqsstri 3635	. . . . . . . . . . . . . . . . . . . . . 22 ..^
162	1, 72, 67, 60, 87	eulerthlem1 15486	. . . . . . . . . . . . . . . . . . . . . . 23
163	162	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
164	161, 163	sseldi 3601	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^
165		elfzoelz 12470	. . . . . . . . . . . . . . . . . . . . 21 ..^
166	164, 165	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
167	166	adantlr 751	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
168	144, 167	syldan 487	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
169	127, 168, 156	seqcl 12821	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
170	169	zred 11482	. . . . . . . . . . . . . . . 16 $/\$ $/\$
171	62	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
172		peano2nn 11032	. . . . . . . . . . . . . . . . . . . . . . . . 25
173	172	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
174	173	nnge1d 11063	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
175	173	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
176		elfz 12332	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
177	83, 176	mp3an2 1412	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
178	175, 137, 177	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
179	174, 132, 178	mpbir2and 957	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
180	179, 67	syl6eleqr 2712	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
181	171, 180	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
182		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22
183	182	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . 21
184	183, 72	elrab2 3366	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
185	181, 184	sylib 208	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^ $/\$
186	185	simpld 475	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
187		elfzoelz 12470	. . . . . . . . . . . . . . . . . 18 ..^
188	186, 187	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
189	121, 188	zmulcld 11488	. . . . . . . . . . . . . . . 16 $/\$ $/\$
190	80	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
191		modmul1 12723	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
192	191	3expia 1267	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
193	159, 170, 189, 190, 192	syl22anc 1327	. . . . . . . . . . . . . . 15 $/\$ $/\$
194	125	zcnd 11483	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
195	157	zcnd 11483	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
196	93	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
197	188	zcnd 11483	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
198	194, 195, 196, 197	mul4d 10248	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
199	196, 123	expp1d 13009	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
200		seqp1 12816	. . . . . . . . . . . . . . . . . . . 20
201	127, 200	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
202	199, 201	oveq12d 6668	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
203	198, 202	eqtr4d 2659	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
204	203	oveq1d 6665	. . . . . . . . . . . . . . . 16 $/\$ $/\$
205	189	zred 11482	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
206	205, 190	modcld 12674	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
207		modabs2 12704	. . . . . . . . . . . . . . . . . . 19 $/\$
208	205, 190, 207	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
209		modmul1 12723	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
210	206, 205, 169, 190, 208, 209	syl221anc 1337	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
211		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
212	211	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23
213	212	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . 22
214		ovex 6678	. . . . . . . . . . . . . . . . . . . . . 22
215	213, 87, 214	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . 21
216	180, 215	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
217	216	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
218		seqp1 12816	. . . . . . . . . . . . . . . . . . . 20
219	127, 218	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
220	206	recnd 10068	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
221	169	zcnd 11483	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
222	220, 221	mulcomd 10061	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
223	217, 219, 222	3eqtr4d 2666	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
224	223	oveq1d 6665	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
225	189	zcnd 11483	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
226	221, 225	mulcomd 10061	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
227	226	oveq1d 6665	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
228	210, 224, 227	3eqtr4rd 2667	. . . . . . . . . . . . . . . 16 $/\$ $/\$
229	204, 228	eqeq12d 2637	. . . . . . . . . . . . . . 15 $/\$ $/\$
230	193, 229	sylibd 229	. . . . . . . . . . . . . 14 $/\$ $/\$
231	102	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
232		gcdcom 15235	. . . . . . . . . . . . . . . . . 18 $/\$
233	231, 188, 232	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
234	185	simprd 479	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
235	233, 234	eqtrd 2656	. . . . . . . . . . . . . . . 16 $/\$ $/\$
236		rpmul 15373	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
237	231, 157, 188, 236	syl3anc 1326	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
238	235, 237	mpan2d 710	. . . . . . . . . . . . . . 15 $/\$ $/\$
239	201	oveq2d 6666	. . . . . . . . . . . . . . . 16 $/\$ $/\$
240	239	eqeq1d 2624	. . . . . . . . . . . . . . 15 $/\$ $/\$
241	238, 240	sylibrd 249	. . . . . . . . . . . . . 14 $/\$ $/\$
242	230, 241	anim12d 586	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
243	242	an12s 843	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
244	243	ex 450	. . . . . . . . . . 11 $/\$ $/\$ $/\$
245	244	a2d 29	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
246	120, 245	syld 47	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
247	19, 32, 45, 58, 109, 246	nnind 11038	. . . . . . . 8 $/\$ $/\$
248	6, 247	mpcom 38	. . . . . . 7 $/\$ $/\$
249	5, 248	mpdan 702	. . . . . 6 $/\$
250	249	simpld 475	. . . . 5
251	3	nnnn0d 11351	. . . . . . . 8
252		zexpcl 12875	. . . . . . . 8 $/\$
253	59, 251, 252	syl2anc 693	. . . . . . 7
254	67	eleq2i 2693	. . . . . . . . 9
255	254, 152	sylan2br 493	. . . . . . . 8 $/\$
256	155	adantl 482	. . . . . . . 8 $/\$ $/\$
257	64, 255, 256	seqcl 12821	. . . . . . 7
258	253, 257	zmulcld 11488	. . . . . 6
259		mulcl 10020	. . . . . . . . 9 $/\$
260	259	adantl 482	. . . . . . . 8 $/\$ $/\$
261		mulcom 10022	. . . . . . . . 9 $/\$
262	261	adantl 482	. . . . . . . 8 $/\$ $/\$
263		mulass 10024	. . . . . . . . 9 $/\$ $/\$
264	263	adantl 482	. . . . . . . 8 $/\$ $/\$ $/\$
265		ssid 3624	. . . . . . . . 9
266	265	a1i 11	. . . . . . . 8
267		f1ocnv 6149	. . . . . . . . . . 11
268	60, 267	syl 17	. . . . . . . . . 10
269	2	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
270	59	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
271	62	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . 20 $/\$
272	271	adantrr 753	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
273	161, 272	sseldi 3601	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
274		elfzoelz 12470	. . . . . . . . . . . . . . . . . 18 ..^
275	273, 274	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
276	270, 275	zmulcld 11488	. . . . . . . . . . . . . . . 16 $/\$ $/\$
277	62	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . 20 $/\$
278	277	adantrl 752	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
279	161, 278	sseldi 3601	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
280		elfzoelz 12470	. . . . . . . . . . . . . . . . . 18 ..^
281	279, 280	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
282	270, 281	zmulcld 11488	. . . . . . . . . . . . . . . 16 $/\$ $/\$
283		moddvds 14991	. . . . . . . . . . . . . . . 16 $/\$ $/\$
284	269, 276, 282, 283	syl3anc 1326	. . . . . . . . . . . . . . 15 $/\$ $/\$
285		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
286	285	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19
287	286	oveq1d 6665	. . . . . . . . . . . . . . . . . 18
288		ovex 6678	. . . . . . . . . . . . . . . . . 18
289	287, 87, 288	fvmpt 6282	. . . . . . . . . . . . . . . . 17
290		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
291	290	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19
292	291	oveq1d 6665	. . . . . . . . . . . . . . . . . 18
293		ovex 6678	. . . . . . . . . . . . . . . . . 18
294	292, 87, 293	fvmpt 6282	. . . . . . . . . . . . . . . . 17
295	289, 294	eqeqan12d 2638	. . . . . . . . . . . . . . . 16 $/\$
296	295	adantl 482	. . . . . . . . . . . . . . 15 $/\$ $/\$
297	93	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
298	275	zcnd 11483	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
299	281	zcnd 11483	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
300	297, 298, 299	subdid 10486	. . . . . . . . . . . . . . . 16 $/\$ $/\$
301	300	breq2d 4665	. . . . . . . . . . . . . . 15 $/\$ $/\$
302	284, 296, 301	3bitr4d 300	. . . . . . . . . . . . . 14 $/\$ $/\$
303		gcdcom 15235	. . . . . . . . . . . . . . . . . 18 $/\$
304	102, 59, 303	syl2anc 693	. . . . . . . . . . . . . . . . 17
305	1	simp3d 1075	. . . . . . . . . . . . . . . . 17
306	304, 305	eqtrd 2656	. . . . . . . . . . . . . . . 16
307	306	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$
308	102	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
309	275, 281	zsubcld 11487	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
310		coprmdvds 15366	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
311	308, 270, 309, 310	syl3anc 1326	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
312	275	zred 11482	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
313	80	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
314		elfzole1 12478	. . . . . . . . . . . . . . . . . . . 20 ..^
315	273, 314	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
316		elfzolt2 12479	. . . . . . . . . . . . . . . . . . . 20 ..^
317	273, 316	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
318		modid 12695	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
319	312, 313, 315, 317, 318	syl22anc 1327	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
320	281	zred 11482	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
321		elfzole1 12478	. . . . . . . . . . . . . . . . . . . 20 ..^
322	279, 321	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
323		elfzolt2 12479	. . . . . . . . . . . . . . . . . . . 20 ..^
324	279, 323	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
325		modid 12695	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
326	320, 313, 322, 324, 325	syl22anc 1327	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
327	319, 326	eqeq12d 2637	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
328		moddvds 14991	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
329	269, 275, 281, 328	syl3anc 1326	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
330		f1of1 6136	. . . . . . . . . . . . . . . . . . 19
331	60, 330	syl 17	. . . . . . . . . . . . . . . . . 18
332		f1fveq 6519	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
333	331, 332	sylan 488	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
334	327, 329, 333	3bitr3d 298	. . . . . . . . . . . . . . . 16 $/\$ $/\$
335	311, 334	sylibd 229	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
336	307, 335	mpan2d 710	. . . . . . . . . . . . . 14 $/\$ $/\$
337	302, 336	sylbid 230	. . . . . . . . . . . . 13 $/\$ $/\$
338	337	ralrimivva 2971	. . . . . . . . . . . 12
339		dff13 6512	. . . . . . . . . . . 12 $/\$
340	162, 338, 339	sylanbrc 698	. . . . . . . . . . 11
341		ovex 6678	. . . . . . . . . . . . . . 15
342	67, 341	eqeltri 2697	. . . . . . . . . . . . . 14
343	342	f1oen 7976	. . . . . . . . . . . . 13
344	60, 343	syl 17	. . . . . . . . . . . 12
345		fzofi 12773	. . . . . . . . . . . . 13 ..^
346		ssfi 8180	. . . . . . . . . . . . 13 ..^ $/\$ ..^
347	345, 161, 346	mp2an 708	. . . . . . . . . . . 12
348		f1finf1o 8187	. . . . . . . . . . . 12 $/\$
349	344, 347, 348	sylancl 694	. . . . . . . . . . 11
350	340, 349	mpbid 222	. . . . . . . . . 10
351		f1oco 6159	. . . . . . . . . 10 $/\$
352	268, 350, 351	syl2anc 693	. . . . . . . . 9
353		f1oeq23 6130	. . . . . . . . . 10 $/\$
354	67, 67, 353	mp2an 708	. . . . . . . . 9
355	352, 354	sylib 208	. . . . . . . 8
356	255	zcnd 11483	. . . . . . . 8 $/\$
357	67	eleq2i 2693	. . . . . . . . 9
358		fvco3 6275	. . . . . . . . . . . 12 $/\$
359	162, 358	sylan 488	. . . . . . . . . . 11 $/\$
360	359	fveq2d 6195	. . . . . . . . . 10 $/\$
361	60	adantr 481	. . . . . . . . . . 11 $/\$
362	162	ffvelrnda 6359	. . . . . . . . . . 11 $/\$
363		f1ocnvfv2 6533	. . . . . . . . . . 11 $/\$
364	361, 362, 363	syl2anc 693	. . . . . . . . . 10 $/\$
365	360, 364	eqtr2d 2657	. . . . . . . . 9 $/\$
366	357, 365	sylan2br 493	. . . . . . . 8 $/\$
367	260, 262, 264, 64, 266, 355, 356, 366	seqf1o 12842	. . . . . . 7
368	367, 257	eqeltrd 2701	. . . . . 6
369		moddvds 14991	. . . . . 6 $/\$ $/\$
370	2, 258, 368, 369	syl3anc 1326	. . . . 5
371	250, 370	mpbid 222	. . . 4
372	257	zcnd 11483	. . . . . . . 8
373	372	mulid2d 10058	. . . . . . 7
374	367, 373	eqtr4d 2659	. . . . . 6
375	374	oveq2d 6666	. . . . 5
376	253	zcnd 11483	. . . . . 6
377		ax-1cn 9994	. . . . . . 7
378		subdir 10464	. . . . . . 7 $/\$ $/\$
379	377, 378	mp3an2 1412	. . . . . 6 $/\$
380	376, 372, 379	syl2anc 693	. . . . 5
381		zsubcl 11419	. . . . . . . 8 $/\$
382	253, 83, 381	sylancl 694	. . . . . . 7
383	382	zcnd 11483	. . . . . 6
384	383, 372	mulcomd 10061	. . . . 5
385	375, 380, 384	3eqtr2d 2662	. . . 4
386	371, 385	breqtrd 4679	. . 3
387	249	simprd 479	. . 3
388		coprmdvds 15366	. . . 4 $/\$ $/\$ $/\$
389	102, 257, 382, 388	syl3anc 1326	. . 3 $/\$
390	386, 387, 389	mp2and 715	. 2
391		moddvds 14991	. . . 4 $/\$ $/\$
392	83, 391	mp3an3 1413	. . 3 $/\$
393	2, 253, 392	syl2anc 693	. 2
394	390, 393	mpbird 247	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 196 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

wral 2912

crab 2916

cvv 3200

wss 3574 class class class wbr 4653

cmpt 4729

ccnv 5113

ccom 5118

wf 5884

wf1 5885

wf1o 5887

cfv 5888 (class class class)co 6650

cen 7952

cfn 7955

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

clt 10074

cle 10075

cmin 10266

cn 11020

cn0 11292

cz 11377

cuz 11687

crp 11832

cfz 12326 ..^cfzo 12465

cmo 12668

cseq 12801

cexp 12860

cdvds 14983

cgcd 15216

cphi 15469

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-rp 11833 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-dvds 14984 df-gcd 15217 df-phi 15471

This theorem is referenced by: eulerth 15488

W3C validator