Theorem 2lgsoddprmlem3

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

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

Proof

Step	Hyp	Ref	Expression
1		lgsdir2lem3	$$⊢\left(N\in \mathbb{Z}\wedge \neg 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)\leftrightarrow 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)\leftrightarrow 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)\leftrightarrow \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)\leftrightarrow 2\parallel 1\right)$$
12		n2dvds1	$$⊢\neg 2\parallel 1$$
13	12	pm2.21i	$$⊢2\parallel 1\to R\in \left\{1,7\right\}$$
14	11 13	biimtrdi	$$⊢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)\leftrightarrow 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)\leftrightarrow 2\parallel 3$$
21	18 20	bitrdi	$$⊢R=5\to \left(2\parallel \left(\frac{R^2-1}{8}\right)\leftrightarrow 2\parallel 3\right)$$
22		n2dvds3	$$⊢\neg 2\parallel 3$$
23	22	pm2.21i	$$⊢2\parallel 3\to R\in \left\{1,7\right\}$$
24	21 23	biimtrdi	$$⊢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 \mathbb{Z}$$
38		3z	$$⊢3\in \mathbb{Z}$$
39		dvdsmul1	$$⊢\left(2\in \mathbb{Z}\wedge 3\in \mathbb{Z}\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)\leftrightarrow R\in \left\{1,7\right\}\right)$$
50	3 49	biimtrdi	$$⊢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)\leftrightarrow R\in \left\{1,7\right\}\right)\right)$$
51	1 50	syl5com	$$⊢\left(N\in \mathbb{Z}\wedge \neg 2\parallel N\right)\to \left(R=N\mathrm{mod}8\to \left(2\parallel \left(\frac{R^2-1}{8}\right)\leftrightarrow R\in \left\{1,7\right\}\right)\right)$$
52	51	3impia	$$⊢\left(N\in \mathbb{Z}\wedge \neg 2\parallel N\wedge R=N\mathrm{mod}8\right)\to \left(2\parallel \left(\frac{R^2-1}{8}\right)\leftrightarrow R\in \left\{1,7\right\}\right)$$