Metamath Proof Explorer


Theorem flzadd

Description: An integer can be moved in and out of the floor of a sum. (Contributed by NM, 2-Jan-2009)

Ref Expression
Assertion flzadd ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( ⌊ ‘ ( 𝑁 + 𝐴 ) ) = ( 𝑁 + ( ⌊ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 fladdz ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ⌊ ‘ ( 𝐴 + 𝑁 ) ) = ( ( ⌊ ‘ 𝐴 ) + 𝑁 ) )
2 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
3 zcn ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
4 addcom ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝐴 + 𝑁 ) = ( 𝑁 + 𝐴 ) )
5 2 3 4 syl2an ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 + 𝑁 ) = ( 𝑁 + 𝐴 ) )
6 5 fveq2d ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ⌊ ‘ ( 𝐴 + 𝑁 ) ) = ( ⌊ ‘ ( 𝑁 + 𝐴 ) ) )
7 reflcl ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
8 7 recnd ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℂ )
9 addcom ( ( ( ⌊ ‘ 𝐴 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( ⌊ ‘ 𝐴 ) + 𝑁 ) = ( 𝑁 + ( ⌊ ‘ 𝐴 ) ) )
10 8 3 9 syl2an ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ( ⌊ ‘ 𝐴 ) + 𝑁 ) = ( 𝑁 + ( ⌊ ‘ 𝐴 ) ) )
11 1 6 10 3eqtr3d ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ⌊ ‘ ( 𝑁 + 𝐴 ) ) = ( 𝑁 + ( ⌊ ‘ 𝐴 ) ) )
12 11 ancoms ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( ⌊ ‘ ( 𝑁 + 𝐴 ) ) = ( 𝑁 + ( ⌊ ‘ 𝐴 ) ) )