Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > elfz2 | 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 396 | . 2 ⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))) | |
2 | df-3an 947 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ)) | |
3 | 2 | anbi1i 451 | . 2 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) ↔ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
4 | df-fz 9742 | . . . 4 ⊢ ... = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ {𝑧 ∈ ℤ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) | |
5 | 4 | elmpocl 5934 | . . 3 ⊢ (𝐾 ∈ (𝑀...𝑁) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
6 | simpl 108 | . . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) | |
7 | elfz1 9746 | . . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) | |
8 | 3anass 949 | . . . . 5 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁) ↔ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) | |
9 | ibar 297 | . . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))))) | |
10 | 8, 9 | syl5bb 191 | . . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))))) |
11 | 7, 10 | bitrd 187 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))))) |
12 | 5, 6, 11 | pm5.21nii 676 | . 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))) |
13 | 1, 3, 12 | 3bitr4ri 212 | 1 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∧ w3a 945 ∈ wcel 1463 {crab 2395 class class class wbr 3897 (class class class)co 5740 ≤ cle 7765 ℤcz 9008 ...cfz 9741 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 586 ax-in2 587 ax-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-14 1475 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 ax-sep 4014 ax-pow 4066 ax-pr 4099 ax-setind 4420 ax-cnex 7675 ax-resscn 7676 |
This theorem depends on definitions: df-bi 116 df-3or 946 df-3an 947 df-tru 1317 df-fal 1320 df-nf 1420 df-sb 1719 df-eu 1978 df-mo 1979 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2245 df-ne 2284 df-ral 2396 df-rex 2397 df-rab 2400 df-v 2660 df-sbc 2881 df-dif 3041 df-un 3043 df-in 3045 df-ss 3052 df-pw 3480 df-sn 3501 df-pr 3502 df-op 3504 df-uni 3705 df-br 3898 df-opab 3958 df-id 4183 df-xp 4513 df-rel 4514 df-cnv 4515 df-co 4516 df-dm 4517 df-iota 5056 df-fun 5093 df-fv 5099 df-ov 5743 df-oprab 5744 df-mpo 5745 df-neg 7900 df-z 9009 df-fz 9742 |
This theorem is referenced by: elfz4 9750 elfzuzb 9751 uzsubsubfz 9778 fzmmmeqm 9789 fzpreddisj 9802 elfz1b 9821 fzp1nel 9835 elfz0ubfz0 9853 elfz0fzfz0 9854 fz0fzelfz0 9855 fz0fzdiffz0 9858 elfzmlbp 9860 fzind2 9967 iseqf1olemqcl 10210 iseqf1olemnab 10212 iseqf1olemab 10213 seq3f1olemqsumkj 10222 seq3f1olemqsumk 10223 summodclem2a 11101 fsum3 11107 fsum3cvg3 11116 fsumcl2lem 11118 fsumadd 11126 fsummulc2 11168 |
Copyright terms: Public domain | W3C validator |