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 e. ZZ -> ( ( N mod 2 ) = 1 <-> -. 2 || N ) )

Proof

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