Metamath Proof Explorer

Theorem ico01fl0

Description: The floor of a real number in [ 0 , 1 ) is 0. Remark: may shorten the proof of modid or a version of it where the antecedent is membership in an interval. (Contributed by BJ, 29-Jun-2019)

		Ref	Expression
	Assertion	ico01fl0	$⊢ A \in [0, 1) \to ⌊A⌋ = 0$

Proof

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2		1xr	$⊢ 1 \in ℝ^{*}$
3		icossre	$⊢ (0 \in ℝ \land 1 \in ℝ^{*}) \to [0, 1) \subseteq ℝ$
4	1 2 3	mp2an	$⊢ [0, 1) \subseteq ℝ$
5	4	sseli	$⊢ A \in [0, 1) \to A \in ℝ$
6		0xr	$⊢ 0 \in ℝ^{*}$
7		elico1	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{}) \to (A \in [0, 1) \leftrightarrow (A \in ℝ^{*} \land 0 \leq A \land A < 1))$
8	6 2 7	mp2an	$⊢ A \in [0, 1) \leftrightarrow (A \in ℝ^{*} \land 0 \leq A \land A < 1)$
9	8	simp2bi	$⊢ A \in [0, 1) \to 0 \leq A$
10	8	simp3bi	$⊢ A \in [0, 1) \to A < 1$
11		recn	$⊢ A \in ℝ \to A \in ℂ$
12	11	addid2d	$⊢ A \in ℝ \to 0 + A = A$
13	12	fveqeq2d	$⊢ A \in ℝ \to (⌊0 + A⌋ = 0 \leftrightarrow ⌊A⌋ = 0)$
14		0z	$⊢ 0 \in ℤ$
15		flbi2	$⊢ (0 \in ℤ \land A \in ℝ) \to (⌊0 + A⌋ = 0 \leftrightarrow (0 \leq A \land A < 1))$
16	14 15	mpan	$⊢ A \in ℝ \to (⌊0 + A⌋ = 0 \leftrightarrow (0 \leq A \land A < 1))$
17	13 16	bitr3d	$⊢ A \in ℝ \to (⌊A⌋ = 0 \leftrightarrow (0 \leq A \land A < 1))$
18	17	biimpar	$⊢ (A \in ℝ \land (0 \leq A \land A < 1)) \to ⌊A⌋ = 0$
19	5 9 10 18	syl12anc	$⊢ A \in [0, 1) \to ⌊A⌋ = 0$