eulerthlemth - Intuitionistic Logic Explorer

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

Theorem eulerthlemth 12720

Description: Lemma for eulerth 12721. The result. (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
eulerthlemth

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem eulerthlemth Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eulerth.1	. . . . . 6 $/\$ $/\$
2		eulerth.2	. . . . . 6 ..^
3		eulerth.4	. . . . . 6
4	1, 2, 3	eulerthlema 12718	. . . . 5
5	1	simp1d 1014	. . . . . 6
6	1	simp2d 1015	. . . . . . . 8
7	5	phicld 12706	. . . . . . . . 9
8	7	nnnn0d 9390	. . . . . . . 8
9		zexpcl 10743	. . . . . . . 8 $/\$
10	6, 8, 9	syl2anc 411	. . . . . . 7
11		1zzd 9441	. . . . . . . . 9
12	7	nnzd 9536	. . . . . . . . 9
13	11, 12	fzfigd 10620	. . . . . . . 8
14		ssrab2 3289	. . . . . . . . . . 11 ..^ ..^
15	2, 14	eqsstri 3236	. . . . . . . . . 10 ..^
16		fzo0ssnn0 10388	. . . . . . . . . . 11 ..^
17		nn0ssz 9432	. . . . . . . . . . 11
18	16, 17	sstri 3213	. . . . . . . . . 10 ..^
19	15, 18	sstri 3213	. . . . . . . . 9
20		f1of 5548	. . . . . . . . . . 11
21	3, 20	syl 14	. . . . . . . . . 10
22	21	ffvelcdmda 5743	. . . . . . . . 9 $/\$
23	19, 22	sselid 3202	. . . . . . . 8 $/\$
24	13, 23	fprodzcl 12086	. . . . . . 7
25	10, 24	zmulcld 9543	. . . . . 6
26		fveq2 5603	. . . . . . . . 9
27		eqid 2209	. . . . . . . . . 10
28	1, 2, 3, 27	eulerthlemh 12719	. . . . . . . . 9
29		eqid 2209	. . . . . . . . . . . . 13
30		fveq2 5603	. . . . . . . . . . . . . . . 16
31	30	oveq2d 5990	. . . . . . . . . . . . . . 15
32	31	oveq1d 5989	. . . . . . . . . . . . . 14
33	32	cbvmptv 4159	. . . . . . . . . . . . 13
34	1, 2, 29, 3, 33	eulerthlem1 12715	. . . . . . . . . . . 12
35		fveq2 5603	. . . . . . . . . . . . . . . 16
36	35	oveq2d 5990	. . . . . . . . . . . . . . 15
37	36	oveq1d 5989	. . . . . . . . . . . . . 14
38	37	cbvmptv 4159	. . . . . . . . . . . . 13
39	38	feq1i 5442	. . . . . . . . . . . 12
40	34, 39	sylib 122	. . . . . . . . . . 11
41		fvco3 5678	. . . . . . . . . . 11 $/\$
42	40, 41	sylan 283	. . . . . . . . . 10 $/\$
43		eqid 2209	. . . . . . . . . . . 12
44		fveq2 5603	. . . . . . . . . . . . . 14
45	44	oveq2d 5990	. . . . . . . . . . . . 13
46	45	oveq1d 5989	. . . . . . . . . . . 12
47		simpr 110	. . . . . . . . . . . 12 $/\$
48	6	adantr 276	. . . . . . . . . . . . . 14 $/\$
49	48, 23	zmulcld 9543	. . . . . . . . . . . . 13 $/\$
50	5	adantr 276	. . . . . . . . . . . . 13 $/\$
51		zmodfzo 10536	. . . . . . . . . . . . 13 $/\$ ..^
52	49, 50, 51	syl2anc 411	. . . . . . . . . . . 12 $/\$ ..^
53	43, 46, 47, 52	fvmptd3 5701	. . . . . . . . . . 11 $/\$
54	53	fveq2d 5607	. . . . . . . . . 10 $/\$
55	42, 54	eqtrd 2242	. . . . . . . . 9 $/\$
56	21	ffvelcdmda 5743	. . . . . . . . . . 11 $/\$
57	19, 56	sselid 3202	. . . . . . . . . 10 $/\$
58	57	zcnd 9538	. . . . . . . . 9 $/\$
59	26, 13, 28, 55, 58	fprodf1o 12065	. . . . . . . 8
60	3	adantr 276	. . . . . . . . . 10 $/\$
61		modgcd 12478	. . . . . . . . . . . . 13 $/\$
62	49, 50, 61	syl2anc 411	. . . . . . . . . . . 12 $/\$
63	50	nnzd 9536	. . . . . . . . . . . . 13 $/\$
64	63, 49	gcdcomd 12461	. . . . . . . . . . . 12 $/\$
65	5	nnzd 9536	. . . . . . . . . . . . . . . 16
66	6, 65	gcdcomd 12461	. . . . . . . . . . . . . . 15
67	1	simp3d 1016	. . . . . . . . . . . . . . 15
68	66, 67	eqtr3d 2244	. . . . . . . . . . . . . 14
69	68	adantr 276	. . . . . . . . . . . . 13 $/\$
70	23, 63	gcdcomd 12461	. . . . . . . . . . . . . 14 $/\$
71		oveq1 5981	. . . . . . . . . . . . . . . . . 18
72	71	eqeq1d 2218	. . . . . . . . . . . . . . . . 17
73	72, 2	elrab2 2942	. . . . . . . . . . . . . . . 16 ..^ $/\$
74	22, 73	sylib 122	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
75	74	simprd 114	. . . . . . . . . . . . . 14 $/\$
76	70, 75	eqtr3d 2244	. . . . . . . . . . . . 13 $/\$
77		rpmul 12586	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
78	63, 48, 23, 77	syl3anc 1252	. . . . . . . . . . . . 13 $/\$ $/\$
79	69, 76, 78	mp2and 433	. . . . . . . . . . . 12 $/\$
80	62, 64, 79	3eqtr2d 2248	. . . . . . . . . . 11 $/\$
81		oveq1 5981	. . . . . . . . . . . . 13
82	81	eqeq1d 2218	. . . . . . . . . . . 12
83	82, 2	elrab2 2942	. . . . . . . . . . 11 ..^ $/\$
84	52, 80, 83	sylanbrc 417	. . . . . . . . . 10 $/\$
85		f1ocnvfv2 5875	. . . . . . . . . 10 $/\$
86	60, 84, 85	syl2anc 411	. . . . . . . . 9 $/\$
87	86	prodeq2dv 12043	. . . . . . . 8
88	59, 87	eqtr2d 2243	. . . . . . 7
89		fveq2 5603	. . . . . . . . 9
90	89	cbvprodv 12036	. . . . . . . 8
91	90, 24	eqeltrid 2296	. . . . . . 7
92	88, 91	eqeltrd 2286	. . . . . 6
93		moddvds 12276	. . . . . 6 $/\$ $/\$
94	5, 25, 92, 93	syl3anc 1252	. . . . 5
95	4, 94	mpbid 147	. . . 4
96	24	zcnd 9538	. . . . . . . 8
97	96	mulid2d 8133	. . . . . . 7
98	90, 88, 97	3eqtr4a 2268	. . . . . 6
99	98	oveq2d 5990	. . . . 5
100	10	zcnd 9538	. . . . . 6
101		ax-1cn 8060	. . . . . . 7
102		subdir 8500	. . . . . . 7 $/\$ $/\$
103	101, 102	mp3an2 1340	. . . . . 6 $/\$
104	100, 96, 103	syl2anc 411	. . . . 5
105	10, 11	zsubcld 9542	. . . . . . 7
106	105	zcnd 9538	. . . . . 6
107	106, 96	mulcomd 8136	. . . . 5
108	99, 104, 107	3eqtr2d 2248	. . . 4
109	95, 108	breqtrd 4088	. . 3
110	1, 2, 3	eulerthlemrprm 12717	. . 3
111		coprmdvds 12580	. . . 4 $/\$ $/\$ $/\$
112	65, 24, 105, 111	syl3anc 1252	. . 3 $/\$
113	109, 110, 112	mp2and 433	. 2
114		1z 9440	. . . 4
115		moddvds 12276	. . . 4 $/\$ $/\$
116	114, 115	mp3an3 1341	. . 3 $/\$
117	5, 10, 116	syl2anc 411	. 2
118	113, 117	mpbird 167	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 983

wceq 1375

wcel 2180

crab 2492 class class class wbr 4062

cmpt 4124

ccnv 4695

ccom 4700

wf 5290

wf1o 5293

cfv 5294 (class class class)co 5974

cc 7965

cc0 7967

c1 7968

cmul 7972

cmin 8285

cn 9078

cn0 9337

cz 9414

cfz 10172 ..^cfzo 10306

cmo 10511

cexp 10727

cprod 12027

cdvds 12264

cgcd 12440

cphi 12697

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 617 ax-in2 618 ax-io 713 ax-5 1473 ax-7 1474 ax-gen 1475 ax-ie1 1519 ax-ie2 1520 ax-8 1530 ax-10 1531 ax-11 1532 ax-i12 1533 ax-bndl 1535 ax-4 1536 ax-17 1552 ax-i9 1556 ax-ial 1560 ax-i5r 1561 ax-13 2182 ax-14 2183 ax-ext 2191 ax-coll 4178 ax-sep 4181 ax-nul 4189 ax-pow 4237 ax-pr 4272 ax-un 4501 ax-setind 4606 ax-iinf 4657 ax-cnex 8058 ax-resscn 8059 ax-1cn 8060 ax-1re 8061 ax-icn 8062 ax-addcl 8063 ax-addrcl 8064 ax-mulcl 8065 ax-mulrcl 8066 ax-addcom 8067 ax-mulcom 8068 ax-addass 8069 ax-mulass 8070 ax-distr 8071 ax-i2m1 8072 ax-0lt1 8073 ax-1rid 8074 ax-0id 8075 ax-rnegex 8076 ax-precex 8077 ax-cnre 8078 ax-pre-ltirr 8079 ax-pre-ltwlin 8080 ax-pre-lttrn 8081 ax-pre-apti 8082 ax-pre-ltadd 8083 ax-pre-mulgt0 8084 ax-pre-mulext 8085 ax-arch 8086 ax-caucvg 8087

This theorem depends on definitions: df-bi 117 df-stab 835 df-dc 839 df-3or 984 df-3an 985 df-tru 1378 df-fal 1381 df-nf 1487 df-sb 1789 df-eu 2060 df-mo 2061 df-clab 2196 df-cleq 2202 df-clel 2205 df-nfc 2341 df-ne 2381 df-nel 2476 df-ral 2493 df-rex 2494 df-reu 2495 df-rmo 2496 df-rab 2497 df-v 2781 df-sbc 3009 df-csb 3105 df-dif 3179 df-un 3181 df-in 3183 df-ss 3190 df-nul 3472 df-if 3583 df-pw 3631 df-sn 3652 df-pr 3653 df-op 3655 df-uni 3868 df-int 3903 df-iun 3946 df-br 4063 df-opab 4125 df-mpt 4126 df-tr 4162 df-id 4361 df-po 4364 df-iso 4365 df-iord 4434 df-on 4436 df-ilim 4437 df-suc 4439 df-iom 4660 df-xp 4702 df-rel 4703 df-cnv 4704 df-co 4705 df-dm 4706 df-rn 4707 df-res 4708 df-ima 4709 df-iota 5254 df-fun 5296 df-fn 5297 df-f 5298 df-f1 5299 df-fo 5300 df-f1o 5301 df-fv 5302 df-isom 5303 df-riota 5927 df-ov 5977 df-oprab 5978 df-mpo 5979 df-1st 6256 df-2nd 6257 df-recs 6421 df-irdg 6486 df-frec 6507 df-1o 6532 df-oadd 6536 df-er 6650 df-en 6858 df-dom 6859 df-fin 6860 df-sup 7119 df-pnf 8151 df-mnf 8152 df-xr 8153 df-ltxr 8154 df-le 8155 df-sub 8287 df-neg 8288 df-reap 8690 df-ap 8697 df-div 8788 df-inn 9079 df-2 9137 df-3 9138 df-4 9139 df-n0 9338 df-z 9415 df-uz 9691 df-q 9783 df-rp 9818 df-fz 10173 df-fzo 10307 df-fl 10457 df-mod 10512 df-seqfrec 10637 df-exp 10728 df-ihash 10965 df-cj 11319 df-re 11320 df-im 11321 df-rsqrt 11475 df-abs 11476 df-clim 11756 df-proddc 12028 df-dvds 12265 df-gcd 12441 df-phi 12699

This theorem is referenced by: eulerth 12721

W3C validator