Theorem 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	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 mod 2 ) = 1 ↔ ¬ 2 ∥ 𝑁 ) )

Proof

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