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

Metamath Proof Explorer

Theorem ltm1

Description: A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006)

Ref Expression
Assertion ltm1 ⊢ A ∈ ℝ → A − 1 < A

Proof

Step Hyp Ref Expression
1 0lt1 ⊢ 0 < 1
2 0re ⊢ 0 ∈ ℝ
3 1re ⊢ 1 ∈ ℝ
4 ltsub2 ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ A ∈ ℝ → 0 < 1 ↔ A − 1 < A − 0
5 2 3 4 mp3an12 ⊢ A ∈ ℝ → 0 < 1 ↔ A − 1 < A − 0
6 1 5 mpbii ⊢ A ∈ ℝ → A − 1 < A − 0
7 recn ⊢ A ∈ ℝ → A ∈ ℂ
8 7 subid1d ⊢ A ∈ ℝ → A − 0 = A
9 6 8 breqtrd ⊢ A ∈ ℝ → A − 1 < A