zesq

Description: An integer is even iff its square is even. (Contributed by Mario Carneiro, 12-Sep-2015)

		Ref	Expression
	Assertion	zesq	$⊢ N \in ℤ \to (\frac{N}{2} \in ℤ \leftrightarrow \frac{N^{2}}{2} \in ℤ)$

Proof

Step	Hyp	Ref	Expression
1		zcn	$⊢ N \in ℤ \to N \in ℂ$
2		sqval	$⊢ N \in ℂ \to N^{2} = N \cdot N$
3	1 2	syl	$⊢ N \in ℤ \to N^{2} = N \cdot N$
4	3	oveq1d	$⊢ N \in ℤ \to \frac{N^{2}}{2} = \frac{N \cdot N}{2}$
5		2cnd	$⊢ N \in ℤ \to 2 \in ℂ$
6		2ne0	$⊢ 2 \neq 0$
7	6	a1i	$⊢ N \in ℤ \to 2 \neq 0$
8	1 1 5 7	divassd	$⊢ N \in ℤ \to \frac{N \cdot N}{2} = N (\frac{N}{2})$
9	4 8	eqtrd	$⊢ N \in ℤ \to \frac{N^{2}}{2} = N (\frac{N}{2})$
10	9	adantr	$⊢ (N \in ℤ \land \frac{N}{2} \in ℤ) \to \frac{N^{2}}{2} = N (\frac{N}{2})$
11		zmulcl	$⊢ (N \in ℤ \land \frac{N}{2} \in ℤ) \to N (\frac{N}{2}) \in ℤ$
12	10 11	eqeltrd	$⊢ (N \in ℤ \land \frac{N}{2} \in ℤ) \to \frac{N^{2}}{2} \in ℤ$
13	1	adantr	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to N \in ℂ$
14		sqcl	$⊢ N \in ℂ \to N^{2} \in ℂ$
15	13 14	syl	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to N^{2} \in ℂ$
16		peano2cn	$⊢ N^{2} \in ℂ \to N^{2} + 1 \in ℂ$
17	15 16	syl	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to N^{2} + 1 \in ℂ$
18	17	halfcld	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to \frac{N^{2} + 1}{2} \in ℂ$
19	18 13	pncand	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to (\frac{N^{2} + 1}{2}) + N - N = \frac{N^{2} + 1}{2}$
20		binom21	$⊢ N \in ℂ \to {(N + 1)}^{2} = N^{2} + 2 \cdot N + 1$
21	13 20	syl	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to {(N + 1)}^{2} = N^{2} + 2 \cdot N + 1$
22		peano2cn	$⊢ N \in ℂ \to N + 1 \in ℂ$
23	13 22	syl	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to N + 1 \in ℂ$
24		sqval	$⊢ N + 1 \in ℂ \to {(N + 1)}^{2} = (N + 1) (N + 1)$
25	23 24	syl	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to {(N + 1)}^{2} = (N + 1) (N + 1)$
26		2cn	$⊢ 2 \in ℂ$
27		mulcl	$⊢ (2 \in ℂ \land N \in ℂ) \to 2 \cdot N \in ℂ$
28	26 13 27	sylancr	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to 2 \cdot N \in ℂ$
29		1cnd	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to 1 \in ℂ$
30	15 28 29	add32d	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to N^{2} + 2 \cdot N + 1 = N^{2} + 1 + 2 \cdot N$
31	21 25 30	3eqtr3d	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to (N + 1) (N + 1) = N^{2} + 1 + 2 \cdot N$
32	31	oveq1d	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to \frac{(N + 1) (N + 1)}{2} = \frac{N^{2} + 1 + 2 \cdot N}{2}$
33		2cnd	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to 2 \in ℂ$
34	6	a1i	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to 2 \neq 0$
35	23 23 33 34	divassd	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to \frac{(N + 1) (N + 1)}{2} = (N + 1) (\frac{N + 1}{2})$
36	17 28 33 34	divdird	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to \frac{N^{2} + 1 + 2 \cdot N}{2} = (\frac{N^{2} + 1}{2}) + (\frac{2 \cdot N}{2})$
37	13 33 34	divcan3d	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to \frac{2 \cdot N}{2} = N$
38	37	oveq2d	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to (\frac{N^{2} + 1}{2}) + (\frac{2 \cdot N}{2}) = (\frac{N^{2} + 1}{2}) + N$
39	36 38	eqtrd	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to \frac{N^{2} + 1 + 2 \cdot N}{2} = (\frac{N^{2} + 1}{2}) + N$
40	32 35 39	3eqtr3d	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to (N + 1) (\frac{N + 1}{2}) = (\frac{N^{2} + 1}{2}) + N$
41		peano2z	$⊢ N \in ℤ \to N + 1 \in ℤ$
42		zmulcl	$⊢ (N + 1 \in ℤ \land \frac{N + 1}{2} \in ℤ) \to (N + 1) (\frac{N + 1}{2}) \in ℤ$
43	41 42	sylan	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to (N + 1) (\frac{N + 1}{2}) \in ℤ$
44	40 43	eqeltrrd	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to (\frac{N^{2} + 1}{2}) + N \in ℤ$
45		simpl	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to N \in ℤ$
46	44 45	zsubcld	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to (\frac{N^{2} + 1}{2}) + N - N \in ℤ$
47	19 46	eqeltrrd	$⊢ (N \in ℤ \land \frac{N + 1}{2} \in ℤ) \to \frac{N^{2} + 1}{2} \in ℤ$
48	47	ex	$⊢ N \in ℤ \to (\frac{N + 1}{2} \in ℤ \to \frac{N^{2} + 1}{2} \in ℤ)$
49	48	con3d	$⊢ N \in ℤ \to (\neg \frac{N^{2} + 1}{2} \in ℤ \to \neg \frac{N + 1}{2} \in ℤ)$
50		zsqcl	$⊢ N \in ℤ \to N^{2} \in ℤ$
51		zeo2	$⊢ N^{2} \in ℤ \to (\frac{N^{2}}{2} \in ℤ \leftrightarrow \neg \frac{N^{2} + 1}{2} \in ℤ)$
52	50 51	syl	$⊢ N \in ℤ \to (\frac{N^{2}}{2} \in ℤ \leftrightarrow \neg \frac{N^{2} + 1}{2} \in ℤ)$
53		zeo2	$⊢ N \in ℤ \to (\frac{N}{2} \in ℤ \leftrightarrow \neg \frac{N + 1}{2} \in ℤ)$
54	49 52 53	3imtr4d	$⊢ N \in ℤ \to (\frac{N^{2}}{2} \in ℤ \to \frac{N}{2} \in ℤ)$
55	54	imp	$⊢ (N \in ℤ \land \frac{N^{2}}{2} \in ℤ) \to \frac{N}{2} \in ℤ$
56	12 55	impbida	$⊢ N \in ℤ \to (\frac{N}{2} \in ℤ \leftrightarrow \frac{N^{2}}{2} \in ℤ)$

Metamath Proof Explorer

Theorem zesq

Proof