Metamath Proof Explorer

Theorem eluzmn

Description: Membership in an earlier upper set of integers. (Contributed by Thierry Arnoux, 8-Oct-2018)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( M e. ZZ /\ N e. NN0 ) -> M e. ZZ )
2 simpr 
 |-  ( ( M e. ZZ /\ N e. NN0 ) -> N e. NN0 )
3 2 nn0zd 
 |-  ( ( M e. ZZ /\ N e. NN0 ) -> N e. ZZ )
4 1 3 zsubcld 
 |-  ( ( M e. ZZ /\ N e. NN0 ) -> ( M - N ) e. ZZ )
5 1 zred 
 |-  ( ( M e. ZZ /\ N e. NN0 ) -> M e. RR )
6 2 nn0red 
 |-  ( ( M e. ZZ /\ N e. NN0 ) -> N e. RR )
7 5 6 readdcld 
 |-  ( ( M e. ZZ /\ N e. NN0 ) -> ( M + N ) e. RR )
8 nn0addge1 
 |-  ( ( M e. RR /\ N e. NN0 ) -> M <_ ( M + N ) )
9 5 8 sylancom 
 |-  ( ( M e. ZZ /\ N e. NN0 ) -> M <_ ( M + N ) )
10 5 7 6 9 lesub1dd 
 |-  ( ( M e. ZZ /\ N e. NN0 ) -> ( M - N ) <_ ( ( M + N ) - N ) )
11 5 recnd 
 |-  ( ( M e. ZZ /\ N e. NN0 ) -> M e. CC )
12 6 recnd 
 |-  ( ( M e. ZZ /\ N e. NN0 ) -> N e. CC )
13 11 12 pncand 
 |-  ( ( M e. ZZ /\ N e. NN0 ) -> ( ( M + N ) - N ) = M )
14 10 13 breqtrd 
 |-  ( ( M e. ZZ /\ N e. NN0 ) -> ( M - N ) <_ M )
15 eluz2 
 |-  ( M e. ( ZZ>= ` ( M - N ) ) <-> ( ( M - N ) e. ZZ /\ M e. ZZ /\ ( M - N ) <_ M ) )
16 4 1 14 15 syl3anbrc 
 |-  ( ( M e. ZZ /\ N e. NN0 ) -> M e. ( ZZ>= ` ( M - N ) ) )