Metamath Proof Explorer

Theorem sqoddm1div8

Description: A squared odd number minus 1 divided by 8 is the odd number multiplied with its successor divided by 2. (Contributed by AV, 19-Jul-2021)

Ref Expression
Assertion sqoddm1div8 ( ( 𝑁 ∈ ℤ ∧ 𝑀 = ( ( 2 · 𝑁 ) + 1 ) ) → ( ( ( 𝑀 ↑ 2 ) − 1 ) / 8 ) = ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑀 = ( ( 2 · 𝑁 ) + 1 ) → ( 𝑀 ↑ 2 ) = ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) )
2 2z ⊢ 2 ∈ ℤ
3 2 a1i ⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℤ )
4 id ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℤ )
5 3 4 zmulcld ⊢ ( 𝑁 ∈ ℤ → ( 2 · 𝑁 ) ∈ ℤ )
6 5 zcnd ⊢ ( 𝑁 ∈ ℤ → ( 2 · 𝑁 ) ∈ ℂ )
7 binom21 ⊢ ( ( 2 · 𝑁 ) ∈ ℂ → ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) = ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) + 1 ) )
8 6 7 syl ⊢ ( 𝑁 ∈ ℤ → ( ( ( 2 · 𝑁 ) + 1 ) ↑ 2 ) = ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) + 1 ) )
9 1 8 sylan9eqr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 = ( ( 2 · 𝑁 ) + 1 ) ) → ( 𝑀 ↑ 2 ) = ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) + 1 ) )
10 9 oveq1d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 = ( ( 2 · 𝑁 ) + 1 ) ) → ( ( 𝑀 ↑ 2 ) − 1 ) = ( ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) + 1 ) − 1 ) )
11 2cnd ⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℂ )
12 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
13 11 12 sqmuld ⊢ ( 𝑁 ∈ ℤ → ( ( 2 · 𝑁 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) )
14 sq2 ⊢ ( 2 ↑ 2 ) = 4
15 14 a1i ⊢ ( 𝑁 ∈ ℤ → ( 2 ↑ 2 ) = 4 )
16 15 oveq1d ⊢ ( 𝑁 ∈ ℤ → ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) = ( 4 · ( 𝑁 ↑ 2 ) ) )
17 13 16 eqtrd ⊢ ( 𝑁 ∈ ℤ → ( ( 2 · 𝑁 ) ↑ 2 ) = ( 4 · ( 𝑁 ↑ 2 ) ) )
18 mulass ⊢ ( ( 2 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 2 · 2 ) · 𝑁 ) = ( 2 · ( 2 · 𝑁 ) ) )
19 18 eqcomd ⊢ ( ( 2 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 2 · ( 2 · 𝑁 ) ) = ( ( 2 · 2 ) · 𝑁 ) )
20 11 11 12 19 syl3anc ⊢ ( 𝑁 ∈ ℤ → ( 2 · ( 2 · 𝑁 ) ) = ( ( 2 · 2 ) · 𝑁 ) )
21 2t2e4 ⊢ ( 2 · 2 ) = 4
22 21 a1i ⊢ ( 𝑁 ∈ ℤ → ( 2 · 2 ) = 4 )
23 22 oveq1d ⊢ ( 𝑁 ∈ ℤ → ( ( 2 · 2 ) · 𝑁 ) = ( 4 · 𝑁 ) )
24 20 23 eqtrd ⊢ ( 𝑁 ∈ ℤ → ( 2 · ( 2 · 𝑁 ) ) = ( 4 · 𝑁 ) )
25 17 24 oveq12d ⊢ ( 𝑁 ∈ ℤ → ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) = ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) )
26 25 oveq1d ⊢ ( 𝑁 ∈ ℤ → ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) + 1 ) = ( ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) + 1 ) )
27 26 oveq1d ⊢ ( 𝑁 ∈ ℤ → ( ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) + 1 ) − 1 ) = ( ( ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) + 1 ) − 1 ) )
28 4z ⊢ 4 ∈ ℤ
29 28 a1i ⊢ ( 𝑁 ∈ ℤ → 4 ∈ ℤ )
30 zsqcl ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ↑ 2 ) ∈ ℤ )
31 29 30 zmulcld ⊢ ( 𝑁 ∈ ℤ → ( 4 · ( 𝑁 ↑ 2 ) ) ∈ ℤ )
32 31 zcnd ⊢ ( 𝑁 ∈ ℤ → ( 4 · ( 𝑁 ↑ 2 ) ) ∈ ℂ )
33 29 4 zmulcld ⊢ ( 𝑁 ∈ ℤ → ( 4 · 𝑁 ) ∈ ℤ )
34 33 zcnd ⊢ ( 𝑁 ∈ ℤ → ( 4 · 𝑁 ) ∈ ℂ )
35 32 34 addcld ⊢ ( 𝑁 ∈ ℤ → ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) ∈ ℂ )
36 pncan1 ⊢ ( ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) ∈ ℂ → ( ( ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) + 1 ) − 1 ) = ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) )
37 35 36 syl ⊢ ( 𝑁 ∈ ℤ → ( ( ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) + 1 ) − 1 ) = ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) )
38 27 37 eqtrd ⊢ ( 𝑁 ∈ ℤ → ( ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) + 1 ) − 1 ) = ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) )
39 38 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 = ( ( 2 · 𝑁 ) + 1 ) ) → ( ( ( ( ( 2 · 𝑁 ) ↑ 2 ) + ( 2 · ( 2 · 𝑁 ) ) ) + 1 ) − 1 ) = ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) )
40 10 39 eqtrd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 = ( ( 2 · 𝑁 ) + 1 ) ) → ( ( 𝑀 ↑ 2 ) − 1 ) = ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) )
41 40 oveq1d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 = ( ( 2 · 𝑁 ) + 1 ) ) → ( ( ( 𝑀 ↑ 2 ) − 1 ) / 8 ) = ( ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) / 8 ) )
42 4cn ⊢ 4 ∈ ℂ
43 42 a1i ⊢ ( 𝑁 ∈ ℤ → 4 ∈ ℂ )
44 30 zcnd ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ↑ 2 ) ∈ ℂ )
45 43 44 12 adddid ⊢ ( 𝑁 ∈ ℤ → ( 4 · ( ( 𝑁 ↑ 2 ) + 𝑁 ) ) = ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) )
46 45 eqcomd ⊢ ( 𝑁 ∈ ℤ → ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) = ( 4 · ( ( 𝑁 ↑ 2 ) + 𝑁 ) ) )
47 46 oveq1d ⊢ ( 𝑁 ∈ ℤ → ( ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) / 8 ) = ( ( 4 · ( ( 𝑁 ↑ 2 ) + 𝑁 ) ) / 8 ) )
48 47 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 = ( ( 2 · 𝑁 ) + 1 ) ) → ( ( ( 4 · ( 𝑁 ↑ 2 ) ) + ( 4 · 𝑁 ) ) / 8 ) = ( ( 4 · ( ( 𝑁 ↑ 2 ) + 𝑁 ) ) / 8 ) )
49 4t2e8 ⊢ ( 4 · 2 ) = 8
50 49 a1i ⊢ ( 𝑁 ∈ ℤ → ( 4 · 2 ) = 8 )
51 50 eqcomd ⊢ ( 𝑁 ∈ ℤ → 8 = ( 4 · 2 ) )
52 51 oveq2d ⊢ ( 𝑁 ∈ ℤ → ( ( 4 · ( ( 𝑁 ↑ 2 ) + 𝑁 ) ) / 8 ) = ( ( 4 · ( ( 𝑁 ↑ 2 ) + 𝑁 ) ) / ( 4 · 2 ) ) )
53 30 4 zaddcld ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 ↑ 2 ) + 𝑁 ) ∈ ℤ )
54 53 zcnd ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 ↑ 2 ) + 𝑁 ) ∈ ℂ )
55 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
56 55 a1i ⊢ ( 𝑁 ∈ ℤ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
57 4ne0 ⊢ 4 ≠ 0
58 42 57 pm3.2i ⊢ ( 4 ∈ ℂ ∧ 4 ≠ 0 )
59 58 a1i ⊢ ( 𝑁 ∈ ℤ → ( 4 ∈ ℂ ∧ 4 ≠ 0 ) )
60 divcan5 ⊢ ( ( ( ( 𝑁 ↑ 2 ) + 𝑁 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ) → ( ( 4 · ( ( 𝑁 ↑ 2 ) + 𝑁 ) ) / ( 4 · 2 ) ) = ( ( ( 𝑁 ↑ 2 ) + 𝑁 ) / 2 ) )
61 54 56 59 60 syl3anc ⊢ ( 𝑁 ∈ ℤ → ( ( 4 · ( ( 𝑁 ↑ 2 ) + 𝑁 ) ) / ( 4 · 2 ) ) = ( ( ( 𝑁 ↑ 2 ) + 𝑁 ) / 2 ) )
62 12 sqvald ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ↑ 2 ) = ( 𝑁 · 𝑁 ) )
63 62 oveq1d ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 ↑ 2 ) + 𝑁 ) = ( ( 𝑁 · 𝑁 ) + 𝑁 ) )
64 12 mulridd ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 · 1 ) = 𝑁 )
65 64 eqcomd ⊢ ( 𝑁 ∈ ℤ → 𝑁 = ( 𝑁 · 1 ) )
66 65 oveq2d ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 · 𝑁 ) + 𝑁 ) = ( ( 𝑁 · 𝑁 ) + ( 𝑁 · 1 ) ) )
67 1cnd ⊢ ( 𝑁 ∈ ℤ → 1 ∈ ℂ )
68 adddi ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑁 · ( 𝑁 + 1 ) ) = ( ( 𝑁 · 𝑁 ) + ( 𝑁 · 1 ) ) )
69 68 eqcomd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 · 𝑁 ) + ( 𝑁 · 1 ) ) = ( 𝑁 · ( 𝑁 + 1 ) ) )
70 12 12 67 69 syl3anc ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 · 𝑁 ) + ( 𝑁 · 1 ) ) = ( 𝑁 · ( 𝑁 + 1 ) ) )
71 63 66 70 3eqtrd ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 ↑ 2 ) + 𝑁 ) = ( 𝑁 · ( 𝑁 + 1 ) ) )
72 71 oveq1d ⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑁 ↑ 2 ) + 𝑁 ) / 2 ) = ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) )
73 52 61 72 3eqtrd ⊢ ( 𝑁 ∈ ℤ → ( ( 4 · ( ( 𝑁 ↑ 2 ) + 𝑁 ) ) / 8 ) = ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) )
74 73 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 = ( ( 2 · 𝑁 ) + 1 ) ) → ( ( 4 · ( ( 𝑁 ↑ 2 ) + 𝑁 ) ) / 8 ) = ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) )
75 41 48 74 3eqtrd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 = ( ( 2 · 𝑁 ) + 1 ) ) → ( ( ( 𝑀 ↑ 2 ) − 1 ) / 8 ) = ( ( 𝑁 · ( 𝑁 + 1 ) ) / 2 ) )