Theorem flcld 13838

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6561  ℝcr 11154  ℤcz 12613  ⌊cfl 13830

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 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-sup 9482  df-inf 9483  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-n0 12527  df-z 12614  df-uz 12879  df-fl 13832

This theorem is referenced by:  flge  13845  flwordi  13852  flword2  13853  fladdz  13865  flhalf  13870  fldiv4p1lem1div2  13875  fldiv4lem1div2uz2  13876  fldiv4lem1div2  13877  ceicl  13881  quoremz  13895  intfracq  13899  fldiv  13900  moddiffl  13922  moddifz  13923  zmodcl  13931  modadd1  13948  modmuladd  13954  modmul1  13965  modsubdir  13981  iexpcyc  14246  absrdbnd  15380  limsupgre  15517  climrlim2  15583  dvdsmod  16366  divalgmod  16443  flodddiv4t2lthalf  16455  bitsp1  16468  bitsmod  16473  bitscmp  16475  bitsuz  16511  modgcd  16569  bezoutlem3  16578  isprm7  16745  hashdvds  16812  prmdiv  16822  odzdvds  16833  fldivp1  16935  pcfac  16937  pcbc  16938  prmreclem4  16957  vdwnnlem3  17035  mulgmodid  19131  odmod  19564  gexdvds  19602  zringlpirlem3  21475  zcld  24835  ovolunlem1a  25531  opnmbllem  25636  mbfi1fseqlem5  25754  dvfsumlem1  26066  dvfsumlem3  26069  sineq0  26566  efif1olem2  26585  ppiltx  27220  dvdsflf1o  27230  ppiub  27248  fsumvma2  27258  logfac2  27261  chpchtsum  27263  pcbcctr  27320  bposlem1  27328  bposlem3  27330  bposlem4  27331  bposlem5  27332  bposlem6  27333  gausslemma2dlem3  27412  gausslemma2dlem4  27413  gausslemma2dlem5  27415  lgseisenlem4  27422  lgseisen  27423  lgsquadlem1  27424  lgsquadlem2  27425  2lgslem1  27438  2lgslem2  27439  chebbnd1lem2  27514  chebbnd1lem3  27515  rplogsumlem2  27529  rpvmasumlem  27531  dchrisumlema  27532  dchrisumlem3  27535  dchrvmasumiflem1  27545  dchrisum0lem1  27560  rplogsum  27571  mulog2sumlem2  27579  pntrsumo1  27609  pntrlog2bndlem2  27622  pntrlog2bndlem4  27624  pntpbnd1  27630  pntpbnd2  27631  pntlemg  27642  pntlemq  27645  pntlemr  27646  pntlemf  27649  ostth2lem2  27678  dya2ub  34272  dya2icoseg  34279  dnibndlem13  36491  knoppndvlem19  36531  ltflcei  37615  opnmbllem0  37663  itg2addnclem2  37679  cntotbnd  37803  aks4d1p1p3  42070  aks4d1p1p2  42071  aks4d1p1p4  42072  aks4d1p3  42079  aks4d1p7d1  42083  aks4d1p7  42084  aks4d1p8  42088  aks4d1p9  42089  aks6d1c2lem4  42128  aks6d1c2  42131  aks6d1c6lem4  42174  aks6d1c7lem1  42181  aks6d1c7lem2  42182  irrapxlem1  42833  irrapxlem2  42834  irrapxlem3  42835  irrapxlem4  42836  pellexlem5  42844  pellfund14  42909  hashnzfz2  44340  hashnzfzclim  44341  sineq0ALT  44957  lefldiveq  45304  ltmod  45653  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkercncflem4  46121  fourierdlem4  46126  fourierdlem7  46129  fourierdlem19  46141  fourierdlem26  46148  fourierdlem41  46163  fourierdlem47  46168  fourierdlem48  46169  fourierdlem49  46170  fourierdlem51  46172  fourierdlem63  46184  fourierdlem65  46186  fourierdlem71  46192  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fldivmod  47340  lighneallem2  47593  modn0mul  48441  fllogbd  48481  fldivexpfllog2  48486  logbpw2m1  48488  fllog2  48489  nnpw2blen  48501  blen1b  48509  nnolog2flm1  48511  blennngt2o2  48513  blennn0e2  48515  digvalnn0  48520  dig2nn1st  48526  dig2nn0  48532  dig2bits  48535  dignn0flhalflem2  48537