eulerthlema - Intuitionistic Logic Explorer

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

Theorem eulerthlema 12184

Description: Lemma for eulerth 12187. (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 1004	. . . . 5
3	2	phicld 12172	. . . 4
4		elnnuz 9523	. . . 4
5	3, 4	sylib 121	. . 3
6		eluzfz2 9988	. . 3
7	5, 6	syl 14	. 2
8		oveq2 5861	. . . . . . 7
9		oveq2 5861	. . . . . . . 8
10	9	prodeq1d 11527	. . . . . . 7
11	8, 10	oveq12d 5871	. . . . . 6
12	11	oveq1d 5868	. . . . 5
13	9	prodeq1d 11527	. . . . . 6
14	13	oveq1d 5868	. . . . 5
15	12, 14	eqeq12d 2185	. . . 4
16	15	imbi2d 229	. . 3
17		oveq2 5861	. . . . . . 7
18		oveq2 5861	. . . . . . . 8
19	18	prodeq1d 11527	. . . . . . 7
20	17, 19	oveq12d 5871	. . . . . 6
21	20	oveq1d 5868	. . . . 5
22	18	prodeq1d 11527	. . . . . 6
23	22	oveq1d 5868	. . . . 5
24	21, 23	eqeq12d 2185	. . . 4
25	24	imbi2d 229	. . 3
26		oveq2 5861	. . . . . . 7
27		oveq2 5861	. . . . . . . 8
28	27	prodeq1d 11527	. . . . . . 7
29	26, 28	oveq12d 5871	. . . . . 6
30	29	oveq1d 5868	. . . . 5
31	27	prodeq1d 11527	. . . . . 6
32	31	oveq1d 5868	. . . . 5
33	30, 32	eqeq12d 2185	. . . 4
34	33	imbi2d 229	. . 3
35		oveq2 5861	. . . . . . 7
36		oveq2 5861	. . . . . . . 8
37	36	prodeq1d 11527	. . . . . . 7
38	35, 37	oveq12d 5871	. . . . . 6
39	38	oveq1d 5868	. . . . 5
40	36	prodeq1d 11527	. . . . . 6
41	40	oveq1d 5868	. . . . 5
42	39, 41	eqeq12d 2185	. . . 4
43	42	imbi2d 229	. . 3
44	1	simp2d 1005	. . . . . . . 8
45		eulerth.2	. . . . . . . . . . . 12 ..^
46		ssrab2 3232	. . . . . . . . . . . 12 ..^ ..^
47	45, 46	eqsstri 3179	. . . . . . . . . . 11 ..^
48		fzo0ssnn0 10171	. . . . . . . . . . 11 ..^
49	47, 48	sstri 3156	. . . . . . . . . 10
50		nn0ssz 9230	. . . . . . . . . 10
51	49, 50	sstri 3156	. . . . . . . . 9
52		eulerth.4	. . . . . . . . . . 11
53		f1of 5442	. . . . . . . . . . 11
54	52, 53	syl 14	. . . . . . . . . 10
55		1nn 8889	. . . . . . . . . . . 12
56	55	a1i 9	. . . . . . . . . . 11
57	3	nnge1d 8921	. . . . . . . . . . 11
58		elfz1b 10046	. . . . . . . . . . 11 $/\$ $/\$
59	56, 3, 57, 58	syl3anbrc 1176	. . . . . . . . . 10
60	54, 59	ffvelrnd 5632	. . . . . . . . 9
61	51, 60	sselid 3145	. . . . . . . 8
62	44, 61	zmulcld 9340	. . . . . . 7
63		zq 9585	. . . . . . 7
64	62, 63	syl 14	. . . . . 6
65		nnq 9592	. . . . . . 7
66	2, 65	syl 14	. . . . . 6
67	2	nngt0d 8922	. . . . . 6
68		modqabs2 10314	. . . . . 6 $/\$ $/\$
69	64, 66, 67, 68	syl3anc 1233	. . . . 5
70		1z 9238	. . . . . . 7
71	62, 2	zmodcld 10301	. . . . . . . 8
72	71	nn0cnd 9190	. . . . . . 7
73		fveq2 5496	. . . . . . . . . 10
74	73	oveq2d 5869	. . . . . . . . 9
75	74	oveq1d 5868	. . . . . . . 8
76	75	fprod1 11557	. . . . . . 7 $/\$
77	70, 72, 76	sylancr 412	. . . . . 6
78	77	oveq1d 5868	. . . . 5
79	44	zcnd 9335	. . . . . . . 8
80	79	exp1d 10604	. . . . . . 7
81		nn0sscn 9140	. . . . . . . . . 10
82	49, 81	sstri 3156	. . . . . . . . 9
83	82, 60	sselid 3145	. . . . . . . 8
84	73	fprod1 11557	. . . . . . . 8 $/\$
85	70, 83, 84	sylancr 412	. . . . . . 7
86	80, 85	oveq12d 5871	. . . . . 6
87	86	oveq1d 5868	. . . . 5
88	69, 78, 87	3eqtr4rd 2214	. . . 4
89	88	a1i 9	. . 3
90	44	adantr 274	. . . . . . . . . . . 12 $/\$ ..^
91		elfzo1 10146	. . . . . . . . . . . . . . 15 ..^ $/\$ $/\$
92	91	simp1bi 1007	. . . . . . . . . . . . . 14 ..^
93	92	adantl 275	. . . . . . . . . . . . 13 $/\$ ..^
94	93	nnnn0d 9188	. . . . . . . . . . . 12 $/\$ ..^
95		zexpcl 10491	. . . . . . . . . . . 12 $/\$
96	90, 94, 95	syl2anc 409	. . . . . . . . . . 11 $/\$ ..^
97	70	a1i 9	. . . . . . . . . . . . 13 $/\$ ..^
98	93	nnzd 9333	. . . . . . . . . . . . 13 $/\$ ..^
99	97, 98	fzfigd 10387	. . . . . . . . . . . 12 $/\$ ..^
100	54	ad2antrr 485	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
101		elfzelz 9981	. . . . . . . . . . . . . . . . . 18
102	101	zred 9334	. . . . . . . . . . . . . . . . 17
103	102	adantl 275	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
104	3	nnzd 9333	. . . . . . . . . . . . . . . . . 18
105	104	ad2antrr 485	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
106	105	zred 9334	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
107	93	nnred 8891	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
108	107	adantr 274	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
109		elfzle2 9984	. . . . . . . . . . . . . . . . . 18
110	109	adantl 275	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
111		elfzolt2 10112	. . . . . . . . . . . . . . . . . 18 ..^
112	111	ad2antlr 486	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
113	103, 108, 106, 110, 112	lelttrd 8044	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
114	103, 106, 113	ltled 8038	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
115		elfzuz 9977	. . . . . . . . . . . . . . . 16
116		elfz5 9973	. . . . . . . . . . . . . . . 16 $/\$
117	115, 105, 116	syl2an2 589	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
118	114, 117	mpbird 166	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
119	100, 118	ffvelrnd 5632	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
120	51, 119	sselid 3145	. . . . . . . . . . . 12 $/\$ ..^ $/\$
121	99, 120	fprodzcl 11572	. . . . . . . . . . 11 $/\$ ..^
122	96, 121	zmulcld 9340	. . . . . . . . . 10 $/\$ ..^
123		zq 9585	. . . . . . . . . 10
124	122, 123	syl 14	. . . . . . . . 9 $/\$ ..^
125	124	adantr 274	. . . . . . . 8 $/\$ ..^ $/\$
126	90	adantr 274	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
127	126, 120	zmulcld 9340	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
128	2	ad2antrr 485	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
129	127, 128	zmodcld 10301	. . . . . . . . . . . 12 $/\$ ..^ $/\$
130	129	nn0zd 9332	. . . . . . . . . . 11 $/\$ ..^ $/\$
131	99, 130	fprodzcl 11572	. . . . . . . . . 10 $/\$ ..^
132		zq 9585	. . . . . . . . . 10
133	131, 132	syl 14	. . . . . . . . 9 $/\$ ..^
134	133	adantr 274	. . . . . . . 8 $/\$ ..^ $/\$
135	44	ad2antrr 485	. . . . . . . . 9 $/\$ ..^ $/\$
136	54	ad2antrr 485	. . . . . . . . . . 11 $/\$ ..^ $/\$
137		fzofzp1 10183	. . . . . . . . . . . 12 ..^
138	137	ad2antlr 486	. . . . . . . . . . 11 $/\$ ..^ $/\$
139	136, 138	ffvelrnd 5632	. . . . . . . . . 10 $/\$ ..^ $/\$
140	51, 139	sselid 3145	. . . . . . . . 9 $/\$ ..^ $/\$
141	135, 140	zmulcld 9340	. . . . . . . 8 $/\$ ..^ $/\$
142	66	ad2antrr 485	. . . . . . . 8 $/\$ ..^ $/\$
143	67	ad2antrr 485	. . . . . . . 8 $/\$ ..^ $/\$
144		simpr 109	. . . . . . . 8 $/\$ ..^ $/\$
145	125, 134, 141, 142, 143, 144	modqmul1 10333	. . . . . . 7 $/\$ ..^ $/\$
146	145	ex 114	. . . . . 6 $/\$ ..^
147	96	zcnd 9335	. . . . . . . . . 10 $/\$ ..^
148	121	zcnd 9335	. . . . . . . . . 10 $/\$ ..^
149	79	adantr 274	. . . . . . . . . 10 $/\$ ..^
150	54	adantr 274	. . . . . . . . . . . 12 $/\$ ..^
151	137	adantl 275	. . . . . . . . . . . 12 $/\$ ..^
152	150, 151	ffvelrnd 5632	. . . . . . . . . . 11 $/\$ ..^
153	82, 152	sselid 3145	. . . . . . . . . 10 $/\$ ..^
154	147, 148, 149, 153	mul4d 8074	. . . . . . . . 9 $/\$ ..^
155	149, 94	expp1d 10610	. . . . . . . . . 10 $/\$ ..^
156		elfzouz 10107	. . . . . . . . . . . 12 ..^
157	156	adantl 275	. . . . . . . . . . 11 $/\$ ..^
158	150	adantr 274	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
159		elfzelz 9981	. . . . . . . . . . . . . . . . 17
160	159	zred 9334	. . . . . . . . . . . . . . . 16
161	160	adantl 275	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
162		peano2re 8055	. . . . . . . . . . . . . . . . 17
163	107, 162	syl 14	. . . . . . . . . . . . . . . 16 $/\$ ..^
164	163	adantr 274	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
165	104	ad2antrr 485	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
166	165	zred 9334	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
167		elfzle2 9984	. . . . . . . . . . . . . . . 16
168	167	adantl 275	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
169	137	ad2antlr 486	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
170		elfzle2 9984	. . . . . . . . . . . . . . . 16
171	169, 170	syl 14	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
172	161, 164, 166, 168, 171	letrd 8043	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
173		elfzuz 9977	. . . . . . . . . . . . . . 15
174	173, 165, 116	syl2an2 589	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
175	172, 174	mpbird 166	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
176	158, 175	ffvelrnd 5632	. . . . . . . . . . . 12 $/\$ ..^ $/\$
177	82, 176	sselid 3145	. . . . . . . . . . 11 $/\$ ..^ $/\$
178		fveq2 5496	. . . . . . . . . . 11
179	157, 177, 178	fprodp1 11563	. . . . . . . . . 10 $/\$ ..^
180	155, 179	oveq12d 5871	. . . . . . . . 9 $/\$ ..^
181	154, 180	eqtr4d 2206	. . . . . . . 8 $/\$ ..^
182	181	oveq1d 5868	. . . . . . 7 $/\$ ..^
183	51, 152	sselid 3145	. . . . . . . . . . . . 13 $/\$ ..^
184	90, 183	zmulcld 9340	. . . . . . . . . . . 12 $/\$ ..^
185	2	adantr 274	. . . . . . . . . . . 12 $/\$ ..^
186	184, 185	zmodcld 10301	. . . . . . . . . . 11 $/\$ ..^
187	186	nn0zd 9332	. . . . . . . . . 10 $/\$ ..^
188		zq 9585	. . . . . . . . . 10
189	187, 188	syl 14	. . . . . . . . 9 $/\$ ..^
190		zq 9585	. . . . . . . . . 10
191	184, 190	syl 14	. . . . . . . . 9 $/\$ ..^
192	66	adantr 274	. . . . . . . . 9 $/\$ ..^
193	67	adantr 274	. . . . . . . . 9 $/\$ ..^
194		modqabs2 10314	. . . . . . . . . 10 $/\$ $/\$
195	191, 192, 193, 194	syl3anc 1233	. . . . . . . . 9 $/\$ ..^
196	189, 191, 131, 192, 193, 195	modqmul1 10333	. . . . . . . 8 $/\$ ..^
197	90	adantr 274	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
198	51, 176	sselid 3145	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
199	197, 198	zmulcld 9340	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
200	185	adantr 274	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
201	199, 200	zmodcld 10301	. . . . . . . . . . . 12 $/\$ ..^ $/\$
202	201	nn0cnd 9190	. . . . . . . . . . 11 $/\$ ..^ $/\$
203	178	oveq2d 5869	. . . . . . . . . . . 12
204	203	oveq1d 5868	. . . . . . . . . . 11
205	157, 202, 204	fprodp1 11563	. . . . . . . . . 10 $/\$ ..^
206	186	nn0cnd 9190	. . . . . . . . . . 11 $/\$ ..^
207	131	zcnd 9335	. . . . . . . . . . 11 $/\$ ..^
208	206, 207	mulcomd 7941	. . . . . . . . . 10 $/\$ ..^
209	205, 208	eqtr4d 2206	. . . . . . . . 9 $/\$ ..^
210	209	oveq1d 5868	. . . . . . . 8 $/\$ ..^
211	149, 153	mulcld 7940	. . . . . . . . . 10 $/\$ ..^
212	207, 211	mulcomd 7941	. . . . . . . . 9 $/\$ ..^
213	212	oveq1d 5868	. . . . . . . 8 $/\$ ..^
214	196, 210, 213	3eqtr4rd 2214	. . . . . . 7 $/\$ ..^
215	182, 214	eqeq12d 2185	. . . . . 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 10195	. 2
220	7, 219	mpcom 36	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $/\$ w3a 973

wceq 1348

wcel 2141

crab 2452 class class class wbr 3989

wf 5194

wf1o 5197

cfv 5198 (class class class)co 5853

cc 7772

cr 7773

cc0 7774

c1 7775

caddc 7777

cmul 7779

clt 7954

cle 7955

cn 8878

cn0 9135

cz 9212

cuz 9487

cq 9578

cfz 9965 ..^cfzo 10098

cmo 10278

cexp 10475

cprod 11513

cgcd 11897

cphi 12163

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 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4104 ax-sep 4107 ax-nul 4115 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-setind 4521 ax-iinf 4572 ax-cnex 7865 ax-resscn 7866 ax-1cn 7867 ax-1re 7868 ax-icn 7869 ax-addcl 7870 ax-addrcl 7871 ax-mulcl 7872 ax-mulrcl 7873 ax-addcom 7874 ax-mulcom 7875 ax-addass 7876 ax-mulass 7877 ax-distr 7878 ax-i2m1 7879 ax-0lt1 7880 ax-1rid 7881 ax-0id 7882 ax-rnegex 7883 ax-precex 7884 ax-cnre 7885 ax-pre-ltirr 7886 ax-pre-ltwlin 7887 ax-pre-lttrn 7888 ax-pre-apti 7889 ax-pre-ltadd 7890 ax-pre-mulgt0 7891 ax-pre-mulext 7892 ax-arch 7893 ax-caucvg 7894

This theorem depends on definitions: df-bi 116 df-dc 830 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rmo 2456 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-if 3527 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-iun 3875 df-br 3990 df-opab 4051 df-mpt 4052 df-tr 4088 df-id 4278 df-po 4281 df-iso 4282 df-iord 4351 df-on 4353 df-ilim 4354 df-suc 4356 df-iom 4575 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-f1 5203 df-fo 5204 df-f1o 5205 df-fv 5206 df-isom 5207 df-riota 5809 df-ov 5856 df-oprab 5857 df-mpo 5858 df-1st 6119 df-2nd 6120 df-recs 6284 df-irdg 6349 df-frec 6370 df-1o 6395 df-oadd 6399 df-er 6513 df-en 6719 df-dom 6720 df-fin 6721 df-sup 6961 df-pnf 7956 df-mnf 7957 df-xr 7958 df-ltxr 7959 df-le 7960 df-sub 8092 df-neg 8093 df-reap 8494 df-ap 8501 df-div 8590 df-inn 8879 df-2 8937 df-3 8938 df-4 8939 df-n0 9136 df-z 9213 df-uz 9488 df-q 9579 df-rp 9611 df-fz 9966 df-fzo 10099 df-fl 10226 df-mod 10279 df-seqfrec 10402 df-exp 10476 df-ihash 10710 df-cj 10806 df-re 10807 df-im 10808 df-rsqrt 10962 df-abs 10963 df-clim 11242 df-proddc 11514 df-dvds 11750 df-gcd 11898 df-phi 12165

This theorem is referenced by: eulerthlemth 12186

W3C validator