Theorem fldiv2

Description: Cancellation of an embedded floor of a ratio. Generalization of Equation 2.4 in CormenLeisersonRivest p. 33 (where A must be an integer). (Contributed by NM, 9-Nov-2008)

	Ref	Expression
Assertion	fldiv2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) / 𝑁 ) ) = ( ⌊ ‘ ( 𝐴 / ( 𝑀 · 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		nndivre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( 𝐴 / 𝑀 ) ∈ ℝ )
2		fldiv	⊢ ( ( ( 𝐴 / 𝑀 ) ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) / 𝑁 ) ) = ( ⌊ ‘ ( ( 𝐴 / 𝑀 ) / 𝑁 ) ) )
3	1 2	stoic3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) / 𝑁 ) ) = ( ⌊ ‘ ( ( 𝐴 / 𝑀 ) / 𝑁 ) ) )
4		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
5		nncn	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
6		nnne0	⊢ ( 𝑀 ∈ ℕ → 𝑀 ≠ 0 )
7	5 6	jca	⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) )
8		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
9		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
10	8 9	jca	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) )
11		divdiv1	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝐴 / 𝑀 ) / 𝑁 ) = ( 𝐴 / ( 𝑀 · 𝑁 ) ) )
12	4 7 10 11	syl3an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 / 𝑀 ) / 𝑁 ) = ( 𝐴 / ( 𝑀 · 𝑁 ) ) )
13	12	fveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝐴 / 𝑀 ) / 𝑁 ) ) = ( ⌊ ‘ ( 𝐴 / ( 𝑀 · 𝑁 ) ) ) )
14	3 13	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) / 𝑁 ) ) = ( ⌊ ‘ ( 𝐴 / ( 𝑀 · 𝑁 ) ) ) )