Theorem flcld 13446

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6418  ℝcr 10801  ℤcz 12249  ⌊cfl 13438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879  ax-pre-sup 10880

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-sup 9131  df-inf 9132  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-nn 11904  df-n0 12164  df-z 12250  df-uz 12512  df-fl 13440

This theorem is referenced by:  flge  13453  flwordi  13460  flword2  13461  fladdz  13473  flhalf  13478  fldiv4p1lem1div2  13483  fldiv4lem1div2uz2  13484  fldiv4lem1div2  13485  ceicl  13489  quoremz  13503  intfracq  13507  fldiv  13508  moddiffl  13530  moddifz  13531  zmodcl  13539  modadd1  13556  modmuladd  13561  modmul1  13572  modsubdir  13588  iexpcyc  13851  absrdbnd  14981  limsupgre  15118  climrlim2  15184  dvdsmod  15966  divalgmod  16043  flodddiv4t2lthalf  16053  bitsp1  16066  bitsmod  16071  bitscmp  16073  bitsuz  16109  modgcd  16168  bezoutlem3  16177  isprm7  16341  hashdvds  16404  prmdiv  16414  odzdvds  16424  fldivp1  16526  pcfac  16528  pcbc  16529  prmreclem4  16548  vdwnnlem3  16626  mulgmodid  18657  odmod  19069  gexdvds  19104  zringlpirlem3  20598  zcld  23882  ovolunlem1a  24565  opnmbllem  24670  mbfi1fseqlem5  24789  dvfsumlem1  25095  dvfsumlem3  25097  sineq0  25585  efif1olem2  25604  ppiltx  26231  dvdsflf1o  26241  ppiub  26257  fsumvma2  26267  logfac2  26270  chpchtsum  26272  pcbcctr  26329  bposlem1  26337  bposlem3  26339  bposlem4  26340  bposlem5  26341  bposlem6  26342  gausslemma2dlem3  26421  gausslemma2dlem4  26422  gausslemma2dlem5  26424  lgseisenlem4  26431  lgseisen  26432  lgsquadlem1  26433  lgsquadlem2  26434  2lgslem1  26447  2lgslem2  26448  chebbnd1lem2  26523  chebbnd1lem3  26524  rplogsumlem2  26538  rpvmasumlem  26540  dchrisumlema  26541  dchrisumlem3  26544  dchrvmasumiflem1  26554  dchrisum0lem1  26569  rplogsum  26580  mulog2sumlem2  26588  pntrsumo1  26618  pntrlog2bndlem2  26631  pntrlog2bndlem4  26633  pntpbnd1  26639  pntpbnd2  26640  pntlemg  26651  pntlemq  26654  pntlemr  26655  pntlemf  26658  ostth2lem2  26687  dya2ub  32137  dya2icoseg  32144  dnibndlem13  34597  knoppndvlem19  34637  ltflcei  35692  opnmbllem0  35740  itg2addnclem2  35756  cntotbnd  35881  aks4d1p1p3  40005  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p3  40014  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8  40023  aks4d1p9  40024  irrapxlem1  40560  irrapxlem2  40561  irrapxlem3  40562  irrapxlem4  40563  pellexlem5  40571  pellfund14  40636  hashnzfz2  41828  hashnzfzclim  41829  sineq0ALT  42446  lefldiveq  42721  ltmod  43069  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dirkertrigeqlem3  43531  dirkertrigeq  43532  dirkercncflem4  43537  fourierdlem4  43542  fourierdlem7  43545  fourierdlem19  43557  fourierdlem26  43564  fourierdlem41  43579  fourierdlem47  43584  fourierdlem48  43585  fourierdlem49  43586  fourierdlem51  43588  fourierdlem63  43600  fourierdlem65  43602  fourierdlem71  43608  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  lighneallem2  44946  fldivmod  45752  modn0mul  45754  fllogbd  45794  fldivexpfllog2  45799  logbpw2m1  45801  fllog2  45802  nnpw2blen  45814  blen1b  45822  nnolog2flm1  45824  blennngt2o2  45826  blennn0e2  45828  digvalnn0  45833  dig2nn1st  45839  dig2nn0  45845  dig2bits  45848  dignn0flhalflem2  45850