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 ∈ ℤ ∧ L ∈ ℤ ∧ L ≠ 0 ∧ ¬ L ∥ K → K L < K L

Proof

Step Hyp Ref Expression
1 zre ⊢ K ∈ ℤ → K ∈ ℝ
2 1 adantr ⊢ K ∈ ℤ ∧ L ∈ ℤ ∧ L ≠ 0 → K ∈ ℝ
3 zre ⊢ L ∈ ℤ → L ∈ ℝ
4 3 ad2antrl ⊢ K ∈ ℤ ∧ L ∈ ℤ ∧ L ≠ 0 → L ∈ ℝ
5 simprr ⊢ K ∈ ℤ ∧ L ∈ ℤ ∧ L ≠ 0 → L ≠ 0
6 2 4 5 redivcld ⊢ K ∈ ℤ ∧ L ∈ ℤ ∧ L ≠ 0 → K L ∈ ℝ
7 6 3adant3 ⊢ K ∈ ℤ ∧ L ∈ ℤ ∧ L ≠ 0 ∧ ¬ L ∥ K → K L ∈ ℝ
8 simprl ⊢ K ∈ ℤ ∧ L ∈ ℤ ∧ L ≠ 0 → L ∈ ℤ
9 simpl ⊢ K ∈ ℤ ∧ L ∈ ℤ ∧ L ≠ 0 → K ∈ ℤ
10 dvdsval2 ⊢ L ∈ ℤ ∧ L ≠ 0 ∧ K ∈ ℤ → L ∥ K ↔ K L ∈ ℤ
11 8 5 9 10 syl3anc ⊢ K ∈ ℤ ∧ L ∈ ℤ ∧ L ≠ 0 → L ∥ K ↔ K L ∈ ℤ
12 11 notbid ⊢ K ∈ ℤ ∧ L ∈ ℤ ∧ L ≠ 0 → ¬ L ∥ K ↔ ¬ K L ∈ ℤ
13 12 biimp3a ⊢ K ∈ ℤ ∧ L ∈ ℤ ∧ L ≠ 0 ∧ ¬ L ∥ K → ¬ K L ∈ ℤ
14 flltnz ⊢ K L ∈ ℝ ∧ ¬ K L ∈ ℤ → K L < K L
15 7 13 14 syl2anc ⊢ K ∈ ℤ ∧ L ∈ ℤ ∧ L ≠ 0 ∧ ¬ L ∥ K → K L < K L