2tceilhalfelfzo1

Description: Two times a positive integer less than (the ceiling of) half of another integer is less than the other integer. This theorem would hold even for integers less than 3, but then a corresponding K would not exist. (Contributed by AV, 9-Sep-2025)

		Ref	Expression
	Assertion	2tceilhalfelfzo1	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉)) \to 2 K < N$

Proof

Step	Hyp	Ref	Expression
1		elfzo1	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \leftrightarrow (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land K < ⌈\frac{N}{2}⌉)$
2		nnz	$⊢ K \in ℕ \to K \in ℤ$
3	2	3ad2ant1	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to K \in ℤ$
4		nnz	$⊢ ⌈\frac{N}{2}⌉ \in ℕ \to ⌈\frac{N}{2}⌉ \in ℤ$
5	4	3ad2ant2	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to ⌈\frac{N}{2}⌉ \in ℤ$
6	3 5	zltlem1d	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to (K < ⌈\frac{N}{2}⌉ \leftrightarrow K \leq ⌈\frac{N}{2}⌉ - 1)$
7		nnre	$⊢ K \in ℕ \to K \in ℝ$
8	7	3ad2ant1	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to K \in ℝ$
9	8	adantr	$⊢ ((K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \land K \leq ⌈\frac{N}{2}⌉ - 1) \to K \in ℝ$
10		nnre	$⊢ ⌈\frac{N}{2}⌉ \in ℕ \to ⌈\frac{N}{2}⌉ \in ℝ$
11		1red	$⊢ ⌈\frac{N}{2}⌉ \in ℕ \to 1 \in ℝ$
12	10 11	resubcld	$⊢ ⌈\frac{N}{2}⌉ \in ℕ \to ⌈\frac{N}{2}⌉ - 1 \in ℝ$
13	12	3ad2ant2	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to ⌈\frac{N}{2}⌉ - 1 \in ℝ$
14	13	adantr	$⊢ ((K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \land K \leq ⌈\frac{N}{2}⌉ - 1) \to ⌈\frac{N}{2}⌉ - 1 \in ℝ$
15		eluzelre	$⊢ N \in ℤ_{\geq 3} \to N \in ℝ$
16	15	rehalfcld	$⊢ N \in ℤ_{\geq 3} \to \frac{N}{2} \in ℝ$
17	16	3ad2ant3	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to \frac{N}{2} \in ℝ$
18	17	adantr	$⊢ ((K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \land K \leq ⌈\frac{N}{2}⌉ - 1) \to \frac{N}{2} \in ℝ$
19		simpr	$⊢ ((K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \land K \leq ⌈\frac{N}{2}⌉ - 1) \to K \leq ⌈\frac{N}{2}⌉ - 1$
20		ceilm1lt	$⊢ \frac{N}{2} \in ℝ \to ⌈\frac{N}{2}⌉ - 1 < \frac{N}{2}$
21	17 20	syl	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to ⌈\frac{N}{2}⌉ - 1 < \frac{N}{2}$
22	21	adantr	$⊢ ((K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \land K \leq ⌈\frac{N}{2}⌉ - 1) \to ⌈\frac{N}{2}⌉ - 1 < \frac{N}{2}$
23	9 14 18 19 22	lelttrd	$⊢ ((K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \land K \leq ⌈\frac{N}{2}⌉ - 1) \to K < \frac{N}{2}$
24	23	ex	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to (K \leq ⌈\frac{N}{2}⌉ - 1 \to K < \frac{N}{2})$
25		2re	$⊢ 2 \in ℝ$
26	25	a1i	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to 2 \in ℝ$
27		2pos	$⊢ 0 < 2$
28	27	a1i	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to 0 < 2$
29		ltmul2	$⊢ (K \in ℝ \land \frac{N}{2} \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (K < \frac{N}{2} \leftrightarrow 2 K < 2 (\frac{N}{2}))$
30	8 17 26 28 29	syl112anc	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to (K < \frac{N}{2} \leftrightarrow 2 K < 2 (\frac{N}{2}))$
31		eluzelcn	$⊢ N \in ℤ_{\geq 3} \to N \in ℂ$
32	31	3ad2ant3	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to N \in ℂ$
33		2cnd	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to 2 \in ℂ$
34		2ne0	$⊢ 2 \neq 0$
35	34	a1i	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to 2 \neq 0$
36	32 33 35	divcan2d	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to 2 (\frac{N}{2}) = N$
37	36	breq2d	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to (2 K < 2 (\frac{N}{2}) \leftrightarrow 2 K < N)$
38	37	biimpd	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to (2 K < 2 (\frac{N}{2}) \to 2 K < N)$
39	30 38	sylbid	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to (K < \frac{N}{2} \to 2 K < N)$
40	24 39	syld	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to (K \leq ⌈\frac{N}{2}⌉ - 1 \to 2 K < N)$
41	6 40	sylbid	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to (K < ⌈\frac{N}{2}⌉ \to 2 K < N)$
42	41	3exp	$⊢ K \in ℕ \to (⌈\frac{N}{2}⌉ \in ℕ \to (N \in ℤ_{\geq 3} \to (K < ⌈\frac{N}{2}⌉ \to 2 K < N)))$
43	42	com34	$⊢ K \in ℕ \to (⌈\frac{N}{2}⌉ \in ℕ \to (K < ⌈\frac{N}{2}⌉ \to (N \in ℤ_{\geq 3} \to 2 K < N)))$
44	43	3imp	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land K < ⌈\frac{N}{2}⌉) \to (N \in ℤ_{\geq 3} \to 2 K < N)$
45	1 44	sylbi	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to (N \in ℤ_{\geq 3} \to 2 K < N)$
46	45	impcom	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉)) \to 2 K < N$

Metamath Proof Explorer

Theorem 2tceilhalfelfzo1

Proof