Theorem fzofi 14030

Description: Half-open integer sets are finite. (Contributed by Stefan O'Rear, 15-Aug-2015.)

Assertion

Ref	Expression
fzofi	⊢ (𝑀..^𝑁) ∈ Fin

Proof of Theorem fzofi

Step	Hyp	Ref	Expression
1		fzoval 13707	. . . 4 ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
2	1	adantl 487	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
3		fzfi 14028	. . 3 ⊢ (𝑀...(𝑁 − 1)) ∈ Fin
4	2, 3	eqeltrdi 2873	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) ∈ Fin)
5		fzof 13703	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
6	5	fdmi 6721	. . . 4 ⊢ dom ..^ = (ℤ × ℤ)
7	6	ndmov 7604	. . 3 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅)
8		0fi 9046	. . 3 ⊢ ∅ ∈ Fin
9	7, 8	eqeltrdi 2873	. 2 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) ∈ Fin)
10	4, 9	pm2.61i 184	1 ⊢ (𝑀..^𝑁) ∈ Fin

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∅c0 4286  𝒫 cpw 4564   × cxp 5661  (class class class)co 7419  Fincfn 8949  1c1 11118   − cmin 11458  ℤcz 12608  ...cfz 13553  ..^cfzo 13701

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-cnex 11173  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-i2m1 11185  ax-1ne0 11186  ax-1rid 11187  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190  ax-pre-lttri 11191  ax-pre-lttrn 11192  ax-pre-ltadd 11193  ax-pre-mulgt0 11194

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-1st 7992  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-fin 8953  df-pnf 11262  df-mnf 11263  df-xr 11264  df-ltxr 11265  df-le 11266  df-sub 11460  df-neg 11461  df-nn 12251  df-n0 12522  df-z 12609  df-uz 12881  df-fz 13554  df-fzo 13702

This theorem is used by:  uzindi  14038  fnfzo0hashnn0  14508  tpf1o  14558  wrdfin  14589  hashwrdn  14604  ccatalpha  14652  s7f1o  15029  telfsumo  15879  fsumparts  15883  geoserg  15945  pwdif  15947  bitsfi  16519  bitsinv1  16524  bitsinvp1  16531  sadcaddlem  16539  sadadd2lem  16541  sadadd3  16543  sadaddlem  16548  sadasslem  16552  sadeq  16554  crth  16861  phimullem  16862  eulerthlem2  16865  eulerth  16866  phisum  16874  prmgaplem3  17137  cshwshashnsame  17187  ablfaclem3  20205  ablfac2  20207  iunmbl  25765  volsup  25768  dvfsumle  26233  dvfsumge  26234  dvfsumabs  26235  advlogexp  26873  dchrisumlem1  27706  dchrisumlem2  27707  dchrisum  27709  vdegp1bi  29947  eupthfi  30629  trlsegvdeglem6  30649  fz1nnct  33218  wrdfsupp  33329  gsummulsubdishift1  33454  gsummulsubdishift2  33455  cycpmconjslem2  33541  evl1deg2  33933  evl1deg3  33934  gsummoncoe1fzo  33953  ply1degltdimlem  34078  sigapildsys  34619  carsgclctunlem3  34777  ccatmulgnn0dir  34999  ofcccat  35000  signsplypnf  35004  signsvvf  35033  prodfzo03  35057  fsum2dsub  35061  reprle  35068  reprsuc  35069  reprfi  35070  reprlt  35073  hashreprin  35074  reprgt  35075  reprinfz1  35076  reprpmtf1o  35080  breprexplema  35084  breprexplemc  35086  breprexpnat  35088  circlemeth  35094  circlemethnat  35095  circlevma  35096  circlemethhgt  35097  hgt750lema  35111  lpadlem2  35137  mvrsfpw  36037  poimirlem26  38356  poimirlem27  38357  poimirlem28  38358  poimirlem30  38360  frlmfzowrdb  43338  frlmvscadiccat  43340  fltnltalem  43454  amgm2d  44984  amgm3d  44985  amgm4d  44986  fourierdlem25  46906  fourierdlem70  46950  fourierdlem71  46951  fourierdlem73  46953  fourierdlem79  46959  fourierdlem80  46960  meaiunlelem  47242  2pwp1prm  48401  gpgorder  48884  nn0sumshdiglemA  49458  nn0sumshdiglemB  49459  nn0mullong  49464  amgmw2d  50711