Theorem 2lgslem1c

Description: Lemma 3 for 2lgslem1 . (Contributed by AV, 19-Jun-2021)

	Ref	Expression
Assertion	2lgslem1c	$$⊢\left(P\in \mathbb{P}\wedge \neg 2\parallel P\right)\to ⌊\frac{P}{4}⌋\le \frac{P-1}{2}$$

Proof

Step	Hyp	Ref	Expression
1		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
2		nnnn0	$$⊢P\in \mathbb{N}\to P\in {\mathbb{N}}_0$$
3		oddnn02np1	$$⊢P\in {\mathbb{N}}_0\to \left(\neg 2\parallel P\leftrightarrow \exists n\in {\mathbb{N}}_{0}2n+1=P\right)$$
4	1 2 3	3syl	$$⊢P\in \mathbb{P}\to \left(\neg 2\parallel P\leftrightarrow \exists n\in {\mathbb{N}}_{0}2n+1=P\right)$$
5		iftrue	$$⊢2\parallel n\to if\left(2\parallel n,\frac{n}{2},\frac{n-1}{2}\right)=\frac{n}{2}$$
6	5	adantr	$$⊢\left(2\parallel n\wedge n\in {\mathbb{N}}_0\right)\to if\left(2\parallel n,\frac{n}{2},\frac{n-1}{2}\right)=\frac{n}{2}$$
7		2nn	$$⊢2\in \mathbb{N}$$
8		nn0ledivnn	$$⊢\left(n\in {\mathbb{N}}_0\wedge 2\in \mathbb{N}\right)\to \frac{n}{2}\le n$$
9	7 8	mpan2	$$⊢n\in {\mathbb{N}}_0\to \frac{n}{2}\le n$$
10	9	adantl	$$⊢\left(2\parallel n\wedge n\in {\mathbb{N}}_0\right)\to \frac{n}{2}\le n$$
11	6 10	eqbrtrd	$$⊢\left(2\parallel n\wedge n\in {\mathbb{N}}_0\right)\to if\left(2\parallel n,\frac{n}{2},\frac{n-1}{2}\right)\le n$$
12		iffalse	$$⊢\neg 2\parallel n\to if\left(2\parallel n,\frac{n}{2},\frac{n-1}{2}\right)=\frac{n-1}{2}$$
13	12	adantr	$$⊢\left(\neg 2\parallel n\wedge n\in {\mathbb{N}}_0\right)\to if\left(2\parallel n,\frac{n}{2},\frac{n-1}{2}\right)=\frac{n-1}{2}$$
14		nn0re	$$⊢n\in {\mathbb{N}}_0\to n\in ℝ$$
15		peano2rem	$$⊢n\in ℝ\to n-1\in ℝ$$
16	15	rehalfcld	$$⊢n\in ℝ\to \frac{n-1}{2}\in ℝ$$
17	14 16	syl	$$⊢n\in {\mathbb{N}}_0\to \frac{n-1}{2}\in ℝ$$
18	14	rehalfcld	$$⊢n\in {\mathbb{N}}_0\to \frac{n}{2}\in ℝ$$
19	14	lem1d	$$⊢n\in {\mathbb{N}}_0\to n-1\le n$$
20	14 15	syl	$$⊢n\in {\mathbb{N}}_0\to n-1\in ℝ$$
21		2re	$$⊢2\in ℝ$$
22		2pos	$$⊢0<2$$
23	21 22	pm3.2i	$$⊢\left(2\in ℝ\wedge 0<2\right)$$
24	23	a1i	$$⊢n\in {\mathbb{N}}_0\to \left(2\in ℝ\wedge 0<2\right)$$
25		lediv1	$$⊢\left(n-1\in ℝ\wedge n\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(n-1\le n\leftrightarrow \frac{n-1}{2}\le \frac{n}{2}\right)$$
26	20 14 24 25	syl3anc	$$⊢n\in {\mathbb{N}}_0\to \left(n-1\le n\leftrightarrow \frac{n-1}{2}\le \frac{n}{2}\right)$$
27	19 26	mpbid	$$⊢n\in {\mathbb{N}}_0\to \frac{n-1}{2}\le \frac{n}{2}$$
28	17 18 14 27 9	letrd	$$⊢n\in {\mathbb{N}}_0\to \frac{n-1}{2}\le n$$
29	28	adantl	$$⊢\left(\neg 2\parallel n\wedge n\in {\mathbb{N}}_0\right)\to \frac{n-1}{2}\le n$$
30	13 29	eqbrtrd	$$⊢\left(\neg 2\parallel n\wedge n\in {\mathbb{N}}_0\right)\to if\left(2\parallel n,\frac{n}{2},\frac{n-1}{2}\right)\le n$$
31	11 30	pm2.61ian	$$⊢n\in {\mathbb{N}}_0\to if\left(2\parallel n,\frac{n}{2},\frac{n-1}{2}\right)\le n$$
32	31	ad2antlr	$$⊢\left(\left(P\in \mathbb{P}\wedge n\in {\mathbb{N}}_0\right)\wedge 2n+1=P\right)\to if\left(2\parallel n,\frac{n}{2},\frac{n-1}{2}\right)\le n$$
33		nn0z	$$⊢n\in {\mathbb{N}}_0\to n\in \mathbb{Z}$$
34	33	adantl	$$⊢\left(P\in \mathbb{P}\wedge n\in {\mathbb{N}}_0\right)\to n\in \mathbb{Z}$$
35		eqcom	$$⊢2n+1=P\leftrightarrow P=2n+1$$
36	35	biimpi	$$⊢2n+1=P\to P=2n+1$$
37		flodddiv4	$$⊢\left(n\in \mathbb{Z}\wedge P=2n+1\right)\to ⌊\frac{P}{4}⌋=if\left(2\parallel n,\frac{n}{2},\frac{n-1}{2}\right)$$
38	34 36 37	syl2an	$$⊢\left(\left(P\in \mathbb{P}\wedge n\in {\mathbb{N}}_0\right)\wedge 2n+1=P\right)\to ⌊\frac{P}{4}⌋=if\left(2\parallel n,\frac{n}{2},\frac{n-1}{2}\right)$$
39		oveq1	$$⊢P=2n+1\to P-1=2n+1-1$$
40	39	eqcoms	$$⊢2n+1=P\to P-1=2n+1-1$$
41	40	adantl	$$⊢\left(\left(P\in \mathbb{P}\wedge n\in {\mathbb{N}}_0\right)\wedge 2n+1=P\right)\to P-1=2n+1-1$$
42		2nn0	$$⊢2\in {\mathbb{N}}_0$$
43	42	a1i	$$⊢n\in {\mathbb{N}}_0\to 2\in {\mathbb{N}}_0$$
44		id	$$⊢n\in {\mathbb{N}}_0\to n\in {\mathbb{N}}_0$$
45	43 44	nn0mulcld	$$⊢n\in {\mathbb{N}}_0\to 2n\in {\mathbb{N}}_0$$
46	45	nn0cnd	$$⊢n\in {\mathbb{N}}_0\to 2n\in ℂ$$
47		pncan1	$$⊢2n\in ℂ\to 2n+1-1=2n$$
48	46 47	syl	$$⊢n\in {\mathbb{N}}_0\to 2n+1-1=2n$$
49	48	ad2antlr	$$⊢\left(\left(P\in \mathbb{P}\wedge n\in {\mathbb{N}}_0\right)\wedge 2n+1=P\right)\to 2n+1-1=2n$$
50	41 49	eqtrd	$$⊢\left(\left(P\in \mathbb{P}\wedge n\in {\mathbb{N}}_0\right)\wedge 2n+1=P\right)\to P-1=2n$$
51	50	oveq1d	$$⊢\left(\left(P\in \mathbb{P}\wedge n\in {\mathbb{N}}_0\right)\wedge 2n+1=P\right)\to \frac{P-1}{2}=\frac{2n}{2}$$
52		nn0cn	$$⊢n\in {\mathbb{N}}_0\to n\in ℂ$$
53		2cnd	$$⊢n\in {\mathbb{N}}_0\to 2\in ℂ$$
54		2ne0	$$⊢2\ne 0$$
55	54	a1i	$$⊢n\in {\mathbb{N}}_0\to 2\ne 0$$
56	52 53 55	divcan3d	$$⊢n\in {\mathbb{N}}_0\to \frac{2n}{2}=n$$
57	56	ad2antlr	$$⊢\left(\left(P\in \mathbb{P}\wedge n\in {\mathbb{N}}_0\right)\wedge 2n+1=P\right)\to \frac{2n}{2}=n$$
58	51 57	eqtrd	$$⊢\left(\left(P\in \mathbb{P}\wedge n\in {\mathbb{N}}_0\right)\wedge 2n+1=P\right)\to \frac{P-1}{2}=n$$
59	32 38 58	3brtr4d	$$⊢\left(\left(P\in \mathbb{P}\wedge n\in {\mathbb{N}}_0\right)\wedge 2n+1=P\right)\to ⌊\frac{P}{4}⌋\le \frac{P-1}{2}$$
60	59	rexlimdva2	$$⊢P\in \mathbb{P}\to \left(\exists n\in {\mathbb{N}}_{0}2n+1=P\to ⌊\frac{P}{4}⌋\le \frac{P-1}{2}\right)$$
61	4 60	sylbid	$$⊢P\in \mathbb{P}\to \left(\neg 2\parallel P\to ⌊\frac{P}{4}⌋\le \frac{P-1}{2}\right)$$
62	61	imp	$$⊢\left(P\in \mathbb{P}\wedge \neg 2\parallel P\right)\to ⌊\frac{P}{4}⌋\le \frac{P-1}{2}$$