mod2eq1n2dvds

Description: An integer is 1 modulo 2 iff it is odd (i.e. not divisible by 2), see example 3 in ApostolNT p. 107. (Contributed by AV, 24-May-2020) (Proof shortened by AV, 5-Jul-2020)

		Ref	Expression
	Assertion	mod2eq1n2dvds	$⊢ N \in ℤ \to (N \mod 2 = 1 \leftrightarrow \neg 2 ∥ N)$

Proof

Step	Hyp	Ref	Expression
1		zeo	$⊢ N \in ℤ \to (\frac{N}{2} \in ℤ \lor \frac{N + 1}{2} \in ℤ)$
2		zre	$⊢ N \in ℤ \to N \in ℝ$
3		2rp	$⊢ 2 \in ℝ^{+}$
4		mod0	$⊢ (N \in ℝ \land 2 \in ℝ^{+}) \to (N \mod 2 = 0 \leftrightarrow \frac{N}{2} \in ℤ)$
5	2 3 4	sylancl	$⊢ N \in ℤ \to (N \mod 2 = 0 \leftrightarrow \frac{N}{2} \in ℤ)$
6	5	biimpar	$⊢ (N \in ℤ \land \frac{N}{2} \in ℤ) \to N \mod 2 = 0$
7		eqeq1	$⊢ N \mod 2 = 0 \to (N \mod 2 = 1 \leftrightarrow 0 = 1)$
8		0ne1	$⊢ 0 \neq 1$
9		eqneqall	$⊢ 0 = 1 \to (0 \neq 1 \to \exists n \in ℤ 2 n + 1 = N)$
10	8 9	mpi	$⊢ 0 = 1 \to \exists n \in ℤ 2 n + 1 = N$
11	7 10	biimtrdi	$⊢ N \mod 2 = 0 \to (N \mod 2 = 1 \to \exists n \in ℤ 2 n + 1 = N)$
12	6 11	syl	$⊢ (N \in ℤ \land \frac{N}{2} \in ℤ) \to (N \mod 2 = 1 \to \exists n \in ℤ 2 n + 1 = N)$
13	12	expcom	$⊢ \frac{N}{2} \in ℤ \to (N \in ℤ \to (N \mod 2 = 1 \to \exists n \in ℤ 2 n + 1 = N))$
14		peano2zm	$⊢ \frac{N + 1}{2} \in ℤ \to (\frac{N + 1}{2}) - 1 \in ℤ$
15		zcn	$⊢ N \in ℤ \to N \in ℂ$
16		xp1d2m1eqxm1d2	$⊢ N \in ℂ \to (\frac{N + 1}{2}) - 1 = \frac{N - 1}{2}$
17	15 16	syl	$⊢ N \in ℤ \to (\frac{N + 1}{2}) - 1 = \frac{N - 1}{2}$
18	17	eleq1d	$⊢ N \in ℤ \to ((\frac{N + 1}{2}) - 1 \in ℤ \leftrightarrow \frac{N - 1}{2} \in ℤ)$
19	18	biimpd	$⊢ N \in ℤ \to ((\frac{N + 1}{2}) - 1 \in ℤ \to \frac{N - 1}{2} \in ℤ)$
20	14 19	mpan9	$⊢ (\frac{N + 1}{2} \in ℤ \land N \in ℤ) \to \frac{N - 1}{2} \in ℤ$
21		oveq2	$⊢ n = \frac{N - 1}{2} \to 2 n = 2 (\frac{N - 1}{2})$
22	21	adantl	$⊢ ((\frac{N + 1}{2} \in ℤ \land N \in ℤ) \land n = \frac{N - 1}{2}) \to 2 n = 2 (\frac{N - 1}{2})$
23	22	oveq1d	$⊢ ((\frac{N + 1}{2} \in ℤ \land N \in ℤ) \land n = \frac{N - 1}{2}) \to 2 n + 1 = 2 (\frac{N - 1}{2}) + 1$
24		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
25	24	zcnd	$⊢ N \in ℤ \to N - 1 \in ℂ$
26		2cnd	$⊢ N \in ℤ \to 2 \in ℂ$
27		2ne0	$⊢ 2 \neq 0$
28	27	a1i	$⊢ N \in ℤ \to 2 \neq 0$
29	25 26 28	divcan2d	$⊢ N \in ℤ \to 2 (\frac{N - 1}{2}) = N - 1$
30	29	oveq1d	$⊢ N \in ℤ \to 2 (\frac{N - 1}{2}) + 1 = N - 1 + 1$
31		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
32	15 31	syl	$⊢ N \in ℤ \to N - 1 + 1 = N$
33	30 32	eqtrd	$⊢ N \in ℤ \to 2 (\frac{N - 1}{2}) + 1 = N$
34	33	ad2antlr	$⊢ ((\frac{N + 1}{2} \in ℤ \land N \in ℤ) \land n = \frac{N - 1}{2}) \to 2 (\frac{N - 1}{2}) + 1 = N$
35	23 34	eqtrd	$⊢ ((\frac{N + 1}{2} \in ℤ \land N \in ℤ) \land n = \frac{N - 1}{2}) \to 2 n + 1 = N$
36	20 35	rspcedeqvd	$⊢ (\frac{N + 1}{2} \in ℤ \land N \in ℤ) \to \exists n \in ℤ 2 n + 1 = N$
37	36	a1d	$⊢ (\frac{N + 1}{2} \in ℤ \land N \in ℤ) \to (N \mod 2 = 1 \to \exists n \in ℤ 2 n + 1 = N)$
38	37	ex	$⊢ \frac{N + 1}{2} \in ℤ \to (N \in ℤ \to (N \mod 2 = 1 \to \exists n \in ℤ 2 n + 1 = N))$
39	13 38	jaoi	$⊢ (\frac{N}{2} \in ℤ \lor \frac{N + 1}{2} \in ℤ) \to (N \in ℤ \to (N \mod 2 = 1 \to \exists n \in ℤ 2 n + 1 = N))$
40	1 39	mpcom	$⊢ N \in ℤ \to (N \mod 2 = 1 \to \exists n \in ℤ 2 n + 1 = N)$
41		oveq1	$⊢ N = 2 n + 1 \to N \mod 2 = (2 n + 1) \mod 2$
42	41	eqcoms	$⊢ 2 n + 1 = N \to N \mod 2 = (2 n + 1) \mod 2$
43		2cnd	$⊢ n \in ℤ \to 2 \in ℂ$
44		zcn	$⊢ n \in ℤ \to n \in ℂ$
45	43 44	mulcomd	$⊢ n \in ℤ \to 2 n = n \cdot 2$
46	45	oveq1d	$⊢ n \in ℤ \to 2 n \mod 2 = n \cdot 2 \mod 2$
47		mulmod0	$⊢ (n \in ℤ \land 2 \in ℝ^{+}) \to n \cdot 2 \mod 2 = 0$
48	3 47	mpan2	$⊢ n \in ℤ \to n \cdot 2 \mod 2 = 0$
49	46 48	eqtrd	$⊢ n \in ℤ \to 2 n \mod 2 = 0$
50	49	oveq1d	$⊢ n \in ℤ \to (2 n \mod 2) + 1 = 0 + 1$
51		0p1e1	$⊢ 0 + 1 = 1$
52	50 51	eqtrdi	$⊢ n \in ℤ \to (2 n \mod 2) + 1 = 1$
53	52	oveq1d	$⊢ n \in ℤ \to ((2 n \mod 2) + 1) \mod 2 = 1 \mod 2$
54		2z	$⊢ 2 \in ℤ$
55	54	a1i	$⊢ n \in ℤ \to 2 \in ℤ$
56		id	$⊢ n \in ℤ \to n \in ℤ$
57	55 56	zmulcld	$⊢ n \in ℤ \to 2 n \in ℤ$
58	57	zred	$⊢ n \in ℤ \to 2 n \in ℝ$
59		1red	$⊢ n \in ℤ \to 1 \in ℝ$
60	3	a1i	$⊢ n \in ℤ \to 2 \in ℝ^{+}$
61		modaddmod	$⊢ (2 n \in ℝ \land 1 \in ℝ \land 2 \in ℝ^{+}) \to ((2 n \mod 2) + 1) \mod 2 = (2 n + 1) \mod 2$
62	58 59 60 61	syl3anc	$⊢ n \in ℤ \to ((2 n \mod 2) + 1) \mod 2 = (2 n + 1) \mod 2$
63		2re	$⊢ 2 \in ℝ$
64		1lt2	$⊢ 1 < 2$
65	63 64	pm3.2i	$⊢ (2 \in ℝ \land 1 < 2)$
66		1mod	$⊢ (2 \in ℝ \land 1 < 2) \to 1 \mod 2 = 1$
67	65 66	mp1i	$⊢ n \in ℤ \to 1 \mod 2 = 1$
68	53 62 67	3eqtr3d	$⊢ n \in ℤ \to (2 n + 1) \mod 2 = 1$
69	68	adantl	$⊢ (N \in ℤ \land n \in ℤ) \to (2 n + 1) \mod 2 = 1$
70	42 69	sylan9eqr	$⊢ ((N \in ℤ \land n \in ℤ) \land 2 n + 1 = N) \to N \mod 2 = 1$
71	70	rexlimdva2	$⊢ N \in ℤ \to (\exists n \in ℤ 2 n + 1 = N \to N \mod 2 = 1)$
72	40 71	impbid	$⊢ N \in ℤ \to (N \mod 2 = 1 \leftrightarrow \exists n \in ℤ 2 n + 1 = N)$
73		odd2np1	$⊢ N \in ℤ \to (\neg 2 ∥ N \leftrightarrow \exists n \in ℤ 2 n + 1 = N)$
74	72 73	bitr4d	$⊢ N \in ℤ \to (N \mod 2 = 1 \leftrightarrow \neg 2 ∥ N)$

Metamath Proof Explorer

Theorem mod2eq1n2dvds

Proof