Theorem flcld 13770

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

Syntax hints:   → wi 4   ∈ wcel 2105  ‘cfv 6543  ℝcr 11115  ℤcz 12565  ⌊cfl 13762

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11172  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192  ax-pre-mulgt0 11193  ax-pre-sup 11194

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-2nd 7980  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-er 8709  df-en 8946  df-dom 8947  df-sdom 8948  df-sup 9443  df-inf 9444  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261  df-sub 11453  df-neg 11454  df-nn 12220  df-n0 12480  df-z 12566  df-uz 12830  df-fl 13764

This theorem is referenced by:  flge  13777  flwordi  13784  flword2  13785  fladdz  13797  flhalf  13802  fldiv4p1lem1div2  13807  fldiv4lem1div2uz2  13808  fldiv4lem1div2  13809  ceicl  13813  quoremz  13827  intfracq  13831  fldiv  13832  moddiffl  13854  moddifz  13855  zmodcl  13863  modadd1  13880  modmuladd  13885  modmul1  13896  modsubdir  13912  iexpcyc  14178  absrdbnd  15295  limsupgre  15432  climrlim2  15498  dvdsmod  16279  divalgmod  16356  flodddiv4t2lthalf  16366  bitsp1  16379  bitsmod  16384  bitscmp  16386  bitsuz  16422  modgcd  16481  bezoutlem3  16490  isprm7  16652  hashdvds  16715  prmdiv  16725  odzdvds  16735  fldivp1  16837  pcfac  16839  pcbc  16840  prmreclem4  16859  vdwnnlem3  16937  mulgmodid  19036  odmod  19462  gexdvds  19500  zringlpirlem3  21323  zcld  24648  ovolunlem1a  25344  opnmbllem  25449  mbfi1fseqlem5  25568  dvfsumlem1  25879  dvfsumlem3  25882  sineq0  26372  efif1olem2  26391  ppiltx  27021  dvdsflf1o  27031  ppiub  27049  fsumvma2  27059  logfac2  27062  chpchtsum  27064  pcbcctr  27121  bposlem1  27129  bposlem3  27131  bposlem4  27132  bposlem5  27133  bposlem6  27134  gausslemma2dlem3  27213  gausslemma2dlem4  27214  gausslemma2dlem5  27216  lgseisenlem4  27223  lgseisen  27224  lgsquadlem1  27225  lgsquadlem2  27226  2lgslem1  27239  2lgslem2  27240  chebbnd1lem2  27315  chebbnd1lem3  27316  rplogsumlem2  27330  rpvmasumlem  27332  dchrisumlema  27333  dchrisumlem3  27336  dchrvmasumiflem1  27346  dchrisum0lem1  27361  rplogsum  27372  mulog2sumlem2  27380  pntrsumo1  27410  pntrlog2bndlem2  27423  pntrlog2bndlem4  27425  pntpbnd1  27431  pntpbnd2  27432  pntlemg  27443  pntlemq  27446  pntlemr  27447  pntlemf  27450  ostth2lem2  27479  dya2ub  33732  dya2icoseg  33739  dnibndlem13  35829  knoppndvlem19  35869  ltflcei  36939  opnmbllem0  36987  itg2addnclem2  37003  cntotbnd  37127  aks4d1p1p3  41400  aks4d1p1p2  41401  aks4d1p1p4  41402  aks4d1p3  41409  aks4d1p7d1  41413  aks4d1p7  41414  aks4d1p8  41418  aks4d1p9  41419  irrapxlem1  42022  irrapxlem2  42023  irrapxlem3  42024  irrapxlem4  42025  pellexlem5  42033  pellfund14  42098  hashnzfz2  43542  hashnzfzclim  43543  sineq0ALT  44160  lefldiveq  44460  ltmod  44812  ioodvbdlimc1lem2  45106  ioodvbdlimc2lem  45108  dirkertrigeqlem3  45274  dirkertrigeq  45275  dirkercncflem4  45280  fourierdlem4  45285  fourierdlem7  45288  fourierdlem19  45300  fourierdlem26  45307  fourierdlem41  45322  fourierdlem47  45327  fourierdlem48  45328  fourierdlem49  45329  fourierdlem51  45331  fourierdlem63  45343  fourierdlem65  45345  fourierdlem71  45351  fourierdlem89  45369  fourierdlem90  45370  fourierdlem91  45371  lighneallem2  46732  fldivmod  47365  modn0mul  47367  fllogbd  47407  fldivexpfllog2  47412  logbpw2m1  47414  fllog2  47415  nnpw2blen  47427  blen1b  47435  nnolog2flm1  47437  blennngt2o2  47439  blennn0e2  47441  digvalnn0  47446  dig2nn1st  47452  dig2nn0  47458  dig2bits  47461  dignn0flhalflem2  47463