Theorem fracge0

Description: The fractional part of a real number is nonnegative. (Contributed by NM, 17-Jul-2008)

	Ref	Expression
Assertion	fracge0	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		flle	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
2		reflcl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
3		subge0	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℝ ) → ( 0 ≤ ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ↔ ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ) )
4	2 3	mpdan	⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ↔ ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ) )
5	1 4	mpbird	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) )