Metamath Proof Explorer

Theorem 2lgslem2

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

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

Proof

Step Hyp Ref Expression
1 2lgslem2.n ⊢ N = P − 1 2 − P 4
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 biimtrdi ⊢ 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 − 1 2 ∈ ℕ
11 10 nnzd ⊢ P ∈ ℙ ∖ 2 → P − 1 2 ∈ ℤ
12 9 11 syl ⊢ P ∈ ℙ ∧ ¬ 2 ∥ P → P − 1 2 ∈ ℤ
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 ∈ ℙ → P 4 ∈ ℝ
20 19 flcld ⊢ P ∈ ℙ → P 4 ∈ ℤ
21 20 adantr ⊢ P ∈ ℙ ∧ ¬ 2 ∥ P → P 4 ∈ ℤ
22 12 21 zsubcld ⊢ P ∈ ℙ ∧ ¬ 2 ∥ P → P − 1 2 − P 4 ∈ ℤ
23 1 22 eqeltrid ⊢ P ∈ ℙ ∧ ¬ 2 ∥ P → N ∈ ℤ