MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  flcld Structured version   Visualization version   GIF version

Theorem flcld 12813
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
StepHypRef Expression
1 flcld.1 . 2 (𝜑𝐴 ∈ ℝ)
2 flcl 12810 . 2 (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℤ)
31, 2syl 17 1 (𝜑 → (⌊‘𝐴) ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  cfv 6049  cr 10147  cz 11589  cfl 12805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225  ax-pre-sup 10226
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-er 7913  df-en 8124  df-dom 8125  df-sdom 8126  df-sup 8515  df-inf 8516  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-nn 11233  df-n0 11505  df-z 11590  df-uz 11900  df-fl 12807
This theorem is referenced by:  flge  12820  flwordi  12827  flword2  12828  fladdz  12840  flhalf  12845  fldiv4p1lem1div2  12850  fldiv4lem1div2uz2  12851  fldiv4lem1div2  12852  ceicl  12856  quoremz  12868  intfracq  12872  fldiv  12873  moddiffl  12895  moddifz  12896  zmodcl  12904  modadd1  12921  modmuladd  12926  modmul1  12937  modsubdir  12953  iexpcyc  13183  absrdbnd  14300  limsupgre  14431  climrlim2  14497  dvdsmod  15272  divalgmod  15351  divalgmodOLD  15352  flodddiv4t2lthalf  15362  bitsp1  15375  bitsmod  15380  bitscmp  15382  bitsuz  15418  modgcd  15475  bezoutlem3  15480  isprm7  15642  hashdvds  15702  prmdiv  15712  odzdvds  15722  fldivp1  15823  pcfac  15825  pcbc  15826  prmreclem4  15845  vdwnnlem3  15923  mulgmodid  17802  odmod  18185  gexdvds  18219  zringlpirlem3  20056  zcld  22837  ovolunlem1a  23484  opnmbllem  23589  mbfi1fseqlem5  23705  dvfsumlem1  24008  dvfsumlem3  24010  sineq0  24493  efif1olem2  24509  ppiltx  25123  dvdsflf1o  25133  ppiub  25149  fsumvma2  25159  logfac2  25162  chpchtsum  25164  pcbcctr  25221  bposlem1  25229  bposlem3  25231  bposlem4  25232  bposlem5  25233  bposlem6  25234  gausslemma2dlem3  25313  gausslemma2dlem4  25314  gausslemma2dlem5  25316  lgseisenlem4  25323  lgseisen  25324  lgsquadlem1  25325  lgsquadlem2  25326  2lgslem1  25339  2lgslem2  25340  chebbnd1lem2  25379  chebbnd1lem3  25380  rplogsumlem2  25394  rpvmasumlem  25396  dchrisumlema  25397  dchrisumlem3  25400  dchrvmasumiflem1  25410  dchrisum0lem1  25425  rplogsum  25436  mulog2sumlem2  25444  pntrsumo1  25474  pntrlog2bndlem2  25487  pntrlog2bndlem4  25489  pntpbnd1  25495  pntpbnd2  25496  pntlemg  25507  pntlemq  25510  pntlemr  25511  pntlemf  25514  ostth2lem2  25543  dya2ub  30662  dya2icoseg  30669  dnibndlem13  32807  knoppndvlem19  32848  ltflcei  33728  opnmbllem0  33776  itg2addnclem2  33793  cntotbnd  33926  irrapxlem1  37906  irrapxlem2  37907  irrapxlem3  37908  irrapxlem4  37909  pellexlem5  37917  pellfund14  37982  hashnzfz2  39040  hashnzfzclim  39041  sineq0ALT  39690  lefldiveq  40022  ltmod  40391  ioodvbdlimc1lem2  40668  ioodvbdlimc2lem  40670  dirkertrigeqlem3  40838  dirkertrigeq  40839  dirkercncflem4  40844  fourierdlem4  40849  fourierdlem7  40852  fourierdlem19  40864  fourierdlem26  40871  fourierdlem41  40886  fourierdlem47  40891  fourierdlem48  40892  fourierdlem49  40893  fourierdlem51  40895  fourierdlem63  40907  fourierdlem65  40909  fourierdlem71  40915  fourierdlem89  40933  fourierdlem90  40934  fourierdlem91  40935  lighneallem2  42051  fldivmod  42841  modn0mul  42843  fllogbd  42882  fldivexpfllog2  42887  logbpw2m1  42889  fllog2  42890  nnpw2blen  42902  blen1b  42910  nnolog2flm1  42912  blennngt2o2  42914  blennn0e2  42916  digvalnn0  42921  dig2nn1st  42927  dig2nn0  42933  dig2bits  42936  dignn0flhalflem2  42938
  Copyright terms: Public domain W3C validator