pockthlem - Intuitionistic Logic Explorer

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

Theorem pockthlem 12387

Description: Lemma for pockthg 12388. (Contributed by Mario Carneiro, 2-Mar-2014.)

**Hypotheses**
Ref	Expression
pockthg.1
pockthg.2
pockthg.3
pockthg.4
pockthlem.5
pockthlem.6
pockthlem.7
pockthlem.8
pockthlem.9
pockthlem.10
pockthlem.11

**Assertion**
Ref	Expression
pockthlem

**Proof of Theorem pockthlem**
Step	Hyp	Ref	Expression
1		pockthlem.7	. . . . . 6
2		prmnn 12141	. . . . . 6
3	1, 2	syl 14	. . . . 5
4		pockthlem.8	. . . . . 6
5	4	nnnn0d 9258	. . . . 5
6	3, 5	nnexpcld 10706	. . . 4
7	6	nnzd 9403	. . 3
8		pockthlem.5	. . . . . 6
9		prmnn 12141	. . . . . 6
10	8, 9	syl 14	. . . . 5
11		pockthlem.9	. . . . 5
12	10	nnzd 9403	. . . . . . . . . 10
13		gcddvds 11995	. . . . . . . . . 10 $/\$ $/\$
14	11, 12, 13	syl2anc 411	. . . . . . . . 9 $/\$
15	14	simpld 112	. . . . . . . 8
16	11, 12	gcdcld 12000	. . . . . . . . . 10
17	16	nn0zd 9402	. . . . . . . . 9
18		pockthg.4	. . . . . . . . . . . . . 14
19		pockthg.1	. . . . . . . . . . . . . . . . 17
20		pockthg.2	. . . . . . . . . . . . . . . . 17
21	19, 20	nnmulcld 8997	. . . . . . . . . . . . . . . 16
22		nnuz 9592	. . . . . . . . . . . . . . . 16
23	21, 22	eleqtrdi 2282	. . . . . . . . . . . . . . 15
24		eluzp1p1 9582	. . . . . . . . . . . . . . 15
25	23, 24	syl 14	. . . . . . . . . . . . . 14
26	18, 25	eqeltrd 2266	. . . . . . . . . . . . 13
27		df-2 9007	. . . . . . . . . . . . . 14
28	27	fveq2i 5537	. . . . . . . . . . . . 13
29	26, 28	eleqtrrdi 2283	. . . . . . . . . . . 12
30		eluz2b2 9632	. . . . . . . . . . . 12 $/\$
31	29, 30	sylib 122	. . . . . . . . . . 11 $/\$
32	31	simpld 112	. . . . . . . . . 10
33	32	nnzd 9403	. . . . . . . . 9
34	14	simprd 114	. . . . . . . . 9
35		pockthlem.6	. . . . . . . . 9
36	17, 12, 33, 34, 35	dvdstrd 11868	. . . . . . . 8
37	32	nnne0d 8993	. . . . . . . . . 10
38		simpr 110	. . . . . . . . . . 11 $/\$
39	38	necon3ai 2409	. . . . . . . . . 10 $/\$
40	37, 39	syl 14	. . . . . . . . 9 $/\$
41		dvdslegcd 11996	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
42	17, 11, 33, 40, 41	syl31anc 1252	. . . . . . . 8 $/\$
43	15, 36, 42	mp2and 433	. . . . . . 7
44		pockthlem.10	. . . . . . . . . 10
45	44	oveq1d 5910	. . . . . . . . 9
46		1z 9308	. . . . . . . . . . . . . 14
47		eluzp1m1 9580	. . . . . . . . . . . . . 14 $/\$
48	46, 26, 47	sylancr 414	. . . . . . . . . . . . 13
49	48, 22	eleqtrrdi 2283	. . . . . . . . . . . 12
50	49	nnnn0d 9258	. . . . . . . . . . 11
51		zexpcl 10565	. . . . . . . . . . 11 $/\$
52	11, 50, 51	syl2anc 411	. . . . . . . . . 10
53		modgcd 12023	. . . . . . . . . 10 $/\$
54	52, 32, 53	syl2anc 411	. . . . . . . . 9
55		gcdcom 12005	. . . . . . . . . . 11 $/\$
56	46, 33, 55	sylancr 414	. . . . . . . . . 10
57		gcd1 12019	. . . . . . . . . . 11
58	33, 57	syl 14	. . . . . . . . . 10
59	56, 58	eqtrd 2222	. . . . . . . . 9
60	45, 54, 59	3eqtr3d 2230	. . . . . . . 8
61		rpexp 12184	. . . . . . . . 9 $/\$ $/\$
62	11, 33, 49, 61	syl3anc 1249	. . . . . . . 8
63	60, 62	mpbid 147	. . . . . . 7
64	43, 63	breqtrd 4044	. . . . . 6
65	10	nnne0d 8993	. . . . . . . . 9
66		simpr 110	. . . . . . . . . 10 $/\$
67	66	necon3ai 2409	. . . . . . . . 9 $/\$
68	65, 67	syl 14	. . . . . . . 8 $/\$
69		gcdn0cl 11994	. . . . . . . 8 $/\$ $/\$ $/\$
70	11, 12, 68, 69	syl21anc 1248	. . . . . . 7
71		nnle1eq1 8972	. . . . . . 7
72	70, 71	syl 14	. . . . . 6
73	64, 72	mpbid 147	. . . . 5
74		odzcl 12274	. . . . 5 $/\$ $/\$
75	10, 11, 73, 74	syl3anc 1249	. . . 4
76	75	nnzd 9403	. . 3
77		prmuz2 12162	. . . . . . . 8
78	8, 77	syl 14	. . . . . . 7
79	78, 28	eleqtrdi 2282	. . . . . 6
80		eluzp1m1 9580	. . . . . 6 $/\$
81	46, 79, 80	sylancr 414	. . . . 5
82	81, 22	eleqtrrdi 2283	. . . 4
83	82	nnzd 9403	. . 3
84	19	nnzd 9403	. . . . . 6
85	49	nnzd 9403	. . . . . 6
86		pcdvds 12346	. . . . . . 7 $/\$
87	1, 19, 86	syl2anc 411	. . . . . 6
88	20	nnzd 9403	. . . . . . . 8
89		dvdsmul1 11851	. . . . . . . 8 $/\$
90	84, 88, 89	syl2anc 411	. . . . . . 7
91	18	oveq1d 5910	. . . . . . . 8
92	21	nncnd 8962	. . . . . . . . 9
93		ax-1cn 7933	. . . . . . . . 9
94		pncan 8192	. . . . . . . . 9 $/\$
95	92, 93, 94	sylancl 413	. . . . . . . 8
96	91, 95	eqtrd 2222	. . . . . . 7
97	90, 96	breqtrrd 4046	. . . . . 6
98	7, 84, 85, 87, 97	dvdstrd 11868	. . . . 5
99	6	nnne0d 8993	. . . . . 6
100		dvdsval2 11828	. . . . . 6 $/\$ $/\$
101	7, 99, 85, 100	syl3anc 1249	. . . . 5
102	98, 101	mpbid 147	. . . 4
103		peano2zm 9320	. . . . . . . 8
104	52, 103	syl 14	. . . . . . 7
105		nnq 9662	. . . . . . . . . . 11
106	32, 105	syl 14	. . . . . . . . . 10
107	31	simprd 114	. . . . . . . . . 10
108		q1mod 10386	. . . . . . . . . 10 $/\$
109	106, 107, 108	syl2anc 411	. . . . . . . . 9
110	44, 109	eqtr4d 2225	. . . . . . . 8
111		1zzd 9309	. . . . . . . . 9
112		moddvds 11837	. . . . . . . . 9 $/\$ $/\$
113	32, 52, 111, 112	syl3anc 1249	. . . . . . . 8
114	110, 113	mpbid 147	. . . . . . 7
115	12, 33, 104, 35, 114	dvdstrd 11868	. . . . . 6
116		odzdvds 12276	. . . . . . 7 $/\$ $/\$ $/\$
117	10, 11, 73, 50, 116	syl31anc 1252	. . . . . 6
118	115, 117	mpbid 147	. . . . 5
119	49	nncnd 8962	. . . . . 6
120	6	nncnd 8962	. . . . . 6
121	6	nnap0d 8994	. . . . . 6 #
122	119, 120, 121	divcanap1d 8777	. . . . 5
123	118, 122	breqtrrd 4046	. . . 4
124		nprmdvds1 12171	. . . . . 6
125	8, 124	syl 14	. . . . 5
126	3	nnzd 9403	. . . . . . . . . . . . 13
127		iddvdsexp 11853	. . . . . . . . . . . . . 14 $/\$
128	126, 4, 127	syl2anc 411	. . . . . . . . . . . . 13
129	126, 7, 85, 128, 98	dvdstrd 11868	. . . . . . . . . . . 12
130	3	nnne0d 8993	. . . . . . . . . . . . 13
131		dvdsval2 11828	. . . . . . . . . . . . 13 $/\$ $/\$
132	126, 130, 85, 131	syl3anc 1249	. . . . . . . . . . . 12
133	129, 132	mpbid 147	. . . . . . . . . . 11
134	50	nn0ge0d 9261	. . . . . . . . . . . 12
135	49	nnred 8961	. . . . . . . . . . . . 13
136	3	nnred 8961	. . . . . . . . . . . . 13
137	3	nngt0d 8992	. . . . . . . . . . . . 13
138		ge0div 8857	. . . . . . . . . . . . 13 $/\$ $/\$
139	135, 136, 137, 138	syl3anc 1249	. . . . . . . . . . . 12
140	134, 139	mpbid 147	. . . . . . . . . . 11
141		elnn0z 9295	. . . . . . . . . . 11 $/\$
142	133, 140, 141	sylanbrc 417	. . . . . . . . . 10
143		zexpcl 10565	. . . . . . . . . 10 $/\$
144	11, 142, 143	syl2anc 411	. . . . . . . . 9
145		peano2zm 9320	. . . . . . . . 9
146	144, 145	syl 14	. . . . . . . 8
147		dvdsgcd 12044	. . . . . . . 8 $/\$ $/\$ $/\$
148	12, 146, 33, 147	syl3anc 1249	. . . . . . 7 $/\$
149	35, 148	mpan2d 428	. . . . . 6
150		odzdvds 12276	. . . . . . . 8 $/\$ $/\$ $/\$
151	10, 11, 73, 142, 150	syl31anc 1252	. . . . . . 7
152	3	nncnd 8962	. . . . . . . . . . 11
153	3	nnap0d 8994	. . . . . . . . . . 11 #
154	4	nnzd 9403	. . . . . . . . . . 11
155	152, 153, 154	expm1apd 10694	. . . . . . . . . 10
156	155	oveq2d 5911	. . . . . . . . 9
157	135, 6	nndivred 8998	. . . . . . . . . . 11
158	157	recnd 8015	. . . . . . . . . 10
159	158, 120, 152, 153	divassapd 8812	. . . . . . . . 9
160	122	oveq1d 5910	. . . . . . . . 9
161	156, 159, 160	3eqtr2d 2228	. . . . . . . 8
162	161	breq2d 4030	. . . . . . 7
163	151, 162	bitr4d 191	. . . . . 6
164		pockthlem.11	. . . . . . 7
165	164	breq2d 4030	. . . . . 6
166	149, 163, 165	3imtr3d 202	. . . . 5
167	125, 166	mtod 664	. . . 4
168		prmpwdvds 12386	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
169	102, 76, 1, 4, 123, 167, 168	syl222anc 1265	. . 3
170		odzphi 12277	. . . . 5 $/\$ $/\$
171	10, 11, 73, 170	syl3anc 1249	. . . 4
172		phiprm 12254	. . . . 5
173	8, 172	syl 14	. . . 4
174	171, 173	breqtrd 4044	. . 3
175	7, 76, 83, 169, 174	dvdstrd 11868	. 2
176		pcdvdsb 12351	. . 3 $/\$ $/\$
177	1, 83, 5, 176	syl3anc 1249	. 2
178	175, 177	mpbird 167	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105

