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