Metamath Proof Explorer


Theorem fldiv4lem1div2uz2

Description: The floor of an integer greater than 1, divided by 4 is less than or equal to the half of the integer minus 1. (Contributed by AV, 5-Jul-2021) (Proof shortened by AV, 9-Jul-2022)

Ref Expression
Assertion fldiv4lem1div2uz2 ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( ( 𝑁 − 1 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 eluzelz ( 𝑁 ∈ ( ℤ ‘ 2 ) → 𝑁 ∈ ℤ )
2 zre ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
3 id ( 𝑁 ∈ ℝ → 𝑁 ∈ ℝ )
4 4re 4 ∈ ℝ
5 4 a1i ( 𝑁 ∈ ℝ → 4 ∈ ℝ )
6 4ne0 4 ≠ 0
7 6 a1i ( 𝑁 ∈ ℝ → 4 ≠ 0 )
8 3 5 7 redivcld ( 𝑁 ∈ ℝ → ( 𝑁 / 4 ) ∈ ℝ )
9 flle ( ( 𝑁 / 4 ) ∈ ℝ → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( 𝑁 / 4 ) )
10 1 2 8 9 4syl ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( 𝑁 / 4 ) )
11 1red ( 𝑁 ∈ ( ℤ ‘ 2 ) → 1 ∈ ℝ )
12 eluzelre ( 𝑁 ∈ ( ℤ ‘ 2 ) → 𝑁 ∈ ℝ )
13 rehalfcl ( 𝑁 ∈ ℝ → ( 𝑁 / 2 ) ∈ ℝ )
14 1 2 13 3syl ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 / 2 ) ∈ ℝ )
15 2rp 2 ∈ ℝ+
16 15 a1i ( 𝑁 ∈ ( ℤ ‘ 2 ) → 2 ∈ ℝ+ )
17 eluzle ( 𝑁 ∈ ( ℤ ‘ 2 ) → 2 ≤ 𝑁 )
18 divge1 ( ( 2 ∈ ℝ+𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → 1 ≤ ( 𝑁 / 2 ) )
19 16 12 17 18 syl3anc ( 𝑁 ∈ ( ℤ ‘ 2 ) → 1 ≤ ( 𝑁 / 2 ) )
20 eluzelcn ( 𝑁 ∈ ( ℤ ‘ 2 ) → 𝑁 ∈ ℂ )
21 subhalfhalf ( 𝑁 ∈ ℂ → ( 𝑁 − ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) )
22 20 21 syl ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 − ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) )
23 19 22 breqtrrd ( 𝑁 ∈ ( ℤ ‘ 2 ) → 1 ≤ ( 𝑁 − ( 𝑁 / 2 ) ) )
24 11 12 14 23 lesubd ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 / 2 ) ≤ ( 𝑁 − 1 ) )
25 2t2e4 ( 2 · 2 ) = 4
26 25 eqcomi 4 = ( 2 · 2 )
27 26 a1i ( 𝑁 ∈ ( ℤ ‘ 2 ) → 4 = ( 2 · 2 ) )
28 27 oveq2d ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 / 4 ) = ( 𝑁 / ( 2 · 2 ) ) )
29 2cnne0 ( 2 ∈ ℂ ∧ 2 ≠ 0 )
30 29 a1i ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
31 divdiv1 ( ( 𝑁 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 𝑁 / 2 ) / 2 ) = ( 𝑁 / ( 2 · 2 ) ) )
32 20 30 30 31 syl3anc ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( ( 𝑁 / 2 ) / 2 ) = ( 𝑁 / ( 2 · 2 ) ) )
33 28 32 eqtr4d ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 / 4 ) = ( ( 𝑁 / 2 ) / 2 ) )
34 33 breq1d ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( ( 𝑁 / 4 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ↔ ( ( 𝑁 / 2 ) / 2 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ) )
35 peano2rem ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℝ )
36 12 35 syl ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 − 1 ) ∈ ℝ )
37 14 36 16 lediv1d ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( ( 𝑁 / 2 ) ≤ ( 𝑁 − 1 ) ↔ ( ( 𝑁 / 2 ) / 2 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ) )
38 34 37 bitr4d ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( ( 𝑁 / 4 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ↔ ( 𝑁 / 2 ) ≤ ( 𝑁 − 1 ) ) )
39 24 38 mpbird ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 / 4 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
40 8 flcld ( 𝑁 ∈ ℝ → ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℤ )
41 40 zred ( 𝑁 ∈ ℝ → ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℝ )
42 35 rehalfcld ( 𝑁 ∈ ℝ → ( ( 𝑁 − 1 ) / 2 ) ∈ ℝ )
43 41 8 42 3jca ( 𝑁 ∈ ℝ → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℝ ∧ ( 𝑁 / 4 ) ∈ ℝ ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℝ ) )
44 letr ( ( ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℝ ∧ ( 𝑁 / 4 ) ∈ ℝ ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℝ ) → ( ( ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( 𝑁 / 4 ) ∧ ( 𝑁 / 4 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( ( 𝑁 − 1 ) / 2 ) ) )
45 1 2 43 44 4syl ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( ( ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( 𝑁 / 4 ) ∧ ( 𝑁 / 4 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( ( 𝑁 − 1 ) / 2 ) ) )
46 10 39 45 mp2and ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( ( 𝑁 − 1 ) / 2 ) )