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

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 𝐵 ) ) / 𝐵 ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) )