eulerthlema - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > eulerthlema		Unicode version

Theorem eulerthlema 12243

Description: Lemma for eulerth 12246. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)

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

**Assertion**
Ref	Expression
eulerthlema

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

Proof of Theorem eulerthlema Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eulerth.1	. . . . . 6 $/\$ $/\$
2	1	simp1d 1010	. . . . 5
3	2	phicld 12231	. . . 4
4		elnnuz 9577	. . . 4
5	3, 4	sylib 122	. . 3
6		eluzfz2 10045	. . 3
7	5, 6	syl 14	. 2
8		oveq2 5896	. . . . . . 7
9		oveq2 5896	. . . . . . . 8
10	9	prodeq1d 11585	. . . . . . 7
11	8, 10	oveq12d 5906	. . . . . 6
12	11	oveq1d 5903	. . . . 5
13	9	prodeq1d 11585	. . . . . 6
14	13	oveq1d 5903	. . . . 5
15	12, 14	eqeq12d 2202	. . . 4
16	15	imbi2d 230	. . 3
17		oveq2 5896	. . . . . . 7
18		oveq2 5896	. . . . . . . 8
19	18	prodeq1d 11585	. . . . . . 7
20	17, 19	oveq12d 5906	. . . . . 6
21	20	oveq1d 5903	. . . . 5
22	18	prodeq1d 11585	. . . . . 6
23	22	oveq1d 5903	. . . . 5
24	21, 23	eqeq12d 2202	. . . 4
25	24	imbi2d 230	. . 3
26		oveq2 5896	. . . . . . 7
27		oveq2 5896	. . . . . . . 8
28	27	prodeq1d 11585	. . . . . . 7
29	26, 28	oveq12d 5906	. . . . . 6
30	29	oveq1d 5903	. . . . 5
31	27	prodeq1d 11585	. . . . . 6
32	31	oveq1d 5903	. . . . 5
33	30, 32	eqeq12d 2202	. . . 4
34	33	imbi2d 230	. . 3
35		oveq2 5896	. . . . . . 7
36		oveq2 5896	. . . . . . . 8
37	36	prodeq1d 11585	. . . . . . 7
38	35, 37	oveq12d 5906	. . . . . 6
39	38	oveq1d 5903	. . . . 5
40	36	prodeq1d 11585	. . . . . 6
41	40	oveq1d 5903	. . . . 5
42	39, 41	eqeq12d 2202	. . . 4
43	42	imbi2d 230	. . 3
44	1	simp2d 1011	. . . . . . . 8
45		eulerth.2	. . . . . . . . . . . 12 ..^
46		ssrab2 3252	. . . . . . . . . . . 12 ..^ ..^
47	45, 46	eqsstri 3199	. . . . . . . . . . 11 ..^
48		fzo0ssnn0 10228	. . . . . . . . . . 11 ..^
49	47, 48	sstri 3176	. . . . . . . . . 10
50		nn0ssz 9284	. . . . . . . . . 10
51	49, 50	sstri 3176	. . . . . . . . 9
52		eulerth.4	. . . . . . . . . . 11
53		f1of 5473	. . . . . . . . . . 11
54	52, 53	syl 14	. . . . . . . . . 10
55		1nn 8943	. . . . . . . . . . . 12
56	55	a1i 9	. . . . . . . . . . 11
57	3	nnge1d 8975	. . . . . . . . . . 11
58		elfz1b 10103	. . . . . . . . . . 11 $/\$ $/\$
59	56, 3, 57, 58	syl3anbrc 1182	. . . . . . . . . 10
60	54, 59	ffvelcdmd 5665	. . . . . . . . 9
61	51, 60	sselid 3165	. . . . . . . 8
62	44, 61	zmulcld 9394	. . . . . . 7
63		zq 9639	. . . . . . 7
64	62, 63	syl 14	. . . . . 6
65		nnq 9646	. . . . . . 7
66	2, 65	syl 14	. . . . . 6
67	2	nngt0d 8976	. . . . . 6
68		modqabs2 10371	. . . . . 6 $/\$ $/\$
69	64, 66, 67, 68	syl3anc 1248	. . . . 5
70		1z 9292	. . . . . . 7
71	62, 2	zmodcld 10358	. . . . . . . 8
72	71	nn0cnd 9244	. . . . . . 7
73		fveq2 5527	. . . . . . . . . 10
74	73	oveq2d 5904	. . . . . . . . 9
75	74	oveq1d 5903	. . . . . . . 8
76	75	fprod1 11615	. . . . . . 7 $/\$
77	70, 72, 76	sylancr 414	. . . . . 6
78	77	oveq1d 5903	. . . . 5
79	44	zcnd 9389	. . . . . . . 8
80	79	exp1d 10662	. . . . . . 7
81		nn0sscn 9194	. . . . . . . . . 10
82	49, 81	sstri 3176	. . . . . . . . 9
83	82, 60	sselid 3165	. . . . . . . 8
84	73	fprod1 11615	. . . . . . . 8 $/\$
85	70, 83, 84	sylancr 414	. . . . . . 7
86	80, 85	oveq12d 5906	. . . . . 6
87	86	oveq1d 5903	. . . . 5
88	69, 78, 87	3eqtr4rd 2231	. . . 4
89	88	a1i 9	. . 3
90	44	adantr 276	. . . . . . . . . . . 12 $/\$ ..^
91		elfzo1 10203	. . . . . . . . . . . . . . 15 ..^ $/\$ $/\$
92	91	simp1bi 1013	. . . . . . . . . . . . . 14 ..^
93	92	adantl 277	. . . . . . . . . . . . 13 $/\$ ..^
94	93	nnnn0d 9242	. . . . . . . . . . . 12 $/\$ ..^
95		zexpcl 10548	. . . . . . . . . . . 12 $/\$
96	90, 94, 95	syl2anc 411	. . . . . . . . . . 11 $/\$ ..^
97	70	a1i 9	. . . . . . . . . . . . 13 $/\$ ..^
98	93	nnzd 9387	. . . . . . . . . . . . 13 $/\$ ..^
99	97, 98	fzfigd 10444	. . . . . . . . . . . 12 $/\$ ..^
100	54	ad2antrr 488	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
101		elfzelz 10038	. . . . . . . . . . . . . . . . . 18
102	101	zred 9388	. . . . . . . . . . . . . . . . 17
103	102	adantl 277	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
104	3	nnzd 9387	. . . . . . . . . . . . . . . . . 18
105	104	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
106	105	zred 9388	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
107	93	nnred 8945	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
108	107	adantr 276	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
109		elfzle2 10041	. . . . . . . . . . . . . . . . . 18
110	109	adantl 277	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
111		elfzolt2 10169	. . . . . . . . . . . . . . . . . 18 ..^
112	111	ad2antlr 489	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
113	103, 108, 106, 110, 112	lelttrd 8095	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
114	103, 106, 113	ltled 8089	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
115		elfzuz 10034	. . . . . . . . . . . . . . . 16
116		elfz5 10030	. . . . . . . . . . . . . . . 16 $/\$
117	115, 105, 116	syl2an2 594	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
118	114, 117	mpbird 167	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
119	100, 118	ffvelcdmd 5665	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
120	51, 119	sselid 3165	. . . . . . . . . . . 12 $/\$ ..^ $/\$
121	99, 120	fprodzcl 11630	. . . . . . . . . . 11 $/\$ ..^
122	96, 121	zmulcld 9394	. . . . . . . . . 10 $/\$ ..^
123		zq 9639	. . . . . . . . . 10
124	122, 123	syl 14	. . . . . . . . 9 $/\$ ..^
125	124	adantr 276	. . . . . . . 8 $/\$ ..^ $/\$
126	90	adantr 276	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
127	126, 120	zmulcld 9394	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
128	2	ad2antrr 488	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
129	127, 128	zmodcld 10358	. . . . . . . . . . . 12 $/\$ ..^ $/\$
130	129	nn0zd 9386	. . . . . . . . . . 11 $/\$ ..^ $/\$
131	99, 130	fprodzcl 11630	. . . . . . . . . 10 $/\$ ..^
132		zq 9639	. . . . . . . . . 10
133	131, 132	syl 14	. . . . . . . . 9 $/\$ ..^
134	133	adantr 276	. . . . . . . 8 $/\$ ..^ $/\$
135	44	ad2antrr 488	. . . . . . . . 9 $/\$ ..^ $/\$
136	54	ad2antrr 488	. . . . . . . . . . 11 $/\$ ..^ $/\$
137		fzofzp1 10240	. . . . . . . . . . . 12 ..^
138	137	ad2antlr 489	. . . . . . . . . . 11 $/\$ ..^ $/\$
139	136, 138	ffvelcdmd 5665	. . . . . . . . . 10 $/\$ ..^ $/\$
140	51, 139	sselid 3165	. . . . . . . . 9 $/\$ ..^ $/\$
141	135, 140	zmulcld 9394	. . . . . . . 8 $/\$ ..^ $/\$
142	66	ad2antrr 488	. . . . . . . 8 $/\$ ..^ $/\$
143	67	ad2antrr 488	. . . . . . . 8 $/\$ ..^ $/\$
144		simpr 110	. . . . . . . 8 $/\$ ..^ $/\$
145	125, 134, 141, 142, 143, 144	modqmul1 10390	. . . . . . 7 $/\$ ..^ $/\$
146	145	ex 115	. . . . . 6 $/\$ ..^
147	96	zcnd 9389	. . . . . . . . . 10 $/\$ ..^
148	121	zcnd 9389	. . . . . . . . . 10 $/\$ ..^
149	79	adantr 276	. . . . . . . . . 10 $/\$ ..^
150	54	adantr 276	. . . . . . . . . . . 12 $/\$ ..^
151	137	adantl 277	. . . . . . . . . . . 12 $/\$ ..^
152	150, 151	ffvelcdmd 5665	. . . . . . . . . . 11 $/\$ ..^
153	82, 152	sselid 3165	. . . . . . . . . 10 $/\$ ..^
154	147, 148, 149, 153	mul4d 8125	. . . . . . . . 9 $/\$ ..^
155	149, 94	expp1d 10668	. . . . . . . . . 10 $/\$ ..^
156		elfzouz 10164	. . . . . . . . . . . 12 ..^
157	156	adantl 277	. . . . . . . . . . 11 $/\$ ..^
158	150	adantr 276	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
159		elfzelz 10038	. . . . . . . . . . . . . . . . 17
160	159	zred 9388	. . . . . . . . . . . . . . . 16
161	160	adantl 277	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
162		peano2re 8106	. . . . . . . . . . . . . . . . 17
163	107, 162	syl 14	. . . . . . . . . . . . . . . 16 $/\$ ..^
164	163	adantr 276	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
165	104	ad2antrr 488	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
166	165	zred 9388	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
167		elfzle2 10041	. . . . . . . . . . . . . . . 16
168	167	adantl 277	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
169	137	ad2antlr 489	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
170		elfzle2 10041	. . . . . . . . . . . . . . . 16
171	169, 170	syl 14	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
172	161, 164, 166, 168, 171	letrd 8094	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
173		elfzuz 10034	. . . . . . . . . . . . . . 15
174	173, 165, 116	syl2an2 594	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
175	172, 174	mpbird 167	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
176	158, 175	ffvelcdmd 5665	. . . . . . . . . . . 12 $/\$ ..^ $/\$
177	82, 176	sselid 3165	. . . . . . . . . . 11 $/\$ ..^ $/\$
178		fveq2 5527	. . . . . . . . . . 11
179	157, 177, 178	fprodp1 11621	. . . . . . . . . 10 $/\$ ..^
180	155, 179	oveq12d 5906	. . . . . . . . 9 $/\$ ..^
181	154, 180	eqtr4d 2223	. . . . . . . 8 $/\$ ..^
182	181	oveq1d 5903	. . . . . . 7 $/\$ ..^
183	51, 152	sselid 3165	. . . . . . . . . . . . 13 $/\$ ..^
184	90, 183	zmulcld 9394	. . . . . . . . . . . 12 $/\$ ..^
185	2	adantr 276	. . . . . . . . . . . 12 $/\$ ..^
186	184, 185	zmodcld 10358	. . . . . . . . . . 11 $/\$ ..^
187	186	nn0zd 9386	. . . . . . . . . 10 $/\$ ..^
188		zq 9639	. . . . . . . . . 10
189	187, 188	syl 14	. . . . . . . . 9 $/\$ ..^
190		zq 9639	. . . . . . . . . 10
191	184, 190	syl 14	. . . . . . . . 9 $/\$ ..^
192	66	adantr 276	. . . . . . . . 9 $/\$ ..^
193	67	adantr 276	. . . . . . . . 9 $/\$ ..^
194		modqabs2 10371	. . . . . . . . . 10 $/\$ $/\$
195	191, 192, 193, 194	syl3anc 1248	. . . . . . . . 9 $/\$ ..^
196	189, 191, 131, 192, 193, 195	modqmul1 10390	. . . . . . . 8 $/\$ ..^
197	90	adantr 276	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
198	51, 176	sselid 3165	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
199	197, 198	zmulcld 9394	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
200	185	adantr 276	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
201	199, 200	zmodcld 10358	. . . . . . . . . . . 12 $/\$ ..^ $/\$
202	201	nn0cnd 9244	. . . . . . . . . . 11 $/\$ ..^ $/\$
203	178	oveq2d 5904	. . . . . . . . . . . 12
204	203	oveq1d 5903	. . . . . . . . . . 11
205	157, 202, 204	fprodp1 11621	. . . . . . . . . 10 $/\$ ..^
206	186	nn0cnd 9244	. . . . . . . . . . 11 $/\$ ..^
207	131	zcnd 9389	. . . . . . . . . . 11 $/\$ ..^
208	206, 207	mulcomd 7992	. . . . . . . . . 10 $/\$ ..^
209	205, 208	eqtr4d 2223	. . . . . . . . 9 $/\$ ..^
210	209	oveq1d 5903	. . . . . . . 8 $/\$ ..^
211	149, 153	mulcld 7991	. . . . . . . . . 10 $/\$ ..^
212	207, 211	mulcomd 7992	. . . . . . . . 9 $/\$ ..^
213	212	oveq1d 5903	. . . . . . . 8 $/\$ ..^
214	196, 210, 213	3eqtr4rd 2231	. . . . . . 7 $/\$ ..^
215	182, 214	eqeq12d 2202	. . . . . 6 $/\$ ..^
216	146, 215	sylibd 149	. . . . 5 $/\$ ..^
217	216	expcom 116	. . . 4 ..^
218	217	a2d 26	. . 3 ..^
219	16, 25, 34, 43, 89, 218	fzind2 10252	. 2
220	7, 219	mpcom 36	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 979

