Metamath Proof Explorer

Theorem 2lgsoddprmlem1

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

Ref Expression
Assertion 2lgsoddprmlem1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N = 8 ⁢ A + B → N 2 − 1 8 = 8 ⁢ A 2 + 2 ⁢ A ⁢ B + B 2 − 1 8

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ N = 8 ⁢ A + B → N 2 = 8 ⁢ A + B 2
2 1 3ad2ant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N = 8 ⁢ A + B → N 2 = 8 ⁢ A + B 2
3 2 oveq1d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N = 8 ⁢ A + B → N 2 − 1 = 8 ⁢ A + B 2 − 1
4 3 oveq1d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N = 8 ⁢ A + B → N 2 − 1 8 = 8 ⁢ A + B 2 − 1 8
5 zcn ⊢ A ∈ ℤ → A ∈ ℂ
6 5 adantr ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ∈ ℂ
7 zcn ⊢ B ∈ ℤ → B ∈ ℂ
8 7 adantl ⊢ A ∈ ℤ ∧ B ∈ ℤ → B ∈ ℂ
9 1cnd ⊢ A ∈ ℤ ∧ B ∈ ℤ → 1 ∈ ℂ
10 8cn ⊢ 8 ∈ ℂ
11 8re ⊢ 8 ∈ ℝ
12 8pos ⊢ 0 < 8
13 11 12 gt0ne0ii ⊢ 8 ≠ 0
14 10 13 pm3.2i ⊢ 8 ∈ ℂ ∧ 8 ≠ 0
15 14 a1i ⊢ A ∈ ℤ ∧ B ∈ ℤ → 8 ∈ ℂ ∧ 8 ≠ 0
16 mulsubdivbinom2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ 1 ∈ ℂ ∧ 8 ∈ ℂ ∧ 8 ≠ 0 → 8 ⁢ A + B 2 − 1 8 = 8 ⁢ A 2 + 2 ⁢ A ⁢ B + B 2 − 1 8
17 6 8 9 15 16 syl31anc ⊢ A ∈ ℤ ∧ B ∈ ℤ → 8 ⁢ A + B 2 − 1 8 = 8 ⁢ A 2 + 2 ⁢ A ⁢ B + B 2 − 1 8
18 17 3adant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N = 8 ⁢ A + B → 8 ⁢ A + B 2 − 1 8 = 8 ⁢ A 2 + 2 ⁢ A ⁢ B + B 2 − 1 8
19 4 18 eqtrd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N = 8 ⁢ A + B → N 2 − 1 8 = 8 ⁢ A 2 + 2 ⁢ A ⁢ B + B 2 − 1 8