Metamath Proof Explorer

Theorem zneo

Description: No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of Apostol p. 28. (Contributed by NM, 31-Jul-2004) (Proof shortened by Mario Carneiro, 18-May-2014)

Ref Expression
Assertion zneo 
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( 2 x. A ) =/= ( ( 2 x. B ) + 1 ) )

Proof

Step Hyp Ref Expression
1 halfnz 
 |-  -. ( 1 / 2 ) e. ZZ
2 2cn 
 |-  2 e. CC
3 zcn 
 |-  ( A e. ZZ -> A e. CC )
4 3 adantr 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> A e. CC )
5 mulcl 
 |-  ( ( 2 e. CC /\ A e. CC ) -> ( 2 x. A ) e. CC )
6 2 4 5 sylancr 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( 2 x. A ) e. CC )
7 zcn 
 |-  ( B e. ZZ -> B e. CC )
8 7 adantl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> B e. CC )
9 mulcl 
 |-  ( ( 2 e. CC /\ B e. CC ) -> ( 2 x. B ) e. CC )
10 2 8 9 sylancr 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( 2 x. B ) e. CC )
11 1cnd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> 1 e. CC )
12 6 10 11 subaddd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( ( 2 x. A ) - ( 2 x. B ) ) = 1 <-> ( ( 2 x. B ) + 1 ) = ( 2 x. A ) ) )
13 2 a1i 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> 2 e. CC )
14 13 4 8 subdid 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( 2 x. ( A - B ) ) = ( ( 2 x. A ) - ( 2 x. B ) ) )
15 14 oveq1d 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( 2 x. ( A - B ) ) / 2 ) = ( ( ( 2 x. A ) - ( 2 x. B ) ) / 2 ) )
16 zsubcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A - B ) e. ZZ )
17 zcn 
 |-  ( ( A - B ) e. ZZ -> ( A - B ) e. CC )
18 16 17 syl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A - B ) e. CC )
19 2ne0 
 |-  2 =/= 0
20 19 a1i 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> 2 =/= 0 )
21 18 13 20 divcan3d 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( 2 x. ( A - B ) ) / 2 ) = ( A - B ) )
22 15 21 eqtr3d 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( ( 2 x. A ) - ( 2 x. B ) ) / 2 ) = ( A - B ) )
23 22 16 eqeltrd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( ( 2 x. A ) - ( 2 x. B ) ) / 2 ) e. ZZ )
24 oveq1 
 |-  ( ( ( 2 x. A ) - ( 2 x. B ) ) = 1 -> ( ( ( 2 x. A ) - ( 2 x. B ) ) / 2 ) = ( 1 / 2 ) )
25 24 eleq1d 
 |-  ( ( ( 2 x. A ) - ( 2 x. B ) ) = 1 -> ( ( ( ( 2 x. A ) - ( 2 x. B ) ) / 2 ) e. ZZ <-> ( 1 / 2 ) e. ZZ ) )
26 23 25 syl5ibcom 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( ( 2 x. A ) - ( 2 x. B ) ) = 1 -> ( 1 / 2 ) e. ZZ ) )
27 12 26 sylbird 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( ( 2 x. B ) + 1 ) = ( 2 x. A ) -> ( 1 / 2 ) e. ZZ ) )
28 27 necon3bd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( -. ( 1 / 2 ) e. ZZ -> ( ( 2 x. B ) + 1 ) =/= ( 2 x. A ) ) )
29 1 28 mpi 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( 2 x. B ) + 1 ) =/= ( 2 x. A ) )
30 29 necomd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( 2 x. A ) =/= ( ( 2 x. B ) + 1 ) )