Theorem flcld 13827

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

Syntax hints:   → wi 4   ∈ wcel 2143  ‘cfv 6536  ℝcr 11094  ℤcz 12586  ⌊cfl 13819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172  ax-pre-sup 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-sup 9398  df-inf 9399  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-nn 12229  df-n0 12500  df-z 12587  df-uz 12858  df-fl 13821

This theorem is referenced by:  flge  13834  flwordi  13841  flword2  13842  fladdz  13854  flhalf  13859  fldiv4p1lem1div2  13864  fldiv4lem1div2uz2  13865  fldiv4lem1div2  13866  ceicl  13870  quoremz  13884  intfracq  13888  fldiv  13889  moddiffl  13911  moddifz  13912  zmodcl  13920  modadd1  13937  modmuladd  13945  modmul1  13956  modsubdir  13972  iexpcyc  14239  absrdbnd  15389  limsupgre  15528  climrlim2  15594  dvdsmod  16382  divalgmod  16459  flodddiv4t2lthalf  16471  bitsp1  16484  bitsmod  16489  bitscmp  16491  bitsuz  16527  modgcd  16585  bezoutlem3  16594  isprm7  16762  hashdvds  16829  prmdiv  16839  odzdvds  16850  fldivp1  16952  pcfac  16954  pcbc  16955  prmreclem4  16974  vdwnnlem3  17052  mulgmodid  19174  odmod  19611  gexdvds  19649  zringlpirlem3  21614  zcld  24971  ovolunlem1a  25655  opnmbllem  25760  mbfi1fseqlem5  25878  dvfsumlem1  26185  dvfsumlem3  26187  sineq0  26689  efif1olem2  26708  ppiltx  27341  dvdsflf1o  27351  ppiub  27368  fsumvma2  27378  logfac2  27381  chpchtsum  27383  pcbcctr  27440  bposlem1  27448  bposlem3  27450  bposlem4  27451  bposlem5  27452  bposlem6  27453  gausslemma2dlem3  27532  gausslemma2dlem4  27533  gausslemma2dlem5  27535  lgseisenlem4  27542  lgseisen  27543  lgsquadlem1  27544  lgsquadlem2  27545  2lgslem1  27558  2lgslem2  27559  chebbnd1lem2  27634  chebbnd1lem3  27635  rplogsumlem2  27649  rpvmasumlem  27651  dchrisumlema  27652  dchrisumlem3  27655  dchrvmasumiflem1  27665  dchrisum0lem1  27680  rplogsum  27691  mulog2sumlem2  27699  pntrsumo1  27729  pntrlog2bndlem2  27742  pntrlog2bndlem4  27744  pntpbnd1  27750  pntpbnd2  27751  pntlemg  27762  pntlemq  27765  pntlemr  27766  pntlemf  27769  ostth2lem2  27798  dya2ub  34660  dya2icoseg  34667  dnibndlem13  37099  knoppndvlem19  37139  ltflcei  38279  opnmbllem0  38327  itg2addnclem2  38343  cntotbnd  38467  aks4d1p1p3  42856  aks4d1p1p2  42857  aks4d1p1p4  42858  aks4d1p3  42865  aks4d1p7d1  42869  aks4d1p7  42870  aks4d1p8  42874  aks4d1p9  42875  aks6d1c2lem4  42914  aks6d1c2  42917  aks6d1c6lem4  42960  aks6d1c7lem1  42967  aks6d1c7lem2  42968  irrapxlem1  43569  irrapxlem2  43570  irrapxlem3  43571  irrapxlem4  43572  pellexlem5  43580  pellfund14  43645  hashnzfz2  45051  hashnzfzclim  45052  sineq0ALT  45665  lefldiveq  46031  ltmod  46372  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  dirkertrigeqlem3  46834  dirkertrigeq  46835  dirkercncflem4  46840  fourierdlem4  46845  fourierdlem7  46848  fourierdlem19  46860  fourierdlem26  46867  fourierdlem41  46882  fourierdlem47  46887  fourierdlem48  46888  fourierdlem49  46889  fourierdlem51  46891  fourierdlem63  46903  fourierdlem65  46905  fourierdlem71  46911  fourierdlem89  46929  fourierdlem90  46930  fourierdlem91  46931  ceilbi  48094  fldivmod  48101  modn0mul  48120  lighneallem2  48378  fllogbd  49360  fldivexpfllog2  49365  logbpw2m1  49367  fllog2  49368  nnpw2blen  49380  blen1b  49388  nnolog2flm1  49390  blennngt2o2  49392  blennn0e2  49394  digvalnn0  49399  dig2nn1st  49405  dig2nn0  49411  dig2bits  49414  dignn0flhalflem2  49416