wceq 1363

wcel 2158

crab 2469 class class class wbr 4015

wf 5224

wf1o 5227

cfv 5228 (class class class)co 5888

cc 7822

cr 7823

cc0 7824

c1 7825

caddc 7827

cmul 7829

clt 8005

cle 8006

cn 8932

cn0 9189

cz 9266

cuz 9541

cq 9632

cfz 10021 ..^cfzo 10155

cmo 10335

cexp 10532

cprod 11571

cgcd 11956

cphi 12222

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2160 ax-14 2161 ax-ext 2169 ax-coll 4130 ax-sep 4133 ax-nul 4141 ax-pow 4186 ax-pr 4221 ax-un 4445 ax-setind 4548 ax-iinf 4599 ax-cnex 7915 ax-resscn 7916 ax-1cn 7917 ax-1re 7918 ax-icn 7919 ax-addcl 7920 ax-addrcl 7921 ax-mulcl 7922 ax-mulrcl 7923 ax-addcom 7924 ax-mulcom 7925 ax-addass 7926 ax-mulass 7927 ax-distr 7928 ax-i2m1 7929 ax-0lt1 7930 ax-1rid 7931 ax-0id 7932 ax-rnegex 7933 ax-precex 7934 ax-cnre 7935 ax-pre-ltirr 7936 ax-pre-ltwlin 7937 ax-pre-lttrn 7938 ax-pre-apti 7939 ax-pre-ltadd 7940 ax-pre-mulgt0 7941 ax-pre-mulext 7942 ax-arch 7943 ax-caucvg 7944

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 980 df-3an 981 df-tru 1366 df-fal 1369 df-nf 1471 df-sb 1773 df-eu 2039 df-mo 2040 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ne 2358 df-nel 2453 df-ral 2470 df-rex 2471 df-reu 2472 df-rmo 2473 df-rab 2474 df-v 2751 df-sbc 2975 df-csb 3070 df-dif 3143 df-un 3145 df-in 3147 df-ss 3154 df-nul 3435 df-if 3547 df-pw 3589 df-sn 3610 df-pr 3611 df-op 3613 df-uni 3822 df-int 3857 df-iun 3900 df-br 4016 df-opab 4077 df-mpt 4078 df-tr 4114 df-id 4305 df-po 4308 df-iso 4309 df-iord 4378 df-on 4380 df-ilim 4381 df-suc 4383 df-iom 4602 df-xp 4644 df-rel 4645 df-cnv 4646 df-co 4647 df-dm 4648 df-rn 4649 df-res 4650 df-ima 4651 df-iota 5190 df-fun 5230 df-fn 5231 df-f 5232 df-f1 5233 df-fo 5234 df-f1o 5235 df-fv 5236 df-isom 5237 df-riota 5844 df-ov 5891 df-oprab 5892 df-mpo 5893 df-1st 6154 df-2nd 6155 df-recs 6319 df-irdg 6384 df-frec 6405 df-1o 6430 df-oadd 6434 df-er 6548 df-en 6754 df-dom 6755 df-fin 6756 df-sup 6996 df-pnf 8007 df-mnf 8008 df-xr 8009 df-ltxr 8010 df-le 8011 df-sub 8143 df-neg 8144 df-reap 8545 df-ap 8552 df-div 8643 df-inn 8933 df-2 8991 df-3 8992 df-4 8993 df-n0 9190 df-z 9267 df-uz 9542 df-q 9633 df-rp 9667 df-fz 10022 df-fzo 10156 df-fl 10283 df-mod 10336 df-seqfrec 10459 df-exp 10533 df-ihash 10769 df-cj 10864 df-re 10865 df-im 10866 df-rsqrt 11020 df-abs 11021 df-clim 11300 df-proddc 11572 df-dvds 11808 df-gcd 11957 df-phi 12224

This theorem is referenced by: eulerthlemth 12245

W3C validator