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