Theorem eluzle 9233

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

Syntax hints:   → wi 4   ∈ wcel 1461   class class class wbr 3893  ‘cfv 5079   ≤ cle 7718  ℤcz 8951  ℤ_≥cuz 9221

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089  ax-cnex 7629  ax-resscn 7630

This theorem depends on definitions:  df-bi 116  df-3or 944  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-rab 2397  df-v 2657  df-sbc 2877  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-br 3894  df-opab 3948  df-mpt 3949  df-id 4173  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-rn 4508  df-res 4509  df-ima 4510  df-iota 5044  df-fun 5081  df-fn 5082  df-f 5083  df-fv 5087  df-ov 5729  df-neg 7852  df-z 8952  df-uz 9222

This theorem is referenced by:  uztrn  9237  uzneg  9239  uzss  9241  uz11  9243  eluzp1l  9245  uzm1  9251  uzin  9253  uzind4  9278  elfz5  9684  elfzle1  9693  elfzle2  9694  elfzle3  9696  uzsplit  9758  uzdisj  9759  uznfz  9769  elfz2nn0  9778  uzsubfz0  9792  nn0disj  9801  fzouzdisj  9843  elfzonelfzo  9893  mulp1mod1  10024  m1modge3gt1  10030  uzennn  10095  seq3split  10138  seq3f1olemqsumk  10158  seq3f1o  10163  seq3coll  10471  seq3shft  10496  cvg1nlemcau  10641  resqrexlemcvg  10676  resqrexlemga  10680  summodclem2a  11035  fsum3  11041  fsum3cvg3  11050  fsumadd  11060  sumsnf  11063  fsummulc2  11102  isumshft  11144  divcnv  11151  geolim2  11166  cvgratnnlemseq  11180  cvgratnnlemsumlt  11182  cvgratz  11186  mertenslemi1  11189  efcllemp  11208  infssuzex  11483  dvdsbnd  11486  ncoprmgcdne1b  11609  hashdvds  11735  cvgcmp2nlemabs  12904