Theorem flge0nn0 12873

Description: The floor of a number greater than or equal to 0 is a nonnegative integer. (Contributed by NM, 26-Apr-2005.)

Assertion

Ref	Expression
flge0nn0	⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ0)

Proof of Theorem flge0nn0

Step	Hyp	Ref	Expression
1		flcl 12848	. . 3 ⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℤ)
2	1	adantr 473	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (⌊‘𝐴) ∈ ℤ)
3		0z 11674	. . . 4 ⊢ 0 ∈ ℤ
4		flge 12858	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 0 ∈ ℤ) → (0 ≤ 𝐴 ↔ 0 ≤ (⌊‘𝐴)))
5	3, 4	mpan2 683	. . 3 ⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐴 ↔ 0 ≤ (⌊‘𝐴)))
6	5	biimpa 469	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 0 ≤ (⌊‘𝐴))
7		elnn0z 11676	. 2 ⊢ ((⌊‘𝐴) ∈ ℕ0 ↔ ((⌊‘𝐴) ∈ ℤ ∧ 0 ≤ (⌊‘𝐴)))
8	2, 6, 7	sylanbrc 579	1 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ0)

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 385   ∈ wcel 2157   class class class wbr 4842  ‘cfv 6100  ℝcr 10222  0cc0 10223   ≤ cle 10363  ℕ₀cn0 11577  ℤcz 11663  ⌊cfl 12843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-sep 4974  ax-nul 4982  ax-pow 5034  ax-pr 5096  ax-un 7182  ax-cnex 10279  ax-resscn 10280  ax-1cn 10281  ax-icn 10282  ax-addcl 10283  ax-addrcl 10284  ax-mulcl 10285  ax-mulrcl 10286  ax-mulcom 10287  ax-addass 10288  ax-mulass 10289  ax-distr 10290  ax-i2m1 10291  ax-1ne0 10292  ax-1rid 10293  ax-rnegex 10294  ax-rrecex 10295  ax-cnre 10296  ax-pre-lttri 10297  ax-pre-lttrn 10298  ax-pre-ltadd 10299  ax-pre-mulgt0 10300  ax-pre-sup 10301

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ne 2971  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3386  df-sbc 3633  df-csb 3728  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-pss 3784  df-nul 4115  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4628  df-iun 4711  df-br 4843  df-opab 4905  df-mpt 4922  df-tr 4945  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5897  df-ord 5943  df-on 5944  df-lim 5945  df-suc 5946  df-iota 6063  df-fun 6102  df-fn 6103  df-f 6104  df-f1 6105  df-fo 6106  df-f1o 6107  df-fv 6108  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-wrecs 7644  df-recs 7706  df-rdg 7744  df-er 7981  df-en 8195  df-dom 8196  df-sdom 8197  df-sup 8589  df-inf 8590  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10557  df-neg 10558  df-nn 11312  df-n0 11578  df-z 11664  df-uz 11928  df-fl 12845

This theorem is referenced by:  fldivnn0  12875  expnbnd  13244  facavg  13338  o1fsum  14880  efcllem  15141  odzdvds  15830  prmreclem3  15952  1arith  15961  odmodnn0  18269  lebnumii  23090  lmnn  23386  vitalilem4  23716  mbfi1fseqlem1  23820  mbfi1fseqlem3  23822  mbfi1fseqlem5  23824  harmoniclbnd  25084  harmonicbnd4  25086  fsumharmonic  25087  ppiltx  25252  logfac2  25291  chpval2  25292  chpchtsum  25293  chpub  25294  logfaclbnd  25296  logfacbnd3  25297  logfacrlim  25298  bposlem1  25358  gausslemma2dlem0d  25433  lgsquadlem2  25455  chtppilimlem1  25511  vmadivsum  25520  rpvmasumlem  25525  dchrisumlema  25526  dchrisumlem1  25527  dchrisum0lem1b  25553  dchrisum0lem1  25554  dchrisum0lem2a  25555  dchrisum0lem3  25557  mudivsum  25568  mulogsumlem  25569  selberglem2  25584  selberg2lem  25588  pntrsumo1  25603  pntrlog2bndlem2  25616  pntrlog2bndlem4  25618  pntrlog2bndlem6a  25620  pntpbnd1  25624  pntpbnd2  25625  pntlemg  25636  pntlemj  25641  pntlemf  25643  ostth2lem2  25672  ostth2lem3  25673  minvecolem3  28250  minvecolem4  28254  itg2addnclem2  33943  irrapxlem4  38164  irrapxlem5  38165  recnnltrp  40326  rpgtrecnn  40330  ioodvbdlimc1lem2  40880  ioodvbdlimc2lem  40882  fourierdlem47  41102  vonioolem1  41629  fllog2  43150  blennnelnn  43158  dignnld  43185  dignn0flhalf  43200