Theorem flcld 11663

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 11660	. 2 |- ( A e. RR -> ( |_ ` A ) e. ZZ )
3	1, 2	syl 16	1 |- ( ph -> ( |_ ` A ) e. ZZ )

Syntax hints:   -> wi 4   e. wcel 1756   ` cfv 5433   RRcr 9296   ZZcz 10661   |_cfl 11655

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4428  ax-nul 4436  ax-pow 4485  ax-pr 4546  ax-un 6387  ax-cnex 9353  ax-resscn 9354  ax-1cn 9355  ax-icn 9356  ax-addcl 9357  ax-addrcl 9358  ax-mulcl 9359  ax-mulrcl 9360  ax-mulcom 9361  ax-addass 9362  ax-mulass 9363  ax-distr 9364  ax-i2m1 9365  ax-1ne0 9366  ax-1rid 9367  ax-rnegex 9368  ax-rrecex 9369  ax-cnre 9370  ax-pre-lttri 9371  ax-pre-lttrn 9372  ax-pre-ltadd 9373  ax-pre-mulgt0 9374  ax-pre-sup 9375

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2735  df-rex 2736  df-reu 2737  df-rmo 2738  df-rab 2739  df-v 2989  df-sbc 3202  df-csb 3304  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-pss 3359  df-nul 3653  df-if 3807  df-pw 3877  df-sn 3893  df-pr 3895  df-tp 3897  df-op 3899  df-uni 4107  df-iun 4188  df-br 4308  df-opab 4366  df-mpt 4367  df-tr 4401  df-eprel 4647  df-id 4651  df-po 4656  df-so 4657  df-fr 4694  df-we 4696  df-ord 4737  df-on 4738  df-lim 4739  df-suc 4740  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-f1 5438  df-fo 5439  df-f1o 5440  df-fv 5441  df-riota 6067  df-ov 6109  df-oprab 6110  df-mpt2 6111  df-om 6492  df-recs 6847  df-rdg 6881  df-er 7116  df-en 7326  df-dom 7327  df-sdom 7328  df-sup 7706  df-pnf 9435  df-mnf 9436  df-xr 9437  df-ltxr 9438  df-le 9439  df-sub 9612  df-neg 9613  df-nn 10338  df-n0 10595  df-z 10662  df-uz 10877  df-fl 11657

This theorem is referenced by:  flge  11670  flwordi  11675  flword2  11676  fladdz  11685  flhalf  11689  ceicl  11697  quoremz  11709  intfracq  11713  fldiv  11714  moddiffl  11734  moddifz  11735  zmodcl  11742  modadd1  11760  modmul1  11767  modsubdir  11782  iexpcyc  11985  absrdbnd  12844  limsupgre  12974  climrlim2  13040  dvdsmod  13605  divalgmod  13625  bitsp1  13642  bitsmod  13647  bitscmp  13649  bitsuz  13685  modgcd  13735  bezoutlem3  13739  hashdvds  13865  prmdiv  13875  odzdvds  13882  fldivp1  13974  pcfac  13976  pcbc  13977  prmreclem4  13995  vdwnnlem3  14073  odmod  16064  gexdvds  16098  zringlpirlem3  17920  zlpirlem3  17925  zcld  20405  ovolunlem1a  20994  opnmbllem  21096  mbfi1fseqlem5  21212  dvfsumlem1  21513  dvfsumlem3  21515  sineq0  21998  efif1olem2  22014  ppiltx  22530  dvdsflf1o  22542  ppiub  22558  fsumvma2  22568  logfac2  22571  chpchtsum  22573  pcbcctr  22630  bposlem1  22638  bposlem3  22640  bposlem4  22641  bposlem5  22642  bposlem6  22643  lgseisenlem4  22706  lgseisen  22707  lgsquadlem1  22708  lgsquadlem2  22709  chebbnd1lem2  22734  chebbnd1lem3  22735  rplogsumlem2  22749  rpvmasumlem  22751  dchrisumlema  22752  dchrisumlem3  22755  dchrvmasumiflem1  22765  dchrisum0lem1  22780  rplogsum  22791  mulog2sumlem2  22799  pntrsumo1  22829  pntrlog2bndlem2  22842  pntrlog2bndlem4  22844  pntpbnd1  22850  pntpbnd2  22851  pntlemg  22862  pntlemq  22865  pntlemr  22866  pntlemf  22869  ostth2lem2  22898  gxmodid  23781  dya2ub  26700  dya2icoseg  26707  ltflcei  28438  opnmbllem0  28446  dvtanlem  28460  itg2addnclem2  28463  cntotbnd  28714  irrapxlem1  29182  irrapxlem2  29183  irrapxlem3  29184  irrapxlem4  29185  pellexlem5  29193  pellfund14  29258  sineq0ALT  31692