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	$⊢ (N \in ℤ \land M = 2 \cdot N + 1) \to \frac{M^{2} - 1}{8} = \frac{N (N + 1)}{2}$

Proof

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

Metamath Proof Explorer

Theorem sqoddm1div8

Proof