Theorem elfzofz 13592

Description: A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.)

Assertion

Ref	Expression
elfzofz	⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (𝑀...𝑁))

Proof of Theorem elfzofz

Step	Hyp	Ref	Expression
1		elfzouz 13580	. 2 ⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
2		elfzouz2 13591	. 2 ⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))
3		elfzuzb 13435	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)))
4	1, 2, 3	sylanbrc 584	1 ⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (𝑀...𝑁))

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6490  (class class class)co 7358  ℤ_≥cuz 12752  ...cfz 13424  ..^cfzo 13571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-cnex 11083  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103  ax-pre-mulgt0 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8222  df-wrecs 8253  df-recs 8302  df-rdg 8340  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11169  df-mnf 11170  df-xr 11171  df-ltxr 11172  df-le 11173  df-sub 11367  df-neg 11368  df-nn 12147  df-n0 12403  df-z 12490  df-uz 12753  df-fz 13425  df-fzo 13572

This theorem is referenced by:  fzossfz  13595  elfzom1elp1fzo  13649  fzone1  13701  uzindi  13906  swrdfv0  14574  pfxsuffeqwrdeq  14622  telfsumo  15726  telfsumo2  15727  fsumparts  15730  prodfn0  15818  hashgcdlem  16716  cshwshashlem2  17025  efgs1b  19669  efgredlem  19680  cpmadugsumlemF  22819  dvfsumle  25967  dvfsumleOLD  25968  dvfsumabs  25970  dvntaylp  26319  taylthlem1  26321  taylthlem2  26322  taylthlem2OLD  26323  pntpbnd1  27537  pntlemj  27554  pntlemi  27555  pntlemf  27556  upgrewlkle2  29664  wlk1walk  29696  wlkp1lem6  29734  trlreslem  29755  upgrwlkdvdelem  29793  crctcshwlkn0lem4  29870  crctcshwlkn0lem5  29871  crctcshwlkn0lem6  29872  clwwisshclwws  30074  trlsegvdeglem1  30279  poimirlem24  37956  poimirlem25  37957  poimirlem29  37961  poimirlem31  37963  elfzfzo  45713  dvnmptdivc  46370  fourierdlem1  46540  fourierdlem12  46551  fourierdlem14  46553  fourierdlem15  46554  fourierdlem20  46559  fourierdlem25  46564  fourierdlem27  46566  fourierdlem41  46580  fourierdlem46  46584  fourierdlem48  46586  fourierdlem49  46587  fourierdlem50  46588  fourierdlem54  46592  fourierdlem63  46601  fourierdlem64  46602  fourierdlem65  46603  fourierdlem69  46607  fourierdlem70  46608  fourierdlem71  46609  fourierdlem72  46610  fourierdlem73  46611  fourierdlem74  46612  fourierdlem75  46613  fourierdlem76  46614  fourierdlem79  46617  fourierdlem80  46618  fourierdlem81  46619  fourierdlem84  46622  fourierdlem85  46623  fourierdlem88  46626  fourierdlem89  46627  fourierdlem90  46628  fourierdlem91  46629  fourierdlem92  46630  fourierdlem93  46631  fourierdlem94  46632  fourierdlem97  46635  fourierdlem102  46640  fourierdlem103  46641  fourierdlem104  46642  fourierdlem111  46649  fourierdlem113  46651  fourierdlem114  46652  ormkglobd  47307  iccpartiltu  47856  iccelpart  47867  iccpartiun  47868  icceuelpartlem  47869  icceuelpart  47870  iccpartdisj  47871  iccpartnel  47872  upgrimwlklem5  48335  gpgedgvtx0  48495