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		2t4e8	$$⊢2\cdot 4=8$$
17	16	oveq1i	$$⊢2\cdot 4\cdot 3=8\cdot 3$$
18		2cn	$$⊢2\in ℂ$$
19	18 12 13	mulassi	$$⊢2\cdot 4\cdot 3=24\cdot 3$$
20	2 13	mulcomi	$$⊢8\cdot 3=3\cdot 8$$
21	17 19 20	3eqtr3i	$$⊢24\cdot 3=3\cdot 8$$
22	15 21	oveq12i	$$⊢4^2+24\cdot 3=2\cdot 8+3\cdot 8$$
23	18 13 2	adddiri	$$⊢\left(2+3\right)\cdot 8=2\cdot 8+3\cdot 8$$
24		3p2e5	$$⊢3+2=5$$
25	13 18 24	addcomli	$$⊢2+3=5$$
26	25	oveq1i	$$⊢\left(2+3\right)\cdot 8=5\cdot 8$$
27	22 23 26	3eqtr2i	$$⊢4^2+24\cdot 3=5\cdot 8$$
28		sq3	$$⊢3^2=9$$
29		df-9	$$⊢9=8+1$$
30	28 29	eqtri	$$⊢3^2=8+1$$
31	27 30	oveq12i	$$⊢4^2+24\cdot 3+3^2=5\cdot 8+8+1$$
32		5cn	$$⊢5\in ℂ$$
33	32 2	mulcli	$$⊢5\cdot 8\in ℂ$$
34	33 2 8	addassi	$$⊢5\cdot 8+8+1=5\cdot 8+8+1$$
35		df-6	$$⊢6=5+1$$
36	35	oveq1i	$$⊢6\cdot 8=\left(5+1\right)\cdot 8$$
37	32	a1i	$$⊢8\in ℂ\to 5\in ℂ$$
38		id	$$⊢8\in ℂ\to 8\in ℂ$$
39	37 38	adddirp1d	$$⊢8\in ℂ\to \left(5+1\right)\cdot 8=5\cdot 8+8$$
40	2 39	ax-mp	$$⊢\left(5+1\right)\cdot 8=5\cdot 8+8$$
41	36 40	eqtri	$$⊢6\cdot 8=5\cdot 8+8$$
42	41	eqcomi	$$⊢5\cdot 8+8=6\cdot 8$$
43	42	oveq1i	$$⊢5\cdot 8+8+1=6\cdot 8+1$$
44	31 34 43	3eqtr2i	$$⊢4^2+24\cdot 3+3^2=6\cdot 8+1$$
45	14 44	eqtri	$$⊢{\left(4+3\right)}^2=6\cdot 8+1$$
46	11 45	eqtri	$$⊢7^2=6\cdot 8+1$$
47	7 8 46	mvrraddi	$$⊢7^2-1=6\cdot 8$$
48	47	oveq1i	$$⊢\frac{7^2-1}{8}=\frac{6\cdot 8}{8}$$
49		2t3e6	$$⊢2\cdot 3=6$$
50	6 48 49	3eqtr4i	$$⊢\frac{7^2-1}{8}=2\cdot 3$$