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

Metamath Proof Explorer

Theorem flodddiv4t2lthalf

Description: The floor of an odd number divided by 4, multiplied by 2 is less than the half of the odd number. (Contributed by AV, 4-Jul-2021) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Assertion flodddiv4t2lthalf ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) · 2 ) < ( 𝑁 / 2 ) )

Proof

Step Hyp Ref Expression
1 flodddiv4lt ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) < ( 𝑁 / 4 ) )
2 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
3 4re ⊢ 4 ∈ ℝ
4 3 a1i ⊢ ( 𝑁 ∈ ℤ → 4 ∈ ℝ )
5 4ne0 ⊢ 4 ≠ 0
6 5 a1i ⊢ ( 𝑁 ∈ ℤ → 4 ≠ 0 )
7 2 4 6 redivcld ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 / 4 ) ∈ ℝ )
8 7 flcld ⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℤ )
9 8 zred ⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℝ )
10 2rp ⊢ 2 ∈ ℝ+
11 10 a1i ⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℝ+ )
12 9 7 11 ltmul1d ⊢ ( 𝑁 ∈ ℤ → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) < ( 𝑁 / 4 ) ↔ ( ( ⌊ ‘ ( 𝑁 / 4 ) ) · 2 ) < ( ( 𝑁 / 4 ) · 2 ) ) )
13 12 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) < ( 𝑁 / 4 ) ↔ ( ( ⌊ ‘ ( 𝑁 / 4 ) ) · 2 ) < ( ( 𝑁 / 4 ) · 2 ) ) )
14 1 13 mpbid ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) · 2 ) < ( ( 𝑁 / 4 ) · 2 ) )
15 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
16 15 halfcld ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 / 2 ) ∈ ℂ )
17 2cnd ⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℂ )
18 2ne0 ⊢ 2 ≠ 0
19 18 a1i ⊢ ( 𝑁 ∈ ℤ → 2 ≠ 0 )
20 16 17 19 divcan1d ⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑁 / 2 ) / 2 ) · 2 ) = ( 𝑁 / 2 ) )
21 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
22 21 a1i ⊢ ( 𝑁 ∈ ℤ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
23 divdiv1 ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 𝑁 / 2 ) / 2 ) = ( 𝑁 / ( 2 · 2 ) ) )
24 15 22 22 23 syl3anc ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 / 2 ) / 2 ) = ( 𝑁 / ( 2 · 2 ) ) )
25 2t2e4 ⊢ ( 2 · 2 ) = 4
26 25 a1i ⊢ ( 𝑁 ∈ ℤ → ( 2 · 2 ) = 4 )
27 26 oveq2d ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 / ( 2 · 2 ) ) = ( 𝑁 / 4 ) )
28 24 27 eqtrd ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 / 2 ) / 2 ) = ( 𝑁 / 4 ) )
29 28 oveq1d ⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑁 / 2 ) / 2 ) · 2 ) = ( ( 𝑁 / 4 ) · 2 ) )
30 20 29 eqtr3d ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 / 2 ) = ( ( 𝑁 / 4 ) · 2 ) )
31 30 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑁 / 2 ) = ( ( 𝑁 / 4 ) · 2 ) )
32 14 31 breqtrrd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) · 2 ) < ( 𝑁 / 2 ) )