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

Theorem uztrn2 10495
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 2499 . . 3  |-  ( N  e.  Z  <->  N  e.  ( ZZ>= `  K )
)
3 uztrn 10494 . . . 4  |-  ( ( M  e.  ( ZZ>= `  N )  /\  N  e.  ( ZZ>= `  K )
)  ->  M  e.  ( ZZ>= `  K )
)
43ancoms 440 . . 3  |-  ( ( N  e.  ( ZZ>= `  K )  /\  M  e.  ( ZZ>= `  N )
)  ->  M  e.  ( ZZ>= `  K )
)
52, 4sylanb 459 . 2  |-  ( ( N  e.  Z  /\  M  e.  ( ZZ>= `  N ) )  ->  M  e.  ( ZZ>= `  K ) )
65, 1syl6eleqr 2526 1  |-  ( ( N  e.  Z  /\  M  e.  ( ZZ>= `  N ) )  ->  M  e.  Z )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    e. wcel 1725   ` cfv 5446   ZZ>=cuz 10480
This theorem is referenced by:  eluznn0  10538  elfzuz2  11054  elfzo1  11165  expmulnbnd  11503  bcval5  11601  rexuz3  12144  r19.29uz  12146  r19.2uz  12147  clim2  12290  clim2c  12291  clim0c  12293  rlimclim1  12331  2clim  12358  climabs0  12371  climcn1  12377  climcn2  12378  climsqz  12426  climsqz2  12427  clim2ser  12440  clim2ser2  12441  climub  12447  isercolllem1  12450  isercoll  12453  climsup  12455  caurcvg2  12463  serf0  12466  iseraltlem1  12467  iseralt  12470  o1fsum  12584  cvgcmp  12587  cvgcmpce  12589  isumsup2  12618  climcndslem1  12621  climcndslem2  12622  climcnds  12623  mertenslem1  12653  mertenslem2  12654  rpnnen2lem6  12811  rpnnen2lem7  12812  rpnnen2lem9  12814  rpnnen2lem11  12816  pcmpt2  13254  pcmptdvds  13255  prmreclem4  13279  prmreclem5  13280  prmreclem6  13281  vdwnnlem2  13356  2expltfac  13418  lmbrf  17316  lmss  17354  lmres  17356  1stcelcls  17516  txlm  17672  uzrest  17921  lmmcvg  19206  lmmbrf  19207  lmnn  19208  iscau4  19224  iscauf  19225  caucfil  19228  cmetcaulem  19233  iscmet3lem3  19235  iscmet3lem1  19236  causs  19243  lmle  19246  lmclim  19247  caubl  19252  caublcls  19253  ovolunlem1a  19384  volsuplem  19441  uniioombllem3  19469  mbflimsup  19550  mbfi1fseqlem6  19604  ulm2  20293  ulmcaulem  20302  ulmcau  20303  ulmss  20305  ulmdvlem1  20308  ulmdvlem3  20310  mtest  20312  itgulm  20316  birthdaylem2  20783  chtub  20988  logfaclbnd  20998  bclbnd  21056  bposlem3  21062  bposlem4  21063  bposlem5  21064  bposlem6  21065  lgsdilem2  21107  chebbnd1lem1  21155  chebbnd1lem2  21156  chebbnd1lem3  21157  dchrisumlema  21174  dchrisumlem2  21176  dchrisumlem3  21177  dchrisum0lem1b  21201  dchrisum0lem1  21202  pntrsumbnd2  21253  pntpbnd1  21272  pntpbnd2  21273  pntlemh  21285  pntlemq  21287  pntlemr  21288  pntlemj  21289  pntlemf  21291  minvecolem3  22370  minvecolem4  22374  h2hcau  22474  h2hlm  22475  chscllem2  23132  lgamgulmlem4  24808  lgamcvg2  24831  sinccvglem  25101  clim2div  25209  ntrivcvgfvn0  25219  ntrivcvgmullem  25221  fprodeq0  25291  lmclim2  26455  geomcau  26456  caures  26457  caushft  26458  heibor1lem  26509  rrncmslem  26532  climinf  27699  stirlinglem12  27801
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-cnex 9038  ax-resscn 9039  ax-pre-lttri 9056  ax-pre-lttrn 9057
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-er 6897  df-en 7102  df-dom 7103  df-sdom 7104  df-pnf 9114  df-mnf 9115  df-xr 9116  df-ltxr 9117  df-le 9118  df-neg 9286  df-z 10275  df-uz 10481
  Copyright terms: Public domain W3C validator