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

Metamath Proof Explorer

Theorem lem1

Description: A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Assertion lem1 ⊢ A ∈ ℝ → A − 1 ≤ A

Proof

Step Hyp Ref Expression
1 ltm1 ⊢ A ∈ ℝ → A − 1 < A
2 peano2rem ⊢ A ∈ ℝ → A − 1 ∈ ℝ
3 ltle ⊢ A − 1 ∈ ℝ ∧ A ∈ ℝ → A − 1 < A → A − 1 ≤ A
4 2 3 mpancom ⊢ A ∈ ℝ → A − 1 < A → A − 1 ≤ A
5 1 4 mpd ⊢ A ∈ ℝ → A − 1 ≤ A