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

Metamath Proof Explorer

Theorem fldiv4lem1div2

Description: The floor of a positive integer divided by 4 is less than or equal to the half of the integer minus 1. (Contributed by AV, 9-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 elnn1uz2 ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) )
2 1lt4 ⊢ 1 < 4
3 1nn0 ⊢ 1 ∈ ℕ0
4 4nn ⊢ 4 ∈ ℕ
5 divfl0 ⊢ ( ( 1 ∈ ℕ0 ∧ 4 ∈ ℕ ) → ( 1 < 4 ↔ ( ⌊ ‘ ( 1 / 4 ) ) = 0 ) )
6 3 4 5 mp2an ⊢ ( 1 < 4 ↔ ( ⌊ ‘ ( 1 / 4 ) ) = 0 )
7 2 6 mpbi ⊢ ( ⌊ ‘ ( 1 / 4 ) ) = 0
8 1re ⊢ 1 ∈ ℝ
9 4re ⊢ 4 ∈ ℝ
10 4ne0 ⊢ 4 ≠ 0
11 redivcl ⊢ ( ( 1 ∈ ℝ ∧ 4 ∈ ℝ ∧ 4 ≠ 0 ) → ( 1 / 4 ) ∈ ℝ )
12 11 flcld ⊢ ( ( 1 ∈ ℝ ∧ 4 ∈ ℝ ∧ 4 ≠ 0 ) → ( ⌊ ‘ ( 1 / 4 ) ) ∈ ℤ )
13 12 zred ⊢ ( ( 1 ∈ ℝ ∧ 4 ∈ ℝ ∧ 4 ≠ 0 ) → ( ⌊ ‘ ( 1 / 4 ) ) ∈ ℝ )
14 8 9 10 13 mp3an ⊢ ( ⌊ ‘ ( 1 / 4 ) ) ∈ ℝ
15 14 eqlei ⊢ ( ( ⌊ ‘ ( 1 / 4 ) ) = 0 → ( ⌊ ‘ ( 1 / 4 ) ) ≤ 0 )
16 7 15 mp1i ⊢ ( 𝑁 = 1 → ( ⌊ ‘ ( 1 / 4 ) ) ≤ 0 )
17 fvoveq1 ⊢ ( 𝑁 = 1 → ( ⌊ ‘ ( 𝑁 / 4 ) ) = ( ⌊ ‘ ( 1 / 4 ) ) )
18 oveq1 ⊢ ( 𝑁 = 1 → ( 𝑁 − 1 ) = ( 1 − 1 ) )
19 1m1e0 ⊢ ( 1 − 1 ) = 0
20 18 19 eqtrdi ⊢ ( 𝑁 = 1 → ( 𝑁 − 1 ) = 0 )
21 20 oveq1d ⊢ ( 𝑁 = 1 → ( ( 𝑁 − 1 ) / 2 ) = ( 0 / 2 ) )
22 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
23 div0 ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 0 / 2 ) = 0 )
24 22 23 ax-mp ⊢ ( 0 / 2 ) = 0
25 21 24 eqtrdi ⊢ ( 𝑁 = 1 → ( ( 𝑁 − 1 ) / 2 ) = 0 )
26 16 17 25 3brtr4d ⊢ ( 𝑁 = 1 → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
27 fldiv4lem1div2uz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
28 26 27 jaoi ⊢ ( ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
29 1 28 sylbi ⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( ( 𝑁 − 1 ) / 2 ) )