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	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 0 ≤ 𝑀 → 𝑁 ∈ ℕ0 ) )

Proof

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