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	$$⊢\left(N\in \mathbb{Z}\wedge A\in ℝ\right)\to ⌊N+A⌋=N+⌊A⌋$$

Proof

Step	Hyp	Ref	Expression
1		fladdz	$$⊢\left(A\in ℝ\wedge N\in \mathbb{Z}\right)\to ⌊A+N⌋=⌊A⌋+N$$
2		recn	$$⊢A\in ℝ\to A\in ℂ$$
3		zcn	$$⊢N\in \mathbb{Z}\to N\in ℂ$$
4		addcom	$$⊢\left(A\in ℂ\wedge N\in ℂ\right)\to A+N=N+A$$
5	2 3 4	syl2an	$$⊢\left(A\in ℝ\wedge N\in \mathbb{Z}\right)\to A+N=N+A$$
6	5	fveq2d	$$⊢\left(A\in ℝ\wedge N\in \mathbb{Z}\right)\to ⌊A+N⌋=⌊N+A⌋$$
7		reflcl	$$⊢A\in ℝ\to ⌊A⌋\in ℝ$$
8	7	recnd	$$⊢A\in ℝ\to ⌊A⌋\in ℂ$$
9		addcom	$$⊢\left(⌊A⌋\in ℂ\wedge N\in ℂ\right)\to ⌊A⌋+N=N+⌊A⌋$$
10	8 3 9	syl2an	$$⊢\left(A\in ℝ\wedge N\in \mathbb{Z}\right)\to ⌊A⌋+N=N+⌊A⌋$$
11	1 6 10	3eqtr3d	$$⊢\left(A\in ℝ\wedge N\in \mathbb{Z}\right)\to ⌊N+A⌋=N+⌊A⌋$$
12	11	ancoms	$$⊢\left(N\in \mathbb{Z}\wedge A\in ℝ\right)\to ⌊N+A⌋=N+⌊A⌋$$