Theorem flpmodeq

Description: Partition of a division into its integer part and the remainder. (Contributed by Alexander van der Vekens, 14-Apr-2018)

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

Proof

Step	Hyp	Ref	Expression
1		modvalr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) = ( 𝐴 − ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) ) )
2	1	eqcomd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 − ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) ) = ( 𝐴 mod 𝐵 ) )
3		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
4	3	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
5		rerpdivcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
6		flcl	⊢ ( ( 𝐴 / 𝐵 ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℤ )
7	6	zcnd	⊢ ( ( 𝐴 / 𝐵 ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℂ )
8	5 7	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℂ )
9		rpcn	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
10	9	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
11	8 10	mulcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) ∈ ℂ )
12		modcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) ∈ ℝ )
13	12	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) ∈ ℂ )
14	4 11 13	subaddd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 − ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) ) = ( 𝐴 mod 𝐵 ) ↔ ( ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) + ( 𝐴 mod 𝐵 ) ) = 𝐴 ) )
15	2 14	mpbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) · 𝐵 ) + ( 𝐴 mod 𝐵 ) ) = 𝐴 )