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

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 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( ⌊ ‘ ( 𝑁 + 𝐴 ) ) = ( 𝑁 + ( ⌊ ‘ 𝐴 ) ) )