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