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

Metamath Proof Explorer

Theorem nn0ge0div

Description: Division of a nonnegative integer by a positive number is not negative. (Contributed by Alexander van der Vekens, 14-Apr-2018)

Ref Expression
Assertion nn0ge0div ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → 0 ≤ ( 𝐾 / 𝐿 ) )

Proof

Step Hyp Ref Expression
1 nn0ge0 ⊢ ( 𝐾 ∈ ℕ0 → 0 ≤ 𝐾 )
2 1 adantr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → 0 ≤ 𝐾 )
3 elnnz ⊢ ( 𝐿 ∈ ℕ ↔ ( 𝐿 ∈ ℤ ∧ 0 < 𝐿 ) )
4 nn0re ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
5 4 adantr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 ∈ ℤ ∧ 0 < 𝐿 ) ) → 𝐾 ∈ ℝ )
6 zre ⊢ ( 𝐿 ∈ ℤ → 𝐿 ∈ ℝ )
7 6 ad2antrl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 ∈ ℤ ∧ 0 < 𝐿 ) ) → 𝐿 ∈ ℝ )
8 simprr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 ∈ ℤ ∧ 0 < 𝐿 ) ) → 0 < 𝐿 )
9 5 7 8 3jca ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 ∈ ℤ ∧ 0 < 𝐿 ) ) → ( 𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 0 < 𝐿 ) )
10 3 9 sylan2b ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → ( 𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 0 < 𝐿 ) )
11 ge0div ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 0 < 𝐿 ) → ( 0 ≤ 𝐾 ↔ 0 ≤ ( 𝐾 / 𝐿 ) ) )
12 10 11 syl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → ( 0 ≤ 𝐾 ↔ 0 ≤ ( 𝐾 / 𝐿 ) ) )
13 2 12 mpbid ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → 0 ≤ ( 𝐾 / 𝐿 ) )