# Metamath Proof Explorer

## Theorem 2lgsoddprmlem3

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

Ref Expression
Assertion 2lgsoddprmlem3 ${⊢}\left({N}\in ℤ\wedge ¬2\parallel {N}\wedge {R}={N}\mathrm{mod}8\right)\to \left(2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)↔{R}\in \left\{1,7\right\}\right)$

### Proof

Step Hyp Ref Expression
1 lgsdir2lem3 ${⊢}\left({N}\in ℤ\wedge ¬2\parallel {N}\right)\to {N}\mathrm{mod}8\in \left(\left\{1,7\right\}\cup \left\{3,5\right\}\right)$
2 eleq1 ${⊢}{N}\mathrm{mod}8={R}\to \left({N}\mathrm{mod}8\in \left(\left\{1,7\right\}\cup \left\{3,5\right\}\right)↔{R}\in \left(\left\{1,7\right\}\cup \left\{3,5\right\}\right)\right)$
3 2 eqcoms ${⊢}{R}={N}\mathrm{mod}8\to \left({N}\mathrm{mod}8\in \left(\left\{1,7\right\}\cup \left\{3,5\right\}\right)↔{R}\in \left(\left\{1,7\right\}\cup \left\{3,5\right\}\right)\right)$
4 elun ${⊢}{R}\in \left(\left\{1,7\right\}\cup \left\{3,5\right\}\right)↔\left({R}\in \left\{1,7\right\}\vee {R}\in \left\{3,5\right\}\right)$
5 elpri ${⊢}{R}\in \left\{3,5\right\}\to \left({R}=3\vee {R}=5\right)$
6 oveq1 ${⊢}{R}=3\to {{R}}^{2}={3}^{2}$
7 6 oveq1d ${⊢}{R}=3\to {{R}}^{2}-1={3}^{2}-1$
8 7 oveq1d ${⊢}{R}=3\to \frac{{{R}}^{2}-1}{8}=\frac{{3}^{2}-1}{8}$
9 2lgsoddprmlem3b ${⊢}\frac{{3}^{2}-1}{8}=1$
10 8 9 eqtrdi ${⊢}{R}=3\to \frac{{{R}}^{2}-1}{8}=1$
11 10 breq2d ${⊢}{R}=3\to \left(2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)↔2\parallel 1\right)$
12 n2dvds1 ${⊢}¬2\parallel 1$
13 12 pm2.21i ${⊢}2\parallel 1\to {R}\in \left\{1,7\right\}$
14 11 13 syl6bi ${⊢}{R}=3\to \left(2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)\to {R}\in \left\{1,7\right\}\right)$
15 oveq1 ${⊢}{R}=5\to {{R}}^{2}={5}^{2}$
16 15 oveq1d ${⊢}{R}=5\to {{R}}^{2}-1={5}^{2}-1$
17 16 oveq1d ${⊢}{R}=5\to \frac{{{R}}^{2}-1}{8}=\frac{{5}^{2}-1}{8}$
18 17 breq2d ${⊢}{R}=5\to \left(2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)↔2\parallel \left(\frac{{5}^{2}-1}{8}\right)\right)$
19 2lgsoddprmlem3c ${⊢}\frac{{5}^{2}-1}{8}=3$
20 19 breq2i ${⊢}2\parallel \left(\frac{{5}^{2}-1}{8}\right)↔2\parallel 3$
21 18 20 syl6bb ${⊢}{R}=5\to \left(2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)↔2\parallel 3\right)$
22 n2dvds3 ${⊢}¬2\parallel 3$
23 22 pm2.21i ${⊢}2\parallel 3\to {R}\in \left\{1,7\right\}$
24 21 23 syl6bi ${⊢}{R}=5\to \left(2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)\to {R}\in \left\{1,7\right\}\right)$
25 14 24 jaoi ${⊢}\left({R}=3\vee {R}=5\right)\to \left(2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)\to {R}\in \left\{1,7\right\}\right)$
26 5 25 syl ${⊢}{R}\in \left\{3,5\right\}\to \left(2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)\to {R}\in \left\{1,7\right\}\right)$
27 26 jao1i ${⊢}\left({R}\in \left\{1,7\right\}\vee {R}\in \left\{3,5\right\}\right)\to \left(2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)\to {R}\in \left\{1,7\right\}\right)$
28 4 27 sylbi ${⊢}{R}\in \left(\left\{1,7\right\}\cup \left\{3,5\right\}\right)\to \left(2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)\to {R}\in \left\{1,7\right\}\right)$
29 elpri ${⊢}{R}\in \left\{1,7\right\}\to \left({R}=1\vee {R}=7\right)$
30 z0even ${⊢}2\parallel 0$
31 oveq1 ${⊢}{R}=1\to {{R}}^{2}={1}^{2}$
32 31 oveq1d ${⊢}{R}=1\to {{R}}^{2}-1={1}^{2}-1$
33 32 oveq1d ${⊢}{R}=1\to \frac{{{R}}^{2}-1}{8}=\frac{{1}^{2}-1}{8}$
34 2lgsoddprmlem3a ${⊢}\frac{{1}^{2}-1}{8}=0$
35 33 34 eqtrdi ${⊢}{R}=1\to \frac{{{R}}^{2}-1}{8}=0$
36 30 35 breqtrrid ${⊢}{R}=1\to 2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)$
37 2z ${⊢}2\in ℤ$
38 3z ${⊢}3\in ℤ$
39 dvdsmul1 ${⊢}\left(2\in ℤ\wedge 3\in ℤ\right)\to 2\parallel 2\cdot 3$
40 37 38 39 mp2an ${⊢}2\parallel 2\cdot 3$
41 oveq1 ${⊢}{R}=7\to {{R}}^{2}={7}^{2}$
42 41 oveq1d ${⊢}{R}=7\to {{R}}^{2}-1={7}^{2}-1$
43 42 oveq1d ${⊢}{R}=7\to \frac{{{R}}^{2}-1}{8}=\frac{{7}^{2}-1}{8}$
44 2lgsoddprmlem3d ${⊢}\frac{{7}^{2}-1}{8}=2\cdot 3$
45 43 44 eqtrdi ${⊢}{R}=7\to \frac{{{R}}^{2}-1}{8}=2\cdot 3$
46 40 45 breqtrrid ${⊢}{R}=7\to 2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)$
47 36 46 jaoi ${⊢}\left({R}=1\vee {R}=7\right)\to 2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)$
48 29 47 syl ${⊢}{R}\in \left\{1,7\right\}\to 2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)$
49 28 48 impbid1 ${⊢}{R}\in \left(\left\{1,7\right\}\cup \left\{3,5\right\}\right)\to \left(2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)↔{R}\in \left\{1,7\right\}\right)$
50 3 49 syl6bi ${⊢}{R}={N}\mathrm{mod}8\to \left({N}\mathrm{mod}8\in \left(\left\{1,7\right\}\cup \left\{3,5\right\}\right)\to \left(2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)↔{R}\in \left\{1,7\right\}\right)\right)$
51 1 50 syl5com ${⊢}\left({N}\in ℤ\wedge ¬2\parallel {N}\right)\to \left({R}={N}\mathrm{mod}8\to \left(2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)↔{R}\in \left\{1,7\right\}\right)\right)$
52 51 3impia ${⊢}\left({N}\in ℤ\wedge ¬2\parallel {N}\wedge {R}={N}\mathrm{mod}8\right)\to \left(2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)↔{R}\in \left\{1,7\right\}\right)$