Theorem flge0nn0

Description: The floor of a number greater than or equal to 0 is a nonnegative integer. (Contributed by NM, 26-Apr-2005)

	Ref	Expression
Assertion	flge0nn0	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		flcl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
3		0z	⊢ 0 ∈ ℤ
4		flge	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℤ ) → ( 0 ≤ 𝐴 ↔ 0 ≤ ( ⌊ ‘ 𝐴 ) ) )
5	3 4	mpan2	⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ 0 ≤ ( ⌊ ‘ 𝐴 ) ) )
6	5	biimpa	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ≤ ( ⌊ ‘ 𝐴 ) )
7		elnn0z	⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ0 ↔ ( ( ⌊ ‘ 𝐴 ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ 𝐴 ) ) )
8	2 6 7	sylanbrc	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ0 )