Theorem 2lgsoddprmlem3b

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

	Ref	Expression
Assertion	2lgsoddprmlem3b	|- ( ( ( 3 ^ 2 ) - 1 ) / 8 ) = 1

Proof

Step	Hyp	Ref	Expression
1		sq3	|- ( 3 ^ 2 ) = 9
2	1	oveq1i	|- ( ( 3 ^ 2 ) - 1 ) = ( 9 - 1 )
3		9m1e8	|- ( 9 - 1 ) = 8
4	2 3	eqtri	|- ( ( 3 ^ 2 ) - 1 ) = 8
5	4	oveq1i	|- ( ( ( 3 ^ 2 ) - 1 ) / 8 ) = ( 8 / 8 )
6		8cn	|- 8 e. CC
7		0re	|- 0 e. RR
8		8pos	|- 0 < 8
9	7 8	gtneii	|- 8 =/= 0
10	6 9	dividi	|- ( 8 / 8 ) = 1
11	5 10	eqtri	|- ( ( ( 3 ^ 2 ) - 1 ) / 8 ) = 1