Theorem flcld 13849

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6573  ℝcr 11183  ℤcz 12639  ⌊cfl 13841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-sup 9511  df-inf 9512  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-nn 12294  df-n0 12554  df-z 12640  df-uz 12904  df-fl 13843

This theorem is referenced by:  flge  13856  flwordi  13863  flword2  13864  fladdz  13876  flhalf  13881  fldiv4p1lem1div2  13886  fldiv4lem1div2uz2  13887  fldiv4lem1div2  13888  ceicl  13892  quoremz  13906  intfracq  13910  fldiv  13911  moddiffl  13933  moddifz  13934  zmodcl  13942  modadd1  13959  modmuladd  13964  modmul1  13975  modsubdir  13991  iexpcyc  14256  absrdbnd  15390  limsupgre  15527  climrlim2  15593  dvdsmod  16377  divalgmod  16454  flodddiv4t2lthalf  16464  bitsp1  16477  bitsmod  16482  bitscmp  16484  bitsuz  16520  modgcd  16579  bezoutlem3  16588  isprm7  16755  hashdvds  16822  prmdiv  16832  odzdvds  16842  fldivp1  16944  pcfac  16946  pcbc  16947  prmreclem4  16966  vdwnnlem3  17044  mulgmodid  19153  odmod  19588  gexdvds  19626  zringlpirlem3  21498  zcld  24854  ovolunlem1a  25550  opnmbllem  25655  mbfi1fseqlem5  25774  dvfsumlem1  26086  dvfsumlem3  26089  sineq0  26584  efif1olem2  26603  ppiltx  27238  dvdsflf1o  27248  ppiub  27266  fsumvma2  27276  logfac2  27279  chpchtsum  27281  pcbcctr  27338  bposlem1  27346  bposlem3  27348  bposlem4  27349  bposlem5  27350  bposlem6  27351  gausslemma2dlem3  27430  gausslemma2dlem4  27431  gausslemma2dlem5  27433  lgseisenlem4  27440  lgseisen  27441  lgsquadlem1  27442  lgsquadlem2  27443  2lgslem1  27456  2lgslem2  27457  chebbnd1lem2  27532  chebbnd1lem3  27533  rplogsumlem2  27547  rpvmasumlem  27549  dchrisumlema  27550  dchrisumlem3  27553  dchrvmasumiflem1  27563  dchrisum0lem1  27578  rplogsum  27589  mulog2sumlem2  27597  pntrsumo1  27627  pntrlog2bndlem2  27640  pntrlog2bndlem4  27642  pntpbnd1  27648  pntpbnd2  27649  pntlemg  27660  pntlemq  27663  pntlemr  27664  pntlemf  27667  ostth2lem2  27696  dya2ub  34235  dya2icoseg  34242  dnibndlem13  36456  knoppndvlem19  36496  ltflcei  37568  opnmbllem0  37616  itg2addnclem2  37632  cntotbnd  37756  aks4d1p1p3  42026  aks4d1p1p2  42027  aks4d1p1p4  42028  aks4d1p3  42035  aks4d1p7d1  42039  aks4d1p7  42040  aks4d1p8  42044  aks4d1p9  42045  aks6d1c2lem4  42084  aks6d1c2  42087  aks6d1c6lem4  42130  aks6d1c7lem1  42137  aks6d1c7lem2  42138  irrapxlem1  42778  irrapxlem2  42779  irrapxlem3  42780  irrapxlem4  42781  pellexlem5  42789  pellfund14  42854  hashnzfz2  44290  hashnzfzclim  44291  sineq0ALT  44908  lefldiveq  45207  ltmod  45559  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dirkertrigeqlem3  46021  dirkertrigeq  46022  dirkercncflem4  46027  fourierdlem4  46032  fourierdlem7  46035  fourierdlem19  46047  fourierdlem26  46054  fourierdlem41  46069  fourierdlem47  46074  fourierdlem48  46075  fourierdlem49  46076  fourierdlem51  46078  fourierdlem63  46090  fourierdlem65  46092  fourierdlem71  46098  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  lighneallem2  47480  fldivmod  48252  modn0mul  48254  fllogbd  48294  fldivexpfllog2  48299  logbpw2m1  48301  fllog2  48302  nnpw2blen  48314  blen1b  48322  nnolog2flm1  48324  blennngt2o2  48326  blennn0e2  48328  digvalnn0  48333  dig2nn1st  48339  dig2nn0  48345  dig2bits  48348  dignn0flhalflem2  48350