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