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

Metamath Proof Explorer

Theorem fldivndvdslt

Description: The floor of an integer divided by a nonzero integer not dividing the first integer is less than the integer divided by the positive integer. (Contributed by AV, 4-Jul-2021)

Ref Expression
Assertion fldivndvdslt 
|- ( ( K e. ZZ /\ ( L e. ZZ /\ L =/= 0 ) /\ -. L || K ) -> ( |_ ` ( K / L ) ) < ( K / L ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( K e. ZZ -> K e. RR )
2 1 adantr 
 |-  ( ( K e. ZZ /\ ( L e. ZZ /\ L =/= 0 ) ) -> K e. RR )
3 zre 
 |-  ( L e. ZZ -> L e. RR )
4 3 ad2antrl 
 |-  ( ( K e. ZZ /\ ( L e. ZZ /\ L =/= 0 ) ) -> L e. RR )
5 simprr 
 |-  ( ( K e. ZZ /\ ( L e. ZZ /\ L =/= 0 ) ) -> L =/= 0 )
6 2 4 5 redivcld 
 |-  ( ( K e. ZZ /\ ( L e. ZZ /\ L =/= 0 ) ) -> ( K / L ) e. RR )
7 6 3adant3 
 |-  ( ( K e. ZZ /\ ( L e. ZZ /\ L =/= 0 ) /\ -. L || K ) -> ( K / L ) e. RR )
8 simprl 
 |-  ( ( K e. ZZ /\ ( L e. ZZ /\ L =/= 0 ) ) -> L e. ZZ )
9 simpl 
 |-  ( ( K e. ZZ /\ ( L e. ZZ /\ L =/= 0 ) ) -> K e. ZZ )
10 dvdsval2 
 |-  ( ( L e. ZZ /\ L =/= 0 /\ K e. ZZ ) -> ( L || K <-> ( K / L ) e. ZZ ) )
11 8 5 9 10 syl3anc 
 |-  ( ( K e. ZZ /\ ( L e. ZZ /\ L =/= 0 ) ) -> ( L || K <-> ( K / L ) e. ZZ ) )
12 11 notbid 
 |-  ( ( K e. ZZ /\ ( L e. ZZ /\ L =/= 0 ) ) -> ( -. L || K <-> -. ( K / L ) e. ZZ ) )
13 12 biimp3a 
 |-  ( ( K e. ZZ /\ ( L e. ZZ /\ L =/= 0 ) /\ -. L || K ) -> -. ( K / L ) e. ZZ )
14 flltnz 
 |-  ( ( ( K / L ) e. RR /\ -. ( K / L ) e. ZZ ) -> ( |_ ` ( K / L ) ) < ( K / L ) )
15 7 13 14 syl2anc 
 |-  ( ( K e. ZZ /\ ( L e. ZZ /\ L =/= 0 ) /\ -. L || K ) -> ( |_ ` ( K / L ) ) < ( K / L ) )