# Metamath Proof Explorer

## Theorem 2lgslem1c

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

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

### Proof

Step Hyp Ref Expression
1 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
2 nnnn0 ${⊢}{P}\in ℕ\to {P}\in {ℕ}_{0}$
3 oddnn02np1 ${⊢}{P}\in {ℕ}_{0}\to \left(¬2\parallel {P}↔\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}2{n}+1={P}\right)$
4 1 2 3 3syl ${⊢}{P}\in ℙ\to \left(¬2\parallel {P}↔\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}2{n}+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 {ℕ}_{0}\right)\to if\left(2\parallel {n},\frac{{n}}{2},\frac{{n}-1}{2}\right)=\frac{{n}}{2}$
7 2nn ${⊢}2\in ℕ$
8 nn0ledivnn ${⊢}\left({n}\in {ℕ}_{0}\wedge 2\in ℕ\right)\to \frac{{n}}{2}\le {n}$
9 7 8 mpan2 ${⊢}{n}\in {ℕ}_{0}\to \frac{{n}}{2}\le {n}$
10 9 adantl ${⊢}\left(2\parallel {n}\wedge {n}\in {ℕ}_{0}\right)\to \frac{{n}}{2}\le {n}$
11 6 10 eqbrtrd ${⊢}\left(2\parallel {n}\wedge {n}\in {ℕ}_{0}\right)\to if\left(2\parallel {n},\frac{{n}}{2},\frac{{n}-1}{2}\right)\le {n}$
12 iffalse ${⊢}¬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(¬2\parallel {n}\wedge {n}\in {ℕ}_{0}\right)\to if\left(2\parallel {n},\frac{{n}}{2},\frac{{n}-1}{2}\right)=\frac{{n}-1}{2}$
14 nn0re ${⊢}{n}\in {ℕ}_{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 {ℕ}_{0}\to \frac{{n}-1}{2}\in ℝ$
18 14 rehalfcld ${⊢}{n}\in {ℕ}_{0}\to \frac{{n}}{2}\in ℝ$
19 14 lem1d ${⊢}{n}\in {ℕ}_{0}\to {n}-1\le {n}$
20 14 15 syl ${⊢}{n}\in {ℕ}_{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 {ℕ}_{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}↔\frac{{n}-1}{2}\le \frac{{n}}{2}\right)$
26 20 14 24 25 syl3anc ${⊢}{n}\in {ℕ}_{0}\to \left({n}-1\le {n}↔\frac{{n}-1}{2}\le \frac{{n}}{2}\right)$
27 19 26 mpbid ${⊢}{n}\in {ℕ}_{0}\to \frac{{n}-1}{2}\le \frac{{n}}{2}$
28 17 18 14 27 9 letrd ${⊢}{n}\in {ℕ}_{0}\to \frac{{n}-1}{2}\le {n}$
29 28 adantl ${⊢}\left(¬2\parallel {n}\wedge {n}\in {ℕ}_{0}\right)\to \frac{{n}-1}{2}\le {n}$
30 13 29 eqbrtrd ${⊢}\left(¬2\parallel {n}\wedge {n}\in {ℕ}_{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 {ℕ}_{0}\to if\left(2\parallel {n},\frac{{n}}{2},\frac{{n}-1}{2}\right)\le {n}$
32 31 ad2antlr ${⊢}\left(\left({P}\in ℙ\wedge {n}\in {ℕ}_{0}\right)\wedge 2{n}+1={P}\right)\to if\left(2\parallel {n},\frac{{n}}{2},\frac{{n}-1}{2}\right)\le {n}$
33 nn0z ${⊢}{n}\in {ℕ}_{0}\to {n}\in ℤ$
34 33 adantl ${⊢}\left({P}\in ℙ\wedge {n}\in {ℕ}_{0}\right)\to {n}\in ℤ$
35 eqcom ${⊢}2{n}+1={P}↔{P}=2{n}+1$
36 35 biimpi ${⊢}2{n}+1={P}\to {P}=2{n}+1$
37 flodddiv4 ${⊢}\left({n}\in ℤ\wedge {P}=2{n}+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 ℙ\wedge {n}\in {ℕ}_{0}\right)\wedge 2{n}+1={P}\right)\to ⌊\frac{{P}}{4}⌋=if\left(2\parallel {n},\frac{{n}}{2},\frac{{n}-1}{2}\right)$
39 oveq1 ${⊢}{P}=2{n}+1\to {P}-1=2{n}+1-1$
40 39 eqcoms ${⊢}2{n}+1={P}\to {P}-1=2{n}+1-1$
41 40 adantl ${⊢}\left(\left({P}\in ℙ\wedge {n}\in {ℕ}_{0}\right)\wedge 2{n}+1={P}\right)\to {P}-1=2{n}+1-1$
42 2nn0 ${⊢}2\in {ℕ}_{0}$
43 42 a1i ${⊢}{n}\in {ℕ}_{0}\to 2\in {ℕ}_{0}$
44 id ${⊢}{n}\in {ℕ}_{0}\to {n}\in {ℕ}_{0}$
45 43 44 nn0mulcld ${⊢}{n}\in {ℕ}_{0}\to 2{n}\in {ℕ}_{0}$
46 45 nn0cnd ${⊢}{n}\in {ℕ}_{0}\to 2{n}\in ℂ$
47 pncan1 ${⊢}2{n}\in ℂ\to 2{n}+1-1=2{n}$
48 46 47 syl ${⊢}{n}\in {ℕ}_{0}\to 2{n}+1-1=2{n}$
49 48 ad2antlr ${⊢}\left(\left({P}\in ℙ\wedge {n}\in {ℕ}_{0}\right)\wedge 2{n}+1={P}\right)\to 2{n}+1-1=2{n}$
50 41 49 eqtrd ${⊢}\left(\left({P}\in ℙ\wedge {n}\in {ℕ}_{0}\right)\wedge 2{n}+1={P}\right)\to {P}-1=2{n}$
51 50 oveq1d ${⊢}\left(\left({P}\in ℙ\wedge {n}\in {ℕ}_{0}\right)\wedge 2{n}+1={P}\right)\to \frac{{P}-1}{2}=\frac{2{n}}{2}$
52 nn0cn ${⊢}{n}\in {ℕ}_{0}\to {n}\in ℂ$
53 2cnd ${⊢}{n}\in {ℕ}_{0}\to 2\in ℂ$
54 2ne0 ${⊢}2\ne 0$
55 54 a1i ${⊢}{n}\in {ℕ}_{0}\to 2\ne 0$
56 52 53 55 divcan3d ${⊢}{n}\in {ℕ}_{0}\to \frac{2{n}}{2}={n}$
57 56 ad2antlr ${⊢}\left(\left({P}\in ℙ\wedge {n}\in {ℕ}_{0}\right)\wedge 2{n}+1={P}\right)\to \frac{2{n}}{2}={n}$
58 51 57 eqtrd ${⊢}\left(\left({P}\in ℙ\wedge {n}\in {ℕ}_{0}\right)\wedge 2{n}+1={P}\right)\to \frac{{P}-1}{2}={n}$
59 32 38 58 3brtr4d ${⊢}\left(\left({P}\in ℙ\wedge {n}\in {ℕ}_{0}\right)\wedge 2{n}+1={P}\right)\to ⌊\frac{{P}}{4}⌋\le \frac{{P}-1}{2}$
60 59 rexlimdva2 ${⊢}{P}\in ℙ\to \left(\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}2{n}+1={P}\to ⌊\frac{{P}}{4}⌋\le \frac{{P}-1}{2}\right)$
61 4 60 sylbid ${⊢}{P}\in ℙ\to \left(¬2\parallel {P}\to ⌊\frac{{P}}{4}⌋\le \frac{{P}-1}{2}\right)$
62 61 imp ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to ⌊\frac{{P}}{4}⌋\le \frac{{P}-1}{2}$