Theorem flsubz

Description: An integer can be moved in and out of the floor of a difference. (Contributed by AV, 29-May-2020)

	Ref	Expression
Assertion	flsubz	$$⊢\left(A\in ℝ\wedge N\in \mathbb{Z}\right)\to ⌊A-N⌋=⌊A⌋-N$$

Proof

Step	Hyp	Ref	Expression
1		recn	$$⊢A\in ℝ\to A\in ℂ$$
2		zcn	$$⊢N\in \mathbb{Z}\to N\in ℂ$$
3		negsub	$$⊢\left(A\in ℂ\wedge N\in ℂ\right)\to A+\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}=A-N$$
4	1 2 3	syl2an	$$⊢\left(A\in ℝ\wedge N\in \mathbb{Z}\right)\to A+\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}=A-N$$
5	4	eqcomd	$$⊢\left(A\in ℝ\wedge N\in \mathbb{Z}\right)\to A-N=A+\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}$$
6	5	fveq2d	$$⊢\left(A\in ℝ\wedge N\in \mathbb{Z}\right)\to ⌊A-N⌋=⌊A+\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}⌋$$
7		znegcl	$$⊢N\in \mathbb{Z}\to -N\in \mathbb{Z}$$
8		fladdz	$$⊢\left(A\in ℝ\wedge -N\in \mathbb{Z}\right)\to ⌊A+\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}⌋=⌊A⌋+\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}$$
9	7 8	sylan2	$$⊢\left(A\in ℝ\wedge N\in \mathbb{Z}\right)\to ⌊A+\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}⌋=⌊A⌋+\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}$$
10		reflcl	$$⊢A\in ℝ\to ⌊A⌋\in ℝ$$
11	10	recnd	$$⊢A\in ℝ\to ⌊A⌋\in ℂ$$
12		negsub	$$⊢\left(⌊A⌋\in ℂ\wedge N\in ℂ\right)\to ⌊A⌋+\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}=⌊A⌋-N$$
13	11 2 12	syl2an	$$⊢\left(A\in ℝ\wedge N\in \mathbb{Z}\right)\to ⌊A⌋+\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}=⌊A⌋-N$$
14	6 9 13	3eqtrd	$$⊢\left(A\in ℝ\wedge N\in \mathbb{Z}\right)\to ⌊A-N⌋=⌊A⌋-N$$