Theorem eluzle 9812

Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.)

Assertion

Ref	Expression
eluzle	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁)

Proof of Theorem eluzle

Step	Hyp	Ref	Expression
1		eluz2 9805	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
2	1	simp3bi 1041	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁)

Syntax hints:   → wi 4   ∈ wcel 2202   class class class wbr 4093  ‘cfv 5333   ≤ cle 8257  ℤcz 9523  ℤ_≥cuz 9799

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-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-cnex 8166  ax-resscn 8167

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-rab 2520  df-v 2805  df-sbc 3033  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-mpt 4157  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-res 4743  df-ima 4744  df-iota 5293  df-fun 5335  df-fn 5336  df-f 5337  df-fv 5341  df-ov 6031  df-neg 8395  df-z 9524  df-uz 9800

This theorem is referenced by:  uztrn  9817  uzneg  9819  uzss  9821  uz11  9823  eluzp1l  9825  uzm1  9831  uzin  9833  uzind4  9866  elfz5  10297  elfzle1  10307  elfzle2  10308  elfzle3  10310  uzsplit  10372  uzdisj  10373  uznfz  10383  elfz2nn0  10392  uzsubfz0  10409  nn0disj  10418  fzouzdisj  10462  fzoun  10463  elfzonelfzo  10521  infssuzex  10539  suprzubdc  10542  fldiv4lem1div2uz2  10612  mulp1mod1  10673  m1modge3gt1  10679  uzennn  10744  seq3split  10796  seq3f1olemqsumk  10820  seq3f1o  10825  seq3coll  11152  swrdlen2  11292  swrdfv2  11293  seq3shft  11461  cvg1nlemcau  11607  resqrexlemcvg  11642  resqrexlemga  11646  summodclem2a  12005  fsum3  12011  fsum3cvg3  12020  fsumadd  12030  sumsnf  12033  fsummulc2  12072  isumshft  12114  divcnv  12121  geolim2  12136  cvgratnnlemseq  12150  cvgratnnlemsumlt  12152  cvgratz  12156  mertenslemi1  12159  prodmodclem3  12199  prodmodclem2a  12200  fprodntrivap  12208  prodsnf  12216  fprodeq0  12241  efcllemp  12282  dvdsbnd  12590  uzwodc  12671  ncoprmgcdne1b  12724  isprm5  12777  hashdvds  12856  pcmpt2  12980  pcfaclem  12985  pcfac  12986  nninfdclemp1  13134  strext  13251  gsumfzval  13537  znidom  14736  lgslem1  15802  lgsdirprm  15836  lgseisen  15876  cvgcmp2nlemabs  16747  gsumgfsumlem  16795