Theorem flcld 13732

Description: The floor (greatest integer) function is an integer (closure law). (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
flcld.1	⊢ (𝜑 → 𝐴 ∈ ℝ)

Assertion

Ref	Expression
flcld	⊢ (𝜑 → (⌊‘𝐴) ∈ ℤ)

Proof of Theorem flcld

Step	Hyp	Ref	Expression
1		flcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		flcl 13729	. 2 ⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℤ)
3	1, 2	syl 17	1 ⊢ (𝜑 → (⌊‘𝐴) ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6502  ℝcr 11039  ℤcz 12502  ⌊cfl 13724

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-cnex 11096  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116  ax-pre-mulgt0 11117  ax-pre-sup 11118

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6269  df-ord 6330  df-on 6331  df-lim 6332  df-suc 6333  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-om 7821  df-2nd 7946  df-frecs 8235  df-wrecs 8266  df-recs 8315  df-rdg 8353  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-sup 9359  df-inf 9360  df-pnf 11182  df-mnf 11183  df-xr 11184  df-ltxr 11185  df-le 11186  df-sub 11380  df-neg 11381  df-nn 12160  df-n0 12416  df-z 12503  df-uz 12766  df-fl 13726

This theorem is referenced by:  flge  13739  flwordi  13746  flword2  13747  fladdz  13759  flhalf  13764  fldiv4p1lem1div2  13769  fldiv4lem1div2uz2  13770  fldiv4lem1div2  13771  ceicl  13775  quoremz  13789  intfracq  13793  fldiv  13794  moddiffl  13816  moddifz  13817  zmodcl  13825  modadd1  13842  modmuladd  13850  modmul1  13861  modsubdir  13877  iexpcyc  14144  absrdbnd  15279  limsupgre  15418  climrlim2  15484  dvdsmod  16270  divalgmod  16347  flodddiv4t2lthalf  16359  bitsp1  16372  bitsmod  16377  bitscmp  16379  bitsuz  16415  modgcd  16473  bezoutlem3  16482  isprm7  16649  hashdvds  16716  prmdiv  16726  odzdvds  16737  fldivp1  16839  pcfac  16841  pcbc  16842  prmreclem4  16861  vdwnnlem3  16939  mulgmodid  19060  odmod  19492  gexdvds  19530  zringlpirlem3  21436  zcld  24775  ovolunlem1a  25470  opnmbllem  25575  mbfi1fseqlem5  25693  dvfsumlem1  26005  dvfsumlem3  26008  sineq0  26506  efif1olem2  26525  ppiltx  27160  dvdsflf1o  27170  ppiub  27188  fsumvma2  27198  logfac2  27201  chpchtsum  27203  pcbcctr  27260  bposlem1  27268  bposlem3  27270  bposlem4  27271  bposlem5  27272  bposlem6  27273  gausslemma2dlem3  27352  gausslemma2dlem4  27353  gausslemma2dlem5  27355  lgseisenlem4  27362  lgseisen  27363  lgsquadlem1  27364  lgsquadlem2  27365  2lgslem1  27378  2lgslem2  27379  chebbnd1lem2  27454  chebbnd1lem3  27455  rplogsumlem2  27469  rpvmasumlem  27471  dchrisumlema  27472  dchrisumlem3  27475  dchrvmasumiflem1  27485  dchrisum0lem1  27500  rplogsum  27511  mulog2sumlem2  27519  pntrsumo1  27549  pntrlog2bndlem2  27562  pntrlog2bndlem4  27564  pntpbnd1  27570  pntpbnd2  27571  pntlemg  27582  pntlemq  27585  pntlemr  27586  pntlemf  27589  ostth2lem2  27618  dya2ub  34454  dya2icoseg  34461  dnibndlem13  36718  knoppndvlem19  36758  ltflcei  37888  opnmbllem0  37936  itg2addnclem2  37952  cntotbnd  38076  aks4d1p1p3  42468  aks4d1p1p2  42469  aks4d1p1p4  42470  aks4d1p3  42477  aks4d1p7d1  42481  aks4d1p7  42482  aks4d1p8  42486  aks4d1p9  42487  aks6d1c2lem4  42526  aks6d1c2  42529  aks6d1c6lem4  42572  aks6d1c7lem1  42579  aks6d1c7lem2  42580  irrapxlem1  43208  irrapxlem2  43209  irrapxlem3  43210  irrapxlem4  43211  pellexlem5  43219  pellfund14  43284  hashnzfz2  44706  hashnzfzclim  44707  sineq0ALT  45321  lefldiveq  45683  ltmod  46025  ioodvbdlimc1lem2  46319  ioodvbdlimc2lem  46321  dirkertrigeqlem3  46487  dirkertrigeq  46488  dirkercncflem4  46493  fourierdlem4  46498  fourierdlem7  46501  fourierdlem19  46513  fourierdlem26  46520  fourierdlem41  46535  fourierdlem47  46540  fourierdlem48  46541  fourierdlem49  46542  fourierdlem51  46544  fourierdlem63  46556  fourierdlem65  46558  fourierdlem71  46564  fourierdlem89  46582  fourierdlem90  46583  fourierdlem91  46584  ceilbi  47722  fldivmod  47727  modn0mul  47746  lighneallem2  47995  fllogbd  48949  fldivexpfllog2  48954  logbpw2m1  48956  fllog2  48957  nnpw2blen  48969  blen1b  48977  nnolog2flm1  48979  blennngt2o2  48981  blennn0e2  48983  digvalnn0  48988  dig2nn1st  48994  dig2nn0  49000  dig2bits  49003  dignn0flhalflem2  49005