Theorem fraclt1

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

	Ref	Expression
Assertion	fraclt1	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) < 1 )

Proof

Step	Hyp	Ref	Expression
1		flltp1	⊢ ( 𝐴 ∈ ℝ → 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) )
2		reflcl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
3		1re	⊢ 1 ∈ ℝ
4		ltsubadd2	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) < 1 ↔ 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
5	3 4	mp3an3	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℝ ) → ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) < 1 ↔ 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
6	2 5	mpdan	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) < 1 ↔ 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
7	1 6	mpbird	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) < 1 )