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 ( ( 𝐾 ∈ ℤ ∧ ( 𝐿 ∈ ℤ ∧ 𝐿 ≠ 0 ) ∧ ¬ 𝐿 ∥ 𝐾 ) → ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) < ( 𝐾 / 𝐿 ) )

Proof

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