Metamath Proof Explorer

Theorem 2lgslem2

Description: Lemma 2 for 2lgs . (Contributed by AV, 20-Jun-2021)

Ref Expression
Hypothesis 2lgslem2.n ⊢N=P−12−P4
Assertion 2lgslem2 ⊢P∈ℙ∧¬2∥P→N∈ℤ

Proof

Step Hyp Ref Expression
1 2lgslem2.n ⊢N=P−12−P4
2 simpl ⊢P∈ℙ∧¬2∥P→P∈ℙ
3 elsng ⊢P∈ℙ→P∈2↔P=2
4 z2even ⊢2∥2
5 breq2 ⊢P=2→2∥P↔2∥2
6 4 5 mpbiri ⊢P=2→2∥P
7 3 6 syl6bi ⊢P∈ℙ→P∈2→2∥P
8 7 con3dimp ⊢P∈ℙ∧¬2∥P→¬P∈2
9 2 8 eldifd ⊢P∈ℙ∧¬2∥P→P∈ℙ∖2
10 oddprm ⊢P∈ℙ∖2→P−12∈ℕ
11 10 nnzd ⊢P∈ℙ∖2→P−12∈ℤ
12 9 11 syl ⊢P∈ℙ∧¬2∥P→P−12∈ℤ
13 prmz ⊢P∈ℙ→P∈ℤ
14 13 zred ⊢P∈ℙ→P∈ℝ
15 4re ⊢4∈ℝ
16 15 a1i ⊢P∈ℙ→4∈ℝ
17 4ne0 ⊢4≠0
18 17 a1i ⊢P∈ℙ→4≠0
19 14 16 18 redivcld ⊢P∈ℙ→P4∈ℝ
20 19 flcld ⊢P∈ℙ→P4∈ℤ
21 20 adantr ⊢P∈ℙ∧¬2∥P→P4∈ℤ
22 12 21 zsubcld ⊢P∈ℙ∧¬2∥P→P−12−P4∈ℤ
23 1 22 eqeltrid ⊢P∈ℙ∧¬2∥P→N∈ℤ