Theorem flcld 13813

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 13810	. 2 ⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℤ)
3	1, 2	syl 17	1 ⊢ (𝜑 → (⌊‘𝐴) ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6530  ℝcr 11126  ℤcz 12586  ⌊cfl 13805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204  ax-pre-sup 11205

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-sup 9452  df-inf 9453  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-nn 12239  df-n0 12500  df-z 12587  df-uz 12851  df-fl 13807

This theorem is referenced by:  flge  13820  flwordi  13827  flword2  13828  fladdz  13840  flhalf  13845  fldiv4p1lem1div2  13850  fldiv4lem1div2uz2  13851  fldiv4lem1div2  13852  ceicl  13856  quoremz  13870  intfracq  13874  fldiv  13875  moddiffl  13897  moddifz  13898  zmodcl  13906  modadd1  13923  modmuladd  13929  modmul1  13940  modsubdir  13956  iexpcyc  14223  absrdbnd  15358  limsupgre  15495  climrlim2  15561  dvdsmod  16346  divalgmod  16423  flodddiv4t2lthalf  16435  bitsp1  16448  bitsmod  16453  bitscmp  16455  bitsuz  16491  modgcd  16549  bezoutlem3  16558  isprm7  16725  hashdvds  16792  prmdiv  16802  odzdvds  16813  fldivp1  16915  pcfac  16917  pcbc  16918  prmreclem4  16937  vdwnnlem3  17015  mulgmodid  19094  odmod  19525  gexdvds  19563  zringlpirlem3  21423  zcld  24751  ovolunlem1a  25447  opnmbllem  25552  mbfi1fseqlem5  25670  dvfsumlem1  25982  dvfsumlem3  25985  sineq0  26483  efif1olem2  26502  ppiltx  27137  dvdsflf1o  27147  ppiub  27165  fsumvma2  27175  logfac2  27178  chpchtsum  27180  pcbcctr  27237  bposlem1  27245  bposlem3  27247  bposlem4  27248  bposlem5  27249  bposlem6  27250  gausslemma2dlem3  27329  gausslemma2dlem4  27330  gausslemma2dlem5  27332  lgseisenlem4  27339  lgseisen  27340  lgsquadlem1  27341  lgsquadlem2  27342  2lgslem1  27355  2lgslem2  27356  chebbnd1lem2  27431  chebbnd1lem3  27432  rplogsumlem2  27446  rpvmasumlem  27448  dchrisumlema  27449  dchrisumlem3  27452  dchrvmasumiflem1  27462  dchrisum0lem1  27477  rplogsum  27488  mulog2sumlem2  27496  pntrsumo1  27526  pntrlog2bndlem2  27539  pntrlog2bndlem4  27541  pntpbnd1  27547  pntpbnd2  27548  pntlemg  27559  pntlemq  27562  pntlemr  27563  pntlemf  27566  ostth2lem2  27595  dya2ub  34248  dya2icoseg  34255  dnibndlem13  36454  knoppndvlem19  36494  ltflcei  37578  opnmbllem0  37626  itg2addnclem2  37642  cntotbnd  37766  aks4d1p1p3  42028  aks4d1p1p2  42029  aks4d1p1p4  42030  aks4d1p3  42037  aks4d1p7d1  42041  aks4d1p7  42042  aks4d1p8  42046  aks4d1p9  42047  aks6d1c2lem4  42086  aks6d1c2  42089  aks6d1c6lem4  42132  aks6d1c7lem1  42139  aks6d1c7lem2  42140  irrapxlem1  42792  irrapxlem2  42793  irrapxlem3  42794  irrapxlem4  42795  pellexlem5  42803  pellfund14  42868  hashnzfz2  44293  hashnzfzclim  44294  sineq0ALT  44909  lefldiveq  45269  ltmod  45615  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkercncflem4  46083  fourierdlem4  46088  fourierdlem7  46091  fourierdlem19  46103  fourierdlem26  46110  fourierdlem41  46125  fourierdlem47  46130  fourierdlem48  46131  fourierdlem49  46132  fourierdlem51  46134  fourierdlem63  46146  fourierdlem65  46148  fourierdlem71  46154  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  ceilbi  47310  fldivmod  47315  lighneallem2  47568  modn0mul  48448  fllogbd  48488  fldivexpfllog2  48493  logbpw2m1  48495  fllog2  48496  nnpw2blen  48508  blen1b  48516  nnolog2flm1  48518  blennngt2o2  48520  blennn0e2  48522  digvalnn0  48527  dig2nn1st  48533  dig2nn0  48539  dig2bits  48542  dignn0flhalflem2  48544