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