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 ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N → N 4 ⋅ 2 < N 2

Proof

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