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

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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) < 𝐵 )

Proof

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