Theorem div4p1lem1div2

Description: An integer greater than 5, divided by 4 and increased by 1, is less than or equal to the half of the integer minus 1. (Contributed by AV, 8-Jul-2021)

	Ref	Expression
Assertion	div4p1lem1div2	⊢ ( ( 𝑁 ∈ ℝ ∧ 6 ≤ 𝑁 ) → ( ( 𝑁 / 4 ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )

Proof

Step	Hyp	Ref	Expression
1		6re	⊢ 6 ∈ ℝ
2	1	a1i	⊢ ( 𝑁 ∈ ℝ → 6 ∈ ℝ )
3		id	⊢ ( 𝑁 ∈ ℝ → 𝑁 ∈ ℝ )
4	2 3 3	leadd2d	⊢ ( 𝑁 ∈ ℝ → ( 6 ≤ 𝑁 ↔ ( 𝑁 + 6 ) ≤ ( 𝑁 + 𝑁 ) ) )
5	4	biimpa	⊢ ( ( 𝑁 ∈ ℝ ∧ 6 ≤ 𝑁 ) → ( 𝑁 + 6 ) ≤ ( 𝑁 + 𝑁 ) )
6		recn	⊢ ( 𝑁 ∈ ℝ → 𝑁 ∈ ℂ )
7	6	times2d	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 · 2 ) = ( 𝑁 + 𝑁 ) )
8	7	adantr	⊢ ( ( 𝑁 ∈ ℝ ∧ 6 ≤ 𝑁 ) → ( 𝑁 · 2 ) = ( 𝑁 + 𝑁 ) )
9	5 8	breqtrrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 6 ≤ 𝑁 ) → ( 𝑁 + 6 ) ≤ ( 𝑁 · 2 ) )
10		4cn	⊢ 4 ∈ ℂ
11	10	a1i	⊢ ( 𝑁 ∈ ℝ → 4 ∈ ℂ )
12		2cn	⊢ 2 ∈ ℂ
13	12	a1i	⊢ ( 𝑁 ∈ ℝ → 2 ∈ ℂ )
14	6 11 13	addassd	⊢ ( 𝑁 ∈ ℝ → ( ( 𝑁 + 4 ) + 2 ) = ( 𝑁 + ( 4 + 2 ) ) )
15		4p2e6	⊢ ( 4 + 2 ) = 6
16	15	oveq2i	⊢ ( 𝑁 + ( 4 + 2 ) ) = ( 𝑁 + 6 )
17	14 16	eqtrdi	⊢ ( 𝑁 ∈ ℝ → ( ( 𝑁 + 4 ) + 2 ) = ( 𝑁 + 6 ) )
18	17	breq1d	⊢ ( 𝑁 ∈ ℝ → ( ( ( 𝑁 + 4 ) + 2 ) ≤ ( 𝑁 · 2 ) ↔ ( 𝑁 + 6 ) ≤ ( 𝑁 · 2 ) ) )
19	18	adantr	⊢ ( ( 𝑁 ∈ ℝ ∧ 6 ≤ 𝑁 ) → ( ( ( 𝑁 + 4 ) + 2 ) ≤ ( 𝑁 · 2 ) ↔ ( 𝑁 + 6 ) ≤ ( 𝑁 · 2 ) ) )
20	9 19	mpbird	⊢ ( ( 𝑁 ∈ ℝ ∧ 6 ≤ 𝑁 ) → ( ( 𝑁 + 4 ) + 2 ) ≤ ( 𝑁 · 2 ) )
21		4re	⊢ 4 ∈ ℝ
22	21	a1i	⊢ ( 𝑁 ∈ ℝ → 4 ∈ ℝ )
23		4ne0	⊢ 4 ≠ 0
24	23	a1i	⊢ ( 𝑁 ∈ ℝ → 4 ≠ 0 )
25	3 22 24	redivcld	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 / 4 ) ∈ ℝ )
26		peano2re	⊢ ( ( 𝑁 / 4 ) ∈ ℝ → ( ( 𝑁 / 4 ) + 1 ) ∈ ℝ )
27	25 26	syl	⊢ ( 𝑁 ∈ ℝ → ( ( 𝑁 / 4 ) + 1 ) ∈ ℝ )
28		peano2rem	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℝ )
29	28	rehalfcld	⊢ ( 𝑁 ∈ ℝ → ( ( 𝑁 − 1 ) / 2 ) ∈ ℝ )
30		4pos	⊢ 0 < 4
31	21 30	pm3.2i	⊢ ( 4 ∈ ℝ ∧ 0 < 4 )
32	31	a1i	⊢ ( 𝑁 ∈ ℝ → ( 4 ∈ ℝ ∧ 0 < 4 ) )
33		lemul1	⊢ ( ( ( ( 𝑁 / 4 ) + 1 ) ∈ ℝ ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℝ ∧ ( 4 ∈ ℝ ∧ 0 < 4 ) ) → ( ( ( 𝑁 / 4 ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ↔ ( ( ( 𝑁 / 4 ) + 1 ) · 4 ) ≤ ( ( ( 𝑁 − 1 ) / 2 ) · 4 ) ) )
34	27 29 32 33	syl3anc	⊢ ( 𝑁 ∈ ℝ → ( ( ( 𝑁 / 4 ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ↔ ( ( ( 𝑁 / 4 ) + 1 ) · 4 ) ≤ ( ( ( 𝑁 − 1 ) / 2 ) · 4 ) ) )
35	25	recnd	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 / 4 ) ∈ ℂ )
36		1cnd	⊢ ( 𝑁 ∈ ℝ → 1 ∈ ℂ )
37	6 11 24	divcan1d	⊢ ( 𝑁 ∈ ℝ → ( ( 𝑁 / 4 ) · 4 ) = 𝑁 )
38	10	mullidi	⊢ ( 1 · 4 ) = 4
39	38	a1i	⊢ ( 𝑁 ∈ ℝ → ( 1 · 4 ) = 4 )
40	37 39	oveq12d	⊢ ( 𝑁 ∈ ℝ → ( ( ( 𝑁 / 4 ) · 4 ) + ( 1 · 4 ) ) = ( 𝑁 + 4 ) )
41	35 11 36 40	joinlmuladdmuld	⊢ ( 𝑁 ∈ ℝ → ( ( ( 𝑁 / 4 ) + 1 ) · 4 ) = ( 𝑁 + 4 ) )
42		2t2e4	⊢ ( 2 · 2 ) = 4
43	42	eqcomi	⊢ 4 = ( 2 · 2 )
44	43	a1i	⊢ ( 𝑁 ∈ ℝ → 4 = ( 2 · 2 ) )
45	44	oveq2d	⊢ ( 𝑁 ∈ ℝ → ( ( ( 𝑁 − 1 ) / 2 ) · 4 ) = ( ( ( 𝑁 − 1 ) / 2 ) · ( 2 · 2 ) ) )
46	29	recnd	⊢ ( 𝑁 ∈ ℝ → ( ( 𝑁 − 1 ) / 2 ) ∈ ℂ )
47		mulass	⊢ ( ( ( ( 𝑁 − 1 ) / 2 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( ( ( 𝑁 − 1 ) / 2 ) · 2 ) · 2 ) = ( ( ( 𝑁 − 1 ) / 2 ) · ( 2 · 2 ) ) )
48	47	eqcomd	⊢ ( ( ( ( 𝑁 − 1 ) / 2 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( ( 𝑁 − 1 ) / 2 ) · ( 2 · 2 ) ) = ( ( ( ( 𝑁 − 1 ) / 2 ) · 2 ) · 2 ) )
49	46 13 13 48	syl3anc	⊢ ( 𝑁 ∈ ℝ → ( ( ( 𝑁 − 1 ) / 2 ) · ( 2 · 2 ) ) = ( ( ( ( 𝑁 − 1 ) / 2 ) · 2 ) · 2 ) )
50	28	recnd	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℂ )
51		2ne0	⊢ 2 ≠ 0
52	51	a1i	⊢ ( 𝑁 ∈ ℝ → 2 ≠ 0 )
53	50 13 52	divcan1d	⊢ ( 𝑁 ∈ ℝ → ( ( ( 𝑁 − 1 ) / 2 ) · 2 ) = ( 𝑁 − 1 ) )
54	53	oveq1d	⊢ ( 𝑁 ∈ ℝ → ( ( ( ( 𝑁 − 1 ) / 2 ) · 2 ) · 2 ) = ( ( 𝑁 − 1 ) · 2 ) )
55	6 36 13	subdird	⊢ ( 𝑁 ∈ ℝ → ( ( 𝑁 − 1 ) · 2 ) = ( ( 𝑁 · 2 ) − ( 1 · 2 ) ) )
56	12	mullidi	⊢ ( 1 · 2 ) = 2
57	56	a1i	⊢ ( 𝑁 ∈ ℝ → ( 1 · 2 ) = 2 )
58	57	oveq2d	⊢ ( 𝑁 ∈ ℝ → ( ( 𝑁 · 2 ) − ( 1 · 2 ) ) = ( ( 𝑁 · 2 ) − 2 ) )
59	54 55 58	3eqtrd	⊢ ( 𝑁 ∈ ℝ → ( ( ( ( 𝑁 − 1 ) / 2 ) · 2 ) · 2 ) = ( ( 𝑁 · 2 ) − 2 ) )
60	45 49 59	3eqtrd	⊢ ( 𝑁 ∈ ℝ → ( ( ( 𝑁 − 1 ) / 2 ) · 4 ) = ( ( 𝑁 · 2 ) − 2 ) )
61	41 60	breq12d	⊢ ( 𝑁 ∈ ℝ → ( ( ( ( 𝑁 / 4 ) + 1 ) · 4 ) ≤ ( ( ( 𝑁 − 1 ) / 2 ) · 4 ) ↔ ( 𝑁 + 4 ) ≤ ( ( 𝑁 · 2 ) − 2 ) ) )
62	3 22	readdcld	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 + 4 ) ∈ ℝ )
63		2re	⊢ 2 ∈ ℝ
64	63	a1i	⊢ ( 𝑁 ∈ ℝ → 2 ∈ ℝ )
65	3 64	remulcld	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 · 2 ) ∈ ℝ )
66		leaddsub	⊢ ( ( ( 𝑁 + 4 ) ∈ ℝ ∧ 2 ∈ ℝ ∧ ( 𝑁 · 2 ) ∈ ℝ ) → ( ( ( 𝑁 + 4 ) + 2 ) ≤ ( 𝑁 · 2 ) ↔ ( 𝑁 + 4 ) ≤ ( ( 𝑁 · 2 ) − 2 ) ) )
67	66	bicomd	⊢ ( ( ( 𝑁 + 4 ) ∈ ℝ ∧ 2 ∈ ℝ ∧ ( 𝑁 · 2 ) ∈ ℝ ) → ( ( 𝑁 + 4 ) ≤ ( ( 𝑁 · 2 ) − 2 ) ↔ ( ( 𝑁 + 4 ) + 2 ) ≤ ( 𝑁 · 2 ) ) )
68	62 64 65 67	syl3anc	⊢ ( 𝑁 ∈ ℝ → ( ( 𝑁 + 4 ) ≤ ( ( 𝑁 · 2 ) − 2 ) ↔ ( ( 𝑁 + 4 ) + 2 ) ≤ ( 𝑁 · 2 ) ) )
69	34 61 68	3bitrd	⊢ ( 𝑁 ∈ ℝ → ( ( ( 𝑁 / 4 ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ↔ ( ( 𝑁 + 4 ) + 2 ) ≤ ( 𝑁 · 2 ) ) )
70	69	adantr	⊢ ( ( 𝑁 ∈ ℝ ∧ 6 ≤ 𝑁 ) → ( ( ( 𝑁 / 4 ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ↔ ( ( 𝑁 + 4 ) + 2 ) ≤ ( 𝑁 · 2 ) ) )
71	20 70	mpbird	⊢ ( ( 𝑁 ∈ ℝ ∧ 6 ≤ 𝑁 ) → ( ( 𝑁 / 4 ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )