| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > elfz2 | Structured version Visualization version GIF version | ||
| Description: Membership in a finite set of sequential integers. We use the fact that an operation's value is empty outside of its domain to show 𝑀 ∈ ℤ and 𝑁 ∈ ℤ. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| Ref | Expression |
|---|---|
| elfz2 | ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | anass 473 | . 2 ⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))) | |
| 2 | df-3an 1103 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ)) | |
| 3 | 2 | anbi1i 635 | . 2 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) ↔ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
| 4 | elfz1 13539 | . . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) | |
| 5 | 3anass 1109 | . . . . 5 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁) ↔ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) | |
| 6 | ibar 537 | . . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))))) | |
| 7 | 5, 6 | bitrid 286 | . . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))))) |
| 8 | 4, 7 | bitrd 282 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))))) |
| 9 | fzf 13538 | . . . . . . 7 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ | |
| 10 | 9 | fdmi 6718 | . . . . . 6 ⊢ dom ... = (ℤ × ℤ) |
| 11 | 10 | ndmov 7595 | . . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = ∅) |
| 12 | 11 | eleq2d 2855 | . . . 4 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ 𝐾 ∈ ∅)) |
| 13 | noel 4299 | . . . . . 6 ⊢ ¬ 𝐾 ∈ ∅ | |
| 14 | 13 | pm2.21i 120 | . . . . 5 ⊢ (𝐾 ∈ ∅ → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
| 15 | simpl 487 | . . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) | |
| 16 | 14, 15 | pm5.21ni 380 | . . . 4 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ ∅ ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))))) |
| 17 | 12, 16 | bitrd 282 | . . 3 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))))) |
| 18 | 8, 17 | pm2.61i 184 | . 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))) |
| 19 | 1, 3, 18 | 3bitr4ri 307 | 1 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 ∈ wcel 2149 ∅c0 4294 𝒫 cpw 4567 class class class wbr 5113 × cxp 5660 (class class class)co 7411 ≤ cle 11243 ℤcz 12590 ...cfz 13534 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pr 5405 ax-un 7733 ax-cnex 11155 ax-resscn 11156 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-id 5557 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-fv 6545 df-ov 7414 df-oprab 7415 df-mpo 7416 df-1st 7985 df-2nd 7986 df-neg 11443 df-z 12591 df-fz 13535 |
| This theorem is referenced by: elfzd 13542 elfz4 13544 elfzuzb 13545 0nelfz1 13570 uzsubsubfz 13573 fzmmmeqm 13584 fzpreddisj 13600 elfz1b 13620 fzdif1 13632 fzp1nel 13638 elfz0ubfz0 13659 elfz0fzfz0 13660 fz0fzelfz0 13661 fz0fzdiffz0 13664 elfzmlbp 13666 preduz 13677 fzind2 13816 swrdswrdlem 14740 swrdswrd 14741 pfxccatin12lem2a 14763 pfxccatin12lem1 14764 swrdccatin2 14765 pfxccatin12lem2 14767 pfxccat3 14770 2cshwcshw 14861 cshwcsh2id 14864 fprodntriv 15995 fprodeq0 16028 prmgaplem4 17113 chfacfscmulgsum 22985 chfacfpmmulgsum 22989 gausslemma2dlem3 27497 2lgslem1a1 27518 crctcshwlkn0lem3 30101 fzne2d 42636 fmul01lt1lem2 46192 dvnprodlem2 46552 stoweidlem34 46639 fourierdlem12 46724 etransclem10 46849 etransclem24 46863 elfzelfzlble 47946 iccpartiltu 48059 31prm 48237 nnsum4primeseven 48453 nnsum4primesevenALTV 48454 |
| Copyright terms: Public domain | W3C validator |