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

Theorem uztrn2 11210
Description: Transitive law for sets of upper integers. (Contributed by Mario Carneiro, 26-Dec-2013.)
Hypothesis
Ref Expression
uztrn2.1  |-  Z  =  ( ZZ>= `  K )
Assertion
Ref Expression
uztrn2  |-  ( ( N  e.  Z  /\  M  e.  ( ZZ>= `  N ) )  ->  M  e.  Z )

Proof of Theorem uztrn2
StepHypRef Expression
1 uztrn2.1 . . . 4  |-  Z  =  ( ZZ>= `  K )
21eleq2i 2532 . . 3  |-  ( N  e.  Z  <->  N  e.  ( ZZ>= `  K )
)
3 uztrn 11209 . . . 4  |-  ( ( M  e.  ( ZZ>= `  N )  /\  N  e.  ( ZZ>= `  K )
)  ->  M  e.  ( ZZ>= `  K )
)
43ancoms 459 . . 3  |-  ( ( N  e.  ( ZZ>= `  K )  /\  M  e.  ( ZZ>= `  N )
)  ->  M  e.  ( ZZ>= `  K )
)
52, 4sylanb 479 . 2  |-  ( ( N  e.  Z  /\  M  e.  ( ZZ>= `  N ) )  ->  M  e.  ( ZZ>= `  K ) )
65, 1syl6eleqr 2551 1  |-  ( ( N  e.  Z  /\  M  e.  ( ZZ>= `  N ) )  ->  M  e.  Z )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1455    e. wcel 1898   ` cfv 5605   ZZ>=cuz 11193
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-pre-lttri 9644  ax-pre-lttrn 9645
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-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  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-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-ov 6323  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-neg 9894  df-z 10972  df-uz 11194
This theorem is referenced by:  eluznn0  11262  eluznn  11263  elfzuz2  11839  rexuz3  13466  r19.29uz  13468  r19.2uz  13469  clim2  13623  clim2c  13624  clim0c  13626  rlimclim1  13664  2clim  13691  climabs0  13704  climcn1  13710  climcn2  13711  climsqz  13759  climsqz2  13760  clim2ser  13773  clim2ser2  13774  climub  13780  climsup  13788  caurcvg2  13799  serf0  13802  iseraltlem1  13803  iseralt  13806  cvgcmp  13931  cvgcmpce  13933  isumsup2  13959  mertenslem1  13995  clim2div  14000  ntrivcvgfvn0  14010  ntrivcvgmullem  14012  fprodeq0  14084  lmbrf  20331  lmss  20369  lmres  20371  txlm  20718  uzrest  20967  lmmcvg  22286  lmmbrf  22287  iscau4  22304  iscauf  22305  caucfil  22308  iscmet3lem3  22315  iscmet3lem1  22316  lmle  22326  lmclim  22327  mbflimsup  22679  mbflimsupOLD  22680  ulm2  23396  ulmcaulem  23405  ulmcau  23406  ulmss  23408  ulmdvlem1  23411  ulmdvlem3  23413  mtest  23415  itgulm  23419  logfaclbnd  24206  bposlem6  24273  caures  32135  caushft  32136  dvgrat  36706  cvgdvgrat  36707  climinf  37770  climinfOLD  37771  clim2f  37802  clim2cf  37817  clim0cf  37821
  Copyright terms: Public domain W3C validator