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

Metamath Proof Explorer

Theorem lep1

Description: A number is less than or equal to itself plus 1. (Contributed by NM, 5-Jan-2006)

		Ref	Expression
	Assertion	lep1	$⊢ A \in ℝ \to A \leq A + 1$

Step	Hyp	Ref	Expression
1		ltp1	$⊢ A \in ℝ \to A < A + 1$
2		peano2re	$⊢ A \in ℝ \to A + 1 \in ℝ$
3		ltle	$⊢ (A \in ℝ \land A + 1 \in ℝ) \to (A < A + 1 \to A \leq A + 1)$
4	2 3	mpdan	$⊢ A \in ℝ \to (A < A + 1 \to A \leq A + 1)$
5	1 4	mpd	$⊢ A \in ℝ \to A \leq A + 1$