pockthlem - Intuitionistic Logic Explorer

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

Theorem pockthlem 12928

Description: Lemma for pockthg 12929. (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 12681	. . . . . 6
3	1, 2	syl 14	. . . . 5
4		pockthlem.8	. . . . . 6
5	4	nnnn0d 9454	. . . . 5
6	3, 5	nnexpcld 10956	. . . 4
7	6	nnzd 9600	. . 3
8		pockthlem.5	. . . . . 6
9		prmnn 12681	. . . . . 6
10	8, 9	syl 14	. . . . 5
11		pockthlem.9	. . . . 5
12	10	nnzd 9600	. . . . . . . . . 10
13		gcddvds 12533	. . . . . . . . . 10 $/\$ $/\$
14	11, 12, 13	syl2anc 411	. . . . . . . . 9 $/\$
15	14	simpld 112	. . . . . . . 8
16	11, 12	gcdcld 12538	. . . . . . . . . 10
17	16	nn0zd 9599	. . . . . . . . 9
18		pockthg.4	. . . . . . . . . . . . . 14
19		pockthg.1	. . . . . . . . . . . . . . . . 17
20		pockthg.2	. . . . . . . . . . . . . . . . 17
21	19, 20	nnmulcld 9191	. . . . . . . . . . . . . . . 16
22		nnuz 9791	. . . . . . . . . . . . . . . 16
23	21, 22	eleqtrdi 2324	. . . . . . . . . . . . . . 15
24		eluzp1p1 9781	. . . . . . . . . . . . . . 15
25	23, 24	syl 14	. . . . . . . . . . . . . 14
26	18, 25	eqeltrd 2308	. . . . . . . . . . . . 13
27		df-2 9201	. . . . . . . . . . . . . 14
28	27	fveq2i 5642	. . . . . . . . . . . . 13
29	26, 28	eleqtrrdi 2325	. . . . . . . . . . . 12
30		eluz2b2 9836	. . . . . . . . . . . 12 $/\$
31	29, 30	sylib 122	. . . . . . . . . . 11 $/\$
32	31	simpld 112	. . . . . . . . . 10
33	32	nnzd 9600	. . . . . . . . 9
34	14	simprd 114	. . . . . . . . 9
35		pockthlem.6	. . . . . . . . 9
36	17, 12, 33, 34, 35	dvdstrd 12390	. . . . . . . 8
37	32	nnne0d 9187	. . . . . . . . . 10
38		simpr 110	. . . . . . . . . . 11 $/\$
39	38	necon3ai 2451	. . . . . . . . . 10 $/\$
40	37, 39	syl 14	. . . . . . . . 9 $/\$
41		dvdslegcd 12534	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
42	17, 11, 33, 40, 41	syl31anc 1276	. . . . . . . 8 $/\$
43	15, 36, 42	mp2and 433	. . . . . . 7
44		pockthlem.10	. . . . . . . . . 10
45	44	oveq1d 6032	. . . . . . . . 9
46		1z 9504	. . . . . . . . . . . . . 14
47		eluzp1m1 9779	. . . . . . . . . . . . . 14 $/\$
48	46, 26, 47	sylancr 414	. . . . . . . . . . . . 13
49	48, 22	eleqtrrdi 2325	. . . . . . . . . . . 12
50	49	nnnn0d 9454	. . . . . . . . . . 11
51		zexpcl 10815	. . . . . . . . . . 11 $/\$
52	11, 50, 51	syl2anc 411	. . . . . . . . . 10
53		modgcd 12561	. . . . . . . . . 10 $/\$
54	52, 32, 53	syl2anc 411	. . . . . . . . 9
55		gcdcom 12543	. . . . . . . . . . 11 $/\$
56	46, 33, 55	sylancr 414	. . . . . . . . . 10
57		gcd1 12557	. . . . . . . . . . 11
58	33, 57	syl 14	. . . . . . . . . 10
59	56, 58	eqtrd 2264	. . . . . . . . 9
60	45, 54, 59	3eqtr3d 2272	. . . . . . . 8
61		rpexp 12724	. . . . . . . . 9 $/\$ $/\$
62	11, 33, 49, 61	syl3anc 1273	. . . . . . . 8
63	60, 62	mpbid 147	. . . . . . 7
64	43, 63	breqtrd 4114	. . . . . 6
65	10	nnne0d 9187	. . . . . . . . 9
66		simpr 110	. . . . . . . . . 10 $/\$
67	66	necon3ai 2451	. . . . . . . . 9 $/\$
68	65, 67	syl 14	. . . . . . . 8 $/\$
69		gcdn0cl 12532	. . . . . . . 8 $/\$ $/\$ $/\$
70	11, 12, 68, 69	syl21anc 1272	. . . . . . 7
71		nnle1eq1 9166	. . . . . . 7
72	70, 71	syl 14	. . . . . 6
73	64, 72	mpbid 147	. . . . 5
74		odzcl 12815	. . . . 5 $/\$ $/\$
75	10, 11, 73, 74	syl3anc 1273	. . . 4
76	75	nnzd 9600	. . 3
77		prmuz2 12702	. . . . . . . 8
78	8, 77	syl 14	. . . . . . 7
79	78, 28	eleqtrdi 2324	. . . . . 6
80		eluzp1m1 9779	. . . . . 6 $/\$
81	46, 79, 80	sylancr 414	. . . . 5
82	81, 22	eleqtrrdi 2325	. . . 4
83	82	nnzd 9600	. . 3
84	19	nnzd 9600	. . . . . 6
85	49	nnzd 9600	. . . . . 6
86		pcdvds 12887	. . . . . . 7 $/\$
87	1, 19, 86	syl2anc 411	. . . . . 6
88	20	nnzd 9600	. . . . . . . 8
89		dvdsmul1 12373	. . . . . . . 8 $/\$
90	84, 88, 89	syl2anc 411	. . . . . . 7
91	18	oveq1d 6032	. . . . . . . 8
92	21	nncnd 9156	. . . . . . . . 9
93		ax-1cn 8124	. . . . . . . . 9
94		pncan 8384	. . . . . . . . 9 $/\$
95	92, 93, 94	sylancl 413	. . . . . . . 8
96	91, 95	eqtrd 2264	. . . . . . 7
97	90, 96	breqtrrd 4116	. . . . . 6
98	7, 84, 85, 87, 97	dvdstrd 12390	. . . . 5
99	6	nnne0d 9187	. . . . . 6
100		dvdsval2 12350	. . . . . 6 $/\$ $/\$
101	7, 99, 85, 100	syl3anc 1273	. . . . 5
102	98, 101	mpbid 147	. . . 4
103		peano2zm 9516	. . . . . . . 8
104	52, 103	syl 14	. . . . . . 7
105		nnq 9866	. . . . . . . . . . 11
106	32, 105	syl 14	. . . . . . . . . 10
107	31	simprd 114	. . . . . . . . . 10
108		q1mod 10617	. . . . . . . . . 10 $/\$
109	106, 107, 108	syl2anc 411	. . . . . . . . 9
110	44, 109	eqtr4d 2267	. . . . . . . 8
111		1zzd 9505	. . . . . . . . 9
112		moddvds 12359	. . . . . . . . 9 $/\$ $/\$
113	32, 52, 111, 112	syl3anc 1273	. . . . . . . 8
114	110, 113	mpbid 147	. . . . . . 7
115	12, 33, 104, 35, 114	dvdstrd 12390	. . . . . 6
116		odzdvds 12817	. . . . . . 7 $/\$ $/\$ $/\$
117	10, 11, 73, 50, 116	syl31anc 1276	. . . . . 6
118	115, 117	mpbid 147	. . . . 5
119	49	nncnd 9156	. . . . . 6
120	6	nncnd 9156	. . . . . 6
121	6	nnap0d 9188	. . . . . 6 #
122	119, 120, 121	divcanap1d 8970	. . . . 5
123	118, 122	breqtrrd 4116	. . . 4
124		nprmdvds1 12711	. . . . . 6
125	8, 124	syl 14	. . . . 5
126	3	nnzd 9600	. . . . . . . . . . . . 13
127		iddvdsexp 12375	. . . . . . . . . . . . . 14 $/\$
128	126, 4, 127	syl2anc 411	. . . . . . . . . . . . 13
129	126, 7, 85, 128, 98	dvdstrd 12390	. . . . . . . . . . . 12
130	3	nnne0d 9187	. . . . . . . . . . . . 13
131		dvdsval2 12350	. . . . . . . . . . . . 13 $/\$ $/\$
132	126, 130, 85, 131	syl3anc 1273	. . . . . . . . . . . 12
133	129, 132	mpbid 147	. . . . . . . . . . 11
134	50	nn0ge0d 9457	. . . . . . . . . . . 12
135	49	nnred 9155	. . . . . . . . . . . . 13
136	3	nnred 9155	. . . . . . . . . . . . 13
137	3	nngt0d 9186	. . . . . . . . . . . . 13
138		ge0div 9050	. . . . . . . . . . . . 13 $/\$ $/\$
139	135, 136, 137, 138	syl3anc 1273	. . . . . . . . . . . 12
140	134, 139	mpbid 147	. . . . . . . . . . 11
141		elnn0z 9491	. . . . . . . . . . 11 $/\$
142	133, 140, 141	sylanbrc 417	. . . . . . . . . 10
143		zexpcl 10815	. . . . . . . . . 10 $/\$
144	11, 142, 143	syl2anc 411	. . . . . . . . 9
145		peano2zm 9516	. . . . . . . . 9
146	144, 145	syl 14	. . . . . . . 8
147		dvdsgcd 12582	. . . . . . . 8 $/\$ $/\$ $/\$
148	12, 146, 33, 147	syl3anc 1273	. . . . . . 7 $/\$
149	35, 148	mpan2d 428	. . . . . 6
150		odzdvds 12817	. . . . . . . 8 $/\$ $/\$ $/\$
151	10, 11, 73, 142, 150	syl31anc 1276	. . . . . . 7
152	3	nncnd 9156	. . . . . . . . . . 11
153	3	nnap0d 9188	. . . . . . . . . . 11 #
154	4	nnzd 9600	. . . . . . . . . . 11
155	152, 153, 154	expm1apd 10944	. . . . . . . . . 10
156	155	oveq2d 6033	. . . . . . . . 9
157	135, 6	nndivred 9192	. . . . . . . . . . 11
158	157	recnd 8207	. . . . . . . . . 10
159	158, 120, 152, 153	divassapd 9005	. . . . . . . . 9
160	122	oveq1d 6032	. . . . . . . . 9
161	156, 159, 160	3eqtr2d 2270	. . . . . . . 8
162	161	breq2d 4100	. . . . . . 7
163	151, 162	bitr4d 191	. . . . . 6
164		pockthlem.11	. . . . . . 7
165	164	breq2d 4100	. . . . . 6
166	149, 163, 165	3imtr3d 202	. . . . 5
167	125, 166	mtod 669	. . . 4
168		prmpwdvds 12927	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
169	102, 76, 1, 4, 123, 167, 168	syl222anc 1289	. . 3
170		odzphi 12818	. . . . 5 $/\$ $/\$
171	10, 11, 73, 170	syl3anc 1273	. . . 4
172		phiprm 12794	. . . . 5
173	8, 172	syl 14	. . . 4
174	171, 173	breqtrd 4114	. . 3
175	7, 76, 83, 169, 174	dvdstrd 12390	. 2
176		pcdvdsb 12892	. . 3 $/\$ $/\$
177	1, 83, 5, 176	syl3anc 1273	. 2
178	175, 177	mpbird 167	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105

wceq 1397

wcel 2202

wne 2402 class class class wbr 4088

cfv 5326 (class class class)co 6017

cc 8029

cr 8030

cc0 8031

c1 8032

caddc 8034

cmul 8036

clt 8213

cle 8214

cmin 8349

cdiv 8851

cn 9142

c2 9193

cn0 9401

cz 9478

cuz 9754

cq 9852

cmo 10583

cexp 10799

cdvds 12347

cgcd 12523

cprime 12678

codz 12779

cphi 12780

cpc 12856

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 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-iinf 4686 ax-cnex 8122 ax-resscn 8123 ax-1cn 8124 ax-1re 8125 ax-icn 8126 ax-addcl 8127 ax-addrcl 8128 ax-mulcl 8129 ax-mulrcl 8130 ax-addcom 8131 ax-mulcom 8132 ax-addass 8133 ax-mulass 8134 ax-distr 8135 ax-i2m1 8136 ax-0lt1 8137 ax-1rid 8138 ax-0id 8139 ax-rnegex 8140 ax-precex 8141 ax-cnre 8142 ax-pre-ltirr 8143 ax-pre-ltwlin 8144 ax-pre-lttrn 8145 ax-pre-apti 8146 ax-pre-ltadd 8147 ax-pre-mulgt0 8148 ax-pre-mulext 8149 ax-arch 8150 ax-caucvg 8151

This theorem depends on definitions: df-bi 117 df-stab 838 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-nel 2498 df-ral 2515 df-rex 2516 df-reu 2517 df-rmo 2518 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-if 3606 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-id 4390 df-po 4393 df-iso 4394 df-iord 4463 df-on 4465 df-ilim 4466 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-isom 5335 df-riota 5970 df-ov 6020 df-oprab 6021 df-mpo 6022 df-1st 6302 df-2nd 6303 df-recs 6470 df-irdg 6535 df-frec 6556 df-1o 6581 df-2o 6582 df-oadd 6585 df-er 6701 df-en 6909 df-dom 6910 df-fin 6911 df-sup 7182 df-inf 7183 df-pnf 8215 df-mnf 8216 df-xr 8217 df-ltxr 8218 df-le 8219 df-sub 8351 df-neg 8352 df-reap 8754 df-ap 8761 df-div 8852 df-inn 9143 df-2 9201 df-3 9202 df-4 9203 df-n0 9402 df-z 9479 df-uz 9755 df-q 9853 df-rp 9888 df-fz 10243 df-fzo 10377 df-fl 10529 df-mod 10584 df-seqfrec 10709 df-exp 10800 df-ihash 11037 df-cj 11402 df-re 11403 df-im 11404 df-rsqrt 11558 df-abs 11559 df-clim 11839 df-proddc 12111 df-dvds 12348 df-gcd 12524 df-prm 12679 df-odz 12781 df-phi 12782 df-pc 12857

This theorem is referenced by: pockthg 12929

W3C validator