MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elfzolt2 Structured version   Visualization version   Unicode version

Theorem elfzolt2 11966
Description: A member in a half-open integer interval is less than the upper bound. (Contributed by Stefan O'Rear, 15-Aug-2015.)
Assertion
Ref Expression
elfzolt2  |-  ( K  e.  ( M..^ N
)  ->  K  <  N )

Proof of Theorem elfzolt2
StepHypRef Expression
1 elfzoelz 11957 . . . 4  |-  ( K  e.  ( M..^ N
)  ->  K  e.  ZZ )
2 elfzoel1 11955 . . . 4  |-  ( K  e.  ( M..^ N
)  ->  M  e.  ZZ )
3 elfzoel2 11956 . . . 4  |-  ( K  e.  ( M..^ N
)  ->  N  e.  ZZ )
4 elfzo 11959 . . . 4  |-  ( ( K  e.  ZZ  /\  M  e.  ZZ  /\  N  e.  ZZ )  ->  ( K  e.  ( M..^ N )  <->  ( M  <_  K  /\  K  < 
N ) ) )
51, 2, 3, 4syl3anc 1276 . . 3  |-  ( K  e.  ( M..^ N
)  ->  ( K  e.  ( M..^ N )  <-> 
( M  <_  K  /\  K  <  N ) ) )
65ibi 249 . 2  |-  ( K  e.  ( M..^ N
)  ->  ( M  <_  K  /\  K  < 
N ) )
76simprd 469 1  |-  ( K  e.  ( M..^ N
)  ->  K  <  N )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    e. wcel 1898   class class class wbr 4418  (class class class)co 6320    < clt 9706    <_ cle 9707   ZZcz 10971  ..^cfzo 11952
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-1st 6825  df-2nd 6826  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-er 7394  df-en 7601  df-dom 7602  df-sdom 7603  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-nn 10643  df-n0 10904  df-z 10972  df-uz 11194  df-fz 11820  df-fzo 11953
This theorem is referenced by:  elfzolt3  11967  elfzolt2b  11968  fzonel  11970  elfzouz2  11971  fzonnsub  11980  fzospliti  11987  fzodisj  11989  fzouzdisj  11991  elfzo0  11993  elfzo1  12002  fzoaddel  12004  elincfzoext  12009  ssfzo12  12041  elfznelfzob  12052  modaddmodlo  12192  ccatrn  12775  swrds2  13072  fzomaxdiflem  13460  fzo0dvdseq  14413  bitsfzolem  14462  bitsfzolemOLD  14463  bitsfzo  14464  sadcaddlem  14486  sadaddlem  14495  sadasslem  14499  sadeq  14501  smuval2  14511  smupvallem  14512  smueqlem  14519  crt  14781  eulerthlem2  14785  prmgaplem6  15081  znf1o  19177  iundisj  22557  tgcgr4  24632  clwlkisclwwlklem2fv1  25566  iundisjf  28253  iundisjfi  28424  smattl  28675  smattr  28676  smatbl  28677  signsplypnf  29489  poimirlem17  32003  poimirlem20  32006  hashgcdlem  36120  elfzfzo  37561  elfzop1le2  37578  dvnmul  37904  iblspltprt  37936  itgspltprt  37942  stoweidlem3  37964  fourierdlem12  38082  fourierdlem50  38121  fourierdlem64  38135  fourierdlem79  38150  iccpartgt  38876  m1modmmod  40693
  Copyright terms: Public domain W3C validator