![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > flge0nn0 | Structured version Visualization version GIF version |
Description: The floor of a number greater than or equal to 0 is a nonnegative integer. (Contributed by NM, 26-Apr-2005.) |
Ref | Expression |
---|---|
flge0nn0 | ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | flcl 12761 | . . 3 ⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℤ) | |
2 | 1 | adantr 472 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (⌊‘𝐴) ∈ ℤ) |
3 | 0z 11551 | . . . 4 ⊢ 0 ∈ ℤ | |
4 | flge 12771 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 0 ∈ ℤ) → (0 ≤ 𝐴 ↔ 0 ≤ (⌊‘𝐴))) | |
5 | 3, 4 | mpan2 709 | . . 3 ⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐴 ↔ 0 ≤ (⌊‘𝐴))) |
6 | 5 | biimpa 502 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 0 ≤ (⌊‘𝐴)) |
7 | elnn0z 11553 | . 2 ⊢ ((⌊‘𝐴) ∈ ℕ0 ↔ ((⌊‘𝐴) ∈ ℤ ∧ 0 ≤ (⌊‘𝐴))) | |
8 | 2, 6, 7 | sylanbrc 701 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ0) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 ∈ wcel 2127 class class class wbr 4792 ‘cfv 6037 ℝcr 10098 0cc0 10099 ≤ cle 10238 ℕ0cn0 11455 ℤcz 11540 ⌊cfl 12756 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-8 2129 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 ax-sep 4921 ax-nul 4929 ax-pow 4980 ax-pr 5043 ax-un 7102 ax-cnex 10155 ax-resscn 10156 ax-1cn 10157 ax-icn 10158 ax-addcl 10159 ax-addrcl 10160 ax-mulcl 10161 ax-mulrcl 10162 ax-mulcom 10163 ax-addass 10164 ax-mulass 10165 ax-distr 10166 ax-i2m1 10167 ax-1ne0 10168 ax-1rid 10169 ax-rnegex 10170 ax-rrecex 10171 ax-cnre 10172 ax-pre-lttri 10173 ax-pre-lttrn 10174 ax-pre-ltadd 10175 ax-pre-mulgt0 10176 ax-pre-sup 10177 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-eu 2599 df-mo 2600 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-ne 2921 df-nel 3024 df-ral 3043 df-rex 3044 df-reu 3045 df-rmo 3046 df-rab 3047 df-v 3330 df-sbc 3565 df-csb 3663 df-dif 3706 df-un 3708 df-in 3710 df-ss 3717 df-pss 3719 df-nul 4047 df-if 4219 df-pw 4292 df-sn 4310 df-pr 4312 df-tp 4314 df-op 4316 df-uni 4577 df-iun 4662 df-br 4793 df-opab 4853 df-mpt 4870 df-tr 4893 df-id 5162 df-eprel 5167 df-po 5175 df-so 5176 df-fr 5213 df-we 5215 df-xp 5260 df-rel 5261 df-cnv 5262 df-co 5263 df-dm 5264 df-rn 5265 df-res 5266 df-ima 5267 df-pred 5829 df-ord 5875 df-on 5876 df-lim 5877 df-suc 5878 df-iota 6000 df-fun 6039 df-fn 6040 df-f 6041 df-f1 6042 df-fo 6043 df-f1o 6044 df-fv 6045 df-riota 6762 df-ov 6804 df-oprab 6805 df-mpt2 6806 df-om 7219 df-wrecs 7564 df-recs 7625 df-rdg 7663 df-er 7899 df-en 8110 df-dom 8111 df-sdom 8112 df-sup 8501 df-inf 8502 df-pnf 10239 df-mnf 10240 df-xr 10241 df-ltxr 10242 df-le 10243 df-sub 10431 df-neg 10432 df-nn 11184 df-n0 11456 df-z 11541 df-uz 11851 df-fl 12758 |
This theorem is referenced by: fldivnn0 12788 expnbnd 13158 facavg 13253 o1fsum 14715 efcllem 14978 odzdvds 15673 prmreclem3 15795 1arith 15804 odmodnn0 18130 lebnumii 22937 lmnn 23232 vitalilem4 23550 mbfi1fseqlem1 23652 mbfi1fseqlem3 23654 mbfi1fseqlem5 23656 harmoniclbnd 24905 harmonicbnd4 24907 fsumharmonic 24908 ppiltx 25073 logfac2 25112 chpval2 25113 chpchtsum 25114 chpub 25115 logfaclbnd 25117 logfacbnd3 25118 logfacrlim 25119 bposlem1 25179 gausslemma2dlem0d 25254 lgsquadlem2 25276 chtppilimlem1 25332 vmadivsum 25341 rpvmasumlem 25346 dchrisumlema 25347 dchrisumlem1 25348 dchrisum0lem1b 25374 dchrisum0lem1 25375 dchrisum0lem2a 25376 dchrisum0lem3 25378 mudivsum 25389 mulogsumlem 25390 selberglem2 25405 selberg2lem 25409 pntrsumo1 25424 pntrlog2bndlem2 25437 pntrlog2bndlem4 25439 pntrlog2bndlem6a 25441 pntpbnd1 25445 pntpbnd2 25446 pntlemg 25457 pntlemj 25462 pntlemf 25464 ostth2lem2 25493 ostth2lem3 25494 minvecolem3 28012 minvecolem4 28016 itg2addnclem2 33744 irrapxlem4 37860 irrapxlem5 37861 recnnltrp 40060 rpgtrecnn 40064 ioodvbdlimc1lem2 40619 ioodvbdlimc2lem 40621 fourierdlem47 40842 vonioolem1 41369 fllog2 42841 blennnelnn 42849 dignnld 42876 dignn0flhalf 42891 |
Copyright terms: Public domain | W3C validator |