Metamath Proof Explorer

Theorem 2tceilhalfelfzo1

Description: Two times a positive integer less than (the ceiling of) half of another integer is less than the other integer. This theorem would hold even for integers less than 3, but then a corresponding K would not exist. (Contributed by AV, 9-Sep-2025)

Ref Expression
Assertion 2tceilhalfelfzo1 
|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( 2 x. K ) < N )

Proof

Step Hyp Ref Expression
1 elfzo1 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) <-> ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ K < ( |^ ` ( N / 2 ) ) ) )
2 nnz 
 |-  ( K e. NN -> K e. ZZ )
3 2 3ad2ant1 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> K e. ZZ )
4 nnz 
 |-  ( ( |^ ` ( N / 2 ) ) e. NN -> ( |^ ` ( N / 2 ) ) e. ZZ )
5 4 3ad2ant2 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( |^ ` ( N / 2 ) ) e. ZZ )
6 3 5 zltlem1d 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( K < ( |^ ` ( N / 2 ) ) <-> K <_ ( ( |^ ` ( N / 2 ) ) - 1 ) ) )
7 nnre 
 |-  ( K e. NN -> K e. RR )
8 7 3ad2ant1 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> K e. RR )
9 8 adantr 
 |-  ( ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) /\ K <_ ( ( |^ ` ( N / 2 ) ) - 1 ) ) -> K e. RR )
10 nnre 
 |-  ( ( |^ ` ( N / 2 ) ) e. NN -> ( |^ ` ( N / 2 ) ) e. RR )
11 1red 
 |-  ( ( |^ ` ( N / 2 ) ) e. NN -> 1 e. RR )
12 10 11 resubcld 
 |-  ( ( |^ ` ( N / 2 ) ) e. NN -> ( ( |^ ` ( N / 2 ) ) - 1 ) e. RR )
13 12 3ad2ant2 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( ( |^ ` ( N / 2 ) ) - 1 ) e. RR )
14 13 adantr 
 |-  ( ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) /\ K <_ ( ( |^ ` ( N / 2 ) ) - 1 ) ) -> ( ( |^ ` ( N / 2 ) ) - 1 ) e. RR )
15 eluzelre 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. RR )
16 15 rehalfcld 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N / 2 ) e. RR )
17 16 3ad2ant3 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( N / 2 ) e. RR )
18 17 adantr 
 |-  ( ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) /\ K <_ ( ( |^ ` ( N / 2 ) ) - 1 ) ) -> ( N / 2 ) e. RR )
19 simpr 
 |-  ( ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) /\ K <_ ( ( |^ ` ( N / 2 ) ) - 1 ) ) -> K <_ ( ( |^ ` ( N / 2 ) ) - 1 ) )
20 ceilm1lt 
 |-  ( ( N / 2 ) e. RR -> ( ( |^ ` ( N / 2 ) ) - 1 ) < ( N / 2 ) )
21 17 20 syl 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( ( |^ ` ( N / 2 ) ) - 1 ) < ( N / 2 ) )
22 21 adantr 
 |-  ( ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) /\ K <_ ( ( |^ ` ( N / 2 ) ) - 1 ) ) -> ( ( |^ ` ( N / 2 ) ) - 1 ) < ( N / 2 ) )
23 9 14 18 19 22 lelttrd 
 |-  ( ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) /\ K <_ ( ( |^ ` ( N / 2 ) ) - 1 ) ) -> K < ( N / 2 ) )
24 23 ex 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( K <_ ( ( |^ ` ( N / 2 ) ) - 1 ) -> K < ( N / 2 ) ) )
25 2re 
 |-  2 e. RR
26 25 a1i 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> 2 e. RR )
27 2pos 
 |-  0 < 2
28 27 a1i 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> 0 < 2 )
29 ltmul2 
 |-  ( ( K e. RR /\ ( N / 2 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( K < ( N / 2 ) <-> ( 2 x. K ) < ( 2 x. ( N / 2 ) ) ) )
30 8 17 26 28 29 syl112anc 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( K < ( N / 2 ) <-> ( 2 x. K ) < ( 2 x. ( N / 2 ) ) ) )
31 eluzelcn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. CC )
32 31 3ad2ant3 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> N e. CC )
33 2cnd 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> 2 e. CC )
34 2ne0 
 |-  2 =/= 0
35 34 a1i 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> 2 =/= 0 )
36 32 33 35 divcan2d 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( 2 x. ( N / 2 ) ) = N )
37 36 breq2d 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( ( 2 x. K ) < ( 2 x. ( N / 2 ) ) <-> ( 2 x. K ) < N ) )
38 37 biimpd 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( ( 2 x. K ) < ( 2 x. ( N / 2 ) ) -> ( 2 x. K ) < N ) )
39 30 38 sylbid 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( K < ( N / 2 ) -> ( 2 x. K ) < N ) )
40 24 39 syld 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( K <_ ( ( |^ ` ( N / 2 ) ) - 1 ) -> ( 2 x. K ) < N ) )
41 6 40 sylbid 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( K < ( |^ ` ( N / 2 ) ) -> ( 2 x. K ) < N ) )
42 41 3exp 
 |-  ( K e. NN -> ( ( |^ ` ( N / 2 ) ) e. NN -> ( N e. ( ZZ>= ` 3 ) -> ( K < ( |^ ` ( N / 2 ) ) -> ( 2 x. K ) < N ) ) ) )
43 42 com34 
 |-  ( K e. NN -> ( ( |^ ` ( N / 2 ) ) e. NN -> ( K < ( |^ ` ( N / 2 ) ) -> ( N e. ( ZZ>= ` 3 ) -> ( 2 x. K ) < N ) ) ) )
44 43 3imp 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ K < ( |^ ` ( N / 2 ) ) ) -> ( N e. ( ZZ>= ` 3 ) -> ( 2 x. K ) < N ) )
45 1 44 sylbi 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> ( N e. ( ZZ>= ` 3 ) -> ( 2 x. K ) < N ) )
46 45 impcom 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( 2 x. K ) < N )