Theorem 2lgsoddprmlem3a

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

	Ref	Expression
Assertion	2lgsoddprmlem3a	⊢ ( ( ( 1 ↑ 2 ) − 1 ) / 8 ) = 0

Proof

Step	Hyp	Ref	Expression
1		sq1	⊢ ( 1 ↑ 2 ) = 1
2	1	oveq1i	⊢ ( ( 1 ↑ 2 ) − 1 ) = ( 1 − 1 )
3		1m1e0	⊢ ( 1 − 1 ) = 0
4	2 3	eqtri	⊢ ( ( 1 ↑ 2 ) − 1 ) = 0
5	4	oveq1i	⊢ ( ( ( 1 ↑ 2 ) − 1 ) / 8 ) = ( 0 / 8 )
6		8cn	⊢ 8 ∈ ℂ
7		0re	⊢ 0 ∈ ℝ
8		8pos	⊢ 0 < 8
9	7 8	gtneii	⊢ 8 ≠ 0
10	6 9	div0i	⊢ ( 0 / 8 ) = 0
11	5 10	eqtri	⊢ ( ( ( 1 ↑ 2 ) − 1 ) / 8 ) = 0