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→N4⋅2<N2

Proof

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