Metamath Proof Explorer

Theorem 2lgslem3

Description: Lemma 3 for 2lgs . (Contributed by AV, 16-Jul-2021)

Ref Expression
Hypothesis 2lgslem2.n ⊢ N = P − 1 2 − P 4
Assertion 2lgslem3 ⊢ P ∈ ℕ ∧ ¬ 2 ∥ P → N mod 2 = if P mod 8 ∈ 1 7 0 1

Proof

Step Hyp Ref Expression
1 2lgslem2.n ⊢ N = P − 1 2 − P 4
2 nnz ⊢ P ∈ ℕ → P ∈ ℤ
3 lgsdir2lem3 ⊢ P ∈ ℤ ∧ ¬ 2 ∥ P → P mod 8 ∈ 1 7 ∪ 3 5
4 2 3 sylan ⊢ P ∈ ℕ ∧ ¬ 2 ∥ P → P mod 8 ∈ 1 7 ∪ 3 5
5 elun ⊢ P mod 8 ∈ 1 7 ∪ 3 5 ↔ P mod 8 ∈ 1 7 ∨ P mod 8 ∈ 3 5
6 ovex ⊢ P mod 8 ∈ V
7 6 elpr ⊢ P mod 8 ∈ 1 7 ↔ P mod 8 = 1 ∨ P mod 8 = 7
8 1 2lgslem3a1 ⊢ P ∈ ℕ ∧ P mod 8 = 1 → N mod 2 = 0
9 8 a1d ⊢ P ∈ ℕ ∧ P mod 8 = 1 → ¬ 2 ∥ P → N mod 2 = 0
10 9 expcom ⊢ P mod 8 = 1 → P ∈ ℕ → ¬ 2 ∥ P → N mod 2 = 0
11 10 impd ⊢ P mod 8 = 1 → P ∈ ℕ ∧ ¬ 2 ∥ P → N mod 2 = 0
12 1 2lgslem3d1 ⊢ P ∈ ℕ ∧ P mod 8 = 7 → N mod 2 = 0
13 12 a1d ⊢ P ∈ ℕ ∧ P mod 8 = 7 → ¬ 2 ∥ P → N mod 2 = 0
14 13 expcom ⊢ P mod 8 = 7 → P ∈ ℕ → ¬ 2 ∥ P → N mod 2 = 0
15 14 impd ⊢ P mod 8 = 7 → P ∈ ℕ ∧ ¬ 2 ∥ P → N mod 2 = 0
16 11 15 jaoi ⊢ P mod 8 = 1 ∨ P mod 8 = 7 → P ∈ ℕ ∧ ¬ 2 ∥ P → N mod 2 = 0
17 7 16 sylbi ⊢ P mod 8 ∈ 1 7 → P ∈ ℕ ∧ ¬ 2 ∥ P → N mod 2 = 0
18 17 imp ⊢ P mod 8 ∈ 1 7 ∧ P ∈ ℕ ∧ ¬ 2 ∥ P → N mod 2 = 0
19 iftrue ⊢ P mod 8 ∈ 1 7 → if P mod 8 ∈ 1 7 0 1 = 0
20 19 adantr ⊢ P mod 8 ∈ 1 7 ∧ P ∈ ℕ ∧ ¬ 2 ∥ P → if P mod 8 ∈ 1 7 0 1 = 0
21 18 20 eqtr4d ⊢ P mod 8 ∈ 1 7 ∧ P ∈ ℕ ∧ ¬ 2 ∥ P → N mod 2 = if P mod 8 ∈ 1 7 0 1
22 21 ex ⊢ P mod 8 ∈ 1 7 → P ∈ ℕ ∧ ¬ 2 ∥ P → N mod 2 = if P mod 8 ∈ 1 7 0 1
23 6 elpr ⊢ P mod 8 ∈ 3 5 ↔ P mod 8 = 3 ∨ P mod 8 = 5
24 1 2lgslem3b1 ⊢ P ∈ ℕ ∧ P mod 8 = 3 → N mod 2 = 1
25 24 expcom ⊢ P mod 8 = 3 → P ∈ ℕ → N mod 2 = 1
26 1 2lgslem3c1 ⊢ P ∈ ℕ ∧ P mod 8 = 5 → N mod 2 = 1
27 26 expcom ⊢ P mod 8 = 5 → P ∈ ℕ → N mod 2 = 1
28 25 27 jaoi ⊢ P mod 8 = 3 ∨ P mod 8 = 5 → P ∈ ℕ → N mod 2 = 1
29 28 imp ⊢ P mod 8 = 3 ∨ P mod 8 = 5 ∧ P ∈ ℕ → N mod 2 = 1
30 1re ⊢ 1 ∈ ℝ
31 1lt3 ⊢ 1 < 3
32 30 31 ltneii ⊢ 1 ≠ 3
33 32 nesymi ⊢ ¬ 3 = 1
34 3re ⊢ 3 ∈ ℝ
35 3lt7 ⊢ 3 < 7
36 34 35 ltneii ⊢ 3 ≠ 7
37 36 neii ⊢ ¬ 3 = 7
38 33 37 pm3.2i ⊢ ¬ 3 = 1 ∧ ¬ 3 = 7
39 eqeq1 ⊢ P mod 8 = 3 → P mod 8 = 1 ↔ 3 = 1
40 39 notbid ⊢ P mod 8 = 3 → ¬ P mod 8 = 1 ↔ ¬ 3 = 1
41 eqeq1 ⊢ P mod 8 = 3 → P mod 8 = 7 ↔ 3 = 7
42 41 notbid ⊢ P mod 8 = 3 → ¬ P mod 8 = 7 ↔ ¬ 3 = 7
43 40 42 anbi12d ⊢ P mod 8 = 3 → ¬ P mod 8 = 1 ∧ ¬ P mod 8 = 7 ↔ ¬ 3 = 1 ∧ ¬ 3 = 7
44 38 43 mpbiri ⊢ P mod 8 = 3 → ¬ P mod 8 = 1 ∧ ¬ P mod 8 = 7
45 1lt5 ⊢ 1 < 5
46 30 45 ltneii ⊢ 1 ≠ 5
47 46 nesymi ⊢ ¬ 5 = 1
48 5re ⊢ 5 ∈ ℝ
49 5lt7 ⊢ 5 < 7
50 48 49 ltneii ⊢ 5 ≠ 7
51 50 neii ⊢ ¬ 5 = 7
52 47 51 pm3.2i ⊢ ¬ 5 = 1 ∧ ¬ 5 = 7
53 eqeq1 ⊢ P mod 8 = 5 → P mod 8 = 1 ↔ 5 = 1
54 53 notbid ⊢ P mod 8 = 5 → ¬ P mod 8 = 1 ↔ ¬ 5 = 1
55 eqeq1 ⊢ P mod 8 = 5 → P mod 8 = 7 ↔ 5 = 7
56 55 notbid ⊢ P mod 8 = 5 → ¬ P mod 8 = 7 ↔ ¬ 5 = 7
57 54 56 anbi12d ⊢ P mod 8 = 5 → ¬ P mod 8 = 1 ∧ ¬ P mod 8 = 7 ↔ ¬ 5 = 1 ∧ ¬ 5 = 7
58 52 57 mpbiri ⊢ P mod 8 = 5 → ¬ P mod 8 = 1 ∧ ¬ P mod 8 = 7
59 44 58 jaoi ⊢ P mod 8 = 3 ∨ P mod 8 = 5 → ¬ P mod 8 = 1 ∧ ¬ P mod 8 = 7
60 59 adantr ⊢ P mod 8 = 3 ∨ P mod 8 = 5 ∧ P ∈ ℕ → ¬ P mod 8 = 1 ∧ ¬ P mod 8 = 7
61 ioran ⊢ ¬ P mod 8 = 1 ∨ P mod 8 = 7 ↔ ¬ P mod 8 = 1 ∧ ¬ P mod 8 = 7
62 61 7 xchnxbir ⊢ ¬ P mod 8 ∈ 1 7 ↔ ¬ P mod 8 = 1 ∧ ¬ P mod 8 = 7
63 60 62 sylibr ⊢ P mod 8 = 3 ∨ P mod 8 = 5 ∧ P ∈ ℕ → ¬ P mod 8 ∈ 1 7
64 63 iffalsed ⊢ P mod 8 = 3 ∨ P mod 8 = 5 ∧ P ∈ ℕ → if P mod 8 ∈ 1 7 0 1 = 1
65 29 64 eqtr4d ⊢ P mod 8 = 3 ∨ P mod 8 = 5 ∧ P ∈ ℕ → N mod 2 = if P mod 8 ∈ 1 7 0 1
66 65 a1d ⊢ P mod 8 = 3 ∨ P mod 8 = 5 ∧ P ∈ ℕ → ¬ 2 ∥ P → N mod 2 = if P mod 8 ∈ 1 7 0 1
67 66 expimpd ⊢ P mod 8 = 3 ∨ P mod 8 = 5 → P ∈ ℕ ∧ ¬ 2 ∥ P → N mod 2 = if P mod 8 ∈ 1 7 0 1
68 23 67 sylbi ⊢ P mod 8 ∈ 3 5 → P ∈ ℕ ∧ ¬ 2 ∥ P → N mod 2 = if P mod 8 ∈ 1 7 0 1
69 22 68 jaoi ⊢ P mod 8 ∈ 1 7 ∨ P mod 8 ∈ 3 5 → P ∈ ℕ ∧ ¬ 2 ∥ P → N mod 2 = if P mod 8 ∈ 1 7 0 1
70 5 69 sylbi ⊢ P mod 8 ∈ 1 7 ∪ 3 5 → P ∈ ℕ ∧ ¬ 2 ∥ P → N mod 2 = if P mod 8 ∈ 1 7 0 1
71 4 70 mpcom ⊢ P ∈ ℕ ∧ ¬ 2 ∥ P → N mod 2 = if P mod 8 ∈ 1 7 0 1