Theorem uzid 9953

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209   class class class wbr 4131  ‘cfv 5380   ≤ cle 8368  ℤcz 9656  ℤ_≥cuz 9938

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-cnex 8277  ax-resscn 8278  ax-pre-ltirr 8298

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-mpt 4195  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-iota 5340  df-fun 5382  df-fv 5388  df-ov 6091  df-pnf 8369  df-mnf 8370  df-xr 8371  df-ltxr 8372  df-le 8373  df-neg 8508  df-z 9657  df-uz 9939

This theorem is used by:  uzidd  9954  uzn0  9955  uz11  9962  eluzfz1  10453  eluzfz2  10454  elfz3  10456  elfz1end  10479  fzssp1  10491  fzpred  10495  fzp1ss  10498  fzpr  10502  fztp  10503  elfz0add  10545  fzolb  10579  zpnn0elfzo  10643  fzosplitsnm1  10645  fzofzp1  10663  fzosplitsn  10669  fzostep1  10674  zsupcllemstep  10680  zsupcllemex  10681  frec2uzuzd  10861  frecuzrdgrrn  10867  frec2uzrdg  10868  frecuzrdgrcl  10869  frecuzrdgsuc  10873  frecuzrdgrclt  10874  frecuzrdgg  10875  frecuzrdgsuctlem  10882  uzsinds  10903  seq3val  10919  seqvalcd  10920  seq3-1  10921  seqf  10923  seq3p1  10924  seq3fveq  10938  seq3-1p  10949  seq3caopr3  10950  iseqf1olemjpcl  10967  iseqf1olemqpcl  10968  seq3f1oleml  10975  seq3f1o  10976  seq3homo  10986  faclbnd3  11204  bcm1k  11221  bcn2  11225  seq3coll  11317  swrds1  11463  pfxccatpfx2  11532  rexuz3  11779  r19.2uz  11782  resqrexlemcvg  11808  resqrexlemgt0  11809  resqrexlemoverl  11810  cau3lem  11904  caubnd2  11907  climconst  12082  climuni  12085  climcau  12139  serf0  12144  fsumparts  12263  isum1p  12285  isumrpcl  12287  cvgratz  12325  mertenslemi1  12328  ntrivcvgap0  12342  fprodabs  12409  eftlub  12483  bitsfzo  12748  bitsinv1  12755  ialgr0  12848  eucalg  12863  oddpwdc  12980  eulerthlemrprm  13037  oddprm  13068  pcfac  13159  pcbc  13160  prmlem0  13250  ballotfilemfp1  13290  ennnfonelem1  13357  gzsumconst  14234  lmconst  15454  2logb9irr  16219  sqrt2cxp2logb9e3  16223  2logb9irrap  16225  ppinprm  16272  chtnprm  16274  ppiublem1  16303  chtqub  16308  bposlem6  16328  lgseisenlem4  16409  lgsquadlem1  16413  lgsquad2  16419  cvgcmp2nlemabs  17299  trilpolemlt1  17309