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

Metamath Proof Explorer

Theorem fllep1

Description: A basic property of the floor (greatest integer) function. (Contributed by Mario Carneiro, 21-May-2016)

		Ref	Expression
	Assertion	fllep1	$⊢ A \in ℝ \to A \leq ⌊A⌋ + 1$

Step	Hyp	Ref	Expression
1		flltp1	$⊢ A \in ℝ \to A < ⌊A⌋ + 1$
2		reflcl	$⊢ A \in ℝ \to ⌊A⌋ \in ℝ$
3		peano2re	$⊢ ⌊A⌋ \in ℝ \to ⌊A⌋ + 1 \in ℝ$
4	2 3	syl	$⊢ A \in ℝ \to ⌊A⌋ + 1 \in ℝ$
5		ltle	$⊢ (A \in ℝ \land ⌊A⌋ + 1 \in ℝ) \to (A < ⌊A⌋ + 1 \to A \leq ⌊A⌋ + 1)$
6	4 5	mpdan	$⊢ A \in ℝ \to (A < ⌊A⌋ + 1 \to A \leq ⌊A⌋ + 1)$
7	1 6	mpd	$⊢ A \in ℝ \to A \leq ⌊A⌋ + 1$