![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reflcl | Structured version Visualization version GIF version |
Description: The floor (greatest integer) function is real. (Contributed by NM, 15-Jul-2008.) |
Ref | Expression |
---|---|
reflcl | ⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | flcl 13003 | . 2 ⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℤ) | |
2 | 1 | zred 11925 | 1 ⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2079 ‘cfv 6217 ℝcr 10371 ⌊cfl 12998 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 ax-sep 5088 ax-nul 5095 ax-pow 5150 ax-pr 5214 ax-un 7310 ax-cnex 10428 ax-resscn 10429 ax-1cn 10430 ax-icn 10431 ax-addcl 10432 ax-addrcl 10433 ax-mulcl 10434 ax-mulrcl 10435 ax-mulcom 10436 ax-addass 10437 ax-mulass 10438 ax-distr 10439 ax-i2m1 10440 ax-1ne0 10441 ax-1rid 10442 ax-rnegex 10443 ax-rrecex 10444 ax-cnre 10445 ax-pre-lttri 10446 ax-pre-lttrn 10447 ax-pre-ltadd 10448 ax-pre-mulgt0 10449 ax-pre-sup 10450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1079 df-3an 1080 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ne 2983 df-nel 3089 df-ral 3108 df-rex 3109 df-reu 3110 df-rmo 3111 df-rab 3112 df-v 3434 df-sbc 3702 df-csb 3807 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-pss 3871 df-nul 4207 df-if 4376 df-pw 4449 df-sn 4467 df-pr 4469 df-tp 4471 df-op 4473 df-uni 4740 df-iun 4821 df-br 4957 df-opab 5019 df-mpt 5036 df-tr 5058 df-id 5340 df-eprel 5345 df-po 5354 df-so 5355 df-fr 5394 df-we 5396 df-xp 5441 df-rel 5442 df-cnv 5443 df-co 5444 df-dm 5445 df-rn 5446 df-res 5447 df-ima 5448 df-pred 6015 df-ord 6061 df-on 6062 df-lim 6063 df-suc 6064 df-iota 6181 df-fun 6219 df-fn 6220 df-f 6221 df-f1 6222 df-fo 6223 df-f1o 6224 df-fv 6225 df-riota 6968 df-ov 7010 df-oprab 7011 df-mpo 7012 df-om 7428 df-wrecs 7789 df-recs 7851 df-rdg 7889 df-er 8130 df-en 8348 df-dom 8349 df-sdom 8350 df-sup 8742 df-inf 8743 df-pnf 10512 df-mnf 10513 df-xr 10514 df-ltxr 10515 df-le 10516 df-sub 10708 df-neg 10709 df-nn 11476 df-n0 11735 df-z 11819 df-uz 12083 df-fl 13000 |
This theorem is referenced by: fllep1 13009 fraclt1 13010 fracle1 13011 fracge0 13012 fllt 13014 flflp1 13015 flid 13016 flltnz 13019 flval3 13023 refldivcl 13031 fladdz 13033 flzadd 13034 flmulnn0 13035 flltdivnn0lt 13041 ceige 13051 ceim1l 13053 flleceil 13059 fleqceilz 13060 intfracq 13065 fldiv 13066 uzsup 13069 modvalr 13078 modfrac 13090 flmod 13091 intfrac 13092 modmulnn 13095 modcyc 13112 modadd1 13114 moddi 13145 modirr 13148 digit2 13435 digit1 13436 facavg 13499 rddif 14522 absrdbnd 14523 rexuzre 14534 o1fsum 14989 flo1 15030 isprm7 15869 opnmbllem 23873 mbfi1fseqlem1 23987 mbfi1fseqlem3 23989 mbfi1fseqlem4 23990 mbfi1fseqlem5 23991 mbfi1fseqlem6 23992 dvfsumlem1 24294 dvfsumlem2 24295 dvfsumlem3 24296 dvfsumlem4 24297 dvfsum2 24302 harmonicbnd4 25258 chtfl 25396 chpfl 25397 ppieq0 25423 ppiltx 25424 ppiub 25450 chpeq0 25454 chtub 25458 logfac2 25463 chpub 25466 logfacubnd 25467 logfaclbnd 25468 lgsquadlem1 25626 chtppilimlem1 25719 vmadivsum 25728 dchrisumlema 25734 dchrisumlem1 25735 dchrisumlem3 25737 dchrmusum2 25740 dchrisum0lem1b 25761 dchrisum0lem1 25762 dchrisum0lem2a 25763 dchrisum0lem3 25765 mudivsum 25776 mulogsumlem 25777 selberglem2 25792 pntrlog2bndlem6 25829 pntpbnd2 25833 pntlemg 25844 pntlemr 25848 pntlemj 25849 pntlemf 25851 pntlemk 25852 minvecolem4 28336 dnicld1 33364 dnibndlem2 33371 dnibndlem3 33372 dnibndlem4 33373 dnibndlem5 33374 dnibndlem7 33376 dnibndlem8 33377 dnibndlem9 33378 dnibndlem10 33379 dnibndlem11 33380 dnibndlem13 33382 dnibnd 33383 knoppcnlem4 33388 ltflcei 34357 leceifl 34358 opnmbllem0 34405 itg2addnclem2 34421 itg2addnclem3 34422 hashnzfzclim 40144 lefldiveq 41053 fourierdlem4 41892 fourierdlem26 41914 fourierdlem47 41934 fourierdlem65 41952 flsubz 44012 dignn0flhalflem2 44111 |
Copyright terms: Public domain | W3C validator |