# Metamath Proof Explorer

## 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}\in {ℤ}_{\ge {M}}\to \left(0\le {M}\to {N}\in {ℕ}_{0}\right)$

### Proof

Step Hyp Ref Expression
1 eluz2 ${⊢}{N}\in {ℤ}_{\ge {M}}↔\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}\le {N}\right)$
2 simpl2 ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}\le {N}\right)\wedge 0\le {M}\right)\to {N}\in ℤ$
3 zre ${⊢}{M}\in ℤ\to {M}\in ℝ$
4 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
5 0red ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to 0\in ℝ$
6 simpl ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to {M}\in ℝ$
7 simpr ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to {N}\in ℝ$
8 5 6 7 3jca ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left(0\in ℝ\wedge {M}\in ℝ\wedge {N}\in ℝ\right)$
9 3 4 8 syl2an ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left(0\in ℝ\wedge {M}\in ℝ\wedge {N}\in ℝ\right)$
10 letr ${⊢}\left(0\in ℝ\wedge {M}\in ℝ\wedge {N}\in ℝ\right)\to \left(\left(0\le {M}\wedge {M}\le {N}\right)\to 0\le {N}\right)$
11 9 10 syl ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left(\left(0\le {M}\wedge {M}\le {N}\right)\to 0\le {N}\right)$
12 11 expcomd ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\le {N}\to \left(0\le {M}\to 0\le {N}\right)\right)$
13 12 ex ${⊢}{M}\in ℤ\to \left({N}\in ℤ\to \left({M}\le {N}\to \left(0\le {M}\to 0\le {N}\right)\right)\right)$
14 13 3imp1 ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}\le {N}\right)\wedge 0\le {M}\right)\to 0\le {N}$
15 elnn0z ${⊢}{N}\in {ℕ}_{0}↔\left({N}\in ℤ\wedge 0\le {N}\right)$
16 2 14 15 sylanbrc ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}\le {N}\right)\wedge 0\le {M}\right)\to {N}\in {ℕ}_{0}$
17 16 ex ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}\le {N}\right)\to \left(0\le {M}\to {N}\in {ℕ}_{0}\right)$
18 1 17 sylbi ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left(0\le {M}\to {N}\in {ℕ}_{0}\right)$