This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )