Metamath Proof Explorer

Theorem uztrn

Description: Transitive law for sets of upper integers. (Contributed by NM, 20-Sep-2005)

Ref Expression
Assertion uztrn 
|- ( ( M e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` N ) ) -> M e. ( ZZ>= ` N ) )

Proof

Step Hyp Ref Expression
1 eluzel2 
 |-  ( K e. ( ZZ>= ` N ) -> N e. ZZ )
2 1 adantl 
 |-  ( ( M e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` N ) ) -> N e. ZZ )
3 eluzelz 
 |-  ( M e. ( ZZ>= ` K ) -> M e. ZZ )
4 3 adantr 
 |-  ( ( M e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` N ) ) -> M e. ZZ )
5 eluzle 
 |-  ( K e. ( ZZ>= ` N ) -> N <_ K )
6 5 adantl 
 |-  ( ( M e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` N ) ) -> N <_ K )
7 eluzle 
 |-  ( M e. ( ZZ>= ` K ) -> K <_ M )
8 7 adantr 
 |-  ( ( M e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` N ) ) -> K <_ M )
9 eluzelz 
 |-  ( K e. ( ZZ>= ` N ) -> K e. ZZ )
10 zletr 
 |-  ( ( N e. ZZ /\ K e. ZZ /\ M e. ZZ ) -> ( ( N <_ K /\ K <_ M ) -> N <_ M ) )
11 1 9 4 10 syl2an23an 
 |-  ( ( M e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` N ) ) -> ( ( N <_ K /\ K <_ M ) -> N <_ M ) )
12 6 8 11 mp2and 
 |-  ( ( M e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` N ) ) -> N <_ M )
13 eluz2 
 |-  ( M e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ M e. ZZ /\ N <_ M ) )
14 2 4 12 13 syl3anbrc 
 |-  ( ( M e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` N ) ) -> M e. ( ZZ>= ` N ) )