![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elfz | Structured version Visualization version GIF version |
Description: Membership in a finite set of sequential integers. (Contributed by NM, 29-Sep-2005.) |
Ref | Expression |
---|---|
elfz | ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfz1 12445 | . . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) | |
2 | 3anass 1081 | . . . . 5 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁) ↔ (𝐾 ∈ ℤ ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) | |
3 | 2 | baib 982 | . . . 4 ⊢ (𝐾 ∈ ℤ → ((𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
4 | 1, 3 | sylan9bb 738 | . . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
5 | 4 | 3impa 1100 | . 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
6 | 5 | 3comr 1119 | 1 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 ∧ w3a 1072 ∈ wcel 2103 class class class wbr 4760 (class class class)co 6765 ≤ cle 10188 ℤcz 11490 ...cfz 12440 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-sep 4889 ax-nul 4897 ax-pr 5011 ax-cnex 10105 ax-resscn 10106 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ral 3019 df-rex 3020 df-rab 3023 df-v 3306 df-sbc 3542 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-nul 4024 df-if 4195 df-sn 4286 df-pr 4288 df-op 4292 df-uni 4545 df-br 4761 df-opab 4821 df-id 5128 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-iota 5964 df-fun 6003 df-fv 6009 df-ov 6768 df-oprab 6769 df-mpt2 6770 df-neg 10382 df-z 11491 df-fz 12441 |
This theorem is referenced by: elfz5 12448 fzadd2 12490 fznatpl1 12509 fzrev 12517 fzctr 12566 elfzo 12587 seqf1olem1 12955 bcval5 13220 isprm3 15519 hashdvds 15603 eulerthlem2 15610 prmreclem5 15747 aannenlem1 24203 basellem3 24929 chtub 25057 bcmono 25122 bposlem1 25129 lgseisenlem1 25220 lgsquadlem1 25225 2lgslem1a 25236 axlowdimlem3 25944 axlowdimlem7 25948 axlowdimlem16 25957 axlowdimlem17 25958 axlowdim 25961 submateqlem1 30103 lmatfvlem 30111 bcneg1 31850 poimirlem15 33656 poimirlem24 33665 poimirlem28 33669 mblfinlem2 33679 itg2addnclem2 33694 fzmul 33769 cntotbnd 33827 fzsplit1nn0 37736 irrapxlem3 37807 pellexlem5 37816 acongrep 37966 fzneg 37968 jm2.23 37982 fmul01 40232 fmuldfeq 40235 stoweidlem26 40663 fourierdlem11 40755 fourierdlem12 40756 fourierdlem15 40759 fourierdlem79 40822 smfmullem4 41424 pfxccat3a 41856 |
Copyright terms: Public domain | W3C validator |