# Metamath Proof Explorer

## Theorem 2lgsoddprmlem1

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

Ref Expression
Assertion 2lgsoddprmlem1 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {N}=8{A}+{B}\right)\to \frac{{{N}}^{2}-1}{8}=8{{A}}^{2}+2{A}{B}+\left(\frac{{{B}}^{2}-1}{8}\right)$

### Proof

Step Hyp Ref Expression
1 oveq1 ${⊢}{N}=8{A}+{B}\to {{N}}^{2}={\left(8{A}+{B}\right)}^{2}$
2 1 3ad2ant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {N}=8{A}+{B}\right)\to {{N}}^{2}={\left(8{A}+{B}\right)}^{2}$
3 2 oveq1d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {N}=8{A}+{B}\right)\to {{N}}^{2}-1={\left(8{A}+{B}\right)}^{2}-1$
4 3 oveq1d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {N}=8{A}+{B}\right)\to \frac{{{N}}^{2}-1}{8}=\frac{{\left(8{A}+{B}\right)}^{2}-1}{8}$
5 zcn ${⊢}{A}\in ℤ\to {A}\in ℂ$
6 5 adantr ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}\in ℂ$
7 zcn ${⊢}{B}\in ℤ\to {B}\in ℂ$
8 7 adantl ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {B}\in ℂ$
9 1cnd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to 1\in ℂ$
10 8cn ${⊢}8\in ℂ$
11 8re ${⊢}8\in ℝ$
12 8pos ${⊢}0<8$
13 11 12 gt0ne0ii ${⊢}8\ne 0$
14 10 13 pm3.2i ${⊢}\left(8\in ℂ\wedge 8\ne 0\right)$
15 14 a1i ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left(8\in ℂ\wedge 8\ne 0\right)$
16 mulsubdivbinom2 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge 1\in ℂ\right)\wedge \left(8\in ℂ\wedge 8\ne 0\right)\right)\to \frac{{\left(8{A}+{B}\right)}^{2}-1}{8}=8{{A}}^{2}+2{A}{B}+\left(\frac{{{B}}^{2}-1}{8}\right)$
17 6 8 9 15 16 syl31anc ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \frac{{\left(8{A}+{B}\right)}^{2}-1}{8}=8{{A}}^{2}+2{A}{B}+\left(\frac{{{B}}^{2}-1}{8}\right)$
18 17 3adant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {N}=8{A}+{B}\right)\to \frac{{\left(8{A}+{B}\right)}^{2}-1}{8}=8{{A}}^{2}+2{A}{B}+\left(\frac{{{B}}^{2}-1}{8}\right)$
19 4 18 eqtrd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {N}=8{A}+{B}\right)\to \frac{{{N}}^{2}-1}{8}=8{{A}}^{2}+2{A}{B}+\left(\frac{{{B}}^{2}-1}{8}\right)$