Theorem flid

Description: An integer is its own floor. (Contributed by NM, 15-Nov-2004)

	Ref	Expression
Assertion	flid	⊢ ( 𝐴 ∈ ℤ → ( ⌊ ‘ 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
2		flle	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
3	1 2	syl	⊢ ( 𝐴 ∈ ℤ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
4	1	leidd	⊢ ( 𝐴 ∈ ℤ → 𝐴 ≤ 𝐴 )
5		flge	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ∈ ℤ ) → ( 𝐴 ≤ 𝐴 ↔ 𝐴 ≤ ( ⌊ ‘ 𝐴 ) ) )
6	1 5	mpancom	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ≤ 𝐴 ↔ 𝐴 ≤ ( ⌊ ‘ 𝐴 ) ) )
7	4 6	mpbid	⊢ ( 𝐴 ∈ ℤ → 𝐴 ≤ ( ⌊ ‘ 𝐴 ) )
8		reflcl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
9	1 8	syl	⊢ ( 𝐴 ∈ ℤ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
10	9 1	letri3d	⊢ ( 𝐴 ∈ ℤ → ( ( ⌊ ‘ 𝐴 ) = 𝐴 ↔ ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ∧ 𝐴 ≤ ( ⌊ ‘ 𝐴 ) ) ) )
11	3 7 10	mpbir2and	⊢ ( 𝐴 ∈ ℤ → ( ⌊ ‘ 𝐴 ) = 𝐴 )