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

Theorem uzss 10881
Description: Subset relationship for two sets of upper integers. (Contributed by NM, 5-Sep-2005.)
Assertion
Ref Expression
uzss  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( ZZ>= `  N )  C_  ( ZZ>=
`  M ) )

Proof of Theorem uzss
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 eluzle 10873 . . . . . 6  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  <_  N )
21adantr 465 . . . . 5  |-  ( ( N  e.  ( ZZ>= `  M )  /\  k  e.  ZZ )  ->  M  <_  N )
3 eluzel2 10866 . . . . . . 7  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
4 eluzelz 10870 . . . . . . 7  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  ZZ )
53, 4jca 532 . . . . . 6  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
6 zre 10650 . . . . . . . 8  |-  ( M  e.  ZZ  ->  M  e.  RR )
7 zre 10650 . . . . . . . 8  |-  ( N  e.  ZZ  ->  N  e.  RR )
8 zre 10650 . . . . . . . 8  |-  ( k  e.  ZZ  ->  k  e.  RR )
9 letr 9468 . . . . . . . 8  |-  ( ( M  e.  RR  /\  N  e.  RR  /\  k  e.  RR )  ->  (
( M  <_  N  /\  N  <_  k )  ->  M  <_  k
) )
106, 7, 8, 9syl3an 1260 . . . . . . 7  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ  /\  k  e.  ZZ )  ->  (
( M  <_  N  /\  N  <_  k )  ->  M  <_  k
) )
11103expa 1187 . . . . . 6  |-  ( ( ( M  e.  ZZ  /\  N  e.  ZZ )  /\  k  e.  ZZ )  ->  ( ( M  <_  N  /\  N  <_  k )  ->  M  <_  k ) )
125, 11sylan 471 . . . . 5  |-  ( ( N  e.  ( ZZ>= `  M )  /\  k  e.  ZZ )  ->  (
( M  <_  N  /\  N  <_  k )  ->  M  <_  k
) )
132, 12mpand 675 . . . 4  |-  ( ( N  e.  ( ZZ>= `  M )  /\  k  e.  ZZ )  ->  ( N  <_  k  ->  M  <_  k ) )
1413imdistanda 693 . . 3  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( (
k  e.  ZZ  /\  N  <_  k )  -> 
( k  e.  ZZ  /\  M  <_  k )
) )
15 eluz1 10865 . . . 4  |-  ( N  e.  ZZ  ->  (
k  e.  ( ZZ>= `  N )  <->  ( k  e.  ZZ  /\  N  <_ 
k ) ) )
164, 15syl 16 . . 3  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( k  e.  ( ZZ>= `  N )  <->  ( k  e.  ZZ  /\  N  <_  k ) ) )
17 eluz1 10865 . . . 4  |-  ( M  e.  ZZ  ->  (
k  e.  ( ZZ>= `  M )  <->  ( k  e.  ZZ  /\  M  <_ 
k ) ) )
183, 17syl 16 . . 3  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( k  e.  ( ZZ>= `  M )  <->  ( k  e.  ZZ  /\  M  <_  k ) ) )
1914, 16, 183imtr4d 268 . 2  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( k  e.  ( ZZ>= `  N )  ->  k  e.  ( ZZ>= `  M ) ) )
2019ssrdv 3362 1  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( ZZ>= `  N )  C_  ( ZZ>=
`  M ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    e. wcel 1756    C_ wss 3328   class class class wbr 4292   ` cfv 5418   RRcr 9281    <_ cle 9419   ZZcz 10646   ZZ>=cuz 10861
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 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372  ax-cnex 9338  ax-resscn 9339  ax-pre-lttri 9356  ax-pre-lttrn 9357
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 2568  df-ne 2608  df-nel 2609  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-ov 6094  df-er 7101  df-en 7311  df-dom 7312  df-sdom 7313  df-pnf 9420  df-mnf 9421  df-xr 9422  df-ltxr 9423  df-le 9424  df-neg 9598  df-z 10647  df-uz 10862
This theorem is referenced by:  uzin  10893  uznnssnn  10902  fzopth  11495  4fvwrd4  11533  fzouzsplit  11584  seqfeq2  11829  rexuzre  12840  cau3lem  12842  climsup  13147  isumsplit  13303  isumrpcl  13306  cvgrat  13343  isprm3  13772  pcfac  13961  lmflf  19578  caucfil  20794  uniioombllem4  21066  mbflimsup  21144  ulmres  21853  ulmcaulem  21859  logfaclbnd  22561  axlowdimlem17  23204  axlowdim  23207  rnlogblem  26458  clim2prod  27403  fprodntriv  27455  climinf  29779  climsuse  29781  fzoopth  30213
  Copyright terms: Public domain W3C validator