Theorem flcld 12982

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

Syntax hints:   → wi 4   ∈ wcel 2051  ‘cfv 6186  ℝcr 10333  ℤcz 11792  ⌊cfl 12974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278  ax-cnex 10390  ax-resscn 10391  ax-1cn 10392  ax-icn 10393  ax-addcl 10394  ax-addrcl 10395  ax-mulcl 10396  ax-mulrcl 10397  ax-mulcom 10398  ax-addass 10399  ax-mulass 10400  ax-distr 10401  ax-i2m1 10402  ax-1ne0 10403  ax-1rid 10404  ax-rnegex 10405  ax-rrecex 10406  ax-cnre 10407  ax-pre-lttri 10408  ax-pre-lttrn 10409  ax-pre-ltadd 10410  ax-pre-mulgt0 10411  ax-pre-sup 10412

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-nel 3069  df-ral 3088  df-rex 3089  df-reu 3090  df-rmo 3091  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-pss 3840  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-tp 4441  df-op 4443  df-uni 4710  df-iun 4791  df-br 4927  df-opab 4989  df-mpt 5006  df-tr 5028  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6936  df-ov 6978  df-oprab 6979  df-mpo 6980  df-om 7396  df-wrecs 7749  df-recs 7811  df-rdg 7849  df-er 8088  df-en 8306  df-dom 8307  df-sdom 8308  df-sup 8700  df-inf 8701  df-pnf 10475  df-mnf 10476  df-xr 10477  df-ltxr 10478  df-le 10479  df-sub 10671  df-neg 10672  df-nn 11439  df-n0 11707  df-z 11793  df-uz 12058  df-fl 12976

This theorem is referenced by:  flge  12989  flwordi  12996  flword2  12997  fladdz  13009  flhalf  13014  fldiv4p1lem1div2  13019  fldiv4lem1div2uz2  13020  fldiv4lem1div2  13021  ceicl  13025  quoremz  13037  intfracq  13041  fldiv  13042  moddiffl  13064  moddifz  13065  zmodcl  13073  modadd1  13090  modmuladd  13095  modmul1  13106  modsubdir  13122  iexpcyc  13383  absrdbnd  14561  limsupgre  14698  climrlim2  14764  dvdsmod  15537  divalgmod  15616  flodddiv4t2lthalf  15626  bitsp1  15639  bitsmod  15644  bitscmp  15646  bitsuz  15682  modgcd  15739  bezoutlem3  15744  isprm7  15907  hashdvds  15967  prmdiv  15977  odzdvds  15987  fldivp1  16088  pcfac  16090  pcbc  16091  prmreclem4  16110  vdwnnlem3  16188  mulgmodid  18063  odmod  18449  gexdvds  18483  zringlpirlem3  20351  zcld  23140  ovolunlem1a  23816  opnmbllem  23921  mbfi1fseqlem5  24039  dvfsumlem1  24342  dvfsumlem3  24344  sineq0  24828  efif1olem2  24844  ppiltx  25472  dvdsflf1o  25482  ppiub  25498  fsumvma2  25508  logfac2  25511  chpchtsum  25513  pcbcctr  25570  bposlem1  25578  bposlem3  25580  bposlem4  25581  bposlem5  25582  bposlem6  25583  gausslemma2dlem3  25662  gausslemma2dlem4  25663  gausslemma2dlem5  25665  lgseisenlem4  25672  lgseisen  25673  lgsquadlem1  25674  lgsquadlem2  25675  2lgslem1  25688  2lgslem2  25689  chebbnd1lem2  25764  chebbnd1lem3  25765  rplogsumlem2  25779  rpvmasumlem  25781  dchrisumlema  25782  dchrisumlem3  25785  dchrvmasumiflem1  25795  dchrisum0lem1  25810  rplogsum  25821  mulog2sumlem2  25829  pntrsumo1  25859  pntrlog2bndlem2  25872  pntrlog2bndlem4  25874  pntpbnd1  25880  pntpbnd2  25881  pntlemg  25892  pntlemq  25895  pntlemr  25896  pntlemf  25899  ostth2lem2  25928  dya2ub  31206  dya2icoseg  31213  dnibndlem13  33382  knoppndvlem19  33422  ltflcei  34354  opnmbllem0  34402  itg2addnclem2  34418  cntotbnd  34549  irrapxlem1  38849  irrapxlem2  38850  irrapxlem3  38851  irrapxlem4  38852  pellexlem5  38860  pellfund14  38925  hashnzfz2  40103  hashnzfzclim  40104  sineq0ALT  40724  lefldiveq  41018  ltmod  41380  ioodvbdlimc1lem2  41677  ioodvbdlimc2lem  41679  dirkertrigeqlem3  41846  dirkertrigeq  41847  dirkercncflem4  41852  fourierdlem4  41857  fourierdlem7  41860  fourierdlem19  41872  fourierdlem26  41879  fourierdlem41  41894  fourierdlem47  41899  fourierdlem48  41900  fourierdlem49  41901  fourierdlem51  41903  fourierdlem63  41915  fourierdlem65  41917  fourierdlem71  41923  fourierdlem89  41941  fourierdlem90  41942  fourierdlem91  41943  lighneallem2  43169  fldivmod  43976  modn0mul  43978  fllogbd  44018  fldivexpfllog2  44023  logbpw2m1  44025  fllog2  44026  nnpw2blen  44038  blen1b  44046  nnolog2flm1  44048  blennngt2o2  44050  blennn0e2  44052  digvalnn0  44057  dig2nn1st  44063  dig2nn0  44069  dig2bits  44072  dignn0flhalflem2  44074