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 ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) / 𝑁 ) ) = ( ⌊ ‘ ( 𝐴 / ( 𝑀 · 𝑁 ) ) ) )

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 ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) / 𝑁 ) ) = ( ⌊ ‘ ( 𝐴 / ( 𝑀 · 𝑁 ) ) ) )