Theorem flcld 13736

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6499  ℝcr 11043  ℤcz 12505  ⌊cfl 13728

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121  ax-pre-sup 11122

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-sup 9369  df-inf 9370  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-nn 12163  df-n0 12419  df-z 12506  df-uz 12770  df-fl 13730

This theorem is referenced by:  flge  13743  flwordi  13750  flword2  13751  fladdz  13763  flhalf  13768  fldiv4p1lem1div2  13773  fldiv4lem1div2uz2  13774  fldiv4lem1div2  13775  ceicl  13779  quoremz  13793  intfracq  13797  fldiv  13798  moddiffl  13820  moddifz  13821  zmodcl  13829  modadd1  13846  modmuladd  13854  modmul1  13865  modsubdir  13881  iexpcyc  14148  absrdbnd  15284  limsupgre  15423  climrlim2  15489  dvdsmod  16275  divalgmod  16352  flodddiv4t2lthalf  16364  bitsp1  16377  bitsmod  16382  bitscmp  16384  bitsuz  16420  modgcd  16478  bezoutlem3  16487  isprm7  16654  hashdvds  16721  prmdiv  16731  odzdvds  16742  fldivp1  16844  pcfac  16846  pcbc  16847  prmreclem4  16866  vdwnnlem3  16944  mulgmodid  19027  odmod  19460  gexdvds  19498  zringlpirlem3  21406  zcld  24735  ovolunlem1a  25430  opnmbllem  25535  mbfi1fseqlem5  25653  dvfsumlem1  25965  dvfsumlem3  25968  sineq0  26466  efif1olem2  26485  ppiltx  27120  dvdsflf1o  27130  ppiub  27148  fsumvma2  27158  logfac2  27161  chpchtsum  27163  pcbcctr  27220  bposlem1  27228  bposlem3  27230  bposlem4  27231  bposlem5  27232  bposlem6  27233  gausslemma2dlem3  27312  gausslemma2dlem4  27313  gausslemma2dlem5  27315  lgseisenlem4  27322  lgseisen  27323  lgsquadlem1  27324  lgsquadlem2  27325  2lgslem1  27338  2lgslem2  27339  chebbnd1lem2  27414  chebbnd1lem3  27415  rplogsumlem2  27429  rpvmasumlem  27431  dchrisumlema  27432  dchrisumlem3  27435  dchrvmasumiflem1  27445  dchrisum0lem1  27460  rplogsum  27471  mulog2sumlem2  27479  pntrsumo1  27509  pntrlog2bndlem2  27522  pntrlog2bndlem4  27524  pntpbnd1  27530  pntpbnd2  27531  pntlemg  27542  pntlemq  27545  pntlemr  27546  pntlemf  27549  ostth2lem2  27578  dya2ub  34254  dya2icoseg  34261  dnibndlem13  36471  knoppndvlem19  36511  ltflcei  37595  opnmbllem0  37643  itg2addnclem2  37659  cntotbnd  37783  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p3  42059  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8  42068  aks4d1p9  42069  aks6d1c2lem4  42108  aks6d1c2  42111  aks6d1c6lem4  42154  aks6d1c7lem1  42161  aks6d1c7lem2  42162  irrapxlem1  42803  irrapxlem2  42804  irrapxlem3  42805  irrapxlem4  42806  pellexlem5  42814  pellfund14  42879  hashnzfz2  44303  hashnzfzclim  44304  sineq0ALT  44919  lefldiveq  45283  ltmod  45629  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dirkertrigeqlem3  46091  dirkertrigeq  46092  dirkercncflem4  46097  fourierdlem4  46102  fourierdlem7  46105  fourierdlem19  46117  fourierdlem26  46124  fourierdlem41  46139  fourierdlem47  46144  fourierdlem48  46145  fourierdlem49  46146  fourierdlem51  46148  fourierdlem63  46160  fourierdlem65  46162  fourierdlem71  46168  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  ceilbi  47327  fldivmod  47332  modn0mul  47351  lighneallem2  47600  fllogbd  48542  fldivexpfllog2  48547  logbpw2m1  48549  fllog2  48550  nnpw2blen  48562  blen1b  48570  nnolog2flm1  48572  blennngt2o2  48574  blennn0e2  48576  digvalnn0  48581  dig2nn1st  48587  dig2nn0  48593  dig2bits  48596  dignn0flhalflem2  48598