Theorem 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	⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑀 ∈ ℤ ) → ( ( 𝑁 / 2 ) ≤ 𝑀 ↔ ( 𝑁 / 2 ) < 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		odd2np1	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
2		0xr	⊢ 0 ∈ ℝ*
3		1xr	⊢ 1 ∈ ℝ*
4		halfre	⊢ ( 1 / 2 ) ∈ ℝ
5	4	rexri	⊢ ( 1 / 2 ) ∈ ℝ*
6	2 3 5	3pm3.2i	⊢ ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ ( 1 / 2 ) ∈ ℝ* )
7		halfgt0	⊢ 0 < ( 1 / 2 )
8		halflt1	⊢ ( 1 / 2 ) < 1
9	7 8	pm3.2i	⊢ ( 0 < ( 1 / 2 ) ∧ ( 1 / 2 ) < 1 )
10		elioo3g	⊢ ( ( 1 / 2 ) ∈ ( 0 (,) 1 ) ↔ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ ( 1 / 2 ) ∈ ℝ* ) ∧ ( 0 < ( 1 / 2 ) ∧ ( 1 / 2 ) < 1 ) ) )
11	6 9 10	mpbir2an	⊢ ( 1 / 2 ) ∈ ( 0 (,) 1 )
12		zltaddlt1le	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 1 / 2 ) ∈ ( 0 (,) 1 ) ) → ( ( 𝑛 + ( 1 / 2 ) ) < 𝑀 ↔ ( 𝑛 + ( 1 / 2 ) ) ≤ 𝑀 ) )
13	11 12	mp3an3	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑛 + ( 1 / 2 ) ) < 𝑀 ↔ ( 𝑛 + ( 1 / 2 ) ) ≤ 𝑀 ) )
14		zcn	⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
15	14	adantr	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → 𝑛 ∈ ℂ )
16		1cnd	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → 1 ∈ ℂ )
17		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
18	17	a1i	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
19		muldivdir	⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) = ( 𝑛 + ( 1 / 2 ) ) )
20	15 16 18 19	syl3anc	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) = ( 𝑛 + ( 1 / 2 ) ) )
21	20	breq1d	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) < 𝑀 ↔ ( 𝑛 + ( 1 / 2 ) ) < 𝑀 ) )
22	20	breq1d	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) ≤ 𝑀 ↔ ( 𝑛 + ( 1 / 2 ) ) ≤ 𝑀 ) )
23	13 21 22	3bitr4rd	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) ≤ 𝑀 ↔ ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) < 𝑀 ) )
24		oveq1	⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) = ( 𝑁 / 2 ) )
25	24	breq1d	⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) ≤ 𝑀 ↔ ( 𝑁 / 2 ) ≤ 𝑀 ) )
26	24	breq1d	⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) < 𝑀 ↔ ( 𝑁 / 2 ) < 𝑀 ) )
27	25 26	bibi12d	⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( ( ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) ≤ 𝑀 ↔ ( ( ( 2 · 𝑛 ) + 1 ) / 2 ) < 𝑀 ) ↔ ( ( 𝑁 / 2 ) ≤ 𝑀 ↔ ( 𝑁 / 2 ) < 𝑀 ) ) )
28	23 27	syl5ibcom	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( ( 𝑁 / 2 ) ≤ 𝑀 ↔ ( 𝑁 / 2 ) < 𝑀 ) ) )
29	28	ex	⊢ ( 𝑛 ∈ ℤ → ( 𝑀 ∈ ℤ → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( ( 𝑁 / 2 ) ≤ 𝑀 ↔ ( 𝑁 / 2 ) < 𝑀 ) ) ) )
30	29	adantl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑀 ∈ ℤ → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( ( 𝑁 / 2 ) ≤ 𝑀 ↔ ( 𝑁 / 2 ) < 𝑀 ) ) ) )
31	30	com23	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( 𝑀 ∈ ℤ → ( ( 𝑁 / 2 ) ≤ 𝑀 ↔ ( 𝑁 / 2 ) < 𝑀 ) ) ) )
32	31	rexlimdva	⊢ ( 𝑁 ∈ ℤ → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( 𝑀 ∈ ℤ → ( ( 𝑁 / 2 ) ≤ 𝑀 ↔ ( 𝑁 / 2 ) < 𝑀 ) ) ) )
33	1 32	sylbid	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 → ( 𝑀 ∈ ℤ → ( ( 𝑁 / 2 ) ≤ 𝑀 ↔ ( 𝑁 / 2 ) < 𝑀 ) ) ) )
34	33	3imp	⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑀 ∈ ℤ ) → ( ( 𝑁 / 2 ) ≤ 𝑀 ↔ ( 𝑁 / 2 ) < 𝑀 ) )