Theorem 2lgsoddprmlem3c

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

	Ref	Expression
Assertion	2lgsoddprmlem3c	$$⊢\frac{5^2-1}{8}=3$$

Proof

Step	Hyp	Ref	Expression
1		df-5	$$⊢5=4+1$$
2	1	oveq1i	$$⊢5^2={\left(4+1\right)}^2$$
3		4cn	$$⊢4\in ℂ$$
4		binom21	$$⊢4\in ℂ\to {\left(4+1\right)}^2=4^2+2\cdot 4+1$$
5	3 4	ax-mp	$$⊢{\left(4+1\right)}^2=4^2+2\cdot 4+1$$
6	2 5	eqtri	$$⊢5^2=4^2+2\cdot 4+1$$
7	6	oveq1i	$$⊢5^2-1=\left(4^2+2\cdot 4\right)+1-1$$
8		3cn	$$⊢3\in ℂ$$
9		8cn	$$⊢8\in ℂ$$
10	8 9	mulcli	$$⊢3\cdot 8\in ℂ$$
11		ax-1cn	$$⊢1\in ℂ$$
12		sq4e2t8	$$⊢4^2=2\cdot 8$$
13		2cn	$$⊢2\in ℂ$$
14		4t2e8	$$⊢4\cdot 2=8$$
15	9	mullidi	$$⊢1\cdot 8=8$$
16	14 15	eqtr4i	$$⊢4\cdot 2=1\cdot 8$$
17	3 13 16	mulcomli	$$⊢2\cdot 4=1\cdot 8$$
18	12 17	oveq12i	$$⊢4^2+2\cdot 4=2\cdot 8+1\cdot 8$$
19	13 11 9	adddiri	$$⊢\left(2+1\right)\cdot 8=2\cdot 8+1\cdot 8$$
20		2p1e3	$$⊢2+1=3$$
21	20	oveq1i	$$⊢\left(2+1\right)\cdot 8=3\cdot 8$$
22	18 19 21	3eqtr2i	$$⊢4^2+2\cdot 4=3\cdot 8$$
23	22	oveq1i	$$⊢4^2+2\cdot 4+1=3\cdot 8+1$$
24	10 11 23	mvrraddi	$$⊢\left(4^2+2\cdot 4\right)+1-1=3\cdot 8$$
25	7 24	eqtri	$$⊢5^2-1=3\cdot 8$$
26	25	oveq1i	$$⊢\frac{5^2-1}{8}=\frac{3\cdot 8}{8}$$
27		0re	$$⊢0\in ℝ$$
28		8pos	$$⊢0<8$$
29	27 28	gtneii	$$⊢8\ne 0$$
30	8 9 29	divcan4i	$$⊢\frac{3\cdot 8}{8}=3$$
31	26 30	eqtri	$$⊢\frac{5^2-1}{8}=3$$