Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fzofi | Structured version Visualization version GIF version |
Description: Half-open integer sets are finite. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
Ref | Expression |
---|---|
fzofi | ⊢ (𝑀..^𝑁) ∈ Fin |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fzoval 13317 | . . . 4 ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) | |
2 | 1 | adantl 481 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
3 | fzfi 13620 | . . 3 ⊢ (𝑀...(𝑁 − 1)) ∈ Fin | |
4 | 2, 3 | eqeltrdi 2847 | . 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) ∈ Fin) |
5 | fzof 13313 | . . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ | |
6 | 5 | fdmi 6596 | . . . 4 ⊢ dom ..^ = (ℤ × ℤ) |
7 | 6 | ndmov 7434 | . . 3 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅) |
8 | 0fin 8916 | . . 3 ⊢ ∅ ∈ Fin | |
9 | 7, 8 | eqeltrdi 2847 | . 2 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) ∈ Fin) |
10 | 4, 9 | pm2.61i 182 | 1 ⊢ (𝑀..^𝑁) ∈ Fin |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ∅c0 4253 𝒫 cpw 4530 × cxp 5578 (class class class)co 7255 Fincfn 8691 1c1 10803 − cmin 11135 ℤcz 12249 ...cfz 13168 ..^cfzo 13311 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-nn 11904 df-n0 12164 df-z 12250 df-uz 12512 df-fz 13169 df-fzo 13312 |
This theorem is referenced by: uzindi 13630 fnfzo0hashnn0 14091 wrdfin 14163 hashwrdn 14178 ccatalpha 14226 telfsumo 15442 fsumparts 15446 geoserg 15506 pwdif 15508 bitsfi 16072 bitsinv1 16077 bitsinvp1 16084 sadcaddlem 16092 sadadd2lem 16094 sadadd3 16096 sadaddlem 16101 sadasslem 16105 sadeq 16107 crth 16407 phimullem 16408 eulerthlem2 16411 eulerth 16412 phisum 16419 prmgaplem3 16682 cshwshashnsame 16733 ablfaclem3 19605 ablfac2 19607 iunmbl 24622 volsup 24625 dvfsumle 25090 dvfsumge 25091 dvfsumabs 25092 advlogexp 25715 dchrisumlem1 26542 dchrisumlem2 26543 dchrisum 26545 vdegp1bi 27807 eupthfi 28470 trlsegvdeglem6 28490 fz1nnct 31026 cycpmconjslem2 31324 sigapildsys 32030 carsgclctunlem3 32187 ccatmulgnn0dir 32421 ofcccat 32422 signsplypnf 32429 signsvvf 32458 prodfzo03 32483 fsum2dsub 32487 reprle 32494 reprsuc 32495 reprfi 32496 reprlt 32499 hashreprin 32500 reprgt 32501 reprinfz1 32502 reprpmtf1o 32506 breprexplema 32510 breprexplemc 32512 breprexpnat 32514 circlemeth 32520 circlemethnat 32521 circlevma 32522 circlemethhgt 32523 hgt750lema 32537 lpadlem2 32560 mvrsfpw 33368 poimirlem26 35730 poimirlem27 35731 poimirlem28 35732 poimirlem30 35734 frlmfzowrdb 40161 frlmvscadiccat 40163 fltnltalem 40415 amgm2d 41698 amgm3d 41699 amgm4d 41700 fourierdlem25 43563 fourierdlem70 43607 fourierdlem71 43608 fourierdlem73 43610 fourierdlem79 43616 fourierdlem80 43617 meaiunlelem 43896 2pwp1prm 44929 nn0sumshdiglemA 45853 nn0sumshdiglemB 45854 nn0mullong 45859 amgmw2d 46394 |
Copyright terms: Public domain | W3C validator |