Metamath Proof Explorer

Theorem flltdivnn0lt

Description: The floor function of a division of a nonnegative integer by a positive integer is less than the division of a greater dividend by the same positive integer. (Contributed by Alexander van der Vekens, 14-Apr-2018)

Ref Expression
Assertion flltdivnn0lt 
|- ( ( K e. NN0 /\ N e. NN0 /\ L e. NN ) -> ( K < N -> ( |_ ` ( K / L ) ) < ( N / L ) ) )

Proof

Step Hyp Ref Expression
1 nn0nndivcl 
 |-  ( ( K e. NN0 /\ L e. NN ) -> ( K / L ) e. RR )
2 reflcl 
 |-  ( ( K / L ) e. RR -> ( |_ ` ( K / L ) ) e. RR )
3 1 2 syl 
 |-  ( ( K e. NN0 /\ L e. NN ) -> ( |_ ` ( K / L ) ) e. RR )
4 3 3adant2 
 |-  ( ( K e. NN0 /\ N e. NN0 /\ L e. NN ) -> ( |_ ` ( K / L ) ) e. RR )
5 1 3adant2 
 |-  ( ( K e. NN0 /\ N e. NN0 /\ L e. NN ) -> ( K / L ) e. RR )
6 nn0nndivcl 
 |-  ( ( N e. NN0 /\ L e. NN ) -> ( N / L ) e. RR )
7 6 3adant1 
 |-  ( ( K e. NN0 /\ N e. NN0 /\ L e. NN ) -> ( N / L ) e. RR )
8 4 5 7 3jca 
 |-  ( ( K e. NN0 /\ N e. NN0 /\ L e. NN ) -> ( ( |_ ` ( K / L ) ) e. RR /\ ( K / L ) e. RR /\ ( N / L ) e. RR ) )
9 8 adantr 
 |-  ( ( ( K e. NN0 /\ N e. NN0 /\ L e. NN ) /\ K < N ) -> ( ( |_ ` ( K / L ) ) e. RR /\ ( K / L ) e. RR /\ ( N / L ) e. RR ) )
10 fldivnn0le 
 |-  ( ( K e. NN0 /\ L e. NN ) -> ( |_ ` ( K / L ) ) <_ ( K / L ) )
11 10 3adant2 
 |-  ( ( K e. NN0 /\ N e. NN0 /\ L e. NN ) -> ( |_ ` ( K / L ) ) <_ ( K / L ) )
12 11 adantr 
 |-  ( ( ( K e. NN0 /\ N e. NN0 /\ L e. NN ) /\ K < N ) -> ( |_ ` ( K / L ) ) <_ ( K / L ) )
13 simpr 
 |-  ( ( ( K e. NN0 /\ N e. NN0 /\ L e. NN ) /\ K < N ) -> K < N )
14 nn0re 
 |-  ( K e. NN0 -> K e. RR )
15 nn0re 
 |-  ( N e. NN0 -> N e. RR )
16 nnre 
 |-  ( L e. NN -> L e. RR )
17 nngt0 
 |-  ( L e. NN -> 0 < L )
18 16 17 jca 
 |-  ( L e. NN -> ( L e. RR /\ 0 < L ) )
19 14 15 18 3anim123i 
 |-  ( ( K e. NN0 /\ N e. NN0 /\ L e. NN ) -> ( K e. RR /\ N e. RR /\ ( L e. RR /\ 0 < L ) ) )
20 19 adantr 
 |-  ( ( ( K e. NN0 /\ N e. NN0 /\ L e. NN ) /\ K < N ) -> ( K e. RR /\ N e. RR /\ ( L e. RR /\ 0 < L ) ) )
21 ltdiv1 
 |-  ( ( K e. RR /\ N e. RR /\ ( L e. RR /\ 0 < L ) ) -> ( K < N <-> ( K / L ) < ( N / L ) ) )
22 20 21 syl 
 |-  ( ( ( K e. NN0 /\ N e. NN0 /\ L e. NN ) /\ K < N ) -> ( K < N <-> ( K / L ) < ( N / L ) ) )
23 13 22 mpbid 
 |-  ( ( ( K e. NN0 /\ N e. NN0 /\ L e. NN ) /\ K < N ) -> ( K / L ) < ( N / L ) )
24 12 23 jca 
 |-  ( ( ( K e. NN0 /\ N e. NN0 /\ L e. NN ) /\ K < N ) -> ( ( |_ ` ( K / L ) ) <_ ( K / L ) /\ ( K / L ) < ( N / L ) ) )
25 lelttr 
 |-  ( ( ( |_ ` ( K / L ) ) e. RR /\ ( K / L ) e. RR /\ ( N / L ) e. RR ) -> ( ( ( |_ ` ( K / L ) ) <_ ( K / L ) /\ ( K / L ) < ( N / L ) ) -> ( |_ ` ( K / L ) ) < ( N / L ) ) )
26 9 24 25 sylc 
 |-  ( ( ( K e. NN0 /\ N e. NN0 /\ L e. NN ) /\ K < N ) -> ( |_ ` ( K / L ) ) < ( N / L ) )
27 26 ex 
 |-  ( ( K e. NN0 /\ N e. NN0 /\ L e. NN ) -> ( K < N -> ( |_ ` ( K / L ) ) < ( N / L ) ) )