2lgsoddprmlem4

		Ref	Expression
	Assertion	2lgsoddprmlem4	$⊢ (N \in ℤ \land \neg 2 ∥ N) \to (2 ∥ (\frac{N^{2} - 1}{8}) \leftrightarrow N \mod 8 \in \{1, 7\})$

Step	Hyp	Ref	Expression
1		eqidd	$⊢ (N \in ℤ \land \neg 2 ∥ N) \to N \mod 8 = N \mod 8$
2		2lgsoddprmlem2	$⊢ (N \in ℤ \land \neg 2 ∥ N \land N \mod 8 = N \mod 8) \to (2 ∥ (\frac{N^{2} - 1}{8}) \leftrightarrow 2 ∥ (\frac{{(N \mod 8)}^{2} - 1}{8}))$
3	1 2	mpd3an3	$⊢ (N \in ℤ \land \neg 2 ∥ N) \to (2 ∥ (\frac{N^{2} - 1}{8}) \leftrightarrow 2 ∥ (\frac{{(N \mod 8)}^{2} - 1}{8}))$
4		2lgsoddprmlem3	$⊢ (N \in ℤ \land \neg 2 ∥ N \land N \mod 8 = N \mod 8) \to (2 ∥ (\frac{{(N \mod 8)}^{2} - 1}{8}) \leftrightarrow N \mod 8 \in \{1, 7\})$
5	1 4	mpd3an3	$⊢ (N \in ℤ \land \neg 2 ∥ N) \to (2 ∥ (\frac{{(N \mod 8)}^{2} - 1}{8}) \leftrightarrow N \mod 8 \in \{1, 7\})$
6	3 5	bitrd	$⊢ (N \in ℤ \land \neg 2 ∥ N) \to (2 ∥ (\frac{N^{2} - 1}{8}) \leftrightarrow N \mod 8 \in \{1, 7\})$

Metamath Proof Explorer