MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pockthlem Unicode version

Theorem pockthlem 14423
Description: Lemma for pockthg 14424. (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
StepHypRef Expression
1 pockthlem.7 . . . . . . 7
2 pockthg.1 . . . . . . 7
3 pcdvds 14387 . . . . . . 7
41, 2, 3syl2anc 661 . . . . . 6
52nnzd 10993 . . . . . . . 8
6 pockthg.2 . . . . . . . . 9
76nnzd 10993 . . . . . . . 8
8 dvdsmul1 14005 . . . . . . . 8
95, 7, 8syl2anc 661 . . . . . . 7
10 pockthg.4 . . . . . . . . 9
1110oveq1d 6311 . . . . . . . 8
122, 6nnmulcld 10608 . . . . . . . . . 10
1312nncnd 10577 . . . . . . . . 9
14 ax-1cn 9571 . . . . . . . . 9
15 pncan 9849 . . . . . . . . 9
1613, 14, 15sylancl 662 . . . . . . . 8
1711, 16eqtrd 2498 . . . . . . 7
189, 17breqtrrd 4478 . . . . . 6
19 prmnn 14220 . . . . . . . . . 10
201, 19syl 16 . . . . . . . . 9
21 pockthlem.8 . . . . . . . . . 10
2221nnnn0d 10877 . . . . . . . . 9
2320, 22nnexpcld 12331 . . . . . . . 8
2423nnzd 10993 . . . . . . 7
25 1z 10919 . . . . . . . . . 10
26 nnuz 11145 . . . . . . . . . . . . 13
2712, 26syl6eleq 2555 . . . . . . . . . . . 12
28 eluzp1p1 11135 . . . . . . . . . . . 12
2927, 28syl 16 . . . . . . . . . . 11
3010, 29eqeltrd 2545 . . . . . . . . . 10
31 eluzp1m1 11133 . . . . . . . . . 10
3225, 30, 31sylancr 663 . . . . . . . . 9
3332, 26syl6eleqr 2556 . . . . . . . 8
3433nnzd 10993 . . . . . . 7
35 dvdstr 14018 . . . . . . 7
3624, 5, 34, 35syl3anc 1228 . . . . . 6
374, 18, 36mp2and 679 . . . . 5
3823nnne0d 10605 . . . . . 6
39 dvdsval2 13989 . . . . . 6
4024, 38, 34, 39syl3anc 1228 . . . . 5
4137, 40mpbid 210 . . . 4
42 pockthlem.5 . . . . . . 7
43 prmnn 14220 . . . . . . 7
4442, 43syl 16 . . . . . 6
45 pockthlem.9 . . . . . 6
4644nnzd 10993 . . . . . . . . . . 11
47 gcddvds 14153 . . . . . . . . . . 11
4845, 46, 47syl2anc 661 . . . . . . . . . 10
4948simpld 459 . . . . . . . . 9
5048simprd 463 . . . . . . . . . 10
51 pockthlem.6 . . . . . . . . . 10
5245, 46gcdcld 14156 . . . . . . . . . . . 12
5352nn0zd 10992 . . . . . . . . . . 11
54 df-2 10619 . . . . . . . . . . . . . . . 16
5554fveq2i 5874 . . . . . . . . . . . . . . 15
5630, 55syl6eleqr 2556 . . . . . . . . . . . . . 14
57 eluz2b2 11183 . . . . . . . . . . . . . 14
5856, 57sylib 196 . . . . . . . . . . . . 13
5958simpld 459 . . . . . . . . . . . 12
6059nnzd 10993 . . . . . . . . . . 11
61 dvdstr 14018 . . . . . . . . . . 11
6253, 46, 60, 61syl3anc 1228 . . . . . . . . . 10
6350, 51, 62mp2and 679 . . . . . . . . 9
6459nnne0d 10605 . . . . . . . . . . 11
65 simpr 461 . . . . . . . . . . . 12
6665necon3ai 2685 . . . . . . . . . . 11
6764, 66syl 16 . . . . . . . . . 10
68 dvdslegcd 14154 . . . . . . . . . 10
6953, 45, 60, 67, 68syl31anc 1231 . . . . . . . . 9
7049, 63, 69mp2and 679 . . . . . . . 8
71 pockthlem.10 . . . . . . . . . . 11
7271oveq1d 6311 . . . . . . . . . 10
7333nnnn0d 10877 . . . . . . . . . . . 12
74 zexpcl 12181 . . . . . . . . . . . 12
7545, 73, 74syl2anc 661 . . . . . . . . . . 11
76 modgcd 14174 . . . . . . . . . . 11
7775, 59, 76syl2anc 661 . . . . . . . . . 10
78 gcdcom 14158 . . . . . . . . . . . 12
7925, 60, 78sylancr 663 . . . . . . . . . . 11
80 gcd1 14170 . . . . . . . . . . . 12
8160, 80syl 16 . . . . . . . . . . 11
8279, 81eqtrd 2498 . . . . . . . . . 10
8372, 77, 823eqtr3d 2506 . . . . . . . . 9
84 rpexp 14261 . . . . . . . . . 10
8545, 60, 33, 84syl3anc 1228 . . . . . . . . 9
8683, 85mpbid 210 . . . . . . . 8
8770, 86breqtrd 4476 . . . . . . 7
8844nnne0d 10605 . . . . . . . . . 10
89 simpr 461 . . . . . . . . . . 11
9089necon3ai 2685 . . . . . . . . . 10
9188, 90syl 16 . . . . . . . . 9
92 gcdn0cl 14152 . . . . . . . . 9
9345, 46, 91, 92syl21anc 1227 . . . . . . . 8
94 nnle1eq1 10589 . . . . . . . 8
9593, 94syl 16 . . . . . . 7
9687, 95mpbid 210 . . . . . 6
97 odzcl 14320 . . . . . 6
9844, 45, 96, 97syl3anc 1228 . . . . 5
9998nnzd 10993 . . . 4
10059nnred 10576 . . . . . . . . . 10
10158simprd 463 . . . . . . . . . 10
102 1mod 12028 . . . . . . . . . 10
103100, 101, 102syl2anc 661 . . . . . . . . 9
10471, 103eqtr4d 2501 . . . . . . . 8
105 1zzd 10920 . . . . . . . . 9
106 moddvds 13993 . . . . . . . . 9
10759, 75, 105, 106syl3anc 1228 . . . . . . . 8
108104, 107mpbid 210 . . . . . . 7
109 peano2zm 10932 . . . . . . . . 9
11075, 109syl 16 . . . . . . . 8
111 dvdstr 14018 . . . . . . . 8
11246, 60, 110, 111syl3anc 1228 . . . . . . 7
11351, 108, 112mp2and 679 . . . . . 6
114 odzdvds 14322 . . . . . . 7
11544, 45, 96, 73, 114syl31anc 1231 . . . . . 6
116113, 115mpbid 210 . . . . 5
11733nncnd 10577 . . . . . 6
11823nncnd 10577 . . . . . 6
119117, 118, 38divcan1d 10346 . . . . 5
120116, 119breqtrrd 4478 . . . 4
121 nprmdvds1 14252 . . . . . 6
12242, 121syl 16 . . . . 5
12320nnzd 10993 . . . . . . . . . . . . . 14
124 iddvdsexp 14007 . . . . . . . . . . . . . 14
125123, 21, 124syl2anc 661 . . . . . . . . . . . . 13
126 dvdstr 14018 . . . . . . . . . . . . . 14
127123, 24, 34, 126syl3anc 1228 . . . . . . . . . . . . 13
128125, 37, 127mp2and 679 . . . . . . . . . . . 12
12920nnne0d 10605 . . . . . . . . . . . . 13
130 dvdsval2 13989 . . . . . . . . . . . . 13
131123, 129, 34, 130syl3anc 1228 . . . . . . . . . . . 12
132128, 131mpbid 210 . . . . . . . . . . 11
13373nn0ge0d 10880 . . . . . . . . . . . 12
13433nnred 10576 . . . . . . . . . . . . 13
13520nnred 10576 . . . . . . . . . . . . 13
13620nngt0d 10604 . . . . . . . . . . . . 13
137 ge0div 10434 . . . . . . . . . . . . 13
138134, 135, 136, 137syl3anc 1228 . . . . . . . . . . . 12
139133, 138mpbid 210 . . . . . . . . . . 11
140 elnn0z 10902 . . . . . . . . . . 11
141132, 139, 140sylanbrc 664 . . . . . . . . . 10
142 zexpcl 12181 . . . . . . . . . 10
14345, 141, 142syl2anc 661 . . . . . . . . 9
144 peano2zm 10932 . . . . . . . . 9
145143, 144syl 16 . . . . . . . 8
146 dvdsgcd 14181 . . . . . . . 8
14746, 145, 60, 146syl3anc 1228 . . . . . . 7
14851, 147mpan2d 674 . . . . . 6
149 odzdvds 14322 . . . . . . . 8
15044, 45, 96, 141, 149syl31anc 1231 . . . . . . 7
15120nncnd 10577 . . . . . . . . . . 11
15221nnzd 10993 . . . . . . . . . . 11
153151, 129, 152expm1d 12320 . . . . . . . . . 10
154153oveq2d 6312 . . . . . . . . 9
155134, 23nndivred 10609 . . . . . . . . . . 11
156155recnd 9643 . . . . . . . . . 10
157156, 118, 151, 129divassd 10380 . . . . . . . . 9
158119oveq1d 6311 . . . . . . . . 9
159154, 157, 1583eqtr2d 2504 . . . . . . . 8
160159breq2d 4464 . . . . . . 7
161150, 160bitr4d 256 . . . . . 6
162 pockthlem.11 . . . . . . 7
163162breq2d 4464 . . . . . 6
164148, 161, 1633imtr3d 267 . . . . 5
165122, 164mtod 177 . . . 4
166 prmpwdvds 14422 . . . 4
16741, 99, 1, 21, 120, 165, 166syl222anc 1244 . . 3
168 odzphi 14323 . . . . 5
16944, 45, 96, 168syl3anc 1228 . . . 4
170 phiprm 14307 . . . . 5
17142, 170syl 16 . . . 4
172169, 171breqtrd 4476 . . 3
173 prmuz2 14235 . . . . . . . . 9
17442, 173syl 16 . . . . . . . 8
175174, 55syl6eleq 2555 . . . . . . 7
176 eluzp1m1 11133 . . . . . . 7
17725, 175, 176sylancr 663 . . . . . 6
178177, 26syl6eleqr 2556 . . . . 5
179178nnzd 10993 . . . 4
180 dvdstr 14018 . . . 4
18124, 99, 179, 180syl3anc 1228 . . 3
182167, 172, 181mp2and 679 . 2
183 pcdvdsb 14392 . . 3
1841, 179, 22, 183syl3anc 1228 . 2
185182, 184mpbird 232 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  =/=wne 2652   class class class wbr 4452  `cfv 5593  (class class class)co 6296   cc 9511   cr 9512  0cc0 9513  1c1 9514   caddc 9516   cmul 9518   clt 9649   cle 9650   cmin 9828   cdiv 10231   cn 10561  2c2 10610   cn0 10820   cz 10889   cuz 11110   cmo 11996   cexp 12166   cdvds 13986   cgcd 14144   cprime 14217   codz 14293   cphi 14294   cpc 14360
This theorem is referenced by:  pockthg  14424
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-cnex 9569  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589  ax-pre-mulgt0 9590  ax-pre-sup 9591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-int 4287  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-1st 6800  df-2nd 6801  df-recs 7061  df-rdg 7095  df-1o 7149  df-2o 7150  df-oadd 7153  df-er 7330  df-map 7441  df-en 7537  df-dom 7538  df-sdom 7539  df-fin 7540  df-sup 7921  df-card 8341  df-cda 8569  df-pnf 9651  df-mnf 9652  df-xr 9653  df-ltxr 9654  df-le 9655  df-sub 9830  df-neg 9831  df-div 10232  df-nn 10562  df-2 10619  df-3 10620  df-n0 10821  df-z 10890  df-uz 11111  df-q 11212  df-rp 11250  df-fz 11702  df-fzo 11825  df-fl 11929  df-mod 11997  df-seq 12108  df-exp 12167  df-hash 12406  df-cj 12932  df-re 12933  df-im 12934  df-sqrt 13068  df-abs 13069  df-dvds 13987  df-gcd 14145  df-prm 14218  df-odz 14295  df-phi 14296  df-pc 14361
  Copyright terms: Public domain W3C validator