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	$$⊢\left(N\in ℝ\wedge 6\le N\right)\to \left(\frac{N}{4}\right)+1\le \frac{N-1}{2}$$

Proof

Step	Hyp	Ref	Expression
1		6re	$$⊢6\in ℝ$$
2	1	a1i	$$⊢N\in ℝ\to 6\in ℝ$$
3		id	$$⊢N\in ℝ\to N\in ℝ$$
4	2 3 3	leadd2d	$$⊢N\in ℝ\to \left(6\le N\leftrightarrow N+6\le N+N\right)$$
5	4	biimpa	$$⊢\left(N\in ℝ\wedge 6\le N\right)\to N+6\le N+N$$
6		recn	$$⊢N\in ℝ\to N\in ℂ$$
7	6	times2d	$$⊢N\in ℝ\to \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2=N+N$$
8	7	adantr	$$⊢\left(N\in ℝ\wedge 6\le N\right)\to \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2=N+N$$
9	5 8	breqtrrd	$$⊢\left(N\in ℝ\wedge 6\le N\right)\to N+6\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2$$
10		4cn	$$⊢4\in ℂ$$
11	10	a1i	$$⊢N\in ℝ\to 4\in ℂ$$
12		2cn	$$⊢2\in ℂ$$
13	12	a1i	$$⊢N\in ℝ\to 2\in ℂ$$
14	6 11 13	addassd	$$⊢N\in ℝ\to N+4+2=N+4+2$$
15		4p2e6	$$⊢4+2=6$$
16	15	oveq2i	$$⊢N+4+2=N+6$$
17	14 16	eqtrdi	$$⊢N\in ℝ\to N+4+2=N+6$$
18	17	breq1d	$$⊢N\in ℝ\to \left(N+4+2\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2\leftrightarrow N+6\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2\right)$$
19	18	adantr	$$⊢\left(N\in ℝ\wedge 6\le N\right)\to \left(N+4+2\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2\leftrightarrow N+6\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2\right)$$
20	9 19	mpbird	$$⊢\left(N\in ℝ\wedge 6\le N\right)\to N+4+2\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2$$
21		4re	$$⊢4\in ℝ$$
22	21	a1i	$$⊢N\in ℝ\to 4\in ℝ$$
23		4ne0	$$⊢4\ne 0$$
24	23	a1i	$$⊢N\in ℝ\to 4\ne 0$$
25	3 22 24	redivcld	$$⊢N\in ℝ\to \frac{N}{4}\in ℝ$$
26		peano2re	$$⊢\frac{N}{4}\in ℝ\to \left(\frac{N}{4}\right)+1\in ℝ$$
27	25 26	syl	$$⊢N\in ℝ\to \left(\frac{N}{4}\right)+1\in ℝ$$
28		peano2rem	$$⊢N\in ℝ\to N-1\in ℝ$$
29	28	rehalfcld	$$⊢N\in ℝ\to \frac{N-1}{2}\in ℝ$$
30		4pos	$$⊢0<4$$
31	21 30	pm3.2i	$$⊢\left(4\in ℝ\wedge 0<4\right)$$
32	31	a1i	$$⊢N\in ℝ\to \left(4\in ℝ\wedge 0<4\right)$$
33		lemul1	$$⊢\left(\left(\frac{N}{4}\right)+1\in ℝ\wedge \frac{N-1}{2}\in ℝ\wedge \left(4\in ℝ\wedge 0<4\right)\right)\to \left(\left(\frac{N}{4}\right)+1\le \frac{N-1}{2}\leftrightarrow \left(\left(\frac{N}{4}\right)+1\right)\cdot 4\le \left(\frac{N-1}{2}\right)\cdot 4\right)$$
34	27 29 32 33	syl3anc	$$⊢N\in ℝ\to \left(\left(\frac{N}{4}\right)+1\le \frac{N-1}{2}\leftrightarrow \left(\left(\frac{N}{4}\right)+1\right)\cdot 4\le \left(\frac{N-1}{2}\right)\cdot 4\right)$$
35	25	recnd	$$⊢N\in ℝ\to \frac{N}{4}\in ℂ$$
36		1cnd	$$⊢N\in ℝ\to 1\in ℂ$$
37	6 11 24	divcan1d	$$⊢N\in ℝ\to \left(\frac{N}{4}\right)\cdot 4=N$$
38	10	mulid2i	$$⊢1\cdot 4=4$$
39	38	a1i	$$⊢N\in ℝ\to 1\cdot 4=4$$
40	37 39	oveq12d	$$⊢N\in ℝ\to \left(\frac{N}{4}\right)\cdot 4+1\cdot 4=N+4$$
41	35 11 36 40	joinlmuladdmuld	$$⊢N\in ℝ\to \left(\left(\frac{N}{4}\right)+1\right)\cdot 4=N+4$$
42		2t2e4	$$⊢2\cdot 2=4$$
43	42	eqcomi	$$⊢4=2\cdot 2$$
44	43	a1i	$$⊢N\in ℝ\to 4=2\cdot 2$$
45	44	oveq2d	$$⊢N\in ℝ\to \left(\frac{N-1}{2}\right)\cdot 4=\left(\frac{N-1}{2}\right)2\cdot 2$$
46	29	recnd	$$⊢N\in ℝ\to \frac{N-1}{2}\in ℂ$$
47		mulass	$$⊢\left(\frac{N-1}{2}\in ℂ\wedge 2\in ℂ\wedge 2\in ℂ\right)\to \left(\frac{N-1}{2}\right)\cdot 2\cdot 2=\left(\frac{N-1}{2}\right)2\cdot 2$$
48	47	eqcomd	$$⊢\left(\frac{N-1}{2}\in ℂ\wedge 2\in ℂ\wedge 2\in ℂ\right)\to \left(\frac{N-1}{2}\right)2\cdot 2=\left(\frac{N-1}{2}\right)\cdot 2\cdot 2$$
49	46 13 13 48	syl3anc	$$⊢N\in ℝ\to \left(\frac{N-1}{2}\right)2\cdot 2=\left(\frac{N-1}{2}\right)\cdot 2\cdot 2$$
50	28	recnd	$$⊢N\in ℝ\to N-1\in ℂ$$
51		2ne0	$$⊢2\ne 0$$
52	51	a1i	$$⊢N\in ℝ\to 2\ne 0$$
53	50 13 52	divcan1d	$$⊢N\in ℝ\to \left(\frac{N-1}{2}\right)\cdot 2=N-1$$
54	53	oveq1d	$$⊢N\in ℝ\to \left(\frac{N-1}{2}\right)\cdot 2\cdot 2=\left(N-1\right)\cdot 2$$
55	6 36 13	subdird	$$⊢N\in ℝ\to \left(N-1\right)\cdot 2=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2-1\cdot 2$$
56	12	mulid2i	$$⊢1\cdot 2=2$$
57	56	a1i	$$⊢N\in ℝ\to 1\cdot 2=2$$
58	57	oveq2d	$$⊢N\in ℝ\to \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2-1\cdot 2=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2-2$$
59	54 55 58	3eqtrd	$$⊢N\in ℝ\to \left(\frac{N-1}{2}\right)\cdot 2\cdot 2=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2-2$$
60	45 49 59	3eqtrd	$$⊢N\in ℝ\to \left(\frac{N-1}{2}\right)\cdot 4=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2-2$$
61	41 60	breq12d	$$⊢N\in ℝ\to \left(\left(\left(\frac{N}{4}\right)+1\right)\cdot 4\le \left(\frac{N-1}{2}\right)\cdot 4\leftrightarrow N+4\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2-2\right)$$
62	3 22	readdcld	$$⊢N\in ℝ\to N+4\in ℝ$$
63		2re	$$⊢2\in ℝ$$
64	63	a1i	$$⊢N\in ℝ\to 2\in ℝ$$
65	3 64	remulcld	$$⊢N\in ℝ\to \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2\in ℝ$$
66		leaddsub	$$⊢\left(N+4\in ℝ\wedge 2\in ℝ\wedge \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2\in ℝ\right)\to \left(N+4+2\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2\leftrightarrow N+4\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2-2\right)$$
67	66	bicomd	$$⊢\left(N+4\in ℝ\wedge 2\in ℝ\wedge \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2\in ℝ\right)\to \left(N+4\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2-2\leftrightarrow N+4+2\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2\right)$$
68	62 64 65 67	syl3anc	$$⊢N\in ℝ\to \left(N+4\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2-2\leftrightarrow N+4+2\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2\right)$$
69	34 61 68	3bitrd	$$⊢N\in ℝ\to \left(\left(\frac{N}{4}\right)+1\le \frac{N-1}{2}\leftrightarrow N+4+2\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2\right)$$
70	69	adantr	$$⊢\left(N\in ℝ\wedge 6\le N\right)\to \left(\left(\frac{N}{4}\right)+1\le \frac{N-1}{2}\leftrightarrow N+4+2\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2\right)$$
71	20 70	mpbird	$$⊢\left(N\in ℝ\wedge 6\le N\right)\to \left(\frac{N}{4}\right)+1\le \frac{N-1}{2}$$