Metamath Proof Explorer

Theorem modge0

Description: The modulo operation is nonnegative. (Contributed by NM, 10-Nov-2008)

Ref Expression
Assertion modge0 ⊢ A ∈ ℝ ∧ B ∈ ℝ + → 0 ≤ A mod B

Proof

Step Hyp Ref Expression
1 fldivle ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A B ≤ A B
2 refldivcl ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A B ∈ ℝ
3 simpl ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A ∈ ℝ
4 rpregt0 ⊢ B ∈ ℝ + → B ∈ ℝ ∧ 0 < B
5 4 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B ∈ ℝ ∧ 0 < B
6 lemuldiv2 ⊢ A B ∈ ℝ ∧ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < B → B ⁢ A B ≤ A ↔ A B ≤ A B
7 2 3 5 6 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B ⁢ A B ≤ A ↔ A B ≤ A B
8 1 7 mpbird ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B ⁢ A B ≤ A
9 rpre ⊢ B ∈ ℝ + → B ∈ ℝ
10 9 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B ∈ ℝ
11 10 2 remulcld ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B ⁢ A B ∈ ℝ
12 subge0 ⊢ A ∈ ℝ ∧ B ⁢ A B ∈ ℝ → 0 ≤ A − B ⁢ A B ↔ B ⁢ A B ≤ A
13 11 12 syldan ⊢ A ∈ ℝ ∧ B ∈ ℝ + → 0 ≤ A − B ⁢ A B ↔ B ⁢ A B ≤ A
14 8 13 mpbird ⊢ A ∈ ℝ ∧ B ∈ ℝ + → 0 ≤ A − B ⁢ A B
15 modval ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A mod B = A − B ⁢ A B
16 14 15 breqtrrd ⊢ A ∈ ℝ ∧ B ∈ ℝ + → 0 ≤ A mod B