Metamath Proof Explorer


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 ) ) )