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 ∈ ℤ ≥ M → 0 ≤ M → N ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 eluz2 ⊢ N ∈ ℤ ≥ M ↔ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N
2 simpl2 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N ∧ 0 ≤ M → N ∈ ℤ
3 zre ⊢ M ∈ ℤ → M ∈ ℝ
4 zre ⊢ N ∈ ℤ → N ∈ ℝ
5 0red ⊢ M ∈ ℝ ∧ N ∈ ℝ → 0 ∈ ℝ
6 simpl ⊢ M ∈ ℝ ∧ N ∈ ℝ → M ∈ ℝ
7 simpr ⊢ M ∈ ℝ ∧ N ∈ ℝ → N ∈ ℝ
8 5 6 7 3jca ⊢ M ∈ ℝ ∧ N ∈ ℝ → 0 ∈ ℝ ∧ M ∈ ℝ ∧ N ∈ ℝ
9 3 4 8 syl2an ⊢ M ∈ ℤ ∧ N ∈ ℤ → 0 ∈ ℝ ∧ M ∈ ℝ ∧ N ∈ ℝ
10 letr ⊢ 0 ∈ ℝ ∧ M ∈ ℝ ∧ N ∈ ℝ → 0 ≤ M ∧ M ≤ N → 0 ≤ N
11 9 10 syl ⊢ M ∈ ℤ ∧ N ∈ ℤ → 0 ≤ M ∧ M ≤ N → 0 ≤ N
12 11 expcomd ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ≤ N → 0 ≤ M → 0 ≤ N
13 12 ex ⊢ M ∈ ℤ → N ∈ ℤ → M ≤ N → 0 ≤ M → 0 ≤ N
14 13 3imp1 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N ∧ 0 ≤ M → 0 ≤ N
15 elnn0z ⊢ N ∈ ℕ 0 ↔ N ∈ ℤ ∧ 0 ≤ N
16 2 14 15 sylanbrc ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N ∧ 0 ≤ M → N ∈ ℕ 0
17 16 ex ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N → 0 ≤ M → N ∈ ℕ 0
18 1 17 sylbi ⊢ N ∈ ℤ ≥ M → 0 ≤ M → N ∈ ℕ 0