Theorem uzid 9864

Description: Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.)

Assertion

Ref	Expression
uzid	⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

Proof of Theorem uzid

Step	Hyp	Ref	Expression
1		zre 9577	. . . 4 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
2	1	leidd 8784	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
3	2	ancli 323	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀))
4		eluz1 9853	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	3, 4	mpbird 167	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203   class class class wbr 4108  ‘cfv 5351   ≤ cle 8305  ℤcz 9573  ℤ_≥cuz 9849

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-in1 619  ax-in2 620  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-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-pr 4321  ax-un 4553  ax-setind 4658  ax-cnex 8214  ax-resscn 8215  ax-pre-ltirr 8235

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-rab 2529  df-v 2814  df-sbc 3042  df-dif 3212  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-br 4109  df-opab 4171  df-mpt 4172  df-id 4413  df-xp 4754  df-rel 4755  df-cnv 4756  df-co 4757  df-dm 4758  df-iota 5311  df-fun 5353  df-fv 5359  df-ov 6052  df-pnf 8306  df-mnf 8307  df-xr 8308  df-ltxr 8309  df-le 8310  df-neg 8443  df-z 9574  df-uz 9850

This theorem is referenced by:  uzidd  9865  uzn0  9866  uz11  9873  eluzfz1  10361  eluzfz2  10362  elfz3  10364  elfz1end  10385  fzssp1  10397  fzpred  10400  fzp1ss  10403  fzpr  10407  fztp  10408  elfz0add  10450  fzolb  10484  zpnn0elfzo  10548  fzosplitsnm1  10550  fzofzp1  10568  fzosplitsn  10574  fzostep1  10579  zsupcllemstep  10585  zsupcllemex  10586  frec2uzuzd  10760  frecuzrdgrrn  10766  frec2uzrdg  10767  frecuzrdgrcl  10768  frecuzrdgsuc  10772  frecuzrdgrclt  10773  frecuzrdgg  10774  frecuzrdgsuctlem  10781  uzsinds  10802  seq3val  10818  seqvalcd  10819  seq3-1  10820  seqf  10822  seq3p1  10823  seq3fveq  10837  seq3-1p  10848  seq3caopr3  10849  iseqf1olemjpcl  10866  iseqf1olemqpcl  10867  seq3f1oleml  10874  seq3f1o  10875  seq3homo  10885  faclbnd3  11101  bcm1k  11118  bcn2  11122  seq3coll  11207  swrds1  11353  pfxccatpfx2  11422  rexuz3  11668  r19.2uz  11671  resqrexlemcvg  11697  resqrexlemgt0  11698  resqrexlemoverl  11699  cau3lem  11792  caubnd2  11795  climconst  11968  climuni  11971  climcau  12025  serf0  12030  fsumparts  12149  isum1p  12171  isumrpcl  12173  cvgratz  12211  mertenslemi1  12214  ntrivcvgap0  12228  fprodabs  12295  eftlub  12369  bitsfzo  12634  bitsinv1  12641  ialgr0  12734  eucalg  12749  pw2dvds  12856  eulerthlemrprm  12919  oddprm  12950  pcfac  13041  pcbc  13042  ennnfonelem1  13147  gsumfzconst  14047  lmconst  15068  2logb9irr  15823  sqrt2cxp2logb9e3  15827  2logb9irrap  15829  lgseisenlem4  15933  lgsquadlem1  15937  lgsquad2  15943  cvgcmp2nlemabs  16803  trilpolemlt1  16812