Metamath Proof Explorer

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 syl6bi ⊢ ( ( 𝑁 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 ∥ 𝑁 ) )