Theorem elfzuz3 12524

Description: Membership in a finite set of sequential integers implies membership in an upper set of integers. (Contributed by NM, 28-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfzuz3	⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))

Proof of Theorem elfzuz3

Step	Hyp	Ref	Expression
1		elfzuzb 12521	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)))
2	1	simprbi 483	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))

Syntax hints:   → wi 4   ∈ wcel 2131  ‘cfv 6041  (class class class)co 6805  ℤ_≥cuz 11871  ...cfz 12511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-cnex 10176  ax-resscn 10177

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-iun 4666  df-br 4797  df-opab 4857  df-mpt 4874  df-id 5166  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-fv 6049  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-1st 7325  df-2nd 7326  df-neg 10453  df-z 11562  df-uz 11872  df-fz 12512

This theorem is referenced by:  elfzel2  12525  elfzle2  12530  peano2fzr  12539  fzsplit2  12551  fzsplit  12552  fznn0sub  12558  fzopth  12563  fzss1  12565  fzss2  12566  fzp1elp1  12579  predfz  12650  fzosplit  12687  fzoend  12745  fzofzp1b  12752  uzindi  12967  seqcl2  13005  seqfveq2  13009  monoord  13017  sermono  13019  seqsplit  13020  seqf1olem2  13027  seqid2  13033  seqhomo  13034  seqz  13035  bcval5  13291  seqcoll  13432  seqcoll2  13433  swrdval2  13611  swrd0val  13612  swrd0len  13613  spllen  13697  splfv2a  13699  fsum0diag2  14706  climcndslem2  14773  prodfn0  14817  lcmflefac  15555  pcbc  15798  vdwlem2  15880  vdwlem5  15883  vdwlem6  15884  vdwlem8  15886  prmgaplem1  15947  psgnunilem5  18106  efgsres  18343  efgredleme  18348  efgcpbllemb  18360  imasdsf1olem  22371  volsup  23516  dvn2bss  23884  dvtaylp  24315  wilth  24988  ftalem1  24990  ppisval2  25022  dvdsppwf1o  25103  logfaclbnd  25138  bposlem6  25205  wlkres  26769  fzsplit3  29854  ballotlemsima  30878  ballotlemfrc  30889  ballotlemfrceq  30891  fzssfzo  30914  wrdres  30918  signstres  30953  fsum2dsub  30986  erdszelem7  31478  erdszelem8  31479  poimirlem1  33715  poimirlem2  33716  poimirlem3  33717  poimirlem4  33718  poimirlem7  33721  poimirlem12  33726  poimirlem15  33729  poimirlem16  33730  poimirlem17  33731  poimirlem19  33733  poimirlem20  33734  poimirlem23  33737  poimirlem24  33738  poimirlem25  33739  poimirlem29  33743  poimirlem31  33745  mettrifi  33858  bcc0  39033  iunincfi  39763  monoordxrv  40202  fmulcl  40308  fmul01lt1lem2  40312  dvnprodlem2  40657  stoweidlem11  40723  stoweidlem17  40729  fourierdlem15  40834  ssfz12  41826  smonoord  41843  pfxres  41890  pfxf  41891  repswpfx  41938