Metamath Proof Explorer

Theorem 2lgsoddprmlem3

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

Ref Expression
Assertion 2lgsoddprmlem3 ⊢N∈ℤ∧¬2∥N∧R=Nmod8→2∥R2−18↔R∈17

Proof

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