Theorem flcld 13751

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6493  ℝcr 11031  ℤcz 12518  ⌊cfl 13743

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 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109  ax-pre-sup 11110

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 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-sup 9349  df-inf 9350  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-nn 12169  df-n0 12432  df-z 12519  df-uz 12783  df-fl 13745

This theorem is referenced by:  flge  13758  flwordi  13765  flword2  13766  fladdz  13778  flhalf  13783  fldiv4p1lem1div2  13788  fldiv4lem1div2uz2  13789  fldiv4lem1div2  13790  ceicl  13794  quoremz  13808  intfracq  13812  fldiv  13813  moddiffl  13835  moddifz  13836  zmodcl  13844  modadd1  13861  modmuladd  13869  modmul1  13880  modsubdir  13896  iexpcyc  14163  absrdbnd  15298  limsupgre  15437  climrlim2  15503  dvdsmod  16292  divalgmod  16369  flodddiv4t2lthalf  16381  bitsp1  16394  bitsmod  16399  bitscmp  16401  bitsuz  16437  modgcd  16495  bezoutlem3  16504  isprm7  16672  hashdvds  16739  prmdiv  16749  odzdvds  16760  fldivp1  16862  pcfac  16864  pcbc  16865  prmreclem4  16884  vdwnnlem3  16962  mulgmodid  19083  odmod  19515  gexdvds  19553  zringlpirlem3  21457  zcld  24792  ovolunlem1a  25476  opnmbllem  25581  mbfi1fseqlem5  25699  dvfsumlem1  26006  dvfsumlem3  26008  sineq0  26504  efif1olem2  26523  ppiltx  27157  dvdsflf1o  27167  ppiub  27184  fsumvma2  27194  logfac2  27197  chpchtsum  27199  pcbcctr  27256  bposlem1  27264  bposlem3  27266  bposlem4  27267  bposlem5  27268  bposlem6  27269  gausslemma2dlem3  27348  gausslemma2dlem4  27349  gausslemma2dlem5  27351  lgseisenlem4  27358  lgseisen  27359  lgsquadlem1  27360  lgsquadlem2  27361  2lgslem1  27374  2lgslem2  27375  chebbnd1lem2  27450  chebbnd1lem3  27451  rplogsumlem2  27465  rpvmasumlem  27467  dchrisumlema  27468  dchrisumlem3  27471  dchrvmasumiflem1  27481  dchrisum0lem1  27496  rplogsum  27507  mulog2sumlem2  27515  pntrsumo1  27545  pntrlog2bndlem2  27558  pntrlog2bndlem4  27560  pntpbnd1  27566  pntpbnd2  27567  pntlemg  27578  pntlemq  27581  pntlemr  27582  pntlemf  27585  ostth2lem2  27614  dya2ub  34433  dya2icoseg  34440  dnibndlem13  36769  knoppndvlem19  36809  ltflcei  37946  opnmbllem0  37994  itg2addnclem2  38010  cntotbnd  38134  aks4d1p1p3  42525  aks4d1p1p2  42526  aks4d1p1p4  42527  aks4d1p3  42534  aks4d1p7d1  42538  aks4d1p7  42539  aks4d1p8  42543  aks4d1p9  42544  aks6d1c2lem4  42583  aks6d1c2  42586  aks6d1c6lem4  42629  aks6d1c7lem1  42636  aks6d1c7lem2  42637  irrapxlem1  43271  irrapxlem2  43272  irrapxlem3  43273  irrapxlem4  43274  pellexlem5  43282  pellfund14  43347  hashnzfz2  44769  hashnzfzclim  44770  sineq0ALT  45384  lefldiveq  45746  ltmod  46087  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  dirkertrigeqlem3  46549  dirkertrigeq  46550  dirkercncflem4  46555  fourierdlem4  46560  fourierdlem7  46563  fourierdlem19  46575  fourierdlem26  46582  fourierdlem41  46597  fourierdlem47  46602  fourierdlem48  46603  fourierdlem49  46604  fourierdlem51  46606  fourierdlem63  46618  fourierdlem65  46620  fourierdlem71  46626  fourierdlem89  46644  fourierdlem90  46645  fourierdlem91  46646  ceilbi  47800  fldivmod  47807  modn0mul  47826  lighneallem2  48084  fllogbd  49051  fldivexpfllog2  49056  logbpw2m1  49058  fllog2  49059  nnpw2blen  49071  blen1b  49079  nnolog2flm1  49081  blennngt2o2  49083  blennn0e2  49085  digvalnn0  49090  dig2nn1st  49096  dig2nn0  49102  dig2bits  49105  dignn0flhalflem2  49107