Theorem 2lgsoddprmlem3c

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

	Ref	Expression
Assertion	2lgsoddprmlem3c	⊢ ( ( ( 5 ↑ 2 ) − 1 ) / 8 ) = 3

Proof

Step	Hyp	Ref	Expression
1		df-5	⊢ 5 = ( 4 + 1 )
2	1	oveq1i	⊢ ( 5 ↑ 2 ) = ( ( 4 + 1 ) ↑ 2 )
3		4cn	⊢ 4 ∈ ℂ
4		binom21	⊢ ( 4 ∈ ℂ → ( ( 4 + 1 ) ↑ 2 ) = ( ( ( 4 ↑ 2 ) + ( 2 · 4 ) ) + 1 ) )
5	3 4	ax-mp	⊢ ( ( 4 + 1 ) ↑ 2 ) = ( ( ( 4 ↑ 2 ) + ( 2 · 4 ) ) + 1 )
6	2 5	eqtri	⊢ ( 5 ↑ 2 ) = ( ( ( 4 ↑ 2 ) + ( 2 · 4 ) ) + 1 )
7	6	oveq1i	⊢ ( ( 5 ↑ 2 ) − 1 ) = ( ( ( ( 4 ↑ 2 ) + ( 2 · 4 ) ) + 1 ) − 1 )
8		3cn	⊢ 3 ∈ ℂ
9		8cn	⊢ 8 ∈ ℂ
10	8 9	mulcli	⊢ ( 3 · 8 ) ∈ ℂ
11		ax-1cn	⊢ 1 ∈ ℂ
12		sq4e2t8	⊢ ( 4 ↑ 2 ) = ( 2 · 8 )
13		2cn	⊢ 2 ∈ ℂ
14		4t2e8	⊢ ( 4 · 2 ) = 8
15	9	mulid2i	⊢ ( 1 · 8 ) = 8
16	14 15	eqtr4i	⊢ ( 4 · 2 ) = ( 1 · 8 )
17	3 13 16	mulcomli	⊢ ( 2 · 4 ) = ( 1 · 8 )
18	12 17	oveq12i	⊢ ( ( 4 ↑ 2 ) + ( 2 · 4 ) ) = ( ( 2 · 8 ) + ( 1 · 8 ) )
19	13 11 9	adddiri	⊢ ( ( 2 + 1 ) · 8 ) = ( ( 2 · 8 ) + ( 1 · 8 ) )
20		2p1e3	⊢ ( 2 + 1 ) = 3
21	20	oveq1i	⊢ ( ( 2 + 1 ) · 8 ) = ( 3 · 8 )
22	18 19 21	3eqtr2i	⊢ ( ( 4 ↑ 2 ) + ( 2 · 4 ) ) = ( 3 · 8 )
23	22	oveq1i	⊢ ( ( ( 4 ↑ 2 ) + ( 2 · 4 ) ) + 1 ) = ( ( 3 · 8 ) + 1 )
24	10 11 23	mvrraddi	⊢ ( ( ( ( 4 ↑ 2 ) + ( 2 · 4 ) ) + 1 ) − 1 ) = ( 3 · 8 )
25	7 24	eqtri	⊢ ( ( 5 ↑ 2 ) − 1 ) = ( 3 · 8 )
26	25	oveq1i	⊢ ( ( ( 5 ↑ 2 ) − 1 ) / 8 ) = ( ( 3 · 8 ) / 8 )
27		0re	⊢ 0 ∈ ℝ
28		8pos	⊢ 0 < 8
29	27 28	gtneii	⊢ 8 ≠ 0
30	8 9 29	divcan4i	⊢ ( ( 3 · 8 ) / 8 ) = 3
31	26 30	eqtri	⊢ ( ( ( 5 ↑ 2 ) − 1 ) / 8 ) = 3