Metamath Proof Explorer


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 ( 𝐴 ∈ ℤ → ( ⌊ ‘ 𝐴 ) = 𝐴 )