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

Theorem flcld 12419
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 12416 . 2 (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℤ)
31, 2syl 17 1 (𝜑 → (⌊‘𝐴) ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  cfv 5790  cr 9792  cz 11213  cfl 12411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4368  df-iun 4452  df-br 4579  df-opab 4639  df-mpt 4640  df-tr 4676  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6936  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-er 7607  df-en 7820  df-dom 7821  df-sdom 7822  df-sup 8209  df-inf 8210  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-nn 10871  df-n0 11143  df-z 11214  df-uz 11523  df-fl 12413
This theorem is referenced by:  flge  12426  flwordi  12433  flword2  12434  fladdz  12446  flhalf  12451  fldiv4p1lem1div2  12456  fldiv4lem1div2uz2  12457  fldiv4lem1div2  12458  ceicl  12462  quoremz  12474  intfracq  12478  fldiv  12479  moddiffl  12501  moddifz  12502  zmodcl  12510  modadd1  12527  modmuladd  12532  modmul1  12543  modsubdir  12559  iexpcyc  12789  absrdbnd  13878  limsupgre  14009  climrlim2  14075  dvdsmod  14837  divalgmod  14916  divalgmodOLD  14917  flodddiv4t2lthalf  14927  bitsp1  14940  bitsmod  14945  bitscmp  14947  bitsuz  14983  modgcd  15040  bezoutlem3  15045  isprm7  15207  hashdvds  15267  prmdiv  15277  odzdvds  15287  fldivp1  15388  pcfac  15390  pcbc  15391  prmreclem4  15410  vdwnnlem3  15488  mulgmodid  17353  odmod  17737  gexdvds  17771  zringlpirlem3  19602  zcld  22372  ovolunlem1a  23016  opnmbllem  23120  mbfi1fseqlem5  23237  dvfsumlem1  23538  dvfsumlem3  23540  sineq0  24022  efif1olem2  24038  ppiltx  24648  dvdsflf1o  24658  ppiub  24674  fsumvma2  24684  logfac2  24687  chpchtsum  24689  pcbcctr  24746  bposlem1  24754  bposlem3  24756  bposlem4  24757  bposlem5  24758  bposlem6  24759  gausslemma2dlem3  24838  gausslemma2dlem4  24839  gausslemma2dlem5  24841  lgseisenlem4  24848  lgseisen  24849  lgsquadlem1  24850  lgsquadlem2  24851  2lgslem1  24864  2lgslem2  24865  chebbnd1lem2  24904  chebbnd1lem3  24905  rplogsumlem2  24919  rpvmasumlem  24921  dchrisumlema  24922  dchrisumlem3  24925  dchrvmasumiflem1  24935  dchrisum0lem1  24950  rplogsum  24961  mulog2sumlem2  24969  pntrsumo1  24999  pntrlog2bndlem2  25012  pntrlog2bndlem4  25014  pntpbnd1  25020  pntpbnd2  25021  pntlemg  25032  pntlemq  25035  pntlemr  25036  pntlemf  25039  ostth2lem2  25068  dya2ub  29453  dya2icoseg  29460  dnibndlem13  31444  knoppndvlem19  31485  ltflcei  32361  opnmbllem0  32409  itg2addnclem2  32426  cntotbnd  32559  irrapxlem1  36198  irrapxlem2  36199  irrapxlem3  36200  irrapxlem4  36201  pellexlem5  36209  pellfund14  36274  hashnzfz2  37336  hashnzfzclim  37337  sineq0ALT  37989  lefldiveq  38240  ltmod  38499  ioodvbdlimc1lem2  38616  ioodvbdlimc2lem  38618  dirkertrigeqlem3  38787  dirkertrigeq  38788  dirkercncflem4  38793  fourierdlem4  38798  fourierdlem7  38801  fourierdlem19  38813  fourierdlem26  38820  fourierdlem41  38835  fourierdlem47  38840  fourierdlem48  38841  fourierdlem49  38842  fourierdlem51  38844  fourierdlem63  38856  fourierdlem65  38858  fourierdlem71  38864  fourierdlem89  38882  fourierdlem90  38883  fourierdlem91  38884  lighneallem2  39856  fldivmod  42099  modn0mul  42101  fllogbd  42144  fldivexpfllog2  42149  logbpw2m1  42151  fllog2  42152  nnpw2blen  42164  blen1b  42172  nnolog2flm1  42174  blennngt2o2  42176  blennn0e2  42178  digvalnn0  42183  dig2nn1st  42189  dig2nn0  42195  dig2bits  42198  dignn0flhalflem2  42200
  Copyright terms: Public domain W3C validator