Metamath Proof Explorer

Theorem modlt

Description: The modulo operation is less than its second argument. (Contributed by NM, 10-Nov-2008)

Ref Expression
Assertion modlt ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A mod B < B

Proof

Step Hyp Ref Expression
1 recn ⊢ A ∈ ℝ → A ∈ ℂ
2 rpcnne0 ⊢ B ∈ ℝ + → B ∈ ℂ ∧ B ≠ 0
3 divcan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ⁢ A B = A
4 3 3expb ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ⁢ A B = A
5 1 2 4 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B ⁢ A B = A
6 5 oveq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B ⁢ A B − B ⁢ A B = A − B ⁢ A B
7 rpcn ⊢ B ∈ ℝ + → B ∈ ℂ
8 7 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B ∈ ℂ
9 rerpdivcl ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A B ∈ ℝ
10 9 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A B ∈ ℂ
11 refldivcl ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A B ∈ ℝ
12 11 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A B ∈ ℂ
13 8 10 12 subdid ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B ⁢ A B − A B = B ⁢ A B − B ⁢ A B
14 modval ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A mod B = A − B ⁢ A B
15 6 13 14 3eqtr4rd ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A mod B = B ⁢ A B − A B
16 fraclt1 ⊢ A B ∈ ℝ → A B − A B < 1
17 9 16 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A B − A B < 1
18 divid ⊢ B ∈ ℂ ∧ B ≠ 0 → B B = 1
19 2 18 syl ⊢ B ∈ ℝ + → B B = 1
20 19 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B B = 1
21 17 20 breqtrrd ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A B − A B < B B
22 9 11 resubcld ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A B − A B ∈ ℝ
23 rpre ⊢ B ∈ ℝ + → B ∈ ℝ
24 23 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B ∈ ℝ
25 rpregt0 ⊢ B ∈ ℝ + → B ∈ ℝ ∧ 0 < B
26 25 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B ∈ ℝ ∧ 0 < B
27 ltmuldiv2 ⊢ A B − A B ∈ ℝ ∧ B ∈ ℝ ∧ B ∈ ℝ ∧ 0 < B → B ⁢ A B − A B < B ↔ A B − A B < B B
28 22 24 26 27 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B ⁢ A B − A B < B ↔ A B − A B < B B
29 21 28 mpbird ⊢ A ∈ ℝ ∧ B ∈ ℝ + → B ⁢ A B − A B < B
30 15 29 eqbrtrd ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A mod B < B