Metamath Proof Explorer

Theorem flnn0div2ge

Description: The floor of a positive integer divided by 2 is greater than or equal to the integer decreased by 1 and then divided by 2. (Contributed by AV, 1-Jun-2020)

Ref Expression
Assertion flnn0div2ge ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) / 2 ) ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) )

Proof

Step Hyp Ref Expression
1 nn0eo ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 / 2 ) ∈ ℕ0 ∨ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) )
2 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
3 peano2rem ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℝ )
4 2 3 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 − 1 ) ∈ ℝ )
5 4 adantl ⊢ ( ( ( 𝑁 / 2 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 − 1 ) ∈ ℝ )
6 2 adantl ⊢ ( ( ( 𝑁 / 2 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
7 2rp ⊢ 2 ∈ ℝ+
8 7 a1i ⊢ ( ( ( 𝑁 / 2 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 2 ∈ ℝ+ )
9 2 lem1d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 − 1 ) ≤ 𝑁 )
10 9 adantl ⊢ ( ( ( 𝑁 / 2 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 − 1 ) ≤ 𝑁 )
11 5 6 8 10 lediv1dd ⊢ ( ( ( 𝑁 / 2 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ≤ ( 𝑁 / 2 ) )
12 nn0z ⊢ ( ( 𝑁 / 2 ) ∈ ℕ0 → ( 𝑁 / 2 ) ∈ ℤ )
13 flid ⊢ ( ( 𝑁 / 2 ) ∈ ℤ → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) )
14 12 13 syl ⊢ ( ( 𝑁 / 2 ) ∈ ℕ0 → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) )
15 14 adantr ⊢ ( ( ( 𝑁 / 2 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) )
16 11 15 breqtrrd ⊢ ( ( ( 𝑁 / 2 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) )
17 16 ex ⊢ ( ( 𝑁 / 2 ) ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) / 2 ) ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
18 nn0o ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 )
19 18 ex ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) )
20 nn0z ⊢ ( ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 → ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ )
21 20 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ )
22 flid ⊢ ( ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ → ( ⌊ ‘ ( ( 𝑁 − 1 ) / 2 ) ) = ( ( 𝑁 − 1 ) / 2 ) )
23 21 22 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) → ( ⌊ ‘ ( ( 𝑁 − 1 ) / 2 ) ) = ( ( 𝑁 − 1 ) / 2 ) )
24 4 rehalfcld ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) / 2 ) ∈ ℝ )
25 24 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℝ )
26 2 rehalfcld ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 / 2 ) ∈ ℝ )
27 26 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑁 / 2 ) ∈ ℝ )
28 2re ⊢ 2 ∈ ℝ
29 2pos ⊢ 0 < 2
30 28 29 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
31 30 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ∈ ℝ ∧ 0 < 2 ) )
32 lediv1 ⊢ ( ( ( 𝑁 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 𝑁 − 1 ) ≤ 𝑁 ↔ ( ( 𝑁 − 1 ) / 2 ) ≤ ( 𝑁 / 2 ) ) )
33 4 2 31 32 syl3anc ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) ≤ 𝑁 ↔ ( ( 𝑁 − 1 ) / 2 ) ≤ ( 𝑁 / 2 ) ) )
34 9 33 mpbid ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) / 2 ) ≤ ( 𝑁 / 2 ) )
35 34 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ≤ ( 𝑁 / 2 ) )
36 flwordi ⊢ ( ( ( ( 𝑁 − 1 ) / 2 ) ∈ ℝ ∧ ( 𝑁 / 2 ) ∈ ℝ ∧ ( ( 𝑁 − 1 ) / 2 ) ≤ ( 𝑁 / 2 ) ) → ( ⌊ ‘ ( ( 𝑁 − 1 ) / 2 ) ) ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) )
37 25 27 35 36 syl3anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) → ( ⌊ ‘ ( ( 𝑁 − 1 ) / 2 ) ) ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) )
38 23 37 eqbrtrrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) )
39 38 ex ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 → ( ( 𝑁 − 1 ) / 2 ) ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
40 19 39 syldc ⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) / 2 ) ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
41 17 40 jaoi ⊢ ( ( ( 𝑁 / 2 ) ∈ ℕ0 ∨ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) / 2 ) ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
42 1 41 mpcom ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) / 2 ) ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) )