eulerthlema - Intuitionistic Logic Explorer

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

Theorem eulerthlema 12162

Description: Lemma for eulerth 12165. (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 999	. . . . 5
3	2	phicld 12150	. . . 4
4		elnnuz 9502	. . . 4
5	3, 4	sylib 121	. . 3
6		eluzfz2 9967	. . 3
7	5, 6	syl 14	. 2
8		oveq2 5850	. . . . . . 7
9		oveq2 5850	. . . . . . . 8
10	9	prodeq1d 11505	. . . . . . 7
11	8, 10	oveq12d 5860	. . . . . 6
12	11	oveq1d 5857	. . . . 5
13	9	prodeq1d 11505	. . . . . 6
14	13	oveq1d 5857	. . . . 5
15	12, 14	eqeq12d 2180	. . . 4
16	15	imbi2d 229	. . 3
17		oveq2 5850	. . . . . . 7
18		oveq2 5850	. . . . . . . 8
19	18	prodeq1d 11505	. . . . . . 7
20	17, 19	oveq12d 5860	. . . . . 6
21	20	oveq1d 5857	. . . . 5
22	18	prodeq1d 11505	. . . . . 6
23	22	oveq1d 5857	. . . . 5
24	21, 23	eqeq12d 2180	. . . 4
25	24	imbi2d 229	. . 3
26		oveq2 5850	. . . . . . 7
27		oveq2 5850	. . . . . . . 8
28	27	prodeq1d 11505	. . . . . . 7
29	26, 28	oveq12d 5860	. . . . . 6
30	29	oveq1d 5857	. . . . 5
31	27	prodeq1d 11505	. . . . . 6
32	31	oveq1d 5857	. . . . 5
33	30, 32	eqeq12d 2180	. . . 4
34	33	imbi2d 229	. . 3
35		oveq2 5850	. . . . . . 7
36		oveq2 5850	. . . . . . . 8
37	36	prodeq1d 11505	. . . . . . 7
38	35, 37	oveq12d 5860	. . . . . 6
39	38	oveq1d 5857	. . . . 5
40	36	prodeq1d 11505	. . . . . 6
41	40	oveq1d 5857	. . . . 5
42	39, 41	eqeq12d 2180	. . . 4
43	42	imbi2d 229	. . 3
44	1	simp2d 1000	. . . . . . . 8
45		eulerth.2	. . . . . . . . . . . 12 ..^
46		ssrab2 3227	. . . . . . . . . . . 12 ..^ ..^
47	45, 46	eqsstri 3174	. . . . . . . . . . 11 ..^
48		fzo0ssnn0 10150	. . . . . . . . . . 11 ..^
49	47, 48	sstri 3151	. . . . . . . . . 10
50		nn0ssz 9209	. . . . . . . . . 10
51	49, 50	sstri 3151	. . . . . . . . 9
52		eulerth.4	. . . . . . . . . . 11
53		f1of 5432	. . . . . . . . . . 11
54	52, 53	syl 14	. . . . . . . . . 10
55		1nn 8868	. . . . . . . . . . . 12
56	55	a1i 9	. . . . . . . . . . 11
57	3	nnge1d 8900	. . . . . . . . . . 11
58		elfz1b 10025	. . . . . . . . . . 11 $/\$ $/\$
59	56, 3, 57, 58	syl3anbrc 1171	. . . . . . . . . 10
60	54, 59	ffvelrnd 5621	. . . . . . . . 9
61	51, 60	sselid 3140	. . . . . . . 8
62	44, 61	zmulcld 9319	. . . . . . 7
63		zq 9564	. . . . . . 7
64	62, 63	syl 14	. . . . . 6
65		nnq 9571	. . . . . . 7
66	2, 65	syl 14	. . . . . 6
67	2	nngt0d 8901	. . . . . 6
68		modqabs2 10293	. . . . . 6 $/\$ $/\$
69	64, 66, 67, 68	syl3anc 1228	. . . . 5
70		1z 9217	. . . . . . 7
71	62, 2	zmodcld 10280	. . . . . . . 8
72	71	nn0cnd 9169	. . . . . . 7
73		fveq2 5486	. . . . . . . . . 10
74	73	oveq2d 5858	. . . . . . . . 9
75	74	oveq1d 5857	. . . . . . . 8
76	75	fprod1 11535	. . . . . . 7 $/\$
77	70, 72, 76	sylancr 411	. . . . . 6
78	77	oveq1d 5857	. . . . 5
79	44	zcnd 9314	. . . . . . . 8
80	79	exp1d 10583	. . . . . . 7
81		nn0sscn 9119	. . . . . . . . . 10
82	49, 81	sstri 3151	. . . . . . . . 9
83	82, 60	sselid 3140	. . . . . . . 8
84	73	fprod1 11535	. . . . . . . 8 $/\$
85	70, 83, 84	sylancr 411	. . . . . . 7
86	80, 85	oveq12d 5860	. . . . . 6
87	86	oveq1d 5857	. . . . 5
88	69, 78, 87	3eqtr4rd 2209	. . . 4
89	88	a1i 9	. . 3
90	44	adantr 274	. . . . . . . . . . . 12 $/\$ ..^
91		elfzo1 10125	. . . . . . . . . . . . . . 15 ..^ $/\$ $/\$
92	91	simp1bi 1002	. . . . . . . . . . . . . 14 ..^
93	92	adantl 275	. . . . . . . . . . . . 13 $/\$ ..^
94	93	nnnn0d 9167	. . . . . . . . . . . 12 $/\$ ..^
95		zexpcl 10470	. . . . . . . . . . . 12 $/\$
96	90, 94, 95	syl2anc 409	. . . . . . . . . . 11 $/\$ ..^
97	70	a1i 9	. . . . . . . . . . . . 13 $/\$ ..^
98	93	nnzd 9312	. . . . . . . . . . . . 13 $/\$ ..^
99	97, 98	fzfigd 10366	. . . . . . . . . . . 12 $/\$ ..^
100	54	ad2antrr 480	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
101		elfzelz 9960	. . . . . . . . . . . . . . . . . 18
102	101	zred 9313	. . . . . . . . . . . . . . . . 17
103	102	adantl 275	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
104	3	nnzd 9312	. . . . . . . . . . . . . . . . . 18
105	104	ad2antrr 480	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
106	105	zred 9313	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
107	93	nnred 8870	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
108	107	adantr 274	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
109		elfzle2 9963	. . . . . . . . . . . . . . . . . 18
110	109	adantl 275	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
111		elfzolt2 10091	. . . . . . . . . . . . . . . . . 18 ..^
112	111	ad2antlr 481	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
113	103, 108, 106, 110, 112	lelttrd 8023	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
114	103, 106, 113	ltled 8017	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
115		elfzuz 9956	. . . . . . . . . . . . . . . 16
116		elfz5 9952	. . . . . . . . . . . . . . . 16 $/\$
117	115, 105, 116	syl2an2 584	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
118	114, 117	mpbird 166	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
119	100, 118	ffvelrnd 5621	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
120	51, 119	sselid 3140	. . . . . . . . . . . 12 $/\$ ..^ $/\$
121	99, 120	fprodzcl 11550	. . . . . . . . . . 11 $/\$ ..^
122	96, 121	zmulcld 9319	. . . . . . . . . 10 $/\$ ..^
123		zq 9564	. . . . . . . . . 10
124	122, 123	syl 14	. . . . . . . . 9 $/\$ ..^
125	124	adantr 274	. . . . . . . 8 $/\$ ..^ $/\$
126	90	adantr 274	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
127	126, 120	zmulcld 9319	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
128	2	ad2antrr 480	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
129	127, 128	zmodcld 10280	. . . . . . . . . . . 12 $/\$ ..^ $/\$
130	129	nn0zd 9311	. . . . . . . . . . 11 $/\$ ..^ $/\$
131	99, 130	fprodzcl 11550	. . . . . . . . . 10 $/\$ ..^
132		zq 9564	. . . . . . . . . 10
133	131, 132	syl 14	. . . . . . . . 9 $/\$ ..^
134	133	adantr 274	. . . . . . . 8 $/\$ ..^ $/\$
135	44	ad2antrr 480	. . . . . . . . 9 $/\$ ..^ $/\$
136	54	ad2antrr 480	. . . . . . . . . . 11 $/\$ ..^ $/\$
137		fzofzp1 10162	. . . . . . . . . . . 12 ..^
138	137	ad2antlr 481	. . . . . . . . . . 11 $/\$ ..^ $/\$
139	136, 138	ffvelrnd 5621	. . . . . . . . . 10 $/\$ ..^ $/\$
140	51, 139	sselid 3140	. . . . . . . . 9 $/\$ ..^ $/\$
141	135, 140	zmulcld 9319	. . . . . . . 8 $/\$ ..^ $/\$
142	66	ad2antrr 480	. . . . . . . 8 $/\$ ..^ $/\$
143	67	ad2antrr 480	. . . . . . . 8 $/\$ ..^ $/\$
144		simpr 109	. . . . . . . 8 $/\$ ..^ $/\$
145	125, 134, 141, 142, 143, 144	modqmul1 10312	. . . . . . 7 $/\$ ..^ $/\$
146	145	ex 114	. . . . . 6 $/\$ ..^
147	96	zcnd 9314	. . . . . . . . . 10 $/\$ ..^
148	121	zcnd 9314	. . . . . . . . . 10 $/\$ ..^
149	79	adantr 274	. . . . . . . . . 10 $/\$ ..^
150	54	adantr 274	. . . . . . . . . . . 12 $/\$ ..^
151	137	adantl 275	. . . . . . . . . . . 12 $/\$ ..^
152	150, 151	ffvelrnd 5621	. . . . . . . . . . 11 $/\$ ..^
153	82, 152	sselid 3140	. . . . . . . . . 10 $/\$ ..^
154	147, 148, 149, 153	mul4d 8053	. . . . . . . . 9 $/\$ ..^
155	149, 94	expp1d 10589	. . . . . . . . . 10 $/\$ ..^
156		elfzouz 10086	. . . . . . . . . . . 12 ..^
157	156	adantl 275	. . . . . . . . . . 11 $/\$ ..^
158	150	adantr 274	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
159		elfzelz 9960	. . . . . . . . . . . . . . . . 17
160	159	zred 9313	. . . . . . . . . . . . . . . 16
161	160	adantl 275	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
162		peano2re 8034	. . . . . . . . . . . . . . . . 17
163	107, 162	syl 14	. . . . . . . . . . . . . . . 16 $/\$ ..^
164	163	adantr 274	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
165	104	ad2antrr 480	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
166	165	zred 9313	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
167		elfzle2 9963	. . . . . . . . . . . . . . . 16
168	167	adantl 275	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
169	137	ad2antlr 481	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
170		elfzle2 9963	. . . . . . . . . . . . . . . 16
171	169, 170	syl 14	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
172	161, 164, 166, 168, 171	letrd 8022	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
173		elfzuz 9956	. . . . . . . . . . . . . . 15
174	173, 165, 116	syl2an2 584	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
175	172, 174	mpbird 166	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
176	158, 175	ffvelrnd 5621	. . . . . . . . . . . 12 $/\$ ..^ $/\$
177	82, 176	sselid 3140	. . . . . . . . . . 11 $/\$ ..^ $/\$
178		fveq2 5486	. . . . . . . . . . 11
179	157, 177, 178	fprodp1 11541	. . . . . . . . . 10 $/\$ ..^
180	155, 179	oveq12d 5860	. . . . . . . . 9 $/\$ ..^
181	154, 180	eqtr4d 2201	. . . . . . . 8 $/\$ ..^
182	181	oveq1d 5857	. . . . . . 7 $/\$ ..^
183	51, 152	sselid 3140	. . . . . . . . . . . . 13 $/\$ ..^
184	90, 183	zmulcld 9319	. . . . . . . . . . . 12 $/\$ ..^
185	2	adantr 274	. . . . . . . . . . . 12 $/\$ ..^
186	184, 185	zmodcld 10280	. . . . . . . . . . 11 $/\$ ..^
187	186	nn0zd 9311	. . . . . . . . . 10 $/\$ ..^
188		zq 9564	. . . . . . . . . 10
189	187, 188	syl 14	. . . . . . . . 9 $/\$ ..^
190		zq 9564	. . . . . . . . . 10
191	184, 190	syl 14	. . . . . . . . 9 $/\$ ..^
192	66	adantr 274	. . . . . . . . 9 $/\$ ..^
193	67	adantr 274	. . . . . . . . 9 $/\$ ..^
194		modqabs2 10293	. . . . . . . . . 10 $/\$ $/\$
195	191, 192, 193, 194	syl3anc 1228	. . . . . . . . 9 $/\$ ..^
196	189, 191, 131, 192, 193, 195	modqmul1 10312	. . . . . . . 8 $/\$ ..^
197	90	adantr 274	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
198	51, 176	sselid 3140	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
199	197, 198	zmulcld 9319	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
200	185	adantr 274	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
201	199, 200	zmodcld 10280	. . . . . . . . . . . 12 $/\$ ..^ $/\$
202	201	nn0cnd 9169	. . . . . . . . . . 11 $/\$ ..^ $/\$
203	178	oveq2d 5858	. . . . . . . . . . . 12
204	203	oveq1d 5857	. . . . . . . . . . 11
205	157, 202, 204	fprodp1 11541	. . . . . . . . . 10 $/\$ ..^
206	186	nn0cnd 9169	. . . . . . . . . . 11 $/\$ ..^
207	131	zcnd 9314	. . . . . . . . . . 11 $/\$ ..^
208	206, 207	mulcomd 7920	. . . . . . . . . 10 $/\$ ..^
209	205, 208	eqtr4d 2201	. . . . . . . . 9 $/\$ ..^
210	209	oveq1d 5857	. . . . . . . 8 $/\$ ..^
211	149, 153	mulcld 7919	. . . . . . . . . 10 $/\$ ..^
212	207, 211	mulcomd 7920	. . . . . . . . 9 $/\$ ..^
213	212	oveq1d 5857	. . . . . . . 8 $/\$ ..^
214	196, 210, 213	3eqtr4rd 2209	. . . . . . 7 $/\$ ..^
215	182, 214	eqeq12d 2180	. . . . . 6 $/\$ ..^
216	146, 215	sylibd 148	. . . . 5 $/\$ ..^
217	216	expcom 115	. . . 4 ..^
218	217	a2d 26	. . 3 ..^
219	16, 25, 34, 43, 89, 218	fzind2 10174	. 2
220	7, 219	mpcom 36	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $/\$ w3a 968

wceq 1343

wcel 2136

crab 2448 class class class wbr 3982

wf 5184

wf1o 5187

cfv 5188 (class class class)co 5842

cc 7751

cr 7752

cc0 7753

c1 7754

caddc 7756

cmul 7758

clt 7933

cle 7934

cn 8857

cn0 9114

cz 9191

cuz 9466

cq 9557

cfz 9944 ..^cfzo 10077

cmo 10257

cexp 10454

cprod 11491

cgcd 11875

cphi 12141

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4097 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565 ax-cnex 7844 ax-resscn 7845 ax-1cn 7846 ax-1re 7847 ax-icn 7848 ax-addcl 7849 ax-addrcl 7850 ax-mulcl 7851 ax-mulrcl 7852 ax-addcom 7853 ax-mulcom 7854 ax-addass 7855 ax-mulass 7856 ax-distr 7857 ax-i2m1 7858 ax-0lt1 7859 ax-1rid 7860 ax-0id 7861 ax-rnegex 7862 ax-precex 7863 ax-cnre 7864 ax-pre-ltirr 7865 ax-pre-ltwlin 7866 ax-pre-lttrn 7867 ax-pre-apti 7868 ax-pre-ltadd 7869 ax-pre-mulgt0 7870 ax-pre-mulext 7871 ax-arch 7872 ax-caucvg 7873

This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-nel 2432 df-ral 2449 df-rex 2450 df-reu 2451 df-rmo 2452 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-if 3521 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-iun 3868 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-id 4271 df-po 4274 df-iso 4275 df-iord 4344 df-on 4346 df-ilim 4347 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-isom 5197 df-riota 5798 df-ov 5845 df-oprab 5846 df-mpo 5847 df-1st 6108 df-2nd 6109 df-recs 6273 df-irdg 6338 df-frec 6359 df-1o 6384 df-oadd 6388 df-er 6501 df-en 6707 df-dom 6708 df-fin 6709 df-sup 6949 df-pnf 7935 df-mnf 7936 df-xr 7937 df-ltxr 7938 df-le 7939 df-sub 8071 df-neg 8072 df-reap 8473 df-ap 8480 df-div 8569 df-inn 8858 df-2 8916 df-3 8917 df-4 8918 df-n0 9115 df-z 9192 df-uz 9467 df-q 9558 df-rp 9590 df-fz 9945 df-fzo 10078 df-fl 10205 df-mod 10258 df-seqfrec 10381 df-exp 10455 df-ihash 10689 df-cj 10784 df-re 10785 df-im 10786 df-rsqrt 10940 df-abs 10941 df-clim 11220 df-proddc 11492 df-dvds 11728 df-gcd 11876 df-phi 12143

This theorem is referenced by: eulerthlemth 12164

W3C validator