This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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