# Metamath Proof Explorer

## Theorem 2lgsoddprmlem4

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

Ref Expression
Assertion 2lgsoddprmlem4 ${⊢}\left({N}\in ℤ\wedge ¬2\parallel {N}\right)\to \left(2\parallel \left(\frac{{{N}}^{2}-1}{8}\right)↔{N}\mathrm{mod}8\in \left\{1,7\right\}\right)$

### Proof

Step Hyp Ref Expression
1 eqidd ${⊢}\left({N}\in ℤ\wedge ¬2\parallel {N}\right)\to {N}\mathrm{mod}8={N}\mathrm{mod}8$
2 2lgsoddprmlem2 ${⊢}\left({N}\in ℤ\wedge ¬2\parallel {N}\wedge {N}\mathrm{mod}8={N}\mathrm{mod}8\right)\to \left(2\parallel \left(\frac{{{N}}^{2}-1}{8}\right)↔2\parallel \left(\frac{{\left({N}\mathrm{mod}8\right)}^{2}-1}{8}\right)\right)$
3 1 2 mpd3an3 ${⊢}\left({N}\in ℤ\wedge ¬2\parallel {N}\right)\to \left(2\parallel \left(\frac{{{N}}^{2}-1}{8}\right)↔2\parallel \left(\frac{{\left({N}\mathrm{mod}8\right)}^{2}-1}{8}\right)\right)$
4 2lgsoddprmlem3 ${⊢}\left({N}\in ℤ\wedge ¬2\parallel {N}\wedge {N}\mathrm{mod}8={N}\mathrm{mod}8\right)\to \left(2\parallel \left(\frac{{\left({N}\mathrm{mod}8\right)}^{2}-1}{8}\right)↔{N}\mathrm{mod}8\in \left\{1,7\right\}\right)$
5 1 4 mpd3an3 ${⊢}\left({N}\in ℤ\wedge ¬2\parallel {N}\right)\to \left(2\parallel \left(\frac{{\left({N}\mathrm{mod}8\right)}^{2}-1}{8}\right)↔{N}\mathrm{mod}8\in \left\{1,7\right\}\right)$
6 3 5 bitrd ${⊢}\left({N}\in ℤ\wedge ¬2\parallel {N}\right)\to \left(2\parallel \left(\frac{{{N}}^{2}-1}{8}\right)↔{N}\mathrm{mod}8\in \left\{1,7\right\}\right)$