Theorem flcld 13763

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

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6544  ℝcr 11109  ℤcz 12558  ⌊cfl 13755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-sup 9437  df-inf 9438  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-n0 12473  df-z 12559  df-uz 12823  df-fl 13757

This theorem is referenced by:  flge  13770  flwordi  13777  flword2  13778  fladdz  13790  flhalf  13795  fldiv4p1lem1div2  13800  fldiv4lem1div2uz2  13801  fldiv4lem1div2  13802  ceicl  13806  quoremz  13820  intfracq  13824  fldiv  13825  moddiffl  13847  moddifz  13848  zmodcl  13856  modadd1  13873  modmuladd  13878  modmul1  13889  modsubdir  13905  iexpcyc  14171  absrdbnd  15288  limsupgre  15425  climrlim2  15491  dvdsmod  16272  divalgmod  16349  flodddiv4t2lthalf  16359  bitsp1  16372  bitsmod  16377  bitscmp  16379  bitsuz  16415  modgcd  16474  bezoutlem3  16483  isprm7  16645  hashdvds  16708  prmdiv  16718  odzdvds  16728  fldivp1  16830  pcfac  16832  pcbc  16833  prmreclem4  16852  vdwnnlem3  16930  mulgmodid  18993  odmod  19414  gexdvds  19452  zringlpirlem3  21034  zcld  24329  ovolunlem1a  25013  opnmbllem  25118  mbfi1fseqlem5  25237  dvfsumlem1  25543  dvfsumlem3  25545  sineq0  26033  efif1olem2  26052  ppiltx  26681  dvdsflf1o  26691  ppiub  26707  fsumvma2  26717  logfac2  26720  chpchtsum  26722  pcbcctr  26779  bposlem1  26787  bposlem3  26789  bposlem4  26790  bposlem5  26791  bposlem6  26792  gausslemma2dlem3  26871  gausslemma2dlem4  26872  gausslemma2dlem5  26874  lgseisenlem4  26881  lgseisen  26882  lgsquadlem1  26883  lgsquadlem2  26884  2lgslem1  26897  2lgslem2  26898  chebbnd1lem2  26973  chebbnd1lem3  26974  rplogsumlem2  26988  rpvmasumlem  26990  dchrisumlema  26991  dchrisumlem3  26994  dchrvmasumiflem1  27004  dchrisum0lem1  27019  rplogsum  27030  mulog2sumlem2  27038  pntrsumo1  27068  pntrlog2bndlem2  27081  pntrlog2bndlem4  27083  pntpbnd1  27089  pntpbnd2  27090  pntlemg  27101  pntlemq  27104  pntlemr  27105  pntlemf  27108  ostth2lem2  27137  dya2ub  33269  dya2icoseg  33276  dnibndlem13  35366  knoppndvlem19  35406  ltflcei  36476  opnmbllem0  36524  itg2addnclem2  36540  cntotbnd  36664  aks4d1p1p3  40934  aks4d1p1p2  40935  aks4d1p1p4  40936  aks4d1p3  40943  aks4d1p7d1  40947  aks4d1p7  40948  aks4d1p8  40952  aks4d1p9  40953  irrapxlem1  41560  irrapxlem2  41561  irrapxlem3  41562  irrapxlem4  41563  pellexlem5  41571  pellfund14  41636  hashnzfz2  43080  hashnzfzclim  43081  sineq0ALT  43698  lefldiveq  44002  ltmod  44354  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dirkertrigeqlem3  44816  dirkertrigeq  44817  dirkercncflem4  44822  fourierdlem4  44827  fourierdlem7  44830  fourierdlem19  44842  fourierdlem26  44849  fourierdlem41  44864  fourierdlem47  44869  fourierdlem48  44870  fourierdlem49  44871  fourierdlem51  44873  fourierdlem63  44885  fourierdlem65  44887  fourierdlem71  44893  fourierdlem89  44911  fourierdlem90  44912  fourierdlem91  44913  lighneallem2  46274  fldivmod  47204  modn0mul  47206  fllogbd  47246  fldivexpfllog2  47251  logbpw2m1  47253  fllog2  47254  nnpw2blen  47266  blen1b  47274  nnolog2flm1  47276  blennngt2o2  47278  blennn0e2  47280  digvalnn0  47285  dig2nn1st  47291  dig2nn0  47297  dig2bits  47300  dignn0flhalflem2  47302