Theorem elfzofz 13680

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 13668	. 2 ⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
2		elfzouz2 13679	. 2 ⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))
3		elfzuzb 13527	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)))
4	1, 2, 3	sylanbrc 581	1 ⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (𝑀...𝑁))

Syntax hints:   → wi 4   ∈ wcel 2098  ‘cfv 6547  (class class class)co 7417  ℤ_≥cuz 12852  ...cfz 13516  ..^cfzo 13659

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 2696  ax-sep 5299  ax-nul 5306  ax-pow 5364  ax-pr 5428  ax-un 7739  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215

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 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3965  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-riota 7373  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7870  df-1st 7992  df-2nd 7993  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-er 8723  df-en 8963  df-dom 8964  df-sdom 8965  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-nn 12243  df-n0 12503  df-z 12589  df-uz 12853  df-fz 13517  df-fzo 13660

This theorem is referenced by:  fzossfz  13683  elfzom1elp1fzo  13731  uzindi  13980  swrdfv0  14632  pfxsuffeqwrdeq  14681  telfsumo  15781  telfsumo2  15782  fsumparts  15785  prodfn0  15873  hashgcdlem  16757  cshwshashlem2  17066  efgs1b  19699  efgredlem  19710  cpmadugsumlemF  22815  dvfsumle  25991  dvfsumleOLD  25992  dvfsumabs  25994  dvntaylp  26343  taylthlem1  26345  taylthlem2  26346  taylthlem2OLD  26347  pntpbnd1  27556  pntlemj  27573  pntlemi  27574  pntlemf  27575  upgrewlkle2  29483  wlk1walk  29516  wlkp1lem6  29555  trlreslem  29576  upgrwlkdvdelem  29613  crctcshwlkn0lem4  29687  crctcshwlkn0lem5  29688  crctcshwlkn0lem6  29689  clwwisshclwws  29888  trlsegvdeglem1  30093  fzone1  32635  poimirlem24  37204  poimirlem25  37205  poimirlem29  37209  poimirlem31  37211  elfzfzo  44738  dvnmptdivc  45406  fourierdlem1  45576  fourierdlem12  45587  fourierdlem14  45589  fourierdlem15  45590  fourierdlem20  45595  fourierdlem25  45600  fourierdlem27  45602  fourierdlem41  45616  fourierdlem46  45620  fourierdlem48  45622  fourierdlem49  45623  fourierdlem50  45624  fourierdlem54  45628  fourierdlem63  45637  fourierdlem64  45638  fourierdlem65  45639  fourierdlem69  45643  fourierdlem70  45644  fourierdlem71  45645  fourierdlem72  45646  fourierdlem73  45647  fourierdlem74  45648  fourierdlem75  45649  fourierdlem76  45650  fourierdlem79  45653  fourierdlem80  45654  fourierdlem81  45655  fourierdlem84  45658  fourierdlem85  45659  fourierdlem88  45662  fourierdlem89  45663  fourierdlem90  45664  fourierdlem91  45665  fourierdlem92  45666  fourierdlem93  45667  fourierdlem94  45668  fourierdlem97  45671  fourierdlem102  45676  fourierdlem103  45677  fourierdlem104  45678  fourierdlem111  45685  fourierdlem113  45687  fourierdlem114  45688  iccpartiltu  46841  iccelpart  46852  iccpartiun  46853  icceuelpartlem  46854  icceuelpart  46855  iccpartdisj  46856  iccpartnel  46857

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »