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

Proof

Step Hyp Ref Expression
1 zeo NN2N+12
2 zre NN
3 2rp 2+
4 mod0 N2+Nmod2=0N2
5 2 3 4 sylancl NNmod2=0N2
6 5 biimpar NN2Nmod2=0
7 eqeq1 Nmod2=0Nmod2=10=1
8 0ne1 01
9 eqneqall 0=101n2n+1=N
10 8 9 mpi 0=1n2n+1=N
11 7 10 syl6bi Nmod2=0Nmod2=1n2n+1=N
12 6 11 syl NN2Nmod2=1n2n+1=N
13 12 expcom N2NNmod2=1n2n+1=N
14 peano2zm N+12N+121
15 zcn NN
16 xp1d2m1eqxm1d2 NN+121=N12
17 15 16 syl NN+121=N12
18 17 eleq1d NN+121N12
19 18 biimpd NN+121N12
20 14 19 mpan9 N+12NN12
21 oveq2 n=N122n=2N12
22 21 adantl N+12Nn=N122n=2N12
23 22 oveq1d N+12Nn=N122n+1=2N12+1
24 peano2zm NN1
25 24 zcnd NN1
26 2cnd N2
27 2ne0 20
28 27 a1i N20
29 25 26 28 divcan2d N2N12=N1
30 29 oveq1d N2N12+1=N-1+1
31 npcan1 NN-1+1=N
32 15 31 syl NN-1+1=N
33 30 32 eqtrd N2N12+1=N
34 33 ad2antlr N+12Nn=N122N12+1=N
35 23 34 eqtrd N+12Nn=N122n+1=N
36 20 35 rspcedeq1vd N+12Nn2n+1=N
37 36 a1d N+12NNmod2=1n2n+1=N
38 37 ex N+12NNmod2=1n2n+1=N
39 13 38 jaoi N2N+12NNmod2=1n2n+1=N
40 1 39 mpcom NNmod2=1n2n+1=N
41 oveq1 N=2n+1Nmod2=2n+1mod2
42 41 eqcoms 2n+1=NNmod2=2n+1mod2
43 2cnd n2
44 zcn nn
45 43 44 mulcomd n2n=n2
46 45 oveq1d n2nmod2=n2mod2
47 mulmod0 n2+n2mod2=0
48 3 47 mpan2 nn2mod2=0
49 46 48 eqtrd n2nmod2=0
50 49 oveq1d n2nmod2+1=0+1
51 0p1e1 0+1=1
52 50 51 eqtrdi n2nmod2+1=1
53 52 oveq1d n2nmod2+1mod2=1mod2
54 2z 2
55 54 a1i n2
56 id nn
57 55 56 zmulcld n2n
58 57 zred n2n
59 1red n1
60 3 a1i n2+
61 modaddmod 2n12+2nmod2+1mod2=2n+1mod2
62 58 59 60 61 syl3anc n2nmod2+1mod2=2n+1mod2
63 2re 2
64 1lt2 1<2
65 63 64 pm3.2i 21<2
66 1mod 21<21mod2=1
67 65 66 mp1i n1mod2=1
68 53 62 67 3eqtr3d n2n+1mod2=1
69 68 adantl Nn2n+1mod2=1
70 42 69 sylan9eqr Nn2n+1=NNmod2=1
71 70 rexlimdva2 Nn2n+1=NNmod2=1
72 40 71 impbid NNmod2=1n2n+1=N
73 odd2np1 N¬2Nn2n+1=N
74 72 73 bitr4d NNmod2=1¬2N