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

Metamath Proof Explorer

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 ) )