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

Theorem uztrn2 10883
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 2507 . . 3  |-  ( N  e.  Z  <->  N  e.  ( ZZ>= `  K )
)
3 uztrn 10882 . . . 4  |-  ( ( M  e.  ( ZZ>= `  N )  /\  N  e.  ( ZZ>= `  K )
)  ->  M  e.  ( ZZ>= `  K )
)
43ancoms 453 . . 3  |-  ( ( N  e.  ( ZZ>= `  K )  /\  M  e.  ( ZZ>= `  N )
)  ->  M  e.  ( ZZ>= `  K )
)
52, 4sylanb 472 . 2  |-  ( ( N  e.  Z  /\  M  e.  ( ZZ>= `  N ) )  ->  M  e.  ( ZZ>= `  K ) )
65, 1syl6eleqr 2534 1  |-  ( ( N  e.  Z  /\  M  e.  ( ZZ>= `  N ) )  ->  M  e.  Z )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   ` cfv 5423   ZZ>=cuz 10866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pow 4475  ax-pr 4536  ax-un 6377  ax-cnex 9343  ax-resscn 9344  ax-pre-lttri 9361  ax-pre-lttrn 9362
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-nel 2614  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-sbc 3192  df-csb 3294  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-pw 3867  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-br 4298  df-opab 4356  df-mpt 4357  df-id 4641  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5386  df-fun 5425  df-fn 5426  df-f 5427  df-f1 5428  df-fo 5429  df-f1o 5430  df-fv 5431  df-ov 6099  df-er 7106  df-en 7316  df-dom 7317  df-sdom 7318  df-pnf 9425  df-mnf 9426  df-xr 9427  df-ltxr 9428  df-le 9429  df-neg 9603  df-z 10652  df-uz 10867
This theorem is referenced by:  eluznn0  10929  eluznn  10930  elfzuz2  11461  rexuz3  12841  r19.29uz  12843  r19.2uz  12844  clim2  12987  clim2c  12988  clim0c  12990  rlimclim1  13028  2clim  13055  climabs0  13068  climcn1  13074  climcn2  13075  climsqz  13123  climsqz2  13124  clim2ser  13137  clim2ser2  13138  climub  13144  climsup  13152  caurcvg2  13160  serf0  13163  iseraltlem1  13164  iseralt  13167  cvgcmp  13284  cvgcmpce  13286  isumsup2  13314  mertenslem1  13349  lmbrf  18869  lmss  18907  lmres  18909  txlm  19226  uzrest  19475  lmmcvg  20777  lmmbrf  20778  iscau4  20795  iscauf  20796  caucfil  20799  iscmet3lem3  20806  iscmet3lem1  20807  lmle  20817  lmclim  20818  mbflimsup  21149  ulm2  21855  ulmcaulem  21864  ulmcau  21865  ulmss  21867  ulmdvlem1  21870  ulmdvlem3  21872  mtest  21874  itgulm  21878  logfaclbnd  22566  bposlem6  22633  lgamgulmlem4  27023  lgamcvg2  27046  sinccvglem  27322  clim2div  27409  ntrivcvgfvn0  27419  ntrivcvgmullem  27421  fprodeq0  27491  lmclim2  28659  geomcau  28660  caures  28661  caushft  28662  heibor1lem  28713  rrncmslem  28736  climinf  29784  stirlinglem12  29885
  Copyright terms: Public domain W3C validator