Theorem flltnz

Description: The floor of a non-integer real is less than it. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	flltnz	⊢ ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℤ ) → ( ⌊ ‘ 𝐴 ) < 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		reflcl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℤ ) → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
3		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℤ ) → 𝐴 ∈ ℝ )
4		fllelt	⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ∧ 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
5	4	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℤ ) → ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ∧ 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
6	5	simpld	⊢ ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℤ ) → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
7		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℤ ) → ¬ 𝐴 ∈ ℤ )
8		flidz	⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) = 𝐴 ↔ 𝐴 ∈ ℤ ) )
9	8	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℤ ) → ( ( ⌊ ‘ 𝐴 ) = 𝐴 ↔ 𝐴 ∈ ℤ ) )
10	7 9	mtbird	⊢ ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℤ ) → ¬ ( ⌊ ‘ 𝐴 ) = 𝐴 )
11	10	neqned	⊢ ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℤ ) → ( ⌊ ‘ 𝐴 ) ≠ 𝐴 )
12	11	necomd	⊢ ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℤ ) → 𝐴 ≠ ( ⌊ ‘ 𝐴 ) )
13	2 3 6 12	leneltd	⊢ ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℤ ) → ( ⌊ ‘ 𝐴 ) < 𝐴 )