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

Theorem uztrn2 10292
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 2380 . . 3  |-  ( N  e.  Z  <->  N  e.  ( ZZ>= `  K )
)
3 uztrn 10291 . . . 4  |-  ( ( M  e.  ( ZZ>= `  N )  /\  N  e.  ( ZZ>= `  K )
)  ->  M  e.  ( ZZ>= `  K )
)
43ancoms 439 . . 3  |-  ( ( N  e.  ( ZZ>= `  K )  /\  M  e.  ( ZZ>= `  N )
)  ->  M  e.  ( ZZ>= `  K )
)
52, 4sylanb 458 . 2  |-  ( ( N  e.  Z  /\  M  e.  ( ZZ>= `  N ) )  ->  M  e.  ( ZZ>= `  K ) )
65, 1syl6eleqr 2407 1  |-  ( ( N  e.  Z  /\  M  e.  ( ZZ>= `  N ) )  ->  M  e.  Z )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1633    e. wcel 1701   ` cfv 5292   ZZ>=cuz 10277
This theorem is referenced by:  eluznn0  10335  elfzuz2  10848  expmulnbnd  11280  bcval5  11377  rexuz3  11879  r19.29uz  11881  r19.2uz  11882  clim2  12025  clim2c  12026  clim0c  12028  rlimclim1  12066  2clim  12093  climabs0  12106  climcn1  12112  climcn2  12113  climsqz  12161  climsqz2  12162  clim2ser  12175  clim2ser2  12176  climub  12182  isercolllem1  12185  isercoll  12188  climsup  12190  caurcvg2  12197  serf0  12200  iseraltlem1  12201  iseralt  12204  o1fsum  12318  cvgcmp  12321  cvgcmpce  12323  isumsup2  12352  climcndslem1  12355  climcndslem2  12356  climcnds  12357  mertenslem1  12387  mertenslem2  12388  rpnnen2lem6  12545  rpnnen2lem7  12546  rpnnen2lem9  12548  rpnnen2lem11  12550  pcmpt2  12988  pcmptdvds  12989  prmreclem4  13013  prmreclem5  13014  prmreclem6  13015  vdwnnlem2  13090  2expltfac  13152  lmbrf  17046  lmss  17082  lmres  17084  1stcelcls  17243  txlm  17398  uzrest  17644  lmmcvg  18740  lmmbrf  18741  lmnn  18742  iscau4  18758  iscauf  18759  caucfil  18762  cmetcaulem  18767  iscmet3lem3  18769  iscmet3lem1  18770  causs  18777  lmle  18780  lmclim  18781  caubl  18786  caublcls  18787  ovolunlem1a  18908  volsuplem  18965  uniioombllem3  18993  mbflimsup  19074  mbfi1fseqlem6  19128  ulm2  19817  ulmcaulem  19824  ulmcau  19825  ulmss  19827  ulmdvlem1  19830  ulmdvlem3  19832  mtest  19834  itgulm  19837  birthdaylem2  20300  chtub  20504  logfaclbnd  20514  bclbnd  20572  bposlem3  20578  bposlem4  20579  bposlem5  20580  bposlem6  20581  lgsdilem2  20623  chebbnd1lem1  20671  chebbnd1lem2  20672  chebbnd1lem3  20673  dchrisumlema  20690  dchrisumlem2  20692  dchrisumlem3  20693  dchrisum0lem1b  20717  dchrisum0lem1  20718  pntrsumbnd2  20769  pntpbnd1  20788  pntpbnd2  20789  pntlemh  20801  pntlemq  20803  pntlemr  20804  pntlemj  20805  pntlemf  20807  minvecolem3  21510  minvecolem4  21514  h2hcau  21614  h2hlm  21615  chscllem2  22272  elfzo1  23300  sinccvglem  24289  clim2div  24397  ntrivcvgfvn0  24404  ntrivcvgmullem  24406  lmclim2  25623  geomcau  25624  caures  25625  caushft  25626  heibor1lem  25681  rrncmslem  25704  climinf  26880  stirlinglem12  26982
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-cnex 8838  ax-resscn 8839  ax-pre-lttri 8856  ax-pre-lttrn 8857
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-nel 2482  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-mpt 4116  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-ov 5903  df-er 6702  df-en 6907  df-dom 6908  df-sdom 6909  df-pnf 8914  df-mnf 8915  df-xr 8916  df-ltxr 8917  df-le 8918  df-neg 9085  df-z 10072  df-uz 10278
  Copyright terms: Public domain W3C validator