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 ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 2 · 𝐾 ) < 𝑁 )

Proof

Step Hyp Ref Expression
1 elfzo1 ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ↔ ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝐾 < ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
2 nnz ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℤ )
3 2 3ad2ant1 ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝐾 ∈ ℤ )
4 nnz ⊢ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
5 4 3ad2ant2 ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
6 3 5 zltlem1d ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝐾 < ( ⌈ ‘ ( 𝑁 / 2 ) ) ↔ 𝐾 ≤ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) − 1 ) ) )
7 nnre ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℝ )
8 7 3ad2ant1 ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝐾 ∈ ℝ )
9 8 adantr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ 𝐾 ≤ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) − 1 ) ) → 𝐾 ∈ ℝ )
10 nnre ⊢ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℝ )
11 1red ⊢ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ → 1 ∈ ℝ )
12 10 11 resubcld ⊢ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ → ( ( ⌈ ‘ ( 𝑁 / 2 ) ) − 1 ) ∈ ℝ )
13 12 3ad2ant2 ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ⌈ ‘ ( 𝑁 / 2 ) ) − 1 ) ∈ ℝ )
14 13 adantr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ 𝐾 ≤ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) − 1 ) ) → ( ( ⌈ ‘ ( 𝑁 / 2 ) ) − 1 ) ∈ ℝ )
15 eluzelre ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℝ )
16 15 rehalfcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 / 2 ) ∈ ℝ )
17 16 3ad2ant3 ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑁 / 2 ) ∈ ℝ )
18 17 adantr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ 𝐾 ≤ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) − 1 ) ) → ( 𝑁 / 2 ) ∈ ℝ )
19 simpr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ 𝐾 ≤ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) − 1 ) ) → 𝐾 ≤ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) − 1 ) )
20 ceilm1lt ⊢ ( ( 𝑁 / 2 ) ∈ ℝ → ( ( ⌈ ‘ ( 𝑁 / 2 ) ) − 1 ) < ( 𝑁 / 2 ) )
21 17 20 syl ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ⌈ ‘ ( 𝑁 / 2 ) ) − 1 ) < ( 𝑁 / 2 ) )
22 21 adantr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ 𝐾 ≤ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) − 1 ) ) → ( ( ⌈ ‘ ( 𝑁 / 2 ) ) − 1 ) < ( 𝑁 / 2 ) )
23 9 14 18 19 22 lelttrd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ 𝐾 ≤ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) − 1 ) ) → 𝐾 < ( 𝑁 / 2 ) )
24 23 ex ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝐾 ≤ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) − 1 ) → 𝐾 < ( 𝑁 / 2 ) ) )
25 2re ⊢ 2 ∈ ℝ
26 25 a1i ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 2 ∈ ℝ )
27 2pos ⊢ 0 < 2
28 27 a1i ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 0 < 2 )
29 ltmul2 ⊢ ( ( 𝐾 ∈ ℝ ∧ ( 𝑁 / 2 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 𝐾 < ( 𝑁 / 2 ) ↔ ( 2 · 𝐾 ) < ( 2 · ( 𝑁 / 2 ) ) ) )
30 8 17 26 28 29 syl112anc ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝐾 < ( 𝑁 / 2 ) ↔ ( 2 · 𝐾 ) < ( 2 · ( 𝑁 / 2 ) ) ) )
31 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℂ )
32 31 3ad2ant3 ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑁 ∈ ℂ )
33 2cnd ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 2 ∈ ℂ )
34 2ne0 ⊢ 2 ≠ 0
35 34 a1i ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 2 ≠ 0 )
36 32 33 35 divcan2d ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 2 · ( 𝑁 / 2 ) ) = 𝑁 )
37 36 breq2d ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 2 · 𝐾 ) < ( 2 · ( 𝑁 / 2 ) ) ↔ ( 2 · 𝐾 ) < 𝑁 ) )
38 37 biimpd ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 2 · 𝐾 ) < ( 2 · ( 𝑁 / 2 ) ) → ( 2 · 𝐾 ) < 𝑁 ) )
39 30 38 sylbid ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝐾 < ( 𝑁 / 2 ) → ( 2 · 𝐾 ) < 𝑁 ) )
40 24 39 syld ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝐾 ≤ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) − 1 ) → ( 2 · 𝐾 ) < 𝑁 ) )
41 6 40 sylbid ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝐾 < ( ⌈ ‘ ( 𝑁 / 2 ) ) → ( 2 · 𝐾 ) < 𝑁 ) )
42 41 3exp ⊢ ( 𝐾 ∈ ℕ → ( ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝐾 < ( ⌈ ‘ ( 𝑁 / 2 ) ) → ( 2 · 𝐾 ) < 𝑁 ) ) ) )
43 42 com34 ⊢ ( 𝐾 ∈ ℕ → ( ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ → ( 𝐾 < ( ⌈ ‘ ( 𝑁 / 2 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 2 · 𝐾 ) < 𝑁 ) ) ) )
44 43 3imp ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝐾 < ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 2 · 𝐾 ) < 𝑁 ) )
45 1 44 sylbi ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 2 · 𝐾 ) < 𝑁 ) )
46 45 impcom ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 2 · 𝐾 ) < 𝑁 )