This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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