Theorem modval

Description: The value of the modulo operation. The modulo congruence notation of number theory, J == K (modulo N ), can be expressed in our notation as ( J mod N ) = ( K mod N ) . Definition 1 in Knuth,The Art of Computer Programming, Vol. I (1972), p. 38. Knuth uses "mod" for the operation and "modulo" for the congruence. Unlike Knuth, we restrict the second argument to positive reals to simplify certain theorems. (This also gives us future flexibility to extend it to any one of several different conventions for a zero or negative second argument, should there be an advantage in doing so.) (Contributed by NM, 10-Nov-2008) (Revised by Mario Carneiro, 3-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		fvoveq1	⊢ ( 𝑥 = 𝐴 → ( ⌊ ‘ ( 𝑥 / 𝑦 ) ) = ( ⌊ ‘ ( 𝐴 / 𝑦 ) ) )
2	1	oveq2d	⊢ ( 𝑥 = 𝐴 → ( 𝑦 · ( ⌊ ‘ ( 𝑥 / 𝑦 ) ) ) = ( 𝑦 · ( ⌊ ‘ ( 𝐴 / 𝑦 ) ) ) )
3		oveq12	⊢ ( ( 𝑥 = 𝐴 ∧ ( 𝑦 · ( ⌊ ‘ ( 𝑥 / 𝑦 ) ) ) = ( 𝑦 · ( ⌊ ‘ ( 𝐴 / 𝑦 ) ) ) ) → ( 𝑥 − ( 𝑦 · ( ⌊ ‘ ( 𝑥 / 𝑦 ) ) ) ) = ( 𝐴 − ( 𝑦 · ( ⌊ ‘ ( 𝐴 / 𝑦 ) ) ) ) )
4	2 3	mpdan	⊢ ( 𝑥 = 𝐴 → ( 𝑥 − ( 𝑦 · ( ⌊ ‘ ( 𝑥 / 𝑦 ) ) ) ) = ( 𝐴 − ( 𝑦 · ( ⌊ ‘ ( 𝐴 / 𝑦 ) ) ) ) )
5		oveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 / 𝑦 ) = ( 𝐴 / 𝐵 ) )
6	5	fveq2d	⊢ ( 𝑦 = 𝐵 → ( ⌊ ‘ ( 𝐴 / 𝑦 ) ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) )
7		oveq12	⊢ ( ( 𝑦 = 𝐵 ∧ ( ⌊ ‘ ( 𝐴 / 𝑦 ) ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) → ( 𝑦 · ( ⌊ ‘ ( 𝐴 / 𝑦 ) ) ) = ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) )
8	6 7	mpdan	⊢ ( 𝑦 = 𝐵 → ( 𝑦 · ( ⌊ ‘ ( 𝐴 / 𝑦 ) ) ) = ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) )
9	8	oveq2d	⊢ ( 𝑦 = 𝐵 → ( 𝐴 − ( 𝑦 · ( ⌊ ‘ ( 𝐴 / 𝑦 ) ) ) ) = ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
10		df-mod	⊢ mod = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ+ ↦ ( 𝑥 − ( 𝑦 · ( ⌊ ‘ ( 𝑥 / 𝑦 ) ) ) ) )
11		ovex	⊢ ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) ∈ V
12	4 9 10 11	ovmpo	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) = ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )