Metamath Proof Explorer

Theorem 2lgsoddprmlem3

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

Ref Expression
Assertion 2lgsoddprmlem3 ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N ∧ R = N mod 8 → 2 ∥ R 2 − 1 8 ↔ R ∈ 1 7

Proof

Step Hyp Ref Expression
1 lgsdir2lem3 ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N → N mod 8 ∈ 1 7 ∪ 3 5
2 eleq1 ⊢ N mod 8 = R → N mod 8 ∈ 1 7 ∪ 3 5 ↔ R ∈ 1 7 ∪ 3 5
3 2 eqcoms ⊢ R = N mod 8 → N mod 8 ∈ 1 7 ∪ 3 5 ↔ R ∈ 1 7 ∪ 3 5
4 elun ⊢ R ∈ 1 7 ∪ 3 5 ↔ R ∈ 1 7 ∨ R ∈ 3 5
5 elpri ⊢ R ∈ 3 5 → R = 3 ∨ R = 5
6 oveq1 ⊢ R = 3 → R 2 = 3 2
7 6 oveq1d ⊢ R = 3 → R 2 − 1 = 3 2 − 1
8 7 oveq1d ⊢ R = 3 → R 2 − 1 8 = 3 2 − 1 8
9 2lgsoddprmlem3b ⊢ 3 2 − 1 8 = 1
10 8 9 eqtrdi ⊢ R = 3 → R 2 − 1 8 = 1
11 10 breq2d ⊢ R = 3 → 2 ∥ R 2 − 1 8 ↔ 2 ∥ 1
12 n2dvds1 ⊢ ¬ 2 ∥ 1
13 12 pm2.21i ⊢ 2 ∥ 1 → R ∈ 1 7
14 11 13 syl6bi ⊢ R = 3 → 2 ∥ R 2 − 1 8 → R ∈ 1 7
15 oveq1 ⊢ R = 5 → R 2 = 5 2
16 15 oveq1d ⊢ R = 5 → R 2 − 1 = 5 2 − 1
17 16 oveq1d ⊢ R = 5 → R 2 − 1 8 = 5 2 − 1 8
18 17 breq2d ⊢ R = 5 → 2 ∥ R 2 − 1 8 ↔ 2 ∥ 5 2 − 1 8
19 2lgsoddprmlem3c ⊢ 5 2 − 1 8 = 3
20 19 breq2i ⊢ 2 ∥ 5 2 − 1 8 ↔ 2 ∥ 3
21 18 20 bitrdi ⊢ R = 5 → 2 ∥ R 2 − 1 8 ↔ 2 ∥ 3
22 n2dvds3 ⊢ ¬ 2 ∥ 3
23 22 pm2.21i ⊢ 2 ∥ 3 → R ∈ 1 7
24 21 23 syl6bi ⊢ R = 5 → 2 ∥ R 2 − 1 8 → R ∈ 1 7
25 14 24 jaoi ⊢ R = 3 ∨ R = 5 → 2 ∥ R 2 − 1 8 → R ∈ 1 7
26 5 25 syl ⊢ R ∈ 3 5 → 2 ∥ R 2 − 1 8 → R ∈ 1 7
27 26 jao1i ⊢ R ∈ 1 7 ∨ R ∈ 3 5 → 2 ∥ R 2 − 1 8 → R ∈ 1 7
28 4 27 sylbi ⊢ R ∈ 1 7 ∪ 3 5 → 2 ∥ R 2 − 1 8 → R ∈ 1 7
29 elpri ⊢ R ∈ 1 7 → R = 1 ∨ R = 7
30 z0even ⊢ 2 ∥ 0
31 oveq1 ⊢ R = 1 → R 2 = 1 2
32 31 oveq1d ⊢ R = 1 → R 2 − 1 = 1 2 − 1
33 32 oveq1d ⊢ R = 1 → R 2 − 1 8 = 1 2 − 1 8
34 2lgsoddprmlem3a ⊢ 1 2 − 1 8 = 0
35 33 34 eqtrdi ⊢ R = 1 → R 2 − 1 8 = 0
36 30 35 breqtrrid ⊢ R = 1 → 2 ∥ R 2 − 1 8
37 2z ⊢ 2 ∈ ℤ
38 3z ⊢ 3 ∈ ℤ
39 dvdsmul1 ⊢ 2 ∈ ℤ ∧ 3 ∈ ℤ → 2 ∥ 2 ⋅ 3
40 37 38 39 mp2an ⊢ 2 ∥ 2 ⋅ 3
41 oveq1 ⊢ R = 7 → R 2 = 7 2
42 41 oveq1d ⊢ R = 7 → R 2 − 1 = 7 2 − 1
43 42 oveq1d ⊢ R = 7 → R 2 − 1 8 = 7 2 − 1 8
44 2lgsoddprmlem3d ⊢ 7 2 − 1 8 = 2 ⋅ 3
45 43 44 eqtrdi ⊢ R = 7 → R 2 − 1 8 = 2 ⋅ 3
46 40 45 breqtrrid ⊢ R = 7 → 2 ∥ R 2 − 1 8
47 36 46 jaoi ⊢ R = 1 ∨ R = 7 → 2 ∥ R 2 − 1 8
48 29 47 syl ⊢ R ∈ 1 7 → 2 ∥ R 2 − 1 8
49 28 48 impbid1 ⊢ R ∈ 1 7 ∪ 3 5 → 2 ∥ R 2 − 1 8 ↔ R ∈ 1 7
50 3 49 syl6bi ⊢ R = N mod 8 → N mod 8 ∈ 1 7 ∪ 3 5 → 2 ∥ R 2 − 1 8 ↔ R ∈ 1 7
51 1 50 syl5com ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N → R = N mod 8 → 2 ∥ R 2 − 1 8 ↔ R ∈ 1 7
52 51 3impia ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N ∧ R = N mod 8 → 2 ∥ R 2 − 1 8 ↔ R ∈ 1 7