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 ) )