Theorem 2lgsoddprmlem1

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

	Ref	Expression
Assertion	2lgsoddprmlem1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 = ( ( 8 · 𝐴 ) + 𝐵 ) ) → ( ( ( 𝑁 ↑ 2 ) − 1 ) / 8 ) = ( ( ( 8 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( ( ( 𝐵 ↑ 2 ) − 1 ) / 8 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑁 = ( ( 8 · 𝐴 ) + 𝐵 ) → ( 𝑁 ↑ 2 ) = ( ( ( 8 · 𝐴 ) + 𝐵 ) ↑ 2 ) )
2	1	3ad2ant3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 = ( ( 8 · 𝐴 ) + 𝐵 ) ) → ( 𝑁 ↑ 2 ) = ( ( ( 8 · 𝐴 ) + 𝐵 ) ↑ 2 ) )
3	2	oveq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 = ( ( 8 · 𝐴 ) + 𝐵 ) ) → ( ( 𝑁 ↑ 2 ) − 1 ) = ( ( ( ( 8 · 𝐴 ) + 𝐵 ) ↑ 2 ) − 1 ) )
4	3	oveq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 = ( ( 8 · 𝐴 ) + 𝐵 ) ) → ( ( ( 𝑁 ↑ 2 ) − 1 ) / 8 ) = ( ( ( ( ( 8 · 𝐴 ) + 𝐵 ) ↑ 2 ) − 1 ) / 8 ) )
5		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
6	5	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℂ )
7		zcn	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
8	7	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℂ )
9		1cnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 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	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 8 ∈ ℂ ∧ 8 ≠ 0 ) )
16		mulsubdivbinom2	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 1 ∈ ℂ ) ∧ ( 8 ∈ ℂ ∧ 8 ≠ 0 ) ) → ( ( ( ( ( 8 · 𝐴 ) + 𝐵 ) ↑ 2 ) − 1 ) / 8 ) = ( ( ( 8 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( ( ( 𝐵 ↑ 2 ) − 1 ) / 8 ) ) )
17	6 8 9 15 16	syl31anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( ( ( 8 · 𝐴 ) + 𝐵 ) ↑ 2 ) − 1 ) / 8 ) = ( ( ( 8 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( ( ( 𝐵 ↑ 2 ) − 1 ) / 8 ) ) )
18	17	3adant3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 = ( ( 8 · 𝐴 ) + 𝐵 ) ) → ( ( ( ( ( 8 · 𝐴 ) + 𝐵 ) ↑ 2 ) − 1 ) / 8 ) = ( ( ( 8 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( ( ( 𝐵 ↑ 2 ) − 1 ) / 8 ) ) )
19	4 18	eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 = ( ( 8 · 𝐴 ) + 𝐵 ) ) → ( ( ( 𝑁 ↑ 2 ) − 1 ) / 8 ) = ( ( ( 8 · ( 𝐴 ↑ 2 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( ( ( 𝐵 ↑ 2 ) − 1 ) / 8 ) ) )