wceq 1364

wcel 2160

wne 2360 class class class wbr 4018

cfv 5235 (class class class)co 5895

cc 7838

cr 7839

cc0 7840

c1 7841

caddc 7843

cmul 7845

clt 8021

cle 8022

cmin 8157

cdiv 8658

cn 8948

c2 8999

cn0 9205

cz 9282

cuz 9557

cq 9648

cmo 10352

cexp 10549

cdvds 11825

cgcd 11974

cprime 12138

codz 12239

cphi 12240

cpc 12315

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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-coll 4133 ax-sep 4136 ax-nul 4144 ax-pow 4192 ax-pr 4227 ax-un 4451 ax-setind 4554 ax-iinf 4605 ax-cnex 7931 ax-resscn 7932 ax-1cn 7933 ax-1re 7934 ax-icn 7935 ax-addcl 7936 ax-addrcl 7937 ax-mulcl 7938 ax-mulrcl 7939 ax-addcom 7940 ax-mulcom 7941 ax-addass 7942 ax-mulass 7943 ax-distr 7944 ax-i2m1 7945 ax-0lt1 7946 ax-1rid 7947 ax-0id 7948 ax-rnegex 7949 ax-precex 7950 ax-cnre 7951 ax-pre-ltirr 7952 ax-pre-ltwlin 7953 ax-pre-lttrn 7954 ax-pre-apti 7955 ax-pre-ltadd 7956 ax-pre-mulgt0 7957 ax-pre-mulext 7958 ax-arch 7959 ax-caucvg 7960

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-reu 2475 df-rmo 2476 df-rab 2477 df-v 2754 df-sbc 2978 df-csb 3073 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-nul 3438 df-if 3550 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-iun 3903 df-br 4019 df-opab 4080 df-mpt 4081 df-tr 4117 df-id 4311 df-po 4314 df-iso 4315 df-iord 4384 df-on 4386 df-ilim 4387 df-suc 4389 df-iom 4608 df-xp 4650 df-rel 4651 df-cnv 4652 df-co 4653 df-dm 4654 df-rn 4655 df-res 4656 df-ima 4657 df-iota 5196 df-fun 5237 df-fn 5238 df-f 5239 df-f1 5240 df-fo 5241 df-f1o 5242 df-fv 5243 df-isom 5244 df-riota 5851 df-ov 5898 df-oprab 5899 df-mpo 5900 df-1st 6164 df-2nd 6165 df-recs 6329 df-irdg 6394 df-frec 6415 df-1o 6440 df-2o 6441 df-oadd 6444 df-er 6558 df-en 6766 df-dom 6767 df-fin 6768 df-sup 7012 df-inf 7013 df-pnf 8023 df-mnf 8024 df-xr 8025 df-ltxr 8026 df-le 8027 df-sub 8159 df-neg 8160 df-reap 8561 df-ap 8568 df-div 8659 df-inn 8949 df-2 9007 df-3 9008 df-4 9009 df-n0 9206 df-z 9283 df-uz 9558 df-q 9649 df-rp 9683 df-fz 10038 df-fzo 10172 df-fl 10300 df-mod 10353 df-seqfrec 10476 df-exp 10550 df-ihash 10787 df-cj 10882 df-re 10883 df-im 10884 df-rsqrt 11038 df-abs 11039 df-clim 11318 df-proddc 11590 df-dvds 11826 df-gcd 11975 df-prm 12139 df-odz 12241 df-phi 12242 df-pc 12316

This theorem is referenced by: pockthg 12388

W3C validator