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 ⊢ A ∈ ℝ ∧ M ∈ ℕ ∧ N ∈ ℕ → A M N = A M ⋅ N

Proof

Step Hyp Ref Expression
1 nndivre ⊢ A ∈ ℝ ∧ M ∈ ℕ → A M ∈ ℝ
2 fldiv ⊢ A M ∈ ℝ ∧ N ∈ ℕ → A M N = A M N
3 1 2 stoic3 ⊢ A ∈ ℝ ∧ M ∈ ℕ ∧ N ∈ ℕ → A M N = A M N
4 recn ⊢ A ∈ ℝ → A ∈ ℂ
5 nncn ⊢ M ∈ ℕ → M ∈ ℂ
6 nnne0 ⊢ M ∈ ℕ → M ≠ 0
7 5 6 jca ⊢ M ∈ ℕ → M ∈ ℂ ∧ M ≠ 0
8 nncn ⊢ N ∈ ℕ → N ∈ ℂ
9 nnne0 ⊢ N ∈ ℕ → N ≠ 0
10 8 9 jca ⊢ N ∈ ℕ → N ∈ ℂ ∧ N ≠ 0
11 divdiv1 ⊢ A ∈ ℂ ∧ M ∈ ℂ ∧ M ≠ 0 ∧ N ∈ ℂ ∧ N ≠ 0 → A M N = A M ⋅ N
12 4 7 10 11 syl3an ⊢ A ∈ ℝ ∧ M ∈ ℕ ∧ N ∈ ℕ → A M N = A M ⋅ N
13 12 fveq2d ⊢ A ∈ ℝ ∧ M ∈ ℕ ∧ N ∈ ℕ → A M N = A M ⋅ N
14 3 13 eqtrd ⊢ A ∈ ℝ ∧ M ∈ ℕ ∧ N ∈ ℕ → A M N = A M ⋅ N