Theorem adddivflid

Description: The floor of a sum of an integer and a fraction is equal to the integer iff the denominator of the fraction is less than the numerator. (Contributed by AV, 14-Jul-2021)

	Ref	Expression
Assertion	adddivflid	|- ( ( A e. ZZ /\ B e. NN0 /\ C e. NN ) -> ( B < C <-> ( |_ ` ( A + ( B / C ) ) ) = A ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	|- ( ( A e. ZZ /\ B e. NN0 /\ C e. NN ) -> A e. ZZ )
2		nn0nndivcl	|- ( ( B e. NN0 /\ C e. NN ) -> ( B / C ) e. RR )
3	2	3adant1	|- ( ( A e. ZZ /\ B e. NN0 /\ C e. NN ) -> ( B / C ) e. RR )
4	1 3	jca	|- ( ( A e. ZZ /\ B e. NN0 /\ C e. NN ) -> ( A e. ZZ /\ ( B / C ) e. RR ) )
5		flbi2	|- ( ( A e. ZZ /\ ( B / C ) e. RR ) -> ( ( |_ ` ( A + ( B / C ) ) ) = A <-> ( 0 <_ ( B / C ) /\ ( B / C ) < 1 ) ) )
6	4 5	syl	|- ( ( A e. ZZ /\ B e. NN0 /\ C e. NN ) -> ( ( |_ ` ( A + ( B / C ) ) ) = A <-> ( 0 <_ ( B / C ) /\ ( B / C ) < 1 ) ) )
7		nn0re	|- ( B e. NN0 -> B e. RR )
8		nn0ge0	|- ( B e. NN0 -> 0 <_ B )
9	7 8	jca	|- ( B e. NN0 -> ( B e. RR /\ 0 <_ B ) )
10		nnre	|- ( C e. NN -> C e. RR )
11		nngt0	|- ( C e. NN -> 0 < C )
12	10 11	jca	|- ( C e. NN -> ( C e. RR /\ 0 < C ) )
13	9 12	anim12i	|- ( ( B e. NN0 /\ C e. NN ) -> ( ( B e. RR /\ 0 <_ B ) /\ ( C e. RR /\ 0 < C ) ) )
14	13	3adant1	|- ( ( A e. ZZ /\ B e. NN0 /\ C e. NN ) -> ( ( B e. RR /\ 0 <_ B ) /\ ( C e. RR /\ 0 < C ) ) )
15		divge0	|- ( ( ( B e. RR /\ 0 <_ B ) /\ ( C e. RR /\ 0 < C ) ) -> 0 <_ ( B / C ) )
16	14 15	syl	|- ( ( A e. ZZ /\ B e. NN0 /\ C e. NN ) -> 0 <_ ( B / C ) )
17	16	biantrurd	|- ( ( A e. ZZ /\ B e. NN0 /\ C e. NN ) -> ( ( B / C ) < 1 <-> ( 0 <_ ( B / C ) /\ ( B / C ) < 1 ) ) )
18		nnrp	|- ( C e. NN -> C e. RR+ )
19	7 18	anim12i	|- ( ( B e. NN0 /\ C e. NN ) -> ( B e. RR /\ C e. RR+ ) )
20	19	3adant1	|- ( ( A e. ZZ /\ B e. NN0 /\ C e. NN ) -> ( B e. RR /\ C e. RR+ ) )
21		divlt1lt	|- ( ( B e. RR /\ C e. RR+ ) -> ( ( B / C ) < 1 <-> B < C ) )
22	20 21	syl	|- ( ( A e. ZZ /\ B e. NN0 /\ C e. NN ) -> ( ( B / C ) < 1 <-> B < C ) )
23	6 17 22	3bitr2rd	|- ( ( A e. ZZ /\ B e. NN0 /\ C e. NN ) -> ( B < C <-> ( |_ ` ( A + ( B / C ) ) ) = A ) )