ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elfz2 Unicode version

Theorem elfz2 9400
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  M  e.  ZZ and  N  e.  ZZ. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
elfz2  |-  ( K  e.  ( M ... N )  <->  ( ( M  e.  ZZ  /\  N  e.  ZZ  /\  K  e.  ZZ )  /\  ( M  <_  K  /\  K  <_  N ) ) )

Proof of Theorem elfz2
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 anass 393 . 2  |-  ( ( ( ( M  e.  ZZ  /\  N  e.  ZZ )  /\  K  e.  ZZ )  /\  ( M  <_  K  /\  K  <_  N ) )  <->  ( ( M  e.  ZZ  /\  N  e.  ZZ )  /\  ( K  e.  ZZ  /\  ( M  <_  K  /\  K  <_  N ) ) ) )
2 df-3an 926 . . 3  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ  /\  K  e.  ZZ )  <->  ( ( M  e.  ZZ  /\  N  e.  ZZ )  /\  K  e.  ZZ ) )
32anbi1i 446 . 2  |-  ( ( ( M  e.  ZZ  /\  N  e.  ZZ  /\  K  e.  ZZ )  /\  ( M  <_  K  /\  K  <_  N ) )  <->  ( ( ( M  e.  ZZ  /\  N  e.  ZZ )  /\  K  e.  ZZ )  /\  ( M  <_  K  /\  K  <_  N
) ) )
4 df-fz 9394 . . . 4  |-  ...  =  ( x  e.  ZZ ,  y  e.  ZZ  |->  { z  e.  ZZ  |  ( x  <_ 
z  /\  z  <_  y ) } )
54elmpt2cl 5824 . . 3  |-  ( K  e.  ( M ... N )  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
6 simpl 107 . . 3  |-  ( ( ( M  e.  ZZ  /\  N  e.  ZZ )  /\  ( K  e.  ZZ  /\  ( M  <_  K  /\  K  <_  N ) ) )  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
7 elfz1 9398 . . . 4  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( K  e.  ( M ... N )  <-> 
( K  e.  ZZ  /\  M  <_  K  /\  K  <_  N ) ) )
8 3anass 928 . . . . 5  |-  ( ( K  e.  ZZ  /\  M  <_  K  /\  K  <_  N )  <->  ( K  e.  ZZ  /\  ( M  <_  K  /\  K  <_  N ) ) )
9 ibar 295 . . . . 5  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( K  e.  ZZ  /\  ( M  <_  K  /\  K  <_  N ) )  <->  ( ( M  e.  ZZ  /\  N  e.  ZZ )  /\  ( K  e.  ZZ  /\  ( M  <_  K  /\  K  <_  N ) ) ) ) )
108, 9syl5bb 190 . . . 4  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( K  e.  ZZ  /\  M  <_  K  /\  K  <_  N
)  <->  ( ( M  e.  ZZ  /\  N  e.  ZZ )  /\  ( K  e.  ZZ  /\  ( M  <_  K  /\  K  <_  N ) ) ) ) )
117, 10bitrd 186 . . 3  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( K  e.  ( M ... N )  <-> 
( ( M  e.  ZZ  /\  N  e.  ZZ )  /\  ( K  e.  ZZ  /\  ( M  <_  K  /\  K  <_  N ) ) ) ) )
125, 6, 11pm5.21nii 655 . 2  |-  ( K  e.  ( M ... N )  <->  ( ( M  e.  ZZ  /\  N  e.  ZZ )  /\  ( K  e.  ZZ  /\  ( M  <_  K  /\  K  <_  N ) ) ) )
131, 3, 123bitr4ri 211 1  |-  ( K  e.  ( M ... N )  <->  ( ( M  e.  ZZ  /\  N  e.  ZZ  /\  K  e.  ZZ )  /\  ( M  <_  K  /\  K  <_  N ) ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 102    <-> wb 103    /\ w3a 924    e. wcel 1438   {crab 2363   class class class wbr 3837  (class class class)co 5634    <_ cle 7502   ZZcz 8720   ...cfz 9393
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-pow 4001  ax-pr 4027  ax-setind 4343  ax-cnex 7415  ax-resscn 7416
This theorem depends on definitions:  df-bi 115  df-3or 925  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-ral 2364  df-rex 2365  df-rab 2368  df-v 2621  df-sbc 2839  df-dif 2999  df-un 3001  df-in 3003  df-ss 3010  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-opab 3892  df-id 4111  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-iota 4967  df-fun 5004  df-fv 5010  df-ov 5637  df-oprab 5638  df-mpt2 5639  df-neg 7635  df-z 8721  df-fz 9394
This theorem is referenced by:  elfz4  9402  elfzuzb  9403  uzsubsubfz  9430  fzmmmeqm  9440  fzpreddisj  9452  elfz1b  9471  fzp1nel  9485  elfz0ubfz0  9501  elfz0fzfz0  9502  fz0fzelfz0  9503  fz0fzdiffz0  9506  elfzmlbp  9508  fzind2  9615  iseqf1olemqcl  9880  iseqf1olemnab  9882  iseqf1olemab  9883  seq3f1olemqsumkj  9892  seq3f1olemqsumk  9893  isummolem2a  10733  fisum  10740  fsum3  10741  fisumcvg3  10750  fsumcl2lem  10753  fsumadd  10761  fsummulc2  10803
  Copyright terms: Public domain W3C validator