Metamath Proof Explorer

Theorem eluzadd

Description: Membership in a later upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by SN, 7-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
2 zaddcl 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( M + K ) e. ZZ )
3 1 2 sylan 
 |-  ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) -> ( M + K ) e. ZZ )
4 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
5 zaddcl 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( N + K ) e. ZZ )
6 4 5 sylan 
 |-  ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) -> ( N + K ) e. ZZ )
7 1 zred 
 |-  ( N e. ( ZZ>= ` M ) -> M e. RR )
8 7 adantr 
 |-  ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) -> M e. RR )
9 eluzelre 
 |-  ( N e. ( ZZ>= ` M ) -> N e. RR )
10 9 adantr 
 |-  ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) -> N e. RR )
11 zre 
 |-  ( K e. ZZ -> K e. RR )
12 11 adantl 
 |-  ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) -> K e. RR )
13 eluzle 
 |-  ( N e. ( ZZ>= ` M ) -> M <_ N )
14 13 adantr 
 |-  ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) -> M <_ N )
15 8 10 12 14 leadd1dd 
 |-  ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) -> ( M + K ) <_ ( N + K ) )
16 eluz2 
 |-  ( ( N + K ) e. ( ZZ>= ` ( M + K ) ) <-> ( ( M + K ) e. ZZ /\ ( N + K ) e. ZZ /\ ( M + K ) <_ ( N + K ) ) )
17 3 6 15 16 syl3anbrc 
 |-  ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) -> ( N + K ) e. ( ZZ>= ` ( M + K ) ) )