Theorem uzid 9889

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 9601	. . . 4 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
2	1	leidd 8806	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
3	2	ancli 323	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀))
4		eluz1 9878	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	3, 4	mpbird 167	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205   class class class wbr 4114  ‘cfv 5357   ≤ cle 8325  ℤcz 9597  ℤ_≥cuz 9874

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 2207  ax-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327  ax-un 4559  ax-setind 4664  ax-cnex 8234  ax-resscn 8235  ax-pre-ltirr 8255

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 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-nel 2510  df-ral 2527  df-rex 2528  df-rab 2531  df-v 2817  df-sbc 3046  df-dif 3216  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-opab 4177  df-mpt 4178  df-id 4419  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-iota 5317  df-fun 5359  df-fv 5365  df-ov 6061  df-pnf 8326  df-mnf 8327  df-xr 8328  df-ltxr 8329  df-le 8330  df-neg 8464  df-z 9598  df-uz 9875

This theorem is referenced by:  uzidd  9890  uzn0  9891  uz11  9898  eluzfz1  10388  eluzfz2  10389  elfz3  10391  elfz1end  10413  fzssp1  10425  fzpred  10429  fzp1ss  10432  fzpr  10436  fztp  10437  elfz0add  10479  fzolb  10513  zpnn0elfzo  10577  fzosplitsnm1  10579  fzofzp1  10597  fzosplitsn  10603  fzostep1  10608  zsupcllemstep  10614  zsupcllemex  10615  frec2uzuzd  10791  frecuzrdgrrn  10797  frec2uzrdg  10798  frecuzrdgrcl  10799  frecuzrdgsuc  10803  frecuzrdgrclt  10804  frecuzrdgg  10805  frecuzrdgsuctlem  10812  uzsinds  10833  seq3val  10849  seqvalcd  10850  seq3-1  10851  seqf  10853  seq3p1  10854  seq3fveq  10868  seq3-1p  10879  seq3caopr3  10880  iseqf1olemjpcl  10897  iseqf1olemqpcl  10898  seq3f1oleml  10905  seq3f1o  10906  seq3homo  10916  faclbnd3  11133  bcm1k  11150  bcn2  11154  seq3coll  11242  swrds1  11388  pfxccatpfx2  11457  rexuz3  11703  r19.2uz  11706  resqrexlemcvg  11732  resqrexlemgt0  11733  resqrexlemoverl  11734  cau3lem  11827  caubnd2  11830  climconst  12003  climuni  12006  climcau  12060  serf0  12065  fsumparts  12184  isum1p  12206  isumrpcl  12208  cvgratz  12246  mertenslemi1  12249  ntrivcvgap0  12263  fprodabs  12330  eftlub  12404  bitsfzo  12669  bitsinv1  12676  ialgr0  12769  eucalg  12784  pw2dvds  12891  eulerthlemrprm  12954  oddprm  12985  pcfac  13076  pcbc  13077  ballotfilemfp1  13178  ennnfonelem1  13245  gsumfzconst  14097  lmconst  15210  2logb9irr  15965  sqrt2cxp2logb9e3  15969  2logb9irrap  15971  lgseisenlem4  16075  lgsquadlem1  16079  lgsquad2  16085  cvgcmp2nlemabs  16955  trilpolemlt1  16964