Theorem fzofzp1 13716

Description: If a point is in a half-open range, the next point is in the closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.)

Assertion

Ref	Expression
fzofzp1	⊢ (𝐶 ∈ (𝐴..^𝐵) → (𝐶 + 1) ∈ (𝐴...𝐵))

Proof of Theorem fzofzp1

Step	Hyp	Ref	Expression
1		elfzoel1 13608	. . . 4 ⊢ (𝐶 ∈ (𝐴..^𝐵) → 𝐴 ∈ ℤ)
2		uzid 12800	. . . 4 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ (ℤ≥‘𝐴))
3		peano2uz 12848	. . . 4 ⊢ (𝐴 ∈ (ℤ≥‘𝐴) → (𝐴 + 1) ∈ (ℤ≥‘𝐴))
4		fzoss1 13638	. . . 4 ⊢ ((𝐴 + 1) ∈ (ℤ≥‘𝐴) → ((𝐴 + 1)..^(𝐵 + 1)) ⊆ (𝐴..^(𝐵 + 1)))
5	1, 2, 3, 4	4syl 19	. . 3 ⊢ (𝐶 ∈ (𝐴..^𝐵) → ((𝐴 + 1)..^(𝐵 + 1)) ⊆ (𝐴..^(𝐵 + 1)))
6		1z 12554	. . . 4 ⊢ 1 ∈ ℤ
7		fzoaddel 13669	. . . 4 ⊢ ((𝐶 ∈ (𝐴..^𝐵) ∧ 1 ∈ ℤ) → (𝐶 + 1) ∈ ((𝐴 + 1)..^(𝐵 + 1)))
8	6, 7	mpan2 692	. . 3 ⊢ (𝐶 ∈ (𝐴..^𝐵) → (𝐶 + 1) ∈ ((𝐴 + 1)..^(𝐵 + 1)))
9	5, 8	sseldd 3923	. 2 ⊢ (𝐶 ∈ (𝐴..^𝐵) → (𝐶 + 1) ∈ (𝐴..^(𝐵 + 1)))
10		elfzoel2 13609	. . 3 ⊢ (𝐶 ∈ (𝐴..^𝐵) → 𝐵 ∈ ℤ)
11		fzval3 13686	. . 3 ⊢ (𝐵 ∈ ℤ → (𝐴...𝐵) = (𝐴..^(𝐵 + 1)))
12	10, 11	syl 17	. 2 ⊢ (𝐶 ∈ (𝐴..^𝐵) → (𝐴...𝐵) = (𝐴..^(𝐵 + 1)))
13	9, 12	eleqtrrd 2840	1 ⊢ (𝐶 ∈ (𝐴..^𝐵) → (𝐶 + 1) ∈ (𝐴...𝐵))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ⊆ wss 3890  ‘cfv 6496  (class class class)co 7364  1c1 11036   + caddc 11038  ℤcz 12521  ℤ_≥cuz 12785  ...cfz 13458  ..^cfzo 13605

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 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686  ax-cnex 11091  ax-resscn 11092  ax-1cn 11093  ax-icn 11094  ax-addcl 11095  ax-addrcl 11096  ax-mulcl 11097  ax-mulrcl 11098  ax-mulcom 11099  ax-addass 11100  ax-mulass 11101  ax-distr 11102  ax-i2m1 11103  ax-1ne0 11104  ax-1rid 11105  ax-rnegex 11106  ax-rrecex 11107  ax-cnre 11108  ax-pre-lttri 11109  ax-pre-lttrn 11110  ax-pre-ltadd 11111  ax-pre-mulgt0 11112

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 5523  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5581  df-we 5583  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-pred 6263  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7321  df-ov 7367  df-oprab 7368  df-mpo 7369  df-om 7815  df-1st 7939  df-2nd 7940  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11178  df-mnf 11179  df-xr 11180  df-ltxr 11181  df-le 11182  df-sub 11376  df-neg 11377  df-nn 12172  df-n0 12435  df-z 12522  df-uz 12786  df-fz 13459  df-fzo 13606

This theorem is referenced by:  fzofzp1b  13717  seqcaopr3  13996  seqcaopr2  13997  seqf1olem2a  13999  swrds1  14626  swrds2  14899  telfsumo  15762  telfsumo2  15763  fsumparts  15766  prodfn0  15856  prodfrec  15857  chnlt  18586  psgnunilem2  19467  gsumzaddlem  19893  dvfsumle  26004  dvfsumge  26005  dvfsumabs  26006  dvntaylp  26354  taylthlem2  26357  taylthlem2OLD  26358  pntlemr  27585  pntlemj  27586  uspgr2wlkeq  29735  wlkres  29758  wlkp1lem6  29766  pthdadjvtx  29817  upgrwlkdvdelem  29825  crctcshwlkn0lem4  29902  crctcshwlkn0lem5  29903  wwlksnred  29981  trlsegvdeglem1  30311  gsummulsubdishift2  33151  gsummulsubdishift1s  33152  gsummulsubdishift2s  33153  cycpmco2f1  33206  cycpmco2rn  33207  cycpmco2lem2  33209  cycpmco2lem3  33210  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmco2  33215  vietalem  33744  pfxwlk  35328  poimirlem24  37987  poimirlem25  37988  poimirlem29  37992  poimirlem31  37994  monoords  45756  fmul01  46036  dvnmptdivc  46392  dvnmul  46397  stoweidlem3  46457  fourierdlem1  46562  fourierdlem12  46573  fourierdlem14  46575  fourierdlem15  46576  fourierdlem20  46581  fourierdlem25  46586  fourierdlem27  46588  fourierdlem41  46602  fourierdlem46  46606  fourierdlem48  46608  fourierdlem49  46609  fourierdlem50  46610  fourierdlem54  46614  fourierdlem63  46623  fourierdlem64  46624  fourierdlem65  46625  fourierdlem69  46629  fourierdlem70  46630  fourierdlem71  46631  fourierdlem72  46632  fourierdlem73  46633  fourierdlem74  46634  fourierdlem75  46635  fourierdlem76  46636  fourierdlem79  46639  fourierdlem80  46640  fourierdlem81  46641  fourierdlem84  46644  fourierdlem88  46648  fourierdlem89  46649  fourierdlem90  46650  fourierdlem91  46651  fourierdlem92  46652  fourierdlem93  46653  fourierdlem94  46654  fourierdlem97  46657  fourierdlem101  46661  fourierdlem102  46662  fourierdlem103  46663  fourierdlem104  46664  fourierdlem111  46671  fourierdlem113  46673  fourierdlem114  46674  chnerlem2  47337  fzopred  47791  iccpartipre  47901  iccelpart  47913  iccpartiun  47914  icceuelpartlem  47915  icceuelpart  47916  iccpartdisj  47917  iccpartnel  47918  bgoldbtbndlem2  48302  bgoldbtbndlem3  48303  upgrimwlklem5  48397