Metamath Proof Explorer


Theorem moddiffl

Description: Value of the modulo operation rewritten to give two ways of expressing the quotient when " A is divided by B using Euclidean division." Multiplying both sides by B , this implies that A mod B differs from A by an integer multiple of B . (Contributed by Jeff Madsen, 17-Jun-2010) (Revised by Mario Carneiro, 6-Sep-2016)

Ref Expression
Assertion moddiffl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 modval ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) = ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
2 1 oveq2d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 − ( 𝐴 mod 𝐵 ) ) = ( 𝐴 − ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) ) )
3 simpl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
4 3 recnd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
5 rpcn ( 𝐵 ∈ ℝ+𝐵 ∈ ℂ )
6 5 adantl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
7 rerpdivcl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
8 7 flcld ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℤ )
9 8 zcnd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℂ )
10 6 9 mulcld ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ∈ ℂ )
11 4 10 nncand ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 − ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) ) = ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) )
12 2 11 eqtrd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 − ( 𝐴 mod 𝐵 ) ) = ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) )
13 12 oveq1d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) = ( ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) / 𝐵 ) )
14 rpne0 ( 𝐵 ∈ ℝ+𝐵 ≠ 0 )
15 14 adantl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ≠ 0 )
16 9 6 15 divcan3d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) / 𝐵 ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) )
17 13 16 eqtrd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) )