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 ⊢ A ∈ ℤ → A = A

Proof

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