Theorem fracge0

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

	Ref	Expression
Assertion	fracge0	$$⊢A\in ℝ\to 0\le A-⌊A⌋$$

Proof

Step	Hyp	Ref	Expression
1		flle	$$⊢A\in ℝ\to ⌊A⌋\le A$$
2		reflcl	$$⊢A\in ℝ\to ⌊A⌋\in ℝ$$
3		subge0	$$⊢\left(A\in ℝ\wedge ⌊A⌋\in ℝ\right)\to \left(0\le A-⌊A⌋\leftrightarrow ⌊A⌋\le A\right)$$
4	2 3	mpdan	$$⊢A\in ℝ\to \left(0\le A-⌊A⌋\leftrightarrow ⌊A⌋\le A\right)$$
5	1 4	mpbird	$$⊢A\in ℝ\to 0\le A-⌊A⌋$$