Theorem fzofi 14117

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 13794	. . . 4 ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
2	1	adantl 487	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
3		fzfi 14115	. . 3 ⊢ (𝑀...(𝑁 − 1)) ∈ Fin
4	2, 3	eqeltrdi 2869	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) ∈ Fin)
5		fzof 13790	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
6	5	fdmi 6721	. . . 4 ⊢ dom ..^ = (ℤ × ℤ)
7	6	ndmov 7605	. . 3 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅)
8		0fi 9070	. . 3 ⊢ ∅ ∈ Fin
9	7, 8	eqeltrdi 2869	. 2 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) ∈ Fin)
10	4, 9	pm2.61i 184	1 ⊢ (𝑀..^𝑁) ∈ Fin

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∅c0 4279  𝒫 cpw 4557   × cxp 5649  (class class class)co 7420  Fincfn 8973  1c1 11201   − cmin 11541  ℤcz 12693  ...cfz 13639  ..^cfzo 13788

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-1o 8476  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-nn 12336  df-n0 12607  df-z 12694  df-uz 12966  df-fz 13640  df-fzo 13789

This theorem is used by:  uzindi  14125  fnfzo0hashnn0  14596  tpf1o  14646  wrdfin  14677  hashwrdn  14692  ccatalpha  14740  s7f1o  15119  telfsumo  15969  fsumparts  15973  geoserg  16035  pwdif  16037  bitsfi  16607  bitsinv1  16612  bitsinvp1  16619  sadcaddlem  16627  sadadd2lem  16629  sadadd3  16631  sadaddlem  16636  sadasslem  16640  sadeq  16642  crth  16955  phimullem  16956  eulerthlem2  16959  eulerth  16960  phisum  16968  prmgaplem3  17231  cshwshashnsame  17281  ablfaclem3  20303  ablfac2  20305  iunmbl  25874  volsup  25877  dvfsumle  26341  dvfsumge  26342  dvfsumabs  26343  advlogexp  26983  dchrisumlem1  27816  dchrisumlem2  27817  dchrisum  27819  vdegp1bi  30118  eupthfi  30806  trlsegvdeglem6  30826  fz1nnct  33393  wrdfsupp  33504  gsummulsubdishift1  33629  gsummulsubdishift2  33630  cycpmconjslem2  33716  evl1deg2  34109  evl1deg3  34110  gsummoncoe1fzo  34129  ply1degltdimlem  34254  sigapildsys  34795  carsgclctunlem3  34952  ccatmulgnn0dir  35174  ofcccat  35175  signsplypnf  35179  signsvvf  35208  prodfzo03  35232  fsum2dsub  35236  reprle  35243  reprsuc  35244  reprfi  35245  reprlt  35248  hashreprin  35249  reprgt  35250  reprinfz1  35251  reprpmtf1o  35255  breprexplema  35259  breprexplemc  35261  breprexpnat  35263  circlemeth  35269  circlemethnat  35270  circlevma  35271  circlemethhgt  35272  hgt750lema  35286  lpadlem2  35312  mvrsfpw  36271  poimirlem26  38564  poimirlem27  38565  poimirlem28  38566  poimirlem30  38568  frlmfzowrdb  43571  frlmvscadiccat  43573  fltnltalem  43673  amgm2d  45197  amgm3d  45198  amgm4d  45199  fourierdlem25  47141  fourierdlem70  47185  fourierdlem71  47186  fourierdlem73  47188  fourierdlem79  47194  fourierdlem80  47195  meaiunlelem  47477  2pwp1prm  48673  gpgorder  49156  nn0sumshdiglemA  49730  nn0sumshdiglemB  49731  nn0mullong  49736  amgmw2d  50988