Theorem 2lgsoddprmlem3a

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

	Ref	Expression
Assertion	2lgsoddprmlem3a	$$⊢\frac{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	$$⊢\frac{1^2-1}{8}=\frac{0}{8}$$
6		8cn	$$⊢8\in ℂ$$
7		0re	$$⊢0\in ℝ$$
8		8pos	$$⊢0<8$$
9	7 8	gtneii	$$⊢8\ne 0$$
10	6 9	div0i	$$⊢\frac{0}{8}=0$$
11	5 10	eqtri	$$⊢\frac{1^2-1}{8}=0$$