Metamath Proof Explorer

Theorem sqoddm1div8z

Description: A squared odd number minus 1 divided by 8 is an integer. (Contributed by AV, 19-Jul-2021)

Ref Expression
Assertion sqoddm1div8z ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N → N 2 − 1 8 ∈ ℤ

Proof

Step Hyp Ref Expression
1 odd2np1 ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ ∃ k ∈ ℤ 2 ⁢ k + 1 = N
2 1 biimpa ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N → ∃ k ∈ ℤ 2 ⁢ k + 1 = N
3 eqcom ⊢ 2 ⁢ k + 1 = N ↔ N = 2 ⁢ k + 1
4 sqoddm1div8 ⊢ k ∈ ℤ ∧ N = 2 ⁢ k + 1 → N 2 − 1 8 = k ⁢ k + 1 2
5 4 adantll ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N ∧ k ∈ ℤ ∧ N = 2 ⁢ k + 1 → N 2 − 1 8 = k ⁢ k + 1 2
6 mulsucdiv2z ⊢ k ∈ ℤ → k ⁢ k + 1 2 ∈ ℤ
7 6 ad2antlr ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N ∧ k ∈ ℤ ∧ N = 2 ⁢ k + 1 → k ⁢ k + 1 2 ∈ ℤ
8 5 7 eqeltrd ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N ∧ k ∈ ℤ ∧ N = 2 ⁢ k + 1 → N 2 − 1 8 ∈ ℤ
9 8 ex ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N ∧ k ∈ ℤ → N = 2 ⁢ k + 1 → N 2 − 1 8 ∈ ℤ
10 3 9 biimtrid ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N ∧ k ∈ ℤ → 2 ⁢ k + 1 = N → N 2 − 1 8 ∈ ℤ
11 10 rexlimdva ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N → ∃ k ∈ ℤ 2 ⁢ k + 1 = N → N 2 − 1 8 ∈ ℤ
12 2 11 mpd ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N → N 2 − 1 8 ∈ ℤ