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

Theorem prmind2 14228
Description: A variation on prmind 14229 assuming complete induction for primes. (Contributed by Mario Carneiro, 20-Jun-2015.)
Hypotheses
Ref Expression
prmind.1
prmind.2
prmind.3
prmind.4
prmind.5
prmind.6
prmind2.7
prmind2.8
Assertion
Ref Expression
prmind2
Distinct variable groups:   ,   ,   , ,   ,   ,   ,   , ,

Proof of Theorem prmind2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfz1end 11744 . . 3
21biimpi 194 . 2
3 oveq2 6304 . . . 4
43raleqdv 3060 . . 3
5 oveq2 6304 . . . 4
65raleqdv 3060 . . 3
7 oveq2 6304 . . . 4
87raleqdv 3060 . . 3
9 oveq2 6304 . . . 4
109raleqdv 3060 . . 3
11 prmind.6 . . . . 5
12 elfz1eq 11726 . . . . . 6
13 prmind.1 . . . . . 6
1412, 13syl 16 . . . . 5
1511, 14mpbiri 233 . . . 4
1615rgen 2817 . . 3
17 peano2nn 10573 . . . . . . . . . . . . 13
1817ad2antrr 725 . . . . . . . . . . . 12
1918nncnd 10577 . . . . . . . . . . 11
20 elfzuz 11713 . . . . . . . . . . . . . 14
2120ad2antrl 727 . . . . . . . . . . . . 13
22 eluz2nn 11148 . . . . . . . . . . . . 13
2321, 22syl 16 . . . . . . . . . . . 12
2423nncnd 10577 . . . . . . . . . . 11
2523nnne0d 10605 . . . . . . . . . . 11
2619, 24, 25divcan2d 10347 . . . . . . . . . 10
27 simprr 757 . . . . . . . . . . . . 13
2823nnzd 10993 . . . . . . . . . . . . . 14
2918nnzd 10993 . . . . . . . . . . . . . 14
30 dvdsval2 13989 . . . . . . . . . . . . . 14
3128, 25, 29, 30syl3anc 1228 . . . . . . . . . . . . 13
3227, 31mpbid 210 . . . . . . . . . . . 12
3324mulid2d 9635 . . . . . . . . . . . . . 14
34 elfzle2 11719 . . . . . . . . . . . . . . . . 17
3534ad2antrl 727 . . . . . . . . . . . . . . . 16
36 nncn 10569 . . . . . . . . . . . . . . . . . 18
3736ad2antrr 725 . . . . . . . . . . . . . . . . 17
38 ax-1cn 9571 . . . . . . . . . . . . . . . . 17
39 pncan 9849 . . . . . . . . . . . . . . . . 17
4037, 38, 39sylancl 662 . . . . . . . . . . . . . . . 16
4135, 40breqtrd 4476 . . . . . . . . . . . . . . 15
42 nnz 10911 . . . . . . . . . . . . . . . . 17
4342ad2antrr 725 . . . . . . . . . . . . . . . 16
44 zleltp1 10939 . . . . . . . . . . . . . . . 16
4528, 43, 44syl2anc 661 . . . . . . . . . . . . . . 15
4641, 45mpbid 210 . . . . . . . . . . . . . 14
4733, 46eqbrtrd 4472 . . . . . . . . . . . . 13
48 1red 9632 . . . . . . . . . . . . . 14
4918nnred 10576 . . . . . . . . . . . . . 14
5023nnred 10576 . . . . . . . . . . . . . 14
5123nngt0d 10604 . . . . . . . . . . . . . 14
52 ltmuldiv 10440 . . . . . . . . . . . . . 14
5348, 49, 50, 51, 52syl112anc 1232 . . . . . . . . . . . . 13
5447, 53mpbid 210 . . . . . . . . . . . 12
55 eluz2b1 11182 . . . . . . . . . . . 12
5632, 54, 55sylanbrc 664 . . . . . . . . . . 11
57 fznn 11776 . . . . . . . . . . . . . . 15
5843, 57syl 16 . . . . . . . . . . . . . 14
5923, 41, 58mpbir2and 922 . . . . . . . . . . . . 13
60 simplr 755 . . . . . . . . . . . . 13
61 prmind.2 . . . . . . . . . . . . . 14
6261rspcv 3206 . . . . . . . . . . . . 13
6359, 60, 62sylc 60 . . . . . . . . . . . 12
6418nnrpd 11284 . . . . . . . . . . . . . . . . 17
6523nnrpd 11284 . . . . . . . . . . . . . . . . 17
6664, 65rpdivcld 11302 . . . . . . . . . . . . . . . 16
6766rpgt0d 11288 . . . . . . . . . . . . . . 15
68 elnnz 10899 . . . . . . . . . . . . . . 15
6932, 67, 68sylanbrc 664 . . . . . . . . . . . . . 14
7018nnne0d 10605 . . . . . . . . . . . . . . . . . 18
7119, 70dividd 10343 . . . . . . . . . . . . . . . . 17
72 eluz2b2 11183 . . . . . . . . . . . . . . . . . . 19
7372simprbi 464 . . . . . . . . . . . . . . . . . 18
7421, 73syl 16 . . . . . . . . . . . . . . . . 17
7571, 74eqbrtrd 4472 . . . . . . . . . . . . . . . 16
7618nngt0d 10604 . . . . . . . . . . . . . . . . 17
77 ltdiv23 10461 . . . . . . . . . . . . . . . . 17
7849, 49, 76, 50, 51, 77syl122anc 1237 . . . . . . . . . . . . . . . 16
7975, 78mpbid 210 . . . . . . . . . . . . . . 15
80 zleltp1 10939 . . . . . . . . . . . . . . . 16
8132, 43, 80syl2anc 661 . . . . . . . . . . . . . . 15
8279, 81mpbird 232 . . . . . . . . . . . . . 14
83 fznn 11776 . . . . . . . . . . . . . . 15
8443, 83syl 16 . . . . . . . . . . . . . 14
8569, 82, 84mpbir2and 922 . . . . . . . . . . . . 13
86 prmind.3 . . . . . . . . . . . . . . 15
8786cbvralv 3084 . . . . . . . . . . . . . 14
8860, 87sylib 196 . . . . . . . . . . . . 13
89 vex 3112 . . . . . . . . . . . . . . . 16
9089, 86sbcie 3362 . . . . . . . . . . . . . . 15
91 dfsbcq 3329 . . . . . . . . . . . . . . 15
9290, 91syl5bbr 259 . . . . . . . . . . . . . 14
9392rspcv 3206 . . . . . . . . . . . . 13
9485, 88, 93sylc 60 . . . . . . . . . . . 12
9563, 94jca 532 . . . . . . . . . . 11
9692anbi2d 703 . . . . . . . . . . . . . 14
97 ovex 6324 . . . . . . . . . . . . . . . 16
98 prmind.4 . . . . . . . . . . . . . . . 16
9997, 98sbcie 3362 . . . . . . . . . . . . . . 15
100 oveq2 6304 . . . . . . . . . . . . . . . 16
101100sbceq1d 3332 . . . . . . . . . . . . . . 15
10299, 101syl5bbr 259 . . . . . . . . . . . . . 14
10396, 102imbi12d 320 . . . . . . . . . . . . 13
104103imbi2d 316 . . . . . . . . . . . 12
105 prmind2.8 . . . . . . . . . . . . 13
106105expcom 435 . . . . . . . . . . . 12
107104, 106vtoclga 3173 . . . . . . . . . . 11
10856, 21, 95, 107syl3c 61 . . . . . . . . . 10
10926, 108sbceq1dd 3333 . . . . . . . . 9
110109rexlimdvaa 2950 . . . . . . . 8
111 ralnex 2903 . . . . . . . . 9
112 simpl 457 . . . . . . . . . . . . . 14
113 elnnuz 11146 . . . . . . . . . . . . . 14
114112, 113sylib 196 . . . . . . . . . . . . 13
115 eluzp1p1 11135 . . . . . . . . . . . . 13
116114, 115syl 16 . . . . . . . . . . . 12
117 df-2 10619 . . . . . . . . . . . . 13
118117fveq2i 5874 . . . . . . . . . . . 12
119116, 118syl6eleqr 2556 . . . . . . . . . . 11
120 isprm3 14226 . . . . . . . . . . . 12
121120baibr 904 . . . . . . . . . . 11
122119, 121syl 16 . . . . . . . . . 10
123 simpr 461 . . . . . . . . . . . . 13
12461cbvralv 3084 . . . . . . . . . . . . 13
125123, 124sylib 196 . . . . . . . . . . . 12
126112nncnd 10577 . . . . . . . . . . . . . . 15
127126, 38, 39sylancl 662 . . . . . . . . . . . . . 14
128127oveq2d 6312 . . . . . . . . . . . . 13
129128raleqdv 3060 . . . . . . . . . . . 12
130125, 129mpbird 232 . . . . . . . . . . 11
131 nfcv 2619 . . . . . . . . . . . 12
132 nfv 1707 . . . . . . . . . . . . 13
133 nfsbc1v 3347 . . . . . . . . . . . . 13
134132, 133nfim 1920 . . . . . . . . . . . 12
135 oveq1 6303 . . . . . . . . . . . . . . 15
136135oveq2d 6312 . . . . . . . . . . . . . 14
137136raleqdv 3060 . . . . . . . . . . . . 13
138 sbceq1a 3338 . . . . . . . . . . . . 13
139137, 138imbi12d 320 . . . . . . . . . . . 12
140 prmind2.7 . . . . . . . . . . . . 13
141140ex 434 . . . . . . . . . . . 12
142131, 134, 139, 141vtoclgaf 3172 . . . . . . . . . . 11
143130, 142syl5com 30 . . . . . . . . . 10
144122, 143sylbid 215 . . . . . . . . 9
145111, 144syl5bir 218 . . . . . . . 8
146110, 145pm2.61d 158 . . . . . . 7
147146ex 434 . . . . . 6
148 ralsnsg 4061 . . . . . . 7
14917, 148syl 16 . . . . . 6
150147, 149sylibrd 234 . . . . 5
151150ancld 553 . . . 4
152 fzsuc 11756 . . . . . . 7
153113, 152sylbi 195 . . . . . 6
154153raleqdv 3060 . . . . 5
155 ralunb 3684 . . . . 5
156154, 155syl6bb 261 . . . 4
157151, 156sylibrd 234 . . 3
1584, 6, 8, 10, 16, 157nnind 10579 . 2
159 prmind.5 . . 3
160159rspcv 3206 . 2
1612, 158, 160sylc 60 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  =/=wne 2652  A.wral 2807  E.wrex 2808  [.wsbc 3327  u.cun 3473  {csn 4029   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   cz 10889   cuz 11110   cfz 11701   cdvds 13986   cprime 14217
This theorem is referenced by:  prmind  14229  4sqlem19  14481
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-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
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-en 7537  df-dom 7538  df-sdom 7539  df-fin 7540  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-n0 10821  df-z 10890  df-uz 11111  df-rp 11250  df-fz 11702  df-dvds 13987  df-prm 14218
  Copyright terms: Public domain W3C validator