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∈ℝ+→AmodB<B

Proof

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