Theorem 2lgsoddprmlem3d

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

	Ref	Expression
Assertion	2lgsoddprmlem3d	$$⊢\frac{7^2-1}{8}=2\cdot 3$$

Proof

Step	Hyp	Ref	Expression
1		6cn	$$⊢6\in ℂ$$
2		8cn	$$⊢8\in ℂ$$
3		0re	$$⊢0\in ℝ$$
4		8pos	$$⊢0<8$$
5	3 4	gtneii	$$⊢8\ne 0$$
6	1 2 5	divcan4i	$$⊢\frac{6\cdot 8}{8}=6$$
7	1 2	mulcli	$$⊢6\cdot 8\in ℂ$$
8		ax-1cn	$$⊢1\in ℂ$$
9		4p3e7	$$⊢4+3=7$$
10	9	eqcomi	$$⊢7=4+3$$
11	10	oveq1i	$$⊢7^2={\left(4+3\right)}^2$$
12		4cn	$$⊢4\in ℂ$$
13		3cn	$$⊢3\in ℂ$$
14	12 13	binom2i	$$⊢{\left(4+3\right)}^2=4^2+24\cdot 3+3^2$$
15		sq4e2t8	$$⊢4^2=2\cdot 8$$
16		2cn	$$⊢2\in ℂ$$
17		4t2e8	$$⊢4\cdot 2=8$$
18	12 16 17	mulcomli	$$⊢2\cdot 4=8$$
19	18	oveq1i	$$⊢2\cdot 4\cdot 3=8\cdot 3$$
20	16 12 13	mulassi	$$⊢2\cdot 4\cdot 3=24\cdot 3$$
21	2 13	mulcomi	$$⊢8\cdot 3=3\cdot 8$$
22	19 20 21	3eqtr3i	$$⊢24\cdot 3=3\cdot 8$$
23	15 22	oveq12i	$$⊢4^2+24\cdot 3=2\cdot 8+3\cdot 8$$
24	16 13 2	adddiri	$$⊢\left(2+3\right)\cdot 8=2\cdot 8+3\cdot 8$$
25		3p2e5	$$⊢3+2=5$$
26	13 16 25	addcomli	$$⊢2+3=5$$
27	26	oveq1i	$$⊢\left(2+3\right)\cdot 8=5\cdot 8$$
28	23 24 27	3eqtr2i	$$⊢4^2+24\cdot 3=5\cdot 8$$
29		sq3	$$⊢3^2=9$$
30		df-9	$$⊢9=8+1$$
31	29 30	eqtri	$$⊢3^2=8+1$$
32	28 31	oveq12i	$$⊢4^2+24\cdot 3+3^2=5\cdot 8+8+1$$
33		5cn	$$⊢5\in ℂ$$
34	33 2	mulcli	$$⊢5\cdot 8\in ℂ$$
35	34 2 8	addassi	$$⊢5\cdot 8+8+1=5\cdot 8+8+1$$
36		df-6	$$⊢6=5+1$$
37	36	oveq1i	$$⊢6\cdot 8=\left(5+1\right)\cdot 8$$
38	33	a1i	$$⊢8\in ℂ\to 5\in ℂ$$
39		id	$$⊢8\in ℂ\to 8\in ℂ$$
40	38 39	adddirp1d	$$⊢8\in ℂ\to \left(5+1\right)\cdot 8=5\cdot 8+8$$
41	2 40	ax-mp	$$⊢\left(5+1\right)\cdot 8=5\cdot 8+8$$
42	37 41	eqtri	$$⊢6\cdot 8=5\cdot 8+8$$
43	42	eqcomi	$$⊢5\cdot 8+8=6\cdot 8$$
44	43	oveq1i	$$⊢5\cdot 8+8+1=6\cdot 8+1$$
45	32 35 44	3eqtr2i	$$⊢4^2+24\cdot 3+3^2=6\cdot 8+1$$
46	14 45	eqtri	$$⊢{\left(4+3\right)}^2=6\cdot 8+1$$
47	11 46	eqtri	$$⊢7^2=6\cdot 8+1$$
48	7 8 47	mvrraddi	$$⊢7^2-1=6\cdot 8$$
49	48	oveq1i	$$⊢\frac{7^2-1}{8}=\frac{6\cdot 8}{8}$$
50		3t2e6	$$⊢3\cdot 2=6$$
51	13 16 50	mulcomli	$$⊢2\cdot 3=6$$
52	6 49 51	3eqtr4i	$$⊢\frac{7^2-1}{8}=2\cdot 3$$