Theorem fldivmod

Description: Expressing the floor of a division by the modulo operator. (Contributed by AV, 6-Jun-2020)

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

Proof

Step	Hyp	Ref	Expression
1		rerpdivcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
2	1	flcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℤ )
3	2	zcnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℂ )
4		rpcn	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
5	4	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
6	3 5	mulcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) ∈ ℂ )
7		modcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) ∈ ℝ )
8	7	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) ∈ ℂ )
9	6 8	pncand	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) + ( 𝐴 mod 𝐵 ) ) − ( 𝐴 mod 𝐵 ) ) = ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) )
10	6 8	addcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) + ( 𝐴 mod 𝐵 ) ) ∈ ℂ )
11	10 8	subcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) + ( 𝐴 mod 𝐵 ) ) − ( 𝐴 mod 𝐵 ) ) ∈ ℂ )
12		rpne0	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ≠ 0 )
13	12	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ≠ 0 )
14	11 3 5 13	divmul3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ( ( ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) + ( 𝐴 mod 𝐵 ) ) − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ↔ ( ( ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) + ( 𝐴 mod 𝐵 ) ) − ( 𝐴 mod 𝐵 ) ) = ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) ) )
15	9 14	mpbird	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ( ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) + ( 𝐴 mod 𝐵 ) ) − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) )
16		flpmodeq	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) + ( 𝐴 mod 𝐵 ) ) = 𝐴 )
17	16	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) + ( 𝐴 mod 𝐵 ) ) − ( 𝐴 mod 𝐵 ) ) = ( 𝐴 − ( 𝐴 mod 𝐵 ) ) )
18	17	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ( ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) + ( 𝐴 mod 𝐵 ) ) − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) = ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) )
19	15 18	eqtr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) )