MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elfzoelz Structured version   Visualization version   GIF version

Theorem elfzoelz 13674
Description: Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.)
Assertion
Ref Expression
elfzoelz (𝐴 ∈ (𝐡..^𝐢) β†’ 𝐴 ∈ β„€)

Proof of Theorem elfzoelz
StepHypRef Expression
1 elfzoel1 13672 . . . 4 (𝐴 ∈ (𝐡..^𝐢) β†’ 𝐡 ∈ β„€)
2 elfzoel2 13673 . . . 4 (𝐴 ∈ (𝐡..^𝐢) β†’ 𝐢 ∈ β„€)
3 fzof 13671 . . . . 5 ..^:(β„€ Γ— β„€)βŸΆπ’« β„€
43fovcl 7556 . . . 4 ((𝐡 ∈ β„€ ∧ 𝐢 ∈ β„€) β†’ (𝐡..^𝐢) ∈ 𝒫 β„€)
51, 2, 4syl2anc 582 . . 3 (𝐴 ∈ (𝐡..^𝐢) β†’ (𝐡..^𝐢) ∈ 𝒫 β„€)
65elpwid 4615 . 2 (𝐴 ∈ (𝐡..^𝐢) β†’ (𝐡..^𝐢) βŠ† β„€)
7 id 22 . 2 (𝐴 ∈ (𝐡..^𝐢) β†’ 𝐴 ∈ (𝐡..^𝐢))
86, 7sseldd 3983 1 (𝐴 ∈ (𝐡..^𝐢) β†’ 𝐴 ∈ β„€)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∈ wcel 2098  π’« cpw 4606  (class class class)co 7426  β„€cz 12598  ..^cfzo 13669
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433  ax-un 7748  ax-cnex 11204  ax-resscn 11205
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-fv 6561  df-ov 7429  df-oprab 7430  df-mpo 7431  df-1st 8001  df-2nd 8002  df-neg 11487  df-z 12599  df-uz 12863  df-fz 13527  df-fzo 13670
This theorem is referenced by:  elfzo2  13677  elfzole1  13682  elfzolt2  13683  elfzolt3  13684  elfzolt2b  13685  elfzop1le2  13687  elfzouz2  13689  fzonnsub  13699  fzospliti  13706  fzodisj  13708  fzodisjsn  13712  fzonmapblen  13720  fzoaddel  13727  elincfzoext  13732  fzosubel  13733  elfzom1elp1fzo1  13774  elfzo1elm1fzo0  13775  elfznelfzob  13780  modaddmodup  13941  modaddmodlo  13942  modfzo0difsn  13950  modsumfzodifsn  13951  addmodlteq  13953  ccatval3  14571  ccatlid  14578  ccatass  14580  ccatrn  14581  ccatalpha  14585  swrdfv0  14641  swrdfv2  14653  swrds1  14658  ccatswrd  14660  pfxfv  14674  ccatpfx  14693  swrdswrd  14697  pfxccatin12lem2a  14719  swrdccatin2  14721  pfxccatin12lem2  14723  revccat  14758  revrev  14759  repswrevw  14779  cshwidxmod  14795  cshwidxmodr  14796  cshwidx0  14798  cshwidxm1  14799  cshweqrep  14813  cshw1  14814  cshimadifsn  14822  cshimadifsn0  14823  cshco  14829  fzomaxdiflem  15331  fzomaxdif  15332  pwdif  15856  pwm1geoser  15857  fzo0dvdseq  16309  fzocongeq  16310  addmodlteqALT  16311  crth  16756  phimullem  16757  eulerthlem1  16759  eulerthlem2  16760  hashgcdlem  16766  hashgcdeq  16767  phisum  16768  reumodprminv  16782  modprm0  16783  nnnn0modprm0  16784  modprmn0modprm0  16785  prmgaplem7  17035  cshwshashlem2  17075  cshwshashlem3  17076  cshwrepswhash1  17081  psgnunilem5  19463  odf1o2  19542  odngen  19546  znf1o  21499  znunithash  21512  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dchrisumlem1  27450  dchrisumlem2  27451  dchrisum  27453  pntlemq  27562  pntlemr  27563  pntlemj  27564  pntlemi  27565  pntlemf  27566  wlk1walk  29481  pthdadjvtx  29572  crctcshwlkn0lem3  29651  crctcshwlkn0lem4  29652  crctcshwlkn0lem5  29653  crctcshwlkn0lem6  29654  crctcshlem2  29657  crctcshwlkn0  29660  crctcshtrl  29662  crctcsh  29663  clwwlkccatlem  29827  clwwisshclwwslem  29852  clwwisshclwws  29853  eucrctshift  30081  eucrct2eupth  30083  ccatf1  32701  cshwrnid  32711  revpfxsfxrev  34766  revwlk  34775  poimirlem8  37142  poimirlem18  37152  poimirlem21  37155  poimirlem22  37156  poimirlem24  37158  frlmvscadiccat  41786  iblspltprt  45408  itgspltprt  45414  stoweidlem3  45438  fourierdlem12  45554  fourierdlem20  45562  fourierdlem46  45587  fourierdlem50  45591  fourierdlem54  45595  fourierdlem63  45604  fourierdlem64  45605  fourierdlem65  45606  fourierdlem76  45617  fourierdlem79  45620  fourierdlem102  45643  fourierdlem103  45644  fourierdlem104  45645  fourierdlem114  45655  iundjiun  45895  carageniuncllem1  45956  caratheodorylem1  45961  natlocalincr  46309  natglobalincr  46310  iccpartipre  46808  iccpartiltu  46809  iccpartigtl  46810  iccpartgt  46814  icceuelpartlem  46822  icceuelpart  46823  iccpartnel  46825  fargshiftf1  46828  bgoldbtbndlem2  47193  m1modmmod  47690  fllog2  47737  nn0sumshdiglemA  47788  nn0sumshdiglemB  47789  nn0mullong  47794
  Copyright terms: Public domain W3C validator