zofldiv2ALTV

Description: The floor of an odd numer divided by 2 is equal to the odd number first decreased by 1 and then divided by 2. (Contributed by AV, 7-Jun-2020) (Revised by AV, 18-Jun-2020)

		Ref	Expression
	Assertion	zofldiv2ALTV	$⊢ N \in Odd \to ⌊\frac{N}{2}⌋ = \frac{N - 1}{2}$

Proof

Step	Hyp	Ref	Expression
1		oddz	$⊢ N \in Odd \to N \in ℤ$
2	1	zcnd	$⊢ N \in Odd \to N \in ℂ$
3		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
4	3	eqcomd	$⊢ N \in ℂ \to N = N - 1 + 1$
5	4	oveq1d	$⊢ N \in ℂ \to \frac{N}{2} = \frac{N - 1 + 1}{2}$
6		peano2cnm	$⊢ N \in ℂ \to N - 1 \in ℂ$
7		1cnd	$⊢ N \in ℂ \to 1 \in ℂ$
8		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
9	8	a1i	$⊢ N \in ℂ \to (2 \in ℂ \land 2 \neq 0)$
10		divdir	$⊢ (N - 1 \in ℂ \land 1 \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{N - 1 + 1}{2} = (\frac{N - 1}{2}) + (\frac{1}{2})$
11	6 7 9 10	syl3anc	$⊢ N \in ℂ \to \frac{N - 1 + 1}{2} = (\frac{N - 1}{2}) + (\frac{1}{2})$
12	5 11	eqtrd	$⊢ N \in ℂ \to \frac{N}{2} = (\frac{N - 1}{2}) + (\frac{1}{2})$
13	2 12	syl	$⊢ N \in Odd \to \frac{N}{2} = (\frac{N - 1}{2}) + (\frac{1}{2})$
14	13	fveq2d	$⊢ N \in Odd \to ⌊\frac{N}{2}⌋ = ⌊(\frac{N - 1}{2}) + (\frac{1}{2})⌋$
15		halfge0	$⊢ 0 \leq \frac{1}{2}$
16		halflt1	$⊢ \frac{1}{2} < 1$
17	15 16	pm3.2i	$⊢ (0 \leq \frac{1}{2} \land \frac{1}{2} < 1)$
18		oddm1div2z	$⊢ N \in Odd \to \frac{N - 1}{2} \in ℤ$
19		halfre	$⊢ \frac{1}{2} \in ℝ$
20		flbi2	$⊢ (\frac{N - 1}{2} \in ℤ \land \frac{1}{2} \in ℝ) \to (⌊(\frac{N - 1}{2}) + (\frac{1}{2})⌋ = \frac{N - 1}{2} \leftrightarrow (0 \leq \frac{1}{2} \land \frac{1}{2} < 1))$
21	18 19 20	sylancl	$⊢ N \in Odd \to (⌊(\frac{N - 1}{2}) + (\frac{1}{2})⌋ = \frac{N - 1}{2} \leftrightarrow (0 \leq \frac{1}{2} \land \frac{1}{2} < 1))$
22	17 21	mpbiri	$⊢ N \in Odd \to ⌊(\frac{N - 1}{2}) + (\frac{1}{2})⌋ = \frac{N - 1}{2}$
23	14 22	eqtrd	$⊢ N \in Odd \to ⌊\frac{N}{2}⌋ = \frac{N - 1}{2}$

Metamath Proof Explorer

Theorem zofldiv2ALTV

Proof