Theorem divfl0

Description: The floor of a fraction is 0 iff the denominator is less than the numerator. (Contributed by AV, 8-Jul-2021)

	Ref	Expression
Assertion	divfl0	|- ( ( A e. NN0 /\ B e. NN ) -> ( A < B <-> ( |_ ` ( A / B ) ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0nndivcl	|- ( ( A e. NN0 /\ B e. NN ) -> ( A / B ) e. RR )
2	1	recnd	|- ( ( A e. NN0 /\ B e. NN ) -> ( A / B ) e. CC )
3		addid2	|- ( ( A / B ) e. CC -> ( 0 + ( A / B ) ) = ( A / B ) )
4	3	eqcomd	|- ( ( A / B ) e. CC -> ( A / B ) = ( 0 + ( A / B ) ) )
5	2 4	syl	|- ( ( A e. NN0 /\ B e. NN ) -> ( A / B ) = ( 0 + ( A / B ) ) )
6	5	fveqeq2d	|- ( ( A e. NN0 /\ B e. NN ) -> ( ( |_ ` ( A / B ) ) = 0 <-> ( |_ ` ( 0 + ( A / B ) ) ) = 0 ) )
7		0z	|- 0 e. ZZ
8		flbi2	|- ( ( 0 e. ZZ /\ ( A / B ) e. RR ) -> ( ( |_ ` ( 0 + ( A / B ) ) ) = 0 <-> ( 0 <_ ( A / B ) /\ ( A / B ) < 1 ) ) )
9	7 1 8	sylancr	|- ( ( A e. NN0 /\ B e. NN ) -> ( ( |_ ` ( 0 + ( A / B ) ) ) = 0 <-> ( 0 <_ ( A / B ) /\ ( A / B ) < 1 ) ) )
10		nn0ge0div	|- ( ( A e. NN0 /\ B e. NN ) -> 0 <_ ( A / B ) )
11	10	biantrurd	|- ( ( A e. NN0 /\ B e. NN ) -> ( ( A / B ) < 1 <-> ( 0 <_ ( A / B ) /\ ( A / B ) < 1 ) ) )
12		nn0re	|- ( A e. NN0 -> A e. RR )
13		nnrp	|- ( B e. NN -> B e. RR+ )
14		divlt1lt	|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) < 1 <-> A < B ) )
15	12 13 14	syl2an	|- ( ( A e. NN0 /\ B e. NN ) -> ( ( A / B ) < 1 <-> A < B ) )
16	11 15	bitr3d	|- ( ( A e. NN0 /\ B e. NN ) -> ( ( 0 <_ ( A / B ) /\ ( A / B ) < 1 ) <-> A < B ) )
17	6 9 16	3bitrrd	|- ( ( A e. NN0 /\ B e. NN ) -> ( A < B <-> ( |_ ` ( A / B ) ) = 0 ) )