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