Metamath Proof Explorer

Theorem 2lgsoddprmlem4

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

Ref Expression
Assertion 2lgsoddprmlem4 ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N → 2 ∥ N 2 − 1 8 ↔ N mod 8 ∈ 1 7

Proof

Step Hyp Ref Expression
1 eqidd ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N → N mod 8 = N mod 8
2 2lgsoddprmlem2 ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N ∧ N mod 8 = N mod 8 → 2 ∥ N 2 − 1 8 ↔ 2 ∥ N mod 8 2 − 1 8
3 1 2 mpd3an3 ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N → 2 ∥ N 2 − 1 8 ↔ 2 ∥ N mod 8 2 − 1 8
4 2lgsoddprmlem3 ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N ∧ N mod 8 = N mod 8 → 2 ∥ N mod 8 2 − 1 8 ↔ N mod 8 ∈ 1 7
5 1 4 mpd3an3 ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N → 2 ∥ N mod 8 2 − 1 8 ↔ N mod 8 ∈ 1 7
6 3 5 bitrd ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N → 2 ∥ N 2 − 1 8 ↔ N mod 8 ∈ 1 7