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 
|- ( N e. ( ZZ>= ` 2 ) -> ( N / 2 ) <_ ( N - 1 ) )

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 1 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. RR )
3 eluzelre 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. RR )
4 2 3 remulcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 x. N ) e. RR )
5 eluzle 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 <_ N )
6 2m1e1 
 |-  ( 2 - 1 ) = 1
7 6 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 - 1 ) = 1 )
8 7 oveq1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 2 - 1 ) x. N ) = ( 1 x. N ) )
9 eluzelcn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. CC )
10 9 mullidd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 x. N ) = N )
11 8 10 eqtrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 2 - 1 ) x. N ) = N )
12 5 11 breqtrrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 <_ ( ( 2 - 1 ) x. N ) )
13 2cnd 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. CC )
14 13 9 mulsubfacd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 2 x. N ) - N ) = ( ( 2 - 1 ) x. N ) )
15 12 14 breqtrrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 <_ ( ( 2 x. N ) - N ) )
16 2 4 3 15 lesubd 
 |-  ( N e. ( ZZ>= ` 2 ) -> N <_ ( ( 2 x. N ) - 2 ) )
17 13 9 muls1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 x. ( N - 1 ) ) = ( ( 2 x. N ) - 2 ) )
18 16 17 breqtrrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> N <_ ( 2 x. ( N - 1 ) ) )
19 1red 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 e. RR )
20 3 19 resubcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. RR )
21 2rp 
 |-  2 e. RR+
22 21 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. RR+ )
23 3 20 22 ledivmuld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N / 2 ) <_ ( N - 1 ) <-> N <_ ( 2 x. ( N - 1 ) ) ) )
24 18 23 mpbird 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N / 2 ) <_ ( N - 1 ) )