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

Theorem flcld 13373
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 13370 . 2 (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℤ)
31, 2syl 17 1 (𝜑 → (⌊‘𝐴) ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2110  cfv 6380  cr 10728  cz 12176  cfl 13365
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-sup 9058  df-inf 9059  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-nn 11831  df-n0 12091  df-z 12177  df-uz 12439  df-fl 13367
This theorem is referenced by:  flge  13380  flwordi  13387  flword2  13388  fladdz  13400  flhalf  13405  fldiv4p1lem1div2  13410  fldiv4lem1div2uz2  13411  fldiv4lem1div2  13412  ceicl  13416  quoremz  13428  intfracq  13432  fldiv  13433  moddiffl  13455  moddifz  13456  zmodcl  13464  modadd1  13481  modmuladd  13486  modmul1  13497  modsubdir  13513  iexpcyc  13775  absrdbnd  14905  limsupgre  15042  climrlim2  15108  dvdsmod  15890  divalgmod  15967  flodddiv4t2lthalf  15977  bitsp1  15990  bitsmod  15995  bitscmp  15997  bitsuz  16033  modgcd  16092  bezoutlem3  16101  isprm7  16265  hashdvds  16328  prmdiv  16338  odzdvds  16348  fldivp1  16450  pcfac  16452  pcbc  16453  prmreclem4  16472  vdwnnlem3  16550  mulgmodid  18530  odmod  18938  gexdvds  18973  zringlpirlem3  20451  zcld  23710  ovolunlem1a  24393  opnmbllem  24498  mbfi1fseqlem5  24617  dvfsumlem1  24923  dvfsumlem3  24925  sineq0  25413  efif1olem2  25432  ppiltx  26059  dvdsflf1o  26069  ppiub  26085  fsumvma2  26095  logfac2  26098  chpchtsum  26100  pcbcctr  26157  bposlem1  26165  bposlem3  26167  bposlem4  26168  bposlem5  26169  bposlem6  26170  gausslemma2dlem3  26249  gausslemma2dlem4  26250  gausslemma2dlem5  26252  lgseisenlem4  26259  lgseisen  26260  lgsquadlem1  26261  lgsquadlem2  26262  2lgslem1  26275  2lgslem2  26276  chebbnd1lem2  26351  chebbnd1lem3  26352  rplogsumlem2  26366  rpvmasumlem  26368  dchrisumlema  26369  dchrisumlem3  26372  dchrvmasumiflem1  26382  dchrisum0lem1  26397  rplogsum  26408  mulog2sumlem2  26416  pntrsumo1  26446  pntrlog2bndlem2  26459  pntrlog2bndlem4  26461  pntpbnd1  26467  pntpbnd2  26468  pntlemg  26479  pntlemq  26482  pntlemr  26483  pntlemf  26486  ostth2lem2  26515  dya2ub  31949  dya2icoseg  31956  dnibndlem13  34407  knoppndvlem19  34447  ltflcei  35502  opnmbllem0  35550  itg2addnclem2  35566  cntotbnd  35691  aks4d1p1p3  39810  aks4d1p1p2  39811  aks4d1p1p4  39812  aks4d1p3  39819  irrapxlem1  40350  irrapxlem2  40351  irrapxlem3  40352  irrapxlem4  40353  pellexlem5  40361  pellfund14  40426  hashnzfz2  41615  hashnzfzclim  41616  sineq0ALT  42233  lefldiveq  42507  ltmod  42857  ioodvbdlimc1lem2  43151  ioodvbdlimc2lem  43153  dirkertrigeqlem3  43319  dirkertrigeq  43320  dirkercncflem4  43325  fourierdlem4  43330  fourierdlem7  43333  fourierdlem19  43345  fourierdlem26  43352  fourierdlem41  43367  fourierdlem47  43372  fourierdlem48  43373  fourierdlem49  43374  fourierdlem51  43376  fourierdlem63  43388  fourierdlem65  43390  fourierdlem71  43396  fourierdlem89  43414  fourierdlem90  43415  fourierdlem91  43416  lighneallem2  44734  fldivmod  45540  modn0mul  45542  fllogbd  45582  fldivexpfllog2  45587  logbpw2m1  45589  fllog2  45590  nnpw2blen  45602  blen1b  45610  nnolog2flm1  45612  blennngt2o2  45614  blennn0e2  45616  digvalnn0  45621  dig2nn1st  45627  dig2nn0  45633  dig2bits  45636  dignn0flhalflem2  45638
  Copyright terms: Public domain W3C validator