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