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 N N mod 2 = 1 ¬ 2 N

Proof

Step Hyp Ref Expression
1 zeo N N 2 N + 1 2
2 zre N N
3 2rp 2 +
4 mod0 N 2 + N mod 2 = 0 N 2
5 2 3 4 sylancl N N mod 2 = 0 N 2
6 5 biimpar N N 2 N mod 2 = 0
7 eqeq1 N mod 2 = 0 N mod 2 = 1 0 = 1
8 0ne1 0 1
9 eqneqall 0 = 1 0 1 n 2 n + 1 = N
10 8 9 mpi 0 = 1 n 2 n + 1 = N
11 7 10 syl6bi N mod 2 = 0 N mod 2 = 1 n 2 n + 1 = N
12 6 11 syl N N 2 N mod 2 = 1 n 2 n + 1 = N
13 12 expcom N 2 N N mod 2 = 1 n 2 n + 1 = N
14 peano2zm N + 1 2 N + 1 2 1
15 zcn N N
16 xp1d2m1eqxm1d2 N N + 1 2 1 = N 1 2
17 15 16 syl N N + 1 2 1 = N 1 2
18 17 eleq1d N N + 1 2 1 N 1 2
19 18 biimpd N N + 1 2 1 N 1 2
20 14 19 mpan9 N + 1 2 N N 1 2
21 oveq2 n = N 1 2 2 n = 2 N 1 2
22 21 adantl N + 1 2 N n = N 1 2 2 n = 2 N 1 2
23 22 oveq1d N + 1 2 N n = N 1 2 2 n + 1 = 2 N 1 2 + 1
24 peano2zm N N 1
25 24 zcnd N N 1
26 2cnd N 2
27 2ne0 2 0
28 27 a1i N 2 0
29 25 26 28 divcan2d N 2 N 1 2 = N 1
30 29 oveq1d N 2 N 1 2 + 1 = N - 1 + 1
31 npcan1 N N - 1 + 1 = N
32 15 31 syl N N - 1 + 1 = N
33 30 32 eqtrd N 2 N 1 2 + 1 = N
34 33 ad2antlr N + 1 2 N n = N 1 2 2 N 1 2 + 1 = N
35 23 34 eqtrd N + 1 2 N n = N 1 2 2 n + 1 = N
36 20 35 rspcedeq1vd N + 1 2 N n 2 n + 1 = N
37 36 a1d N + 1 2 N N mod 2 = 1 n 2 n + 1 = N
38 37 ex N + 1 2 N N mod 2 = 1 n 2 n + 1 = N
39 13 38 jaoi N 2 N + 1 2 N N mod 2 = 1 n 2 n + 1 = N
40 1 39 mpcom N N mod 2 = 1 n 2 n + 1 = N
41 oveq1 N = 2 n + 1 N mod 2 = 2 n + 1 mod 2
42 41 eqcoms 2 n + 1 = N N mod 2 = 2 n + 1 mod 2
43 2cnd n 2
44 zcn n n
45 43 44 mulcomd n 2 n = n 2
46 45 oveq1d n 2 n mod 2 = n 2 mod 2
47 mulmod0 n 2 + n 2 mod 2 = 0
48 3 47 mpan2 n n 2 mod 2 = 0
49 46 48 eqtrd n 2 n mod 2 = 0
50 49 oveq1d n 2 n mod 2 + 1 = 0 + 1
51 0p1e1 0 + 1 = 1
52 50 51 eqtrdi n 2 n mod 2 + 1 = 1
53 52 oveq1d n 2 n mod 2 + 1 mod 2 = 1 mod 2
54 2z 2
55 54 a1i n 2
56 id n n
57 55 56 zmulcld n 2 n
58 57 zred n 2 n
59 1red n 1
60 3 a1i n 2 +
61 modaddmod 2 n 1 2 + 2 n mod 2 + 1 mod 2 = 2 n + 1 mod 2
62 58 59 60 61 syl3anc n 2 n mod 2 + 1 mod 2 = 2 n + 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 n 1 mod 2 = 1
68 53 62 67 3eqtr3d n 2 n + 1 mod 2 = 1
69 68 adantl N n 2 n + 1 mod 2 = 1
70 42 69 sylan9eqr N n 2 n + 1 = N N mod 2 = 1
71 70 rexlimdva2 N n 2 n + 1 = N N mod 2 = 1
72 40 71 impbid N N mod 2 = 1 n 2 n + 1 = N
73 odd2np1 N ¬ 2 N n 2 n + 1 = N
74 72 73 bitr4d N N mod 2 = 1 ¬ 2 N