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