fraclt1

Description: The fractional part of a real number is less than one. (Contributed by NM, 15-Jul-2008)

		Ref	Expression
	Assertion	fraclt1	$⊢ A \in ℝ \to A - ⌊A⌋ < 1$

Step	Hyp	Ref	Expression
1		flltp1	$⊢ A \in ℝ \to A < ⌊A⌋ + 1$
2		reflcl	$⊢ A \in ℝ \to ⌊A⌋ \in ℝ$
3		1re	$⊢ 1 \in ℝ$
4		ltsubadd2	$⊢ (A \in ℝ \land ⌊A⌋ \in ℝ \land 1 \in ℝ) \to (A - ⌊A⌋ < 1 \leftrightarrow A < ⌊A⌋ + 1)$
5	3 4	mp3an3	$⊢ (A \in ℝ \land ⌊A⌋ \in ℝ) \to (A - ⌊A⌋ < 1 \leftrightarrow A < ⌊A⌋ + 1)$
6	2 5	mpdan	$⊢ A \in ℝ \to (A - ⌊A⌋ < 1 \leftrightarrow A < ⌊A⌋ + 1)$
7	1 6	mpbird	$⊢ A \in ℝ \to A - ⌊A⌋ < 1$

Metamath Proof Explorer