fladdz

Description: An integer can be moved in and out of the floor of a sum. (Contributed by NM, 27-Apr-2005) (Proof shortened by Fan Zheng, 16-Jun-2016)

		Ref	Expression
	Assertion	fladdz	$⊢ (A \in ℝ \land N \in ℤ) \to ⌊A + N⌋ = ⌊A⌋ + N$

Proof

Step	Hyp	Ref	Expression
1		reflcl	$⊢ A \in ℝ \to ⌊A⌋ \in ℝ$
2	1	adantr	$⊢ (A \in ℝ \land N \in ℤ) \to ⌊A⌋ \in ℝ$
3		simpl	$⊢ (A \in ℝ \land N \in ℤ) \to A \in ℝ$
4		simpr	$⊢ (A \in ℝ \land N \in ℤ) \to N \in ℤ$
5	4	zred	$⊢ (A \in ℝ \land N \in ℤ) \to N \in ℝ$
6		flle	$⊢ A \in ℝ \to ⌊A⌋ \leq A$
7	6	adantr	$⊢ (A \in ℝ \land N \in ℤ) \to ⌊A⌋ \leq A$
8	2 3 5 7	leadd1dd	$⊢ (A \in ℝ \land N \in ℤ) \to ⌊A⌋ + N \leq A + N$
9		1red	$⊢ (A \in ℝ \land N \in ℤ) \to 1 \in ℝ$
10	2 9	readdcld	$⊢ (A \in ℝ \land N \in ℤ) \to ⌊A⌋ + 1 \in ℝ$
11		flltp1	$⊢ A \in ℝ \to A < ⌊A⌋ + 1$
12	11	adantr	$⊢ (A \in ℝ \land N \in ℤ) \to A < ⌊A⌋ + 1$
13	3 10 5 12	ltadd1dd	$⊢ (A \in ℝ \land N \in ℤ) \to A + N < ⌊A⌋ + 1 + N$
14	2	recnd	$⊢ (A \in ℝ \land N \in ℤ) \to ⌊A⌋ \in ℂ$
15		1cnd	$⊢ (A \in ℝ \land N \in ℤ) \to 1 \in ℂ$
16	5	recnd	$⊢ (A \in ℝ \land N \in ℤ) \to N \in ℂ$
17	14 15 16	add32d	$⊢ (A \in ℝ \land N \in ℤ) \to ⌊A⌋ + 1 + N = ⌊A⌋ + N + 1$
18	13 17	breqtrd	$⊢ (A \in ℝ \land N \in ℤ) \to A + N < ⌊A⌋ + N + 1$
19	3 5	readdcld	$⊢ (A \in ℝ \land N \in ℤ) \to A + N \in ℝ$
20	3	flcld	$⊢ (A \in ℝ \land N \in ℤ) \to ⌊A⌋ \in ℤ$
21	20 4	zaddcld	$⊢ (A \in ℝ \land N \in ℤ) \to ⌊A⌋ + N \in ℤ$
22		flbi	$⊢ (A + N \in ℝ \land ⌊A⌋ + N \in ℤ) \to (⌊A + N⌋ = ⌊A⌋ + N \leftrightarrow (⌊A⌋ + N \leq A + N \land A + N < ⌊A⌋ + N + 1))$
23	19 21 22	syl2anc	$⊢ (A \in ℝ \land N \in ℤ) \to (⌊A + N⌋ = ⌊A⌋ + N \leftrightarrow (⌊A⌋ + N \leq A + N \land A + N < ⌊A⌋ + N + 1))$
24	8 18 23	mpbir2and	$⊢ (A \in ℝ \land N \in ℤ) \to ⌊A + N⌋ = ⌊A⌋ + N$

Metamath Proof Explorer

Theorem fladdz

Proof