fldiv4lem1div2

Description: The floor of a positive integer divided by 4 is less than or equal to the half of the integer minus 1. (Contributed by AV, 9-Jul-2021)

		Ref	Expression
	Assertion	fldiv4lem1div2	$⊢ N \in ℕ \to ⌊\frac{N}{4}⌋ \leq \frac{N - 1}{2}$

Proof

Step	Hyp	Ref	Expression
1		elnn1uz2	$⊢ N \in ℕ \leftrightarrow (N = 1 \lor N \in ℤ_{\geq 2})$
2		1lt4	$⊢ 1 < 4$
3		1nn0	$⊢ 1 \in ℕ_{0}$
4		4nn	$⊢ 4 \in ℕ$
5		divfl0	$⊢ (1 \in ℕ_{0} \land 4 \in ℕ) \to (1 < 4 \leftrightarrow ⌊\frac{1}{4}⌋ = 0)$
6	3 4 5	mp2an	$⊢ 1 < 4 \leftrightarrow ⌊\frac{1}{4}⌋ = 0$
7	2 6	mpbi	$⊢ ⌊\frac{1}{4}⌋ = 0$
8		1re	$⊢ 1 \in ℝ$
9		4re	$⊢ 4 \in ℝ$
10		4ne0	$⊢ 4 \neq 0$
11		redivcl	$⊢ (1 \in ℝ \land 4 \in ℝ \land 4 \neq 0) \to \frac{1}{4} \in ℝ$
12	11	flcld	$⊢ (1 \in ℝ \land 4 \in ℝ \land 4 \neq 0) \to ⌊\frac{1}{4}⌋ \in ℤ$
13	12	zred	$⊢ (1 \in ℝ \land 4 \in ℝ \land 4 \neq 0) \to ⌊\frac{1}{4}⌋ \in ℝ$
14	8 9 10 13	mp3an	$⊢ ⌊\frac{1}{4}⌋ \in ℝ$
15	14	eqlei	$⊢ ⌊\frac{1}{4}⌋ = 0 \to ⌊\frac{1}{4}⌋ \leq 0$
16	7 15	mp1i	$⊢ N = 1 \to ⌊\frac{1}{4}⌋ \leq 0$
17		fvoveq1	$⊢ N = 1 \to ⌊\frac{N}{4}⌋ = ⌊\frac{1}{4}⌋$
18		oveq1	$⊢ N = 1 \to N - 1 = 1 - 1$
19		1m1e0	$⊢ 1 - 1 = 0$
20	18 19	eqtrdi	$⊢ N = 1 \to N - 1 = 0$
21	20	oveq1d	$⊢ N = 1 \to \frac{N - 1}{2} = \frac{0}{2}$
22		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
23		div0	$⊢ (2 \in ℂ \land 2 \neq 0) \to \frac{0}{2} = 0$
24	22 23	ax-mp	$⊢ \frac{0}{2} = 0$
25	21 24	eqtrdi	$⊢ N = 1 \to \frac{N - 1}{2} = 0$
26	16 17 25	3brtr4d	$⊢ N = 1 \to ⌊\frac{N}{4}⌋ \leq \frac{N - 1}{2}$
27		fldiv4lem1div2uz2	$⊢ N \in ℤ_{\geq 2} \to ⌊\frac{N}{4}⌋ \leq \frac{N - 1}{2}$
28	26 27	jaoi	$⊢ (N = 1 \lor N \in ℤ_{\geq 2}) \to ⌊\frac{N}{4}⌋ \leq \frac{N - 1}{2}$
29	1 28	sylbi	$⊢ N \in ℕ \to ⌊\frac{N}{4}⌋ \leq \frac{N - 1}{2}$

Metamath Proof Explorer

Theorem fldiv4lem1div2

Proof