Theorem eluzge0nn0

Description: If an integer is greater than or equal to a nonnegative integer, then it is a nonnegative integer. (Contributed by Alexander van der Vekens, 27-Aug-2018)

	Ref	Expression
Assertion	eluzge0nn0	|- ( N e. ( ZZ>= ` M ) -> ( 0 <_ M -> N e. NN0 ) )

Proof

Step	Hyp	Ref	Expression
1		eluz2	|- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
2		simpl2	|- ( ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) /\ 0 <_ M ) -> N e. ZZ )
3		zre	|- ( M e. ZZ -> M e. RR )
4		zre	|- ( N e. ZZ -> N e. RR )
5		0red	|- ( ( M e. RR /\ N e. RR ) -> 0 e. RR )
6		simpl	|- ( ( M e. RR /\ N e. RR ) -> M e. RR )
7		simpr	|- ( ( M e. RR /\ N e. RR ) -> N e. RR )
8	5 6 7	3jca	|- ( ( M e. RR /\ N e. RR ) -> ( 0 e. RR /\ M e. RR /\ N e. RR ) )
9	3 4 8	syl2an	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( 0 e. RR /\ M e. RR /\ N e. RR ) )
10		letr	|- ( ( 0 e. RR /\ M e. RR /\ N e. RR ) -> ( ( 0 <_ M /\ M <_ N ) -> 0 <_ N ) )
11	9 10	syl	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( 0 <_ M /\ M <_ N ) -> 0 <_ N ) )
12	11	expcomd	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N -> ( 0 <_ M -> 0 <_ N ) ) )
13	12	ex	|- ( M e. ZZ -> ( N e. ZZ -> ( M <_ N -> ( 0 <_ M -> 0 <_ N ) ) ) )
14	13	3imp1	|- ( ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) /\ 0 <_ M ) -> 0 <_ N )
15		elnn0z	|- ( N e. NN0 <-> ( N e. ZZ /\ 0 <_ N ) )
16	2 14 15	sylanbrc	|- ( ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) /\ 0 <_ M ) -> N e. NN0 )
17	16	ex	|- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( 0 <_ M -> N e. NN0 ) )
18	1 17	sylbi	|- ( N e. ( ZZ>= ` M ) -> ( 0 <_ M -> N e. NN0 ) )