Theorem eluzle 9767

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 9760	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
2	1	simp3bi 1040	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁)

Syntax hints:   → wi 4   ∈ wcel 2202   class class class wbr 4088  ‘cfv 5326   ≤ cle 8214  ℤcz 9478  ℤ_≥cuz 9754

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 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-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-cnex 8122  ax-resscn 8123

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  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-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-sbc 3032  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-mpt 4152  df-id 4390  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-fv 5334  df-ov 6020  df-neg 8352  df-z 9479  df-uz 9755

This theorem is referenced by:  uztrn  9772  uzneg  9774  uzss  9776  uz11  9778  eluzp1l  9780  uzm1  9786  uzin  9788  uzind4  9821  elfz5  10251  elfzle1  10261  elfzle2  10262  elfzle3  10264  uzsplit  10326  uzdisj  10327  uznfz  10337  elfz2nn0  10346  uzsubfz0  10363  nn0disj  10372  fzouzdisj  10416  fzoun  10417  elfzonelfzo  10474  infssuzex  10492  suprzubdc  10495  fldiv4lem1div2uz2  10565  mulp1mod1  10626  m1modge3gt1  10632  uzennn  10697  seq3split  10749  seq3f1olemqsumk  10773  seq3f1o  10778  seq3coll  11105  swrdlen2  11242  swrdfv2  11243  seq3shft  11398  cvg1nlemcau  11544  resqrexlemcvg  11579  resqrexlemga  11583  summodclem2a  11941  fsum3  11947  fsum3cvg3  11956  fsumadd  11966  sumsnf  11969  fsummulc2  12008  isumshft  12050  divcnv  12057  geolim2  12072  cvgratnnlemseq  12086  cvgratnnlemsumlt  12088  cvgratz  12092  mertenslemi1  12095  prodmodclem3  12135  prodmodclem2a  12136  fprodntrivap  12144  prodsnf  12152  fprodeq0  12177  efcllemp  12218  dvdsbnd  12526  uzwodc  12607  ncoprmgcdne1b  12660  isprm5  12713  hashdvds  12792  pcmpt2  12916  pcfaclem  12921  pcfac  12922  nninfdclemp1  13070  strext  13187  gsumfzval  13473  znidom  14670  lgslem1  15728  lgsdirprm  15762  lgseisen  15802  cvgcmp2nlemabs  16636  gsumgfsumlem  16683