This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) < 𝑀 ) )