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

Metamath Proof Explorer

Theorem ge2halflem1

Description: Half of an integer greater than 1 is less than or equal to the integer minus 1. (Contributed by AV, 1-Sep-2025)

Ref Expression
Assertion ge2halflem1 ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 / 2 ) ≤ ( 𝑁 − 1 ) )

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 1 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℝ )
3 eluzelre ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℝ )
4 2 3 remulcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · 𝑁 ) ∈ ℝ )
5 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝑁 )
6 2m1e1 ⊢ ( 2 − 1 ) = 1
7 6 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 − 1 ) = 1 )
8 7 oveq1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 − 1 ) · 𝑁 ) = ( 1 · 𝑁 ) )
9 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℂ )
10 9 mullidd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 1 · 𝑁 ) = 𝑁 )
11 8 10 eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 − 1 ) · 𝑁 ) = 𝑁 )
12 5 11 breqtrrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ ( ( 2 − 1 ) · 𝑁 ) )
13 2cnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℂ )
14 13 9 mulsubfacd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 · 𝑁 ) − 𝑁 ) = ( ( 2 − 1 ) · 𝑁 ) )
15 12 14 breqtrrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ ( ( 2 · 𝑁 ) − 𝑁 ) )
16 2 4 3 15 lesubd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ≤ ( ( 2 · 𝑁 ) − 2 ) )
17 13 9 muls1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( 𝑁 − 1 ) ) = ( ( 2 · 𝑁 ) − 2 ) )
18 16 17 breqtrrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ≤ ( 2 · ( 𝑁 − 1 ) ) )
19 1red ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℝ )
20 3 19 resubcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 1 ) ∈ ℝ )
21 2rp ⊢ 2 ∈ ℝ+
22 21 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℝ+ )
23 3 20 22 ledivmuld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 / 2 ) ≤ ( 𝑁 − 1 ) ↔ 𝑁 ≤ ( 2 · ( 𝑁 − 1 ) ) ) )
24 18 23 mpbird ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 / 2 ) ≤ ( 𝑁 − 1 ) )