Theorem uzid 9874

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205   class class class wbr 4111  ‘cfv 5354   ≤ cle 8314  ℤcz 9582  ℤ_≥cuz 9859

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 4230  ax-pow 4289  ax-pr 4324  ax-un 4556  ax-setind 4661  ax-cnex 8223  ax-resscn 8224  ax-pre-ltirr 8244

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 3045  df-dif 3215  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-opab 4174  df-mpt 4175  df-id 4416  df-xp 4757  df-rel 4758  df-cnv 4759  df-co 4760  df-dm 4761  df-iota 5314  df-fun 5356  df-fv 5362  df-ov 6055  df-pnf 8315  df-mnf 8316  df-xr 8317  df-ltxr 8318  df-le 8319  df-neg 8452  df-z 9583  df-uz 9860

This theorem is referenced by:  uzidd  9875  uzn0  9876  uz11  9883  eluzfz1  10371  eluzfz2  10372  elfz3  10374  elfz1end  10395  fzssp1  10407  fzpred  10411  fzp1ss  10414  fzpr  10418  fztp  10419  elfz0add  10461  fzolb  10495  zpnn0elfzo  10559  fzosplitsnm1  10561  fzofzp1  10579  fzosplitsn  10585  fzostep1  10590  zsupcllemstep  10596  zsupcllemex  10597  frec2uzuzd  10771  frecuzrdgrrn  10777  frec2uzrdg  10778  frecuzrdgrcl  10779  frecuzrdgsuc  10783  frecuzrdgrclt  10784  frecuzrdgg  10785  frecuzrdgsuctlem  10792  uzsinds  10813  seq3val  10829  seqvalcd  10830  seq3-1  10831  seqf  10833  seq3p1  10834  seq3fveq  10848  seq3-1p  10859  seq3caopr3  10860  iseqf1olemjpcl  10877  iseqf1olemqpcl  10878  seq3f1oleml  10885  seq3f1o  10886  seq3homo  10896  faclbnd3  11113  bcm1k  11130  bcn2  11134  seq3coll  11222  swrds1  11368  pfxccatpfx2  11437  rexuz3  11683  r19.2uz  11686  resqrexlemcvg  11712  resqrexlemgt0  11713  resqrexlemoverl  11714  cau3lem  11807  caubnd2  11810  climconst  11983  climuni  11986  climcau  12040  serf0  12045  fsumparts  12164  isum1p  12186  isumrpcl  12188  cvgratz  12226  mertenslemi1  12229  ntrivcvgap0  12243  fprodabs  12310  eftlub  12384  bitsfzo  12649  bitsinv1  12656  ialgr0  12749  eucalg  12764  pw2dvds  12871  eulerthlemrprm  12934  oddprm  12965  pcfac  13056  pcbc  13057  ballotfilemfp1  13156  ennnfonelem1  13179  gsumfzconst  14079  lmconst  15130  2logb9irr  15885  sqrt2cxp2logb9e3  15889  2logb9irrap  15891  lgseisenlem4  15995  lgsquadlem1  15999  lgsquad2  16005  cvgcmp2nlemabs  16865  trilpolemlt1  16874