Theorem flcld 12066

Description: The floor (greatest integer) function is an integer (closure law). (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
flcld.1	|- ( ph -> A e. RR )

Assertion

Ref	Expression
flcld	|- ( ph -> ( |_ ` A ) e. ZZ )

Proof of Theorem flcld

Step	Hyp	Ref	Expression
1		flcld.1	. 2 |- ( ph -> A e. RR )
2		flcl 12063	. 2 |- ( A e. RR -> ( |_ ` A ) e. ZZ )
3	1, 2	syl 17	1 |- ( ph -> ( |_ ` A ) e. ZZ )

Syntax hints:   -> wi 4   e. wcel 1898   ` cfv 5601   RRcr 9564   ZZcz 10966   |_cfl 12058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642  ax-pre-sup 9643

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-sup 7982  df-inf 7983  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-n0 10899  df-z 10967  df-uz 11189  df-fl 12060

This theorem is referenced by:  flge  12073  flwordi  12079  flword2  12080  fladdz  12090  flhalf  12094  ceicl  12102  quoremz  12114  intfracq  12118  fldiv  12119  moddiffl  12140  moddifz  12141  zmodcl  12148  modadd1  12166  modmul1  12175  modsubdir  12190  iexpcyc  12411  absrdbnd  13453  limsupgre  13591  limsupgreOLD  13592  climrlim2  13660  dvdsmod  14411  divalgmod  14436  bitsp1  14453  bitsmod  14459  bitscmp  14461  bitsuz  14497  modgcd  14549  bezoutlem3OLD  14554  bezoutlem3  14557  hashdvds  14772  prmdiv  14782  odzdvds  14789  odzdvdsOLD  14795  fldivp1  14891  pcfac  14893  pcbc  14894  prmreclem4  14912  vdwnnlem3  14996  odmod  17244  gexdvds  17284  zringlpirlem3OLD  19104  zringlpirlem3  19106  zcld  21880  ovolunlem1a  22498  opnmbllem  22608  mbfi1fseqlem5  22726  dvfsumlem1  23027  dvfsumlem3  23029  sineq0  23525  efif1olem2  23541  ppiltx  24153  dvdsflf1o  24165  ppiub  24181  fsumvma2  24191  logfac2  24194  chpchtsum  24196  pcbcctr  24253  bposlem1  24261  bposlem3  24263  bposlem4  24264  bposlem5  24265  bposlem6  24266  lgseisenlem4  24329  lgseisen  24330  lgsquadlem1  24331  lgsquadlem2  24332  chebbnd1lem2  24357  chebbnd1lem3  24358  rplogsumlem2  24372  rpvmasumlem  24374  dchrisumlema  24375  dchrisumlem3  24378  dchrvmasumiflem1  24388  dchrisum0lem1  24403  rplogsum  24414  mulog2sumlem2  24422  pntrsumo1  24452  pntrlog2bndlem2  24465  pntrlog2bndlem4  24467  pntpbnd1  24473  pntpbnd2  24474  pntlemg  24485  pntlemq  24488  pntlemr  24489  pntlemf  24492  ostth2lem2  24521  gxmodid  26056  dya2ub  29141  dya2icoseg  29148  ltflcei  31978  opnmbllem0  32021  dvtanlemOLD  32036  itg2addnclem2  32039  cntotbnd  32173  irrapxlem1  35711  irrapxlem2  35712  irrapxlem3  35713  irrapxlem4  35714  pellexlem5  35722  pellfund14  35791  isprm7  36704  hashnzfz2  36714  hashnzfzclim  36715  sineq0ALT  37374  lefldiveq  37544  ltmod  37756  ioodvbdlimc1lem2  37842  ioodvbdlimc1lem2OLD  37844  ioodvbdlimc2lem  37846  ioodvbdlimc2lemOLD  37847  dirkertrigeqlem3  38000  dirkertrigeq  38001  dirkercncflem4  38006  fourierdlem4  38011  fourierdlem7  38014  fourierdlem19  38026  fourierdlem26  38033  fourierdlem41  38049  fourierdlem47  38055  fourierdlem48  38056  fourierdlem49  38057  fourierdlem51  38059  fourierdlem63  38071  fourierdlem65  38073  fourierdlem71  38079  fourierdlem89  38097  fourierdlem90  38098  fourierdlem91  38099  fldivmod  40594  modn0mul  40596  fllogbd  40644  fldivexpfllog2  40649  logbpw2m1  40651  fllog2  40652  nnpw2blen  40664  blen1b  40672  nnolog2flm1  40674  blennngt2o2  40676  blennn0e2  40678  digvalnn0  40683  dig2nn1st  40689  dig2nn0  40695  dig2bits  40698  dignn0flhalflem2  40700