ltoddhalfle

Description: An integer is less than half of an odd number iff it is less than or equal to the half of the predecessor of the odd number (which is an even number). (Contributed by AV, 29-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		odd2np1	$⊢ N \in ℤ \to (\neg 2 ∥ N \leftrightarrow \exists n \in ℤ 2 n + 1 = N)$
2		halfre	$⊢ \frac{1}{2} \in ℝ$
3	2	a1i	$⊢ n \in ℤ \to \frac{1}{2} \in ℝ$
4		1red	$⊢ n \in ℤ \to 1 \in ℝ$
5		zre	$⊢ n \in ℤ \to n \in ℝ$
6	3 4 5	3jca	$⊢ n \in ℤ \to (\frac{1}{2} \in ℝ \land 1 \in ℝ \land n \in ℝ)$
7	6	adantr	$⊢ (n \in ℤ \land M \in ℤ) \to (\frac{1}{2} \in ℝ \land 1 \in ℝ \land n \in ℝ)$
8		halflt1	$⊢ \frac{1}{2} < 1$
9		axltadd	$⊢ (\frac{1}{2} \in ℝ \land 1 \in ℝ \land n \in ℝ) \to (\frac{1}{2} < 1 \to n + (\frac{1}{2}) < n + 1)$
10	7 8 9	mpisyl	$⊢ (n \in ℤ \land M \in ℤ) \to n + (\frac{1}{2}) < n + 1$
11		zre	$⊢ M \in ℤ \to M \in ℝ$
12	11	adantl	$⊢ (n \in ℤ \land M \in ℤ) \to M \in ℝ$
13	5 3	readdcld	$⊢ n \in ℤ \to n + (\frac{1}{2}) \in ℝ$
14	13	adantr	$⊢ (n \in ℤ \land M \in ℤ) \to n + (\frac{1}{2}) \in ℝ$
15		peano2z	$⊢ n \in ℤ \to n + 1 \in ℤ$
16	15	zred	$⊢ n \in ℤ \to n + 1 \in ℝ$
17	16	adantr	$⊢ (n \in ℤ \land M \in ℤ) \to n + 1 \in ℝ$
18		lttr	$⊢ (M \in ℝ \land n + (\frac{1}{2}) \in ℝ \land n + 1 \in ℝ) \to ((M < n + (\frac{1}{2}) \land n + (\frac{1}{2}) < n + 1) \to M < n + 1)$
19	12 14 17 18	syl3anc	$⊢ (n \in ℤ \land M \in ℤ) \to ((M < n + (\frac{1}{2}) \land n + (\frac{1}{2}) < n + 1) \to M < n + 1)$
20	10 19	mpan2d	$⊢ (n \in ℤ \land M \in ℤ) \to (M < n + (\frac{1}{2}) \to M < n + 1)$
21		zleltp1	$⊢ (M \in ℤ \land n \in ℤ) \to (M \leq n \leftrightarrow M < n + 1)$
22	21	ancoms	$⊢ (n \in ℤ \land M \in ℤ) \to (M \leq n \leftrightarrow M < n + 1)$
23	20 22	sylibrd	$⊢ (n \in ℤ \land M \in ℤ) \to (M < n + (\frac{1}{2}) \to M \leq n)$
24		halfgt0	$⊢ 0 < \frac{1}{2}$
25	3 5	jca	$⊢ n \in ℤ \to (\frac{1}{2} \in ℝ \land n \in ℝ)$
26	25	adantr	$⊢ (n \in ℤ \land M \in ℤ) \to (\frac{1}{2} \in ℝ \land n \in ℝ)$
27		ltaddpos	$⊢ (\frac{1}{2} \in ℝ \land n \in ℝ) \to (0 < \frac{1}{2} \leftrightarrow n < n + (\frac{1}{2}))$
28	26 27	syl	$⊢ (n \in ℤ \land M \in ℤ) \to (0 < \frac{1}{2} \leftrightarrow n < n + (\frac{1}{2}))$
29	24 28	mpbii	$⊢ (n \in ℤ \land M \in ℤ) \to n < n + (\frac{1}{2})$
30	5	adantr	$⊢ (n \in ℤ \land M \in ℤ) \to n \in ℝ$
31		lelttr	$⊢ (M \in ℝ \land n \in ℝ \land n + (\frac{1}{2}) \in ℝ) \to ((M \leq n \land n < n + (\frac{1}{2})) \to M < n + (\frac{1}{2}))$
32	12 30 14 31	syl3anc	$⊢ (n \in ℤ \land M \in ℤ) \to ((M \leq n \land n < n + (\frac{1}{2})) \to M < n + (\frac{1}{2}))$
33	29 32	mpan2d	$⊢ (n \in ℤ \land M \in ℤ) \to (M \leq n \to M < n + (\frac{1}{2}))$
34	23 33	impbid	$⊢ (n \in ℤ \land M \in ℤ) \to (M < n + (\frac{1}{2}) \leftrightarrow M \leq n)$
35		zcn	$⊢ n \in ℤ \to n \in ℂ$
36		1cnd	$⊢ n \in ℤ \to 1 \in ℂ$
37		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
38	37	a1i	$⊢ n \in ℤ \to (2 \in ℂ \land 2 \neq 0)$
39		muldivdir	$⊢ (n \in ℂ \land 1 \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{2 n + 1}{2} = n + (\frac{1}{2})$
40	35 36 38 39	syl3anc	$⊢ n \in ℤ \to \frac{2 n + 1}{2} = n + (\frac{1}{2})$
41	40	breq2d	$⊢ n \in ℤ \to (M < \frac{2 n + 1}{2} \leftrightarrow M < n + (\frac{1}{2}))$
42	41	adantr	$⊢ (n \in ℤ \land M \in ℤ) \to (M < \frac{2 n + 1}{2} \leftrightarrow M < n + (\frac{1}{2}))$
43		2z	$⊢ 2 \in ℤ$
44	43	a1i	$⊢ n \in ℤ \to 2 \in ℤ$
45		id	$⊢ n \in ℤ \to n \in ℤ$
46	44 45	zmulcld	$⊢ n \in ℤ \to 2 n \in ℤ$
47	46	zcnd	$⊢ n \in ℤ \to 2 n \in ℂ$
48	47	adantr	$⊢ (n \in ℤ \land M \in ℤ) \to 2 n \in ℂ$
49		pncan1	$⊢ 2 n \in ℂ \to 2 n + 1 - 1 = 2 n$
50	48 49	syl	$⊢ (n \in ℤ \land M \in ℤ) \to 2 n + 1 - 1 = 2 n$
51	50	oveq1d	$⊢ (n \in ℤ \land M \in ℤ) \to \frac{2 n + 1 - 1}{2} = \frac{2 n}{2}$
52		2cnd	$⊢ n \in ℤ \to 2 \in ℂ$
53		2ne0	$⊢ 2 \neq 0$
54	53	a1i	$⊢ n \in ℤ \to 2 \neq 0$
55	35 52 54	divcan3d	$⊢ n \in ℤ \to \frac{2 n}{2} = n$
56	55	adantr	$⊢ (n \in ℤ \land M \in ℤ) \to \frac{2 n}{2} = n$
57	51 56	eqtrd	$⊢ (n \in ℤ \land M \in ℤ) \to \frac{2 n + 1 - 1}{2} = n$
58	57	breq2d	$⊢ (n \in ℤ \land M \in ℤ) \to (M \leq \frac{2 n + 1 - 1}{2} \leftrightarrow M \leq n)$
59	34 42 58	3bitr4d	$⊢ (n \in ℤ \land M \in ℤ) \to (M < \frac{2 n + 1}{2} \leftrightarrow M \leq \frac{2 n + 1 - 1}{2})$
60		oveq1	$⊢ 2 n + 1 = N \to \frac{2 n + 1}{2} = \frac{N}{2}$
61	60	breq2d	$⊢ 2 n + 1 = N \to (M < \frac{2 n + 1}{2} \leftrightarrow M < \frac{N}{2})$
62		oveq1	$⊢ 2 n + 1 = N \to 2 n + 1 - 1 = N - 1$
63	62	oveq1d	$⊢ 2 n + 1 = N \to \frac{2 n + 1 - 1}{2} = \frac{N - 1}{2}$
64	63	breq2d	$⊢ 2 n + 1 = N \to (M \leq \frac{2 n + 1 - 1}{2} \leftrightarrow M \leq \frac{N - 1}{2})$
65	61 64	bibi12d	$⊢ 2 n + 1 = N \to ((M < \frac{2 n + 1}{2} \leftrightarrow M \leq \frac{2 n + 1 - 1}{2}) \leftrightarrow (M < \frac{N}{2} \leftrightarrow M \leq \frac{N - 1}{2}))$
66	59 65	syl5ibcom	$⊢ (n \in ℤ \land M \in ℤ) \to (2 n + 1 = N \to (M < \frac{N}{2} \leftrightarrow M \leq \frac{N - 1}{2}))$
67	66	ex	$⊢ n \in ℤ \to (M \in ℤ \to (2 n + 1 = N \to (M < \frac{N}{2} \leftrightarrow M \leq \frac{N - 1}{2})))$
68	67	adantl	$⊢ (N \in ℤ \land n \in ℤ) \to (M \in ℤ \to (2 n + 1 = N \to (M < \frac{N}{2} \leftrightarrow M \leq \frac{N - 1}{2})))$
69	68	com23	$⊢ (N \in ℤ \land n \in ℤ) \to (2 n + 1 = N \to (M \in ℤ \to (M < \frac{N}{2} \leftrightarrow M \leq \frac{N - 1}{2})))$
70	69	rexlimdva	$⊢ N \in ℤ \to (\exists n \in ℤ 2 n + 1 = N \to (M \in ℤ \to (M < \frac{N}{2} \leftrightarrow M \leq \frac{N - 1}{2})))$
71	1 70	sylbid	$⊢ N \in ℤ \to (\neg 2 ∥ N \to (M \in ℤ \to (M < \frac{N}{2} \leftrightarrow M \leq \frac{N - 1}{2})))$
72	71	3imp	$⊢ (N \in ℤ \land \neg 2 ∥ N \land M \in ℤ) \to (M < \frac{N}{2} \leftrightarrow M \leq \frac{N - 1}{2})$

Metamath Proof Explorer

Theorem ltoddhalfle

Proof