Metamath Proof Explorer

Theorem uzaddcl

Description: Addition closure law for an upper set of integers. (Contributed by NM, 4-Jun-2006)

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

Proof

Step Hyp Ref Expression
1 eluzelcn 
 |-  ( N e. ( ZZ>= ` M ) -> N e. CC )
2 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
3 ax-1cn 
 |-  1 e. CC
4 addass 
 |-  ( ( N e. CC /\ k e. CC /\ 1 e. CC ) -> ( ( N + k ) + 1 ) = ( N + ( k + 1 ) ) )
5 3 4 mp3an3 
 |-  ( ( N e. CC /\ k e. CC ) -> ( ( N + k ) + 1 ) = ( N + ( k + 1 ) ) )
6 1 2 5 syl2anr 
 |-  ( ( k e. NN0 /\ N e. ( ZZ>= ` M ) ) -> ( ( N + k ) + 1 ) = ( N + ( k + 1 ) ) )
7 6 adantr 
 |-  ( ( ( k e. NN0 /\ N e. ( ZZ>= ` M ) ) /\ ( N + k ) e. ( ZZ>= ` M ) ) -> ( ( N + k ) + 1 ) = ( N + ( k + 1 ) ) )
8 peano2uz 
 |-  ( ( N + k ) e. ( ZZ>= ` M ) -> ( ( N + k ) + 1 ) e. ( ZZ>= ` M ) )
9 8 adantl 
 |-  ( ( ( k e. NN0 /\ N e. ( ZZ>= ` M ) ) /\ ( N + k ) e. ( ZZ>= ` M ) ) -> ( ( N + k ) + 1 ) e. ( ZZ>= ` M ) )
10 7 9 eqeltrrd 
 |-  ( ( ( k e. NN0 /\ N e. ( ZZ>= ` M ) ) /\ ( N + k ) e. ( ZZ>= ` M ) ) -> ( N + ( k + 1 ) ) e. ( ZZ>= ` M ) )
11 10 exp31 
 |-  ( k e. NN0 -> ( N e. ( ZZ>= ` M ) -> ( ( N + k ) e. ( ZZ>= ` M ) -> ( N + ( k + 1 ) ) e. ( ZZ>= ` M ) ) ) )
12 11 a2d 
 |-  ( k e. NN0 -> ( ( N e. ( ZZ>= ` M ) -> ( N + k ) e. ( ZZ>= ` M ) ) -> ( N e. ( ZZ>= ` M ) -> ( N + ( k + 1 ) ) e. ( ZZ>= ` M ) ) ) )
13 1 addid1d 
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 0 ) = N )
14 13 eleq1d 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( N + 0 ) e. ( ZZ>= ` M ) <-> N e. ( ZZ>= ` M ) ) )
15 14 ibir 
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 0 ) e. ( ZZ>= ` M ) )
16 oveq2 
 |-  ( j = 0 -> ( N + j ) = ( N + 0 ) )
17 16 eleq1d 
 |-  ( j = 0 -> ( ( N + j ) e. ( ZZ>= ` M ) <-> ( N + 0 ) e. ( ZZ>= ` M ) ) )
18 17 imbi2d 
 |-  ( j = 0 -> ( ( N e. ( ZZ>= ` M ) -> ( N + j ) e. ( ZZ>= ` M ) ) <-> ( N e. ( ZZ>= ` M ) -> ( N + 0 ) e. ( ZZ>= ` M ) ) ) )
19 oveq2 
 |-  ( j = k -> ( N + j ) = ( N + k ) )
20 19 eleq1d 
 |-  ( j = k -> ( ( N + j ) e. ( ZZ>= ` M ) <-> ( N + k ) e. ( ZZ>= ` M ) ) )
21 20 imbi2d 
 |-  ( j = k -> ( ( N e. ( ZZ>= ` M ) -> ( N + j ) e. ( ZZ>= ` M ) ) <-> ( N e. ( ZZ>= ` M ) -> ( N + k ) e. ( ZZ>= ` M ) ) ) )
22 oveq2 
 |-  ( j = ( k + 1 ) -> ( N + j ) = ( N + ( k + 1 ) ) )
23 22 eleq1d 
 |-  ( j = ( k + 1 ) -> ( ( N + j ) e. ( ZZ>= ` M ) <-> ( N + ( k + 1 ) ) e. ( ZZ>= ` M ) ) )
24 23 imbi2d 
 |-  ( j = ( k + 1 ) -> ( ( N e. ( ZZ>= ` M ) -> ( N + j ) e. ( ZZ>= ` M ) ) <-> ( N e. ( ZZ>= ` M ) -> ( N + ( k + 1 ) ) e. ( ZZ>= ` M ) ) ) )
25 oveq2 
 |-  ( j = K -> ( N + j ) = ( N + K ) )
26 25 eleq1d 
 |-  ( j = K -> ( ( N + j ) e. ( ZZ>= ` M ) <-> ( N + K ) e. ( ZZ>= ` M ) ) )
27 26 imbi2d 
 |-  ( j = K -> ( ( N e. ( ZZ>= ` M ) -> ( N + j ) e. ( ZZ>= ` M ) ) <-> ( N e. ( ZZ>= ` M ) -> ( N + K ) e. ( ZZ>= ` M ) ) ) )
28 12 15 18 21 24 27 nn0indALT 
 |-  ( K e. NN0 -> ( N e. ( ZZ>= ` M ) -> ( N + K ) e. ( ZZ>= ` M ) ) )
29 28 impcom 
 |-  ( ( N e. ( ZZ>= ` M ) /\ K e. NN0 ) -> ( N + K ) e. ( ZZ>= ` M ) )