Metamath Proof Explorer

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	$⊢ (A \in ℝ \land M \in ℕ \land N \in ℕ) \to ⌊\frac{⌊\frac{A}{M}⌋}{N}⌋ = ⌊\frac{A}{M \cdot N}⌋$

Proof

Step	Hyp	Ref	Expression
1		nndivre	$⊢ (A \in ℝ \land M \in ℕ) \to \frac{A}{M} \in ℝ$
2		fldiv	$⊢ (\frac{A}{M} \in ℝ \land N \in ℕ) \to ⌊\frac{⌊\frac{A}{M}⌋}{N}⌋ = ⌊\frac{\frac{A}{M}}{N}⌋$
3	1 2	stoic3	$⊢ (A \in ℝ \land M \in ℕ \land N \in ℕ) \to ⌊\frac{⌊\frac{A}{M}⌋}{N}⌋ = ⌊\frac{\frac{A}{M}}{N}⌋$
4		recn	$⊢ A \in ℝ \to A \in ℂ$
5		nncn	$⊢ M \in ℕ \to M \in ℂ$
6		nnne0	$⊢ M \in ℕ \to M \neq 0$
7	5 6	jca	$⊢ M \in ℕ \to (M \in ℂ \land M \neq 0)$
8		nncn	$⊢ N \in ℕ \to N \in ℂ$
9		nnne0	$⊢ N \in ℕ \to N \neq 0$
10	8 9	jca	$⊢ N \in ℕ \to (N \in ℂ \land N \neq 0)$
11		divdiv1	$⊢ (A \in ℂ \land (M \in ℂ \land M \neq 0) \land (N \in ℂ \land N \neq 0)) \to \frac{\frac{A}{M}}{N} = \frac{A}{M \cdot N}$
12	4 7 10 11	syl3an	$⊢ (A \in ℝ \land M \in ℕ \land N \in ℕ) \to \frac{\frac{A}{M}}{N} = \frac{A}{M \cdot N}$
13	12	fveq2d	$⊢ (A \in ℝ \land M \in ℕ \land N \in ℕ) \to ⌊\frac{\frac{A}{M}}{N}⌋ = ⌊\frac{A}{M \cdot N}⌋$
14	3 13	eqtrd	$⊢ (A \in ℝ \land M \in ℕ \land N \in ℕ) \to ⌊\frac{⌊\frac{A}{M}⌋}{N}⌋ = ⌊\frac{A}{M \cdot N}⌋$