halfleoddlt

Description: An integer is greater than half of an odd number iff it is greater than or equal to the half of the odd number. (Contributed by AV, 1-Jul-2021)

		Ref	Expression
	Assertion	halfleoddlt	$⊢ (N \in ℤ \land \neg 2 ∥ N \land M \in ℤ) \to (\frac{N}{2} \leq M \leftrightarrow \frac{N}{2} < M)$

Proof

Step	Hyp	Ref	Expression
1		odd2np1	$⊢ N \in ℤ \to (\neg 2 ∥ N \leftrightarrow \exists n \in ℤ 2 n + 1 = N)$
2		0xr	$⊢ 0 \in ℝ^{*}$
3		1xr	$⊢ 1 \in ℝ^{*}$
4		halfre	$⊢ \frac{1}{2} \in ℝ$
5	4	rexri	$⊢ \frac{1}{2} \in ℝ^{*}$
6	2 3 5	3pm3.2i	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{} \land \frac{1}{2} \in ℝ^{*})$
7		halfgt0	$⊢ 0 < \frac{1}{2}$
8		halflt1	$⊢ \frac{1}{2} < 1$
9	7 8	pm3.2i	$⊢ (0 < \frac{1}{2} \land \frac{1}{2} < 1)$
10		elioo3g	$⊢ \frac{1}{2} \in (0, 1) \leftrightarrow ((0 \in ℝ^{} \land 1 \in ℝ^{} \land \frac{1}{2} \in ℝ^{*}) \land (0 < \frac{1}{2} \land \frac{1}{2} < 1))$
11	6 9 10	mpbir2an	$⊢ \frac{1}{2} \in (0, 1)$
12		zltaddlt1le	$⊢ (n \in ℤ \land M \in ℤ \land \frac{1}{2} \in (0, 1)) \to (n + (\frac{1}{2}) < M \leftrightarrow n + (\frac{1}{2}) \leq M)$
13	11 12	mp3an3	$⊢ (n \in ℤ \land M \in ℤ) \to (n + (\frac{1}{2}) < M \leftrightarrow n + (\frac{1}{2}) \leq M)$
14		zcn	$⊢ n \in ℤ \to n \in ℂ$
15	14	adantr	$⊢ (n \in ℤ \land M \in ℤ) \to n \in ℂ$
16		1cnd	$⊢ (n \in ℤ \land M \in ℤ) \to 1 \in ℂ$
17		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
18	17	a1i	$⊢ (n \in ℤ \land M \in ℤ) \to (2 \in ℂ \land 2 \neq 0)$
19		muldivdir	$⊢ (n \in ℂ \land 1 \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{2 n + 1}{2} = n + (\frac{1}{2})$
20	15 16 18 19	syl3anc	$⊢ (n \in ℤ \land M \in ℤ) \to \frac{2 n + 1}{2} = n + (\frac{1}{2})$
21	20	breq1d	$⊢ (n \in ℤ \land M \in ℤ) \to (\frac{2 n + 1}{2} < M \leftrightarrow n + (\frac{1}{2}) < M)$
22	20	breq1d	$⊢ (n \in ℤ \land M \in ℤ) \to (\frac{2 n + 1}{2} \leq M \leftrightarrow n + (\frac{1}{2}) \leq M)$
23	13 21 22	3bitr4rd	$⊢ (n \in ℤ \land M \in ℤ) \to (\frac{2 n + 1}{2} \leq M \leftrightarrow \frac{2 n + 1}{2} < M)$
24		oveq1	$⊢ 2 n + 1 = N \to \frac{2 n + 1}{2} = \frac{N}{2}$
25	24	breq1d	$⊢ 2 n + 1 = N \to (\frac{2 n + 1}{2} \leq M \leftrightarrow \frac{N}{2} \leq M)$
26	24	breq1d	$⊢ 2 n + 1 = N \to (\frac{2 n + 1}{2} < M \leftrightarrow \frac{N}{2} < M)$
27	25 26	bibi12d	$⊢ 2 n + 1 = N \to ((\frac{2 n + 1}{2} \leq M \leftrightarrow \frac{2 n + 1}{2} < M) \leftrightarrow (\frac{N}{2} \leq M \leftrightarrow \frac{N}{2} < M))$
28	23 27	syl5ibcom	$⊢ (n \in ℤ \land M \in ℤ) \to (2 n + 1 = N \to (\frac{N}{2} \leq M \leftrightarrow \frac{N}{2} < M))$
29	28	ex	$⊢ n \in ℤ \to (M \in ℤ \to (2 n + 1 = N \to (\frac{N}{2} \leq M \leftrightarrow \frac{N}{2} < M)))$
30	29	adantl	$⊢ (N \in ℤ \land n \in ℤ) \to (M \in ℤ \to (2 n + 1 = N \to (\frac{N}{2} \leq M \leftrightarrow \frac{N}{2} < M)))$
31	30	com23	$⊢ (N \in ℤ \land n \in ℤ) \to (2 n + 1 = N \to (M \in ℤ \to (\frac{N}{2} \leq M \leftrightarrow \frac{N}{2} < M)))$
32	31	rexlimdva	$⊢ N \in ℤ \to (\exists n \in ℤ 2 n + 1 = N \to (M \in ℤ \to (\frac{N}{2} \leq M \leftrightarrow \frac{N}{2} < M)))$
33	1 32	sylbid	$⊢ N \in ℤ \to (\neg 2 ∥ N \to (M \in ℤ \to (\frac{N}{2} \leq M \leftrightarrow \frac{N}{2} < M)))$
34	33	3imp	$⊢ (N \in ℤ \land \neg 2 ∥ N \land M \in ℤ) \to (\frac{N}{2} \leq M \leftrightarrow \frac{N}{2} < M)$

Metamath Proof Explorer

Theorem halfleoddlt

Proof