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