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 e. ( 0 [,) 1 ) -> ( |_ ` A ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		0re	|- 0 e. RR
2		1xr	|- 1 e. RR*
3		icossre	|- ( ( 0 e. RR /\ 1 e. RR* ) -> ( 0 [,) 1 ) C_ RR )
4	1 2 3	mp2an	|- ( 0 [,) 1 ) C_ RR
5	4	sseli	|- ( A e. ( 0 [,) 1 ) -> A e. RR )
6		0xr	|- 0 e. RR*
7		elico1	|- ( ( 0 e. RR* /\ 1 e. RR* ) -> ( A e. ( 0 [,) 1 ) <-> ( A e. RR* /\ 0 <_ A /\ A < 1 ) ) )
8	6 2 7	mp2an	|- ( A e. ( 0 [,) 1 ) <-> ( A e. RR* /\ 0 <_ A /\ A < 1 ) )
9	8	simp2bi	|- ( A e. ( 0 [,) 1 ) -> 0 <_ A )
10	8	simp3bi	|- ( A e. ( 0 [,) 1 ) -> A < 1 )
11		recn	|- ( A e. RR -> A e. CC )
12	11	addid2d	|- ( A e. RR -> ( 0 + A ) = A )
13	12	fveqeq2d	|- ( A e. RR -> ( ( |_ ` ( 0 + A ) ) = 0 <-> ( |_ ` A ) = 0 ) )
14		0z	|- 0 e. ZZ
15		flbi2	|- ( ( 0 e. ZZ /\ A e. RR ) -> ( ( |_ ` ( 0 + A ) ) = 0 <-> ( 0 <_ A /\ A < 1 ) ) )
16	14 15	mpan	|- ( A e. RR -> ( ( |_ ` ( 0 + A ) ) = 0 <-> ( 0 <_ A /\ A < 1 ) ) )
17	13 16	bitr3d	|- ( A e. RR -> ( ( |_ ` A ) = 0 <-> ( 0 <_ A /\ A < 1 ) ) )
18	17	biimpar	|- ( ( A e. RR /\ ( 0 <_ A /\ A < 1 ) ) -> ( |_ ` A ) = 0 )
19	5 9 10 18	syl12anc	|- ( A e. ( 0 [,) 1 ) -> ( |_ ` A ) = 0 )