Theorem flcld 13808

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

Syntax hints:   → wi 4   ∈ wcel 2142  ‘cfv 6521  ℝcr 11072  ℤcz 12568  ⌊cfl 13800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150  ax-pre-sup 11151

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-sup 9388  df-inf 9389  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-nn 12211  df-n0 12482  df-z 12569  df-uz 12840  df-fl 13802

This theorem is referenced by:  flge  13815  flwordi  13822  flword2  13823  fladdz  13835  flhalf  13840  fldiv4p1lem1div2  13845  fldiv4lem1div2uz2  13846  fldiv4lem1div2  13847  ceicl  13851  quoremz  13865  intfracq  13869  fldiv  13870  moddiffl  13892  moddifz  13893  zmodcl  13901  modadd1  13918  modmuladd  13926  modmul1  13937  modsubdir  13953  iexpcyc  14220  absrdbnd  15369  limsupgre  15508  climrlim2  15574  dvdsmod  16363  divalgmod  16440  flodddiv4t2lthalf  16452  bitsp1  16465  bitsmod  16470  bitscmp  16472  bitsuz  16508  modgcd  16566  bezoutlem3  16575  isprm7  16743  hashdvds  16810  prmdiv  16820  odzdvds  16831  fldivp1  16933  pcfac  16935  pcbc  16936  prmreclem4  16955  vdwnnlem3  17033  mulgmodid  19155  odmod  19586  gexdvds  19624  zringlpirlem3  21516  zcld  24874  ovolunlem1a  25558  opnmbllem  25663  mbfi1fseqlem5  25781  dvfsumlem1  26088  dvfsumlem3  26090  sineq0  26589  efif1olem2  26608  ppiltx  27241  dvdsflf1o  27251  ppiub  27268  fsumvma2  27278  logfac2  27281  chpchtsum  27283  pcbcctr  27340  bposlem1  27348  bposlem3  27350  bposlem4  27351  bposlem5  27352  bposlem6  27353  gausslemma2dlem3  27432  gausslemma2dlem4  27433  gausslemma2dlem5  27435  lgseisenlem4  27442  lgseisen  27443  lgsquadlem1  27444  lgsquadlem2  27445  2lgslem1  27458  2lgslem2  27459  chebbnd1lem2  27534  chebbnd1lem3  27535  rplogsumlem2  27549  rpvmasumlem  27551  dchrisumlema  27552  dchrisumlem3  27555  dchrvmasumiflem1  27565  dchrisum0lem1  27580  rplogsum  27591  mulog2sumlem2  27599  pntrsumo1  27629  pntrlog2bndlem2  27642  pntrlog2bndlem4  27644  pntpbnd1  27650  pntpbnd2  27651  pntlemg  27662  pntlemq  27665  pntlemr  27666  pntlemf  27669  ostth2lem2  27698  dya2ub  34567  dya2icoseg  34574  dnibndlem13  36928  knoppndvlem19  36968  ltflcei  38107  opnmbllem0  38155  itg2addnclem2  38171  cntotbnd  38295  aks4d1p1p3  42686  aks4d1p1p2  42687  aks4d1p1p4  42688  aks4d1p3  42695  aks4d1p7d1  42699  aks4d1p7  42700  aks4d1p8  42704  aks4d1p9  42705  aks6d1c2lem4  42744  aks6d1c2  42747  aks6d1c6lem4  42790  aks6d1c7lem1  42797  aks6d1c7lem2  42798  irrapxlem1  43399  irrapxlem2  43400  irrapxlem3  43401  irrapxlem4  43402  pellexlem5  43410  pellfund14  43475  hashnzfz2  44897  hashnzfzclim  44898  sineq0ALT  45512  lefldiveq  45871  ltmod  46212  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  dirkertrigeqlem3  46674  dirkertrigeq  46675  dirkercncflem4  46680  fourierdlem4  46685  fourierdlem7  46688  fourierdlem19  46700  fourierdlem26  46707  fourierdlem41  46722  fourierdlem47  46727  fourierdlem48  46728  fourierdlem49  46729  fourierdlem51  46731  fourierdlem63  46743  fourierdlem65  46745  fourierdlem71  46751  fourierdlem89  46769  fourierdlem90  46770  fourierdlem91  46771  ceilbi  47931  fldivmod  47938  modn0mul  47957  lighneallem2  48215  fllogbd  49182  fldivexpfllog2  49187  logbpw2m1  49189  fllog2  49190  nnpw2blen  49202  blen1b  49210  nnolog2flm1  49212  blennngt2o2  49214  blennn0e2  49216  digvalnn0  49221  dig2nn1st  49227  dig2nn0  49233  dig2bits  49236  dignn0flhalflem2  49238